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

On Tue, 14 Apr 2015, Florian Haftmann wrote:

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 =
  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 vaguely remember discussions about this problem with Clemens Ballarin, back to 2005 at the least. The use of the Pure.prop marker is canonical to avoid fragile tools using variations of old "COMP" (which are still not as forgotten as they deserve).

I can't say on the spot, if it can be made more smooth to end-users. This approach is already there for several years, i.e. not a regression. I have ticket the thread as "important", but the normal release schedule takes priority at the moment.


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