*To*: Søren Haagerup <shaagerup at gmail.com>*Subject*: Re: [isabelle] Converting apply-style induction to Structured Isar*From*: Christian Urban <urbanc at in.tum.de>*Date*: Thu, 31 Mar 2011 15:03:28 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <AANLkTimFPW2Lvvm3Pa6M9ybLRWEmu_SvAvqjjOFv=oP0@mail.gmail.com>*References*: <AANLkTimFPW2Lvvm3Pa6M9ybLRWEmu_SvAvqjjOFv=oP0@mail.gmail.com>*User-agent*: Internet Messaging Program (IMP) H3 (4.3.8)

Quoting Søren Haagerup <shaagerup at gmail.com>:

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 Is there a way to make a concise structured proof of this fact?

Well, you have to keep in mind that a 'good' Isar proof conveys more information than an apply-script. In a 'good' Isar proof you should be able to easily read off the proof idea. This means in practice that an Isar proof is sometimes a bit more verbose. However looking at your proof, I would formulate it as follows. lemma cata_uniq : assumes a: "cata c f b" shows "c as = catafunc f b as" proof (induct as) case (Singleton a) show "c (Singleton a) = catafunc f b (Singleton a)" using a by (simp add: catafunc_def cata_def) next case (Snoc as a) have hyp: "c as = catafunc f b as" by fact

also have "... = b (c as) (f a)"

also have "... = b (catafunc f b as) (f a)" using hyp by auto finally show "c (Snoc as a) = catafunc f b (Snoc as a)" by simp qed

lemma cata_uniq : assumes a: "cata c f b" shows "c as = catafunc f b as" proof (induct as) case (Snoc as a) have hyp: "c as = catafunc f b as" by fact have "c (Snoc as a) = c (app as (Singleton a))" by (simp only: cons_rewrite) also have "... = b (c as) (f a)"

also have "... = b (catafunc f b as) (f a)" using hyp by auto finally show "c (Snoc as a) = catafunc f b (Snoc as a)" by simp qed (simp add: a[unfolded cata_def]) OK, this is not as short as your apply-script and the two solutions, but as said above the purpose of an Isar proof is not to be as concise as an apply-script, but to easily read off the proof idea (your calculation). This might mean in this case that the proof is a bit more verbose (but this is not always the case).

I have a hard time going from Apply-style induction proofs to the Structured Isar-style.

My experience is also that going from an apply script to an Isar proof is not that easy. Fiddling with an apply script usually completely buries the proof idea. Constructing then the corresponding Isar proof means that one has to think again about what are the important steps in the proof are. That can sometimes be non-obvious. Hope this helps, Christian

**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: [isabelle] Pairs/tuples
- 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