Re: [isabelle] Lattices and syntactic classes



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.