unify Card_Univ and Cardinality
authorAndreas Lochbihler
Thu May 31 16:58:38 2012 +0200 (2012-05-31)
changeset 4805153a0df441e20
parent 48042 918a92d4079f
child 48052 b74766e4c11e
unify Card_Univ and Cardinality
src/HOL/IsaMakefile
src/HOL/Library/Card_Univ.thy
src/HOL/Library/Cardinality.thy
src/HOL/Library/FinFun.thy
     1.1 --- a/src/HOL/IsaMakefile	Wed May 30 16:05:21 2012 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu May 31 16:58:38 2012 +0200
     1.3 @@ -441,8 +441,7 @@
     1.4    Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy		\
     1.5    Library/AList.thy Library/AList_Mapping.thy 				\
     1.6    Library/BigO.thy Library/Binomial.thy 				\
     1.7 -  Library/Bit.thy Library/Boolean_Algebra.thy Library/Card_Univ.thy	\
     1.8 -  Library/Cardinality.thy						\
     1.9 +  Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy	\
    1.10    Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy	\
    1.11    Library/Code_Char_ord.thy Library/Code_Integer.thy			\
    1.12    Library/Code_Nat.thy Library/Code_Natural.thy				\
     2.1 --- a/src/HOL/Library/Card_Univ.thy	Wed May 30 16:05:21 2012 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,333 +0,0 @@
     2.4 -(* Author: Andreas Lochbihler, KIT *)
     2.5 -
     2.6 -header {* A type class for computing the cardinality of a type's universe *}
     2.7 -
     2.8 -theory Card_Univ imports Main begin
     2.9 -
    2.10 -subsection {* A type class for computing the cardinality of a type's universe *}
    2.11 -
    2.12 -class card_UNIV = 
    2.13 -  fixes card_UNIV :: "'a itself \<Rightarrow> nat"
    2.14 -  assumes card_UNIV: "card_UNIV x = card (UNIV :: 'a set)"
    2.15 -begin
    2.16 -
    2.17 -lemma card_UNIV_neq_0_finite_UNIV:
    2.18 -  "card_UNIV x \<noteq> 0 \<longleftrightarrow> finite (UNIV :: 'a set)"
    2.19 -by(simp add: card_UNIV card_eq_0_iff)
    2.20 -
    2.21 -lemma card_UNIV_ge_0_finite_UNIV:
    2.22 -  "card_UNIV x > 0 \<longleftrightarrow> finite (UNIV :: 'a set)"
    2.23 -by(auto simp add: card_UNIV intro: card_ge_0_finite finite_UNIV_card_ge_0)
    2.24 -
    2.25 -lemma card_UNIV_eq_0_infinite_UNIV:
    2.26 -  "card_UNIV x = 0 \<longleftrightarrow> \<not> finite (UNIV :: 'a set)"
    2.27 -by(simp add: card_UNIV card_eq_0_iff)
    2.28 -
    2.29 -definition is_list_UNIV :: "'a list \<Rightarrow> bool"
    2.30 -where "is_list_UNIV xs = (let c = card_UNIV (TYPE('a)) in if c = 0 then False else size (remdups xs) = c)"
    2.31 -
    2.32 -lemma is_list_UNIV_iff:
    2.33 -  fixes xs :: "'a list"
    2.34 -  shows "is_list_UNIV xs \<longleftrightarrow> set xs = UNIV"
    2.35 -proof
    2.36 -  assume "is_list_UNIV xs"
    2.37 -  hence c: "card_UNIV (TYPE('a)) > 0" and xs: "size (remdups xs) = card_UNIV (TYPE('a))"
    2.38 -    unfolding is_list_UNIV_def by(simp_all add: Let_def split: split_if_asm)
    2.39 -  from c have fin: "finite (UNIV :: 'a set)" by(auto simp add: card_UNIV_ge_0_finite_UNIV)
    2.40 -  have "card (set (remdups xs)) = size (remdups xs)" by(subst distinct_card) auto
    2.41 -  also note set_remdups
    2.42 -  finally show "set xs = UNIV" using fin unfolding xs card_UNIV by-(rule card_eq_UNIV_imp_eq_UNIV)
    2.43 -next
    2.44 -  assume xs: "set xs = UNIV"
    2.45 -  from finite_set[of xs] have fin: "finite (UNIV :: 'a set)" unfolding xs .
    2.46 -  hence "card_UNIV (TYPE ('a)) \<noteq> 0" unfolding card_UNIV_neq_0_finite_UNIV .
    2.47 -  moreover have "size (remdups xs) = card (set (remdups xs))"
    2.48 -    by(subst distinct_card) auto
    2.49 -  ultimately show "is_list_UNIV xs" using xs by(simp add: is_list_UNIV_def Let_def card_UNIV)
    2.50 -qed
    2.51 -
    2.52 -lemma card_UNIV_eq_0_is_list_UNIV_False:
    2.53 -  assumes cU0: "card_UNIV x = 0"
    2.54 -  shows "is_list_UNIV = (\<lambda>xs. False)"
    2.55 -proof(rule ext)
    2.56 -  fix xs :: "'a list"
    2.57 -  from cU0 have "\<not> finite (UNIV :: 'a set)"
    2.58 -    by(auto simp only: card_UNIV_eq_0_infinite_UNIV)
    2.59 -  moreover have "finite (set xs)" by(rule finite_set)
    2.60 -  ultimately have "(UNIV :: 'a set) \<noteq> set xs" by(auto simp del: finite_set)
    2.61 -  thus "is_list_UNIV xs = False" unfolding is_list_UNIV_iff by simp
    2.62 -qed
    2.63 -
    2.64 -end
    2.65 -
    2.66 -subsection {* Instantiations for @{text "card_UNIV"} *}
    2.67 -
    2.68 -subsubsection {* @{typ "nat"} *}
    2.69 -
    2.70 -instantiation nat :: card_UNIV begin
    2.71 -
    2.72 -definition card_UNIV_nat_def:
    2.73 -  "card_UNIV_class.card_UNIV = (\<lambda>a :: nat itself. 0)"
    2.74 -
    2.75 -instance proof
    2.76 -  fix x :: "nat itself"
    2.77 -  show "card_UNIV x = card (UNIV :: nat set)"
    2.78 -    unfolding card_UNIV_nat_def by simp
    2.79 -qed
    2.80 -
    2.81 -end
    2.82 -
    2.83 -subsubsection {* @{typ "int"} *}
    2.84 -
    2.85 -instantiation int :: card_UNIV begin
    2.86 -
    2.87 -definition card_UNIV_int_def:
    2.88 -  "card_UNIV_class.card_UNIV = (\<lambda>a :: int itself. 0)"
    2.89 -
    2.90 -instance proof
    2.91 -  fix x :: "int itself"
    2.92 -  show "card_UNIV x = card (UNIV :: int set)"
    2.93 -    unfolding card_UNIV_int_def by(simp add: infinite_UNIV_int)
    2.94 -qed
    2.95 -
    2.96 -end
    2.97 -
    2.98 -subsubsection {* @{typ "'a list"} *}
    2.99 -
   2.100 -instantiation list :: (type) card_UNIV begin
   2.101 -
   2.102 -definition card_UNIV_list_def:
   2.103 -  "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a list itself. 0)"
   2.104 -
   2.105 -instance proof
   2.106 -  fix x :: "'a list itself"
   2.107 -  show "card_UNIV x = card (UNIV :: 'a list set)"
   2.108 -    unfolding card_UNIV_list_def by(simp add: infinite_UNIV_listI)
   2.109 -qed
   2.110 -
   2.111 -end
   2.112 -
   2.113 -subsubsection {* @{typ "unit"} *}
   2.114 -
   2.115 -lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
   2.116 -  unfolding UNIV_unit by simp
   2.117 -
   2.118 -instantiation unit :: card_UNIV begin
   2.119 -
   2.120 -definition card_UNIV_unit_def: 
   2.121 -  "card_UNIV_class.card_UNIV = (\<lambda>a :: unit itself. 1)"
   2.122 -
   2.123 -instance proof
   2.124 -  fix x :: "unit itself"
   2.125 -  show "card_UNIV x = card (UNIV :: unit set)"
   2.126 -    by(simp add: card_UNIV_unit_def card_UNIV_unit)
   2.127 -qed
   2.128 -
   2.129 -end
   2.130 -
   2.131 -subsubsection {* @{typ "bool"} *}
   2.132 -
   2.133 -lemma card_UNIV_bool: "card (UNIV :: bool set) = 2"
   2.134 -  unfolding UNIV_bool by simp
   2.135 -
   2.136 -instantiation bool :: card_UNIV begin
   2.137 -
   2.138 -definition card_UNIV_bool_def: 
   2.139 -  "card_UNIV_class.card_UNIV = (\<lambda>a :: bool itself. 2)"
   2.140 -
   2.141 -instance proof
   2.142 -  fix x :: "bool itself"
   2.143 -  show "card_UNIV x = card (UNIV :: bool set)"
   2.144 -    by(simp add: card_UNIV_bool_def card_UNIV_bool)
   2.145 -qed
   2.146 -
   2.147 -end
   2.148 -
   2.149 -subsubsection {* @{typ "char"} *}
   2.150 -
   2.151 -lemma card_UNIV_char: "card (UNIV :: char set) = 256"
   2.152 -proof -
   2.153 -  from enum_distinct
   2.154 -  have "card (set (Enum.enum :: char list)) = length (Enum.enum :: char list)"
   2.155 -    by (rule distinct_card)
   2.156 -  also have "set Enum.enum = (UNIV :: char set)" by (auto intro: in_enum)
   2.157 -  also note enum_chars
   2.158 -  finally show ?thesis by (simp add: chars_def)
   2.159 -qed
   2.160 -
   2.161 -instantiation char :: card_UNIV begin
   2.162 -
   2.163 -definition card_UNIV_char_def: 
   2.164 -  "card_UNIV_class.card_UNIV = (\<lambda>a :: char itself. 256)"
   2.165 -
   2.166 -instance proof
   2.167 -  fix x :: "char itself"
   2.168 -  show "card_UNIV x = card (UNIV :: char set)"
   2.169 -    by(simp add: card_UNIV_char_def card_UNIV_char)
   2.170 -qed
   2.171 -
   2.172 -end
   2.173 -
   2.174 -subsubsection {* @{typ "'a \<times> 'b"} *}
   2.175 -
   2.176 -instantiation prod :: (card_UNIV, card_UNIV) card_UNIV begin
   2.177 -
   2.178 -definition card_UNIV_product_def: 
   2.179 -  "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<times> 'b) itself. card_UNIV (TYPE('a)) * card_UNIV (TYPE('b)))"
   2.180 -
   2.181 -instance proof
   2.182 -  fix x :: "('a \<times> 'b) itself"
   2.183 -  show "card_UNIV x = card (UNIV :: ('a \<times> 'b) set)"
   2.184 -    by(simp add: card_UNIV_product_def card_UNIV UNIV_Times_UNIV[symmetric] card_cartesian_product del: UNIV_Times_UNIV)
   2.185 -qed
   2.186 -
   2.187 -end
   2.188 -
   2.189 -subsubsection {* @{typ "'a + 'b"} *}
   2.190 -
   2.191 -instantiation sum :: (card_UNIV, card_UNIV) card_UNIV begin
   2.192 -
   2.193 -definition card_UNIV_sum_def: 
   2.194 -  "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a + 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
   2.195 -                           in if ca \<noteq> 0 \<and> cb \<noteq> 0 then ca + cb else 0)"
   2.196 -
   2.197 -instance proof
   2.198 -  fix x :: "('a + 'b) itself"
   2.199 -  show "card_UNIV x = card (UNIV :: ('a + 'b) set)"
   2.200 -    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)
   2.201 -qed
   2.202 -
   2.203 -end
   2.204 -
   2.205 -subsubsection {* @{typ "'a \<Rightarrow> 'b"} *}
   2.206 -
   2.207 -instantiation "fun" :: (card_UNIV, card_UNIV) card_UNIV begin
   2.208 -
   2.209 -definition card_UNIV_fun_def: 
   2.210 -  "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<Rightarrow> 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
   2.211 -                           in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)"
   2.212 -
   2.213 -instance proof
   2.214 -  fix x :: "('a \<Rightarrow> 'b) itself"
   2.215 -
   2.216 -  { assume "0 < card (UNIV :: 'a set)"
   2.217 -    and "0 < card (UNIV :: 'b set)"
   2.218 -    hence fina: "finite (UNIV :: 'a set)" and finb: "finite (UNIV :: 'b set)"
   2.219 -      by(simp_all only: card_ge_0_finite)
   2.220 -    from finite_distinct_list[OF finb] obtain bs 
   2.221 -      where bs: "set bs = (UNIV :: 'b set)" and distb: "distinct bs" by blast
   2.222 -    from finite_distinct_list[OF fina] obtain as
   2.223 -      where as: "set as = (UNIV :: 'a set)" and dista: "distinct as" by blast
   2.224 -    have cb: "card (UNIV :: 'b set) = length bs"
   2.225 -      unfolding bs[symmetric] distinct_card[OF distb] ..
   2.226 -    have ca: "card (UNIV :: 'a set) = length as"
   2.227 -      unfolding as[symmetric] distinct_card[OF dista] ..
   2.228 -    let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (Enum.n_lists (length as) bs)"
   2.229 -    have "UNIV = set ?xs"
   2.230 -    proof(rule UNIV_eq_I)
   2.231 -      fix f :: "'a \<Rightarrow> 'b"
   2.232 -      from as have "f = the \<circ> map_of (zip as (map f as))"
   2.233 -        by(auto simp add: map_of_zip_map intro: ext)
   2.234 -      thus "f \<in> set ?xs" using bs by(auto simp add: set_n_lists)
   2.235 -    qed
   2.236 -    moreover have "distinct ?xs" unfolding distinct_map
   2.237 -    proof(intro conjI distinct_n_lists distb inj_onI)
   2.238 -      fix xs ys :: "'b list"
   2.239 -      assume xs: "xs \<in> set (Enum.n_lists (length as) bs)"
   2.240 -        and ys: "ys \<in> set (Enum.n_lists (length as) bs)"
   2.241 -        and eq: "the \<circ> map_of (zip as xs) = the \<circ> map_of (zip as ys)"
   2.242 -      from xs ys have [simp]: "length xs = length as" "length ys = length as"
   2.243 -        by(simp_all add: length_n_lists_elem)
   2.244 -      have "map_of (zip as xs) = map_of (zip as ys)"
   2.245 -      proof
   2.246 -        fix x
   2.247 -        from as bs have "\<exists>y. map_of (zip as xs) x = Some y" "\<exists>y. map_of (zip as ys) x = Some y"
   2.248 -          by(simp_all add: map_of_zip_is_Some[symmetric])
   2.249 -        with eq show "map_of (zip as xs) x = map_of (zip as ys) x"
   2.250 -          by(auto dest: fun_cong[where x=x])
   2.251 -      qed
   2.252 -      with dista show "xs = ys" by(simp add: map_of_zip_inject)
   2.253 -    qed
   2.254 -    hence "card (set ?xs) = length ?xs" by(simp only: distinct_card)
   2.255 -    moreover have "length ?xs = length bs ^ length as" by(simp add: length_n_lists)
   2.256 -    ultimately have "card (UNIV :: ('a \<Rightarrow> 'b) set) = card (UNIV :: 'b set) ^ card (UNIV :: 'a set)"
   2.257 -      using cb ca by simp }
   2.258 -  moreover {
   2.259 -    assume cb: "card (UNIV :: 'b set) = Suc 0"
   2.260 -    then obtain b where b: "UNIV = {b :: 'b}" by(auto simp add: card_Suc_eq)
   2.261 -    have eq: "UNIV = {\<lambda>x :: 'a. b ::'b}"
   2.262 -    proof(rule UNIV_eq_I)
   2.263 -      fix x :: "'a \<Rightarrow> 'b"
   2.264 -      { fix y
   2.265 -        have "x y \<in> UNIV" ..
   2.266 -        hence "x y = b" unfolding b by simp }
   2.267 -      thus "x \<in> {\<lambda>x. b}" by(auto intro: ext)
   2.268 -    qed
   2.269 -    have "card (UNIV :: ('a \<Rightarrow> 'b) set) = Suc 0" unfolding eq by simp }
   2.270 -  ultimately show "card_UNIV x = card (UNIV :: ('a \<Rightarrow> 'b) set)"
   2.271 -    unfolding card_UNIV_fun_def card_UNIV Let_def
   2.272 -    by(auto simp del: One_nat_def)(auto simp add: card_eq_0_iff dest: finite_fun_UNIVD2 finite_fun_UNIVD1)
   2.273 -qed
   2.274 -
   2.275 -end
   2.276 -
   2.277 -subsubsection {* @{typ "'a option"} *}
   2.278 -
   2.279 -instantiation option :: (card_UNIV) card_UNIV
   2.280 -begin
   2.281 -
   2.282 -definition card_UNIV_option_def: 
   2.283 -  "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a option itself. let c = card_UNIV (TYPE('a))
   2.284 -                           in if c \<noteq> 0 then Suc c else 0)"
   2.285 -
   2.286 -instance proof
   2.287 -  fix x :: "'a option itself"
   2.288 -  show "card_UNIV x = card (UNIV :: 'a option set)"
   2.289 -    unfolding UNIV_option_conv
   2.290 -    by(auto simp add: card_UNIV_option_def card_UNIV card_eq_0_iff Let_def intro: inj_Some dest: finite_imageD)
   2.291 -      (subst card_insert_disjoint, auto simp add: card_eq_0_iff card_image inj_Some intro: finite_imageI card_ge_0_finite)
   2.292 -qed
   2.293 -
   2.294 -end
   2.295 -
   2.296 -subsection {* Code setup for equality on sets *}
   2.297 -
   2.298 -definition eq_set :: "'a :: card_UNIV set \<Rightarrow> 'a :: card_UNIV set \<Rightarrow> bool"
   2.299 -where [simp, code del]: "eq_set = op ="
   2.300 -
   2.301 -lemmas [code_unfold] = eq_set_def[symmetric]
   2.302 -
   2.303 -lemma card_Compl:
   2.304 -  "finite A \<Longrightarrow> card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)"
   2.305 -by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest)
   2.306 -
   2.307 -lemma eq_set_code [code]:
   2.308 -  fixes xs ys :: "'a :: card_UNIV list"
   2.309 -  defines "rhs \<equiv> 
   2.310 -  let n = card_UNIV TYPE('a)
   2.311 -  in if n = 0 then False else 
   2.312 -        let xs' = remdups xs; ys' = remdups ys 
   2.313 -        in length xs' + length ys' = n \<and> (\<forall>x \<in> set xs'. x \<notin> set ys') \<and> (\<forall>y \<in> set ys'. y \<notin> set xs')"
   2.314 -  shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs" (is ?thesis1)
   2.315 -  and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs" (is ?thesis2)
   2.316 -  and "eq_set (set xs) (set ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)" (is ?thesis3)
   2.317 -  and "eq_set (List.coset xs) (List.coset ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)" (is ?thesis4)
   2.318 -proof -
   2.319 -  show ?thesis1 (is "?lhs \<longleftrightarrow> ?rhs")
   2.320 -  proof
   2.321 -    assume ?lhs thus ?rhs
   2.322 -      by(auto simp add: rhs_def Let_def card_set[symmetric] card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set)
   2.323 -  next
   2.324 -    assume ?rhs
   2.325 -    moreover have "\<lbrakk> \<forall>y\<in>set xs. y \<notin> set ys; \<forall>x\<in>set ys. x \<notin> set xs \<rbrakk> \<Longrightarrow> set xs \<inter> set ys = {}" by blast
   2.326 -    ultimately show ?lhs
   2.327 -      by(auto simp add: rhs_def Let_def  card_set[symmetric] card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"] dest: card_eq_UNIV_imp_eq_UNIV split: split_if_asm)
   2.328 -  qed
   2.329 -  thus ?thesis2 unfolding eq_set_def by blast
   2.330 -  show ?thesis3 ?thesis4 unfolding eq_set_def List.coset_def by blast+
   2.331 -qed
   2.332 -
   2.333 -(* test code setup *)
   2.334 -value [code] "List.coset [True] = set [False] \<and> set [] = List.coset [True, False]"
   2.335 -
   2.336 -end
   2.337 \ No newline at end of file
     3.1 --- a/src/HOL/Library/Cardinality.thy	Wed May 30 16:05:21 2012 +0200
     3.2 +++ b/src/HOL/Library/Cardinality.thy	Thu May 31 16:58:38 2012 +0200
     3.3 @@ -1,5 +1,5 @@
     3.4  (*  Title:      HOL/Library/Cardinality.thy
     3.5 -    Author:     Brian Huffman
     3.6 +    Author:     Brian Huffman, Andreas Lochbihler
     3.7  *)
     3.8  
     3.9  header {* Cardinality of types *}
    3.10 @@ -86,4 +86,326 @@
    3.11  lemma one_less_int_card: "1 < int CARD('a::card2)"
    3.12    using one_less_card [where 'a='a] by simp
    3.13  
    3.14 +subsection {* A type class for computing the cardinality of types *}
    3.15 +
    3.16 +class card_UNIV = 
    3.17 +  fixes card_UNIV :: "'a itself \<Rightarrow> nat"
    3.18 +  assumes card_UNIV: "card_UNIV x = card (UNIV :: 'a set)"
    3.19 +begin
    3.20 +
    3.21 +lemma card_UNIV_neq_0_finite_UNIV:
    3.22 +  "card_UNIV x \<noteq> 0 \<longleftrightarrow> finite (UNIV :: 'a set)"
    3.23 +by(simp add: card_UNIV card_eq_0_iff)
    3.24 +
    3.25 +lemma card_UNIV_ge_0_finite_UNIV:
    3.26 +  "card_UNIV x > 0 \<longleftrightarrow> finite (UNIV :: 'a set)"
    3.27 +by(auto simp add: card_UNIV intro: card_ge_0_finite finite_UNIV_card_ge_0)
    3.28 +
    3.29 +lemma card_UNIV_eq_0_infinite_UNIV:
    3.30 +  "card_UNIV x = 0 \<longleftrightarrow> \<not> finite (UNIV :: 'a set)"
    3.31 +by(simp add: card_UNIV card_eq_0_iff)
    3.32 +
    3.33 +definition is_list_UNIV :: "'a list \<Rightarrow> bool"
    3.34 +where "is_list_UNIV xs = (let c = card_UNIV (TYPE('a)) in if c = 0 then False else size (remdups xs) = c)"
    3.35 +
    3.36 +lemma is_list_UNIV_iff: fixes xs :: "'a list"
    3.37 +  shows "is_list_UNIV xs \<longleftrightarrow> set xs = UNIV"
    3.38 +proof
    3.39 +  assume "is_list_UNIV xs"
    3.40 +  hence c: "card_UNIV (TYPE('a)) > 0" and xs: "size (remdups xs) = card_UNIV (TYPE('a))"
    3.41 +    unfolding is_list_UNIV_def by(simp_all add: Let_def split: split_if_asm)
    3.42 +  from c have fin: "finite (UNIV :: 'a set)" by(auto simp add: card_UNIV_ge_0_finite_UNIV)
    3.43 +  have "card (set (remdups xs)) = size (remdups xs)" by(subst distinct_card) auto
    3.44 +  also note set_remdups
    3.45 +  finally show "set xs = UNIV" using fin unfolding xs card_UNIV by-(rule card_eq_UNIV_imp_eq_UNIV)
    3.46 +next
    3.47 +  assume xs: "set xs = UNIV"
    3.48 +  from finite_set[of xs] have fin: "finite (UNIV :: 'a set)" unfolding xs .
    3.49 +  hence "card_UNIV (TYPE ('a)) \<noteq> 0" unfolding card_UNIV_neq_0_finite_UNIV .
    3.50 +  moreover have "size (remdups xs) = card (set (remdups xs))"
    3.51 +    by(subst distinct_card) auto
    3.52 +  ultimately show "is_list_UNIV xs" using xs by(simp add: is_list_UNIV_def Let_def card_UNIV)
    3.53 +qed
    3.54 +
    3.55 +lemma card_UNIV_eq_0_is_list_UNIV_False:
    3.56 +  assumes cU0: "card_UNIV x = 0"
    3.57 +  shows "is_list_UNIV = (\<lambda>xs. False)"
    3.58 +proof(rule ext)
    3.59 +  fix xs :: "'a list"
    3.60 +  from cU0 have "\<not> finite (UNIV :: 'a set)"
    3.61 +    by(auto simp only: card_UNIV_eq_0_infinite_UNIV)
    3.62 +  moreover have "finite (set xs)" by(rule finite_set)
    3.63 +  ultimately have "(UNIV :: 'a set) \<noteq> set xs" by(auto simp del: finite_set)
    3.64 +  thus "is_list_UNIV xs = False" unfolding is_list_UNIV_iff by simp
    3.65 +qed
    3.66 +
    3.67  end
    3.68 +
    3.69 +subsection {* Instantiations for @{text "card_UNIV"} *}
    3.70 +
    3.71 +subsubsection {* @{typ "nat"} *}
    3.72 +
    3.73 +instantiation nat :: card_UNIV begin
    3.74 +
    3.75 +definition "card_UNIV_class.card_UNIV = (\<lambda>a :: nat itself. 0)"
    3.76 +
    3.77 +instance proof
    3.78 +  fix x :: "nat itself"
    3.79 +  show "card_UNIV x = card (UNIV :: nat set)"
    3.80 +    unfolding card_UNIV_nat_def by simp
    3.81 +qed
    3.82 +
    3.83 +end
    3.84 +
    3.85 +subsubsection {* @{typ "int"} *}
    3.86 +
    3.87 +instantiation int :: card_UNIV begin
    3.88 +
    3.89 +definition "card_UNIV_class.card_UNIV = (\<lambda>a :: int itself. 0)"
    3.90 +
    3.91 +instance proof
    3.92 +  fix x :: "int itself"
    3.93 +  show "card_UNIV x = card (UNIV :: int set)"
    3.94 +    unfolding card_UNIV_int_def by(simp add: infinite_UNIV_int)
    3.95 +qed
    3.96 +
    3.97 +end
    3.98 +
    3.99 +subsubsection {* @{typ "'a list"} *}
   3.100 +
   3.101 +instantiation list :: (type) card_UNIV begin
   3.102 +
   3.103 +definition "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a list itself. 0)"
   3.104 +
   3.105 +instance proof
   3.106 +  fix x :: "'a list itself"
   3.107 +  show "card_UNIV x = card (UNIV :: 'a list set)"
   3.108 +    unfolding card_UNIV_list_def by(simp add: infinite_UNIV_listI)
   3.109 +qed
   3.110 +
   3.111 +end
   3.112 +
   3.113 +subsubsection {* @{typ "unit"} *}
   3.114 +
   3.115 +lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
   3.116 +  unfolding UNIV_unit by simp
   3.117 +
   3.118 +instantiation unit :: card_UNIV begin
   3.119 +
   3.120 +definition card_UNIV_unit_def: 
   3.121 +  "card_UNIV_class.card_UNIV = (\<lambda>a :: unit itself. 1)"
   3.122 +
   3.123 +instance proof
   3.124 +  fix x :: "unit itself"
   3.125 +  show "card_UNIV x = card (UNIV :: unit set)"
   3.126 +    by(simp add: card_UNIV_unit_def card_UNIV_unit)
   3.127 +qed
   3.128 +
   3.129 +end
   3.130 +
   3.131 +subsubsection {* @{typ "bool"} *}
   3.132 +
   3.133 +lemma card_UNIV_bool: "card (UNIV :: bool set) = 2"
   3.134 +  unfolding UNIV_bool by simp
   3.135 +
   3.136 +instantiation bool :: card_UNIV begin
   3.137 +
   3.138 +definition card_UNIV_bool_def: 
   3.139 +  "card_UNIV_class.card_UNIV = (\<lambda>a :: bool itself. 2)"
   3.140 +
   3.141 +instance proof
   3.142 +  fix x :: "bool itself"
   3.143 +  show "card_UNIV x = card (UNIV :: bool set)"
   3.144 +    by(simp add: card_UNIV_bool_def card_UNIV_bool)
   3.145 +qed
   3.146 +
   3.147 +end
   3.148 +
   3.149 +subsubsection {* @{typ "char"} *}
   3.150 +
   3.151 +lemma card_UNIV_char: "card (UNIV :: char set) = 256"
   3.152 +proof -
   3.153 +  from enum_distinct
   3.154 +  have "card (set (Enum.enum :: char list)) = length (Enum.enum :: char list)"
   3.155 +    by (rule distinct_card)
   3.156 +  also have "set Enum.enum = (UNIV :: char set)" by (auto intro: in_enum)
   3.157 +  also note enum_chars
   3.158 +  finally show ?thesis by (simp add: chars_def)
   3.159 +qed
   3.160 +
   3.161 +instantiation char :: card_UNIV begin
   3.162 +
   3.163 +definition card_UNIV_char_def: 
   3.164 +  "card_UNIV_class.card_UNIV = (\<lambda>a :: char itself. 256)"
   3.165 +
   3.166 +instance proof
   3.167 +  fix x :: "char itself"
   3.168 +  show "card_UNIV x = card (UNIV :: char set)"
   3.169 +    by(simp add: card_UNIV_char_def card_UNIV_char)
   3.170 +qed
   3.171 +
   3.172 +end
   3.173 +
   3.174 +subsubsection {* @{typ "'a \<times> 'b"} *}
   3.175 +
   3.176 +instantiation prod :: (card_UNIV, card_UNIV) card_UNIV begin
   3.177 +
   3.178 +definition card_UNIV_product_def: 
   3.179 +  "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<times> 'b) itself. card_UNIV (TYPE('a)) * card_UNIV (TYPE('b)))"
   3.180 +
   3.181 +instance proof
   3.182 +  fix x :: "('a \<times> 'b) itself"
   3.183 +  show "card_UNIV x = card (UNIV :: ('a \<times> 'b) set)"
   3.184 +    by(simp add: card_UNIV_product_def card_UNIV UNIV_Times_UNIV[symmetric] card_cartesian_product del: UNIV_Times_UNIV)
   3.185 +qed
   3.186 +
   3.187 +end
   3.188 +
   3.189 +subsubsection {* @{typ "'a + 'b"} *}
   3.190 +
   3.191 +instantiation sum :: (card_UNIV, card_UNIV) card_UNIV begin
   3.192 +
   3.193 +definition card_UNIV_sum_def: 
   3.194 +  "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a + 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
   3.195 +                           in if ca \<noteq> 0 \<and> cb \<noteq> 0 then ca + cb else 0)"
   3.196 +
   3.197 +instance proof
   3.198 +  fix x :: "('a + 'b) itself"
   3.199 +  show "card_UNIV x = card (UNIV :: ('a + 'b) set)"
   3.200 +    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)
   3.201 +qed
   3.202 +
   3.203 +end
   3.204 +
   3.205 +subsubsection {* @{typ "'a \<Rightarrow> 'b"} *}
   3.206 +
   3.207 +instantiation "fun" :: (card_UNIV, card_UNIV) card_UNIV begin
   3.208 +
   3.209 +definition card_UNIV_fun_def: 
   3.210 +  "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<Rightarrow> 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
   3.211 +                           in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)"
   3.212 +
   3.213 +instance proof
   3.214 +  fix x :: "('a \<Rightarrow> 'b) itself"
   3.215 +
   3.216 +  { assume "0 < card (UNIV :: 'a set)"
   3.217 +    and "0 < card (UNIV :: 'b set)"
   3.218 +    hence fina: "finite (UNIV :: 'a set)" and finb: "finite (UNIV :: 'b set)"
   3.219 +      by(simp_all only: card_ge_0_finite)
   3.220 +    from finite_distinct_list[OF finb] obtain bs 
   3.221 +      where bs: "set bs = (UNIV :: 'b set)" and distb: "distinct bs" by blast
   3.222 +    from finite_distinct_list[OF fina] obtain as
   3.223 +      where as: "set as = (UNIV :: 'a set)" and dista: "distinct as" by blast
   3.224 +    have cb: "card (UNIV :: 'b set) = length bs"
   3.225 +      unfolding bs[symmetric] distinct_card[OF distb] ..
   3.226 +    have ca: "card (UNIV :: 'a set) = length as"
   3.227 +      unfolding as[symmetric] distinct_card[OF dista] ..
   3.228 +    let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (Enum.n_lists (length as) bs)"
   3.229 +    have "UNIV = set ?xs"
   3.230 +    proof(rule UNIV_eq_I)
   3.231 +      fix f :: "'a \<Rightarrow> 'b"
   3.232 +      from as have "f = the \<circ> map_of (zip as (map f as))"
   3.233 +        by(auto simp add: map_of_zip_map intro: ext)
   3.234 +      thus "f \<in> set ?xs" using bs by(auto simp add: set_n_lists)
   3.235 +    qed
   3.236 +    moreover have "distinct ?xs" unfolding distinct_map
   3.237 +    proof(intro conjI distinct_n_lists distb inj_onI)
   3.238 +      fix xs ys :: "'b list"
   3.239 +      assume xs: "xs \<in> set (Enum.n_lists (length as) bs)"
   3.240 +        and ys: "ys \<in> set (Enum.n_lists (length as) bs)"
   3.241 +        and eq: "the \<circ> map_of (zip as xs) = the \<circ> map_of (zip as ys)"
   3.242 +      from xs ys have [simp]: "length xs = length as" "length ys = length as"
   3.243 +        by(simp_all add: length_n_lists_elem)
   3.244 +      have "map_of (zip as xs) = map_of (zip as ys)"
   3.245 +      proof
   3.246 +        fix x
   3.247 +        from as bs have "\<exists>y. map_of (zip as xs) x = Some y" "\<exists>y. map_of (zip as ys) x = Some y"
   3.248 +          by(simp_all add: map_of_zip_is_Some[symmetric])
   3.249 +        with eq show "map_of (zip as xs) x = map_of (zip as ys) x"
   3.250 +          by(auto dest: fun_cong[where x=x])
   3.251 +      qed
   3.252 +      with dista show "xs = ys" by(simp add: map_of_zip_inject)
   3.253 +    qed
   3.254 +    hence "card (set ?xs) = length ?xs" by(simp only: distinct_card)
   3.255 +    moreover have "length ?xs = length bs ^ length as" by(simp add: length_n_lists)
   3.256 +    ultimately have "card (UNIV :: ('a \<Rightarrow> 'b) set) = card (UNIV :: 'b set) ^ card (UNIV :: 'a set)"
   3.257 +      using cb ca by simp }
   3.258 +  moreover {
   3.259 +    assume cb: "card (UNIV :: 'b set) = Suc 0"
   3.260 +    then obtain b where b: "UNIV = {b :: 'b}" by(auto simp add: card_Suc_eq)
   3.261 +    have eq: "UNIV = {\<lambda>x :: 'a. b ::'b}"
   3.262 +    proof(rule UNIV_eq_I)
   3.263 +      fix x :: "'a \<Rightarrow> 'b"
   3.264 +      { fix y
   3.265 +        have "x y \<in> UNIV" ..
   3.266 +        hence "x y = b" unfolding b by simp }
   3.267 +      thus "x \<in> {\<lambda>x. b}" by(auto intro: ext)
   3.268 +    qed
   3.269 +    have "card (UNIV :: ('a \<Rightarrow> 'b) set) = Suc 0" unfolding eq by simp }
   3.270 +  ultimately show "card_UNIV x = card (UNIV :: ('a \<Rightarrow> 'b) set)"
   3.271 +    unfolding card_UNIV_fun_def card_UNIV Let_def
   3.272 +    by(auto simp del: One_nat_def)(auto simp add: card_eq_0_iff dest: finite_fun_UNIVD2 finite_fun_UNIVD1)
   3.273 +qed
   3.274 +
   3.275 +end
   3.276 +
   3.277 +subsubsection {* @{typ "'a option"} *}
   3.278 +
   3.279 +instantiation option :: (card_UNIV) card_UNIV
   3.280 +begin
   3.281 +
   3.282 +definition card_UNIV_option_def: 
   3.283 +  "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a option itself. let c = card_UNIV (TYPE('a))
   3.284 +                           in if c \<noteq> 0 then Suc c else 0)"
   3.285 +
   3.286 +instance proof
   3.287 +  fix x :: "'a option itself"
   3.288 +  show "card_UNIV x = card (UNIV :: 'a option set)"
   3.289 +    unfolding UNIV_option_conv
   3.290 +    by(auto simp add: card_UNIV_option_def card_UNIV card_eq_0_iff Let_def intro: inj_Some dest: finite_imageD)
   3.291 +      (subst card_insert_disjoint, auto simp add: card_eq_0_iff card_image inj_Some intro: finite_imageI card_ge_0_finite)
   3.292 +qed
   3.293 +
   3.294 +end
   3.295 +
   3.296 +subsection {* Code setup for equality on sets *}
   3.297 +
   3.298 +definition eq_set :: "'a :: card_UNIV set \<Rightarrow> 'a :: card_UNIV set \<Rightarrow> bool"
   3.299 +where [simp, code del]: "eq_set = op ="
   3.300 +
   3.301 +lemmas [code_unfold] = eq_set_def[symmetric]
   3.302 +
   3.303 +lemma card_Compl:
   3.304 +  "finite A \<Longrightarrow> card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)"
   3.305 +by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest)
   3.306 +
   3.307 +lemma eq_set_code [code]:
   3.308 +  fixes xs ys :: "'a :: card_UNIV list"
   3.309 +  defines "rhs \<equiv> 
   3.310 +  let n = card_UNIV TYPE('a)
   3.311 +  in if n = 0 then False else 
   3.312 +        let xs' = remdups xs; ys' = remdups ys 
   3.313 +        in length xs' + length ys' = n \<and> (\<forall>x \<in> set xs'. x \<notin> set ys') \<and> (\<forall>y \<in> set ys'. y \<notin> set xs')"
   3.314 +  shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs" (is ?thesis1)
   3.315 +  and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs" (is ?thesis2)
   3.316 +  and "eq_set (set xs) (set ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)" (is ?thesis3)
   3.317 +  and "eq_set (List.coset xs) (List.coset ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)" (is ?thesis4)
   3.318 +proof -
   3.319 +  show ?thesis1 (is "?lhs \<longleftrightarrow> ?rhs")
   3.320 +  proof
   3.321 +    assume ?lhs thus ?rhs
   3.322 +      by(auto simp add: rhs_def Let_def List.card_set[symmetric] card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set)
   3.323 +  next
   3.324 +    assume ?rhs
   3.325 +    moreover have "\<lbrakk> \<forall>y\<in>set xs. y \<notin> set ys; \<forall>x\<in>set ys. x \<notin> set xs \<rbrakk> \<Longrightarrow> set xs \<inter> set ys = {}" by blast
   3.326 +    ultimately show ?lhs
   3.327 +      by(auto simp add: rhs_def Let_def List.card_set[symmetric] card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"] dest: card_eq_UNIV_imp_eq_UNIV split: split_if_asm)
   3.328 +  qed
   3.329 +  thus ?thesis2 unfolding eq_set_def by blast
   3.330 +  show ?thesis3 ?thesis4 unfolding eq_set_def List.coset_def by blast+
   3.331 +qed
   3.332 +
   3.333 +(* test code setup *)
   3.334 +value [code] "List.coset [True] = set [False] \<and> set [] = List.coset [True, False]"
   3.335 +
   3.336 +end
     4.1 --- a/src/HOL/Library/FinFun.thy	Wed May 30 16:05:21 2012 +0200
     4.2 +++ b/src/HOL/Library/FinFun.thy	Thu May 31 16:58:38 2012 +0200
     4.3 @@ -3,7 +3,7 @@
     4.4  header {* Almost everywhere constant functions *}
     4.5  
     4.6  theory FinFun
     4.7 -imports Card_Univ
     4.8 +imports Cardinality
     4.9  begin
    4.10  
    4.11  text {*