Patrick Nicodemus (Oct 28 2023 at 20:19): Patrick Nicodemus (Oct 28 2023 at 20:19):I want to write a locale where I do
fix A B C...
define a new thing in terms of A B and C...
make assumptions about the new thing in the locale
Is this possible? I see "defines" in the manual but this appears to be deprecated
Patrick Nicodemus (Oct 28 2023 at 20:20):I guess I can do "fix" and define its behavior by additional assumptions but I want something where the definition will unfold automatically by simplification I guess.
Maximilian Schäffeler (Oct 28 2023 at 21:07):What do you mean by "make assumptions about the new thing in the locale"?
Patrick Nicodemus (Oct 28 2023 at 21:43):Basically as I understand it the structure of a locale definition is:
locale XYZ =
(inheritance declarations in the form of locale expressions)
for A : type (infix notation) and B : type (notation )...
fixes ...
assumes ...
fixes ..
assumes...
What I want to do is something like
locale partial_magma =
fixes E : "'a => bool" (* existence/ well-definedness predicate coding the domain of phi*)
defines KlEq where "KlEq x y = (E x \/ E y ==> x = y)" (infix \cong 52)
fixes phi : "'a => 'a => 'a" (infix cdot 60)
assumes assoc : " (x \cdot y) \cdot z \cong x \cdot (y \cdot z)" (* multiplication is associative on its domain *)
Here I'm defining a new thing within the locale, KlEq, that i can refer to later (in the body of "assoc" or other locale assumptions.)
I could do this with
fixes KlEq :: "'a => 'a => bool"
assumes "KlEq x y = (E x \/ E y ==> x y)
or perhaps I could define a notation for it (although i'm not sure of the syntax for that either)
But yeah I have a fairly complicated locale definition and I want to define intermediary constructs midway through the locale definition that I use to express more sophisticated /complex assumptions about the locale.
Patrick Nicodemus (Oct 28 2023 at 21:44):I believe "defines" is a legitimate keyword here but the tutorial on locales does not mention it and suggests that it is "only in place for backwards compatibility reasons" which I read as a form of deprecation
Patrick Nicodemus (Oct 28 2023 at 21:58):I am also able to solve this problem by having two locale definitions, one which extends the other. Like in this case I could make "set equipped with a subset" its own locale, define KlEq in that locale, and then have everything else extend this locale. But it may not be worth it to define a new locale for everything.
Mathias Fleury (Oct 29 2023 at 18:03):Defining two locales is the standard idiom
Last updated: Apr 28 2024 at 16:17 UTC