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