cleaned up
authorhuffman
Thu Feb 19 23:18:28 2009 -0800 (2009-02-19)
changeset 30001dd27e16677b2
parent 30000 453077188eac
child 30005 7d97e20728d4
child 30006 f54b48cda286
child 30015 1baeda435aa6
child 30255 ba1c4fe06792
cleaned up
src/HOL/Library/Numeral_Type.thy
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Thu Feb 19 18:16:19 2009 -0800
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Thu Feb 19 23:18:28 2009 -0800
     1.3 @@ -42,32 +42,54 @@
     1.4  end
     1.5  *}
     1.6  
     1.7 -lemma card_unit: "CARD(unit) = 1"
     1.8 +lemma card_unit [simp]: "CARD(unit) = 1"
     1.9    unfolding UNIV_unit by simp
    1.10  
    1.11 -lemma card_bool: "CARD(bool) = 2"
    1.12 +lemma card_bool [simp]: "CARD(bool) = 2"
    1.13    unfolding UNIV_bool by simp
    1.14  
    1.15 -lemma card_prod: "CARD('a::finite \<times> 'b::finite) = CARD('a) * CARD('b)"
    1.16 +lemma card_prod [simp]: "CARD('a \<times> 'b) = CARD('a::finite) * CARD('b::finite)"
    1.17    unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product)
    1.18  
    1.19 -lemma card_sum: "CARD('a::finite + 'b::finite) = CARD('a) + CARD('b)"
    1.20 +lemma card_sum [simp]: "CARD('a + 'b) = CARD('a::finite) + CARD('b::finite)"
    1.21    unfolding UNIV_Plus_UNIV [symmetric] by (simp only: finite card_Plus)
    1.22  
    1.23 -lemma card_option: "CARD('a::finite option) = Suc CARD('a)"
    1.24 +lemma card_option [simp]: "CARD('a option) = Suc CARD('a::finite)"
    1.25    unfolding insert_None_conv_UNIV [symmetric]
    1.26    apply (subgoal_tac "(None::'a option) \<notin> range Some")
    1.27    apply (simp add: card_image)
    1.28    apply fast
    1.29    done
    1.30  
    1.31 -lemma card_set: "CARD('a::finite set) = 2 ^ CARD('a)"
    1.32 +lemma card_set [simp]: "CARD('a set) = 2 ^ CARD('a::finite)"
    1.33    unfolding Pow_UNIV [symmetric]
    1.34    by (simp only: card_Pow finite numeral_2_eq_2)
    1.35  
    1.36 -lemma card_finite_pos [simp]: "0 < CARD('a::finite)"
    1.37 +lemma card_nat [simp]: "CARD(nat) = 0"
    1.38 +  by (simp add: infinite_UNIV_nat card_eq_0_iff)
    1.39 +
    1.40 +
    1.41 +subsection {* Classes with at least 1 and 2  *}
    1.42 +
    1.43 +text {* Class finite already captures "at least 1" *}
    1.44 +
    1.45 +lemma zero_less_card_finite [simp]: "0 < CARD('a::finite)"
    1.46    unfolding neq0_conv [symmetric] by simp
    1.47  
    1.48 +lemma one_le_card_finite [simp]: "Suc 0 \<le> CARD('a::finite)"
    1.49 +  by (simp add: less_Suc_eq_le [symmetric])
    1.50 +
    1.51 +text {* Class for cardinality "at least 2" *}
    1.52 +
    1.53 +class card2 = finite + 
    1.54 +  assumes two_le_card: "2 \<le> CARD('a)"
    1.55 +
    1.56 +lemma one_less_card: "Suc 0 < CARD('a::card2)"
    1.57 +  using two_le_card [where 'a='a] by simp
    1.58 +
    1.59 +lemma one_less_int_card: "1 < int CARD('a::card2)"
    1.60 +  using one_less_card [where 'a='a] by simp
    1.61 +
    1.62  
    1.63  subsection {* Numeral Types *}
    1.64  
    1.65 @@ -86,6 +108,22 @@
    1.66      by simp
    1.67  qed
    1.68  
    1.69 +lemma card_num0 [simp]: "CARD (num0) = 0"
    1.70 +  unfolding type_definition.card [OF type_definition_num0]
    1.71 +  by simp
    1.72 +
    1.73 +lemma card_num1 [simp]: "CARD(num1) = 1"
    1.74 +  unfolding type_definition.card [OF type_definition_num1]
    1.75 +  by (simp only: card_unit)
    1.76 +
    1.77 +lemma card_bit0 [simp]: "CARD('a bit0) = 2 * CARD('a::finite)"
    1.78 +  unfolding type_definition.card [OF type_definition_bit0]
    1.79 +  by simp
    1.80 +
    1.81 +lemma card_bit1 [simp]: "CARD('a bit1) = Suc (2 * CARD('a::finite))"
    1.82 +  unfolding type_definition.card [OF type_definition_bit1]
    1.83 +  by simp
    1.84 +
    1.85  instance num1 :: finite
    1.86  proof
    1.87    show "finite (UNIV::num1 set)"
    1.88 @@ -93,47 +131,24 @@
    1.89      using finite by (rule finite_imageI)
    1.90  qed
    1.91  
    1.92 -instance bit0 :: (finite) finite
    1.93 +instance bit0 :: (finite) card2
    1.94  proof
    1.95    show "finite (UNIV::'a bit0 set)"
    1.96      unfolding type_definition.univ [OF type_definition_bit0]
    1.97      by simp
    1.98 +  show "2 \<le> CARD('a bit0)"
    1.99 +    by simp
   1.100  qed
   1.101  
   1.102 -instance bit1 :: (finite) finite
   1.103 +instance bit1 :: (finite) card2
   1.104  proof
   1.105    show "finite (UNIV::'a bit1 set)"
   1.106      unfolding type_definition.univ [OF type_definition_bit1]
   1.107      by simp
   1.108 +  show "2 \<le> CARD('a bit1)"
   1.109 +    by simp
   1.110  qed
   1.111  
   1.112 -lemma card_num1: "CARD(num1) = 1"
   1.113 -  unfolding type_definition.card [OF type_definition_num1]
   1.114 -  by (simp only: card_unit)
   1.115 -
   1.116 -lemma card_bit0: "CARD('a::finite bit0) = 2 * CARD('a)"
   1.117 -  unfolding type_definition.card [OF type_definition_bit0]
   1.118 -  by simp
   1.119 -
   1.120 -lemma card_bit1: "CARD('a::finite bit1) = Suc (2 * CARD('a))"
   1.121 -  unfolding type_definition.card [OF type_definition_bit1]
   1.122 -  by simp
   1.123 -
   1.124 -lemma card_num0: "CARD (num0) = 0"
   1.125 -  by (simp add: infinite_UNIV_nat card_eq_0_iff type_definition.card [OF type_definition_num0])
   1.126 -
   1.127 -lemmas card_univ_simps [simp] =
   1.128 -  card_unit
   1.129 -  card_bool
   1.130 -  card_prod
   1.131 -  card_sum
   1.132 -  card_option
   1.133 -  card_set
   1.134 -  card_num1
   1.135 -  card_bit0
   1.136 -  card_bit1
   1.137 -  card_num0
   1.138 -
   1.139  
   1.140  subsection {* Locale for modular arithmetic subtypes *}
   1.141  
   1.142 @@ -288,8 +303,7 @@
   1.143             "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
   1.144  apply (rule mod_type.intro)
   1.145  apply (simp add: int_mult type_definition_bit0)
   1.146 -apply simp
   1.147 -using card_finite_pos [where ?'a='a] apply arith
   1.148 +apply (rule one_less_int_card)
   1.149  apply (rule zero_bit0_def)
   1.150  apply (rule one_bit0_def)
   1.151  apply (rule plus_bit0_def [unfolded Abs_bit0'_def])
   1.152 @@ -305,7 +319,7 @@
   1.153             "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
   1.154  apply (rule mod_type.intro)
   1.155  apply (simp add: int_mult type_definition_bit1)
   1.156 -apply simp
   1.157 +apply (rule one_less_int_card)
   1.158  apply (rule zero_bit1_def)
   1.159  apply (rule one_bit1_def)
   1.160  apply (rule plus_bit1_def [unfolded Abs_bit1'_def])
   1.161 @@ -422,39 +436,6 @@
   1.162  in [("bit0", bit_tr' 0), ("bit1", bit_tr' 1)] end;
   1.163  *}
   1.164  
   1.165 -
   1.166 -subsection {* Classes with at least 1 and 2  *}
   1.167 -
   1.168 -text {* Class finite already captures "at least 1" *}
   1.169 -
   1.170 -lemma zero_less_card_finite [simp]:
   1.171 -  "0 < CARD('a::finite)"
   1.172 -proof (cases "CARD('a::finite) = 0")
   1.173 -  case False thus ?thesis by (simp del: card_0_eq)
   1.174 -next
   1.175 -  case True
   1.176 -  thus ?thesis by (simp add: finite)
   1.177 -qed
   1.178 -
   1.179 -lemma one_le_card_finite [simp]:
   1.180 -  "Suc 0 <= CARD('a::finite)"
   1.181 -  by (simp add: less_Suc_eq_le [symmetric] zero_less_card_finite)
   1.182 -
   1.183 -
   1.184 -text {* Class for cardinality "at least 2" *}
   1.185 -
   1.186 -class card2 = finite + 
   1.187 -  assumes two_le_card: "2 <= CARD('a)"
   1.188 -
   1.189 -lemma one_less_card: "Suc 0 < CARD('a::card2)"
   1.190 -  using two_le_card [where 'a='a] by simp
   1.191 -
   1.192 -instance bit0 :: (finite) card2
   1.193 -  by intro_classes (simp add: one_le_card_finite)
   1.194 -
   1.195 -instance bit1 :: (finite) card2
   1.196 -  by intro_classes (simp add: one_le_card_finite)
   1.197 -
   1.198  subsection {* Examples *}
   1.199  
   1.200  lemma "CARD(0) = 0" by simp