Re: [isabelle] Converting apply-style induction to Structured Isar
- To: Søren Haagerup <shaagerup at gmail.com>
- Subject: Re: [isabelle] Converting apply-style induction to Structured Isar
- From: Rafal Kolanski <rafalk at cse.unsw.edu.au>
- Date: Fri, 01 Apr 2011 10:09:33 +1100
- 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: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:220.127.116.11) Gecko/20110223 Thunderbird/3.1.8
While drinking tea, I took a quick stab at it too, here's what I ended
lemma cata_uniq2: "cata c f b ==> c as = catafunc f b as"
proof (induct as)
case (Singleton a) thus ?case by simp
case (Snoc as a)
by (subst catafunc.simps)
(simp add: cons_rewrite del: app.simps)
The "cons_rewrite" lemma is in direct conflict with app.simps, so they
can't both be in the simpset at the same time.
If you repeatedly run into this type of conflict, you might want to
remove the function equations from the simpset using:
declare app.simps[simp del]
Then you can always add them back in to the simplifier when needed.
By now, you should have a nice collection of various people's proving
styles in Isar :)
On 31/03/11 22:29, Søren Haagerup wrote:
I have a hard time going from Apply-style induction proofs to the
In the apply-style case, the proof of "cata_uniq" is a mere 4 lines:
In the structured style, I need to write much more:
Is there a way to make a concise structured proof of this fact?
This archive was generated by a fusion of
Pipermail (Mailman edition) and