Re: [isabelle] correct Isabelle/ML idiom for parsing assumption for new locale

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,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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