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