Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] correct Isabelle/ML idiom for parsing assumpti...


view this post on Zulip 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.

view this post on Zulip 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: Mar 29 2024 at 04:18 UTC