Email Gateway (Aug 23 2022 at 08:22): Email Gateway (Aug 23 2022 at 08:22):From: Norbert Schirmer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle users,
When adding a theorem with a simp attribute via ‘Global_Theory.add_thm' within a local theory by ‘Local_Theory.background_theory’, I have the following surprising behaviour:
While the theorem can be retrieved by its name it is not added to the simplest of the resulting local theory. Only after reinitialising the local theory the theorem also appears in the simpset. Is this expected behaviour?
Further remarks:
The following ML code snippet illustrates this:
val foo = @{lemma "x = x" by simp}
fun add_foo thy = Global_Theory.add_thm ((Binding.name "foo", foo), [Simplifier.simp_add]) thy |> snd
val lthy = Named_Target.theory_init @{theory}
|> Local_Theory.background_theory add_foo
val target_ctxt = Local_Theory.target_of lthy
val reinit_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy)
val exit_ctxt = Local_Theory.exit lthy
val reenter_lthy = Named_Target.theory_init (Local_Theory.exit_global lthy)
fun get_foo ctxt = Proof_Context.get_thm ctxt "foo"
fun get_foo_from_ss ctxt = Simplifier.simpset_of ctxt
|> dest_ss |> #simps |> map fst |> find_first (String.isSubstring "foo")
fun get ctxt = (get_foo ctxt, get_foo_from_ss ctxt)
val res_lthy = get lthy (* ("?x = ?x", NONE) *)
val res_target = get target_ctxt (* ("?x = ?x", NONE) *)
val res_exit = get exit_ctxt (* ("?x = ?x", NONE) *)
val res_reinit = get reinit_ctxt (* ("?x = ?x", SOME "background_theory.foo") *)
val res_reenter = get reenter_lthy (* ("?x = ?x", SOME "background_theory.foo") *)
Regards,
Norbert
background_theory.thy
Email Gateway (Aug 23 2022 at 08:22):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Norbert,
this is as expected: Local_Theory.notes is the application proper
interface, whereas the others are part of the primitive devices from
which the interfaces are built.
What is your reason to hesitate using Local_Theory.notes or what's your
overal application?
Cheers,
Florian
signature.asc
Email Gateway (Aug 23 2022 at 08:22):From: Norbert Schirmer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi Florian,
The reason is the integration of “legacy tools” that are still defined as 'thy -> thy’ (e.g. the HOL record package) into a chain of “local_theory -> local_theory” tools. I had the impression that this is one of purposes of “Local_Theory.background_theory”. In case of the simpset one can explicitly merge them afterwards, but my general concern is that I don’t know which other data might also be affected and not propagated to the local_theory. Is there a better way?
Regards,
Norbert
Email Gateway (Aug 23 2022 at 08:27):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Norbert,
The reason is the integration of “legacy tools” that are still defined as 'thy -> thy’ (e.g. the HOL record package) into a chain of “local_theory -> local_theory” tools. I had the impression that this is one of purposes of “Local_Theory.background_theory”. In case of the simpset one can explicitly merge them afterwards, but my general concern is that I don’t know which other data might also be affected and not propagated to the local_theory. Is there a better way?
it is not so simple – otherwise localizing packages would be trivial.
Your application seems quite ambitious. Is there are chance that e. g.
we both could have look at it face-to-face? Discussing all the details
of localization by mail is tedious.
Cheers,
Florian
Regards,
Norbert
On 5. Feb 2020, at 19:00, Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de> wrote:
Hi Norbert,
When adding a theorem with a simp attribute via ‘Global_Theory.add_thm' within a local theory by ‘Local_Theory.background_theory’, I have the following surprising behaviour:
While the theorem can be retrieved by its name it is not added to the simplest of the resulting local theory. Only after reinitialising the local theory the theorem also appears in the simpset. Is this expected behaviour?
Further remarks: * Global_Theory.note_thms has the same effect as Global_Theory.add_thm. * Local_Theory.notes also adds the theorem to the simpset (as expected).
this is as expected: Local_Theory.notes is the application proper
interface, whereas the others are part of the primitive devices from
which the interfaces are built.What is your reason to hesitate using Local_Theory.notes or what's your
overal application?Cheers,
Florian
Last updated: Apr 19 2024 at 08:19 UTC