*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] Lattices and syntactic classes*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Date*: Thu, 01 Sep 2011 13:16:02 +0300*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*In-reply-to*: <CAAMXsibGijfJgnAUxF2pX9+5=z3gkXMVJUowCMKfCq+XD0sq7w@mail.gmail.com>*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> <CAAMXsibGijfJgnAUxF2pX9+5=z3gkXMVJUowCMKfCq+XD0sq7w@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:6.0) Gecko/20110812 Thunderbird/6.0

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_innerHistorically, 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

- Next by Date: Re: [isabelle] Unify.matchers and term representation
- Next by Thread: Re: [isabelle] Lattices and syntactic classes
- Cl-isabelle-users September 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