src/HOL/Library/Cardinality.thy
changeset 48052 b74766e4c11e
parent 48051 53a0df441e20
child 48053 9bc78a08ff0a
equal deleted inserted replaced
48051:53a0df441e20 48052:b74766e4c11e
   159 
   159 
   160 subsubsection {* @{typ "int"} *}
   160 subsubsection {* @{typ "int"} *}
   161 
   161 
   162 instantiation int :: card_UNIV begin
   162 instantiation int :: card_UNIV begin
   163 
   163 
   164 definition "card_UNIV_class.card_UNIV = (\<lambda>a :: int itself. 0)"
   164 definition "card_UNIV = (\<lambda>a :: int itself. 0)"
   165 
   165 
   166 instance proof
   166 instance proof
   167   fix x :: "int itself"
   167   fix x :: "int itself"
   168   show "card_UNIV x = card (UNIV :: int set)"
   168   show "card_UNIV x = card (UNIV :: int set)"
   169     unfolding card_UNIV_int_def by(simp add: infinite_UNIV_int)
   169     unfolding card_UNIV_int_def by(simp add: infinite_UNIV_int)
   173 
   173 
   174 subsubsection {* @{typ "'a list"} *}
   174 subsubsection {* @{typ "'a list"} *}
   175 
   175 
   176 instantiation list :: (type) card_UNIV begin
   176 instantiation list :: (type) card_UNIV begin
   177 
   177 
   178 definition "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a list itself. 0)"
   178 definition "card_UNIV = (\<lambda>a :: 'a list itself. 0)"
   179 
   179 
   180 instance proof
   180 instance proof
   181   fix x :: "'a list itself"
   181   fix x :: "'a list itself"
   182   show "card_UNIV x = card (UNIV :: 'a list set)"
   182   show "card_UNIV x = card (UNIV :: 'a list set)"
   183     unfolding card_UNIV_list_def by(simp add: infinite_UNIV_listI)
   183     unfolding card_UNIV_list_def by(simp add: infinite_UNIV_listI)
   185 
   185 
   186 end
   186 end
   187 
   187 
   188 subsubsection {* @{typ "unit"} *}
   188 subsubsection {* @{typ "unit"} *}
   189 
   189 
   190 lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
       
   191   unfolding UNIV_unit by simp
       
   192 
       
   193 instantiation unit :: card_UNIV begin
   190 instantiation unit :: card_UNIV begin
   194 
   191 
   195 definition card_UNIV_unit_def: 
   192 definition "card_UNIV = (\<lambda>a :: unit itself. 1)"
   196   "card_UNIV_class.card_UNIV = (\<lambda>a :: unit itself. 1)"
       
   197 
   193 
   198 instance proof
   194 instance proof
   199   fix x :: "unit itself"
   195   fix x :: "unit itself"
   200   show "card_UNIV x = card (UNIV :: unit set)"
   196   show "card_UNIV x = card (UNIV :: unit set)"
   201     by(simp add: card_UNIV_unit_def card_UNIV_unit)
   197     by(simp add: card_UNIV_unit_def card_UNIV_unit)
   203 
   199 
   204 end
   200 end
   205 
   201 
   206 subsubsection {* @{typ "bool"} *}
   202 subsubsection {* @{typ "bool"} *}
   207 
   203 
   208 lemma card_UNIV_bool: "card (UNIV :: bool set) = 2"
       
   209   unfolding UNIV_bool by simp
       
   210 
       
   211 instantiation bool :: card_UNIV begin
   204 instantiation bool :: card_UNIV begin
   212 
   205 
   213 definition card_UNIV_bool_def: 
   206 definition "card_UNIV = (\<lambda>a :: bool itself. 2)"
   214   "card_UNIV_class.card_UNIV = (\<lambda>a :: bool itself. 2)"
       
   215 
   207 
   216 instance proof
   208 instance proof
   217   fix x :: "bool itself"
   209   fix x :: "bool itself"
   218   show "card_UNIV x = card (UNIV :: bool set)"
   210   show "card_UNIV x = card (UNIV :: bool set)"
   219     by(simp add: card_UNIV_bool_def card_UNIV_bool)
   211     by(simp add: card_UNIV_bool_def card_UNIV_bool)
   233   finally show ?thesis by (simp add: chars_def)
   225   finally show ?thesis by (simp add: chars_def)
   234 qed
   226 qed
   235 
   227 
   236 instantiation char :: card_UNIV begin
   228 instantiation char :: card_UNIV begin
   237 
   229 
   238 definition card_UNIV_char_def: 
   230 definition "card_UNIV_class.card_UNIV = (\<lambda>a :: char itself. 256)"
   239   "card_UNIV_class.card_UNIV = (\<lambda>a :: char itself. 256)"
       
   240 
   231 
   241 instance proof
   232 instance proof
   242   fix x :: "char itself"
   233   fix x :: "char itself"
   243   show "card_UNIV x = card (UNIV :: char set)"
   234   show "card_UNIV x = card (UNIV :: char set)"
   244     by(simp add: card_UNIV_char_def card_UNIV_char)
   235     by(simp add: card_UNIV_char_def card_UNIV_char)
   248 
   239 
   249 subsubsection {* @{typ "'a \<times> 'b"} *}
   240 subsubsection {* @{typ "'a \<times> 'b"} *}
   250 
   241 
   251 instantiation prod :: (card_UNIV, card_UNIV) card_UNIV begin
   242 instantiation prod :: (card_UNIV, card_UNIV) card_UNIV begin
   252 
   243 
   253 definition card_UNIV_product_def: 
   244 definition "card_UNIV = (\<lambda>a :: ('a \<times> 'b) itself. card_UNIV (TYPE('a)) * card_UNIV (TYPE('b)))"
   254   "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<times> 'b) itself. card_UNIV (TYPE('a)) * card_UNIV (TYPE('b)))"
       
   255 
   245 
   256 instance proof
   246 instance proof
   257   fix x :: "('a \<times> 'b) itself"
   247   fix x :: "('a \<times> 'b) itself"
   258   show "card_UNIV x = card (UNIV :: ('a \<times> 'b) set)"
   248   show "card_UNIV x = card (UNIV :: ('a \<times> 'b) set)"
   259     by(simp add: card_UNIV_product_def card_UNIV UNIV_Times_UNIV[symmetric] card_cartesian_product del: UNIV_Times_UNIV)
   249     by(simp add: card_UNIV_prod_def card_UNIV UNIV_Times_UNIV[symmetric] card_cartesian_product del: UNIV_Times_UNIV)
   260 qed
   250 qed
   261 
   251 
   262 end
   252 end
   263 
   253 
   264 subsubsection {* @{typ "'a + 'b"} *}
   254 subsubsection {* @{typ "'a + 'b"} *}
   265 
   255 
   266 instantiation sum :: (card_UNIV, card_UNIV) card_UNIV begin
   256 instantiation sum :: (card_UNIV, card_UNIV) card_UNIV begin
   267 
   257 
   268 definition card_UNIV_sum_def: 
   258 definition "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a + 'b) itself. 
   269   "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a + 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
   259   let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
   270                            in if ca \<noteq> 0 \<and> cb \<noteq> 0 then ca + cb else 0)"
   260   in if ca \<noteq> 0 \<and> cb \<noteq> 0 then ca + cb else 0)"
   271 
   261 
   272 instance proof
   262 instance proof
   273   fix x :: "('a + 'b) itself"
   263   fix x :: "('a + 'b) itself"
   274   show "card_UNIV x = card (UNIV :: ('a + 'b) set)"
   264   show "card_UNIV x = card (UNIV :: ('a + 'b) set)"
   275     by (auto simp add: card_UNIV_sum_def card_UNIV card_eq_0_iff UNIV_Plus_UNIV[symmetric] finite_Plus_iff Let_def card_Plus simp del: UNIV_Plus_UNIV dest!: card_ge_0_finite)
   265     by (auto simp add: card_UNIV_sum_def card_UNIV card_eq_0_iff UNIV_Plus_UNIV[symmetric] finite_Plus_iff Let_def card_Plus simp del: UNIV_Plus_UNIV dest!: card_ge_0_finite)
   279 
   269 
   280 subsubsection {* @{typ "'a \<Rightarrow> 'b"} *}
   270 subsubsection {* @{typ "'a \<Rightarrow> 'b"} *}
   281 
   271 
   282 instantiation "fun" :: (card_UNIV, card_UNIV) card_UNIV begin
   272 instantiation "fun" :: (card_UNIV, card_UNIV) card_UNIV begin
   283 
   273 
   284 definition card_UNIV_fun_def: 
   274 definition "card_UNIV = 
   285   "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<Rightarrow> 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
   275   (\<lambda>a :: ('a \<Rightarrow> 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
   286                            in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)"
   276                             in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)"
   287 
   277 
   288 instance proof
   278 instance proof
   289   fix x :: "('a \<Rightarrow> 'b) itself"
   279   fix x :: "('a \<Rightarrow> 'b) itself"
   290 
   280 
   291   { assume "0 < card (UNIV :: 'a set)"
   281   { assume "0 < card (UNIV :: 'a set)"
   352 subsubsection {* @{typ "'a option"} *}
   342 subsubsection {* @{typ "'a option"} *}
   353 
   343 
   354 instantiation option :: (card_UNIV) card_UNIV
   344 instantiation option :: (card_UNIV) card_UNIV
   355 begin
   345 begin
   356 
   346 
   357 definition card_UNIV_option_def: 
   347 definition "card_UNIV = (\<lambda>a :: 'a option itself. let c = card_UNIV (TYPE('a)) in if c \<noteq> 0 then Suc c else 0)"
   358   "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a option itself. let c = card_UNIV (TYPE('a))
       
   359                            in if c \<noteq> 0 then Suc c else 0)"
       
   360 
   348 
   361 instance proof
   349 instance proof
   362   fix x :: "'a option itself"
   350   fix x :: "'a option itself"
   363   show "card_UNIV x = card (UNIV :: 'a option set)"
   351   show "card_UNIV x = card (UNIV :: 'a option set)"
   364     unfolding UNIV_option_conv
   352     unfolding UNIV_option_conv