src/HOL/Finite_Set.thy
 author wenzelm Wed Sep 17 21:27:14 2008 +0200 (2008-09-17) changeset 28263 69eaa97e7e96 parent 27981 feb0c01cf0fb child 28823 dcbef866c9e2 permissions -rw-r--r--
moved global ML bindings to global place;
```     1 (*  Title:      HOL/Finite_Set.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
```
```     4                 with contributions by Jeremy Avigad
```
```     5 *)
```
```     6
```
```     7 header {* Finite sets *}
```
```     8
```
```     9 theory Finite_Set
```
```    10 imports Datatype Divides Transitive_Closure
```
```    11 begin
```
```    12
```
```    13 subsection {* Definition and basic properties *}
```
```    14
```
```    15 inductive finite :: "'a set => bool"
```
```    16   where
```
```    17     emptyI [simp, intro!]: "finite {}"
```
```    18   | insertI [simp, intro!]: "finite A ==> finite (insert a A)"
```
```    19
```
```    20 lemma ex_new_if_finite: -- "does not depend on def of finite at all"
```
```    21   assumes "\<not> finite (UNIV :: 'a set)" and "finite A"
```
```    22   shows "\<exists>a::'a. a \<notin> A"
```
```    23 proof -
```
```    24   from prems have "A \<noteq> UNIV" by blast
```
```    25   thus ?thesis by blast
```
```    26 qed
```
```    27
```
```    28 lemma finite_induct [case_names empty insert, induct set: finite]:
```
```    29   "finite F ==>
```
```    30     P {} ==> (!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F"
```
```    31   -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
```
```    32 proof -
```
```    33   assume "P {}" and
```
```    34     insert: "!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)"
```
```    35   assume "finite F"
```
```    36   thus "P F"
```
```    37   proof induct
```
```    38     show "P {}" by fact
```
```    39     fix x F assume F: "finite F" and P: "P F"
```
```    40     show "P (insert x F)"
```
```    41     proof cases
```
```    42       assume "x \<in> F"
```
```    43       hence "insert x F = F" by (rule insert_absorb)
```
```    44       with P show ?thesis by (simp only:)
```
```    45     next
```
```    46       assume "x \<notin> F"
```
```    47       from F this P show ?thesis by (rule insert)
```
```    48     qed
```
```    49   qed
```
```    50 qed
```
```    51
```
```    52 lemma finite_ne_induct[case_names singleton insert, consumes 2]:
```
```    53 assumes fin: "finite F" shows "F \<noteq> {} \<Longrightarrow>
```
```    54  \<lbrakk> \<And>x. P{x};
```
```    55    \<And>x F. \<lbrakk> finite F; F \<noteq> {}; x \<notin> F; P F \<rbrakk> \<Longrightarrow> P (insert x F) \<rbrakk>
```
```    56  \<Longrightarrow> P F"
```
```    57 using fin
```
```    58 proof induct
```
```    59   case empty thus ?case by simp
```
```    60 next
```
```    61   case (insert x F)
```
```    62   show ?case
```
```    63   proof cases
```
```    64     assume "F = {}"
```
```    65     thus ?thesis using `P {x}` by simp
```
```    66   next
```
```    67     assume "F \<noteq> {}"
```
```    68     thus ?thesis using insert by blast
```
```    69   qed
```
```    70 qed
```
```    71
```
```    72 lemma finite_subset_induct [consumes 2, case_names empty insert]:
```
```    73   assumes "finite F" and "F \<subseteq> A"
```
```    74     and empty: "P {}"
```
```    75     and insert: "!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
```
```    76   shows "P F"
```
```    77 proof -
```
```    78   from `finite F` and `F \<subseteq> A`
```
```    79   show ?thesis
```
```    80   proof induct
```
```    81     show "P {}" by fact
```
```    82   next
```
```    83     fix x F
```
```    84     assume "finite F" and "x \<notin> F" and
```
```    85       P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A"
```
```    86     show "P (insert x F)"
```
```    87     proof (rule insert)
```
```    88       from i show "x \<in> A" by blast
```
```    89       from i have "F \<subseteq> A" by blast
```
```    90       with P show "P F" .
```
```    91       show "finite F" by fact
```
```    92       show "x \<notin> F" by fact
```
```    93     qed
```
```    94   qed
```
```    95 qed
```
```    96
```
```    97
```
```    98 text{* Finite sets are the images of initial segments of natural numbers: *}
```
```    99
```
```   100 lemma finite_imp_nat_seg_image_inj_on:
```
```   101   assumes fin: "finite A"
```
```   102   shows "\<exists> (n::nat) f. A = f ` {i. i<n} & inj_on f {i. i<n}"
```
```   103 using fin
```
```   104 proof induct
```
```   105   case empty
```
```   106   show ?case
```
```   107   proof show "\<exists>f. {} = f ` {i::nat. i < 0} & inj_on f {i. i<0}" by simp
```
```   108   qed
```
```   109 next
```
```   110   case (insert a A)
```
```   111   have notinA: "a \<notin> A" by fact
```
```   112   from insert.hyps obtain n f
```
```   113     where "A = f ` {i::nat. i < n}" "inj_on f {i. i < n}" by blast
```
```   114   hence "insert a A = f(n:=a) ` {i. i < Suc n}"
```
```   115         "inj_on (f(n:=a)) {i. i < Suc n}" using notinA
```
```   116     by (auto simp add: image_def Ball_def inj_on_def less_Suc_eq)
```
```   117   thus ?case by blast
```
```   118 qed
```
```   119
```
```   120 lemma nat_seg_image_imp_finite:
```
```   121   "!!f A. A = f ` {i::nat. i<n} \<Longrightarrow> finite A"
```
```   122 proof (induct n)
```
```   123   case 0 thus ?case by simp
```
```   124 next
```
```   125   case (Suc n)
```
```   126   let ?B = "f ` {i. i < n}"
```
```   127   have finB: "finite ?B" by(rule Suc.hyps[OF refl])
```
```   128   show ?case
```
```   129   proof cases
```
```   130     assume "\<exists>k<n. f n = f k"
```
```   131     hence "A = ?B" using Suc.prems by(auto simp:less_Suc_eq)
```
```   132     thus ?thesis using finB by simp
```
```   133   next
```
```   134     assume "\<not>(\<exists> k<n. f n = f k)"
```
```   135     hence "A = insert (f n) ?B" using Suc.prems by(auto simp:less_Suc_eq)
```
```   136     thus ?thesis using finB by simp
```
```   137   qed
```
```   138 qed
```
```   139
```
```   140 lemma finite_conv_nat_seg_image:
```
```   141   "finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})"
```
```   142 by(blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on)
```
```   143
```
```   144
```
```   145 subsubsection{* Finiteness and set theoretic constructions *}
```
```   146
```
```   147 lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)"
```
```   148   -- {* The union of two finite sets is finite. *}
```
```   149   by (induct set: finite) simp_all
```
```   150
```
```   151 lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A"
```
```   152   -- {* Every subset of a finite set is finite. *}
```
```   153 proof -
```
```   154   assume "finite B"
```
```   155   thus "!!A. A \<subseteq> B ==> finite A"
```
```   156   proof induct
```
```   157     case empty
```
```   158     thus ?case by simp
```
```   159   next
```
```   160     case (insert x F A)
```
```   161     have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F ==> finite (A - {x})" by fact+
```
```   162     show "finite A"
```
```   163     proof cases
```
```   164       assume x: "x \<in> A"
```
```   165       with A have "A - {x} \<subseteq> F" by (simp add: subset_insert_iff)
```
```   166       with r have "finite (A - {x})" .
```
```   167       hence "finite (insert x (A - {x}))" ..
```
```   168       also have "insert x (A - {x}) = A" using x by (rule insert_Diff)
```
```   169       finally show ?thesis .
```
```   170     next
```
```   171       show "A \<subseteq> F ==> ?thesis" by fact
```
```   172       assume "x \<notin> A"
```
```   173       with A show "A \<subseteq> F" by (simp add: subset_insert_iff)
```
```   174     qed
```
```   175   qed
```
```   176 qed
```
```   177
```
```   178 lemma finite_Collect_subset[simp]: "finite A \<Longrightarrow> finite{x \<in> A. P x}"
```
```   179 using finite_subset[of "{x \<in> A. P x}" "A"] by blast
```
```   180
```
```   181 lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
```
```   182   by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
```
```   183
```
```   184 lemma finite_Int [simp, intro]: "finite F | finite G ==> finite (F Int G)"
```
```   185   -- {* The converse obviously fails. *}
```
```   186   by (blast intro: finite_subset)
```
```   187
```
```   188 lemma finite_insert [simp]: "finite (insert a A) = finite A"
```
```   189   apply (subst insert_is_Un)
```
```   190   apply (simp only: finite_Un, blast)
```
```   191   done
```
```   192
```
```   193 lemma finite_Union[simp, intro]:
```
```   194  "\<lbrakk> finite A; !!M. M \<in> A \<Longrightarrow> finite M \<rbrakk> \<Longrightarrow> finite(\<Union>A)"
```
```   195 by (induct rule:finite_induct) simp_all
```
```   196
```
```   197 lemma finite_empty_induct:
```
```   198   assumes "finite A"
```
```   199     and "P A"
```
```   200     and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})"
```
```   201   shows "P {}"
```
```   202 proof -
```
```   203   have "P (A - A)"
```
```   204   proof -
```
```   205     {
```
```   206       fix c b :: "'a set"
```
```   207       assume c: "finite c" and b: "finite b"
```
```   208 	and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y - {x})"
```
```   209       have "c \<subseteq> b ==> P (b - c)"
```
```   210 	using c
```
```   211       proof induct
```
```   212 	case empty
```
```   213 	from P1 show ?case by simp
```
```   214       next
```
```   215 	case (insert x F)
```
```   216 	have "P (b - F - {x})"
```
```   217 	proof (rule P2)
```
```   218           from _ b show "finite (b - F)" by (rule finite_subset) blast
```
```   219           from insert show "x \<in> b - F" by simp
```
```   220           from insert show "P (b - F)" by simp
```
```   221 	qed
```
```   222 	also have "b - F - {x} = b - insert x F" by (rule Diff_insert [symmetric])
```
```   223 	finally show ?case .
```
```   224       qed
```
```   225     }
```
```   226     then show ?thesis by this (simp_all add: assms)
```
```   227   qed
```
```   228   then show ?thesis by simp
```
```   229 qed
```
```   230
```
```   231 lemma finite_Diff [simp]: "finite B ==> finite (B - Ba)"
```
```   232   by (rule Diff_subset [THEN finite_subset])
```
```   233
```
```   234 lemma finite_Diff_insert [iff]: "finite (A - insert a B) = finite (A - B)"
```
```   235   apply (subst Diff_insert)
```
```   236   apply (case_tac "a : A - B")
```
```   237    apply (rule finite_insert [symmetric, THEN trans])
```
```   238    apply (subst insert_Diff, simp_all)
```
```   239   done
```
```   240
```
```   241 lemma finite_Diff_singleton [simp]: "finite (A - {a}) = finite A"
```
```   242   by simp
```
```   243
```
```   244
```
```   245 text {* Image and Inverse Image over Finite Sets *}
```
```   246
```
```   247 lemma finite_imageI[simp]: "finite F ==> finite (h ` F)"
```
```   248   -- {* The image of a finite set is finite. *}
```
```   249   by (induct set: finite) simp_all
```
```   250
```
```   251 lemma finite_surj: "finite A ==> B <= f ` A ==> finite B"
```
```   252   apply (frule finite_imageI)
```
```   253   apply (erule finite_subset, assumption)
```
```   254   done
```
```   255
```
```   256 lemma finite_range_imageI:
```
```   257     "finite (range g) ==> finite (range (%x. f (g x)))"
```
```   258   apply (drule finite_imageI, simp add: range_composition)
```
```   259   done
```
```   260
```
```   261 lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A"
```
```   262 proof -
```
```   263   have aux: "!!A. finite (A - {}) = finite A" by simp
```
```   264   fix B :: "'a set"
```
```   265   assume "finite B"
```
```   266   thus "!!A. f`A = B ==> inj_on f A ==> finite A"
```
```   267     apply induct
```
```   268      apply simp
```
```   269     apply (subgoal_tac "EX y:A. f y = x & F = f ` (A - {y})")
```
```   270      apply clarify
```
```   271      apply (simp (no_asm_use) add: inj_on_def)
```
```   272      apply (blast dest!: aux [THEN iffD1], atomize)
```
```   273     apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl)
```
```   274     apply (frule subsetD [OF equalityD2 insertI1], clarify)
```
```   275     apply (rule_tac x = xa in bexI)
```
```   276      apply (simp_all add: inj_on_image_set_diff)
```
```   277     done
```
```   278 qed (rule refl)
```
```   279
```
```   280
```
```   281 lemma inj_vimage_singleton: "inj f ==> f-`{a} \<subseteq> {THE x. f x = a}"
```
```   282   -- {* The inverse image of a singleton under an injective function
```
```   283          is included in a singleton. *}
```
```   284   apply (auto simp add: inj_on_def)
```
```   285   apply (blast intro: the_equality [symmetric])
```
```   286   done
```
```   287
```
```   288 lemma finite_vimageI: "[|finite F; inj h|] ==> finite (h -` F)"
```
```   289   -- {* The inverse image of a finite set under an injective function
```
```   290          is finite. *}
```
```   291   apply (induct set: finite)
```
```   292    apply simp_all
```
```   293   apply (subst vimage_insert)
```
```   294   apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
```
```   295   done
```
```   296
```
```   297
```
```   298 text {* The finite UNION of finite sets *}
```
```   299
```
```   300 lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
```
```   301   by (induct set: finite) simp_all
```
```   302
```
```   303 text {*
```
```   304   Strengthen RHS to
```
```   305   @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x \<noteq> {}})"}?
```
```   306
```
```   307   We'd need to prove
```
```   308   @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x \<noteq> {}}"}
```
```   309   by induction. *}
```
```   310
```
```   311 lemma finite_UN [simp]: "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
```
```   312   by (blast intro: finite_UN_I finite_subset)
```
```   313
```
```   314
```
```   315 lemma finite_Plus: "[| finite A; finite B |] ==> finite (A <+> B)"
```
```   316 by (simp add: Plus_def)
```
```   317
```
```   318 text {* Sigma of finite sets *}
```
```   319
```
```   320 lemma finite_SigmaI [simp]:
```
```   321     "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)"
```
```   322   by (unfold Sigma_def) (blast intro!: finite_UN_I)
```
```   323
```
```   324 lemma finite_cartesian_product: "[| finite A; finite B |] ==>
```
```   325     finite (A <*> B)"
```
```   326   by (rule finite_SigmaI)
```
```   327
```
```   328 lemma finite_Prod_UNIV:
```
```   329     "finite (UNIV::'a set) ==> finite (UNIV::'b set) ==> finite (UNIV::('a * 'b) set)"
```
```   330   apply (subgoal_tac "(UNIV:: ('a * 'b) set) = Sigma UNIV (%x. UNIV)")
```
```   331    apply (erule ssubst)
```
```   332    apply (erule finite_SigmaI, auto)
```
```   333   done
```
```   334
```
```   335 lemma finite_cartesian_productD1:
```
```   336      "[| finite (A <*> B); B \<noteq> {} |] ==> finite A"
```
```   337 apply (auto simp add: finite_conv_nat_seg_image)
```
```   338 apply (drule_tac x=n in spec)
```
```   339 apply (drule_tac x="fst o f" in spec)
```
```   340 apply (auto simp add: o_def)
```
```   341  prefer 2 apply (force dest!: equalityD2)
```
```   342 apply (drule equalityD1)
```
```   343 apply (rename_tac y x)
```
```   344 apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)")
```
```   345  prefer 2 apply force
```
```   346 apply clarify
```
```   347 apply (rule_tac x=k in image_eqI, auto)
```
```   348 done
```
```   349
```
```   350 lemma finite_cartesian_productD2:
```
```   351      "[| finite (A <*> B); A \<noteq> {} |] ==> finite B"
```
```   352 apply (auto simp add: finite_conv_nat_seg_image)
```
```   353 apply (drule_tac x=n in spec)
```
```   354 apply (drule_tac x="snd o f" in spec)
```
```   355 apply (auto simp add: o_def)
```
```   356  prefer 2 apply (force dest!: equalityD2)
```
```   357 apply (drule equalityD1)
```
```   358 apply (rename_tac x y)
```
```   359 apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)")
```
```   360  prefer 2 apply force
```
```   361 apply clarify
```
```   362 apply (rule_tac x=k in image_eqI, auto)
```
```   363 done
```
```   364
```
```   365
```
```   366 text {* The powerset of a finite set *}
```
```   367
```
```   368 lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A"
```
```   369 proof
```
```   370   assume "finite (Pow A)"
```
```   371   with _ have "finite ((%x. {x}) ` A)" by (rule finite_subset) blast
```
```   372   thus "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp
```
```   373 next
```
```   374   assume "finite A"
```
```   375   thus "finite (Pow A)"
```
```   376     by induct (simp_all add: finite_UnI finite_imageI Pow_insert)
```
```   377 qed
```
```   378
```
```   379
```
```   380 lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A"
```
```   381 by(blast intro: finite_subset[OF subset_Pow_Union])
```
```   382
```
```   383
```
```   384 lemma finite_converse [iff]: "finite (r^-1) = finite r"
```
```   385   apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
```
```   386    apply simp
```
```   387    apply (rule iffI)
```
```   388     apply (erule finite_imageD [unfolded inj_on_def])
```
```   389     apply (simp split add: split_split)
```
```   390    apply (erule finite_imageI)
```
```   391   apply (simp add: converse_def image_def, auto)
```
```   392   apply (rule bexI)
```
```   393    prefer 2 apply assumption
```
```   394   apply simp
```
```   395   done
```
```   396
```
```   397
```
```   398 text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi
```
```   399 Ehmety) *}
```
```   400
```
```   401 lemma finite_Field: "finite r ==> finite (Field r)"
```
```   402   -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
```
```   403   apply (induct set: finite)
```
```   404    apply (auto simp add: Field_def Domain_insert Range_insert)
```
```   405   done
```
```   406
```
```   407 lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
```
```   408   apply clarify
```
```   409   apply (erule trancl_induct)
```
```   410    apply (auto simp add: Field_def)
```
```   411   done
```
```   412
```
```   413 lemma finite_trancl: "finite (r^+) = finite r"
```
```   414   apply auto
```
```   415    prefer 2
```
```   416    apply (rule trancl_subset_Field2 [THEN finite_subset])
```
```   417    apply (rule finite_SigmaI)
```
```   418     prefer 3
```
```   419     apply (blast intro: r_into_trancl' finite_subset)
```
```   420    apply (auto simp add: finite_Field)
```
```   421   done
```
```   422
```
```   423
```
```   424 subsection {* Class @{text finite}  *}
```
```   425
```
```   426 setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
```
```   427 class finite = itself +
```
```   428   assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
```
```   429 setup {* Sign.parent_path *}
```
```   430 hide const finite
```
```   431
```
```   432 context finite
```
```   433 begin
```
```   434
```
```   435 lemma finite [simp]: "finite (A \<Colon> 'a set)"
```
```   436   by (rule subset_UNIV finite_UNIV finite_subset)+
```
```   437
```
```   438 end
```
```   439
```
```   440 lemma UNIV_unit [noatp]:
```
```   441   "UNIV = {()}" by auto
```
```   442
```
```   443 instance unit :: finite
```
```   444   by default (simp add: UNIV_unit)
```
```   445
```
```   446 lemma UNIV_bool [noatp]:
```
```   447   "UNIV = {False, True}" by auto
```
```   448
```
```   449 instance bool :: finite
```
```   450   by default (simp add: UNIV_bool)
```
```   451
```
```   452 instance * :: (finite, finite) finite
```
```   453   by default (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
```
```   454
```
```   455 lemma inj_graph: "inj (%f. {(x, y). y = f x})"
```
```   456   by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
```
```   457
```
```   458 instance "fun" :: (finite, finite) finite
```
```   459 proof
```
```   460   show "finite (UNIV :: ('a => 'b) set)"
```
```   461   proof (rule finite_imageD)
```
```   462     let ?graph = "%f::'a => 'b. {(x, y). y = f x}"
```
```   463     have "range ?graph \<subseteq> Pow UNIV" by simp
```
```   464     moreover have "finite (Pow (UNIV :: ('a * 'b) set))"
```
```   465       by (simp only: finite_Pow_iff finite)
```
```   466     ultimately show "finite (range ?graph)"
```
```   467       by (rule finite_subset)
```
```   468     show "inj ?graph" by (rule inj_graph)
```
```   469   qed
```
```   470 qed
```
```   471
```
```   472 instance "+" :: (finite, finite) finite
```
```   473   by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
```
```   474
```
```   475 instance option :: (finite) finite
```
```   476   by default (simp add: insert_None_conv_UNIV [symmetric])
```
```   477
```
```   478
```
```   479 subsection {* A fold functional for finite sets *}
```
```   480
```
```   481 text {* The intended behaviour is
```
```   482 @{text "fold f g z {x\<^isub>1, ..., x\<^isub>n} = f (g x\<^isub>1) (\<dots> (f (g x\<^isub>n) z)\<dots>)"}
```
```   483 if @{text f} is associative-commutative. For an application of @{text fold}
```
```   484 se the definitions of sums and products over finite sets.
```
```   485 *}
```
```   486
```
```   487 inductive
```
```   488   foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a => bool"
```
```   489   for f ::  "'a => 'a => 'a"
```
```   490   and g :: "'b => 'a"
```
```   491   and z :: 'a
```
```   492 where
```
```   493   emptyI [intro]: "foldSet f g z {} z"
```
```   494 | insertI [intro]:
```
```   495      "\<lbrakk> x \<notin> A; foldSet f g z A y \<rbrakk>
```
```   496       \<Longrightarrow> foldSet f g z (insert x A) (f (g x) y)"
```
```   497
```
```   498 inductive_cases empty_foldSetE [elim!]: "foldSet f g z {} x"
```
```   499
```
```   500 constdefs
```
```   501   fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a"
```
```   502   "fold f g z A == THE x. foldSet f g z A x"
```
```   503
```
```   504 text{*A tempting alternative for the definiens is
```
```   505 @{term "if finite A then THE x. foldSet f g e A x else e"}.
```
```   506 It allows the removal of finiteness assumptions from the theorems
```
```   507 @{text fold_commute}, @{text fold_reindex} and @{text fold_distrib}.
```
```   508 The proofs become ugly, with @{text rule_format}. It is not worth the effort.*}
```
```   509
```
```   510
```
```   511 lemma Diff1_foldSet:
```
```   512   "foldSet f g z (A - {x}) y ==> x: A ==> foldSet f g z A (f (g x) y)"
```
```   513 by (erule insert_Diff [THEN subst], rule foldSet.intros, auto)
```
```   514
```
```   515 lemma foldSet_imp_finite: "foldSet f g z A x==> finite A"
```
```   516   by (induct set: foldSet) auto
```
```   517
```
```   518 lemma finite_imp_foldSet: "finite A ==> EX x. foldSet f g z A x"
```
```   519   by (induct set: finite) auto
```
```   520
```
```   521
```
```   522 subsubsection{*From @{term foldSet} to @{term fold}*}
```
```   523
```
```   524 lemma image_less_Suc: "h ` {i. i < Suc m} = insert (h m) (h ` {i. i < m})"
```
```   525   by (auto simp add: less_Suc_eq)
```
```   526
```
```   527 lemma insert_image_inj_on_eq:
```
```   528      "[|insert (h m) A = h ` {i. i < Suc m}; h m \<notin> A;
```
```   529         inj_on h {i. i < Suc m}|]
```
```   530       ==> A = h ` {i. i < m}"
```
```   531 apply (auto simp add: image_less_Suc inj_on_def)
```
```   532 apply (blast intro: less_trans)
```
```   533 done
```
```   534
```
```   535 lemma insert_inj_onE:
```
```   536   assumes aA: "insert a A = h`{i::nat. i<n}" and anot: "a \<notin> A"
```
```   537       and inj_on: "inj_on h {i::nat. i<n}"
```
```   538   shows "\<exists>hm m. inj_on hm {i::nat. i<m} & A = hm ` {i. i<m} & m < n"
```
```   539 proof (cases n)
```
```   540   case 0 thus ?thesis using aA by auto
```
```   541 next
```
```   542   case (Suc m)
```
```   543   have nSuc: "n = Suc m" by fact
```
```   544   have mlessn: "m<n" by (simp add: nSuc)
```
```   545   from aA obtain k where hkeq: "h k = a" and klessn: "k<n" by (blast elim!: equalityE)
```
```   546   let ?hm = "Fun.swap k m h"
```
```   547   have inj_hm: "inj_on ?hm {i. i < n}" using klessn mlessn
```
```   548     by (simp add: inj_on_swap_iff inj_on)
```
```   549   show ?thesis
```
```   550   proof (intro exI conjI)
```
```   551     show "inj_on ?hm {i. i < m}" using inj_hm
```
```   552       by (auto simp add: nSuc less_Suc_eq intro: subset_inj_on)
```
```   553     show "m<n" by (rule mlessn)
```
```   554     show "A = ?hm ` {i. i < m}"
```
```   555     proof (rule insert_image_inj_on_eq)
```
```   556       show "inj_on (Fun.swap k m h) {i. i < Suc m}" using inj_hm nSuc by simp
```
```   557       show "?hm m \<notin> A" by (simp add: swap_def hkeq anot)
```
```   558       show "insert (?hm m) A = ?hm ` {i. i < Suc m}"
```
```   559 	using aA hkeq nSuc klessn
```
```   560 	by (auto simp add: swap_def image_less_Suc fun_upd_image
```
```   561 			   less_Suc_eq inj_on_image_set_diff [OF inj_on])
```
```   562     qed
```
```   563   qed
```
```   564 qed
```
```   565
```
```   566 context ab_semigroup_mult
```
```   567 begin
```
```   568
```
```   569 lemma foldSet_determ_aux:
```
```   570   "!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; inj_on h {i. i<n};
```
```   571                 foldSet times g z A x; foldSet times g z A x' \<rbrakk>
```
```   572    \<Longrightarrow> x' = x"
```
```   573 proof (induct n rule: less_induct)
```
```   574   case (less n)
```
```   575     have IH: "!!m h A x x'.
```
```   576                \<lbrakk>m<n; A = h ` {i. i<m}; inj_on h {i. i<m};
```
```   577                 foldSet times g z A x; foldSet times g z A x'\<rbrakk> \<Longrightarrow> x' = x" by fact
```
```   578     have Afoldx: "foldSet times g z A x" and Afoldx': "foldSet times g z A x'"
```
```   579      and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" by fact+
```
```   580     show ?case
```
```   581     proof (rule foldSet.cases [OF Afoldx])
```
```   582       assume "A = {}" and "x = z"
```
```   583       with Afoldx' show "x' = x" by blast
```
```   584     next
```
```   585       fix B b u
```
```   586       assume AbB: "A = insert b B" and x: "x = g b * u"
```
```   587          and notinB: "b \<notin> B" and Bu: "foldSet times g z B u"
```
```   588       show "x'=x"
```
```   589       proof (rule foldSet.cases [OF Afoldx'])
```
```   590         assume "A = {}" and "x' = z"
```
```   591         with AbB show "x' = x" by blast
```
```   592       next
```
```   593 	fix C c v
```
```   594 	assume AcC: "A = insert c C" and x': "x' = g c * v"
```
```   595            and notinC: "c \<notin> C" and Cv: "foldSet times g z C v"
```
```   596 	from A AbB have Beq: "insert b B = h`{i. i<n}" by simp
```
```   597         from insert_inj_onE [OF Beq notinB injh]
```
```   598         obtain hB mB where inj_onB: "inj_on hB {i. i < mB}"
```
```   599                      and Beq: "B = hB ` {i. i < mB}"
```
```   600                      and lessB: "mB < n" by auto
```
```   601 	from A AcC have Ceq: "insert c C = h`{i. i<n}" by simp
```
```   602         from insert_inj_onE [OF Ceq notinC injh]
```
```   603         obtain hC mC where inj_onC: "inj_on hC {i. i < mC}"
```
```   604                        and Ceq: "C = hC ` {i. i < mC}"
```
```   605                        and lessC: "mC < n" by auto
```
```   606 	show "x'=x"
```
```   607 	proof cases
```
```   608           assume "b=c"
```
```   609 	  then moreover have "B = C" using AbB AcC notinB notinC by auto
```
```   610 	  ultimately show ?thesis  using Bu Cv x x' IH[OF lessC Ceq inj_onC]
```
```   611             by auto
```
```   612 	next
```
```   613 	  assume diff: "b \<noteq> c"
```
```   614 	  let ?D = "B - {c}"
```
```   615 	  have B: "B = insert c ?D" and C: "C = insert b ?D"
```
```   616 	    using AbB AcC notinB notinC diff by(blast elim!:equalityE)+
```
```   617 	  have "finite A" by(rule foldSet_imp_finite[OF Afoldx])
```
```   618 	  with AbB have "finite ?D" by simp
```
```   619 	  then obtain d where Dfoldd: "foldSet times g z ?D d"
```
```   620 	    using finite_imp_foldSet by iprover
```
```   621 	  moreover have cinB: "c \<in> B" using B by auto
```
```   622 	  ultimately have "foldSet times g z B (g c * d)"
```
```   623 	    by(rule Diff1_foldSet)
```
```   624 	  then have "g c * d = u" by (rule IH [OF lessB Beq inj_onB Bu])
```
```   625           then have "u = g c * d" ..
```
```   626           moreover have "v = g b * d"
```
```   627 	  proof (rule sym, rule IH [OF lessC Ceq inj_onC Cv])
```
```   628 	    show "foldSet times g z C (g b * d)" using C notinB Dfoldd
```
```   629 	      by fastsimp
```
```   630 	  qed
```
```   631 	  ultimately show ?thesis using x x'
```
```   632 	    by (simp add: mult_left_commute)
```
```   633 	qed
```
```   634       qed
```
```   635     qed
```
```   636   qed
```
```   637
```
```   638 lemma foldSet_determ:
```
```   639   "foldSet times g z A x ==> foldSet times g z A y ==> y = x"
```
```   640 apply (frule foldSet_imp_finite [THEN finite_imp_nat_seg_image_inj_on])
```
```   641 apply (blast intro: foldSet_determ_aux [rule_format])
```
```   642 done
```
```   643
```
```   644 lemma fold_equality: "foldSet times g z A y ==> fold times g z A = y"
```
```   645   by (unfold fold_def) (blast intro: foldSet_determ)
```
```   646
```
```   647 text{* The base case for @{text fold}: *}
```
```   648
```
```   649 lemma (in -) fold_empty [simp]: "fold f g z {} = z"
```
```   650   by (unfold fold_def) blast
```
```   651
```
```   652 lemma fold_insert_aux: "x \<notin> A ==>
```
```   653     (foldSet times g z (insert x A) v) =
```
```   654     (EX y. foldSet times g z A y & v = g x * y)"
```
```   655   apply auto
```
```   656   apply (rule_tac A1 = A and f1 = times in finite_imp_foldSet [THEN exE])
```
```   657    apply (fastsimp dest: foldSet_imp_finite)
```
```   658   apply (blast intro: foldSet_determ)
```
```   659   done
```
```   660
```
```   661 text{* The recursion equation for @{text fold}: *}
```
```   662
```
```   663 lemma fold_insert [simp]:
```
```   664     "finite A ==> x \<notin> A ==> fold times g z (insert x A) = g x * fold times g z A"
```
```   665   apply (unfold fold_def)
```
```   666   apply (simp add: fold_insert_aux)
```
```   667   apply (rule the_equality)
```
```   668   apply (auto intro: finite_imp_foldSet
```
```   669     cong add: conj_cong simp add: fold_def [symmetric] fold_equality)
```
```   670   done
```
```   671
```
```   672 lemma fold_rec:
```
```   673 assumes fin: "finite A" and a: "a:A"
```
```   674 shows "fold times g z A = g a * fold times g z (A - {a})"
```
```   675 proof-
```
```   676   have A: "A = insert a (A - {a})" using a by blast
```
```   677   hence "fold times g z A = fold times g z (insert a (A - {a}))" by simp
```
```   678   also have "\<dots> = g a * fold times g z (A - {a})"
```
```   679     by(rule fold_insert) (simp add:fin)+
```
```   680   finally show ?thesis .
```
```   681 qed
```
```   682
```
```   683 end
```
```   684
```
```   685 text{* A simplified version for idempotent functions: *}
```
```   686
```
```   687 context ab_semigroup_idem_mult
```
```   688 begin
```
```   689
```
```   690 lemma fold_insert_idem:
```
```   691 assumes finA: "finite A"
```
```   692 shows "fold times g z (insert a A) = g a * fold times g z A"
```
```   693 proof cases
```
```   694   assume "a \<in> A"
```
```   695   then obtain B where A: "A = insert a B" and disj: "a \<notin> B"
```
```   696     by(blast dest: mk_disjoint_insert)
```
```   697   show ?thesis
```
```   698   proof -
```
```   699     from finA A have finB: "finite B" by(blast intro: finite_subset)
```
```   700     have "fold times g z (insert a A) = fold times g z (insert a B)" using A by simp
```
```   701     also have "\<dots> = g a * fold times g z B"
```
```   702       using finB disj by simp
```
```   703     also have "\<dots> = g a * fold times g z A"
```
```   704       using A finB disj
```
```   705 	by (simp add: mult_idem mult_assoc [symmetric])
```
```   706     finally show ?thesis .
```
```   707   qed
```
```   708 next
```
```   709   assume "a \<notin> A"
```
```   710   with finA show ?thesis by simp
```
```   711 qed
```
```   712
```
```   713 lemma foldI_conv_id:
```
```   714   "finite A \<Longrightarrow> fold times g z A = fold times id z (g ` A)"
```
```   715 by(erule finite_induct)(simp_all add: fold_insert_idem del: fold_insert)
```
```   716
```
```   717 end
```
```   718
```
```   719 subsubsection{*Lemmas about @{text fold}*}
```
```   720
```
```   721 context ab_semigroup_mult
```
```   722 begin
```
```   723
```
```   724 lemma fold_commute:
```
```   725   "finite A ==> (!!z. x * (fold times g z A) = fold times g (x * z) A)"
```
```   726   apply (induct set: finite)
```
```   727    apply simp
```
```   728   apply (simp add: mult_left_commute [of x])
```
```   729   done
```
```   730
```
```   731 lemma fold_nest_Un_Int:
```
```   732   "finite A ==> finite B
```
```   733     ==> fold times g (fold times g z B) A = fold times g (fold times g z (A Int B)) (A Un B)"
```
```   734   apply (induct set: finite)
```
```   735    apply simp
```
```   736   apply (simp add: fold_commute Int_insert_left insert_absorb)
```
```   737   done
```
```   738
```
```   739 lemma fold_nest_Un_disjoint:
```
```   740   "finite A ==> finite B ==> A Int B = {}
```
```   741     ==> fold times g z (A Un B) = fold times g (fold times g z B) A"
```
```   742   by (simp add: fold_nest_Un_Int)
```
```   743
```
```   744 lemma fold_reindex:
```
```   745 assumes fin: "finite A"
```
```   746 shows "inj_on h A \<Longrightarrow> fold times g z (h ` A) = fold times (g \<circ> h) z A"
```
```   747 using fin apply induct
```
```   748  apply simp
```
```   749 apply simp
```
```   750 done
```
```   751
```
```   752 text{*
```
```   753   Fusion theorem, as described in Graham Hutton's paper,
```
```   754   A Tutorial on the Universality and Expressiveness of Fold,
```
```   755   JFP 9:4 (355-372), 1999.
```
```   756 *}
```
```   757
```
```   758 lemma fold_fusion:
```
```   759   assumes "ab_semigroup_mult g"
```
```   760   assumes fin: "finite A"
```
```   761     and hyp: "\<And>x y. h (g x y) = times x (h y)"
```
```   762   shows "h (fold g j w A) = fold times j (h w) A"
```
```   763 proof -
```
```   764   interpret ab_semigroup_mult [g] by fact
```
```   765   show ?thesis using fin hyp by (induct set: finite) simp_all
```
```   766 qed
```
```   767
```
```   768 lemma fold_cong:
```
```   769   "finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold times g z A = fold times h z A"
```
```   770   apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold times g z C = fold times h z C")
```
```   771    apply simp
```
```   772   apply (erule finite_induct, simp)
```
```   773   apply (simp add: subset_insert_iff, clarify)
```
```   774   apply (subgoal_tac "finite C")
```
```   775    prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
```
```   776   apply (subgoal_tac "C = insert x (C - {x})")
```
```   777    prefer 2 apply blast
```
```   778   apply (erule ssubst)
```
```   779   apply (drule spec)
```
```   780   apply (erule (1) notE impE)
```
```   781   apply (simp add: Ball_def del: insert_Diff_single)
```
```   782   done
```
```   783
```
```   784 end
```
```   785
```
```   786 context comm_monoid_mult
```
```   787 begin
```
```   788
```
```   789 lemma fold_Un_Int:
```
```   790   "finite A ==> finite B ==>
```
```   791     fold times g 1 A * fold times g 1 B =
```
```   792     fold times g 1 (A Un B) * fold times g 1 (A Int B)"
```
```   793   by (induct set: finite)
```
```   794     (auto simp add: mult_ac insert_absorb Int_insert_left)
```
```   795
```
```   796 corollary fold_Un_disjoint:
```
```   797   "finite A ==> finite B ==> A Int B = {} ==>
```
```   798     fold times g 1 (A Un B) = fold times g 1 A * fold times g 1 B"
```
```   799   by (simp add: fold_Un_Int)
```
```   800
```
```   801 lemma fold_UN_disjoint:
```
```   802   "\<lbrakk> finite I; ALL i:I. finite (A i);
```
```   803      ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {} \<rbrakk>
```
```   804    \<Longrightarrow> fold times g 1 (UNION I A) =
```
```   805        fold times (%i. fold times g 1 (A i)) 1 I"
```
```   806   apply (induct set: finite, simp, atomize)
```
```   807   apply (subgoal_tac "ALL i:F. x \<noteq> i")
```
```   808    prefer 2 apply blast
```
```   809   apply (subgoal_tac "A x Int UNION F A = {}")
```
```   810    prefer 2 apply blast
```
```   811   apply (simp add: fold_Un_disjoint)
```
```   812   done
```
```   813
```
```   814 lemma fold_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
```
```   815   fold times (%x. fold times (g x) 1 (B x)) 1 A =
```
```   816   fold times (split g) 1 (SIGMA x:A. B x)"
```
```   817 apply (subst Sigma_def)
```
```   818 apply (subst fold_UN_disjoint, assumption, simp)
```
```   819  apply blast
```
```   820 apply (erule fold_cong)
```
```   821 apply (subst fold_UN_disjoint, simp, simp)
```
```   822  apply blast
```
```   823 apply simp
```
```   824 done
```
```   825
```
```   826 lemma fold_distrib: "finite A \<Longrightarrow>
```
```   827    fold times (%x. g x * h x) 1 A = fold times g 1 A *  fold times h 1 A"
```
```   828   by (erule finite_induct) (simp_all add: mult_ac)
```
```   829
```
```   830 end
```
```   831
```
```   832
```
```   833 subsection {* Generalized summation over a set *}
```
```   834
```
```   835 interpretation comm_monoid_add: comm_monoid_mult ["0::'a::comm_monoid_add" "op +"]
```
```   836   by unfold_locales (auto intro: add_assoc add_commute)
```
```   837
```
```   838 constdefs
```
```   839   setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
```
```   840   "setsum f A == if finite A then fold (op +) f 0 A else 0"
```
```   841
```
```   842 abbreviation
```
```   843   Setsum  ("\<Sum>_"  999) where
```
```   844   "\<Sum>A == setsum (%x. x) A"
```
```   845
```
```   846 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
```
```   847 written @{text"\<Sum>x\<in>A. e"}. *}
```
```   848
```
```   849 syntax
```
```   850   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
```
```   851 syntax (xsymbols)
```
```   852   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
```
```   853 syntax (HTML output)
```
```   854   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
```
```   855
```
```   856 translations -- {* Beware of argument permutation! *}
```
```   857   "SUM i:A. b" == "setsum (%i. b) A"
```
```   858   "\<Sum>i\<in>A. b" == "setsum (%i. b) A"
```
```   859
```
```   860 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
```
```   861  @{text"\<Sum>x|P. e"}. *}
```
```   862
```
```   863 syntax
```
```   864   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
```
```   865 syntax (xsymbols)
```
```   866   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
```
```   867 syntax (HTML output)
```
```   868   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
```
```   869
```
```   870 translations
```
```   871   "SUM x|P. t" => "setsum (%x. t) {x. P}"
```
```   872   "\<Sum>x|P. t" => "setsum (%x. t) {x. P}"
```
```   873
```
```   874 print_translation {*
```
```   875 let
```
```   876   fun setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) \$ Abs(y,Ty,P)] =
```
```   877     if x<>y then raise Match
```
```   878     else let val x' = Syntax.mark_bound x
```
```   879              val t' = subst_bound(x',t)
```
```   880              val P' = subst_bound(x',P)
```
```   881          in Syntax.const "_qsetsum" \$ Syntax.mark_bound x \$ P' \$ t' end
```
```   882 in [("setsum", setsum_tr')] end
```
```   883 *}
```
```   884
```
```   885
```
```   886 lemma setsum_empty [simp]: "setsum f {} = 0"
```
```   887   by (simp add: setsum_def)
```
```   888
```
```   889 lemma setsum_insert [simp]:
```
```   890     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
```
```   891   by (simp add: setsum_def)
```
```   892
```
```   893 lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0"
```
```   894   by (simp add: setsum_def)
```
```   895
```
```   896 lemma setsum_reindex:
```
```   897      "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
```
```   898 by(auto simp add: setsum_def comm_monoid_add.fold_reindex dest!:finite_imageD)
```
```   899
```
```   900 lemma setsum_reindex_id:
```
```   901      "inj_on f B ==> setsum f B = setsum id (f ` B)"
```
```   902 by (auto simp add: setsum_reindex)
```
```   903
```
```   904 lemma setsum_cong:
```
```   905   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
```
```   906 by(fastsimp simp: setsum_def intro: comm_monoid_add.fold_cong)
```
```   907
```
```   908 lemma strong_setsum_cong[cong]:
```
```   909   "A = B ==> (!!x. x:B =simp=> f x = g x)
```
```   910    ==> setsum (%x. f x) A = setsum (%x. g x) B"
```
```   911 by(fastsimp simp: simp_implies_def setsum_def intro: comm_monoid_add.fold_cong)
```
```   912
```
```   913 lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A";
```
```   914   by (rule setsum_cong[OF refl], auto);
```
```   915
```
```   916 lemma setsum_reindex_cong:
```
```   917      "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|]
```
```   918       ==> setsum h B = setsum g A"
```
```   919   by (simp add: setsum_reindex cong: setsum_cong)
```
```   920
```
```   921 lemma setsum_0[simp]: "setsum (%i. 0) A = 0"
```
```   922 apply (clarsimp simp: setsum_def)
```
```   923 apply (erule finite_induct, auto)
```
```   924 done
```
```   925
```
```   926 lemma setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0"
```
```   927 by(simp add:setsum_cong)
```
```   928
```
```   929 lemma setsum_Un_Int: "finite A ==> finite B ==>
```
```   930   setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
```
```   931   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
```
```   932 by(simp add: setsum_def comm_monoid_add.fold_Un_Int [symmetric])
```
```   933
```
```   934 lemma setsum_Un_disjoint: "finite A ==> finite B
```
```   935   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
```
```   936 by (subst setsum_Un_Int [symmetric], auto)
```
```   937
```
```   938 (*But we can't get rid of finite I. If infinite, although the rhs is 0,
```
```   939   the lhs need not be, since UNION I A could still be finite.*)
```
```   940 lemma setsum_UN_disjoint:
```
```   941     "finite I ==> (ALL i:I. finite (A i)) ==>
```
```   942         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
```
```   943       setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
```
```   944 by(simp add: setsum_def comm_monoid_add.fold_UN_disjoint cong: setsum_cong)
```
```   945
```
```   946 text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
```
```   947 directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
```
```   948 lemma setsum_Union_disjoint:
```
```   949   "[| (ALL A:C. finite A);
```
```   950       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
```
```   951    ==> setsum f (Union C) = setsum (setsum f) C"
```
```   952 apply (cases "finite C")
```
```   953  prefer 2 apply (force dest: finite_UnionD simp add: setsum_def)
```
```   954   apply (frule setsum_UN_disjoint [of C id f])
```
```   955  apply (unfold Union_def id_def, assumption+)
```
```   956 done
```
```   957
```
```   958 (*But we can't get rid of finite A. If infinite, although the lhs is 0,
```
```   959   the rhs need not be, since SIGMA A B could still be finite.*)
```
```   960 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
```
```   961     (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
```
```   962 by(simp add:setsum_def comm_monoid_add.fold_Sigma split_def cong:setsum_cong)
```
```   963
```
```   964 text{*Here we can eliminate the finiteness assumptions, by cases.*}
```
```   965 lemma setsum_cartesian_product:
```
```   966    "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)"
```
```   967 apply (cases "finite A")
```
```   968  apply (cases "finite B")
```
```   969   apply (simp add: setsum_Sigma)
```
```   970  apply (cases "A={}", simp)
```
```   971  apply (simp)
```
```   972 apply (auto simp add: setsum_def
```
```   973             dest: finite_cartesian_productD1 finite_cartesian_productD2)
```
```   974 done
```
```   975
```
```   976 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
```
```   977 by(simp add:setsum_def comm_monoid_add.fold_distrib)
```
```   978
```
```   979
```
```   980 subsubsection {* Properties in more restricted classes of structures *}
```
```   981
```
```   982 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
```
```   983   apply (case_tac "finite A")
```
```   984    prefer 2 apply (simp add: setsum_def)
```
```   985   apply (erule rev_mp)
```
```   986   apply (erule finite_induct, auto)
```
```   987   done
```
```   988
```
```   989 lemma setsum_eq_0_iff [simp]:
```
```   990     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
```
```   991   by (induct set: finite) auto
```
```   992
```
```   993 lemma setsum_Un_nat: "finite A ==> finite B ==>
```
```   994     (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
```
```   995   -- {* For the natural numbers, we have subtraction. *}
```
```   996   by (subst setsum_Un_Int [symmetric], auto simp add: ring_simps)
```
```   997
```
```   998 lemma setsum_Un: "finite A ==> finite B ==>
```
```   999     (setsum f (A Un B) :: 'a :: ab_group_add) =
```
```  1000       setsum f A + setsum f B - setsum f (A Int B)"
```
```  1001   by (subst setsum_Un_Int [symmetric], auto simp add: ring_simps)
```
```  1002
```
```  1003 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
```
```  1004     (if a:A then setsum f A - f a else setsum f A)"
```
```  1005   apply (case_tac "finite A")
```
```  1006    prefer 2 apply (simp add: setsum_def)
```
```  1007   apply (erule finite_induct)
```
```  1008    apply (auto simp add: insert_Diff_if)
```
```  1009   apply (drule_tac a = a in mk_disjoint_insert, auto)
```
```  1010   done
```
```  1011
```
```  1012 lemma setsum_diff1: "finite A \<Longrightarrow>
```
```  1013   (setsum f (A - {a}) :: ('a::ab_group_add)) =
```
```  1014   (if a:A then setsum f A - f a else setsum f A)"
```
```  1015   by (erule finite_induct) (auto simp add: insert_Diff_if)
```
```  1016
```
```  1017 lemma setsum_diff1'[rule_format]: "finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x)"
```
```  1018   apply (erule finite_induct[where F=A and P="% A. (a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x))"])
```
```  1019   apply (auto simp add: insert_Diff_if add_ac)
```
```  1020   done
```
```  1021
```
```  1022 (* By Jeremy Siek: *)
```
```  1023
```
```  1024 lemma setsum_diff_nat:
```
```  1025   assumes "finite B"
```
```  1026     and "B \<subseteq> A"
```
```  1027   shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
```
```  1028   using prems
```
```  1029 proof induct
```
```  1030   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
```
```  1031 next
```
```  1032   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
```
```  1033     and xFinA: "insert x F \<subseteq> A"
```
```  1034     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
```
```  1035   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
```
```  1036   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
```
```  1037     by (simp add: setsum_diff1_nat)
```
```  1038   from xFinA have "F \<subseteq> A" by simp
```
```  1039   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
```
```  1040   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
```
```  1041     by simp
```
```  1042   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
```
```  1043   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
```
```  1044     by simp
```
```  1045   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
```
```  1046   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
```
```  1047     by simp
```
```  1048   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
```
```  1049 qed
```
```  1050
```
```  1051 lemma setsum_diff:
```
```  1052   assumes le: "finite A" "B \<subseteq> A"
```
```  1053   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
```
```  1054 proof -
```
```  1055   from le have finiteB: "finite B" using finite_subset by auto
```
```  1056   show ?thesis using finiteB le
```
```  1057   proof induct
```
```  1058     case empty
```
```  1059     thus ?case by auto
```
```  1060   next
```
```  1061     case (insert x F)
```
```  1062     thus ?case using le finiteB
```
```  1063       by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
```
```  1064   qed
```
```  1065 qed
```
```  1066
```
```  1067 lemma setsum_mono:
```
```  1068   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))"
```
```  1069   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
```
```  1070 proof (cases "finite K")
```
```  1071   case True
```
```  1072   thus ?thesis using le
```
```  1073   proof induct
```
```  1074     case empty
```
```  1075     thus ?case by simp
```
```  1076   next
```
```  1077     case insert
```
```  1078     thus ?case using add_mono by fastsimp
```
```  1079   qed
```
```  1080 next
```
```  1081   case False
```
```  1082   thus ?thesis
```
```  1083     by (simp add: setsum_def)
```
```  1084 qed
```
```  1085
```
```  1086 lemma setsum_strict_mono:
```
```  1087   fixes f :: "'a \<Rightarrow> 'b::{pordered_cancel_ab_semigroup_add,comm_monoid_add}"
```
```  1088   assumes "finite A"  "A \<noteq> {}"
```
```  1089     and "!!x. x:A \<Longrightarrow> f x < g x"
```
```  1090   shows "setsum f A < setsum g A"
```
```  1091   using prems
```
```  1092 proof (induct rule: finite_ne_induct)
```
```  1093   case singleton thus ?case by simp
```
```  1094 next
```
```  1095   case insert thus ?case by (auto simp: add_strict_mono)
```
```  1096 qed
```
```  1097
```
```  1098 lemma setsum_negf:
```
```  1099   "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
```
```  1100 proof (cases "finite A")
```
```  1101   case True thus ?thesis by (induct set: finite) auto
```
```  1102 next
```
```  1103   case False thus ?thesis by (simp add: setsum_def)
```
```  1104 qed
```
```  1105
```
```  1106 lemma setsum_subtractf:
```
```  1107   "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
```
```  1108     setsum f A - setsum g A"
```
```  1109 proof (cases "finite A")
```
```  1110   case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
```
```  1111 next
```
```  1112   case False thus ?thesis by (simp add: setsum_def)
```
```  1113 qed
```
```  1114
```
```  1115 lemma setsum_nonneg:
```
```  1116   assumes nn: "\<forall>x\<in>A. (0::'a::{pordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
```
```  1117   shows "0 \<le> setsum f A"
```
```  1118 proof (cases "finite A")
```
```  1119   case True thus ?thesis using nn
```
```  1120   proof induct
```
```  1121     case empty then show ?case by simp
```
```  1122   next
```
```  1123     case (insert x F)
```
```  1124     then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
```
```  1125     with insert show ?case by simp
```
```  1126   qed
```
```  1127 next
```
```  1128   case False thus ?thesis by (simp add: setsum_def)
```
```  1129 qed
```
```  1130
```
```  1131 lemma setsum_nonpos:
```
```  1132   assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{pordered_ab_semigroup_add,comm_monoid_add})"
```
```  1133   shows "setsum f A \<le> 0"
```
```  1134 proof (cases "finite A")
```
```  1135   case True thus ?thesis using np
```
```  1136   proof induct
```
```  1137     case empty then show ?case by simp
```
```  1138   next
```
```  1139     case (insert x F)
```
```  1140     then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
```
```  1141     with insert show ?case by simp
```
```  1142   qed
```
```  1143 next
```
```  1144   case False thus ?thesis by (simp add: setsum_def)
```
```  1145 qed
```
```  1146
```
```  1147 lemma setsum_mono2:
```
```  1148 fixes f :: "'a \<Rightarrow> 'b :: {pordered_ab_semigroup_add_imp_le,comm_monoid_add}"
```
```  1149 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
```
```  1150 shows "setsum f A \<le> setsum f B"
```
```  1151 proof -
```
```  1152   have "setsum f A \<le> setsum f A + setsum f (B-A)"
```
```  1153     by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
```
```  1154   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
```
```  1155     by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
```
```  1156   also have "A \<union> (B-A) = B" using sub by blast
```
```  1157   finally show ?thesis .
```
```  1158 qed
```
```  1159
```
```  1160 lemma setsum_mono3: "finite B ==> A <= B ==>
```
```  1161     ALL x: B - A.
```
```  1162       0 <= ((f x)::'a::{comm_monoid_add,pordered_ab_semigroup_add}) ==>
```
```  1163         setsum f A <= setsum f B"
```
```  1164   apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
```
```  1165   apply (erule ssubst)
```
```  1166   apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
```
```  1167   apply simp
```
```  1168   apply (rule add_left_mono)
```
```  1169   apply (erule setsum_nonneg)
```
```  1170   apply (subst setsum_Un_disjoint [THEN sym])
```
```  1171   apply (erule finite_subset, assumption)
```
```  1172   apply (rule finite_subset)
```
```  1173   prefer 2
```
```  1174   apply assumption
```
```  1175   apply auto
```
```  1176   apply (rule setsum_cong)
```
```  1177   apply auto
```
```  1178 done
```
```  1179
```
```  1180 lemma setsum_right_distrib:
```
```  1181   fixes f :: "'a => ('b::semiring_0)"
```
```  1182   shows "r * setsum f A = setsum (%n. r * f n) A"
```
```  1183 proof (cases "finite A")
```
```  1184   case True
```
```  1185   thus ?thesis
```
```  1186   proof induct
```
```  1187     case empty thus ?case by simp
```
```  1188   next
```
```  1189     case (insert x A) thus ?case by (simp add: right_distrib)
```
```  1190   qed
```
```  1191 next
```
```  1192   case False thus ?thesis by (simp add: setsum_def)
```
```  1193 qed
```
```  1194
```
```  1195 lemma setsum_left_distrib:
```
```  1196   "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
```
```  1197 proof (cases "finite A")
```
```  1198   case True
```
```  1199   then show ?thesis
```
```  1200   proof induct
```
```  1201     case empty thus ?case by simp
```
```  1202   next
```
```  1203     case (insert x A) thus ?case by (simp add: left_distrib)
```
```  1204   qed
```
```  1205 next
```
```  1206   case False thus ?thesis by (simp add: setsum_def)
```
```  1207 qed
```
```  1208
```
```  1209 lemma setsum_divide_distrib:
```
```  1210   "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
```
```  1211 proof (cases "finite A")
```
```  1212   case True
```
```  1213   then show ?thesis
```
```  1214   proof induct
```
```  1215     case empty thus ?case by simp
```
```  1216   next
```
```  1217     case (insert x A) thus ?case by (simp add: add_divide_distrib)
```
```  1218   qed
```
```  1219 next
```
```  1220   case False thus ?thesis by (simp add: setsum_def)
```
```  1221 qed
```
```  1222
```
```  1223 lemma setsum_abs[iff]:
```
```  1224   fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
```
```  1225   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
```
```  1226 proof (cases "finite A")
```
```  1227   case True
```
```  1228   thus ?thesis
```
```  1229   proof induct
```
```  1230     case empty thus ?case by simp
```
```  1231   next
```
```  1232     case (insert x A)
```
```  1233     thus ?case by (auto intro: abs_triangle_ineq order_trans)
```
```  1234   qed
```
```  1235 next
```
```  1236   case False thus ?thesis by (simp add: setsum_def)
```
```  1237 qed
```
```  1238
```
```  1239 lemma setsum_abs_ge_zero[iff]:
```
```  1240   fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
```
```  1241   shows "0 \<le> setsum (%i. abs(f i)) A"
```
```  1242 proof (cases "finite A")
```
```  1243   case True
```
```  1244   thus ?thesis
```
```  1245   proof induct
```
```  1246     case empty thus ?case by simp
```
```  1247   next
```
```  1248     case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg)
```
```  1249   qed
```
```  1250 next
```
```  1251   case False thus ?thesis by (simp add: setsum_def)
```
```  1252 qed
```
```  1253
```
```  1254 lemma abs_setsum_abs[simp]:
```
```  1255   fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
```
```  1256   shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
```
```  1257 proof (cases "finite A")
```
```  1258   case True
```
```  1259   thus ?thesis
```
```  1260   proof induct
```
```  1261     case empty thus ?case by simp
```
```  1262   next
```
```  1263     case (insert a A)
```
```  1264     hence "\<bar>\<Sum>a\<in>insert a A. \<bar>f a\<bar>\<bar> = \<bar>\<bar>f a\<bar> + (\<Sum>a\<in>A. \<bar>f a\<bar>)\<bar>" by simp
```
```  1265     also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
```
```  1266     also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
```
```  1267       by (simp del: abs_of_nonneg)
```
```  1268     also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
```
```  1269     finally show ?case .
```
```  1270   qed
```
```  1271 next
```
```  1272   case False thus ?thesis by (simp add: setsum_def)
```
```  1273 qed
```
```  1274
```
```  1275
```
```  1276 text {* Commuting outer and inner summation *}
```
```  1277
```
```  1278 lemma swap_inj_on:
```
```  1279   "inj_on (%(i, j). (j, i)) (A \<times> B)"
```
```  1280   by (unfold inj_on_def) fast
```
```  1281
```
```  1282 lemma swap_product:
```
```  1283   "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
```
```  1284   by (simp add: split_def image_def) blast
```
```  1285
```
```  1286 lemma setsum_commute:
```
```  1287   "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
```
```  1288 proof (simp add: setsum_cartesian_product)
```
```  1289   have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
```
```  1290     (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
```
```  1291     (is "?s = _")
```
```  1292     apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on)
```
```  1293     apply (simp add: split_def)
```
```  1294     done
```
```  1295   also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
```
```  1296     (is "_ = ?t")
```
```  1297     apply (simp add: swap_product)
```
```  1298     done
```
```  1299   finally show "?s = ?t" .
```
```  1300 qed
```
```  1301
```
```  1302 lemma setsum_product:
```
```  1303   fixes f :: "'a => ('b::semiring_0)"
```
```  1304   shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
```
```  1305   by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
```
```  1306
```
```  1307
```
```  1308 subsection {* Generalized product over a set *}
```
```  1309
```
```  1310 constdefs
```
```  1311   setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
```
```  1312   "setprod f A == if finite A then fold (op *) f 1 A else 1"
```
```  1313
```
```  1314 abbreviation
```
```  1315   Setprod  ("\<Prod>_"  999) where
```
```  1316   "\<Prod>A == setprod (%x. x) A"
```
```  1317
```
```  1318 syntax
```
```  1319   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
```
```  1320 syntax (xsymbols)
```
```  1321   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
```
```  1322 syntax (HTML output)
```
```  1323   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
```
```  1324
```
```  1325 translations -- {* Beware of argument permutation! *}
```
```  1326   "PROD i:A. b" == "setprod (%i. b) A"
```
```  1327   "\<Prod>i\<in>A. b" == "setprod (%i. b) A"
```
```  1328
```
```  1329 text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
```
```  1330  @{text"\<Prod>x|P. e"}. *}
```
```  1331
```
```  1332 syntax
```
```  1333   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
```
```  1334 syntax (xsymbols)
```
```  1335   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
```
```  1336 syntax (HTML output)
```
```  1337   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
```
```  1338
```
```  1339 translations
```
```  1340   "PROD x|P. t" => "setprod (%x. t) {x. P}"
```
```  1341   "\<Prod>x|P. t" => "setprod (%x. t) {x. P}"
```
```  1342
```
```  1343
```
```  1344 lemma setprod_empty [simp]: "setprod f {} = 1"
```
```  1345   by (auto simp add: setprod_def)
```
```  1346
```
```  1347 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
```
```  1348     setprod f (insert a A) = f a * setprod f A"
```
```  1349   by (simp add: setprod_def)
```
```  1350
```
```  1351 lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
```
```  1352   by (simp add: setprod_def)
```
```  1353
```
```  1354 lemma setprod_reindex:
```
```  1355      "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
```
```  1356 by(auto simp: setprod_def fold_reindex dest!:finite_imageD)
```
```  1357
```
```  1358 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
```
```  1359 by (auto simp add: setprod_reindex)
```
```  1360
```
```  1361 lemma setprod_cong:
```
```  1362   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
```
```  1363 by(fastsimp simp: setprod_def intro: fold_cong)
```
```  1364
```
```  1365 lemma strong_setprod_cong:
```
```  1366   "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
```
```  1367 by(fastsimp simp: simp_implies_def setprod_def intro: fold_cong)
```
```  1368
```
```  1369 lemma setprod_reindex_cong: "inj_on f A ==>
```
```  1370     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
```
```  1371   by (frule setprod_reindex, simp)
```
```  1372
```
```  1373
```
```  1374 lemma setprod_1: "setprod (%i. 1) A = 1"
```
```  1375   apply (case_tac "finite A")
```
```  1376   apply (erule finite_induct, auto simp add: mult_ac)
```
```  1377   done
```
```  1378
```
```  1379 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
```
```  1380   apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
```
```  1381   apply (erule ssubst, rule setprod_1)
```
```  1382   apply (rule setprod_cong, auto)
```
```  1383   done
```
```  1384
```
```  1385 lemma setprod_Un_Int: "finite A ==> finite B
```
```  1386     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
```
```  1387 by(simp add: setprod_def fold_Un_Int[symmetric])
```
```  1388
```
```  1389 lemma setprod_Un_disjoint: "finite A ==> finite B
```
```  1390   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
```
```  1391 by (subst setprod_Un_Int [symmetric], auto)
```
```  1392
```
```  1393 lemma setprod_UN_disjoint:
```
```  1394     "finite I ==> (ALL i:I. finite (A i)) ==>
```
```  1395         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
```
```  1396       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
```
```  1397 by(simp add: setprod_def fold_UN_disjoint cong: setprod_cong)
```
```  1398
```
```  1399 lemma setprod_Union_disjoint:
```
```  1400   "[| (ALL A:C. finite A);
```
```  1401       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
```
```  1402    ==> setprod f (Union C) = setprod (setprod f) C"
```
```  1403 apply (cases "finite C")
```
```  1404  prefer 2 apply (force dest: finite_UnionD simp add: setprod_def)
```
```  1405   apply (frule setprod_UN_disjoint [of C id f])
```
```  1406  apply (unfold Union_def id_def, assumption+)
```
```  1407 done
```
```  1408
```
```  1409 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
```
```  1410     (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
```
```  1411     (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
```
```  1412 by(simp add:setprod_def fold_Sigma split_def cong:setprod_cong)
```
```  1413
```
```  1414 text{*Here we can eliminate the finiteness assumptions, by cases.*}
```
```  1415 lemma setprod_cartesian_product:
```
```  1416      "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
```
```  1417 apply (cases "finite A")
```
```  1418  apply (cases "finite B")
```
```  1419   apply (simp add: setprod_Sigma)
```
```  1420  apply (cases "A={}", simp)
```
```  1421  apply (simp add: setprod_1)
```
```  1422 apply (auto simp add: setprod_def
```
```  1423             dest: finite_cartesian_productD1 finite_cartesian_productD2)
```
```  1424 done
```
```  1425
```
```  1426 lemma setprod_timesf:
```
```  1427      "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
```
```  1428 by(simp add:setprod_def fold_distrib)
```
```  1429
```
```  1430
```
```  1431 subsubsection {* Properties in more restricted classes of structures *}
```
```  1432
```
```  1433 lemma setprod_eq_1_iff [simp]:
```
```  1434     "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
```
```  1435   by (induct set: finite) auto
```
```  1436
```
```  1437 lemma setprod_zero:
```
```  1438      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
```
```  1439   apply (induct set: finite, force, clarsimp)
```
```  1440   apply (erule disjE, auto)
```
```  1441   done
```
```  1442
```
```  1443 lemma setprod_nonneg [rule_format]:
```
```  1444      "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A"
```
```  1445   apply (case_tac "finite A")
```
```  1446   apply (induct set: finite, force, clarsimp)
```
```  1447   apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
```
```  1448   apply (rule mult_mono, assumption+)
```
```  1449   apply (auto simp add: setprod_def)
```
```  1450   done
```
```  1451
```
```  1452 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x)
```
```  1453      --> 0 < setprod f A"
```
```  1454   apply (case_tac "finite A")
```
```  1455   apply (induct set: finite, force, clarsimp)
```
```  1456   apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
```
```  1457   apply (rule mult_strict_mono, assumption+)
```
```  1458   apply (auto simp add: setprod_def)
```
```  1459   done
```
```  1460
```
```  1461 lemma setprod_nonzero [rule_format]:
```
```  1462     "(ALL x y. (x::'a::comm_semiring_1) * y = 0 --> x = 0 | y = 0) ==>
```
```  1463       finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
```
```  1464   apply (erule finite_induct, auto)
```
```  1465   done
```
```  1466
```
```  1467 lemma setprod_zero_eq:
```
```  1468     "(ALL x y. (x::'a::comm_semiring_1) * y = 0 --> x = 0 | y = 0) ==>
```
```  1469      finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
```
```  1470   apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
```
```  1471   done
```
```  1472
```
```  1473 lemma setprod_nonzero_field:
```
```  1474     "finite A ==> (ALL x: A. f x \<noteq> (0::'a::idom)) ==> setprod f A \<noteq> 0"
```
```  1475   apply (rule setprod_nonzero, auto)
```
```  1476   done
```
```  1477
```
```  1478 lemma setprod_zero_eq_field:
```
```  1479     "finite A ==> (setprod f A = (0::'a::idom)) = (EX x: A. f x = 0)"
```
```  1480   apply (rule setprod_zero_eq, auto)
```
```  1481   done
```
```  1482
```
```  1483 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
```
```  1484     (setprod f (A Un B) :: 'a ::{field})
```
```  1485       = setprod f A * setprod f B / setprod f (A Int B)"
```
```  1486   apply (subst setprod_Un_Int [symmetric], auto)
```
```  1487   apply (subgoal_tac "finite (A Int B)")
```
```  1488   apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
```
```  1489   apply (subst times_divide_eq_right [THEN sym], auto)
```
```  1490   done
```
```  1491
```
```  1492 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
```
```  1493     (setprod f (A - {a}) :: 'a :: {field}) =
```
```  1494       (if a:A then setprod f A / f a else setprod f A)"
```
```  1495 by (erule finite_induct) (auto simp add: insert_Diff_if)
```
```  1496
```
```  1497 lemma setprod_inversef: "finite A ==>
```
```  1498     ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
```
```  1499       setprod (inverse \<circ> f) A = inverse (setprod f A)"
```
```  1500   apply (erule finite_induct)
```
```  1501   apply (simp, simp)
```
```  1502   done
```
```  1503
```
```  1504 lemma setprod_dividef:
```
```  1505      "[|finite A;
```
```  1506         \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
```
```  1507       ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
```
```  1508   apply (subgoal_tac
```
```  1509          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
```
```  1510   apply (erule ssubst)
```
```  1511   apply (subst divide_inverse)
```
```  1512   apply (subst setprod_timesf)
```
```  1513   apply (subst setprod_inversef, assumption+, rule refl)
```
```  1514   apply (rule setprod_cong, rule refl)
```
```  1515   apply (subst divide_inverse, auto)
```
```  1516   done
```
```  1517
```
```  1518 subsection {* Finite cardinality *}
```
```  1519
```
```  1520 text {* This definition, although traditional, is ugly to work with:
```
```  1521 @{text "card A == LEAST n. EX f. A = {f i | i. i < n}"}.
```
```  1522 But now that we have @{text setsum} things are easy:
```
```  1523 *}
```
```  1524
```
```  1525 definition
```
```  1526   card :: "'a set \<Rightarrow> nat"
```
```  1527 where
```
```  1528   "card A = setsum (\<lambda>x. 1) A"
```
```  1529
```
```  1530 lemma card_empty [simp]: "card {} = 0"
```
```  1531 by (simp add: card_def)
```
```  1532
```
```  1533 lemma card_infinite [simp]: "~ finite A ==> card A = 0"
```
```  1534 by (simp add: card_def)
```
```  1535
```
```  1536 lemma card_eq_setsum: "card A = setsum (%x. 1) A"
```
```  1537 by (simp add: card_def)
```
```  1538
```
```  1539 lemma card_insert_disjoint [simp]:
```
```  1540   "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
```
```  1541 by(simp add: card_def)
```
```  1542
```
```  1543 lemma card_insert_if:
```
```  1544     "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
```
```  1545   by (simp add: insert_absorb)
```
```  1546
```
```  1547 lemma card_0_eq [simp,noatp]: "finite A ==> (card A = 0) = (A = {})"
```
```  1548   apply auto
```
```  1549   apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
```
```  1550   done
```
```  1551
```
```  1552 lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
```
```  1553 by auto
```
```  1554
```
```  1555
```
```  1556 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
```
```  1557 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
```
```  1558 apply(simp del:insert_Diff_single)
```
```  1559 done
```
```  1560
```
```  1561 lemma card_Diff_singleton:
```
```  1562   "finite A ==> x: A ==> card (A - {x}) = card A - 1"
```
```  1563 by (simp add: card_Suc_Diff1 [symmetric])
```
```  1564
```
```  1565 lemma card_Diff_singleton_if:
```
```  1566   "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
```
```  1567 by (simp add: card_Diff_singleton)
```
```  1568
```
```  1569 lemma card_Diff_insert[simp]:
```
```  1570 assumes "finite A" and "a:A" and "a ~: B"
```
```  1571 shows "card(A - insert a B) = card(A - B) - 1"
```
```  1572 proof -
```
```  1573   have "A - insert a B = (A - B) - {a}" using assms by blast
```
```  1574   then show ?thesis using assms by(simp add:card_Diff_singleton)
```
```  1575 qed
```
```  1576
```
```  1577 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
```
```  1578 by (simp add: card_insert_if card_Suc_Diff1 del:card_Diff_insert)
```
```  1579
```
```  1580 lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
```
```  1581 by (simp add: card_insert_if)
```
```  1582
```
```  1583 lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
```
```  1584 by (simp add: card_def setsum_mono2)
```
```  1585
```
```  1586 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
```
```  1587   apply (induct set: finite, simp, clarify)
```
```  1588   apply (subgoal_tac "finite A & A - {x} <= F")
```
```  1589    prefer 2 apply (blast intro: finite_subset, atomize)
```
```  1590   apply (drule_tac x = "A - {x}" in spec)
```
```  1591   apply (simp add: card_Diff_singleton_if split add: split_if_asm)
```
```  1592   apply (case_tac "card A", auto)
```
```  1593   done
```
```  1594
```
```  1595 lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
```
```  1596 apply (simp add: psubset_eq linorder_not_le [symmetric])
```
```  1597 apply (blast dest: card_seteq)
```
```  1598 done
```
```  1599
```
```  1600 lemma card_Un_Int: "finite A ==> finite B
```
```  1601     ==> card A + card B = card (A Un B) + card (A Int B)"
```
```  1602 by(simp add:card_def setsum_Un_Int)
```
```  1603
```
```  1604 lemma card_Un_disjoint: "finite A ==> finite B
```
```  1605     ==> A Int B = {} ==> card (A Un B) = card A + card B"
```
```  1606 by (simp add: card_Un_Int)
```
```  1607
```
```  1608 lemma card_Diff_subset:
```
```  1609   "finite B ==> B <= A ==> card (A - B) = card A - card B"
```
```  1610 by(simp add:card_def setsum_diff_nat)
```
```  1611
```
```  1612 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
```
```  1613   apply (rule Suc_less_SucD)
```
```  1614   apply (simp add: card_Suc_Diff1 del:card_Diff_insert)
```
```  1615   done
```
```  1616
```
```  1617 lemma card_Diff2_less:
```
```  1618     "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
```
```  1619   apply (case_tac "x = y")
```
```  1620    apply (simp add: card_Diff1_less del:card_Diff_insert)
```
```  1621   apply (rule less_trans)
```
```  1622    prefer 2 apply (auto intro!: card_Diff1_less simp del:card_Diff_insert)
```
```  1623   done
```
```  1624
```
```  1625 lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
```
```  1626   apply (case_tac "x : A")
```
```  1627    apply (simp_all add: card_Diff1_less less_imp_le)
```
```  1628   done
```
```  1629
```
```  1630 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
```
```  1631 by (erule psubsetI, blast)
```
```  1632
```
```  1633 lemma insert_partition:
```
```  1634   "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
```
```  1635   \<Longrightarrow> x \<inter> \<Union> F = {}"
```
```  1636 by auto
```
```  1637
```
```  1638 text{* main cardinality theorem *}
```
```  1639 lemma card_partition [rule_format]:
```
```  1640      "finite C ==>
```
```  1641         finite (\<Union> C) -->
```
```  1642         (\<forall>c\<in>C. card c = k) -->
```
```  1643         (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->
```
```  1644         k * card(C) = card (\<Union> C)"
```
```  1645 apply (erule finite_induct, simp)
```
```  1646 apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition
```
```  1647        finite_subset [of _ "\<Union> (insert x F)"])
```
```  1648 done
```
```  1649
```
```  1650
```
```  1651 text{*The form of a finite set of given cardinality*}
```
```  1652
```
```  1653 lemma card_eq_SucD:
```
```  1654 assumes "card A = Suc k"
```
```  1655 shows "\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={})"
```
```  1656 proof -
```
```  1657   have fin: "finite A" using assms by (auto intro: ccontr)
```
```  1658   moreover have "card A \<noteq> 0" using assms by auto
```
```  1659   ultimately obtain b where b: "b \<in> A" by auto
```
```  1660   show ?thesis
```
```  1661   proof (intro exI conjI)
```
```  1662     show "A = insert b (A-{b})" using b by blast
```
```  1663     show "b \<notin> A - {b}" by blast
```
```  1664     show "card (A - {b}) = k" and "k = 0 \<longrightarrow> A - {b} = {}"
```
```  1665       using assms b fin by(fastsimp dest:mk_disjoint_insert)+
```
```  1666   qed
```
```  1667 qed
```
```  1668
```
```  1669 lemma card_Suc_eq:
```
```  1670   "(card A = Suc k) =
```
```  1671    (\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={}))"
```
```  1672 apply(rule iffI)
```
```  1673  apply(erule card_eq_SucD)
```
```  1674 apply(auto)
```
```  1675 apply(subst card_insert)
```
```  1676  apply(auto intro:ccontr)
```
```  1677 done
```
```  1678
```
```  1679 lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
```
```  1680 apply (cases "finite A")
```
```  1681 apply (erule finite_induct)
```
```  1682 apply (auto simp add: ring_simps)
```
```  1683 done
```
```  1684
```
```  1685 lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{recpower, comm_monoid_mult})) = y^(card A)"
```
```  1686   apply (erule finite_induct)
```
```  1687   apply (auto simp add: power_Suc)
```
```  1688   done
```
```  1689
```
```  1690 lemma setsum_bounded:
```
```  1691   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, pordered_ab_semigroup_add})"
```
```  1692   shows "setsum f A \<le> of_nat(card A) * K"
```
```  1693 proof (cases "finite A")
```
```  1694   case True
```
```  1695   thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
```
```  1696 next
```
```  1697   case False thus ?thesis by (simp add: setsum_def)
```
```  1698 qed
```
```  1699
```
```  1700
```
```  1701 subsubsection {* Cardinality of unions *}
```
```  1702
```
```  1703 lemma card_UN_disjoint:
```
```  1704     "finite I ==> (ALL i:I. finite (A i)) ==>
```
```  1705         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
```
```  1706       card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
```
```  1707   apply (simp add: card_def del: setsum_constant)
```
```  1708   apply (subgoal_tac
```
```  1709            "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
```
```  1710   apply (simp add: setsum_UN_disjoint del: setsum_constant)
```
```  1711   apply (simp cong: setsum_cong)
```
```  1712   done
```
```  1713
```
```  1714 lemma card_Union_disjoint:
```
```  1715   "finite C ==> (ALL A:C. finite A) ==>
```
```  1716         (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
```
```  1717       card (Union C) = setsum card C"
```
```  1718   apply (frule card_UN_disjoint [of C id])
```
```  1719   apply (unfold Union_def id_def, assumption+)
```
```  1720   done
```
```  1721
```
```  1722 subsubsection {* Cardinality of image *}
```
```  1723
```
```  1724 text{*The image of a finite set can be expressed using @{term fold}.*}
```
```  1725 lemma image_eq_fold: "finite A ==> f ` A = fold (op Un) (%x. {f x}) {} A"
```
```  1726 proof (induct rule: finite_induct)
```
```  1727   case empty then show ?case by simp
```
```  1728 next
```
```  1729   interpret ab_semigroup_mult ["op Un"]
```
```  1730     by unfold_locales auto
```
```  1731   case insert
```
```  1732   then show ?case by simp
```
```  1733 qed
```
```  1734
```
```  1735 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
```
```  1736   apply (induct set: finite)
```
```  1737    apply simp
```
```  1738   apply (simp add: le_SucI finite_imageI card_insert_if)
```
```  1739   done
```
```  1740
```
```  1741 lemma card_image: "inj_on f A ==> card (f ` A) = card A"
```
```  1742 by(simp add:card_def setsum_reindex o_def del:setsum_constant)
```
```  1743
```
```  1744 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
```
```  1745 by (simp add: card_seteq card_image)
```
```  1746
```
```  1747 lemma eq_card_imp_inj_on:
```
```  1748   "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
```
```  1749 apply (induct rule:finite_induct)
```
```  1750 apply simp
```
```  1751 apply(frule card_image_le[where f = f])
```
```  1752 apply(simp add:card_insert_if split:if_splits)
```
```  1753 done
```
```  1754
```
```  1755 lemma inj_on_iff_eq_card:
```
```  1756   "finite A ==> inj_on f A = (card(f ` A) = card A)"
```
```  1757 by(blast intro: card_image eq_card_imp_inj_on)
```
```  1758
```
```  1759
```
```  1760 lemma card_inj_on_le:
```
```  1761     "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
```
```  1762 apply (subgoal_tac "finite A")
```
```  1763  apply (force intro: card_mono simp add: card_image [symmetric])
```
```  1764 apply (blast intro: finite_imageD dest: finite_subset)
```
```  1765 done
```
```  1766
```
```  1767 lemma card_bij_eq:
```
```  1768     "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
```
```  1769        finite A; finite B |] ==> card A = card B"
```
```  1770   by (auto intro: le_anti_sym card_inj_on_le)
```
```  1771
```
```  1772
```
```  1773 subsubsection {* Cardinality of products *}
```
```  1774
```
```  1775 (*
```
```  1776 lemma SigmaI_insert: "y \<notin> A ==>
```
```  1777   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
```
```  1778   by auto
```
```  1779 *)
```
```  1780
```
```  1781 lemma card_SigmaI [simp]:
```
```  1782   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
```
```  1783   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
```
```  1784 by(simp add:card_def setsum_Sigma del:setsum_constant)
```
```  1785
```
```  1786 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
```
```  1787 apply (cases "finite A")
```
```  1788 apply (cases "finite B")
```
```  1789 apply (auto simp add: card_eq_0_iff
```
```  1790             dest: finite_cartesian_productD1 finite_cartesian_productD2)
```
```  1791 done
```
```  1792
```
```  1793 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
```
```  1794 by (simp add: card_cartesian_product)
```
```  1795
```
```  1796
```
```  1797
```
```  1798 subsubsection {* Cardinality of the Powerset *}
```
```  1799
```
```  1800 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
```
```  1801   apply (induct set: finite)
```
```  1802    apply (simp_all add: Pow_insert)
```
```  1803   apply (subst card_Un_disjoint, blast)
```
```  1804     apply (blast intro: finite_imageI, blast)
```
```  1805   apply (subgoal_tac "inj_on (insert x) (Pow F)")
```
```  1806    apply (simp add: card_image Pow_insert)
```
```  1807   apply (unfold inj_on_def)
```
```  1808   apply (blast elim!: equalityE)
```
```  1809   done
```
```  1810
```
```  1811 text {* Relates to equivalence classes.  Based on a theorem of F. Kamm�ller.  *}
```
```  1812
```
```  1813 lemma dvd_partition:
```
```  1814   "finite (Union C) ==>
```
```  1815     ALL c : C. k dvd card c ==>
```
```  1816     (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
```
```  1817   k dvd card (Union C)"
```
```  1818 apply(frule finite_UnionD)
```
```  1819 apply(rotate_tac -1)
```
```  1820   apply (induct set: finite, simp_all, clarify)
```
```  1821   apply (subst card_Un_disjoint)
```
```  1822   apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
```
```  1823   done
```
```  1824
```
```  1825
```
```  1826 subsubsection {* Relating injectivity and surjectivity *}
```
```  1827
```
```  1828 lemma finite_surj_inj: "finite(A) \<Longrightarrow> A <= f`A \<Longrightarrow> inj_on f A"
```
```  1829 apply(rule eq_card_imp_inj_on, assumption)
```
```  1830 apply(frule finite_imageI)
```
```  1831 apply(drule (1) card_seteq)
```
```  1832 apply(erule card_image_le)
```
```  1833 apply simp
```
```  1834 done
```
```  1835
```
```  1836 lemma finite_UNIV_surj_inj: fixes f :: "'a \<Rightarrow> 'a"
```
```  1837 shows "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
```
```  1838 by (blast intro: finite_surj_inj subset_UNIV dest:surj_range)
```
```  1839
```
```  1840 lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a"
```
```  1841 shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
```
```  1842 by(fastsimp simp:surj_def dest!: endo_inj_surj)
```
```  1843
```
```  1844 corollary infinite_UNIV_nat: "~finite(UNIV::nat set)"
```
```  1845 proof
```
```  1846   assume "finite(UNIV::nat set)"
```
```  1847   with finite_UNIV_inj_surj[of Suc]
```
```  1848   show False by simp (blast dest: Suc_neq_Zero surjD)
```
```  1849 qed
```
```  1850
```
```  1851
```
```  1852 subsection{* A fold functional for non-empty sets *}
```
```  1853
```
```  1854 text{* Does not require start value. *}
```
```  1855
```
```  1856 inductive
```
```  1857   fold1Set :: "('a => 'a => 'a) => 'a set => 'a => bool"
```
```  1858   for f :: "'a => 'a => 'a"
```
```  1859 where
```
```  1860   fold1Set_insertI [intro]:
```
```  1861    "\<lbrakk> foldSet f id a A x; a \<notin> A \<rbrakk> \<Longrightarrow> fold1Set f (insert a A) x"
```
```  1862
```
```  1863 constdefs
```
```  1864   fold1 :: "('a => 'a => 'a) => 'a set => 'a"
```
```  1865   "fold1 f A == THE x. fold1Set f A x"
```
```  1866
```
```  1867 lemma fold1Set_nonempty:
```
```  1868   "fold1Set f A x \<Longrightarrow> A \<noteq> {}"
```
```  1869   by(erule fold1Set.cases, simp_all)
```
```  1870
```
```  1871 inductive_cases empty_fold1SetE [elim!]: "fold1Set f {} x"
```
```  1872
```
```  1873 inductive_cases insert_fold1SetE [elim!]: "fold1Set f (insert a X) x"
```
```  1874
```
```  1875
```
```  1876 lemma fold1Set_sing [iff]: "(fold1Set f {a} b) = (a = b)"
```
```  1877   by (blast intro: foldSet.intros elim: foldSet.cases)
```
```  1878
```
```  1879 lemma fold1_singleton [simp]: "fold1 f {a} = a"
```
```  1880   by (unfold fold1_def) blast
```
```  1881
```
```  1882 lemma finite_nonempty_imp_fold1Set:
```
```  1883   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. fold1Set f A x"
```
```  1884 apply (induct A rule: finite_induct)
```
```  1885 apply (auto dest: finite_imp_foldSet [of _ f id])
```
```  1886 done
```
```  1887
```
```  1888 text{*First, some lemmas about @{term foldSet}.*}
```
```  1889
```
```  1890 context ab_semigroup_mult
```
```  1891 begin
```
```  1892
```
```  1893 lemma foldSet_insert_swap:
```
```  1894 assumes fold: "foldSet times id b A y"
```
```  1895 shows "b \<notin> A \<Longrightarrow> foldSet times id z (insert b A) (z * y)"
```
```  1896 using fold
```
```  1897 proof (induct rule: foldSet.induct)
```
```  1898   case emptyI thus ?case by (force simp add: fold_insert_aux mult_commute)
```
```  1899 next
```
```  1900   case (insertI x A y)
```
```  1901     have "foldSet times (\<lambda>u. u) z (insert x (insert b A)) (x * (z * y))"
```
```  1902       using insertI by force  --{*how does @{term id} get unfolded?*}
```
```  1903     thus ?case by (simp add: insert_commute mult_ac)
```
```  1904 qed
```
```  1905
```
```  1906 lemma foldSet_permute_diff:
```
```  1907 assumes fold: "foldSet times id b A x"
```
```  1908 shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> foldSet times id a (insert b (A-{a})) x"
```
```  1909 using fold
```
```  1910 proof (induct rule: foldSet.induct)
```
```  1911   case emptyI thus ?case by simp
```
```  1912 next
```
```  1913   case (insertI x A y)
```
```  1914   have "a = x \<or> a \<in> A" using insertI by simp
```
```  1915   thus ?case
```
```  1916   proof
```
```  1917     assume "a = x"
```
```  1918     with insertI show ?thesis
```
```  1919       by (simp add: id_def [symmetric], blast intro: foldSet_insert_swap)
```
```  1920   next
```
```  1921     assume ainA: "a \<in> A"
```
```  1922     hence "foldSet times id a (insert x (insert b (A - {a}))) (x * y)"
```
```  1923       using insertI by (force simp: id_def)
```
```  1924     moreover
```
```  1925     have "insert x (insert b (A - {a})) = insert b (insert x A - {a})"
```
```  1926       using ainA insertI by blast
```
```  1927     ultimately show ?thesis by (simp add: id_def)
```
```  1928   qed
```
```  1929 qed
```
```  1930
```
```  1931 lemma fold1_eq_fold:
```
```  1932      "[|finite A; a \<notin> A|] ==> fold1 times (insert a A) = fold times id a A"
```
```  1933 apply (simp add: fold1_def fold_def)
```
```  1934 apply (rule the_equality)
```
```  1935 apply (best intro: foldSet_determ theI dest: finite_imp_foldSet [of _ times id])
```
```  1936 apply (rule sym, clarify)
```
```  1937 apply (case_tac "Aa=A")
```
```  1938  apply (best intro: the_equality foldSet_determ)
```
```  1939 apply (subgoal_tac "foldSet times id a A x")
```
```  1940  apply (best intro: the_equality foldSet_determ)
```
```  1941 apply (subgoal_tac "insert aa (Aa - {a}) = A")
```
```  1942  prefer 2 apply (blast elim: equalityE)
```
```  1943 apply (auto dest: foldSet_permute_diff [where a=a])
```
```  1944 done
```
```  1945
```
```  1946 lemma nonempty_iff: "(A \<noteq> {}) = (\<exists>x B. A = insert x B & x \<notin> B)"
```
```  1947 apply safe
```
```  1948 apply simp
```
```  1949 apply (drule_tac x=x in spec)
```
```  1950 apply (drule_tac x="A-{x}" in spec, auto)
```
```  1951 done
```
```  1952
```
```  1953 lemma fold1_insert:
```
```  1954   assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A"
```
```  1955   shows "fold1 times (insert x A) = x * fold1 times A"
```
```  1956 proof -
```
```  1957   from nonempty obtain a A' where "A = insert a A' & a ~: A'"
```
```  1958     by (auto simp add: nonempty_iff)
```
```  1959   with A show ?thesis
```
```  1960     by (simp add: insert_commute [of x] fold1_eq_fold eq_commute)
```
```  1961 qed
```
```  1962
```
```  1963 end
```
```  1964
```
```  1965 context ab_semigroup_idem_mult
```
```  1966 begin
```
```  1967
```
```  1968 lemma fold1_insert_idem [simp]:
```
```  1969   assumes nonempty: "A \<noteq> {}" and A: "finite A"
```
```  1970   shows "fold1 times (insert x A) = x * fold1 times A"
```
```  1971 proof -
```
```  1972   from nonempty obtain a A' where A': "A = insert a A' & a ~: A'"
```
```  1973     by (auto simp add: nonempty_iff)
```
```  1974   show ?thesis
```
```  1975   proof cases
```
```  1976     assume "a = x"
```
```  1977     thus ?thesis
```
```  1978     proof cases
```
```  1979       assume "A' = {}"
```
```  1980       with prems show ?thesis by (simp add: mult_idem)
```
```  1981     next
```
```  1982       assume "A' \<noteq> {}"
```
```  1983       with prems show ?thesis
```
```  1984 	by (simp add: fold1_insert mult_assoc [symmetric] mult_idem)
```
```  1985     qed
```
```  1986   next
```
```  1987     assume "a \<noteq> x"
```
```  1988     with prems show ?thesis
```
```  1989       by (simp add: insert_commute fold1_eq_fold fold_insert_idem)
```
```  1990   qed
```
```  1991 qed
```
```  1992
```
```  1993 lemma hom_fold1_commute:
```
```  1994 assumes hom: "!!x y. h (x * y) = h x * h y"
```
```  1995 and N: "finite N" "N \<noteq> {}" shows "h (fold1 times N) = fold1 times (h ` N)"
```
```  1996 using N proof (induct rule: finite_ne_induct)
```
```  1997   case singleton thus ?case by simp
```
```  1998 next
```
```  1999   case (insert n N)
```
```  2000   then have "h (fold1 times (insert n N)) = h (n * fold1 times N)" by simp
```
```  2001   also have "\<dots> = h n * h (fold1 times N)" by(rule hom)
```
```  2002   also have "h (fold1 times N) = fold1 times (h ` N)" by(rule insert)
```
```  2003   also have "times (h n) \<dots> = fold1 times (insert (h n) (h ` N))"
```
```  2004     using insert by(simp)
```
```  2005   also have "insert (h n) (h ` N) = h ` insert n N" by simp
```
```  2006   finally show ?case .
```
```  2007 qed
```
```  2008
```
```  2009 end
```
```  2010
```
```  2011
```
```  2012 text{* Now the recursion rules for definitions: *}
```
```  2013
```
```  2014 lemma fold1_singleton_def: "g = fold1 f \<Longrightarrow> g {a} = a"
```
```  2015 by(simp add:fold1_singleton)
```
```  2016
```
```  2017 lemma (in ab_semigroup_mult) fold1_insert_def:
```
```  2018   "\<lbrakk> g = fold1 times; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A"
```
```  2019 by (simp add:fold1_insert)
```
```  2020
```
```  2021 lemma (in ab_semigroup_idem_mult) fold1_insert_idem_def:
```
```  2022   "\<lbrakk> g = fold1 times; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A"
```
```  2023 by simp
```
```  2024
```
```  2025 subsubsection{* Determinacy for @{term fold1Set} *}
```
```  2026
```
```  2027 text{*Not actually used!!*}
```
```  2028
```
```  2029 context ab_semigroup_mult
```
```  2030 begin
```
```  2031
```
```  2032 lemma foldSet_permute:
```
```  2033   "[|foldSet times id b (insert a A) x; a \<notin> A; b \<notin> A|]
```
```  2034    ==> foldSet times id a (insert b A) x"
```
```  2035 apply (cases "a=b")
```
```  2036 apply (auto dest: foldSet_permute_diff)
```
```  2037 done
```
```  2038
```
```  2039 lemma fold1Set_determ:
```
```  2040   "fold1Set times A x ==> fold1Set times A y ==> y = x"
```
```  2041 proof (clarify elim!: fold1Set.cases)
```
```  2042   fix A x B y a b
```
```  2043   assume Ax: "foldSet times id a A x"
```
```  2044   assume By: "foldSet times id b B y"
```
```  2045   assume anotA:  "a \<notin> A"
```
```  2046   assume bnotB:  "b \<notin> B"
```
```  2047   assume eq: "insert a A = insert b B"
```
```  2048   show "y=x"
```
```  2049   proof cases
```
```  2050     assume same: "a=b"
```
```  2051     hence "A=B" using anotA bnotB eq by (blast elim!: equalityE)
```
```  2052     thus ?thesis using Ax By same by (blast intro: foldSet_determ)
```
```  2053   next
```
```  2054     assume diff: "a\<noteq>b"
```
```  2055     let ?D = "B - {a}"
```
```  2056     have B: "B = insert a ?D" and A: "A = insert b ?D"
```
```  2057      and aB: "a \<in> B" and bA: "b \<in> A"
```
```  2058       using eq anotA bnotB diff by (blast elim!:equalityE)+
```
```  2059     with aB bnotB By
```
```  2060     have "foldSet times id a (insert b ?D) y"
```
```  2061       by (auto intro: foldSet_permute simp add: insert_absorb)
```
```  2062     moreover
```
```  2063     have "foldSet times id a (insert b ?D) x"
```
```  2064       by (simp add: A [symmetric] Ax)
```
```  2065     ultimately show ?thesis by (blast intro: foldSet_determ)
```
```  2066   qed
```
```  2067 qed
```
```  2068
```
```  2069 lemma fold1Set_equality: "fold1Set times A y ==> fold1 times A = y"
```
```  2070   by (unfold fold1_def) (blast intro: fold1Set_determ)
```
```  2071
```
```  2072 end
```
```  2073
```
```  2074 declare
```
```  2075   empty_foldSetE [rule del]   foldSet.intros [rule del]
```
```  2076   empty_fold1SetE [rule del]  insert_fold1SetE [rule del]
```
```  2077   -- {* No more proofs involve these relations. *}
```
```  2078
```
```  2079 subsubsection {* Lemmas about @{text fold1} *}
```
```  2080
```
```  2081 context ab_semigroup_mult
```
```  2082 begin
```
```  2083
```
```  2084 lemma fold1_Un:
```
```  2085 assumes A: "finite A" "A \<noteq> {}"
```
```  2086 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A Int B = {} \<Longrightarrow>
```
```  2087        fold1 times (A Un B) = fold1 times A * fold1 times B"
```
```  2088 using A by (induct rule: finite_ne_induct)
```
```  2089   (simp_all add: fold1_insert mult_assoc)
```
```  2090
```
```  2091 lemma fold1_in:
```
```  2092   assumes A: "finite (A)" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x,y}"
```
```  2093   shows "fold1 times A \<in> A"
```
```  2094 using A
```
```  2095 proof (induct rule:finite_ne_induct)
```
```  2096   case singleton thus ?case by simp
```
```  2097 next
```
```  2098   case insert thus ?case using elem by (force simp add:fold1_insert)
```
```  2099 qed
```
```  2100
```
```  2101 end
```
```  2102
```
```  2103 lemma (in ab_semigroup_idem_mult) fold1_Un2:
```
```  2104 assumes A: "finite A" "A \<noteq> {}"
```
```  2105 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow>
```
```  2106        fold1 times (A Un B) = fold1 times A * fold1 times B"
```
```  2107 using A
```
```  2108 proof(induct rule:finite_ne_induct)
```
```  2109   case singleton thus ?case by simp
```
```  2110 next
```
```  2111   case insert thus ?case by (simp add: mult_assoc)
```
```  2112 qed
```
```  2113
```
```  2114
```
```  2115 subsubsection {* Fold1 in lattices with @{const inf} and @{const sup} *}
```
```  2116
```
```  2117 text{*
```
```  2118   As an application of @{text fold1} we define infimum
```
```  2119   and supremum in (not necessarily complete!) lattices
```
```  2120   over (non-empty) sets by means of @{text fold1}.
```
```  2121 *}
```
```  2122
```
```  2123 context lower_semilattice
```
```  2124 begin
```
```  2125
```
```  2126 lemma ab_semigroup_idem_mult_inf:
```
```  2127   "ab_semigroup_idem_mult inf"
```
```  2128   apply unfold_locales
```
```  2129   apply (rule inf_assoc)
```
```  2130   apply (rule inf_commute)
```
```  2131   apply (rule inf_idem)
```
```  2132   done
```
```  2133
```
```  2134 lemma below_fold1_iff:
```
```  2135   assumes "finite A" "A \<noteq> {}"
```
```  2136   shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
```
```  2137 proof -
```
```  2138   interpret ab_semigroup_idem_mult [inf]
```
```  2139     by (rule ab_semigroup_idem_mult_inf)
```
```  2140   show ?thesis using assms by (induct rule: finite_ne_induct) simp_all
```
```  2141 qed
```
```  2142
```
```  2143 lemma fold1_belowI:
```
```  2144   assumes "finite A"
```
```  2145     and "a \<in> A"
```
```  2146   shows "fold1 inf A \<le> a"
```
```  2147 proof -
```
```  2148   from assms have "A \<noteq> {}" by auto
```
```  2149   from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
```
```  2150   proof (induct rule: finite_ne_induct)
```
```  2151     case singleton thus ?case by simp
```
```  2152   next
```
```  2153     interpret ab_semigroup_idem_mult [inf]
```
```  2154       by (rule ab_semigroup_idem_mult_inf)
```
```  2155     case (insert x F)
```
```  2156     from insert(5) have "a = x \<or> a \<in> F" by simp
```
```  2157     thus ?case
```
```  2158     proof
```
```  2159       assume "a = x" thus ?thesis using insert
```
```  2160         by (simp add: mult_ac_idem)
```
```  2161     next
```
```  2162       assume "a \<in> F"
```
```  2163       hence bel: "fold1 inf F \<le> a" by (rule insert)
```
```  2164       have "inf (fold1 inf (insert x F)) a = inf x (inf (fold1 inf F) a)"
```
```  2165         using insert by (simp add: mult_ac_idem)
```
```  2166       also have "inf (fold1 inf F) a = fold1 inf F"
```
```  2167         using bel by (auto intro: antisym)
```
```  2168       also have "inf x \<dots> = fold1 inf (insert x F)"
```
```  2169         using insert by (simp add: mult_ac_idem)
```
```  2170       finally have aux: "inf (fold1 inf (insert x F)) a = fold1 inf (insert x F)" .
```
```  2171       moreover have "inf (fold1 inf (insert x F)) a \<le> a" by simp
```
```  2172       ultimately show ?thesis by simp
```
```  2173     qed
```
```  2174   qed
```
```  2175 qed
```
```  2176
```
```  2177 end
```
```  2178
```
```  2179 lemma (in upper_semilattice) ab_semigroup_idem_mult_sup:
```
```  2180   "ab_semigroup_idem_mult sup"
```
```  2181   by (rule lower_semilattice.ab_semigroup_idem_mult_inf)
```
```  2182     (rule dual_lattice)
```
```  2183
```
```  2184 context lattice
```
```  2185 begin
```
```  2186
```
```  2187 definition
```
```  2188   Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_"  900)
```
```  2189 where
```
```  2190   "Inf_fin = fold1 inf"
```
```  2191
```
```  2192 definition
```
```  2193   Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_"  900)
```
```  2194 where
```
```  2195   "Sup_fin = fold1 sup"
```
```  2196
```
```  2197 lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A"
```
```  2198 apply(unfold Sup_fin_def Inf_fin_def)
```
```  2199 apply(subgoal_tac "EX a. a:A")
```
```  2200 prefer 2 apply blast
```
```  2201 apply(erule exE)
```
```  2202 apply(rule order_trans)
```
```  2203 apply(erule (1) fold1_belowI)
```
```  2204 apply(erule (1) lower_semilattice.fold1_belowI [OF dual_lattice])
```
```  2205 done
```
```  2206
```
```  2207 lemma sup_Inf_absorb [simp]:
```
```  2208   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^bsub>fin\<^esub>A) = a"
```
```  2209 apply(subst sup_commute)
```
```  2210 apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI)
```
```  2211 done
```
```  2212
```
```  2213 lemma inf_Sup_absorb [simp]:
```
```  2214   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a"
```
```  2215 by (simp add: Sup_fin_def inf_absorb1
```
```  2216   lower_semilattice.fold1_belowI [OF dual_lattice])
```
```  2217
```
```  2218 end
```
```  2219
```
```  2220 context distrib_lattice
```
```  2221 begin
```
```  2222
```
```  2223 lemma sup_Inf1_distrib:
```
```  2224   assumes "finite A"
```
```  2225     and "A \<noteq> {}"
```
```  2226   shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
```
```  2227 proof -
```
```  2228   interpret ab_semigroup_idem_mult [inf]
```
```  2229     by (rule ab_semigroup_idem_mult_inf)
```
```  2230   from assms show ?thesis
```
```  2231     by (simp add: Inf_fin_def image_def
```
```  2232       hom_fold1_commute [where h="sup x", OF sup_inf_distrib1])
```
```  2233         (rule arg_cong [where f="fold1 inf"], blast)
```
```  2234 qed
```
```  2235
```
```  2236 lemma sup_Inf2_distrib:
```
```  2237   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
```
```  2238   shows "sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B) = \<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B}"
```
```  2239 using A proof (induct rule: finite_ne_induct)
```
```  2240   case singleton thus ?case
```
```  2241     by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
```
```  2242 next
```
```  2243   interpret ab_semigroup_idem_mult [inf]
```
```  2244     by (rule ab_semigroup_idem_mult_inf)
```
```  2245   case (insert x A)
```
```  2246   have finB: "finite {sup x b |b. b \<in> B}"
```
```  2247     by(rule finite_surj[where f = "sup x", OF B(1)], auto)
```
```  2248   have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
```
```  2249   proof -
```
```  2250     have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
```
```  2251       by blast
```
```  2252     thus ?thesis by(simp add: insert(1) B(1))
```
```  2253   qed
```
```  2254   have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
```
```  2255   have "sup (\<Sqinter>\<^bsub>fin\<^esub>(insert x A)) (\<Sqinter>\<^bsub>fin\<^esub>B) = sup (inf x (\<Sqinter>\<^bsub>fin\<^esub>A)) (\<Sqinter>\<^bsub>fin\<^esub>B)"
```
```  2256     using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def])
```
```  2257   also have "\<dots> = inf (sup x (\<Sqinter>\<^bsub>fin\<^esub>B)) (sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B))" by(rule sup_inf_distrib2)
```
```  2258   also have "\<dots> = inf (\<Sqinter>\<^bsub>fin\<^esub>{sup x b|b. b \<in> B}) (\<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B})"
```
```  2259     using insert by(simp add:sup_Inf1_distrib[OF B])
```
```  2260   also have "\<dots> = \<Sqinter>\<^bsub>fin\<^esub>({sup x b |b. b \<in> B} \<union> {sup a b |a b. a \<in> A \<and> b \<in> B})"
```
```  2261     (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M")
```
```  2262     using B insert
```
```  2263     by (simp add: Inf_fin_def fold1_Un2 [OF finB _ finAB ne])
```
```  2264   also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
```
```  2265     by blast
```
```  2266   finally show ?case .
```
```  2267 qed
```
```  2268
```
```  2269 lemma inf_Sup1_distrib:
```
```  2270   assumes "finite A" and "A \<noteq> {}"
```
```  2271   shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
```
```  2272 proof -
```
```  2273   interpret ab_semigroup_idem_mult [sup]
```
```  2274     by (rule ab_semigroup_idem_mult_sup)
```
```  2275   from assms show ?thesis
```
```  2276     by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1])
```
```  2277       (rule arg_cong [where f="fold1 sup"], blast)
```
```  2278 qed
```
```  2279
```
```  2280 lemma inf_Sup2_distrib:
```
```  2281   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
```
```  2282   shows "inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B) = \<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B}"
```
```  2283 using A proof (induct rule: finite_ne_induct)
```
```  2284   case singleton thus ?case
```
```  2285     by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def])
```
```  2286 next
```
```  2287   case (insert x A)
```
```  2288   have finB: "finite {inf x b |b. b \<in> B}"
```
```  2289     by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
```
```  2290   have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
```
```  2291   proof -
```
```  2292     have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
```
```  2293       by blast
```
```  2294     thus ?thesis by(simp add: insert(1) B(1))
```
```  2295   qed
```
```  2296   have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
```
```  2297   interpret ab_semigroup_idem_mult [sup]
```
```  2298     by (rule ab_semigroup_idem_mult_sup)
```
```  2299   have "inf (\<Squnion>\<^bsub>fin\<^esub>(insert x A)) (\<Squnion>\<^bsub>fin\<^esub>B) = inf (sup x (\<Squnion>\<^bsub>fin\<^esub>A)) (\<Squnion>\<^bsub>fin\<^esub>B)"
```
```  2300     using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
```
```  2301   also have "\<dots> = sup (inf x (\<Squnion>\<^bsub>fin\<^esub>B)) (inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B))" by(rule inf_sup_distrib2)
```
```  2302   also have "\<dots> = sup (\<Squnion>\<^bsub>fin\<^esub>{inf x b|b. b \<in> B}) (\<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B})"
```
```  2303     using insert by(simp add:inf_Sup1_distrib[OF B])
```
```  2304   also have "\<dots> = \<Squnion>\<^bsub>fin\<^esub>({inf x b |b. b \<in> B} \<union> {inf a b |a b. a \<in> A \<and> b \<in> B})"
```
```  2305     (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M")
```
```  2306     using B insert
```
```  2307     by (simp add: Sup_fin_def fold1_Un2 [OF finB _ finAB ne])
```
```  2308   also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
```
```  2309     by blast
```
```  2310   finally show ?case .
```
```  2311 qed
```
```  2312
```
```  2313 end
```
```  2314
```
```  2315 context complete_lattice
```
```  2316 begin
```
```  2317
```
```  2318 text {*
```
```  2319   Coincidence on finite sets in complete lattices:
```
```  2320 *}
```
```  2321
```
```  2322 lemma Inf_fin_Inf:
```
```  2323   assumes "finite A" and "A \<noteq> {}"
```
```  2324   shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
```
```  2325 proof -
```
```  2326   interpret ab_semigroup_idem_mult [inf]
```
```  2327     by (rule ab_semigroup_idem_mult_inf)
```
```  2328   from assms show ?thesis
```
```  2329   unfolding Inf_fin_def by (induct A set: finite)
```
```  2330     (simp_all add: Inf_insert_simp)
```
```  2331 qed
```
```  2332
```
```  2333 lemma Sup_fin_Sup:
```
```  2334   assumes "finite A" and "A \<noteq> {}"
```
```  2335   shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
```
```  2336 proof -
```
```  2337   interpret ab_semigroup_idem_mult [sup]
```
```  2338     by (rule ab_semigroup_idem_mult_sup)
```
```  2339   from assms show ?thesis
```
```  2340   unfolding Sup_fin_def by (induct A set: finite)
```
```  2341     (simp_all add: Sup_insert_simp)
```
```  2342 qed
```
```  2343
```
```  2344 end
```
```  2345
```
```  2346
```
```  2347 subsubsection {* Fold1 in linear orders with @{const min} and @{const max} *}
```
```  2348
```
```  2349 text{*
```
```  2350   As an application of @{text fold1} we define minimum
```
```  2351   and maximum in (not necessarily complete!) linear orders
```
```  2352   over (non-empty) sets by means of @{text fold1}.
```
```  2353 *}
```
```  2354
```
```  2355 context linorder
```
```  2356 begin
```
```  2357
```
```  2358 lemma ab_semigroup_idem_mult_min:
```
```  2359   "ab_semigroup_idem_mult min"
```
```  2360   by unfold_locales (auto simp add: min_def)
```
```  2361
```
```  2362 lemma ab_semigroup_idem_mult_max:
```
```  2363   "ab_semigroup_idem_mult max"
```
```  2364   by unfold_locales (auto simp add: max_def)
```
```  2365
```
```  2366 lemma min_lattice:
```
```  2367   "lower_semilattice (op \<le>) (op <) min"
```
```  2368   by unfold_locales (auto simp add: min_def)
```
```  2369
```
```  2370 lemma max_lattice:
```
```  2371   "lower_semilattice (op \<ge>) (op >) max"
```
```  2372   by unfold_locales (auto simp add: max_def)
```
```  2373
```
```  2374 lemma dual_max:
```
```  2375   "ord.max (op \<ge>) = min"
```
```  2376   by (auto simp add: ord.max_def_raw min_def_raw expand_fun_eq)
```
```  2377
```
```  2378 lemma dual_min:
```
```  2379   "ord.min (op \<ge>) = max"
```
```  2380   by (auto simp add: ord.min_def_raw max_def_raw expand_fun_eq)
```
```  2381
```
```  2382 lemma strict_below_fold1_iff:
```
```  2383   assumes "finite A" and "A \<noteq> {}"
```
```  2384   shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
```
```  2385 proof -
```
```  2386   interpret ab_semigroup_idem_mult [min]
```
```  2387     by (rule ab_semigroup_idem_mult_min)
```
```  2388   from assms show ?thesis
```
```  2389   by (induct rule: finite_ne_induct)
```
```  2390     (simp_all add: fold1_insert)
```
```  2391 qed
```
```  2392
```
```  2393 lemma fold1_below_iff:
```
```  2394   assumes "finite A" and "A \<noteq> {}"
```
```  2395   shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
```
```  2396 proof -
```
```  2397   interpret ab_semigroup_idem_mult [min]
```
```  2398     by (rule ab_semigroup_idem_mult_min)
```
```  2399   from assms show ?thesis
```
```  2400   by (induct rule: finite_ne_induct)
```
```  2401     (simp_all add: fold1_insert min_le_iff_disj)
```
```  2402 qed
```
```  2403
```
```  2404 lemma fold1_strict_below_iff:
```
```  2405   assumes "finite A" and "A \<noteq> {}"
```
```  2406   shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
```
```  2407 proof -
```
```  2408   interpret ab_semigroup_idem_mult [min]
```
```  2409     by (rule ab_semigroup_idem_mult_min)
```
```  2410   from assms show ?thesis
```
```  2411   by (induct rule: finite_ne_induct)
```
```  2412     (simp_all add: fold1_insert min_less_iff_disj)
```
```  2413 qed
```
```  2414
```
```  2415 lemma fold1_antimono:
```
```  2416   assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
```
```  2417   shows "fold1 min B \<le> fold1 min A"
```
```  2418 proof cases
```
```  2419   assume "A = B" thus ?thesis by simp
```
```  2420 next
```
```  2421   interpret ab_semigroup_idem_mult [min]
```
```  2422     by (rule ab_semigroup_idem_mult_min)
```
```  2423   assume "A \<noteq> B"
```
```  2424   have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
```
```  2425   have "fold1 min B = fold1 min (A \<union> (B-A))" by(subst B)(rule refl)
```
```  2426   also have "\<dots> = min (fold1 min A) (fold1 min (B-A))"
```
```  2427   proof -
```
```  2428     have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
```
```  2429     moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`]) (* by(blast intro:finite_Diff prems) fails *)
```
```  2430     moreover have "(B-A) \<noteq> {}" using prems by blast
```
```  2431     moreover have "A Int (B-A) = {}" using prems by blast
```
```  2432     ultimately show ?thesis using `A \<noteq> {}` by (rule_tac fold1_Un)
```
```  2433   qed
```
```  2434   also have "\<dots> \<le> fold1 min A" by (simp add: min_le_iff_disj)
```
```  2435   finally show ?thesis .
```
```  2436 qed
```
```  2437
```
```  2438 definition
```
```  2439   Min :: "'a set \<Rightarrow> 'a"
```
```  2440 where
```
```  2441   "Min = fold1 min"
```
```  2442
```
```  2443 definition
```
```  2444   Max :: "'a set \<Rightarrow> 'a"
```
```  2445 where
```
```  2446   "Max = fold1 max"
```
```  2447
```
```  2448 lemmas Min_singleton [simp] = fold1_singleton_def [OF Min_def]
```
```  2449 lemmas Max_singleton [simp] = fold1_singleton_def [OF Max_def]
```
```  2450
```
```  2451 lemma Min_insert [simp]:
```
```  2452   assumes "finite A" and "A \<noteq> {}"
```
```  2453   shows "Min (insert x A) = min x (Min A)"
```
```  2454 proof -
```
```  2455   interpret ab_semigroup_idem_mult [min]
```
```  2456     by (rule ab_semigroup_idem_mult_min)
```
```  2457   from assms show ?thesis by (rule fold1_insert_idem_def [OF Min_def])
```
```  2458 qed
```
```  2459
```
```  2460 lemma Max_insert [simp]:
```
```  2461   assumes "finite A" and "A \<noteq> {}"
```
```  2462   shows "Max (insert x A) = max x (Max A)"
```
```  2463 proof -
```
```  2464   interpret ab_semigroup_idem_mult [max]
```
```  2465     by (rule ab_semigroup_idem_mult_max)
```
```  2466   from assms show ?thesis by (rule fold1_insert_idem_def [OF Max_def])
```
```  2467 qed
```
```  2468
```
```  2469 lemma Min_in [simp]:
```
```  2470   assumes "finite A" and "A \<noteq> {}"
```
```  2471   shows "Min A \<in> A"
```
```  2472 proof -
```
```  2473   interpret ab_semigroup_idem_mult [min]
```
```  2474     by (rule ab_semigroup_idem_mult_min)
```
```  2475   from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def)
```
```  2476 qed
```
```  2477
```
```  2478 lemma Max_in [simp]:
```
```  2479   assumes "finite A" and "A \<noteq> {}"
```
```  2480   shows "Max A \<in> A"
```
```  2481 proof -
```
```  2482   interpret ab_semigroup_idem_mult [max]
```
```  2483     by (rule ab_semigroup_idem_mult_max)
```
```  2484   from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
```
```  2485 qed
```
```  2486
```
```  2487 lemma Min_Un:
```
```  2488   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
```
```  2489   shows "Min (A \<union> B) = min (Min A) (Min B)"
```
```  2490 proof -
```
```  2491   interpret ab_semigroup_idem_mult [min]
```
```  2492     by (rule ab_semigroup_idem_mult_min)
```
```  2493   from assms show ?thesis
```
```  2494     by (simp add: Min_def fold1_Un2)
```
```  2495 qed
```
```  2496
```
```  2497 lemma Max_Un:
```
```  2498   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
```
```  2499   shows "Max (A \<union> B) = max (Max A) (Max B)"
```
```  2500 proof -
```
```  2501   interpret ab_semigroup_idem_mult [max]
```
```  2502     by (rule ab_semigroup_idem_mult_max)
```
```  2503   from assms show ?thesis
```
```  2504     by (simp add: Max_def fold1_Un2)
```
```  2505 qed
```
```  2506
```
```  2507 lemma hom_Min_commute:
```
```  2508   assumes "\<And>x y. h (min x y) = min (h x) (h y)"
```
```  2509     and "finite N" and "N \<noteq> {}"
```
```  2510   shows "h (Min N) = Min (h ` N)"
```
```  2511 proof -
```
```  2512   interpret ab_semigroup_idem_mult [min]
```
```  2513     by (rule ab_semigroup_idem_mult_min)
```
```  2514   from assms show ?thesis
```
```  2515     by (simp add: Min_def hom_fold1_commute)
```
```  2516 qed
```
```  2517
```
```  2518 lemma hom_Max_commute:
```
```  2519   assumes "\<And>x y. h (max x y) = max (h x) (h y)"
```
```  2520     and "finite N" and "N \<noteq> {}"
```
```  2521   shows "h (Max N) = Max (h ` N)"
```
```  2522 proof -
```
```  2523   interpret ab_semigroup_idem_mult [max]
```
```  2524     by (rule ab_semigroup_idem_mult_max)
```
```  2525   from assms show ?thesis
```
```  2526     by (simp add: Max_def hom_fold1_commute [of h])
```
```  2527 qed
```
```  2528
```
```  2529 lemma Min_le [simp]:
```
```  2530   assumes "finite A" and "x \<in> A"
```
```  2531   shows "Min A \<le> x"
```
```  2532 proof -
```
```  2533   interpret lower_semilattice ["op \<le>" "op <" min]
```
```  2534     by (rule min_lattice)
```
```  2535   from assms show ?thesis by (simp add: Min_def fold1_belowI)
```
```  2536 qed
```
```  2537
```
```  2538 lemma Max_ge [simp]:
```
```  2539   assumes "finite A" and "x \<in> A"
```
```  2540   shows "x \<le> Max A"
```
```  2541 proof -
```
```  2542   invoke lower_semilattice ["op \<ge>" "op >" max]
```
```  2543     by (rule max_lattice)
```
```  2544   from assms show ?thesis by (simp add: Max_def fold1_belowI)
```
```  2545 qed
```
```  2546
```
```  2547 lemma Min_ge_iff [simp, noatp]:
```
```  2548   assumes "finite A" and "A \<noteq> {}"
```
```  2549   shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
```
```  2550 proof -
```
```  2551   interpret lower_semilattice ["op \<le>" "op <" min]
```
```  2552     by (rule min_lattice)
```
```  2553   from assms show ?thesis by (simp add: Min_def below_fold1_iff)
```
```  2554 qed
```
```  2555
```
```  2556 lemma Max_le_iff [simp, noatp]:
```
```  2557   assumes "finite A" and "A \<noteq> {}"
```
```  2558   shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
```
```  2559 proof -
```
```  2560   invoke lower_semilattice ["op \<ge>" "op >" max]
```
```  2561     by (rule max_lattice)
```
```  2562   from assms show ?thesis by (simp add: Max_def below_fold1_iff)
```
```  2563 qed
```
```  2564
```
```  2565 lemma Min_gr_iff [simp, noatp]:
```
```  2566   assumes "finite A" and "A \<noteq> {}"
```
```  2567   shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
```
```  2568 proof -
```
```  2569   interpret lower_semilattice ["op \<le>" "op <" min]
```
```  2570     by (rule min_lattice)
```
```  2571   from assms show ?thesis by (simp add: Min_def strict_below_fold1_iff)
```
```  2572 qed
```
```  2573
```
```  2574 lemma Max_less_iff [simp, noatp]:
```
```  2575   assumes "finite A" and "A \<noteq> {}"
```
```  2576   shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
```
```  2577 proof -
```
```  2578   note Max = Max_def
```
```  2579   interpret linorder ["op \<ge>" "op >"]
```
```  2580     by (rule dual_linorder)
```
```  2581   from assms show ?thesis
```
```  2582     by (simp add: Max strict_below_fold1_iff [folded dual_max])
```
```  2583 qed
```
```  2584
```
```  2585 lemma Min_le_iff [noatp]:
```
```  2586   assumes "finite A" and "A \<noteq> {}"
```
```  2587   shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
```
```  2588 proof -
```
```  2589   interpret lower_semilattice ["op \<le>" "op <" min]
```
```  2590     by (rule min_lattice)
```
```  2591   from assms show ?thesis
```
```  2592     by (simp add: Min_def fold1_below_iff)
```
```  2593 qed
```
```  2594
```
```  2595 lemma Max_ge_iff [noatp]:
```
```  2596   assumes "finite A" and "A \<noteq> {}"
```
```  2597   shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
```
```  2598 proof -
```
```  2599   note Max = Max_def
```
```  2600   interpret linorder ["op \<ge>" "op >"]
```
```  2601     by (rule dual_linorder)
```
```  2602   from assms show ?thesis
```
```  2603     by (simp add: Max fold1_below_iff [folded dual_max])
```
```  2604 qed
```
```  2605
```
```  2606 lemma Min_less_iff [noatp]:
```
```  2607   assumes "finite A" and "A \<noteq> {}"
```
```  2608   shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
```
```  2609 proof -
```
```  2610   interpret lower_semilattice ["op \<le>" "op <" min]
```
```  2611     by (rule min_lattice)
```
```  2612   from assms show ?thesis
```
```  2613     by (simp add: Min_def fold1_strict_below_iff)
```
```  2614 qed
```
```  2615
```
```  2616 lemma Max_gr_iff [noatp]:
```
```  2617   assumes "finite A" and "A \<noteq> {}"
```
```  2618   shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
```
```  2619 proof -
```
```  2620   note Max = Max_def
```
```  2621   interpret linorder ["op \<ge>" "op >"]
```
```  2622     by (rule dual_linorder)
```
```  2623   from assms show ?thesis
```
```  2624     by (simp add: Max fold1_strict_below_iff [folded dual_max])
```
```  2625 qed
```
```  2626
```
```  2627 lemma Min_antimono:
```
```  2628   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
```
```  2629   shows "Min N \<le> Min M"
```
```  2630 proof -
```
```  2631   interpret distrib_lattice ["op \<le>" "op <" min max]
```
```  2632     by (rule distrib_lattice_min_max)
```
```  2633   from assms show ?thesis by (simp add: Min_def fold1_antimono)
```
```  2634 qed
```
```  2635
```
```  2636 lemma Max_mono:
```
```  2637   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
```
```  2638   shows "Max M \<le> Max N"
```
```  2639 proof -
```
```  2640   note Max = Max_def
```
```  2641   interpret linorder ["op \<ge>" "op >"]
```
```  2642     by (rule dual_linorder)
```
```  2643   from assms show ?thesis
```
```  2644     by (simp add: Max fold1_antimono [folded dual_max])
```
```  2645 qed
```
```  2646
```
```  2647 lemma finite_linorder_induct[consumes 1, case_names empty insert]:
```
```  2648  "finite A \<Longrightarrow> P {} \<Longrightarrow>
```
```  2649   (!!A b. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
```
```  2650   \<Longrightarrow> P A"
```
```  2651 proof (induct A rule: measure_induct_rule[where f=card])
```
```  2652   fix A :: "'a set"
```
```  2653   assume IH: "!! B. card B < card A \<Longrightarrow> finite B \<Longrightarrow> P {} \<Longrightarrow>
```
```  2654                  (!!A b. finite A \<Longrightarrow> (\<forall>a\<in>A. a<b) \<Longrightarrow> P A \<Longrightarrow> P (insert b A))
```
```  2655                   \<Longrightarrow> P B"
```
```  2656   and "finite A" and "P {}"
```
```  2657   and step: "!!A b. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
```
```  2658   show "P A"
```
```  2659   proof (cases "A = {}")
```
```  2660     assume "A = {}" thus "P A" using `P {}` by simp
```
```  2661   next
```
```  2662     let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B"
```
```  2663     assume "A \<noteq> {}"
```
```  2664     with `finite A` have "Max A : A" by auto
```
```  2665     hence A: "?A = A" using insert_Diff_single insert_absorb by auto
```
```  2666     note card_Diff1_less[OF `finite A` `Max A : A`]
```
```  2667     moreover have "finite ?B" using `finite A` by simp
```
```  2668     ultimately have "P ?B" using `P {}` step IH by blast
```
```  2669     moreover have "\<forall>a\<in>?B. a < Max A"
```
```  2670       using Max_ge [OF `finite A`] by fastsimp
```
```  2671     ultimately show "P A"
```
```  2672       using A insert_Diff_single step[OF `finite ?B`] by fastsimp
```
```  2673   qed
```
```  2674 qed
```
```  2675
```
```  2676 end
```
```  2677
```
```  2678 context ordered_ab_semigroup_add
```
```  2679 begin
```
```  2680
```
```  2681 lemma add_Min_commute:
```
```  2682   fixes k
```
```  2683   assumes "finite N" and "N \<noteq> {}"
```
```  2684   shows "k + Min N = Min {k + m | m. m \<in> N}"
```
```  2685 proof -
```
```  2686   have "\<And>x y. k + min x y = min (k + x) (k + y)"
```
```  2687     by (simp add: min_def not_le)
```
```  2688       (blast intro: antisym less_imp_le add_left_mono)
```
```  2689   with assms show ?thesis
```
```  2690     using hom_Min_commute [of "plus k" N]
```
```  2691     by simp (blast intro: arg_cong [where f = Min])
```
```  2692 qed
```
```  2693
```
```  2694 lemma add_Max_commute:
```
```  2695   fixes k
```
```  2696   assumes "finite N" and "N \<noteq> {}"
```
```  2697   shows "k + Max N = Max {k + m | m. m \<in> N}"
```
```  2698 proof -
```
```  2699   have "\<And>x y. k + max x y = max (k + x) (k + y)"
```
```  2700     by (simp add: max_def not_le)
```
```  2701       (blast intro: antisym less_imp_le add_left_mono)
```
```  2702   with assms show ?thesis
```
```  2703     using hom_Max_commute [of "plus k" N]
```
```  2704     by simp (blast intro: arg_cong [where f = Max])
```
```  2705 qed
```
```  2706
```
```  2707 end
```
```  2708
```
```  2709 end
```