src/HOL/Big_Operators.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 44937 22c0857b8aab
child 46033 6fc579c917b8
permissions -rw-r--r--
Quotient_Info stores only relation maps
     1 (*  Title:      HOL/Big_Operators.thy
     2     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     3                 with contributions by Jeremy Avigad
     4 *)
     5 
     6 header {* Big operators and finite (non-empty) sets *}
     7 
     8 theory Big_Operators
     9 imports Plain
    10 begin
    11 
    12 subsection {* Generic monoid operation over a set *}
    13 
    14 no_notation times (infixl "*" 70)
    15 no_notation Groups.one ("1")
    16 
    17 locale comm_monoid_big = comm_monoid +
    18   fixes F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
    19   assumes F_eq: "F g A = (if finite A then fold_image (op *) g 1 A else 1)"
    20 
    21 sublocale comm_monoid_big < folding_image proof
    22 qed (simp add: F_eq)
    23 
    24 context comm_monoid_big
    25 begin
    26 
    27 lemma infinite [simp]:
    28   "\<not> finite A \<Longrightarrow> F g A = 1"
    29   by (simp add: F_eq)
    30 
    31 lemma F_cong:
    32   assumes "A = B" "\<And>x. x \<in> B \<Longrightarrow> h x = g x"
    33   shows "F h A = F g B"
    34 proof cases
    35   assume "finite A"
    36   with assms show ?thesis unfolding `A = B` by (simp cong: cong)
    37 next
    38   assume "\<not> finite A"
    39   then show ?thesis unfolding `A = B` by simp
    40 qed
    41 
    42 lemma If_cases:
    43   fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
    44   assumes fA: "finite A"
    45   shows "F (\<lambda>x. if P x then h x else g x) A =
    46          F h (A \<inter> {x. P x}) * F g (A \<inter> - {x. P x})"
    47 proof-
    48   have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}" 
    49           "(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}" 
    50     by blast+
    51   from fA 
    52   have f: "finite (A \<inter> {x. P x})" "finite (A \<inter> -{x. P x})" by auto
    53   let ?g = "\<lambda>x. if P x then h x else g x"
    54   from union_disjoint[OF f a(2), of ?g] a(1)
    55   show ?thesis
    56     by (subst (1 2) F_cong) simp_all
    57 qed
    58 
    59 end
    60 
    61 text {* for ad-hoc proofs for @{const fold_image} *}
    62 
    63 lemma (in comm_monoid_add) comm_monoid_mult:
    64   "class.comm_monoid_mult (op +) 0"
    65 proof qed (auto intro: add_assoc add_commute)
    66 
    67 notation times (infixl "*" 70)
    68 notation Groups.one ("1")
    69 
    70 
    71 subsection {* Generalized summation over a set *}
    72 
    73 definition (in comm_monoid_add) setsum :: "('b \<Rightarrow> 'a) => 'b set => 'a" where
    74   "setsum f A = (if finite A then fold_image (op +) f 0 A else 0)"
    75 
    76 sublocale comm_monoid_add < setsum!: comm_monoid_big "op +" 0 setsum proof
    77 qed (fact setsum_def)
    78 
    79 abbreviation
    80   Setsum  ("\<Sum>_" [1000] 999) where
    81   "\<Sum>A == setsum (%x. x) A"
    82 
    83 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
    84 written @{text"\<Sum>x\<in>A. e"}. *}
    85 
    86 syntax
    87   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
    88 syntax (xsymbols)
    89   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
    90 syntax (HTML output)
    91   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
    92 
    93 translations -- {* Beware of argument permutation! *}
    94   "SUM i:A. b" == "CONST setsum (%i. b) A"
    95   "\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
    96 
    97 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
    98  @{text"\<Sum>x|P. e"}. *}
    99 
   100 syntax
   101   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
   102 syntax (xsymbols)
   103   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   104 syntax (HTML output)
   105   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   106 
   107 translations
   108   "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
   109   "\<Sum>x|P. t" => "CONST setsum (%x. t) {x. P}"
   110 
   111 print_translation {*
   112 let
   113   fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
   114         if x <> y then raise Match
   115         else
   116           let
   117             val x' = Syntax_Trans.mark_bound x;
   118             val t' = subst_bound (x', t);
   119             val P' = subst_bound (x', P);
   120           in Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound x $ P' $ t' end
   121     | setsum_tr' _ = raise Match;
   122 in [(@{const_syntax setsum}, setsum_tr')] end
   123 *}
   124 
   125 lemma setsum_empty:
   126   "setsum f {} = 0"
   127   by (fact setsum.empty)
   128 
   129 lemma setsum_insert:
   130   "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   131   by (fact setsum.insert)
   132 
   133 lemma setsum_infinite:
   134   "~ finite A ==> setsum f A = 0"
   135   by (fact setsum.infinite)
   136 
   137 lemma (in comm_monoid_add) setsum_reindex:
   138   assumes "inj_on f B" shows "setsum h (f ` B) = setsum (h \<circ> f) B"
   139 proof -
   140   interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
   141   from assms show ?thesis by (auto simp add: setsum_def fold_image_reindex dest!:finite_imageD)
   142 qed
   143 
   144 lemma (in comm_monoid_add) setsum_reindex_id:
   145   "inj_on f B ==> setsum f B = setsum id (f ` B)"
   146   by (simp add: setsum_reindex)
   147 
   148 lemma (in comm_monoid_add) setsum_reindex_nonzero: 
   149   assumes fS: "finite S"
   150   and nz: "\<And> x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x = f y \<Longrightarrow> h (f x) = 0"
   151   shows "setsum h (f ` S) = setsum (h o f) S"
   152 using nz
   153 proof(induct rule: finite_induct[OF fS])
   154   case 1 thus ?case by simp
   155 next
   156   case (2 x F) 
   157   {assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto
   158     then obtain y where y: "y \<in> F" "f x = f y" by auto 
   159     from "2.hyps" y have xy: "x \<noteq> y" by auto
   160     
   161     from "2.prems"[of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp
   162     have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto
   163     also have "\<dots> = setsum (h o f) (insert x F)" 
   164       unfolding setsum.insert[OF `finite F` `x\<notin>F`]
   165       using h0
   166       apply simp
   167       apply (rule "2.hyps"(3))
   168       apply (rule_tac y="y" in  "2.prems")
   169       apply simp_all
   170       done
   171     finally have ?case .}
   172   moreover
   173   {assume fxF: "f x \<notin> f ` F"
   174     have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)" 
   175       using fxF "2.hyps" by simp 
   176     also have "\<dots> = setsum (h o f) (insert x F)"
   177       unfolding setsum.insert[OF `finite F` `x\<notin>F`]
   178       apply simp
   179       apply (rule cong [OF refl [of "op + (h (f x))"]])
   180       apply (rule "2.hyps"(3))
   181       apply (rule_tac y="y" in  "2.prems")
   182       apply simp_all
   183       done
   184     finally have ?case .}
   185   ultimately show ?case by blast
   186 qed
   187 
   188 lemma (in comm_monoid_add) setsum_cong:
   189   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
   190   by (cases "finite A") (auto intro: setsum.cong)
   191 
   192 lemma (in comm_monoid_add) strong_setsum_cong [cong]:
   193   "A = B ==> (!!x. x:B =simp=> f x = g x)
   194    ==> setsum (%x. f x) A = setsum (%x. g x) B"
   195   by (rule setsum_cong) (simp_all add: simp_implies_def)
   196 
   197 lemma (in comm_monoid_add) setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A"
   198   by (auto intro: setsum_cong)
   199 
   200 lemma (in comm_monoid_add) setsum_reindex_cong:
   201    "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|] 
   202     ==> setsum h B = setsum g A"
   203   by (simp add: setsum_reindex)
   204 
   205 lemma (in comm_monoid_add) setsum_0[simp]: "setsum (%i. 0) A = 0"
   206   by (cases "finite A") (erule finite_induct, auto)
   207 
   208 lemma (in comm_monoid_add) setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0"
   209   by (simp add:setsum_cong)
   210 
   211 lemma (in comm_monoid_add) setsum_Un_Int: "finite A ==> finite B ==>
   212   setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
   213   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   214   by (fact setsum.union_inter)
   215 
   216 lemma (in comm_monoid_add) setsum_Un_disjoint: "finite A ==> finite B
   217   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
   218   by (fact setsum.union_disjoint)
   219 
   220 lemma setsum_mono_zero_left: 
   221   assumes fT: "finite T" and ST: "S \<subseteq> T"
   222   and z: "\<forall>i \<in> T - S. f i = 0"
   223   shows "setsum f S = setsum f T"
   224 proof-
   225   have eq: "T = S \<union> (T - S)" using ST by blast
   226   have d: "S \<inter> (T - S) = {}" using ST by blast
   227   from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
   228   show ?thesis 
   229   by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
   230 qed
   231 
   232 lemma setsum_mono_zero_right: 
   233   "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. f i = 0 \<Longrightarrow> setsum f T = setsum f S"
   234 by(blast intro!: setsum_mono_zero_left[symmetric])
   235 
   236 lemma setsum_mono_zero_cong_left: 
   237   assumes fT: "finite T" and ST: "S \<subseteq> T"
   238   and z: "\<forall>i \<in> T - S. g i = 0"
   239   and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
   240   shows "setsum f S = setsum g T"
   241 proof-
   242   have eq: "T = S \<union> (T - S)" using ST by blast
   243   have d: "S \<inter> (T - S) = {}" using ST by blast
   244   from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
   245   show ?thesis 
   246     using fg by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
   247 qed
   248 
   249 lemma setsum_mono_zero_cong_right: 
   250   assumes fT: "finite T" and ST: "S \<subseteq> T"
   251   and z: "\<forall>i \<in> T - S. f i = 0"
   252   and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
   253   shows "setsum f T = setsum g S"
   254 using setsum_mono_zero_cong_left[OF fT ST z] fg[symmetric] by auto 
   255 
   256 lemma setsum_delta: 
   257   assumes fS: "finite S"
   258   shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
   259 proof-
   260   let ?f = "(\<lambda>k. if k=a then b k else 0)"
   261   {assume a: "a \<notin> S"
   262     hence "\<forall> k\<in> S. ?f k = 0" by simp
   263     hence ?thesis  using a by simp}
   264   moreover 
   265   {assume a: "a \<in> S"
   266     let ?A = "S - {a}"
   267     let ?B = "{a}"
   268     have eq: "S = ?A \<union> ?B" using a by blast 
   269     have dj: "?A \<inter> ?B = {}" by simp
   270     from fS have fAB: "finite ?A" "finite ?B" by auto  
   271     have "setsum ?f S = setsum ?f ?A + setsum ?f ?B"
   272       using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
   273       by simp
   274     then have ?thesis  using a by simp}
   275   ultimately show ?thesis by blast
   276 qed
   277 lemma setsum_delta': 
   278   assumes fS: "finite S" shows 
   279   "setsum (\<lambda>k. if a = k then b k else 0) S = 
   280      (if a\<in> S then b a else 0)"
   281   using setsum_delta[OF fS, of a b, symmetric] 
   282   by (auto intro: setsum_cong)
   283 
   284 lemma setsum_restrict_set:
   285   assumes fA: "finite A"
   286   shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A"
   287 proof-
   288   from fA have fab: "finite (A \<inter> B)" by auto
   289   have aba: "A \<inter> B \<subseteq> A" by blast
   290   let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0"
   291   from setsum_mono_zero_left[OF fA aba, of ?g]
   292   show ?thesis by simp
   293 qed
   294 
   295 lemma setsum_cases:
   296   assumes fA: "finite A"
   297   shows "setsum (\<lambda>x. if P x then f x else g x) A =
   298          setsum f (A \<inter> {x. P x}) + setsum g (A \<inter> - {x. P x})"
   299   using setsum.If_cases[OF fA] .
   300 
   301 (*But we can't get rid of finite I. If infinite, although the rhs is 0, 
   302   the lhs need not be, since UNION I A could still be finite.*)
   303 lemma (in comm_monoid_add) setsum_UN_disjoint:
   304   assumes "finite I" and "ALL i:I. finite (A i)"
   305     and "ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}"
   306   shows "setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
   307 proof -
   308   interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
   309   from assms show ?thesis by (simp add: setsum_def fold_image_UN_disjoint)
   310 qed
   311 
   312 text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
   313 directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
   314 lemma setsum_Union_disjoint:
   315   assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}"
   316   shows "setsum f (Union C) = setsum (setsum f) C"
   317 proof cases
   318   assume "finite C"
   319   from setsum_UN_disjoint[OF this assms]
   320   show ?thesis
   321     by (simp add: SUP_def)
   322 qed (force dest: finite_UnionD simp add: setsum_def)
   323 
   324 (*But we can't get rid of finite A. If infinite, although the lhs is 0, 
   325   the rhs need not be, since SIGMA A B could still be finite.*)
   326 lemma (in comm_monoid_add) setsum_Sigma:
   327   assumes "finite A" and  "ALL x:A. finite (B x)"
   328   shows "(\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
   329 proof -
   330   interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
   331   from assms show ?thesis by (simp add: setsum_def fold_image_Sigma split_def)
   332 qed
   333 
   334 text{*Here we can eliminate the finiteness assumptions, by cases.*}
   335 lemma setsum_cartesian_product: 
   336    "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)"
   337 apply (cases "finite A") 
   338  apply (cases "finite B") 
   339   apply (simp add: setsum_Sigma)
   340  apply (cases "A={}", simp)
   341  apply (simp) 
   342 apply (auto simp add: setsum_def
   343             dest: finite_cartesian_productD1 finite_cartesian_productD2) 
   344 done
   345 
   346 lemma (in comm_monoid_add) setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
   347   by (cases "finite A") (simp_all add: setsum.distrib)
   348 
   349 
   350 subsubsection {* Properties in more restricted classes of structures *}
   351 
   352 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   353 apply (case_tac "finite A")
   354  prefer 2 apply (simp add: setsum_def)
   355 apply (erule rev_mp)
   356 apply (erule finite_induct, auto)
   357 done
   358 
   359 lemma setsum_eq_0_iff [simp]:
   360     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   361 by (induct set: finite) auto
   362 
   363 lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
   364   (setsum f A = Suc 0) = (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
   365 apply(erule finite_induct)
   366 apply (auto simp add:add_is_1)
   367 done
   368 
   369 lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
   370 
   371 lemma setsum_Un_nat: "finite A ==> finite B ==>
   372   (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   373   -- {* For the natural numbers, we have subtraction. *}
   374 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
   375 
   376 lemma setsum_Un: "finite A ==> finite B ==>
   377   (setsum f (A Un B) :: 'a :: ab_group_add) =
   378    setsum f A + setsum f B - setsum f (A Int B)"
   379 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
   380 
   381 lemma (in comm_monoid_add) setsum_eq_general_reverses:
   382   assumes fS: "finite S" and fT: "finite T"
   383   and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
   384   and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x"
   385   shows "setsum f S = setsum g T"
   386 proof -
   387   interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
   388   show ?thesis
   389   apply (simp add: setsum_def fS fT)
   390   apply (rule fold_image_eq_general_inverses)
   391   apply (rule fS)
   392   apply (erule kh)
   393   apply (erule hk)
   394   done
   395 qed
   396 
   397 lemma (in comm_monoid_add) setsum_Un_zero:  
   398   assumes fS: "finite S" and fT: "finite T"
   399   and I0: "\<forall>x \<in> S\<inter>T. f x = 0"
   400   shows "setsum f (S \<union> T) = setsum f S  + setsum f T"
   401 proof -
   402   interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
   403   show ?thesis
   404   using fS fT
   405   apply (simp add: setsum_def)
   406   apply (rule fold_image_Un_one)
   407   using I0 by auto
   408 qed
   409 
   410 lemma setsum_UNION_zero: 
   411   assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T"
   412   and f0: "\<And>T1 T2 x. T1\<in>S \<Longrightarrow> T2\<in>S \<Longrightarrow> T1 \<noteq> T2 \<Longrightarrow> x \<in> T1 \<Longrightarrow> x \<in> T2 \<Longrightarrow> f x = 0"
   413   shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S"
   414   using fSS f0
   415 proof(induct rule: finite_induct[OF fS])
   416   case 1 thus ?case by simp
   417 next
   418   case (2 T F)
   419   then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F" 
   420     and H: "setsum f (\<Union> F) = setsum (setsum f) F" by auto
   421   from fTF have fUF: "finite (\<Union>F)" by auto
   422   from "2.prems" TF fTF
   423   show ?case 
   424     by (auto simp add: H[symmetric] intro: setsum_Un_zero[OF fTF(1) fUF, of f])
   425 qed
   426 
   427 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
   428   (if a:A then setsum f A - f a else setsum f A)"
   429 apply (case_tac "finite A")
   430  prefer 2 apply (simp add: setsum_def)
   431 apply (erule finite_induct)
   432  apply (auto simp add: insert_Diff_if)
   433 apply (drule_tac a = a in mk_disjoint_insert, auto)
   434 done
   435 
   436 lemma setsum_diff1: "finite A \<Longrightarrow>
   437   (setsum f (A - {a}) :: ('a::ab_group_add)) =
   438   (if a:A then setsum f A - f a else setsum f A)"
   439 by (erule finite_induct) (auto simp add: insert_Diff_if)
   440 
   441 lemma setsum_diff1'[rule_format]:
   442   "finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x)"
   443 apply (erule finite_induct[where F=A and P="% A. (a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x))"])
   444 apply (auto simp add: insert_Diff_if add_ac)
   445 done
   446 
   447 lemma setsum_diff1_ring: assumes "finite A" "a \<in> A"
   448   shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)"
   449 unfolding setsum_diff1'[OF assms] by auto
   450 
   451 (* By Jeremy Siek: *)
   452 
   453 lemma setsum_diff_nat: 
   454 assumes "finite B" and "B \<subseteq> A"
   455 shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
   456 using assms
   457 proof induct
   458   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
   459 next
   460   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
   461     and xFinA: "insert x F \<subseteq> A"
   462     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
   463   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
   464   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
   465     by (simp add: setsum_diff1_nat)
   466   from xFinA have "F \<subseteq> A" by simp
   467   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
   468   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
   469     by simp
   470   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
   471   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
   472     by simp
   473   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
   474   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
   475     by simp
   476   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
   477 qed
   478 
   479 lemma setsum_diff:
   480   assumes le: "finite A" "B \<subseteq> A"
   481   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
   482 proof -
   483   from le have finiteB: "finite B" using finite_subset by auto
   484   show ?thesis using finiteB le
   485   proof induct
   486     case empty
   487     thus ?case by auto
   488   next
   489     case (insert x F)
   490     thus ?case using le finiteB 
   491       by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
   492   qed
   493 qed
   494 
   495 lemma setsum_mono:
   496   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, ordered_ab_semigroup_add}))"
   497   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
   498 proof (cases "finite K")
   499   case True
   500   thus ?thesis using le
   501   proof induct
   502     case empty
   503     thus ?case by simp
   504   next
   505     case insert
   506     thus ?case using add_mono by fastforce
   507   qed
   508 next
   509   case False
   510   thus ?thesis
   511     by (simp add: setsum_def)
   512 qed
   513 
   514 lemma setsum_strict_mono:
   515   fixes f :: "'a \<Rightarrow> 'b::{ordered_cancel_ab_semigroup_add,comm_monoid_add}"
   516   assumes "finite A"  "A \<noteq> {}"
   517     and "!!x. x:A \<Longrightarrow> f x < g x"
   518   shows "setsum f A < setsum g A"
   519   using assms
   520 proof (induct rule: finite_ne_induct)
   521   case singleton thus ?case by simp
   522 next
   523   case insert thus ?case by (auto simp: add_strict_mono)
   524 qed
   525 
   526 lemma setsum_negf:
   527   "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
   528 proof (cases "finite A")
   529   case True thus ?thesis by (induct set: finite) auto
   530 next
   531   case False thus ?thesis by (simp add: setsum_def)
   532 qed
   533 
   534 lemma setsum_subtractf:
   535   "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
   536     setsum f A - setsum g A"
   537 proof (cases "finite A")
   538   case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
   539 next
   540   case False thus ?thesis by (simp add: setsum_def)
   541 qed
   542 
   543 lemma setsum_nonneg:
   544   assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
   545   shows "0 \<le> setsum f A"
   546 proof (cases "finite A")
   547   case True thus ?thesis using nn
   548   proof induct
   549     case empty then show ?case by simp
   550   next
   551     case (insert x F)
   552     then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
   553     with insert show ?case by simp
   554   qed
   555 next
   556   case False thus ?thesis by (simp add: setsum_def)
   557 qed
   558 
   559 lemma setsum_nonpos:
   560   assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{ordered_ab_semigroup_add,comm_monoid_add})"
   561   shows "setsum f A \<le> 0"
   562 proof (cases "finite A")
   563   case True thus ?thesis using np
   564   proof induct
   565     case empty then show ?case by simp
   566   next
   567     case (insert x F)
   568     then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
   569     with insert show ?case by simp
   570   qed
   571 next
   572   case False thus ?thesis by (simp add: setsum_def)
   573 qed
   574 
   575 lemma setsum_nonneg_leq_bound:
   576   fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
   577   assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s"
   578   shows "f i \<le> B"
   579 proof -
   580   have "0 \<le> (\<Sum> i \<in> s - {i}. f i)" and "0 \<le> f i"
   581     using assms by (auto intro!: setsum_nonneg)
   582   moreover
   583   have "(\<Sum> i \<in> s - {i}. f i) + f i = B"
   584     using assms by (simp add: setsum_diff1)
   585   ultimately show ?thesis by auto
   586 qed
   587 
   588 lemma setsum_nonneg_0:
   589   fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
   590   assumes "finite s" and pos: "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
   591   and "(\<Sum> i \<in> s. f i) = 0" and i: "i \<in> s"
   592   shows "f i = 0"
   593   using setsum_nonneg_leq_bound[OF assms] pos[OF i] by auto
   594 
   595 lemma setsum_mono2:
   596 fixes f :: "'a \<Rightarrow> 'b :: ordered_comm_monoid_add"
   597 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
   598 shows "setsum f A \<le> setsum f B"
   599 proof -
   600   have "setsum f A \<le> setsum f A + setsum f (B-A)"
   601     by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
   602   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
   603     by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
   604   also have "A \<union> (B-A) = B" using sub by blast
   605   finally show ?thesis .
   606 qed
   607 
   608 lemma setsum_mono3: "finite B ==> A <= B ==> 
   609     ALL x: B - A. 
   610       0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==>
   611         setsum f A <= setsum f B"
   612   apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
   613   apply (erule ssubst)
   614   apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
   615   apply simp
   616   apply (rule add_left_mono)
   617   apply (erule setsum_nonneg)
   618   apply (subst setsum_Un_disjoint [THEN sym])
   619   apply (erule finite_subset, assumption)
   620   apply (rule finite_subset)
   621   prefer 2
   622   apply assumption
   623   apply (auto simp add: sup_absorb2)
   624 done
   625 
   626 lemma setsum_right_distrib: 
   627   fixes f :: "'a => ('b::semiring_0)"
   628   shows "r * setsum f A = setsum (%n. r * f n) A"
   629 proof (cases "finite A")
   630   case True
   631   thus ?thesis
   632   proof induct
   633     case empty thus ?case by simp
   634   next
   635     case (insert x A) thus ?case by (simp add: right_distrib)
   636   qed
   637 next
   638   case False thus ?thesis by (simp add: setsum_def)
   639 qed
   640 
   641 lemma setsum_left_distrib:
   642   "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
   643 proof (cases "finite A")
   644   case True
   645   then show ?thesis
   646   proof induct
   647     case empty thus ?case by simp
   648   next
   649     case (insert x A) thus ?case by (simp add: left_distrib)
   650   qed
   651 next
   652   case False thus ?thesis by (simp add: setsum_def)
   653 qed
   654 
   655 lemma setsum_divide_distrib:
   656   "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
   657 proof (cases "finite A")
   658   case True
   659   then show ?thesis
   660   proof induct
   661     case empty thus ?case by simp
   662   next
   663     case (insert x A) thus ?case by (simp add: add_divide_distrib)
   664   qed
   665 next
   666   case False thus ?thesis by (simp add: setsum_def)
   667 qed
   668 
   669 lemma setsum_abs[iff]: 
   670   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   671   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
   672 proof (cases "finite A")
   673   case True
   674   thus ?thesis
   675   proof induct
   676     case empty thus ?case by simp
   677   next
   678     case (insert x A)
   679     thus ?case by (auto intro: abs_triangle_ineq order_trans)
   680   qed
   681 next
   682   case False thus ?thesis by (simp add: setsum_def)
   683 qed
   684 
   685 lemma setsum_abs_ge_zero[iff]: 
   686   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   687   shows "0 \<le> setsum (%i. abs(f i)) A"
   688 proof (cases "finite A")
   689   case True
   690   thus ?thesis
   691   proof induct
   692     case empty thus ?case by simp
   693   next
   694     case (insert x A) thus ?case by auto
   695   qed
   696 next
   697   case False thus ?thesis by (simp add: setsum_def)
   698 qed
   699 
   700 lemma abs_setsum_abs[simp]: 
   701   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   702   shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
   703 proof (cases "finite A")
   704   case True
   705   thus ?thesis
   706   proof induct
   707     case empty thus ?case by simp
   708   next
   709     case (insert a A)
   710     hence "\<bar>\<Sum>a\<in>insert a A. \<bar>f a\<bar>\<bar> = \<bar>\<bar>f a\<bar> + (\<Sum>a\<in>A. \<bar>f a\<bar>)\<bar>" by simp
   711     also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
   712     also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
   713       by (simp del: abs_of_nonneg)
   714     also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
   715     finally show ?case .
   716   qed
   717 next
   718   case False thus ?thesis by (simp add: setsum_def)
   719 qed
   720 
   721 lemma setsum_Plus:
   722   fixes A :: "'a set" and B :: "'b set"
   723   assumes fin: "finite A" "finite B"
   724   shows "setsum f (A <+> B) = setsum (f \<circ> Inl) A + setsum (f \<circ> Inr) B"
   725 proof -
   726   have "A <+> B = Inl ` A \<union> Inr ` B" by auto
   727   moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)"
   728     by auto
   729   moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto
   730   moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI)
   731   ultimately show ?thesis using fin by(simp add: setsum_Un_disjoint setsum_reindex)
   732 qed
   733 
   734 
   735 text {* Commuting outer and inner summation *}
   736 
   737 lemma setsum_commute:
   738   "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
   739 proof (simp add: setsum_cartesian_product)
   740   have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
   741     (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
   742     (is "?s = _")
   743     apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on)
   744     apply (simp add: split_def)
   745     done
   746   also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
   747     (is "_ = ?t")
   748     apply (simp add: swap_product)
   749     done
   750   finally show "?s = ?t" .
   751 qed
   752 
   753 lemma setsum_product:
   754   fixes f :: "'a => ('b::semiring_0)"
   755   shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
   756   by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
   757 
   758 lemma setsum_mult_setsum_if_inj:
   759 fixes f :: "'a => ('b::semiring_0)"
   760 shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==>
   761   setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}"
   762 by(auto simp: setsum_product setsum_cartesian_product
   763         intro!:  setsum_reindex_cong[symmetric])
   764 
   765 lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
   766 apply (cases "finite A")
   767 apply (erule finite_induct)
   768 apply (auto simp add: algebra_simps)
   769 done
   770 
   771 lemma setsum_bounded:
   772   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
   773   shows "setsum f A \<le> of_nat(card A) * K"
   774 proof (cases "finite A")
   775   case True
   776   thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
   777 next
   778   case False thus ?thesis by (simp add: setsum_def)
   779 qed
   780 
   781 
   782 subsubsection {* Cardinality as special case of @{const setsum} *}
   783 
   784 lemma card_eq_setsum:
   785   "card A = setsum (\<lambda>x. 1) A"
   786   by (simp only: card_def setsum_def)
   787 
   788 lemma card_UN_disjoint:
   789   "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 (simp_all add: SUP_def id_def)
   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(fastforce 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(fastforce 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   assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}" 
  1000   shows "setprod f (Union C) = setprod (setprod f) C"
  1001 proof cases
  1002   assume "finite C"
  1003   from setprod_UN_disjoint[OF this assms]
  1004   show ?thesis
  1005     by (simp add: SUP_def)
  1006 qed (force dest: finite_UnionD simp add: setprod_def)
  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])
  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 = {b} \<union> 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 qed
  1441 
  1442 lemma Sup_fin_Sup:
  1443   assumes "finite A" and "A \<noteq> {}"
  1444   shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
  1445 proof -
  1446   interpret ab_semigroup_idem_mult sup
  1447     by (rule ab_semigroup_idem_mult_sup)
  1448   from `A \<noteq> {}` obtain b B where "A = {b} \<union> B" by auto
  1449   moreover with `finite A` have "finite B" by simp
  1450   ultimately show ?thesis  
  1451   by (simp add: Sup_fin_def fold1_eq_fold_idem sup_Sup_fold_sup [symmetric])
  1452 qed
  1453 
  1454 end
  1455 
  1456 
  1457 subsection {* Versions of @{const min} and @{const max} on non-empty sets *}
  1458 
  1459 definition (in linorder) Min :: "'a set \<Rightarrow> 'a" where
  1460   "Min = fold1 min"
  1461 
  1462 definition (in linorder) Max :: "'a set \<Rightarrow> 'a" where
  1463   "Max = fold1 max"
  1464 
  1465 sublocale linorder < Min!: semilattice_big min Min proof
  1466 qed (simp add: Min_def)
  1467 
  1468 sublocale linorder < Max!: semilattice_big max Max proof
  1469 qed (simp add: Max_def)
  1470 
  1471 context linorder
  1472 begin
  1473 
  1474 lemmas Min_singleton = Min.singleton
  1475 lemmas Max_singleton = Max.singleton
  1476 
  1477 lemma Min_insert:
  1478   assumes "finite A" and "A \<noteq> {}"
  1479   shows "Min (insert x A) = min x (Min A)"
  1480   using assms by simp
  1481 
  1482 lemma Max_insert:
  1483   assumes "finite A" and "A \<noteq> {}"
  1484   shows "Max (insert x A) = max x (Max A)"
  1485   using assms by simp
  1486 
  1487 lemma Min_Un:
  1488   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
  1489   shows "Min (A \<union> B) = min (Min A) (Min B)"
  1490   using assms by (rule Min.union_idem)
  1491 
  1492 lemma Max_Un:
  1493   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
  1494   shows "Max (A \<union> B) = max (Max A) (Max B)"
  1495   using assms by (rule Max.union_idem)
  1496 
  1497 lemma hom_Min_commute:
  1498   assumes "\<And>x y. h (min x y) = min (h x) (h y)"
  1499     and "finite N" and "N \<noteq> {}"
  1500   shows "h (Min N) = Min (h ` N)"
  1501   using assms by (rule Min.hom_commute)
  1502 
  1503 lemma hom_Max_commute:
  1504   assumes "\<And>x y. h (max x y) = max (h x) (h y)"
  1505     and "finite N" and "N \<noteq> {}"
  1506   shows "h (Max N) = Max (h ` N)"
  1507   using assms by (rule Max.hom_commute)
  1508 
  1509 lemma ab_semigroup_idem_mult_min:
  1510   "class.ab_semigroup_idem_mult min"
  1511   proof qed (auto simp add: min_def)
  1512 
  1513 lemma ab_semigroup_idem_mult_max:
  1514   "class.ab_semigroup_idem_mult max"
  1515   proof qed (auto simp add: max_def)
  1516 
  1517 lemma max_lattice:
  1518   "class.semilattice_inf max (op \<ge>) (op >)"
  1519   by (fact min_max.dual_semilattice)
  1520 
  1521 lemma dual_max:
  1522   "ord.max (op \<ge>) = min"
  1523   by (auto simp add: ord.max_def_raw min_def fun_eq_iff)
  1524 
  1525 lemma dual_min:
  1526   "ord.min (op \<ge>) = max"
  1527   by (auto simp add: ord.min_def_raw max_def fun_eq_iff)
  1528 
  1529 lemma strict_below_fold1_iff:
  1530   assumes "finite A" and "A \<noteq> {}"
  1531   shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
  1532 proof -
  1533   interpret ab_semigroup_idem_mult min
  1534     by (rule ab_semigroup_idem_mult_min)
  1535   from assms show ?thesis
  1536   by (induct rule: finite_ne_induct)
  1537     (simp_all add: fold1_insert)
  1538 qed
  1539 
  1540 lemma fold1_below_iff:
  1541   assumes "finite A" and "A \<noteq> {}"
  1542   shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
  1543 proof -
  1544   interpret ab_semigroup_idem_mult min
  1545     by (rule ab_semigroup_idem_mult_min)
  1546   from assms show ?thesis
  1547   by (induct rule: finite_ne_induct)
  1548     (simp_all add: fold1_insert min_le_iff_disj)
  1549 qed
  1550 
  1551 lemma fold1_strict_below_iff:
  1552   assumes "finite A" and "A \<noteq> {}"
  1553   shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
  1554 proof -
  1555   interpret ab_semigroup_idem_mult min
  1556     by (rule ab_semigroup_idem_mult_min)
  1557   from assms show ?thesis
  1558   by (induct rule: finite_ne_induct)
  1559     (simp_all add: fold1_insert min_less_iff_disj)
  1560 qed
  1561 
  1562 lemma fold1_antimono:
  1563   assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
  1564   shows "fold1 min B \<le> fold1 min A"
  1565 proof cases
  1566   assume "A = B" thus ?thesis by simp
  1567 next
  1568   interpret ab_semigroup_idem_mult min
  1569     by (rule ab_semigroup_idem_mult_min)
  1570   assume neq: "A \<noteq> B"
  1571   have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
  1572   have "fold1 min B = fold1 min (A \<union> (B-A))" by(subst B)(rule refl)
  1573   also have "\<dots> = min (fold1 min A) (fold1 min (B-A))"
  1574   proof -
  1575     have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
  1576     moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`])
  1577     moreover have "(B-A) \<noteq> {}" using assms neq by blast
  1578     moreover have "A Int (B-A) = {}" using assms by blast
  1579     ultimately show ?thesis using `A \<noteq> {}` by (rule_tac fold1_Un)
  1580   qed
  1581   also have "\<dots> \<le> fold1 min A" by (simp add: min_le_iff_disj)
  1582   finally show ?thesis .
  1583 qed
  1584 
  1585 lemma Min_in [simp]:
  1586   assumes "finite A" and "A \<noteq> {}"
  1587   shows "Min A \<in> A"
  1588 proof -
  1589   interpret ab_semigroup_idem_mult min
  1590     by (rule ab_semigroup_idem_mult_min)
  1591   from assms fold1_in show ?thesis by (fastforce simp: Min_def min_def)
  1592 qed
  1593 
  1594 lemma Max_in [simp]:
  1595   assumes "finite A" and "A \<noteq> {}"
  1596   shows "Max A \<in> A"
  1597 proof -
  1598   interpret ab_semigroup_idem_mult max
  1599     by (rule ab_semigroup_idem_mult_max)
  1600   from assms fold1_in [of A] show ?thesis by (fastforce simp: Max_def max_def)
  1601 qed
  1602 
  1603 lemma Min_le [simp]:
  1604   assumes "finite A" and "x \<in> A"
  1605   shows "Min A \<le> x"
  1606   using assms by (simp add: Min_def min_max.fold1_belowI)
  1607 
  1608 lemma Max_ge [simp]:
  1609   assumes "finite A" and "x \<in> A"
  1610   shows "x \<le> Max A"
  1611   by (simp add: Max_def semilattice_inf.fold1_belowI [OF max_lattice] assms)
  1612 
  1613 lemma Min_ge_iff [simp, no_atp]:
  1614   assumes "finite A" and "A \<noteq> {}"
  1615   shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
  1616   using assms by (simp add: Min_def min_max.below_fold1_iff)
  1617 
  1618 lemma Max_le_iff [simp, no_atp]:
  1619   assumes "finite A" and "A \<noteq> {}"
  1620   shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
  1621   by (simp add: Max_def semilattice_inf.below_fold1_iff [OF max_lattice] assms)
  1622 
  1623 lemma Min_gr_iff [simp, no_atp]:
  1624   assumes "finite A" and "A \<noteq> {}"
  1625   shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
  1626   using assms by (simp add: Min_def strict_below_fold1_iff)
  1627 
  1628 lemma Max_less_iff [simp, no_atp]:
  1629   assumes "finite A" and "A \<noteq> {}"
  1630   shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
  1631   by (simp add: Max_def linorder.dual_max [OF dual_linorder]
  1632     linorder.strict_below_fold1_iff [OF dual_linorder] assms)
  1633 
  1634 lemma Min_le_iff [no_atp]:
  1635   assumes "finite A" and "A \<noteq> {}"
  1636   shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
  1637   using assms by (simp add: Min_def fold1_below_iff)
  1638 
  1639 lemma Max_ge_iff [no_atp]:
  1640   assumes "finite A" and "A \<noteq> {}"
  1641   shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
  1642   by (simp add: Max_def linorder.dual_max [OF dual_linorder]
  1643     linorder.fold1_below_iff [OF dual_linorder] assms)
  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   by (simp add: Max_def linorder.dual_max [OF dual_linorder]
  1654     linorder.fold1_strict_below_iff [OF dual_linorder] assms)
  1655 
  1656 lemma Min_eqI:
  1657   assumes "finite A"
  1658   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
  1659     and "x \<in> A"
  1660   shows "Min A = x"
  1661 proof (rule antisym)
  1662   from `x \<in> A` have "A \<noteq> {}" by auto
  1663   with assms show "Min A \<ge> x" by simp
  1664 next
  1665   from assms show "x \<ge> Min A" by simp
  1666 qed
  1667 
  1668 lemma Max_eqI:
  1669   assumes "finite A"
  1670   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
  1671     and "x \<in> A"
  1672   shows "Max A = x"
  1673 proof (rule antisym)
  1674   from `x \<in> A` have "A \<noteq> {}" by auto
  1675   with assms show "Max A \<le> x" by simp
  1676 next
  1677   from assms show "x \<le> Max A" by simp
  1678 qed
  1679 
  1680 lemma Min_antimono:
  1681   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
  1682   shows "Min N \<le> Min M"
  1683   using assms by (simp add: Min_def fold1_antimono)
  1684 
  1685 lemma Max_mono:
  1686   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
  1687   shows "Max M \<le> Max N"
  1688   by (simp add: Max_def linorder.dual_max [OF dual_linorder]
  1689     linorder.fold1_antimono [OF dual_linorder] assms)
  1690 
  1691 lemma finite_linorder_max_induct[consumes 1, case_names empty insert]:
  1692  assumes fin: "finite A"
  1693  and   empty: "P {}" 
  1694  and  insert: "(!!b A. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))"
  1695  shows "P A"
  1696 using fin empty insert
  1697 proof (induct rule: finite_psubset_induct)
  1698   case (psubset A)
  1699   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 
  1700   have fin: "finite A" by fact 
  1701   have empty: "P {}" by fact
  1702   have step: "\<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)" by fact
  1703   show "P A"
  1704   proof (cases "A = {}")
  1705     assume "A = {}" 
  1706     then show "P A" using `P {}` by simp
  1707   next
  1708     let ?B = "A - {Max A}" 
  1709     let ?A = "insert (Max A) ?B"
  1710     have "finite ?B" using `finite A` by simp
  1711     assume "A \<noteq> {}"
  1712     with `finite A` have "Max A : A" by auto
  1713     then have A: "?A = A" using insert_Diff_single insert_absorb by auto
  1714     then have "P ?B" using `P {}` step IH[of ?B] by blast
  1715     moreover 
  1716     have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastforce
  1717     ultimately show "P A" using A insert_Diff_single step[OF `finite ?B`] by fastforce
  1718   qed
  1719 qed
  1720 
  1721 lemma finite_linorder_min_induct[consumes 1, case_names empty insert]:
  1722  "\<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"
  1723 by(rule linorder.finite_linorder_max_induct[OF dual_linorder])
  1724 
  1725 end
  1726 
  1727 context linordered_ab_semigroup_add
  1728 begin
  1729 
  1730 lemma add_Min_commute:
  1731   fixes k
  1732   assumes "finite N" and "N \<noteq> {}"
  1733   shows "k + Min N = Min {k + m | m. m \<in> N}"
  1734 proof -
  1735   have "\<And>x y. k + min x y = min (k + x) (k + y)"
  1736     by (simp add: min_def not_le)
  1737       (blast intro: antisym less_imp_le add_left_mono)
  1738   with assms show ?thesis
  1739     using hom_Min_commute [of "plus k" N]
  1740     by simp (blast intro: arg_cong [where f = Min])
  1741 qed
  1742 
  1743 lemma add_Max_commute:
  1744   fixes k
  1745   assumes "finite N" and "N \<noteq> {}"
  1746   shows "k + Max N = Max {k + m | m. m \<in> N}"
  1747 proof -
  1748   have "\<And>x y. k + max x y = max (k + x) (k + y)"
  1749     by (simp add: max_def not_le)
  1750       (blast intro: antisym less_imp_le add_left_mono)
  1751   with assms show ?thesis
  1752     using hom_Max_commute [of "plus k" N]
  1753     by simp (blast intro: arg_cong [where f = Max])
  1754 qed
  1755 
  1756 end
  1757 
  1758 context linordered_ab_group_add
  1759 begin
  1760 
  1761 lemma minus_Max_eq_Min [simp]:
  1762   "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Max S) = Min (uminus ` S)"
  1763   by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min)
  1764 
  1765 lemma minus_Min_eq_Max [simp]:
  1766   "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Min S) = Max (uminus ` S)"
  1767   by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max)
  1768 
  1769 end
  1770 
  1771 end