[isabelle] Using Isar on Induction
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:
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
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?
Aaron W. Hsu | arcfide at sacrideo.us | http://www.sacrideo.us
Programming is just another word for the lost art of thinking.
This archive was generated by a fusion of
Pipermail (Mailman edition) and