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