src/HOL/Finite_Set.thy
 author nipkow Fri Aug 28 18:52:41 2009 +0200 (2009-08-28) changeset 32436 10cd49e0c067 parent 32203 992ac8942691 child 32437 66f1a0dfe7d9 permissions -rw-r--r--
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
```     1 (*  Title:      HOL/Finite_Set.thy
```
```     2     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
```
```     3                 with contributions by Jeremy Avigad
```
```     4 *)
```
```     5
```
```     6 header {* Finite sets *}
```
```     7
```
```     8 theory Finite_Set
```
```     9 imports Nat Product_Type Power
```
```    10 begin
```
```    11
```
```    12 subsection {* Definition and basic properties *}
```
```    13
```
```    14 inductive finite :: "'a set => bool"
```
```    15   where
```
```    16     emptyI [simp, intro!]: "finite {}"
```
```    17   | insertI [simp, intro!]: "finite A ==> finite (insert a A)"
```
```    18
```
```    19 lemma ex_new_if_finite: -- "does not depend on def of finite at all"
```
```    20   assumes "\<not> finite (UNIV :: 'a set)" and "finite A"
```
```    21   shows "\<exists>a::'a. a \<notin> A"
```
```    22 proof -
```
```    23   from assms have "A \<noteq> UNIV" by blast
```
```    24   thus ?thesis by blast
```
```    25 qed
```
```    26
```
```    27 lemma finite_induct [case_names empty insert, induct set: finite]:
```
```    28   "finite F ==>
```
```    29     P {} ==> (!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F"
```
```    30   -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
```
```    31 proof -
```
```    32   assume "P {}" and
```
```    33     insert: "!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)"
```
```    34   assume "finite F"
```
```    35   thus "P F"
```
```    36   proof induct
```
```    37     show "P {}" by fact
```
```    38     fix x F assume F: "finite F" and P: "P F"
```
```    39     show "P (insert x F)"
```
```    40     proof cases
```
```    41       assume "x \<in> F"
```
```    42       hence "insert x F = F" by (rule insert_absorb)
```
```    43       with P show ?thesis by (simp only:)
```
```    44     next
```
```    45       assume "x \<notin> F"
```
```    46       from F this P show ?thesis by (rule insert)
```
```    47     qed
```
```    48   qed
```
```    49 qed
```
```    50
```
```    51 lemma finite_ne_induct[case_names singleton insert, consumes 2]:
```
```    52 assumes fin: "finite F" shows "F \<noteq> {} \<Longrightarrow>
```
```    53  \<lbrakk> \<And>x. P{x};
```
```    54    \<And>x F. \<lbrakk> finite F; F \<noteq> {}; x \<notin> F; P F \<rbrakk> \<Longrightarrow> P (insert x F) \<rbrakk>
```
```    55  \<Longrightarrow> P F"
```
```    56 using fin
```
```    57 proof induct
```
```    58   case empty thus ?case by simp
```
```    59 next
```
```    60   case (insert x F)
```
```    61   show ?case
```
```    62   proof cases
```
```    63     assume "F = {}"
```
```    64     thus ?thesis using `P {x}` by simp
```
```    65   next
```
```    66     assume "F \<noteq> {}"
```
```    67     thus ?thesis using insert by blast
```
```    68   qed
```
```    69 qed
```
```    70
```
```    71 lemma finite_subset_induct [consumes 2, case_names empty insert]:
```
```    72   assumes "finite F" and "F \<subseteq> A"
```
```    73     and empty: "P {}"
```
```    74     and insert: "!!a F. finite F ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
```
```    75   shows "P F"
```
```    76 proof -
```
```    77   from `finite F` and `F \<subseteq> A`
```
```    78   show ?thesis
```
```    79   proof induct
```
```    80     show "P {}" by fact
```
```    81   next
```
```    82     fix x F
```
```    83     assume "finite F" and "x \<notin> F" and
```
```    84       P: "F \<subseteq> A ==> P F" and i: "insert x F \<subseteq> A"
```
```    85     show "P (insert x F)"
```
```    86     proof (rule insert)
```
```    87       from i show "x \<in> A" by blast
```
```    88       from i have "F \<subseteq> A" by blast
```
```    89       with P show "P F" .
```
```    90       show "finite F" by fact
```
```    91       show "x \<notin> F" by fact
```
```    92     qed
```
```    93   qed
```
```    94 qed
```
```    95
```
```    96
```
```    97 text{* A finite choice principle. Does not need the SOME choice operator. *}
```
```    98 lemma finite_set_choice:
```
```    99   "finite A \<Longrightarrow> ALL x:A. (EX y. P x y) \<Longrightarrow> EX f. ALL x:A. P x (f x)"
```
```   100 proof (induct set: finite)
```
```   101   case empty thus ?case by simp
```
```   102 next
```
```   103   case (insert a A)
```
```   104   then obtain f b where f: "ALL x:A. P x (f x)" and ab: "P a b" by auto
```
```   105   show ?case (is "EX f. ?P f")
```
```   106   proof
```
```   107     show "?P(%x. if x = a then b else f x)" using f ab by auto
```
```   108   qed
```
```   109 qed
```
```   110
```
```   111
```
```   112 text{* Finite sets are the images of initial segments of natural numbers: *}
```
```   113
```
```   114 lemma finite_imp_nat_seg_image_inj_on:
```
```   115   assumes fin: "finite A"
```
```   116   shows "\<exists> (n::nat) f. A = f ` {i. i<n} & inj_on f {i. i<n}"
```
```   117 using fin
```
```   118 proof induct
```
```   119   case empty
```
```   120   show ?case
```
```   121   proof show "\<exists>f. {} = f ` {i::nat. i < 0} & inj_on f {i. i<0}" by simp
```
```   122   qed
```
```   123 next
```
```   124   case (insert a A)
```
```   125   have notinA: "a \<notin> A" by fact
```
```   126   from insert.hyps obtain n f
```
```   127     where "A = f ` {i::nat. i < n}" "inj_on f {i. i < n}" by blast
```
```   128   hence "insert a A = f(n:=a) ` {i. i < Suc n}"
```
```   129         "inj_on (f(n:=a)) {i. i < Suc n}" using notinA
```
```   130     by (auto simp add: image_def Ball_def inj_on_def less_Suc_eq)
```
```   131   thus ?case by blast
```
```   132 qed
```
```   133
```
```   134 lemma nat_seg_image_imp_finite:
```
```   135   "!!f A. A = f ` {i::nat. i<n} \<Longrightarrow> finite A"
```
```   136 proof (induct n)
```
```   137   case 0 thus ?case by simp
```
```   138 next
```
```   139   case (Suc n)
```
```   140   let ?B = "f ` {i. i < n}"
```
```   141   have finB: "finite ?B" by(rule Suc.hyps[OF refl])
```
```   142   show ?case
```
```   143   proof cases
```
```   144     assume "\<exists>k<n. f n = f k"
```
```   145     hence "A = ?B" using Suc.prems by(auto simp:less_Suc_eq)
```
```   146     thus ?thesis using finB by simp
```
```   147   next
```
```   148     assume "\<not>(\<exists> k<n. f n = f k)"
```
```   149     hence "A = insert (f n) ?B" using Suc.prems by(auto simp:less_Suc_eq)
```
```   150     thus ?thesis using finB by simp
```
```   151   qed
```
```   152 qed
```
```   153
```
```   154 lemma finite_conv_nat_seg_image:
```
```   155   "finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})"
```
```   156 by(blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on)
```
```   157
```
```   158 lemma finite_Collect_less_nat[iff]: "finite{n::nat. n<k}"
```
```   159 by(fastsimp simp: finite_conv_nat_seg_image)
```
```   160
```
```   161
```
```   162 subsubsection{* Finiteness and set theoretic constructions *}
```
```   163
```
```   164 lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)"
```
```   165 by (induct set: finite) simp_all
```
```   166
```
```   167 lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A"
```
```   168   -- {* Every subset of a finite set is finite. *}
```
```   169 proof -
```
```   170   assume "finite B"
```
```   171   thus "!!A. A \<subseteq> B ==> finite A"
```
```   172   proof induct
```
```   173     case empty
```
```   174     thus ?case by simp
```
```   175   next
```
```   176     case (insert x F A)
```
```   177     have A: "A \<subseteq> insert x F" and r: "A - {x} \<subseteq> F ==> finite (A - {x})" by fact+
```
```   178     show "finite A"
```
```   179     proof cases
```
```   180       assume x: "x \<in> A"
```
```   181       with A have "A - {x} \<subseteq> F" by (simp add: subset_insert_iff)
```
```   182       with r have "finite (A - {x})" .
```
```   183       hence "finite (insert x (A - {x}))" ..
```
```   184       also have "insert x (A - {x}) = A" using x by (rule insert_Diff)
```
```   185       finally show ?thesis .
```
```   186     next
```
```   187       show "A \<subseteq> F ==> ?thesis" by fact
```
```   188       assume "x \<notin> A"
```
```   189       with A show "A \<subseteq> F" by (simp add: subset_insert_iff)
```
```   190     qed
```
```   191   qed
```
```   192 qed
```
```   193
```
```   194 lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
```
```   195 by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
```
```   196
```
```   197 lemma finite_Collect_disjI[simp]:
```
```   198   "finite{x. P x | Q x} = (finite{x. P x} & finite{x. Q x})"
```
```   199 by(simp add:Collect_disj_eq)
```
```   200
```
```   201 lemma finite_Int [simp, intro]: "finite F | finite G ==> finite (F Int G)"
```
```   202   -- {* The converse obviously fails. *}
```
```   203 by (blast intro: finite_subset)
```
```   204
```
```   205 lemma finite_Collect_conjI [simp, intro]:
```
```   206   "finite{x. P x} | finite{x. Q x} ==> finite{x. P x & Q x}"
```
```   207   -- {* The converse obviously fails. *}
```
```   208 by(simp add:Collect_conj_eq)
```
```   209
```
```   210 lemma finite_Collect_le_nat[iff]: "finite{n::nat. n<=k}"
```
```   211 by(simp add: le_eq_less_or_eq)
```
```   212
```
```   213 lemma finite_insert [simp]: "finite (insert a A) = finite A"
```
```   214   apply (subst insert_is_Un)
```
```   215   apply (simp only: finite_Un, blast)
```
```   216   done
```
```   217
```
```   218 lemma finite_Union[simp, intro]:
```
```   219  "\<lbrakk> finite A; !!M. M \<in> A \<Longrightarrow> finite M \<rbrakk> \<Longrightarrow> finite(\<Union>A)"
```
```   220 by (induct rule:finite_induct) simp_all
```
```   221
```
```   222 lemma finite_Inter[intro]: "EX A:M. finite(A) \<Longrightarrow> finite(Inter M)"
```
```   223 by (blast intro: Inter_lower finite_subset)
```
```   224
```
```   225 lemma finite_INT[intro]: "EX x:I. finite(A x) \<Longrightarrow> finite(INT x:I. A x)"
```
```   226 by (blast intro: INT_lower finite_subset)
```
```   227
```
```   228 lemma finite_empty_induct:
```
```   229   assumes "finite A"
```
```   230     and "P A"
```
```   231     and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})"
```
```   232   shows "P {}"
```
```   233 proof -
```
```   234   have "P (A - A)"
```
```   235   proof -
```
```   236     {
```
```   237       fix c b :: "'a set"
```
```   238       assume c: "finite c" and b: "finite b"
```
```   239 	and P1: "P b" and P2: "!!x y. finite y ==> x \<in> y ==> P y ==> P (y - {x})"
```
```   240       have "c \<subseteq> b ==> P (b - c)"
```
```   241 	using c
```
```   242       proof induct
```
```   243 	case empty
```
```   244 	from P1 show ?case by simp
```
```   245       next
```
```   246 	case (insert x F)
```
```   247 	have "P (b - F - {x})"
```
```   248 	proof (rule P2)
```
```   249           from _ b show "finite (b - F)" by (rule finite_subset) blast
```
```   250           from insert show "x \<in> b - F" by simp
```
```   251           from insert show "P (b - F)" by simp
```
```   252 	qed
```
```   253 	also have "b - F - {x} = b - insert x F" by (rule Diff_insert [symmetric])
```
```   254 	finally show ?case .
```
```   255       qed
```
```   256     }
```
```   257     then show ?thesis by this (simp_all add: assms)
```
```   258   qed
```
```   259   then show ?thesis by simp
```
```   260 qed
```
```   261
```
```   262 lemma finite_Diff [simp]: "finite A ==> finite (A - B)"
```
```   263 by (rule Diff_subset [THEN finite_subset])
```
```   264
```
```   265 lemma finite_Diff2 [simp]:
```
```   266   assumes "finite B" shows "finite (A - B) = finite A"
```
```   267 proof -
```
```   268   have "finite A \<longleftrightarrow> finite((A-B) Un (A Int B))" by(simp add: Un_Diff_Int)
```
```   269   also have "\<dots> \<longleftrightarrow> finite(A-B)" using `finite B` by(simp)
```
```   270   finally show ?thesis ..
```
```   271 qed
```
```   272
```
```   273 lemma finite_compl[simp]:
```
```   274   "finite(A::'a set) \<Longrightarrow> finite(-A) = finite(UNIV::'a set)"
```
```   275 by(simp add:Compl_eq_Diff_UNIV)
```
```   276
```
```   277 lemma finite_Collect_not[simp]:
```
```   278   "finite{x::'a. P x} \<Longrightarrow> finite{x. ~P x} = finite(UNIV::'a set)"
```
```   279 by(simp add:Collect_neg_eq)
```
```   280
```
```   281 lemma finite_Diff_insert [iff]: "finite (A - insert a B) = finite (A - B)"
```
```   282   apply (subst Diff_insert)
```
```   283   apply (case_tac "a : A - B")
```
```   284    apply (rule finite_insert [symmetric, THEN trans])
```
```   285    apply (subst insert_Diff, simp_all)
```
```   286   done
```
```   287
```
```   288
```
```   289 text {* Image and Inverse Image over Finite Sets *}
```
```   290
```
```   291 lemma finite_imageI[simp]: "finite F ==> finite (h ` F)"
```
```   292   -- {* The image of a finite set is finite. *}
```
```   293   by (induct set: finite) simp_all
```
```   294
```
```   295 lemma finite_image_set [simp]:
```
```   296   "finite {x. P x} \<Longrightarrow> finite { f x | x. P x }"
```
```   297   by (simp add: image_Collect [symmetric])
```
```   298
```
```   299 lemma finite_surj: "finite A ==> B <= f ` A ==> finite B"
```
```   300   apply (frule finite_imageI)
```
```   301   apply (erule finite_subset, assumption)
```
```   302   done
```
```   303
```
```   304 lemma finite_range_imageI:
```
```   305     "finite (range g) ==> finite (range (%x. f (g x)))"
```
```   306   apply (drule finite_imageI, simp add: range_composition)
```
```   307   done
```
```   308
```
```   309 lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A"
```
```   310 proof -
```
```   311   have aux: "!!A. finite (A - {}) = finite A" by simp
```
```   312   fix B :: "'a set"
```
```   313   assume "finite B"
```
```   314   thus "!!A. f`A = B ==> inj_on f A ==> finite A"
```
```   315     apply induct
```
```   316      apply simp
```
```   317     apply (subgoal_tac "EX y:A. f y = x & F = f ` (A - {y})")
```
```   318      apply clarify
```
```   319      apply (simp (no_asm_use) add: inj_on_def)
```
```   320      apply (blast dest!: aux [THEN iffD1], atomize)
```
```   321     apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl)
```
```   322     apply (frule subsetD [OF equalityD2 insertI1], clarify)
```
```   323     apply (rule_tac x = xa in bexI)
```
```   324      apply (simp_all add: inj_on_image_set_diff)
```
```   325     done
```
```   326 qed (rule refl)
```
```   327
```
```   328
```
```   329 lemma inj_vimage_singleton: "inj f ==> f-`{a} \<subseteq> {THE x. f x = a}"
```
```   330   -- {* The inverse image of a singleton under an injective function
```
```   331          is included in a singleton. *}
```
```   332   apply (auto simp add: inj_on_def)
```
```   333   apply (blast intro: the_equality [symmetric])
```
```   334   done
```
```   335
```
```   336 lemma finite_vimageI: "[|finite F; inj h|] ==> finite (h -` F)"
```
```   337   -- {* The inverse image of a finite set under an injective function
```
```   338          is finite. *}
```
```   339   apply (induct set: finite)
```
```   340    apply simp_all
```
```   341   apply (subst vimage_insert)
```
```   342   apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
```
```   343   done
```
```   344
```
```   345
```
```   346 text {* The finite UNION of finite sets *}
```
```   347
```
```   348 lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
```
```   349   by (induct set: finite) simp_all
```
```   350
```
```   351 text {*
```
```   352   Strengthen RHS to
```
```   353   @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x \<noteq> {}})"}?
```
```   354
```
```   355   We'd need to prove
```
```   356   @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x \<noteq> {}}"}
```
```   357   by induction. *}
```
```   358
```
```   359 lemma finite_UN [simp]:
```
```   360   "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
```
```   361 by (blast intro: finite_UN_I finite_subset)
```
```   362
```
```   363 lemma finite_Collect_bex[simp]: "finite A \<Longrightarrow>
```
```   364   finite{x. EX y:A. Q x y} = (ALL y:A. finite{x. Q x y})"
```
```   365 apply(subgoal_tac "{x. EX y:A. Q x y} = UNION A (%y. {x. Q x y})")
```
```   366  apply auto
```
```   367 done
```
```   368
```
```   369 lemma finite_Collect_bounded_ex[simp]: "finite{y. P y} \<Longrightarrow>
```
```   370   finite{x. EX y. P y & Q x y} = (ALL y. P y \<longrightarrow> finite{x. Q x y})"
```
```   371 apply(subgoal_tac "{x. EX y. P y & Q x y} = UNION {y. P y} (%y. {x. Q x y})")
```
```   372  apply auto
```
```   373 done
```
```   374
```
```   375
```
```   376 lemma finite_Plus: "[| finite A; finite B |] ==> finite (A <+> B)"
```
```   377 by (simp add: Plus_def)
```
```   378
```
```   379 lemma finite_PlusD:
```
```   380   fixes A :: "'a set" and B :: "'b set"
```
```   381   assumes fin: "finite (A <+> B)"
```
```   382   shows "finite A" "finite B"
```
```   383 proof -
```
```   384   have "Inl ` A \<subseteq> A <+> B" by auto
```
```   385   hence "finite (Inl ` A :: ('a + 'b) set)" using fin by(rule finite_subset)
```
```   386   thus "finite A" by(rule finite_imageD)(auto intro: inj_onI)
```
```   387 next
```
```   388   have "Inr ` B \<subseteq> A <+> B" by auto
```
```   389   hence "finite (Inr ` B :: ('a + 'b) set)" using fin by(rule finite_subset)
```
```   390   thus "finite B" by(rule finite_imageD)(auto intro: inj_onI)
```
```   391 qed
```
```   392
```
```   393 lemma finite_Plus_iff[simp]: "finite (A <+> B) \<longleftrightarrow> finite A \<and> finite B"
```
```   394 by(auto intro: finite_PlusD finite_Plus)
```
```   395
```
```   396 lemma finite_Plus_UNIV_iff[simp]:
```
```   397   "finite (UNIV :: ('a + 'b) set) =
```
```   398   (finite (UNIV :: 'a set) & finite (UNIV :: 'b set))"
```
```   399 by(subst UNIV_Plus_UNIV[symmetric])(rule finite_Plus_iff)
```
```   400
```
```   401
```
```   402 text {* Sigma of finite sets *}
```
```   403
```
```   404 lemma finite_SigmaI [simp]:
```
```   405     "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)"
```
```   406   by (unfold Sigma_def) (blast intro!: finite_UN_I)
```
```   407
```
```   408 lemma finite_cartesian_product: "[| finite A; finite B |] ==>
```
```   409     finite (A <*> B)"
```
```   410   by (rule finite_SigmaI)
```
```   411
```
```   412 lemma finite_Prod_UNIV:
```
```   413     "finite (UNIV::'a set) ==> finite (UNIV::'b set) ==> finite (UNIV::('a * 'b) set)"
```
```   414   apply (subgoal_tac "(UNIV:: ('a * 'b) set) = Sigma UNIV (%x. UNIV)")
```
```   415    apply (erule ssubst)
```
```   416    apply (erule finite_SigmaI, auto)
```
```   417   done
```
```   418
```
```   419 lemma finite_cartesian_productD1:
```
```   420      "[| finite (A <*> B); B \<noteq> {} |] ==> finite A"
```
```   421 apply (auto simp add: finite_conv_nat_seg_image)
```
```   422 apply (drule_tac x=n in spec)
```
```   423 apply (drule_tac x="fst o f" in spec)
```
```   424 apply (auto simp add: o_def)
```
```   425  prefer 2 apply (force dest!: equalityD2)
```
```   426 apply (drule equalityD1)
```
```   427 apply (rename_tac y x)
```
```   428 apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)")
```
```   429  prefer 2 apply force
```
```   430 apply clarify
```
```   431 apply (rule_tac x=k in image_eqI, auto)
```
```   432 done
```
```   433
```
```   434 lemma finite_cartesian_productD2:
```
```   435      "[| finite (A <*> B); A \<noteq> {} |] ==> finite B"
```
```   436 apply (auto simp add: finite_conv_nat_seg_image)
```
```   437 apply (drule_tac x=n in spec)
```
```   438 apply (drule_tac x="snd o f" in spec)
```
```   439 apply (auto simp add: o_def)
```
```   440  prefer 2 apply (force dest!: equalityD2)
```
```   441 apply (drule equalityD1)
```
```   442 apply (rename_tac x y)
```
```   443 apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)")
```
```   444  prefer 2 apply force
```
```   445 apply clarify
```
```   446 apply (rule_tac x=k in image_eqI, auto)
```
```   447 done
```
```   448
```
```   449
```
```   450 text {* The powerset of a finite set *}
```
```   451
```
```   452 lemma finite_Pow_iff [iff]: "finite (Pow A) = finite A"
```
```   453 proof
```
```   454   assume "finite (Pow A)"
```
```   455   with _ have "finite ((%x. {x}) ` A)" by (rule finite_subset) blast
```
```   456   thus "finite A" by (rule finite_imageD [unfolded inj_on_def]) simp
```
```   457 next
```
```   458   assume "finite A"
```
```   459   thus "finite (Pow A)"
```
```   460     by induct (simp_all add: finite_UnI finite_imageI Pow_insert)
```
```   461 qed
```
```   462
```
```   463 lemma finite_Collect_subsets[simp,intro]: "finite A \<Longrightarrow> finite{B. B \<subseteq> A}"
```
```   464 by(simp add: Pow_def[symmetric])
```
```   465
```
```   466
```
```   467 lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A"
```
```   468 by(blast intro: finite_subset[OF subset_Pow_Union])
```
```   469
```
```   470
```
```   471 lemma finite_subset_image:
```
```   472   assumes "finite B"
```
```   473   shows "B \<subseteq> f ` A \<Longrightarrow> \<exists>C\<subseteq>A. finite C \<and> B = f ` C"
```
```   474 using assms proof(induct)
```
```   475   case empty thus ?case by simp
```
```   476 next
```
```   477   case insert thus ?case
```
```   478     by (clarsimp simp del: image_insert simp add: image_insert[symmetric])
```
```   479        blast
```
```   480 qed
```
```   481
```
```   482
```
```   483 subsection {* Class @{text finite}  *}
```
```   484
```
```   485 setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
```
```   486 class finite =
```
```   487   assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
```
```   488 setup {* Sign.parent_path *}
```
```   489 hide const finite
```
```   490
```
```   491 context finite
```
```   492 begin
```
```   493
```
```   494 lemma finite [simp]: "finite (A \<Colon> 'a set)"
```
```   495   by (rule subset_UNIV finite_UNIV finite_subset)+
```
```   496
```
```   497 end
```
```   498
```
```   499 lemma UNIV_unit [noatp]:
```
```   500   "UNIV = {()}" by auto
```
```   501
```
```   502 instance unit :: finite
```
```   503   by default (simp add: UNIV_unit)
```
```   504
```
```   505 lemma UNIV_bool [noatp]:
```
```   506   "UNIV = {False, True}" by auto
```
```   507
```
```   508 instance bool :: finite
```
```   509   by default (simp add: UNIV_bool)
```
```   510
```
```   511 instance * :: (finite, finite) finite
```
```   512   by default (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
```
```   513
```
```   514 lemma inj_graph: "inj (%f. {(x, y). y = f x})"
```
```   515   by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
```
```   516
```
```   517 instance "fun" :: (finite, finite) finite
```
```   518 proof
```
```   519   show "finite (UNIV :: ('a => 'b) set)"
```
```   520   proof (rule finite_imageD)
```
```   521     let ?graph = "%f::'a => 'b. {(x, y). y = f x}"
```
```   522     have "range ?graph \<subseteq> Pow UNIV" by simp
```
```   523     moreover have "finite (Pow (UNIV :: ('a * 'b) set))"
```
```   524       by (simp only: finite_Pow_iff finite)
```
```   525     ultimately show "finite (range ?graph)"
```
```   526       by (rule finite_subset)
```
```   527     show "inj ?graph" by (rule inj_graph)
```
```   528   qed
```
```   529 qed
```
```   530
```
```   531 instance "+" :: (finite, finite) finite
```
```   532   by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
```
```   533
```
```   534
```
```   535 subsection {* A fold functional for finite sets *}
```
```   536
```
```   537 text {* The intended behaviour is
```
```   538 @{text "fold f z {x\<^isub>1, ..., x\<^isub>n} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"}
```
```   539 if @{text f} is ``left-commutative'':
```
```   540 *}
```
```   541
```
```   542 locale fun_left_comm =
```
```   543   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
```
```   544   assumes fun_left_comm: "f x (f y z) = f y (f x z)"
```
```   545 begin
```
```   546
```
```   547 text{* On a functional level it looks much nicer: *}
```
```   548
```
```   549 lemma fun_comp_comm:  "f x \<circ> f y = f y \<circ> f x"
```
```   550 by (simp add: fun_left_comm expand_fun_eq)
```
```   551
```
```   552 end
```
```   553
```
```   554 inductive fold_graph :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool"
```
```   555 for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and z :: 'b where
```
```   556   emptyI [intro]: "fold_graph f z {} z" |
```
```   557   insertI [intro]: "x \<notin> A \<Longrightarrow> fold_graph f z A y
```
```   558       \<Longrightarrow> fold_graph f z (insert x A) (f x y)"
```
```   559
```
```   560 inductive_cases empty_fold_graphE [elim!]: "fold_graph f z {} x"
```
```   561
```
```   562 definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b" where
```
```   563 [code del]: "fold f z A = (THE y. fold_graph f z A y)"
```
```   564
```
```   565 text{*A tempting alternative for the definiens is
```
```   566 @{term "if finite A then THE y. fold_graph f z A y else e"}.
```
```   567 It allows the removal of finiteness assumptions from the theorems
```
```   568 @{text fold_comm}, @{text fold_reindex} and @{text fold_distrib}.
```
```   569 The proofs become ugly. It is not worth the effort. (???) *}
```
```   570
```
```   571
```
```   572 lemma Diff1_fold_graph:
```
```   573   "fold_graph f z (A - {x}) y \<Longrightarrow> x \<in> A \<Longrightarrow> fold_graph f z A (f x y)"
```
```   574 by (erule insert_Diff [THEN subst], rule fold_graph.intros, auto)
```
```   575
```
```   576 lemma fold_graph_imp_finite: "fold_graph f z A x \<Longrightarrow> finite A"
```
```   577 by (induct set: fold_graph) auto
```
```   578
```
```   579 lemma finite_imp_fold_graph: "finite A \<Longrightarrow> \<exists>x. fold_graph f z A x"
```
```   580 by (induct set: finite) auto
```
```   581
```
```   582
```
```   583 subsubsection{*From @{const fold_graph} to @{term fold}*}
```
```   584
```
```   585 lemma image_less_Suc: "h ` {i. i < Suc m} = insert (h m) (h ` {i. i < m})"
```
```   586   by (auto simp add: less_Suc_eq)
```
```   587
```
```   588 lemma insert_image_inj_on_eq:
```
```   589      "[|insert (h m) A = h ` {i. i < Suc m}; h m \<notin> A;
```
```   590         inj_on h {i. i < Suc m}|]
```
```   591       ==> A = h ` {i. i < m}"
```
```   592 apply (auto simp add: image_less_Suc inj_on_def)
```
```   593 apply (blast intro: less_trans)
```
```   594 done
```
```   595
```
```   596 lemma insert_inj_onE:
```
```   597   assumes aA: "insert a A = h`{i::nat. i<n}" and anot: "a \<notin> A"
```
```   598       and inj_on: "inj_on h {i::nat. i<n}"
```
```   599   shows "\<exists>hm m. inj_on hm {i::nat. i<m} & A = hm ` {i. i<m} & m < n"
```
```   600 proof (cases n)
```
```   601   case 0 thus ?thesis using aA by auto
```
```   602 next
```
```   603   case (Suc m)
```
```   604   have nSuc: "n = Suc m" by fact
```
```   605   have mlessn: "m<n" by (simp add: nSuc)
```
```   606   from aA obtain k where hkeq: "h k = a" and klessn: "k<n" by (blast elim!: equalityE)
```
```   607   let ?hm = "Fun.swap k m h"
```
```   608   have inj_hm: "inj_on ?hm {i. i < n}" using klessn mlessn
```
```   609     by (simp add: inj_on_swap_iff inj_on)
```
```   610   show ?thesis
```
```   611   proof (intro exI conjI)
```
```   612     show "inj_on ?hm {i. i < m}" using inj_hm
```
```   613       by (auto simp add: nSuc less_Suc_eq intro: subset_inj_on)
```
```   614     show "m<n" by (rule mlessn)
```
```   615     show "A = ?hm ` {i. i < m}"
```
```   616     proof (rule insert_image_inj_on_eq)
```
```   617       show "inj_on (Fun.swap k m h) {i. i < Suc m}" using inj_hm nSuc by simp
```
```   618       show "?hm m \<notin> A" by (simp add: swap_def hkeq anot)
```
```   619       show "insert (?hm m) A = ?hm ` {i. i < Suc m}"
```
```   620 	using aA hkeq nSuc klessn
```
```   621 	by (auto simp add: swap_def image_less_Suc fun_upd_image
```
```   622 			   less_Suc_eq inj_on_image_set_diff [OF inj_on])
```
```   623     qed
```
```   624   qed
```
```   625 qed
```
```   626
```
```   627 context fun_left_comm
```
```   628 begin
```
```   629
```
```   630 lemma fold_graph_determ_aux:
```
```   631   "A = h`{i::nat. i<n} \<Longrightarrow> inj_on h {i. i<n}
```
```   632    \<Longrightarrow> fold_graph f z A x \<Longrightarrow> fold_graph f z A x'
```
```   633    \<Longrightarrow> x' = x"
```
```   634 proof (induct n arbitrary: A x x' h rule: less_induct)
```
```   635   case (less n)
```
```   636   have IH: "\<And>m h A x x'. m < n \<Longrightarrow> A = h ` {i. i<m}
```
```   637       \<Longrightarrow> inj_on h {i. i<m} \<Longrightarrow> fold_graph f z A x
```
```   638       \<Longrightarrow> fold_graph f z A x' \<Longrightarrow> x' = x" by fact
```
```   639   have Afoldx: "fold_graph f z A x" and Afoldx': "fold_graph f z A x'"
```
```   640     and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" by fact+
```
```   641   show ?case
```
```   642   proof (rule fold_graph.cases [OF Afoldx])
```
```   643     assume "A = {}" and "x = z"
```
```   644     with Afoldx' show "x' = x" by auto
```
```   645   next
```
```   646     fix B b u
```
```   647     assume AbB: "A = insert b B" and x: "x = f b u"
```
```   648       and notinB: "b \<notin> B" and Bu: "fold_graph f z B u"
```
```   649     show "x'=x"
```
```   650     proof (rule fold_graph.cases [OF Afoldx'])
```
```   651       assume "A = {}" and "x' = z"
```
```   652       with AbB show "x' = x" by blast
```
```   653     next
```
```   654       fix C c v
```
```   655       assume AcC: "A = insert c C" and x': "x' = f c v"
```
```   656         and notinC: "c \<notin> C" and Cv: "fold_graph f z C v"
```
```   657       from A AbB have Beq: "insert b B = h`{i. i<n}" by simp
```
```   658       from insert_inj_onE [OF Beq notinB injh]
```
```   659       obtain hB mB where inj_onB: "inj_on hB {i. i < mB}"
```
```   660         and Beq: "B = hB ` {i. i < mB}" and lessB: "mB < n" by auto
```
```   661       from A AcC have Ceq: "insert c C = h`{i. i<n}" by simp
```
```   662       from insert_inj_onE [OF Ceq notinC injh]
```
```   663       obtain hC mC where inj_onC: "inj_on hC {i. i < mC}"
```
```   664         and Ceq: "C = hC ` {i. i < mC}" and lessC: "mC < n" by auto
```
```   665       show "x'=x"
```
```   666       proof cases
```
```   667         assume "b=c"
```
```   668 	then moreover have "B = C" using AbB AcC notinB notinC by auto
```
```   669 	ultimately show ?thesis  using Bu Cv x x' IH [OF lessC Ceq inj_onC]
```
```   670           by auto
```
```   671       next
```
```   672 	assume diff: "b \<noteq> c"
```
```   673 	let ?D = "B - {c}"
```
```   674 	have B: "B = insert c ?D" and C: "C = insert b ?D"
```
```   675 	  using AbB AcC notinB notinC diff by(blast elim!:equalityE)+
```
```   676 	have "finite A" by(rule fold_graph_imp_finite [OF Afoldx])
```
```   677 	with AbB have "finite ?D" by simp
```
```   678 	then obtain d where Dfoldd: "fold_graph f z ?D d"
```
```   679 	  using finite_imp_fold_graph by iprover
```
```   680 	moreover have cinB: "c \<in> B" using B by auto
```
```   681 	ultimately have "fold_graph f z B (f c d)" by(rule Diff1_fold_graph)
```
```   682 	hence "f c d = u" by (rule IH [OF lessB Beq inj_onB Bu])
```
```   683         moreover have "f b d = v"
```
```   684 	proof (rule IH[OF lessC Ceq inj_onC Cv])
```
```   685 	  show "fold_graph f z C (f b d)" using C notinB Dfoldd by fastsimp
```
```   686 	qed
```
```   687 	ultimately show ?thesis
```
```   688           using fun_left_comm [of c b] x x' by (auto simp add: o_def)
```
```   689       qed
```
```   690     qed
```
```   691   qed
```
```   692 qed
```
```   693
```
```   694 lemma fold_graph_determ:
```
```   695   "fold_graph f z A x \<Longrightarrow> fold_graph f z A y \<Longrightarrow> y = x"
```
```   696 apply (frule fold_graph_imp_finite [THEN finite_imp_nat_seg_image_inj_on])
```
```   697 apply (blast intro: fold_graph_determ_aux [rule_format])
```
```   698 done
```
```   699
```
```   700 lemma fold_equality:
```
```   701   "fold_graph f z A y \<Longrightarrow> fold f z A = y"
```
```   702 by (unfold fold_def) (blast intro: fold_graph_determ)
```
```   703
```
```   704 text{* The base case for @{text fold}: *}
```
```   705
```
```   706 lemma (in -) fold_empty [simp]: "fold f z {} = z"
```
```   707 by (unfold fold_def) blast
```
```   708
```
```   709 text{* The various recursion equations for @{const fold}: *}
```
```   710
```
```   711 lemma fold_insert_aux: "x \<notin> A
```
```   712   \<Longrightarrow> fold_graph f z (insert x A) v \<longleftrightarrow>
```
```   713       (\<exists>y. fold_graph f z A y \<and> v = f x y)"
```
```   714 apply auto
```
```   715 apply (rule_tac A1 = A and f1 = f in finite_imp_fold_graph [THEN exE])
```
```   716  apply (fastsimp dest: fold_graph_imp_finite)
```
```   717 apply (blast intro: fold_graph_determ)
```
```   718 done
```
```   719
```
```   720 lemma fold_insert [simp]:
```
```   721   "finite A ==> x \<notin> A ==> fold f z (insert x A) = f x (fold f z A)"
```
```   722 apply (simp add: fold_def fold_insert_aux)
```
```   723 apply (rule the_equality)
```
```   724  apply (auto intro: finite_imp_fold_graph
```
```   725         cong add: conj_cong simp add: fold_def[symmetric] fold_equality)
```
```   726 done
```
```   727
```
```   728 lemma fold_fun_comm:
```
```   729   "finite A \<Longrightarrow> f x (fold f z A) = fold f (f x z) A"
```
```   730 proof (induct rule: finite_induct)
```
```   731   case empty then show ?case by simp
```
```   732 next
```
```   733   case (insert y A) then show ?case
```
```   734     by (simp add: fun_left_comm[of x])
```
```   735 qed
```
```   736
```
```   737 lemma fold_insert2:
```
```   738   "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A"
```
```   739 by (simp add: fold_insert fold_fun_comm)
```
```   740
```
```   741 lemma fold_rec:
```
```   742 assumes "finite A" and "x \<in> A"
```
```   743 shows "fold f z A = f x (fold f z (A - {x}))"
```
```   744 proof -
```
```   745   have A: "A = insert x (A - {x})" using `x \<in> A` by blast
```
```   746   then have "fold f z A = fold f z (insert x (A - {x}))" by simp
```
```   747   also have "\<dots> = f x (fold f z (A - {x}))"
```
```   748     by (rule fold_insert) (simp add: `finite A`)+
```
```   749   finally show ?thesis .
```
```   750 qed
```
```   751
```
```   752 lemma fold_insert_remove:
```
```   753   assumes "finite A"
```
```   754   shows "fold f z (insert x A) = f x (fold f z (A - {x}))"
```
```   755 proof -
```
```   756   from `finite A` have "finite (insert x A)" by auto
```
```   757   moreover have "x \<in> insert x A" by auto
```
```   758   ultimately have "fold f z (insert x A) = f x (fold f z (insert x A - {x}))"
```
```   759     by (rule fold_rec)
```
```   760   then show ?thesis by simp
```
```   761 qed
```
```   762
```
```   763 end
```
```   764
```
```   765 text{* A simplified version for idempotent functions: *}
```
```   766
```
```   767 locale fun_left_comm_idem = fun_left_comm +
```
```   768   assumes fun_left_idem: "f x (f x z) = f x z"
```
```   769 begin
```
```   770
```
```   771 text{* The nice version: *}
```
```   772 lemma fun_comp_idem : "f x o f x = f x"
```
```   773 by (simp add: fun_left_idem expand_fun_eq)
```
```   774
```
```   775 lemma fold_insert_idem:
```
```   776   assumes fin: "finite A"
```
```   777   shows "fold f z (insert x A) = f x (fold f z A)"
```
```   778 proof cases
```
```   779   assume "x \<in> A"
```
```   780   then obtain B where "A = insert x B" and "x \<notin> B" by (rule set_insert)
```
```   781   then show ?thesis using assms by (simp add:fun_left_idem)
```
```   782 next
```
```   783   assume "x \<notin> A" then show ?thesis using assms by simp
```
```   784 qed
```
```   785
```
```   786 declare fold_insert[simp del] fold_insert_idem[simp]
```
```   787
```
```   788 lemma fold_insert_idem2:
```
```   789   "finite A \<Longrightarrow> fold f z (insert x A) = fold f (f x z) A"
```
```   790 by(simp add:fold_fun_comm)
```
```   791
```
```   792 end
```
```   793
```
```   794 context ab_semigroup_idem_mult
```
```   795 begin
```
```   796
```
```   797 lemma fun_left_comm_idem: "fun_left_comm_idem(op *)"
```
```   798 apply unfold_locales
```
```   799  apply (simp add: mult_ac)
```
```   800 apply (simp add: mult_idem mult_assoc[symmetric])
```
```   801 done
```
```   802
```
```   803 end
```
```   804
```
```   805 context lower_semilattice
```
```   806 begin
```
```   807
```
```   808 lemma ab_semigroup_idem_mult_inf: "ab_semigroup_idem_mult inf"
```
```   809 proof qed (rule inf_assoc inf_commute inf_idem)+
```
```   810
```
```   811 lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> fold inf b (insert a A) = inf a (fold inf b A)"
```
```   812 by(rule fun_left_comm_idem.fold_insert_idem[OF ab_semigroup_idem_mult.fun_left_comm_idem[OF ab_semigroup_idem_mult_inf]])
```
```   813
```
```   814 lemma inf_le_fold_inf: "finite A \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> fold inf c A"
```
```   815 by (induct pred: finite) (auto intro: le_infI1)
```
```   816
```
```   817 lemma fold_inf_le_inf: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> fold inf b A \<le> inf a b"
```
```   818 proof(induct arbitrary: a pred:finite)
```
```   819   case empty thus ?case by simp
```
```   820 next
```
```   821   case (insert x A)
```
```   822   show ?case
```
```   823   proof cases
```
```   824     assume "A = {}" thus ?thesis using insert by simp
```
```   825   next
```
```   826     assume "A \<noteq> {}" thus ?thesis using insert by (auto intro: le_infI2)
```
```   827   qed
```
```   828 qed
```
```   829
```
```   830 end
```
```   831
```
```   832 context upper_semilattice
```
```   833 begin
```
```   834
```
```   835 lemma ab_semigroup_idem_mult_sup: "ab_semigroup_idem_mult sup"
```
```   836 by (rule lower_semilattice.ab_semigroup_idem_mult_inf)(rule dual_semilattice)
```
```   837
```
```   838 lemma fold_sup_insert[simp]: "finite A \<Longrightarrow> fold sup b (insert a A) = sup a (fold sup b A)"
```
```   839 by(rule lower_semilattice.fold_inf_insert)(rule dual_semilattice)
```
```   840
```
```   841 lemma fold_sup_le_sup: "finite A \<Longrightarrow> ALL a:A. a \<le> b \<Longrightarrow> fold sup c A \<le> sup b c"
```
```   842 by(rule lower_semilattice.inf_le_fold_inf)(rule dual_semilattice)
```
```   843
```
```   844 lemma sup_le_fold_sup: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a b \<le> fold sup b A"
```
```   845 by(rule lower_semilattice.fold_inf_le_inf)(rule dual_semilattice)
```
```   846
```
```   847 end
```
```   848
```
```   849
```
```   850 subsubsection{* The derived combinator @{text fold_image} *}
```
```   851
```
```   852 definition fold_image :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"
```
```   853 where "fold_image f g = fold (%x y. f (g x) y)"
```
```   854
```
```   855 lemma fold_image_empty[simp]: "fold_image f g z {} = z"
```
```   856 by(simp add:fold_image_def)
```
```   857
```
```   858 context ab_semigroup_mult
```
```   859 begin
```
```   860
```
```   861 lemma fold_image_insert[simp]:
```
```   862 assumes "finite A" and "a \<notin> A"
```
```   863 shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)"
```
```   864 proof -
```
```   865   interpret I: fun_left_comm "%x y. (g x) * y"
```
```   866     by unfold_locales (simp add: mult_ac)
```
```   867   show ?thesis using assms by(simp add:fold_image_def)
```
```   868 qed
```
```   869
```
```   870 (*
```
```   871 lemma fold_commute:
```
```   872   "finite A ==> (!!z. x * (fold times g z A) = fold times g (x * z) A)"
```
```   873   apply (induct set: finite)
```
```   874    apply simp
```
```   875   apply (simp add: mult_left_commute [of x])
```
```   876   done
```
```   877
```
```   878 lemma fold_nest_Un_Int:
```
```   879   "finite A ==> finite B
```
```   880     ==> fold times g (fold times g z B) A = fold times g (fold times g z (A Int B)) (A Un B)"
```
```   881   apply (induct set: finite)
```
```   882    apply simp
```
```   883   apply (simp add: fold_commute Int_insert_left insert_absorb)
```
```   884   done
```
```   885
```
```   886 lemma fold_nest_Un_disjoint:
```
```   887   "finite A ==> finite B ==> A Int B = {}
```
```   888     ==> fold times g z (A Un B) = fold times g (fold times g z B) A"
```
```   889   by (simp add: fold_nest_Un_Int)
```
```   890 *)
```
```   891
```
```   892 lemma fold_image_reindex:
```
```   893 assumes fin: "finite A"
```
```   894 shows "inj_on h A \<Longrightarrow> fold_image times g z (h`A) = fold_image times (g\<circ>h) z A"
```
```   895 using fin by induct auto
```
```   896
```
```   897 (*
```
```   898 text{*
```
```   899   Fusion theorem, as described in Graham Hutton's paper,
```
```   900   A Tutorial on the Universality and Expressiveness of Fold,
```
```   901   JFP 9:4 (355-372), 1999.
```
```   902 *}
```
```   903
```
```   904 lemma fold_fusion:
```
```   905   assumes "ab_semigroup_mult g"
```
```   906   assumes fin: "finite A"
```
```   907     and hyp: "\<And>x y. h (g x y) = times x (h y)"
```
```   908   shows "h (fold g j w A) = fold times j (h w) A"
```
```   909 proof -
```
```   910   class_interpret ab_semigroup_mult [g] by fact
```
```   911   show ?thesis using fin hyp by (induct set: finite) simp_all
```
```   912 qed
```
```   913 *)
```
```   914
```
```   915 lemma fold_image_cong:
```
```   916   "finite A \<Longrightarrow>
```
```   917   (!!x. x:A ==> g x = h x) ==> fold_image times g z A = fold_image times h z A"
```
```   918 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")
```
```   919  apply simp
```
```   920 apply (erule finite_induct, simp)
```
```   921 apply (simp add: subset_insert_iff, clarify)
```
```   922 apply (subgoal_tac "finite C")
```
```   923  prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
```
```   924 apply (subgoal_tac "C = insert x (C - {x})")
```
```   925  prefer 2 apply blast
```
```   926 apply (erule ssubst)
```
```   927 apply (drule spec)
```
```   928 apply (erule (1) notE impE)
```
```   929 apply (simp add: Ball_def del: insert_Diff_single)
```
```   930 done
```
```   931
```
```   932 end
```
```   933
```
```   934 context comm_monoid_mult
```
```   935 begin
```
```   936
```
```   937 lemma fold_image_Un_Int:
```
```   938   "finite A ==> finite B ==>
```
```   939     fold_image times g 1 A * fold_image times g 1 B =
```
```   940     fold_image times g 1 (A Un B) * fold_image times g 1 (A Int B)"
```
```   941 by (induct set: finite)
```
```   942    (auto simp add: mult_ac insert_absorb Int_insert_left)
```
```   943
```
```   944 corollary fold_Un_disjoint:
```
```   945   "finite A ==> finite B ==> A Int B = {} ==>
```
```   946    fold_image times g 1 (A Un B) =
```
```   947    fold_image times g 1 A * fold_image times g 1 B"
```
```   948 by (simp add: fold_image_Un_Int)
```
```   949
```
```   950 lemma fold_image_UN_disjoint:
```
```   951   "\<lbrakk> finite I; ALL i:I. finite (A i);
```
```   952      ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {} \<rbrakk>
```
```   953    \<Longrightarrow> fold_image times g 1 (UNION I A) =
```
```   954        fold_image times (%i. fold_image times g 1 (A i)) 1 I"
```
```   955 apply (induct set: finite, simp, atomize)
```
```   956 apply (subgoal_tac "ALL i:F. x \<noteq> i")
```
```   957  prefer 2 apply blast
```
```   958 apply (subgoal_tac "A x Int UNION F A = {}")
```
```   959  prefer 2 apply blast
```
```   960 apply (simp add: fold_Un_disjoint)
```
```   961 done
```
```   962
```
```   963 lemma fold_image_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
```
```   964   fold_image times (%x. fold_image times (g x) 1 (B x)) 1 A =
```
```   965   fold_image times (split g) 1 (SIGMA x:A. B x)"
```
```   966 apply (subst Sigma_def)
```
```   967 apply (subst fold_image_UN_disjoint, assumption, simp)
```
```   968  apply blast
```
```   969 apply (erule fold_image_cong)
```
```   970 apply (subst fold_image_UN_disjoint, simp, simp)
```
```   971  apply blast
```
```   972 apply simp
```
```   973 done
```
```   974
```
```   975 lemma fold_image_distrib: "finite A \<Longrightarrow>
```
```   976    fold_image times (%x. g x * h x) 1 A =
```
```   977    fold_image times g 1 A *  fold_image times h 1 A"
```
```   978 by (erule finite_induct) (simp_all add: mult_ac)
```
```   979
```
```   980 lemma fold_image_related:
```
```   981   assumes Re: "R e e"
```
```   982   and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)"
```
```   983   and fS: "finite S" and Rfg: "\<forall>x\<in>S. R (h x) (g x)"
```
```   984   shows "R (fold_image (op *) h e S) (fold_image (op *) g e S)"
```
```   985   using fS by (rule finite_subset_induct) (insert assms, auto)
```
```   986
```
```   987 lemma  fold_image_eq_general:
```
```   988   assumes fS: "finite S"
```
```   989   and h: "\<forall>y\<in>S'. \<exists>!x. x\<in> S \<and> h(x) = y"
```
```   990   and f12:  "\<forall>x\<in>S. h x \<in> S' \<and> f2(h x) = f1 x"
```
```   991   shows "fold_image (op *) f1 e S = fold_image (op *) f2 e S'"
```
```   992 proof-
```
```   993   from h f12 have hS: "h ` S = S'" by auto
```
```   994   {fix x y assume H: "x \<in> S" "y \<in> S" "h x = h y"
```
```   995     from f12 h H  have "x = y" by auto }
```
```   996   hence hinj: "inj_on h S" unfolding inj_on_def Ex1_def by blast
```
```   997   from f12 have th: "\<And>x. x \<in> S \<Longrightarrow> (f2 \<circ> h) x = f1 x" by auto
```
```   998   from hS have "fold_image (op *) f2 e S' = fold_image (op *) f2 e (h ` S)" by simp
```
```   999   also have "\<dots> = fold_image (op *) (f2 o h) e S"
```
```  1000     using fold_image_reindex[OF fS hinj, of f2 e] .
```
```  1001   also have "\<dots> = fold_image (op *) f1 e S " using th fold_image_cong[OF fS, of "f2 o h" f1 e]
```
```  1002     by blast
```
```  1003   finally show ?thesis ..
```
```  1004 qed
```
```  1005
```
```  1006 lemma fold_image_eq_general_inverses:
```
```  1007   assumes fS: "finite S"
```
```  1008   and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
```
```  1009   and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x  \<and> g (h x) = f x"
```
```  1010   shows "fold_image (op *) f e S = fold_image (op *) g e T"
```
```  1011   (* metis solves it, but not yet available here *)
```
```  1012   apply (rule fold_image_eq_general[OF fS, of T h g f e])
```
```  1013   apply (rule ballI)
```
```  1014   apply (frule kh)
```
```  1015   apply (rule ex1I[])
```
```  1016   apply blast
```
```  1017   apply clarsimp
```
```  1018   apply (drule hk) apply simp
```
```  1019   apply (rule sym)
```
```  1020   apply (erule conjunct1[OF conjunct2[OF hk]])
```
```  1021   apply (rule ballI)
```
```  1022   apply (drule  hk)
```
```  1023   apply blast
```
```  1024   done
```
```  1025
```
```  1026 end
```
```  1027
```
```  1028 subsection {* Generalized summation over a set *}
```
```  1029
```
```  1030 interpretation comm_monoid_add: comm_monoid_mult "0::'a::comm_monoid_add" "op +"
```
```  1031   proof qed (auto intro: add_assoc add_commute)
```
```  1032
```
```  1033 definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
```
```  1034 where "setsum f A == if finite A then fold_image (op +) f 0 A else 0"
```
```  1035
```
```  1036 abbreviation
```
```  1037   Setsum  ("\<Sum>_" [1000] 999) where
```
```  1038   "\<Sum>A == setsum (%x. x) A"
```
```  1039
```
```  1040 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
```
```  1041 written @{text"\<Sum>x\<in>A. e"}. *}
```
```  1042
```
```  1043 syntax
```
```  1044   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
```
```  1045 syntax (xsymbols)
```
```  1046   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
```
```  1047 syntax (HTML output)
```
```  1048   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
```
```  1049
```
```  1050 translations -- {* Beware of argument permutation! *}
```
```  1051   "SUM i:A. b" == "CONST setsum (%i. b) A"
```
```  1052   "\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
```
```  1053
```
```  1054 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
```
```  1055  @{text"\<Sum>x|P. e"}. *}
```
```  1056
```
```  1057 syntax
```
```  1058   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
```
```  1059 syntax (xsymbols)
```
```  1060   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
```
```  1061 syntax (HTML output)
```
```  1062   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
```
```  1063
```
```  1064 translations
```
```  1065   "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
```
```  1066   "\<Sum>x|P. t" => "CONST setsum (%x. t) {x. P}"
```
```  1067
```
```  1068 print_translation {*
```
```  1069 let
```
```  1070   fun setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) \$ Abs(y,Ty,P)] =
```
```  1071     if x<>y then raise Match
```
```  1072     else let val x' = Syntax.mark_bound x
```
```  1073              val t' = subst_bound(x',t)
```
```  1074              val P' = subst_bound(x',P)
```
```  1075          in Syntax.const "_qsetsum" \$ Syntax.mark_bound x \$ P' \$ t' end
```
```  1076 in [("setsum", setsum_tr')] end
```
```  1077 *}
```
```  1078
```
```  1079
```
```  1080 lemma setsum_empty [simp]: "setsum f {} = 0"
```
```  1081 by (simp add: setsum_def)
```
```  1082
```
```  1083 lemma setsum_insert [simp]:
```
```  1084   "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
```
```  1085 by (simp add: setsum_def)
```
```  1086
```
```  1087 lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0"
```
```  1088 by (simp add: setsum_def)
```
```  1089
```
```  1090 lemma setsum_reindex:
```
```  1091      "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
```
```  1092 by(auto simp add: setsum_def comm_monoid_add.fold_image_reindex dest!:finite_imageD)
```
```  1093
```
```  1094 lemma setsum_reindex_id:
```
```  1095      "inj_on f B ==> setsum f B = setsum id (f ` B)"
```
```  1096 by (auto simp add: setsum_reindex)
```
```  1097
```
```  1098 lemma setsum_reindex_nonzero:
```
```  1099   assumes fS: "finite S"
```
```  1100   and nz: "\<And> x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x = f y \<Longrightarrow> h (f x) = 0"
```
```  1101   shows "setsum h (f ` S) = setsum (h o f) S"
```
```  1102 using nz
```
```  1103 proof(induct rule: finite_induct[OF fS])
```
```  1104   case 1 thus ?case by simp
```
```  1105 next
```
```  1106   case (2 x F)
```
```  1107   {assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto
```
```  1108     then obtain y where y: "y \<in> F" "f x = f y" by auto
```
```  1109     from "2.hyps" y have xy: "x \<noteq> y" by auto
```
```  1110
```
```  1111     from "2.prems"[of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp
```
```  1112     have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto
```
```  1113     also have "\<dots> = setsum (h o f) (insert x F)"
```
```  1114       unfolding setsum_insert[OF `finite F` `x\<notin>F`]
```
```  1115       using h0
```
```  1116       apply simp
```
```  1117       apply (rule "2.hyps"(3))
```
```  1118       apply (rule_tac y="y" in  "2.prems")
```
```  1119       apply simp_all
```
```  1120       done
```
```  1121     finally have ?case .}
```
```  1122   moreover
```
```  1123   {assume fxF: "f x \<notin> f ` F"
```
```  1124     have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)"
```
```  1125       using fxF "2.hyps" by simp
```
```  1126     also have "\<dots> = setsum (h o f) (insert x F)"
```
```  1127       unfolding setsum_insert[OF `finite F` `x\<notin>F`]
```
```  1128       apply simp
```
```  1129       apply (rule cong[OF refl[of "op + (h (f x))"]])
```
```  1130       apply (rule "2.hyps"(3))
```
```  1131       apply (rule_tac y="y" in  "2.prems")
```
```  1132       apply simp_all
```
```  1133       done
```
```  1134     finally have ?case .}
```
```  1135   ultimately show ?case by blast
```
```  1136 qed
```
```  1137
```
```  1138 lemma setsum_cong:
```
```  1139   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
```
```  1140 by(fastsimp simp: setsum_def intro: comm_monoid_add.fold_image_cong)
```
```  1141
```
```  1142 lemma strong_setsum_cong[cong]:
```
```  1143   "A = B ==> (!!x. x:B =simp=> f x = g x)
```
```  1144    ==> setsum (%x. f x) A = setsum (%x. g x) B"
```
```  1145 by(fastsimp simp: simp_implies_def setsum_def intro: comm_monoid_add.fold_image_cong)
```
```  1146
```
```  1147 lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A";
```
```  1148 by (rule setsum_cong[OF refl], auto);
```
```  1149
```
```  1150 lemma setsum_reindex_cong:
```
```  1151    "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|]
```
```  1152     ==> setsum h B = setsum g A"
```
```  1153 by (simp add: setsum_reindex cong: setsum_cong)
```
```  1154
```
```  1155
```
```  1156 lemma setsum_0[simp]: "setsum (%i. 0) A = 0"
```
```  1157 apply (clarsimp simp: setsum_def)
```
```  1158 apply (erule finite_induct, auto)
```
```  1159 done
```
```  1160
```
```  1161 lemma setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0"
```
```  1162 by(simp add:setsum_cong)
```
```  1163
```
```  1164 lemma setsum_Un_Int: "finite A ==> finite B ==>
```
```  1165   setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
```
```  1166   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
```
```  1167 by(simp add: setsum_def comm_monoid_add.fold_image_Un_Int [symmetric])
```
```  1168
```
```  1169 lemma setsum_Un_disjoint: "finite A ==> finite B
```
```  1170   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
```
```  1171 by (subst setsum_Un_Int [symmetric], auto)
```
```  1172
```
```  1173 lemma setsum_mono_zero_left:
```
```  1174   assumes fT: "finite T" and ST: "S \<subseteq> T"
```
```  1175   and z: "\<forall>i \<in> T - S. f i = 0"
```
```  1176   shows "setsum f S = setsum f T"
```
```  1177 proof-
```
```  1178   have eq: "T = S \<union> (T - S)" using ST by blast
```
```  1179   have d: "S \<inter> (T - S) = {}" using ST by blast
```
```  1180   from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
```
```  1181   show ?thesis
```
```  1182   by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
```
```  1183 qed
```
```  1184
```
```  1185 lemma setsum_mono_zero_right:
```
```  1186   "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. f i = 0 \<Longrightarrow> setsum f T = setsum f S"
```
```  1187 by(blast intro!: setsum_mono_zero_left[symmetric])
```
```  1188
```
```  1189 lemma setsum_mono_zero_cong_left:
```
```  1190   assumes fT: "finite T" and ST: "S \<subseteq> T"
```
```  1191   and z: "\<forall>i \<in> T - S. g i = 0"
```
```  1192   and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
```
```  1193   shows "setsum f S = setsum g T"
```
```  1194 proof-
```
```  1195   have eq: "T = S \<union> (T - S)" using ST by blast
```
```  1196   have d: "S \<inter> (T - S) = {}" using ST by blast
```
```  1197   from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
```
```  1198   show ?thesis
```
```  1199     using fg by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
```
```  1200 qed
```
```  1201
```
```  1202 lemma setsum_mono_zero_cong_right:
```
```  1203   assumes fT: "finite T" and ST: "S \<subseteq> T"
```
```  1204   and z: "\<forall>i \<in> T - S. f i = 0"
```
```  1205   and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
```
```  1206   shows "setsum f T = setsum g S"
```
```  1207 using setsum_mono_zero_cong_left[OF fT ST z] fg[symmetric] by auto
```
```  1208
```
```  1209 lemma setsum_delta:
```
```  1210   assumes fS: "finite S"
```
```  1211   shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
```
```  1212 proof-
```
```  1213   let ?f = "(\<lambda>k. if k=a then b k else 0)"
```
```  1214   {assume a: "a \<notin> S"
```
```  1215     hence "\<forall> k\<in> S. ?f k = 0" by simp
```
```  1216     hence ?thesis  using a by simp}
```
```  1217   moreover
```
```  1218   {assume a: "a \<in> S"
```
```  1219     let ?A = "S - {a}"
```
```  1220     let ?B = "{a}"
```
```  1221     have eq: "S = ?A \<union> ?B" using a by blast
```
```  1222     have dj: "?A \<inter> ?B = {}" by simp
```
```  1223     from fS have fAB: "finite ?A" "finite ?B" by auto
```
```  1224     have "setsum ?f S = setsum ?f ?A + setsum ?f ?B"
```
```  1225       using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
```
```  1226       by simp
```
```  1227     then have ?thesis  using a by simp}
```
```  1228   ultimately show ?thesis by blast
```
```  1229 qed
```
```  1230 lemma setsum_delta':
```
```  1231   assumes fS: "finite S" shows
```
```  1232   "setsum (\<lambda>k. if a = k then b k else 0) S =
```
```  1233      (if a\<in> S then b a else 0)"
```
```  1234   using setsum_delta[OF fS, of a b, symmetric]
```
```  1235   by (auto intro: setsum_cong)
```
```  1236
```
```  1237 lemma setsum_restrict_set:
```
```  1238   assumes fA: "finite A"
```
```  1239   shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A"
```
```  1240 proof-
```
```  1241   from fA have fab: "finite (A \<inter> B)" by auto
```
```  1242   have aba: "A \<inter> B \<subseteq> A" by blast
```
```  1243   let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0"
```
```  1244   from setsum_mono_zero_left[OF fA aba, of ?g]
```
```  1245   show ?thesis by simp
```
```  1246 qed
```
```  1247
```
```  1248 lemma setsum_cases:
```
```  1249   assumes fA: "finite A"
```
```  1250   shows "setsum (\<lambda>x. if x \<in> B then f x else g x) A =
```
```  1251          setsum f (A \<inter> B) + setsum g (A \<inter> - B)"
```
```  1252 proof-
```
```  1253   have a: "A = A \<inter> B \<union> A \<inter> -B" "(A \<inter> B) \<inter> (A \<inter> -B) = {}"
```
```  1254     by blast+
```
```  1255   from fA
```
```  1256   have f: "finite (A \<inter> B)" "finite (A \<inter> -B)" by auto
```
```  1257   let ?g = "\<lambda>x. if x \<in> B then f x else g x"
```
```  1258   from setsum_Un_disjoint[OF f a(2), of ?g] a(1)
```
```  1259   show ?thesis by simp
```
```  1260 qed
```
```  1261
```
```  1262
```
```  1263 (*But we can't get rid of finite I. If infinite, although the rhs is 0,
```
```  1264   the lhs need not be, since UNION I A could still be finite.*)
```
```  1265 lemma setsum_UN_disjoint:
```
```  1266     "finite I ==> (ALL i:I. finite (A i)) ==>
```
```  1267         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
```
```  1268       setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
```
```  1269 by(simp add: setsum_def comm_monoid_add.fold_image_UN_disjoint cong: setsum_cong)
```
```  1270
```
```  1271 text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
```
```  1272 directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
```
```  1273 lemma setsum_Union_disjoint:
```
```  1274   "[| (ALL A:C. finite A);
```
```  1275       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
```
```  1276    ==> setsum f (Union C) = setsum (setsum f) C"
```
```  1277 apply (cases "finite C")
```
```  1278  prefer 2 apply (force dest: finite_UnionD simp add: setsum_def)
```
```  1279   apply (frule setsum_UN_disjoint [of C id f])
```
```  1280  apply (unfold Union_def id_def, assumption+)
```
```  1281 done
```
```  1282
```
```  1283 (*But we can't get rid of finite A. If infinite, although the lhs is 0,
```
```  1284   the rhs need not be, since SIGMA A B could still be finite.*)
```
```  1285 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
```
```  1286     (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
```
```  1287 by(simp add:setsum_def comm_monoid_add.fold_image_Sigma split_def cong:setsum_cong)
```
```  1288
```
```  1289 text{*Here we can eliminate the finiteness assumptions, by cases.*}
```
```  1290 lemma setsum_cartesian_product:
```
```  1291    "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)"
```
```  1292 apply (cases "finite A")
```
```  1293  apply (cases "finite B")
```
```  1294   apply (simp add: setsum_Sigma)
```
```  1295  apply (cases "A={}", simp)
```
```  1296  apply (simp)
```
```  1297 apply (auto simp add: setsum_def
```
```  1298             dest: finite_cartesian_productD1 finite_cartesian_productD2)
```
```  1299 done
```
```  1300
```
```  1301 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
```
```  1302 by(simp add:setsum_def comm_monoid_add.fold_image_distrib)
```
```  1303
```
```  1304
```
```  1305 subsubsection {* Properties in more restricted classes of structures *}
```
```  1306
```
```  1307 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
```
```  1308 apply (case_tac "finite A")
```
```  1309  prefer 2 apply (simp add: setsum_def)
```
```  1310 apply (erule rev_mp)
```
```  1311 apply (erule finite_induct, auto)
```
```  1312 done
```
```  1313
```
```  1314 lemma setsum_eq_0_iff [simp]:
```
```  1315     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
```
```  1316 by (induct set: finite) auto
```
```  1317
```
```  1318 lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
```
```  1319   (setsum f A = Suc 0) = (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
```
```  1320 apply(erule finite_induct)
```
```  1321 apply (auto simp add:add_is_1)
```
```  1322 done
```
```  1323
```
```  1324 lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
```
```  1325
```
```  1326 lemma setsum_Un_nat: "finite A ==> finite B ==>
```
```  1327   (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
```
```  1328   -- {* For the natural numbers, we have subtraction. *}
```
```  1329 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
```
```  1330
```
```  1331 lemma setsum_Un: "finite A ==> finite B ==>
```
```  1332   (setsum f (A Un B) :: 'a :: ab_group_add) =
```
```  1333    setsum f A + setsum f B - setsum f (A Int B)"
```
```  1334 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
```
```  1335
```
```  1336 lemma (in comm_monoid_mult) fold_image_1: "finite S \<Longrightarrow> (\<forall>x\<in>S. f x = 1) \<Longrightarrow> fold_image op * f 1 S = 1"
```
```  1337   apply (induct set: finite)
```
```  1338   apply simp by (auto simp add: fold_image_insert)
```
```  1339
```
```  1340 lemma (in comm_monoid_mult) fold_image_Un_one:
```
```  1341   assumes fS: "finite S" and fT: "finite T"
```
```  1342   and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
```
```  1343   shows "fold_image (op *) f 1 (S \<union> T) = fold_image (op *) f 1 S * fold_image (op *) f 1 T"
```
```  1344 proof-
```
```  1345   have "fold_image op * f 1 (S \<inter> T) = 1"
```
```  1346     apply (rule fold_image_1)
```
```  1347     using fS fT I0 by auto
```
```  1348   with fold_image_Un_Int[OF fS fT] show ?thesis by simp
```
```  1349 qed
```
```  1350
```
```  1351 lemma setsum_eq_general_reverses:
```
```  1352   assumes fS: "finite S" and fT: "finite T"
```
```  1353   and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
```
```  1354   and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x"
```
```  1355   shows "setsum f S = setsum g T"
```
```  1356   apply (simp add: setsum_def fS fT)
```
```  1357   apply (rule comm_monoid_add.fold_image_eq_general_inverses[OF fS])
```
```  1358   apply (erule kh)
```
```  1359   apply (erule hk)
```
```  1360   done
```
```  1361
```
```  1362
```
```  1363
```
```  1364 lemma setsum_Un_zero:
```
```  1365   assumes fS: "finite S" and fT: "finite T"
```
```  1366   and I0: "\<forall>x \<in> S\<inter>T. f x = 0"
```
```  1367   shows "setsum f (S \<union> T) = setsum f S  + setsum f T"
```
```  1368   using fS fT
```
```  1369   apply (simp add: setsum_def)
```
```  1370   apply (rule comm_monoid_add.fold_image_Un_one)
```
```  1371   using I0 by auto
```
```  1372
```
```  1373
```
```  1374 lemma setsum_UNION_zero:
```
```  1375   assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T"
```
```  1376   and f0: "\<And>T1 T2 x. T1\<in>S \<Longrightarrow> T2\<in>S \<Longrightarrow> T1 \<noteq> T2 \<Longrightarrow> x \<in> T1 \<Longrightarrow> x \<in> T2 \<Longrightarrow> f x = 0"
```
```  1377   shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S"
```
```  1378   using fSS f0
```
```  1379 proof(induct rule: finite_induct[OF fS])
```
```  1380   case 1 thus ?case by simp
```
```  1381 next
```
```  1382   case (2 T F)
```
```  1383   then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F"
```
```  1384     and H: "setsum f (\<Union> F) = setsum (setsum f) F" by (auto simp add: finite_insert)
```
```  1385   from fTF have fUF: "finite (\<Union>F)" by (auto intro: finite_Union)
```
```  1386   from "2.prems" TF fTF
```
```  1387   show ?case
```
```  1388     by (auto simp add: H[symmetric] intro: setsum_Un_zero[OF fTF(1) fUF, of f])
```
```  1389 qed
```
```  1390
```
```  1391
```
```  1392 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
```
```  1393   (if a:A then setsum f A - f a else setsum f A)"
```
```  1394 apply (case_tac "finite A")
```
```  1395  prefer 2 apply (simp add: setsum_def)
```
```  1396 apply (erule finite_induct)
```
```  1397  apply (auto simp add: insert_Diff_if)
```
```  1398 apply (drule_tac a = a in mk_disjoint_insert, auto)
```
```  1399 done
```
```  1400
```
```  1401 lemma setsum_diff1: "finite A \<Longrightarrow>
```
```  1402   (setsum f (A - {a}) :: ('a::ab_group_add)) =
```
```  1403   (if a:A then setsum f A - f a else setsum f A)"
```
```  1404 by (erule finite_induct) (auto simp add: insert_Diff_if)
```
```  1405
```
```  1406 lemma setsum_diff1'[rule_format]:
```
```  1407   "finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x)"
```
```  1408 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))"])
```
```  1409 apply (auto simp add: insert_Diff_if add_ac)
```
```  1410 done
```
```  1411
```
```  1412 lemma setsum_diff1_ring: assumes "finite A" "a \<in> A"
```
```  1413   shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)"
```
```  1414 unfolding setsum_diff1'[OF assms] by auto
```
```  1415
```
```  1416 (* By Jeremy Siek: *)
```
```  1417
```
```  1418 lemma setsum_diff_nat:
```
```  1419 assumes "finite B" and "B \<subseteq> A"
```
```  1420 shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
```
```  1421 using assms
```
```  1422 proof induct
```
```  1423   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
```
```  1424 next
```
```  1425   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
```
```  1426     and xFinA: "insert x F \<subseteq> A"
```
```  1427     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
```
```  1428   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
```
```  1429   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
```
```  1430     by (simp add: setsum_diff1_nat)
```
```  1431   from xFinA have "F \<subseteq> A" by simp
```
```  1432   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
```
```  1433   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
```
```  1434     by simp
```
```  1435   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
```
```  1436   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
```
```  1437     by simp
```
```  1438   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
```
```  1439   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
```
```  1440     by simp
```
```  1441   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
```
```  1442 qed
```
```  1443
```
```  1444 lemma setsum_diff:
```
```  1445   assumes le: "finite A" "B \<subseteq> A"
```
```  1446   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
```
```  1447 proof -
```
```  1448   from le have finiteB: "finite B" using finite_subset by auto
```
```  1449   show ?thesis using finiteB le
```
```  1450   proof induct
```
```  1451     case empty
```
```  1452     thus ?case by auto
```
```  1453   next
```
```  1454     case (insert x F)
```
```  1455     thus ?case using le finiteB
```
```  1456       by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
```
```  1457   qed
```
```  1458 qed
```
```  1459
```
```  1460 lemma setsum_mono:
```
```  1461   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))"
```
```  1462   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
```
```  1463 proof (cases "finite K")
```
```  1464   case True
```
```  1465   thus ?thesis using le
```
```  1466   proof induct
```
```  1467     case empty
```
```  1468     thus ?case by simp
```
```  1469   next
```
```  1470     case insert
```
```  1471     thus ?case using add_mono by fastsimp
```
```  1472   qed
```
```  1473 next
```
```  1474   case False
```
```  1475   thus ?thesis
```
```  1476     by (simp add: setsum_def)
```
```  1477 qed
```
```  1478
```
```  1479 lemma setsum_strict_mono:
```
```  1480   fixes f :: "'a \<Rightarrow> 'b::{pordered_cancel_ab_semigroup_add,comm_monoid_add}"
```
```  1481   assumes "finite A"  "A \<noteq> {}"
```
```  1482     and "!!x. x:A \<Longrightarrow> f x < g x"
```
```  1483   shows "setsum f A < setsum g A"
```
```  1484   using prems
```
```  1485 proof (induct rule: finite_ne_induct)
```
```  1486   case singleton thus ?case by simp
```
```  1487 next
```
```  1488   case insert thus ?case by (auto simp: add_strict_mono)
```
```  1489 qed
```
```  1490
```
```  1491 lemma setsum_negf:
```
```  1492   "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
```
```  1493 proof (cases "finite A")
```
```  1494   case True thus ?thesis by (induct set: finite) auto
```
```  1495 next
```
```  1496   case False thus ?thesis by (simp add: setsum_def)
```
```  1497 qed
```
```  1498
```
```  1499 lemma setsum_subtractf:
```
```  1500   "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
```
```  1501     setsum f A - setsum g A"
```
```  1502 proof (cases "finite A")
```
```  1503   case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
```
```  1504 next
```
```  1505   case False thus ?thesis by (simp add: setsum_def)
```
```  1506 qed
```
```  1507
```
```  1508 lemma setsum_nonneg:
```
```  1509   assumes nn: "\<forall>x\<in>A. (0::'a::{pordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
```
```  1510   shows "0 \<le> setsum f A"
```
```  1511 proof (cases "finite A")
```
```  1512   case True thus ?thesis using nn
```
```  1513   proof induct
```
```  1514     case empty then show ?case by simp
```
```  1515   next
```
```  1516     case (insert x F)
```
```  1517     then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
```
```  1518     with insert show ?case by simp
```
```  1519   qed
```
```  1520 next
```
```  1521   case False thus ?thesis by (simp add: setsum_def)
```
```  1522 qed
```
```  1523
```
```  1524 lemma setsum_nonpos:
```
```  1525   assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{pordered_ab_semigroup_add,comm_monoid_add})"
```
```  1526   shows "setsum f A \<le> 0"
```
```  1527 proof (cases "finite A")
```
```  1528   case True thus ?thesis using np
```
```  1529   proof induct
```
```  1530     case empty then show ?case by simp
```
```  1531   next
```
```  1532     case (insert x F)
```
```  1533     then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
```
```  1534     with insert show ?case by simp
```
```  1535   qed
```
```  1536 next
```
```  1537   case False thus ?thesis by (simp add: setsum_def)
```
```  1538 qed
```
```  1539
```
```  1540 lemma setsum_mono2:
```
```  1541 fixes f :: "'a \<Rightarrow> 'b :: {pordered_ab_semigroup_add_imp_le,comm_monoid_add}"
```
```  1542 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
```
```  1543 shows "setsum f A \<le> setsum f B"
```
```  1544 proof -
```
```  1545   have "setsum f A \<le> setsum f A + setsum f (B-A)"
```
```  1546     by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
```
```  1547   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
```
```  1548     by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
```
```  1549   also have "A \<union> (B-A) = B" using sub by blast
```
```  1550   finally show ?thesis .
```
```  1551 qed
```
```  1552
```
```  1553 lemma setsum_mono3: "finite B ==> A <= B ==>
```
```  1554     ALL x: B - A.
```
```  1555       0 <= ((f x)::'a::{comm_monoid_add,pordered_ab_semigroup_add}) ==>
```
```  1556         setsum f A <= setsum f B"
```
```  1557   apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
```
```  1558   apply (erule ssubst)
```
```  1559   apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
```
```  1560   apply simp
```
```  1561   apply (rule add_left_mono)
```
```  1562   apply (erule setsum_nonneg)
```
```  1563   apply (subst setsum_Un_disjoint [THEN sym])
```
```  1564   apply (erule finite_subset, assumption)
```
```  1565   apply (rule finite_subset)
```
```  1566   prefer 2
```
```  1567   apply assumption
```
```  1568   apply auto
```
```  1569   apply (rule setsum_cong)
```
```  1570   apply auto
```
```  1571 done
```
```  1572
```
```  1573 lemma setsum_right_distrib:
```
```  1574   fixes f :: "'a => ('b::semiring_0)"
```
```  1575   shows "r * setsum f A = setsum (%n. r * f n) A"
```
```  1576 proof (cases "finite A")
```
```  1577   case True
```
```  1578   thus ?thesis
```
```  1579   proof induct
```
```  1580     case empty thus ?case by simp
```
```  1581   next
```
```  1582     case (insert x A) thus ?case by (simp add: right_distrib)
```
```  1583   qed
```
```  1584 next
```
```  1585   case False thus ?thesis by (simp add: setsum_def)
```
```  1586 qed
```
```  1587
```
```  1588 lemma setsum_left_distrib:
```
```  1589   "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
```
```  1590 proof (cases "finite A")
```
```  1591   case True
```
```  1592   then show ?thesis
```
```  1593   proof induct
```
```  1594     case empty thus ?case by simp
```
```  1595   next
```
```  1596     case (insert x A) thus ?case by (simp add: left_distrib)
```
```  1597   qed
```
```  1598 next
```
```  1599   case False thus ?thesis by (simp add: setsum_def)
```
```  1600 qed
```
```  1601
```
```  1602 lemma setsum_divide_distrib:
```
```  1603   "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
```
```  1604 proof (cases "finite A")
```
```  1605   case True
```
```  1606   then show ?thesis
```
```  1607   proof induct
```
```  1608     case empty thus ?case by simp
```
```  1609   next
```
```  1610     case (insert x A) thus ?case by (simp add: add_divide_distrib)
```
```  1611   qed
```
```  1612 next
```
```  1613   case False thus ?thesis by (simp add: setsum_def)
```
```  1614 qed
```
```  1615
```
```  1616 lemma setsum_abs[iff]:
```
```  1617   fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
```
```  1618   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
```
```  1619 proof (cases "finite A")
```
```  1620   case True
```
```  1621   thus ?thesis
```
```  1622   proof induct
```
```  1623     case empty thus ?case by simp
```
```  1624   next
```
```  1625     case (insert x A)
```
```  1626     thus ?case by (auto intro: abs_triangle_ineq order_trans)
```
```  1627   qed
```
```  1628 next
```
```  1629   case False thus ?thesis by (simp add: setsum_def)
```
```  1630 qed
```
```  1631
```
```  1632 lemma setsum_abs_ge_zero[iff]:
```
```  1633   fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
```
```  1634   shows "0 \<le> setsum (%i. abs(f i)) A"
```
```  1635 proof (cases "finite A")
```
```  1636   case True
```
```  1637   thus ?thesis
```
```  1638   proof induct
```
```  1639     case empty thus ?case by simp
```
```  1640   next
```
```  1641     case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg)
```
```  1642   qed
```
```  1643 next
```
```  1644   case False thus ?thesis by (simp add: setsum_def)
```
```  1645 qed
```
```  1646
```
```  1647 lemma abs_setsum_abs[simp]:
```
```  1648   fixes f :: "'a => ('b::pordered_ab_group_add_abs)"
```
```  1649   shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
```
```  1650 proof (cases "finite A")
```
```  1651   case True
```
```  1652   thus ?thesis
```
```  1653   proof induct
```
```  1654     case empty thus ?case by simp
```
```  1655   next
```
```  1656     case (insert a A)
```
```  1657     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
```
```  1658     also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
```
```  1659     also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
```
```  1660       by (simp del: abs_of_nonneg)
```
```  1661     also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
```
```  1662     finally show ?case .
```
```  1663   qed
```
```  1664 next
```
```  1665   case False thus ?thesis by (simp add: setsum_def)
```
```  1666 qed
```
```  1667
```
```  1668
```
```  1669 lemma setsum_Plus:
```
```  1670   fixes A :: "'a set" and B :: "'b set"
```
```  1671   assumes fin: "finite A" "finite B"
```
```  1672   shows "setsum f (A <+> B) = setsum (f \<circ> Inl) A + setsum (f \<circ> Inr) B"
```
```  1673 proof -
```
```  1674   have "A <+> B = Inl ` A \<union> Inr ` B" by auto
```
```  1675   moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)"
```
```  1676     by(auto intro: finite_imageI)
```
```  1677   moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto
```
```  1678   moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI)
```
```  1679   ultimately show ?thesis using fin by(simp add: setsum_Un_disjoint setsum_reindex)
```
```  1680 qed
```
```  1681
```
```  1682
```
```  1683 text {* Commuting outer and inner summation *}
```
```  1684
```
```  1685 lemma swap_inj_on:
```
```  1686   "inj_on (%(i, j). (j, i)) (A \<times> B)"
```
```  1687   by (unfold inj_on_def) fast
```
```  1688
```
```  1689 lemma swap_product:
```
```  1690   "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
```
```  1691   by (simp add: split_def image_def) blast
```
```  1692
```
```  1693 lemma setsum_commute:
```
```  1694   "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
```
```  1695 proof (simp add: setsum_cartesian_product)
```
```  1696   have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
```
```  1697     (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
```
```  1698     (is "?s = _")
```
```  1699     apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on)
```
```  1700     apply (simp add: split_def)
```
```  1701     done
```
```  1702   also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
```
```  1703     (is "_ = ?t")
```
```  1704     apply (simp add: swap_product)
```
```  1705     done
```
```  1706   finally show "?s = ?t" .
```
```  1707 qed
```
```  1708
```
```  1709 lemma setsum_product:
```
```  1710   fixes f :: "'a => ('b::semiring_0)"
```
```  1711   shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
```
```  1712   by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
```
```  1713
```
```  1714
```
```  1715 subsection {* Generalized product over a set *}
```
```  1716
```
```  1717 definition setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
```
```  1718 where "setprod f A == if finite A then fold_image (op *) f 1 A else 1"
```
```  1719
```
```  1720 abbreviation
```
```  1721   Setprod  ("\<Prod>_" [1000] 999) where
```
```  1722   "\<Prod>A == setprod (%x. x) A"
```
```  1723
```
```  1724 syntax
```
```  1725   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
```
```  1726 syntax (xsymbols)
```
```  1727   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
```
```  1728 syntax (HTML output)
```
```  1729   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
```
```  1730
```
```  1731 translations -- {* Beware of argument permutation! *}
```
```  1732   "PROD i:A. b" == "CONST setprod (%i. b) A"
```
```  1733   "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A"
```
```  1734
```
```  1735 text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
```
```  1736  @{text"\<Prod>x|P. e"}. *}
```
```  1737
```
```  1738 syntax
```
```  1739   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
```
```  1740 syntax (xsymbols)
```
```  1741   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
```
```  1742 syntax (HTML output)
```
```  1743   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
```
```  1744
```
```  1745 translations
```
```  1746   "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
```
```  1747   "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
```
```  1748
```
```  1749
```
```  1750 lemma setprod_empty [simp]: "setprod f {} = 1"
```
```  1751 by (auto simp add: setprod_def)
```
```  1752
```
```  1753 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
```
```  1754     setprod f (insert a A) = f a * setprod f A"
```
```  1755 by (simp add: setprod_def)
```
```  1756
```
```  1757 lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
```
```  1758 by (simp add: setprod_def)
```
```  1759
```
```  1760 lemma setprod_reindex:
```
```  1761    "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
```
```  1762 by(auto simp: setprod_def fold_image_reindex dest!:finite_imageD)
```
```  1763
```
```  1764 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
```
```  1765 by (auto simp add: setprod_reindex)
```
```  1766
```
```  1767 lemma setprod_cong:
```
```  1768   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
```
```  1769 by(fastsimp simp: setprod_def intro: fold_image_cong)
```
```  1770
```
```  1771 lemma strong_setprod_cong[cong]:
```
```  1772   "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
```
```  1773 by(fastsimp simp: simp_implies_def setprod_def intro: fold_image_cong)
```
```  1774
```
```  1775 lemma setprod_reindex_cong: "inj_on f A ==>
```
```  1776     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
```
```  1777 by (frule setprod_reindex, simp)
```
```  1778
```
```  1779 lemma strong_setprod_reindex_cong: assumes i: "inj_on f A"
```
```  1780   and B: "B = f ` A" and eq: "\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x"
```
```  1781   shows "setprod h B = setprod g A"
```
```  1782 proof-
```
```  1783     have "setprod h B = setprod (h o f) A"
```
```  1784       by (simp add: B setprod_reindex[OF i, of h])
```
```  1785     then show ?thesis apply simp
```
```  1786       apply (rule setprod_cong)
```
```  1787       apply simp
```
```  1788       by (simp add: eq)
```
```  1789 qed
```
```  1790
```
```  1791 lemma setprod_Un_one:
```
```  1792   assumes fS: "finite S" and fT: "finite T"
```
```  1793   and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
```
```  1794   shows "setprod f (S \<union> T) = setprod f S  * setprod f T"
```
```  1795   using fS fT
```
```  1796   apply (simp add: setprod_def)
```
```  1797   apply (rule fold_image_Un_one)
```
```  1798   using I0 by auto
```
```  1799
```
```  1800
```
```  1801 lemma setprod_1: "setprod (%i. 1) A = 1"
```
```  1802 apply (case_tac "finite A")
```
```  1803 apply (erule finite_induct, auto simp add: mult_ac)
```
```  1804 done
```
```  1805
```
```  1806 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
```
```  1807 apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
```
```  1808 apply (erule ssubst, rule setprod_1)
```
```  1809 apply (rule setprod_cong, auto)
```
```  1810 done
```
```  1811
```
```  1812 lemma setprod_Un_Int: "finite A ==> finite B
```
```  1813     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
```
```  1814 by(simp add: setprod_def fold_image_Un_Int[symmetric])
```
```  1815
```
```  1816 lemma setprod_Un_disjoint: "finite A ==> finite B
```
```  1817   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
```
```  1818 by (subst setprod_Un_Int [symmetric], auto)
```
```  1819
```
```  1820 lemma setprod_mono_one_left:
```
```  1821   assumes fT: "finite T" and ST: "S \<subseteq> T"
```
```  1822   and z: "\<forall>i \<in> T - S. f i = 1"
```
```  1823   shows "setprod f S = setprod f T"
```
```  1824 proof-
```
```  1825   have eq: "T = S \<union> (T - S)" using ST by blast
```
```  1826   have d: "S \<inter> (T - S) = {}" using ST by blast
```
```  1827   from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
```
```  1828   show ?thesis
```
```  1829   by (simp add: setprod_Un_disjoint[OF f d, unfolded eq[symmetric]] setprod_1'[OF z])
```
```  1830 qed
```
```  1831
```
```  1832 lemmas setprod_mono_one_right = setprod_mono_one_left [THEN sym]
```
```  1833
```
```  1834 lemma setprod_delta:
```
```  1835   assumes fS: "finite S"
```
```  1836   shows "setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
```
```  1837 proof-
```
```  1838   let ?f = "(\<lambda>k. if k=a then b k else 1)"
```
```  1839   {assume a: "a \<notin> S"
```
```  1840     hence "\<forall> k\<in> S. ?f k = 1" by simp
```
```  1841     hence ?thesis  using a by (simp add: setprod_1 cong add: setprod_cong) }
```
```  1842   moreover
```
```  1843   {assume a: "a \<in> S"
```
```  1844     let ?A = "S - {a}"
```
```  1845     let ?B = "{a}"
```
```  1846     have eq: "S = ?A \<union> ?B" using a by blast
```
```  1847     have dj: "?A \<inter> ?B = {}" by simp
```
```  1848     from fS have fAB: "finite ?A" "finite ?B" by auto
```
```  1849     have fA1: "setprod ?f ?A = 1" apply (rule setprod_1') by auto
```
```  1850     have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
```
```  1851       using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
```
```  1852       by simp
```
```  1853     then have ?thesis  using a by (simp add: fA1 cong add: setprod_cong cong del: if_weak_cong)}
```
```  1854   ultimately show ?thesis by blast
```
```  1855 qed
```
```  1856
```
```  1857 lemma setprod_delta':
```
```  1858   assumes fS: "finite S" shows
```
```  1859   "setprod (\<lambda>k. if a = k then b k else 1) S =
```
```  1860      (if a\<in> S then b a else 1)"
```
```  1861   using setprod_delta[OF fS, of a b, symmetric]
```
```  1862   by (auto intro: setprod_cong)
```
```  1863
```
```  1864
```
```  1865 lemma setprod_UN_disjoint:
```
```  1866     "finite I ==> (ALL i:I. finite (A i)) ==>
```
```  1867         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
```
```  1868       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
```
```  1869 by(simp add: setprod_def fold_image_UN_disjoint cong: setprod_cong)
```
```  1870
```
```  1871 lemma setprod_Union_disjoint:
```
```  1872   "[| (ALL A:C. finite A);
```
```  1873       (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
```
```  1874    ==> setprod f (Union C) = setprod (setprod f) C"
```
```  1875 apply (cases "finite C")
```
```  1876  prefer 2 apply (force dest: finite_UnionD simp add: setprod_def)
```
```  1877   apply (frule setprod_UN_disjoint [of C id f])
```
```  1878  apply (unfold Union_def id_def, assumption+)
```
```  1879 done
```
```  1880
```
```  1881 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
```
```  1882     (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
```
```  1883     (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
```
```  1884 by(simp add:setprod_def fold_image_Sigma split_def cong:setprod_cong)
```
```  1885
```
```  1886 text{*Here we can eliminate the finiteness assumptions, by cases.*}
```
```  1887 lemma setprod_cartesian_product:
```
```  1888      "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
```
```  1889 apply (cases "finite A")
```
```  1890  apply (cases "finite B")
```
```  1891   apply (simp add: setprod_Sigma)
```
```  1892  apply (cases "A={}", simp)
```
```  1893  apply (simp add: setprod_1)
```
```  1894 apply (auto simp add: setprod_def
```
```  1895             dest: finite_cartesian_productD1 finite_cartesian_productD2)
```
```  1896 done
```
```  1897
```
```  1898 lemma setprod_timesf:
```
```  1899      "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
```
```  1900 by(simp add:setprod_def fold_image_distrib)
```
```  1901
```
```  1902
```
```  1903 subsubsection {* Properties in more restricted classes of structures *}
```
```  1904
```
```  1905 lemma setprod_eq_1_iff [simp]:
```
```  1906   "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
```
```  1907 by (induct set: finite) auto
```
```  1908
```
```  1909 lemma setprod_zero:
```
```  1910      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
```
```  1911 apply (induct set: finite, force, clarsimp)
```
```  1912 apply (erule disjE, auto)
```
```  1913 done
```
```  1914
```
```  1915 lemma setprod_nonneg [rule_format]:
```
```  1916    "(ALL x: A. (0::'a::ordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
```
```  1917 by (cases "finite A", induct set: finite, simp_all add: mult_nonneg_nonneg)
```
```  1918
```
```  1919 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_semidom) < f x)
```
```  1920   --> 0 < setprod f A"
```
```  1921 by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos)
```
```  1922
```
```  1923 lemma setprod_zero_iff[simp]: "finite A ==>
```
```  1924   (setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) =
```
```  1925   (EX x: A. f x = 0)"
```
```  1926 by (erule finite_induct, auto simp:no_zero_divisors)
```
```  1927
```
```  1928 lemma setprod_pos_nat:
```
```  1929   "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
```
```  1930 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
```
```  1931
```
```  1932 lemma setprod_pos_nat_iff[simp]:
```
```  1933   "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
```
```  1934 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
```
```  1935
```
```  1936 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
```
```  1937   (setprod f (A Un B) :: 'a ::{field})
```
```  1938    = setprod f A * setprod f B / setprod f (A Int B)"
```
```  1939 by (subst setprod_Un_Int [symmetric], auto)
```
```  1940
```
```  1941 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
```
```  1942   (setprod f (A - {a}) :: 'a :: {field}) =
```
```  1943   (if a:A then setprod f A / f a else setprod f A)"
```
```  1944 by (erule finite_induct) (auto simp add: insert_Diff_if)
```
```  1945
```
```  1946 lemma setprod_inversef:
```
```  1947   fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}"
```
```  1948   shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)"
```
```  1949 by (erule finite_induct) auto
```
```  1950
```
```  1951 lemma setprod_dividef:
```
```  1952   fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}"
```
```  1953   shows "finite A
```
```  1954     ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
```
```  1955 apply (subgoal_tac
```
```  1956          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
```
```  1957 apply (erule ssubst)
```
```  1958 apply (subst divide_inverse)
```
```  1959 apply (subst setprod_timesf)
```
```  1960 apply (subst setprod_inversef, assumption+, rule refl)
```
```  1961 apply (rule setprod_cong, rule refl)
```
```  1962 apply (subst divide_inverse, auto)
```
```  1963 done
```
```  1964
```
```  1965 lemma setprod_dvd_setprod [rule_format]:
```
```  1966     "(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A"
```
```  1967   apply (cases "finite A")
```
```  1968   apply (induct set: finite)
```
```  1969   apply (auto simp add: dvd_def)
```
```  1970   apply (rule_tac x = "k * ka" in exI)
```
```  1971   apply (simp add: algebra_simps)
```
```  1972 done
```
```  1973
```
```  1974 lemma setprod_dvd_setprod_subset:
```
```  1975   "finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B"
```
```  1976   apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)")
```
```  1977   apply (unfold dvd_def, blast)
```
```  1978   apply (subst setprod_Un_disjoint [symmetric])
```
```  1979   apply (auto elim: finite_subset intro: setprod_cong)
```
```  1980 done
```
```  1981
```
```  1982 lemma setprod_dvd_setprod_subset2:
```
```  1983   "finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow>
```
```  1984       setprod f A dvd setprod g B"
```
```  1985   apply (rule dvd_trans)
```
```  1986   apply (rule setprod_dvd_setprod, erule (1) bspec)
```
```  1987   apply (erule (1) setprod_dvd_setprod_subset)
```
```  1988 done
```
```  1989
```
```  1990 lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow>
```
```  1991     (f i ::'a::comm_semiring_1) dvd setprod f A"
```
```  1992 by (induct set: finite) (auto intro: dvd_mult)
```
```  1993
```
```  1994 lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow>
```
```  1995     (d::'a::comm_semiring_1) dvd (SUM x : A. f x)"
```
```  1996   apply (cases "finite A")
```
```  1997   apply (induct set: finite)
```
```  1998   apply auto
```
```  1999 done
```
```  2000
```
```  2001
```
```  2002 subsection {* Finite cardinality *}
```
```  2003
```
```  2004 text {* This definition, although traditional, is ugly to work with:
```
```  2005 @{text "card A == LEAST n. EX f. A = {f i | i. i < n}"}.
```
```  2006 But now that we have @{text setsum} things are easy:
```
```  2007 *}
```
```  2008
```
```  2009 definition card :: "'a set \<Rightarrow> nat" where
```
```  2010   "card A = setsum (\<lambda>x. 1) A"
```
```  2011
```
```  2012 lemmas card_eq_setsum = card_def
```
```  2013
```
```  2014 lemma card_empty [simp]: "card {} = 0"
```
```  2015   by (simp add: card_def)
```
```  2016
```
```  2017 lemma card_insert_disjoint [simp]:
```
```  2018   "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
```
```  2019   by (simp add: card_def)
```
```  2020
```
```  2021 lemma card_insert_if:
```
```  2022   "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
```
```  2023   by (simp add: insert_absorb)
```
```  2024
```
```  2025 lemma card_infinite [simp]: "~ finite A ==> card A = 0"
```
```  2026   by (simp add: card_def)
```
```  2027
```
```  2028 lemma card_ge_0_finite:
```
```  2029   "card A > 0 \<Longrightarrow> finite A"
```
```  2030   by (rule ccontr) simp
```
```  2031
```
```  2032 lemma card_0_eq [simp,noatp]: "finite A ==> (card A = 0) = (A = {})"
```
```  2033   apply auto
```
```  2034   apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
```
```  2035   done
```
```  2036
```
```  2037 lemma finite_UNIV_card_ge_0:
```
```  2038   "finite (UNIV :: 'a set) \<Longrightarrow> card (UNIV :: 'a set) > 0"
```
```  2039   by (rule ccontr) simp
```
```  2040
```
```  2041 lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
```
```  2042   by auto
```
```  2043
```
```  2044 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
```
```  2045 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
```
```  2046 apply(simp del:insert_Diff_single)
```
```  2047 done
```
```  2048
```
```  2049 lemma card_Diff_singleton:
```
```  2050   "finite A ==> x: A ==> card (A - {x}) = card A - 1"
```
```  2051 by (simp add: card_Suc_Diff1 [symmetric])
```
```  2052
```
```  2053 lemma card_Diff_singleton_if:
```
```  2054   "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
```
```  2055 by (simp add: card_Diff_singleton)
```
```  2056
```
```  2057 lemma card_Diff_insert[simp]:
```
```  2058 assumes "finite A" and "a:A" and "a ~: B"
```
```  2059 shows "card(A - insert a B) = card(A - B) - 1"
```
```  2060 proof -
```
```  2061   have "A - insert a B = (A - B) - {a}" using assms by blast
```
```  2062   then show ?thesis using assms by(simp add:card_Diff_singleton)
```
```  2063 qed
```
```  2064
```
```  2065 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
```
```  2066 by (simp add: card_insert_if card_Suc_Diff1 del:card_Diff_insert)
```
```  2067
```
```  2068 lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
```
```  2069 by (simp add: card_insert_if)
```
```  2070
```
```  2071 lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
```
```  2072 by (simp add: card_def setsum_mono2)
```
```  2073
```
```  2074 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
```
```  2075 apply (induct set: finite, simp, clarify)
```
```  2076 apply (subgoal_tac "finite A & A - {x} <= F")
```
```  2077  prefer 2 apply (blast intro: finite_subset, atomize)
```
```  2078 apply (drule_tac x = "A - {x}" in spec)
```
```  2079 apply (simp add: card_Diff_singleton_if split add: split_if_asm)
```
```  2080 apply (case_tac "card A", auto)
```
```  2081 done
```
```  2082
```
```  2083 lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
```
```  2084 apply (simp add: psubset_eq linorder_not_le [symmetric])
```
```  2085 apply (blast dest: card_seteq)
```
```  2086 done
```
```  2087
```
```  2088 lemma card_Un_Int: "finite A ==> finite B
```
```  2089     ==> card A + card B = card (A Un B) + card (A Int B)"
```
```  2090 by(simp add:card_def setsum_Un_Int)
```
```  2091
```
```  2092 lemma card_Un_disjoint: "finite A ==> finite B
```
```  2093     ==> A Int B = {} ==> card (A Un B) = card A + card B"
```
```  2094 by (simp add: card_Un_Int)
```
```  2095
```
```  2096 lemma card_Diff_subset:
```
```  2097   "finite B ==> B <= A ==> card (A - B) = card A - card B"
```
```  2098 by(simp add:card_def setsum_diff_nat)
```
```  2099
```
```  2100 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
```
```  2101 apply (rule Suc_less_SucD)
```
```  2102 apply (simp add: card_Suc_Diff1 del:card_Diff_insert)
```
```  2103 done
```
```  2104
```
```  2105 lemma card_Diff2_less:
```
```  2106   "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
```
```  2107 apply (case_tac "x = y")
```
```  2108  apply (simp add: card_Diff1_less del:card_Diff_insert)
```
```  2109 apply (rule less_trans)
```
```  2110  prefer 2 apply (auto intro!: card_Diff1_less simp del:card_Diff_insert)
```
```  2111 done
```
```  2112
```
```  2113 lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
```
```  2114 apply (case_tac "x : A")
```
```  2115  apply (simp_all add: card_Diff1_less less_imp_le)
```
```  2116 done
```
```  2117
```
```  2118 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
```
```  2119 by (erule psubsetI, blast)
```
```  2120
```
```  2121 lemma insert_partition:
```
```  2122   "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
```
```  2123   \<Longrightarrow> x \<inter> \<Union> F = {}"
```
```  2124 by auto
```
```  2125
```
```  2126 lemma finite_psubset_induct[consumes 1, case_names psubset]:
```
```  2127   assumes "finite A" and "!!A. finite A \<Longrightarrow> (!!B. finite B \<Longrightarrow> B \<subset> A \<Longrightarrow> P(B)) \<Longrightarrow> P(A)" shows "P A"
```
```  2128 using assms(1)
```
```  2129 proof (induct A rule: measure_induct_rule[where f=card])
```
```  2130   case (less A)
```
```  2131   show ?case
```
```  2132   proof(rule assms(2)[OF less(2)])
```
```  2133     fix B assume "finite B" "B \<subset> A"
```
```  2134     show "P B" by(rule less(1)[OF psubset_card_mono[OF less(2) `B \<subset> A`] `finite B`])
```
```  2135   qed
```
```  2136 qed
```
```  2137
```
```  2138 text{* main cardinality theorem *}
```
```  2139 lemma card_partition [rule_format]:
```
```  2140   "finite C ==>
```
```  2141      finite (\<Union> C) -->
```
```  2142      (\<forall>c\<in>C. card c = k) -->
```
```  2143      (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->
```
```  2144      k * card(C) = card (\<Union> C)"
```
```  2145 apply (erule finite_induct, simp)
```
```  2146 apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition
```
```  2147        finite_subset [of _ "\<Union> (insert x F)"])
```
```  2148 done
```
```  2149
```
```  2150 lemma card_eq_UNIV_imp_eq_UNIV:
```
```  2151   assumes fin: "finite (UNIV :: 'a set)"
```
```  2152   and card: "card A = card (UNIV :: 'a set)"
```
```  2153   shows "A = (UNIV :: 'a set)"
```
```  2154 proof
```
```  2155   show "A \<subseteq> UNIV" by simp
```
```  2156   show "UNIV \<subseteq> A"
```
```  2157   proof
```
```  2158     fix x
```
```  2159     show "x \<in> A"
```
```  2160     proof (rule ccontr)
```
```  2161       assume "x \<notin> A"
```
```  2162       then have "A \<subset> UNIV" by auto
```
```  2163       with fin have "card A < card (UNIV :: 'a set)" by (fact psubset_card_mono)
```
```  2164       with card show False by simp
```
```  2165     qed
```
```  2166   qed
```
```  2167 qed
```
```  2168
```
```  2169 text{*The form of a finite set of given cardinality*}
```
```  2170
```
```  2171 lemma card_eq_SucD:
```
```  2172 assumes "card A = Suc k"
```
```  2173 shows "\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={})"
```
```  2174 proof -
```
```  2175   have fin: "finite A" using assms by (auto intro: ccontr)
```
```  2176   moreover have "card A \<noteq> 0" using assms by auto
```
```  2177   ultimately obtain b where b: "b \<in> A" by auto
```
```  2178   show ?thesis
```
```  2179   proof (intro exI conjI)
```
```  2180     show "A = insert b (A-{b})" using b by blast
```
```  2181     show "b \<notin> A - {b}" by blast
```
```  2182     show "card (A - {b}) = k" and "k = 0 \<longrightarrow> A - {b} = {}"
```
```  2183       using assms b fin by(fastsimp dest:mk_disjoint_insert)+
```
```  2184   qed
```
```  2185 qed
```
```  2186
```
```  2187 lemma card_Suc_eq:
```
```  2188   "(card A = Suc k) =
```
```  2189    (\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={}))"
```
```  2190 apply(rule iffI)
```
```  2191  apply(erule card_eq_SucD)
```
```  2192 apply(auto)
```
```  2193 apply(subst card_insert)
```
```  2194  apply(auto intro:ccontr)
```
```  2195 done
```
```  2196
```
```  2197 lemma finite_fun_UNIVD2:
```
```  2198   assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
```
```  2199   shows "finite (UNIV :: 'b set)"
```
```  2200 proof -
```
```  2201   from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))"
```
```  2202     by(rule finite_imageI)
```
```  2203   moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary)"
```
```  2204     by(rule UNIV_eq_I) auto
```
```  2205   ultimately show "finite (UNIV :: 'b set)" by simp
```
```  2206 qed
```
```  2207
```
```  2208 lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
```
```  2209 apply (cases "finite A")
```
```  2210 apply (erule finite_induct)
```
```  2211 apply (auto simp add: algebra_simps)
```
```  2212 done
```
```  2213
```
```  2214 lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
```
```  2215 apply (erule finite_induct)
```
```  2216 apply (auto simp add: power_Suc)
```
```  2217 done
```
```  2218
```
```  2219 lemma setprod_gen_delta:
```
```  2220   assumes fS: "finite S"
```
```  2221   shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::{comm_monoid_mult}) * c^ (card S - 1) else c^ card S)"
```
```  2222 proof-
```
```  2223   let ?f = "(\<lambda>k. if k=a then b k else c)"
```
```  2224   {assume a: "a \<notin> S"
```
```  2225     hence "\<forall> k\<in> S. ?f k = c" by simp
```
```  2226     hence ?thesis  using a setprod_constant[OF fS, of c] by (simp add: setprod_1 cong add: setprod_cong) }
```
```  2227   moreover
```
```  2228   {assume a: "a \<in> S"
```
```  2229     let ?A = "S - {a}"
```
```  2230     let ?B = "{a}"
```
```  2231     have eq: "S = ?A \<union> ?B" using a by blast
```
```  2232     have dj: "?A \<inter> ?B = {}" by simp
```
```  2233     from fS have fAB: "finite ?A" "finite ?B" by auto
```
```  2234     have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
```
```  2235       apply (rule setprod_cong) by auto
```
```  2236     have cA: "card ?A = card S - 1" using fS a by auto
```
```  2237     have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
```
```  2238     have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
```
```  2239       using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
```
```  2240       by simp
```
```  2241     then have ?thesis using a cA
```
```  2242       by (simp add: fA1 ring_simps cong add: setprod_cong cong del: if_weak_cong)}
```
```  2243   ultimately show ?thesis by blast
```
```  2244 qed
```
```  2245
```
```  2246
```
```  2247 lemma setsum_bounded:
```
```  2248   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, pordered_ab_semigroup_add})"
```
```  2249   shows "setsum f A \<le> of_nat(card A) * K"
```
```  2250 proof (cases "finite A")
```
```  2251   case True
```
```  2252   thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
```
```  2253 next
```
```  2254   case False thus ?thesis by (simp add: setsum_def)
```
```  2255 qed
```
```  2256
```
```  2257
```
```  2258 lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
```
```  2259   unfolding UNIV_unit by simp
```
```  2260
```
```  2261
```
```  2262 subsubsection {* Cardinality of unions *}
```
```  2263
```
```  2264 lemma card_UN_disjoint:
```
```  2265   "finite I ==> (ALL i:I. finite (A i)) ==>
```
```  2266    (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {})
```
```  2267    ==> card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
```
```  2268 apply (simp add: card_def del: setsum_constant)
```
```  2269 apply (subgoal_tac
```
```  2270          "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
```
```  2271 apply (simp add: setsum_UN_disjoint del: setsum_constant)
```
```  2272 apply (simp cong: setsum_cong)
```
```  2273 done
```
```  2274
```
```  2275 lemma card_Union_disjoint:
```
```  2276   "finite C ==> (ALL A:C. finite A) ==>
```
```  2277    (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
```
```  2278    ==> card (Union C) = setsum card C"
```
```  2279 apply (frule card_UN_disjoint [of C id])
```
```  2280 apply (unfold Union_def id_def, assumption+)
```
```  2281 done
```
```  2282
```
```  2283
```
```  2284 subsubsection {* Cardinality of image *}
```
```  2285
```
```  2286 text{*The image of a finite set can be expressed using @{term fold_image}.*}
```
```  2287 lemma image_eq_fold_image:
```
```  2288   "finite A ==> f ` A = fold_image (op Un) (%x. {f x}) {} A"
```
```  2289 proof (induct rule: finite_induct)
```
```  2290   case empty then show ?case by simp
```
```  2291 next
```
```  2292   interpret ab_semigroup_mult "op Un"
```
```  2293     proof qed auto
```
```  2294   case insert
```
```  2295   then show ?case by simp
```
```  2296 qed
```
```  2297
```
```  2298 lemma card_image_le: "finite A ==> card (f ` A) <= card A"
```
```  2299 apply (induct set: finite)
```
```  2300  apply simp
```
```  2301 apply (simp add: le_SucI finite_imageI card_insert_if)
```
```  2302 done
```
```  2303
```
```  2304 lemma card_image: "inj_on f A ==> card (f ` A) = card A"
```
```  2305 by(simp add:card_def setsum_reindex o_def del:setsum_constant)
```
```  2306
```
```  2307 lemma bij_betw_same_card: "bij_betw f A B \<Longrightarrow> card A = card B"
```
```  2308 by(auto simp: card_image bij_betw_def)
```
```  2309
```
```  2310 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
```
```  2311 by (simp add: card_seteq card_image)
```
```  2312
```
```  2313 lemma eq_card_imp_inj_on:
```
```  2314   "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
```
```  2315 apply (induct rule:finite_induct)
```
```  2316 apply simp
```
```  2317 apply(frule card_image_le[where f = f])
```
```  2318 apply(simp add:card_insert_if split:if_splits)
```
```  2319 done
```
```  2320
```
```  2321 lemma inj_on_iff_eq_card:
```
```  2322   "finite A ==> inj_on f A = (card(f ` A) = card A)"
```
```  2323 by(blast intro: card_image eq_card_imp_inj_on)
```
```  2324
```
```  2325
```
```  2326 lemma card_inj_on_le:
```
```  2327   "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
```
```  2328 apply (subgoal_tac "finite A")
```
```  2329  apply (force intro: card_mono simp add: card_image [symmetric])
```
```  2330 apply (blast intro: finite_imageD dest: finite_subset)
```
```  2331 done
```
```  2332
```
```  2333 lemma card_bij_eq:
```
```  2334   "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
```
```  2335      finite A; finite B |] ==> card A = card B"
```
```  2336 by (auto intro: le_anti_sym card_inj_on_le)
```
```  2337
```
```  2338
```
```  2339 subsubsection {* Cardinality of products *}
```
```  2340
```
```  2341 (*
```
```  2342 lemma SigmaI_insert: "y \<notin> A ==>
```
```  2343   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
```
```  2344   by auto
```
```  2345 *)
```
```  2346
```
```  2347 lemma card_SigmaI [simp]:
```
```  2348   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
```
```  2349   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
```
```  2350 by(simp add:card_def setsum_Sigma del:setsum_constant)
```
```  2351
```
```  2352 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
```
```  2353 apply (cases "finite A")
```
```  2354 apply (cases "finite B")
```
```  2355 apply (auto simp add: card_eq_0_iff
```
```  2356             dest: finite_cartesian_productD1 finite_cartesian_productD2)
```
```  2357 done
```
```  2358
```
```  2359 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
```
```  2360 by (simp add: card_cartesian_product)
```
```  2361
```
```  2362
```
```  2363 subsubsection {* Cardinality of sums *}
```
```  2364
```
```  2365 lemma card_Plus:
```
```  2366   assumes "finite A" and "finite B"
```
```  2367   shows "card (A <+> B) = card A + card B"
```
```  2368 proof -
```
```  2369   have "Inl`A \<inter> Inr`B = {}" by fast
```
```  2370   with assms show ?thesis
```
```  2371     unfolding Plus_def
```
```  2372     by (simp add: card_Un_disjoint card_image)
```
```  2373 qed
```
```  2374
```
```  2375 lemma card_Plus_conv_if:
```
```  2376   "card (A <+> B) = (if finite A \<and> finite B then card(A) + card(B) else 0)"
```
```  2377 by(auto simp: card_def setsum_Plus simp del: setsum_constant)
```
```  2378
```
```  2379
```
```  2380 subsubsection {* Cardinality of the Powerset *}
```
```  2381
```
```  2382 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
```
```  2383 apply (induct set: finite)
```
```  2384  apply (simp_all add: Pow_insert)
```
```  2385 apply (subst card_Un_disjoint, blast)
```
```  2386   apply (blast intro: finite_imageI, blast)
```
```  2387 apply (subgoal_tac "inj_on (insert x) (Pow F)")
```
```  2388  apply (simp add: card_image Pow_insert)
```
```  2389 apply (unfold inj_on_def)
```
```  2390 apply (blast elim!: equalityE)
```
```  2391 done
```
```  2392
```
```  2393 text {* Relates to equivalence classes.  Based on a theorem of F. Kammüller.  *}
```
```  2394
```
```  2395 lemma dvd_partition:
```
```  2396   "finite (Union C) ==>
```
```  2397     ALL c : C. k dvd card c ==>
```
```  2398     (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
```
```  2399   k dvd card (Union C)"
```
```  2400 apply(frule finite_UnionD)
```
```  2401 apply(rotate_tac -1)
```
```  2402 apply (induct set: finite, simp_all, clarify)
```
```  2403 apply (subst card_Un_disjoint)
```
```  2404    apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
```
```  2405 done
```
```  2406
```
```  2407
```
```  2408 subsubsection {* Relating injectivity and surjectivity *}
```
```  2409
```
```  2410 lemma finite_surj_inj: "finite(A) \<Longrightarrow> A <= f`A \<Longrightarrow> inj_on f A"
```
```  2411 apply(rule eq_card_imp_inj_on, assumption)
```
```  2412 apply(frule finite_imageI)
```
```  2413 apply(drule (1) card_seteq)
```
```  2414  apply(erule card_image_le)
```
```  2415 apply simp
```
```  2416 done
```
```  2417
```
```  2418 lemma finite_UNIV_surj_inj: fixes f :: "'a \<Rightarrow> 'a"
```
```  2419 shows "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
```
```  2420 by (blast intro: finite_surj_inj subset_UNIV dest:surj_range)
```
```  2421
```
```  2422 lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a"
```
```  2423 shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
```
```  2424 by(fastsimp simp:surj_def dest!: endo_inj_surj)
```
```  2425
```
```  2426 corollary infinite_UNIV_nat[iff]: "~finite(UNIV::nat set)"
```
```  2427 proof
```
```  2428   assume "finite(UNIV::nat set)"
```
```  2429   with finite_UNIV_inj_surj[of Suc]
```
```  2430   show False by simp (blast dest: Suc_neq_Zero surjD)
```
```  2431 qed
```
```  2432
```
```  2433 (* Often leads to bogus ATP proofs because of reduced type information, hence noatp *)
```
```  2434 lemma infinite_UNIV_char_0[noatp]:
```
```  2435   "\<not> finite (UNIV::'a::semiring_char_0 set)"
```
```  2436 proof
```
```  2437   assume "finite (UNIV::'a set)"
```
```  2438   with subset_UNIV have "finite (range of_nat::'a set)"
```
```  2439     by (rule finite_subset)
```
```  2440   moreover have "inj (of_nat::nat \<Rightarrow> 'a)"
```
```  2441     by (simp add: inj_on_def)
```
```  2442   ultimately have "finite (UNIV::nat set)"
```
```  2443     by (rule finite_imageD)
```
```  2444   then show "False"
```
```  2445     by (simp add: infinite_UNIV_nat)
```
```  2446 qed
```
```  2447
```
```  2448 subsection{* A fold functional for non-empty sets *}
```
```  2449
```
```  2450 text{* Does not require start value. *}
```
```  2451
```
```  2452 inductive
```
```  2453   fold1Set :: "('a => 'a => 'a) => 'a set => 'a => bool"
```
```  2454   for f :: "'a => 'a => 'a"
```
```  2455 where
```
```  2456   fold1Set_insertI [intro]:
```
```  2457    "\<lbrakk> fold_graph f a A x; a \<notin> A \<rbrakk> \<Longrightarrow> fold1Set f (insert a A) x"
```
```  2458
```
```  2459 constdefs
```
```  2460   fold1 :: "('a => 'a => 'a) => 'a set => 'a"
```
```  2461   "fold1 f A == THE x. fold1Set f A x"
```
```  2462
```
```  2463 lemma fold1Set_nonempty:
```
```  2464   "fold1Set f A x \<Longrightarrow> A \<noteq> {}"
```
```  2465 by(erule fold1Set.cases, simp_all)
```
```  2466
```
```  2467 inductive_cases empty_fold1SetE [elim!]: "fold1Set f {} x"
```
```  2468
```
```  2469 inductive_cases insert_fold1SetE [elim!]: "fold1Set f (insert a X) x"
```
```  2470
```
```  2471
```
```  2472 lemma fold1Set_sing [iff]: "(fold1Set f {a} b) = (a = b)"
```
```  2473 by (blast intro: fold_graph.intros elim: fold_graph.cases)
```
```  2474
```
```  2475 lemma fold1_singleton [simp]: "fold1 f {a} = a"
```
```  2476 by (unfold fold1_def) blast
```
```  2477
```
```  2478 lemma finite_nonempty_imp_fold1Set:
```
```  2479   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. fold1Set f A x"
```
```  2480 apply (induct A rule: finite_induct)
```
```  2481 apply (auto dest: finite_imp_fold_graph [of _ f])
```
```  2482 done
```
```  2483
```
```  2484 text{*First, some lemmas about @{const fold_graph}.*}
```
```  2485
```
```  2486 context ab_semigroup_mult
```
```  2487 begin
```
```  2488
```
```  2489 lemma fun_left_comm: "fun_left_comm(op *)"
```
```  2490 by unfold_locales (simp add: mult_ac)
```
```  2491
```
```  2492 lemma fold_graph_insert_swap:
```
```  2493 assumes fold: "fold_graph times (b::'a) A y" and "b \<notin> A"
```
```  2494 shows "fold_graph times z (insert b A) (z * y)"
```
```  2495 proof -
```
```  2496   interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
```
```  2497 from assms show ?thesis
```
```  2498 proof (induct rule: fold_graph.induct)
```
```  2499   case emptyI thus ?case by (force simp add: fold_insert_aux mult_commute)
```
```  2500 next
```
```  2501   case (insertI x A y)
```
```  2502     have "fold_graph times z (insert x (insert b A)) (x * (z * y))"
```
```  2503       using insertI by force  --{*how does @{term id} get unfolded?*}
```
```  2504     thus ?case by (simp add: insert_commute mult_ac)
```
```  2505 qed
```
```  2506 qed
```
```  2507
```
```  2508 lemma fold_graph_permute_diff:
```
```  2509 assumes fold: "fold_graph times b A x"
```
```  2510 shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> fold_graph times a (insert b (A-{a})) x"
```
```  2511 using fold
```
```  2512 proof (induct rule: fold_graph.induct)
```
```  2513   case emptyI thus ?case by simp
```
```  2514 next
```
```  2515   case (insertI x A y)
```
```  2516   have "a = x \<or> a \<in> A" using insertI by simp
```
```  2517   thus ?case
```
```  2518   proof
```
```  2519     assume "a = x"
```
```  2520     with insertI show ?thesis
```
```  2521       by (simp add: id_def [symmetric], blast intro: fold_graph_insert_swap)
```
```  2522   next
```
```  2523     assume ainA: "a \<in> A"
```
```  2524     hence "fold_graph times a (insert x (insert b (A - {a}))) (x * y)"
```
```  2525       using insertI by force
```
```  2526     moreover
```
```  2527     have "insert x (insert b (A - {a})) = insert b (insert x A - {a})"
```
```  2528       using ainA insertI by blast
```
```  2529     ultimately show ?thesis by simp
```
```  2530   qed
```
```  2531 qed
```
```  2532
```
```  2533 lemma fold1_eq_fold:
```
```  2534 assumes "finite A" "a \<notin> A" shows "fold1 times (insert a A) = fold times a A"
```
```  2535 proof -
```
```  2536   interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
```
```  2537   from assms show ?thesis
```
```  2538 apply (simp add: fold1_def fold_def)
```
```  2539 apply (rule the_equality)
```
```  2540 apply (best intro: fold_graph_determ theI dest: finite_imp_fold_graph [of _ times])
```
```  2541 apply (rule sym, clarify)
```
```  2542 apply (case_tac "Aa=A")
```
```  2543  apply (best intro: the_equality fold_graph_determ)
```
```  2544 apply (subgoal_tac "fold_graph times a A x")
```
```  2545  apply (best intro: the_equality fold_graph_determ)
```
```  2546 apply (subgoal_tac "insert aa (Aa - {a}) = A")
```
```  2547  prefer 2 apply (blast elim: equalityE)
```
```  2548 apply (auto dest: fold_graph_permute_diff [where a=a])
```
```  2549 done
```
```  2550 qed
```
```  2551
```
```  2552 lemma nonempty_iff: "(A \<noteq> {}) = (\<exists>x B. A = insert x B & x \<notin> B)"
```
```  2553 apply safe
```
```  2554  apply simp
```
```  2555  apply (drule_tac x=x in spec)
```
```  2556  apply (drule_tac x="A-{x}" in spec, auto)
```
```  2557 done
```
```  2558
```
```  2559 lemma fold1_insert:
```
```  2560   assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A"
```
```  2561   shows "fold1 times (insert x A) = x * fold1 times A"
```
```  2562 proof -
```
```  2563   interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
```
```  2564   from nonempty obtain a A' where "A = insert a A' & a ~: A'"
```
```  2565     by (auto simp add: nonempty_iff)
```
```  2566   with A show ?thesis
```
```  2567     by (simp add: insert_commute [of x] fold1_eq_fold eq_commute)
```
```  2568 qed
```
```  2569
```
```  2570 end
```
```  2571
```
```  2572 context ab_semigroup_idem_mult
```
```  2573 begin
```
```  2574
```
```  2575 lemma fold1_insert_idem [simp]:
```
```  2576   assumes nonempty: "A \<noteq> {}" and A: "finite A"
```
```  2577   shows "fold1 times (insert x A) = x * fold1 times A"
```
```  2578 proof -
```
```  2579   interpret fun_left_comm_idem "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"
```
```  2580     by (rule fun_left_comm_idem)
```
```  2581   from nonempty obtain a A' where A': "A = insert a A' & a ~: A'"
```
```  2582     by (auto simp add: nonempty_iff)
```
```  2583   show ?thesis
```
```  2584   proof cases
```
```  2585     assume "a = x"
```
```  2586     thus ?thesis
```
```  2587     proof cases
```
```  2588       assume "A' = {}"
```
```  2589       with prems show ?thesis by (simp add: mult_idem)
```
```  2590     next
```
```  2591       assume "A' \<noteq> {}"
```
```  2592       with prems show ?thesis
```
```  2593 	by (simp add: fold1_insert mult_assoc [symmetric] mult_idem)
```
```  2594     qed
```
```  2595   next
```
```  2596     assume "a \<noteq> x"
```
```  2597     with prems show ?thesis
```
```  2598       by (simp add: insert_commute fold1_eq_fold fold_insert_idem)
```
```  2599   qed
```
```  2600 qed
```
```  2601
```
```  2602 lemma hom_fold1_commute:
```
```  2603 assumes hom: "!!x y. h (x * y) = h x * h y"
```
```  2604 and N: "finite N" "N \<noteq> {}" shows "h (fold1 times N) = fold1 times (h ` N)"
```
```  2605 using N proof (induct rule: finite_ne_induct)
```
```  2606   case singleton thus ?case by simp
```
```  2607 next
```
```  2608   case (insert n N)
```
```  2609   then have "h (fold1 times (insert n N)) = h (n * fold1 times N)" by simp
```
```  2610   also have "\<dots> = h n * h (fold1 times N)" by(rule hom)
```
```  2611   also have "h (fold1 times N) = fold1 times (h ` N)" by(rule insert)
```
```  2612   also have "times (h n) \<dots> = fold1 times (insert (h n) (h ` N))"
```
```  2613     using insert by(simp)
```
```  2614   also have "insert (h n) (h ` N) = h ` insert n N" by simp
```
```  2615   finally show ?case .
```
```  2616 qed
```
```  2617
```
```  2618 end
```
```  2619
```
```  2620
```
```  2621 text{* Now the recursion rules for definitions: *}
```
```  2622
```
```  2623 lemma fold1_singleton_def: "g = fold1 f \<Longrightarrow> g {a} = a"
```
```  2624 by(simp add:fold1_singleton)
```
```  2625
```
```  2626 lemma (in ab_semigroup_mult) fold1_insert_def:
```
```  2627   "\<lbrakk> g = fold1 times; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A"
```
```  2628 by (simp add:fold1_insert)
```
```  2629
```
```  2630 lemma (in ab_semigroup_idem_mult) fold1_insert_idem_def:
```
```  2631   "\<lbrakk> g = fold1 times; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g (insert x A) = x * g A"
```
```  2632 by simp
```
```  2633
```
```  2634 subsubsection{* Determinacy for @{term fold1Set} *}
```
```  2635
```
```  2636 (*Not actually used!!*)
```
```  2637 (*
```
```  2638 context ab_semigroup_mult
```
```  2639 begin
```
```  2640
```
```  2641 lemma fold_graph_permute:
```
```  2642   "[|fold_graph times id b (insert a A) x; a \<notin> A; b \<notin> A|]
```
```  2643    ==> fold_graph times id a (insert b A) x"
```
```  2644 apply (cases "a=b")
```
```  2645 apply (auto dest: fold_graph_permute_diff)
```
```  2646 done
```
```  2647
```
```  2648 lemma fold1Set_determ:
```
```  2649   "fold1Set times A x ==> fold1Set times A y ==> y = x"
```
```  2650 proof (clarify elim!: fold1Set.cases)
```
```  2651   fix A x B y a b
```
```  2652   assume Ax: "fold_graph times id a A x"
```
```  2653   assume By: "fold_graph times id b B y"
```
```  2654   assume anotA:  "a \<notin> A"
```
```  2655   assume bnotB:  "b \<notin> B"
```
```  2656   assume eq: "insert a A = insert b B"
```
```  2657   show "y=x"
```
```  2658   proof cases
```
```  2659     assume same: "a=b"
```
```  2660     hence "A=B" using anotA bnotB eq by (blast elim!: equalityE)
```
```  2661     thus ?thesis using Ax By same by (blast intro: fold_graph_determ)
```
```  2662   next
```
```  2663     assume diff: "a\<noteq>b"
```
```  2664     let ?D = "B - {a}"
```
```  2665     have B: "B = insert a ?D" and A: "A = insert b ?D"
```
```  2666      and aB: "a \<in> B" and bA: "b \<in> A"
```
```  2667       using eq anotA bnotB diff by (blast elim!:equalityE)+
```
```  2668     with aB bnotB By
```
```  2669     have "fold_graph times id a (insert b ?D) y"
```
```  2670       by (auto intro: fold_graph_permute simp add: insert_absorb)
```
```  2671     moreover
```
```  2672     have "fold_graph times id a (insert b ?D) x"
```
```  2673       by (simp add: A [symmetric] Ax)
```
```  2674     ultimately show ?thesis by (blast intro: fold_graph_determ)
```
```  2675   qed
```
```  2676 qed
```
```  2677
```
```  2678 lemma fold1Set_equality: "fold1Set times A y ==> fold1 times A = y"
```
```  2679   by (unfold fold1_def) (blast intro: fold1Set_determ)
```
```  2680
```
```  2681 end
```
```  2682 *)
```
```  2683
```
```  2684 declare
```
```  2685   empty_fold_graphE [rule del]  fold_graph.intros [rule del]
```
```  2686   empty_fold1SetE [rule del]  insert_fold1SetE [rule del]
```
```  2687   -- {* No more proofs involve these relations. *}
```
```  2688
```
```  2689 subsubsection {* Lemmas about @{text fold1} *}
```
```  2690
```
```  2691 context ab_semigroup_mult
```
```  2692 begin
```
```  2693
```
```  2694 lemma fold1_Un:
```
```  2695 assumes A: "finite A" "A \<noteq> {}"
```
```  2696 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A Int B = {} \<Longrightarrow>
```
```  2697        fold1 times (A Un B) = fold1 times A * fold1 times B"
```
```  2698 using A by (induct rule: finite_ne_induct)
```
```  2699   (simp_all add: fold1_insert mult_assoc)
```
```  2700
```
```  2701 lemma fold1_in:
```
```  2702   assumes A: "finite (A)" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x,y}"
```
```  2703   shows "fold1 times A \<in> A"
```
```  2704 using A
```
```  2705 proof (induct rule:finite_ne_induct)
```
```  2706   case singleton thus ?case by simp
```
```  2707 next
```
```  2708   case insert thus ?case using elem by (force simp add:fold1_insert)
```
```  2709 qed
```
```  2710
```
```  2711 end
```
```  2712
```
```  2713 lemma (in ab_semigroup_idem_mult) fold1_Un2:
```
```  2714 assumes A: "finite A" "A \<noteq> {}"
```
```  2715 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow>
```
```  2716        fold1 times (A Un B) = fold1 times A * fold1 times B"
```
```  2717 using A
```
```  2718 proof(induct rule:finite_ne_induct)
```
```  2719   case singleton thus ?case by simp
```
```  2720 next
```
```  2721   case insert thus ?case by (simp add: mult_assoc)
```
```  2722 qed
```
```  2723
```
```  2724
```
```  2725 subsubsection {* Fold1 in lattices with @{const inf} and @{const sup} *}
```
```  2726
```
```  2727 text{*
```
```  2728   As an application of @{text fold1} we define infimum
```
```  2729   and supremum in (not necessarily complete!) lattices
```
```  2730   over (non-empty) sets by means of @{text fold1}.
```
```  2731 *}
```
```  2732
```
```  2733 context lower_semilattice
```
```  2734 begin
```
```  2735
```
```  2736 lemma below_fold1_iff:
```
```  2737   assumes "finite A" "A \<noteq> {}"
```
```  2738   shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
```
```  2739 proof -
```
```  2740   interpret ab_semigroup_idem_mult inf
```
```  2741     by (rule ab_semigroup_idem_mult_inf)
```
```  2742   show ?thesis using assms by (induct rule: finite_ne_induct) simp_all
```
```  2743 qed
```
```  2744
```
```  2745 lemma fold1_belowI:
```
```  2746   assumes "finite A"
```
```  2747     and "a \<in> A"
```
```  2748   shows "fold1 inf A \<le> a"
```
```  2749 proof -
```
```  2750   from assms have "A \<noteq> {}" by auto
```
```  2751   from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
```
```  2752   proof (induct rule: finite_ne_induct)
```
```  2753     case singleton thus ?case by simp
```
```  2754   next
```
```  2755     interpret ab_semigroup_idem_mult inf
```
```  2756       by (rule ab_semigroup_idem_mult_inf)
```
```  2757     case (insert x F)
```
```  2758     from insert(5) have "a = x \<or> a \<in> F" by simp
```
```  2759     thus ?case
```
```  2760     proof
```
```  2761       assume "a = x" thus ?thesis using insert
```
```  2762         by (simp add: mult_ac)
```
```  2763     next
```
```  2764       assume "a \<in> F"
```
```  2765       hence bel: "fold1 inf F \<le> a" by (rule insert)
```
```  2766       have "inf (fold1 inf (insert x F)) a = inf x (inf (fold1 inf F) a)"
```
```  2767         using insert by (simp add: mult_ac)
```
```  2768       also have "inf (fold1 inf F) a = fold1 inf F"
```
```  2769         using bel by (auto intro: antisym)
```
```  2770       also have "inf x \<dots> = fold1 inf (insert x F)"
```
```  2771         using insert by (simp add: mult_ac)
```
```  2772       finally have aux: "inf (fold1 inf (insert x F)) a = fold1 inf (insert x F)" .
```
```  2773       moreover have "inf (fold1 inf (insert x F)) a \<le> a" by simp
```
```  2774       ultimately show ?thesis by simp
```
```  2775     qed
```
```  2776   qed
```
```  2777 qed
```
```  2778
```
```  2779 end
```
```  2780
```
```  2781 context lattice
```
```  2782 begin
```
```  2783
```
```  2784 definition
```
```  2785   Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900)
```
```  2786 where
```
```  2787   "Inf_fin = fold1 inf"
```
```  2788
```
```  2789 definition
```
```  2790   Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900)
```
```  2791 where
```
```  2792   "Sup_fin = fold1 sup"
```
```  2793
```
```  2794 lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A"
```
```  2795 apply(unfold Sup_fin_def Inf_fin_def)
```
```  2796 apply(subgoal_tac "EX a. a:A")
```
```  2797 prefer 2 apply blast
```
```  2798 apply(erule exE)
```
```  2799 apply(rule order_trans)
```
```  2800 apply(erule (1) fold1_belowI)
```
```  2801 apply(erule (1) lower_semilattice.fold1_belowI [OF dual_semilattice])
```
```  2802 done
```
```  2803
```
```  2804 lemma sup_Inf_absorb [simp]:
```
```  2805   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^bsub>fin\<^esub>A) = a"
```
```  2806 apply(subst sup_commute)
```
```  2807 apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI)
```
```  2808 done
```
```  2809
```
```  2810 lemma inf_Sup_absorb [simp]:
```
```  2811   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a"
```
```  2812 by (simp add: Sup_fin_def inf_absorb1
```
```  2813   lower_semilattice.fold1_belowI [OF dual_semilattice])
```
```  2814
```
```  2815 end
```
```  2816
```
```  2817 context distrib_lattice
```
```  2818 begin
```
```  2819
```
```  2820 lemma sup_Inf1_distrib:
```
```  2821   assumes "finite A"
```
```  2822     and "A \<noteq> {}"
```
```  2823   shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
```
```  2824 proof -
```
```  2825   interpret ab_semigroup_idem_mult inf
```
```  2826     by (rule ab_semigroup_idem_mult_inf)
```
```  2827   from assms show ?thesis
```
```  2828     by (simp add: Inf_fin_def image_def
```
```  2829       hom_fold1_commute [where h="sup x", OF sup_inf_distrib1])
```
```  2830         (rule arg_cong [where f="fold1 inf"], blast)
```
```  2831 qed
```
```  2832
```
```  2833 lemma sup_Inf2_distrib:
```
```  2834   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
```
```  2835   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}"
```
```  2836 using A proof (induct rule: finite_ne_induct)
```
```  2837   case singleton thus ?case
```
```  2838     by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
```
```  2839 next
```
```  2840   interpret ab_semigroup_idem_mult inf
```
```  2841     by (rule ab_semigroup_idem_mult_inf)
```
```  2842   case (insert x A)
```
```  2843   have finB: "finite {sup x b |b. b \<in> B}"
```
```  2844     by(rule finite_surj[where f = "sup x", OF B(1)], auto)
```
```  2845   have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
```
```  2846   proof -
```
```  2847     have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
```
```  2848       by blast
```
```  2849     thus ?thesis by(simp add: insert(1) B(1))
```
```  2850   qed
```
```  2851   have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
```
```  2852   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)"
```
```  2853     using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def])
```
```  2854   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)
```
```  2855   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})"
```
```  2856     using insert by(simp add:sup_Inf1_distrib[OF B])
```
```  2857   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})"
```
```  2858     (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M")
```
```  2859     using B insert
```
```  2860     by (simp add: Inf_fin_def fold1_Un2 [OF finB _ finAB ne])
```
```  2861   also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
```
```  2862     by blast
```
```  2863   finally show ?case .
```
```  2864 qed
```
```  2865
```
```  2866 lemma inf_Sup1_distrib:
```
```  2867   assumes "finite A" and "A \<noteq> {}"
```
```  2868   shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
```
```  2869 proof -
```
```  2870   interpret ab_semigroup_idem_mult sup
```
```  2871     by (rule ab_semigroup_idem_mult_sup)
```
```  2872   from assms show ?thesis
```
```  2873     by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1])
```
```  2874       (rule arg_cong [where f="fold1 sup"], blast)
```
```  2875 qed
```
```  2876
```
```  2877 lemma inf_Sup2_distrib:
```
```  2878   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
```
```  2879   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}"
```
```  2880 using A proof (induct rule: finite_ne_induct)
```
```  2881   case singleton thus ?case
```
```  2882     by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def])
```
```  2883 next
```
```  2884   case (insert x A)
```
```  2885   have finB: "finite {inf x b |b. b \<in> B}"
```
```  2886     by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
```
```  2887   have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
```
```  2888   proof -
```
```  2889     have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
```
```  2890       by blast
```
```  2891     thus ?thesis by(simp add: insert(1) B(1))
```
```  2892   qed
```
```  2893   have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
```
```  2894   interpret ab_semigroup_idem_mult sup
```
```  2895     by (rule ab_semigroup_idem_mult_sup)
```
```  2896   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)"
```
```  2897     using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
```
```  2898   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)
```
```  2899   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})"
```
```  2900     using insert by(simp add:inf_Sup1_distrib[OF B])
```
```  2901   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})"
```
```  2902     (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M")
```
```  2903     using B insert
```
```  2904     by (simp add: Sup_fin_def fold1_Un2 [OF finB _ finAB ne])
```
```  2905   also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
```
```  2906     by blast
```
```  2907   finally show ?case .
```
```  2908 qed
```
```  2909
```
```  2910 end
```
```  2911
```
```  2912 context complete_lattice
```
```  2913 begin
```
```  2914
```
```  2915 text {*
```
```  2916   Coincidence on finite sets in complete lattices:
```
```  2917 *}
```
```  2918
```
```  2919 lemma Inf_fin_Inf:
```
```  2920   assumes "finite A" and "A \<noteq> {}"
```
```  2921   shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
```
```  2922 proof -
```
```  2923     interpret ab_semigroup_idem_mult inf
```
```  2924     by (rule ab_semigroup_idem_mult_inf)
```
```  2925   from assms show ?thesis
```
```  2926   unfolding Inf_fin_def by (induct A set: finite)
```
```  2927     (simp_all add: Inf_insert_simp)
```
```  2928 qed
```
```  2929
```
```  2930 lemma Sup_fin_Sup:
```
```  2931   assumes "finite A" and "A \<noteq> {}"
```
```  2932   shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
```
```  2933 proof -
```
```  2934   interpret ab_semigroup_idem_mult sup
```
```  2935     by (rule ab_semigroup_idem_mult_sup)
```
```  2936   from assms show ?thesis
```
```  2937   unfolding Sup_fin_def by (induct A set: finite)
```
```  2938     (simp_all add: Sup_insert_simp)
```
```  2939 qed
```
```  2940
```
```  2941 end
```
```  2942
```
```  2943
```
```  2944 subsubsection {* Fold1 in linear orders with @{const min} and @{const max} *}
```
```  2945
```
```  2946 text{*
```
```  2947   As an application of @{text fold1} we define minimum
```
```  2948   and maximum in (not necessarily complete!) linear orders
```
```  2949   over (non-empty) sets by means of @{text fold1}.
```
```  2950 *}
```
```  2951
```
```  2952 context linorder
```
```  2953 begin
```
```  2954
```
```  2955 lemma ab_semigroup_idem_mult_min:
```
```  2956   "ab_semigroup_idem_mult min"
```
```  2957   proof qed (auto simp add: min_def)
```
```  2958
```
```  2959 lemma ab_semigroup_idem_mult_max:
```
```  2960   "ab_semigroup_idem_mult max"
```
```  2961   proof qed (auto simp add: max_def)
```
```  2962
```
```  2963 lemma max_lattice:
```
```  2964   "lower_semilattice (op \<ge>) (op >) max"
```
```  2965   by (fact min_max.dual_semilattice)
```
```  2966
```
```  2967 lemma dual_max:
```
```  2968   "ord.max (op \<ge>) = min"
```
```  2969   by (auto simp add: ord.max_def_raw min_def_raw expand_fun_eq)
```
```  2970
```
```  2971 lemma dual_min:
```
```  2972   "ord.min (op \<ge>) = max"
```
```  2973   by (auto simp add: ord.min_def_raw max_def_raw expand_fun_eq)
```
```  2974
```
```  2975 lemma strict_below_fold1_iff:
```
```  2976   assumes "finite A" and "A \<noteq> {}"
```
```  2977   shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
```
```  2978 proof -
```
```  2979   interpret ab_semigroup_idem_mult min
```
```  2980     by (rule ab_semigroup_idem_mult_min)
```
```  2981   from assms show ?thesis
```
```  2982   by (induct rule: finite_ne_induct)
```
```  2983     (simp_all add: fold1_insert)
```
```  2984 qed
```
```  2985
```
```  2986 lemma fold1_below_iff:
```
```  2987   assumes "finite A" and "A \<noteq> {}"
```
```  2988   shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
```
```  2989 proof -
```
```  2990   interpret ab_semigroup_idem_mult min
```
```  2991     by (rule ab_semigroup_idem_mult_min)
```
```  2992   from assms show ?thesis
```
```  2993   by (induct rule: finite_ne_induct)
```
```  2994     (simp_all add: fold1_insert min_le_iff_disj)
```
```  2995 qed
```
```  2996
```
```  2997 lemma fold1_strict_below_iff:
```
```  2998   assumes "finite A" and "A \<noteq> {}"
```
```  2999   shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
```
```  3000 proof -
```
```  3001   interpret ab_semigroup_idem_mult min
```
```  3002     by (rule ab_semigroup_idem_mult_min)
```
```  3003   from assms show ?thesis
```
```  3004   by (induct rule: finite_ne_induct)
```
```  3005     (simp_all add: fold1_insert min_less_iff_disj)
```
```  3006 qed
```
```  3007
```
```  3008 lemma fold1_antimono:
```
```  3009   assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
```
```  3010   shows "fold1 min B \<le> fold1 min A"
```
```  3011 proof cases
```
```  3012   assume "A = B" thus ?thesis by simp
```
```  3013 next
```
```  3014   interpret ab_semigroup_idem_mult min
```
```  3015     by (rule ab_semigroup_idem_mult_min)
```
```  3016   assume "A \<noteq> B"
```
```  3017   have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
```
```  3018   have "fold1 min B = fold1 min (A \<union> (B-A))" by(subst B)(rule refl)
```
```  3019   also have "\<dots> = min (fold1 min A) (fold1 min (B-A))"
```
```  3020   proof -
```
```  3021     have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
```
```  3022     moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`]) (* by(blast intro:finite_Diff prems) fails *)
```
```  3023     moreover have "(B-A) \<noteq> {}" using prems by blast
```
```  3024     moreover have "A Int (B-A) = {}" using prems by blast
```
```  3025     ultimately show ?thesis using `A \<noteq> {}` by (rule_tac fold1_Un)
```
```  3026   qed
```
```  3027   also have "\<dots> \<le> fold1 min A" by (simp add: min_le_iff_disj)
```
```  3028   finally show ?thesis .
```
```  3029 qed
```
```  3030
```
```  3031 definition
```
```  3032   Min :: "'a set \<Rightarrow> 'a"
```
```  3033 where
```
```  3034   "Min = fold1 min"
```
```  3035
```
```  3036 definition
```
```  3037   Max :: "'a set \<Rightarrow> 'a"
```
```  3038 where
```
```  3039   "Max = fold1 max"
```
```  3040
```
```  3041 lemmas Min_singleton [simp] = fold1_singleton_def [OF Min_def]
```
```  3042 lemmas Max_singleton [simp] = fold1_singleton_def [OF Max_def]
```
```  3043
```
```  3044 lemma Min_insert [simp]:
```
```  3045   assumes "finite A" and "A \<noteq> {}"
```
```  3046   shows "Min (insert x A) = min x (Min A)"
```
```  3047 proof -
```
```  3048   interpret ab_semigroup_idem_mult min
```
```  3049     by (rule ab_semigroup_idem_mult_min)
```
```  3050   from assms show ?thesis by (rule fold1_insert_idem_def [OF Min_def])
```
```  3051 qed
```
```  3052
```
```  3053 lemma Max_insert [simp]:
```
```  3054   assumes "finite A" and "A \<noteq> {}"
```
```  3055   shows "Max (insert x A) = max x (Max A)"
```
```  3056 proof -
```
```  3057   interpret ab_semigroup_idem_mult max
```
```  3058     by (rule ab_semigroup_idem_mult_max)
```
```  3059   from assms show ?thesis by (rule fold1_insert_idem_def [OF Max_def])
```
```  3060 qed
```
```  3061
```
```  3062 lemma Min_in [simp]:
```
```  3063   assumes "finite A" and "A \<noteq> {}"
```
```  3064   shows "Min A \<in> A"
```
```  3065 proof -
```
```  3066   interpret ab_semigroup_idem_mult min
```
```  3067     by (rule ab_semigroup_idem_mult_min)
```
```  3068   from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def)
```
```  3069 qed
```
```  3070
```
```  3071 lemma Max_in [simp]:
```
```  3072   assumes "finite A" and "A \<noteq> {}"
```
```  3073   shows "Max A \<in> A"
```
```  3074 proof -
```
```  3075   interpret ab_semigroup_idem_mult max
```
```  3076     by (rule ab_semigroup_idem_mult_max)
```
```  3077   from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
```
```  3078 qed
```
```  3079
```
```  3080 lemma Min_Un:
```
```  3081   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
```
```  3082   shows "Min (A \<union> B) = min (Min A) (Min B)"
```
```  3083 proof -
```
```  3084   interpret ab_semigroup_idem_mult min
```
```  3085     by (rule ab_semigroup_idem_mult_min)
```
```  3086   from assms show ?thesis
```
```  3087     by (simp add: Min_def fold1_Un2)
```
```  3088 qed
```
```  3089
```
```  3090 lemma Max_Un:
```
```  3091   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
```
```  3092   shows "Max (A \<union> B) = max (Max A) (Max B)"
```
```  3093 proof -
```
```  3094   interpret ab_semigroup_idem_mult max
```
```  3095     by (rule ab_semigroup_idem_mult_max)
```
```  3096   from assms show ?thesis
```
```  3097     by (simp add: Max_def fold1_Un2)
```
```  3098 qed
```
```  3099
```
```  3100 lemma hom_Min_commute:
```
```  3101   assumes "\<And>x y. h (min x y) = min (h x) (h y)"
```
```  3102     and "finite N" and "N \<noteq> {}"
```
```  3103   shows "h (Min N) = Min (h ` N)"
```
```  3104 proof -
```
```  3105   interpret ab_semigroup_idem_mult min
```
```  3106     by (rule ab_semigroup_idem_mult_min)
```
```  3107   from assms show ?thesis
```
```  3108     by (simp add: Min_def hom_fold1_commute)
```
```  3109 qed
```
```  3110
```
```  3111 lemma hom_Max_commute:
```
```  3112   assumes "\<And>x y. h (max x y) = max (h x) (h y)"
```
```  3113     and "finite N" and "N \<noteq> {}"
```
```  3114   shows "h (Max N) = Max (h ` N)"
```
```  3115 proof -
```
```  3116   interpret ab_semigroup_idem_mult max
```
```  3117     by (rule ab_semigroup_idem_mult_max)
```
```  3118   from assms show ?thesis
```
```  3119     by (simp add: Max_def hom_fold1_commute [of h])
```
```  3120 qed
```
```  3121
```
```  3122 lemma Min_le [simp]:
```
```  3123   assumes "finite A" and "x \<in> A"
```
```  3124   shows "Min A \<le> x"
```
```  3125   using assms by (simp add: Min_def min_max.fold1_belowI)
```
```  3126
```
```  3127 lemma Max_ge [simp]:
```
```  3128   assumes "finite A" and "x \<in> A"
```
```  3129   shows "x \<le> Max A"
```
```  3130 proof -
```
```  3131   interpret lower_semilattice "op \<ge>" "op >" max
```
```  3132     by (rule max_lattice)
```
```  3133   from assms show ?thesis by (simp add: Max_def fold1_belowI)
```
```  3134 qed
```
```  3135
```
```  3136 lemma Min_ge_iff [simp, noatp]:
```
```  3137   assumes "finite A" and "A \<noteq> {}"
```
```  3138   shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
```
```  3139   using assms by (simp add: Min_def min_max.below_fold1_iff)
```
```  3140
```
```  3141 lemma Max_le_iff [simp, noatp]:
```
```  3142   assumes "finite A" and "A \<noteq> {}"
```
```  3143   shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
```
```  3144 proof -
```
```  3145   interpret lower_semilattice "op \<ge>" "op >" max
```
```  3146     by (rule max_lattice)
```
```  3147   from assms show ?thesis by (simp add: Max_def below_fold1_iff)
```
```  3148 qed
```
```  3149
```
```  3150 lemma Min_gr_iff [simp, noatp]:
```
```  3151   assumes "finite A" and "A \<noteq> {}"
```
```  3152   shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
```
```  3153   using assms by (simp add: Min_def strict_below_fold1_iff)
```
```  3154
```
```  3155 lemma Max_less_iff [simp, noatp]:
```
```  3156   assumes "finite A" and "A \<noteq> {}"
```
```  3157   shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
```
```  3158 proof -
```
```  3159   interpret dual: linorder "op \<ge>" "op >"
```
```  3160     by (rule dual_linorder)
```
```  3161   from assms show ?thesis
```
```  3162     by (simp add: Max_def dual.strict_below_fold1_iff [folded dual.dual_max])
```
```  3163 qed
```
```  3164
```
```  3165 lemma Min_le_iff [noatp]:
```
```  3166   assumes "finite A" and "A \<noteq> {}"
```
```  3167   shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
```
```  3168   using assms by (simp add: Min_def fold1_below_iff)
```
```  3169
```
```  3170 lemma Max_ge_iff [noatp]:
```
```  3171   assumes "finite A" and "A \<noteq> {}"
```
```  3172   shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
```
```  3173 proof -
```
```  3174   interpret dual: linorder "op \<ge>" "op >"
```
```  3175     by (rule dual_linorder)
```
```  3176   from assms show ?thesis
```
```  3177     by (simp add: Max_def dual.fold1_below_iff [folded dual.dual_max])
```
```  3178 qed
```
```  3179
```
```  3180 lemma Min_less_iff [noatp]:
```
```  3181   assumes "finite A" and "A \<noteq> {}"
```
```  3182   shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
```
```  3183   using assms by (simp add: Min_def fold1_strict_below_iff)
```
```  3184
```
```  3185 lemma Max_gr_iff [noatp]:
```
```  3186   assumes "finite A" and "A \<noteq> {}"
```
```  3187   shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
```
```  3188 proof -
```
```  3189   interpret dual: linorder "op \<ge>" "op >"
```
```  3190     by (rule dual_linorder)
```
```  3191   from assms show ?thesis
```
```  3192     by (simp add: Max_def dual.fold1_strict_below_iff [folded dual.dual_max])
```
```  3193 qed
```
```  3194
```
```  3195 lemma Min_eqI:
```
```  3196   assumes "finite A"
```
```  3197   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
```
```  3198     and "x \<in> A"
```
```  3199   shows "Min A = x"
```
```  3200 proof (rule antisym)
```
```  3201   from `x \<in> A` have "A \<noteq> {}" by auto
```
```  3202   with assms show "Min A \<ge> x" by simp
```
```  3203 next
```
```  3204   from assms show "x \<ge> Min A" by simp
```
```  3205 qed
```
```  3206
```
```  3207 lemma Max_eqI:
```
```  3208   assumes "finite A"
```
```  3209   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
```
```  3210     and "x \<in> A"
```
```  3211   shows "Max A = x"
```
```  3212 proof (rule antisym)
```
```  3213   from `x \<in> A` have "A \<noteq> {}" by auto
```
```  3214   with assms show "Max A \<le> x" by simp
```
```  3215 next
```
```  3216   from assms show "x \<le> Max A" by simp
```
```  3217 qed
```
```  3218
```
```  3219 lemma Min_antimono:
```
```  3220   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
```
```  3221   shows "Min N \<le> Min M"
```
```  3222   using assms by (simp add: Min_def fold1_antimono)
```
```  3223
```
```  3224 lemma Max_mono:
```
```  3225   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
```
```  3226   shows "Max M \<le> Max N"
```
```  3227 proof -
```
```  3228   interpret dual: linorder "op \<ge>" "op >"
```
```  3229     by (rule dual_linorder)
```
```  3230   from assms show ?thesis
```
```  3231     by (simp add: Max_def dual.fold1_antimono [folded dual.dual_max])
```
```  3232 qed
```
```  3233
```
```  3234 lemma finite_linorder_max_induct[consumes 1, case_names empty insert]:
```
```  3235  "finite A \<Longrightarrow> P {} \<Longrightarrow>
```
```  3236   (!!A b. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
```
```  3237   \<Longrightarrow> P A"
```
```  3238 proof (induct rule: finite_psubset_induct)
```
```  3239   fix A :: "'a set"
```
```  3240   assume IH: "!! B. finite B \<Longrightarrow> B < A \<Longrightarrow> P {} \<Longrightarrow>
```
```  3241                  (!!A b. finite A \<Longrightarrow> (\<forall>a\<in>A. a<b) \<Longrightarrow> P A \<Longrightarrow> P (insert b A))
```
```  3242                   \<Longrightarrow> P B"
```
```  3243   and "finite A" and "P {}"
```
```  3244   and step: "!!A b. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
```
```  3245   show "P A"
```
```  3246   proof (cases "A = {}")
```
```  3247     assume "A = {}" thus "P A" using `P {}` by simp
```
```  3248   next
```
```  3249     let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B"
```
```  3250     assume "A \<noteq> {}"
```
```  3251     with `finite A` have "Max A : A" by auto
```
```  3252     hence A: "?A = A" using insert_Diff_single insert_absorb by auto
```
```  3253     moreover have "finite ?B" using `finite A` by simp
```
```  3254     ultimately have "P ?B" using `P {}` step IH by blast
```
```  3255     moreover have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastsimp
```
```  3256     ultimately show "P A" using A insert_Diff_single step[OF `finite ?B`] by fastsimp
```
```  3257   qed
```
```  3258 qed
```
```  3259
```
```  3260 lemma finite_linorder_min_induct[consumes 1, case_names empty insert]:
```
```  3261   "\<lbrakk>finite A; P {}; \<And>A b. \<lbrakk>finite A; \<forall>a\<in>A. b < a; P A\<rbrakk> \<Longrightarrow> P (insert b A)\<rbrakk> \<Longrightarrow> P A"
```
```  3262 by(rule linorder.finite_linorder_max_induct[OF dual_linorder])
```
```  3263
```
```  3264 end
```
```  3265
```
```  3266 context ordered_ab_semigroup_add
```
```  3267 begin
```
```  3268
```
```  3269 lemma add_Min_commute:
```
```  3270   fixes k
```
```  3271   assumes "finite N" and "N \<noteq> {}"
```
```  3272   shows "k + Min N = Min {k + m | m. m \<in> N}"
```
```  3273 proof -
```
```  3274   have "\<And>x y. k + min x y = min (k + x) (k + y)"
```
```  3275     by (simp add: min_def not_le)
```
```  3276       (blast intro: antisym less_imp_le add_left_mono)
```
```  3277   with assms show ?thesis
```
```  3278     using hom_Min_commute [of "plus k" N]
```
```  3279     by simp (blast intro: arg_cong [where f = Min])
```
```  3280 qed
```
```  3281
```
```  3282 lemma add_Max_commute:
```
```  3283   fixes k
```
```  3284   assumes "finite N" and "N \<noteq> {}"
```
```  3285   shows "k + Max N = Max {k + m | m. m \<in> N}"
```
```  3286 proof -
```
```  3287   have "\<And>x y. k + max x y = max (k + x) (k + y)"
```
```  3288     by (simp add: max_def not_le)
```
```  3289       (blast intro: antisym less_imp_le add_left_mono)
```
```  3290   with assms show ?thesis
```
```  3291     using hom_Max_commute [of "plus k" N]
```
```  3292     by simp (blast intro: arg_cong [where f = Max])
```
```  3293 qed
```
```  3294
```
```  3295 end
```
```  3296
```
```  3297
```
```  3298 subsection {* Expressing set operations via @{const fold} *}
```
```  3299
```
```  3300 lemma (in fun_left_comm) fun_left_comm_apply:
```
```  3301   "fun_left_comm (\<lambda>x. f (g x))"
```
```  3302 proof
```
```  3303 qed (simp_all add: fun_left_comm)
```
```  3304
```
```  3305 lemma (in fun_left_comm_idem) fun_left_comm_idem_apply:
```
```  3306   "fun_left_comm_idem (\<lambda>x. f (g x))"
```
```  3307   by (rule fun_left_comm_idem.intro, rule fun_left_comm_apply, unfold_locales)
```
```  3308     (simp_all add: fun_left_idem)
```
```  3309
```
```  3310 lemma fun_left_comm_idem_insert:
```
```  3311   "fun_left_comm_idem insert"
```
```  3312 proof
```
```  3313 qed auto
```
```  3314
```
```  3315 lemma fun_left_comm_idem_remove:
```
```  3316   "fun_left_comm_idem (\<lambda>x A. A - {x})"
```
```  3317 proof
```
```  3318 qed auto
```
```  3319
```
```  3320 lemma fun_left_comm_idem_inter:
```
```  3321   "fun_left_comm_idem op \<inter>"
```
```  3322 proof
```
```  3323 qed auto
```
```  3324
```
```  3325 lemma fun_left_comm_idem_union:
```
```  3326   "fun_left_comm_idem op \<union>"
```
```  3327 proof
```
```  3328 qed auto
```
```  3329
```
```  3330 lemma union_fold_insert:
```
```  3331   assumes "finite A"
```
```  3332   shows "A \<union> B = fold insert B A"
```
```  3333 proof -
```
```  3334   interpret fun_left_comm_idem insert by (fact fun_left_comm_idem_insert)
```
```  3335   from `finite A` show ?thesis by (induct A arbitrary: B) simp_all
```
```  3336 qed
```
```  3337
```
```  3338 lemma minus_fold_remove:
```
```  3339   assumes "finite A"
```
```  3340   shows "B - A = fold (\<lambda>x A. A - {x}) B A"
```
```  3341 proof -
```
```  3342   interpret fun_left_comm_idem "\<lambda>x A. A - {x}" by (fact fun_left_comm_idem_remove)
```
```  3343   from `finite A` show ?thesis by (induct A arbitrary: B) auto
```
```  3344 qed
```
```  3345
```
```  3346 lemma inter_Inter_fold_inter:
```
```  3347   assumes "finite A"
```
```  3348   shows "B \<inter> Inter A = fold (op \<inter>) B A"
```
```  3349 proof -
```
```  3350   interpret fun_left_comm_idem "op \<inter>" by (fact fun_left_comm_idem_inter)
```
```  3351   from `finite A` show ?thesis by (induct A arbitrary: B)
```
```  3352     (simp_all add: fold_fun_comm Int_commute)
```
```  3353 qed
```
```  3354
```
```  3355 lemma union_Union_fold_union:
```
```  3356   assumes "finite A"
```
```  3357   shows "B \<union> Union A = fold (op \<union>) B A"
```
```  3358 proof -
```
```  3359   interpret fun_left_comm_idem "op \<union>" by (fact fun_left_comm_idem_union)
```
```  3360   from `finite A` show ?thesis by (induct A arbitrary: B)
```
```  3361     (simp_all add: fold_fun_comm Un_commute)
```
```  3362 qed
```
```  3363
```
```  3364 lemma Inter_fold_inter:
```
```  3365   assumes "finite A"
```
```  3366   shows "Inter A = fold (op \<inter>) UNIV A"
```
```  3367   using assms inter_Inter_fold_inter [of A UNIV] by simp
```
```  3368
```
```  3369 lemma Union_fold_union:
```
```  3370   assumes "finite A"
```
```  3371   shows "Union A = fold (op \<union>) {} A"
```
```  3372   using assms union_Union_fold_union [of A "{}"] by simp
```
```  3373
```
```  3374 lemma inter_INTER_fold_inter:
```
```  3375   assumes "finite A"
```
```  3376   shows "B \<inter> INTER A f = fold (\<lambda>A. op \<inter> (f A)) B A" (is "?inter = ?fold")
```
```  3377 proof (rule sym)
```
```  3378   interpret fun_left_comm_idem "op \<inter>" by (fact fun_left_comm_idem_inter)
```
```  3379   interpret fun_left_comm_idem "\<lambda>A. op \<inter> (f A)" by (fact fun_left_comm_idem_apply)
```
```  3380   from `finite A` show "?fold = ?inter" by (induct A arbitrary: B) auto
```
```  3381 qed
```
```  3382
```
```  3383 lemma union_UNION_fold_union:
```
```  3384   assumes "finite A"
```
```  3385   shows "B \<union> UNION A f = fold (\<lambda>A. op \<union> (f A)) B A" (is "?union = ?fold")
```
```  3386 proof (rule sym)
```
```  3387   interpret fun_left_comm_idem "op \<union>" by (fact fun_left_comm_idem_union)
```
```  3388   interpret fun_left_comm_idem "\<lambda>A. op \<union> (f A)" by (fact fun_left_comm_idem_apply)
```
```  3389   from `finite A` show "?fold = ?union" by (induct A arbitrary: B) auto
```
```  3390 qed
```
```  3391
```
```  3392 lemma INTER_fold_inter:
```
```  3393   assumes "finite A"
```
```  3394   shows "INTER A f = fold (\<lambda>A. op \<inter> (f A)) UNIV A"
```
```  3395   using assms inter_INTER_fold_inter [of A UNIV] by simp
```
```  3396
```
```  3397 lemma UNION_fold_union:
```
```  3398   assumes "finite A"
```
```  3399   shows "UNION A f = fold (\<lambda>A. op \<union> (f A)) {} A"
```
```  3400   using assms union_UNION_fold_union [of A "{}"] by simp
```
```  3401
```
```  3402 end
```