src/HOL/Finite_Set.thy
 author nipkow Thu Dec 11 08:52:50 2008 +0100 (2008-12-11) changeset 29106 25e28a4070f3 parent 29025 8c8859c0d734 child 29223 e09c53289830 permissions -rw-r--r--
Testfile for Stefan's code generator
```     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 assms 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 z {x\<^isub>1, ..., x\<^isub>n} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"}
```
```   483 if @{text f} is ``left-commutative'':
```
```   484 *}
```
```   485
```
```   486 locale fun_left_comm =
```
```   487   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
```
```   488   assumes fun_left_comm: "f x (f y z) = f y (f x z)"
```
```   489 begin
```
```   490
```
```   491 text{* On a functional level it looks much nicer: *}
```
```   492
```
```   493 lemma fun_comp_comm:  "f x \<circ> f y = f y \<circ> f x"
```
```   494 by (simp add: fun_left_comm expand_fun_eq)
```
```   495
```
```   496 end
```
```   497
```
```   498 inductive fold_graph :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool"
```
```   499 for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and z :: 'b where
```
```   500   emptyI [intro]: "fold_graph f z {} z" |
```
```   501   insertI [intro]: "x \<notin> A \<Longrightarrow> fold_graph f z A y
```
```   502       \<Longrightarrow> fold_graph f z (insert x A) (f x y)"
```
```   503
```
```   504 inductive_cases empty_fold_graphE [elim!]: "fold_graph f z {} x"
```
```   505
```
```   506 definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b" where
```
```   507 [code del]: "fold f z A = (THE y. fold_graph f z A y)"
```
```   508
```
```   509 text{*A tempting alternative for the definiens is
```
```   510 @{term "if finite A then THE y. fold_graph f z A y else e"}.
```
```   511 It allows the removal of finiteness assumptions from the theorems
```
```   512 @{text fold_comm}, @{text fold_reindex} and @{text fold_distrib}.
```
```   513 The proofs become ugly. It is not worth the effort. (???) *}
```
```   514
```
```   515
```
```   516 lemma Diff1_fold_graph:
```
```   517   "fold_graph f z (A - {x}) y \<Longrightarrow> x \<in> A \<Longrightarrow> fold_graph f z A (f x y)"
```
```   518 by (erule insert_Diff [THEN subst], rule fold_graph.intros, auto)
```
```   519
```
```   520 lemma fold_graph_imp_finite: "fold_graph f z A x \<Longrightarrow> finite A"
```
```   521 by (induct set: fold_graph) auto
```
```   522
```
```   523 lemma finite_imp_fold_graph: "finite A \<Longrightarrow> \<exists>x. fold_graph f z A x"
```
```   524 by (induct set: finite) auto
```
```   525
```
```   526
```
```   527 subsubsection{*From @{const fold_graph} to @{term fold}*}
```
```   528
```
```   529 lemma image_less_Suc: "h ` {i. i < Suc m} = insert (h m) (h ` {i. i < m})"
```
```   530   by (auto simp add: less_Suc_eq)
```
```   531
```
```   532 lemma insert_image_inj_on_eq:
```
```   533      "[|insert (h m) A = h ` {i. i < Suc m}; h m \<notin> A;
```
```   534         inj_on h {i. i < Suc m}|]
```
```   535       ==> A = h ` {i. i < m}"
```
```   536 apply (auto simp add: image_less_Suc inj_on_def)
```
```   537 apply (blast intro: less_trans)
```
```   538 done
```
```   539
```
```   540 lemma insert_inj_onE:
```
```   541   assumes aA: "insert a A = h`{i::nat. i<n}" and anot: "a \<notin> A"
```
```   542       and inj_on: "inj_on h {i::nat. i<n}"
```
```   543   shows "\<exists>hm m. inj_on hm {i::nat. i<m} & A = hm ` {i. i<m} & m < n"
```
```   544 proof (cases n)
```
```   545   case 0 thus ?thesis using aA by auto
```
```   546 next
```
```   547   case (Suc m)
```
```   548   have nSuc: "n = Suc m" by fact
```
```   549   have mlessn: "m<n" by (simp add: nSuc)
```
```   550   from aA obtain k where hkeq: "h k = a" and klessn: "k<n" by (blast elim!: equalityE)
```
```   551   let ?hm = "Fun.swap k m h"
```
```   552   have inj_hm: "inj_on ?hm {i. i < n}" using klessn mlessn
```
```   553     by (simp add: inj_on_swap_iff inj_on)
```
```   554   show ?thesis
```
```   555   proof (intro exI conjI)
```
```   556     show "inj_on ?hm {i. i < m}" using inj_hm
```
```   557       by (auto simp add: nSuc less_Suc_eq intro: subset_inj_on)
```
```   558     show "m<n" by (rule mlessn)
```
```   559     show "A = ?hm ` {i. i < m}"
```
```   560     proof (rule insert_image_inj_on_eq)
```
```   561       show "inj_on (Fun.swap k m h) {i. i < Suc m}" using inj_hm nSuc by simp
```
```   562       show "?hm m \<notin> A" by (simp add: swap_def hkeq anot)
```
```   563       show "insert (?hm m) A = ?hm ` {i. i < Suc m}"
```
```   564 	using aA hkeq nSuc klessn
```
```   565 	by (auto simp add: swap_def image_less_Suc fun_upd_image
```
```   566 			   less_Suc_eq inj_on_image_set_diff [OF inj_on])
```
```   567     qed
```
```   568   qed
```
```   569 qed
```
```   570
```
```   571 context fun_left_comm
```
```   572 begin
```
```   573
```
```   574 lemma fold_graph_determ_aux:
```
```   575   "A = h`{i::nat. i<n} \<Longrightarrow> inj_on h {i. i<n}
```
```   576    \<Longrightarrow> fold_graph f z A x \<Longrightarrow> fold_graph f z A x'
```
```   577    \<Longrightarrow> x' = x"
```
```   578 proof (induct n arbitrary: A x x' h rule: less_induct)
```
```   579   case (less n)
```
```   580   have IH: "\<And>m h A x x'. m < n \<Longrightarrow> A = h ` {i. i<m}
```
```   581       \<Longrightarrow> inj_on h {i. i<m} \<Longrightarrow> fold_graph f z A x
```
```   582       \<Longrightarrow> fold_graph f z A x' \<Longrightarrow> x' = x" by fact
```
```   583   have Afoldx: "fold_graph f z A x" and Afoldx': "fold_graph f z A x'"
```
```   584     and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" by fact+
```
```   585   show ?case
```
```   586   proof (rule fold_graph.cases [OF Afoldx])
```
```   587     assume "A = {}" and "x = z"
```
```   588     with Afoldx' show "x' = x" by auto
```
```   589   next
```
```   590     fix B b u
```
```   591     assume AbB: "A = insert b B" and x: "x = f b u"
```
```   592       and notinB: "b \<notin> B" and Bu: "fold_graph f z B u"
```
```   593     show "x'=x"
```
```   594     proof (rule fold_graph.cases [OF Afoldx'])
```
```   595       assume "A = {}" and "x' = z"
```
```   596       with AbB show "x' = x" by blast
```
```   597     next
```
```   598       fix C c v
```
```   599       assume AcC: "A = insert c C" and x': "x' = f c v"
```
```   600         and notinC: "c \<notin> C" and Cv: "fold_graph f z C v"
```
```   601       from A AbB have Beq: "insert b B = h`{i. i<n}" by simp
```
```   602       from insert_inj_onE [OF Beq notinB injh]
```
```   603       obtain hB mB where inj_onB: "inj_on hB {i. i < mB}"
```
```   604         and Beq: "B = hB ` {i. i < mB}" and lessB: "mB < n" by auto
```
```   605       from A AcC have Ceq: "insert c C = h`{i. i<n}" by simp
```
```   606       from insert_inj_onE [OF Ceq notinC injh]
```
```   607       obtain hC mC where inj_onC: "inj_on hC {i. i < mC}"
```
```   608         and Ceq: "C = hC ` {i. i < mC}" and lessC: "mC < n" by auto
```
```   609       show "x'=x"
```
```   610       proof cases
```
```   611         assume "b=c"
```
```   612 	then moreover have "B = C" using AbB AcC notinB notinC by auto
```
```   613 	ultimately show ?thesis  using Bu Cv x x' IH [OF lessC Ceq inj_onC]
```
```   614           by auto
```
```   615       next
```
```   616 	assume diff: "b \<noteq> c"
```
```   617 	let ?D = "B - {c}"
```
```   618 	have B: "B = insert c ?D" and C: "C = insert b ?D"
```
```   619 	  using AbB AcC notinB notinC diff by(blast elim!:equalityE)+
```
```   620 	have "finite A" by(rule fold_graph_imp_finite [OF Afoldx])
```
```   621 	with AbB have "finite ?D" by simp
```
```   622 	then obtain d where Dfoldd: "fold_graph f z ?D d"
```
```   623 	  using finite_imp_fold_graph by iprover
```
```   624 	moreover have cinB: "c \<in> B" using B by auto
```
```   625 	ultimately have "fold_graph f z B (f c d)" by(rule Diff1_fold_graph)
```
```   626 	hence "f c d = u" by (rule IH [OF lessB Beq inj_onB Bu])
```
```   627         moreover have "f b d = v"
```
```   628 	proof (rule IH[OF lessC Ceq inj_onC Cv])
```
```   629 	  show "fold_graph f z C (f b d)" using C notinB Dfoldd by fastsimp
```
```   630 	qed
```
```   631 	ultimately show ?thesis
```
```   632           using fun_left_comm [of c b] x x' by (auto simp add: o_def)
```
```   633       qed
```
```   634     qed
```
```   635   qed
```
```   636 qed
```
```   637
```
```   638 lemma fold_graph_determ:
```
```   639   "fold_graph f z A x \<Longrightarrow> fold_graph f z A y \<Longrightarrow> y = x"
```
```   640 apply (frule fold_graph_imp_finite [THEN finite_imp_nat_seg_image_inj_on])
```
```   641 apply (blast intro: fold_graph_determ_aux [rule_format])
```
```   642 done
```
```   643
```
```   644 lemma fold_equality:
```
```   645   "fold_graph f z A y \<Longrightarrow> fold f z A = y"
```
```   646 by (unfold fold_def) (blast intro: fold_graph_determ)
```
```   647
```
```   648 text{* The base case for @{text fold}: *}
```
```   649
```
```   650 lemma (in -) fold_empty [simp]: "fold f z {} = z"
```
```   651 by (unfold fold_def) blast
```
```   652
```
```   653 text{* The various recursion equations for @{const fold}: *}
```
```   654
```
```   655 lemma fold_insert_aux: "x \<notin> A
```
```   656   \<Longrightarrow> fold_graph f z (insert x A) v \<longleftrightarrow>
```
```   657       (\<exists>y. fold_graph f z A y \<and> v = f x y)"
```
```   658 apply auto
```
```   659 apply (rule_tac A1 = A and f1 = f in finite_imp_fold_graph [THEN exE])
```
```   660  apply (fastsimp dest: fold_graph_imp_finite)
```
```   661 apply (blast intro: fold_graph_determ)
```
```   662 done
```
```   663
```
```   664 lemma fold_insert [simp]:
```
```   665   "finite A ==> x \<notin> A ==> fold f z (insert x A) = f x (fold f z A)"
```
```   666 apply (simp add: fold_def fold_insert_aux)
```
```   667 apply (rule the_equality)
```
```   668  apply (auto intro: finite_imp_fold_graph
```
```   669         cong add: conj_cong simp add: fold_def[symmetric] fold_equality)
```
```   670 done
```
```   671
```
```   672 lemma fold_fun_comm:
```
```   673   "finite A \<Longrightarrow> f x (fold f z A) = fold f (f x z) A"
```
```   674 proof (induct rule: finite_induct)
```
```   675   case empty then show ?case by simp
```
```   676 next
```
```   677   case (insert y A) then show ?case
```
```   678     by (simp add: fun_left_comm[of x])
```
```   679 qed
```
```   680
```
```   681 lemma fold_insert2:
```
```   682   "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A"
```
```   683 by (simp add: fold_insert fold_fun_comm)
```
```   684
```
```   685 lemma fold_rec:
```
```   686 assumes "finite A" and "x \<in> A"
```
```   687 shows "fold f z A = f x (fold f z (A - {x}))"
```
```   688 proof -
```
```   689   have A: "A = insert x (A - {x})" using `x \<in> A` by blast
```
```   690   then have "fold f z A = fold f z (insert x (A - {x}))" by simp
```
```   691   also have "\<dots> = f x (fold f z (A - {x}))"
```
```   692     by (rule fold_insert) (simp add: `finite A`)+
```
```   693   finally show ?thesis .
```
```   694 qed
```
```   695
```
```   696 lemma fold_insert_remove:
```
```   697   assumes "finite A"
```
```   698   shows "fold f z (insert x A) = f x (fold f z (A - {x}))"
```
```   699 proof -
```
```   700   from `finite A` have "finite (insert x A)" by auto
```
```   701   moreover have "x \<in> insert x A" by auto
```
```   702   ultimately have "fold f z (insert x A) = f x (fold f z (insert x A - {x}))"
```
```   703     by (rule fold_rec)
```
```   704   then show ?thesis by simp
```
```   705 qed
```
```   706
```
```   707 end
```
```   708
```
```   709 text{* A simplified version for idempotent functions: *}
```
```   710
```
```   711 locale fun_left_comm_idem = fun_left_comm +
```
```   712   assumes fun_left_idem: "f x (f x z) = f x z"
```
```   713 begin
```
```   714
```
```   715 text{* The nice version: *}
```
```   716 lemma fun_comp_idem : "f x o f x = f x"
```
```   717 by (simp add: fun_left_idem expand_fun_eq)
```
```   718
```
```   719 lemma fold_insert_idem:
```
```   720   assumes fin: "finite A"
```
```   721   shows "fold f z (insert x A) = f x (fold f z A)"
```
```   722 proof cases
```
```   723   assume "x \<in> A"
```
```   724   then obtain B where "A = insert x B" and "x \<notin> B" by (rule set_insert)
```
```   725   then show ?thesis using assms by (simp add:fun_left_idem)
```
```   726 next
```
```   727   assume "x \<notin> A" then show ?thesis using assms by simp
```
```   728 qed
```
```   729
```
```   730 declare fold_insert[simp del] fold_insert_idem[simp]
```
```   731
```
```   732 lemma fold_insert_idem2:
```
```   733   "finite A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A"
```
```   734 by(simp add:fold_fun_comm)
```
```   735
```
```   736 end
```
```   737
```
```   738 subsubsection{* The derived combinator @{text fold_image} *}
```
```   739
```
```   740 definition fold_image :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"
```
```   741 where "fold_image f g = fold (%x y. f (g x) y)"
```
```   742
```
```   743 lemma fold_image_empty[simp]: "fold_image f g z {} = z"
```
```   744 by(simp add:fold_image_def)
```
```   745
```
```   746 context ab_semigroup_mult
```
```   747 begin
```
```   748
```
```   749 lemma fold_image_insert[simp]:
```
```   750 assumes "finite A" and "a \<notin> A"
```
```   751 shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)"
```
```   752 proof -
```
```   753   interpret I: fun_left_comm ["%x y. (g x) * y"]
```
```   754     by unfold_locales (simp add: mult_ac)
```
```   755   show ?thesis using assms by(simp add:fold_image_def I.fold_insert)
```
```   756 qed
```
```   757
```
```   758 (*
```
```   759 lemma fold_commute:
```
```   760   "finite A ==> (!!z. x * (fold times g z A) = fold times g (x * z) A)"
```
```   761   apply (induct set: finite)
```
```   762    apply simp
```
```   763   apply (simp add: mult_left_commute [of x])
```
```   764   done
```
```   765
```
```   766 lemma fold_nest_Un_Int:
```
```   767   "finite A ==> finite B
```
```   768     ==> fold times g (fold times g z B) A = fold times g (fold times g z (A Int B)) (A Un B)"
```
```   769   apply (induct set: finite)
```
```   770    apply simp
```
```   771   apply (simp add: fold_commute Int_insert_left insert_absorb)
```
```   772   done
```
```   773
```
```   774 lemma fold_nest_Un_disjoint:
```
```   775   "finite A ==> finite B ==> A Int B = {}
```
```   776     ==> fold times g z (A Un B) = fold times g (fold times g z B) A"
```
```   777   by (simp add: fold_nest_Un_Int)
```
```   778 *)
```
```   779
```
```   780 lemma fold_image_reindex:
```
```   781 assumes fin: "finite A"
```
```   782 shows "inj_on h A \<Longrightarrow> fold_image times g z (h`A) = fold_image times (g\<circ>h) z A"
```
```   783 using fin apply induct
```
```   784  apply simp
```
```   785 apply simp
```
```   786 done
```
```   787
```
```   788 (*
```
```   789 text{*
```
```   790   Fusion theorem, as described in Graham Hutton's paper,
```
```   791   A Tutorial on the Universality and Expressiveness of Fold,
```
```   792   JFP 9:4 (355-372), 1999.
```
```   793 *}
```
```   794
```
```   795 lemma fold_fusion:
```
```   796   assumes "ab_semigroup_mult g"
```
```   797   assumes fin: "finite A"
```
```   798     and hyp: "\<And>x y. h (g x y) = times x (h y)"
```
```   799   shows "h (fold g j w A) = fold times j (h w) A"
```
```   800 proof -
```
```   801   interpret ab_semigroup_mult [g] by fact
```
```   802   show ?thesis using fin hyp by (induct set: finite) simp_all
```
```   803 qed
```
```   804 *)
```
```   805
```
```   806 lemma fold_image_cong:
```
```   807   "finite A \<Longrightarrow>
```
```   808   (!!x. x:A ==> g x = h x) ==> fold_image times g z A = fold_image times h z A"
```
```   809 apply (subgoal_tac "ALL C. C <= A --> (ALL x:C. g x = h x) --> fold_image times g z C = fold_image times h z C")
```
```   810  apply simp
```
```   811 apply (erule finite_induct, simp)
```
```   812 apply (simp add: subset_insert_iff, clarify)
```
```   813 apply (subgoal_tac "finite C")
```
```   814  prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
```
```   815 apply (subgoal_tac "C = insert x (C - {x})")
```
```   816  prefer 2 apply blast
```
```   817 apply (erule ssubst)
```
```   818 apply (drule spec)
```
```   819 apply (erule (1) notE impE)
```
```   820 apply (simp add: Ball_def del: insert_Diff_single)
```
```   821 done
```
```   822
```
```   823 end
```
```   824
```
```   825 context comm_monoid_mult
```
```   826 begin
```
```   827
```
```   828 lemma fold_image_Un_Int:
```
```   829   "finite A ==> finite B ==>
```
```   830     fold_image times g 1 A * fold_image times g 1 B =
```
```   831     fold_image times g 1 (A Un B) * fold_image times g 1 (A Int B)"
```
```   832 by (induct set: finite)
```
```   833    (auto simp add: mult_ac insert_absorb Int_insert_left)
```
```   834
```
```   835 corollary fold_Un_disjoint:
```
```   836   "finite A ==> finite B ==> A Int B = {} ==>
```
```   837    fold_image times g 1 (A Un B) =
```
```   838    fold_image times g 1 A * fold_image times g 1 B"
```
```   839 by (simp add: fold_image_Un_Int)
```
```   840
```
```   841 lemma fold_image_UN_disjoint:
```
```   842   "\<lbrakk> finite I; ALL i:I. finite (A i);
```
```   843      ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {} \<rbrakk>
```
```   844    \<Longrightarrow> fold_image times g 1 (UNION I A) =
```
```   845        fold_image times (%i. fold_image times g 1 (A i)) 1 I"
```
```   846 apply (induct set: finite, simp, atomize)
```
```   847 apply (subgoal_tac "ALL i:F. x \<noteq> i")
```
```   848  prefer 2 apply blast
```
```   849 apply (subgoal_tac "A x Int UNION F A = {}")
```
```   850  prefer 2 apply blast
```
```   851 apply (simp add: fold_Un_disjoint)
```
```   852 done
```
```   853
```
```   854 lemma fold_image_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
```
```   855   fold_image times (%x. fold_image times (g x) 1 (B x)) 1 A =
```
```   856   fold_image times (split g) 1 (SIGMA x:A. B x)"
```
```   857 apply (subst Sigma_def)
```
```   858 apply (subst fold_image_UN_disjoint, assumption, simp)
```
```   859  apply blast
```
```   860 apply (erule fold_image_cong)
```
```   861 apply (subst fold_image_UN_disjoint, simp, simp)
```
```   862  apply blast
```
```   863 apply simp
```
```   864 done
```
```   865
```
```   866 lemma fold_image_distrib: "finite A \<Longrightarrow>
```
```   867    fold_image times (%x. g x * h x) 1 A =
```
```   868    fold_image times g 1 A *  fold_image times h 1 A"
```
```   869 by (erule finite_induct) (simp_all add: mult_ac)
```
```   870
```
```   871 end
```
```   872
```
```   873
```
```   874 subsection {* Generalized summation over a set *}
```
```   875
```
```   876 interpretation comm_monoid_add: comm_monoid_mult ["0::'a::comm_monoid_add" "op +"]
```
```   877   proof qed (auto intro: add_assoc add_commute)
```
```   878
```
```   879 definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
```
```   880 where "setsum f A == if finite A then fold_image (op +) f 0 A else 0"
```
```   881
```
```   882 abbreviation
```
```   883   Setsum  ("\<Sum>_"  999) where
```
```   884   "\<Sum>A == setsum (%x. x) A"
```
```   885
```
```   886 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
```
```   887 written @{text"\<Sum>x\<in>A. e"}. *}
```
```   888
```
```   889 syntax
```
```   890   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
```
```   891 syntax (xsymbols)
```
```   892   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
```
```   893 syntax (HTML output)
```
```   894   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
```
```   895
```
```   896 translations -- {* Beware of argument permutation! *}
```
```   897   "SUM i:A. b" == "CONST setsum (%i. b) A"
```
```   898   "\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
```
```   899
```
```   900 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
```
```   901  @{text"\<Sum>x|P. e"}. *}
```
```   902
```
```   903 syntax
```
```   904   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
```
```   905 syntax (xsymbols)
```
```   906   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
```
```   907 syntax (HTML output)
```
```   908   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
```
```   909
```
```   910 translations
```
```   911   "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
```
```   912   "\<Sum>x|P. t" => "CONST setsum (%x. t) {x. P}"
```
```   913
```
```   914 print_translation {*
```
```   915 let
```
```   916   fun setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) \$ Abs(y,Ty,P)] =
```
```   917     if x<>y then raise Match
```
```   918     else let val x' = Syntax.mark_bound x
```
```   919              val t' = subst_bound(x',t)
```
```   920              val P' = subst_bound(x',P)
```
```   921          in Syntax.const "_qsetsum" \$ Syntax.mark_bound x \$ P' \$ t' end
```
```   922 in [("setsum", setsum_tr')] end
```
```   923 *}
```
```   924
```
```   925
```
```   926 lemma setsum_empty [simp]: "setsum f {} = 0"
```
```   927 by (simp add: setsum_def)
```
```   928
```
```   929 lemma setsum_insert [simp]:
```
```   930   "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
```
```   931 by (simp add: setsum_def)
```
```   932
```
```   933 lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0"
```
```   934 by (simp add: setsum_def)
```
```   935
```
```   936 lemma setsum_reindex:
```
```   937      "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
```
```   938 by(auto simp add: setsum_def comm_monoid_add.fold_image_reindex dest!:finite_imageD)
```
```   939
```
```   940 lemma setsum_reindex_id:
```
```   941      "inj_on f B ==> setsum f B = setsum id (f ` B)"
```
```   942 by (auto simp add: setsum_reindex)
```
```   943
```
```   944 lemma setsum_cong:
```
```   945   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
```
```   946 by(fastsimp simp: setsum_def intro: comm_monoid_add.fold_image_cong)
```
```   947
```
```   948 lemma strong_setsum_cong[cong]:
```
```   949   "A = B ==> (!!x. x:B =simp=> f x = g x)
```
```   950    ==> setsum (%x. f x) A = setsum (%x. g x) B"
```
```   951 by(fastsimp simp: simp_implies_def setsum_def intro: comm_monoid_add.fold_image_cong)
```
```   952
```
```   953 lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A";
```
```   954 by (rule setsum_cong[OF refl], auto);
```
```   955
```
```   956 lemma setsum_reindex_cong:
```
```   957    "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|]
```
```   958     ==> setsum h B = setsum g A"
```
```   959 by (simp add: setsum_reindex cong: setsum_cong)
```
```   960
```
```   961 lemma setsum_0[simp]: "setsum (%i. 0) A = 0"
```
```   962 apply (clarsimp simp: setsum_def)
```
```   963 apply (erule finite_induct, auto)
```
```   964 done
```
```   965
```
```   966 lemma setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0"
```
```   967 by(simp add:setsum_cong)
```
```   968
```
```   969 lemma setsum_Un_Int: "finite A ==> finite B ==>
```
```   970   setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
```
```   971   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
```
```   972 by(simp add: setsum_def comm_monoid_add.fold_image_Un_Int [symmetric])
```
```   973
```
```   974 lemma setsum_Un_disjoint: "finite A ==> finite B
```
```   975   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
```
```   976 by (subst setsum_Un_Int [symmetric], auto)
```
```   977
```
```   978 (*But we can't get rid of finite I. If infinite, although the rhs is 0,
```
```   979   the lhs need not be, since UNION I A could still be finite.*)
```
```   980 lemma setsum_UN_disjoint:
```
```   981     "finite I ==> (ALL i:I. finite (A i)) ==>
```
```   982         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
```
```   983       setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
```
```   984 by(simp add: setsum_def comm_monoid_add.fold_image_UN_disjoint cong: setsum_cong)
```
```   985
```
```   986 text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
```
```   987 directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
```
```   988 lemma setsum_Union_disjoint:
```
```   989   "[| (ALL A:C. finite A);
```
```   990       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
```
```   991    ==> setsum f (Union C) = setsum (setsum f) C"
```
```   992 apply (cases "finite C")
```
```   993  prefer 2 apply (force dest: finite_UnionD simp add: setsum_def)
```
```   994   apply (frule setsum_UN_disjoint [of C id f])
```
```   995  apply (unfold Union_def id_def, assumption+)
```
```   996 done
```
```   997
```
```   998 (*But we can't get rid of finite A. If infinite, although the lhs is 0,
```
```   999   the rhs need not be, since SIGMA A B could still be finite.*)
```
```  1000 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
```
```  1001     (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
```
```  1002 by(simp add:setsum_def comm_monoid_add.fold_image_Sigma split_def cong:setsum_cong)
```
```  1003
```
```  1004 text{*Here we can eliminate the finiteness assumptions, by cases.*}
```
```  1005 lemma setsum_cartesian_product:
```
```  1006    "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)"
```
```  1007 apply (cases "finite A")
```
```  1008  apply (cases "finite B")
```
```  1009   apply (simp add: setsum_Sigma)
```
```  1010  apply (cases "A={}", simp)
```
```  1011  apply (simp)
```
```  1012 apply (auto simp add: setsum_def
```
```  1013             dest: finite_cartesian_productD1 finite_cartesian_productD2)
```
```  1014 done
```
```  1015
```
```  1016 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
```
```  1017 by(simp add:setsum_def comm_monoid_add.fold_image_distrib)
```
```  1018
```
```  1019
```
```  1020 subsubsection {* Properties in more restricted classes of structures *}
```
```  1021
```
```  1022 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
```
```  1023 apply (case_tac "finite A")
```
```  1024  prefer 2 apply (simp add: setsum_def)
```
```  1025 apply (erule rev_mp)
```
```  1026 apply (erule finite_induct, auto)
```
```  1027 done
```
```  1028
```
```  1029 lemma setsum_eq_0_iff [simp]:
```
```  1030     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
```
```  1031 by (induct set: finite) auto
```
```  1032
```
```  1033 lemma setsum_Un_nat: "finite A ==> finite B ==>
```
```  1034   (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
```
```  1035   -- {* For the natural numbers, we have subtraction. *}
```
```  1036 by (subst setsum_Un_Int [symmetric], auto simp add: ring_simps)
```
```  1037
```
```  1038 lemma setsum_Un: "finite A ==> finite B ==>
```
```  1039   (setsum f (A Un B) :: 'a :: ab_group_add) =
```
```  1040    setsum f A + setsum f B - setsum f (A Int B)"
```
```  1041 by (subst setsum_Un_Int [symmetric], auto simp add: ring_simps)
```
```  1042
```
```  1043 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
```
```  1044   (if a:A then setsum f A - f a else setsum f A)"
```
```  1045 apply (case_tac "finite A")
```
```  1046  prefer 2 apply (simp add: setsum_def)
```
```  1047 apply (erule finite_induct)
```
```  1048  apply (auto simp add: insert_Diff_if)
```
```  1049 apply (drule_tac a = a in mk_disjoint_insert, auto)
```
```  1050 done
```
```  1051
```
```  1052 lemma setsum_diff1: "finite A \<Longrightarrow>
```
```  1053   (setsum f (A - {a}) :: ('a::ab_group_add)) =
```
```  1054   (if a:A then setsum f A - f a else setsum f A)"
```
```  1055 by (erule finite_induct) (auto simp add: insert_Diff_if)
```
```  1056
```
```  1057 lemma setsum_diff1'[rule_format]:
```
```  1058   "finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x)"
```
```  1059 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))"])
```
```  1060 apply (auto simp add: insert_Diff_if add_ac)
```
```  1061 done
```
```  1062
```
```  1063 (* By Jeremy Siek: *)
```
```  1064
```
```  1065 lemma setsum_diff_nat:
```
```  1066 assumes "finite B" and "B \<subseteq> A"
```
```  1067 shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
```
```  1068 using assms
```
```  1069 proof induct
```
```  1070   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
```
```  1071 next
```
```  1072   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
```
```  1073     and xFinA: "insert x F \<subseteq> A"
```
```  1074     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
```
```  1075   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
```
```  1076   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
```
```  1077     by (simp add: setsum_diff1_nat)
```
```  1078   from xFinA have "F \<subseteq> A" by simp
```
```  1079   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
```
```  1080   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
```
```  1081     by simp
```
```  1082   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
```
```  1083   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
```
```  1084     by simp
```
```  1085   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
```
```  1086   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
```
```  1087     by simp
```
```  1088   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
```
```  1089 qed
```
```  1090
```
```  1091 lemma setsum_diff:
```
```  1092   assumes le: "finite A" "B \<subseteq> A"
```
```  1093   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
```
```  1094 proof -
```
```  1095   from le have finiteB: "finite B" using finite_subset by auto
```
```  1096   show ?thesis using finiteB le
```
```  1097   proof induct
```
```  1098     case empty
```
```  1099     thus ?case by auto
```
```  1100   next
```
```  1101     case (insert x F)
```
```  1102     thus ?case using le finiteB
```
```  1103       by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
```
```  1104   qed
```
```  1105 qed
```
```  1106
```
```  1107 lemma setsum_mono:
```
```  1108   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))"
```
```  1109   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
```
```  1110 proof (cases "finite K")
```
```  1111   case True
```
```  1112   thus ?thesis using le
```
```  1113   proof induct
```
```  1114     case empty
```
```  1115     thus ?case by simp
```
```  1116   next
```
```  1117     case insert
```
```  1118     thus ?case using add_mono by fastsimp
```
```  1119   qed
```
```  1120 next
```
```  1121   case False
```
```  1122   thus ?thesis
```
```  1123     by (simp add: setsum_def)
```
```  1124 qed
```
```  1125
```
```  1126 lemma setsum_strict_mono:
```
```  1127   fixes f :: "'a \<Rightarrow> 'b::{pordered_cancel_ab_semigroup_add,comm_monoid_add}"
```
```  1128   assumes "finite A"  "A \<noteq> {}"
```
```  1129     and "!!x. x:A \<Longrightarrow> f x < g x"
```
```  1130   shows "setsum f A < setsum g A"
```
```  1131   using prems
```
```  1132 proof (induct rule: finite_ne_induct)
```
```  1133   case singleton thus ?case by simp
```
```  1134 next
```
```  1135   case insert thus ?case by (auto simp: add_strict_mono)
```
```  1136 qed
```
```  1137
```
```  1138 lemma setsum_negf:
```
```  1139   "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
```
```  1140 proof (cases "finite A")
```
```  1141   case True thus ?thesis by (induct set: finite) auto
```
```  1142 next
```
```  1143   case False thus ?thesis by (simp add: setsum_def)
```
```  1144 qed
```
```  1145
```
```  1146 lemma setsum_subtractf:
```
```  1147   "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
```
```  1148     setsum f A - setsum g A"
```
```  1149 proof (cases "finite A")
```
```  1150   case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
```
```  1151 next
```
```  1152   case False thus ?thesis by (simp add: setsum_def)
```
```  1153 qed
```
```  1154
```
```  1155 lemma setsum_nonneg:
```
```  1156   assumes nn: "\<forall>x\<in>A. (0::'a::{pordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
```
```  1157   shows "0 \<le> setsum f A"
```
```  1158 proof (cases "finite A")
```
```  1159   case True thus ?thesis using nn
```
```  1160   proof induct
```
```  1161     case empty then show ?case by simp
```
```  1162   next
```
```  1163     case (insert x F)
```
```  1164     then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
```
```  1165     with insert show ?case by simp
```
```  1166   qed
```
```  1167 next
```
```  1168   case False thus ?thesis by (simp add: setsum_def)
```
```  1169 qed
```
```  1170
```
```  1171 lemma setsum_nonpos:
```
```  1172   assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{pordered_ab_semigroup_add,comm_monoid_add})"
```
```  1173   shows "setsum f A \<le> 0"
```
```  1174 proof (cases "finite A")
```
```  1175   case True thus ?thesis using np
```
```  1176   proof induct
```
```  1177     case empty then show ?case by simp
```
```  1178   next
```
```  1179     case (insert x F)
```
```  1180     then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
```
```  1181     with insert show ?case by simp
```
```  1182   qed
```
```  1183 next
```
```  1184   case False thus ?thesis by (simp add: setsum_def)
```
```  1185 qed
```
```  1186
```
```  1187 lemma setsum_mono2:
```
```  1188 fixes f :: "'a \<Rightarrow> 'b :: {pordered_ab_semigroup_add_imp_le,comm_monoid_add}"
```
```  1189 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
```
```  1190 shows "setsum f A \<le> setsum f B"
```
```  1191 proof -
```
```  1192   have "setsum f A \<le> setsum f A + setsum f (B-A)"
```
```  1193     by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
```
```  1194   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
```
```  1195     by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
```
```  1196   also have "A \<union> (B-A) = B" using sub by blast
```
```  1197   finally show ?thesis .
```
```  1198 qed
```
```  1199
```
```  1200 lemma setsum_mono3: "finite B ==> A <= B ==>
```
```  1201     ALL x: B - A.
```
```  1202       0 <= ((f x)::'a::{comm_monoid_add,pordered_ab_semigroup_add}) ==>
```
```  1203         setsum f A <= setsum f B"
```
```  1204   apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
```
```  1205   apply (erule ssubst)
```
```  1206   apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
```
```  1207   apply simp
```
```  1208   apply (rule add_left_mono)
```
```  1209   apply (erule setsum_nonneg)
```
```  1210   apply (subst setsum_Un_disjoint [THEN sym])
```
```  1211   apply (erule finite_subset, assumption)
```
```  1212   apply (rule finite_subset)
```
```  1213   prefer 2
```
```  1214   apply assumption
```
```  1215   apply auto
```
```  1216   apply (rule setsum_cong)
```
```  1217   apply auto
```
```  1218 done
```
```  1219
```
```  1220 lemma setsum_right_distrib:
```
```  1221   fixes f :: "'a => ('b::semiring_0)"
```
```  1222   shows "r * setsum f A = setsum (%n. r * f n) A"
```
```  1223 proof (cases "finite A")
```
```  1224   case True
```
```  1225   thus ?thesis
```
```  1226   proof induct
```
```  1227     case empty thus ?case by simp
```
```  1228   next
```
```  1229     case (insert x A) thus ?case by (simp add: right_distrib)
```
```  1230   qed
```
```  1231 next
```
```  1232   case False thus ?thesis by (simp add: setsum_def)
```
```  1233 qed
```
```  1234
```
```  1235 lemma setsum_left_distrib:
```
```  1236   "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
```
```  1237 proof (cases "finite A")
```
```  1238   case True
```
```  1239   then show ?thesis
```
```  1240   proof induct
```
```  1241     case empty thus ?case by simp
```
```  1242   next
```
```  1243     case (insert x A) thus ?case by (simp add: left_distrib)
```
```  1244   qed
```
```  1245 next
```
```  1246   case False thus ?thesis by (simp add: setsum_def)
```
```  1247 qed
```
```  1248
```
```  1249 lemma setsum_divide_distrib:
```
```  1250   "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
```
```  1251 proof (cases "finite A")
```
```  1252   case True
```
```  1253   then show ?thesis
```
```  1254   proof induct
```
```  1255     case empty thus ?case by simp
```
```  1256   next
```
```  1257     case (insert x A) thus ?case by (simp add: add_divide_distrib)
```
```  1258   qed
```
```  1259 next
```
```  1260   case False thus ?thesis by (simp add: setsum_def)
```
```  1261 qed
```
```  1262
```
```  1263 lemma setsum_abs[iff]:
```
```  1264   fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
```
```  1265   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
```
```  1266 proof (cases "finite A")
```
```  1267   case True
```
```  1268   thus ?thesis
```
```  1269   proof induct
```
```  1270     case empty thus ?case by simp
```
```  1271   next
```
```  1272     case (insert x A)
```
```  1273     thus ?case by (auto intro: abs_triangle_ineq order_trans)
```
```  1274   qed
```
```  1275 next
```
```  1276   case False thus ?thesis by (simp add: setsum_def)
```
```  1277 qed
```
```  1278
```
```  1279 lemma setsum_abs_ge_zero[iff]:
```
```  1280   fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
```
```  1281   shows "0 \<le> setsum (%i. abs(f i)) A"
```
```  1282 proof (cases "finite A")
```
```  1283   case True
```
```  1284   thus ?thesis
```
```  1285   proof induct
```
```  1286     case empty thus ?case by simp
```
```  1287   next
```
```  1288     case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg)
```
```  1289   qed
```
```  1290 next
```
```  1291   case False thus ?thesis by (simp add: setsum_def)
```
```  1292 qed
```
```  1293
```
```  1294 lemma abs_setsum_abs[simp]:
```
```  1295   fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
```
```  1296   shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
```
```  1297 proof (cases "finite A")
```
```  1298   case True
```
```  1299   thus ?thesis
```
```  1300   proof induct
```
```  1301     case empty thus ?case by simp
```
```  1302   next
```
```  1303     case (insert a A)
```
```  1304     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
```
```  1305     also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
```
```  1306     also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
```
```  1307       by (simp del: abs_of_nonneg)
```
```  1308     also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
```
```  1309     finally show ?case .
```
```  1310   qed
```
```  1311 next
```
```  1312   case False thus ?thesis by (simp add: setsum_def)
```
```  1313 qed
```
```  1314
```
```  1315
```
```  1316 text {* Commuting outer and inner summation *}
```
```  1317
```
```  1318 lemma swap_inj_on:
```
```  1319   "inj_on (%(i, j). (j, i)) (A \<times> B)"
```
```  1320   by (unfold inj_on_def) fast
```
```  1321
```
```  1322 lemma swap_product:
```
```  1323   "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
```
```  1324   by (simp add: split_def image_def) blast
```
```  1325
```
```  1326 lemma setsum_commute:
```
```  1327   "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
```
```  1328 proof (simp add: setsum_cartesian_product)
```
```  1329   have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
```
```  1330     (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
```
```  1331     (is "?s = _")
```
```  1332     apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on)
```
```  1333     apply (simp add: split_def)
```
```  1334     done
```
```  1335   also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
```
```  1336     (is "_ = ?t")
```
```  1337     apply (simp add: swap_product)
```
```  1338     done
```
```  1339   finally show "?s = ?t" .
```
```  1340 qed
```
```  1341
```
```  1342 lemma setsum_product:
```
```  1343   fixes f :: "'a => ('b::semiring_0)"
```
```  1344   shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
```
```  1345   by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
```
```  1346
```
```  1347
```
```  1348 subsection {* Generalized product over a set *}
```
```  1349
```
```  1350 definition setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
```
```  1351 where "setprod f A == if finite A then fold_image (op *) f 1 A else 1"
```
```  1352
```
```  1353 abbreviation
```
```  1354   Setprod  ("\<Prod>_"  999) where
```
```  1355   "\<Prod>A == setprod (%x. x) A"
```
```  1356
```
```  1357 syntax
```
```  1358   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
```
```  1359 syntax (xsymbols)
```
```  1360   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
```
```  1361 syntax (HTML output)
```
```  1362   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
```
```  1363
```
```  1364 translations -- {* Beware of argument permutation! *}
```
```  1365   "PROD i:A. b" == "CONST setprod (%i. b) A"
```
```  1366   "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A"
```
```  1367
```
```  1368 text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
```
```  1369  @{text"\<Prod>x|P. e"}. *}
```
```  1370
```
```  1371 syntax
```
```  1372   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
```
```  1373 syntax (xsymbols)
```
```  1374   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
```
```  1375 syntax (HTML output)
```
```  1376   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
```
```  1377
```
```  1378 translations
```
```  1379   "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
```
```  1380   "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
```
```  1381
```
```  1382
```
```  1383 lemma setprod_empty [simp]: "setprod f {} = 1"
```
```  1384 by (auto simp add: setprod_def)
```
```  1385
```
```  1386 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
```
```  1387     setprod f (insert a A) = f a * setprod f A"
```
```  1388 by (simp add: setprod_def)
```
```  1389
```
```  1390 lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
```
```  1391 by (simp add: setprod_def)
```
```  1392
```
```  1393 lemma setprod_reindex:
```
```  1394    "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
```
```  1395 by(auto simp: setprod_def fold_image_reindex dest!:finite_imageD)
```
```  1396
```
```  1397 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
```
```  1398 by (auto simp add: setprod_reindex)
```
```  1399
```
```  1400 lemma setprod_cong:
```
```  1401   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
```
```  1402 by(fastsimp simp: setprod_def intro: fold_image_cong)
```
```  1403
```
```  1404 lemma strong_setprod_cong:
```
```  1405   "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
```
```  1406 by(fastsimp simp: simp_implies_def setprod_def intro: fold_image_cong)
```
```  1407
```
```  1408 lemma setprod_reindex_cong: "inj_on f A ==>
```
```  1409     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
```
```  1410 by (frule setprod_reindex, simp)
```
```  1411
```
```  1412
```
```  1413 lemma setprod_1: "setprod (%i. 1) A = 1"
```
```  1414 apply (case_tac "finite A")
```
```  1415 apply (erule finite_induct, auto simp add: mult_ac)
```
```  1416 done
```
```  1417
```
```  1418 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
```
```  1419 apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
```
```  1420 apply (erule ssubst, rule setprod_1)
```
```  1421 apply (rule setprod_cong, auto)
```
```  1422 done
```
```  1423
```
```  1424 lemma setprod_Un_Int: "finite A ==> finite B
```
```  1425     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
```
```  1426 by(simp add: setprod_def fold_image_Un_Int[symmetric])
```
```  1427
```
```  1428 lemma setprod_Un_disjoint: "finite A ==> finite B
```
```  1429   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
```
```  1430 by (subst setprod_Un_Int [symmetric], auto)
```
```  1431
```
```  1432 lemma setprod_UN_disjoint:
```
```  1433     "finite I ==> (ALL i:I. finite (A i)) ==>
```
```  1434         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
```
```  1435       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
```
```  1436 by(simp add: setprod_def fold_image_UN_disjoint cong: setprod_cong)
```
```  1437
```
```  1438 lemma setprod_Union_disjoint:
```
```  1439   "[| (ALL A:C. finite A);
```
```  1440       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
```
```  1441    ==> setprod f (Union C) = setprod (setprod f) C"
```
```  1442 apply (cases "finite C")
```
```  1443  prefer 2 apply (force dest: finite_UnionD simp add: setprod_def)
```
```  1444   apply (frule setprod_UN_disjoint [of C id f])
```
```  1445  apply (unfold Union_def id_def, assumption+)
```
```  1446 done
```
```  1447
```
```  1448 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
```
```  1449     (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
```
```  1450     (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
```
```  1451 by(simp add:setprod_def fold_image_Sigma split_def cong:setprod_cong)
```
```  1452
```
```  1453 text{*Here we can eliminate the finiteness assumptions, by cases.*}
```
```  1454 lemma setprod_cartesian_product:
```
```  1455      "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
```
```  1456 apply (cases "finite A")
```
```  1457  apply (cases "finite B")
```
```  1458   apply (simp add: setprod_Sigma)
```
```  1459  apply (cases "A={}", simp)
```
```  1460  apply (simp add: setprod_1)
```
```  1461 apply (auto simp add: setprod_def
```
```  1462             dest: finite_cartesian_productD1 finite_cartesian_productD2)
```
```  1463 done
```
```  1464
```
```  1465 lemma setprod_timesf:
```
```  1466      "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
```
```  1467 by(simp add:setprod_def fold_image_distrib)
```
```  1468
```
```  1469
```
```  1470 subsubsection {* Properties in more restricted classes of structures *}
```
```  1471
```
```  1472 lemma setprod_eq_1_iff [simp]:
```
```  1473   "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
```
```  1474 by (induct set: finite) auto
```
```  1475
```
```  1476 lemma setprod_zero:
```
```  1477      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
```
```  1478 apply (induct set: finite, force, clarsimp)
```
```  1479 apply (erule disjE, auto)
```
```  1480 done
```
```  1481
```
```  1482 lemma setprod_nonneg [rule_format]:
```
```  1483    "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A"
```
```  1484 apply (case_tac "finite A")
```
```  1485 apply (induct set: finite, force, clarsimp)
```
```  1486 apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
```
```  1487 apply (rule mult_mono, assumption+)
```
```  1488 apply (auto simp add: setprod_def)
```
```  1489 done
```
```  1490
```
```  1491 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x)
```
```  1492   --> 0 < setprod f A"
```
```  1493 apply (case_tac "finite A")
```
```  1494 apply (induct set: finite, force, clarsimp)
```
```  1495 apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
```
```  1496 apply (rule mult_strict_mono, assumption+)
```
```  1497 apply (auto simp add: setprod_def)
```
```  1498 done
```
```  1499
```
```  1500 lemma setprod_nonzero [rule_format]:
```
```  1501   "(ALL x y. (x::'a::comm_semiring_1) * y = 0 --> x = 0 | y = 0) ==>
```
```  1502     finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
```
```  1503 by (erule finite_induct, auto)
```
```  1504
```
```  1505 lemma setprod_zero_eq:
```
```  1506     "(ALL x y. (x::'a::comm_semiring_1) * y = 0 --> x = 0 | y = 0) ==>
```
```  1507      finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
```
```  1508 by (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
```
```  1509
```
```  1510 lemma setprod_nonzero_field:
```
```  1511     "finite A ==> (ALL x: A. f x \<noteq> (0::'a::idom)) ==> setprod f A \<noteq> 0"
```
```  1512 by (rule setprod_nonzero, auto)
```
```  1513
```
```  1514 lemma setprod_zero_eq_field:
```
```  1515     "finite A ==> (setprod f A = (0::'a::idom)) = (EX x: A. f x = 0)"
```
```  1516 by (rule setprod_zero_eq, auto)
```
```  1517
```
```  1518 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
```
```  1519   (setprod f (A Un B) :: 'a ::{field})
```
```  1520    = setprod f A * setprod f B / setprod f (A Int B)"
```
```  1521 apply (subst setprod_Un_Int [symmetric], auto)
```
```  1522 apply (subgoal_tac "finite (A Int B)")
```
```  1523 apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
```
```  1524 apply (subst times_divide_eq_right [THEN sym], auto)
```
```  1525 done
```
```  1526
```
```  1527 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
```
```  1528   (setprod f (A - {a}) :: 'a :: {field}) =
```
```  1529   (if a:A then setprod f A / f a else setprod f A)"
```
```  1530 by (erule finite_induct) (auto simp add: insert_Diff_if)
```
```  1531
```
```  1532 lemma setprod_inversef: "finite A ==>
```
```  1533   ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
```
```  1534   setprod (inverse \<circ> f) A = inverse (setprod f A)"
```
```  1535 by (erule finite_induct) auto
```
```  1536
```
```  1537 lemma setprod_dividef:
```
```  1538    "[|finite A;
```
```  1539       \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
```
```  1540     ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
```
```  1541 apply (subgoal_tac
```
```  1542          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
```
```  1543 apply (erule ssubst)
```
```  1544 apply (subst divide_inverse)
```
```  1545 apply (subst setprod_timesf)
```
```  1546 apply (subst setprod_inversef, assumption+, rule refl)
```
```  1547 apply (rule setprod_cong, rule refl)
```
```  1548 apply (subst divide_inverse, auto)
```
```  1549 done
```
```  1550
```
```  1551
```
```  1552 subsection {* Finite cardinality *}
```
```  1553
```
```  1554 text {* This definition, although traditional, is ugly to work with:
```
```  1555 @{text "card A == LEAST n. EX f. A = {f i | i. i < n}"}.
```
```  1556 But now that we have @{text setsum} things are easy:
```
```  1557 *}
```
```  1558
```
```  1559 definition card :: "'a set \<Rightarrow> nat"
```
```  1560 where "card A = setsum (\<lambda>x. 1) A"
```
```  1561
```
```  1562 lemma card_empty [simp]: "card {} = 0"
```
```  1563 by (simp add: card_def)
```
```  1564
```
```  1565 lemma card_infinite [simp]: "~ finite A ==> card A = 0"
```
```  1566 by (simp add: card_def)
```
```  1567
```
```  1568 lemma card_eq_setsum: "card A = setsum (%x. 1) A"
```
```  1569 by (simp add: card_def)
```
```  1570
```
```  1571 lemma card_insert_disjoint [simp]:
```
```  1572   "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
```
```  1573 by(simp add: card_def)
```
```  1574
```
```  1575 lemma card_insert_if:
```
```  1576   "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
```
```  1577 by (simp add: insert_absorb)
```
```  1578
```
```  1579 lemma card_0_eq [simp,noatp]: "finite A ==> (card A = 0) = (A = {})"
```
```  1580 apply auto
```
```  1581 apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
```
```  1582 done
```
```  1583
```
```  1584 lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
```
```  1585 by auto
```
```  1586
```
```  1587
```
```  1588 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
```
```  1589 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
```
```  1590 apply(simp del:insert_Diff_single)
```
```  1591 done
```
```  1592
```
```  1593 lemma card_Diff_singleton:
```
```  1594   "finite A ==> x: A ==> card (A - {x}) = card A - 1"
```
```  1595 by (simp add: card_Suc_Diff1 [symmetric])
```
```  1596
```
```  1597 lemma card_Diff_singleton_if:
```
```  1598   "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
```
```  1599 by (simp add: card_Diff_singleton)
```
```  1600
```
```  1601 lemma card_Diff_insert[simp]:
```
```  1602 assumes "finite A" and "a:A" and "a ~: B"
```
```  1603 shows "card(A - insert a B) = card(A - B) - 1"
```
```  1604 proof -
```
```  1605   have "A - insert a B = (A - B) - {a}" using assms by blast
```
```  1606   then show ?thesis using assms by(simp add:card_Diff_singleton)
```
```  1607 qed
```
```  1608
```
```  1609 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
```
```  1610 by (simp add: card_insert_if card_Suc_Diff1 del:card_Diff_insert)
```
```  1611
```
```  1612 lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
```
```  1613 by (simp add: card_insert_if)
```
```  1614
```
```  1615 lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
```
```  1616 by (simp add: card_def setsum_mono2)
```
```  1617
```
```  1618 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
```
```  1619 apply (induct set: finite, simp, clarify)
```
```  1620 apply (subgoal_tac "finite A & A - {x} <= F")
```
```  1621  prefer 2 apply (blast intro: finite_subset, atomize)
```
```  1622 apply (drule_tac x = "A - {x}" in spec)
```
```  1623 apply (simp add: card_Diff_singleton_if split add: split_if_asm)
```
```  1624 apply (case_tac "card A", auto)
```
```  1625 done
```
```  1626
```
```  1627 lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
```
```  1628 apply (simp add: psubset_eq linorder_not_le [symmetric])
```
```  1629 apply (blast dest: card_seteq)
```
```  1630 done
```
```  1631
```
```  1632 lemma card_Un_Int: "finite A ==> finite B
```
```  1633     ==> card A + card B = card (A Un B) + card (A Int B)"
```
```  1634 by(simp add:card_def setsum_Un_Int)
```
```  1635
```
```  1636 lemma card_Un_disjoint: "finite A ==> finite B
```
```  1637     ==> A Int B = {} ==> card (A Un B) = card A + card B"
```
```  1638 by (simp add: card_Un_Int)
```
```  1639
```
```  1640 lemma card_Diff_subset:
```
```  1641   "finite B ==> B <= A ==> card (A - B) = card A - card B"
```
```  1642 by(simp add:card_def setsum_diff_nat)
```
```  1643
```
```  1644 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
```
```  1645 apply (rule Suc_less_SucD)
```
```  1646 apply (simp add: card_Suc_Diff1 del:card_Diff_insert)
```
```  1647 done
```
```  1648
```
```  1649 lemma card_Diff2_less:
```
```  1650   "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
```
```  1651 apply (case_tac "x = y")
```
```  1652  apply (simp add: card_Diff1_less del:card_Diff_insert)
```
```  1653 apply (rule less_trans)
```
```  1654  prefer 2 apply (auto intro!: card_Diff1_less simp del:card_Diff_insert)
```
```  1655 done
```
```  1656
```
```  1657 lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
```
```  1658 apply (case_tac "x : A")
```
```  1659  apply (simp_all add: card_Diff1_less less_imp_le)
```
```  1660 done
```
```  1661
```
```  1662 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
```
```  1663 by (erule psubsetI, blast)
```
```  1664
```
```  1665 lemma insert_partition:
```
```  1666   "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
```
```  1667   \<Longrightarrow> x \<inter> \<Union> F = {}"
```
```  1668 by auto
```
```  1669
```
```  1670 text{* main cardinality theorem *}
```
```  1671 lemma card_partition [rule_format]:
```
```  1672   "finite C ==>
```
```  1673      finite (\<Union> C) -->
```
```  1674      (\<forall>c\<in>C. card c = k) -->
```
```  1675      (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->
```
```  1676      k * card(C) = card (\<Union> C)"
```
```  1677 apply (erule finite_induct, simp)
```
```  1678 apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition
```
```  1679        finite_subset [of _ "\<Union> (insert x F)"])
```
```  1680 done
```
```  1681
```
```  1682
```
```  1683 text{*The form of a finite set of given cardinality*}
```
```  1684
```
```  1685 lemma card_eq_SucD:
```
```  1686 assumes "card A = Suc k"
```
```  1687 shows "\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={})"
```
```  1688 proof -
```
```  1689   have fin: "finite A" using assms by (auto intro: ccontr)
```
```  1690   moreover have "card A \<noteq> 0" using assms by auto
```
```  1691   ultimately obtain b where b: "b \<in> A" by auto
```
```  1692   show ?thesis
```
```  1693   proof (intro exI conjI)
```
```  1694     show "A = insert b (A-{b})" using b by blast
```
```  1695     show "b \<notin> A - {b}" by blast
```
```  1696     show "card (A - {b}) = k" and "k = 0 \<longrightarrow> A - {b} = {}"
```
```  1697       using assms b fin by(fastsimp dest:mk_disjoint_insert)+
```
```  1698   qed
```
```  1699 qed
```
```  1700
```
```  1701 lemma card_Suc_eq:
```
```  1702   "(card A = Suc k) =
```
```  1703    (\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={}))"
```
```  1704 apply(rule iffI)
```
```  1705  apply(erule card_eq_SucD)
```
```  1706 apply(auto)
```
```  1707 apply(subst card_insert)
```
```  1708  apply(auto intro:ccontr)
```
```  1709 done
```
```  1710
```
```  1711 lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
```
```  1712 apply (cases "finite A")
```
```  1713 apply (erule finite_induct)
```
```  1714 apply (auto simp add: ring_simps)
```
```  1715 done
```
```  1716
```
```  1717 lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{recpower, comm_monoid_mult})) = y^(card A)"
```
```  1718 apply (erule finite_induct)
```
```  1719 apply (auto simp add: power_Suc)
```
```  1720 done
```
```  1721
```
```  1722 lemma setsum_bounded:
```
```  1723   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, pordered_ab_semigroup_add})"
```
```  1724   shows "setsum f A \<le> of_nat(card A) * K"
```
```  1725 proof (cases "finite A")
```
```  1726   case True
```
```  1727   thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
```
```  1728 next
```
```  1729   case False thus ?thesis by (simp add: setsum_def)
```
```  1730 qed
```
```  1731
```
```  1732
```
```  1733 subsubsection {* Cardinality of unions *}
```
```  1734
```
```  1735 lemma card_UN_disjoint:
```
```  1736   "finite I ==> (ALL i:I. finite (A i)) ==>
```
```  1737    (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {})
```
```  1738    ==> card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
```
```  1739 apply (simp add: card_def del: setsum_constant)
```
```  1740 apply (subgoal_tac
```
```  1741          "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
```
```  1742 apply (simp add: setsum_UN_disjoint del: setsum_constant)
```
```  1743 apply (simp cong: setsum_cong)
```
```  1744 done
```
```  1745
```
```  1746 lemma card_Union_disjoint:
```
```  1747   "finite C ==> (ALL A:C. finite A) ==>
```
```  1748    (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
```
```  1749    ==> card (Union C) = setsum card C"
```
```  1750 apply (frule card_UN_disjoint [of C id])
```
```  1751 apply (unfold Union_def id_def, assumption+)
```
```  1752 done
```
```  1753
```
```  1754
```
```  1755 subsubsection {* Cardinality of image *}
```
```  1756
```
```  1757 text{*The image of a finite set can be expressed using @{term fold_image}.*}
```
```  1758 lemma image_eq_fold_image:
```
```  1759   "finite A ==> f ` A = fold_image (op Un) (%x. {f x}) {} A"
```
```  1760 proof (induct rule: finite_induct)
```
```  1761   case empty then show ?case by simp
```
```  1762 next
```
```  1763   interpret ab_semigroup_mult ["op Un"]
```
```  1764     proof qed auto
```
```  1765   case insert
```
```  1766   then show ?case by simp
```
```  1767 qed
```
```  1768
```
```  1769 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
```
```  1770 apply (induct set: finite)
```
```  1771  apply simp
```
```  1772 apply (simp add: le_SucI finite_imageI card_insert_if)
```
```  1773 done
```
```  1774
```
```  1775 lemma card_image: "inj_on f A ==> card (f ` A) = card A"
```
```  1776 by(simp add:card_def setsum_reindex o_def del:setsum_constant)
```
```  1777
```
```  1778 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
```
```  1779 by (simp add: card_seteq card_image)
```
```  1780
```
```  1781 lemma eq_card_imp_inj_on:
```
```  1782   "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
```
```  1783 apply (induct rule:finite_induct)
```
```  1784 apply simp
```
```  1785 apply(frule card_image_le[where f = f])
```
```  1786 apply(simp add:card_insert_if split:if_splits)
```
```  1787 done
```
```  1788
```
```  1789 lemma inj_on_iff_eq_card:
```
```  1790   "finite A ==> inj_on f A = (card(f ` A) = card A)"
```
```  1791 by(blast intro: card_image eq_card_imp_inj_on)
```
```  1792
```
```  1793
```
```  1794 lemma card_inj_on_le:
```
```  1795   "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
```
```  1796 apply (subgoal_tac "finite A")
```
```  1797  apply (force intro: card_mono simp add: card_image [symmetric])
```
```  1798 apply (blast intro: finite_imageD dest: finite_subset)
```
```  1799 done
```
```  1800
```
```  1801 lemma card_bij_eq:
```
```  1802   "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
```
```  1803      finite A; finite B |] ==> card A = card B"
```
```  1804 by (auto intro: le_anti_sym card_inj_on_le)
```
```  1805
```
```  1806
```
```  1807 subsubsection {* Cardinality of products *}
```
```  1808
```
```  1809 (*
```
```  1810 lemma SigmaI_insert: "y \<notin> A ==>
```
```  1811   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
```
```  1812   by auto
```
```  1813 *)
```
```  1814
```
```  1815 lemma card_SigmaI [simp]:
```
```  1816   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
```
```  1817   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
```
```  1818 by(simp add:card_def setsum_Sigma del:setsum_constant)
```
```  1819
```
```  1820 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
```
```  1821 apply (cases "finite A")
```
```  1822 apply (cases "finite B")
```
```  1823 apply (auto simp add: card_eq_0_iff
```
```  1824             dest: finite_cartesian_productD1 finite_cartesian_productD2)
```
```  1825 done
```
```  1826
```
```  1827 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
```
```  1828 by (simp add: card_cartesian_product)
```
```  1829
```
```  1830
```
```  1831 subsubsection {* Cardinality of sums *}
```
```  1832
```
```  1833 lemma card_Plus:
```
```  1834   assumes "finite A" and "finite B"
```
```  1835   shows "card (A <+> B) = card A + card B"
```
```  1836 proof -
```
```  1837   have "Inl`A \<inter> Inr`B = {}" by fast
```
```  1838   with assms show ?thesis
```
```  1839     unfolding Plus_def
```
```  1840     by (simp add: card_Un_disjoint card_image)
```
```  1841 qed
```
```  1842
```
```  1843
```
```  1844 subsubsection {* Cardinality of the Powerset *}
```
```  1845
```
```  1846 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
```
```  1847 apply (induct set: finite)
```
```  1848  apply (simp_all add: Pow_insert)
```
```  1849 apply (subst card_Un_disjoint, blast)
```
```  1850   apply (blast intro: finite_imageI, blast)
```
```  1851 apply (subgoal_tac "inj_on (insert x) (Pow F)")
```
```  1852  apply (simp add: card_image Pow_insert)
```
```  1853 apply (unfold inj_on_def)
```
```  1854 apply (blast elim!: equalityE)
```
```  1855 done
```
```  1856
```
```  1857 text {* Relates to equivalence classes.  Based on a theorem of F. Kamm�ller.  *}
```
```  1858
```
```  1859 lemma dvd_partition:
```
```  1860   "finite (Union C) ==>
```
```  1861     ALL c : C. k dvd card c ==>
```
```  1862     (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
```
```  1863   k dvd card (Union C)"
```
```  1864 apply(frule finite_UnionD)
```
```  1865 apply(rotate_tac -1)
```
```  1866 apply (induct set: finite, simp_all, clarify)
```
```  1867 apply (subst card_Un_disjoint)
```
```  1868    apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
```
```  1869 done
```
```  1870
```
```  1871
```
```  1872 subsubsection {* Relating injectivity and surjectivity *}
```
```  1873
```
```  1874 lemma finite_surj_inj: "finite(A) \<Longrightarrow> A <= f`A \<Longrightarrow> inj_on f A"
```
```  1875 apply(rule eq_card_imp_inj_on, assumption)
```
```  1876 apply(frule finite_imageI)
```
```  1877 apply(drule (1) card_seteq)
```
```  1878  apply(erule card_image_le)
```
```  1879 apply simp
```
```  1880 done
```
```  1881
```
```  1882 lemma finite_UNIV_surj_inj: fixes f :: "'a \<Rightarrow> 'a"
```
```  1883 shows "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
```
```  1884 by (blast intro: finite_surj_inj subset_UNIV dest:surj_range)
```
```  1885
```
```  1886 lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a"
```
```  1887 shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
```
```  1888 by(fastsimp simp:surj_def dest!: endo_inj_surj)
```
```  1889
```
```  1890 corollary infinite_UNIV_nat: "~finite(UNIV::nat set)"
```
```  1891 proof
```
```  1892   assume "finite(UNIV::nat set)"
```
```  1893   with finite_UNIV_inj_surj[of Suc]
```
```  1894   show False by simp (blast dest: Suc_neq_Zero surjD)
```
```  1895 qed
```
```  1896
```
```  1897
```
```  1898 subsection{* A fold functional for non-empty sets *}
```
```  1899
```
```  1900 text{* Does not require start value. *}
```
```  1901
```
```  1902 inductive
```
```  1903   fold1Set :: "('a => 'a => 'a) => 'a set => 'a => bool"
```
```  1904   for f :: "'a => 'a => 'a"
```
```  1905 where
```
```  1906   fold1Set_insertI [intro]:
```
```  1907    "\<lbrakk> fold_graph f a A x; a \<notin> A \<rbrakk> \<Longrightarrow> fold1Set f (insert a A) x"
```
```  1908
```
```  1909 constdefs
```
```  1910   fold1 :: "('a => 'a => 'a) => 'a set => 'a"
```
```  1911   "fold1 f A == THE x. fold1Set f A x"
```
```  1912
```
```  1913 lemma fold1Set_nonempty:
```
```  1914   "fold1Set f A x \<Longrightarrow> A \<noteq> {}"
```
```  1915 by(erule fold1Set.cases, simp_all)
```
```  1916
```
```  1917 inductive_cases empty_fold1SetE [elim!]: "fold1Set f {} x"
```
```  1918
```
```  1919 inductive_cases insert_fold1SetE [elim!]: "fold1Set f (insert a X) x"
```
```  1920
```
```  1921
```
```  1922 lemma fold1Set_sing [iff]: "(fold1Set f {a} b) = (a = b)"
```
```  1923 by (blast intro: fold_graph.intros elim: fold_graph.cases)
```
```  1924
```
```  1925 lemma fold1_singleton [simp]: "fold1 f {a} = a"
```
```  1926 by (unfold fold1_def) blast
```
```  1927
```
```  1928 lemma finite_nonempty_imp_fold1Set:
```
```  1929   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. fold1Set f A x"
```
```  1930 apply (induct A rule: finite_induct)
```
```  1931 apply (auto dest: finite_imp_fold_graph [of _ f])
```
```  1932 done
```
```  1933
```
```  1934 text{*First, some lemmas about @{const fold_graph}.*}
```
```  1935
```
```  1936 context ab_semigroup_mult
```
```  1937 begin
```
```  1938
```
```  1939 lemma fun_left_comm: "fun_left_comm(op *)"
```
```  1940 by unfold_locales (simp add: mult_ac)
```
```  1941
```
```  1942 lemma fold_graph_insert_swap:
```
```  1943 assumes fold: "fold_graph times (b::'a) A y" and "b \<notin> A"
```
```  1944 shows "fold_graph times z (insert b A) (z * y)"
```
```  1945 proof -
```
```  1946   interpret fun_left_comm ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"] by (rule fun_left_comm)
```
```  1947 from assms show ?thesis
```
```  1948 proof (induct rule: fold_graph.induct)
```
```  1949   case emptyI thus ?case by (force simp add: fold_insert_aux mult_commute)
```
```  1950 next
```
```  1951   case (insertI x A y)
```
```  1952     have "fold_graph times z (insert x (insert b A)) (x * (z * y))"
```
```  1953       using insertI by force  --{*how does @{term id} get unfolded?*}
```
```  1954     thus ?case by (simp add: insert_commute mult_ac)
```
```  1955 qed
```
```  1956 qed
```
```  1957
```
```  1958 lemma fold_graph_permute_diff:
```
```  1959 assumes fold: "fold_graph times b A x"
```
```  1960 shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> fold_graph times a (insert b (A-{a})) x"
```
```  1961 using fold
```
```  1962 proof (induct rule: fold_graph.induct)
```
```  1963   case emptyI thus ?case by simp
```
```  1964 next
```
```  1965   case (insertI x A y)
```
```  1966   have "a = x \<or> a \<in> A" using insertI by simp
```
```  1967   thus ?case
```
```  1968   proof
```
```  1969     assume "a = x"
```
```  1970     with insertI show ?thesis
```
```  1971       by (simp add: id_def [symmetric], blast intro: fold_graph_insert_swap)
```
```  1972   next
```
```  1973     assume ainA: "a \<in> A"
```
```  1974     hence "fold_graph times a (insert x (insert b (A - {a}))) (x * y)"
```
```  1975       using insertI by force
```
```  1976     moreover
```
```  1977     have "insert x (insert b (A - {a})) = insert b (insert x A - {a})"
```
```  1978       using ainA insertI by blast
```
```  1979     ultimately show ?thesis by simp
```
```  1980   qed
```
```  1981 qed
```
```  1982
```
```  1983 lemma fold1_eq_fold:
```
```  1984 assumes "finite A" "a \<notin> A" shows "fold1 times (insert a A) = fold times a A"
```
```  1985 proof -
```
```  1986   interpret fun_left_comm ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"] by (rule fun_left_comm)
```
```  1987   from assms show ?thesis
```
```  1988 apply (simp add: fold1_def fold_def)
```
```  1989 apply (rule the_equality)
```
```  1990 apply (best intro: fold_graph_determ theI dest: finite_imp_fold_graph [of _ times])
```
```  1991 apply (rule sym, clarify)
```
```  1992 apply (case_tac "Aa=A")
```
```  1993  apply (best intro: the_equality fold_graph_determ)
```
```  1994 apply (subgoal_tac "fold_graph times a A x")
```
```  1995  apply (best intro: the_equality fold_graph_determ)
```
```  1996 apply (subgoal_tac "insert aa (Aa - {a}) = A")
```
```  1997  prefer 2 apply (blast elim: equalityE)
```
```  1998 apply (auto dest: fold_graph_permute_diff [where a=a])
```
```  1999 done
```
```  2000 qed
```
```  2001
```
```  2002 lemma nonempty_iff: "(A \<noteq> {}) = (\<exists>x B. A = insert x B & x \<notin> B)"
```
```  2003 apply safe
```
```  2004  apply simp
```
```  2005  apply (drule_tac x=x in spec)
```
```  2006  apply (drule_tac x="A-{x}" in spec, auto)
```
```  2007 done
```
```  2008
```
```  2009 lemma fold1_insert:
```
```  2010   assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A"
```
```  2011   shows "fold1 times (insert x A) = x * fold1 times A"
```
```  2012 proof -
```
```  2013   interpret fun_left_comm ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"] by (rule fun_left_comm)
```
```  2014   from nonempty obtain a A' where "A = insert a A' & a ~: A'"
```
```  2015     by (auto simp add: nonempty_iff)
```
```  2016   with A show ?thesis
```
```  2017     by (simp add: insert_commute [of x] fold1_eq_fold eq_commute)
```
```  2018 qed
```
```  2019
```
```  2020 end
```
```  2021
```
```  2022 context ab_semigroup_idem_mult
```
```  2023 begin
```
```  2024
```
```  2025 lemma fun_left_comm_idem: "fun_left_comm_idem(op *)"
```
```  2026 apply unfold_locales
```
```  2027  apply (simp add: mult_ac)
```
```  2028 apply (simp add: mult_idem mult_assoc[symmetric])
```
```  2029 done
```
```  2030
```
```  2031
```
```  2032 lemma fold1_insert_idem [simp]:
```
```  2033   assumes nonempty: "A \<noteq> {}" and A: "finite A"
```
```  2034   shows "fold1 times (insert x A) = x * fold1 times A"
```
```  2035 proof -
```
```  2036   interpret fun_left_comm_idem ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"]
```
```  2037     by (rule fun_left_comm_idem)
```
```  2038   from nonempty obtain a A' where A': "A = insert a A' & a ~: A'"
```
```  2039     by (auto simp add: nonempty_iff)
```
```  2040   show ?thesis
```
```  2041   proof cases
```
```  2042     assume "a = x"
```
```  2043     thus ?thesis
```
```  2044     proof cases
```
```  2045       assume "A' = {}"
```
```  2046       with prems show ?thesis by (simp add: mult_idem)
```
```  2047     next
```
```  2048       assume "A' \<noteq> {}"
```
```  2049       with prems show ?thesis
```
```  2050 	by (simp add: fold1_insert mult_assoc [symmetric] mult_idem)
```
```  2051     qed
```
```  2052   next
```
```  2053     assume "a \<noteq> x"
```
```  2054     with prems show ?thesis
```
```  2055       by (simp add: insert_commute fold1_eq_fold fold_insert_idem)
```
```  2056   qed
```
```  2057 qed
```
```  2058
```
```  2059 lemma hom_fold1_commute:
```
```  2060 assumes hom: "!!x y. h (x * y) = h x * h y"
```
```  2061 and N: "finite N" "N \<noteq> {}" shows "h (fold1 times N) = fold1 times (h ` N)"
```
```  2062 using N proof (induct rule: finite_ne_induct)
```
```  2063   case singleton thus ?case by simp
```
```  2064 next
```
```  2065   case (insert n N)
```
```  2066   then have "h (fold1 times (insert n N)) = h (n * fold1 times N)" by simp
```
```  2067   also have "\<dots> = h n * h (fold1 times N)" by(rule hom)
```
```  2068   also have "h (fold1 times N) = fold1 times (h ` N)" by(rule insert)
```
```  2069   also have "times (h n) \<dots> = fold1 times (insert (h n) (h ` N))"
```
```  2070     using insert by(simp)
```
```  2071   also have "insert (h n) (h ` N) = h ` insert n N" by simp
```
```  2072   finally show ?case .
```
```  2073 qed
```
```  2074
```
```  2075 end
```
```  2076
```
```  2077
```
```  2078 text{* Now the recursion rules for definitions: *}
```
```  2079
```
```  2080 lemma fold1_singleton_def: "g = fold1 f \<Longrightarrow> g {a} = a"
```
```  2081 by(simp add:fold1_singleton)
```
```  2082
```
```  2083 lemma (in ab_semigroup_mult) fold1_insert_def:
```
```  2084   "\<lbrakk> g = fold1 times; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A"
```
```  2085 by (simp add:fold1_insert)
```
```  2086
```
```  2087 lemma (in ab_semigroup_idem_mult) fold1_insert_idem_def:
```
```  2088   "\<lbrakk> g = fold1 times; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A"
```
```  2089 by simp
```
```  2090
```
```  2091 subsubsection{* Determinacy for @{term fold1Set} *}
```
```  2092
```
```  2093 (*Not actually used!!*)
```
```  2094 (*
```
```  2095 context ab_semigroup_mult
```
```  2096 begin
```
```  2097
```
```  2098 lemma fold_graph_permute:
```
```  2099   "[|fold_graph times id b (insert a A) x; a \<notin> A; b \<notin> A|]
```
```  2100    ==> fold_graph times id a (insert b A) x"
```
```  2101 apply (cases "a=b")
```
```  2102 apply (auto dest: fold_graph_permute_diff)
```
```  2103 done
```
```  2104
```
```  2105 lemma fold1Set_determ:
```
```  2106   "fold1Set times A x ==> fold1Set times A y ==> y = x"
```
```  2107 proof (clarify elim!: fold1Set.cases)
```
```  2108   fix A x B y a b
```
```  2109   assume Ax: "fold_graph times id a A x"
```
```  2110   assume By: "fold_graph times id b B y"
```
```  2111   assume anotA:  "a \<notin> A"
```
```  2112   assume bnotB:  "b \<notin> B"
```
```  2113   assume eq: "insert a A = insert b B"
```
```  2114   show "y=x"
```
```  2115   proof cases
```
```  2116     assume same: "a=b"
```
```  2117     hence "A=B" using anotA bnotB eq by (blast elim!: equalityE)
```
```  2118     thus ?thesis using Ax By same by (blast intro: fold_graph_determ)
```
```  2119   next
```
```  2120     assume diff: "a\<noteq>b"
```
```  2121     let ?D = "B - {a}"
```
```  2122     have B: "B = insert a ?D" and A: "A = insert b ?D"
```
```  2123      and aB: "a \<in> B" and bA: "b \<in> A"
```
```  2124       using eq anotA bnotB diff by (blast elim!:equalityE)+
```
```  2125     with aB bnotB By
```
```  2126     have "fold_graph times id a (insert b ?D) y"
```
```  2127       by (auto intro: fold_graph_permute simp add: insert_absorb)
```
```  2128     moreover
```
```  2129     have "fold_graph times id a (insert b ?D) x"
```
```  2130       by (simp add: A [symmetric] Ax)
```
```  2131     ultimately show ?thesis by (blast intro: fold_graph_determ)
```
```  2132   qed
```
```  2133 qed
```
```  2134
```
```  2135 lemma fold1Set_equality: "fold1Set times A y ==> fold1 times A = y"
```
```  2136   by (unfold fold1_def) (blast intro: fold1Set_determ)
```
```  2137
```
```  2138 end
```
```  2139 *)
```
```  2140
```
```  2141 declare
```
```  2142   empty_fold_graphE [rule del]  fold_graph.intros [rule del]
```
```  2143   empty_fold1SetE [rule del]  insert_fold1SetE [rule del]
```
```  2144   -- {* No more proofs involve these relations. *}
```
```  2145
```
```  2146 subsubsection {* Lemmas about @{text fold1} *}
```
```  2147
```
```  2148 context ab_semigroup_mult
```
```  2149 begin
```
```  2150
```
```  2151 lemma fold1_Un:
```
```  2152 assumes A: "finite A" "A \<noteq> {}"
```
```  2153 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A Int B = {} \<Longrightarrow>
```
```  2154        fold1 times (A Un B) = fold1 times A * fold1 times B"
```
```  2155 using A by (induct rule: finite_ne_induct)
```
```  2156   (simp_all add: fold1_insert mult_assoc)
```
```  2157
```
```  2158 lemma fold1_in:
```
```  2159   assumes A: "finite (A)" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x,y}"
```
```  2160   shows "fold1 times A \<in> A"
```
```  2161 using A
```
```  2162 proof (induct rule:finite_ne_induct)
```
```  2163   case singleton thus ?case by simp
```
```  2164 next
```
```  2165   case insert thus ?case using elem by (force simp add:fold1_insert)
```
```  2166 qed
```
```  2167
```
```  2168 end
```
```  2169
```
```  2170 lemma (in ab_semigroup_idem_mult) fold1_Un2:
```
```  2171 assumes A: "finite A" "A \<noteq> {}"
```
```  2172 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow>
```
```  2173        fold1 times (A Un B) = fold1 times A * fold1 times B"
```
```  2174 using A
```
```  2175 proof(induct rule:finite_ne_induct)
```
```  2176   case singleton thus ?case by simp
```
```  2177 next
```
```  2178   case insert thus ?case by (simp add: mult_assoc)
```
```  2179 qed
```
```  2180
```
```  2181
```
```  2182 subsubsection {* Fold1 in lattices with @{const inf} and @{const sup} *}
```
```  2183
```
```  2184 text{*
```
```  2185   As an application of @{text fold1} we define infimum
```
```  2186   and supremum in (not necessarily complete!) lattices
```
```  2187   over (non-empty) sets by means of @{text fold1}.
```
```  2188 *}
```
```  2189
```
```  2190 context lower_semilattice
```
```  2191 begin
```
```  2192
```
```  2193 lemma ab_semigroup_idem_mult_inf:
```
```  2194   "ab_semigroup_idem_mult inf"
```
```  2195   proof qed (rule inf_assoc inf_commute inf_idem)+
```
```  2196
```
```  2197 lemma below_fold1_iff:
```
```  2198   assumes "finite A" "A \<noteq> {}"
```
```  2199   shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
```
```  2200 proof -
```
```  2201   interpret ab_semigroup_idem_mult [inf]
```
```  2202     by (rule ab_semigroup_idem_mult_inf)
```
```  2203   show ?thesis using assms by (induct rule: finite_ne_induct) simp_all
```
```  2204 qed
```
```  2205
```
```  2206 lemma fold1_belowI:
```
```  2207   assumes "finite A"
```
```  2208     and "a \<in> A"
```
```  2209   shows "fold1 inf A \<le> a"
```
```  2210 proof -
```
```  2211   from assms have "A \<noteq> {}" by auto
```
```  2212   from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
```
```  2213   proof (induct rule: finite_ne_induct)
```
```  2214     case singleton thus ?case by simp
```
```  2215   next
```
```  2216     interpret ab_semigroup_idem_mult [inf]
```
```  2217       by (rule ab_semigroup_idem_mult_inf)
```
```  2218     case (insert x F)
```
```  2219     from insert(5) have "a = x \<or> a \<in> F" by simp
```
```  2220     thus ?case
```
```  2221     proof
```
```  2222       assume "a = x" thus ?thesis using insert
```
```  2223         by (simp add: mult_ac_idem)
```
```  2224     next
```
```  2225       assume "a \<in> F"
```
```  2226       hence bel: "fold1 inf F \<le> a" by (rule insert)
```
```  2227       have "inf (fold1 inf (insert x F)) a = inf x (inf (fold1 inf F) a)"
```
```  2228         using insert by (simp add: mult_ac_idem)
```
```  2229       also have "inf (fold1 inf F) a = fold1 inf F"
```
```  2230         using bel by (auto intro: antisym)
```
```  2231       also have "inf x \<dots> = fold1 inf (insert x F)"
```
```  2232         using insert by (simp add: mult_ac_idem)
```
```  2233       finally have aux: "inf (fold1 inf (insert x F)) a = fold1 inf (insert x F)" .
```
```  2234       moreover have "inf (fold1 inf (insert x F)) a \<le> a" by simp
```
```  2235       ultimately show ?thesis by simp
```
```  2236     qed
```
```  2237   qed
```
```  2238 qed
```
```  2239
```
```  2240 end
```
```  2241
```
```  2242 lemma (in upper_semilattice) ab_semigroup_idem_mult_sup:
```
```  2243   "ab_semigroup_idem_mult sup"
```
```  2244   by (rule lower_semilattice.ab_semigroup_idem_mult_inf)
```
```  2245     (rule dual_lattice)
```
```  2246
```
```  2247 context lattice
```
```  2248 begin
```
```  2249
```
```  2250 definition
```
```  2251   Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_"  900)
```
```  2252 where
```
```  2253   "Inf_fin = fold1 inf"
```
```  2254
```
```  2255 definition
```
```  2256   Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_"  900)
```
```  2257 where
```
```  2258   "Sup_fin = fold1 sup"
```
```  2259
```
```  2260 lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A"
```
```  2261 apply(unfold Sup_fin_def Inf_fin_def)
```
```  2262 apply(subgoal_tac "EX a. a:A")
```
```  2263 prefer 2 apply blast
```
```  2264 apply(erule exE)
```
```  2265 apply(rule order_trans)
```
```  2266 apply(erule (1) fold1_belowI)
```
```  2267 apply(erule (1) lower_semilattice.fold1_belowI [OF dual_lattice])
```
```  2268 done
```
```  2269
```
```  2270 lemma sup_Inf_absorb [simp]:
```
```  2271   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^bsub>fin\<^esub>A) = a"
```
```  2272 apply(subst sup_commute)
```
```  2273 apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI)
```
```  2274 done
```
```  2275
```
```  2276 lemma inf_Sup_absorb [simp]:
```
```  2277   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a"
```
```  2278 by (simp add: Sup_fin_def inf_absorb1
```
```  2279   lower_semilattice.fold1_belowI [OF dual_lattice])
```
```  2280
```
```  2281 end
```
```  2282
```
```  2283 context distrib_lattice
```
```  2284 begin
```
```  2285
```
```  2286 lemma sup_Inf1_distrib:
```
```  2287   assumes "finite A"
```
```  2288     and "A \<noteq> {}"
```
```  2289   shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
```
```  2290 proof -
```
```  2291   interpret ab_semigroup_idem_mult [inf]
```
```  2292     by (rule ab_semigroup_idem_mult_inf)
```
```  2293   from assms show ?thesis
```
```  2294     by (simp add: Inf_fin_def image_def
```
```  2295       hom_fold1_commute [where h="sup x", OF sup_inf_distrib1])
```
```  2296         (rule arg_cong [where f="fold1 inf"], blast)
```
```  2297 qed
```
```  2298
```
```  2299 lemma sup_Inf2_distrib:
```
```  2300   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
```
```  2301   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}"
```
```  2302 using A proof (induct rule: finite_ne_induct)
```
```  2303   case singleton thus ?case
```
```  2304     by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
```
```  2305 next
```
```  2306   interpret ab_semigroup_idem_mult [inf]
```
```  2307     by (rule ab_semigroup_idem_mult_inf)
```
```  2308   case (insert x A)
```
```  2309   have finB: "finite {sup x b |b. b \<in> B}"
```
```  2310     by(rule finite_surj[where f = "sup x", OF B(1)], auto)
```
```  2311   have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
```
```  2312   proof -
```
```  2313     have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
```
```  2314       by blast
```
```  2315     thus ?thesis by(simp add: insert(1) B(1))
```
```  2316   qed
```
```  2317   have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
```
```  2318   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)"
```
```  2319     using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def])
```
```  2320   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)
```
```  2321   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})"
```
```  2322     using insert by(simp add:sup_Inf1_distrib[OF B])
```
```  2323   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})"
```
```  2324     (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M")
```
```  2325     using B insert
```
```  2326     by (simp add: Inf_fin_def fold1_Un2 [OF finB _ finAB ne])
```
```  2327   also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
```
```  2328     by blast
```
```  2329   finally show ?case .
```
```  2330 qed
```
```  2331
```
```  2332 lemma inf_Sup1_distrib:
```
```  2333   assumes "finite A" and "A \<noteq> {}"
```
```  2334   shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
```
```  2335 proof -
```
```  2336   interpret ab_semigroup_idem_mult [sup]
```
```  2337     by (rule ab_semigroup_idem_mult_sup)
```
```  2338   from assms show ?thesis
```
```  2339     by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1])
```
```  2340       (rule arg_cong [where f="fold1 sup"], blast)
```
```  2341 qed
```
```  2342
```
```  2343 lemma inf_Sup2_distrib:
```
```  2344   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
```
```  2345   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}"
```
```  2346 using A proof (induct rule: finite_ne_induct)
```
```  2347   case singleton thus ?case
```
```  2348     by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def])
```
```  2349 next
```
```  2350   case (insert x A)
```
```  2351   have finB: "finite {inf x b |b. b \<in> B}"
```
```  2352     by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
```
```  2353   have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
```
```  2354   proof -
```
```  2355     have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
```
```  2356       by blast
```
```  2357     thus ?thesis by(simp add: insert(1) B(1))
```
```  2358   qed
```
```  2359   have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
```
```  2360   interpret ab_semigroup_idem_mult [sup]
```
```  2361     by (rule ab_semigroup_idem_mult_sup)
```
```  2362   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)"
```
```  2363     using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
```
```  2364   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)
```
```  2365   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})"
```
```  2366     using insert by(simp add:inf_Sup1_distrib[OF B])
```
```  2367   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})"
```
```  2368     (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M")
```
```  2369     using B insert
```
```  2370     by (simp add: Sup_fin_def fold1_Un2 [OF finB _ finAB ne])
```
```  2371   also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
```
```  2372     by blast
```
```  2373   finally show ?case .
```
```  2374 qed
```
```  2375
```
```  2376 end
```
```  2377
```
```  2378 context complete_lattice
```
```  2379 begin
```
```  2380
```
```  2381 text {*
```
```  2382   Coincidence on finite sets in complete lattices:
```
```  2383 *}
```
```  2384
```
```  2385 lemma Inf_fin_Inf:
```
```  2386   assumes "finite A" and "A \<noteq> {}"
```
```  2387   shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
```
```  2388 proof -
```
```  2389   interpret ab_semigroup_idem_mult [inf]
```
```  2390     by (rule ab_semigroup_idem_mult_inf)
```
```  2391   from assms show ?thesis
```
```  2392   unfolding Inf_fin_def by (induct A set: finite)
```
```  2393     (simp_all add: Inf_insert_simp)
```
```  2394 qed
```
```  2395
```
```  2396 lemma Sup_fin_Sup:
```
```  2397   assumes "finite A" and "A \<noteq> {}"
```
```  2398   shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
```
```  2399 proof -
```
```  2400   interpret ab_semigroup_idem_mult [sup]
```
```  2401     by (rule ab_semigroup_idem_mult_sup)
```
```  2402   from assms show ?thesis
```
```  2403   unfolding Sup_fin_def by (induct A set: finite)
```
```  2404     (simp_all add: Sup_insert_simp)
```
```  2405 qed
```
```  2406
```
```  2407 end
```
```  2408
```
```  2409
```
```  2410 subsubsection {* Fold1 in linear orders with @{const min} and @{const max} *}
```
```  2411
```
```  2412 text{*
```
```  2413   As an application of @{text fold1} we define minimum
```
```  2414   and maximum in (not necessarily complete!) linear orders
```
```  2415   over (non-empty) sets by means of @{text fold1}.
```
```  2416 *}
```
```  2417
```
```  2418 context linorder
```
```  2419 begin
```
```  2420
```
```  2421 lemma ab_semigroup_idem_mult_min:
```
```  2422   "ab_semigroup_idem_mult min"
```
```  2423   proof qed (auto simp add: min_def)
```
```  2424
```
```  2425 lemma ab_semigroup_idem_mult_max:
```
```  2426   "ab_semigroup_idem_mult max"
```
```  2427   proof qed (auto simp add: max_def)
```
```  2428
```
```  2429 lemma min_lattice:
```
```  2430   "lower_semilattice (op \<le>) (op <) min"
```
```  2431   proof qed (auto simp add: min_def)
```
```  2432
```
```  2433 lemma max_lattice:
```
```  2434   "lower_semilattice (op \<ge>) (op >) max"
```
```  2435   proof qed (auto simp add: max_def)
```
```  2436
```
```  2437 lemma dual_max:
```
```  2438   "ord.max (op \<ge>) = min"
```
```  2439   by (auto simp add: ord.max_def_raw min_def_raw expand_fun_eq)
```
```  2440
```
```  2441 lemma dual_min:
```
```  2442   "ord.min (op \<ge>) = max"
```
```  2443   by (auto simp add: ord.min_def_raw max_def_raw expand_fun_eq)
```
```  2444
```
```  2445 lemma strict_below_fold1_iff:
```
```  2446   assumes "finite A" and "A \<noteq> {}"
```
```  2447   shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
```
```  2448 proof -
```
```  2449   interpret ab_semigroup_idem_mult [min]
```
```  2450     by (rule ab_semigroup_idem_mult_min)
```
```  2451   from assms show ?thesis
```
```  2452   by (induct rule: finite_ne_induct)
```
```  2453     (simp_all add: fold1_insert)
```
```  2454 qed
```
```  2455
```
```  2456 lemma fold1_below_iff:
```
```  2457   assumes "finite A" and "A \<noteq> {}"
```
```  2458   shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
```
```  2459 proof -
```
```  2460   interpret ab_semigroup_idem_mult [min]
```
```  2461     by (rule ab_semigroup_idem_mult_min)
```
```  2462   from assms show ?thesis
```
```  2463   by (induct rule: finite_ne_induct)
```
```  2464     (simp_all add: fold1_insert min_le_iff_disj)
```
```  2465 qed
```
```  2466
```
```  2467 lemma fold1_strict_below_iff:
```
```  2468   assumes "finite A" and "A \<noteq> {}"
```
```  2469   shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
```
```  2470 proof -
```
```  2471   interpret ab_semigroup_idem_mult [min]
```
```  2472     by (rule ab_semigroup_idem_mult_min)
```
```  2473   from assms show ?thesis
```
```  2474   by (induct rule: finite_ne_induct)
```
```  2475     (simp_all add: fold1_insert min_less_iff_disj)
```
```  2476 qed
```
```  2477
```
```  2478 lemma fold1_antimono:
```
```  2479   assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
```
```  2480   shows "fold1 min B \<le> fold1 min A"
```
```  2481 proof cases
```
```  2482   assume "A = B" thus ?thesis by simp
```
```  2483 next
```
```  2484   interpret ab_semigroup_idem_mult [min]
```
```  2485     by (rule ab_semigroup_idem_mult_min)
```
```  2486   assume "A \<noteq> B"
```
```  2487   have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
```
```  2488   have "fold1 min B = fold1 min (A \<union> (B-A))" by(subst B)(rule refl)
```
```  2489   also have "\<dots> = min (fold1 min A) (fold1 min (B-A))"
```
```  2490   proof -
```
```  2491     have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
```
```  2492     moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`]) (* by(blast intro:finite_Diff prems) fails *)
```
```  2493     moreover have "(B-A) \<noteq> {}" using prems by blast
```
```  2494     moreover have "A Int (B-A) = {}" using prems by blast
```
```  2495     ultimately show ?thesis using `A \<noteq> {}` by (rule_tac fold1_Un)
```
```  2496   qed
```
```  2497   also have "\<dots> \<le> fold1 min A" by (simp add: min_le_iff_disj)
```
```  2498   finally show ?thesis .
```
```  2499 qed
```
```  2500
```
```  2501 definition
```
```  2502   Min :: "'a set \<Rightarrow> 'a"
```
```  2503 where
```
```  2504   "Min = fold1 min"
```
```  2505
```
```  2506 definition
```
```  2507   Max :: "'a set \<Rightarrow> 'a"
```
```  2508 where
```
```  2509   "Max = fold1 max"
```
```  2510
```
```  2511 lemmas Min_singleton [simp] = fold1_singleton_def [OF Min_def]
```
```  2512 lemmas Max_singleton [simp] = fold1_singleton_def [OF Max_def]
```
```  2513
```
```  2514 lemma Min_insert [simp]:
```
```  2515   assumes "finite A" and "A \<noteq> {}"
```
```  2516   shows "Min (insert x A) = min x (Min A)"
```
```  2517 proof -
```
```  2518   interpret ab_semigroup_idem_mult [min]
```
```  2519     by (rule ab_semigroup_idem_mult_min)
```
```  2520   from assms show ?thesis by (rule fold1_insert_idem_def [OF Min_def])
```
```  2521 qed
```
```  2522
```
```  2523 lemma Max_insert [simp]:
```
```  2524   assumes "finite A" and "A \<noteq> {}"
```
```  2525   shows "Max (insert x A) = max x (Max A)"
```
```  2526 proof -
```
```  2527   interpret ab_semigroup_idem_mult [max]
```
```  2528     by (rule ab_semigroup_idem_mult_max)
```
```  2529   from assms show ?thesis by (rule fold1_insert_idem_def [OF Max_def])
```
```  2530 qed
```
```  2531
```
```  2532 lemma Min_in [simp]:
```
```  2533   assumes "finite A" and "A \<noteq> {}"
```
```  2534   shows "Min A \<in> A"
```
```  2535 proof -
```
```  2536   interpret ab_semigroup_idem_mult [min]
```
```  2537     by (rule ab_semigroup_idem_mult_min)
```
```  2538   from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def)
```
```  2539 qed
```
```  2540
```
```  2541 lemma Max_in [simp]:
```
```  2542   assumes "finite A" and "A \<noteq> {}"
```
```  2543   shows "Max A \<in> A"
```
```  2544 proof -
```
```  2545   interpret ab_semigroup_idem_mult [max]
```
```  2546     by (rule ab_semigroup_idem_mult_max)
```
```  2547   from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
```
```  2548 qed
```
```  2549
```
```  2550 lemma Min_Un:
```
```  2551   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
```
```  2552   shows "Min (A \<union> B) = min (Min A) (Min B)"
```
```  2553 proof -
```
```  2554   interpret ab_semigroup_idem_mult [min]
```
```  2555     by (rule ab_semigroup_idem_mult_min)
```
```  2556   from assms show ?thesis
```
```  2557     by (simp add: Min_def fold1_Un2)
```
```  2558 qed
```
```  2559
```
```  2560 lemma Max_Un:
```
```  2561   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
```
```  2562   shows "Max (A \<union> B) = max (Max A) (Max B)"
```
```  2563 proof -
```
```  2564   interpret ab_semigroup_idem_mult [max]
```
```  2565     by (rule ab_semigroup_idem_mult_max)
```
```  2566   from assms show ?thesis
```
```  2567     by (simp add: Max_def fold1_Un2)
```
```  2568 qed
```
```  2569
```
```  2570 lemma hom_Min_commute:
```
```  2571   assumes "\<And>x y. h (min x y) = min (h x) (h y)"
```
```  2572     and "finite N" and "N \<noteq> {}"
```
```  2573   shows "h (Min N) = Min (h ` N)"
```
```  2574 proof -
```
```  2575   interpret ab_semigroup_idem_mult [min]
```
```  2576     by (rule ab_semigroup_idem_mult_min)
```
```  2577   from assms show ?thesis
```
```  2578     by (simp add: Min_def hom_fold1_commute)
```
```  2579 qed
```
```  2580
```
```  2581 lemma hom_Max_commute:
```
```  2582   assumes "\<And>x y. h (max x y) = max (h x) (h y)"
```
```  2583     and "finite N" and "N \<noteq> {}"
```
```  2584   shows "h (Max N) = Max (h ` N)"
```
```  2585 proof -
```
```  2586   interpret ab_semigroup_idem_mult [max]
```
```  2587     by (rule ab_semigroup_idem_mult_max)
```
```  2588   from assms show ?thesis
```
```  2589     by (simp add: Max_def hom_fold1_commute [of h])
```
```  2590 qed
```
```  2591
```
```  2592 lemma Min_le [simp]:
```
```  2593   assumes "finite A" and "x \<in> A"
```
```  2594   shows "Min A \<le> x"
```
```  2595 proof -
```
```  2596   interpret lower_semilattice ["op \<le>" "op <" min]
```
```  2597     by (rule min_lattice)
```
```  2598   from assms show ?thesis by (simp add: Min_def fold1_belowI)
```
```  2599 qed
```
```  2600
```
```  2601 lemma Max_ge [simp]:
```
```  2602   assumes "finite A" and "x \<in> A"
```
```  2603   shows "x \<le> Max A"
```
```  2604 proof -
```
```  2605   invoke lower_semilattice ["op \<ge>" "op >" max]
```
```  2606     by (rule max_lattice)
```
```  2607   from assms show ?thesis by (simp add: Max_def fold1_belowI)
```
```  2608 qed
```
```  2609
```
```  2610 lemma Min_ge_iff [simp, noatp]:
```
```  2611   assumes "finite A" and "A \<noteq> {}"
```
```  2612   shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
```
```  2613 proof -
```
```  2614   interpret lower_semilattice ["op \<le>" "op <" min]
```
```  2615     by (rule min_lattice)
```
```  2616   from assms show ?thesis by (simp add: Min_def below_fold1_iff)
```
```  2617 qed
```
```  2618
```
```  2619 lemma Max_le_iff [simp, noatp]:
```
```  2620   assumes "finite A" and "A \<noteq> {}"
```
```  2621   shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
```
```  2622 proof -
```
```  2623   invoke lower_semilattice ["op \<ge>" "op >" max]
```
```  2624     by (rule max_lattice)
```
```  2625   from assms show ?thesis by (simp add: Max_def below_fold1_iff)
```
```  2626 qed
```
```  2627
```
```  2628 lemma Min_gr_iff [simp, noatp]:
```
```  2629   assumes "finite A" and "A \<noteq> {}"
```
```  2630   shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
```
```  2631 proof -
```
```  2632   interpret lower_semilattice ["op \<le>" "op <" min]
```
```  2633     by (rule min_lattice)
```
```  2634   from assms show ?thesis by (simp add: Min_def strict_below_fold1_iff)
```
```  2635 qed
```
```  2636
```
```  2637 lemma Max_less_iff [simp, noatp]:
```
```  2638   assumes "finite A" and "A \<noteq> {}"
```
```  2639   shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
```
```  2640 proof -
```
```  2641   note Max = Max_def
```
```  2642   interpret linorder ["op \<ge>" "op >"]
```
```  2643     by (rule dual_linorder)
```
```  2644   from assms show ?thesis
```
```  2645     by (simp add: Max strict_below_fold1_iff [folded dual_max])
```
```  2646 qed
```
```  2647
```
```  2648 lemma Min_le_iff [noatp]:
```
```  2649   assumes "finite A" and "A \<noteq> {}"
```
```  2650   shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
```
```  2651 proof -
```
```  2652   interpret lower_semilattice ["op \<le>" "op <" min]
```
```  2653     by (rule min_lattice)
```
```  2654   from assms show ?thesis
```
```  2655     by (simp add: Min_def fold1_below_iff)
```
```  2656 qed
```
```  2657
```
```  2658 lemma Max_ge_iff [noatp]:
```
```  2659   assumes "finite A" and "A \<noteq> {}"
```
```  2660   shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
```
```  2661 proof -
```
```  2662   note Max = Max_def
```
```  2663   interpret linorder ["op \<ge>" "op >"]
```
```  2664     by (rule dual_linorder)
```
```  2665   from assms show ?thesis
```
```  2666     by (simp add: Max fold1_below_iff [folded dual_max])
```
```  2667 qed
```
```  2668
```
```  2669 lemma Min_less_iff [noatp]:
```
```  2670   assumes "finite A" and "A \<noteq> {}"
```
```  2671   shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
```
```  2672 proof -
```
```  2673   interpret lower_semilattice ["op \<le>" "op <" min]
```
```  2674     by (rule min_lattice)
```
```  2675   from assms show ?thesis
```
```  2676     by (simp add: Min_def fold1_strict_below_iff)
```
```  2677 qed
```
```  2678
```
```  2679 lemma Max_gr_iff [noatp]:
```
```  2680   assumes "finite A" and "A \<noteq> {}"
```
```  2681   shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
```
```  2682 proof -
```
```  2683   note Max = Max_def
```
```  2684   interpret linorder ["op \<ge>" "op >"]
```
```  2685     by (rule dual_linorder)
```
```  2686   from assms show ?thesis
```
```  2687     by (simp add: Max fold1_strict_below_iff [folded dual_max])
```
```  2688 qed
```
```  2689
```
```  2690 lemma Min_antimono:
```
```  2691   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
```
```  2692   shows "Min N \<le> Min M"
```
```  2693 proof -
```
```  2694   interpret distrib_lattice ["op \<le>" "op <" min max]
```
```  2695     by (rule distrib_lattice_min_max)
```
```  2696   from assms show ?thesis by (simp add: Min_def fold1_antimono)
```
```  2697 qed
```
```  2698
```
```  2699 lemma Max_mono:
```
```  2700   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
```
```  2701   shows "Max M \<le> Max N"
```
```  2702 proof -
```
```  2703   note Max = Max_def
```
```  2704   interpret linorder ["op \<ge>" "op >"]
```
```  2705     by (rule dual_linorder)
```
```  2706   from assms show ?thesis
```
```  2707     by (simp add: Max fold1_antimono [folded dual_max])
```
```  2708 qed
```
```  2709
```
```  2710 lemma finite_linorder_induct[consumes 1, case_names empty insert]:
```
```  2711  "finite A \<Longrightarrow> P {} \<Longrightarrow>
```
```  2712   (!!A b. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
```
```  2713   \<Longrightarrow> P A"
```
```  2714 proof (induct A rule: measure_induct_rule[where f=card])
```
```  2715   fix A :: "'a set"
```
```  2716   assume IH: "!! B. card B < card A \<Longrightarrow> finite B \<Longrightarrow> P {} \<Longrightarrow>
```
```  2717                  (!!A b. finite A \<Longrightarrow> (\<forall>a\<in>A. a<b) \<Longrightarrow> P A \<Longrightarrow> P (insert b A))
```
```  2718                   \<Longrightarrow> P B"
```
```  2719   and "finite A" and "P {}"
```
```  2720   and step: "!!A b. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
```
```  2721   show "P A"
```
```  2722   proof (cases "A = {}")
```
```  2723     assume "A = {}" thus "P A" using `P {}` by simp
```
```  2724   next
```
```  2725     let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B"
```
```  2726     assume "A \<noteq> {}"
```
```  2727     with `finite A` have "Max A : A" by auto
```
```  2728     hence A: "?A = A" using insert_Diff_single insert_absorb by auto
```
```  2729     note card_Diff1_less[OF `finite A` `Max A : A`]
```
```  2730     moreover have "finite ?B" using `finite A` by simp
```
```  2731     ultimately have "P ?B" using `P {}` step IH by blast
```
```  2732     moreover have "\<forall>a\<in>?B. a < Max A"
```
```  2733       using Max_ge [OF `finite A`] by fastsimp
```
```  2734     ultimately show "P A"
```
```  2735       using A insert_Diff_single step[OF `finite ?B`] by fastsimp
```
```  2736   qed
```
```  2737 qed
```
```  2738
```
```  2739 end
```
```  2740
```
```  2741 context ordered_ab_semigroup_add
```
```  2742 begin
```
```  2743
```
```  2744 lemma add_Min_commute:
```
```  2745   fixes k
```
```  2746   assumes "finite N" and "N \<noteq> {}"
```
```  2747   shows "k + Min N = Min {k + m | m. m \<in> N}"
```
```  2748 proof -
```
```  2749   have "\<And>x y. k + min x y = min (k + x) (k + y)"
```
```  2750     by (simp add: min_def not_le)
```
```  2751       (blast intro: antisym less_imp_le add_left_mono)
```
```  2752   with assms show ?thesis
```
```  2753     using hom_Min_commute [of "plus k" N]
```
```  2754     by simp (blast intro: arg_cong [where f = Min])
```
```  2755 qed
```
```  2756
```
```  2757 lemma add_Max_commute:
```
```  2758   fixes k
```
```  2759   assumes "finite N" and "N \<noteq> {}"
```
```  2760   shows "k + Max N = Max {k + m | m. m \<in> N}"
```
```  2761 proof -
```
```  2762   have "\<And>x y. k + max x y = max (k + x) (k + y)"
```
```  2763     by (simp add: max_def not_le)
```
```  2764       (blast intro: antisym less_imp_le add_left_mono)
```
```  2765   with assms show ?thesis
```
```  2766     using hom_Max_commute [of "plus k" N]
```
```  2767     by simp (blast intro: arg_cong [where f = Max])
```
```  2768 qed
```
```  2769
```
```  2770 end
```
```  2771
```
```  2772 end
```