tutorial.thy

Tutorial

theory ToyList
imports Datatype
begin

datatype 'a list = Nil ("[]")
| Cons 'a "'a list"    (infixr "#" 65)

(* This is append function: *)
primrec app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65)
where
"[] @ ys      = ys" |
"(x # xs) @ ys = x # (xs @ ys)"

primrec rev :: "'a list \<Rightarrow> 'a list" where
"rev []       = []" |
"rev (Cons x xs) = (rev xs) @ (x # [])"

value "rev (a # b # c # [])"

lemma app_Nil2 [simp]: "xs @ [] = xs"
apply (induct_tac xs)
apply (auto)
done

lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
apply (induct_tac xs)
apply (auto)
done

lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
apply (induct_tac xs)
apply (auto)
done

theorem rev_rev [simp]: "rev(rev xs) = xs"
apply (induct_tac xs)
apply (auto)
done

datatype 'a tree =
Tip
| Node "'a tree" 'a "'a tree"

primrec mirror :: "'a tree \<Rightarrow> 'a tree"
where
"mirror Tip = Tip" |
"mirror (Node ls x rs) = (Node (mirror rs) x (mirror ls))"

lemma mirror_mirror : "mirror(mirror t) = t"
apply (induct_tac t)
apply (auto)
done

value "length (a # b # c # [])"

value "Node a b c"

primrec flatten :: "'a tree \<Rightarrow> 'a list"
where
"flatten Tip = Nil" |
"flatten (Node ls x rs) = (flatten ls) @ (x # []) @ (flatten rs)"

lemma flatten_mirror [simp] : "flatten(mirror t) = rev (flatten t)"
apply (induct_tac t)
apply (auto)
done


(* 2.5.6 *)
datatype boolex = Const bool | Var nat | Neg boolex
|And boolex boolex

primrec "value" :: "boolex \<Rightarrow> (nat \<Rightarrow> bool ) \<Rightarrow> bool "
where
"value (Const b) env = b" |
"value (Var x)   env = env x" |
"value (Neg b)   env = (~ value b env)" |
"value (And b c) env = (value b env \<and> value c env)"

end