Re: [isabelle] interpret/moreover/ultimately



On Fri, 9 Mar 2012, Brian Huffman wrote:

On Fri, Mar 9, 2012 at 2:04 PM, Christian Sternagel
<c-sterna at jaist.ac.jp> wrote:
Hi there,

recently I experienced some strange behavior (Isabelle2011-1 in jedit) which
is reproduced in the small example below:

notepad begin
 fix l le B
 interpret preorder l le sorry

At this point in your proof script, try

ML_val {* Thm.concl_of @{thm this} *}

and you will see that there is a constant "prop :: prop => prop"
wrapped around the conclusion of this fact, outside the "Trueprop".

Then try

ML_val {* Thm.concl_of @{thm `class.preorder l le`} *}

And you will see that no "prop" constant is there.

Perhaps Makarius can say more about what this "prop" constant is for, and why it appears in the theorem exported by the interpret command.

Locale interpretation essentially needs to discharge "hyps" from local theorems, by establishing a suitable "witness". To preserve the literal structure of the same, without the usual normalization of regular results, the internal goal statement is protected via the funny prop constant. (This device is explained in the Isar implementation manual section 2.3.2; it is useful for extraordinary situations in ML, but should normally never be encountered in end-user proof documents.)

The confusion above stems from the accident that 'interpret' exposes this internal result to the Isar proof context via "this". (I have gone through all reachable Isabelle example and found a few more such misunderstandings, where forward chaining was done after 'interpret' without any effect, and eliminated them.)


Note that after "interpret foobar" the context knows about the fact "foobar_axioms" in the proven instance; the same works for any other imported substructures, not just part that was visible in the auxiliary goal state.


	Makarius


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