# 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.*