[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:

theory EvenDouble
imports Main
begin

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
   
end

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 MHonArc.