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



Hi Clemens,

Unfortunately this also does not show any effect.

Regards,
Norbert

--

Norbert Schirmer (nschirmer at apple.com)
 SEG Formal Verification



On 20. Sep 2021, at 20:19, Clemens Ballarin <ballarin at in.tum.de> wrote:

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


On 2021-09-17 15:29, Norbert Schirmer via Cl-isabelle-users wrote:
Hi,
When using Interpretation.interpretation within Isabelle/ML the
declarations of the interpreted locale are surprisingly not activated.
I attempt to accumulate some facts in named theorems that come from
the interpretation.
In Isar it reads and works perfectly fine as follows:
named_theorems
my_rules
locale nonzero =
fixes n::nat
assumes non_zero: "0 < n"
begin
lemma le [my_rules]: "Suc 0 < Suc n"
by (simp add: non_zero)
thm my_rules ―‹Suc 0 < Suc n›
end
thm my_rules ―‹empty›
locale foo =
fixes m::nat
assumes m[simp]: "m = Suc (Suc 0)"
begin
thm my_rules ―‹empty›
interpretation two: nonzero where n=m
by (unfold_locales) simp
thm two.le
thm my_rules ―‹@{term ‹Suc 0 < Suc m›}›
interpretation one: nonzero where n="Suc 0"
by (unfold_locales) simp
thm my_rules ―‹@{term ‹Suc 0 < Suc m›}, @{term ‹Suc 0 < Suc (Suc 0)›}›
thm one.le
thm two.le
end
=================================
I expected the same to happen in Isabelle/ML using
Interpretation.interpretation.
However there is no effect on my_rules
ML ‹
val expr_one = ([(@{locale "nonzero"}, (("one", true),
         (_expression_.Positional ([SOME @{term "Suc 0"}]), [])))], [])

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} ―‹[]›

end
ML_val ‹
val lthy =
@{theory}
|> Named_Target.init [] @{locale foo}
|> 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}

Any suggestions on how to approach this in Isabelle/ML?
Find the source and some more examples in the attachment.
Regards,
Norbert
--
Norbert Schirmer (nschirmer at apple.com <mailto:nschirmer at apple.com>)
 SEG Formal Verification
Regards,
Norbert
--
Norbert Schirmer (nschirmer at apple.com)
 SEG Formal Verification



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