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