Re: [isabelle] Declarations not activated by Interpretation.interpretation

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))),
> <>_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.


Attachment: OpenPGP_signature
Description: OpenPGP digital signature

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