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
qed simp

Tobias

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
> 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?
> 
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.