*To*: Alexander Krauss <krauss at in.tum.de>*Subject*: Re: [isabelle] Lattices and syntactic classes*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Thu, 1 Sep 2011 16:59:01 -0700*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*: <4E5FF16D.3080906@in.tum.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> <CAAMXsibGijfJgnAUxF2pX9+5=z3gkXMVJUowCMKfCq+XD0sq7w@mail.gmail.com> <4E5FF16D.3080906@in.tum.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: > But note that to simplify your instantiation proofs you can > prove a specific introduction rule for P ==> OFCLASS('a, left_inf) where > P is the body of your left_inf class. I have plenty of experience with these OFCLASS introduction rules; see HOLCF/Cpodef.thy, HOLCF/Completion.thy, and Library/Numeral_Type.thy for various examples of mine. But note that in all of these examples, the overloaded constants in the assumptions of the theorems are all defined in *syntactic* type classes. In Viorel's case with the "left_inf" class, the goal is to make a rule that lets us prove left_inf instances without having to reprove all the semilattice_inf axioms every time. class left_inf = semilattice_inf + times + left_imp + assumes "<some axioms for times and left_imp>" assumes inf_l_def: "(inf a b) = (left_imp a b) * a" So we would want a lemma like this: lemma lift_inf_class_intro: assumes "<some axioms for times and left_imp>" assumes "(inf a b :: 'a) = (left_imp a b) * a" shows "OFCLASS('a, left_inf_class)" The problem is that "inf" doesn't come from a purely syntactic class: The use of "inf" constrains type variable 'a to have sort "semilattice_inf". This means that we can only apply this rule on types for which we've already proved the semilattice_inf instance -- exactly what we wanted to avoid! As a workaround, we would need to issue some Sign.add_const_constraint ML commands before and after proving lemma lift_inf_class_intro, to temporarily relax the sort constraints for "inf". (I use the same trick in HOLCF/Domain.thy for lemma typedef_domain_class.) These ML commands are not really user-friendly, and getting them exactly right is a bit of a pain. On Thu, Sep 1, 2011 at 1:56 PM, Alexander Krauss <krauss at in.tum.de> wrote: > 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... I guess the intro_classes method must maintain a list of introduction rules for OFCLASS predicates; maybe we could just introduce an attribute for adding new theorems to this list (replacing any pre-existing rule for the same class). I wouldn't expect this to be too hard to implement. But I think that the real challenge for making the process user-friendly is to find a way to avoid mucking around with "Sign.add_const_constraint". - Brian

**References**:**Re: [isabelle] Lattices and syntactic classes***From:*Alexander Krauss

- Previous by Date: Re: [isabelle] Multiple type variables in class specification
- Next by Date: Re: [isabelle] code generation for saturated naturals
- 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