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



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.