diff -r 6aa09d2a6cf9 -r 847e95ca9b0a src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Wed Jun 30 16:28:13 2010 +0200
+++ b/src/HOL/Library/Numeral_Type.thy	Wed Jun 30 16:28:13 2010 +0200
@@ -5,92 +5,9 @@
 header {* Numeral Syntax for Types *}
 
 theory Numeral_Type
-imports Main
+imports Cardinality
 begin
 
-subsection {* Preliminary lemmas *}
-(* These should be moved elsewhere *)
-
-lemma (in type_definition) univ:
-  "UNIV = Abs ` A"
-proof
-  show "Abs ` A \<subseteq> UNIV" by (rule subset_UNIV)
-  show "UNIV \<subseteq> Abs ` A"
-  proof
-    fix x :: 'b
-    have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric])
-    moreover have "Rep x \<in> A" by (rule Rep)
-    ultimately show "x \<in> Abs ` A" by (rule image_eqI)
-  qed
-qed
-
-lemma (in type_definition) card: "card (UNIV :: 'b set) = card A"
-  by (simp add: univ card_image inj_on_def Abs_inject)
-
-
-subsection {* Cardinalities of types *}
-
-syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
-
-translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)"
-
-typed_print_translation {*
-let
-  fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_, [T, _]))] =
-    Syntax.const @{syntax_const "_type_card"} $ Syntax.term_of_typ show_sorts T;
-in [(@{const_syntax card}, card_univ_tr')]
-end
-*}
-
-lemma card_unit [simp]: "CARD(unit) = 1"
-  unfolding UNIV_unit by simp
-
-lemma card_bool [simp]: "CARD(bool) = 2"
-  unfolding UNIV_bool by simp
-
-lemma card_prod [simp]: "CARD('a \<times> 'b) = CARD('a::finite) * CARD('b::finite)"
-  unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product)
-
-lemma card_sum [simp]: "CARD('a + 'b) = CARD('a::finite) + CARD('b::finite)"
-  unfolding UNIV_Plus_UNIV [symmetric] by (simp only: finite card_Plus)
-
-lemma card_option [simp]: "CARD('a option) = Suc CARD('a::finite)"
-  unfolding UNIV_option_conv
-  apply (subgoal_tac "(None::'a option) \<notin> range Some")
-  apply (simp add: card_image)
-  apply fast
-  done
-
-lemma card_set [simp]: "CARD('a set) = 2 ^ CARD('a::finite)"
-  unfolding Pow_UNIV [symmetric]
-  by (simp only: card_Pow finite numeral_2_eq_2)
-
-lemma card_nat [simp]: "CARD(nat) = 0"
-  by (simp add: infinite_UNIV_nat card_eq_0_iff)
-
-
-subsection {* Classes with at least 1 and 2  *}
-
-text {* Class finite already captures "at least 1" *}
-
-lemma zero_less_card_finite [simp]: "0 < CARD('a::finite)"
-  unfolding neq0_conv [symmetric] by simp
-
-lemma one_le_card_finite [simp]: "Suc 0 \<le> CARD('a::finite)"
-  by (simp add: less_Suc_eq_le [symmetric])
-
-text {* Class for cardinality "at least 2" *}
-
-class card2 = finite + 
-  assumes two_le_card: "2 \<le> CARD('a)"
-
-lemma one_less_card: "Suc 0 < CARD('a::card2)"
-  using two_le_card [where 'a='a] by simp
-
-lemma one_less_int_card: "1 < int CARD('a::card2)"
-  using one_less_card [where 'a='a] by simp
-
-
 subsection {* Numeral Types *}
 
 typedef (open) num0 = "UNIV :: nat set" ..
@@ -150,7 +67,7 @@
 qed
 
 
-subsection {* Locale for modular arithmetic subtypes *}
+subsection {* Locales for for modular arithmetic subtypes *}
 
 locale mod_type =
   fixes n :: int