*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Using Isar on Induction*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sun, 29 Apr 2012 18:39:53 +0200*In-reply-to*: <jnidic$48m$1@dough.gmane.org>*References*: <jnidic$48m$1@dough.gmane.org>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:11.0) Gecko/20120327 Thunderbird/11.0.1

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

**Follow-Ups**:**Re: [isabelle] Using Isar on Induction***From:*Aaron W. Hsu

**References**:**[isabelle] Using Isar on Induction***From:*Aaron W. Hsu

- Previous by Date: Re: [isabelle] Document Typesetting
- Next by Date: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Previous by Thread: Re: [isabelle] Using Isar on Induction
- Next by Thread: Re: [isabelle] Using Isar on Induction
- Cl-isabelle-users April 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list