Re: [isabelle] interpretation and sublocale add Pure.prop to ?thesis

> AFAIR in src/Pure/Isar/element.ML there some functions for ÂwitnessesÂ,
> i.e. hypotheses as protected facts which later on allow to instantiate
> facts accordingly during interpretation.  These use Pure.prop to protect
> their propositions internally.

After a second inspection, the story seems to be quite obvious:

in src/Pure/element.ML, find

> val refine_witness =
>   Proof.refine (Method.Basic (fn ctxt => EMPTY_CASES o
>     K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (resolve_tac ctxt [Drule.protectI]))))))));

> fun gen_witness_proof proof after_qed wit_propss eq_props =
>   let
>     â
>   in proof after_qed' propss #> refine_witness #> Seq.hd end;

i.e. the initial proof goal (?thesis) is, in most practical cases,
immediately refined by Drule.protectI, and the goal left afterwards does
not match ?thesis any longer.

There have been substantial reasons why witnesses are protected by
Pure.prop, but this is beyond my historic memory.

No line in this code goes back beyond Jan. 2009, but at that time the
whole locale machinery was reimplemented, but the witness business
remained the same, undergoing some iterations of polishing.


> I do not know whether this can be lifted somehow, but I guess not.
> This is a very technical detail of the locale implementation indeed.
> 	Florian


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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