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