1.1 --- a/src/HOL/Finite_Set.thy Mon Jul 02 12:23:30 2012 +0200
1.2 +++ b/src/HOL/Finite_Set.thy Tue Jul 03 13:56:12 2012 +0200
1.3 @@ -404,6 +404,11 @@
1.4 by (auto simp add: finite_conv_nat_seg_image)
1.5 qed
1.6
1.7 +lemma finite_prod:
1.8 + "finite (UNIV :: ('a \<times> 'b) set) \<longleftrightarrow> finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set)"
1.9 +by(auto simp add: UNIV_Times_UNIV[symmetric] simp del: UNIV_Times_UNIV
1.10 + dest: finite_cartesian_productD1 finite_cartesian_productD2)
1.11 +
1.12 lemma finite_Pow_iff [iff]:
1.13 "finite (Pow A) \<longleftrightarrow> finite A"
1.14 proof
1.15 @@ -420,6 +425,9 @@
1.16 "finite A \<Longrightarrow> finite {B. B \<subseteq> A}"
1.17 by (simp add: Pow_def [symmetric])
1.18
1.19 +lemma finite_set: "finite (UNIV :: 'a set set) \<longleftrightarrow> finite (UNIV :: 'a set)"
1.20 +by(simp only: finite_Pow_iff Pow_UNIV[symmetric])
1.21 +
1.22 lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A"
1.23 by (blast intro: finite_subset [OF subset_Pow_Union])
1.24
2.1 --- a/src/HOL/Library/Cardinality.thy Mon Jul 02 12:23:30 2012 +0200
2.2 +++ b/src/HOL/Library/Cardinality.thy Tue Jul 03 13:56:12 2012 +0200
2.3 @@ -30,6 +30,12 @@
2.4 lemma finite_range_Some: "finite (range (Some :: 'a \<Rightarrow> 'a option)) = finite (UNIV :: 'a set)"
2.5 by(auto dest: finite_imageD intro: inj_Some)
2.6
2.7 +lemma infinite_literal: "\<not> finite (UNIV :: String.literal set)"
2.8 +proof -
2.9 + have "inj STR" by(auto intro: injI)
2.10 + thus ?thesis
2.11 + by(auto simp add: type_definition.univ[OF type_definition_literal] infinite_UNIV_listI dest: finite_imageD)
2.12 +qed
2.13
2.14 subsection {* Cardinalities of types *}
2.15
2.16 @@ -131,6 +137,18 @@
2.17 by(auto simp del: One_nat_def)(auto simp add: card_eq_0_iff dest: finite_fun_UNIVD2 finite_fun_UNIVD1)
2.18 qed
2.19
2.20 +corollary finite_UNIV_fun:
2.21 + "finite (UNIV :: ('a \<Rightarrow> 'b) set) \<longleftrightarrow>
2.22 + finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set) \<or> CARD('b) = 1"
2.23 + (is "?lhs \<longleftrightarrow> ?rhs")
2.24 +proof -
2.25 + have "?lhs \<longleftrightarrow> CARD('a \<Rightarrow> 'b) > 0" by(simp add: card_gt_0_iff)
2.26 + also have "\<dots> \<longleftrightarrow> CARD('a) > 0 \<and> CARD('b) > 0 \<or> CARD('b) = 1"
2.27 + by(simp add: card_fun)
2.28 + also have "\<dots> = ?rhs" by(simp add: card_gt_0_iff)
2.29 + finally show ?thesis .
2.30 +qed
2.31 +
2.32 lemma card_nibble: "CARD(nibble) = 16"
2.33 unfolding UNIV_nibble by simp
2.34
2.35 @@ -141,10 +159,7 @@
2.36 qed
2.37
2.38 lemma card_literal: "CARD(String.literal) = 0"
2.39 -proof -
2.40 - have "inj STR" by(auto intro: injI)
2.41 - thus ?thesis by(simp add: type_definition.univ[OF type_definition_literal] card_image infinite_UNIV_listI)
2.42 -qed
2.43 +by(simp add: card_eq_0_iff infinite_literal)
2.44
2.45 subsection {* Classes with at least 1 and 2 *}
2.46
2.47 @@ -167,6 +182,20 @@
2.48 lemma one_less_int_card: "1 < int CARD('a::card2)"
2.49 using one_less_card [where 'a='a] by simp
2.50
2.51 +
2.52 +subsection {* A type class for deciding finiteness of types *}
2.53 +
2.54 +type_synonym 'a finite_UNIV = "('a, bool) phantom"
2.55 +
2.56 +class finite_UNIV =
2.57 + fixes finite_UNIV :: "('a, bool) phantom"
2.58 + assumes finite_UNIV: "finite_UNIV = Phantom('a) (finite (UNIV :: 'a set))"
2.59 +
2.60 +lemma finite_UNIV_code [code_unfold]:
2.61 + "finite (UNIV :: 'a :: finite_UNIV set)
2.62 + \<longleftrightarrow> of_phantom (finite_UNIV :: 'a finite_UNIV)"
2.63 +by(simp add: finite_UNIV)
2.64 +
2.65 subsection {* A type class for computing the cardinality of types *}
2.66
2.67 definition is_list_UNIV :: "'a list \<Rightarrow> bool"
2.68 @@ -178,7 +207,7 @@
2.69
2.70 type_synonym 'a card_UNIV = "('a, nat) phantom"
2.71
2.72 -class card_UNIV =
2.73 +class card_UNIV = finite_UNIV +
2.74 fixes card_UNIV :: "'a card_UNIV"
2.75 assumes card_UNIV: "card_UNIV = Phantom('a) CARD('a)"
2.76
2.77 @@ -191,60 +220,76 @@
2.78 (let c = CARD('a :: card_UNIV) in if c = 0 then False else size (remdups xs) = c)"
2.79 by(rule is_list_UNIV_def)
2.80
2.81 -lemma finite_UNIV_conv_card_UNIV [code_unfold]:
2.82 - "finite (UNIV :: 'a :: card_UNIV set) \<longleftrightarrow>
2.83 - of_phantom (card_UNIV :: 'a card_UNIV) > 0"
2.84 -by(simp add: card_UNIV card_gt_0_iff)
2.85 -
2.86 subsection {* Instantiations for @{text "card_UNIV"} *}
2.87
2.88 instantiation nat :: card_UNIV begin
2.89 +definition "finite_UNIV = Phantom(nat) False"
2.90 definition "card_UNIV = Phantom(nat) 0"
2.91 -instance by intro_classes (simp add: card_UNIV_nat_def)
2.92 +instance by intro_classes (simp_all add: finite_UNIV_nat_def card_UNIV_nat_def)
2.93 end
2.94
2.95 instantiation int :: card_UNIV begin
2.96 +definition "finite_UNIV = Phantom(int) False"
2.97 definition "card_UNIV = Phantom(int) 0"
2.98 -instance by intro_classes (simp add: card_UNIV_int_def infinite_UNIV_int)
2.99 +instance by intro_classes (simp_all add: card_UNIV_int_def finite_UNIV_int_def infinite_UNIV_int)
2.100 end
2.101
2.102 instantiation code_numeral :: card_UNIV begin
2.103 +definition "finite_UNIV = Phantom(code_numeral) False"
2.104 definition "card_UNIV = Phantom(code_numeral) 0"
2.105 -instance
2.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)
2.107 +instance
2.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)
2.109 end
2.110
2.111 instantiation list :: (type) card_UNIV begin
2.112 +definition "finite_UNIV = Phantom('a list) False"
2.113 definition "card_UNIV = Phantom('a list) 0"
2.114 -instance by intro_classes (simp add: card_UNIV_list_def infinite_UNIV_listI)
2.115 +instance by intro_classes (simp_all add: card_UNIV_list_def finite_UNIV_list_def infinite_UNIV_listI)
2.116 end
2.117
2.118 instantiation unit :: card_UNIV begin
2.119 +definition "finite_UNIV = Phantom(unit) True"
2.120 definition "card_UNIV = Phantom(unit) 1"
2.121 -instance by intro_classes (simp add: card_UNIV_unit_def card_UNIV_unit)
2.122 +instance by intro_classes (simp_all add: card_UNIV_unit_def finite_UNIV_unit_def)
2.123 end
2.124
2.125 instantiation bool :: card_UNIV begin
2.126 +definition "finite_UNIV = Phantom(bool) True"
2.127 definition "card_UNIV = Phantom(bool) 2"
2.128 -instance by(intro_classes)(simp add: card_UNIV_bool_def card_UNIV_bool)
2.129 +instance by(intro_classes)(simp_all add: card_UNIV_bool_def finite_UNIV_bool_def)
2.130 end
2.131
2.132 instantiation nibble :: card_UNIV begin
2.133 +definition "finite_UNIV = Phantom(nibble) True"
2.134 definition "card_UNIV = Phantom(nibble) 16"
2.135 -instance by(intro_classes)(simp add: card_UNIV_nibble_def card_nibble)
2.136 +instance by(intro_classes)(simp_all add: card_UNIV_nibble_def card_nibble finite_UNIV_nibble_def)
2.137 end
2.138
2.139 instantiation char :: card_UNIV begin
2.140 +definition "finite_UNIV = Phantom(char) True"
2.141 definition "card_UNIV = Phantom(char) 256"
2.142 -instance by intro_classes (simp add: card_UNIV_char_def card_UNIV_char)
2.143 +instance by intro_classes (simp_all add: card_UNIV_char_def card_UNIV_char finite_UNIV_char_def)
2.144 +end
2.145 +
2.146 +instantiation prod :: (finite_UNIV, finite_UNIV) finite_UNIV begin
2.147 +definition "finite_UNIV = Phantom('a \<times> 'b)
2.148 + (of_phantom (finite_UNIV :: 'a finite_UNIV) \<and> of_phantom (finite_UNIV :: 'b finite_UNIV))"
2.149 +instance by intro_classes (simp add: finite_UNIV_prod_def finite_UNIV finite_prod)
2.150 end
2.151
2.152 instantiation prod :: (card_UNIV, card_UNIV) card_UNIV begin
2.153 -definition "card_UNIV =
2.154 - Phantom('a \<times> 'b) (of_phantom (card_UNIV :: 'a card_UNIV) * of_phantom (card_UNIV :: 'b card_UNIV))"
2.155 +definition "card_UNIV = Phantom('a \<times> 'b)
2.156 + (of_phantom (card_UNIV :: 'a card_UNIV) * of_phantom (card_UNIV :: 'b card_UNIV))"
2.157 instance by intro_classes (simp add: card_UNIV_prod_def card_UNIV)
2.158 end
2.159
2.160 +instantiation sum :: (finite_UNIV, finite_UNIV) finite_UNIV begin
2.161 +definition "finite_UNIV = Phantom('a + 'b)
2.162 + (of_phantom (finite_UNIV :: 'a finite_UNIV) \<and> of_phantom (finite_UNIV :: 'b finite_UNIV))"
2.163 +instance
2.164 + by intro_classes (simp add: UNIV_Plus_UNIV[symmetric] finite_UNIV_sum_def finite_UNIV del: UNIV_Plus_UNIV)
2.165 +end
2.166 +
2.167 instantiation sum :: (card_UNIV, card_UNIV) card_UNIV begin
2.168 definition "card_UNIV = Phantom('a + 'b)
2.169 (let ca = of_phantom (card_UNIV :: 'a card_UNIV);
2.170 @@ -253,6 +298,14 @@
2.171 instance by intro_classes (auto simp add: card_UNIV_sum_def card_UNIV card_UNIV_sum)
2.172 end
2.173
2.174 +instantiation "fun" :: (finite_UNIV, card_UNIV) finite_UNIV begin
2.175 +definition "finite_UNIV = Phantom('a \<Rightarrow> 'b)
2.176 + (let cb = of_phantom (card_UNIV :: 'b card_UNIV)
2.177 + in cb = 1 \<or> of_phantom (finite_UNIV :: 'a finite_UNIV) \<and> cb \<noteq> 0)"
2.178 +instance
2.179 + by intro_classes (auto simp add: finite_UNIV_fun_def Let_def card_UNIV finite_UNIV finite_UNIV_fun card_gt_0_iff)
2.180 +end
2.181 +
2.182 instantiation "fun" :: (card_UNIV, card_UNIV) card_UNIV begin
2.183 definition "card_UNIV = Phantom('a \<Rightarrow> 'b)
2.184 (let ca = of_phantom (card_UNIV :: 'a card_UNIV);
2.185 @@ -261,6 +314,11 @@
2.186 instance by intro_classes (simp add: card_UNIV_fun_def card_UNIV Let_def card_fun)
2.187 end
2.188
2.189 +instantiation option :: (finite_UNIV) finite_UNIV begin
2.190 +definition "finite_UNIV = Phantom('a option) (of_phantom (finite_UNIV :: 'a finite_UNIV))"
2.191 +instance by intro_classes (simp add: finite_UNIV_option_def finite_UNIV)
2.192 +end
2.193 +
2.194 instantiation option :: (card_UNIV) card_UNIV begin
2.195 definition "card_UNIV = Phantom('a option)
2.196 (let c = of_phantom (card_UNIV :: 'a card_UNIV) in if c \<noteq> 0 then Suc c else 0)"
2.197 @@ -268,8 +326,15 @@
2.198 end
2.199
2.200 instantiation String.literal :: card_UNIV begin
2.201 +definition "finite_UNIV = Phantom(String.literal) False"
2.202 definition "card_UNIV = Phantom(String.literal) 0"
2.203 -instance by intro_classes (simp add: card_UNIV_literal_def card_literal)
2.204 +instance
2.205 + by intro_classes (simp_all add: card_UNIV_literal_def finite_UNIV_literal_def infinite_literal card_literal)
2.206 +end
2.207 +
2.208 +instantiation set :: (finite_UNIV) finite_UNIV begin
2.209 +definition "finite_UNIV = Phantom('a set) (of_phantom (finite_UNIV :: 'a finite_UNIV))"
2.210 +instance by intro_classes (simp add: finite_UNIV_set_def finite_UNIV Finite_Set.finite_set)
2.211 end
2.212
2.213 instantiation set :: (card_UNIV) card_UNIV begin
2.214 @@ -278,7 +343,6 @@
2.215 instance by intro_classes (simp add: card_UNIV_set_def card_UNIV_set card_UNIV)
2.216 end
2.217
2.218 -
2.219 lemma UNIV_finite_1: "UNIV = set [finite_1.a\<^isub>1]"
2.220 by(auto intro: finite_1.exhaust)
2.221
2.222 @@ -296,28 +360,38 @@
2.223 by(auto intro: finite_5.exhaust)
2.224
2.225 instantiation Enum.finite_1 :: card_UNIV begin
2.226 +definition "finite_UNIV = Phantom(Enum.finite_1) True"
2.227 definition "card_UNIV = Phantom(Enum.finite_1) 1"
2.228 -instance by intro_classes (simp add: UNIV_finite_1 card_UNIV_finite_1_def)
2.229 +instance
2.230 + by intro_classes (simp_all add: UNIV_finite_1 card_UNIV_finite_1_def finite_UNIV_finite_1_def)
2.231 end
2.232
2.233 instantiation Enum.finite_2 :: card_UNIV begin
2.234 +definition "finite_UNIV = Phantom(Enum.finite_2) True"
2.235 definition "card_UNIV = Phantom(Enum.finite_2) 2"
2.236 -instance by intro_classes (simp add: UNIV_finite_2 card_UNIV_finite_2_def)
2.237 +instance
2.238 + by intro_classes (simp_all add: UNIV_finite_2 card_UNIV_finite_2_def finite_UNIV_finite_2_def)
2.239 end
2.240
2.241 instantiation Enum.finite_3 :: card_UNIV begin
2.242 +definition "finite_UNIV = Phantom(Enum.finite_3) True"
2.243 definition "card_UNIV = Phantom(Enum.finite_3) 3"
2.244 -instance by intro_classes (simp add: UNIV_finite_3 card_UNIV_finite_3_def)
2.245 +instance
2.246 + by intro_classes (simp_all add: UNIV_finite_3 card_UNIV_finite_3_def finite_UNIV_finite_3_def)
2.247 end
2.248
2.249 instantiation Enum.finite_4 :: card_UNIV begin
2.250 +definition "finite_UNIV = Phantom(Enum.finite_4) True"
2.251 definition "card_UNIV = Phantom(Enum.finite_4) 4"
2.252 -instance by intro_classes (simp add: UNIV_finite_4 card_UNIV_finite_4_def)
2.253 +instance
2.254 + by intro_classes (simp_all add: UNIV_finite_4 card_UNIV_finite_4_def finite_UNIV_finite_4_def)
2.255 end
2.256
2.257 instantiation Enum.finite_5 :: card_UNIV begin
2.258 +definition "finite_UNIV = Phantom(Enum.finite_5) True"
2.259 definition "card_UNIV = Phantom(Enum.finite_5) 5"
2.260 -instance by intro_classes (simp add: UNIV_finite_5 card_UNIV_finite_5_def)
2.261 +instance
2.262 + by intro_classes (simp_all add: UNIV_finite_5 card_UNIV_finite_5_def finite_UNIV_finite_5_def)
2.263 end
2.264
2.265 subsection {* Code setup for sets *}
2.266 @@ -346,8 +420,8 @@
2.267
2.268 lemma finite'_code [code]:
2.269 "finite' (set xs) \<longleftrightarrow> True"
2.270 - "finite' (List.coset xs) \<longleftrightarrow> CARD('a) > 0"
2.271 -by(simp_all add: card_gt_0_iff)
2.272 + "finite' (List.coset xs) \<longleftrightarrow> of_phantom (finite_UNIV :: 'a finite_UNIV)"
2.273 +by(simp_all add: card_gt_0_iff finite_UNIV)
2.274
2.275 definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
2.276 where [simp, code del, code_abbrev]: "subset' = op \<subseteq>"