Email Gateway (Aug 22 2022 at 11:50): Email Gateway (Aug 22 2022 at 11:50):From: Michael Norrish <Michael.Norrish@nicta.com.au>
I want to embed a locale L2 within L1. L1 has a local constant called c, and the user's assumption I'm parsing includes references to c.
At the Isabelle/ML level, I therefore have code that looks like
val lthy = Named_Target.init L1name thy
val asm = Syntax.read_term lthy user_string
val e = Element.Assumes [((L2name, []), [(@{term "Trueprop"} $ asm, [])])]
This seems to correctly handle the user's "c" as a reference to constant c, but then I need to create L2, and trying with
Expression.add_locale L2name L2name L1expr [e] thy
seems to reinterpret the c in e as something that needs universal quantification rather than as a reference to L1's constant.
So, what's the right way to do this?
Michael
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 12:04):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Michael,
Am 09.11.2015 um 05:48 schrieb Michael Norrish:
I want to embed a locale L2 within L1. L1 has a local constant called c, and the user's assumption I'm parsing includes references to c.
i.e. there is locale parameter c in L1; locale parameters are
represented internally. a free term variables.
At the Isabelle/ML level, I therefore have code that looks like
val lthy = Named_Target.init L1name thy
val asm = Syntax.read_term lthy user_string
val e = Element.Assumes [((L2name, []), [(@{term "Trueprop"} $ asm, [])])]This seems to correctly handle the user's "c" as a reference to constant c, but then I need to create L2, and trying with
Expression.add_locale L2name L2name L1expr [e] thy
seems to reinterpret the c in e as something that needs universal quantification rather than as a reference to L1's constant.
Risking a shot in the dark, I guess that you have to include c in the
second component of L1expr, which corresponds to the »for« clause in
Isar text.
Hope this helps,
Florian
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC