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



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>

- that the use of insert in this way be blessed with some outer syntax.

Best of luck with the IDE issues. :-)

cheers
peter




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