Re: [isabelle] Using Isar on Induction

Instead of "by (simp only: dd) simp", try "unfolding dd by simp".

The "unfolding" command will do rewriting on the goal and in the
chained facts, but unlike "apply simp" it leaves the chained facts as
chained facts.

- Brian

On Sun, Apr 29, 2012 at 5:46 AM, Aaron W. Hsu <arcfide at> wrote:
> 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 |
> Programming is just another word for the lost art of thinking.

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