[isabelle] Declarations not activated by Interpretation.interpretation



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_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_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)
 SEG Formal Verification
Regards,
Norbert

--

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

Attachment: Interpretation_Ex.thy
Description: Binary data




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