Re: [isabelle] Lattices and syntactic classes
- 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.firstname.lastname@example.org> <4E5745D1.email@example.com> <4E582373.firstname.lastname@example.org> <4E5B5646.email@example.com> <4E5CC512.firstname.lastname@example.org> <4E5CC902.email@example.com> <4E5E832B.firstname.lastname@example.org> <CAAMXsibGijfJgnAUxF2pX9+5=z3gkXMVJUowCMKfCq+XD0sq7w@mail.gmail.com>
- User-agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:188.8.131.52) 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
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...
This archive was generated by a fusion of
Pipermail (Mailman edition) and