Re: [isabelle] Using Isar on Induction
In general, if you want to show more steps of an equational proof, you can do so
via the "also/finally" elements:
theorem even_double: "evenb (double x 0)"
proof (induct x)
case (Suc x)
have "evenb (double (Suc x) 0) = evenb(Suc(Suc(double x 0)))"
by(simp only: dd)
also have "... = evenb(double x 0)" by(simp only: evenb.simps)
also have "... = True" by(simp add: Suc)
finally show ?case by simp
Am 29/04/2012 05:46, schrieb Aaron W. Hsu:
> I am a bit confused about using Isar on some simple inductions.
> Suppose that I have a proof that is nearly automatic except that I need
> to apply a single simplification first. Here's a small example:
> theory EvenDouble
> imports Main
> fun evenb :: "nat ⇒ bool" where
> "evenb 0 = True" |
> "evenb (Suc 0) = False" |
> "evenb (Suc (Suc n)) = evenb n"
> primrec double :: "nat ⇒ nat ⇒ nat" where
> "double 0 y = y" |
> "double (Suc x) y = double x (Suc (Suc y))"
> lemma dd: "double (Suc x) y = Suc (Suc (double x y))"
> by (induct x arbitrary: y) simp_all
> theorem even_double: "evenb (double x 0)"
> proof (induct x)
> case (Suc x) thus ?case by (simp only: dd) simp
> qed simp
> I do not like the proof of even_double because the whole point is to show
> the main critical step, and I feel like that is lost by just chaining a
> couple of methods together. However, being a total noob, I cannot see
> how to insert that intermediate simplification explicitly before showing
> the ?case. In particular, everything that I put between "thus ?case" and
> the "case" causes the induction hypothesis to be removed from my current
> facts, and I do not want to remove facts; I just want to show that single
> simplification and then use the facts later. How do I do this in Isar?
This archive was generated by a fusion of
Pipermail (Mailman edition) and