Email Gateway (Aug 18 2022 at 18:54): Email Gateway (Aug 18 2022 at 18:54):From: Makarius <makarius@sketis.net>
"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
Email Gateway (Aug 18 2022 at 18:54):From: Peter Gammie <peteg42@gmail.com>
Makarius,
On 06/01/2012, at 11:08 PM, Makarius wrote:
"Fudge" seems to be a recent slang word that I do quite understand, or is this North American?
It might be. I don't think it's recent.
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.
I understand, but my point is that Isar allows me to name a fact but does not let me use it in a context where I need to - forcing me to employ the otherwise useless "insert" tactic. (In other contexts one can say "using ...", or appeal to the more powerful cut_tac if necessary.) This makes me think some outer syntax is missing.
I was vaguely proposing that:
...
qed <terminal method>
be generalised to something like:
qed (using fact+)? <terminal method>
Best of luck with the IDE issues. :-)
cheers
peter
Email Gateway (Aug 18 2022 at 18:56):From: Peter Gammie <peteg42@gmail.com>
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
Last updated: Nov 21 2024 at 12:39 UTC