Email Gateway (Sep 20 2021 at 18:19): Email Gateway (Sep 20 2021 at 18:19):From: Clemens Ballarin <ballarin@in.tum.de>
Hi Norbert,
There have been many refactorings since I've implemented this, so I
cannot tell you for sure. However, it seems to me that you should be
using 'isar_interpretation' rather than 'interpretation'.
Clemens
Email Gateway (Sep 20 2021 at 21:10):From: Norbert Schirmer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi Clemens,
Unfortunately this also does not show any effect.
Regards,
Norbert
Email Gateway (Sep 23 2021 at 13:46):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Norbert,
the issue is a little bit delicate.
First, to clarify the ML interfaces:
Interpretation.interpretation is for bounded interpretation within
context begin/end blocks.
Interpretation.isar_interpretation mimics the Isar keyword
»interpretation« which has a different meaning at the theory level.
Following »explicit is better than implict«,
Interpretation.interpretation seems the right thing for your application.
Now, the problem itself:
context foo
begin
ML_val ‹
val lthy =
@{context}
|> Interpretation.interpretation expr_one
|> Proof.global_terminal_proof ((Method.Basic (fn ctxt => SIMPLE_METHOD (
(Locale.intro_locales_tac {strict = false, eager = true} ctxt [] THEN
asm_full_simp_tac ctxt 1))), Position.no
<http://Position.no>_range), NONE)val thms = Named_Theorems.get lthy @{named_theorems my_rules} ―‹[]›
A second glimpse:
val thms = Named_Theorems.get (Local_Theory.target_of lthy)
@{named_theorems my_rules} ―‹[]›
What happens here? Declarations stemming from bounded interpretations
are »as it is by now« only applied in a target context, but never in
the »eigen context«. So far this has never raised any attention since
after each Isar interpretation, the target context is restored, any
obviously there haven’t been any programmatic applications of
interpretation in bounded contexts so far.
I deem the position in the code which is responsible for that glitch is
in generic_target.ML:
val local_interpretation = standard_registration (fn (n, level) => level
= n - 1);
The check is too strict: it should not only cover level = n - 1 (the
uppermost nested local theory) but level = n also (the eigen context).
I will have a look at this and see whether this suffices.
Cheers,
Florian
OpenPGP_signature
Email Gateway (Sep 29 2021 at 09:59):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Norbert,
see now https://isabelle.in.tum.de/repos/isabelle/rev/690928dd6f8f
It would also be possible to apply declarations it all levels of the
nested target, but at the moment I am reluctant to undertake such a
change in user-observable behaviour.
Florian
OpenPGP_signature
Email Gateway (Sep 29 2021 at 10:25):From: Makarius <makarius@sketis.net>
I have tried to track the emergence of the level "n - 1" / formerly map_top
and found this old changeset:
changeset: 52119:90ba620333d0
user: haftmann
date: Wed May 22 22:56:17 2013 +0200
files: src/Pure/Isar/expression.ML src/Pure/Isar/local_theory.ML
description:
interpretation must always operate on the last element in a local theory
stack, not on all elements: interpretated facts must disappear after pop from
local theory stack, and transfer from last target is not enough
The "must always" is not explained in the text; maybe you still remember the
reasons.
Makarius
Last updated: Jul 15 2022 at 23:21 UTC