Theory Induction

Up to index of Isabelle/HOL/IsarTut

theory Induction = Main + Mirrors:
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