theory BinaryTree imports ToyList begin datatype 'a tree = Tip | Node "'a tree" 'a "'a tree" term "Tip" term "Node Tip True Tip" term "Node Tip x Tip" term "Node xs x xs" primrec mirror :: "'a tree => 'a tree" where "mirror (Tip) = Tip"| "mirror (Node xs x ys) = Node (mirror ys) x (mirror xs)" value "mirror(Node Tip True Tip)" value "mirror(Node (Node Tip True Tip) False (Node Tip False Tip))" lemma mirror_mirror: "mirror(mirror t) = t" apply(induct_tac t) apply(auto) done primrec flatten :: "'a tree => 'a list" where "flatten (Tip) = []"| "flatten (Node xs x ys) = (flatten xs) @ (x#flatten ys)" value "(flatten (Node Tip True Tip))" lemma flatten_mirror: "flatten(mirror t) = rev(flatten t)" apply(induct_tac t) apply(auto) done value "flatten(Node (Node Tip False Tip) True Tip)" value "flatten(mirror(Node (Node Tip False Tip) True Tip))" value "rev(flatten(Node (Node Tip False Tip) True Tip))" value "flatten(Node (Node Tip False Tip) True Tip)" value "flatten(mirror(Node (Node Tip False Tip) True Tip))" value "rev(flatten(Node (Node Tip False Tip) True Tip))" primrec flatten2 :: "'a tree \ 'a list \ 'a list" where "flatten2 Tip xl = xl"| "flatten2 (Node xs x ys) xl = flatten2 xs (x#flatten2 ys xl)" value "flatten(Node (Node Tip False Tip) True Tip)" value "flatten2 (Node (Node Tip False Tip) True Tip) []" value "flatten(mirror(Node (Node Tip False Tip) True Tip))" value "flatten2 (mirror(Node (Node Tip False Tip) True Tip)) []" lemma "flatten2 t [] = flatten t" apply(induct_tac t, simp_all) oops lemma "flatten2 t ys = flatten t @ ys" apply(induct_tac t, simp_all) oops lemma flatten2general: "\ ys. flatten2 t ys = flatten t @ ys" apply(induct_tac t, simp_all) done thm flatten2general lemma "flatten2 t [] = flatten t" by (simp add: flatten2general) lemma "itrev xs [] = rev xs" apply(induct_tac xs, simp_all) oops --"Generalize goals for induction by replacing constants,here [] by variables" lemma "itrev xs ys = rev xs @ ys" apply(induct_tac xs, simp_all) oops --"Induction hypothesis is still too weak beacause ys is fixed" lemma "\ ys. itrev xs ys = rev xs @ ys" apply(induct_tac xs, simp_all) done --"Generalize goals for induction by universally quantifying all free variables (except the induction variable itself)" end