Up to index of Isabelle/HOL/IsarTut

theory Induction = Main + Mirrors: text {* Beginning section 3.2. I'm including Mirrors so I don't have to retype the background definitions for the exercise. *} consts itrev :: "'a list => 'a list => 'a list" primrec "itrev [] ys = ys" "itrev (x#xs) ys = itrev xs (x#ys)" text {* Let's do this proof by proving the stronger inductive result as an embedded lemma: *} lemma "itrev xs [] = rev xs" proof - have "!ys. itrev xs ys = (rev xs) @ ys" by (induct xs, auto) thus ?thesis by simp qed text {* The only really tricky part about that was to remember to put in the quatifier on ys. Note that Isabelle required it as well. Exercise 3.2.1 *} consts flatten2:: "'a tree => 'a list => 'a list" text {* Since the list constructor works right-to-left we need to do a right-to-left in-order traversal. *} primrec "flatten2 Tip acc = acc" "flatten2 (Node l a r) acc = flatten2 l (a # (flatten2 r acc))" text {* Now it gets interesting. This is where I started to get irritated with Isabelle proof scripts, though I see now that it isn't really all that bad if you ask the question in the right way: *} theorem "!acc. flatten2 t acc = (flatten t)@acc" apply (induct_tac t, auto) done text {* So let's do a pretty Isar proof: *} theorem "flatten2 t [] = flatten t" proof - have "!acc. flatten2 t acc = (flatten t)@acc" by (induct t, auto) thus ?thesis by simp qed end

**lemma**

itrev xs [] = rev xs

**theorem**

ALL acc. flatten2 t acc = flatten t @ acc

**theorem**

flatten2 t [] = flatten t