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


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
  case (Snoc as a)
  thus ?case
    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 :)


Rafal Kolanski.

On 31/03/11 22:29, Søren Haagerup wrote:

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:

In the structured style, I need to write much more:

Is there a way to make a concise structured proof of this fact?

Best regards,

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