src/HOL/Library/Cardinality.thy
changeset 48176 3d9c1ddb9f47
parent 48165 d07a0b9601aa
child 49689 b8a710806de9
     1.1 --- a/src/HOL/Library/Cardinality.thy	Tue Jul 03 09:25:42 2012 +0200
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Tue Jul 03 09:26:52 2012 +0200
     1.3 @@ -30,6 +30,12 @@
     1.4  lemma finite_range_Some: "finite (range (Some :: 'a \<Rightarrow> 'a option)) = finite (UNIV :: 'a set)"
     1.5  by(auto dest: finite_imageD intro: inj_Some)
     1.6  
     1.7 +lemma infinite_literal: "\<not> finite (UNIV :: String.literal set)"
     1.8 +proof -
     1.9 +  have "inj STR" by(auto intro: injI)
    1.10 +  thus ?thesis
    1.11 +    by(auto simp add: type_definition.univ[OF type_definition_literal] infinite_UNIV_listI dest: finite_imageD)
    1.12 +qed
    1.13  
    1.14  subsection {* Cardinalities of types *}
    1.15  
    1.16 @@ -131,6 +137,18 @@
    1.17      by(auto simp del: One_nat_def)(auto simp add: card_eq_0_iff dest: finite_fun_UNIVD2 finite_fun_UNIVD1)
    1.18  qed
    1.19  
    1.20 +corollary finite_UNIV_fun:
    1.21 +  "finite (UNIV :: ('a \<Rightarrow> 'b) set) \<longleftrightarrow>
    1.22 +   finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set) \<or> CARD('b) = 1"
    1.23 +  (is "?lhs \<longleftrightarrow> ?rhs")
    1.24 +proof -
    1.25 +  have "?lhs \<longleftrightarrow> CARD('a \<Rightarrow> 'b) > 0" by(simp add: card_gt_0_iff)
    1.26 +  also have "\<dots> \<longleftrightarrow> CARD('a) > 0 \<and> CARD('b) > 0 \<or> CARD('b) = 1"
    1.27 +    by(simp add: card_fun)
    1.28 +  also have "\<dots> = ?rhs" by(simp add: card_gt_0_iff)
    1.29 +  finally show ?thesis .
    1.30 +qed
    1.31 +
    1.32  lemma card_nibble: "CARD(nibble) = 16"
    1.33  unfolding UNIV_nibble by simp
    1.34  
    1.35 @@ -141,10 +159,7 @@
    1.36  qed
    1.37  
    1.38  lemma card_literal: "CARD(String.literal) = 0"
    1.39 -proof -
    1.40 -  have "inj STR" by(auto intro: injI)
    1.41 -  thus ?thesis by(simp add: type_definition.univ[OF type_definition_literal] card_image infinite_UNIV_listI)
    1.42 -qed
    1.43 +by(simp add: card_eq_0_iff infinite_literal)
    1.44  
    1.45  subsection {* Classes with at least 1 and 2  *}
    1.46  
    1.47 @@ -167,6 +182,20 @@
    1.48  lemma one_less_int_card: "1 < int CARD('a::card2)"
    1.49    using one_less_card [where 'a='a] by simp
    1.50  
    1.51 +
    1.52 +subsection {* A type class for deciding finiteness of types *}
    1.53 +
    1.54 +type_synonym 'a finite_UNIV = "('a, bool) phantom"
    1.55 +
    1.56 +class finite_UNIV = 
    1.57 +  fixes finite_UNIV :: "('a, bool) phantom"
    1.58 +  assumes finite_UNIV: "finite_UNIV = Phantom('a) (finite (UNIV :: 'a set))"
    1.59 +
    1.60 +lemma finite_UNIV_code [code_unfold]:
    1.61 +  "finite (UNIV :: 'a :: finite_UNIV set)
    1.62 +  \<longleftrightarrow> of_phantom (finite_UNIV :: 'a finite_UNIV)"
    1.63 +by(simp add: finite_UNIV)
    1.64 +
    1.65  subsection {* A type class for computing the cardinality of types *}
    1.66  
    1.67  definition is_list_UNIV :: "'a list \<Rightarrow> bool"
    1.68 @@ -178,7 +207,7 @@
    1.69  
    1.70  type_synonym 'a card_UNIV = "('a, nat) phantom"
    1.71  
    1.72 -class card_UNIV = 
    1.73 +class card_UNIV = finite_UNIV +
    1.74    fixes card_UNIV :: "'a card_UNIV"
    1.75    assumes card_UNIV: "card_UNIV = Phantom('a) CARD('a)"
    1.76  
    1.77 @@ -191,60 +220,76 @@
    1.78    (let c = CARD('a :: card_UNIV) in if c = 0 then False else size (remdups xs) = c)"
    1.79  by(rule is_list_UNIV_def)
    1.80  
    1.81 -lemma finite_UNIV_conv_card_UNIV [code_unfold]:
    1.82 -  "finite (UNIV :: 'a :: card_UNIV set) \<longleftrightarrow> 
    1.83 -  of_phantom (card_UNIV :: 'a card_UNIV) > 0"
    1.84 -by(simp add: card_UNIV card_gt_0_iff)
    1.85 -
    1.86  subsection {* Instantiations for @{text "card_UNIV"} *}
    1.87  
    1.88  instantiation nat :: card_UNIV begin
    1.89 +definition "finite_UNIV = Phantom(nat) False"
    1.90  definition "card_UNIV = Phantom(nat) 0"
    1.91 -instance by intro_classes (simp add: card_UNIV_nat_def)
    1.92 +instance by intro_classes (simp_all add: finite_UNIV_nat_def card_UNIV_nat_def)
    1.93  end
    1.94  
    1.95  instantiation int :: card_UNIV begin
    1.96 +definition "finite_UNIV = Phantom(int) False"
    1.97  definition "card_UNIV = Phantom(int) 0"
    1.98 -instance by intro_classes (simp add: card_UNIV_int_def infinite_UNIV_int)
    1.99 +instance by intro_classes (simp_all add: card_UNIV_int_def finite_UNIV_int_def infinite_UNIV_int)
   1.100  end
   1.101  
   1.102  instantiation code_numeral :: card_UNIV begin
   1.103 +definition "finite_UNIV = Phantom(code_numeral) False"
   1.104  definition "card_UNIV = Phantom(code_numeral) 0"
   1.105 -instance 
   1.106 -  by(intro_classes)(auto simp add: card_UNIV_code_numeral_def type_definition.univ[OF type_definition_code_numeral] card_eq_0_iff dest!: finite_imageD intro: inj_onI)
   1.107 +instance
   1.108 +  by(intro_classes)(auto simp add: card_UNIV_code_numeral_def finite_UNIV_code_numeral_def type_definition.univ[OF type_definition_code_numeral] card_eq_0_iff dest!: finite_imageD intro: inj_onI)
   1.109  end
   1.110  
   1.111  instantiation list :: (type) card_UNIV begin
   1.112 +definition "finite_UNIV = Phantom('a list) False"
   1.113  definition "card_UNIV = Phantom('a list) 0"
   1.114 -instance by intro_classes (simp add: card_UNIV_list_def infinite_UNIV_listI)
   1.115 +instance by intro_classes (simp_all add: card_UNIV_list_def finite_UNIV_list_def infinite_UNIV_listI)
   1.116  end
   1.117  
   1.118  instantiation unit :: card_UNIV begin
   1.119 +definition "finite_UNIV = Phantom(unit) True"
   1.120  definition "card_UNIV = Phantom(unit) 1"
   1.121 -instance by intro_classes (simp add: card_UNIV_unit_def card_UNIV_unit)
   1.122 +instance by intro_classes (simp_all add: card_UNIV_unit_def finite_UNIV_unit_def)
   1.123  end
   1.124  
   1.125  instantiation bool :: card_UNIV begin
   1.126 +definition "finite_UNIV = Phantom(bool) True"
   1.127  definition "card_UNIV = Phantom(bool) 2"
   1.128 -instance by(intro_classes)(simp add: card_UNIV_bool_def card_UNIV_bool)
   1.129 +instance by(intro_classes)(simp_all add: card_UNIV_bool_def finite_UNIV_bool_def)
   1.130  end
   1.131  
   1.132  instantiation nibble :: card_UNIV begin
   1.133 +definition "finite_UNIV = Phantom(nibble) True"
   1.134  definition "card_UNIV = Phantom(nibble) 16"
   1.135 -instance by(intro_classes)(simp add: card_UNIV_nibble_def card_nibble)
   1.136 +instance by(intro_classes)(simp_all add: card_UNIV_nibble_def card_nibble finite_UNIV_nibble_def)
   1.137  end
   1.138  
   1.139  instantiation char :: card_UNIV begin
   1.140 +definition "finite_UNIV = Phantom(char) True"
   1.141  definition "card_UNIV = Phantom(char) 256"
   1.142 -instance by intro_classes (simp add: card_UNIV_char_def card_UNIV_char)
   1.143 +instance by intro_classes (simp_all add: card_UNIV_char_def card_UNIV_char finite_UNIV_char_def)
   1.144 +end
   1.145 +
   1.146 +instantiation prod :: (finite_UNIV, finite_UNIV) finite_UNIV begin
   1.147 +definition "finite_UNIV = Phantom('a \<times> 'b) 
   1.148 +  (of_phantom (finite_UNIV :: 'a finite_UNIV) \<and> of_phantom (finite_UNIV :: 'b finite_UNIV))"
   1.149 +instance by intro_classes (simp add: finite_UNIV_prod_def finite_UNIV finite_prod)
   1.150  end
   1.151  
   1.152  instantiation prod :: (card_UNIV, card_UNIV) card_UNIV begin
   1.153 -definition "card_UNIV = 
   1.154 -  Phantom('a \<times> 'b) (of_phantom (card_UNIV :: 'a card_UNIV) * of_phantom (card_UNIV :: 'b card_UNIV))"
   1.155 +definition "card_UNIV = Phantom('a \<times> 'b) 
   1.156 +  (of_phantom (card_UNIV :: 'a card_UNIV) * of_phantom (card_UNIV :: 'b card_UNIV))"
   1.157  instance by intro_classes (simp add: card_UNIV_prod_def card_UNIV)
   1.158  end
   1.159  
   1.160 +instantiation sum :: (finite_UNIV, finite_UNIV) finite_UNIV begin
   1.161 +definition "finite_UNIV = Phantom('a + 'b)
   1.162 +  (of_phantom (finite_UNIV :: 'a finite_UNIV) \<and> of_phantom (finite_UNIV :: 'b finite_UNIV))"
   1.163 +instance
   1.164 +  by intro_classes (simp add: UNIV_Plus_UNIV[symmetric] finite_UNIV_sum_def finite_UNIV del: UNIV_Plus_UNIV)
   1.165 +end
   1.166 +
   1.167  instantiation sum :: (card_UNIV, card_UNIV) card_UNIV begin
   1.168  definition "card_UNIV = Phantom('a + 'b)
   1.169    (let ca = of_phantom (card_UNIV :: 'a card_UNIV); 
   1.170 @@ -253,6 +298,14 @@
   1.171  instance by intro_classes (auto simp add: card_UNIV_sum_def card_UNIV card_UNIV_sum)
   1.172  end
   1.173  
   1.174 +instantiation "fun" :: (finite_UNIV, card_UNIV) finite_UNIV begin
   1.175 +definition "finite_UNIV = Phantom('a \<Rightarrow> 'b)
   1.176 +  (let cb = of_phantom (card_UNIV :: 'b card_UNIV)
   1.177 +   in cb = 1 \<or> of_phantom (finite_UNIV :: 'a finite_UNIV) \<and> cb \<noteq> 0)"
   1.178 +instance
   1.179 +  by intro_classes (auto simp add: finite_UNIV_fun_def Let_def card_UNIV finite_UNIV finite_UNIV_fun card_gt_0_iff)
   1.180 +end
   1.181 +
   1.182  instantiation "fun" :: (card_UNIV, card_UNIV) card_UNIV begin
   1.183  definition "card_UNIV = Phantom('a \<Rightarrow> 'b)
   1.184    (let ca = of_phantom (card_UNIV :: 'a card_UNIV);
   1.185 @@ -261,6 +314,11 @@
   1.186  instance by intro_classes (simp add: card_UNIV_fun_def card_UNIV Let_def card_fun)
   1.187  end
   1.188  
   1.189 +instantiation option :: (finite_UNIV) finite_UNIV begin
   1.190 +definition "finite_UNIV = Phantom('a option) (of_phantom (finite_UNIV :: 'a finite_UNIV))"
   1.191 +instance by intro_classes (simp add: finite_UNIV_option_def finite_UNIV)
   1.192 +end
   1.193 +
   1.194  instantiation option :: (card_UNIV) card_UNIV begin
   1.195  definition "card_UNIV = Phantom('a option)
   1.196    (let c = of_phantom (card_UNIV :: 'a card_UNIV) in if c \<noteq> 0 then Suc c else 0)"
   1.197 @@ -268,8 +326,15 @@
   1.198  end
   1.199  
   1.200  instantiation String.literal :: card_UNIV begin
   1.201 +definition "finite_UNIV = Phantom(String.literal) False"
   1.202  definition "card_UNIV = Phantom(String.literal) 0"
   1.203 -instance by intro_classes (simp add: card_UNIV_literal_def card_literal)
   1.204 +instance
   1.205 +  by intro_classes (simp_all add: card_UNIV_literal_def finite_UNIV_literal_def infinite_literal card_literal)
   1.206 +end
   1.207 +
   1.208 +instantiation set :: (finite_UNIV) finite_UNIV begin
   1.209 +definition "finite_UNIV = Phantom('a set) (of_phantom (finite_UNIV :: 'a finite_UNIV))"
   1.210 +instance by intro_classes (simp add: finite_UNIV_set_def finite_UNIV Finite_Set.finite_set)
   1.211  end
   1.212  
   1.213  instantiation set :: (card_UNIV) card_UNIV begin
   1.214 @@ -278,7 +343,6 @@
   1.215  instance by intro_classes (simp add: card_UNIV_set_def card_UNIV_set card_UNIV)
   1.216  end
   1.217  
   1.218 -
   1.219  lemma UNIV_finite_1: "UNIV = set [finite_1.a\<^isub>1]"
   1.220  by(auto intro: finite_1.exhaust)
   1.221  
   1.222 @@ -296,28 +360,38 @@
   1.223  by(auto intro: finite_5.exhaust)
   1.224  
   1.225  instantiation Enum.finite_1 :: card_UNIV begin
   1.226 +definition "finite_UNIV = Phantom(Enum.finite_1) True"
   1.227  definition "card_UNIV = Phantom(Enum.finite_1) 1"
   1.228 -instance by intro_classes (simp add: UNIV_finite_1 card_UNIV_finite_1_def)
   1.229 +instance
   1.230 +  by intro_classes (simp_all add: UNIV_finite_1 card_UNIV_finite_1_def finite_UNIV_finite_1_def)
   1.231  end
   1.232  
   1.233  instantiation Enum.finite_2 :: card_UNIV begin
   1.234 +definition "finite_UNIV = Phantom(Enum.finite_2) True"
   1.235  definition "card_UNIV = Phantom(Enum.finite_2) 2"
   1.236 -instance by intro_classes (simp add: UNIV_finite_2 card_UNIV_finite_2_def)
   1.237 +instance
   1.238 +  by intro_classes (simp_all add: UNIV_finite_2 card_UNIV_finite_2_def finite_UNIV_finite_2_def)
   1.239  end
   1.240  
   1.241  instantiation Enum.finite_3 :: card_UNIV begin
   1.242 +definition "finite_UNIV = Phantom(Enum.finite_3) True"
   1.243  definition "card_UNIV = Phantom(Enum.finite_3) 3"
   1.244 -instance by intro_classes (simp add: UNIV_finite_3 card_UNIV_finite_3_def)
   1.245 +instance
   1.246 +  by intro_classes (simp_all add: UNIV_finite_3 card_UNIV_finite_3_def finite_UNIV_finite_3_def)
   1.247  end
   1.248  
   1.249  instantiation Enum.finite_4 :: card_UNIV begin
   1.250 +definition "finite_UNIV = Phantom(Enum.finite_4) True"
   1.251  definition "card_UNIV = Phantom(Enum.finite_4) 4"
   1.252 -instance by intro_classes (simp add: UNIV_finite_4 card_UNIV_finite_4_def)
   1.253 +instance
   1.254 +  by intro_classes (simp_all add: UNIV_finite_4 card_UNIV_finite_4_def finite_UNIV_finite_4_def)
   1.255  end
   1.256  
   1.257  instantiation Enum.finite_5 :: card_UNIV begin
   1.258 +definition "finite_UNIV = Phantom(Enum.finite_5) True"
   1.259  definition "card_UNIV = Phantom(Enum.finite_5) 5"
   1.260 -instance by intro_classes (simp add: UNIV_finite_5 card_UNIV_finite_5_def)
   1.261 +instance
   1.262 +  by intro_classes (simp_all add: UNIV_finite_5 card_UNIV_finite_5_def finite_UNIV_finite_5_def)
   1.263  end
   1.264  
   1.265  subsection {* Code setup for sets *}
   1.266 @@ -346,8 +420,8 @@
   1.267  
   1.268  lemma finite'_code [code]:
   1.269    "finite' (set xs) \<longleftrightarrow> True"
   1.270 -  "finite' (List.coset xs) \<longleftrightarrow> CARD('a) > 0"
   1.271 -by(simp_all add: card_gt_0_iff)
   1.272 +  "finite' (List.coset xs) \<longleftrightarrow> of_phantom (finite_UNIV :: 'a finite_UNIV)"
   1.273 +by(simp_all add: card_gt_0_iff finite_UNIV)
   1.274  
   1.275  definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
   1.276  where [simp, code del, code_abbrev]: "subset' = op \<subseteq>"