[isabelle] New type class definitions and the underlying type classes



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




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