src/HOL/Big_Operators.thy
author nipkow
Wed Aug 15 12:18:30 2012 +0200 (2012-08-15)
changeset 48819 6cf7a9d8bbaf
parent 46904 f30e941b4512
child 48820 bfd136281c13
permissions -rw-r--r--
abstracted lemmas
     1 (*  Title:      HOL/Big_Operators.thy
     2     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     3                 with contributions by Jeremy Avigad
     4 *)
     5 
     6 header {* Big operators and finite (non-empty) sets *}
     7 
     8 theory Big_Operators
     9 imports Plain
    10 begin
    11 
    12 subsection {* Generic monoid operation over a set *}
    13 
    14 no_notation times (infixl "*" 70)
    15 no_notation Groups.one ("1")
    16 
    17 locale comm_monoid_big = comm_monoid +
    18   fixes F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
    19   assumes F_eq: "F g A = (if finite A then fold_image (op *) g 1 A else 1)"
    20 
    21 sublocale comm_monoid_big < folding_image proof
    22 qed (simp add: F_eq)
    23 
    24 context comm_monoid_big
    25 begin
    26 
    27 lemma infinite [simp]:
    28   "\<not> finite A \<Longrightarrow> F g A = 1"
    29   by (simp add: F_eq)
    30 
    31 lemma F_cong:
    32   assumes "A = B" "\<And>x. x \<in> B \<Longrightarrow> h x = g x"
    33   shows "F h A = F g B"
    34 proof cases
    35   assume "finite A"
    36   with assms show ?thesis unfolding `A = B` by (simp cong: cong)
    37 next
    38   assume "\<not> finite A"
    39   then show ?thesis unfolding `A = B` by simp
    40 qed
    41 
    42 lemma F_unit[simp]: "F (%i. 1) A = 1"
    43 by (cases "finite A") (erule finite_induct, auto)
    44 
    45 lemma F_unit': "ALL a:A. g a = 1 ==> F g A = 1"
    46 by (simp add:F_cong)
    47 
    48 lemma If_cases:
    49   fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
    50   assumes fA: "finite A"
    51   shows "F (\<lambda>x. if P x then h x else g x) A =
    52          F h (A \<inter> {x. P x}) * F g (A \<inter> - {x. P x})"
    53 proof-
    54   have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}" 
    55           "(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}" 
    56     by blast+
    57   from fA 
    58   have f: "finite (A \<inter> {x. P x})" "finite (A \<inter> -{x. P x})" by auto
    59   let ?g = "\<lambda>x. if P x then h x else g x"
    60   from union_disjoint[OF f a(2), of ?g] a(1)
    61   show ?thesis
    62     by (subst (1 2) F_cong) simp_all
    63 qed
    64 
    65 end
    66 
    67 text {* for ad-hoc proofs for @{const fold_image} *}
    68 
    69 lemma (in comm_monoid_add) comm_monoid_mult:
    70   "class.comm_monoid_mult (op +) 0"
    71 proof qed (auto intro: add_assoc add_commute)
    72 
    73 notation times (infixl "*" 70)
    74 notation Groups.one ("1")
    75 
    76 
    77 subsection {* Generalized summation over a set *}
    78 
    79 definition (in comm_monoid_add) setsum :: "('b \<Rightarrow> 'a) => 'b set => 'a" where
    80   "setsum f A = (if finite A then fold_image (op +) f 0 A else 0)"
    81 
    82 sublocale comm_monoid_add < setsum!: comm_monoid_big "op +" 0 setsum proof
    83 qed (fact setsum_def)
    84 
    85 abbreviation
    86   Setsum  ("\<Sum>_" [1000] 999) where
    87   "\<Sum>A == setsum (%x. x) A"
    88 
    89 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
    90 written @{text"\<Sum>x\<in>A. e"}. *}
    91 
    92 syntax
    93   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
    94 syntax (xsymbols)
    95   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
    96 syntax (HTML output)
    97   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
    98 
    99 translations -- {* Beware of argument permutation! *}
   100   "SUM i:A. b" == "CONST setsum (%i. b) A"
   101   "\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
   102 
   103 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
   104  @{text"\<Sum>x|P. e"}. *}
   105 
   106 syntax
   107   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
   108 syntax (xsymbols)
   109   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   110 syntax (HTML output)
   111   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   112 
   113 translations
   114   "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
   115   "\<Sum>x|P. t" => "CONST setsum (%x. t) {x. P}"
   116 
   117 print_translation {*
   118 let
   119   fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
   120         if x <> y then raise Match
   121         else
   122           let
   123             val x' = Syntax_Trans.mark_bound x;
   124             val t' = subst_bound (x', t);
   125             val P' = subst_bound (x', P);
   126           in Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound x $ P' $ t' end
   127     | setsum_tr' _ = raise Match;
   128 in [(@{const_syntax setsum}, setsum_tr')] end
   129 *}
   130 
   131 lemma setsum_empty:
   132   "setsum f {} = 0"
   133   by (fact setsum.empty)
   134 
   135 lemma setsum_insert:
   136   "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   137   by (fact setsum.insert)
   138 
   139 lemma setsum_infinite:
   140   "~ finite A ==> setsum f A = 0"
   141   by (fact setsum.infinite)
   142 
   143 lemma (in comm_monoid_add) setsum_reindex:
   144   assumes "inj_on f B" shows "setsum h (f ` B) = setsum (h \<circ> f) B"
   145 proof -
   146   interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
   147   from assms show ?thesis by (auto simp add: setsum_def fold_image_reindex dest!:finite_imageD)
   148 qed
   149 
   150 lemma (in comm_monoid_add) setsum_reindex_id:
   151   "inj_on f B ==> setsum f B = setsum id (f ` B)"
   152   by (simp add: setsum_reindex)
   153 
   154 lemma (in comm_monoid_add) setsum_reindex_nonzero: 
   155   assumes fS: "finite S"
   156   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"
   157   shows "setsum h (f ` S) = setsum (h o f) S"
   158 using nz
   159 proof(induct rule: finite_induct[OF fS])
   160   case 1 thus ?case by simp
   161 next
   162   case (2 x F) 
   163   {assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto
   164     then obtain y where y: "y \<in> F" "f x = f y" by auto 
   165     from "2.hyps" y have xy: "x \<noteq> y" by auto
   166     
   167     from "2.prems"[of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp
   168     have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto
   169     also have "\<dots> = setsum (h o f) (insert x F)" 
   170       unfolding setsum.insert[OF `finite F` `x\<notin>F`]
   171       using h0
   172       apply simp
   173       apply (rule "2.hyps"(3))
   174       apply (rule_tac y="y" in  "2.prems")
   175       apply simp_all
   176       done
   177     finally have ?case .}
   178   moreover
   179   {assume fxF: "f x \<notin> f ` F"
   180     have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)" 
   181       using fxF "2.hyps" by simp 
   182     also have "\<dots> = setsum (h o f) (insert x F)"
   183       unfolding setsum.insert[OF `finite F` `x\<notin>F`]
   184       apply simp
   185       apply (rule cong [OF refl [of "op + (h (f x))"]])
   186       apply (rule "2.hyps"(3))
   187       apply (rule_tac y="y" in  "2.prems")
   188       apply simp_all
   189       done
   190     finally have ?case .}
   191   ultimately show ?case by blast
   192 qed
   193 
   194 lemma (in comm_monoid_add) setsum_cong:
   195   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
   196   by (cases "finite A") (auto intro: setsum.cong)
   197 
   198 lemma (in comm_monoid_add) strong_setsum_cong [cong]:
   199   "A = B ==> (!!x. x:B =simp=> f x = g x)
   200    ==> setsum (%x. f x) A = setsum (%x. g x) B"
   201   by (rule setsum_cong) (simp_all add: simp_implies_def)
   202 
   203 lemma (in comm_monoid_add) setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A"
   204   by (auto intro: setsum_cong)
   205 
   206 lemma (in comm_monoid_add) setsum_reindex_cong:
   207    "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|] 
   208     ==> setsum h B = setsum g A"
   209   by (simp add: setsum_reindex)
   210 
   211 lemmas setsum_0 = setsum.F_unit
   212 lemmas setsum_0' = setsum.F_unit'
   213 
   214 lemma (in comm_monoid_add) setsum_Un_Int: "finite A ==> finite B ==>
   215   setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
   216   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   217   by (fact setsum.union_inter)
   218 
   219 lemma (in comm_monoid_add) setsum_Un_disjoint: "finite A ==> finite B
   220   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
   221   by (fact setsum.union_disjoint)
   222 
   223 lemma setsum_mono_zero_left: 
   224   assumes fT: "finite T" and ST: "S \<subseteq> T"
   225   and z: "\<forall>i \<in> T - S. f i = 0"
   226   shows "setsum f S = setsum f T"
   227 proof-
   228   have eq: "T = S \<union> (T - S)" using ST by blast
   229   have d: "S \<inter> (T - S) = {}" using ST by blast
   230   from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
   231   show ?thesis 
   232   by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
   233 qed
   234 
   235 lemma setsum_mono_zero_right: 
   236   "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. f i = 0 \<Longrightarrow> setsum f T = setsum f S"
   237 by(blast intro!: setsum_mono_zero_left[symmetric])
   238 
   239 lemma setsum_mono_zero_cong_left: 
   240   assumes fT: "finite T" and ST: "S \<subseteq> T"
   241   and z: "\<forall>i \<in> T - S. g i = 0"
   242   and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
   243   shows "setsum f S = setsum g T"
   244 proof-
   245   have eq: "T = S \<union> (T - S)" using ST by blast
   246   have d: "S \<inter> (T - S) = {}" using ST by blast
   247   from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
   248   show ?thesis 
   249     using fg by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
   250 qed
   251 
   252 lemma setsum_mono_zero_cong_right: 
   253   assumes fT: "finite T" and ST: "S \<subseteq> T"
   254   and z: "\<forall>i \<in> T - S. f i = 0"
   255   and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
   256   shows "setsum f T = setsum g S"
   257 using setsum_mono_zero_cong_left[OF fT ST z] fg[symmetric] by auto 
   258 
   259 lemma setsum_delta: 
   260   assumes fS: "finite S"
   261   shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
   262 proof-
   263   let ?f = "(\<lambda>k. if k=a then b k else 0)"
   264   {assume a: "a \<notin> S"
   265     hence "\<forall> k\<in> S. ?f k = 0" by simp
   266     hence ?thesis  using a by simp}
   267   moreover 
   268   {assume a: "a \<in> S"
   269     let ?A = "S - {a}"
   270     let ?B = "{a}"
   271     have eq: "S = ?A \<union> ?B" using a by blast 
   272     have dj: "?A \<inter> ?B = {}" by simp
   273     from fS have fAB: "finite ?A" "finite ?B" by auto  
   274     have "setsum ?f S = setsum ?f ?A + setsum ?f ?B"
   275       using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
   276       by simp
   277     then have ?thesis  using a by simp}
   278   ultimately show ?thesis by blast
   279 qed
   280 lemma setsum_delta': 
   281   assumes fS: "finite S" shows 
   282   "setsum (\<lambda>k. if a = k then b k else 0) S = 
   283      (if a\<in> S then b a else 0)"
   284   using setsum_delta[OF fS, of a b, symmetric] 
   285   by (auto intro: setsum_cong)
   286 
   287 lemma setsum_restrict_set:
   288   assumes fA: "finite A"
   289   shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A"
   290 proof-
   291   from fA have fab: "finite (A \<inter> B)" by auto
   292   have aba: "A \<inter> B \<subseteq> A" by blast
   293   let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0"
   294   from setsum_mono_zero_left[OF fA aba, of ?g]
   295   show ?thesis by simp
   296 qed
   297 
   298 lemma setsum_cases:
   299   assumes fA: "finite A"
   300   shows "setsum (\<lambda>x. if P x then f x else g x) A =
   301          setsum f (A \<inter> {x. P x}) + setsum g (A \<inter> - {x. P x})"
   302   using setsum.If_cases[OF fA] .
   303 
   304 (*But we can't get rid of finite I. If infinite, although the rhs is 0, 
   305   the lhs need not be, since UNION I A could still be finite.*)
   306 lemma (in comm_monoid_add) setsum_UN_disjoint:
   307   assumes "finite I" and "ALL i:I. finite (A i)"
   308     and "ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}"
   309   shows "setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
   310 proof -
   311   interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
   312   from assms show ?thesis by (simp add: setsum_def fold_image_UN_disjoint)
   313 qed
   314 
   315 text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
   316 directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
   317 lemma setsum_Union_disjoint:
   318   assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}"
   319   shows "setsum f (Union C) = setsum (setsum f) C"
   320 proof cases
   321   assume "finite C"
   322   from setsum_UN_disjoint[OF this assms]
   323   show ?thesis
   324     by (simp add: SUP_def)
   325 qed (force dest: finite_UnionD simp add: setsum_def)
   326 
   327 (*But we can't get rid of finite A. If infinite, although the lhs is 0, 
   328   the rhs need not be, since SIGMA A B could still be finite.*)
   329 lemma (in comm_monoid_add) setsum_Sigma:
   330   assumes "finite A" and  "ALL x:A. finite (B x)"
   331   shows "(\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
   332 proof -
   333   interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
   334   from assms show ?thesis by (simp add: setsum_def fold_image_Sigma split_def)
   335 qed
   336 
   337 text{*Here we can eliminate the finiteness assumptions, by cases.*}
   338 lemma setsum_cartesian_product: 
   339    "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)"
   340 apply (cases "finite A") 
   341  apply (cases "finite B") 
   342   apply (simp add: setsum_Sigma)
   343  apply (cases "A={}", simp)
   344  apply (simp) 
   345 apply (auto simp add: setsum_def
   346             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
   347 done
   348 
   349 lemma (in comm_monoid_add) setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
   350   by (cases "finite A") (simp_all add: setsum.distrib)
   351 
   352 
   353 subsubsection {* Properties in more restricted classes of structures *}
   354 
   355 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   356 apply (case_tac "finite A")
   357  prefer 2 apply (simp add: setsum_def)
   358 apply (erule rev_mp)
   359 apply (erule finite_induct, auto)
   360 done
   361 
   362 lemma setsum_eq_0_iff [simp]:
   363     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   364 by (induct set: finite) auto
   365 
   366 lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
   367   (setsum f A = Suc 0) = (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
   368 apply(erule finite_induct)
   369 apply (auto simp add:add_is_1)
   370 done
   371 
   372 lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
   373 
   374 lemma setsum_Un_nat: "finite A ==> finite B ==>
   375   (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   376   -- {* For the natural numbers, we have subtraction. *}
   377 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
   378 
   379 lemma setsum_Un: "finite A ==> finite B ==>
   380   (setsum f (A Un B) :: 'a :: ab_group_add) =
   381    setsum f A + setsum f B - setsum f (A Int B)"
   382 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
   383 
   384 lemma (in comm_monoid_add) setsum_eq_general_reverses:
   385   assumes fS: "finite S" and fT: "finite T"
   386   and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
   387   and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x"
   388   shows "setsum f S = setsum g T"
   389 proof -
   390   interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
   391   show ?thesis
   392   apply (simp add: setsum_def fS fT)
   393   apply (rule fold_image_eq_general_inverses)
   394   apply (rule fS)
   395   apply (erule kh)
   396   apply (erule hk)
   397   done
   398 qed
   399 
   400 lemma (in comm_monoid_add) setsum_Un_zero:  
   401   assumes fS: "finite S" and fT: "finite T"
   402   and I0: "\<forall>x \<in> S\<inter>T. f x = 0"
   403   shows "setsum f (S \<union> T) = setsum f S  + setsum f T"
   404 proof -
   405   interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
   406   show ?thesis
   407   using fS fT
   408   apply (simp add: setsum_def)
   409   apply (rule fold_image_Un_one)
   410   using I0 by auto
   411 qed
   412 
   413 lemma setsum_UNION_zero: 
   414   assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T"
   415   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"
   416   shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S"
   417   using fSS f0
   418 proof(induct rule: finite_induct[OF fS])
   419   case 1 thus ?case by simp
   420 next
   421   case (2 T F)
   422   then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F" 
   423     and H: "setsum f (\<Union> F) = setsum (setsum f) F" by auto
   424   from fTF have fUF: "finite (\<Union>F)" by auto
   425   from "2.prems" TF fTF
   426   show ?case 
   427     by (auto simp add: H[symmetric] intro: setsum_Un_zero[OF fTF(1) fUF, of f])
   428 qed
   429 
   430 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
   431   (if a:A then setsum f A - f a else setsum f A)"
   432 apply (case_tac "finite A")
   433  prefer 2 apply (simp add: setsum_def)
   434 apply (erule finite_induct)
   435  apply (auto simp add: insert_Diff_if)
   436 apply (drule_tac a = a in mk_disjoint_insert, auto)
   437 done
   438 
   439 lemma setsum_diff1: "finite A \<Longrightarrow>
   440   (setsum f (A - {a}) :: ('a::ab_group_add)) =
   441   (if a:A then setsum f A - f a else setsum f A)"
   442 by (erule finite_induct) (auto simp add: insert_Diff_if)
   443 
   444 lemma setsum_diff1'[rule_format]:
   445   "finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x)"
   446 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))"])
   447 apply (auto simp add: insert_Diff_if add_ac)
   448 done
   449 
   450 lemma setsum_diff1_ring: assumes "finite A" "a \<in> A"
   451   shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)"
   452 unfolding setsum_diff1'[OF assms] by auto
   453 
   454 (* By Jeremy Siek: *)
   455 
   456 lemma setsum_diff_nat: 
   457 assumes "finite B" and "B \<subseteq> A"
   458 shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
   459 using assms
   460 proof induct
   461   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
   462 next
   463   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
   464     and xFinA: "insert x F \<subseteq> A"
   465     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
   466   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
   467   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
   468     by (simp add: setsum_diff1_nat)
   469   from xFinA have "F \<subseteq> A" by simp
   470   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
   471   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
   472     by simp
   473   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
   474   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
   475     by simp
   476   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
   477   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
   478     by simp
   479   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
   480 qed
   481 
   482 lemma setsum_diff:
   483   assumes le: "finite A" "B \<subseteq> A"
   484   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
   485 proof -
   486   from le have finiteB: "finite B" using finite_subset by auto
   487   show ?thesis using finiteB le
   488   proof induct
   489     case empty
   490     thus ?case by auto
   491   next
   492     case (insert x F)
   493     thus ?case using le finiteB 
   494       by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
   495   qed
   496 qed
   497 
   498 lemma setsum_mono:
   499   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, ordered_ab_semigroup_add}))"
   500   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
   501 proof (cases "finite K")
   502   case True
   503   thus ?thesis using le
   504   proof induct
   505     case empty
   506     thus ?case by simp
   507   next
   508     case insert
   509     thus ?case using add_mono by fastforce
   510   qed
   511 next
   512   case False
   513   thus ?thesis
   514     by (simp add: setsum_def)
   515 qed
   516 
   517 lemma setsum_strict_mono:
   518   fixes f :: "'a \<Rightarrow> 'b::{ordered_cancel_ab_semigroup_add,comm_monoid_add}"
   519   assumes "finite A"  "A \<noteq> {}"
   520     and "!!x. x:A \<Longrightarrow> f x < g x"
   521   shows "setsum f A < setsum g A"
   522   using assms
   523 proof (induct rule: finite_ne_induct)
   524   case singleton thus ?case by simp
   525 next
   526   case insert thus ?case by (auto simp: add_strict_mono)
   527 qed
   528 
   529 lemma setsum_strict_mono_ex1:
   530 fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_cancel_ab_semigroup_add}"
   531 assumes "finite A" and "ALL x:A. f x \<le> g x" and "EX a:A. f a < g a"
   532 shows "setsum f A < setsum g A"
   533 proof-
   534   from assms(3) obtain a where a: "a:A" "f a < g a" by blast
   535   have "setsum f A = setsum f ((A-{a}) \<union> {a})"
   536     by(simp add:insert_absorb[OF `a:A`])
   537   also have "\<dots> = setsum f (A-{a}) + setsum f {a}"
   538     using `finite A` by(subst setsum_Un_disjoint) auto
   539   also have "setsum f (A-{a}) \<le> setsum g (A-{a})"
   540     by(rule setsum_mono)(simp add: assms(2))
   541   also have "setsum f {a} < setsum g {a}" using a by simp
   542   also have "setsum g (A - {a}) + setsum g {a} = setsum g((A-{a}) \<union> {a})"
   543     using `finite A` by(subst setsum_Un_disjoint[symmetric]) auto
   544   also have "\<dots> = setsum g A" by(simp add:insert_absorb[OF `a:A`])
   545   finally show ?thesis by (metis add_right_mono add_strict_left_mono)
   546 qed
   547 
   548 lemma setsum_negf:
   549   "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
   550 proof (cases "finite A")
   551   case True thus ?thesis by (induct set: finite) auto
   552 next
   553   case False thus ?thesis by (simp add: setsum_def)
   554 qed
   555 
   556 lemma setsum_subtractf:
   557   "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
   558     setsum f A - setsum g A"
   559 proof (cases "finite A")
   560   case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
   561 next
   562   case False thus ?thesis by (simp add: setsum_def)
   563 qed
   564 
   565 lemma setsum_nonneg:
   566   assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
   567   shows "0 \<le> setsum f A"
   568 proof (cases "finite A")
   569   case True thus ?thesis using nn
   570   proof induct
   571     case empty then show ?case by simp
   572   next
   573     case (insert x F)
   574     then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
   575     with insert show ?case by simp
   576   qed
   577 next
   578   case False thus ?thesis by (simp add: setsum_def)
   579 qed
   580 
   581 lemma setsum_nonpos:
   582   assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{ordered_ab_semigroup_add,comm_monoid_add})"
   583   shows "setsum f A \<le> 0"
   584 proof (cases "finite A")
   585   case True thus ?thesis using np
   586   proof induct
   587     case empty then show ?case by simp
   588   next
   589     case (insert x F)
   590     then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
   591     with insert show ?case by simp
   592   qed
   593 next
   594   case False thus ?thesis by (simp add: setsum_def)
   595 qed
   596 
   597 lemma setsum_nonneg_leq_bound:
   598   fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
   599   assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s"
   600   shows "f i \<le> B"
   601 proof -
   602   have "0 \<le> (\<Sum> i \<in> s - {i}. f i)" and "0 \<le> f i"
   603     using assms by (auto intro!: setsum_nonneg)
   604   moreover
   605   have "(\<Sum> i \<in> s - {i}. f i) + f i = B"
   606     using assms by (simp add: setsum_diff1)
   607   ultimately show ?thesis by auto
   608 qed
   609 
   610 lemma setsum_nonneg_0:
   611   fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
   612   assumes "finite s" and pos: "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
   613   and "(\<Sum> i \<in> s. f i) = 0" and i: "i \<in> s"
   614   shows "f i = 0"
   615   using setsum_nonneg_leq_bound[OF assms] pos[OF i] by auto
   616 
   617 lemma setsum_mono2:
   618 fixes f :: "'a \<Rightarrow> 'b :: ordered_comm_monoid_add"
   619 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
   620 shows "setsum f A \<le> setsum f B"
   621 proof -
   622   have "setsum f A \<le> setsum f A + setsum f (B-A)"
   623     by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
   624   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
   625     by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
   626   also have "A \<union> (B-A) = B" using sub by blast
   627   finally show ?thesis .
   628 qed
   629 
   630 lemma setsum_mono3: "finite B ==> A <= B ==> 
   631     ALL x: B - A. 
   632       0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==>
   633         setsum f A <= setsum f B"
   634   apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
   635   apply (erule ssubst)
   636   apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
   637   apply simp
   638   apply (rule add_left_mono)
   639   apply (erule setsum_nonneg)
   640   apply (subst setsum_Un_disjoint [THEN sym])
   641   apply (erule finite_subset, assumption)
   642   apply (rule finite_subset)
   643   prefer 2
   644   apply assumption
   645   apply (auto simp add: sup_absorb2)
   646 done
   647 
   648 lemma setsum_right_distrib: 
   649   fixes f :: "'a => ('b::semiring_0)"
   650   shows "r * setsum f A = setsum (%n. r * f n) A"
   651 proof (cases "finite A")
   652   case True
   653   thus ?thesis
   654   proof induct
   655     case empty thus ?case by simp
   656   next
   657     case (insert x A) thus ?case by (simp add: right_distrib)
   658   qed
   659 next
   660   case False thus ?thesis by (simp add: setsum_def)
   661 qed
   662 
   663 lemma setsum_left_distrib:
   664   "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
   665 proof (cases "finite A")
   666   case True
   667   then show ?thesis
   668   proof induct
   669     case empty thus ?case by simp
   670   next
   671     case (insert x A) thus ?case by (simp add: left_distrib)
   672   qed
   673 next
   674   case False thus ?thesis by (simp add: setsum_def)
   675 qed
   676 
   677 lemma setsum_divide_distrib:
   678   "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
   679 proof (cases "finite A")
   680   case True
   681   then show ?thesis
   682   proof induct
   683     case empty thus ?case by simp
   684   next
   685     case (insert x A) thus ?case by (simp add: add_divide_distrib)
   686   qed
   687 next
   688   case False thus ?thesis by (simp add: setsum_def)
   689 qed
   690 
   691 lemma setsum_abs[iff]: 
   692   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   693   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
   694 proof (cases "finite A")
   695   case True
   696   thus ?thesis
   697   proof induct
   698     case empty thus ?case by simp
   699   next
   700     case (insert x A)
   701     thus ?case by (auto intro: abs_triangle_ineq order_trans)
   702   qed
   703 next
   704   case False thus ?thesis by (simp add: setsum_def)
   705 qed
   706 
   707 lemma setsum_abs_ge_zero[iff]: 
   708   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   709   shows "0 \<le> setsum (%i. abs(f i)) A"
   710 proof (cases "finite A")
   711   case True
   712   thus ?thesis
   713   proof induct
   714     case empty thus ?case by simp
   715   next
   716     case (insert x A) thus ?case by auto
   717   qed
   718 next
   719   case False thus ?thesis by (simp add: setsum_def)
   720 qed
   721 
   722 lemma abs_setsum_abs[simp]: 
   723   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   724   shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
   725 proof (cases "finite A")
   726   case True
   727   thus ?thesis
   728   proof induct
   729     case empty thus ?case by simp
   730   next
   731     case (insert a A)
   732     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
   733     also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
   734     also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
   735       by (simp del: abs_of_nonneg)
   736     also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
   737     finally show ?case .
   738   qed
   739 next
   740   case False thus ?thesis by (simp add: setsum_def)
   741 qed
   742 
   743 lemma setsum_Plus:
   744   fixes A :: "'a set" and B :: "'b set"
   745   assumes fin: "finite A" "finite B"
   746   shows "setsum f (A <+> B) = setsum (f \<circ> Inl) A + setsum (f \<circ> Inr) B"
   747 proof -
   748   have "A <+> B = Inl ` A \<union> Inr ` B" by auto
   749   moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)"
   750     by auto
   751   moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto
   752   moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI)
   753   ultimately show ?thesis using fin by(simp add: setsum_Un_disjoint setsum_reindex)
   754 qed
   755 
   756 
   757 text {* Commuting outer and inner summation *}
   758 
   759 lemma setsum_commute:
   760   "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
   761 proof (simp add: setsum_cartesian_product)
   762   have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
   763     (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
   764     (is "?s = _")
   765     apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on)
   766     apply (simp add: split_def)
   767     done
   768   also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
   769     (is "_ = ?t")
   770     apply (simp add: swap_product)
   771     done
   772   finally show "?s = ?t" .
   773 qed
   774 
   775 lemma setsum_product:
   776   fixes f :: "'a => ('b::semiring_0)"
   777   shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
   778   by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
   779 
   780 lemma setsum_mult_setsum_if_inj:
   781 fixes f :: "'a => ('b::semiring_0)"
   782 shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==>
   783   setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}"
   784 by(auto simp: setsum_product setsum_cartesian_product
   785         intro!:  setsum_reindex_cong[symmetric])
   786 
   787 lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
   788 apply (cases "finite A")
   789 apply (erule finite_induct)
   790 apply (auto simp add: algebra_simps)
   791 done
   792 
   793 lemma setsum_bounded:
   794   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
   795   shows "setsum f A \<le> of_nat(card A) * K"
   796 proof (cases "finite A")
   797   case True
   798   thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
   799 next
   800   case False thus ?thesis by (simp add: setsum_def)
   801 qed
   802 
   803 
   804 subsubsection {* Cardinality as special case of @{const setsum} *}
   805 
   806 lemma card_eq_setsum:
   807   "card A = setsum (\<lambda>x. 1) A"
   808   by (simp only: card_def setsum_def)
   809 
   810 lemma card_UN_disjoint:
   811   assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
   812     and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
   813   shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
   814 proof -
   815   have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)" by simp
   816   with assms show ?thesis by (simp add: card_eq_setsum setsum_UN_disjoint del: setsum_constant)
   817 qed
   818 
   819 lemma card_Union_disjoint:
   820   "finite C ==> (ALL A:C. finite A) ==>
   821    (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
   822    ==> card (Union C) = setsum card C"
   823 apply (frule card_UN_disjoint [of C id])
   824 apply (simp_all add: SUP_def id_def)
   825 done
   826 
   827 text{*The image of a finite set can be expressed using @{term fold_image}.*}
   828 lemma image_eq_fold_image:
   829   "finite A ==> f ` A = fold_image (op Un) (%x. {f x}) {} A"
   830 proof (induct rule: finite_induct)
   831   case empty then show ?case by simp
   832 next
   833   interpret ab_semigroup_mult "op Un"
   834     proof qed auto
   835   case insert 
   836   then show ?case by simp
   837 qed
   838 
   839 subsubsection {* Cardinality of products *}
   840 
   841 lemma card_SigmaI [simp]:
   842   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
   843   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
   844 by(simp add: card_eq_setsum setsum_Sigma del:setsum_constant)
   845 
   846 (*
   847 lemma SigmaI_insert: "y \<notin> A ==>
   848   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
   849   by auto
   850 *)
   851 
   852 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
   853   by (cases "finite A \<and> finite B")
   854     (auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2)
   855 
   856 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
   857 by (simp add: card_cartesian_product)
   858 
   859 
   860 subsection {* Generalized product over a set *}
   861 
   862 definition (in comm_monoid_mult) setprod :: "('b \<Rightarrow> 'a) => 'b set => 'a" where
   863   "setprod f A = (if finite A then fold_image (op *) f 1 A else 1)"
   864 
   865 sublocale comm_monoid_mult < setprod!: comm_monoid_big "op *" 1 setprod proof
   866 qed (fact setprod_def)
   867 
   868 abbreviation
   869   Setprod  ("\<Prod>_" [1000] 999) where
   870   "\<Prod>A == setprod (%x. x) A"
   871 
   872 syntax
   873   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
   874 syntax (xsymbols)
   875   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
   876 syntax (HTML output)
   877   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
   878 
   879 translations -- {* Beware of argument permutation! *}
   880   "PROD i:A. b" == "CONST setprod (%i. b) A" 
   881   "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A" 
   882 
   883 text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
   884  @{text"\<Prod>x|P. e"}. *}
   885 
   886 syntax
   887   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
   888 syntax (xsymbols)
   889   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
   890 syntax (HTML output)
   891   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
   892 
   893 translations
   894   "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
   895   "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
   896 
   897 lemma setprod_empty: "setprod f {} = 1"
   898   by (fact setprod.empty)
   899 
   900 lemma setprod_insert: "[| finite A; a \<notin> A |] ==>
   901     setprod f (insert a A) = f a * setprod f A"
   902   by (fact setprod.insert)
   903 
   904 lemma setprod_infinite: "~ finite A ==> setprod f A = 1"
   905   by (fact setprod.infinite)
   906 
   907 lemma setprod_reindex:
   908    "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
   909 by(auto simp: setprod_def fold_image_reindex dest!:finite_imageD)
   910 
   911 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
   912 by (auto simp add: setprod_reindex)
   913 
   914 lemma setprod_cong:
   915   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
   916 by(fastforce simp: setprod_def intro: fold_image_cong)
   917 
   918 lemma strong_setprod_cong[cong]:
   919   "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
   920 by(fastforce simp: simp_implies_def setprod_def intro: fold_image_cong)
   921 
   922 lemma setprod_reindex_cong: "inj_on f A ==>
   923     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
   924 by (frule setprod_reindex, simp)
   925 
   926 lemma strong_setprod_reindex_cong: assumes i: "inj_on f A"
   927   and B: "B = f ` A" and eq: "\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x"
   928   shows "setprod h B = setprod g A"
   929 proof-
   930     have "setprod h B = setprod (h o f) A"
   931       by (simp add: B setprod_reindex[OF i, of h])
   932     then show ?thesis apply simp
   933       apply (rule setprod_cong)
   934       apply simp
   935       by (simp add: eq)
   936 qed
   937 
   938 lemma setprod_Un_one:  
   939   assumes fS: "finite S" and fT: "finite T"
   940   and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
   941   shows "setprod f (S \<union> T) = setprod f S  * setprod f T"
   942   using fS fT
   943   apply (simp add: setprod_def)
   944   apply (rule fold_image_Un_one)
   945   using I0 by auto
   946 
   947 
   948 lemmas setprod_1 = setprod.F_unit
   949 lemmas setprod_1' = setprod.F_unit'
   950 
   951 
   952 lemma setprod_Un_Int: "finite A ==> finite B
   953     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
   954 by(simp add: setprod_def fold_image_Un_Int[symmetric])
   955 
   956 lemma setprod_Un_disjoint: "finite A ==> finite B
   957   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
   958 by (subst setprod_Un_Int [symmetric], auto)
   959 
   960 lemma setprod_mono_one_left: 
   961   assumes fT: "finite T" and ST: "S \<subseteq> T"
   962   and z: "\<forall>i \<in> T - S. f i = 1"
   963   shows "setprod f S = setprod f T"
   964 proof-
   965   have eq: "T = S \<union> (T - S)" using ST by blast
   966   have d: "S \<inter> (T - S) = {}" using ST by blast
   967   from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
   968   show ?thesis
   969   by (simp add: setprod_Un_disjoint[OF f d, unfolded eq[symmetric]] setprod_1'[OF z])
   970 qed
   971 
   972 lemmas setprod_mono_one_right = setprod_mono_one_left [THEN sym]
   973 
   974 lemma setprod_delta: 
   975   assumes fS: "finite S"
   976   shows "setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
   977 proof-
   978   let ?f = "(\<lambda>k. if k=a then b k else 1)"
   979   {assume a: "a \<notin> S"
   980     hence "\<forall> k\<in> S. ?f k = 1" by simp
   981     hence ?thesis  using a by (simp add: setprod_1) }
   982   moreover 
   983   {assume a: "a \<in> S"
   984     let ?A = "S - {a}"
   985     let ?B = "{a}"
   986     have eq: "S = ?A \<union> ?B" using a by blast 
   987     have dj: "?A \<inter> ?B = {}" by simp
   988     from fS have fAB: "finite ?A" "finite ?B" by auto  
   989     have fA1: "setprod ?f ?A = 1" apply (rule setprod_1') by auto
   990     have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
   991       using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
   992       by simp
   993     then have ?thesis using a by (simp add: fA1 cong: setprod_cong cong del: if_weak_cong)}
   994   ultimately show ?thesis by blast
   995 qed
   996 
   997 lemma setprod_delta': 
   998   assumes fS: "finite S" shows 
   999   "setprod (\<lambda>k. if a = k then b k else 1) S = 
  1000      (if a\<in> S then b a else 1)"
  1001   using setprod_delta[OF fS, of a b, symmetric] 
  1002   by (auto intro: setprod_cong)
  1003 
  1004 
  1005 lemma setprod_UN_disjoint:
  1006     "finite I ==> (ALL i:I. finite (A i)) ==>
  1007         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1008       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
  1009   by (simp add: setprod_def fold_image_UN_disjoint)
  1010 
  1011 lemma setprod_Union_disjoint:
  1012   assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}" 
  1013   shows "setprod f (Union C) = setprod (setprod f) C"
  1014 proof cases
  1015   assume "finite C"
  1016   from setprod_UN_disjoint[OF this assms]
  1017   show ?thesis
  1018     by (simp add: SUP_def)
  1019 qed (force dest: finite_UnionD simp add: setprod_def)
  1020 
  1021 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  1022     (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
  1023     (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
  1024 by(simp add:setprod_def fold_image_Sigma split_def)
  1025 
  1026 text{*Here we can eliminate the finiteness assumptions, by cases.*}
  1027 lemma setprod_cartesian_product: 
  1028      "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
  1029 apply (cases "finite A") 
  1030  apply (cases "finite B") 
  1031   apply (simp add: setprod_Sigma)
  1032  apply (cases "A={}", simp)
  1033  apply (simp add: setprod_1) 
  1034 apply (auto simp add: setprod_def
  1035             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
  1036 done
  1037 
  1038 lemma setprod_timesf:
  1039      "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
  1040 by(simp add:setprod_def fold_image_distrib)
  1041 
  1042 
  1043 subsubsection {* Properties in more restricted classes of structures *}
  1044 
  1045 lemma setprod_eq_1_iff [simp]:
  1046   "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
  1047 by (induct set: finite) auto
  1048 
  1049 lemma setprod_zero:
  1050      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
  1051 apply (induct set: finite, force, clarsimp)
  1052 apply (erule disjE, auto)
  1053 done
  1054 
  1055 lemma setprod_nonneg [rule_format]:
  1056    "(ALL x: A. (0::'a::linordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
  1057 by (cases "finite A", induct set: finite, simp_all add: mult_nonneg_nonneg)
  1058 
  1059 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x)
  1060   --> 0 < setprod f A"
  1061 by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos)
  1062 
  1063 lemma setprod_zero_iff[simp]: "finite A ==> 
  1064   (setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) =
  1065   (EX x: A. f x = 0)"
  1066 by (erule finite_induct, auto simp:no_zero_divisors)
  1067 
  1068 lemma setprod_pos_nat:
  1069   "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
  1070 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
  1071 
  1072 lemma setprod_pos_nat_iff[simp]:
  1073   "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
  1074 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
  1075 
  1076 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
  1077   (setprod f (A Un B) :: 'a ::{field})
  1078    = setprod f A * setprod f B / setprod f (A Int B)"
  1079 by (subst setprod_Un_Int [symmetric], auto)
  1080 
  1081 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
  1082   (setprod f (A - {a}) :: 'a :: {field}) =
  1083   (if a:A then setprod f A / f a else setprod f A)"
  1084   by (erule finite_induct) (auto simp add: insert_Diff_if)
  1085 
  1086 lemma setprod_inversef: 
  1087   fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
  1088   shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)"
  1089 by (erule finite_induct) auto
  1090 
  1091 lemma setprod_dividef:
  1092   fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
  1093   shows "finite A
  1094     ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
  1095 apply (subgoal_tac
  1096          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
  1097 apply (erule ssubst)
  1098 apply (subst divide_inverse)
  1099 apply (subst setprod_timesf)
  1100 apply (subst setprod_inversef, assumption+, rule refl)
  1101 apply (rule setprod_cong, rule refl)
  1102 apply (subst divide_inverse, auto)
  1103 done
  1104 
  1105 lemma setprod_dvd_setprod [rule_format]: 
  1106     "(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A"
  1107   apply (cases "finite A")
  1108   apply (induct set: finite)
  1109   apply (auto simp add: dvd_def)
  1110   apply (rule_tac x = "k * ka" in exI)
  1111   apply (simp add: algebra_simps)
  1112 done
  1113 
  1114 lemma setprod_dvd_setprod_subset:
  1115   "finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B"
  1116   apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)")
  1117   apply (unfold dvd_def, blast)
  1118   apply (subst setprod_Un_disjoint [symmetric])
  1119   apply (auto elim: finite_subset intro: setprod_cong)
  1120 done
  1121 
  1122 lemma setprod_dvd_setprod_subset2:
  1123   "finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow> 
  1124       setprod f A dvd setprod g B"
  1125   apply (rule dvd_trans)
  1126   apply (rule setprod_dvd_setprod, erule (1) bspec)
  1127   apply (erule (1) setprod_dvd_setprod_subset)
  1128 done
  1129 
  1130 lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow> 
  1131     (f i ::'a::comm_semiring_1) dvd setprod f A"
  1132 by (induct set: finite) (auto intro: dvd_mult)
  1133 
  1134 lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow> 
  1135     (d::'a::comm_semiring_1) dvd (SUM x : A. f x)"
  1136   apply (cases "finite A")
  1137   apply (induct set: finite)
  1138   apply auto
  1139 done
  1140 
  1141 lemma setprod_mono:
  1142   fixes f :: "'a \<Rightarrow> 'b\<Colon>linordered_semidom"
  1143   assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i"
  1144   shows "setprod f A \<le> setprod g A"
  1145 proof (cases "finite A")
  1146   case True
  1147   hence ?thesis "setprod f A \<ge> 0" using subset_refl[of A]
  1148   proof (induct A rule: finite_subset_induct)
  1149     case (insert a F)
  1150     thus "setprod f (insert a F) \<le> setprod g (insert a F)" "0 \<le> setprod f (insert a F)"
  1151       unfolding setprod_insert[OF insert(1,3)]
  1152       using assms[rule_format,OF insert(2)] insert
  1153       by (auto intro: mult_mono mult_nonneg_nonneg)
  1154   qed auto
  1155   thus ?thesis by simp
  1156 qed auto
  1157 
  1158 lemma abs_setprod:
  1159   fixes f :: "'a \<Rightarrow> 'b\<Colon>{linordered_field,abs}"
  1160   shows "abs (setprod f A) = setprod (\<lambda>x. abs (f x)) A"
  1161 proof (cases "finite A")
  1162   case True thus ?thesis
  1163     by induct (auto simp add: field_simps abs_mult)
  1164 qed auto
  1165 
  1166 lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
  1167 apply (erule finite_induct)
  1168 apply auto
  1169 done
  1170 
  1171 lemma setprod_gen_delta:
  1172   assumes fS: "finite S"
  1173   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)"
  1174 proof-
  1175   let ?f = "(\<lambda>k. if k=a then b k else c)"
  1176   {assume a: "a \<notin> S"
  1177     hence "\<forall> k\<in> S. ?f k = c" by simp
  1178     hence ?thesis  using a setprod_constant[OF fS, of c] by (simp add: setprod_1 cong add: setprod_cong) }
  1179   moreover 
  1180   {assume a: "a \<in> S"
  1181     let ?A = "S - {a}"
  1182     let ?B = "{a}"
  1183     have eq: "S = ?A \<union> ?B" using a by blast 
  1184     have dj: "?A \<inter> ?B = {}" by simp
  1185     from fS have fAB: "finite ?A" "finite ?B" by auto  
  1186     have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
  1187       apply (rule setprod_cong) by auto
  1188     have cA: "card ?A = card S - 1" using fS a by auto
  1189     have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
  1190     have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
  1191       using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
  1192       by simp
  1193     then have ?thesis using a cA
  1194       by (simp add: fA1 field_simps cong add: setprod_cong cong del: if_weak_cong)}
  1195   ultimately show ?thesis by blast
  1196 qed
  1197 
  1198 
  1199 subsection {* Versions of @{const inf} and @{const sup} on non-empty sets *}
  1200 
  1201 no_notation times (infixl "*" 70)
  1202 no_notation Groups.one ("1")
  1203 
  1204 locale semilattice_big = semilattice +
  1205   fixes F :: "'a set \<Rightarrow> 'a"
  1206   assumes F_eq: "finite A \<Longrightarrow> F A = fold1 (op *) A"
  1207 
  1208 sublocale semilattice_big < folding_one_idem proof
  1209 qed (simp_all add: F_eq)
  1210 
  1211 notation times (infixl "*" 70)
  1212 notation Groups.one ("1")
  1213 
  1214 context lattice
  1215 begin
  1216 
  1217 definition Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900) where
  1218   "Inf_fin = fold1 inf"
  1219 
  1220 definition Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900) where
  1221   "Sup_fin = fold1 sup"
  1222 
  1223 end
  1224 
  1225 sublocale lattice < Inf_fin!: semilattice_big inf Inf_fin proof
  1226 qed (simp add: Inf_fin_def)
  1227 
  1228 sublocale lattice < Sup_fin!: semilattice_big sup Sup_fin proof
  1229 qed (simp add: Sup_fin_def)
  1230 
  1231 context semilattice_inf
  1232 begin
  1233 
  1234 lemma ab_semigroup_idem_mult_inf:
  1235   "class.ab_semigroup_idem_mult inf"
  1236 proof qed (rule inf_assoc inf_commute inf_idem)+
  1237 
  1238 lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> Finite_Set.fold inf b (insert a A) = inf a (Finite_Set.fold inf b A)"
  1239 by(rule comp_fun_idem.fold_insert_idem[OF ab_semigroup_idem_mult.comp_fun_idem[OF ab_semigroup_idem_mult_inf]])
  1240 
  1241 lemma inf_le_fold_inf: "finite A \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> Finite_Set.fold inf c A"
  1242 by (induct pred: finite) (auto intro: le_infI1)
  1243 
  1244 lemma fold_inf_le_inf: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> Finite_Set.fold inf b A \<le> inf a b"
  1245 proof(induct arbitrary: a pred:finite)
  1246   case empty thus ?case by simp
  1247 next
  1248   case (insert x A)
  1249   show ?case
  1250   proof cases
  1251     assume "A = {}" thus ?thesis using insert by simp
  1252   next
  1253     assume "A \<noteq> {}" thus ?thesis using insert by (auto intro: le_infI2)
  1254   qed
  1255 qed
  1256 
  1257 lemma below_fold1_iff:
  1258   assumes "finite A" "A \<noteq> {}"
  1259   shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
  1260 proof -
  1261   interpret ab_semigroup_idem_mult inf
  1262     by (rule ab_semigroup_idem_mult_inf)
  1263   show ?thesis using assms by (induct rule: finite_ne_induct) simp_all
  1264 qed
  1265 
  1266 lemma fold1_belowI:
  1267   assumes "finite A"
  1268     and "a \<in> A"
  1269   shows "fold1 inf A \<le> a"
  1270 proof -
  1271   from assms have "A \<noteq> {}" by auto
  1272   from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
  1273   proof (induct rule: finite_ne_induct)
  1274     case singleton thus ?case by simp
  1275   next
  1276     interpret ab_semigroup_idem_mult inf
  1277       by (rule ab_semigroup_idem_mult_inf)
  1278     case (insert x F)
  1279     from insert(5) have "a = x \<or> a \<in> F" by simp
  1280     thus ?case
  1281     proof
  1282       assume "a = x" thus ?thesis using insert
  1283         by (simp add: mult_ac)
  1284     next
  1285       assume "a \<in> F"
  1286       hence bel: "fold1 inf F \<le> a" by (rule insert)
  1287       have "inf (fold1 inf (insert x F)) a = inf x (inf (fold1 inf F) a)"
  1288         using insert by (simp add: mult_ac)
  1289       also have "inf (fold1 inf F) a = fold1 inf F"
  1290         using bel by (auto intro: antisym)
  1291       also have "inf x \<dots> = fold1 inf (insert x F)"
  1292         using insert by (simp add: mult_ac)
  1293       finally have aux: "inf (fold1 inf (insert x F)) a = fold1 inf (insert x F)" .
  1294       moreover have "inf (fold1 inf (insert x F)) a \<le> a" by simp
  1295       ultimately show ?thesis by simp
  1296     qed
  1297   qed
  1298 qed
  1299 
  1300 end
  1301 
  1302 context semilattice_sup
  1303 begin
  1304 
  1305 lemma ab_semigroup_idem_mult_sup: "class.ab_semigroup_idem_mult sup"
  1306 by (rule semilattice_inf.ab_semigroup_idem_mult_inf)(rule dual_semilattice)
  1307 
  1308 lemma fold_sup_insert[simp]: "finite A \<Longrightarrow> Finite_Set.fold sup b (insert a A) = sup a (Finite_Set.fold sup b A)"
  1309 by(rule semilattice_inf.fold_inf_insert)(rule dual_semilattice)
  1310 
  1311 lemma fold_sup_le_sup: "finite A \<Longrightarrow> ALL a:A. a \<le> b \<Longrightarrow> Finite_Set.fold sup c A \<le> sup b c"
  1312 by(rule semilattice_inf.inf_le_fold_inf)(rule dual_semilattice)
  1313 
  1314 lemma sup_le_fold_sup: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a b \<le> Finite_Set.fold sup b A"
  1315 by(rule semilattice_inf.fold_inf_le_inf)(rule dual_semilattice)
  1316 
  1317 end
  1318 
  1319 context lattice
  1320 begin
  1321 
  1322 lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A"
  1323 apply(unfold Sup_fin_def Inf_fin_def)
  1324 apply(subgoal_tac "EX a. a:A")
  1325 prefer 2 apply blast
  1326 apply(erule exE)
  1327 apply(rule order_trans)
  1328 apply(erule (1) fold1_belowI)
  1329 apply(erule (1) semilattice_inf.fold1_belowI [OF dual_semilattice])
  1330 done
  1331 
  1332 lemma sup_Inf_absorb [simp]:
  1333   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^bsub>fin\<^esub>A) = a"
  1334 apply(subst sup_commute)
  1335 apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI)
  1336 done
  1337 
  1338 lemma inf_Sup_absorb [simp]:
  1339   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a"
  1340 by (simp add: Sup_fin_def inf_absorb1
  1341   semilattice_inf.fold1_belowI [OF dual_semilattice])
  1342 
  1343 end
  1344 
  1345 context distrib_lattice
  1346 begin
  1347 
  1348 lemma sup_Inf1_distrib:
  1349   assumes "finite A"
  1350     and "A \<noteq> {}"
  1351   shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
  1352 proof -
  1353   interpret ab_semigroup_idem_mult inf
  1354     by (rule ab_semigroup_idem_mult_inf)
  1355   from assms show ?thesis
  1356     by (simp add: Inf_fin_def image_def
  1357       hom_fold1_commute [where h="sup x", OF sup_inf_distrib1])
  1358         (rule arg_cong [where f="fold1 inf"], blast)
  1359 qed
  1360 
  1361 lemma sup_Inf2_distrib:
  1362   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  1363   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}"
  1364 using A proof (induct rule: finite_ne_induct)
  1365   case singleton thus ?case
  1366     by (simp add: sup_Inf1_distrib [OF B])
  1367 next
  1368   interpret ab_semigroup_idem_mult inf
  1369     by (rule ab_semigroup_idem_mult_inf)
  1370   case (insert x A)
  1371   have finB: "finite {sup x b |b. b \<in> B}"
  1372     by(rule finite_surj[where f = "sup x", OF B(1)], auto)
  1373   have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
  1374   proof -
  1375     have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
  1376       by blast
  1377     thus ?thesis by(simp add: insert(1) B(1))
  1378   qed
  1379   have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  1380   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)"
  1381     using insert by simp
  1382   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)
  1383   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})"
  1384     using insert by(simp add:sup_Inf1_distrib[OF B])
  1385   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})"
  1386     (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M")
  1387     using B insert
  1388     by (simp add: Inf_fin_def fold1_Un2 [OF finB _ finAB ne])
  1389   also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
  1390     by blast
  1391   finally show ?case .
  1392 qed
  1393 
  1394 lemma inf_Sup1_distrib:
  1395   assumes "finite A" and "A \<noteq> {}"
  1396   shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
  1397 proof -
  1398   interpret ab_semigroup_idem_mult sup
  1399     by (rule ab_semigroup_idem_mult_sup)
  1400   from assms show ?thesis
  1401     by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1])
  1402       (rule arg_cong [where f="fold1 sup"], blast)
  1403 qed
  1404 
  1405 lemma inf_Sup2_distrib:
  1406   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  1407   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}"
  1408 using A proof (induct rule: finite_ne_induct)
  1409   case singleton thus ?case
  1410     by(simp add: inf_Sup1_distrib [OF B])
  1411 next
  1412   case (insert x A)
  1413   have finB: "finite {inf x b |b. b \<in> B}"
  1414     by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
  1415   have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
  1416   proof -
  1417     have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
  1418       by blast
  1419     thus ?thesis by(simp add: insert(1) B(1))
  1420   qed
  1421   have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  1422   interpret ab_semigroup_idem_mult sup
  1423     by (rule ab_semigroup_idem_mult_sup)
  1424   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)"
  1425     using insert by simp
  1426   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)
  1427   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})"
  1428     using insert by(simp add:inf_Sup1_distrib[OF B])
  1429   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})"
  1430     (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M")
  1431     using B insert
  1432     by (simp add: Sup_fin_def fold1_Un2 [OF finB _ finAB ne])
  1433   also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
  1434     by blast
  1435   finally show ?case .
  1436 qed
  1437 
  1438 end
  1439 
  1440 context complete_lattice
  1441 begin
  1442 
  1443 lemma Inf_fin_Inf:
  1444   assumes "finite A" and "A \<noteq> {}"
  1445   shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
  1446 proof -
  1447   interpret ab_semigroup_idem_mult inf
  1448     by (rule ab_semigroup_idem_mult_inf)
  1449   from `A \<noteq> {}` obtain b B where "A = {b} \<union> B" by auto
  1450   moreover with `finite A` have "finite B" by simp
  1451   ultimately show ?thesis
  1452     by (simp add: Inf_fin_def fold1_eq_fold_idem inf_Inf_fold_inf [symmetric])
  1453 qed
  1454 
  1455 lemma Sup_fin_Sup:
  1456   assumes "finite A" and "A \<noteq> {}"
  1457   shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
  1458 proof -
  1459   interpret ab_semigroup_idem_mult sup
  1460     by (rule ab_semigroup_idem_mult_sup)
  1461   from `A \<noteq> {}` obtain b B where "A = {b} \<union> B" by auto
  1462   moreover with `finite A` have "finite B" by simp
  1463   ultimately show ?thesis  
  1464   by (simp add: Sup_fin_def fold1_eq_fold_idem sup_Sup_fold_sup [symmetric])
  1465 qed
  1466 
  1467 end
  1468 
  1469 
  1470 subsection {* Versions of @{const min} and @{const max} on non-empty sets *}
  1471 
  1472 definition (in linorder) Min :: "'a set \<Rightarrow> 'a" where
  1473   "Min = fold1 min"
  1474 
  1475 definition (in linorder) Max :: "'a set \<Rightarrow> 'a" where
  1476   "Max = fold1 max"
  1477 
  1478 sublocale linorder < Min!: semilattice_big min Min proof
  1479 qed (simp add: Min_def)
  1480 
  1481 sublocale linorder < Max!: semilattice_big max Max proof
  1482 qed (simp add: Max_def)
  1483 
  1484 context linorder
  1485 begin
  1486 
  1487 lemmas Min_singleton = Min.singleton
  1488 lemmas Max_singleton = Max.singleton
  1489 
  1490 lemma Min_insert:
  1491   assumes "finite A" and "A \<noteq> {}"
  1492   shows "Min (insert x A) = min x (Min A)"
  1493   using assms by simp
  1494 
  1495 lemma Max_insert:
  1496   assumes "finite A" and "A \<noteq> {}"
  1497   shows "Max (insert x A) = max x (Max A)"
  1498   using assms by simp
  1499 
  1500 lemma Min_Un:
  1501   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
  1502   shows "Min (A \<union> B) = min (Min A) (Min B)"
  1503   using assms by (rule Min.union_idem)
  1504 
  1505 lemma Max_Un:
  1506   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
  1507   shows "Max (A \<union> B) = max (Max A) (Max B)"
  1508   using assms by (rule Max.union_idem)
  1509 
  1510 lemma hom_Min_commute:
  1511   assumes "\<And>x y. h (min x y) = min (h x) (h y)"
  1512     and "finite N" and "N \<noteq> {}"
  1513   shows "h (Min N) = Min (h ` N)"
  1514   using assms by (rule Min.hom_commute)
  1515 
  1516 lemma hom_Max_commute:
  1517   assumes "\<And>x y. h (max x y) = max (h x) (h y)"
  1518     and "finite N" and "N \<noteq> {}"
  1519   shows "h (Max N) = Max (h ` N)"
  1520   using assms by (rule Max.hom_commute)
  1521 
  1522 lemma ab_semigroup_idem_mult_min:
  1523   "class.ab_semigroup_idem_mult min"
  1524   proof qed (auto simp add: min_def)
  1525 
  1526 lemma ab_semigroup_idem_mult_max:
  1527   "class.ab_semigroup_idem_mult max"
  1528   proof qed (auto simp add: max_def)
  1529 
  1530 lemma max_lattice:
  1531   "class.semilattice_inf max (op \<ge>) (op >)"
  1532   by (fact min_max.dual_semilattice)
  1533 
  1534 lemma dual_max:
  1535   "ord.max (op \<ge>) = min"
  1536   by (auto simp add: ord.max_def min_def fun_eq_iff)
  1537 
  1538 lemma dual_min:
  1539   "ord.min (op \<ge>) = max"
  1540   by (auto simp add: ord.min_def max_def fun_eq_iff)
  1541 
  1542 lemma strict_below_fold1_iff:
  1543   assumes "finite A" and "A \<noteq> {}"
  1544   shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
  1545 proof -
  1546   interpret ab_semigroup_idem_mult min
  1547     by (rule ab_semigroup_idem_mult_min)
  1548   from assms show ?thesis
  1549   by (induct rule: finite_ne_induct)
  1550     (simp_all add: fold1_insert)
  1551 qed
  1552 
  1553 lemma fold1_below_iff:
  1554   assumes "finite A" and "A \<noteq> {}"
  1555   shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
  1556 proof -
  1557   interpret ab_semigroup_idem_mult min
  1558     by (rule ab_semigroup_idem_mult_min)
  1559   from assms show ?thesis
  1560   by (induct rule: finite_ne_induct)
  1561     (simp_all add: fold1_insert min_le_iff_disj)
  1562 qed
  1563 
  1564 lemma fold1_strict_below_iff:
  1565   assumes "finite A" and "A \<noteq> {}"
  1566   shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
  1567 proof -
  1568   interpret ab_semigroup_idem_mult min
  1569     by (rule ab_semigroup_idem_mult_min)
  1570   from assms show ?thesis
  1571   by (induct rule: finite_ne_induct)
  1572     (simp_all add: fold1_insert min_less_iff_disj)
  1573 qed
  1574 
  1575 lemma fold1_antimono:
  1576   assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
  1577   shows "fold1 min B \<le> fold1 min A"
  1578 proof cases
  1579   assume "A = B" thus ?thesis by simp
  1580 next
  1581   interpret ab_semigroup_idem_mult min
  1582     by (rule ab_semigroup_idem_mult_min)
  1583   assume neq: "A \<noteq> B"
  1584   have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
  1585   have "fold1 min B = fold1 min (A \<union> (B-A))" by(subst B)(rule refl)
  1586   also have "\<dots> = min (fold1 min A) (fold1 min (B-A))"
  1587   proof -
  1588     have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
  1589     moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`])
  1590     moreover have "(B-A) \<noteq> {}" using assms neq by blast
  1591     moreover have "A Int (B-A) = {}" using assms by blast
  1592     ultimately show ?thesis using `A \<noteq> {}` by (rule_tac fold1_Un)
  1593   qed
  1594   also have "\<dots> \<le> fold1 min A" by (simp add: min_le_iff_disj)
  1595   finally show ?thesis .
  1596 qed
  1597 
  1598 lemma Min_in [simp]:
  1599   assumes "finite A" and "A \<noteq> {}"
  1600   shows "Min A \<in> A"
  1601 proof -
  1602   interpret ab_semigroup_idem_mult min
  1603     by (rule ab_semigroup_idem_mult_min)
  1604   from assms fold1_in show ?thesis by (fastforce simp: Min_def min_def)
  1605 qed
  1606 
  1607 lemma Max_in [simp]:
  1608   assumes "finite A" and "A \<noteq> {}"
  1609   shows "Max A \<in> A"
  1610 proof -
  1611   interpret ab_semigroup_idem_mult max
  1612     by (rule ab_semigroup_idem_mult_max)
  1613   from assms fold1_in [of A] show ?thesis by (fastforce simp: Max_def max_def)
  1614 qed
  1615 
  1616 lemma Min_le [simp]:
  1617   assumes "finite A" and "x \<in> A"
  1618   shows "Min A \<le> x"
  1619   using assms by (simp add: Min_def min_max.fold1_belowI)
  1620 
  1621 lemma Max_ge [simp]:
  1622   assumes "finite A" and "x \<in> A"
  1623   shows "x \<le> Max A"
  1624   by (simp add: Max_def semilattice_inf.fold1_belowI [OF max_lattice] assms)
  1625 
  1626 lemma Min_ge_iff [simp, no_atp]:
  1627   assumes "finite A" and "A \<noteq> {}"
  1628   shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
  1629   using assms by (simp add: Min_def min_max.below_fold1_iff)
  1630 
  1631 lemma Max_le_iff [simp, no_atp]:
  1632   assumes "finite A" and "A \<noteq> {}"
  1633   shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
  1634   by (simp add: Max_def semilattice_inf.below_fold1_iff [OF max_lattice] assms)
  1635 
  1636 lemma Min_gr_iff [simp, no_atp]:
  1637   assumes "finite A" and "A \<noteq> {}"
  1638   shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
  1639   using assms by (simp add: Min_def strict_below_fold1_iff)
  1640 
  1641 lemma Max_less_iff [simp, no_atp]:
  1642   assumes "finite A" and "A \<noteq> {}"
  1643   shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
  1644   by (simp add: Max_def linorder.dual_max [OF dual_linorder]
  1645     linorder.strict_below_fold1_iff [OF dual_linorder] assms)
  1646 
  1647 lemma Min_le_iff [no_atp]:
  1648   assumes "finite A" and "A \<noteq> {}"
  1649   shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
  1650   using assms by (simp add: Min_def fold1_below_iff)
  1651 
  1652 lemma Max_ge_iff [no_atp]:
  1653   assumes "finite A" and "A \<noteq> {}"
  1654   shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
  1655   by (simp add: Max_def linorder.dual_max [OF dual_linorder]
  1656     linorder.fold1_below_iff [OF dual_linorder] assms)
  1657 
  1658 lemma Min_less_iff [no_atp]:
  1659   assumes "finite A" and "A \<noteq> {}"
  1660   shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
  1661   using assms by (simp add: Min_def fold1_strict_below_iff)
  1662 
  1663 lemma Max_gr_iff [no_atp]:
  1664   assumes "finite A" and "A \<noteq> {}"
  1665   shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
  1666   by (simp add: Max_def linorder.dual_max [OF dual_linorder]
  1667     linorder.fold1_strict_below_iff [OF dual_linorder] assms)
  1668 
  1669 lemma Min_eqI:
  1670   assumes "finite A"
  1671   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
  1672     and "x \<in> A"
  1673   shows "Min A = x"
  1674 proof (rule antisym)
  1675   from `x \<in> A` have "A \<noteq> {}" by auto
  1676   with assms show "Min A \<ge> x" by simp
  1677 next
  1678   from assms show "x \<ge> Min A" by simp
  1679 qed
  1680 
  1681 lemma Max_eqI:
  1682   assumes "finite A"
  1683   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
  1684     and "x \<in> A"
  1685   shows "Max A = x"
  1686 proof (rule antisym)
  1687   from `x \<in> A` have "A \<noteq> {}" by auto
  1688   with assms show "Max A \<le> x" by simp
  1689 next
  1690   from assms show "x \<le> Max A" by simp
  1691 qed
  1692 
  1693 lemma Min_antimono:
  1694   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
  1695   shows "Min N \<le> Min M"
  1696   using assms by (simp add: Min_def fold1_antimono)
  1697 
  1698 lemma Max_mono:
  1699   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
  1700   shows "Max M \<le> Max N"
  1701   by (simp add: Max_def linorder.dual_max [OF dual_linorder]
  1702     linorder.fold1_antimono [OF dual_linorder] assms)
  1703 
  1704 lemma finite_linorder_max_induct[consumes 1, case_names empty insert]:
  1705  assumes fin: "finite A"
  1706  and   empty: "P {}" 
  1707  and  insert: "(!!b A. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))"
  1708  shows "P A"
  1709 using fin empty insert
  1710 proof (induct rule: finite_psubset_induct)
  1711   case (psubset A)
  1712   have IH: "\<And>B. \<lbrakk>B < A; P {}; (\<And>A b. \<lbrakk>finite A; \<forall>a\<in>A. a<b; P A\<rbrakk> \<Longrightarrow> P (insert b A))\<rbrakk> \<Longrightarrow> P B" by fact 
  1713   have fin: "finite A" by fact 
  1714   have empty: "P {}" by fact
  1715   have step: "\<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)" by fact
  1716   show "P A"
  1717   proof (cases "A = {}")
  1718     assume "A = {}" 
  1719     then show "P A" using `P {}` by simp
  1720   next
  1721     let ?B = "A - {Max A}" 
  1722     let ?A = "insert (Max A) ?B"
  1723     have "finite ?B" using `finite A` by simp
  1724     assume "A \<noteq> {}"
  1725     with `finite A` have "Max A : A" by auto
  1726     then have A: "?A = A" using insert_Diff_single insert_absorb by auto
  1727     then have "P ?B" using `P {}` step IH[of ?B] by blast
  1728     moreover 
  1729     have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastforce
  1730     ultimately show "P A" using A insert_Diff_single step[OF `finite ?B`] by fastforce
  1731   qed
  1732 qed
  1733 
  1734 lemma finite_linorder_min_induct[consumes 1, case_names empty insert]:
  1735  "\<lbrakk>finite A; P {}; \<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. b < a; P A\<rbrakk> \<Longrightarrow> P (insert b A)\<rbrakk> \<Longrightarrow> P A"
  1736 by(rule linorder.finite_linorder_max_induct[OF dual_linorder])
  1737 
  1738 end
  1739 
  1740 context linordered_ab_semigroup_add
  1741 begin
  1742 
  1743 lemma add_Min_commute:
  1744   fixes k
  1745   assumes "finite N" and "N \<noteq> {}"
  1746   shows "k + Min N = Min {k + m | m. m \<in> N}"
  1747 proof -
  1748   have "\<And>x y. k + min x y = min (k + x) (k + y)"
  1749     by (simp add: min_def not_le)
  1750       (blast intro: antisym less_imp_le add_left_mono)
  1751   with assms show ?thesis
  1752     using hom_Min_commute [of "plus k" N]
  1753     by simp (blast intro: arg_cong [where f = Min])
  1754 qed
  1755 
  1756 lemma add_Max_commute:
  1757   fixes k
  1758   assumes "finite N" and "N \<noteq> {}"
  1759   shows "k + Max N = Max {k + m | m. m \<in> N}"
  1760 proof -
  1761   have "\<And>x y. k + max x y = max (k + x) (k + y)"
  1762     by (simp add: max_def not_le)
  1763       (blast intro: antisym less_imp_le add_left_mono)
  1764   with assms show ?thesis
  1765     using hom_Max_commute [of "plus k" N]
  1766     by simp (blast intro: arg_cong [where f = Max])
  1767 qed
  1768 
  1769 end
  1770 
  1771 context linordered_ab_group_add
  1772 begin
  1773 
  1774 lemma minus_Max_eq_Min [simp]:
  1775   "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Max S) = Min (uminus ` S)"
  1776   by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min)
  1777 
  1778 lemma minus_Min_eq_Max [simp]:
  1779   "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Min S) = Max (uminus ` S)"
  1780   by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max)
  1781 
  1782 end
  1783 
  1784 end