Email Gateway (Aug 18 2022 at 14:25): Email Gateway (Aug 18 2022 at 14:25):From: Peter Gammie <peteg42@gmail.com>
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
Email Gateway (Aug 18 2022 at 14:25):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,
sublocale L ⊆ A by (unfold_locales)
if you want to instantiate the 'a' parameter in locale 'A', this is your
"only chance", e.g.
sublocale L ⊆ A x X x
Then you also should add a namespace prefix, e.g.
sublocale L ⊆ A: A x X x
If this is not what you intend to do, do not hesitate to ask further
questions with some hints what you plan to model. Locales are a
powerful abstraction mechanisms, but their application sometimes
requires some care and inadvertently comes with some restrictions.
Hope this helps
Florian
signature.asc
Email Gateway (Aug 18 2022 at 14:26):From: Peter Gammie <peteg42@gmail.com>
Florian:
Thanks for your comments.
I came to understand that I was asking for too much: at the very least, Isabelle has no syntax for (lambda-) abstracting a free variable from several definitions (like what happens in the example I posted).
So I gave up on these locales and went back to the tried and true record + predicate approach. I'm not so happy with that as I lose the syntactic niceties (e.g. a pleasant introduction mechanism) but it is not so bad.
cheers
peter
Last updated: Nov 21 2024 at 12:39 UTC