src/HOL/Library/Cardinality.thy
author Andreas Lochbihler
Fri Jun 01 13:52:51 2012 +0200 (2012-06-01)
changeset 48058 11a732f7d79f
parent 48053 9bc78a08ff0a
child 48059 f6ce99d3719b
permissions -rw-r--r--
drop redundant sort constraint
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@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
definition "card_UNIV_class.card_UNIV = (\<lambda>a :: nat itself. 0)"
Andreas@48053
   150
instance by intro_classes (simp add: card_UNIV_nat_def)
Andreas@48051
   151
end
Andreas@48051
   152
Andreas@48051
   153
subsubsection {* @{typ "int"} *}
Andreas@48051
   154
Andreas@48051
   155
instantiation int :: card_UNIV begin
Andreas@48052
   156
definition "card_UNIV = (\<lambda>a :: int itself. 0)"
Andreas@48053
   157
instance by intro_classes (simp add: card_UNIV_int_def infinite_UNIV_int)
Andreas@48051
   158
end
Andreas@48051
   159
Andreas@48051
   160
subsubsection {* @{typ "'a list"} *}
Andreas@48051
   161
Andreas@48051
   162
instantiation list :: (type) card_UNIV begin
Andreas@48052
   163
definition "card_UNIV = (\<lambda>a :: 'a list itself. 0)"
Andreas@48053
   164
instance by intro_classes (simp add: card_UNIV_list_def infinite_UNIV_listI)
Andreas@48051
   165
end
Andreas@48051
   166
Andreas@48051
   167
subsubsection {* @{typ "unit"} *}
Andreas@48051
   168
Andreas@48051
   169
instantiation unit :: card_UNIV begin
Andreas@48052
   170
definition "card_UNIV = (\<lambda>a :: unit itself. 1)"
Andreas@48053
   171
instance by intro_classes (simp add: card_UNIV_unit_def card_UNIV_unit)
Andreas@48051
   172
end
Andreas@48051
   173
Andreas@48051
   174
subsubsection {* @{typ "bool"} *}
Andreas@48051
   175
Andreas@48051
   176
instantiation bool :: card_UNIV begin
Andreas@48052
   177
definition "card_UNIV = (\<lambda>a :: bool itself. 2)"
Andreas@48053
   178
instance by(intro_classes)(simp add: card_UNIV_bool_def card_UNIV_bool)
Andreas@48051
   179
end
Andreas@48051
   180
Andreas@48051
   181
subsubsection {* @{typ "char"} *}
Andreas@48051
   182
Andreas@48051
   183
lemma card_UNIV_char: "card (UNIV :: char set) = 256"
Andreas@48051
   184
proof -
Andreas@48051
   185
  from enum_distinct
Andreas@48051
   186
  have "card (set (Enum.enum :: char list)) = length (Enum.enum :: char list)"
Andreas@48051
   187
    by (rule distinct_card)
Andreas@48051
   188
  also have "set Enum.enum = (UNIV :: char set)" by (auto intro: in_enum)
Andreas@48051
   189
  also note enum_chars
Andreas@48051
   190
  finally show ?thesis by (simp add: chars_def)
Andreas@48051
   191
qed
Andreas@48051
   192
Andreas@48051
   193
instantiation char :: card_UNIV begin
Andreas@48052
   194
definition "card_UNIV_class.card_UNIV = (\<lambda>a :: char itself. 256)"
Andreas@48053
   195
instance by intro_classes (simp add: card_UNIV_char_def card_UNIV_char)
Andreas@48051
   196
end
Andreas@48051
   197
Andreas@48051
   198
subsubsection {* @{typ "'a \<times> 'b"} *}
Andreas@48051
   199
Andreas@48051
   200
instantiation prod :: (card_UNIV, card_UNIV) card_UNIV begin
Andreas@48052
   201
definition "card_UNIV = (\<lambda>a :: ('a \<times> 'b) itself. card_UNIV (TYPE('a)) * card_UNIV (TYPE('b)))"
Andreas@48053
   202
instance 
Andreas@48053
   203
  by intro_classes (simp add: card_UNIV_prod_def card_UNIV UNIV_Times_UNIV[symmetric] card_cartesian_product del: UNIV_Times_UNIV)
Andreas@48051
   204
end
Andreas@48051
   205
Andreas@48051
   206
subsubsection {* @{typ "'a + 'b"} *}
Andreas@48051
   207
Andreas@48051
   208
instantiation sum :: (card_UNIV, card_UNIV) card_UNIV begin
Andreas@48052
   209
definition "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a + 'b) itself. 
Andreas@48052
   210
  let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
Andreas@48052
   211
  in if ca \<noteq> 0 \<and> cb \<noteq> 0 then ca + cb else 0)"
Andreas@48053
   212
instance
Andreas@48053
   213
  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
   214
end
Andreas@48051
   215
Andreas@48051
   216
subsubsection {* @{typ "'a \<Rightarrow> 'b"} *}
Andreas@48051
   217
Andreas@48051
   218
instantiation "fun" :: (card_UNIV, card_UNIV) card_UNIV begin
Andreas@48051
   219
Andreas@48052
   220
definition "card_UNIV = 
Andreas@48052
   221
  (\<lambda>a :: ('a \<Rightarrow> 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
Andreas@48052
   222
                            in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)"
Andreas@48051
   223
Andreas@48051
   224
instance proof
Andreas@48051
   225
  fix x :: "('a \<Rightarrow> 'b) itself"
Andreas@48051
   226
Andreas@48051
   227
  { assume "0 < card (UNIV :: 'a set)"
Andreas@48051
   228
    and "0 < card (UNIV :: 'b set)"
Andreas@48051
   229
    hence fina: "finite (UNIV :: 'a set)" and finb: "finite (UNIV :: 'b set)"
Andreas@48051
   230
      by(simp_all only: card_ge_0_finite)
Andreas@48051
   231
    from finite_distinct_list[OF finb] obtain bs 
Andreas@48051
   232
      where bs: "set bs = (UNIV :: 'b set)" and distb: "distinct bs" by blast
Andreas@48051
   233
    from finite_distinct_list[OF fina] obtain as
Andreas@48051
   234
      where as: "set as = (UNIV :: 'a set)" and dista: "distinct as" by blast
Andreas@48051
   235
    have cb: "card (UNIV :: 'b set) = length bs"
Andreas@48051
   236
      unfolding bs[symmetric] distinct_card[OF distb] ..
Andreas@48051
   237
    have ca: "card (UNIV :: 'a set) = length as"
Andreas@48051
   238
      unfolding as[symmetric] distinct_card[OF dista] ..
Andreas@48051
   239
    let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (Enum.n_lists (length as) bs)"
Andreas@48051
   240
    have "UNIV = set ?xs"
Andreas@48051
   241
    proof(rule UNIV_eq_I)
Andreas@48051
   242
      fix f :: "'a \<Rightarrow> 'b"
Andreas@48051
   243
      from as have "f = the \<circ> map_of (zip as (map f as))"
Andreas@48053
   244
        by(auto simp add: map_of_zip_map)
Andreas@48051
   245
      thus "f \<in> set ?xs" using bs by(auto simp add: set_n_lists)
Andreas@48051
   246
    qed
Andreas@48051
   247
    moreover have "distinct ?xs" unfolding distinct_map
Andreas@48051
   248
    proof(intro conjI distinct_n_lists distb inj_onI)
Andreas@48051
   249
      fix xs ys :: "'b list"
Andreas@48051
   250
      assume xs: "xs \<in> set (Enum.n_lists (length as) bs)"
Andreas@48051
   251
        and ys: "ys \<in> set (Enum.n_lists (length as) bs)"
Andreas@48051
   252
        and eq: "the \<circ> map_of (zip as xs) = the \<circ> map_of (zip as ys)"
Andreas@48051
   253
      from xs ys have [simp]: "length xs = length as" "length ys = length as"
Andreas@48051
   254
        by(simp_all add: length_n_lists_elem)
Andreas@48051
   255
      have "map_of (zip as xs) = map_of (zip as ys)"
Andreas@48051
   256
      proof
Andreas@48051
   257
        fix x
Andreas@48051
   258
        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
   259
          by(simp_all add: map_of_zip_is_Some[symmetric])
Andreas@48051
   260
        with eq show "map_of (zip as xs) x = map_of (zip as ys) x"
Andreas@48051
   261
          by(auto dest: fun_cong[where x=x])
Andreas@48051
   262
      qed
Andreas@48051
   263
      with dista show "xs = ys" by(simp add: map_of_zip_inject)
Andreas@48051
   264
    qed
Andreas@48051
   265
    hence "card (set ?xs) = length ?xs" by(simp only: distinct_card)
Andreas@48051
   266
    moreover have "length ?xs = length bs ^ length as" by(simp add: length_n_lists)
Andreas@48051
   267
    ultimately have "card (UNIV :: ('a \<Rightarrow> 'b) set) = card (UNIV :: 'b set) ^ card (UNIV :: 'a set)"
Andreas@48051
   268
      using cb ca by simp }
Andreas@48051
   269
  moreover {
Andreas@48051
   270
    assume cb: "card (UNIV :: 'b set) = Suc 0"
Andreas@48051
   271
    then obtain b where b: "UNIV = {b :: 'b}" by(auto simp add: card_Suc_eq)
Andreas@48051
   272
    have eq: "UNIV = {\<lambda>x :: 'a. b ::'b}"
Andreas@48051
   273
    proof(rule UNIV_eq_I)
Andreas@48051
   274
      fix x :: "'a \<Rightarrow> 'b"
Andreas@48051
   275
      { fix y
Andreas@48051
   276
        have "x y \<in> UNIV" ..
Andreas@48051
   277
        hence "x y = b" unfolding b by simp }
Andreas@48053
   278
      thus "x \<in> {\<lambda>x. b}" by(auto)
Andreas@48051
   279
    qed
Andreas@48051
   280
    have "card (UNIV :: ('a \<Rightarrow> 'b) set) = Suc 0" unfolding eq by simp }
Andreas@48051
   281
  ultimately show "card_UNIV x = card (UNIV :: ('a \<Rightarrow> 'b) set)"
Andreas@48051
   282
    unfolding card_UNIV_fun_def card_UNIV Let_def
Andreas@48051
   283
    by(auto simp del: One_nat_def)(auto simp add: card_eq_0_iff dest: finite_fun_UNIVD2 finite_fun_UNIVD1)
Andreas@48051
   284
qed
Andreas@48051
   285
Andreas@48051
   286
end
Andreas@48051
   287
Andreas@48051
   288
subsubsection {* @{typ "'a option"} *}
Andreas@48051
   289
Andreas@48051
   290
instantiation option :: (card_UNIV) card_UNIV
Andreas@48051
   291
begin
Andreas@48051
   292
Andreas@48052
   293
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
   294
Andreas@48051
   295
instance proof
Andreas@48051
   296
  fix x :: "'a option itself"
Andreas@48051
   297
  show "card_UNIV x = card (UNIV :: 'a option set)"
Andreas@48053
   298
    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
   299
      (subst card_insert_disjoint, auto simp add: card_eq_0_iff card_image inj_Some intro: finite_imageI card_ge_0_finite)
Andreas@48051
   300
qed
Andreas@48051
   301
Andreas@48051
   302
end
Andreas@48051
   303
Andreas@48051
   304
subsection {* Code setup for equality on sets *}
Andreas@48051
   305
Andreas@48051
   306
definition eq_set :: "'a :: card_UNIV set \<Rightarrow> 'a :: card_UNIV set \<Rightarrow> bool"
Andreas@48051
   307
where [simp, code del]: "eq_set = op ="
Andreas@48051
   308
Andreas@48051
   309
lemmas [code_unfold] = eq_set_def[symmetric]
Andreas@48051
   310
Andreas@48051
   311
lemma card_Compl:
Andreas@48051
   312
  "finite A \<Longrightarrow> card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)"
Andreas@48051
   313
by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest)
Andreas@48051
   314
Andreas@48051
   315
lemma eq_set_code [code]:
Andreas@48051
   316
  fixes xs ys :: "'a :: card_UNIV list"
Andreas@48051
   317
  defines "rhs \<equiv> 
Andreas@48051
   318
  let n = card_UNIV TYPE('a)
Andreas@48051
   319
  in if n = 0 then False else 
Andreas@48051
   320
        let xs' = remdups xs; ys' = remdups ys 
Andreas@48051
   321
        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
   322
  shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs" (is ?thesis1)
Andreas@48051
   323
  and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs" (is ?thesis2)
Andreas@48051
   324
  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
   325
  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
   326
proof -
Andreas@48051
   327
  show ?thesis1 (is "?lhs \<longleftrightarrow> ?rhs")
Andreas@48051
   328
  proof
Andreas@48051
   329
    assume ?lhs thus ?rhs
Andreas@48051
   330
      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
   331
  next
Andreas@48051
   332
    assume ?rhs
Andreas@48051
   333
    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
   334
    ultimately show ?lhs
Andreas@48051
   335
      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
   336
  qed
Andreas@48051
   337
  thus ?thesis2 unfolding eq_set_def by blast
Andreas@48051
   338
  show ?thesis3 ?thesis4 unfolding eq_set_def List.coset_def by blast+
Andreas@48051
   339
qed
Andreas@48051
   340
Andreas@48051
   341
(* test code setup *)
Andreas@48051
   342
value [code] "List.coset [True] = set [False] \<and> set [] = List.coset [True, False]"
Andreas@48051
   343
Andreas@48051
   344
end