Re: [isabelle] Lattices and syntactic classes



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.