Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Declarations not activated byInterpretation.i...


view this post on Zulip Email Gateway (Sep 17 2021 at 13:29):

From: Norbert Schirmer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
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@apple.com <mailto:nschirmer@apple.com>)
 SEG Formal Verification
Regards,
Norbert

--

Norbert Schirmer (nschirmer@apple.com)
 SEG Formal Verification
Interpretation_Ex.thy


Last updated: Mar 29 2024 at 08:18 UTC