Re: [isabelle] Issue with multiple superclasses



Dear Brian,

thanks, that did the trick. I failed to notice the "begin po"-blocks
that you wrapped your definitions in HOLCF in.

Greetings,
Joachim


Am Dienstag, den 24.07.2012, 19:43 +0200 schrieb Brian Huffman:
> 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
> 

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.info.uni-karlsruhe.de/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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