[isabelle] chaining facts into the terminal method after "qed"



Hi,

I have an induction of this form:

datatype D = a | b | c | d

lemma
  assumes A: "A"
  assumes B: "B (x :: D)"
  shows "C x"
using B
proof(induct x)
  case a with A show ?case sorry (* non trivial *)
next
  case b with A show ?case sorry (* trivial *)
next
  case c with A show ?case sorry (* trivial *)
next
  case d with A show ?case sorry (* trivial *)
qed

I would like to write this instead:

lemma
  assumes A: "A"
  assumes B: "B (x :: D)"
  shows "C x"
using B
proof(induct x)
  case a with A show ?case sorry (* non trivial *)
qed using A by ...

I have fudged this in the past by using the "insert" method:

...
qed (insert A, ...)

Would it be possible to generalise what's allowed after "qed"?

Logically I could chain A into the induction too, but this obfuscates the induction hypothesis.

cheers
peter

-- 
http://peteg.org/






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