src/HOL/Big_Operators.thy
author wenzelm
Thu May 24 17:25:53 2012 +0200 (2012-05-24)
changeset 47988 e4b69e10b990
parent 46904 f30e941b4512
child 48819 6cf7a9d8bbaf
permissions -rw-r--r--
tuned proofs;
     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_strict_mono_ex1:
   527 fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_cancel_ab_semigroup_add}"
   528 assumes "finite A" and "ALL x:A. f x \<le> g x" and "EX a:A. f a < g a"
   529 shows "setsum f A < setsum g A"
   530 proof-
   531   from assms(3) obtain a where a: "a:A" "f a < g a" by blast
   532   have "setsum f A = setsum f ((A-{a}) \<union> {a})"
   533     by(simp add:insert_absorb[OF `a:A`])
   534   also have "\<dots> = setsum f (A-{a}) + setsum f {a}"
   535     using `finite A` by(subst setsum_Un_disjoint) auto
   536   also have "setsum f (A-{a}) \<le> setsum g (A-{a})"
   537     by(rule setsum_mono)(simp add: assms(2))
   538   also have "setsum f {a} < setsum g {a}" using a by simp
   539   also have "setsum g (A - {a}) + setsum g {a} = setsum g((A-{a}) \<union> {a})"
   540     using `finite A` by(subst setsum_Un_disjoint[symmetric]) auto
   541   also have "\<dots> = setsum g A" by(simp add:insert_absorb[OF `a:A`])
   542   finally show ?thesis by (metis add_right_mono add_strict_left_mono)
   543 qed
   544 
   545 lemma setsum_negf:
   546   "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
   547 proof (cases "finite A")
   548   case True thus ?thesis by (induct set: finite) auto
   549 next
   550   case False thus ?thesis by (simp add: setsum_def)
   551 qed
   552 
   553 lemma setsum_subtractf:
   554   "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
   555     setsum f A - setsum g A"
   556 proof (cases "finite A")
   557   case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
   558 next
   559   case False thus ?thesis by (simp add: setsum_def)
   560 qed
   561 
   562 lemma setsum_nonneg:
   563   assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
   564   shows "0 \<le> setsum f A"
   565 proof (cases "finite A")
   566   case True thus ?thesis using nn
   567   proof induct
   568     case empty then show ?case by simp
   569   next
   570     case (insert x F)
   571     then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
   572     with insert show ?case by simp
   573   qed
   574 next
   575   case False thus ?thesis by (simp add: setsum_def)
   576 qed
   577 
   578 lemma setsum_nonpos:
   579   assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{ordered_ab_semigroup_add,comm_monoid_add})"
   580   shows "setsum f A \<le> 0"
   581 proof (cases "finite A")
   582   case True thus ?thesis using np
   583   proof induct
   584     case empty then show ?case by simp
   585   next
   586     case (insert x F)
   587     then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
   588     with insert show ?case by simp
   589   qed
   590 next
   591   case False thus ?thesis by (simp add: setsum_def)
   592 qed
   593 
   594 lemma setsum_nonneg_leq_bound:
   595   fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
   596   assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s"
   597   shows "f i \<le> B"
   598 proof -
   599   have "0 \<le> (\<Sum> i \<in> s - {i}. f i)" and "0 \<le> f i"
   600     using assms by (auto intro!: setsum_nonneg)
   601   moreover
   602   have "(\<Sum> i \<in> s - {i}. f i) + f i = B"
   603     using assms by (simp add: setsum_diff1)
   604   ultimately show ?thesis by auto
   605 qed
   606 
   607 lemma setsum_nonneg_0:
   608   fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
   609   assumes "finite s" and pos: "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
   610   and "(\<Sum> i \<in> s. f i) = 0" and i: "i \<in> s"
   611   shows "f i = 0"
   612   using setsum_nonneg_leq_bound[OF assms] pos[OF i] by auto
   613 
   614 lemma setsum_mono2:
   615 fixes f :: "'a \<Rightarrow> 'b :: ordered_comm_monoid_add"
   616 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
   617 shows "setsum f A \<le> setsum f B"
   618 proof -
   619   have "setsum f A \<le> setsum f A + setsum f (B-A)"
   620     by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
   621   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
   622     by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
   623   also have "A \<union> (B-A) = B" using sub by blast
   624   finally show ?thesis .
   625 qed
   626 
   627 lemma setsum_mono3: "finite B ==> A <= B ==> 
   628     ALL x: B - A. 
   629       0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==>
   630         setsum f A <= setsum f B"
   631   apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
   632   apply (erule ssubst)
   633   apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
   634   apply simp
   635   apply (rule add_left_mono)
   636   apply (erule setsum_nonneg)
   637   apply (subst setsum_Un_disjoint [THEN sym])
   638   apply (erule finite_subset, assumption)
   639   apply (rule finite_subset)
   640   prefer 2
   641   apply assumption
   642   apply (auto simp add: sup_absorb2)
   643 done
   644 
   645 lemma setsum_right_distrib: 
   646   fixes f :: "'a => ('b::semiring_0)"
   647   shows "r * setsum f A = setsum (%n. r * f n) A"
   648 proof (cases "finite A")
   649   case True
   650   thus ?thesis
   651   proof induct
   652     case empty thus ?case by simp
   653   next
   654     case (insert x A) thus ?case by (simp add: right_distrib)
   655   qed
   656 next
   657   case False thus ?thesis by (simp add: setsum_def)
   658 qed
   659 
   660 lemma setsum_left_distrib:
   661   "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
   662 proof (cases "finite A")
   663   case True
   664   then show ?thesis
   665   proof induct
   666     case empty thus ?case by simp
   667   next
   668     case (insert x A) thus ?case by (simp add: left_distrib)
   669   qed
   670 next
   671   case False thus ?thesis by (simp add: setsum_def)
   672 qed
   673 
   674 lemma setsum_divide_distrib:
   675   "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
   676 proof (cases "finite A")
   677   case True
   678   then show ?thesis
   679   proof induct
   680     case empty thus ?case by simp
   681   next
   682     case (insert x A) thus ?case by (simp add: add_divide_distrib)
   683   qed
   684 next
   685   case False thus ?thesis by (simp add: setsum_def)
   686 qed
   687 
   688 lemma setsum_abs[iff]: 
   689   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   690   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
   691 proof (cases "finite A")
   692   case True
   693   thus ?thesis
   694   proof induct
   695     case empty thus ?case by simp
   696   next
   697     case (insert x A)
   698     thus ?case by (auto intro: abs_triangle_ineq order_trans)
   699   qed
   700 next
   701   case False thus ?thesis by (simp add: setsum_def)
   702 qed
   703 
   704 lemma setsum_abs_ge_zero[iff]: 
   705   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   706   shows "0 \<le> setsum (%i. abs(f i)) A"
   707 proof (cases "finite A")
   708   case True
   709   thus ?thesis
   710   proof induct
   711     case empty thus ?case by simp
   712   next
   713     case (insert x A) thus ?case by auto
   714   qed
   715 next
   716   case False thus ?thesis by (simp add: setsum_def)
   717 qed
   718 
   719 lemma abs_setsum_abs[simp]: 
   720   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   721   shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
   722 proof (cases "finite A")
   723   case True
   724   thus ?thesis
   725   proof induct
   726     case empty thus ?case by simp
   727   next
   728     case (insert a A)
   729     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
   730     also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
   731     also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
   732       by (simp del: abs_of_nonneg)
   733     also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
   734     finally show ?case .
   735   qed
   736 next
   737   case False thus ?thesis by (simp add: setsum_def)
   738 qed
   739 
   740 lemma setsum_Plus:
   741   fixes A :: "'a set" and B :: "'b set"
   742   assumes fin: "finite A" "finite B"
   743   shows "setsum f (A <+> B) = setsum (f \<circ> Inl) A + setsum (f \<circ> Inr) B"
   744 proof -
   745   have "A <+> B = Inl ` A \<union> Inr ` B" by auto
   746   moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)"
   747     by auto
   748   moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto
   749   moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI)
   750   ultimately show ?thesis using fin by(simp add: setsum_Un_disjoint setsum_reindex)
   751 qed
   752 
   753 
   754 text {* Commuting outer and inner summation *}
   755 
   756 lemma setsum_commute:
   757   "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
   758 proof (simp add: setsum_cartesian_product)
   759   have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
   760     (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
   761     (is "?s = _")
   762     apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on)
   763     apply (simp add: split_def)
   764     done
   765   also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
   766     (is "_ = ?t")
   767     apply (simp add: swap_product)
   768     done
   769   finally show "?s = ?t" .
   770 qed
   771 
   772 lemma setsum_product:
   773   fixes f :: "'a => ('b::semiring_0)"
   774   shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
   775   by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
   776 
   777 lemma setsum_mult_setsum_if_inj:
   778 fixes f :: "'a => ('b::semiring_0)"
   779 shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==>
   780   setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}"
   781 by(auto simp: setsum_product setsum_cartesian_product
   782         intro!:  setsum_reindex_cong[symmetric])
   783 
   784 lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
   785 apply (cases "finite A")
   786 apply (erule finite_induct)
   787 apply (auto simp add: algebra_simps)
   788 done
   789 
   790 lemma setsum_bounded:
   791   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
   792   shows "setsum f A \<le> of_nat(card A) * K"
   793 proof (cases "finite A")
   794   case True
   795   thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
   796 next
   797   case False thus ?thesis by (simp add: setsum_def)
   798 qed
   799 
   800 
   801 subsubsection {* Cardinality as special case of @{const setsum} *}
   802 
   803 lemma card_eq_setsum:
   804   "card A = setsum (\<lambda>x. 1) A"
   805   by (simp only: card_def setsum_def)
   806 
   807 lemma card_UN_disjoint:
   808   assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
   809     and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
   810   shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
   811 proof -
   812   have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)" by simp
   813   with assms show ?thesis by (simp add: card_eq_setsum setsum_UN_disjoint del: setsum_constant)
   814 qed
   815 
   816 lemma card_Union_disjoint:
   817   "finite C ==> (ALL A:C. finite A) ==>
   818    (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
   819    ==> card (Union C) = setsum card C"
   820 apply (frule card_UN_disjoint [of C id])
   821 apply (simp_all add: SUP_def id_def)
   822 done
   823 
   824 text{*The image of a finite set can be expressed using @{term fold_image}.*}
   825 lemma image_eq_fold_image:
   826   "finite A ==> f ` A = fold_image (op Un) (%x. {f x}) {} A"
   827 proof (induct rule: finite_induct)
   828   case empty then show ?case by simp
   829 next
   830   interpret ab_semigroup_mult "op Un"
   831     proof qed auto
   832   case insert 
   833   then show ?case by simp
   834 qed
   835 
   836 subsubsection {* Cardinality of products *}
   837 
   838 lemma card_SigmaI [simp]:
   839   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
   840   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
   841 by(simp add: card_eq_setsum setsum_Sigma del:setsum_constant)
   842 
   843 (*
   844 lemma SigmaI_insert: "y \<notin> A ==>
   845   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
   846   by auto
   847 *)
   848 
   849 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
   850   by (cases "finite A \<and> finite B")
   851     (auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2)
   852 
   853 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
   854 by (simp add: card_cartesian_product)
   855 
   856 
   857 subsection {* Generalized product over a set *}
   858 
   859 definition (in comm_monoid_mult) setprod :: "('b \<Rightarrow> 'a) => 'b set => 'a" where
   860   "setprod f A = (if finite A then fold_image (op *) f 1 A else 1)"
   861 
   862 sublocale comm_monoid_mult < setprod!: comm_monoid_big "op *" 1 setprod proof
   863 qed (fact setprod_def)
   864 
   865 abbreviation
   866   Setprod  ("\<Prod>_" [1000] 999) where
   867   "\<Prod>A == setprod (%x. x) A"
   868 
   869 syntax
   870   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
   871 syntax (xsymbols)
   872   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
   873 syntax (HTML output)
   874   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
   875 
   876 translations -- {* Beware of argument permutation! *}
   877   "PROD i:A. b" == "CONST setprod (%i. b) A" 
   878   "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A" 
   879 
   880 text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
   881  @{text"\<Prod>x|P. e"}. *}
   882 
   883 syntax
   884   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
   885 syntax (xsymbols)
   886   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
   887 syntax (HTML output)
   888   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
   889 
   890 translations
   891   "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
   892   "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
   893 
   894 lemma setprod_empty: "setprod f {} = 1"
   895   by (fact setprod.empty)
   896 
   897 lemma setprod_insert: "[| finite A; a \<notin> A |] ==>
   898     setprod f (insert a A) = f a * setprod f A"
   899   by (fact setprod.insert)
   900 
   901 lemma setprod_infinite: "~ finite A ==> setprod f A = 1"
   902   by (fact setprod.infinite)
   903 
   904 lemma setprod_reindex:
   905    "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
   906 by(auto simp: setprod_def fold_image_reindex dest!:finite_imageD)
   907 
   908 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
   909 by (auto simp add: setprod_reindex)
   910 
   911 lemma setprod_cong:
   912   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
   913 by(fastforce simp: setprod_def intro: fold_image_cong)
   914 
   915 lemma strong_setprod_cong[cong]:
   916   "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
   917 by(fastforce simp: simp_implies_def setprod_def intro: fold_image_cong)
   918 
   919 lemma setprod_reindex_cong: "inj_on f A ==>
   920     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
   921 by (frule setprod_reindex, simp)
   922 
   923 lemma strong_setprod_reindex_cong: assumes i: "inj_on f A"
   924   and B: "B = f ` A" and eq: "\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x"
   925   shows "setprod h B = setprod g A"
   926 proof-
   927     have "setprod h B = setprod (h o f) A"
   928       by (simp add: B setprod_reindex[OF i, of h])
   929     then show ?thesis apply simp
   930       apply (rule setprod_cong)
   931       apply simp
   932       by (simp add: eq)
   933 qed
   934 
   935 lemma setprod_Un_one:  
   936   assumes fS: "finite S" and fT: "finite T"
   937   and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
   938   shows "setprod f (S \<union> T) = setprod f S  * setprod f T"
   939   using fS fT
   940   apply (simp add: setprod_def)
   941   apply (rule fold_image_Un_one)
   942   using I0 by auto
   943 
   944 
   945 lemma setprod_1: "setprod (%i. 1) A = 1"
   946 apply (case_tac "finite A")
   947 apply (erule finite_induct, auto simp add: mult_ac)
   948 done
   949 
   950 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
   951 apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
   952 apply (erule ssubst, rule setprod_1)
   953 apply (rule setprod_cong, auto)
   954 done
   955 
   956 lemma setprod_Un_Int: "finite A ==> finite B
   957     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
   958 by(simp add: setprod_def fold_image_Un_Int[symmetric])
   959 
   960 lemma setprod_Un_disjoint: "finite A ==> finite B
   961   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
   962 by (subst setprod_Un_Int [symmetric], auto)
   963 
   964 lemma setprod_mono_one_left: 
   965   assumes fT: "finite T" and ST: "S \<subseteq> T"
   966   and z: "\<forall>i \<in> T - S. f i = 1"
   967   shows "setprod f S = setprod f T"
   968 proof-
   969   have eq: "T = S \<union> (T - S)" using ST by blast
   970   have d: "S \<inter> (T - S) = {}" using ST by blast
   971   from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
   972   show ?thesis
   973   by (simp add: setprod_Un_disjoint[OF f d, unfolded eq[symmetric]] setprod_1'[OF z])
   974 qed
   975 
   976 lemmas setprod_mono_one_right = setprod_mono_one_left [THEN sym]
   977 
   978 lemma setprod_delta: 
   979   assumes fS: "finite S"
   980   shows "setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
   981 proof-
   982   let ?f = "(\<lambda>k. if k=a then b k else 1)"
   983   {assume a: "a \<notin> S"
   984     hence "\<forall> k\<in> S. ?f k = 1" by simp
   985     hence ?thesis  using a by (simp add: setprod_1) }
   986   moreover 
   987   {assume a: "a \<in> S"
   988     let ?A = "S - {a}"
   989     let ?B = "{a}"
   990     have eq: "S = ?A \<union> ?B" using a by blast 
   991     have dj: "?A \<inter> ?B = {}" by simp
   992     from fS have fAB: "finite ?A" "finite ?B" by auto  
   993     have fA1: "setprod ?f ?A = 1" apply (rule setprod_1') by auto
   994     have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
   995       using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
   996       by simp
   997     then have ?thesis using a by (simp add: fA1 cong: setprod_cong cong del: if_weak_cong)}
   998   ultimately show ?thesis by blast
   999 qed
  1000 
  1001 lemma setprod_delta': 
  1002   assumes fS: "finite S" shows 
  1003   "setprod (\<lambda>k. if a = k then b k else 1) S = 
  1004      (if a\<in> S then b a else 1)"
  1005   using setprod_delta[OF fS, of a b, symmetric] 
  1006   by (auto intro: setprod_cong)
  1007 
  1008 
  1009 lemma setprod_UN_disjoint:
  1010     "finite I ==> (ALL i:I. finite (A i)) ==>
  1011         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1012       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
  1013   by (simp add: setprod_def fold_image_UN_disjoint)
  1014 
  1015 lemma setprod_Union_disjoint:
  1016   assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}" 
  1017   shows "setprod f (Union C) = setprod (setprod f) C"
  1018 proof cases
  1019   assume "finite C"
  1020   from setprod_UN_disjoint[OF this assms]
  1021   show ?thesis
  1022     by (simp add: SUP_def)
  1023 qed (force dest: finite_UnionD simp add: setprod_def)
  1024 
  1025 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  1026     (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
  1027     (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
  1028 by(simp add:setprod_def fold_image_Sigma split_def)
  1029 
  1030 text{*Here we can eliminate the finiteness assumptions, by cases.*}
  1031 lemma setprod_cartesian_product: 
  1032      "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
  1033 apply (cases "finite A") 
  1034  apply (cases "finite B") 
  1035   apply (simp add: setprod_Sigma)
  1036  apply (cases "A={}", simp)
  1037  apply (simp add: setprod_1) 
  1038 apply (auto simp add: setprod_def
  1039             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
  1040 done
  1041 
  1042 lemma setprod_timesf:
  1043      "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
  1044 by(simp add:setprod_def fold_image_distrib)
  1045 
  1046 
  1047 subsubsection {* Properties in more restricted classes of structures *}
  1048 
  1049 lemma setprod_eq_1_iff [simp]:
  1050   "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
  1051 by (induct set: finite) auto
  1052 
  1053 lemma setprod_zero:
  1054      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
  1055 apply (induct set: finite, force, clarsimp)
  1056 apply (erule disjE, auto)
  1057 done
  1058 
  1059 lemma setprod_nonneg [rule_format]:
  1060    "(ALL x: A. (0::'a::linordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
  1061 by (cases "finite A", induct set: finite, simp_all add: mult_nonneg_nonneg)
  1062 
  1063 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x)
  1064   --> 0 < setprod f A"
  1065 by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos)
  1066 
  1067 lemma setprod_zero_iff[simp]: "finite A ==> 
  1068   (setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) =
  1069   (EX x: A. f x = 0)"
  1070 by (erule finite_induct, auto simp:no_zero_divisors)
  1071 
  1072 lemma setprod_pos_nat:
  1073   "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
  1074 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
  1075 
  1076 lemma setprod_pos_nat_iff[simp]:
  1077   "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
  1078 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
  1079 
  1080 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
  1081   (setprod f (A Un B) :: 'a ::{field})
  1082    = setprod f A * setprod f B / setprod f (A Int B)"
  1083 by (subst setprod_Un_Int [symmetric], auto)
  1084 
  1085 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
  1086   (setprod f (A - {a}) :: 'a :: {field}) =
  1087   (if a:A then setprod f A / f a else setprod f A)"
  1088   by (erule finite_induct) (auto simp add: insert_Diff_if)
  1089 
  1090 lemma setprod_inversef: 
  1091   fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
  1092   shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)"
  1093 by (erule finite_induct) auto
  1094 
  1095 lemma setprod_dividef:
  1096   fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
  1097   shows "finite A
  1098     ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
  1099 apply (subgoal_tac
  1100          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
  1101 apply (erule ssubst)
  1102 apply (subst divide_inverse)
  1103 apply (subst setprod_timesf)
  1104 apply (subst setprod_inversef, assumption+, rule refl)
  1105 apply (rule setprod_cong, rule refl)
  1106 apply (subst divide_inverse, auto)
  1107 done
  1108 
  1109 lemma setprod_dvd_setprod [rule_format]: 
  1110     "(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A"
  1111   apply (cases "finite A")
  1112   apply (induct set: finite)
  1113   apply (auto simp add: dvd_def)
  1114   apply (rule_tac x = "k * ka" in exI)
  1115   apply (simp add: algebra_simps)
  1116 done
  1117 
  1118 lemma setprod_dvd_setprod_subset:
  1119   "finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B"
  1120   apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)")
  1121   apply (unfold dvd_def, blast)
  1122   apply (subst setprod_Un_disjoint [symmetric])
  1123   apply (auto elim: finite_subset intro: setprod_cong)
  1124 done
  1125 
  1126 lemma setprod_dvd_setprod_subset2:
  1127   "finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow> 
  1128       setprod f A dvd setprod g B"
  1129   apply (rule dvd_trans)
  1130   apply (rule setprod_dvd_setprod, erule (1) bspec)
  1131   apply (erule (1) setprod_dvd_setprod_subset)
  1132 done
  1133 
  1134 lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow> 
  1135     (f i ::'a::comm_semiring_1) dvd setprod f A"
  1136 by (induct set: finite) (auto intro: dvd_mult)
  1137 
  1138 lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow> 
  1139     (d::'a::comm_semiring_1) dvd (SUM x : A. f x)"
  1140   apply (cases "finite A")
  1141   apply (induct set: finite)
  1142   apply auto
  1143 done
  1144 
  1145 lemma setprod_mono:
  1146   fixes f :: "'a \<Rightarrow> 'b\<Colon>linordered_semidom"
  1147   assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i"
  1148   shows "setprod f A \<le> setprod g A"
  1149 proof (cases "finite A")
  1150   case True
  1151   hence ?thesis "setprod f A \<ge> 0" using subset_refl[of A]
  1152   proof (induct A rule: finite_subset_induct)
  1153     case (insert a F)
  1154     thus "setprod f (insert a F) \<le> setprod g (insert a F)" "0 \<le> setprod f (insert a F)"
  1155       unfolding setprod_insert[OF insert(1,3)]
  1156       using assms[rule_format,OF insert(2)] insert
  1157       by (auto intro: mult_mono mult_nonneg_nonneg)
  1158   qed auto
  1159   thus ?thesis by simp
  1160 qed auto
  1161 
  1162 lemma abs_setprod:
  1163   fixes f :: "'a \<Rightarrow> 'b\<Colon>{linordered_field,abs}"
  1164   shows "abs (setprod f A) = setprod (\<lambda>x. abs (f x)) A"
  1165 proof (cases "finite A")
  1166   case True thus ?thesis
  1167     by induct (auto simp add: field_simps abs_mult)
  1168 qed auto
  1169 
  1170 lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
  1171 apply (erule finite_induct)
  1172 apply auto
  1173 done
  1174 
  1175 lemma setprod_gen_delta:
  1176   assumes fS: "finite S"
  1177   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)"
  1178 proof-
  1179   let ?f = "(\<lambda>k. if k=a then b k else c)"
  1180   {assume a: "a \<notin> S"
  1181     hence "\<forall> k\<in> S. ?f k = c" by simp
  1182     hence ?thesis  using a setprod_constant[OF fS, of c] by (simp add: setprod_1 cong add: setprod_cong) }
  1183   moreover 
  1184   {assume a: "a \<in> S"
  1185     let ?A = "S - {a}"
  1186     let ?B = "{a}"
  1187     have eq: "S = ?A \<union> ?B" using a by blast 
  1188     have dj: "?A \<inter> ?B = {}" by simp
  1189     from fS have fAB: "finite ?A" "finite ?B" by auto  
  1190     have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
  1191       apply (rule setprod_cong) by auto
  1192     have cA: "card ?A = card S - 1" using fS a by auto
  1193     have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
  1194     have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
  1195       using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
  1196       by simp
  1197     then have ?thesis using a cA
  1198       by (simp add: fA1 field_simps cong add: setprod_cong cong del: if_weak_cong)}
  1199   ultimately show ?thesis by blast
  1200 qed
  1201 
  1202 
  1203 subsection {* Versions of @{const inf} and @{const sup} on non-empty sets *}
  1204 
  1205 no_notation times (infixl "*" 70)
  1206 no_notation Groups.one ("1")
  1207 
  1208 locale semilattice_big = semilattice +
  1209   fixes F :: "'a set \<Rightarrow> 'a"
  1210   assumes F_eq: "finite A \<Longrightarrow> F A = fold1 (op *) A"
  1211 
  1212 sublocale semilattice_big < folding_one_idem proof
  1213 qed (simp_all add: F_eq)
  1214 
  1215 notation times (infixl "*" 70)
  1216 notation Groups.one ("1")
  1217 
  1218 context lattice
  1219 begin
  1220 
  1221 definition Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900) where
  1222   "Inf_fin = fold1 inf"
  1223 
  1224 definition Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900) where
  1225   "Sup_fin = fold1 sup"
  1226 
  1227 end
  1228 
  1229 sublocale lattice < Inf_fin!: semilattice_big inf Inf_fin proof
  1230 qed (simp add: Inf_fin_def)
  1231 
  1232 sublocale lattice < Sup_fin!: semilattice_big sup Sup_fin proof
  1233 qed (simp add: Sup_fin_def)
  1234 
  1235 context semilattice_inf
  1236 begin
  1237 
  1238 lemma ab_semigroup_idem_mult_inf:
  1239   "class.ab_semigroup_idem_mult inf"
  1240 proof qed (rule inf_assoc inf_commute inf_idem)+
  1241 
  1242 lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> Finite_Set.fold inf b (insert a A) = inf a (Finite_Set.fold inf b A)"
  1243 by(rule comp_fun_idem.fold_insert_idem[OF ab_semigroup_idem_mult.comp_fun_idem[OF ab_semigroup_idem_mult_inf]])
  1244 
  1245 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"
  1246 by (induct pred: finite) (auto intro: le_infI1)
  1247 
  1248 lemma fold_inf_le_inf: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> Finite_Set.fold inf b A \<le> inf a b"
  1249 proof(induct arbitrary: a pred:finite)
  1250   case empty thus ?case by simp
  1251 next
  1252   case (insert x A)
  1253   show ?case
  1254   proof cases
  1255     assume "A = {}" thus ?thesis using insert by simp
  1256   next
  1257     assume "A \<noteq> {}" thus ?thesis using insert by (auto intro: le_infI2)
  1258   qed
  1259 qed
  1260 
  1261 lemma below_fold1_iff:
  1262   assumes "finite A" "A \<noteq> {}"
  1263   shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
  1264 proof -
  1265   interpret ab_semigroup_idem_mult inf
  1266     by (rule ab_semigroup_idem_mult_inf)
  1267   show ?thesis using assms by (induct rule: finite_ne_induct) simp_all
  1268 qed
  1269 
  1270 lemma fold1_belowI:
  1271   assumes "finite A"
  1272     and "a \<in> A"
  1273   shows "fold1 inf A \<le> a"
  1274 proof -
  1275   from assms have "A \<noteq> {}" by auto
  1276   from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
  1277   proof (induct rule: finite_ne_induct)
  1278     case singleton thus ?case by simp
  1279   next
  1280     interpret ab_semigroup_idem_mult inf
  1281       by (rule ab_semigroup_idem_mult_inf)
  1282     case (insert x F)
  1283     from insert(5) have "a = x \<or> a \<in> F" by simp
  1284     thus ?case
  1285     proof
  1286       assume "a = x" thus ?thesis using insert
  1287         by (simp add: mult_ac)
  1288     next
  1289       assume "a \<in> F"
  1290       hence bel: "fold1 inf F \<le> a" by (rule insert)
  1291       have "inf (fold1 inf (insert x F)) a = inf x (inf (fold1 inf F) a)"
  1292         using insert by (simp add: mult_ac)
  1293       also have "inf (fold1 inf F) a = fold1 inf F"
  1294         using bel by (auto intro: antisym)
  1295       also have "inf x \<dots> = fold1 inf (insert x F)"
  1296         using insert by (simp add: mult_ac)
  1297       finally have aux: "inf (fold1 inf (insert x F)) a = fold1 inf (insert x F)" .
  1298       moreover have "inf (fold1 inf (insert x F)) a \<le> a" by simp
  1299       ultimately show ?thesis by simp
  1300     qed
  1301   qed
  1302 qed
  1303 
  1304 end
  1305 
  1306 context semilattice_sup
  1307 begin
  1308 
  1309 lemma ab_semigroup_idem_mult_sup: "class.ab_semigroup_idem_mult sup"
  1310 by (rule semilattice_inf.ab_semigroup_idem_mult_inf)(rule dual_semilattice)
  1311 
  1312 lemma fold_sup_insert[simp]: "finite A \<Longrightarrow> Finite_Set.fold sup b (insert a A) = sup a (Finite_Set.fold sup b A)"
  1313 by(rule semilattice_inf.fold_inf_insert)(rule dual_semilattice)
  1314 
  1315 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"
  1316 by(rule semilattice_inf.inf_le_fold_inf)(rule dual_semilattice)
  1317 
  1318 lemma sup_le_fold_sup: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a b \<le> Finite_Set.fold sup b A"
  1319 by(rule semilattice_inf.fold_inf_le_inf)(rule dual_semilattice)
  1320 
  1321 end
  1322 
  1323 context lattice
  1324 begin
  1325 
  1326 lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A"
  1327 apply(unfold Sup_fin_def Inf_fin_def)
  1328 apply(subgoal_tac "EX a. a:A")
  1329 prefer 2 apply blast
  1330 apply(erule exE)
  1331 apply(rule order_trans)
  1332 apply(erule (1) fold1_belowI)
  1333 apply(erule (1) semilattice_inf.fold1_belowI [OF dual_semilattice])
  1334 done
  1335 
  1336 lemma sup_Inf_absorb [simp]:
  1337   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^bsub>fin\<^esub>A) = a"
  1338 apply(subst sup_commute)
  1339 apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI)
  1340 done
  1341 
  1342 lemma inf_Sup_absorb [simp]:
  1343   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a"
  1344 by (simp add: Sup_fin_def inf_absorb1
  1345   semilattice_inf.fold1_belowI [OF dual_semilattice])
  1346 
  1347 end
  1348 
  1349 context distrib_lattice
  1350 begin
  1351 
  1352 lemma sup_Inf1_distrib:
  1353   assumes "finite A"
  1354     and "A \<noteq> {}"
  1355   shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
  1356 proof -
  1357   interpret ab_semigroup_idem_mult inf
  1358     by (rule ab_semigroup_idem_mult_inf)
  1359   from assms show ?thesis
  1360     by (simp add: Inf_fin_def image_def
  1361       hom_fold1_commute [where h="sup x", OF sup_inf_distrib1])
  1362         (rule arg_cong [where f="fold1 inf"], blast)
  1363 qed
  1364 
  1365 lemma sup_Inf2_distrib:
  1366   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  1367   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}"
  1368 using A proof (induct rule: finite_ne_induct)
  1369   case singleton thus ?case
  1370     by (simp add: sup_Inf1_distrib [OF B])
  1371 next
  1372   interpret ab_semigroup_idem_mult inf
  1373     by (rule ab_semigroup_idem_mult_inf)
  1374   case (insert x A)
  1375   have finB: "finite {sup x b |b. b \<in> B}"
  1376     by(rule finite_surj[where f = "sup x", OF B(1)], auto)
  1377   have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
  1378   proof -
  1379     have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
  1380       by blast
  1381     thus ?thesis by(simp add: insert(1) B(1))
  1382   qed
  1383   have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  1384   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)"
  1385     using insert by simp
  1386   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)
  1387   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})"
  1388     using insert by(simp add:sup_Inf1_distrib[OF B])
  1389   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})"
  1390     (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M")
  1391     using B insert
  1392     by (simp add: Inf_fin_def fold1_Un2 [OF finB _ finAB ne])
  1393   also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
  1394     by blast
  1395   finally show ?case .
  1396 qed
  1397 
  1398 lemma inf_Sup1_distrib:
  1399   assumes "finite A" and "A \<noteq> {}"
  1400   shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
  1401 proof -
  1402   interpret ab_semigroup_idem_mult sup
  1403     by (rule ab_semigroup_idem_mult_sup)
  1404   from assms show ?thesis
  1405     by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1])
  1406       (rule arg_cong [where f="fold1 sup"], blast)
  1407 qed
  1408 
  1409 lemma inf_Sup2_distrib:
  1410   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  1411   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}"
  1412 using A proof (induct rule: finite_ne_induct)
  1413   case singleton thus ?case
  1414     by(simp add: inf_Sup1_distrib [OF B])
  1415 next
  1416   case (insert x A)
  1417   have finB: "finite {inf x b |b. b \<in> B}"
  1418     by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
  1419   have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
  1420   proof -
  1421     have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
  1422       by blast
  1423     thus ?thesis by(simp add: insert(1) B(1))
  1424   qed
  1425   have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  1426   interpret ab_semigroup_idem_mult sup
  1427     by (rule ab_semigroup_idem_mult_sup)
  1428   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)"
  1429     using insert by simp
  1430   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)
  1431   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})"
  1432     using insert by(simp add:inf_Sup1_distrib[OF B])
  1433   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})"
  1434     (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M")
  1435     using B insert
  1436     by (simp add: Sup_fin_def fold1_Un2 [OF finB _ finAB ne])
  1437   also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
  1438     by blast
  1439   finally show ?case .
  1440 qed
  1441 
  1442 end
  1443 
  1444 context complete_lattice
  1445 begin
  1446 
  1447 lemma Inf_fin_Inf:
  1448   assumes "finite A" and "A \<noteq> {}"
  1449   shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
  1450 proof -
  1451   interpret ab_semigroup_idem_mult inf
  1452     by (rule ab_semigroup_idem_mult_inf)
  1453   from `A \<noteq> {}` obtain b B where "A = {b} \<union> B" by auto
  1454   moreover with `finite A` have "finite B" by simp
  1455   ultimately show ?thesis
  1456     by (simp add: Inf_fin_def fold1_eq_fold_idem inf_Inf_fold_inf [symmetric])
  1457 qed
  1458 
  1459 lemma Sup_fin_Sup:
  1460   assumes "finite A" and "A \<noteq> {}"
  1461   shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
  1462 proof -
  1463   interpret ab_semigroup_idem_mult sup
  1464     by (rule ab_semigroup_idem_mult_sup)
  1465   from `A \<noteq> {}` obtain b B where "A = {b} \<union> B" by auto
  1466   moreover with `finite A` have "finite B" by simp
  1467   ultimately show ?thesis  
  1468   by (simp add: Sup_fin_def fold1_eq_fold_idem sup_Sup_fold_sup [symmetric])
  1469 qed
  1470 
  1471 end
  1472 
  1473 
  1474 subsection {* Versions of @{const min} and @{const max} on non-empty sets *}
  1475 
  1476 definition (in linorder) Min :: "'a set \<Rightarrow> 'a" where
  1477   "Min = fold1 min"
  1478 
  1479 definition (in linorder) Max :: "'a set \<Rightarrow> 'a" where
  1480   "Max = fold1 max"
  1481 
  1482 sublocale linorder < Min!: semilattice_big min Min proof
  1483 qed (simp add: Min_def)
  1484 
  1485 sublocale linorder < Max!: semilattice_big max Max proof
  1486 qed (simp add: Max_def)
  1487 
  1488 context linorder
  1489 begin
  1490 
  1491 lemmas Min_singleton = Min.singleton
  1492 lemmas Max_singleton = Max.singleton
  1493 
  1494 lemma Min_insert:
  1495   assumes "finite A" and "A \<noteq> {}"
  1496   shows "Min (insert x A) = min x (Min A)"
  1497   using assms by simp
  1498 
  1499 lemma Max_insert:
  1500   assumes "finite A" and "A \<noteq> {}"
  1501   shows "Max (insert x A) = max x (Max A)"
  1502   using assms by simp
  1503 
  1504 lemma Min_Un:
  1505   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
  1506   shows "Min (A \<union> B) = min (Min A) (Min B)"
  1507   using assms by (rule Min.union_idem)
  1508 
  1509 lemma Max_Un:
  1510   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
  1511   shows "Max (A \<union> B) = max (Max A) (Max B)"
  1512   using assms by (rule Max.union_idem)
  1513 
  1514 lemma hom_Min_commute:
  1515   assumes "\<And>x y. h (min x y) = min (h x) (h y)"
  1516     and "finite N" and "N \<noteq> {}"
  1517   shows "h (Min N) = Min (h ` N)"
  1518   using assms by (rule Min.hom_commute)
  1519 
  1520 lemma hom_Max_commute:
  1521   assumes "\<And>x y. h (max x y) = max (h x) (h y)"
  1522     and "finite N" and "N \<noteq> {}"
  1523   shows "h (Max N) = Max (h ` N)"
  1524   using assms by (rule Max.hom_commute)
  1525 
  1526 lemma ab_semigroup_idem_mult_min:
  1527   "class.ab_semigroup_idem_mult min"
  1528   proof qed (auto simp add: min_def)
  1529 
  1530 lemma ab_semigroup_idem_mult_max:
  1531   "class.ab_semigroup_idem_mult max"
  1532   proof qed (auto simp add: max_def)
  1533 
  1534 lemma max_lattice:
  1535   "class.semilattice_inf max (op \<ge>) (op >)"
  1536   by (fact min_max.dual_semilattice)
  1537 
  1538 lemma dual_max:
  1539   "ord.max (op \<ge>) = min"
  1540   by (auto simp add: ord.max_def min_def fun_eq_iff)
  1541 
  1542 lemma dual_min:
  1543   "ord.min (op \<ge>) = max"
  1544   by (auto simp add: ord.min_def max_def fun_eq_iff)
  1545 
  1546 lemma strict_below_fold1_iff:
  1547   assumes "finite A" and "A \<noteq> {}"
  1548   shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
  1549 proof -
  1550   interpret ab_semigroup_idem_mult min
  1551     by (rule ab_semigroup_idem_mult_min)
  1552   from assms show ?thesis
  1553   by (induct rule: finite_ne_induct)
  1554     (simp_all add: fold1_insert)
  1555 qed
  1556 
  1557 lemma fold1_below_iff:
  1558   assumes "finite A" and "A \<noteq> {}"
  1559   shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
  1560 proof -
  1561   interpret ab_semigroup_idem_mult min
  1562     by (rule ab_semigroup_idem_mult_min)
  1563   from assms show ?thesis
  1564   by (induct rule: finite_ne_induct)
  1565     (simp_all add: fold1_insert min_le_iff_disj)
  1566 qed
  1567 
  1568 lemma fold1_strict_below_iff:
  1569   assumes "finite A" and "A \<noteq> {}"
  1570   shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
  1571 proof -
  1572   interpret ab_semigroup_idem_mult min
  1573     by (rule ab_semigroup_idem_mult_min)
  1574   from assms show ?thesis
  1575   by (induct rule: finite_ne_induct)
  1576     (simp_all add: fold1_insert min_less_iff_disj)
  1577 qed
  1578 
  1579 lemma fold1_antimono:
  1580   assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
  1581   shows "fold1 min B \<le> fold1 min A"
  1582 proof cases
  1583   assume "A = B" thus ?thesis by simp
  1584 next
  1585   interpret ab_semigroup_idem_mult min
  1586     by (rule ab_semigroup_idem_mult_min)
  1587   assume neq: "A \<noteq> B"
  1588   have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
  1589   have "fold1 min B = fold1 min (A \<union> (B-A))" by(subst B)(rule refl)
  1590   also have "\<dots> = min (fold1 min A) (fold1 min (B-A))"
  1591   proof -
  1592     have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
  1593     moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`])
  1594     moreover have "(B-A) \<noteq> {}" using assms neq by blast
  1595     moreover have "A Int (B-A) = {}" using assms by blast
  1596     ultimately show ?thesis using `A \<noteq> {}` by (rule_tac fold1_Un)
  1597   qed
  1598   also have "\<dots> \<le> fold1 min A" by (simp add: min_le_iff_disj)
  1599   finally show ?thesis .
  1600 qed
  1601 
  1602 lemma Min_in [simp]:
  1603   assumes "finite A" and "A \<noteq> {}"
  1604   shows "Min A \<in> A"
  1605 proof -
  1606   interpret ab_semigroup_idem_mult min
  1607     by (rule ab_semigroup_idem_mult_min)
  1608   from assms fold1_in show ?thesis by (fastforce simp: Min_def min_def)
  1609 qed
  1610 
  1611 lemma Max_in [simp]:
  1612   assumes "finite A" and "A \<noteq> {}"
  1613   shows "Max A \<in> A"
  1614 proof -
  1615   interpret ab_semigroup_idem_mult max
  1616     by (rule ab_semigroup_idem_mult_max)
  1617   from assms fold1_in [of A] show ?thesis by (fastforce simp: Max_def max_def)
  1618 qed
  1619 
  1620 lemma Min_le [simp]:
  1621   assumes "finite A" and "x \<in> A"
  1622   shows "Min A \<le> x"
  1623   using assms by (simp add: Min_def min_max.fold1_belowI)
  1624 
  1625 lemma Max_ge [simp]:
  1626   assumes "finite A" and "x \<in> A"
  1627   shows "x \<le> Max A"
  1628   by (simp add: Max_def semilattice_inf.fold1_belowI [OF max_lattice] assms)
  1629 
  1630 lemma Min_ge_iff [simp, no_atp]:
  1631   assumes "finite A" and "A \<noteq> {}"
  1632   shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
  1633   using assms by (simp add: Min_def min_max.below_fold1_iff)
  1634 
  1635 lemma Max_le_iff [simp, no_atp]:
  1636   assumes "finite A" and "A \<noteq> {}"
  1637   shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
  1638   by (simp add: Max_def semilattice_inf.below_fold1_iff [OF max_lattice] assms)
  1639 
  1640 lemma Min_gr_iff [simp, no_atp]:
  1641   assumes "finite A" and "A \<noteq> {}"
  1642   shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
  1643   using assms by (simp add: Min_def strict_below_fold1_iff)
  1644 
  1645 lemma Max_less_iff [simp, no_atp]:
  1646   assumes "finite A" and "A \<noteq> {}"
  1647   shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
  1648   by (simp add: Max_def linorder.dual_max [OF dual_linorder]
  1649     linorder.strict_below_fold1_iff [OF dual_linorder] assms)
  1650 
  1651 lemma Min_le_iff [no_atp]:
  1652   assumes "finite A" and "A \<noteq> {}"
  1653   shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
  1654   using assms by (simp add: Min_def fold1_below_iff)
  1655 
  1656 lemma Max_ge_iff [no_atp]:
  1657   assumes "finite A" and "A \<noteq> {}"
  1658   shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
  1659   by (simp add: Max_def linorder.dual_max [OF dual_linorder]
  1660     linorder.fold1_below_iff [OF dual_linorder] assms)
  1661 
  1662 lemma Min_less_iff [no_atp]:
  1663   assumes "finite A" and "A \<noteq> {}"
  1664   shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
  1665   using assms by (simp add: Min_def fold1_strict_below_iff)
  1666 
  1667 lemma Max_gr_iff [no_atp]:
  1668   assumes "finite A" and "A \<noteq> {}"
  1669   shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
  1670   by (simp add: Max_def linorder.dual_max [OF dual_linorder]
  1671     linorder.fold1_strict_below_iff [OF dual_linorder] assms)
  1672 
  1673 lemma Min_eqI:
  1674   assumes "finite A"
  1675   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
  1676     and "x \<in> A"
  1677   shows "Min A = x"
  1678 proof (rule antisym)
  1679   from `x \<in> A` have "A \<noteq> {}" by auto
  1680   with assms show "Min A \<ge> x" by simp
  1681 next
  1682   from assms show "x \<ge> Min A" by simp
  1683 qed
  1684 
  1685 lemma Max_eqI:
  1686   assumes "finite A"
  1687   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
  1688     and "x \<in> A"
  1689   shows "Max A = x"
  1690 proof (rule antisym)
  1691   from `x \<in> A` have "A \<noteq> {}" by auto
  1692   with assms show "Max A \<le> x" by simp
  1693 next
  1694   from assms show "x \<le> Max A" by simp
  1695 qed
  1696 
  1697 lemma Min_antimono:
  1698   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
  1699   shows "Min N \<le> Min M"
  1700   using assms by (simp add: Min_def fold1_antimono)
  1701 
  1702 lemma Max_mono:
  1703   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
  1704   shows "Max M \<le> Max N"
  1705   by (simp add: Max_def linorder.dual_max [OF dual_linorder]
  1706     linorder.fold1_antimono [OF dual_linorder] assms)
  1707 
  1708 lemma finite_linorder_max_induct[consumes 1, case_names empty insert]:
  1709  assumes fin: "finite A"
  1710  and   empty: "P {}" 
  1711  and  insert: "(!!b A. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))"
  1712  shows "P A"
  1713 using fin empty insert
  1714 proof (induct rule: finite_psubset_induct)
  1715   case (psubset A)
  1716   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 
  1717   have fin: "finite A" by fact 
  1718   have empty: "P {}" by fact
  1719   have step: "\<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)" by fact
  1720   show "P A"
  1721   proof (cases "A = {}")
  1722     assume "A = {}" 
  1723     then show "P A" using `P {}` by simp
  1724   next
  1725     let ?B = "A - {Max A}" 
  1726     let ?A = "insert (Max A) ?B"
  1727     have "finite ?B" using `finite A` by simp
  1728     assume "A \<noteq> {}"
  1729     with `finite A` have "Max A : A" by auto
  1730     then have A: "?A = A" using insert_Diff_single insert_absorb by auto
  1731     then have "P ?B" using `P {}` step IH[of ?B] by blast
  1732     moreover 
  1733     have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastforce
  1734     ultimately show "P A" using A insert_Diff_single step[OF `finite ?B`] by fastforce
  1735   qed
  1736 qed
  1737 
  1738 lemma finite_linorder_min_induct[consumes 1, case_names empty insert]:
  1739  "\<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"
  1740 by(rule linorder.finite_linorder_max_induct[OF dual_linorder])
  1741 
  1742 end
  1743 
  1744 context linordered_ab_semigroup_add
  1745 begin
  1746 
  1747 lemma add_Min_commute:
  1748   fixes k
  1749   assumes "finite N" and "N \<noteq> {}"
  1750   shows "k + Min N = Min {k + m | m. m \<in> N}"
  1751 proof -
  1752   have "\<And>x y. k + min x y = min (k + x) (k + y)"
  1753     by (simp add: min_def not_le)
  1754       (blast intro: antisym less_imp_le add_left_mono)
  1755   with assms show ?thesis
  1756     using hom_Min_commute [of "plus k" N]
  1757     by simp (blast intro: arg_cong [where f = Min])
  1758 qed
  1759 
  1760 lemma add_Max_commute:
  1761   fixes k
  1762   assumes "finite N" and "N \<noteq> {}"
  1763   shows "k + Max N = Max {k + m | m. m \<in> N}"
  1764 proof -
  1765   have "\<And>x y. k + max x y = max (k + x) (k + y)"
  1766     by (simp add: max_def not_le)
  1767       (blast intro: antisym less_imp_le add_left_mono)
  1768   with assms show ?thesis
  1769     using hom_Max_commute [of "plus k" N]
  1770     by simp (blast intro: arg_cong [where f = Max])
  1771 qed
  1772 
  1773 end
  1774 
  1775 context linordered_ab_group_add
  1776 begin
  1777 
  1778 lemma minus_Max_eq_Min [simp]:
  1779   "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Max S) = Min (uminus ` S)"
  1780   by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min)
  1781 
  1782 lemma minus_Min_eq_Max [simp]:
  1783   "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Min S) = Max (uminus ` S)"
  1784   by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max)
  1785 
  1786 end
  1787 
  1788 end