src/HOL/Library/Cardinality.thy
author Andreas Lochbihler
Fri Jun 01 14:34:46 2012 +0200 (2012-06-01)
changeset 48059 f6ce99d3719b
parent 48058 11a732f7d79f
child 48060 1f4d00a7f59f
permissions -rw-r--r--
simplify card_UNIV type class,
tuned proofs
haftmann@37653
     1
(*  Title:      HOL/Library/Cardinality.thy
Andreas@48051
     2
    Author:     Brian Huffman, Andreas Lochbihler
kleing@24332
     3
*)
kleing@24332
     4
haftmann@37653
     5
header {* Cardinality of types *}
kleing@24332
     6
haftmann@37653
     7
theory Cardinality
huffman@47108
     8
imports "~~/src/HOL/Main"
kleing@24332
     9
begin
kleing@24332
    10
kleing@24332
    11
subsection {* Preliminary lemmas *}
kleing@24332
    12
(* These should be moved elsewhere *)
kleing@24332
    13
kleing@24332
    14
lemma (in type_definition) univ:
kleing@24332
    15
  "UNIV = Abs ` A"
kleing@24332
    16
proof
kleing@24332
    17
  show "Abs ` A \<subseteq> UNIV" by (rule subset_UNIV)
kleing@24332
    18
  show "UNIV \<subseteq> Abs ` A"
kleing@24332
    19
  proof
kleing@24332
    20
    fix x :: 'b
kleing@24332
    21
    have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric])
kleing@24332
    22
    moreover have "Rep x \<in> A" by (rule Rep)
kleing@24332
    23
    ultimately show "x \<in> Abs ` A" by (rule image_eqI)
kleing@24332
    24
  qed
kleing@24332
    25
qed
kleing@24332
    26
kleing@24332
    27
lemma (in type_definition) card: "card (UNIV :: 'b set) = card A"
kleing@24332
    28
  by (simp add: univ card_image inj_on_def Abs_inject)
kleing@24332
    29
kleing@24332
    30
kleing@24332
    31
subsection {* Cardinalities of types *}
kleing@24332
    32
kleing@24332
    33
syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
kleing@24332
    34
wenzelm@35431
    35
translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)"
kleing@24332
    36
wenzelm@42247
    37
typed_print_translation (advanced) {*
wenzelm@42247
    38
  let
wenzelm@42247
    39
    fun card_univ_tr' ctxt _ [Const (@{const_syntax UNIV}, Type (_, [T, _]))] =
wenzelm@42247
    40
      Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ ctxt T;
wenzelm@42247
    41
  in [(@{const_syntax card}, card_univ_tr')] end
huffman@24407
    42
*}
huffman@24407
    43
huffman@30001
    44
lemma card_unit [simp]: "CARD(unit) = 1"
haftmann@26153
    45
  unfolding UNIV_unit by simp
kleing@24332
    46
Andreas@48058
    47
lemma card_prod [simp]: "CARD('a \<times> 'b) = CARD('a) * CARD('b)"
haftmann@26153
    48
  unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product)
kleing@24332
    49
huffman@30001
    50
lemma card_sum [simp]: "CARD('a + 'b) = CARD('a::finite) + CARD('b::finite)"
haftmann@26153
    51
  unfolding UNIV_Plus_UNIV [symmetric] by (simp only: finite card_Plus)
kleing@24332
    52
huffman@30001
    53
lemma card_option [simp]: "CARD('a option) = Suc CARD('a::finite)"
nipkow@31080
    54
  unfolding UNIV_option_conv
kleing@24332
    55
  apply (subgoal_tac "(None::'a option) \<notin> range Some")
huffman@29997
    56
  apply (simp add: card_image)
kleing@24332
    57
  apply fast
kleing@24332
    58
  done
kleing@24332
    59
huffman@30001
    60
lemma card_set [simp]: "CARD('a set) = 2 ^ CARD('a::finite)"
haftmann@26153
    61
  unfolding Pow_UNIV [symmetric]
huffman@47221
    62
  by (simp only: card_Pow finite)
kleing@24332
    63
huffman@30001
    64
lemma card_nat [simp]: "CARD(nat) = 0"
huffman@44142
    65
  by (simp add: card_eq_0_iff)
huffman@30001
    66
huffman@30001
    67
huffman@30001
    68
subsection {* Classes with at least 1 and 2  *}
huffman@30001
    69
huffman@30001
    70
text {* Class finite already captures "at least 1" *}
huffman@30001
    71
huffman@30001
    72
lemma zero_less_card_finite [simp]: "0 < CARD('a::finite)"
huffman@29997
    73
  unfolding neq0_conv [symmetric] by simp
huffman@29997
    74
huffman@30001
    75
lemma one_le_card_finite [simp]: "Suc 0 \<le> CARD('a::finite)"
huffman@30001
    76
  by (simp add: less_Suc_eq_le [symmetric])
huffman@30001
    77
huffman@30001
    78
text {* Class for cardinality "at least 2" *}
huffman@30001
    79
huffman@30001
    80
class card2 = finite + 
huffman@30001
    81
  assumes two_le_card: "2 \<le> CARD('a)"
huffman@30001
    82
huffman@30001
    83
lemma one_less_card: "Suc 0 < CARD('a::card2)"
huffman@30001
    84
  using two_le_card [where 'a='a] by simp
huffman@30001
    85
huffman@30001
    86
lemma one_less_int_card: "1 < int CARD('a::card2)"
huffman@30001
    87
  using one_less_card [where 'a='a] by simp
huffman@30001
    88
Andreas@48051
    89
subsection {* A type class for computing the cardinality of types *}
Andreas@48051
    90
Andreas@48059
    91
definition is_list_UNIV :: "'a list \<Rightarrow> bool"
Andreas@48059
    92
where "is_list_UNIV xs = (let c = CARD('a) in if c = 0 then False else size (remdups xs) = c)"
Andreas@48059
    93
Andreas@48059
    94
lemmas [code_unfold] = is_list_UNIV_def[abs_def]
Andreas@48059
    95
Andreas@48059
    96
lemma is_list_UNIV_iff: "is_list_UNIV xs \<longleftrightarrow> set xs = UNIV"
Andreas@48059
    97
by(auto simp add: is_list_UNIV_def Let_def card_eq_0_iff List.card_set[symmetric] 
Andreas@48059
    98
   dest: subst[where P="finite", OF _ finite_set] card_eq_UNIV_imp_eq_UNIV)
Andreas@48059
    99
Andreas@48059
   100
lemma card_UNIV_eq_0_is_list_UNIV_False:
Andreas@48059
   101
  "CARD('a) = 0 \<Longrightarrow> is_list_UNIV = (\<lambda>xs :: 'a list. False)"
Andreas@48059
   102
by(simp add: is_list_UNIV_def[abs_def])
Andreas@48059
   103
Andreas@48051
   104
class card_UNIV = 
Andreas@48051
   105
  fixes card_UNIV :: "'a itself \<Rightarrow> nat"
Andreas@48059
   106
  assumes card_UNIV: "card_UNIV x = CARD('a)"
Andreas@48051
   107
Andreas@48059
   108
lemma card_UNIV_code [code_unfold]: "CARD('a :: card_UNIV) = card_UNIV TYPE('a)"
Andreas@48059
   109
by(simp add: card_UNIV)
Andreas@48051
   110
Andreas@48051
   111
subsection {* Instantiations for @{text "card_UNIV"} *}
Andreas@48051
   112
Andreas@48051
   113
subsubsection {* @{typ "nat"} *}
Andreas@48051
   114
Andreas@48051
   115
instantiation nat :: card_UNIV begin
Andreas@48051
   116
definition "card_UNIV_class.card_UNIV = (\<lambda>a :: nat itself. 0)"
Andreas@48053
   117
instance by intro_classes (simp add: card_UNIV_nat_def)
Andreas@48051
   118
end
Andreas@48051
   119
Andreas@48051
   120
subsubsection {* @{typ "int"} *}
Andreas@48051
   121
Andreas@48051
   122
instantiation int :: card_UNIV begin
Andreas@48052
   123
definition "card_UNIV = (\<lambda>a :: int itself. 0)"
Andreas@48053
   124
instance by intro_classes (simp add: card_UNIV_int_def infinite_UNIV_int)
Andreas@48051
   125
end
Andreas@48051
   126
Andreas@48051
   127
subsubsection {* @{typ "'a list"} *}
Andreas@48051
   128
Andreas@48051
   129
instantiation list :: (type) card_UNIV begin
Andreas@48052
   130
definition "card_UNIV = (\<lambda>a :: 'a list itself. 0)"
Andreas@48053
   131
instance by intro_classes (simp add: card_UNIV_list_def infinite_UNIV_listI)
Andreas@48051
   132
end
Andreas@48051
   133
Andreas@48051
   134
subsubsection {* @{typ "unit"} *}
Andreas@48051
   135
Andreas@48051
   136
instantiation unit :: card_UNIV begin
Andreas@48052
   137
definition "card_UNIV = (\<lambda>a :: unit itself. 1)"
Andreas@48053
   138
instance by intro_classes (simp add: card_UNIV_unit_def card_UNIV_unit)
Andreas@48051
   139
end
Andreas@48051
   140
Andreas@48051
   141
subsubsection {* @{typ "bool"} *}
Andreas@48051
   142
Andreas@48051
   143
instantiation bool :: card_UNIV begin
Andreas@48052
   144
definition "card_UNIV = (\<lambda>a :: bool itself. 2)"
Andreas@48053
   145
instance by(intro_classes)(simp add: card_UNIV_bool_def card_UNIV_bool)
Andreas@48051
   146
end
Andreas@48051
   147
Andreas@48051
   148
subsubsection {* @{typ "char"} *}
Andreas@48051
   149
Andreas@48051
   150
lemma card_UNIV_char: "card (UNIV :: char set) = 256"
Andreas@48051
   151
proof -
Andreas@48051
   152
  from enum_distinct
Andreas@48051
   153
  have "card (set (Enum.enum :: char list)) = length (Enum.enum :: char list)"
Andreas@48051
   154
    by (rule distinct_card)
Andreas@48051
   155
  also have "set Enum.enum = (UNIV :: char set)" by (auto intro: in_enum)
Andreas@48051
   156
  also note enum_chars
Andreas@48051
   157
  finally show ?thesis by (simp add: chars_def)
Andreas@48051
   158
qed
Andreas@48051
   159
Andreas@48051
   160
instantiation char :: card_UNIV begin
Andreas@48052
   161
definition "card_UNIV_class.card_UNIV = (\<lambda>a :: char itself. 256)"
Andreas@48053
   162
instance by intro_classes (simp add: card_UNIV_char_def card_UNIV_char)
Andreas@48051
   163
end
Andreas@48051
   164
Andreas@48051
   165
subsubsection {* @{typ "'a \<times> 'b"} *}
Andreas@48051
   166
Andreas@48051
   167
instantiation prod :: (card_UNIV, card_UNIV) card_UNIV begin
Andreas@48052
   168
definition "card_UNIV = (\<lambda>a :: ('a \<times> 'b) itself. card_UNIV (TYPE('a)) * card_UNIV (TYPE('b)))"
Andreas@48053
   169
instance 
Andreas@48053
   170
  by intro_classes (simp add: card_UNIV_prod_def card_UNIV UNIV_Times_UNIV[symmetric] card_cartesian_product del: UNIV_Times_UNIV)
Andreas@48051
   171
end
Andreas@48051
   172
Andreas@48051
   173
subsubsection {* @{typ "'a + 'b"} *}
Andreas@48051
   174
Andreas@48051
   175
instantiation sum :: (card_UNIV, card_UNIV) card_UNIV begin
Andreas@48052
   176
definition "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a + 'b) itself. 
Andreas@48052
   177
  let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
Andreas@48052
   178
  in if ca \<noteq> 0 \<and> cb \<noteq> 0 then ca + cb else 0)"
Andreas@48053
   179
instance
Andreas@48053
   180
  by intro_classes (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)
Andreas@48051
   181
end
Andreas@48051
   182
Andreas@48051
   183
subsubsection {* @{typ "'a \<Rightarrow> 'b"} *}
Andreas@48051
   184
Andreas@48051
   185
instantiation "fun" :: (card_UNIV, card_UNIV) card_UNIV begin
Andreas@48051
   186
Andreas@48052
   187
definition "card_UNIV = 
Andreas@48052
   188
  (\<lambda>a :: ('a \<Rightarrow> 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
Andreas@48052
   189
                            in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)"
Andreas@48051
   190
Andreas@48051
   191
instance proof
Andreas@48051
   192
  fix x :: "('a \<Rightarrow> 'b) itself"
Andreas@48051
   193
Andreas@48051
   194
  { assume "0 < card (UNIV :: 'a set)"
Andreas@48051
   195
    and "0 < card (UNIV :: 'b set)"
Andreas@48051
   196
    hence fina: "finite (UNIV :: 'a set)" and finb: "finite (UNIV :: 'b set)"
Andreas@48051
   197
      by(simp_all only: card_ge_0_finite)
Andreas@48051
   198
    from finite_distinct_list[OF finb] obtain bs 
Andreas@48051
   199
      where bs: "set bs = (UNIV :: 'b set)" and distb: "distinct bs" by blast
Andreas@48051
   200
    from finite_distinct_list[OF fina] obtain as
Andreas@48051
   201
      where as: "set as = (UNIV :: 'a set)" and dista: "distinct as" by blast
Andreas@48051
   202
    have cb: "card (UNIV :: 'b set) = length bs"
Andreas@48051
   203
      unfolding bs[symmetric] distinct_card[OF distb] ..
Andreas@48051
   204
    have ca: "card (UNIV :: 'a set) = length as"
Andreas@48051
   205
      unfolding as[symmetric] distinct_card[OF dista] ..
Andreas@48051
   206
    let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (Enum.n_lists (length as) bs)"
Andreas@48051
   207
    have "UNIV = set ?xs"
Andreas@48051
   208
    proof(rule UNIV_eq_I)
Andreas@48051
   209
      fix f :: "'a \<Rightarrow> 'b"
Andreas@48051
   210
      from as have "f = the \<circ> map_of (zip as (map f as))"
Andreas@48053
   211
        by(auto simp add: map_of_zip_map)
Andreas@48051
   212
      thus "f \<in> set ?xs" using bs by(auto simp add: set_n_lists)
Andreas@48051
   213
    qed
Andreas@48051
   214
    moreover have "distinct ?xs" unfolding distinct_map
Andreas@48051
   215
    proof(intro conjI distinct_n_lists distb inj_onI)
Andreas@48051
   216
      fix xs ys :: "'b list"
Andreas@48051
   217
      assume xs: "xs \<in> set (Enum.n_lists (length as) bs)"
Andreas@48051
   218
        and ys: "ys \<in> set (Enum.n_lists (length as) bs)"
Andreas@48051
   219
        and eq: "the \<circ> map_of (zip as xs) = the \<circ> map_of (zip as ys)"
Andreas@48051
   220
      from xs ys have [simp]: "length xs = length as" "length ys = length as"
Andreas@48051
   221
        by(simp_all add: length_n_lists_elem)
Andreas@48051
   222
      have "map_of (zip as xs) = map_of (zip as ys)"
Andreas@48051
   223
      proof
Andreas@48051
   224
        fix x
Andreas@48051
   225
        from as bs have "\<exists>y. map_of (zip as xs) x = Some y" "\<exists>y. map_of (zip as ys) x = Some y"
Andreas@48051
   226
          by(simp_all add: map_of_zip_is_Some[symmetric])
Andreas@48051
   227
        with eq show "map_of (zip as xs) x = map_of (zip as ys) x"
Andreas@48051
   228
          by(auto dest: fun_cong[where x=x])
Andreas@48051
   229
      qed
Andreas@48051
   230
      with dista show "xs = ys" by(simp add: map_of_zip_inject)
Andreas@48051
   231
    qed
Andreas@48051
   232
    hence "card (set ?xs) = length ?xs" by(simp only: distinct_card)
Andreas@48051
   233
    moreover have "length ?xs = length bs ^ length as" by(simp add: length_n_lists)
Andreas@48051
   234
    ultimately have "card (UNIV :: ('a \<Rightarrow> 'b) set) = card (UNIV :: 'b set) ^ card (UNIV :: 'a set)"
Andreas@48051
   235
      using cb ca by simp }
Andreas@48051
   236
  moreover {
Andreas@48051
   237
    assume cb: "card (UNIV :: 'b set) = Suc 0"
Andreas@48051
   238
    then obtain b where b: "UNIV = {b :: 'b}" by(auto simp add: card_Suc_eq)
Andreas@48051
   239
    have eq: "UNIV = {\<lambda>x :: 'a. b ::'b}"
Andreas@48051
   240
    proof(rule UNIV_eq_I)
Andreas@48051
   241
      fix x :: "'a \<Rightarrow> 'b"
Andreas@48051
   242
      { fix y
Andreas@48051
   243
        have "x y \<in> UNIV" ..
Andreas@48051
   244
        hence "x y = b" unfolding b by simp }
Andreas@48053
   245
      thus "x \<in> {\<lambda>x. b}" by(auto)
Andreas@48051
   246
    qed
Andreas@48051
   247
    have "card (UNIV :: ('a \<Rightarrow> 'b) set) = Suc 0" unfolding eq by simp }
Andreas@48051
   248
  ultimately show "card_UNIV x = card (UNIV :: ('a \<Rightarrow> 'b) set)"
Andreas@48051
   249
    unfolding card_UNIV_fun_def card_UNIV Let_def
Andreas@48051
   250
    by(auto simp del: One_nat_def)(auto simp add: card_eq_0_iff dest: finite_fun_UNIVD2 finite_fun_UNIVD1)
Andreas@48051
   251
qed
Andreas@48051
   252
Andreas@48051
   253
end
Andreas@48051
   254
Andreas@48051
   255
subsubsection {* @{typ "'a option"} *}
Andreas@48051
   256
Andreas@48051
   257
instantiation option :: (card_UNIV) card_UNIV
Andreas@48051
   258
begin
Andreas@48051
   259
Andreas@48052
   260
definition "card_UNIV = (\<lambda>a :: 'a option itself. let c = card_UNIV (TYPE('a)) in if c \<noteq> 0 then Suc c else 0)"
Andreas@48051
   261
Andreas@48051
   262
instance proof
Andreas@48051
   263
  fix x :: "'a option itself"
Andreas@48051
   264
  show "card_UNIV x = card (UNIV :: 'a option set)"
Andreas@48053
   265
    by(auto simp add: UNIV_option_conv card_UNIV_option_def card_UNIV card_eq_0_iff Let_def intro: inj_Some dest: finite_imageD)
Andreas@48051
   266
      (subst card_insert_disjoint, auto simp add: card_eq_0_iff card_image inj_Some intro: finite_imageI card_ge_0_finite)
Andreas@48051
   267
qed
Andreas@48051
   268
Andreas@48051
   269
end
Andreas@48051
   270
Andreas@48051
   271
subsection {* Code setup for equality on sets *}
Andreas@48051
   272
Andreas@48051
   273
definition eq_set :: "'a :: card_UNIV set \<Rightarrow> 'a :: card_UNIV set \<Rightarrow> bool"
Andreas@48051
   274
where [simp, code del]: "eq_set = op ="
Andreas@48051
   275
Andreas@48051
   276
lemmas [code_unfold] = eq_set_def[symmetric]
Andreas@48051
   277
Andreas@48051
   278
lemma card_Compl:
Andreas@48051
   279
  "finite A \<Longrightarrow> card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)"
Andreas@48051
   280
by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest)
Andreas@48051
   281
Andreas@48051
   282
lemma eq_set_code [code]:
Andreas@48051
   283
  fixes xs ys :: "'a :: card_UNIV list"
Andreas@48051
   284
  defines "rhs \<equiv> 
Andreas@48059
   285
  let n = CARD('a)
Andreas@48051
   286
  in if n = 0 then False else 
Andreas@48051
   287
        let xs' = remdups xs; ys' = remdups ys 
Andreas@48051
   288
        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')"
Andreas@48051
   289
  shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs" (is ?thesis1)
Andreas@48051
   290
  and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs" (is ?thesis2)
Andreas@48051
   291
  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)
Andreas@48051
   292
  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)
Andreas@48051
   293
proof -
Andreas@48051
   294
  show ?thesis1 (is "?lhs \<longleftrightarrow> ?rhs")
Andreas@48051
   295
  proof
Andreas@48051
   296
    assume ?lhs thus ?rhs
Andreas@48051
   297
      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)
Andreas@48051
   298
  next
Andreas@48051
   299
    assume ?rhs
Andreas@48051
   300
    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
Andreas@48051
   301
    ultimately show ?lhs
Andreas@48051
   302
      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)
Andreas@48051
   303
  qed
Andreas@48051
   304
  thus ?thesis2 unfolding eq_set_def by blast
Andreas@48051
   305
  show ?thesis3 ?thesis4 unfolding eq_set_def List.coset_def by blast+
Andreas@48051
   306
qed
Andreas@48051
   307
Andreas@48051
   308
(* test code setup *)
Andreas@48051
   309
value [code] "List.coset [True] = set [False] \<and> set [] = List.coset [True, False]"
Andreas@48051
   310
Andreas@48051
   311
end