Re: [isabelle] Lattices and syntactic classes



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




On 8/31/11 10:58 PM, Brian Huffman wrote:
On Wed, Aug 31, 2011 at 11:53 AM, Florian Haftmann
<florian.haftmann at 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 defined

class 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 order

begin

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.

- Brian







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