Re: [isabelle] Converting apply-style induction to Structured Isar



Hi,

While drinking tea, I took a quick stab at it too, here's what I ended up with:

lemma cata_uniq2: "cata c f b ==> c as = catafunc f b as"
  unfolding cata_def
proof (induct as)
  case (Singleton a) thus ?case by simp
next
  case (Snoc as a)
  thus ?case
    by (subst catafunc.simps)
       (simp add: cons_rewrite del: app.simps)
qed

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 :)

Sincerely,

Rafal Kolanski.


On 31/03/11 22:29, Søren Haagerup wrote:
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?

Best regards,
Søren





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.