2757 lemma exists_eq_sort: 

  2757 lemma exists_eq_sort: 

  2758   shows "\<exists>a. a \<in> {a. sort_of a \<in> range sort_fun}"

  2758   shows "\<exists>a. a \<in> {a. sort_of a \<in> range sort_fun}"

  2759   by (rule_tac x="Atom (sort_fun x) y" in exI, simp)

  2759   by (rule_tac x="Atom (sort_fun x) y" in exI, simp)

  2760 

  2760 

  2761 lemma at_base_class:

  2761 lemma at_base_class:

  2763   fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"

  2763   fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"

  2764   assumes type: "type_definition Rep Abs {a. sort_of a \<in> range sort_fun}"

  2764   assumes type: "type_definition Rep Abs {a. sort_of a \<in> range sort_fun}"

  2765   assumes atom_def: "\<And>a. atom a = Rep a"

  2765   assumes atom_def: "\<And>a. atom a = Rep a"

  2766   assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"

  2766   assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"

  2767   shows "OFCLASS('a, at_base_class)"

  2767   shows "OFCLASS('a, at_base_class)"