src/HOL/Finite_Set.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 63982 4c4049e3bad8
child 67443 3abf6a722518
permissions -rw-r--r--
executable domain membership checks
wenzelm@12396
     1
(*  Title:      HOL/Finite_Set.thy
wenzelm@63612
     2
    Author:     Tobias Nipkow
wenzelm@63612
     3
    Author:     Lawrence C Paulson
wenzelm@63612
     4
    Author:     Markus Wenzel
wenzelm@63612
     5
    Author:     Jeremy Avigad
wenzelm@63612
     6
    Author:     Andrei Popescu
wenzelm@12396
     7
*)
wenzelm@12396
     8
wenzelm@60758
     9
section \<open>Finite sets\<close>
wenzelm@12396
    10
nipkow@15131
    11
theory Finite_Set
wenzelm@63612
    12
  imports Product_Type Sum_Type Fields
nipkow@15131
    13
begin
wenzelm@12396
    14
wenzelm@60758
    15
subsection \<open>Predicate for finite sets\<close>
wenzelm@12396
    16
wenzelm@63612
    17
context notes [[inductive_internals]]
wenzelm@61681
    18
begin
wenzelm@61681
    19
haftmann@41656
    20
inductive finite :: "'a set \<Rightarrow> bool"
wenzelm@63612
    21
  where
wenzelm@63612
    22
    emptyI [simp, intro!]: "finite {}"
wenzelm@63612
    23
  | insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)"
haftmann@41656
    24
wenzelm@61681
    25
end
wenzelm@61681
    26
wenzelm@60758
    27
simproc_setup finite_Collect ("finite (Collect P)") = \<open>K Set_Comprehension_Pointfree.simproc\<close>
rafal@48109
    28
traytel@54611
    29
declare [[simproc del: finite_Collect]]
traytel@54611
    30
haftmann@41656
    31
lemma finite_induct [case_names empty insert, induct set: finite]:
wenzelm@61799
    32
  \<comment> \<open>Discharging \<open>x \<notin> F\<close> entails extra work.\<close>
haftmann@41656
    33
  assumes "finite F"
haftmann@41656
    34
  assumes "P {}"
haftmann@41656
    35
    and insert: "\<And>x F. finite F \<Longrightarrow> x \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert x F)"
haftmann@41656
    36
  shows "P F"
wenzelm@63404
    37
  using \<open>finite F\<close>
wenzelm@46898
    38
proof induct
haftmann@41656
    39
  show "P {}" by fact
wenzelm@63404
    40
next
wenzelm@63404
    41
  fix x F
wenzelm@63404
    42
  assume F: "finite F" and P: "P F"
haftmann@41656
    43
  show "P (insert x F)"
haftmann@41656
    44
  proof cases
haftmann@41656
    45
    assume "x \<in> F"
wenzelm@63404
    46
    then have "insert x F = F" by (rule insert_absorb)
haftmann@41656
    47
    with P show ?thesis by (simp only:)
haftmann@41656
    48
  next
haftmann@41656
    49
    assume "x \<notin> F"
haftmann@41656
    50
    from F this P show ?thesis by (rule insert)
haftmann@41656
    51
  qed
haftmann@41656
    52
qed
haftmann@41656
    53
haftmann@51622
    54
lemma infinite_finite_induct [case_names infinite empty insert]:
haftmann@51622
    55
  assumes infinite: "\<And>A. \<not> finite A \<Longrightarrow> P A"
wenzelm@63404
    56
    and empty: "P {}"
wenzelm@63404
    57
    and insert: "\<And>x F. finite F \<Longrightarrow> x \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert x F)"
haftmann@51622
    58
  shows "P A"
haftmann@51622
    59
proof (cases "finite A")
wenzelm@63404
    60
  case False
wenzelm@63404
    61
  with infinite show ?thesis .
haftmann@51622
    62
next
wenzelm@63404
    63
  case True
wenzelm@63404
    64
  then show ?thesis by (induct A) (fact empty insert)+
haftmann@51622
    65
qed
haftmann@51622
    66
haftmann@41656
    67
wenzelm@60758
    68
subsubsection \<open>Choice principles\<close>
wenzelm@12396
    69
wenzelm@61799
    70
lemma ex_new_if_finite: \<comment> "does not depend on def of finite at all"
wenzelm@14661
    71
  assumes "\<not> finite (UNIV :: 'a set)" and "finite A"
wenzelm@14661
    72
  shows "\<exists>a::'a. a \<notin> A"
wenzelm@14661
    73
proof -
haftmann@28823
    74
  from assms have "A \<noteq> UNIV" by blast
haftmann@41656
    75
  then show ?thesis by blast
wenzelm@12396
    76
qed
wenzelm@12396
    77
wenzelm@60758
    78
text \<open>A finite choice principle. Does not need the SOME choice operator.\<close>
nipkow@15484
    79
wenzelm@63404
    80
lemma finite_set_choice: "finite A \<Longrightarrow> \<forall>x\<in>A. \<exists>y. P x y \<Longrightarrow> \<exists>f. \<forall>x\<in>A. P x (f x)"
haftmann@41656
    81
proof (induct rule: finite_induct)
wenzelm@63404
    82
  case empty
wenzelm@63404
    83
  then show ?case by simp
nipkow@29923
    84
next
nipkow@29923
    85
  case (insert a A)
wenzelm@63404
    86
  then obtain f b where f: "\<forall>x\<in>A. P x (f x)" and ab: "P a b"
wenzelm@63404
    87
    by auto
wenzelm@63404
    88
  show ?case (is "\<exists>f. ?P f")
nipkow@29923
    89
  proof
wenzelm@63404
    90
    show "?P (\<lambda>x. if x = a then b else f x)"
wenzelm@63404
    91
      using f ab by auto
nipkow@29923
    92
  qed
nipkow@29923
    93
qed
nipkow@29923
    94
haftmann@23878
    95
wenzelm@60758
    96
subsubsection \<open>Finite sets are the images of initial segments of natural numbers\<close>
nipkow@15392
    97
paulson@15510
    98
lemma finite_imp_nat_seg_image_inj_on:
wenzelm@63404
    99
  assumes "finite A"
haftmann@41656
   100
  shows "\<exists>(n::nat) f. A = f ` {i. i < n} \<and> inj_on f {i. i < n}"
wenzelm@63404
   101
  using assms
wenzelm@46898
   102
proof induct
nipkow@15392
   103
  case empty
haftmann@41656
   104
  show ?case
haftmann@41656
   105
  proof
wenzelm@63404
   106
    show "\<exists>f. {} = f ` {i::nat. i < 0} \<and> inj_on f {i. i < 0}"
wenzelm@63404
   107
      by simp
paulson@15510
   108
  qed
nipkow@15392
   109
next
nipkow@15392
   110
  case (insert a A)
wenzelm@23389
   111
  have notinA: "a \<notin> A" by fact
wenzelm@63404
   112
  from insert.hyps obtain n f where "A = f ` {i::nat. i < n}" "inj_on f {i. i < n}"
wenzelm@63404
   113
    by blast
wenzelm@63404
   114
  then have "insert a A = f(n:=a) ` {i. i < Suc n}" and "inj_on (f(n:=a)) {i. i < Suc n}"
wenzelm@63404
   115
    using notinA by (auto simp add: image_def Ball_def inj_on_def less_Suc_eq)
wenzelm@63404
   116
  then show ?case by blast
nipkow@15392
   117
qed
nipkow@15392
   118
wenzelm@63404
   119
lemma nat_seg_image_imp_finite: "A = f ` {i::nat. i < n} \<Longrightarrow> finite A"
haftmann@41656
   120
proof (induct n arbitrary: A)
wenzelm@63404
   121
  case 0
wenzelm@63404
   122
  then show ?case by simp
nipkow@15392
   123
next
nipkow@15392
   124
  case (Suc n)
nipkow@15392
   125
  let ?B = "f ` {i. i < n}"
wenzelm@63404
   126
  have finB: "finite ?B" by (rule Suc.hyps[OF refl])
nipkow@15392
   127
  show ?case
wenzelm@63404
   128
  proof (cases "\<exists>k<n. f n = f k")
wenzelm@63404
   129
    case True
wenzelm@63404
   130
    then have "A = ?B"
wenzelm@63404
   131
      using Suc.prems by (auto simp:less_Suc_eq)
wenzelm@63404
   132
    then show ?thesis
wenzelm@63404
   133
      using finB by simp
nipkow@15392
   134
  next
wenzelm@63404
   135
    case False
wenzelm@63404
   136
    then have "A = insert (f n) ?B"
wenzelm@63404
   137
      using Suc.prems by (auto simp:less_Suc_eq)
wenzelm@63404
   138
    then show ?thesis using finB by simp
nipkow@15392
   139
  qed
nipkow@15392
   140
qed
nipkow@15392
   141
wenzelm@63982
   142
lemma finite_conv_nat_seg_image: "finite A \<longleftrightarrow> (\<exists>n f. A = f ` {i::nat. i < n})"
haftmann@41656
   143
  by (blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on)
nipkow@15392
   144
nipkow@32988
   145
lemma finite_imp_inj_to_nat_seg:
haftmann@41656
   146
  assumes "finite A"
wenzelm@63982
   147
  shows "\<exists>f n. f ` A = {i::nat. i < n} \<and> inj_on f A"
nipkow@32988
   148
proof -
wenzelm@63404
   149
  from finite_imp_nat_seg_image_inj_on [OF \<open>finite A\<close>]
wenzelm@63612
   150
  obtain f and n :: nat where bij: "bij_betw f {i. i<n} A"
wenzelm@63404
   151
    by (auto simp: bij_betw_def)
nipkow@33057
   152
  let ?f = "the_inv_into {i. i<n} f"
wenzelm@63404
   153
  have "inj_on ?f A \<and> ?f ` A = {i. i<n}"
nipkow@33057
   154
    by (fold bij_betw_def) (rule bij_betw_the_inv_into[OF bij])
wenzelm@63404
   155
  then show ?thesis by blast
nipkow@32988
   156
qed
nipkow@32988
   157
wenzelm@63404
   158
lemma finite_Collect_less_nat [iff]: "finite {n::nat. n < k}"
nipkow@44890
   159
  by (fastforce simp: finite_conv_nat_seg_image)
nipkow@29920
   160
wenzelm@63404
   161
lemma finite_Collect_le_nat [iff]: "finite {n::nat. n \<le> k}"
haftmann@41656
   162
  by (simp add: le_eq_less_or_eq Collect_disj_eq)
nipkow@15392
   163
haftmann@41656
   164
wenzelm@60758
   165
subsubsection \<open>Finiteness and common set operations\<close>
wenzelm@12396
   166
wenzelm@63404
   167
lemma rev_finite_subset: "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> finite A"
haftmann@41656
   168
proof (induct arbitrary: A rule: finite_induct)
haftmann@41656
   169
  case empty
haftmann@41656
   170
  then show ?case by simp
haftmann@41656
   171
next
haftmann@41656
   172
  case (insert x F A)
wenzelm@63404
   173
  have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F \<Longrightarrow> finite (A - {x})"
wenzelm@63404
   174
    by fact+
haftmann@41656
   175
  show "finite A"
haftmann@41656
   176
  proof cases
haftmann@41656
   177
    assume x: "x \<in> A"
haftmann@41656
   178
    with A have "A - {x} \<subseteq> F" by (simp add: subset_insert_iff)
haftmann@41656
   179
    with r have "finite (A - {x})" .
wenzelm@63404
   180
    then have "finite (insert x (A - {x}))" ..
wenzelm@63404
   181
    also have "insert x (A - {x}) = A"
wenzelm@63404
   182
      using x by (rule insert_Diff)
haftmann@41656
   183
    finally show ?thesis .
wenzelm@12396
   184
  next
wenzelm@60595
   185
    show ?thesis when "A \<subseteq> F"
wenzelm@60595
   186
      using that by fact
haftmann@41656
   187
    assume "x \<notin> A"
wenzelm@63404
   188
    with A show "A \<subseteq> F"
wenzelm@63404
   189
      by (simp add: subset_insert_iff)
wenzelm@12396
   190
  qed
wenzelm@12396
   191
qed
wenzelm@12396
   192
wenzelm@63404
   193
lemma finite_subset: "A \<subseteq> B \<Longrightarrow> finite B \<Longrightarrow> finite A"
haftmann@41656
   194
  by (rule rev_finite_subset)
nipkow@29901
   195
haftmann@41656
   196
lemma finite_UnI:
haftmann@41656
   197
  assumes "finite F" and "finite G"
haftmann@41656
   198
  shows "finite (F \<union> G)"
haftmann@41656
   199
  using assms by induct simp_all
nipkow@31992
   200
wenzelm@63404
   201
lemma finite_Un [iff]: "finite (F \<union> G) \<longleftrightarrow> finite F \<and> finite G"
haftmann@41656
   202
  by (blast intro: finite_UnI finite_subset [of _ "F \<union> G"])
nipkow@31992
   203
haftmann@41656
   204
lemma finite_insert [simp]: "finite (insert a A) \<longleftrightarrow> finite A"
wenzelm@12396
   205
proof -
haftmann@41656
   206
  have "finite {a} \<and> finite A \<longleftrightarrow> finite A" by simp
haftmann@41656
   207
  then have "finite ({a} \<union> A) \<longleftrightarrow> finite A" by (simp only: finite_Un)
wenzelm@23389
   208
  then show ?thesis by simp
wenzelm@12396
   209
qed
wenzelm@12396
   210
wenzelm@63404
   211
lemma finite_Int [simp, intro]: "finite F \<or> finite G \<Longrightarrow> finite (F \<inter> G)"
haftmann@41656
   212
  by (blast intro: finite_subset)
haftmann@41656
   213
haftmann@41656
   214
lemma finite_Collect_conjI [simp, intro]:
haftmann@41656
   215
  "finite {x. P x} \<or> finite {x. Q x} \<Longrightarrow> finite {x. P x \<and> Q x}"
haftmann@41656
   216
  by (simp add: Collect_conj_eq)
haftmann@41656
   217
haftmann@41656
   218
lemma finite_Collect_disjI [simp]:
haftmann@41656
   219
  "finite {x. P x \<or> Q x} \<longleftrightarrow> finite {x. P x} \<and> finite {x. Q x}"
haftmann@41656
   220
  by (simp add: Collect_disj_eq)
haftmann@41656
   221
wenzelm@63404
   222
lemma finite_Diff [simp, intro]: "finite A \<Longrightarrow> finite (A - B)"
haftmann@41656
   223
  by (rule finite_subset, rule Diff_subset)
nipkow@29901
   224
nipkow@29901
   225
lemma finite_Diff2 [simp]:
haftmann@41656
   226
  assumes "finite B"
haftmann@41656
   227
  shows "finite (A - B) \<longleftrightarrow> finite A"
nipkow@29901
   228
proof -
wenzelm@63404
   229
  have "finite A \<longleftrightarrow> finite ((A - B) \<union> (A \<inter> B))"
wenzelm@63404
   230
    by (simp add: Un_Diff_Int)
wenzelm@63404
   231
  also have "\<dots> \<longleftrightarrow> finite (A - B)"
wenzelm@63404
   232
    using \<open>finite B\<close> by simp
nipkow@29901
   233
  finally show ?thesis ..
nipkow@29901
   234
qed
nipkow@29901
   235
wenzelm@63404
   236
lemma finite_Diff_insert [iff]: "finite (A - insert a B) \<longleftrightarrow> finite (A - B)"
haftmann@41656
   237
proof -
haftmann@41656
   238
  have "finite (A - B) \<longleftrightarrow> finite (A - B - {a})" by simp
haftmann@41656
   239
  moreover have "A - insert a B = A - B - {a}" by auto
haftmann@41656
   240
  ultimately show ?thesis by simp
haftmann@41656
   241
qed
haftmann@41656
   242
wenzelm@63404
   243
lemma finite_compl [simp]:
haftmann@41656
   244
  "finite (A :: 'a set) \<Longrightarrow> finite (- A) \<longleftrightarrow> finite (UNIV :: 'a set)"
haftmann@41656
   245
  by (simp add: Compl_eq_Diff_UNIV)
wenzelm@12396
   246
wenzelm@63404
   247
lemma finite_Collect_not [simp]:
haftmann@41656
   248
  "finite {x :: 'a. P x} \<Longrightarrow> finite {x. \<not> P x} \<longleftrightarrow> finite (UNIV :: 'a set)"
haftmann@41656
   249
  by (simp add: Collect_neg_eq)
haftmann@41656
   250
haftmann@41656
   251
lemma finite_Union [simp, intro]:
wenzelm@63404
   252
  "finite A \<Longrightarrow> (\<And>M. M \<in> A \<Longrightarrow> finite M) \<Longrightarrow> finite (\<Union>A)"
haftmann@41656
   253
  by (induct rule: finite_induct) simp_all
haftmann@41656
   254
haftmann@41656
   255
lemma finite_UN_I [intro]:
haftmann@41656
   256
  "finite A \<Longrightarrow> (\<And>a. a \<in> A \<Longrightarrow> finite (B a)) \<Longrightarrow> finite (\<Union>a\<in>A. B a)"
haftmann@41656
   257
  by (induct rule: finite_induct) simp_all
nipkow@29903
   258
wenzelm@63404
   259
lemma finite_UN [simp]: "finite A \<Longrightarrow> finite (UNION A B) \<longleftrightarrow> (\<forall>x\<in>A. finite (B x))"
haftmann@41656
   260
  by (blast intro: finite_subset)
haftmann@41656
   261
wenzelm@63404
   262
lemma finite_Inter [intro]: "\<exists>A\<in>M. finite A \<Longrightarrow> finite (\<Inter>M)"
haftmann@41656
   263
  by (blast intro: Inter_lower finite_subset)
wenzelm@12396
   264
wenzelm@63404
   265
lemma finite_INT [intro]: "\<exists>x\<in>I. finite (A x) \<Longrightarrow> finite (\<Inter>x\<in>I. A x)"
haftmann@41656
   266
  by (blast intro: INT_lower finite_subset)
paulson@13825
   267
wenzelm@63404
   268
lemma finite_imageI [simp, intro]: "finite F \<Longrightarrow> finite (h ` F)"
haftmann@41656
   269
  by (induct rule: finite_induct) simp_all
paulson@13825
   270
wenzelm@63404
   271
lemma finite_image_set [simp]: "finite {x. P x} \<Longrightarrow> finite {f x |x. P x}"
haftmann@31768
   272
  by (simp add: image_Collect [symmetric])
haftmann@31768
   273
lp15@59504
   274
lemma finite_image_set2:
wenzelm@63404
   275
  "finite {x. P x} \<Longrightarrow> finite {y. Q y} \<Longrightarrow> finite {f x y |x y. P x \<and> Q y}"
lp15@59504
   276
  by (rule finite_subset [where B = "\<Union>x \<in> {x. P x}. \<Union>y \<in> {y. Q y}. {f x y}"]) auto
lp15@59504
   277
haftmann@41656
   278
lemma finite_imageD:
haftmann@42206
   279
  assumes "finite (f ` A)" and "inj_on f A"
haftmann@42206
   280
  shows "finite A"
wenzelm@63404
   281
  using assms
wenzelm@46898
   282
proof (induct "f ` A" arbitrary: A)
wenzelm@63404
   283
  case empty
wenzelm@63404
   284
  then show ?case by simp
haftmann@42206
   285
next
haftmann@42206
   286
  case (insert x B)
wenzelm@63404
   287
  then have B_A: "insert x B = f ` A"
wenzelm@63404
   288
    by simp
wenzelm@63404
   289
  then obtain y where "x = f y" and "y \<in> A"
wenzelm@63404
   290
    by blast
wenzelm@63404
   291
  from B_A \<open>x \<notin> B\<close> have "B = f ` A - {x}"
wenzelm@63404
   292
    by blast
wenzelm@63404
   293
  with B_A \<open>x \<notin> B\<close> \<open>x = f y\<close> \<open>inj_on f A\<close> \<open>y \<in> A\<close> have "B = f ` (A - {y})"
paulson@60303
   294
    by (simp add: inj_on_image_set_diff Set.Diff_subset)
wenzelm@63404
   295
  moreover from \<open>inj_on f A\<close> have "inj_on f (A - {y})"
wenzelm@63404
   296
    by (rule inj_on_diff)
wenzelm@63404
   297
  ultimately have "finite (A - {y})"
wenzelm@63404
   298
    by (rule insert.hyps)
wenzelm@63404
   299
  then show "finite A"
wenzelm@63404
   300
    by simp
haftmann@42206
   301
qed
wenzelm@12396
   302
wenzelm@63404
   303
lemma finite_image_iff: "inj_on f A \<Longrightarrow> finite (f ` A) \<longleftrightarrow> finite A"
wenzelm@63404
   304
  using finite_imageD by blast
lp15@62618
   305
wenzelm@63404
   306
lemma finite_surj: "finite A \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> finite B"
haftmann@41656
   307
  by (erule finite_subset) (rule finite_imageI)
wenzelm@12396
   308
wenzelm@63404
   309
lemma finite_range_imageI: "finite (range g) \<Longrightarrow> finite (range (\<lambda>x. f (g x)))"
haftmann@41656
   310
  by (drule finite_imageI) (simp add: range_composition)
paulson@13825
   311
haftmann@41656
   312
lemma finite_subset_image:
haftmann@41656
   313
  assumes "finite B"
haftmann@41656
   314
  shows "B \<subseteq> f ` A \<Longrightarrow> \<exists>C\<subseteq>A. finite C \<and> B = f ` C"
wenzelm@63404
   315
  using assms
wenzelm@46898
   316
proof induct
wenzelm@63404
   317
  case empty
wenzelm@63404
   318
  then show ?case by simp
haftmann@41656
   319
next
wenzelm@63404
   320
  case insert
wenzelm@63404
   321
  then show ?case
wenzelm@63612
   322
    by (clarsimp simp del: image_insert simp add: image_insert [symmetric]) blast  (* slow *)
haftmann@41656
   323
qed
haftmann@41656
   324
wenzelm@63404
   325
lemma finite_vimage_IntI: "finite F \<Longrightarrow> inj_on h A \<Longrightarrow> finite (h -` F \<inter> A)"
haftmann@41656
   326
  apply (induct rule: finite_induct)
wenzelm@21575
   327
   apply simp_all
paulson@14430
   328
  apply (subst vimage_insert)
hoelzl@43991
   329
  apply (simp add: finite_subset [OF inj_on_vimage_singleton] Int_Un_distrib2)
paulson@13825
   330
  done
paulson@13825
   331
lp15@61762
   332
lemma finite_finite_vimage_IntI:
wenzelm@63612
   333
  assumes "finite F"
wenzelm@63612
   334
    and "\<And>y. y \<in> F \<Longrightarrow> finite ((h -` {y}) \<inter> A)"
lp15@61762
   335
  shows "finite (h -` F \<inter> A)"
lp15@61762
   336
proof -
lp15@61762
   337
  have *: "h -` F \<inter> A = (\<Union> y\<in>F. (h -` {y}) \<inter> A)"
lp15@61762
   338
    by blast
lp15@61762
   339
  show ?thesis
lp15@61762
   340
    by (simp only: * assms finite_UN_I)
lp15@61762
   341
qed
lp15@61762
   342
wenzelm@63404
   343
lemma finite_vimageI: "finite F \<Longrightarrow> inj h \<Longrightarrow> finite (h -` F)"
hoelzl@43991
   344
  using finite_vimage_IntI[of F h UNIV] by auto
hoelzl@43991
   345
wenzelm@63404
   346
lemma finite_vimageD': "finite (f -` A) \<Longrightarrow> A \<subseteq> range f \<Longrightarrow> finite A"
wenzelm@63404
   347
  by (auto simp add: subset_image_iff intro: finite_subset[rotated])
Andreas@59519
   348
wenzelm@63404
   349
lemma finite_vimageD: "finite (h -` F) \<Longrightarrow> surj h \<Longrightarrow> finite F"
wenzelm@63404
   350
  by (auto dest: finite_vimageD')
huffman@34111
   351
huffman@34111
   352
lemma finite_vimage_iff: "bij h \<Longrightarrow> finite (h -` F) \<longleftrightarrow> finite F"
huffman@34111
   353
  unfolding bij_def by (auto elim: finite_vimageD finite_vimageI)
huffman@34111
   354
haftmann@41656
   355
lemma finite_Collect_bex [simp]:
haftmann@41656
   356
  assumes "finite A"
haftmann@41656
   357
  shows "finite {x. \<exists>y\<in>A. Q x y} \<longleftrightarrow> (\<forall>y\<in>A. finite {x. Q x y})"
haftmann@41656
   358
proof -
haftmann@41656
   359
  have "{x. \<exists>y\<in>A. Q x y} = (\<Union>y\<in>A. {x. Q x y})" by auto
haftmann@41656
   360
  with assms show ?thesis by simp
haftmann@41656
   361
qed
wenzelm@12396
   362
haftmann@41656
   363
lemma finite_Collect_bounded_ex [simp]:
haftmann@41656
   364
  assumes "finite {y. P y}"
haftmann@41656
   365
  shows "finite {x. \<exists>y. P y \<and> Q x y} \<longleftrightarrow> (\<forall>y. P y \<longrightarrow> finite {x. Q x y})"
haftmann@41656
   366
proof -
wenzelm@63404
   367
  have "{x. \<exists>y. P y \<and> Q x y} = (\<Union>y\<in>{y. P y}. {x. Q x y})"
wenzelm@63404
   368
    by auto
wenzelm@63404
   369
  with assms show ?thesis
wenzelm@63404
   370
    by simp
haftmann@41656
   371
qed
nipkow@29920
   372
wenzelm@63404
   373
lemma finite_Plus: "finite A \<Longrightarrow> finite B \<Longrightarrow> finite (A <+> B)"
haftmann@41656
   374
  by (simp add: Plus_def)
nipkow@17022
   375
wenzelm@63404
   376
lemma finite_PlusD:
nipkow@31080
   377
  fixes A :: "'a set" and B :: "'b set"
nipkow@31080
   378
  assumes fin: "finite (A <+> B)"
nipkow@31080
   379
  shows "finite A" "finite B"
nipkow@31080
   380
proof -
wenzelm@63404
   381
  have "Inl ` A \<subseteq> A <+> B"
wenzelm@63404
   382
    by auto
wenzelm@63404
   383
  then have "finite (Inl ` A :: ('a + 'b) set)"
wenzelm@63404
   384
    using fin by (rule finite_subset)
wenzelm@63404
   385
  then show "finite A"
wenzelm@63404
   386
    by (rule finite_imageD) (auto intro: inj_onI)
nipkow@31080
   387
next
wenzelm@63404
   388
  have "Inr ` B \<subseteq> A <+> B"
wenzelm@63404
   389
    by auto
wenzelm@63404
   390
  then have "finite (Inr ` B :: ('a + 'b) set)"
wenzelm@63404
   391
    using fin by (rule finite_subset)
wenzelm@63404
   392
  then show "finite B"
wenzelm@63404
   393
    by (rule finite_imageD) (auto intro: inj_onI)
nipkow@31080
   394
qed
nipkow@31080
   395
wenzelm@63404
   396
lemma finite_Plus_iff [simp]: "finite (A <+> B) \<longleftrightarrow> finite A \<and> finite B"
haftmann@41656
   397
  by (auto intro: finite_PlusD finite_Plus)
nipkow@31080
   398
haftmann@41656
   399
lemma finite_Plus_UNIV_iff [simp]:
haftmann@41656
   400
  "finite (UNIV :: ('a + 'b) set) \<longleftrightarrow> finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set)"
haftmann@41656
   401
  by (subst UNIV_Plus_UNIV [symmetric]) (rule finite_Plus_iff)
wenzelm@12396
   402
nipkow@40786
   403
lemma finite_SigmaI [simp, intro]:
wenzelm@63404
   404
  "finite A \<Longrightarrow> (\<And>a. a\<in>A \<Longrightarrow> finite (B a)) \<Longrightarrow> finite (SIGMA a:A. B a)"
wenzelm@63404
   405
  unfolding Sigma_def by blast
wenzelm@12396
   406
Andreas@51290
   407
lemma finite_SigmaI2:
Andreas@51290
   408
  assumes "finite {x\<in>A. B x \<noteq> {}}"
Andreas@51290
   409
  and "\<And>a. a \<in> A \<Longrightarrow> finite (B a)"
Andreas@51290
   410
  shows "finite (Sigma A B)"
Andreas@51290
   411
proof -
wenzelm@63404
   412
  from assms have "finite (Sigma {x\<in>A. B x \<noteq> {}} B)"
wenzelm@63404
   413
    by auto
wenzelm@63404
   414
  also have "Sigma {x:A. B x \<noteq> {}} B = Sigma A B"
wenzelm@63404
   415
    by auto
Andreas@51290
   416
  finally show ?thesis .
Andreas@51290
   417
qed
Andreas@51290
   418
wenzelm@63404
   419
lemma finite_cartesian_product: "finite A \<Longrightarrow> finite B \<Longrightarrow> finite (A \<times> B)"
nipkow@15402
   420
  by (rule finite_SigmaI)
nipkow@15402
   421
wenzelm@12396
   422
lemma finite_Prod_UNIV:
haftmann@41656
   423
  "finite (UNIV :: 'a set) \<Longrightarrow> finite (UNIV :: 'b set) \<Longrightarrow> finite (UNIV :: ('a \<times> 'b) set)"
haftmann@41656
   424
  by (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product)
wenzelm@12396
   425
paulson@15409
   426
lemma finite_cartesian_productD1:
haftmann@42207
   427
  assumes "finite (A \<times> B)" and "B \<noteq> {}"
haftmann@42207
   428
  shows "finite A"
haftmann@42207
   429
proof -
haftmann@42207
   430
  from assms obtain n f where "A \<times> B = f ` {i::nat. i < n}"
haftmann@42207
   431
    by (auto simp add: finite_conv_nat_seg_image)
wenzelm@63404
   432
  then have "fst ` (A \<times> B) = fst ` f ` {i::nat. i < n}"
wenzelm@63404
   433
    by simp
wenzelm@60758
   434
  with \<open>B \<noteq> {}\<close> have "A = (fst \<circ> f) ` {i::nat. i < n}"
haftmann@56154
   435
    by (simp add: image_comp)
wenzelm@63404
   436
  then have "\<exists>n f. A = f ` {i::nat. i < n}"
wenzelm@63404
   437
    by blast
haftmann@42207
   438
  then show ?thesis
haftmann@42207
   439
    by (auto simp add: finite_conv_nat_seg_image)
haftmann@42207
   440
qed
paulson@15409
   441
paulson@15409
   442
lemma finite_cartesian_productD2:
haftmann@42207
   443
  assumes "finite (A \<times> B)" and "A \<noteq> {}"
haftmann@42207
   444
  shows "finite B"
haftmann@42207
   445
proof -
haftmann@42207
   446
  from assms obtain n f where "A \<times> B = f ` {i::nat. i < n}"
haftmann@42207
   447
    by (auto simp add: finite_conv_nat_seg_image)
wenzelm@63404
   448
  then have "snd ` (A \<times> B) = snd ` f ` {i::nat. i < n}"
wenzelm@63404
   449
    by simp
wenzelm@60758
   450
  with \<open>A \<noteq> {}\<close> have "B = (snd \<circ> f) ` {i::nat. i < n}"
haftmann@56154
   451
    by (simp add: image_comp)
wenzelm@63404
   452
  then have "\<exists>n f. B = f ` {i::nat. i < n}"
wenzelm@63404
   453
    by blast
haftmann@42207
   454
  then show ?thesis
haftmann@42207
   455
    by (auto simp add: finite_conv_nat_seg_image)
haftmann@42207
   456
qed
paulson@15409
   457
hoelzl@57025
   458
lemma finite_cartesian_product_iff:
hoelzl@57025
   459
  "finite (A \<times> B) \<longleftrightarrow> (A = {} \<or> B = {} \<or> (finite A \<and> finite B))"
hoelzl@57025
   460
  by (auto dest: finite_cartesian_productD1 finite_cartesian_productD2 finite_cartesian_product)
hoelzl@57025
   461
wenzelm@63404
   462
lemma finite_prod:
Andreas@48175
   463
  "finite (UNIV :: ('a \<times> 'b) set) \<longleftrightarrow> finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set)"
hoelzl@57025
   464
  using finite_cartesian_product_iff[of UNIV UNIV] by simp
Andreas@48175
   465
wenzelm@63404
   466
lemma finite_Pow_iff [iff]: "finite (Pow A) \<longleftrightarrow> finite A"
wenzelm@12396
   467
proof
wenzelm@12396
   468
  assume "finite (Pow A)"
wenzelm@63404
   469
  then have "finite ((\<lambda>x. {x}) ` A)"
wenzelm@63612
   470
    by (blast intro: finite_subset)  (* somewhat slow *)
wenzelm@63404
   471
  then show "finite A"
wenzelm@63404
   472
    by (rule finite_imageD [unfolded inj_on_def]) simp
wenzelm@12396
   473
next
wenzelm@12396
   474
  assume "finite A"
haftmann@41656
   475
  then show "finite (Pow A)"
huffman@35216
   476
    by induct (simp_all add: Pow_insert)
wenzelm@12396
   477
qed
wenzelm@12396
   478
wenzelm@63404
   479
corollary finite_Collect_subsets [simp, intro]: "finite A \<Longrightarrow> finite {B. B \<subseteq> A}"
haftmann@41656
   480
  by (simp add: Pow_def [symmetric])
nipkow@29918
   481
Andreas@48175
   482
lemma finite_set: "finite (UNIV :: 'a set set) \<longleftrightarrow> finite (UNIV :: 'a set)"
wenzelm@63404
   483
  by (simp only: finite_Pow_iff Pow_UNIV[symmetric])
Andreas@48175
   484
wenzelm@63404
   485
lemma finite_UnionD: "finite (\<Union>A) \<Longrightarrow> finite A"
haftmann@41656
   486
  by (blast intro: finite_subset [OF subset_Pow_Union])
nipkow@15392
   487
wenzelm@63404
   488
lemma finite_set_of_finite_funs:
wenzelm@63404
   489
  assumes "finite A" "finite B"
wenzelm@63404
   490
  shows "finite {f. \<forall>x. (x \<in> A \<longrightarrow> f x \<in> B) \<and> (x \<notin> A \<longrightarrow> f x = d)}" (is "finite ?S")
wenzelm@63404
   491
proof -
nipkow@53820
   492
  let ?F = "\<lambda>f. {(a,b). a \<in> A \<and> b = f a}"
wenzelm@63404
   493
  have "?F ` ?S \<subseteq> Pow(A \<times> B)"
wenzelm@63404
   494
    by auto
wenzelm@63404
   495
  from finite_subset[OF this] assms have 1: "finite (?F ` ?S)"
wenzelm@63404
   496
    by simp
nipkow@53820
   497
  have 2: "inj_on ?F ?S"
wenzelm@63612
   498
    by (fastforce simp add: inj_on_def set_eq_iff fun_eq_iff)  (* somewhat slow *)
wenzelm@63404
   499
  show ?thesis
wenzelm@63404
   500
    by (rule finite_imageD [OF 1 2])
nipkow@53820
   501
qed
nipkow@15392
   502
haftmann@58195
   503
lemma not_finite_existsD:
haftmann@58195
   504
  assumes "\<not> finite {a. P a}"
haftmann@58195
   505
  shows "\<exists>a. P a"
haftmann@58195
   506
proof (rule classical)
wenzelm@63404
   507
  assume "\<not> ?thesis"
haftmann@58195
   508
  with assms show ?thesis by auto
haftmann@58195
   509
qed
haftmann@58195
   510
haftmann@58195
   511
wenzelm@60758
   512
subsubsection \<open>Further induction rules on finite sets\<close>
haftmann@41656
   513
haftmann@41656
   514
lemma finite_ne_induct [case_names singleton insert, consumes 2]:
haftmann@41656
   515
  assumes "finite F" and "F \<noteq> {}"
haftmann@41656
   516
  assumes "\<And>x. P {x}"
haftmann@41656
   517
    and "\<And>x F. finite F \<Longrightarrow> F \<noteq> {} \<Longrightarrow> x \<notin> F \<Longrightarrow> P F  \<Longrightarrow> P (insert x F)"
haftmann@41656
   518
  shows "P F"
wenzelm@63404
   519
  using assms
wenzelm@46898
   520
proof induct
wenzelm@63404
   521
  case empty
wenzelm@63404
   522
  then show ?case by simp
haftmann@41656
   523
next
wenzelm@63404
   524
  case (insert x F)
wenzelm@63404
   525
  then show ?case by cases auto
haftmann@41656
   526
qed
haftmann@41656
   527
haftmann@41656
   528
lemma finite_subset_induct [consumes 2, case_names empty insert]:
haftmann@41656
   529
  assumes "finite F" and "F \<subseteq> A"
wenzelm@63612
   530
    and empty: "P {}"
haftmann@41656
   531
    and insert: "\<And>a F. finite F \<Longrightarrow> a \<in> A \<Longrightarrow> a \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert a F)"
haftmann@41656
   532
  shows "P F"
wenzelm@63404
   533
  using \<open>finite F\<close> \<open>F \<subseteq> A\<close>
wenzelm@46898
   534
proof induct
haftmann@41656
   535
  show "P {}" by fact
nipkow@31441
   536
next
haftmann@41656
   537
  fix x F
wenzelm@63404
   538
  assume "finite F" and "x \<notin> F" and P: "F \<subseteq> A \<Longrightarrow> P F" and i: "insert x F \<subseteq> A"
haftmann@41656
   539
  show "P (insert x F)"
haftmann@41656
   540
  proof (rule insert)
haftmann@41656
   541
    from i show "x \<in> A" by blast
haftmann@41656
   542
    from i have "F \<subseteq> A" by blast
haftmann@41656
   543
    with P show "P F" .
haftmann@41656
   544
    show "finite F" by fact
haftmann@41656
   545
    show "x \<notin> F" by fact
haftmann@41656
   546
  qed
haftmann@41656
   547
qed
haftmann@41656
   548
haftmann@41656
   549
lemma finite_empty_induct:
haftmann@41656
   550
  assumes "finite A"
wenzelm@63612
   551
    and "P A"
haftmann@41656
   552
    and remove: "\<And>a A. finite A \<Longrightarrow> a \<in> A \<Longrightarrow> P A \<Longrightarrow> P (A - {a})"
haftmann@41656
   553
  shows "P {}"
haftmann@41656
   554
proof -
wenzelm@63404
   555
  have "P (A - B)" if "B \<subseteq> A" for B :: "'a set"
haftmann@41656
   556
  proof -
wenzelm@63404
   557
    from \<open>finite A\<close> that have "finite B"
wenzelm@63404
   558
      by (rule rev_finite_subset)
wenzelm@60758
   559
    from this \<open>B \<subseteq> A\<close> show "P (A - B)"
haftmann@41656
   560
    proof induct
haftmann@41656
   561
      case empty
wenzelm@60758
   562
      from \<open>P A\<close> show ?case by simp
haftmann@41656
   563
    next
haftmann@41656
   564
      case (insert b B)
haftmann@41656
   565
      have "P (A - B - {b})"
haftmann@41656
   566
      proof (rule remove)
wenzelm@63404
   567
        from \<open>finite A\<close> show "finite (A - B)"
wenzelm@63404
   568
          by induct auto
wenzelm@63404
   569
        from insert show "b \<in> A - B"
wenzelm@63404
   570
          by simp
wenzelm@63404
   571
        from insert show "P (A - B)"
wenzelm@63404
   572
          by simp
haftmann@41656
   573
      qed
wenzelm@63404
   574
      also have "A - B - {b} = A - insert b B"
wenzelm@63404
   575
        by (rule Diff_insert [symmetric])
haftmann@41656
   576
      finally show ?case .
haftmann@41656
   577
    qed
haftmann@41656
   578
  qed
haftmann@41656
   579
  then have "P (A - A)" by blast
haftmann@41656
   580
  then show ?thesis by simp
nipkow@31441
   581
qed
nipkow@31441
   582
haftmann@58195
   583
lemma finite_update_induct [consumes 1, case_names const update]:
haftmann@58195
   584
  assumes finite: "finite {a. f a \<noteq> c}"
wenzelm@63404
   585
    and const: "P (\<lambda>a. c)"
wenzelm@63404
   586
    and update: "\<And>a b f. finite {a. f a \<noteq> c} \<Longrightarrow> f a = c \<Longrightarrow> b \<noteq> c \<Longrightarrow> P f \<Longrightarrow> P (f(a := b))"
haftmann@58195
   587
  shows "P f"
wenzelm@63404
   588
  using finite
wenzelm@63404
   589
proof (induct "{a. f a \<noteq> c}" arbitrary: f)
wenzelm@63404
   590
  case empty
wenzelm@63404
   591
  with const show ?case by simp
haftmann@58195
   592
next
haftmann@58195
   593
  case (insert a A)
haftmann@58195
   594
  then have "A = {a'. (f(a := c)) a' \<noteq> c}" and "f a \<noteq> c"
haftmann@58195
   595
    by auto
wenzelm@60758
   596
  with \<open>finite A\<close> have "finite {a'. (f(a := c)) a' \<noteq> c}"
haftmann@58195
   597
    by simp
haftmann@58195
   598
  have "(f(a := c)) a = c"
haftmann@58195
   599
    by simp
wenzelm@60758
   600
  from insert \<open>A = {a'. (f(a := c)) a' \<noteq> c}\<close> have "P (f(a := c))"
haftmann@58195
   601
    by simp
wenzelm@63404
   602
  with \<open>finite {a'. (f(a := c)) a' \<noteq> c}\<close> \<open>(f(a := c)) a = c\<close> \<open>f a \<noteq> c\<close>
wenzelm@63404
   603
  have "P ((f(a := c))(a := f a))"
haftmann@58195
   604
    by (rule update)
haftmann@58195
   605
  then show ?case by simp
haftmann@58195
   606
qed
haftmann@58195
   607
Andreas@63561
   608
lemma finite_subset_induct' [consumes 2, case_names empty insert]:
Andreas@63561
   609
  assumes "finite F" and "F \<subseteq> A"
wenzelm@63612
   610
    and empty: "P {}"
wenzelm@63612
   611
    and insert: "\<And>a F. \<lbrakk>finite F; a \<in> A; F \<subseteq> A; a \<notin> F; P F \<rbrakk> \<Longrightarrow> P (insert a F)"
Andreas@63561
   612
  shows "P F"
wenzelm@63915
   613
  using assms(1,2)
wenzelm@63915
   614
proof induct
wenzelm@63915
   615
  show "P {}" by fact
wenzelm@63915
   616
next
wenzelm@63915
   617
  fix x F
wenzelm@63915
   618
  assume "finite F" and "x \<notin> F" and
wenzelm@63915
   619
    P: "F \<subseteq> A \<Longrightarrow> P F" and i: "insert x F \<subseteq> A"
wenzelm@63915
   620
  show "P (insert x F)"
wenzelm@63915
   621
  proof (rule insert)
wenzelm@63915
   622
    from i show "x \<in> A" by blast
wenzelm@63915
   623
    from i have "F \<subseteq> A" by blast
wenzelm@63915
   624
    with P show "P F" .
wenzelm@63915
   625
    show "finite F" by fact
wenzelm@63915
   626
    show "x \<notin> F" by fact
wenzelm@63915
   627
    show "F \<subseteq> A" by fact
Andreas@63561
   628
  qed
Andreas@63561
   629
qed
Andreas@63561
   630
haftmann@58195
   631
wenzelm@61799
   632
subsection \<open>Class \<open>finite\<close>\<close>
haftmann@26041
   633
wenzelm@63612
   634
class finite =
wenzelm@63612
   635
  assumes finite_UNIV: "finite (UNIV :: 'a set)"
huffman@27430
   636
begin
huffman@27430
   637
wenzelm@61076
   638
lemma finite [simp]: "finite (A :: 'a set)"
haftmann@26441
   639
  by (rule subset_UNIV finite_UNIV finite_subset)+
haftmann@26041
   640
wenzelm@61076
   641
lemma finite_code [code]: "finite (A :: 'a set) \<longleftrightarrow> True"
bulwahn@40922
   642
  by simp
bulwahn@40922
   643
huffman@27430
   644
end
huffman@27430
   645
wenzelm@46898
   646
instance prod :: (finite, finite) finite
wenzelm@61169
   647
  by standard (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
haftmann@26146
   648
wenzelm@63404
   649
lemma inj_graph: "inj (\<lambda>f. {(x, y). y = f x})"
wenzelm@63404
   650
  by (rule inj_onI) (auto simp add: set_eq_iff fun_eq_iff)
haftmann@26041
   651
haftmann@26146
   652
instance "fun" :: (finite, finite) finite
haftmann@26146
   653
proof
wenzelm@63404
   654
  show "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
haftmann@26041
   655
  proof (rule finite_imageD)
wenzelm@63404
   656
    let ?graph = "\<lambda>f::'a \<Rightarrow> 'b. {(x, y). y = f x}"
wenzelm@63404
   657
    have "range ?graph \<subseteq> Pow UNIV"
wenzelm@63404
   658
      by simp
berghofe@26792
   659
    moreover have "finite (Pow (UNIV :: ('a * 'b) set))"
berghofe@26792
   660
      by (simp only: finite_Pow_iff finite)
berghofe@26792
   661
    ultimately show "finite (range ?graph)"
berghofe@26792
   662
      by (rule finite_subset)
wenzelm@63404
   663
    show "inj ?graph"
wenzelm@63404
   664
      by (rule inj_graph)
haftmann@26041
   665
  qed
haftmann@26041
   666
qed
haftmann@26041
   667
wenzelm@46898
   668
instance bool :: finite
wenzelm@61169
   669
  by standard (simp add: UNIV_bool)
haftmann@44831
   670
haftmann@45962
   671
instance set :: (finite) finite
wenzelm@61169
   672
  by standard (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite)
haftmann@45962
   673
wenzelm@46898
   674
instance unit :: finite
wenzelm@61169
   675
  by standard (simp add: UNIV_unit)
haftmann@44831
   676
wenzelm@46898
   677
instance sum :: (finite, finite) finite
wenzelm@61169
   678
  by standard (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
haftmann@27981
   679
haftmann@26041
   680
wenzelm@60758
   681
subsection \<open>A basic fold functional for finite sets\<close>
nipkow@15392
   682
wenzelm@60758
   683
text \<open>The intended behaviour is
wenzelm@63404
   684
  \<open>fold f z {x\<^sub>1, \<dots>, x\<^sub>n} = f x\<^sub>1 (\<dots> (f x\<^sub>n z)\<dots>)\<close>
wenzelm@63404
   685
  if \<open>f\<close> is ``left-commutative'':
wenzelm@60758
   686
\<close>
nipkow@15392
   687
haftmann@42871
   688
locale comp_fun_commute =
nipkow@28853
   689
  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
haftmann@42871
   690
  assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
nipkow@28853
   691
begin
nipkow@28853
   692
haftmann@51489
   693
lemma fun_left_comm: "f y (f x z) = f x (f y z)"
haftmann@42871
   694
  using comp_fun_commute by (simp add: fun_eq_iff)
nipkow@28853
   695
wenzelm@63404
   696
lemma commute_left_comp: "f y \<circ> (f x \<circ> g) = f x \<circ> (f y \<circ> g)"
haftmann@51489
   697
  by (simp add: o_assoc comp_fun_commute)
haftmann@51489
   698
nipkow@28853
   699
end
nipkow@28853
   700
nipkow@28853
   701
inductive fold_graph :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool"
wenzelm@63404
   702
  for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and z :: 'b
wenzelm@63612
   703
  where
wenzelm@63612
   704
    emptyI [intro]: "fold_graph f z {} z"
wenzelm@63612
   705
  | insertI [intro]: "x \<notin> A \<Longrightarrow> fold_graph f z A y \<Longrightarrow> fold_graph f z (insert x A) (f x y)"
nipkow@28853
   706
nipkow@28853
   707
inductive_cases empty_fold_graphE [elim!]: "fold_graph f z {} x"
nipkow@28853
   708
wenzelm@63404
   709
definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"
wenzelm@63404
   710
  where "fold f z A = (if finite A then (THE y. fold_graph f z A y) else z)"
nipkow@15392
   711
wenzelm@63404
   712
text \<open>
wenzelm@63404
   713
  A tempting alternative for the definiens is
wenzelm@63404
   714
  @{term "if finite A then THE y. fold_graph f z A y else e"}.
wenzelm@63404
   715
  It allows the removal of finiteness assumptions from the theorems
wenzelm@63404
   716
  \<open>fold_comm\<close>, \<open>fold_reindex\<close> and \<open>fold_distrib\<close>.
wenzelm@63404
   717
  The proofs become ugly. It is not worth the effort. (???)
wenzelm@63404
   718
\<close>
nipkow@28853
   719
nipkow@28853
   720
lemma finite_imp_fold_graph: "finite A \<Longrightarrow> \<exists>x. fold_graph f z A x"
wenzelm@63404
   721
  by (induct rule: finite_induct) auto
nipkow@28853
   722
nipkow@28853
   723
wenzelm@63404
   724
subsubsection \<open>From @{const fold_graph} to @{term fold}\<close>
nipkow@15392
   725
haftmann@42871
   726
context comp_fun_commute
haftmann@26041
   727
begin
haftmann@26041
   728
haftmann@51489
   729
lemma fold_graph_finite:
haftmann@51489
   730
  assumes "fold_graph f z A y"
haftmann@51489
   731
  shows "finite A"
haftmann@51489
   732
  using assms by induct simp_all
haftmann@51489
   733
huffman@36045
   734
lemma fold_graph_insertE_aux:
huffman@36045
   735
  "fold_graph f z A y \<Longrightarrow> a \<in> A \<Longrightarrow> \<exists>y'. y = f a y' \<and> fold_graph f z (A - {a}) y'"
huffman@36045
   736
proof (induct set: fold_graph)
wenzelm@63404
   737
  case emptyI
wenzelm@63404
   738
  then show ?case by simp
wenzelm@63404
   739
next
wenzelm@63404
   740
  case (insertI x A y)
wenzelm@63404
   741
  show ?case
huffman@36045
   742
  proof (cases "x = a")
wenzelm@63404
   743
    case True
wenzelm@63404
   744
    with insertI show ?thesis by auto
nipkow@28853
   745
  next
wenzelm@63404
   746
    case False
huffman@36045
   747
    then obtain y' where y: "y = f a y'" and y': "fold_graph f z (A - {a}) y'"
huffman@36045
   748
      using insertI by auto
haftmann@42875
   749
    have "f x y = f a (f x y')"
huffman@36045
   750
      unfolding y by (rule fun_left_comm)
haftmann@42875
   751
    moreover have "fold_graph f z (insert x A - {a}) (f x y')"
wenzelm@60758
   752
      using y' and \<open>x \<noteq> a\<close> and \<open>x \<notin> A\<close>
huffman@36045
   753
      by (simp add: insert_Diff_if fold_graph.insertI)
wenzelm@63404
   754
    ultimately show ?thesis
wenzelm@63404
   755
      by fast
nipkow@15392
   756
  qed
wenzelm@63404
   757
qed
huffman@36045
   758
huffman@36045
   759
lemma fold_graph_insertE:
huffman@36045
   760
  assumes "fold_graph f z (insert x A) v" and "x \<notin> A"
huffman@36045
   761
  obtains y where "v = f x y" and "fold_graph f z A y"
wenzelm@63404
   762
  using assms by (auto dest: fold_graph_insertE_aux [OF _ insertI1])
nipkow@28853
   763
wenzelm@63404
   764
lemma fold_graph_determ: "fold_graph f z A x \<Longrightarrow> fold_graph f z A y \<Longrightarrow> y = x"
huffman@36045
   765
proof (induct arbitrary: y set: fold_graph)
wenzelm@63404
   766
  case emptyI
wenzelm@63404
   767
  then show ?case by fast
wenzelm@63404
   768
next
huffman@36045
   769
  case (insertI x A y v)
wenzelm@60758
   770
  from \<open>fold_graph f z (insert x A) v\<close> and \<open>x \<notin> A\<close>
huffman@36045
   771
  obtain y' where "v = f x y'" and "fold_graph f z A y'"
huffman@36045
   772
    by (rule fold_graph_insertE)
wenzelm@63404
   773
  from \<open>fold_graph f z A y'\<close> have "y' = y"
wenzelm@63404
   774
    by (rule insertI)
wenzelm@63404
   775
  with \<open>v = f x y'\<close> show "v = f x y"
wenzelm@63404
   776
    by simp
wenzelm@63404
   777
qed
nipkow@15392
   778
wenzelm@63404
   779
lemma fold_equality: "fold_graph f z A y \<Longrightarrow> fold f z A = y"
haftmann@51489
   780
  by (cases "finite A") (auto simp add: fold_def intro: fold_graph_determ dest: fold_graph_finite)
nipkow@15392
   781
haftmann@42272
   782
lemma fold_graph_fold:
haftmann@42272
   783
  assumes "finite A"
haftmann@42272
   784
  shows "fold_graph f z A (fold f z A)"
haftmann@42272
   785
proof -
wenzelm@63404
   786
  from assms have "\<exists>x. fold_graph f z A x"
wenzelm@63404
   787
    by (rule finite_imp_fold_graph)
haftmann@42272
   788
  moreover note fold_graph_determ
wenzelm@63404
   789
  ultimately have "\<exists>!x. fold_graph f z A x"
wenzelm@63404
   790
    by (rule ex_ex1I)
wenzelm@63404
   791
  then have "fold_graph f z A (The (fold_graph f z A))"
wenzelm@63404
   792
    by (rule theI')
wenzelm@63404
   793
  with assms show ?thesis
wenzelm@63404
   794
    by (simp add: fold_def)
haftmann@42272
   795
qed
huffman@36045
   796
wenzelm@61799
   797
text \<open>The base case for \<open>fold\<close>:\<close>
nipkow@15392
   798
wenzelm@63404
   799
lemma (in -) fold_infinite [simp]: "\<not> finite A \<Longrightarrow> fold f z A = z"
wenzelm@63404
   800
  by (auto simp: fold_def)
haftmann@51489
   801
wenzelm@63404
   802
lemma (in -) fold_empty [simp]: "fold f z {} = z"
wenzelm@63404
   803
  by (auto simp: fold_def)
nipkow@28853
   804
wenzelm@63404
   805
text \<open>The various recursion equations for @{const fold}:\<close>
nipkow@28853
   806
haftmann@26041
   807
lemma fold_insert [simp]:
haftmann@42875
   808
  assumes "finite A" and "x \<notin> A"
haftmann@42875
   809
  shows "fold f z (insert x A) = f x (fold f z A)"
haftmann@42875
   810
proof (rule fold_equality)
haftmann@51489
   811
  fix z
wenzelm@63404
   812
  from \<open>finite A\<close> have "fold_graph f z A (fold f z A)"
wenzelm@63404
   813
    by (rule fold_graph_fold)
wenzelm@63404
   814
  with \<open>x \<notin> A\<close> have "fold_graph f z (insert x A) (f x (fold f z A))"
wenzelm@63404
   815
    by (rule fold_graph.insertI)
wenzelm@63404
   816
  then show "fold_graph f z (insert x A) (f x (fold f z A))"
wenzelm@63404
   817
    by simp
haftmann@42875
   818
qed
nipkow@28853
   819
haftmann@51489
   820
declare (in -) empty_fold_graphE [rule del] fold_graph.intros [rule del]
wenzelm@61799
   821
  \<comment> \<open>No more proofs involve these.\<close>
haftmann@51489
   822
wenzelm@63404
   823
lemma fold_fun_left_comm: "finite A \<Longrightarrow> f x (fold f z A) = fold f (f x z) A"
nipkow@28853
   824
proof (induct rule: finite_induct)
wenzelm@63404
   825
  case empty
wenzelm@63404
   826
  then show ?case by simp
nipkow@28853
   827
next
wenzelm@63404
   828
  case insert
wenzelm@63404
   829
  then show ?case
haftmann@51489
   830
    by (simp add: fun_left_comm [of x])
nipkow@28853
   831
qed
nipkow@28853
   832
wenzelm@63404
   833
lemma fold_insert2: "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> fold f z (insert x A)  = fold f (f x z) A"
haftmann@51489
   834
  by (simp add: fold_fun_left_comm)
nipkow@15392
   835
haftmann@26041
   836
lemma fold_rec:
haftmann@42875
   837
  assumes "finite A" and "x \<in> A"
haftmann@42875
   838
  shows "fold f z A = f x (fold f z (A - {x}))"
nipkow@28853
   839
proof -
wenzelm@63404
   840
  have A: "A = insert x (A - {x})"
wenzelm@63404
   841
    using \<open>x \<in> A\<close> by blast
wenzelm@63404
   842
  then have "fold f z A = fold f z (insert x (A - {x}))"
wenzelm@63404
   843
    by simp
nipkow@28853
   844
  also have "\<dots> = f x (fold f z (A - {x}))"
wenzelm@60758
   845
    by (rule fold_insert) (simp add: \<open>finite A\<close>)+
nipkow@15535
   846
  finally show ?thesis .
nipkow@15535
   847
qed
nipkow@15535
   848
nipkow@28853
   849
lemma fold_insert_remove:
nipkow@28853
   850
  assumes "finite A"
nipkow@28853
   851
  shows "fold f z (insert x A) = f x (fold f z (A - {x}))"
nipkow@28853
   852
proof -
wenzelm@63404
   853
  from \<open>finite A\<close> have "finite (insert x A)"
wenzelm@63404
   854
    by auto
wenzelm@63404
   855
  moreover have "x \<in> insert x A"
wenzelm@63404
   856
    by auto
nipkow@28853
   857
  ultimately have "fold f z (insert x A) = f x (fold f z (insert x A - {x}))"
nipkow@28853
   858
    by (rule fold_rec)
wenzelm@63404
   859
  then show ?thesis
wenzelm@63404
   860
    by simp
nipkow@28853
   861
qed
nipkow@28853
   862
Andreas@57598
   863
lemma fold_set_union_disj:
Andreas@57598
   864
  assumes "finite A" "finite B" "A \<inter> B = {}"
Andreas@57598
   865
  shows "Finite_Set.fold f z (A \<union> B) = Finite_Set.fold f (Finite_Set.fold f z A) B"
wenzelm@63404
   866
  using assms(2,1,3) by induct simp_all
Andreas@57598
   867
haftmann@51598
   868
end
haftmann@51598
   869
wenzelm@63404
   870
text \<open>Other properties of @{const fold}:\<close>
kuncar@48619
   871
kuncar@48619
   872
lemma fold_image:
haftmann@51598
   873
  assumes "inj_on g A"
haftmann@51489
   874
  shows "fold f z (g ` A) = fold (f \<circ> g) z A"
haftmann@51598
   875
proof (cases "finite A")
wenzelm@63404
   876
  case False
wenzelm@63404
   877
  with assms show ?thesis
wenzelm@63404
   878
    by (auto dest: finite_imageD simp add: fold_def)
haftmann@51598
   879
next
haftmann@51598
   880
  case True
haftmann@51598
   881
  have "fold_graph f z (g ` A) = fold_graph (f \<circ> g) z A"
haftmann@51598
   882
  proof
haftmann@51598
   883
    fix w
haftmann@51598
   884
    show "fold_graph f z (g ` A) w \<longleftrightarrow> fold_graph (f \<circ> g) z A w" (is "?P \<longleftrightarrow> ?Q")
haftmann@51598
   885
    proof
wenzelm@63404
   886
      assume ?P
wenzelm@63404
   887
      then show ?Q
wenzelm@63404
   888
        using assms
haftmann@51598
   889
      proof (induct "g ` A" w arbitrary: A)
wenzelm@63404
   890
        case emptyI
wenzelm@63404
   891
        then show ?case by (auto intro: fold_graph.emptyI)
haftmann@51598
   892
      next
haftmann@51598
   893
        case (insertI x A r B)
wenzelm@63404
   894
        from \<open>inj_on g B\<close> \<open>x \<notin> A\<close> \<open>insert x A = image g B\<close> obtain x' A'
wenzelm@63404
   895
          where "x' \<notin> A'" and [simp]: "B = insert x' A'" "x = g x'" "A = g ` A'"
haftmann@51598
   896
          by (rule inj_img_insertE)
wenzelm@63404
   897
        from insertI.prems have "fold_graph (f \<circ> g) z A' r"
haftmann@51598
   898
          by (auto intro: insertI.hyps)
wenzelm@60758
   899
        with \<open>x' \<notin> A'\<close> have "fold_graph (f \<circ> g) z (insert x' A') ((f \<circ> g) x' r)"
haftmann@51598
   900
          by (rule fold_graph.insertI)
wenzelm@63404
   901
        then show ?case
wenzelm@63404
   902
          by simp
haftmann@51598
   903
      qed
haftmann@51598
   904
    next
wenzelm@63404
   905
      assume ?Q
wenzelm@63404
   906
      then show ?P
wenzelm@63404
   907
        using assms
haftmann@51598
   908
      proof induct
wenzelm@63404
   909
        case emptyI
wenzelm@63404
   910
        then show ?case
wenzelm@63404
   911
          by (auto intro: fold_graph.emptyI)
haftmann@51598
   912
      next
haftmann@51598
   913
        case (insertI x A r)
wenzelm@63404
   914
        from \<open>x \<notin> A\<close> insertI.prems have "g x \<notin> g ` A"
wenzelm@63404
   915
          by auto
wenzelm@63404
   916
        moreover from insertI have "fold_graph f z (g ` A) r"
wenzelm@63404
   917
          by simp
haftmann@51598
   918
        ultimately have "fold_graph f z (insert (g x) (g ` A)) (f (g x) r)"
haftmann@51598
   919
          by (rule fold_graph.insertI)
wenzelm@63404
   920
        then show ?case
wenzelm@63404
   921
          by simp
haftmann@51598
   922
      qed
haftmann@51598
   923
    qed
haftmann@51598
   924
  qed
wenzelm@63404
   925
  with True assms show ?thesis
wenzelm@63404
   926
    by (auto simp add: fold_def)
haftmann@51598
   927
qed
nipkow@15392
   928
haftmann@49724
   929
lemma fold_cong:
haftmann@49724
   930
  assumes "comp_fun_commute f" "comp_fun_commute g"
wenzelm@63404
   931
    and "finite A"
wenzelm@63404
   932
    and cong: "\<And>x. x \<in> A \<Longrightarrow> f x = g x"
haftmann@51489
   933
    and "s = t" and "A = B"
haftmann@51489
   934
  shows "fold f s A = fold g t B"
haftmann@49724
   935
proof -
wenzelm@63404
   936
  have "fold f s A = fold g s A"
wenzelm@63404
   937
    using \<open>finite A\<close> cong
wenzelm@63404
   938
  proof (induct A)
wenzelm@63404
   939
    case empty
wenzelm@63404
   940
    then show ?case by simp
haftmann@49724
   941
  next
wenzelm@63404
   942
    case insert
wenzelm@60758
   943
    interpret f: comp_fun_commute f by (fact \<open>comp_fun_commute f\<close>)
wenzelm@60758
   944
    interpret g: comp_fun_commute g by (fact \<open>comp_fun_commute g\<close>)
haftmann@49724
   945
    from insert show ?case by simp
haftmann@49724
   946
  qed
haftmann@49724
   947
  with assms show ?thesis by simp
haftmann@49724
   948
qed
haftmann@49724
   949
haftmann@49724
   950
wenzelm@60758
   951
text \<open>A simplified version for idempotent functions:\<close>
nipkow@15480
   952
haftmann@42871
   953
locale comp_fun_idem = comp_fun_commute +
haftmann@51489
   954
  assumes comp_fun_idem: "f x \<circ> f x = f x"
haftmann@26041
   955
begin
haftmann@26041
   956
haftmann@42869
   957
lemma fun_left_idem: "f x (f x z) = f x z"
haftmann@42871
   958
  using comp_fun_idem by (simp add: fun_eq_iff)
nipkow@28853
   959
haftmann@26041
   960
lemma fold_insert_idem:
nipkow@28853
   961
  assumes fin: "finite A"
haftmann@51489
   962
  shows "fold f z (insert x A)  = f x (fold f z A)"
nipkow@15480
   963
proof cases
nipkow@28853
   964
  assume "x \<in> A"
wenzelm@63404
   965
  then obtain B where "A = insert x B" and "x \<notin> B"
wenzelm@63404
   966
    by (rule set_insert)
wenzelm@63404
   967
  then show ?thesis
wenzelm@63404
   968
    using assms by (simp add: comp_fun_idem fun_left_idem)
nipkow@15480
   969
next
wenzelm@63404
   970
  assume "x \<notin> A"
wenzelm@63404
   971
  then show ?thesis
wenzelm@63404
   972
    using assms by simp
nipkow@15480
   973
qed
nipkow@15480
   974
haftmann@51489
   975
declare fold_insert [simp del] fold_insert_idem [simp]
nipkow@28853
   976
wenzelm@63404
   977
lemma fold_insert_idem2: "finite A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A"
haftmann@51489
   978
  by (simp add: fold_fun_left_comm)
nipkow@15484
   979
haftmann@26041
   980
end
haftmann@26041
   981
haftmann@35817
   982
wenzelm@61799
   983
subsubsection \<open>Liftings to \<open>comp_fun_commute\<close> etc.\<close>
haftmann@35817
   984
wenzelm@63404
   985
lemma (in comp_fun_commute) comp_comp_fun_commute: "comp_fun_commute (f \<circ> g)"
wenzelm@63404
   986
  by standard (simp_all add: comp_fun_commute)
haftmann@35817
   987
wenzelm@63404
   988
lemma (in comp_fun_idem) comp_comp_fun_idem: "comp_fun_idem (f \<circ> g)"
haftmann@42871
   989
  by (rule comp_fun_idem.intro, rule comp_comp_fun_commute, unfold_locales)
haftmann@42871
   990
    (simp_all add: comp_fun_idem)
haftmann@35817
   991
wenzelm@63404
   992
lemma (in comp_fun_commute) comp_fun_commute_funpow: "comp_fun_commute (\<lambda>x. f x ^^ g x)"
haftmann@49723
   993
proof
wenzelm@63404
   994
  show "f y ^^ g y \<circ> f x ^^ g x = f x ^^ g x \<circ> f y ^^ g y" for x y
haftmann@49723
   995
  proof (cases "x = y")
wenzelm@63404
   996
    case True
wenzelm@63404
   997
    then show ?thesis by simp
haftmann@49723
   998
  next
wenzelm@63404
   999
    case False
wenzelm@63404
  1000
    show ?thesis
haftmann@49723
  1001
    proof (induct "g x" arbitrary: g)
wenzelm@63404
  1002
      case 0
wenzelm@63404
  1003
      then show ?case by simp
haftmann@49723
  1004
    next
haftmann@49723
  1005
      case (Suc n g)
haftmann@49723
  1006
      have hyp1: "f y ^^ g y \<circ> f x = f x \<circ> f y ^^ g y"
haftmann@49723
  1007
      proof (induct "g y" arbitrary: g)
wenzelm@63404
  1008
        case 0
wenzelm@63404
  1009
        then show ?case by simp
haftmann@49723
  1010
      next
haftmann@49723
  1011
        case (Suc n g)
wenzelm@63040
  1012
        define h where "h z = g z - 1" for z
wenzelm@63404
  1013
        with Suc have "n = h y"
wenzelm@63404
  1014
          by simp
haftmann@49723
  1015
        with Suc have hyp: "f y ^^ h y \<circ> f x = f x \<circ> f y ^^ h y"
haftmann@49723
  1016
          by auto
wenzelm@63404
  1017
        from Suc h_def have "g y = Suc (h y)"
wenzelm@63404
  1018
          by simp
wenzelm@63404
  1019
        then show ?case
wenzelm@63404
  1020
          by (simp add: comp_assoc hyp) (simp add: o_assoc comp_fun_commute)
haftmann@49723
  1021
      qed
wenzelm@63040
  1022
      define h where "h z = (if z = x then g x - 1 else g z)" for z
wenzelm@63404
  1023
      with Suc have "n = h x"
wenzelm@63404
  1024
        by simp
haftmann@49723
  1025
      with Suc have "f y ^^ h y \<circ> f x ^^ h x = f x ^^ h x \<circ> f y ^^ h y"
haftmann@49723
  1026
        by auto
wenzelm@63404
  1027
      with False h_def have hyp2: "f y ^^ g y \<circ> f x ^^ h x = f x ^^ h x \<circ> f y ^^ g y"
wenzelm@63404
  1028
        by simp
wenzelm@63404
  1029
      from Suc h_def have "g x = Suc (h x)"
wenzelm@63404
  1030
        by simp
wenzelm@63404
  1031
      then show ?case
wenzelm@63404
  1032
        by (simp del: funpow.simps add: funpow_Suc_right o_assoc hyp2) (simp add: comp_assoc hyp1)
haftmann@49723
  1033
    qed
haftmann@49723
  1034
  qed
haftmann@49723
  1035
qed
haftmann@49723
  1036
haftmann@49723
  1037
wenzelm@60758
  1038
subsubsection \<open>Expressing set operations via @{const fold}\<close>
haftmann@49723
  1039
wenzelm@63404
  1040
lemma comp_fun_commute_const: "comp_fun_commute (\<lambda>_. f)"
wenzelm@63404
  1041
  by standard rule
haftmann@51489
  1042
wenzelm@63404
  1043
lemma comp_fun_idem_insert: "comp_fun_idem insert"
wenzelm@63404
  1044
  by standard auto
haftmann@35817
  1045
wenzelm@63404
  1046
lemma comp_fun_idem_remove: "comp_fun_idem Set.remove"
wenzelm@63404
  1047
  by standard auto
nipkow@31992
  1048
wenzelm@63404
  1049
lemma (in semilattice_inf) comp_fun_idem_inf: "comp_fun_idem inf"
wenzelm@63404
  1050
  by standard (auto simp add: inf_left_commute)
haftmann@35817
  1051
wenzelm@63404
  1052
lemma (in semilattice_sup) comp_fun_idem_sup: "comp_fun_idem sup"
wenzelm@63404
  1053
  by standard (auto simp add: sup_left_commute)
nipkow@31992
  1054
haftmann@35817
  1055
lemma union_fold_insert:
haftmann@35817
  1056
  assumes "finite A"
haftmann@35817
  1057
  shows "A \<union> B = fold insert B A"
haftmann@35817
  1058
proof -
wenzelm@63404
  1059
  interpret comp_fun_idem insert
wenzelm@63404
  1060
    by (fact comp_fun_idem_insert)
wenzelm@63404
  1061
  from \<open>finite A\<close> show ?thesis
wenzelm@63404
  1062
    by (induct A arbitrary: B) simp_all
haftmann@35817
  1063
qed
nipkow@31992
  1064
haftmann@35817
  1065
lemma minus_fold_remove:
haftmann@35817
  1066
  assumes "finite A"
haftmann@46146
  1067
  shows "B - A = fold Set.remove B A"
haftmann@35817
  1068
proof -
wenzelm@63404
  1069
  interpret comp_fun_idem Set.remove
wenzelm@63404
  1070
    by (fact comp_fun_idem_remove)
wenzelm@63404
  1071
  from \<open>finite A\<close> have "fold Set.remove B A = B - A"
wenzelm@63612
  1072
    by (induct A arbitrary: B) auto  (* slow *)
haftmann@46146
  1073
  then show ?thesis ..
haftmann@35817
  1074
qed
haftmann@35817
  1075
haftmann@51489
  1076
lemma comp_fun_commute_filter_fold:
haftmann@51489
  1077
  "comp_fun_commute (\<lambda>x A'. if P x then Set.insert x A' else A')"
wenzelm@63404
  1078
proof -
kuncar@48619
  1079
  interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
wenzelm@61169
  1080
  show ?thesis by standard (auto simp: fun_eq_iff)
kuncar@48619
  1081
qed
kuncar@48619
  1082
kuncar@49758
  1083
lemma Set_filter_fold:
kuncar@48619
  1084
  assumes "finite A"
kuncar@49758
  1085
  shows "Set.filter P A = fold (\<lambda>x A'. if P x then Set.insert x A' else A') {} A"
wenzelm@63404
  1086
  using assms
wenzelm@63404
  1087
  by induct
wenzelm@63404
  1088
    (auto simp add: Set.filter_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold])
kuncar@49758
  1089
wenzelm@63404
  1090
lemma inter_Set_filter:
kuncar@49758
  1091
  assumes "finite B"
kuncar@49758
  1092
  shows "A \<inter> B = Set.filter (\<lambda>x. x \<in> A) B"
wenzelm@63404
  1093
  using assms
wenzelm@63404
  1094
  by induct (auto simp: Set.filter_def)
kuncar@48619
  1095
kuncar@48619
  1096
lemma image_fold_insert:
kuncar@48619
  1097
  assumes "finite A"
kuncar@48619
  1098
  shows "image f A = fold (\<lambda>k A. Set.insert (f k) A) {} A"
kuncar@48619
  1099
proof -
wenzelm@63404
  1100
  interpret comp_fun_commute "\<lambda>k A. Set.insert (f k) A"
wenzelm@63404
  1101
    by standard auto
wenzelm@63404
  1102
  show ?thesis
wenzelm@63404
  1103
    using assms by (induct A) auto
kuncar@48619
  1104
qed
kuncar@48619
  1105
kuncar@48619
  1106
lemma Ball_fold:
kuncar@48619
  1107
  assumes "finite A"
kuncar@48619
  1108
  shows "Ball A P = fold (\<lambda>k s. s \<and> P k) True A"
kuncar@48619
  1109
proof -
wenzelm@63404
  1110
  interpret comp_fun_commute "\<lambda>k s. s \<and> P k"
wenzelm@63404
  1111
    by standard auto
wenzelm@63404
  1112
  show ?thesis
wenzelm@63404
  1113
    using assms by (induct A) auto
kuncar@48619
  1114
qed
kuncar@48619
  1115
kuncar@48619
  1116
lemma Bex_fold:
kuncar@48619
  1117
  assumes "finite A"
kuncar@48619
  1118
  shows "Bex A P = fold (\<lambda>k s. s \<or> P k) False A"
kuncar@48619
  1119
proof -
wenzelm@63404
  1120
  interpret comp_fun_commute "\<lambda>k s. s \<or> P k"
wenzelm@63404
  1121
    by standard auto
wenzelm@63404
  1122
  show ?thesis
wenzelm@63404
  1123
    using assms by (induct A) auto
kuncar@48619
  1124
qed
kuncar@48619
  1125
wenzelm@63404
  1126
lemma comp_fun_commute_Pow_fold: "comp_fun_commute (\<lambda>x A. A \<union> Set.insert x ` A)"
wenzelm@63612
  1127
  by (clarsimp simp: fun_eq_iff comp_fun_commute_def) blast  (* somewhat slow *)
kuncar@48619
  1128
kuncar@48619
  1129
lemma Pow_fold:
kuncar@48619
  1130
  assumes "finite A"
kuncar@48619
  1131
  shows "Pow A = fold (\<lambda>x A. A \<union> Set.insert x ` A) {{}} A"
kuncar@48619
  1132
proof -
wenzelm@63404
  1133
  interpret comp_fun_commute "\<lambda>x A. A \<union> Set.insert x ` A"
wenzelm@63404
  1134
    by (rule comp_fun_commute_Pow_fold)
wenzelm@63404
  1135
  show ?thesis
wenzelm@63404
  1136
    using assms by (induct A) (auto simp: Pow_insert)
kuncar@48619
  1137
qed
kuncar@48619
  1138
kuncar@48619
  1139
lemma fold_union_pair:
kuncar@48619
  1140
  assumes "finite B"
kuncar@48619
  1141
  shows "(\<Union>y\<in>B. {(x, y)}) \<union> A = fold (\<lambda>y. Set.insert (x, y)) A B"
kuncar@48619
  1142
proof -
wenzelm@63404
  1143
  interpret comp_fun_commute "\<lambda>y. Set.insert (x, y)"
wenzelm@63404
  1144
    by standard auto
wenzelm@63404
  1145
  show ?thesis
wenzelm@63404
  1146
    using assms by (induct arbitrary: A) simp_all
kuncar@48619
  1147
qed
kuncar@48619
  1148
wenzelm@63404
  1149
lemma comp_fun_commute_product_fold:
wenzelm@63404
  1150
  "finite B \<Longrightarrow> comp_fun_commute (\<lambda>x z. fold (\<lambda>y. Set.insert (x, y)) z B)"
wenzelm@63404
  1151
  by standard (auto simp: fold_union_pair [symmetric])
kuncar@48619
  1152
kuncar@48619
  1153
lemma product_fold:
wenzelm@63404
  1154
  assumes "finite A" "finite B"
haftmann@51489
  1155
  shows "A \<times> B = fold (\<lambda>x z. fold (\<lambda>y. Set.insert (x, y)) z B) {} A"
wenzelm@63404
  1156
  using assms unfolding Sigma_def
wenzelm@63404
  1157
  by (induct A)
wenzelm@63404
  1158
    (simp_all add: comp_fun_commute.fold_insert[OF comp_fun_commute_product_fold] fold_union_pair)
kuncar@48619
  1159
haftmann@35817
  1160
context complete_lattice
nipkow@31992
  1161
begin
nipkow@31992
  1162
haftmann@35817
  1163
lemma inf_Inf_fold_inf:
haftmann@35817
  1164
  assumes "finite A"
haftmann@51489
  1165
  shows "inf (Inf A) B = fold inf B A"
haftmann@35817
  1166
proof -
wenzelm@63404
  1167
  interpret comp_fun_idem inf
wenzelm@63404
  1168
    by (fact comp_fun_idem_inf)
wenzelm@63404
  1169
  from \<open>finite A\<close> fold_fun_left_comm show ?thesis
wenzelm@63404
  1170
    by (induct A arbitrary: B) (simp_all add: inf_commute fun_eq_iff)
haftmann@35817
  1171
qed
nipkow@31992
  1172
haftmann@35817
  1173
lemma sup_Sup_fold_sup:
haftmann@35817
  1174
  assumes "finite A"
haftmann@51489
  1175
  shows "sup (Sup A) B = fold sup B A"
haftmann@35817
  1176
proof -
wenzelm@63404
  1177
  interpret comp_fun_idem sup
wenzelm@63404
  1178
    by (fact comp_fun_idem_sup)
wenzelm@63404
  1179
  from \<open>finite A\<close> fold_fun_left_comm show ?thesis
wenzelm@63404
  1180
    by (induct A arbitrary: B) (simp_all add: sup_commute fun_eq_iff)
nipkow@31992
  1181
qed
nipkow@31992
  1182
wenzelm@63404
  1183
lemma Inf_fold_inf: "finite A \<Longrightarrow> Inf A = fold inf top A"
wenzelm@63404
  1184
  using inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2)
haftmann@35817
  1185
wenzelm@63404
  1186
lemma Sup_fold_sup: "finite A \<Longrightarrow> Sup A = fold sup bot A"
wenzelm@63404
  1187
  using sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2)
nipkow@31992
  1188
haftmann@46146
  1189
lemma inf_INF_fold_inf:
haftmann@35817
  1190
  assumes "finite A"
wenzelm@63404
  1191
  shows "inf B (INFIMUM A f) = fold (inf \<circ> f) B A" (is "?inf = ?fold")
wenzelm@63404
  1192
proof -
haftmann@42871
  1193
  interpret comp_fun_idem inf by (fact comp_fun_idem_inf)
haftmann@42871
  1194
  interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
wenzelm@63404
  1195
  from \<open>finite A\<close> have "?fold = ?inf"
wenzelm@63404
  1196
    by (induct A arbitrary: B) (simp_all add: inf_left_commute)
wenzelm@63404
  1197
  then show ?thesis ..
haftmann@35817
  1198
qed
nipkow@31992
  1199
haftmann@46146
  1200
lemma sup_SUP_fold_sup:
haftmann@35817
  1201
  assumes "finite A"
wenzelm@63404
  1202
  shows "sup B (SUPREMUM A f) = fold (sup \<circ> f) B A" (is "?sup = ?fold")
wenzelm@63404
  1203
proof -
haftmann@42871
  1204
  interpret comp_fun_idem sup by (fact comp_fun_idem_sup)
haftmann@42871
  1205
  interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
wenzelm@63404
  1206
  from \<open>finite A\<close> have "?fold = ?sup"
wenzelm@63404
  1207
    by (induct A arbitrary: B) (simp_all add: sup_left_commute)
wenzelm@63404
  1208
  then show ?thesis ..
haftmann@35817
  1209
qed
nipkow@31992
  1210
wenzelm@63404
  1211
lemma INF_fold_inf: "finite A \<Longrightarrow> INFIMUM A f = fold (inf \<circ> f) top A"
wenzelm@63404
  1212
  using inf_INF_fold_inf [of A top] by simp
nipkow@31992
  1213
wenzelm@63404
  1214
lemma SUP_fold_sup: "finite A \<Longrightarrow> SUPREMUM A f = fold (sup \<circ> f) bot A"
wenzelm@63404
  1215
  using sup_SUP_fold_sup [of A bot] by simp
nipkow@31992
  1216
nipkow@31992
  1217
end
nipkow@31992
  1218
nipkow@31992
  1219
wenzelm@60758
  1220
subsection \<open>Locales as mini-packages for fold operations\<close>
haftmann@34007
  1221
wenzelm@60758
  1222
subsubsection \<open>The natural case\<close>
haftmann@35719
  1223
haftmann@35719
  1224
locale folding =
wenzelm@63612
  1225
  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and z :: "'b"
haftmann@42871
  1226
  assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
haftmann@35719
  1227
begin
haftmann@35719
  1228
haftmann@54870
  1229
interpretation fold?: comp_fun_commute f
wenzelm@63612
  1230
  by standard (use comp_fun_commute in \<open>simp add: fun_eq_iff\<close>)
haftmann@54867
  1231
haftmann@51489
  1232
definition F :: "'a set \<Rightarrow> 'b"
wenzelm@63404
  1233
  where eq_fold: "F A = fold f z A"
haftmann@51489
  1234
wenzelm@61169
  1235
lemma empty [simp]:"F {} = z"
haftmann@51489
  1236
  by (simp add: eq_fold)
haftmann@35719
  1237
wenzelm@61169
  1238
lemma infinite [simp]: "\<not> finite A \<Longrightarrow> F A = z"
haftmann@51489
  1239
  by (simp add: eq_fold)
wenzelm@63404
  1240
haftmann@35719
  1241
lemma insert [simp]:
haftmann@35719
  1242
  assumes "finite A" and "x \<notin> A"
haftmann@51489
  1243
  shows "F (insert x A) = f x (F A)"
haftmann@35719
  1244
proof -
haftmann@51489
  1245
  from fold_insert assms
haftmann@51489
  1246
  have "fold f z (insert x A) = f x (fold f z A)" by simp
wenzelm@60758
  1247
  with \<open>finite A\<close> show ?thesis by (simp add: eq_fold fun_eq_iff)
haftmann@35719
  1248
qed
wenzelm@63404
  1249
haftmann@35719
  1250
lemma remove:
haftmann@35719
  1251
  assumes "finite A" and "x \<in> A"
haftmann@51489
  1252
  shows "F A = f x (F (A - {x}))"
haftmann@35719
  1253
proof -
wenzelm@60758
  1254
  from \<open>x \<in> A\<close> obtain B where A: "A = insert x B" and "x \<notin> B"
haftmann@35719
  1255
    by (auto dest: mk_disjoint_insert)
wenzelm@60758
  1256
  moreover from \<open>finite A\<close> A have "finite B" by simp
haftmann@35719
  1257
  ultimately show ?thesis by simp
haftmann@35719
  1258
qed
haftmann@35719
  1259
wenzelm@63404
  1260
lemma insert_remove: "finite A \<Longrightarrow> F (insert x A) = f x (F (A - {x}))"
wenzelm@63404
  1261
  by (cases "x \<in> A") (simp_all add: remove insert_absorb)
haftmann@35719
  1262
haftmann@34007
  1263
end
haftmann@35719
  1264
haftmann@35817
  1265
wenzelm@60758
  1266
subsubsection \<open>With idempotency\<close>
haftmann@35817
  1267
haftmann@35719
  1268
locale folding_idem = folding +
haftmann@51489
  1269
  assumes comp_fun_idem: "f x \<circ> f x = f x"
haftmann@35719
  1270
begin
haftmann@35719
  1271
haftmann@35817
  1272
declare insert [simp del]
haftmann@35719
  1273
haftmann@54870
  1274
interpretation fold?: comp_fun_idem f
wenzelm@61169
  1275
  by standard (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff)
haftmann@54867
  1276
haftmann@35719
  1277
lemma insert_idem [simp]:
haftmann@35719
  1278
  assumes "finite A"
haftmann@51489
  1279
  shows "F (insert x A) = f x (F A)"
haftmann@35817
  1280
proof -
haftmann@51489
  1281
  from fold_insert_idem assms
haftmann@51489
  1282
  have "fold f z (insert x A) = f x (fold f z A)" by simp
wenzelm@60758
  1283
  with \<open>finite A\<close> show ?thesis by (simp add: eq_fold fun_eq_iff)
haftmann@35719
  1284
qed
haftmann@35719
  1285
haftmann@35719
  1286
end
haftmann@35719
  1287
haftmann@35817
  1288
wenzelm@60758
  1289
subsection \<open>Finite cardinality\<close>
haftmann@35722
  1290
wenzelm@60758
  1291
text \<open>
haftmann@51489
  1292
  The traditional definition
wenzelm@63404
  1293
  @{prop "card A \<equiv> LEAST n. \<exists>f. A = {f i |i. i < n}"}
haftmann@51489
  1294
  is ugly to work with.
haftmann@51489
  1295
  But now that we have @{const fold} things are easy:
wenzelm@60758
  1296
\<close>
haftmann@35722
  1297
haftmann@61890
  1298
global_interpretation card: folding "\<lambda>_. Suc" 0
haftmann@61778
  1299
  defines card = "folding.F (\<lambda>_. Suc) 0"
haftmann@61778
  1300
  by standard rule
haftmann@35722
  1301
wenzelm@63404
  1302
lemma card_infinite: "\<not> finite A \<Longrightarrow> card A = 0"
haftmann@51489
  1303
  by (fact card.infinite)
haftmann@35722
  1304
wenzelm@63404
  1305
lemma card_empty: "card {} = 0"
haftmann@35722
  1306
  by (fact card.empty)
haftmann@35722
  1307
wenzelm@63404
  1308
lemma card_insert_disjoint: "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> card (insert x A) = Suc (card A)"
haftmann@51489
  1309
  by (fact card.insert)
haftmann@35722
  1310
wenzelm@63404
  1311
lemma card_insert_if: "finite A \<Longrightarrow> card (insert x A) = (if x \<in> A then card A else Suc (card A))"
haftmann@35722
  1312
  by auto (simp add: card.insert_remove card.remove)
haftmann@35722
  1313
wenzelm@63404
  1314
lemma card_ge_0_finite: "card A > 0 \<Longrightarrow> finite A"
haftmann@35722
  1315
  by (rule ccontr) simp
haftmann@35722
  1316
wenzelm@63404
  1317
lemma card_0_eq [simp]: "finite A \<Longrightarrow> card A = 0 \<longleftrightarrow> A = {}"
haftmann@35722
  1318
  by (auto dest: mk_disjoint_insert)
haftmann@35722
  1319
wenzelm@63404
  1320
lemma finite_UNIV_card_ge_0: "finite (UNIV :: 'a set) \<Longrightarrow> card (UNIV :: 'a set) > 0"
haftmann@35722
  1321
  by (rule ccontr) simp
haftmann@35722
  1322
wenzelm@63404
  1323
lemma card_eq_0_iff: "card A = 0 \<longleftrightarrow> A = {} \<or> \<not> finite A"
haftmann@35722
  1324
  by auto
haftmann@35722
  1325
wenzelm@63404
  1326
lemma card_range_greater_zero: "finite (range f) \<Longrightarrow> card (range f) > 0"
haftmann@63365
  1327
  by (rule ccontr) (simp add: card_eq_0_iff)
haftmann@63365
  1328
wenzelm@63404
  1329
lemma card_gt_0_iff: "0 < card A \<longleftrightarrow> A \<noteq> {} \<and> finite A"
wenzelm@63404
  1330
  by (simp add: neq0_conv [symmetric] card_eq_0_iff)
haftmann@35722
  1331
wenzelm@63404
  1332
lemma card_Suc_Diff1: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> Suc (card (A - {x})) = card A"
wenzelm@63404
  1333
  apply (rule insert_Diff [THEN subst, where t = A])
wenzelm@63612
  1334
   apply assumption
wenzelm@63404
  1335
  apply (simp del: insert_Diff_single)
wenzelm@63404
  1336
  done
haftmann@35722
  1337
wenzelm@63404
  1338
lemma card_insert_le_m1: "n > 0 \<Longrightarrow> card y \<le> n - 1 \<Longrightarrow> card (insert x y) \<le> n"
paulson@60762
  1339
  apply (cases "finite y")
wenzelm@63612
  1340
   apply (cases "x \<in> y")
wenzelm@63612
  1341
    apply (auto simp: insert_absorb)
paulson@60762
  1342
  done
paulson@60762
  1343
wenzelm@63404
  1344
lemma card_Diff_singleton: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> card (A - {x}) = card A - 1"
haftmann@51489
  1345
  by (simp add: card_Suc_Diff1 [symmetric])
haftmann@35722
  1346
haftmann@35722
  1347
lemma card_Diff_singleton_if:
haftmann@51489
  1348
  "finite A \<Longrightarrow> card (A - {x}) = (if x \<in> A then card A - 1 else card A)"
haftmann@51489
  1349
  by (simp add: card_Diff_singleton)
haftmann@35722
  1350
haftmann@35722
  1351
lemma card_Diff_insert[simp]:
haftmann@51489
  1352
  assumes "finite A" and "a \<in> A" and "a \<notin> B"
haftmann@51489
  1353
  shows "card (A - insert a B) = card (A - B) - 1"
haftmann@35722
  1354
proof -
wenzelm@63404
  1355
  have "A - insert a B = (A - B) - {a}"
wenzelm@63404
  1356
    using assms by blast
wenzelm@63404
  1357
  then show ?thesis
wenzelm@63404
  1358
    using assms by (simp add: card_Diff_singleton)
haftmann@35722
  1359
qed
haftmann@35722
  1360
wenzelm@63404
  1361
lemma card_insert: "finite A \<Longrightarrow> card (insert x A) = Suc (card (A - {x}))"
haftmann@51489
  1362
  by (fact card.insert_remove)
haftmann@35722
  1363
wenzelm@63404
  1364
lemma card_insert_le: "finite A \<Longrightarrow> card A \<le> card (insert x A)"
wenzelm@63404
  1365
  by (simp add: card_insert_if)
haftmann@35722
  1366
wenzelm@63404
  1367
lemma card_Collect_less_nat[simp]: "card {i::nat. i < n} = n"
wenzelm@63404
  1368
  by (induct n) (simp_all add:less_Suc_eq Collect_disj_eq)
nipkow@41987
  1369
wenzelm@63404
  1370
lemma card_Collect_le_nat[simp]: "card {i::nat. i \<le> n} = Suc n"
wenzelm@63404
  1371
  using card_Collect_less_nat[of "Suc n"] by (simp add: less_Suc_eq_le)
nipkow@41987
  1372
haftmann@35722
  1373
lemma card_mono:
haftmann@35722
  1374
  assumes "finite B" and "A \<subseteq> B"
haftmann@35722
  1375
  shows "card A \<le> card B"
haftmann@35722
  1376
proof -
wenzelm@63404
  1377
  from assms have "finite A"
wenzelm@63404
  1378
    by (auto intro: finite_subset)
wenzelm@63404
  1379
  then show ?thesis
wenzelm@63404
  1380
    using assms
wenzelm@63404
  1381
  proof (induct A arbitrary: B)
wenzelm@63404
  1382
    case empty
wenzelm@63404
  1383
    then show ?case by simp
haftmann@35722
  1384
  next
haftmann@35722
  1385
    case (insert x A)
wenzelm@63404
  1386
    then have "x \<in> B"
wenzelm@63404
  1387
      by simp
wenzelm@63404
  1388
    from insert have "A \<subseteq> B - {x}" and "finite (B - {x})"
wenzelm@63404
  1389
      by auto
wenzelm@63404
  1390
    with insert.hyps have "card A \<le> card (B - {x})"
wenzelm@63404
  1391
      by auto
wenzelm@63404
  1392
    with \<open>finite A\<close> \<open>x \<notin> A\<close> \<open>finite B\<close> \<open>x \<in> B\<close> show ?case
wenzelm@63404
  1393
      by simp (simp only: card.remove)
haftmann@35722
  1394
  qed
haftmann@35722
  1395
qed
haftmann@35722
  1396
wenzelm@63404
  1397
lemma card_seteq: "finite B \<Longrightarrow> (\<And>A. A \<subseteq> B \<Longrightarrow> card B \<le> card A \<Longrightarrow> A = B)"
wenzelm@63404
  1398
  apply (induct rule: finite_induct)
wenzelm@63612
  1399
   apply simp
wenzelm@63404
  1400
  apply clarify
wenzelm@63404
  1401
  apply (subgoal_tac "finite A \<and> A - {x} \<subseteq> F")
wenzelm@63404
  1402
   prefer 2 apply (blast intro: finite_subset, atomize)
wenzelm@63404
  1403
  apply (drule_tac x = "A - {x}" in spec)
nipkow@63648
  1404
  apply (simp add: card_Diff_singleton_if split: if_split_asm)
wenzelm@63404
  1405
  apply (case_tac "card A", auto)
wenzelm@63404
  1406
  done
haftmann@35722
  1407
wenzelm@63404
  1408
lemma psubset_card_mono: "finite B \<Longrightarrow> A < B \<Longrightarrow> card A < card B"
wenzelm@63404
  1409
  apply (simp add: psubset_eq linorder_not_le [symmetric])
wenzelm@63404
  1410
  apply (blast dest: card_seteq)
wenzelm@63404
  1411
  done
haftmann@35722
  1412
haftmann@51489
  1413
lemma card_Un_Int:
wenzelm@63404
  1414
  assumes "finite A" "finite B"
haftmann@51489
  1415
  shows "card A + card B = card (A \<union> B) + card (A \<inter> B)"
wenzelm@63404
  1416
  using assms
wenzelm@63404
  1417
proof (induct A)
wenzelm@63404
  1418
  case empty
wenzelm@63404
  1419
  then show ?case by simp
haftmann@51489
  1420
next
wenzelm@63404
  1421
  case insert
wenzelm@63404
  1422
  then show ?case
haftmann@51489
  1423
    by (auto simp add: insert_absorb Int_insert_left)
haftmann@51489
  1424
qed
haftmann@35722
  1425
wenzelm@63404
  1426
lemma card_Un_disjoint: "finite A \<Longrightarrow> finite B \<Longrightarrow> A \<inter> B = {} \<Longrightarrow> card (A \<union> B) = card A + card B"
wenzelm@63404
  1427
  using card_Un_Int [of A B] by simp
haftmann@35722
  1428
nipkow@59336
  1429
lemma card_Un_le: "card (A \<union> B) \<le> card A + card B"
wenzelm@63404
  1430
  apply (cases "finite A")
wenzelm@63404
  1431
   apply (cases "finite B")
wenzelm@63612
  1432
    apply (use le_iff_add card_Un_Int in blast)
wenzelm@63404
  1433
   apply simp
wenzelm@63404
  1434
  apply simp
wenzelm@63404
  1435
  done
nipkow@59336
  1436
haftmann@35722
  1437
lemma card_Diff_subset:
wenzelm@63404
  1438
  assumes "finite B"
wenzelm@63404
  1439
    and "B \<subseteq> A"
haftmann@35722
  1440
  shows "card (A - B) = card A - card B"
wenzelm@63915
  1441
  using assms
haftmann@35722
  1442
proof (cases "finite A")
wenzelm@63404
  1443
  case False
wenzelm@63404
  1444
  with assms show ?thesis
wenzelm@63404
  1445
    by simp
haftmann@35722
  1446
next
wenzelm@63404
  1447
  case True
wenzelm@63404
  1448
  with assms show ?thesis
wenzelm@63404
  1449
    by (induct B arbitrary: A) simp_all
haftmann@35722
  1450
qed
haftmann@35722
  1451
haftmann@35722
  1452
lemma card_Diff_subset_Int:
wenzelm@63404
  1453
  assumes "finite (A \<inter> B)"
wenzelm@63404
  1454
  shows "card (A - B) = card A - card (A \<inter> B)"
haftmann@35722
  1455
proof -
haftmann@35722
  1456
  have "A - B = A - A \<inter> B" by auto
wenzelm@63404
  1457
  with assms show ?thesis
wenzelm@63404
  1458
    by (simp add: card_Diff_subset)
haftmann@35722
  1459
qed
haftmann@35722
  1460
nipkow@40716
  1461
lemma diff_card_le_card_Diff:
wenzelm@63404
  1462
  assumes "finite B"
wenzelm@63404
  1463
  shows "card A - card B \<le> card (A - B)"
wenzelm@63404
  1464
proof -
nipkow@40716
  1465
  have "card A - card B \<le> card A - card (A \<inter> B)"
nipkow@40716
  1466
    using card_mono[OF assms Int_lower2, of A] by arith
wenzelm@63404
  1467
  also have "\<dots> = card (A - B)"
wenzelm@63404
  1468
    using assms by (simp add: card_Diff_subset_Int)
nipkow@40716
  1469
  finally show ?thesis .
nipkow@40716
  1470
qed
nipkow@40716
  1471
wenzelm@63404
  1472
lemma card_Diff1_less: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> card (A - {x}) < card A"
wenzelm@63404
  1473
  by (rule Suc_less_SucD) (simp add: card_Suc_Diff1 del: card_Diff_insert)
haftmann@35722
  1474
wenzelm@63404
  1475
lemma card_Diff2_less: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> card (A - {x} - {y}) < card A"
wenzelm@63404
  1476
  apply (cases "x = y")
wenzelm@63404
  1477
   apply (simp add: card_Diff1_less del:card_Diff_insert)
wenzelm@63404
  1478
  apply (rule less_trans)
wenzelm@63404
  1479
   prefer 2 apply (auto intro!: card_Diff1_less simp del: card_Diff_insert)
wenzelm@63404
  1480
  done
haftmann@35722
  1481
wenzelm@63404
  1482
lemma card_Diff1_le: "finite A \<Longrightarrow> card (A - {x}) \<le> card A"
wenzelm@63404
  1483
  by (cases "x \<in> A") (simp_all add: card_Diff1_less less_imp_le)
haftmann@35722
  1484
wenzelm@63404
  1485
lemma card_psubset: "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> card A < card B \<Longrightarrow> A < B"
wenzelm@63404
  1486
  by (erule psubsetI) blast
haftmann@35722
  1487
hoelzl@54413
  1488
lemma card_le_inj:
hoelzl@54413
  1489
  assumes fA: "finite A"
hoelzl@54413
  1490
    and fB: "finite B"
hoelzl@54413
  1491
    and c: "card A \<le> card B"
hoelzl@54413
  1492
  shows "\<exists>f. f ` A \<subseteq> B \<and> inj_on f A"
hoelzl@54413
  1493
  using fA fB c
hoelzl@54413
  1494
proof (induct arbitrary: B rule: finite_induct)
hoelzl@54413
  1495
  case empty
hoelzl@54413
  1496
  then show ?case by simp
hoelzl@54413
  1497
next
hoelzl@54413
  1498
  case (insert x s t)
hoelzl@54413
  1499
  then show ?case
wenzelm@63404
  1500
  proof (induct rule: finite_induct [OF insert.prems(1)])
hoelzl@54413
  1501
    case 1
hoelzl@54413
  1502
    then show ?case by simp
hoelzl@54413
  1503
  next
hoelzl@54413
  1504
    case (2 y t)
hoelzl@54413
  1505
    from "2.prems"(1,2,5) "2.hyps"(1,2) have cst: "card s \<le> card t"
hoelzl@54413
  1506
      by simp
hoelzl@54413
  1507
    from "2.prems"(3) [OF "2.hyps"(1) cst]
hoelzl@54413
  1508
    obtain f where "f ` s \<subseteq> t" "inj_on f s"
hoelzl@54413
  1509
      by blast
hoelzl@54413
  1510
    with "2.prems"(2) "2.hyps"(2) show ?case
hoelzl@54413
  1511
      apply -
hoelzl@54413
  1512
      apply (rule exI[where x = "\<lambda>z. if z = x then y else f z"])
hoelzl@54413
  1513
      apply (auto simp add: inj_on_def)
hoelzl@54413
  1514
      done
hoelzl@54413
  1515
  qed
hoelzl@54413
  1516
qed
hoelzl@54413
  1517
hoelzl@54413
  1518
lemma card_subset_eq:
hoelzl@54413
  1519
  assumes fB: "finite B"
hoelzl@54413
  1520
    and AB: "A \<subseteq> B"
hoelzl@54413
  1521
    and c: "card A = card B"
hoelzl@54413
  1522
  shows "A = B"
hoelzl@54413
  1523
proof -
hoelzl@54413
  1524
  from fB AB have fA: "finite A"
hoelzl@54413
  1525
    by (auto intro: finite_subset)
hoelzl@54413
  1526
  from fA fB have fBA: "finite (B - A)"
hoelzl@54413
  1527
    by auto
hoelzl@54413
  1528
  have e: "A \<inter> (B - A) = {}"
hoelzl@54413
  1529
    by blast
hoelzl@54413
  1530
  have eq: "A \<union> (B - A) = B"
hoelzl@54413
  1531
    using AB by blast
hoelzl@54413
  1532
  from card_Un_disjoint[OF fA fBA e, unfolded eq c] have "card (B - A) = 0"
hoelzl@54413
  1533
    by arith
hoelzl@54413
  1534
  then have "B - A = {}"
hoelzl@54413
  1535
    unfolding card_eq_0_iff using fA fB by simp
hoelzl@54413
  1536
  with AB show "A = B"
hoelzl@54413
  1537
    by blast
hoelzl@54413
  1538
qed
hoelzl@54413
  1539
haftmann@35722
  1540
lemma insert_partition:
wenzelm@63404
  1541
  "x \<notin> F \<Longrightarrow> \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<Longrightarrow> x \<inter> \<Union>F = {}"
wenzelm@63612
  1542
  by auto  (* somewhat slow *)
haftmann@35722
  1543
wenzelm@63404
  1544
lemma finite_psubset_induct [consumes 1, case_names psubset]:
wenzelm@63404
  1545
  assumes finite: "finite A"
wenzelm@63404
  1546
    and major: "\<And>A. finite A \<Longrightarrow> (\<And>B. B \<subset> A \<Longrightarrow> P B) \<Longrightarrow> P A"
urbanc@36079
  1547
  shows "P A"
wenzelm@63404
  1548
  using finite
urbanc@36079
  1549
proof (induct A taking: card rule: measure_induct_rule)
haftmann@35722
  1550
  case (less A)
urbanc@36079
  1551
  have fin: "finite A" by fact
wenzelm@63404
  1552
  have ih: "card B < card A \<Longrightarrow> finite B \<Longrightarrow> P B" for B by fact
wenzelm@63404
  1553
  have "P B" if "B \<subset> A" for B
wenzelm@63404
  1554
  proof -
wenzelm@63404
  1555
    from that have "card B < card A"
wenzelm@63404
  1556
      using psubset_card_mono fin by blast
urbanc@36079
  1557
    moreover
wenzelm@63404
  1558
    from that have "B \<subseteq> A"
wenzelm@63404
  1559
      by auto
wenzelm@63404
  1560
    then have "finite B"
wenzelm@63404
  1561
      using fin finite_subset by blast
wenzelm@63404
  1562
    ultimately show ?thesis using ih by simp
wenzelm@63404
  1563
  qed
urbanc@36079
  1564
  with fin show "P A" using major by blast
haftmann@35722
  1565
qed
haftmann@35722
  1566
wenzelm@63404
  1567
lemma finite_induct_select [consumes 1, case_names empty select]:
hoelzl@54413
  1568
  assumes "finite S"
wenzelm@63404
  1569
    and "P {}"
wenzelm@63404
  1570
    and select: "\<And>T. T \<subset> S \<Longrightarrow> P T \<Longrightarrow> \<exists>s\<in>S - T. P (insert s T)"
hoelzl@54413
  1571
  shows "P S"
hoelzl@54413
  1572
proof -
hoelzl@54413
  1573
  have "0 \<le> card S" by simp
hoelzl@54413
  1574
  then have "\<exists>T \<subseteq> S. card T = card S \<and> P T"
hoelzl@54413
  1575
  proof (induct rule: dec_induct)
wenzelm@63404
  1576
    case base with \<open>P {}\<close>
wenzelm@63404
  1577
    show ?case
hoelzl@54413
  1578
      by (intro exI[of _ "{}"]) auto
hoelzl@54413
  1579
  next
hoelzl@54413
  1580
    case (step n)
hoelzl@54413
  1581
    then obtain T where T: "T \<subseteq> S" "card T = n" "P T"
hoelzl@54413
  1582
      by auto
wenzelm@60758
  1583
    with \<open>n < card S\<close> have "T \<subset> S" "P T"
hoelzl@54413
  1584
      by auto
hoelzl@54413
  1585
    with select[of T] obtain s where "s \<in> S" "s \<notin> T" "P (insert s T)"
hoelzl@54413
  1586
      by auto
wenzelm@60758
  1587
    with step(2) T \<open>finite S\<close> show ?case
hoelzl@54413
  1588
      by (intro exI[of _ "insert s T"]) (auto dest: finite_subset)
hoelzl@54413
  1589
  qed
wenzelm@60758
  1590
  with \<open>finite S\<close> show "P S"
hoelzl@54413
  1591
    by (auto dest: card_subset_eq)
hoelzl@54413
  1592
qed
hoelzl@54413
  1593
eberlm@63099
  1594
lemma remove_induct [case_names empty infinite remove]:
wenzelm@63404
  1595
  assumes empty: "P ({} :: 'a set)"
wenzelm@63404
  1596
    and infinite: "\<not> finite B \<Longrightarrow> P B"
wenzelm@63404
  1597
    and remove: "\<And>A. finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> P (A - {x})) \<Longrightarrow> P A"
eberlm@63099
  1598
  shows "P B"
eberlm@63099
  1599
proof (cases "finite B")
wenzelm@63612
  1600
  case False
wenzelm@63404
  1601
  then show ?thesis by (rule infinite)
eberlm@63099
  1602
next
wenzelm@63612
  1603
  case True
eberlm@63099
  1604
  define A where "A = B"
wenzelm@63612
  1605
  with True have "finite A" "A \<subseteq> B"
wenzelm@63612
  1606
    by simp_all
wenzelm@63404
  1607
  then show "P A"
wenzelm@63404
  1608
  proof (induct "card A" arbitrary: A)
eberlm@63099
  1609
    case 0
wenzelm@63404
  1610
    then have "A = {}" by auto
eberlm@63099
  1611
    with empty show ?case by simp
eberlm@63099
  1612
  next
eberlm@63099
  1613
    case (Suc n A)
wenzelm@63404
  1614
    from \<open>A \<subseteq> B\<close> and \<open>finite B\<close> have "finite A"
wenzelm@63404
  1615
      by (rule finite_subset)
eberlm@63099
  1616
    moreover from Suc.hyps have "A \<noteq> {}" by auto
eberlm@63099
  1617
    moreover note \<open>A \<subseteq> B\<close>
eberlm@63099
  1618
    moreover have "P (A - {x})" if x: "x \<in> A" for x
eberlm@63099
  1619
      using x Suc.prems \<open>Suc n = card A\<close> by (intro Suc) auto
eberlm@63099
  1620
    ultimately show ?case by (rule remove)
eberlm@63099
  1621
  qed
eberlm@63099
  1622
qed
eberlm@63099
  1623
eberlm@63099
  1624
lemma finite_remove_induct [consumes 1, case_names empty remove]:
wenzelm@63404
  1625
  fixes P :: "'a set \<Rightarrow> bool"
wenzelm@63612
  1626
  assumes "finite B"
wenzelm@63612
  1627
    and "P {}"
wenzelm@63612
  1628
    and "\<And>A. finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> P (A - {x})) \<Longrightarrow> P A"
eberlm@63099
  1629
  defines "B' \<equiv> B"
wenzelm@63404
  1630
  shows "P B'"
wenzelm@63404
  1631
  by (induct B' rule: remove_induct) (simp_all add: assms)
eberlm@63099
  1632
eberlm@63099
  1633
wenzelm@63404
  1634
text \<open>Main cardinality theorem.\<close>
haftmann@35722
  1635
lemma card_partition [rule_format]:
wenzelm@63404
  1636
  "finite C \<Longrightarrow> finite (\<Union>C) \<Longrightarrow> (\<forall>c\<in>C. card c = k) \<Longrightarrow>
wenzelm@63404
  1637
    (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {}) \<Longrightarrow>
wenzelm@63404
  1638
    k * card C = card (\<Union>C)"
wenzelm@63612
  1639
proof (induct rule: finite_induct)
wenzelm@63612
  1640
  case empty
wenzelm@63612
  1641
  then show ?case by simp
wenzelm@63612
  1642
next
wenzelm@63612
  1643
  case (insert x F)
wenzelm@63612
  1644
  then show ?case
wenzelm@63612
  1645
    by (simp add: card_Un_disjoint insert_partition finite_subset [of _ "\<Union>(insert _ _)"])
wenzelm@63612
  1646
qed
haftmann@35722
  1647
haftmann@35722
  1648
lemma card_eq_UNIV_imp_eq_UNIV:
haftmann@35722
  1649
  assumes fin: "finite (UNIV :: 'a set)"
wenzelm@63404
  1650
    and card: "card A = card (UNIV :: 'a set)"
haftmann@35722
  1651
  shows "A = (UNIV :: 'a set)"
haftmann@35722
  1652
proof
haftmann@35722
  1653
  show "A \<subseteq> UNIV" by simp
haftmann@35722
  1654
  show "UNIV \<subseteq> A"
haftmann@35722
  1655
  proof
wenzelm@63404
  1656
    show "x \<in> A" for x
haftmann@35722
  1657
    proof (rule ccontr)
haftmann@35722
  1658
      assume "x \<notin> A"
haftmann@35722
  1659
      then have "A \<subset> UNIV" by auto
wenzelm@63404
  1660
      with fin have "card A < card (UNIV :: 'a set)"
wenzelm@63404
  1661
        by (fact psubset_card_mono)
haftmann@35722
  1662
      with card show False by simp
haftmann@35722
  1663
    qed
haftmann@35722
  1664
  qed
haftmann@35722
  1665
qed
haftmann@35722
  1666
wenzelm@63404
  1667
text \<open>The form of a finite set of given cardinality\<close>
haftmann@35722
  1668
haftmann@35722
  1669
lemma card_eq_SucD:
wenzelm@63404
  1670
  assumes "card A = Suc k"
wenzelm@63404
  1671
  shows "\<exists>b B. A = insert b B \<and> b \<notin> B \<and> card B = k \<and> (k = 0 \<longrightarrow> B = {})"
haftmann@35722
  1672
proof -
wenzelm@63404
  1673
  have fin: "finite A"
wenzelm@63404
  1674
    using assms by (auto intro: ccontr)
wenzelm@63404
  1675
  moreover have "card A \<noteq> 0"
wenzelm@63404
  1676
    using assms by auto
wenzelm@63404
  1677
  ultimately obtain b where b: "b \<in> A"
wenzelm@63404
  1678
    by auto
haftmann@35722
  1679
  show ?thesis
haftmann@35722
  1680
  proof (intro exI conjI)
wenzelm@63404
  1681
    show "A = insert b (A - {b})"
wenzelm@63404
  1682
      using b by blast
wenzelm@63404
  1683
    show "b \<notin> A - {b}"
wenzelm@63404
  1684
      by blast
haftmann@35722
  1685
    show "card (A - {b}) = k" and "k = 0 \<longrightarrow> A - {b} = {}"
wenzelm@63612
  1686
      using assms b fin by (fastforce dest: mk_disjoint_insert)+
haftmann@35722
  1687
  qed
haftmann@35722
  1688
qed
haftmann@35722
  1689
haftmann@35722
  1690
lemma card_Suc_eq:
wenzelm@63404
  1691
  "card A = Suc k \<longleftrightarrow>
wenzelm@63404
  1692
    (\<exists>b B. A = insert b B \<and> b \<notin> B \<and> card B = k \<and> (k = 0 \<longrightarrow> B = {}))"
wenzelm@63404
  1693
  apply (auto elim!: card_eq_SucD)
wenzelm@63404
  1694
  apply (subst card.insert)
wenzelm@63612
  1695
    apply (auto simp add: intro:ccontr)
wenzelm@63404
  1696
  done
haftmann@35722
  1697
paulson@61518
  1698
lemma card_1_singletonE:
wenzelm@63404
  1699
  assumes "card A = 1"
wenzelm@63404
  1700
  obtains x where "A = {x}"
paulson@61518
  1701
  using assms by (auto simp: card_Suc_eq)
paulson@61518
  1702
eberlm@63099
  1703
lemma is_singleton_altdef: "is_singleton A \<longleftrightarrow> card A = 1"
eberlm@63099
  1704
  unfolding is_singleton_def
eberlm@63099
  1705
  by (auto elim!: card_1_singletonE is_singletonE simp del: One_nat_def)
eberlm@63099
  1706
wenzelm@63404
  1707
lemma card_le_Suc_iff:
wenzelm@63404
  1708
  "finite A \<Longrightarrow> Suc n \<le> card A = (\<exists>a B. A = insert a B \<and> a \<notin> B \<and> n \<le> card B \<and> finite B)"
wenzelm@63404
  1709
  by (fastforce simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff
wenzelm@63404
  1710
    dest: subset_singletonD split: nat.splits if_splits)
nipkow@44744
  1711
haftmann@35722
  1712
lemma finite_fun_UNIVD2:
haftmann@35722
  1713
  assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
haftmann@35722
  1714
  shows "finite (UNIV :: 'b set)"
haftmann@35722
  1715
proof -
wenzelm@63404
  1716
  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))" for arbitrary
haftmann@46146
  1717
    by (rule finite_imageI)
wenzelm@63404
  1718
  moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary)" for arbitrary
haftmann@46146
  1719
    by (rule UNIV_eq_I) auto
wenzelm@63404
  1720
  ultimately show "finite (UNIV :: 'b set)"
wenzelm@63404
  1721
    by simp
haftmann@35722
  1722
qed
haftmann@35722
  1723
huffman@48063
  1724
lemma card_UNIV_unit [simp]: "card (UNIV :: unit set) = 1"
haftmann@35722
  1725
  unfolding UNIV_unit by simp
haftmann@35722
  1726
hoelzl@57447
  1727
lemma infinite_arbitrarily_large:
hoelzl@57447
  1728
  assumes "\<not> finite A"
hoelzl@57447
  1729
  shows "\<exists>B. finite B \<and> card B = n \<and> B \<subseteq> A"
hoelzl@57447
  1730
proof (induction n)
wenzelm@63404
  1731
  case 0
wenzelm@63404
  1732
  show ?case by (intro exI[of _ "{}"]) auto
wenzelm@63404
  1733
next
hoelzl@57447
  1734
  case (Suc n)
wenzelm@63404
  1735
  then obtain B where B: "finite B \<and> card B = n \<and> B \<subseteq> A" ..
wenzelm@60758
  1736
  with \<open>\<not> finite A\<close> have "A \<noteq> B" by auto
hoelzl@57447
  1737
  with B have "B \<subset> A" by auto
wenzelm@63404
  1738
  then have "\<exists>x. x \<in> A - B"
wenzelm@63404
  1739
    by (elim psubset_imp_ex_mem)
wenzelm@63404
  1740
  then obtain x where x: "x \<in> A - B" ..
hoelzl@57447
  1741
  with B have "finite (insert x B) \<and> card (insert x B) = Suc n \<and> insert x B \<subseteq> A"
hoelzl@57447
  1742
    by auto
wenzelm@63404
  1743
  then show "\<exists>B. finite B \<and> card B = Suc n \<and> B \<subseteq> A" ..
hoelzl@57447
  1744
qed
haftmann@35722
  1745
wenzelm@63404
  1746
wenzelm@60758
  1747
subsubsection \<open>Cardinality of image\<close>
haftmann@35722
  1748
wenzelm@63404
  1749
lemma card_image_le: "finite A \<Longrightarrow> card (f ` A) \<le> card A"
paulson@54570
  1750
  by (induct rule: finite_induct) (simp_all add: le_SucI card_insert_if)
haftmann@35722
  1751
wenzelm@63915
  1752
lemma card_image: "inj_on f A \<Longrightarrow> card (f ` A) = card A"
wenzelm@63915
  1753
proof (induct A rule: infinite_finite_induct)
wenzelm@63915
  1754
  case (infinite A)
wenzelm@63915
  1755
  then have "\<not> finite (f ` A)" by (auto dest: finite_imageD)
wenzelm@63915
  1756
  with infinite show ?case by simp
wenzelm@63915
  1757
qed simp_all
haftmann@35722
  1758
haftmann@35722
  1759
lemma bij_betw_same_card: "bij_betw f A B \<Longrightarrow> card A = card B"
wenzelm@63612
  1760
  by (auto simp: card_image bij_betw_def)
haftmann@35722
  1761
wenzelm@63404
  1762
lemma endo_inj_surj: "finite A \<Longrightarrow> f ` A \<subseteq> A \<Longrightarrow> inj_on f A \<Longrightarrow> f ` A = A"
wenzelm@63404
  1763
  by (simp add: card_seteq card_image)
haftmann@35722
  1764
haftmann@35722
  1765
lemma eq_card_imp_inj_on:
wenzelm@63404
  1766
  assumes "finite A" "card(f ` A) = card A"
wenzelm@63404
  1767
  shows "inj_on f A"
wenzelm@63404
  1768
  using assms
paulson@54570
  1769
proof (induct rule:finite_induct)
wenzelm@63404
  1770
  case empty
wenzelm@63404
  1771
  show ?case by simp
paulson@54570
  1772
next
paulson@54570
  1773
  case (insert x A)
wenzelm@63404
  1774
  then show ?case
wenzelm@63404
  1775
    using card_image_le [of A f] by (simp add: card_insert_if split: if_splits)
paulson@54570
  1776
qed
haftmann@35722
  1777
wenzelm@63404
  1778
lemma inj_on_iff_eq_card: "finite A \<Longrightarrow> inj_on f A \<longleftrightarrow> card (f ` A) = card A"
paulson@54570
  1779
  by (blast intro: card_image eq_card_imp_inj_on)
haftmann@35722
  1780
haftmann@35722
  1781
lemma card_inj_on_le:
wenzelm@63404
  1782
  assumes "inj_on f A" "f ` A \<subseteq> B" "finite B"
wenzelm@63404
  1783
  shows "card A \<le> card B"
paulson@54570
  1784
proof -
wenzelm@63404
  1785
  have "finite A"
wenzelm@63404
  1786
    using assms by (blast intro: finite_imageD dest: finite_subset)
wenzelm@63404
  1787
  then show ?thesis
wenzelm@63404
  1788
    using assms by (force intro: card_mono simp: card_image [symmetric])
paulson@54570
  1789
qed
haftmann@35722
  1790
lp15@59504
  1791
lemma surj_card_le: "finite A \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> card B \<le> card A"
lp15@59504
  1792
  by (blast intro: card_image_le card_mono le_trans)
lp15@59504
  1793
haftmann@35722
  1794
lemma card_bij_eq:
wenzelm@63404
  1795
  "inj_on f A \<Longrightarrow> f ` A \<subseteq> B \<Longrightarrow> inj_on g B \<Longrightarrow> g ` B \<subseteq> A \<Longrightarrow> finite A \<Longrightarrow> finite B
wenzelm@63404
  1796
    \<Longrightarrow> card A = card B"
wenzelm@63404
  1797
  by (auto intro: le_antisym card_inj_on_le)
wenzelm@63404
  1798
wenzelm@63404
  1799
lemma bij_betw_finite: "bij_betw f A B \<Longrightarrow> finite A \<longleftrightarrow> finite B"
wenzelm@63404
  1800
  unfolding bij_betw_def using finite_imageD [of f A] by auto
haftmann@35722
  1801
wenzelm@63404
  1802
lemma inj_on_finite: "inj_on f A \<Longrightarrow> f ` A \<le> B \<Longrightarrow> finite B \<Longrightarrow> finite A"
wenzelm@63404
  1803
  using finite_imageD finite_subset by blast
haftmann@35722
  1804
wenzelm@63404
  1805
lemma card_vimage_inj: "inj f \<Longrightarrow> A \<subseteq> range f \<Longrightarrow> card (f -` A) = card A"
wenzelm@63404
  1806
  by (auto 4 3 simp: subset_image_iff inj_vimage_image_eq
wenzelm@63404
  1807
      intro: card_image[symmetric, OF subset_inj_on])
blanchet@55020
  1808
haftmann@41656
  1809
wenzelm@60758
  1810
subsubsection \<open>Pigeonhole Principles\<close>
nipkow@37466
  1811
wenzelm@63404
  1812
lemma pigeonhole: "card A > card (f ` A) \<Longrightarrow> \<not> inj_on f A "
wenzelm@63404
  1813
  by (auto dest: card_image less_irrefl_nat)
nipkow@37466
  1814
nipkow@37466
  1815
lemma pigeonhole_infinite:
wenzelm@63404
  1816
  assumes "\<not> finite A" and "finite (f`A)"
wenzelm@63404
  1817
  shows "\<exists>a0\<in>A. \<not> finite {a\<in>A. f a = f a0}"
wenzelm@63404
  1818
  using assms(2,1)
wenzelm@63404
  1819
proof (induct "f`A" arbitrary: A rule: finite_induct)
wenzelm@63404
  1820
  case empty
wenzelm@63404
  1821
  then show ?case by simp
wenzelm@63404
  1822
next
wenzelm@63404
  1823
  case (insert b F)
wenzelm@63404
  1824
  show ?case
wenzelm@63404
  1825
  proof (cases "finite {a\<in>A. f a = b}")
wenzelm@63404
  1826
    case True
wenzelm@63404
  1827
    with \<open>\<not> finite A\<close> have "\<not> finite (A - {a\<in>A. f a = b})"
wenzelm@63404
  1828
      by simp
wenzelm@63404
  1829
    also have "A - {a\<in>A. f a = b} = {a\<in>A. f a \<noteq> b}"
wenzelm@63404
  1830
      by blast
wenzelm@63404
  1831
    finally have "\<not> finite {a\<in>A. f a \<noteq> b}" .
wenzelm@63404
  1832
    from insert(3)[OF _ this] insert(2,4) show ?thesis
wenzelm@63404
  1833
      by simp (blast intro: rev_finite_subset)
nipkow@37466
  1834
  next
wenzelm@63404
  1835
    case False
wenzelm@63404
  1836
    then have "{a \<in> A. f a = b} \<noteq> {}" by force
wenzelm@63404
  1837
    with False show ?thesis by blast
nipkow@37466
  1838
  qed
nipkow@37466
  1839
qed
nipkow@37466
  1840
nipkow@37466
  1841
lemma pigeonhole_infinite_rel:
wenzelm@63404
  1842
  assumes "\<not> finite A"
wenzelm@63404
  1843
    and "finite B"
wenzelm@63404
  1844
    and "\<forall>a\<in>A. \<exists>b\<in>B. R a b"
wenzelm@63404
  1845
  shows "\<exists>b\<in>B. \<not> finite {a:A. R a b}"
nipkow@37466
  1846
proof -
wenzelm@63404
  1847
  let ?F = "\<lambda>a. {b\<in>B. R a b}"
wenzelm@63404
  1848
  from finite_Pow_iff[THEN iffD2, OF \<open>finite B\<close>] have "finite (?F ` A)"
wenzelm@63404
  1849
    by (blast intro: rev_finite_subset)
wenzelm@63404
  1850
  from pigeonhole_infinite [where f = ?F, OF assms(1) this]
wenzelm@63612
  1851
  obtain a0 where "a0 \<in> A" and infinite: "\<not> finite {a\<in>A. ?F a = ?F a0}" ..
wenzelm@63404
  1852
  obtain b0 where "b0 \<in> B" and "R a0 b0"
wenzelm@63404
  1853
    using \<open>a0 \<in> A\<close> assms(3) by blast
wenzelm@63612
  1854
  have "finite {a\<in>A. ?F a = ?F a0}" if "finite {a\<in>A. R a b0}"
wenzelm@63404
  1855
    using \<open>b0 \<in> B\<close> \<open>R a0 b0\<close> that by (blast intro: rev_finite_subset)
wenzelm@63612
  1856
  with infinite \<open>b0 \<in> B\<close> show ?thesis
wenzelm@63404
  1857
    by blast
nipkow@37466
  1858
qed
nipkow@37466
  1859
nipkow@37466
  1860
wenzelm@60758
  1861
subsubsection \<open>Cardinality of sums\<close>
haftmann@35722
  1862
haftmann@35722
  1863
lemma card_Plus:
wenzelm@63404
  1864
  assumes "finite A" "finite B"
haftmann@35722
  1865
  shows "card (A <+> B) = card A + card B"
haftmann@35722
  1866
proof -
haftmann@35722
  1867
  have "Inl`A \<inter> Inr`B = {}" by fast
haftmann@35722
  1868
  with assms show ?thesis
wenzelm@63404
  1869
    by (simp add: Plus_def card_Un_disjoint card_image)
haftmann@35722
  1870
qed
haftmann@35722
  1871
haftmann@35722
  1872
lemma card_Plus_conv_if:
haftmann@35722
  1873
  "card (A <+> B) = (if finite A \<and> finite B then card A + card B else 0)"
haftmann@35722
  1874
  by (auto simp add: card_Plus)
haftmann@35722
  1875
wenzelm@63404
  1876
text \<open>Relates to equivalence classes.  Based on a theorem of F. Kammüller.\<close>
haftmann@35722
  1877
haftmann@35722
  1878
lemma dvd_partition:
wenzelm@63404
  1879
  assumes f: "finite (\<Union>C)"
wenzelm@63404
  1880
    and "\<forall>c\<in>C. k dvd card c" "\<forall>c1\<in>C. \<forall>c2\<in>C. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {}"
wenzelm@63404
  1881
  shows "k dvd card (\<Union>C)"
paulson@54570
  1882
proof -
wenzelm@63404
  1883
  have "finite C"
paulson@54570
  1884
    by (rule finite_UnionD [OF f])
wenzelm@63404
  1885
  then show ?thesis
wenzelm@63404
  1886
    using assms
paulson@54570
  1887
  proof (induct rule: finite_induct)
wenzelm@63404
  1888
    case empty
wenzelm@63404
  1889
    show ?case by simp
paulson@54570
  1890
  next
wenzelm@63404
  1891
    case insert
wenzelm@63404
  1892
    then show ?case
paulson@54570
  1893
      apply simp
paulson@54570
  1894
      apply (subst card_Un_disjoint)
wenzelm@63612
  1895
         apply (auto simp add: disjoint_eq_subset_Compl)
paulson@54570
  1896
      done
paulson@54570
  1897
  qed
paulson@54570
  1898
qed
haftmann@35722
  1899
wenzelm@63404
  1900
wenzelm@60758
  1901
subsubsection \<open>Relating injectivity and surjectivity\<close>
haftmann@35722
  1902
wenzelm@63404
  1903
lemma finite_surj_inj:
wenzelm@63404
  1904
  assumes "finite A" "A \<subseteq> f ` A"
wenzelm@63404
  1905
  shows "inj_on f A"
paulson@54570
  1906
proof -
wenzelm@63404
  1907
  have "f ` A = A"
paulson@54570
  1908
    by (rule card_seteq [THEN sym]) (auto simp add: assms card_image_le)
paulson@54570
  1909
  then show ?thesis using assms
paulson@54570
  1910
    by (simp add: eq_card_imp_inj_on)
paulson@54570
  1911
qed
haftmann@35722
  1912
wenzelm@63612
  1913
lemma finite_UNIV_surj_inj: "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
wenzelm@63612
  1914
  for f :: "'a \<Rightarrow> 'a"
wenzelm@63404
  1915
  by (blast intro: finite_surj_inj subset_UNIV)
haftmann@35722
  1916
wenzelm@63612
  1917
lemma finite_UNIV_inj_surj: "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
wenzelm@63612
  1918
  for f :: "'a \<Rightarrow> 'a"
wenzelm@63404
  1919
  by (fastforce simp:surj_def dest!: endo_inj_surj)
haftmann@35722
  1920
wenzelm@63404
  1921
corollary infinite_UNIV_nat [iff]: "\<not> finite (UNIV :: nat set)"
haftmann@35722
  1922
proof
haftmann@51489
  1923
  assume "finite (UNIV :: nat set)"
wenzelm@63404
  1924
  with finite_UNIV_inj_surj [of Suc] show False
wenzelm@63404
  1925
    by simp (blast dest: Suc_neq_Zero surjD)
haftmann@35722
  1926
qed
haftmann@35722
  1927
wenzelm@63404
  1928
lemma infinite_UNIV_char_0: "\<not> finite (UNIV :: 'a::semiring_char_0 set)"
haftmann@35722
  1929
proof
haftmann@51489
  1930
  assume "finite (UNIV :: 'a set)"
haftmann@51489
  1931
  with subset_UNIV have "finite (range of_nat :: 'a set)"
haftmann@35722
  1932
    by (rule finite_subset)
haftmann@51489
  1933
  moreover have "inj (of_nat :: nat \<Rightarrow> 'a)"
haftmann@35722
  1934
    by (simp add: inj_on_def)
haftmann@51489
  1935
  ultimately have "finite (UNIV :: nat set)"
haftmann@35722
  1936
    by (rule finite_imageD)
haftmann@51489
  1937
  then show False
haftmann@35722
  1938
    by simp
haftmann@35722
  1939
qed
haftmann@35722
  1940
kuncar@49758
  1941
hide_const (open) Finite_Set.fold
haftmann@46033
  1942
lp15@61810
  1943
wenzelm@63404
  1944
subsection \<open>Infinite Sets\<close>
lp15@61810
  1945
lp15@61810
  1946
text \<open>
lp15@61810
  1947
  Some elementary facts about infinite sets, mostly by Stephan Merz.
lp15@61810
  1948
  Beware! Because "infinite" merely abbreviates a negation, these
lp15@61810
  1949
  lemmas may not work well with \<open>blast\<close>.
lp15@61810
  1950
\<close>
lp15@61810
  1951
lp15@61810
  1952
abbreviation infinite :: "'a set \<Rightarrow> bool"
lp15@61810
  1953
  where "infinite S \<equiv> \<not> finite S"
lp15@61810
  1954
lp15@61810
  1955
text \<open>
lp15@61810
  1956
  Infinite sets are non-empty, and if we remove some elements from an
lp15@61810
  1957
  infinite set, the result is still infinite.
lp15@61810
  1958
\<close>
lp15@61810
  1959
lp15@61810
  1960
lemma infinite_imp_nonempty: "infinite S \<Longrightarrow> S \<noteq> {}"
lp15@61810
  1961
  by auto
lp15@61810
  1962
lp15@61810
  1963
lemma infinite_remove: "infinite S \<Longrightarrow> infinite (S - {a})"
lp15@61810
  1964
  by simp
lp15@61810
  1965
lp15@61810
  1966
lemma Diff_infinite_finite:
wenzelm@63404
  1967
  assumes "finite T" "infinite S"
lp15@61810
  1968
  shows "infinite (S - T)"
wenzelm@63404
  1969
  using \<open>finite T\<close>
lp15@61810
  1970
proof induct
wenzelm@63404
  1971
  from \<open>infinite S\<close> show "infinite (S - {})"
wenzelm@63404
  1972
    by auto
lp15@61810
  1973
next
lp15@61810
  1974
  fix T x
lp15@61810
  1975
  assume ih: "infinite (S - T)"
lp15@61810
  1976
  have "S - (insert x T) = (S - T) - {x}"
lp15@61810
  1977
    by (rule Diff_insert)
wenzelm@63404
  1978
  with ih show "infinite (S - (insert x T))"
lp15@61810
  1979
    by (simp add: infinite_remove)
lp15@61810
  1980
qed
lp15@61810
  1981
lp15@61810
  1982
lemma Un_infinite: "infinite S \<Longrightarrow> infinite (S \<union> T)"
lp15@61810
  1983
  by simp
lp15@61810
  1984
lp15@61810
  1985
lemma infinite_Un: "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
lp15@61810
  1986
  by simp
lp15@61810
  1987
lp15@61810
  1988
lemma infinite_super:
wenzelm@63404
  1989
  assumes "S \<subseteq> T"
wenzelm@63404
  1990
    and "infinite S"
lp15@61810
  1991
  shows "infinite T"
lp15@61810
  1992
proof
lp15@61810
  1993
  assume "finite T"
wenzelm@63404
  1994
  with \<open>S \<subseteq> T\<close> have "finite S" by (simp add: finite_subset)
wenzelm@63404
  1995
  with \<open>infinite S\<close> show False by simp
lp15@61810
  1996
qed
lp15@61810
  1997
lp15@61810
  1998
proposition infinite_coinduct [consumes 1, case_names infinite]:
lp15@61810
  1999
  assumes "X A"
wenzelm@63404
  2000
    and step: "\<And>A. X A \<Longrightarrow> \<exists>x\<in>A. X (A - {x}) \<or> infinite (A - {x})"
lp15@61810
  2001
  shows "infinite A"
lp15@61810
  2002
proof
lp15@61810
  2003
  assume "finite A"
wenzelm@63404
  2004
  then show False
wenzelm@63404
  2005
    using \<open>X A\<close>
lp15@61810
  2006
  proof (induction rule: finite_psubset_induct)
lp15@61810
  2007
    case (psubset A)
lp15@61810
  2008
    then obtain x where "x \<in> A" "X (A - {x}) \<or> infinite (A - {x})"
lp15@61810
  2009
      using local.step psubset.prems by blast
lp15@61810
  2010
    then have "X (A - {x})"
lp15@61810
  2011
      using psubset.hyps by blast
lp15@61810
  2012
    show False
lp15@61810
  2013
      apply (rule psubset.IH [where B = "A - {x}"])
wenzelm@63612
  2014
       apply (use \<open>x \<in> A\<close> in blast)
wenzelm@63404
  2015
      apply (simp add: \<open>X (A - {x})\<close>)
wenzelm@63404
  2016
      done
lp15@61810
  2017
  qed
lp15@61810
  2018
qed
lp15@61810
  2019
lp15@61810
  2020
text \<open>
lp15@61810
  2021
  For any function with infinite domain and finite range there is some
lp15@61810
  2022
  element that is the image of infinitely many domain elements.  In
lp15@61810
  2023
  particular, any infinite sequence of elements from a finite set
lp15@61810
  2024
  contains some element that occurs infinitely often.
lp15@61810
  2025
\<close>
lp15@61810
  2026
lp15@61810
  2027
lemma inf_img_fin_dom':
wenzelm@63404
  2028
  assumes img: "finite (f ` A)"
wenzelm@63404
  2029
    and dom: "infinite A"
lp15@61810
  2030
  shows "\<exists>y \<in> f ` A. infinite (f -` {y} \<inter> A)"
lp15@61810
  2031
proof (rule ccontr)
lp15@61810
  2032
  have "A \<subseteq> (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by auto
wenzelm@63404
  2033
  moreover assume "\<not> ?thesis"
lp15@61810
  2034
  with img have "finite (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by blast
wenzelm@63404
  2035
  ultimately have "finite A" by (rule finite_subset)
lp15@61810
  2036
  with dom show False by contradiction
lp15@61810
  2037
qed
lp15@61810
  2038
lp15@61810
  2039
lemma inf_img_fin_domE':
lp15@61810
  2040
  assumes "finite (f ` A)" and "infinite A"
lp15@61810
  2041
  obtains y where "y \<in> f`A" and "infinite (f -` {y} \<inter> A)"
lp15@61810
  2042
  using assms by (blast dest: inf_img_fin_dom')
lp15@61810
  2043
lp15@61810
  2044
lemma inf_img_fin_dom:
lp15@61810
  2045
  assumes img: "finite (f`A)" and dom: "infinite A"
lp15@61810
  2046
  shows "\<exists>y \<in> f`A. infinite (f -` {y})"
wenzelm@63404
  2047
  using inf_img_fin_dom'[OF assms] by auto
lp15@61810
  2048
lp15@61810
  2049
lemma inf_img_fin_domE:
lp15@61810
  2050
  assumes "finite (f`A)" and "infinite A"
lp15@61810
  2051
  obtains y where "y \<in> f`A" and "infinite (f -` {y})"
lp15@61810
  2052
  using assms by (blast dest: inf_img_fin_dom)
lp15@61810
  2053
wenzelm@63404
  2054
proposition finite_image_absD: "finite (abs ` S) \<Longrightarrow> finite S"
wenzelm@63404
  2055
  for S :: "'a::linordered_ring set"
lp15@61810
  2056
  by (rule ccontr) (auto simp: abs_eq_iff vimage_def dest: inf_img_fin_dom)
lp15@61810
  2057
haftmann@35722
  2058
end