Re: [isabelle] Lattices and syntactic classes



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 + x = x) we can define a partial order as "x <= y <-> x + y = y". Again, one relies on the syntactic class "ord" here.

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





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