Re: [isabelle] Issue with multiple superclasses



Hi Joachim,

A general principle for reasoning with classes is that if you want to
prove lemmas within the class context, you need to define *all* the
related constants inside the appropriate class contexts as well.
Otherwise you may run into problems with the so-called "base sort"
inferred for the classes. (To get a better idea of what is going on,
try turning on [[show_sorts]], and print the type of a class locale
predicate, e.g. "term class.Nonempty_Meet_cpo".)

Most classes in the Isabelle libraries have "type" as the base sort
(this is the sort that type 'a will have within the class context) but
some classes in HOLCF have "cpo" as the base sort, due to the fact
that they refer to constants with continuous function types that are
only defined on class cpo.

I haven't tried this code yet, but I would suggest changing
"definition is_lb" to "definition (in po) is_lb", and similarly for
is_glb; alternatively, wrap both definitions in a "context po begin
... end" block.

Hope this helps,
- Brian

On Tue, Jul 24, 2012 at 6:00 PM, Joachim Breitner <breitner at kit.edu> wrote:
> Hello,
>
> I have a problem with type classes and multiple subclasses, and here is
> a stripped-town testcase:
>
>         theory "Test"
>         imports
>           "~~/src/HOL/HOLCF/HOLCF"
>         begin
>
>         default_sort cpo
>
>         class Top_cpo = cpo +
>           assumes most: "∃x. ∀y. y ⊑ x"
>         begin
>
>           definition top :: "'a"
>             where "top = (THE x. ∀y. y ⊑ x)"
>
>           notation (xsymbols)
>             top ("⊤")
>         end
>
>         definition is_lb :: "'a set => 'a => bool" (infix ">|" 55) where
>           "S >| x <-> (∀y∈S. x ⊑ y)"
>
>         definition is_glb :: "'a set => 'a => bool" (infix ">>|" 55)
>         where
>           "S >>| x <-> S >| x ∧ (∀u. S >| u --> u ⊑ x)"
>
>         definition glb :: "'a set => 'a" ("⨅_" [60]60) where
>           "glb S = (THE x. S >>| x)"
>
>         class Nonempty_Meet_cpo = cpo +
>           assumes nonempty_meet_exists: "S ≠ {} ⟹ ∃x. S >>| x"
>
>         class Meet_cpo = Top_cpo + Nonempty_Meet_cpo
>         begin
>           lemma "∃ x. {} >>| (x::'a)"
>              apply (rule_tac x = "⊤" in exI)
>         (*
>          Type unification failed: Variable 'a::cpo not of sort Top_cpo
>
>         Failed to meet type constraint:
>
>         Term:  ⊤ :: ??'a
>         Type:  'a
>         *)
>           oops
>
>         end
>
> I would assume that the 'a inside the context of class will have that
> sort (Meet_cpo) and hence by implication Top_cpo, but it seems it does
> not. Would someone be so kind and help me out here?
>
> (This is on Isabelle2012.)
>
> Thanks,
> Joachim
>
> --
> Dipl.-Math. Dipl.-Inform. Joachim Breitner
> Wissenschaftlicher Mitarbeiter
> http://pp.info.uni-karlsruhe.de/~breitner





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