--- 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