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