*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] making local definitions programmatically*From*: Michael Norrish <Michael.Norrish at nicta.com.au>*Date*: Thu, 24 Apr 2008 10:01:50 +1000*Cc*: USR Isabelle <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <480EDFAE.7000106@informatik.tu-muenchen.de>*References*: <480ED955.8000403@nicta.com.au> <480EDFAE.7000106@informatik.tu-muenchen.de>*User-agent*: Icedove 1.5.0.14pre (X11/20071018)

Florian Haftmann wrote: > the best thing is to use the "check" interface which does the job > for you: > Syntax.check_term @{context} (Const ("local.C1", dummyT)) > yield a completely inferred and expanded term representing the local > constant C1. This saves you from educated guesses what the expanded > foundation term of a local constant actually is. Note that "check" > is a part of the canonical interface for reading terms [...] > This allows to aggregate "skeleton terms" with dummy types and check > them to get complete internal terms. > Example: > locale L = > fixes c0 :: "'a \<Rightarrow> 'a" > begin > > definition > "c1 x = c0 (c0 x)" > > definition > "c2 x = c1 (c1 x)" > > ML {* Syntax.parse_term @{context} "c1" *} > ML {* Syntax.check_term @{context} (Const ("local.c1", dummyT)) *} > end But can I then pass an expanded term, one which mentions the implicit locale parameters explicitly, to LocalTheory.define? My experiments suggest I can't. If I put this into the locale ML {* val t = Syntax.check_term @{context} (Const("local.c1", dummyT)) val ctxt' = LocalTheory.define Thm.definitionK (("c3", NoSyn), (("", []), t)) @{context} *} then I get an error "Illegal application of command "consts" in local theory mode". What should t be to make this definition work? Or should I be using some other definitional principle? And is prepending "local." the canonical way to get an acceptable name for the locale's constants? Michael.

**Follow-Ups**:**Re: [isabelle] making local definitions programmatically***From:*Florian Haftmann

**References**:**[isabelle] making local definitions programmatically***From:*Michael Norrish

**Re: [isabelle] making local definitions programmatically***From:*Florian Haftmann

- Previous by Date: [isabelle] Partial functions
- Next by Date: Re: [isabelle] making local definitions programmatically
- Previous by Thread: Re: [isabelle] making local definitions programmatically
- Next by Thread: Re: [isabelle] making local definitions programmatically
- Cl-isabelle-users April 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list