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)
next
  case (Snoc as a)
  from assms show ?case
    by (simp only: Snoc cata_def cons_rewrite) simp
qed

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.

cheers

chris

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