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