*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] Lattices and syntactic classes*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Thu, 01 Sep 2011 22:56:13 +0200*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>, Viorel Preoteasa <viorel.preoteasa at abo.fi>*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 (X11; U; Linux i686; en-US; rv:1.9.1.16) Gecko/20101227 Icedove/3.0.11

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

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.

Alex

**Follow-Ups**:**Re: [isabelle] Lattices and syntactic classes***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Unify.matchers and term representation
- Next by Date: [isabelle] Multiple type variables in class specification
- Previous by Thread: Re: [isabelle] Lattices and syntactic classes
- 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