Up to index of Isabelle/HOL/IsarTut

theory Mirrors = Main: text {* Solution to exercise 2.4.1. I'm not at all sure why the first few proofs in the ToyList theory went through without ``from prems'' but these both seem to need that clause. Go figure. *} datatype 'a tree = Tip | Node "'a tree" 'a "'a tree" consts mirror :: "'a tree => 'a tree" primrec "mirror Tip = Tip" "mirror (Node l a r) = Node (mirror r) a (mirror l)" lemma mirror_mirror: "mirror(mirror t) = t" (is "?mm t") proof (induct t) show "?mm Tip" by simp next fix l a r assume "?mm l" "?mm r" from prems show "?mm (Node l a r)" by simp qed consts flatten:: "'a tree => 'a list" primrec "flatten Tip = []" "flatten (Node l a r) = (flatten l)@[a]@(flatten r)" lemma "flatten(mirror t) = rev(flatten t)" (is "?P t") proof (induct t) show "?P Tip" by simp next fix l a r assume "?P l" "?P r" from prems show "?P (Node l a r)" by simp qed end

**lemma** *mirror_mirror:*

mirror (mirror t) = t

**lemma**

flatten (mirror t) = rev (flatten t)