# [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.