src/HOL/Library/Cardinality.thy
author Andreas Lochbihler
Thu May 31 16:58:38 2012 +0200 (2012-05-31)
changeset 48051 53a0df441e20
parent 47221 7205eb4a0a05
child 48052 b74766e4c11e
permissions -rw-r--r--
unify Card_Univ and Cardinality
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
huffman@30001
    47
lemma card_prod [simp]: "CARD('a \<times> 'b) = CARD('a::finite) * CARD('b::finite)"
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@48051
    91
class card_UNIV = 
Andreas@48051
    92
  fixes card_UNIV :: "'a itself \<Rightarrow> nat"
Andreas@48051
    93
  assumes card_UNIV: "card_UNIV x = card (UNIV :: 'a set)"
Andreas@48051
    94
begin
Andreas@48051
    95
Andreas@48051
    96
lemma card_UNIV_neq_0_finite_UNIV:
Andreas@48051
    97
  "card_UNIV x \<noteq> 0 \<longleftrightarrow> finite (UNIV :: 'a set)"
Andreas@48051
    98
by(simp add: card_UNIV card_eq_0_iff)
Andreas@48051
    99
Andreas@48051
   100
lemma card_UNIV_ge_0_finite_UNIV:
Andreas@48051
   101
  "card_UNIV x > 0 \<longleftrightarrow> finite (UNIV :: 'a set)"
Andreas@48051
   102
by(auto simp add: card_UNIV intro: card_ge_0_finite finite_UNIV_card_ge_0)
Andreas@48051
   103
Andreas@48051
   104
lemma card_UNIV_eq_0_infinite_UNIV:
Andreas@48051
   105
  "card_UNIV x = 0 \<longleftrightarrow> \<not> finite (UNIV :: 'a set)"
Andreas@48051
   106
by(simp add: card_UNIV card_eq_0_iff)
Andreas@48051
   107
Andreas@48051
   108
definition is_list_UNIV :: "'a list \<Rightarrow> bool"
Andreas@48051
   109
where "is_list_UNIV xs = (let c = card_UNIV (TYPE('a)) in if c = 0 then False else size (remdups xs) = c)"
Andreas@48051
   110
Andreas@48051
   111
lemma is_list_UNIV_iff: fixes xs :: "'a list"
Andreas@48051
   112
  shows "is_list_UNIV xs \<longleftrightarrow> set xs = UNIV"
Andreas@48051
   113
proof
Andreas@48051
   114
  assume "is_list_UNIV xs"
Andreas@48051
   115
  hence c: "card_UNIV (TYPE('a)) > 0" and xs: "size (remdups xs) = card_UNIV (TYPE('a))"
Andreas@48051
   116
    unfolding is_list_UNIV_def by(simp_all add: Let_def split: split_if_asm)
Andreas@48051
   117
  from c have fin: "finite (UNIV :: 'a set)" by(auto simp add: card_UNIV_ge_0_finite_UNIV)
Andreas@48051
   118
  have "card (set (remdups xs)) = size (remdups xs)" by(subst distinct_card) auto
Andreas@48051
   119
  also note set_remdups
Andreas@48051
   120
  finally show "set xs = UNIV" using fin unfolding xs card_UNIV by-(rule card_eq_UNIV_imp_eq_UNIV)
Andreas@48051
   121
next
Andreas@48051
   122
  assume xs: "set xs = UNIV"
Andreas@48051
   123
  from finite_set[of xs] have fin: "finite (UNIV :: 'a set)" unfolding xs .
Andreas@48051
   124
  hence "card_UNIV (TYPE ('a)) \<noteq> 0" unfolding card_UNIV_neq_0_finite_UNIV .
Andreas@48051
   125
  moreover have "size (remdups xs) = card (set (remdups xs))"
Andreas@48051
   126
    by(subst distinct_card) auto
Andreas@48051
   127
  ultimately show "is_list_UNIV xs" using xs by(simp add: is_list_UNIV_def Let_def card_UNIV)
Andreas@48051
   128
qed
Andreas@48051
   129
Andreas@48051
   130
lemma card_UNIV_eq_0_is_list_UNIV_False:
Andreas@48051
   131
  assumes cU0: "card_UNIV x = 0"
Andreas@48051
   132
  shows "is_list_UNIV = (\<lambda>xs. False)"
Andreas@48051
   133
proof(rule ext)
Andreas@48051
   134
  fix xs :: "'a list"
Andreas@48051
   135
  from cU0 have "\<not> finite (UNIV :: 'a set)"
Andreas@48051
   136
    by(auto simp only: card_UNIV_eq_0_infinite_UNIV)
Andreas@48051
   137
  moreover have "finite (set xs)" by(rule finite_set)
Andreas@48051
   138
  ultimately have "(UNIV :: 'a set) \<noteq> set xs" by(auto simp del: finite_set)
Andreas@48051
   139
  thus "is_list_UNIV xs = False" unfolding is_list_UNIV_iff by simp
Andreas@48051
   140
qed
Andreas@48051
   141
huffman@29997
   142
end
Andreas@48051
   143
Andreas@48051
   144
subsection {* Instantiations for @{text "card_UNIV"} *}
Andreas@48051
   145
Andreas@48051
   146
subsubsection {* @{typ "nat"} *}
Andreas@48051
   147
Andreas@48051
   148
instantiation nat :: card_UNIV begin
Andreas@48051
   149
Andreas@48051
   150
definition "card_UNIV_class.card_UNIV = (\<lambda>a :: nat itself. 0)"
Andreas@48051
   151
Andreas@48051
   152
instance proof
Andreas@48051
   153
  fix x :: "nat itself"
Andreas@48051
   154
  show "card_UNIV x = card (UNIV :: nat set)"
Andreas@48051
   155
    unfolding card_UNIV_nat_def by simp
Andreas@48051
   156
qed
Andreas@48051
   157
Andreas@48051
   158
end
Andreas@48051
   159
Andreas@48051
   160
subsubsection {* @{typ "int"} *}
Andreas@48051
   161
Andreas@48051
   162
instantiation int :: card_UNIV begin
Andreas@48051
   163
Andreas@48051
   164
definition "card_UNIV_class.card_UNIV = (\<lambda>a :: int itself. 0)"
Andreas@48051
   165
Andreas@48051
   166
instance proof
Andreas@48051
   167
  fix x :: "int itself"
Andreas@48051
   168
  show "card_UNIV x = card (UNIV :: int set)"
Andreas@48051
   169
    unfolding card_UNIV_int_def by(simp add: infinite_UNIV_int)
Andreas@48051
   170
qed
Andreas@48051
   171
Andreas@48051
   172
end
Andreas@48051
   173
Andreas@48051
   174
subsubsection {* @{typ "'a list"} *}
Andreas@48051
   175
Andreas@48051
   176
instantiation list :: (type) card_UNIV begin
Andreas@48051
   177
Andreas@48051
   178
definition "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a list itself. 0)"
Andreas@48051
   179
Andreas@48051
   180
instance proof
Andreas@48051
   181
  fix x :: "'a list itself"
Andreas@48051
   182
  show "card_UNIV x = card (UNIV :: 'a list set)"
Andreas@48051
   183
    unfolding card_UNIV_list_def by(simp add: infinite_UNIV_listI)
Andreas@48051
   184
qed
Andreas@48051
   185
Andreas@48051
   186
end
Andreas@48051
   187
Andreas@48051
   188
subsubsection {* @{typ "unit"} *}
Andreas@48051
   189
Andreas@48051
   190
lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
Andreas@48051
   191
  unfolding UNIV_unit by simp
Andreas@48051
   192
Andreas@48051
   193
instantiation unit :: card_UNIV begin
Andreas@48051
   194
Andreas@48051
   195
definition card_UNIV_unit_def: 
Andreas@48051
   196
  "card_UNIV_class.card_UNIV = (\<lambda>a :: unit itself. 1)"
Andreas@48051
   197
Andreas@48051
   198
instance proof
Andreas@48051
   199
  fix x :: "unit itself"
Andreas@48051
   200
  show "card_UNIV x = card (UNIV :: unit set)"
Andreas@48051
   201
    by(simp add: card_UNIV_unit_def card_UNIV_unit)
Andreas@48051
   202
qed
Andreas@48051
   203
Andreas@48051
   204
end
Andreas@48051
   205
Andreas@48051
   206
subsubsection {* @{typ "bool"} *}
Andreas@48051
   207
Andreas@48051
   208
lemma card_UNIV_bool: "card (UNIV :: bool set) = 2"
Andreas@48051
   209
  unfolding UNIV_bool by simp
Andreas@48051
   210
Andreas@48051
   211
instantiation bool :: card_UNIV begin
Andreas@48051
   212
Andreas@48051
   213
definition card_UNIV_bool_def: 
Andreas@48051
   214
  "card_UNIV_class.card_UNIV = (\<lambda>a :: bool itself. 2)"
Andreas@48051
   215
Andreas@48051
   216
instance proof
Andreas@48051
   217
  fix x :: "bool itself"
Andreas@48051
   218
  show "card_UNIV x = card (UNIV :: bool set)"
Andreas@48051
   219
    by(simp add: card_UNIV_bool_def card_UNIV_bool)
Andreas@48051
   220
qed
Andreas@48051
   221
Andreas@48051
   222
end
Andreas@48051
   223
Andreas@48051
   224
subsubsection {* @{typ "char"} *}
Andreas@48051
   225
Andreas@48051
   226
lemma card_UNIV_char: "card (UNIV :: char set) = 256"
Andreas@48051
   227
proof -
Andreas@48051
   228
  from enum_distinct
Andreas@48051
   229
  have "card (set (Enum.enum :: char list)) = length (Enum.enum :: char list)"
Andreas@48051
   230
    by (rule distinct_card)
Andreas@48051
   231
  also have "set Enum.enum = (UNIV :: char set)" by (auto intro: in_enum)
Andreas@48051
   232
  also note enum_chars
Andreas@48051
   233
  finally show ?thesis by (simp add: chars_def)
Andreas@48051
   234
qed
Andreas@48051
   235
Andreas@48051
   236
instantiation char :: card_UNIV begin
Andreas@48051
   237
Andreas@48051
   238
definition card_UNIV_char_def: 
Andreas@48051
   239
  "card_UNIV_class.card_UNIV = (\<lambda>a :: char itself. 256)"
Andreas@48051
   240
Andreas@48051
   241
instance proof
Andreas@48051
   242
  fix x :: "char itself"
Andreas@48051
   243
  show "card_UNIV x = card (UNIV :: char set)"
Andreas@48051
   244
    by(simp add: card_UNIV_char_def card_UNIV_char)
Andreas@48051
   245
qed
Andreas@48051
   246
Andreas@48051
   247
end
Andreas@48051
   248
Andreas@48051
   249
subsubsection {* @{typ "'a \<times> 'b"} *}
Andreas@48051
   250
Andreas@48051
   251
instantiation prod :: (card_UNIV, card_UNIV) card_UNIV begin
Andreas@48051
   252
Andreas@48051
   253
definition card_UNIV_product_def: 
Andreas@48051
   254
  "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<times> 'b) itself. card_UNIV (TYPE('a)) * card_UNIV (TYPE('b)))"
Andreas@48051
   255
Andreas@48051
   256
instance proof
Andreas@48051
   257
  fix x :: "('a \<times> 'b) itself"
Andreas@48051
   258
  show "card_UNIV x = card (UNIV :: ('a \<times> 'b) set)"
Andreas@48051
   259
    by(simp add: card_UNIV_product_def card_UNIV UNIV_Times_UNIV[symmetric] card_cartesian_product del: UNIV_Times_UNIV)
Andreas@48051
   260
qed
Andreas@48051
   261
Andreas@48051
   262
end
Andreas@48051
   263
Andreas@48051
   264
subsubsection {* @{typ "'a + 'b"} *}
Andreas@48051
   265
Andreas@48051
   266
instantiation sum :: (card_UNIV, card_UNIV) card_UNIV begin
Andreas@48051
   267
Andreas@48051
   268
definition card_UNIV_sum_def: 
Andreas@48051
   269
  "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a + 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
Andreas@48051
   270
                           in if ca \<noteq> 0 \<and> cb \<noteq> 0 then ca + cb else 0)"
Andreas@48051
   271
Andreas@48051
   272
instance proof
Andreas@48051
   273
  fix x :: "('a + 'b) itself"
Andreas@48051
   274
  show "card_UNIV x = card (UNIV :: ('a + 'b) set)"
Andreas@48051
   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)
Andreas@48051
   276
qed
Andreas@48051
   277
Andreas@48051
   278
end
Andreas@48051
   279
Andreas@48051
   280
subsubsection {* @{typ "'a \<Rightarrow> 'b"} *}
Andreas@48051
   281
Andreas@48051
   282
instantiation "fun" :: (card_UNIV, card_UNIV) card_UNIV begin
Andreas@48051
   283
Andreas@48051
   284
definition card_UNIV_fun_def: 
Andreas@48051
   285
  "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<Rightarrow> 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
Andreas@48051
   286
                           in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)"
Andreas@48051
   287
Andreas@48051
   288
instance proof
Andreas@48051
   289
  fix x :: "('a \<Rightarrow> 'b) itself"
Andreas@48051
   290
Andreas@48051
   291
  { assume "0 < card (UNIV :: 'a set)"
Andreas@48051
   292
    and "0 < card (UNIV :: 'b set)"
Andreas@48051
   293
    hence fina: "finite (UNIV :: 'a set)" and finb: "finite (UNIV :: 'b set)"
Andreas@48051
   294
      by(simp_all only: card_ge_0_finite)
Andreas@48051
   295
    from finite_distinct_list[OF finb] obtain bs 
Andreas@48051
   296
      where bs: "set bs = (UNIV :: 'b set)" and distb: "distinct bs" by blast
Andreas@48051
   297
    from finite_distinct_list[OF fina] obtain as
Andreas@48051
   298
      where as: "set as = (UNIV :: 'a set)" and dista: "distinct as" by blast
Andreas@48051
   299
    have cb: "card (UNIV :: 'b set) = length bs"
Andreas@48051
   300
      unfolding bs[symmetric] distinct_card[OF distb] ..
Andreas@48051
   301
    have ca: "card (UNIV :: 'a set) = length as"
Andreas@48051
   302
      unfolding as[symmetric] distinct_card[OF dista] ..
Andreas@48051
   303
    let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (Enum.n_lists (length as) bs)"
Andreas@48051
   304
    have "UNIV = set ?xs"
Andreas@48051
   305
    proof(rule UNIV_eq_I)
Andreas@48051
   306
      fix f :: "'a \<Rightarrow> 'b"
Andreas@48051
   307
      from as have "f = the \<circ> map_of (zip as (map f as))"
Andreas@48051
   308
        by(auto simp add: map_of_zip_map intro: ext)
Andreas@48051
   309
      thus "f \<in> set ?xs" using bs by(auto simp add: set_n_lists)
Andreas@48051
   310
    qed
Andreas@48051
   311
    moreover have "distinct ?xs" unfolding distinct_map
Andreas@48051
   312
    proof(intro conjI distinct_n_lists distb inj_onI)
Andreas@48051
   313
      fix xs ys :: "'b list"
Andreas@48051
   314
      assume xs: "xs \<in> set (Enum.n_lists (length as) bs)"
Andreas@48051
   315
        and ys: "ys \<in> set (Enum.n_lists (length as) bs)"
Andreas@48051
   316
        and eq: "the \<circ> map_of (zip as xs) = the \<circ> map_of (zip as ys)"
Andreas@48051
   317
      from xs ys have [simp]: "length xs = length as" "length ys = length as"
Andreas@48051
   318
        by(simp_all add: length_n_lists_elem)
Andreas@48051
   319
      have "map_of (zip as xs) = map_of (zip as ys)"
Andreas@48051
   320
      proof
Andreas@48051
   321
        fix x
Andreas@48051
   322
        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
   323
          by(simp_all add: map_of_zip_is_Some[symmetric])
Andreas@48051
   324
        with eq show "map_of (zip as xs) x = map_of (zip as ys) x"
Andreas@48051
   325
          by(auto dest: fun_cong[where x=x])
Andreas@48051
   326
      qed
Andreas@48051
   327
      with dista show "xs = ys" by(simp add: map_of_zip_inject)
Andreas@48051
   328
    qed
Andreas@48051
   329
    hence "card (set ?xs) = length ?xs" by(simp only: distinct_card)
Andreas@48051
   330
    moreover have "length ?xs = length bs ^ length as" by(simp add: length_n_lists)
Andreas@48051
   331
    ultimately have "card (UNIV :: ('a \<Rightarrow> 'b) set) = card (UNIV :: 'b set) ^ card (UNIV :: 'a set)"
Andreas@48051
   332
      using cb ca by simp }
Andreas@48051
   333
  moreover {
Andreas@48051
   334
    assume cb: "card (UNIV :: 'b set) = Suc 0"
Andreas@48051
   335
    then obtain b where b: "UNIV = {b :: 'b}" by(auto simp add: card_Suc_eq)
Andreas@48051
   336
    have eq: "UNIV = {\<lambda>x :: 'a. b ::'b}"
Andreas@48051
   337
    proof(rule UNIV_eq_I)
Andreas@48051
   338
      fix x :: "'a \<Rightarrow> 'b"
Andreas@48051
   339
      { fix y
Andreas@48051
   340
        have "x y \<in> UNIV" ..
Andreas@48051
   341
        hence "x y = b" unfolding b by simp }
Andreas@48051
   342
      thus "x \<in> {\<lambda>x. b}" by(auto intro: ext)
Andreas@48051
   343
    qed
Andreas@48051
   344
    have "card (UNIV :: ('a \<Rightarrow> 'b) set) = Suc 0" unfolding eq by simp }
Andreas@48051
   345
  ultimately show "card_UNIV x = card (UNIV :: ('a \<Rightarrow> 'b) set)"
Andreas@48051
   346
    unfolding card_UNIV_fun_def card_UNIV Let_def
Andreas@48051
   347
    by(auto simp del: One_nat_def)(auto simp add: card_eq_0_iff dest: finite_fun_UNIVD2 finite_fun_UNIVD1)
Andreas@48051
   348
qed
Andreas@48051
   349
Andreas@48051
   350
end
Andreas@48051
   351
Andreas@48051
   352
subsubsection {* @{typ "'a option"} *}
Andreas@48051
   353
Andreas@48051
   354
instantiation option :: (card_UNIV) card_UNIV
Andreas@48051
   355
begin
Andreas@48051
   356
Andreas@48051
   357
definition card_UNIV_option_def: 
Andreas@48051
   358
  "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a option itself. let c = card_UNIV (TYPE('a))
Andreas@48051
   359
                           in if c \<noteq> 0 then Suc c else 0)"
Andreas@48051
   360
Andreas@48051
   361
instance proof
Andreas@48051
   362
  fix x :: "'a option itself"
Andreas@48051
   363
  show "card_UNIV x = card (UNIV :: 'a option set)"
Andreas@48051
   364
    unfolding UNIV_option_conv
Andreas@48051
   365
    by(auto simp add: card_UNIV_option_def card_UNIV card_eq_0_iff Let_def intro: inj_Some dest: finite_imageD)
Andreas@48051
   366
      (subst card_insert_disjoint, auto simp add: card_eq_0_iff card_image inj_Some intro: finite_imageI card_ge_0_finite)
Andreas@48051
   367
qed
Andreas@48051
   368
Andreas@48051
   369
end
Andreas@48051
   370
Andreas@48051
   371
subsection {* Code setup for equality on sets *}
Andreas@48051
   372
Andreas@48051
   373
definition eq_set :: "'a :: card_UNIV set \<Rightarrow> 'a :: card_UNIV set \<Rightarrow> bool"
Andreas@48051
   374
where [simp, code del]: "eq_set = op ="
Andreas@48051
   375
Andreas@48051
   376
lemmas [code_unfold] = eq_set_def[symmetric]
Andreas@48051
   377
Andreas@48051
   378
lemma card_Compl:
Andreas@48051
   379
  "finite A \<Longrightarrow> card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)"
Andreas@48051
   380
by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest)
Andreas@48051
   381
Andreas@48051
   382
lemma eq_set_code [code]:
Andreas@48051
   383
  fixes xs ys :: "'a :: card_UNIV list"
Andreas@48051
   384
  defines "rhs \<equiv> 
Andreas@48051
   385
  let n = card_UNIV TYPE('a)
Andreas@48051
   386
  in if n = 0 then False else 
Andreas@48051
   387
        let xs' = remdups xs; ys' = remdups ys 
Andreas@48051
   388
        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
   389
  shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs" (is ?thesis1)
Andreas@48051
   390
  and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs" (is ?thesis2)
Andreas@48051
   391
  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
   392
  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
   393
proof -
Andreas@48051
   394
  show ?thesis1 (is "?lhs \<longleftrightarrow> ?rhs")
Andreas@48051
   395
  proof
Andreas@48051
   396
    assume ?lhs thus ?rhs
Andreas@48051
   397
      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
   398
  next
Andreas@48051
   399
    assume ?rhs
Andreas@48051
   400
    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
   401
    ultimately show ?lhs
Andreas@48051
   402
      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
   403
  qed
Andreas@48051
   404
  thus ?thesis2 unfolding eq_set_def by blast
Andreas@48051
   405
  show ?thesis3 ?thesis4 unfolding eq_set_def List.coset_def by blast+
Andreas@48051
   406
qed
Andreas@48051
   407
Andreas@48051
   408
(* test code setup *)
Andreas@48051
   409
value [code] "List.coset [True] = set [False] \<and> set [] = List.coset [True, False]"
Andreas@48051
   410
Andreas@48051
   411
end