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