Email Gateway (Aug 22 2022 at 09:08): Email Gateway (Aug 22 2022 at 09:08):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Isar experts,
In interpretation and sublocale statements, the generated abbreviation ?thesis contains an
additional Pure.prop . Unfortunately, this marker renders ?thesis unusable for show
statements.
Here's a minimal example:
locale l = fixes x assumes "x = x"
interpretation l "Suc 0"
proof -
(* ?thesis here is "Pure.prop (HOL.Trueprop (l (Suc 0)))" *)
show "PROP ?thesis" (* does not work -> failed to refine any pending goal *)
show "Trueprop (l (Suc 0))" (* works *)
Why do interpretation and sublocale statements add this Pure.prop marker to ?thesis? And
what is Pure.prop needed for at all?
Best,
Andreas
Email Gateway (Aug 22 2022 at 09:11):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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.
Florian
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
Email Gateway (Aug 22 2022 at 09:11):From: Makarius <makarius@sketis.net>
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.
Makarius
Email Gateway (Aug 22 2022 at 09:41):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,
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.
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
signature.asc
Last updated: Apr 25 2024 at 20:15 UTC