*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] simulating term-level abstraction using locales*From*: Peter Gammie <peteg42 at gmail.com>*Date*: Thu, 17 Dec 2009 15:41:49 +1100

Hello, I want to make a bunch of definitions using a fairly large context, and then turn those definitions into a function of one of the parameters for use in later definitions/lemmas. Here is a sketch of what I've tried: (* Attempt to simulate lambda abstraction at the locale level. Locale L is a large context. Locale A just adds a fixed-but-arbitrary parameter 'a' to it, then a series of definitions are made using 'a' and L, and a lemma or two shown. We later want to use the lemmas of A in the context of L for arbitrary values of 'a'. The complication is we want 'a' to be lambda-abstractable in later terms. We need the "for" clause in A otherwise the type variables are renamed. *) theory t imports Main begin locale L = fixes x :: "'a" and X :: "'a set" assumes x: "x ∈ X" print_locale L lemma (in L) P: "x ∈ X ⟹ P x" sorry locale A = L x X for x and X :: "'a set" + fixes a :: "'a" print_locale A definition (in A) "f y ≡ {a}" definition (in A) "g y ≡ X - {a}" lemma (in A) Q: "Q (f y) (g y) x ⟹ x ∈ X" sorry (* Propagate def's and Q and into locale L. Trivial as A has no axioms. *) sublocale L ⊆ A by (unfold_locales) print_locale! A print_locale! L (* How do we give 'a' a value here? *) lemma (in L) "(λy. Q (f y) (g y) x) 1 ⟹ P x" proof - from Q have "⋀y. Q (f y) (g y) x" unfolding f_def g_def (* wheels have fallen off *) I have a feeling I'm doing it wrong. I could do this at the term level, but it gets unreadable quite quickly. BTW I saw Brian Huffman's post: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2008-June/msg00045.html that looked like it might be a step towards solving my problem. The ML code has rotted wrt Isabelle-2009-1, and the implementation manual has a big FIXME for the section on attributes. Any chance of a pointer or fix? cheers peter -- http://peteg.org/

**Follow-Ups**:**Re: [isabelle] simulating term-level abstraction using locales***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] blast works incretable slow at tty mode
- Next by Date: Re: [isabelle] simulating term-level abstraction using locales
- Previous by Thread: [isabelle] LPAR-16 - Dakar, Senegal - April 2010
- Next by Thread: Re: [isabelle] simulating term-level abstraction using locales
- Cl-isabelle-users December 2009 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