[isabelle] simulating term-level abstraction using locales


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

locale L =
  fixes x :: "'a"
    and X :: "'a set"
  assumes x: "x ∈ X"

print_locale L

lemma (in L) P: "x ∈ X ⟹ P x"

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"

(* 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:


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?



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