*To*: Søren Haagerup <shaagerup at gmail.com>*Subject*: Re: [isabelle] Converting apply-style induction to Structured Isar*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Thu, 31 Mar 2011 14:28:55 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <AANLkTimFPW2Lvvm3Pa6M9ybLRWEmu_SvAvqjjOFv=oP0@mail.gmail.com>*Organization*: Technische Universität München*References*: <AANLkTimFPW2Lvvm3Pa6M9ybLRWEmu_SvAvqjjOFv=oP0@mail.gmail.com>

Am Donnerstag, den 31.03.2011, 13:29 +0200 schrieb Søren Haagerup: > Hello, > > I have a hard time going from Apply-style induction proofs to the > Structured Isar-style. > > In the apply-style case, the proof of "cata_uniq" is a mere 4 lines: > http://gawis.dk/misc/apply_sample.thy > > In the structured style, I need to write much more: > http://gawis.dk/misc/structured_sample.thy - Do not add catafunc_def, this is the wrong simp rule. The rules catafunc.simps are automatically added to the simpset by primrec. This also adds the rules for "app" to the simp set, which is the inverse of cata_rewrite, and hence when you add cata_rewrite without removing app.simps, like "simp add: cata_rewrite" the simplifier does not terminate. Instead use "simp add: cata_rewrite del: app.simps" - You cata_helper lemma is always a good idea to add. Probably named added to the simplifier. However adding rules to the automatization needs some experience, but you should try to play with it. (they also look like nice dest rules) - The "case" command lets you specify the fixed variables no need to add "fix" and "assume". - If you use "case" with the method "induct" the thesis is not named ?thesis but ?case, the facts are named after the case name (look at Isabelle / Show me / Facts) : proof (induct c) case (Cons1 a b c) then show ?case ... next case (Cons2 a b c) then show ?case ... qed - In your structured cata_uniq you do not need the additional show "" proof - ... qed command. - My solution would be: lemma cata_uniq: "cata c f b ==> c as = catafunc f b as" proof (induct as) case (Snoc as a) then have "c (app as (Singleton a)) = b (catafunc f b as) (f a)" by (simp_all add: cata_def del: app.simps) then show ?case by simp qed (simp add: cata_def) (** the method supplied to "qed" is applied to the remaining goals. Here it is the Singleton case. **) - Another possible solution would be: lemma cata_uniq: "cata c f b ==> c as = catafunc f b as" proof (induct as) case (Snoc as a) then show ?case by (simp add: cata_def cons_rewrite del: app.simps) simp qed (simp add: cata_def) This is shorted but probably not as readable and stable as the previous proof. The lines by (simp add: cata_def cons_rewrite del: app.simps) simp are the same as proof (simp add: cata_def cons_rewrite del: app.simps) qed simp Hope this helps, Johannes > Is there a way to make a concise structured proof of this fact? > > Best regards, > Søren

**Follow-Ups**:**Re: [isabelle] Converting apply-style induction to Structured Isar***From:*Søren Haagerup

**References**:**[isabelle] Converting apply-style induction to Structured Isar***From:*Søren Haagerup

- Previous by Date: Re: [isabelle] Converting apply-style induction to Structured Isar
- Next by Date: Re: [isabelle] Converting apply-style induction to Structured Isar
- Previous by Thread: Re: [isabelle] Converting apply-style induction to Structured Isar
- Next by Thread: Re: [isabelle] Converting apply-style induction to Structured Isar
- Cl-isabelle-users March 2011 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