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

How about

lemma cata_uniq:
  assumes "cata c f b"
  shows "c as = catafunc f b as"
proof (induct as)
  case (Singleton a)
  from assms show ?case
    by (simp add: catafunc_def cata_def)
  case (Snoc as a)
  from assms show ?case
    by (simp only: Snoc cata_def cons_rewrite) simp

The fact that I need to split the final step into 2 parts (one only using cons_rewrite cata_def and the induction hypothesis, and the other using all the simplification rules that are around) indicates that some of your equations may be oriented in the wrong direction (without the split, the simplifier loops). But I didn't have closer look. Another thing that I find strange in your original proof is the use of catafunc_def which was defined via "fun" an hence provides simplification rules catafunc.simps.

A few words on the above proof: Fixing local variables and stating assumptions (e.g., the IH) is done automatically when using "case", e.g.,

  case (Snoc as a)

is a kind of abbreviation for

  fix as a
  assume "c as = catafunc f b as"

I hope this helps.



On 03/31/2011 01:29 PM, 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.