Email Gateway (Aug 18 2022 at 18:18): Email Gateway (Aug 18 2022 at 18:18):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Viorel,
the answer to your issue has many facets.
Historically, syntactic classes where necessary since the class +
operations & instantiation infrastructure has not yet emerged. With the
class package my first thought was to avoid syntactic classes entirely,
since they allow to write down things for which one might expect certain
properties to hold, which, in fact, do not, only with more specific sort
constraints:
(a + b) + c = a + (b + c)
2 + 2 = 4 -- an Isabelle classic!
(an aside: there is a similar issue with min/max which are defined
purely syntactical, not only on linear orders)
I kept the then existing syntactic classes a) for backward compatibility
and b) since they carry syntax by default. The case for inf and sup
then was different.
Nowadays I have to admit that in situations like yours syntactic classes
for inf and sup would allow a more liberal building of the class
hierarchy. Indeed, I recently had some thoughts how you could achieve
something like »import class parameters, but with different
specification from which the original specification follows«, in essence
a class with simultaneous subclass. But it looked rather complicated.
I have no strong opinion whether to turn inf and sup into syntactic
classes. But note that to simplify your instantiation proofs you can
prove a specific introduction rule for P ==> OFCLASS('a, left_inf) where
P is the body of your left_inf class.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 18:18):From: Brian Huffman <brianh@cs.pdx.edu>
On Wed, Aug 31, 2011 at 11:53 AM, Florian Haftmann
<florian.haftmann@informatik.tu-muenchen.de> wrote:
Hi Viorel,
Ultimately the structure is a (semi-) lattice, but the axioms are
different.
Imagine an algebraic structure with some operations *, left_imp which
satisfies
some properties and in which inf can be definedclass left_inf = inf + times + left_imp + order +
assumes some axioms for times and left_imp
and inf_l_def: "(inf a b) = (left_imp a b) * a"
and definition of orderbegin
in this setting the fact that inf is a semi-lattice operation can be
proved from the axioms of times and left_imp.
There are several similar situations that arise in Isabelle's real
analysis class hierarchy. For example, RealVector.thy introduces type
classes topological_space and metric_space. Every metric space is also
a topological space, so we definitely want a subclass relationship
topological_space < metric_space. The naive way to formalize these
classes is shown below.
class topological_space =
fixes "open" :: "'a set => bool"
assumes open_UNIV: "open UNIV"
assumes open_Int: "open S ==> open T ==> open (S \<inter> T)"
assumes open_Union:: "ALL S:K. open S ==> open (Union K)"
class metric_space = topological_space +
fixes dist :: "'a => 'a => real"
assumes dist_eq_0_iff: "(dist x y = 0) = (x = y)"
assumes dist_triangle2: "dist x y \<le> dist x z + dist y z"
assumes open_dist: "open S = (ALL x:S. EX e>0. ALL y. dist y x < e --> y : S)"
Of course, the problem here is that whenever we want to prove an
instance of the metric_space class, Isabelle expects us to re-prove
all the topological_space axioms as well, even though they are implied
by the metric_space axioms! To avoid this, I broke up the class
definitions using some syntactic classes:
class "open" = fixes "open" :: "'a set => bool"
class topological_space = "open" +
assumes open_UNIV: "open UNIV"
assumes open_Int: "open S ==> open T ==> open (S \<inter> T)"
assumes open_Union:: "ALL S:K. open S ==> open (Union K)"
class dist = fixes dist :: "'a => 'a => real"
class open_dist = "open" + dist +
assumes open_dist: "open S = (ALL x:S. EX e>0. ALL y. dist y x < e --> y : S)"
class metric_space = open_dist +
assumes dist_eq_0_iff: "(dist x y = 0) = (x = y)"
assumes dist_triangle2: "dist x y \<le> dist x z + dist y z"
Then we can prove a subclass relationship:
instance topological_space < metric_space
proof ...
Now instance proofs for metric_space give us exactly the proof
obligations we want.
Similar relationships exist among a whole sequence of classes, and
they are set up in a similar manner:
topological_space < metric_space < real_normed_vector < real_inner
Historically, syntactic classes where necessary since the class +
operations & instantiation infrastructure has not yet emerged. With the
class package my first thought was to avoid syntactic classes entirely,
since they allow to write down things for which one might expect certain
properties to hold, which, in fact, do not, only with more specific sort
constraints:(a + b) + c = a + (b + c)
2 + 2 = 4 -- an Isabelle classic!
The redefined class hierarchy as I presented it above still has this
same kind of problem: If you write something like "dist x y = dist y
x", the inferred sort for x and y is "dist", and not "metric_space" as
you would like. I solve this problem with the following ML command:
setup {* Sign.add_const_constraint
(@{const_name dist}, SOME @{typ "'a::metric_space => 'a => real"}) *}
This tells Isabelle's parser/typechecker to automatically infer a
metric_space class constraint whenever the "dist" constant is used.
This works great most of the time, but there are rare occasions when I
need to temporarily turn off the extra constraints (see
Library/Inner_Product.thy) which is a pain.
Nowadays I have to admit that in situations like yours syntactic classes
for inf and sup would allow a more liberal building of the class
hierarchy. Indeed, I recently had some thoughts how you could achieve
something like »import class parameters, but with different
specification from which the original specification follows«, in essence
a class with simultaneous subclass. But it looked rather complicated.
Such a feature might be worthwhile; after all, my workaround for the
problem is rather complicated too! This feature would let us radically
simplify the class hierarchy in the real analysis theories. It would
also let us simplify the group/ring class hierarchy a bit. But perhaps
most importantly, it would let users define classes like Viorel's
"left_inf" class in the most natural way.
Email Gateway (Aug 18 2022 at 18:19):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello Brian, Florian,
Thank you for your answers.
It seems that the only reason for not having
syntactic classes for inf and sup is because
an expression "inf a b", by default will
have a too week type. However you do accept
this compromise for the arithmetic operators
which seems more difficult to justify.
As Brian pointed out syntactic classes are needed
also when dealing with topological and metric spaces
in order to avoid reproving things for every instantiation.
I have another example which is also in the favor of
syntactic classes. In Isabelle 2009 the operations
Inf and Sup were defined as part of the complete
lattice structure, and now they are syntactic classes.
It seems that there was a similar problem for the complete
lattice operations.
Best regards,
Viorel
Email Gateway (Aug 18 2022 at 18:20):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
A further aspect: Pure.intro declaration have precedence over the intro
classes method, as shown in the folling silly example:
lemma nonsense [Pure.intro]:
"False \<Longrightarrow> OFCLASS('a, default_class)"
..
instance bool :: default
apply default
oops
By declaring your customary class introduction rules Pure.intro, they
are preferred in instance proofs.
Florian
signature.asc
Email Gateway (Aug 18 2022 at 18:21):From: Makarius <makarius@sketis.net>
Does that solve the issues that were raised on this thread earlier? I
have followed the matter only with one eye, without really understanding
the full situation.
The "default" proof step is a little bit entangled, it tries to be smart
in including certain aspects of "intro_classes" to make such proof
patterns look somehow obvious. The classical reasoner overrides "default"
later once more, to add its classical viewpoint to the "rule" part.
If there is a need for it, such things can certainly be reformed, but it
would require a brief inspection of the status quo and the parts of the
history leading to it.
If plain Pure.intro (which already works with the "rule" method, BTW) is
sufficient, it is even easier.
Makarius
Email Gateway (Aug 18 2022 at 18:21):From: Alexander Krauss <krauss@in.tum.de>
To me this looks rather like a workaround for some specific situations.
If I understand correctly, it wouldn't work with a more complex class
hierarchy, where parts of the instance may already be established etc.
The issue certainly deserves more thourough examination at some point.
For now I have just added (5e51075cbd97) the syntactic classes for inf
and sup, which were originally asked for by Viorel. This is a rather
straightforward thing, and the more general typings that may arise seem
to have little impact in practice.
Alex
Email Gateway (Aug 18 2022 at 18:21):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
By declaring your customary class introduction rules Pure.intro, they
are preferred in instance proofs.Does that solve the issues that were raised on this thread earlier?
To me this looks rather like a workaround for some specific situations.
If I understand correctly, it wouldn't work with a more complex class
hierarchy, where parts of the instance may already be established etc.
The issue certainly deserves more thourough examination at some point.
Indeed.
For now I have just added (5e51075cbd97) the syntactic classes for inf
and sup, which were originally asked for by Viorel. This is a rather
straightforward thing, and the more general typings that may arise seem
to have little impact in practice.
OK.
Florian
signature.asc
Email Gateway (Aug 18 2022 at 18:21):From: Alexander Krauss <krauss@in.tum.de>
On 08/31/2011 09:58 PM, Brian Huffman wrote:
[...]
To avoid this, I broke up the class
definitions using some syntactic classes:class "open" = fixes "open" :: "'a set => bool"
class topological_space = "open" +
assumes open_UNIV: "open UNIV"
assumes open_Int: "open S ==> open T ==> open (S \<inter> T)"
assumes open_Union:: "ALL S:K. open S ==> open (Union K)"class dist = fixes dist :: "'a => 'a => real"
class open_dist = "open" + dist +
assumes open_dist: "open S = (ALL x:S. EX e>0. ALL y. dist y x< e --> y : S)"class metric_space = open_dist +
assumes dist_eq_0_iff: "(dist x y = 0) = (x = y)"
assumes dist_triangle2: "dist x y \<le> dist x z + dist y z"Then we can prove a subclass relationship:
instance topological_space< metric_space
proof ...Now instance proofs for metric_space give us exactly the proof
obligations we want.Similar relationships exist among a whole sequence of classes, and
they are set up in a similar manner:
topological_space< metric_space< real_normed_vector< real_inner
Another instance of that same pattern is in
HOL/Library/Kleene_Algebra.thy: In any idempotent additive structure (x
Nowadays I have to admit that in situations like yours syntactic classes
for inf and sup would allow a more liberal building of the class
hierarchy. Indeed, I recently had some thoughts how you could achieve
something like »import class parameters, but with different
specification from which the original specification follows«, in essence
a class with simultaneous subclass. But it looked rather complicated.Such a feature might be worthwhile; after all, my workaround for the
problem is rather complicated too! This feature would let us radically
simplify the class hierarchy in the real analysis theories. It would
also let us simplify the group/ring class hierarchy a bit. But perhaps
most importantly, it would let users define classes like Viorel's
"left_inf" class in the most natural way.
Could one maybe achieve the same effect by declaring the subclass
relationship (instead of proving it later), but then have the
"intro_classes" method (or whatever its name was exactly) apply some
user-supplied rule to prove the original axioms from the new
specification? In other words, formalize the workaround suggested by
Florian a little bit more, with some minimalistic tool support... But
this will need more thought...
Alex
Email Gateway (Aug 18 2022 at 18:22):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
To me this looks rather like a workaround for some specific
situations. If I understand correctly, it wouldn't work with a more
complex class hierarchy, where parts of the instance may already be
established etc. The issue certainly deserves more thourough
examination at some point.For now I have just added (5e51075cbd97) the syntactic classes for inf
and sup, which were originally asked for by Viorel. This is a rather
straightforward thing, and the more general typings that may arise
seem to have little impact in practice.
Thank you for this change. I did use a work around which worked well. So
the alternatives suggested did not seem better to me.
The work around that I used is the following:
class inf =
fixes inf :: "'a => 'a => 'a" (infixl "\<sqinter>" 70)
class sup =
fixes sup :: "'a => 'a => 'a" (infixl "\<squnion>" 65)
class lattice_infix = order + inf + sup +
assumes lattice: "class.lattice (op \<le>) (op <) inf sup"
sublocale lattice_infix < lattice "op \<le>" "op <" inf sup
by (rule lattice)
After this I used lattice_infix instead of lattice. It seems that
this way works better and it is more general that the ways
suggested earlier.
Viorel
>
>
Email Gateway (Aug 18 2022 at 18:25):From: Brian Huffman <brianh@cs.pdx.edu>
I guess the intro_classes method must maintain a list of introduction
rules for OFCLASS predicates; maybe we could just introduce an
attribute for adding new theorems to this list (replacing any
pre-existing rule for the same class). I wouldn't expect this to be
too hard to implement.
But I think that the real challenge for making the process
user-friendly is to find a way to avoid mucking around with
"Sign.add_const_constraint".
Last updated: Apr 19 2024 at 12:27 UTC