*Subject*: [isabelle] New type class definitions and the underlying type classes*From*: Jesus Aransay <jesus-maria.aransay at unirioja.es>*Date*: Tue, 26 Mar 2013 13:56:02 +0100*Cc*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Sender*: jmaransay at gmail.com

Dear all, the two type classes in the theory at the end of the mail seem to behave differently, at least with respect to the "subclass finite" command issued inside of them, but I could not find a suitable explanation. Is there any reason why in the second "subclass" command the lemma "finite_example" cannot be applied to solve the subclass predicate? More generally, is there a difference between the two following type class definitions? Is there a "better" or a "more appropriate" way to proceed? class B = bar + fixes foo :: "'a::type" ... and class B = fixes foo :: "'a::bar" ... Thanks for any hint, Jesus theory Theory imports "$ISABELLE_HOME/src/HOL/Library/Cardinality" "$ISABELLE_HOME/src/HOL/Library/Phantom_Type" begin declare[[show_sorts, show_consts, show_types]] class example = plus + fixes Rep :: "'a::{type} => nat" and Abs :: "nat => 'a" assumes type: "type_definition Rep Abs {0..<CARD('a)}" and add_def: "x + y = Abs ((Rep x + Rep y) mod (CARD ('a)))" and size: "0 < CARD('a)" begin lemma finite_example: "finite (UNIV::'a set)" using type_definition.card[OF type] card_ge_0_finite size by simp subclass finite proof show "finite (UNIV::'a set)" using finite_example . qed end class example1 = fixes Rep :: "'a::{plus} => nat" and Abs :: "nat => 'a" assumes type: "type_definition Rep Abs {0..<CARD('a)}" and add_def: "x + y = Abs ((Rep x + Rep y) mod (CARD ('a)))" and size: "0 < CARD('a)" begin lemma finite_example: "finite (UNIV::'a set)" using type_definition.card[OF type] card_ge_0_finite size by simp subclass finite proof show "finite (UNIV::'a set)" using finite_example sorry qed end end

**Follow-Ups**:**Re: [isabelle] New type class definitions and the underlying type classes***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] Make quickcheck/nitpick/sledgehammer run in background in jEdit?
- Next by Date: [isabelle] Announcement Elbe 1.65
- Previous by Thread: Re: [isabelle] Make quickcheck/nitpick/sledgehammer run in background in jEdit?
- Next by Thread: Re: [isabelle] New type class definitions and the underlying type classes
- Cl-isabelle-users March 2013 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