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



On Wed, 4 Jan 2012, Peter Gammie wrote:

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"?

"Fudge" seems to be a recent slang word that I do quite understand, or is this North American?


Concerning the meaning of the above, the concept of Isar facts vs. goal refinements are explained to some extent in section 6.2 of the implementation manual. Roughly you have something like this:

  <using facts>
  <goal>
  proof <initial method>
    <body>
  qed <terminal method>

The initial step (with the "using" part) is usually fully "structured" in the sense explained in section 6.2: methods like "rule" or "induct" take facts very seriously in what they do. Moving further towards the tail position, some structure is given up: the terminal method merely finishes what is left, usually using "simple methods" in the sense of 6.2, where facts are only inserted as "insert" does. (BTW, it is bad style to make a weakly structured initial method application -- simp, auto etc. -- and then try to proceed in a structured way towards the end.)

So the above use of qed "insert" is in accordance with the usual Isar style, even though complex method expressions at qed time tend to become slightly ugly.


For the special situation of induction, the general plan of action is to provide reasonably mechanisms for proof composition into the Prover IDE at some point. E.g. the cases would be spelt out explictly by the IDE, and the user gets a chance to expand the non-trivial ones or tweak the trivial ones, even if most of them happen to be almost the same. Once we are getting closer to this, one can revisit the old questions about effective composition and maintanence of big induction proofs, wrt. changes of the inductive specifications etc.

Here is a historically interesting example, which has defined the received Isar proof style to a large extent. At that point http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2002/src/HOL/Unix/Unix.thy#l425 all cases are expanded uniformaly -- and automatically benefit from independent failure reports and parallel evaluation (around 2008/2009). At some later stage one subproof was changed independently so we now see
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2011-1/src/HOL/Unix/Unix.thy#l425

This definitely shows some redundancy in the text, but postulating a decent Prover IDE it might actually work out in everyday hard work as well, without having to make tight "proof scripts" again.


	Makarius






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