src/HOL/Library/Numeral_Type.thy
changeset 37653 847e95ca9b0a
parent 36350 bc7982c54e37
child 46236 ae79f2978a67
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Wed Jun 30 16:28:13 2010 +0200
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Wed Jun 30 16:28:13 2010 +0200
     1.3 @@ -5,92 +5,9 @@
     1.4  header {* Numeral Syntax for Types *}
     1.5  
     1.6  theory Numeral_Type
     1.7 -imports Main
     1.8 +imports Cardinality
     1.9  begin
    1.10  
    1.11 -subsection {* Preliminary lemmas *}
    1.12 -(* These should be moved elsewhere *)
    1.13 -
    1.14 -lemma (in type_definition) univ:
    1.15 -  "UNIV = Abs ` A"
    1.16 -proof
    1.17 -  show "Abs ` A \<subseteq> UNIV" by (rule subset_UNIV)
    1.18 -  show "UNIV \<subseteq> Abs ` A"
    1.19 -  proof
    1.20 -    fix x :: 'b
    1.21 -    have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric])
    1.22 -    moreover have "Rep x \<in> A" by (rule Rep)
    1.23 -    ultimately show "x \<in> Abs ` A" by (rule image_eqI)
    1.24 -  qed
    1.25 -qed
    1.26 -
    1.27 -lemma (in type_definition) card: "card (UNIV :: 'b set) = card A"
    1.28 -  by (simp add: univ card_image inj_on_def Abs_inject)
    1.29 -
    1.30 -
    1.31 -subsection {* Cardinalities of types *}
    1.32 -
    1.33 -syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
    1.34 -
    1.35 -translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)"
    1.36 -
    1.37 -typed_print_translation {*
    1.38 -let
    1.39 -  fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_, [T, _]))] =
    1.40 -    Syntax.const @{syntax_const "_type_card"} $ Syntax.term_of_typ show_sorts T;
    1.41 -in [(@{const_syntax card}, card_univ_tr')]
    1.42 -end
    1.43 -*}
    1.44 -
    1.45 -lemma card_unit [simp]: "CARD(unit) = 1"
    1.46 -  unfolding UNIV_unit by simp
    1.47 -
    1.48 -lemma card_bool [simp]: "CARD(bool) = 2"
    1.49 -  unfolding UNIV_bool by simp
    1.50 -
    1.51 -lemma card_prod [simp]: "CARD('a \<times> 'b) = CARD('a::finite) * CARD('b::finite)"
    1.52 -  unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product)
    1.53 -
    1.54 -lemma card_sum [simp]: "CARD('a + 'b) = CARD('a::finite) + CARD('b::finite)"
    1.55 -  unfolding UNIV_Plus_UNIV [symmetric] by (simp only: finite card_Plus)
    1.56 -
    1.57 -lemma card_option [simp]: "CARD('a option) = Suc CARD('a::finite)"
    1.58 -  unfolding UNIV_option_conv
    1.59 -  apply (subgoal_tac "(None::'a option) \<notin> range Some")
    1.60 -  apply (simp add: card_image)
    1.61 -  apply fast
    1.62 -  done
    1.63 -
    1.64 -lemma card_set [simp]: "CARD('a set) = 2 ^ CARD('a::finite)"
    1.65 -  unfolding Pow_UNIV [symmetric]
    1.66 -  by (simp only: card_Pow finite numeral_2_eq_2)
    1.67 -
    1.68 -lemma card_nat [simp]: "CARD(nat) = 0"
    1.69 -  by (simp add: infinite_UNIV_nat card_eq_0_iff)
    1.70 -
    1.71 -
    1.72 -subsection {* Classes with at least 1 and 2  *}
    1.73 -
    1.74 -text {* Class finite already captures "at least 1" *}
    1.75 -
    1.76 -lemma zero_less_card_finite [simp]: "0 < CARD('a::finite)"
    1.77 -  unfolding neq0_conv [symmetric] by simp
    1.78 -
    1.79 -lemma one_le_card_finite [simp]: "Suc 0 \<le> CARD('a::finite)"
    1.80 -  by (simp add: less_Suc_eq_le [symmetric])
    1.81 -
    1.82 -text {* Class for cardinality "at least 2" *}
    1.83 -
    1.84 -class card2 = finite + 
    1.85 -  assumes two_le_card: "2 \<le> CARD('a)"
    1.86 -
    1.87 -lemma one_less_card: "Suc 0 < CARD('a::card2)"
    1.88 -  using two_le_card [where 'a='a] by simp
    1.89 -
    1.90 -lemma one_less_int_card: "1 < int CARD('a::card2)"
    1.91 -  using one_less_card [where 'a='a] by simp
    1.92 -
    1.93 -
    1.94  subsection {* Numeral Types *}
    1.95  
    1.96  typedef (open) num0 = "UNIV :: nat set" ..
    1.97 @@ -150,7 +67,7 @@
    1.98  qed
    1.99  
   1.100  
   1.101 -subsection {* Locale for modular arithmetic subtypes *}
   1.102 +subsection {* Locales for for modular arithmetic subtypes *}
   1.103  
   1.104  locale mod_type =
   1.105    fixes n :: int