Email Gateway (Aug 19 2022 at 07:52): Email Gateway (Aug 19 2022 at 07:52):From: Joachim Breitner <breitner@kit.edu>
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
signature.asc
Email Gateway (Aug 19 2022 at 07:52):From: Brian Huffman <huffman@in.tum.de>
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,
Email Gateway (Aug 19 2022 at 07:52):From: Joachim Breitner <breitner@kit.edu>
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
signature.asc
Last updated: Apr 20 2024 at 01:05 UTC