Email Gateway (Aug 18 2022 at 13:53): Email Gateway (Aug 18 2022 at 13:53):From: Randy Pollack <rpollack@inf.ed.ac.uk>
I'm reasoning about a properties of a fixed hypothetical function. I
want to say "if F has some specified properties then some given
variant, F0 of F, has the same properties".
First, "F has property HE":
locale fixF = fixes F :: sometype
begin
abbreviation HE :: "bool" where "HE == ...
...
end
locale HE = fixF + assumes HE[rule_format]: HE
If some F has property HE then some variant, F0, of F depending on an
arbitrary constant, v0, also has that property. I can say:
locale HEv0 = HE + fixes v0 :: sometype =
definition F0 :: Ftyp where "F0 X = (if ... then v0 else F X)"
lemma shows "fixF.HE F0"
proof (... using HE ...) qed
If we interpret locale HEv0 with some actual FF and vv, we get a
context where F is interpreted by FF, v is interpreted by vv, and
"fixF.HE (%X. if ... then vv else FF X)"
is a theorem. This is as expected. But we have proved that given FF
(with property HE) and vv then (%X. if ... then vv else FF X)
is a good interpretation of locale HE.
Is there a locale expression (?) that when interpreted with with FF
and vv, gives the context of HE interpreted with
(%X. if ... then vv else FF X)? (Maybe using a "where" clause?)
Thanks,
Randy
Email Gateway (Aug 18 2022 at 13:54):From: Clemens Ballarin <ballarin@in.tum.de>
Quoting Randy Pollack <rpollack@inf.ed.ac.uk>:
I'm reasoning about a properties of a fixed hypothetical function. I
want to say "if F has some specified properties then some given
variant, F0 of F, has the same properties".First, "F has property HE":
locale fixF = fixes F :: sometype
begin
abbreviation HE :: "bool" where "HE == ...
...
end
locale HE = fixF + assumes HE[rule_format]: HEIf some F has property HE then some variant, F0, of F depending on an
arbitrary constant, v0, also has that property.
As Andreas has already indicated, this statement can be expressed in
the locales language using the sublocale command. Larry has once
called this "conditional interpretation" and I quote from the e-mail
exchange:
Larry's question:
Is there such a thing as a conditional interpretation? I used locales
to describe a certain transformation on continued fractions that is
only valid subject to certain conditions. If I want to apply this setup
in a completely concrete situation, then we have full information and
all necessary conditions can be proved. but can I use locales to
describe a special case of the transformation that is still subject to
various conditions? It seems illegal to insert a "assumes" clause in an
interpretation or to nest an interpretation within a locale.
My reply:
the way to deal with such a situation is to declare a locale for the
condition, saylocale cond = ...
and then use the sublocale command to make an interpretation relative to
condsublocale cond < expr
where expr is the locale expression you want to have interpreted.
The effect of this is that whenever the context cond is entered, the
interpretation expr is added automatically. The same applies if cond
is interpreted or used in the rhs of another sublocale command.
"Conditional interpretation" seems to be an important usage scenario
for the sublocale command. I will add it to the next revision of the
tutorial. The module hierarchy point of view taken there doesn't seem
helpful for many users.
Clemens
Email Gateway (Aug 18 2022 at 13:54):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
Hi Randy,
Is there a locale expression (?) that when interpreted with with FF
and vv, gives the context of HE interpreted with
(%X. if ... then vv else FF X)? (Maybe using a "where" clause?)
If I understand you correctly, you want to have an interpretation of HE
for F0 (with the F0's definition unfolded) whenever you interpret HEv0.
You can do this by making HEv0 a sublocale of HE with F instantiated to F0:
sublocale HEv0 < F0HE : HE "%X. if ... then v0 else F X"
unfolding F0_def[symmetric]
by(unfold_locales)(rule HEF0)
where HEF0 refers to your lemma that shows "fixF.HE F0".
Now, whenever you interpret HEv0, this also interprets HE with F0
unfolded. The constants and lemmas generated by this process are
prefixed by F0HE to distinguish them from those that obtained directly
from HE. Also, already inside the HEv0 locale, you can access the HE
context for F0.
Is that what you wanted?
Regards,
Andreas
Randy Pollack schrieb:
I'm reasoning about a properties of a fixed hypothetical function. I
want to say "if F has some specified properties then some given
variant, F0 of F, has the same properties".First, "F has property HE":
locale fixF = fixes F :: sometype
begin
abbreviation HE :: "bool" where "HE == ...
...
end
locale HE = fixF + assumes HE[rule_format]: HEIf some F has property HE then some variant, F0, of F depending on an
arbitrary constant, v0, also has that property. I can say:locale HEv0 = HE + fixes v0 :: sometype =
definition F0 :: Ftyp where "F0 X = (if ... then v0 else F X)"
lemma shows "fixF.HE F0"
proof (... using HE ...) qedIf we interpret locale HEv0 with some actual FF and vv, we get a
context where F is interpreted by FF, v is interpreted by vv, and"fixF.HE (%X. if ... then vv else FF X)"
is a theorem. This is as expected. But we have proved that given FF
(with property HE) and vv then (%X. if ... then vv else FF X)
is a good interpretation of locale HE.Is there a locale expression (?) that when interpreted with with FF
and vv, gives the context of HE interpreted with (%X. if ... then vv
else FF X)? (Maybe using a "where" clause?)Thanks,
Randy
Email Gateway (Aug 18 2022 at 20:20):From: Randy Pollack <rpollack@inf.ed.ac.uk>
Hi,
I want to use the locale "preorder" from HOL Main. First I try
to see the locale predicate for "preorder", as described in the
locales tutorial:
thm preorder_def
(*** Unknown fact "preorder_def" (line 3 of ...
What is my misunderstanding?
Next, I define a locale:
locale funny =
p1: preorder where
less_eq = p1le and less = p1lt
for p1le::"'a => 'a => bool"
and p1lt::"'a => 'a => bool"
+
fixes p2le:: "nat => 'a => 'a"
and p2lt:: "nat => 'a => 'a"
assumes p2leAx: "\forall n. preorder p2le p2lt"
Note the use of the (first class) locale predicate in assumption
p2leAx. My intension is that this locale has one carrier ('a), a
preorder on that carrier (p1) and a family of preorders indexed
by naturals (p2le), also on the same carrier. Since I don't know
how to include a family of locales in a locale definition, I use
the first class locale predicate. Is there a better way to
construct this structure?
When isabelle checks this locale "funny" it says:
### Additional type variable(s) in locale specification "funny": 'b
What does that mean? It seems to come from the use of
the "preorder" locale predicate in assumption "p2leAx", but I've
been explicit about the instantiation of "preorder"?
Finally, the context "preorder" contains some definitions and
lemmas outside the original locale definition of "preorder".
(E.g. in the context preorder I define the symmetric closure of
less_eq, and prove that is an equivalence.) Can I access those
definitions and lemmas for the preorder "p2le" in my example?
Thanks for any help,
Randy
Email Gateway (Aug 18 2022 at 20:21):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Randy,
I want to use the locale "preorder" from HOL Main.
preorder is primarily a type class. Every type class has an associated locale,
for which the naming conventions differ a bit: Some names need to be prefixed
with "class.".
thm preorder_def
(*** Unknown fact "preorder_def" (line 3 of ...
thm class.preorder_def is what you want.
Next, I define a locale:
locale funny =
p1: preorder where
less_eq = p1le and less = p1lt
for p1le::"'a => 'a => bool"
and p1lt::"'a => 'a => bool"
+
fixes p2le:: "nat => 'a => 'a"
and p2lt:: "nat => 'a => 'a"
assumes p2leAx: "\forall n. preorder p2le p2lt"
The declaration has 3 flaws:
As preorder is a type class, the corresponding predicate from the locale
assumptions is "class.preorder", not preorder. In the above form, preorder in
p2leAx is a free variable that is quantified over. Although the locale itself is
called preorder without prefix!
When you replace "preorder" with "class.preorder" in p2leAx, Isabelle now
generates a type error, which guides you to the second issue: The quantifier
over n is vacuous because n does not appear inside the quantifier. Hence, type
inference computes a type 'b for n, which does not occur among the parameters.
Hence, the warning about additional type variables.
The type for p2le and p2lt are wrong, they should be "nat => 'a => 'a => bool"
Here's the declaration you want:
locale funny =
p1: preorder where
less_eq = p1le and less = p1lt
for p1le::"'a => 'a => bool"
and p1lt::"'a => 'a => bool"
+
fixes p2le:: "nat => 'a => 'a => bool"
and p2lt:: "nat => 'a => 'a => bool"
assumes p2leAx: "class.preorder (p2le n) (p2lt n)"
Note that you can drop the quantifier on n, because locale declarations
implicitly quantify universally over all free variables in the assumptions.
Is there a better way to construct this structure?
No, this is the canonical way, see also this thread:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2010-March/msg00005.html
Finally, the context "preorder" contains some definitions and
lemmas outside the original locale definition of "preorder".
(E.g. in the context preorder I define the symmetric closure of
less_eq, and prove that is an equivalence.) Can I access those
definitions and lemmas for the preorder "p2le" in my example?
You first have to make funny a sublocale of preorder as follows:
sublocale funny < p2!: preorder "p2le n" "p2lt n" for n by(rule p2leAx)
The "p2!" determines the prefix to be used. For example:
context funny begin
thm p2.less_asym
Andreas
Last updated: Nov 21 2024 at 12:39 UTC