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