*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] Lattices and syntactic classes*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Wed, 31 Aug 2011 12:58:18 -0700*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>, Viorel Preoteasa <viorel.preoteasa at abo.fi>*In-reply-to*: <4E5E832B.9060902@informatik.tu-muenchen.de>*References*: <4E5644D5.2020205@in.tum.de> <4E5745D1.9020600@abo.fi> <4E582373.80901@in.tum.de> <4E5B5646.1080408@abo.fi> <4E5CC512.2010403@in.tum.de> <4E5CC902.6030007@abo.fi> <4E5E832B.9060902@informatik.tu-muenchen.de>*Sender*: huffman.brian.c at gmail.com

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

**References**:**Re: [isabelle] Lattices and syntactic classes***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] Lattices and syntactic classes
- Previous by Thread: Re: [isabelle] Lattices and syntactic classes
- Cl-isabelle-users August 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list