author haftmann Wed Mar 10 16:53:27 2010 +0100 (2010-03-10) changeset 35719 99b6152aedf5 parent 35686 abf91fba0a70 child 35720 3fc79186a2f6
split off theory Big_Operators from theory Finite_Set
 src/HOL/Big_Operators.thy file | annotate | diff | revisions src/HOL/Finite_Set.thy file | annotate | diff | revisions src/HOL/IsaMakefile file | annotate | diff | revisions src/HOL/Option.thy file | annotate | diff | revisions src/HOL/Wellfounded.thy file | annotate | diff | revisions
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Big_Operators.thy	Wed Mar 10 16:53:27 2010 +0100
1.3 @@ -0,0 +1,2062 @@
1.4 +(*  Title:      HOL/Big_Operators.thy
1.5 +    Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
1.6 +                with contributions by Jeremy Avigad
1.7 +*)
1.8 +
1.9 +header {* Big operators and finite (non-empty) sets *}
1.10 +
1.11 +theory Big_Operators
1.12 +imports Finite_Set
1.13 +begin
1.14 +
1.15 +subsection {* Generalized summation over a set *}
1.16 +
1.19 +
1.20 +definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
1.21 +where "setsum f A == if finite A then fold_image (op +) f 0 A else 0"
1.22 +
1.23 +abbreviation
1.24 +  Setsum  ("\<Sum>_" [1000] 999) where
1.25 +  "\<Sum>A == setsum (%x. x) A"
1.26 +
1.27 +text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
1.28 +written @{text"\<Sum>x\<in>A. e"}. *}
1.29 +
1.30 +syntax
1.31 +  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
1.32 +syntax (xsymbols)
1.33 +  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
1.34 +syntax (HTML output)
1.35 +  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
1.36 +
1.37 +translations -- {* Beware of argument permutation! *}
1.38 +  "SUM i:A. b" == "CONST setsum (%i. b) A"
1.39 +  "\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
1.40 +
1.41 +text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
1.42 + @{text"\<Sum>x|P. e"}. *}
1.43 +
1.44 +syntax
1.45 +  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
1.46 +syntax (xsymbols)
1.47 +  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
1.48 +syntax (HTML output)
1.49 +  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
1.50 +
1.51 +translations
1.52 +  "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
1.53 +  "\<Sum>x|P. t" => "CONST setsum (%x. t) {x. P}"
1.54 +
1.55 +print_translation {*
1.56 +let
1.57 +  fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) \$ Abs (y, Ty, P)] =
1.58 +        if x <> y then raise Match
1.59 +        else
1.60 +          let
1.61 +            val x' = Syntax.mark_bound x;
1.62 +            val t' = subst_bound (x', t);
1.63 +            val P' = subst_bound (x', P);
1.64 +          in Syntax.const @{syntax_const "_qsetsum"} \$ Syntax.mark_bound x \$ P' \$ t' end
1.65 +    | setsum_tr' _ = raise Match;
1.66 +in [(@{const_syntax setsum}, setsum_tr')] end
1.67 +*}
1.68 +
1.69 +
1.70 +lemma setsum_empty [simp]: "setsum f {} = 0"
1.72 +
1.73 +lemma setsum_insert [simp]:
1.74 +  "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
1.76 +
1.77 +lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0"
1.79 +
1.80 +lemma setsum_reindex:
1.81 +     "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
1.83 +
1.84 +lemma setsum_reindex_id:
1.85 +     "inj_on f B ==> setsum f B = setsum id (f ` B)"
1.86 +by (auto simp add: setsum_reindex)
1.87 +
1.88 +lemma setsum_reindex_nonzero:
1.89 +  assumes fS: "finite S"
1.90 +  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"
1.91 +  shows "setsum h (f ` S) = setsum (h o f) S"
1.92 +using nz
1.93 +proof(induct rule: finite_induct[OF fS])
1.94 +  case 1 thus ?case by simp
1.95 +next
1.96 +  case (2 x F)
1.97 +  {assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto
1.98 +    then obtain y where y: "y \<in> F" "f x = f y" by auto
1.99 +    from "2.hyps" y have xy: "x \<noteq> y" by auto
1.100 +
1.101 +    from "2.prems"[of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp
1.102 +    have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto
1.103 +    also have "\<dots> = setsum (h o f) (insert x F)"
1.104 +      unfolding setsum_insert[OF `finite F` `x\<notin>F`]
1.105 +      using h0
1.106 +      apply simp
1.107 +      apply (rule "2.hyps"(3))
1.108 +      apply (rule_tac y="y" in  "2.prems")
1.109 +      apply simp_all
1.110 +      done
1.111 +    finally have ?case .}
1.112 +  moreover
1.113 +  {assume fxF: "f x \<notin> f ` F"
1.114 +    have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)"
1.115 +      using fxF "2.hyps" by simp
1.116 +    also have "\<dots> = setsum (h o f) (insert x F)"
1.117 +      unfolding setsum_insert[OF `finite F` `x\<notin>F`]
1.118 +      apply simp
1.119 +      apply (rule cong[OF refl[of "op + (h (f x))"]])
1.120 +      apply (rule "2.hyps"(3))
1.121 +      apply (rule_tac y="y" in  "2.prems")
1.122 +      apply simp_all
1.123 +      done
1.124 +    finally have ?case .}
1.125 +  ultimately show ?case by blast
1.126 +qed
1.127 +
1.128 +lemma setsum_cong:
1.129 +  "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
1.130 +by(fastsimp simp: setsum_def intro: comm_monoid_add.fold_image_cong)
1.131 +
1.132 +lemma strong_setsum_cong[cong]:
1.133 +  "A = B ==> (!!x. x:B =simp=> f x = g x)
1.134 +   ==> setsum (%x. f x) A = setsum (%x. g x) B"
1.135 +by(fastsimp simp: simp_implies_def setsum_def intro: comm_monoid_add.fold_image_cong)
1.136 +
1.137 +lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A"
1.138 +by (rule setsum_cong[OF refl], auto)
1.139 +
1.140 +lemma setsum_reindex_cong:
1.141 +   "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|]
1.142 +    ==> setsum h B = setsum g A"
1.143 +by (simp add: setsum_reindex cong: setsum_cong)
1.144 +
1.145 +
1.146 +lemma setsum_0[simp]: "setsum (%i. 0) A = 0"
1.147 +apply (clarsimp simp: setsum_def)
1.148 +apply (erule finite_induct, auto)
1.149 +done
1.150 +
1.151 +lemma setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0"
1.153 +
1.154 +lemma setsum_Un_Int: "finite A ==> finite B ==>
1.155 +  setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
1.156 +  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
1.158 +
1.159 +lemma setsum_Un_disjoint: "finite A ==> finite B
1.160 +  ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
1.161 +by (subst setsum_Un_Int [symmetric], auto)
1.162 +
1.163 +lemma setsum_mono_zero_left:
1.164 +  assumes fT: "finite T" and ST: "S \<subseteq> T"
1.165 +  and z: "\<forall>i \<in> T - S. f i = 0"
1.166 +  shows "setsum f S = setsum f T"
1.167 +proof-
1.168 +  have eq: "T = S \<union> (T - S)" using ST by blast
1.169 +  have d: "S \<inter> (T - S) = {}" using ST by blast
1.170 +  from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
1.171 +  show ?thesis
1.172 +  by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
1.173 +qed
1.174 +
1.175 +lemma setsum_mono_zero_right:
1.176 +  "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. f i = 0 \<Longrightarrow> setsum f T = setsum f S"
1.177 +by(blast intro!: setsum_mono_zero_left[symmetric])
1.178 +
1.179 +lemma setsum_mono_zero_cong_left:
1.180 +  assumes fT: "finite T" and ST: "S \<subseteq> T"
1.181 +  and z: "\<forall>i \<in> T - S. g i = 0"
1.182 +  and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
1.183 +  shows "setsum f S = setsum g T"
1.184 +proof-
1.185 +  have eq: "T = S \<union> (T - S)" using ST by blast
1.186 +  have d: "S \<inter> (T - S) = {}" using ST by blast
1.187 +  from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
1.188 +  show ?thesis
1.189 +    using fg by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
1.190 +qed
1.191 +
1.192 +lemma setsum_mono_zero_cong_right:
1.193 +  assumes fT: "finite T" and ST: "S \<subseteq> T"
1.194 +  and z: "\<forall>i \<in> T - S. f i = 0"
1.195 +  and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
1.196 +  shows "setsum f T = setsum g S"
1.197 +using setsum_mono_zero_cong_left[OF fT ST z] fg[symmetric] by auto
1.198 +
1.199 +lemma setsum_delta:
1.200 +  assumes fS: "finite S"
1.201 +  shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
1.202 +proof-
1.203 +  let ?f = "(\<lambda>k. if k=a then b k else 0)"
1.204 +  {assume a: "a \<notin> S"
1.205 +    hence "\<forall> k\<in> S. ?f k = 0" by simp
1.206 +    hence ?thesis  using a by simp}
1.207 +  moreover
1.208 +  {assume a: "a \<in> S"
1.209 +    let ?A = "S - {a}"
1.210 +    let ?B = "{a}"
1.211 +    have eq: "S = ?A \<union> ?B" using a by blast
1.212 +    have dj: "?A \<inter> ?B = {}" by simp
1.213 +    from fS have fAB: "finite ?A" "finite ?B" by auto
1.214 +    have "setsum ?f S = setsum ?f ?A + setsum ?f ?B"
1.215 +      using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
1.216 +      by simp
1.217 +    then have ?thesis  using a by simp}
1.218 +  ultimately show ?thesis by blast
1.219 +qed
1.220 +lemma setsum_delta':
1.221 +  assumes fS: "finite S" shows
1.222 +  "setsum (\<lambda>k. if a = k then b k else 0) S =
1.223 +     (if a\<in> S then b a else 0)"
1.224 +  using setsum_delta[OF fS, of a b, symmetric]
1.225 +  by (auto intro: setsum_cong)
1.226 +
1.227 +lemma setsum_restrict_set:
1.228 +  assumes fA: "finite A"
1.229 +  shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A"
1.230 +proof-
1.231 +  from fA have fab: "finite (A \<inter> B)" by auto
1.232 +  have aba: "A \<inter> B \<subseteq> A" by blast
1.233 +  let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0"
1.234 +  from setsum_mono_zero_left[OF fA aba, of ?g]
1.235 +  show ?thesis by simp
1.236 +qed
1.237 +
1.238 +lemma setsum_cases:
1.239 +  assumes fA: "finite A"
1.240 +  shows "setsum (\<lambda>x. if P x then f x else g x) A =
1.241 +         setsum f (A \<inter> {x. P x}) + setsum g (A \<inter> - {x. P x})"
1.242 +proof-
1.243 +  have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}"
1.244 +          "(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}"
1.245 +    by blast+
1.246 +  from fA
1.247 +  have f: "finite (A \<inter> {x. P x})" "finite (A \<inter> -{x. P x})" by auto
1.248 +  let ?g = "\<lambda>x. if P x then f x else g x"
1.249 +  from setsum_Un_disjoint[OF f a(2), of ?g] a(1)
1.250 +  show ?thesis by simp
1.251 +qed
1.252 +
1.253 +
1.254 +(*But we can't get rid of finite I. If infinite, although the rhs is 0,
1.255 +  the lhs need not be, since UNION I A could still be finite.*)
1.256 +lemma setsum_UN_disjoint:
1.257 +    "finite I ==> (ALL i:I. finite (A i)) ==>
1.258 +        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
1.259 +      setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
1.261 +
1.262 +text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
1.263 +directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
1.264 +lemma setsum_Union_disjoint:
1.265 +  "[| (ALL A:C. finite A);
1.266 +      (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
1.267 +   ==> setsum f (Union C) = setsum (setsum f) C"
1.268 +apply (cases "finite C")
1.269 + prefer 2 apply (force dest: finite_UnionD simp add: setsum_def)
1.270 +  apply (frule setsum_UN_disjoint [of C id f])
1.271 + apply (unfold Union_def id_def, assumption+)
1.272 +done
1.273 +
1.274 +(*But we can't get rid of finite A. If infinite, although the lhs is 0,
1.275 +  the rhs need not be, since SIGMA A B could still be finite.*)
1.276 +lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
1.277 +    (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
1.279 +
1.280 +text{*Here we can eliminate the finiteness assumptions, by cases.*}
1.281 +lemma setsum_cartesian_product:
1.282 +   "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)"
1.283 +apply (cases "finite A")
1.284 + apply (cases "finite B")
1.285 +  apply (simp add: setsum_Sigma)
1.286 + apply (cases "A={}", simp)
1.287 + apply (simp)
1.288 +apply (auto simp add: setsum_def
1.289 +            dest: finite_cartesian_productD1 finite_cartesian_productD2)
1.290 +done
1.291 +
1.292 +lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
1.294 +
1.295 +
1.296 +subsubsection {* Properties in more restricted classes of structures *}
1.297 +
1.298 +lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
1.299 +apply (case_tac "finite A")
1.300 + prefer 2 apply (simp add: setsum_def)
1.301 +apply (erule rev_mp)
1.302 +apply (erule finite_induct, auto)
1.303 +done
1.304 +
1.305 +lemma setsum_eq_0_iff [simp]:
1.306 +    "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
1.307 +by (induct set: finite) auto
1.308 +
1.309 +lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
1.310 +  (setsum f A = Suc 0) = (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
1.311 +apply(erule finite_induct)
1.313 +done
1.314 +
1.315 +lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
1.316 +
1.317 +lemma setsum_Un_nat: "finite A ==> finite B ==>
1.318 +  (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
1.319 +  -- {* For the natural numbers, we have subtraction. *}
1.320 +by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
1.321 +
1.322 +lemma setsum_Un: "finite A ==> finite B ==>
1.323 +  (setsum f (A Un B) :: 'a :: ab_group_add) =
1.324 +   setsum f A + setsum f B - setsum f (A Int B)"
1.325 +by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
1.326 +
1.327 +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"
1.328 +  apply (induct set: finite)
1.329 +  apply simp by auto
1.330 +
1.331 +lemma (in comm_monoid_mult) fold_image_Un_one:
1.332 +  assumes fS: "finite S" and fT: "finite T"
1.333 +  and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
1.334 +  shows "fold_image (op *) f 1 (S \<union> T) = fold_image (op *) f 1 S * fold_image (op *) f 1 T"
1.335 +proof-
1.336 +  have "fold_image op * f 1 (S \<inter> T) = 1"
1.337 +    apply (rule fold_image_1)
1.338 +    using fS fT I0 by auto
1.339 +  with fold_image_Un_Int[OF fS fT] show ?thesis by simp
1.340 +qed
1.341 +
1.342 +lemma setsum_eq_general_reverses:
1.343 +  assumes fS: "finite S" and fT: "finite T"
1.344 +  and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
1.345 +  and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x"
1.346 +  shows "setsum f S = setsum g T"
1.347 +  apply (simp add: setsum_def fS fT)
1.348 +  apply (rule comm_monoid_add.fold_image_eq_general_inverses[OF fS])
1.349 +  apply (erule kh)
1.350 +  apply (erule hk)
1.351 +  done
1.352 +
1.353 +
1.354 +
1.355 +lemma setsum_Un_zero:
1.356 +  assumes fS: "finite S" and fT: "finite T"
1.357 +  and I0: "\<forall>x \<in> S\<inter>T. f x = 0"
1.358 +  shows "setsum f (S \<union> T) = setsum f S  + setsum f T"
1.359 +  using fS fT
1.360 +  apply (simp add: setsum_def)
1.362 +  using I0 by auto
1.363 +
1.364 +
1.365 +lemma setsum_UNION_zero:
1.366 +  assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T"
1.367 +  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"
1.368 +  shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S"
1.369 +  using fSS f0
1.370 +proof(induct rule: finite_induct[OF fS])
1.371 +  case 1 thus ?case by simp
1.372 +next
1.373 +  case (2 T F)
1.374 +  then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F"
1.375 +    and H: "setsum f (\<Union> F) = setsum (setsum f) F" by auto
1.376 +  from fTF have fUF: "finite (\<Union>F)" by auto
1.377 +  from "2.prems" TF fTF
1.378 +  show ?case
1.379 +    by (auto simp add: H[symmetric] intro: setsum_Un_zero[OF fTF(1) fUF, of f])
1.380 +qed
1.381 +
1.382 +
1.383 +lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
1.384 +  (if a:A then setsum f A - f a else setsum f A)"
1.385 +apply (case_tac "finite A")
1.386 + prefer 2 apply (simp add: setsum_def)
1.387 +apply (erule finite_induct)
1.388 + apply (auto simp add: insert_Diff_if)
1.389 +apply (drule_tac a = a in mk_disjoint_insert, auto)
1.390 +done
1.391 +
1.392 +lemma setsum_diff1: "finite A \<Longrightarrow>
1.393 +  (setsum f (A - {a}) :: ('a::ab_group_add)) =
1.394 +  (if a:A then setsum f A - f a else setsum f A)"
1.395 +by (erule finite_induct) (auto simp add: insert_Diff_if)
1.396 +
1.397 +lemma setsum_diff1'[rule_format]:
1.398 +  "finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x)"
1.399 +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))"])
1.401 +done
1.402 +
1.403 +lemma setsum_diff1_ring: assumes "finite A" "a \<in> A"
1.404 +  shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)"
1.405 +unfolding setsum_diff1'[OF assms] by auto
1.406 +
1.407 +(* By Jeremy Siek: *)
1.408 +
1.409 +lemma setsum_diff_nat:
1.410 +assumes "finite B" and "B \<subseteq> A"
1.411 +shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
1.412 +using assms
1.413 +proof induct
1.414 +  show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
1.415 +next
1.416 +  fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
1.417 +    and xFinA: "insert x F \<subseteq> A"
1.418 +    and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
1.419 +  from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
1.420 +  from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
1.421 +    by (simp add: setsum_diff1_nat)
1.422 +  from xFinA have "F \<subseteq> A" by simp
1.423 +  with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
1.424 +  with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
1.425 +    by simp
1.426 +  from xnotinF have "A - insert x F = (A - F) - {x}" by auto
1.427 +  with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
1.428 +    by simp
1.429 +  from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
1.430 +  with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
1.431 +    by simp
1.432 +  thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
1.433 +qed
1.434 +
1.435 +lemma setsum_diff:
1.436 +  assumes le: "finite A" "B \<subseteq> A"
1.437 +  shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
1.438 +proof -
1.439 +  from le have finiteB: "finite B" using finite_subset by auto
1.440 +  show ?thesis using finiteB le
1.441 +  proof induct
1.442 +    case empty
1.443 +    thus ?case by auto
1.444 +  next
1.445 +    case (insert x F)
1.446 +    thus ?case using le finiteB
1.447 +      by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
1.448 +  qed
1.449 +qed
1.450 +
1.451 +lemma setsum_mono:
1.452 +  assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, ordered_ab_semigroup_add}))"
1.453 +  shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
1.454 +proof (cases "finite K")
1.455 +  case True
1.456 +  thus ?thesis using le
1.457 +  proof induct
1.458 +    case empty
1.459 +    thus ?case by simp
1.460 +  next
1.461 +    case insert
1.462 +    thus ?case using add_mono by fastsimp
1.463 +  qed
1.464 +next
1.465 +  case False
1.466 +  thus ?thesis
1.467 +    by (simp add: setsum_def)
1.468 +qed
1.469 +
1.470 +lemma setsum_strict_mono:
1.472 +  assumes "finite A"  "A \<noteq> {}"
1.473 +    and "!!x. x:A \<Longrightarrow> f x < g x"
1.474 +  shows "setsum f A < setsum g A"
1.475 +  using prems
1.476 +proof (induct rule: finite_ne_induct)
1.477 +  case singleton thus ?case by simp
1.478 +next
1.479 +  case insert thus ?case by (auto simp: add_strict_mono)
1.480 +qed
1.481 +
1.482 +lemma setsum_negf:
1.483 +  "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
1.484 +proof (cases "finite A")
1.485 +  case True thus ?thesis by (induct set: finite) auto
1.486 +next
1.487 +  case False thus ?thesis by (simp add: setsum_def)
1.488 +qed
1.489 +
1.490 +lemma setsum_subtractf:
1.491 +  "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
1.492 +    setsum f A - setsum g A"
1.493 +proof (cases "finite A")
1.494 +  case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
1.495 +next
1.496 +  case False thus ?thesis by (simp add: setsum_def)
1.497 +qed
1.498 +
1.499 +lemma setsum_nonneg:
1.501 +  shows "0 \<le> setsum f A"
1.502 +proof (cases "finite A")
1.503 +  case True thus ?thesis using nn
1.504 +  proof induct
1.505 +    case empty then show ?case by simp
1.506 +  next
1.507 +    case (insert x F)
1.508 +    then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
1.509 +    with insert show ?case by simp
1.510 +  qed
1.511 +next
1.512 +  case False thus ?thesis by (simp add: setsum_def)
1.513 +qed
1.514 +
1.515 +lemma setsum_nonpos:
1.517 +  shows "setsum f A \<le> 0"
1.518 +proof (cases "finite A")
1.519 +  case True thus ?thesis using np
1.520 +  proof induct
1.521 +    case empty then show ?case by simp
1.522 +  next
1.523 +    case (insert x F)
1.524 +    then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
1.525 +    with insert show ?case by simp
1.526 +  qed
1.527 +next
1.528 +  case False thus ?thesis by (simp add: setsum_def)
1.529 +qed
1.530 +
1.531 +lemma setsum_mono2:
1.533 +assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
1.534 +shows "setsum f A \<le> setsum f B"
1.535 +proof -
1.536 +  have "setsum f A \<le> setsum f A + setsum f (B-A)"
1.538 +  also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
1.539 +    by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
1.540 +  also have "A \<union> (B-A) = B" using sub by blast
1.541 +  finally show ?thesis .
1.542 +qed
1.543 +
1.544 +lemma setsum_mono3: "finite B ==> A <= B ==>
1.545 +    ALL x: B - A.
1.547 +        setsum f A <= setsum f B"
1.548 +  apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
1.549 +  apply (erule ssubst)
1.550 +  apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
1.551 +  apply simp
1.553 +  apply (erule setsum_nonneg)
1.554 +  apply (subst setsum_Un_disjoint [THEN sym])
1.555 +  apply (erule finite_subset, assumption)
1.556 +  apply (rule finite_subset)
1.557 +  prefer 2
1.558 +  apply assumption
1.559 +  apply (auto simp add: sup_absorb2)
1.560 +done
1.561 +
1.562 +lemma setsum_right_distrib:
1.563 +  fixes f :: "'a => ('b::semiring_0)"
1.564 +  shows "r * setsum f A = setsum (%n. r * f n) A"
1.565 +proof (cases "finite A")
1.566 +  case True
1.567 +  thus ?thesis
1.568 +  proof induct
1.569 +    case empty thus ?case by simp
1.570 +  next
1.571 +    case (insert x A) thus ?case by (simp add: right_distrib)
1.572 +  qed
1.573 +next
1.574 +  case False thus ?thesis by (simp add: setsum_def)
1.575 +qed
1.576 +
1.577 +lemma setsum_left_distrib:
1.578 +  "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
1.579 +proof (cases "finite A")
1.580 +  case True
1.581 +  then show ?thesis
1.582 +  proof induct
1.583 +    case empty thus ?case by simp
1.584 +  next
1.585 +    case (insert x A) thus ?case by (simp add: left_distrib)
1.586 +  qed
1.587 +next
1.588 +  case False thus ?thesis by (simp add: setsum_def)
1.589 +qed
1.590 +
1.591 +lemma setsum_divide_distrib:
1.592 +  "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
1.593 +proof (cases "finite A")
1.594 +  case True
1.595 +  then show ?thesis
1.596 +  proof induct
1.597 +    case empty thus ?case by simp
1.598 +  next
1.599 +    case (insert x A) thus ?case by (simp add: add_divide_distrib)
1.600 +  qed
1.601 +next
1.602 +  case False thus ?thesis by (simp add: setsum_def)
1.603 +qed
1.604 +
1.605 +lemma setsum_abs[iff]:
1.606 +  fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
1.607 +  shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
1.608 +proof (cases "finite A")
1.609 +  case True
1.610 +  thus ?thesis
1.611 +  proof induct
1.612 +    case empty thus ?case by simp
1.613 +  next
1.614 +    case (insert x A)
1.615 +    thus ?case by (auto intro: abs_triangle_ineq order_trans)
1.616 +  qed
1.617 +next
1.618 +  case False thus ?thesis by (simp add: setsum_def)
1.619 +qed
1.620 +
1.621 +lemma setsum_abs_ge_zero[iff]:
1.622 +  fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
1.623 +  shows "0 \<le> setsum (%i. abs(f i)) A"
1.624 +proof (cases "finite A")
1.625 +  case True
1.626 +  thus ?thesis
1.627 +  proof induct
1.628 +    case empty thus ?case by simp
1.629 +  next
1.630 +    case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg)
1.631 +  qed
1.632 +next
1.633 +  case False thus ?thesis by (simp add: setsum_def)
1.634 +qed
1.635 +
1.636 +lemma abs_setsum_abs[simp]:
1.637 +  fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
1.638 +  shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
1.639 +proof (cases "finite A")
1.640 +  case True
1.641 +  thus ?thesis
1.642 +  proof induct
1.643 +    case empty thus ?case by simp
1.644 +  next
1.645 +    case (insert a A)
1.646 +    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
1.647 +    also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
1.648 +    also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
1.649 +      by (simp del: abs_of_nonneg)
1.650 +    also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
1.651 +    finally show ?case .
1.652 +  qed
1.653 +next
1.654 +  case False thus ?thesis by (simp add: setsum_def)
1.655 +qed
1.656 +
1.657 +
1.658 +lemma setsum_Plus:
1.659 +  fixes A :: "'a set" and B :: "'b set"
1.660 +  assumes fin: "finite A" "finite B"
1.661 +  shows "setsum f (A <+> B) = setsum (f \<circ> Inl) A + setsum (f \<circ> Inr) B"
1.662 +proof -
1.663 +  have "A <+> B = Inl ` A \<union> Inr ` B" by auto
1.664 +  moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)"
1.665 +    by(auto intro: finite_imageI)
1.666 +  moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto
1.667 +  moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI)
1.668 +  ultimately show ?thesis using fin by(simp add: setsum_Un_disjoint setsum_reindex)
1.669 +qed
1.670 +
1.671 +
1.672 +text {* Commuting outer and inner summation *}
1.673 +
1.674 +lemma swap_inj_on:
1.675 +  "inj_on (%(i, j). (j, i)) (A \<times> B)"
1.676 +  by (unfold inj_on_def) fast
1.677 +
1.678 +lemma swap_product:
1.679 +  "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
1.680 +  by (simp add: split_def image_def) blast
1.681 +
1.682 +lemma setsum_commute:
1.683 +  "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
1.685 +  have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
1.686 +    (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
1.687 +    (is "?s = _")
1.688 +    apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on)
1.689 +    apply (simp add: split_def)
1.690 +    done
1.691 +  also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
1.692 +    (is "_ = ?t")
1.693 +    apply (simp add: swap_product)
1.694 +    done
1.695 +  finally show "?s = ?t" .
1.696 +qed
1.697 +
1.698 +lemma setsum_product:
1.699 +  fixes f :: "'a => ('b::semiring_0)"
1.700 +  shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
1.701 +  by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
1.702 +
1.703 +lemma setsum_mult_setsum_if_inj:
1.704 +fixes f :: "'a => ('b::semiring_0)"
1.705 +shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==>
1.706 +  setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}"
1.707 +by(auto simp: setsum_product setsum_cartesian_product
1.708 +        intro!:  setsum_reindex_cong[symmetric])
1.709 +
1.710 +
1.711 +subsection {* Generalized product over a set *}
1.712 +
1.713 +definition setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
1.714 +where "setprod f A == if finite A then fold_image (op *) f 1 A else 1"
1.715 +
1.716 +abbreviation
1.717 +  Setprod  ("\<Prod>_" [1000] 999) where
1.718 +  "\<Prod>A == setprod (%x. x) A"
1.719 +
1.720 +syntax
1.721 +  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
1.722 +syntax (xsymbols)
1.723 +  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
1.724 +syntax (HTML output)
1.725 +  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
1.726 +
1.727 +translations -- {* Beware of argument permutation! *}
1.728 +  "PROD i:A. b" == "CONST setprod (%i. b) A"
1.729 +  "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A"
1.730 +
1.731 +text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
1.732 + @{text"\<Prod>x|P. e"}. *}
1.733 +
1.734 +syntax
1.735 +  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
1.736 +syntax (xsymbols)
1.737 +  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
1.738 +syntax (HTML output)
1.739 +  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
1.740 +
1.741 +translations
1.742 +  "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
1.743 +  "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
1.744 +
1.745 +
1.746 +lemma setprod_empty [simp]: "setprod f {} = 1"
1.747 +by (auto simp add: setprod_def)
1.748 +
1.749 +lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
1.750 +    setprod f (insert a A) = f a * setprod f A"
1.752 +
1.753 +lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
1.755 +
1.756 +lemma setprod_reindex:
1.757 +   "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
1.758 +by(auto simp: setprod_def fold_image_reindex dest!:finite_imageD)
1.759 +
1.760 +lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
1.761 +by (auto simp add: setprod_reindex)
1.762 +
1.763 +lemma setprod_cong:
1.764 +  "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
1.765 +by(fastsimp simp: setprod_def intro: fold_image_cong)
1.766 +
1.767 +lemma strong_setprod_cong[cong]:
1.768 +  "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
1.769 +by(fastsimp simp: simp_implies_def setprod_def intro: fold_image_cong)
1.770 +
1.771 +lemma setprod_reindex_cong: "inj_on f A ==>
1.772 +    B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
1.773 +by (frule setprod_reindex, simp)
1.774 +
1.775 +lemma strong_setprod_reindex_cong: assumes i: "inj_on f A"
1.776 +  and B: "B = f ` A" and eq: "\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x"
1.777 +  shows "setprod h B = setprod g A"
1.778 +proof-
1.779 +    have "setprod h B = setprod (h o f) A"
1.780 +      by (simp add: B setprod_reindex[OF i, of h])
1.781 +    then show ?thesis apply simp
1.782 +      apply (rule setprod_cong)
1.783 +      apply simp
1.784 +      by (simp add: eq)
1.785 +qed
1.786 +
1.787 +lemma setprod_Un_one:
1.788 +  assumes fS: "finite S" and fT: "finite T"
1.789 +  and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
1.790 +  shows "setprod f (S \<union> T) = setprod f S  * setprod f T"
1.791 +  using fS fT
1.792 +  apply (simp add: setprod_def)
1.793 +  apply (rule fold_image_Un_one)
1.794 +  using I0 by auto
1.795 +
1.796 +
1.797 +lemma setprod_1: "setprod (%i. 1) A = 1"
1.798 +apply (case_tac "finite A")
1.799 +apply (erule finite_induct, auto simp add: mult_ac)
1.800 +done
1.801 +
1.802 +lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
1.803 +apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
1.804 +apply (erule ssubst, rule setprod_1)
1.805 +apply (rule setprod_cong, auto)
1.806 +done
1.807 +
1.808 +lemma setprod_Un_Int: "finite A ==> finite B
1.809 +    ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
1.811 +
1.812 +lemma setprod_Un_disjoint: "finite A ==> finite B
1.813 +  ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
1.814 +by (subst setprod_Un_Int [symmetric], auto)
1.815 +
1.816 +lemma setprod_mono_one_left:
1.817 +  assumes fT: "finite T" and ST: "S \<subseteq> T"
1.818 +  and z: "\<forall>i \<in> T - S. f i = 1"
1.819 +  shows "setprod f S = setprod f T"
1.820 +proof-
1.821 +  have eq: "T = S \<union> (T - S)" using ST by blast
1.822 +  have d: "S \<inter> (T - S) = {}" using ST by blast
1.823 +  from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
1.824 +  show ?thesis
1.825 +  by (simp add: setprod_Un_disjoint[OF f d, unfolded eq[symmetric]] setprod_1'[OF z])
1.826 +qed
1.827 +
1.828 +lemmas setprod_mono_one_right = setprod_mono_one_left [THEN sym]
1.829 +
1.830 +lemma setprod_delta:
1.831 +  assumes fS: "finite S"
1.832 +  shows "setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
1.833 +proof-
1.834 +  let ?f = "(\<lambda>k. if k=a then b k else 1)"
1.835 +  {assume a: "a \<notin> S"
1.836 +    hence "\<forall> k\<in> S. ?f k = 1" by simp
1.837 +    hence ?thesis  using a by (simp add: setprod_1 cong add: setprod_cong) }
1.838 +  moreover
1.839 +  {assume a: "a \<in> S"
1.840 +    let ?A = "S - {a}"
1.841 +    let ?B = "{a}"
1.842 +    have eq: "S = ?A \<union> ?B" using a by blast
1.843 +    have dj: "?A \<inter> ?B = {}" by simp
1.844 +    from fS have fAB: "finite ?A" "finite ?B" by auto
1.845 +    have fA1: "setprod ?f ?A = 1" apply (rule setprod_1') by auto
1.846 +    have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
1.847 +      using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
1.848 +      by simp
1.849 +    then have ?thesis  using a by (simp add: fA1 cong add: setprod_cong cong del: if_weak_cong)}
1.850 +  ultimately show ?thesis by blast
1.851 +qed
1.852 +
1.853 +lemma setprod_delta':
1.854 +  assumes fS: "finite S" shows
1.855 +  "setprod (\<lambda>k. if a = k then b k else 1) S =
1.856 +     (if a\<in> S then b a else 1)"
1.857 +  using setprod_delta[OF fS, of a b, symmetric]
1.858 +  by (auto intro: setprod_cong)
1.859 +
1.860 +
1.861 +lemma setprod_UN_disjoint:
1.862 +    "finite I ==> (ALL i:I. finite (A i)) ==>
1.863 +        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
1.864 +      setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
1.865 +by(simp add: setprod_def fold_image_UN_disjoint cong: setprod_cong)
1.866 +
1.867 +lemma setprod_Union_disjoint:
1.868 +  "[| (ALL A:C. finite A);
1.869 +      (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
1.870 +   ==> setprod f (Union C) = setprod (setprod f) C"
1.871 +apply (cases "finite C")
1.872 + prefer 2 apply (force dest: finite_UnionD simp add: setprod_def)
1.873 +  apply (frule setprod_UN_disjoint [of C id f])
1.874 + apply (unfold Union_def id_def, assumption+)
1.875 +done
1.876 +
1.877 +lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
1.878 +    (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
1.879 +    (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
1.880 +by(simp add:setprod_def fold_image_Sigma split_def cong:setprod_cong)
1.881 +
1.882 +text{*Here we can eliminate the finiteness assumptions, by cases.*}
1.883 +lemma setprod_cartesian_product:
1.884 +     "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
1.885 +apply (cases "finite A")
1.886 + apply (cases "finite B")
1.887 +  apply (simp add: setprod_Sigma)
1.888 + apply (cases "A={}", simp)
1.889 + apply (simp add: setprod_1)
1.890 +apply (auto simp add: setprod_def
1.891 +            dest: finite_cartesian_productD1 finite_cartesian_productD2)
1.892 +done
1.893 +
1.894 +lemma setprod_timesf:
1.895 +     "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
1.897 +
1.898 +
1.899 +subsubsection {* Properties in more restricted classes of structures *}
1.900 +
1.901 +lemma setprod_eq_1_iff [simp]:
1.902 +  "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
1.903 +by (induct set: finite) auto
1.904 +
1.905 +lemma setprod_zero:
1.906 +     "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
1.907 +apply (induct set: finite, force, clarsimp)
1.908 +apply (erule disjE, auto)
1.909 +done
1.910 +
1.911 +lemma setprod_nonneg [rule_format]:
1.912 +   "(ALL x: A. (0::'a::linordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
1.913 +by (cases "finite A", induct set: finite, simp_all add: mult_nonneg_nonneg)
1.914 +
1.915 +lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x)
1.916 +  --> 0 < setprod f A"
1.917 +by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos)
1.918 +
1.919 +lemma setprod_zero_iff[simp]: "finite A ==>
1.920 +  (setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) =
1.921 +  (EX x: A. f x = 0)"
1.922 +by (erule finite_induct, auto simp:no_zero_divisors)
1.923 +
1.924 +lemma setprod_pos_nat:
1.925 +  "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
1.926 +using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
1.927 +
1.928 +lemma setprod_pos_nat_iff[simp]:
1.929 +  "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
1.930 +using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
1.931 +
1.932 +lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
1.933 +  (setprod f (A Un B) :: 'a ::{field})
1.934 +   = setprod f A * setprod f B / setprod f (A Int B)"
1.935 +by (subst setprod_Un_Int [symmetric], auto)
1.936 +
1.937 +lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
1.938 +  (setprod f (A - {a}) :: 'a :: {field}) =
1.939 +  (if a:A then setprod f A / f a else setprod f A)"
1.940 +by (erule finite_induct) (auto simp add: insert_Diff_if)
1.941 +
1.942 +lemma setprod_inversef:
1.943 +  fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}"
1.944 +  shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)"
1.945 +by (erule finite_induct) auto
1.946 +
1.947 +lemma setprod_dividef:
1.948 +  fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}"
1.949 +  shows "finite A
1.950 +    ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
1.951 +apply (subgoal_tac
1.952 +         "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
1.953 +apply (erule ssubst)
1.954 +apply (subst divide_inverse)
1.955 +apply (subst setprod_timesf)
1.956 +apply (subst setprod_inversef, assumption+, rule refl)
1.957 +apply (rule setprod_cong, rule refl)
1.958 +apply (subst divide_inverse, auto)
1.959 +done
1.960 +
1.961 +lemma setprod_dvd_setprod [rule_format]:
1.962 +    "(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A"
1.963 +  apply (cases "finite A")
1.964 +  apply (induct set: finite)
1.965 +  apply (auto simp add: dvd_def)
1.966 +  apply (rule_tac x = "k * ka" in exI)
1.967 +  apply (simp add: algebra_simps)
1.968 +done
1.969 +
1.970 +lemma setprod_dvd_setprod_subset:
1.971 +  "finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B"
1.972 +  apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)")
1.973 +  apply (unfold dvd_def, blast)
1.974 +  apply (subst setprod_Un_disjoint [symmetric])
1.975 +  apply (auto elim: finite_subset intro: setprod_cong)
1.976 +done
1.977 +
1.978 +lemma setprod_dvd_setprod_subset2:
1.979 +  "finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow>
1.980 +      setprod f A dvd setprod g B"
1.981 +  apply (rule dvd_trans)
1.982 +  apply (rule setprod_dvd_setprod, erule (1) bspec)
1.983 +  apply (erule (1) setprod_dvd_setprod_subset)
1.984 +done
1.985 +
1.986 +lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow>
1.987 +    (f i ::'a::comm_semiring_1) dvd setprod f A"
1.988 +by (induct set: finite) (auto intro: dvd_mult)
1.989 +
1.990 +lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow>
1.991 +    (d::'a::comm_semiring_1) dvd (SUM x : A. f x)"
1.992 +  apply (cases "finite A")
1.993 +  apply (induct set: finite)
1.994 +  apply auto
1.995 +done
1.996 +
1.997 +lemma setprod_mono:
1.998 +  fixes f :: "'a \<Rightarrow> 'b\<Colon>linordered_semidom"
1.999 +  assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i"
1.1000 +  shows "setprod f A \<le> setprod g A"
1.1001 +proof (cases "finite A")
1.1002 +  case True
1.1003 +  hence ?thesis "setprod f A \<ge> 0" using subset_refl[of A]
1.1004 +  proof (induct A rule: finite_subset_induct)
1.1005 +    case (insert a F)
1.1006 +    thus "setprod f (insert a F) \<le> setprod g (insert a F)" "0 \<le> setprod f (insert a F)"
1.1007 +      unfolding setprod_insert[OF insert(1,3)]
1.1008 +      using assms[rule_format,OF insert(2)] insert
1.1009 +      by (auto intro: mult_mono mult_nonneg_nonneg)
1.1010 +  qed auto
1.1011 +  thus ?thesis by simp
1.1012 +qed auto
1.1013 +
1.1014 +lemma abs_setprod:
1.1015 +  fixes f :: "'a \<Rightarrow> 'b\<Colon>{linordered_field,abs}"
1.1016 +  shows "abs (setprod f A) = setprod (\<lambda>x. abs (f x)) A"
1.1017 +proof (cases "finite A")
1.1018 +  case True thus ?thesis
1.1019 +    by induct (auto simp add: field_simps abs_mult)
1.1020 +qed auto
1.1021 +
1.1022 +
1.1023 +subsection {* Finite cardinality *}
1.1024 +
1.1025 +text {* This definition, although traditional, is ugly to work with:
1.1026 +@{text "card A == LEAST n. EX f. A = {f i | i. i < n}"}.
1.1027 +But now that we have @{text setsum} things are easy:
1.1028 +*}
1.1029 +
1.1030 +definition card :: "'a set \<Rightarrow> nat" where
1.1031 +  "card A = setsum (\<lambda>x. 1) A"
1.1032 +
1.1033 +lemmas card_eq_setsum = card_def
1.1034 +
1.1035 +lemma card_empty [simp]: "card {} = 0"
1.1036 +  by (simp add: card_def)
1.1037 +
1.1038 +lemma card_insert_disjoint [simp]:
1.1039 +  "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
1.1040 +  by (simp add: card_def)
1.1041 +
1.1042 +lemma card_insert_if:
1.1043 +  "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
1.1044 +  by (simp add: insert_absorb)
1.1045 +
1.1046 +lemma card_infinite [simp]: "~ finite A ==> card A = 0"
1.1047 +  by (simp add: card_def)
1.1048 +
1.1049 +lemma card_ge_0_finite:
1.1050 +  "card A > 0 \<Longrightarrow> finite A"
1.1051 +  by (rule ccontr) simp
1.1052 +
1.1053 +lemma card_0_eq [simp,noatp]: "finite A ==> (card A = 0) = (A = {})"
1.1054 +  apply auto
1.1055 +  apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
1.1056 +  done
1.1057 +
1.1058 +lemma finite_UNIV_card_ge_0:
1.1059 +  "finite (UNIV :: 'a set) \<Longrightarrow> card (UNIV :: 'a set) > 0"
1.1060 +  by (rule ccontr) simp
1.1061 +
1.1062 +lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
1.1063 +  by auto
1.1064 +
1.1065 +lemma card_gt_0_iff: "(0 < card A) = (A \<noteq> {} & finite A)"
1.1066 +  by (simp add: neq0_conv [symmetric] card_eq_0_iff)
1.1067 +
1.1068 +lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
1.1069 +apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
1.1070 +apply(simp del:insert_Diff_single)
1.1071 +done
1.1072 +
1.1073 +lemma card_Diff_singleton:
1.1074 +  "finite A ==> x: A ==> card (A - {x}) = card A - 1"
1.1075 +by (simp add: card_Suc_Diff1 [symmetric])
1.1076 +
1.1077 +lemma card_Diff_singleton_if:
1.1078 +  "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
1.1080 +
1.1081 +lemma card_Diff_insert[simp]:
1.1082 +assumes "finite A" and "a:A" and "a ~: B"
1.1083 +shows "card(A - insert a B) = card(A - B) - 1"
1.1084 +proof -
1.1085 +  have "A - insert a B = (A - B) - {a}" using assms by blast
1.1086 +  then show ?thesis using assms by(simp add:card_Diff_singleton)
1.1087 +qed
1.1088 +
1.1089 +lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
1.1090 +by (simp add: card_insert_if card_Suc_Diff1 del:card_Diff_insert)
1.1091 +
1.1092 +lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
1.1094 +
1.1095 +lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
1.1096 +by (simp add: card_def setsum_mono2)
1.1097 +
1.1098 +lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
1.1099 +apply (induct set: finite, simp, clarify)
1.1100 +apply (subgoal_tac "finite A & A - {x} <= F")
1.1101 + prefer 2 apply (blast intro: finite_subset, atomize)
1.1102 +apply (drule_tac x = "A - {x}" in spec)
1.1104 +apply (case_tac "card A", auto)
1.1105 +done
1.1106 +
1.1107 +lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
1.1108 +apply (simp add: psubset_eq linorder_not_le [symmetric])
1.1109 +apply (blast dest: card_seteq)
1.1110 +done
1.1111 +
1.1112 +lemma card_Un_Int: "finite A ==> finite B
1.1113 +    ==> card A + card B = card (A Un B) + card (A Int B)"
1.1115 +
1.1116 +lemma card_Un_disjoint: "finite A ==> finite B
1.1117 +    ==> A Int B = {} ==> card (A Un B) = card A + card B"
1.1119 +
1.1120 +lemma card_Diff_subset:
1.1121 +  "finite B ==> B <= A ==> card (A - B) = card A - card B"
1.1123 +
1.1124 +lemma card_Diff_subset_Int:
1.1125 +  assumes AB: "finite (A \<inter> B)" shows "card (A - B) = card A - card (A \<inter> B)"
1.1126 +proof -
1.1127 +  have "A - B = A - A \<inter> B" by auto
1.1128 +  thus ?thesis
1.1129 +    by (simp add: card_Diff_subset AB)
1.1130 +qed
1.1131 +
1.1132 +lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
1.1133 +apply (rule Suc_less_SucD)
1.1134 +apply (simp add: card_Suc_Diff1 del:card_Diff_insert)
1.1135 +done
1.1136 +
1.1137 +lemma card_Diff2_less:
1.1138 +  "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
1.1139 +apply (case_tac "x = y")
1.1140 + apply (simp add: card_Diff1_less del:card_Diff_insert)
1.1141 +apply (rule less_trans)
1.1142 + prefer 2 apply (auto intro!: card_Diff1_less simp del:card_Diff_insert)
1.1143 +done
1.1144 +
1.1145 +lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
1.1146 +apply (case_tac "x : A")
1.1147 + apply (simp_all add: card_Diff1_less less_imp_le)
1.1148 +done
1.1149 +
1.1150 +lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
1.1151 +by (erule psubsetI, blast)
1.1152 +
1.1153 +lemma insert_partition:
1.1154 +  "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
1.1155 +  \<Longrightarrow> x \<inter> \<Union> F = {}"
1.1156 +by auto
1.1157 +
1.1158 +lemma finite_psubset_induct[consumes 1, case_names psubset]:
1.1159 +  assumes "finite A" and "!!A. finite A \<Longrightarrow> (!!B. finite B \<Longrightarrow> B \<subset> A \<Longrightarrow> P(B)) \<Longrightarrow> P(A)" shows "P A"
1.1160 +using assms(1)
1.1161 +proof (induct A rule: measure_induct_rule[where f=card])
1.1162 +  case (less A)
1.1163 +  show ?case
1.1164 +  proof(rule assms(2)[OF less(2)])
1.1165 +    fix B assume "finite B" "B \<subset> A"
1.1166 +    show "P B" by(rule less(1)[OF psubset_card_mono[OF less(2) `B \<subset> A`] `finite B`])
1.1167 +  qed
1.1168 +qed
1.1169 +
1.1170 +text{* main cardinality theorem *}
1.1171 +lemma card_partition [rule_format]:
1.1172 +  "finite C ==>
1.1173 +     finite (\<Union> C) -->
1.1174 +     (\<forall>c\<in>C. card c = k) -->
1.1175 +     (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->
1.1176 +     k * card(C) = card (\<Union> C)"
1.1177 +apply (erule finite_induct, simp)
1.1178 +apply (simp add: card_Un_disjoint insert_partition
1.1179 +       finite_subset [of _ "\<Union> (insert x F)"])
1.1180 +done
1.1181 +
1.1182 +lemma card_eq_UNIV_imp_eq_UNIV:
1.1183 +  assumes fin: "finite (UNIV :: 'a set)"
1.1184 +  and card: "card A = card (UNIV :: 'a set)"
1.1185 +  shows "A = (UNIV :: 'a set)"
1.1186 +proof
1.1187 +  show "A \<subseteq> UNIV" by simp
1.1188 +  show "UNIV \<subseteq> A"
1.1189 +  proof
1.1190 +    fix x
1.1191 +    show "x \<in> A"
1.1192 +    proof (rule ccontr)
1.1193 +      assume "x \<notin> A"
1.1194 +      then have "A \<subset> UNIV" by auto
1.1195 +      with fin have "card A < card (UNIV :: 'a set)" by (fact psubset_card_mono)
1.1196 +      with card show False by simp
1.1197 +    qed
1.1198 +  qed
1.1199 +qed
1.1200 +
1.1201 +text{*The form of a finite set of given cardinality*}
1.1202 +
1.1203 +lemma card_eq_SucD:
1.1204 +assumes "card A = Suc k"
1.1205 +shows "\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={})"
1.1206 +proof -
1.1207 +  have fin: "finite A" using assms by (auto intro: ccontr)
1.1208 +  moreover have "card A \<noteq> 0" using assms by auto
1.1209 +  ultimately obtain b where b: "b \<in> A" by auto
1.1210 +  show ?thesis
1.1211 +  proof (intro exI conjI)
1.1212 +    show "A = insert b (A-{b})" using b by blast
1.1213 +    show "b \<notin> A - {b}" by blast
1.1214 +    show "card (A - {b}) = k" and "k = 0 \<longrightarrow> A - {b} = {}"
1.1215 +      using assms b fin by(fastsimp dest:mk_disjoint_insert)+
1.1216 +  qed
1.1217 +qed
1.1218 +
1.1219 +lemma card_Suc_eq:
1.1220 +  "(card A = Suc k) =
1.1221 +   (\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={}))"
1.1222 +apply(rule iffI)
1.1223 + apply(erule card_eq_SucD)
1.1224 +apply(auto)
1.1225 +apply(subst card_insert)
1.1226 + apply(auto intro:ccontr)
1.1227 +done
1.1228 +
1.1229 +lemma finite_fun_UNIVD2:
1.1230 +  assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
1.1231 +  shows "finite (UNIV :: 'b set)"
1.1232 +proof -
1.1233 +  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))"
1.1234 +    by(rule finite_imageI)
1.1235 +  moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary)"
1.1236 +    by(rule UNIV_eq_I) auto
1.1237 +  ultimately show "finite (UNIV :: 'b set)" by simp
1.1238 +qed
1.1239 +
1.1240 +lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
1.1241 +apply (cases "finite A")
1.1242 +apply (erule finite_induct)
1.1243 +apply (auto simp add: algebra_simps)
1.1244 +done
1.1245 +
1.1246 +lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
1.1247 +apply (erule finite_induct)
1.1248 +apply auto
1.1249 +done
1.1250 +
1.1251 +lemma setprod_gen_delta:
1.1252 +  assumes fS: "finite S"
1.1253 +  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)"
1.1254 +proof-
1.1255 +  let ?f = "(\<lambda>k. if k=a then b k else c)"
1.1256 +  {assume a: "a \<notin> S"
1.1257 +    hence "\<forall> k\<in> S. ?f k = c" by simp
1.1258 +    hence ?thesis  using a setprod_constant[OF fS, of c] by (simp add: setprod_1 cong add: setprod_cong) }
1.1259 +  moreover
1.1260 +  {assume a: "a \<in> S"
1.1261 +    let ?A = "S - {a}"
1.1262 +    let ?B = "{a}"
1.1263 +    have eq: "S = ?A \<union> ?B" using a by blast
1.1264 +    have dj: "?A \<inter> ?B = {}" by simp
1.1265 +    from fS have fAB: "finite ?A" "finite ?B" by auto
1.1266 +    have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
1.1267 +      apply (rule setprod_cong) by auto
1.1268 +    have cA: "card ?A = card S - 1" using fS a by auto
1.1269 +    have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
1.1270 +    have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
1.1271 +      using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
1.1272 +      by simp
1.1273 +    then have ?thesis using a cA
1.1274 +      by (simp add: fA1 ring_simps cong add: setprod_cong cong del: if_weak_cong)}
1.1275 +  ultimately show ?thesis by blast
1.1276 +qed
1.1277 +
1.1278 +
1.1279 +lemma setsum_bounded:
1.1280 +  assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
1.1281 +  shows "setsum f A \<le> of_nat(card A) * K"
1.1282 +proof (cases "finite A")
1.1283 +  case True
1.1284 +  thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
1.1285 +next
1.1286 +  case False thus ?thesis by (simp add: setsum_def)
1.1287 +qed
1.1288 +
1.1289 +
1.1290 +lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
1.1291 +  unfolding UNIV_unit by simp
1.1292 +
1.1293 +
1.1294 +subsubsection {* Cardinality of unions *}
1.1295 +
1.1296 +lemma card_UN_disjoint:
1.1297 +  "finite I ==> (ALL i:I. finite (A i)) ==>
1.1298 +   (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {})
1.1299 +   ==> card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
1.1300 +apply (simp add: card_def del: setsum_constant)
1.1301 +apply (subgoal_tac
1.1302 +         "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
1.1303 +apply (simp add: setsum_UN_disjoint del: setsum_constant)
1.1304 +apply (simp cong: setsum_cong)
1.1305 +done
1.1306 +
1.1307 +lemma card_Union_disjoint:
1.1308 +  "finite C ==> (ALL A:C. finite A) ==>
1.1309 +   (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
1.1310 +   ==> card (Union C) = setsum card C"
1.1311 +apply (frule card_UN_disjoint [of C id])
1.1312 +apply (unfold Union_def id_def, assumption+)
1.1313 +done
1.1314 +
1.1315 +
1.1316 +subsubsection {* Cardinality of image *}
1.1317 +
1.1318 +text{*The image of a finite set can be expressed using @{term fold_image}.*}
1.1319 +lemma image_eq_fold_image:
1.1320 +  "finite A ==> f ` A = fold_image (op Un) (%x. {f x}) {} A"
1.1321 +proof (induct rule: finite_induct)
1.1322 +  case empty then show ?case by simp
1.1323 +next
1.1324 +  interpret ab_semigroup_mult "op Un"
1.1325 +    proof qed auto
1.1326 +  case insert
1.1327 +  then show ?case by simp
1.1328 +qed
1.1329 +
1.1330 +lemma card_image_le: "finite A ==> card (f ` A) <= card A"
1.1331 +apply (induct set: finite)
1.1332 + apply simp
1.1333 +apply (simp add: le_SucI card_insert_if)
1.1334 +done
1.1335 +
1.1336 +lemma card_image: "inj_on f A ==> card (f ` A) = card A"
1.1337 +by(simp add:card_def setsum_reindex o_def del:setsum_constant)
1.1338 +
1.1339 +lemma bij_betw_same_card: "bij_betw f A B \<Longrightarrow> card A = card B"
1.1340 +by(auto simp: card_image bij_betw_def)
1.1341 +
1.1342 +lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
1.1343 +by (simp add: card_seteq card_image)
1.1344 +
1.1345 +lemma eq_card_imp_inj_on:
1.1346 +  "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
1.1347 +apply (induct rule:finite_induct)
1.1348 +apply simp
1.1349 +apply(frule card_image_le[where f = f])
1.1351 +done
1.1352 +
1.1353 +lemma inj_on_iff_eq_card:
1.1354 +  "finite A ==> inj_on f A = (card(f ` A) = card A)"
1.1355 +by(blast intro: card_image eq_card_imp_inj_on)
1.1356 +
1.1357 +
1.1358 +lemma card_inj_on_le:
1.1359 +  "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
1.1360 +apply (subgoal_tac "finite A")
1.1361 + apply (force intro: card_mono simp add: card_image [symmetric])
1.1362 +apply (blast intro: finite_imageD dest: finite_subset)
1.1363 +done
1.1364 +
1.1365 +lemma card_bij_eq:
1.1366 +  "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
1.1367 +     finite A; finite B |] ==> card A = card B"
1.1368 +by (auto intro: le_antisym card_inj_on_le)
1.1369 +
1.1370 +
1.1371 +subsubsection {* Cardinality of products *}
1.1372 +
1.1373 +(*
1.1374 +lemma SigmaI_insert: "y \<notin> A ==>
1.1375 +  (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
1.1376 +  by auto
1.1377 +*)
1.1378 +
1.1379 +lemma card_SigmaI [simp]:
1.1380 +  "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
1.1381 +  \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
1.1383 +
1.1384 +lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
1.1385 +apply (cases "finite A")
1.1386 +apply (cases "finite B")
1.1387 +apply (auto simp add: card_eq_0_iff
1.1388 +            dest: finite_cartesian_productD1 finite_cartesian_productD2)
1.1389 +done
1.1390 +
1.1391 +lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
1.1393 +
1.1394 +
1.1395 +subsubsection {* Cardinality of sums *}
1.1396 +
1.1397 +lemma card_Plus:
1.1398 +  assumes "finite A" and "finite B"
1.1399 +  shows "card (A <+> B) = card A + card B"
1.1400 +proof -
1.1401 +  have "Inl`A \<inter> Inr`B = {}" by fast
1.1402 +  with assms show ?thesis
1.1403 +    unfolding Plus_def
1.1404 +    by (simp add: card_Un_disjoint card_image)
1.1405 +qed
1.1406 +
1.1407 +lemma card_Plus_conv_if:
1.1408 +  "card (A <+> B) = (if finite A \<and> finite B then card(A) + card(B) else 0)"
1.1409 +by(auto simp: card_def setsum_Plus simp del: setsum_constant)
1.1410 +
1.1411 +
1.1412 +subsubsection {* Cardinality of the Powerset *}
1.1413 +
1.1414 +lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
1.1415 +apply (induct set: finite)
1.1416 + apply (simp_all add: Pow_insert)
1.1417 +apply (subst card_Un_disjoint, blast)
1.1418 +  apply (blast intro: finite_imageI, blast)
1.1419 +apply (subgoal_tac "inj_on (insert x) (Pow F)")
1.1420 + apply (simp add: card_image Pow_insert)
1.1421 +apply (unfold inj_on_def)
1.1422 +apply (blast elim!: equalityE)
1.1423 +done
1.1424 +
1.1425 +text {* Relates to equivalence classes.  Based on a theorem of F. Kammüller.  *}
1.1426 +
1.1427 +lemma dvd_partition:
1.1428 +  "finite (Union C) ==>
1.1429 +    ALL c : C. k dvd card c ==>
1.1430 +    (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
1.1431 +  k dvd card (Union C)"
1.1432 +apply(frule finite_UnionD)
1.1433 +apply(rotate_tac -1)
1.1434 +apply (induct set: finite, simp_all, clarify)
1.1435 +apply (subst card_Un_disjoint)
1.1436 +   apply (auto simp add: disjoint_eq_subset_Compl)
1.1437 +done
1.1438 +
1.1439 +
1.1440 +subsubsection {* Relating injectivity and surjectivity *}
1.1441 +
1.1442 +lemma finite_surj_inj: "finite(A) \<Longrightarrow> A <= f`A \<Longrightarrow> inj_on f A"
1.1443 +apply(rule eq_card_imp_inj_on, assumption)
1.1444 +apply(frule finite_imageI)
1.1445 +apply(drule (1) card_seteq)
1.1446 + apply(erule card_image_le)
1.1447 +apply simp
1.1448 +done
1.1449 +
1.1450 +lemma finite_UNIV_surj_inj: fixes f :: "'a \<Rightarrow> 'a"
1.1451 +shows "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
1.1452 +by (blast intro: finite_surj_inj subset_UNIV dest:surj_range)
1.1453 +
1.1454 +lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a"
1.1455 +shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
1.1456 +by(fastsimp simp:surj_def dest!: endo_inj_surj)
1.1457 +
1.1458 +corollary infinite_UNIV_nat[iff]: "~finite(UNIV::nat set)"
1.1459 +proof
1.1460 +  assume "finite(UNIV::nat set)"
1.1461 +  with finite_UNIV_inj_surj[of Suc]
1.1462 +  show False by simp (blast dest: Suc_neq_Zero surjD)
1.1463 +qed
1.1464 +
1.1465 +(* Often leads to bogus ATP proofs because of reduced type information, hence noatp *)
1.1466 +lemma infinite_UNIV_char_0[noatp]:
1.1467 +  "\<not> finite (UNIV::'a::semiring_char_0 set)"
1.1468 +proof
1.1469 +  assume "finite (UNIV::'a set)"
1.1470 +  with subset_UNIV have "finite (range of_nat::'a set)"
1.1471 +    by (rule finite_subset)
1.1472 +  moreover have "inj (of_nat::nat \<Rightarrow> 'a)"
1.1473 +    by (simp add: inj_on_def)
1.1474 +  ultimately have "finite (UNIV::nat set)"
1.1475 +    by (rule finite_imageD)
1.1476 +  then show "False"
1.1477 +    by simp
1.1478 +qed
1.1479 +
1.1480 +subsubsection {* Fold1 in lattices with @{const inf} and @{const sup} *}
1.1481 +
1.1482 +text{*
1.1483 +  As an application of @{text fold1} we define infimum
1.1484 +  and supremum in (not necessarily complete!) lattices
1.1485 +  over (non-empty) sets by means of @{text fold1}.
1.1486 +*}
1.1487 +
1.1488 +context semilattice_inf
1.1489 +begin
1.1490 +
1.1491 +lemma below_fold1_iff:
1.1492 +  assumes "finite A" "A \<noteq> {}"
1.1493 +  shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
1.1494 +proof -
1.1495 +  interpret ab_semigroup_idem_mult inf
1.1496 +    by (rule ab_semigroup_idem_mult_inf)
1.1497 +  show ?thesis using assms by (induct rule: finite_ne_induct) simp_all
1.1498 +qed
1.1499 +
1.1500 +lemma fold1_belowI:
1.1501 +  assumes "finite A"
1.1502 +    and "a \<in> A"
1.1503 +  shows "fold1 inf A \<le> a"
1.1504 +proof -
1.1505 +  from assms have "A \<noteq> {}" by auto
1.1506 +  from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
1.1507 +  proof (induct rule: finite_ne_induct)
1.1508 +    case singleton thus ?case by simp
1.1509 +  next
1.1510 +    interpret ab_semigroup_idem_mult inf
1.1511 +      by (rule ab_semigroup_idem_mult_inf)
1.1512 +    case (insert x F)
1.1513 +    from insert(5) have "a = x \<or> a \<in> F" by simp
1.1514 +    thus ?case
1.1515 +    proof
1.1516 +      assume "a = x" thus ?thesis using insert
1.1517 +        by (simp add: mult_ac)
1.1518 +    next
1.1519 +      assume "a \<in> F"
1.1520 +      hence bel: "fold1 inf F \<le> a" by (rule insert)
1.1521 +      have "inf (fold1 inf (insert x F)) a = inf x (inf (fold1 inf F) a)"
1.1522 +        using insert by (simp add: mult_ac)
1.1523 +      also have "inf (fold1 inf F) a = fold1 inf F"
1.1524 +        using bel by (auto intro: antisym)
1.1525 +      also have "inf x \<dots> = fold1 inf (insert x F)"
1.1526 +        using insert by (simp add: mult_ac)
1.1527 +      finally have aux: "inf (fold1 inf (insert x F)) a = fold1 inf (insert x F)" .
1.1528 +      moreover have "inf (fold1 inf (insert x F)) a \<le> a" by simp
1.1529 +      ultimately show ?thesis by simp
1.1530 +    qed
1.1531 +  qed
1.1532 +qed
1.1533 +
1.1534 +end
1.1535 +
1.1536 +context lattice
1.1537 +begin
1.1538 +
1.1539 +definition
1.1540 +  Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900)
1.1541 +where
1.1542 +  "Inf_fin = fold1 inf"
1.1543 +
1.1544 +definition
1.1545 +  Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900)
1.1546 +where
1.1547 +  "Sup_fin = fold1 sup"
1.1548 +
1.1549 +lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A"
1.1550 +apply(unfold Sup_fin_def Inf_fin_def)
1.1551 +apply(subgoal_tac "EX a. a:A")
1.1552 +prefer 2 apply blast
1.1553 +apply(erule exE)
1.1554 +apply(rule order_trans)
1.1555 +apply(erule (1) fold1_belowI)
1.1556 +apply(erule (1) semilattice_inf.fold1_belowI [OF dual_semilattice])
1.1557 +done
1.1558 +
1.1559 +lemma sup_Inf_absorb [simp]:
1.1560 +  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^bsub>fin\<^esub>A) = a"
1.1561 +apply(subst sup_commute)
1.1562 +apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI)
1.1563 +done
1.1564 +
1.1565 +lemma inf_Sup_absorb [simp]:
1.1566 +  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a"
1.1567 +by (simp add: Sup_fin_def inf_absorb1
1.1568 +  semilattice_inf.fold1_belowI [OF dual_semilattice])
1.1569 +
1.1570 +end
1.1571 +
1.1572 +context distrib_lattice
1.1573 +begin
1.1574 +
1.1575 +lemma sup_Inf1_distrib:
1.1576 +  assumes "finite A"
1.1577 +    and "A \<noteq> {}"
1.1578 +  shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
1.1579 +proof -
1.1580 +  interpret ab_semigroup_idem_mult inf
1.1581 +    by (rule ab_semigroup_idem_mult_inf)
1.1582 +  from assms show ?thesis
1.1583 +    by (simp add: Inf_fin_def image_def
1.1584 +      hom_fold1_commute [where h="sup x", OF sup_inf_distrib1])
1.1585 +        (rule arg_cong [where f="fold1 inf"], blast)
1.1586 +qed
1.1587 +
1.1588 +lemma sup_Inf2_distrib:
1.1589 +  assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
1.1590 +  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}"
1.1591 +using A proof (induct rule: finite_ne_induct)
1.1592 +  case singleton thus ?case
1.1593 +    by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
1.1594 +next
1.1595 +  interpret ab_semigroup_idem_mult inf
1.1596 +    by (rule ab_semigroup_idem_mult_inf)
1.1597 +  case (insert x A)
1.1598 +  have finB: "finite {sup x b |b. b \<in> B}"
1.1599 +    by(rule finite_surj[where f = "sup x", OF B(1)], auto)
1.1600 +  have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
1.1601 +  proof -
1.1602 +    have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
1.1603 +      by blast
1.1604 +    thus ?thesis by(simp add: insert(1) B(1))
1.1605 +  qed
1.1606 +  have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
1.1607 +  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)"
1.1608 +    using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def])
1.1609 +  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)
1.1610 +  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})"
1.1611 +    using insert by(simp add:sup_Inf1_distrib[OF B])
1.1612 +  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})"
1.1613 +    (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M")
1.1614 +    using B insert
1.1615 +    by (simp add: Inf_fin_def fold1_Un2 [OF finB _ finAB ne])
1.1616 +  also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
1.1617 +    by blast
1.1618 +  finally show ?case .
1.1619 +qed
1.1620 +
1.1621 +lemma inf_Sup1_distrib:
1.1622 +  assumes "finite A" and "A \<noteq> {}"
1.1623 +  shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
1.1624 +proof -
1.1625 +  interpret ab_semigroup_idem_mult sup
1.1626 +    by (rule ab_semigroup_idem_mult_sup)
1.1627 +  from assms show ?thesis
1.1628 +    by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1])
1.1629 +      (rule arg_cong [where f="fold1 sup"], blast)
1.1630 +qed
1.1631 +
1.1632 +lemma inf_Sup2_distrib:
1.1633 +  assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
1.1634 +  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}"
1.1635 +using A proof (induct rule: finite_ne_induct)
1.1636 +  case singleton thus ?case
1.1637 +    by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def])
1.1638 +next
1.1639 +  case (insert x A)
1.1640 +  have finB: "finite {inf x b |b. b \<in> B}"
1.1641 +    by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
1.1642 +  have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
1.1643 +  proof -
1.1644 +    have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
1.1645 +      by blast
1.1646 +    thus ?thesis by(simp add: insert(1) B(1))
1.1647 +  qed
1.1648 +  have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
1.1649 +  interpret ab_semigroup_idem_mult sup
1.1650 +    by (rule ab_semigroup_idem_mult_sup)
1.1651 +  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)"
1.1652 +    using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
1.1653 +  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)
1.1654 +  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})"
1.1655 +    using insert by(simp add:inf_Sup1_distrib[OF B])
1.1656 +  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})"
1.1657 +    (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M")
1.1658 +    using B insert
1.1659 +    by (simp add: Sup_fin_def fold1_Un2 [OF finB _ finAB ne])
1.1660 +  also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
1.1661 +    by blast
1.1662 +  finally show ?case .
1.1663 +qed
1.1664 +
1.1665 +end
1.1666 +
1.1667 +context complete_lattice
1.1668 +begin
1.1669 +
1.1670 +lemma Inf_fin_Inf:
1.1671 +  assumes "finite A" and "A \<noteq> {}"
1.1672 +  shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
1.1673 +proof -
1.1674 +  interpret ab_semigroup_idem_mult inf
1.1675 +    by (rule ab_semigroup_idem_mult_inf)
1.1676 +  from `A \<noteq> {}` obtain b B where "A = insert b B" by auto
1.1677 +  moreover with `finite A` have "finite B" by simp
1.1678 +  ultimately show ?thesis
1.1679 +  by (simp add: Inf_fin_def fold1_eq_fold_idem inf_Inf_fold_inf [symmetric])
1.1681 +qed
1.1682 +
1.1683 +lemma Sup_fin_Sup:
1.1684 +  assumes "finite A" and "A \<noteq> {}"
1.1685 +  shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
1.1686 +proof -
1.1687 +  interpret ab_semigroup_idem_mult sup
1.1688 +    by (rule ab_semigroup_idem_mult_sup)
1.1689 +  from `A \<noteq> {}` obtain b B where "A = insert b B" by auto
1.1690 +  moreover with `finite A` have "finite B" by simp
1.1691 +  ultimately show ?thesis
1.1692 +  by (simp add: Sup_fin_def fold1_eq_fold_idem sup_Sup_fold_sup [symmetric])
1.1694 +qed
1.1695 +
1.1696 +end
1.1697 +
1.1698 +
1.1699 +subsubsection {* Fold1 in linear orders with @{const min} and @{const max} *}
1.1700 +
1.1701 +text{*
1.1702 +  As an application of @{text fold1} we define minimum
1.1703 +  and maximum in (not necessarily complete!) linear orders
1.1704 +  over (non-empty) sets by means of @{text fold1}.
1.1705 +*}
1.1706 +
1.1707 +context linorder
1.1708 +begin
1.1709 +
1.1710 +lemma ab_semigroup_idem_mult_min:
1.1711 +  "ab_semigroup_idem_mult min"
1.1712 +  proof qed (auto simp add: min_def)
1.1713 +
1.1714 +lemma ab_semigroup_idem_mult_max:
1.1715 +  "ab_semigroup_idem_mult max"
1.1716 +  proof qed (auto simp add: max_def)
1.1717 +
1.1718 +lemma max_lattice:
1.1719 +  "semilattice_inf (op \<ge>) (op >) max"
1.1720 +  by (fact min_max.dual_semilattice)
1.1721 +
1.1722 +lemma dual_max:
1.1723 +  "ord.max (op \<ge>) = min"
1.1724 +  by (auto simp add: ord.max_def_raw min_def expand_fun_eq)
1.1725 +
1.1726 +lemma dual_min:
1.1727 +  "ord.min (op \<ge>) = max"
1.1728 +  by (auto simp add: ord.min_def_raw max_def expand_fun_eq)
1.1729 +
1.1730 +lemma strict_below_fold1_iff:
1.1731 +  assumes "finite A" and "A \<noteq> {}"
1.1732 +  shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
1.1733 +proof -
1.1734 +  interpret ab_semigroup_idem_mult min
1.1735 +    by (rule ab_semigroup_idem_mult_min)
1.1736 +  from assms show ?thesis
1.1737 +  by (induct rule: finite_ne_induct)
1.1739 +qed
1.1740 +
1.1741 +lemma fold1_below_iff:
1.1742 +  assumes "finite A" and "A \<noteq> {}"
1.1743 +  shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
1.1744 +proof -
1.1745 +  interpret ab_semigroup_idem_mult min
1.1746 +    by (rule ab_semigroup_idem_mult_min)
1.1747 +  from assms show ?thesis
1.1748 +  by (induct rule: finite_ne_induct)
1.1749 +    (simp_all add: fold1_insert min_le_iff_disj)
1.1750 +qed
1.1751 +
1.1752 +lemma fold1_strict_below_iff:
1.1753 +  assumes "finite A" and "A \<noteq> {}"
1.1754 +  shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
1.1755 +proof -
1.1756 +  interpret ab_semigroup_idem_mult min
1.1757 +    by (rule ab_semigroup_idem_mult_min)
1.1758 +  from assms show ?thesis
1.1759 +  by (induct rule: finite_ne_induct)
1.1760 +    (simp_all add: fold1_insert min_less_iff_disj)
1.1761 +qed
1.1762 +
1.1763 +lemma fold1_antimono:
1.1764 +  assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
1.1765 +  shows "fold1 min B \<le> fold1 min A"
1.1766 +proof cases
1.1767 +  assume "A = B" thus ?thesis by simp
1.1768 +next
1.1769 +  interpret ab_semigroup_idem_mult min
1.1770 +    by (rule ab_semigroup_idem_mult_min)
1.1771 +  assume "A \<noteq> B"
1.1772 +  have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
1.1773 +  have "fold1 min B = fold1 min (A \<union> (B-A))" by(subst B)(rule refl)
1.1774 +  also have "\<dots> = min (fold1 min A) (fold1 min (B-A))"
1.1775 +  proof -
1.1776 +    have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
1.1777 +    moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`]) (* by(blast intro:finite_Diff prems) fails *)
1.1778 +    moreover have "(B-A) \<noteq> {}" using prems by blast
1.1779 +    moreover have "A Int (B-A) = {}" using prems by blast
1.1780 +    ultimately show ?thesis using `A \<noteq> {}` by (rule_tac fold1_Un)
1.1781 +  qed
1.1782 +  also have "\<dots> \<le> fold1 min A" by (simp add: min_le_iff_disj)
1.1783 +  finally show ?thesis .
1.1784 +qed
1.1785 +
1.1786 +definition
1.1787 +  Min :: "'a set \<Rightarrow> 'a"
1.1788 +where
1.1789 +  "Min = fold1 min"
1.1790 +
1.1791 +definition
1.1792 +  Max :: "'a set \<Rightarrow> 'a"
1.1793 +where
1.1794 +  "Max = fold1 max"
1.1795 +
1.1796 +lemmas Min_singleton [simp] = fold1_singleton_def [OF Min_def]
1.1797 +lemmas Max_singleton [simp] = fold1_singleton_def [OF Max_def]
1.1798 +
1.1799 +lemma Min_insert [simp]:
1.1800 +  assumes "finite A" and "A \<noteq> {}"
1.1801 +  shows "Min (insert x A) = min x (Min A)"
1.1802 +proof -
1.1803 +  interpret ab_semigroup_idem_mult min
1.1804 +    by (rule ab_semigroup_idem_mult_min)
1.1805 +  from assms show ?thesis by (rule fold1_insert_idem_def [OF Min_def])
1.1806 +qed
1.1807 +
1.1808 +lemma Max_insert [simp]:
1.1809 +  assumes "finite A" and "A \<noteq> {}"
1.1810 +  shows "Max (insert x A) = max x (Max A)"
1.1811 +proof -
1.1812 +  interpret ab_semigroup_idem_mult max
1.1813 +    by (rule ab_semigroup_idem_mult_max)
1.1814 +  from assms show ?thesis by (rule fold1_insert_idem_def [OF Max_def])
1.1815 +qed
1.1816 +
1.1817 +lemma Min_in [simp]:
1.1818 +  assumes "finite A" and "A \<noteq> {}"
1.1819 +  shows "Min A \<in> A"
1.1820 +proof -
1.1821 +  interpret ab_semigroup_idem_mult min
1.1822 +    by (rule ab_semigroup_idem_mult_min)
1.1823 +  from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def)
1.1824 +qed
1.1825 +
1.1826 +lemma Max_in [simp]:
1.1827 +  assumes "finite A" and "A \<noteq> {}"
1.1828 +  shows "Max A \<in> A"
1.1829 +proof -
1.1830 +  interpret ab_semigroup_idem_mult max
1.1831 +    by (rule ab_semigroup_idem_mult_max)
1.1832 +  from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
1.1833 +qed
1.1834 +
1.1835 +lemma Min_Un:
1.1836 +  assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
1.1837 +  shows "Min (A \<union> B) = min (Min A) (Min B)"
1.1838 +proof -
1.1839 +  interpret ab_semigroup_idem_mult min
1.1840 +    by (rule ab_semigroup_idem_mult_min)
1.1841 +  from assms show ?thesis
1.1842 +    by (simp add: Min_def fold1_Un2)
1.1843 +qed
1.1844 +
1.1845 +lemma Max_Un:
1.1846 +  assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
1.1847 +  shows "Max (A \<union> B) = max (Max A) (Max B)"
1.1848 +proof -
1.1849 +  interpret ab_semigroup_idem_mult max
1.1850 +    by (rule ab_semigroup_idem_mult_max)
1.1851 +  from assms show ?thesis
1.1852 +    by (simp add: Max_def fold1_Un2)
1.1853 +qed
1.1854 +
1.1855 +lemma hom_Min_commute:
1.1856 +  assumes "\<And>x y. h (min x y) = min (h x) (h y)"
1.1857 +    and "finite N" and "N \<noteq> {}"
1.1858 +  shows "h (Min N) = Min (h ` N)"
1.1859 +proof -
1.1860 +  interpret ab_semigroup_idem_mult min
1.1861 +    by (rule ab_semigroup_idem_mult_min)
1.1862 +  from assms show ?thesis
1.1863 +    by (simp add: Min_def hom_fold1_commute)
1.1864 +qed
1.1865 +
1.1866 +lemma hom_Max_commute:
1.1867 +  assumes "\<And>x y. h (max x y) = max (h x) (h y)"
1.1868 +    and "finite N" and "N \<noteq> {}"
1.1869 +  shows "h (Max N) = Max (h ` N)"
1.1870 +proof -
1.1871 +  interpret ab_semigroup_idem_mult max
1.1872 +    by (rule ab_semigroup_idem_mult_max)
1.1873 +  from assms show ?thesis
1.1874 +    by (simp add: Max_def hom_fold1_commute [of h])
1.1875 +qed
1.1876 +
1.1877 +lemma Min_le [simp]:
1.1878 +  assumes "finite A" and "x \<in> A"
1.1879 +  shows "Min A \<le> x"
1.1880 +  using assms by (simp add: Min_def min_max.fold1_belowI)
1.1881 +
1.1882 +lemma Max_ge [simp]:
1.1883 +  assumes "finite A" and "x \<in> A"
1.1884 +  shows "x \<le> Max A"
1.1885 +proof -
1.1886 +  interpret semilattice_inf "op \<ge>" "op >" max
1.1887 +    by (rule max_lattice)
1.1888 +  from assms show ?thesis by (simp add: Max_def fold1_belowI)
1.1889 +qed
1.1890 +
1.1891 +lemma Min_ge_iff [simp, noatp]:
1.1892 +  assumes "finite A" and "A \<noteq> {}"
1.1893 +  shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
1.1894 +  using assms by (simp add: Min_def min_max.below_fold1_iff)
1.1895 +
1.1896 +lemma Max_le_iff [simp, noatp]:
1.1897 +  assumes "finite A" and "A \<noteq> {}"
1.1898 +  shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
1.1899 +proof -
1.1900 +  interpret semilattice_inf "op \<ge>" "op >" max
1.1901 +    by (rule max_lattice)
1.1902 +  from assms show ?thesis by (simp add: Max_def below_fold1_iff)
1.1903 +qed
1.1904 +
1.1905 +lemma Min_gr_iff [simp, noatp]:
1.1906 +  assumes "finite A" and "A \<noteq> {}"
1.1907 +  shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
1.1908 +  using assms by (simp add: Min_def strict_below_fold1_iff)
1.1909 +
1.1910 +lemma Max_less_iff [simp, noatp]:
1.1911 +  assumes "finite A" and "A \<noteq> {}"
1.1912 +  shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
1.1913 +proof -
1.1914 +  interpret dual: linorder "op \<ge>" "op >"
1.1915 +    by (rule dual_linorder)
1.1916 +  from assms show ?thesis
1.1917 +    by (simp add: Max_def dual.strict_below_fold1_iff [folded dual.dual_max])
1.1918 +qed
1.1919 +
1.1920 +lemma Min_le_iff [noatp]:
1.1921 +  assumes "finite A" and "A \<noteq> {}"
1.1922 +  shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
1.1923 +  using assms by (simp add: Min_def fold1_below_iff)
1.1924 +
1.1925 +lemma Max_ge_iff [noatp]:
1.1926 +  assumes "finite A" and "A \<noteq> {}"
1.1927 +  shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
1.1928 +proof -
1.1929 +  interpret dual: linorder "op \<ge>" "op >"
1.1930 +    by (rule dual_linorder)
1.1931 +  from assms show ?thesis
1.1932 +    by (simp add: Max_def dual.fold1_below_iff [folded dual.dual_max])
1.1933 +qed
1.1934 +
1.1935 +lemma Min_less_iff [noatp]:
1.1936 +  assumes "finite A" and "A \<noteq> {}"
1.1937 +  shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
1.1938 +  using assms by (simp add: Min_def fold1_strict_below_iff)
1.1939 +
1.1940 +lemma Max_gr_iff [noatp]:
1.1941 +  assumes "finite A" and "A \<noteq> {}"
1.1942 +  shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
1.1943 +proof -
1.1944 +  interpret dual: linorder "op \<ge>" "op >"
1.1945 +    by (rule dual_linorder)
1.1946 +  from assms show ?thesis
1.1947 +    by (simp add: Max_def dual.fold1_strict_below_iff [folded dual.dual_max])
1.1948 +qed
1.1949 +
1.1950 +lemma Min_eqI:
1.1951 +  assumes "finite A"
1.1952 +  assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
1.1953 +    and "x \<in> A"
1.1954 +  shows "Min A = x"
1.1955 +proof (rule antisym)
1.1956 +  from `x \<in> A` have "A \<noteq> {}" by auto
1.1957 +  with assms show "Min A \<ge> x" by simp
1.1958 +next
1.1959 +  from assms show "x \<ge> Min A" by simp
1.1960 +qed
1.1961 +
1.1962 +lemma Max_eqI:
1.1963 +  assumes "finite A"
1.1964 +  assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
1.1965 +    and "x \<in> A"
1.1966 +  shows "Max A = x"
1.1967 +proof (rule antisym)
1.1968 +  from `x \<in> A` have "A \<noteq> {}" by auto
1.1969 +  with assms show "Max A \<le> x" by simp
1.1970 +next
1.1971 +  from assms show "x \<le> Max A" by simp
1.1972 +qed
1.1973 +
1.1974 +lemma Min_antimono:
1.1975 +  assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
1.1976 +  shows "Min N \<le> Min M"
1.1977 +  using assms by (simp add: Min_def fold1_antimono)
1.1978 +
1.1979 +lemma Max_mono:
1.1980 +  assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
1.1981 +  shows "Max M \<le> Max N"
1.1982 +proof -
1.1983 +  interpret dual: linorder "op \<ge>" "op >"
1.1984 +    by (rule dual_linorder)
1.1985 +  from assms show ?thesis
1.1986 +    by (simp add: Max_def dual.fold1_antimono [folded dual.dual_max])
1.1987 +qed
1.1988 +
1.1989 +lemma finite_linorder_max_induct[consumes 1, case_names empty insert]:
1.1990 + "finite A \<Longrightarrow> P {} \<Longrightarrow>
1.1991 +  (!!b A. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
1.1992 +  \<Longrightarrow> P A"
1.1993 +proof (induct rule: finite_psubset_induct)
1.1994 +  fix A :: "'a set"
1.1995 +  assume IH: "!! B. finite B \<Longrightarrow> B < A \<Longrightarrow> P {} \<Longrightarrow>
1.1996 +                 (!!b A. finite A \<Longrightarrow> (\<forall>a\<in>A. a<b) \<Longrightarrow> P A \<Longrightarrow> P (insert b A))
1.1997 +                  \<Longrightarrow> P B"
1.1998 +  and "finite A" and "P {}"
1.1999 +  and step: "!!b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
1.2000 +  show "P A"
1.2001 +  proof (cases "A = {}")
1.2002 +    assume "A = {}" thus "P A" using `P {}` by simp
1.2003 +  next
1.2004 +    let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B"
1.2005 +    assume "A \<noteq> {}"
1.2006 +    with `finite A` have "Max A : A" by auto
1.2007 +    hence A: "?A = A" using insert_Diff_single insert_absorb by auto
1.2008 +    moreover have "finite ?B" using `finite A` by simp
1.2009 +    ultimately have "P ?B" using `P {}` step IH[of ?B] by blast
1.2010 +    moreover have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastsimp
1.2011 +    ultimately show "P A" using A insert_Diff_single step[OF `finite ?B`] by fastsimp
1.2012 +  qed
1.2013 +qed
1.2014 +
1.2015 +lemma finite_linorder_min_induct[consumes 1, case_names empty insert]:
1.2016 + "\<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"
1.2017 +by(rule linorder.finite_linorder_max_induct[OF dual_linorder])
1.2018 +
1.2019 +end
1.2020 +
1.2022 +begin
1.2023 +
1.2025 +  fixes k
1.2026 +  assumes "finite N" and "N \<noteq> {}"
1.2027 +  shows "k + Min N = Min {k + m | m. m \<in> N}"
1.2028 +proof -
1.2029 +  have "\<And>x y. k + min x y = min (k + x) (k + y)"
1.2030 +    by (simp add: min_def not_le)
1.2031 +      (blast intro: antisym less_imp_le add_left_mono)
1.2032 +  with assms show ?thesis
1.2033 +    using hom_Min_commute [of "plus k" N]
1.2034 +    by simp (blast intro: arg_cong [where f = Min])
1.2035 +qed
1.2036 +
1.2038 +  fixes k
1.2039 +  assumes "finite N" and "N \<noteq> {}"
1.2040 +  shows "k + Max N = Max {k + m | m. m \<in> N}"
1.2041 +proof -
1.2042 +  have "\<And>x y. k + max x y = max (k + x) (k + y)"
1.2043 +    by (simp add: max_def not_le)
1.2044 +      (blast intro: antisym less_imp_le add_left_mono)
1.2045 +  with assms show ?thesis
1.2046 +    using hom_Max_commute [of "plus k" N]
1.2047 +    by simp (blast intro: arg_cong [where f = Max])
1.2048 +qed
1.2049 +
1.2050 +end
1.2051 +
1.2053 +begin
1.2054 +
1.2055 +lemma minus_Max_eq_Min [simp]:
1.2056 +  "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Max S) = Min (uminus ` S)"
1.2057 +  by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min)
1.2058 +
1.2059 +lemma minus_Min_eq_Max [simp]:
1.2060 +  "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Min S) = Max (uminus ` S)"
1.2061 +  by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max)
1.2062 +
1.2063 +end
1.2064 +
1.2065 +end
```
```     2.1 --- a/src/HOL/Finite_Set.thy	Wed Mar 10 08:04:50 2010 +0100
2.2 +++ b/src/HOL/Finite_Set.thy	Wed Mar 10 16:53:27 2010 +0100
2.3 @@ -6,7 +6,7 @@
2.4  header {* Finite sets *}
2.5
2.6  theory Finite_Set
2.7 -imports Power Product_Type Sum_Type
2.8 +imports Power Option
2.9  begin
2.10
2.11  subsection {* Definition and basic properties *}
2.12 @@ -527,17 +527,24 @@
2.13  lemma UNIV_unit [noatp]:
2.14    "UNIV = {()}" by auto
2.15
2.16 -instance unit :: finite
2.17 -  by default (simp add: UNIV_unit)
2.18 +instance unit :: finite proof
2.20
2.21  lemma UNIV_bool [noatp]:
2.22    "UNIV = {False, True}" by auto
2.23
2.24 -instance bool :: finite
2.25 -  by default (simp add: UNIV_bool)
2.26 +instance bool :: finite proof
2.28 +
2.29 +instance * :: (finite, finite) finite proof
2.30 +qed (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
2.31
2.32 -instance * :: (finite, finite) finite
2.33 -  by default (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
2.34 +lemma finite_option_UNIV [simp]:
2.35 +  "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
2.36 +  by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
2.37 +
2.38 +instance option :: (finite) finite proof
2.40
2.41  lemma inj_graph: "inj (%f. {(x, y). y = f x})"
2.42    by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
2.43 @@ -556,8 +563,8 @@
2.44    qed
2.45  qed
2.46
2.47 -instance "+" :: (finite, finite) finite
2.48 -  by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
2.49 +instance "+" :: (finite, finite) finite proof
2.50 +qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
2.51
2.52
2.53  subsection {* A fold functional for finite sets *}
2.54 @@ -1053,1470 +1060,6 @@
2.55
2.56  end
2.57
2.58 -subsection {* Generalized summation over a set *}
2.59 -
2.62 -
2.63 -definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
2.64 -where "setsum f A == if finite A then fold_image (op +) f 0 A else 0"
2.65 -
2.66 -abbreviation
2.67 -  Setsum  ("\<Sum>_" [1000] 999) where
2.68 -  "\<Sum>A == setsum (%x. x) A"
2.69 -
2.70 -text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
2.71 -written @{text"\<Sum>x\<in>A. e"}. *}
2.72 -
2.73 -syntax
2.74 -  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
2.75 -syntax (xsymbols)
2.76 -  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
2.77 -syntax (HTML output)
2.78 -  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
2.79 -
2.80 -translations -- {* Beware of argument permutation! *}
2.81 -  "SUM i:A. b" == "CONST setsum (%i. b) A"
2.82 -  "\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
2.83 -
2.84 -text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
2.85 - @{text"\<Sum>x|P. e"}. *}
2.86 -
2.87 -syntax
2.88 -  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
2.89 -syntax (xsymbols)
2.90 -  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
2.91 -syntax (HTML output)
2.92 -  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
2.93 -
2.94 -translations
2.95 -  "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
2.96 -  "\<Sum>x|P. t" => "CONST setsum (%x. t) {x. P}"
2.97 -
2.98 -print_translation {*
2.99 -let
2.100 -  fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) \$ Abs (y, Ty, P)] =
2.101 -        if x <> y then raise Match
2.102 -        else
2.103 -          let
2.104 -            val x' = Syntax.mark_bound x;
2.105 -            val t' = subst_bound (x', t);
2.106 -            val P' = subst_bound (x', P);
2.107 -          in Syntax.const @{syntax_const "_qsetsum"} \$ Syntax.mark_bound x \$ P' \$ t' end
2.108 -    | setsum_tr' _ = raise Match;
2.109 -in [(@{const_syntax setsum}, setsum_tr')] end
2.110 -*}
2.111 -
2.112 -
2.113 -lemma setsum_empty [simp]: "setsum f {} = 0"
2.115 -
2.116 -lemma setsum_insert [simp]:
2.117 -  "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
2.119 -
2.120 -lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0"
2.122 -
2.123 -lemma setsum_reindex:
2.124 -     "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
2.126 -
2.127 -lemma setsum_reindex_id:
2.128 -     "inj_on f B ==> setsum f B = setsum id (f ` B)"
2.129 -by (auto simp add: setsum_reindex)
2.130 -
2.131 -lemma setsum_reindex_nonzero:
2.132 -  assumes fS: "finite S"
2.133 -  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"
2.134 -  shows "setsum h (f ` S) = setsum (h o f) S"
2.135 -using nz
2.136 -proof(induct rule: finite_induct[OF fS])
2.137 -  case 1 thus ?case by simp
2.138 -next
2.139 -  case (2 x F)
2.140 -  {assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto
2.141 -    then obtain y where y: "y \<in> F" "f x = f y" by auto
2.142 -    from "2.hyps" y have xy: "x \<noteq> y" by auto
2.143 -
2.144 -    from "2.prems"[of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp
2.145 -    have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto
2.146 -    also have "\<dots> = setsum (h o f) (insert x F)"
2.147 -      unfolding setsum_insert[OF `finite F` `x\<notin>F`]
2.148 -      using h0
2.149 -      apply simp
2.150 -      apply (rule "2.hyps"(3))
2.151 -      apply (rule_tac y="y" in  "2.prems")
2.152 -      apply simp_all
2.153 -      done
2.154 -    finally have ?case .}
2.155 -  moreover
2.156 -  {assume fxF: "f x \<notin> f ` F"
2.157 -    have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)"
2.158 -      using fxF "2.hyps" by simp
2.159 -    also have "\<dots> = setsum (h o f) (insert x F)"
2.160 -      unfolding setsum_insert[OF `finite F` `x\<notin>F`]
2.161 -      apply simp
2.162 -      apply (rule cong[OF refl[of "op + (h (f x))"]])
2.163 -      apply (rule "2.hyps"(3))
2.164 -      apply (rule_tac y="y" in  "2.prems")
2.165 -      apply simp_all
2.166 -      done
2.167 -    finally have ?case .}
2.168 -  ultimately show ?case by blast
2.169 -qed
2.170 -
2.171 -lemma setsum_cong:
2.172 -  "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
2.173 -by(fastsimp simp: setsum_def intro: comm_monoid_add.fold_image_cong)
2.174 -
2.175 -lemma strong_setsum_cong[cong]:
2.176 -  "A = B ==> (!!x. x:B =simp=> f x = g x)
2.177 -   ==> setsum (%x. f x) A = setsum (%x. g x) B"
2.178 -by(fastsimp simp: simp_implies_def setsum_def intro: comm_monoid_add.fold_image_cong)
2.179 -
2.180 -lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A"
2.181 -by (rule setsum_cong[OF refl], auto)
2.182 -
2.183 -lemma setsum_reindex_cong:
2.184 -   "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|]
2.185 -    ==> setsum h B = setsum g A"
2.186 -by (simp add: setsum_reindex cong: setsum_cong)
2.187 -
2.188 -
2.189 -lemma setsum_0[simp]: "setsum (%i. 0) A = 0"
2.190 -apply (clarsimp simp: setsum_def)
2.191 -apply (erule finite_induct, auto)
2.192 -done
2.193 -
2.194 -lemma setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0"
2.196 -
2.197 -lemma setsum_Un_Int: "finite A ==> finite B ==>
2.198 -  setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
2.199 -  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
2.201 -
2.202 -lemma setsum_Un_disjoint: "finite A ==> finite B
2.203 -  ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
2.204 -by (subst setsum_Un_Int [symmetric], auto)
2.205 -
2.206 -lemma setsum_mono_zero_left:
2.207 -  assumes fT: "finite T" and ST: "S \<subseteq> T"
2.208 -  and z: "\<forall>i \<in> T - S. f i = 0"
2.209 -  shows "setsum f S = setsum f T"
2.210 -proof-
2.211 -  have eq: "T = S \<union> (T - S)" using ST by blast
2.212 -  have d: "S \<inter> (T - S) = {}" using ST by blast
2.213 -  from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
2.214 -  show ?thesis
2.215 -  by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
2.216 -qed
2.217 -
2.218 -lemma setsum_mono_zero_right:
2.219 -  "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. f i = 0 \<Longrightarrow> setsum f T = setsum f S"
2.220 -by(blast intro!: setsum_mono_zero_left[symmetric])
2.221 -
2.222 -lemma setsum_mono_zero_cong_left:
2.223 -  assumes fT: "finite T" and ST: "S \<subseteq> T"
2.224 -  and z: "\<forall>i \<in> T - S. g i = 0"
2.225 -  and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
2.226 -  shows "setsum f S = setsum g T"
2.227 -proof-
2.228 -  have eq: "T = S \<union> (T - S)" using ST by blast
2.229 -  have d: "S \<inter> (T - S) = {}" using ST by blast
2.230 -  from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
2.231 -  show ?thesis
2.232 -    using fg by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
2.233 -qed
2.234 -
2.235 -lemma setsum_mono_zero_cong_right:
2.236 -  assumes fT: "finite T" and ST: "S \<subseteq> T"
2.237 -  and z: "\<forall>i \<in> T - S. f i = 0"
2.238 -  and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
2.239 -  shows "setsum f T = setsum g S"
2.240 -using setsum_mono_zero_cong_left[OF fT ST z] fg[symmetric] by auto
2.241 -
2.242 -lemma setsum_delta:
2.243 -  assumes fS: "finite S"
2.244 -  shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
2.245 -proof-
2.246 -  let ?f = "(\<lambda>k. if k=a then b k else 0)"
2.247 -  {assume a: "a \<notin> S"
2.248 -    hence "\<forall> k\<in> S. ?f k = 0" by simp
2.249 -    hence ?thesis  using a by simp}
2.250 -  moreover
2.251 -  {assume a: "a \<in> S"
2.252 -    let ?A = "S - {a}"
2.253 -    let ?B = "{a}"
2.254 -    have eq: "S = ?A \<union> ?B" using a by blast
2.255 -    have dj: "?A \<inter> ?B = {}" by simp
2.256 -    from fS have fAB: "finite ?A" "finite ?B" by auto
2.257 -    have "setsum ?f S = setsum ?f ?A + setsum ?f ?B"
2.258 -      using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
2.259 -      by simp
2.260 -    then have ?thesis  using a by simp}
2.261 -  ultimately show ?thesis by blast
2.262 -qed
2.263 -lemma setsum_delta':
2.264 -  assumes fS: "finite S" shows
2.265 -  "setsum (\<lambda>k. if a = k then b k else 0) S =
2.266 -     (if a\<in> S then b a else 0)"
2.267 -  using setsum_delta[OF fS, of a b, symmetric]
2.268 -  by (auto intro: setsum_cong)
2.269 -
2.270 -lemma setsum_restrict_set:
2.271 -  assumes fA: "finite A"
2.272 -  shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A"
2.273 -proof-
2.274 -  from fA have fab: "finite (A \<inter> B)" by auto
2.275 -  have aba: "A \<inter> B \<subseteq> A" by blast
2.276 -  let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0"
2.277 -  from setsum_mono_zero_left[OF fA aba, of ?g]
2.278 -  show ?thesis by simp
2.279 -qed
2.280 -
2.281 -lemma setsum_cases:
2.282 -  assumes fA: "finite A"
2.283 -  shows "setsum (\<lambda>x. if P x then f x else g x) A =
2.284 -         setsum f (A \<inter> {x. P x}) + setsum g (A \<inter> - {x. P x})"
2.285 -proof-
2.286 -  have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}"
2.287 -          "(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}"
2.288 -    by blast+
2.289 -  from fA
2.290 -  have f: "finite (A \<inter> {x. P x})" "finite (A \<inter> -{x. P x})" by auto
2.291 -  let ?g = "\<lambda>x. if P x then f x else g x"
2.292 -  from setsum_Un_disjoint[OF f a(2), of ?g] a(1)
2.293 -  show ?thesis by simp
2.294 -qed
2.295 -
2.296 -
2.297 -(*But we can't get rid of finite I. If infinite, although the rhs is 0,
2.298 -  the lhs need not be, since UNION I A could still be finite.*)
2.299 -lemma setsum_UN_disjoint:
2.300 -    "finite I ==> (ALL i:I. finite (A i)) ==>
2.301 -        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
2.302 -      setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
2.304 -
2.305 -text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
2.306 -directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
2.307 -lemma setsum_Union_disjoint:
2.308 -  "[| (ALL A:C. finite A);
2.309 -      (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
2.310 -   ==> setsum f (Union C) = setsum (setsum f) C"
2.311 -apply (cases "finite C")
2.312 - prefer 2 apply (force dest: finite_UnionD simp add: setsum_def)
2.313 -  apply (frule setsum_UN_disjoint [of C id f])
2.314 - apply (unfold Union_def id_def, assumption+)
2.315 -done
2.316 -
2.317 -(*But we can't get rid of finite A. If infinite, although the lhs is 0,
2.318 -  the rhs need not be, since SIGMA A B could still be finite.*)
2.319 -lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
2.320 -    (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
2.322 -
2.323 -text{*Here we can eliminate the finiteness assumptions, by cases.*}
2.324 -lemma setsum_cartesian_product:
2.325 -   "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)"
2.326 -apply (cases "finite A")
2.327 - apply (cases "finite B")
2.328 -  apply (simp add: setsum_Sigma)
2.329 - apply (cases "A={}", simp)
2.330 - apply (simp)
2.331 -apply (auto simp add: setsum_def
2.332 -            dest: finite_cartesian_productD1 finite_cartesian_productD2)
2.333 -done
2.334 -
2.335 -lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
2.337 -
2.338 -
2.339 -subsubsection {* Properties in more restricted classes of structures *}
2.340 -
2.341 -lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
2.342 -apply (case_tac "finite A")
2.343 - prefer 2 apply (simp add: setsum_def)
2.344 -apply (erule rev_mp)
2.345 -apply (erule finite_induct, auto)
2.346 -done
2.347 -
2.348 -lemma setsum_eq_0_iff [simp]:
2.349 -    "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
2.350 -by (induct set: finite) auto
2.351 -
2.352 -lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
2.353 -  (setsum f A = Suc 0) = (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
2.354 -apply(erule finite_induct)
2.356 -done
2.357 -
2.358 -lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
2.359 -
2.360 -lemma setsum_Un_nat: "finite A ==> finite B ==>
2.361 -  (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
2.362 -  -- {* For the natural numbers, we have subtraction. *}
2.363 -by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
2.364 -
2.365 -lemma setsum_Un: "finite A ==> finite B ==>
2.366 -  (setsum f (A Un B) :: 'a :: ab_group_add) =
2.367 -   setsum f A + setsum f B - setsum f (A Int B)"
2.368 -by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
2.369 -
2.370 -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"
2.371 -  apply (induct set: finite)
2.372 -  apply simp by auto
2.373 -
2.374 -lemma (in comm_monoid_mult) fold_image_Un_one:
2.375 -  assumes fS: "finite S" and fT: "finite T"
2.376 -  and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
2.377 -  shows "fold_image (op *) f 1 (S \<union> T) = fold_image (op *) f 1 S * fold_image (op *) f 1 T"
2.378 -proof-
2.379 -  have "fold_image op * f 1 (S \<inter> T) = 1"
2.380 -    apply (rule fold_image_1)
2.381 -    using fS fT I0 by auto
2.382 -  with fold_image_Un_Int[OF fS fT] show ?thesis by simp
2.383 -qed
2.384 -
2.385 -lemma setsum_eq_general_reverses:
2.386 -  assumes fS: "finite S" and fT: "finite T"
2.387 -  and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
2.388 -  and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x"
2.389 -  shows "setsum f S = setsum g T"
2.390 -  apply (simp add: setsum_def fS fT)
2.391 -  apply (rule comm_monoid_add.fold_image_eq_general_inverses[OF fS])
2.392 -  apply (erule kh)
2.393 -  apply (erule hk)
2.394 -  done
2.395 -
2.396 -
2.397 -
2.398 -lemma setsum_Un_zero:
2.399 -  assumes fS: "finite S" and fT: "finite T"
2.400 -  and I0: "\<forall>x \<in> S\<inter>T. f x = 0"
2.401 -  shows "setsum f (S \<union> T) = setsum f S  + setsum f T"
2.402 -  using fS fT
2.403 -  apply (simp add: setsum_def)
2.405 -  using I0 by auto
2.406 -
2.407 -
2.408 -lemma setsum_UNION_zero:
2.409 -  assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T"
2.410 -  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"
2.411 -  shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S"
2.412 -  using fSS f0
2.413 -proof(induct rule: finite_induct[OF fS])
2.414 -  case 1 thus ?case by simp
2.415 -next
2.416 -  case (2 T F)
2.417 -  then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F"
2.418 -    and H: "setsum f (\<Union> F) = setsum (setsum f) F" by auto
2.419 -  from fTF have fUF: "finite (\<Union>F)" by auto
2.420 -  from "2.prems" TF fTF
2.421 -  show ?case
2.422 -    by (auto simp add: H[symmetric] intro: setsum_Un_zero[OF fTF(1) fUF, of f])
2.423 -qed
2.424 -
2.425 -
2.426 -lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
2.427 -  (if a:A then setsum f A - f a else setsum f A)"
2.428 -apply (case_tac "finite A")
2.429 - prefer 2 apply (simp add: setsum_def)
2.430 -apply (erule finite_induct)
2.431 - apply (auto simp add: insert_Diff_if)
2.432 -apply (drule_tac a = a in mk_disjoint_insert, auto)
2.433 -done
2.434 -
2.435 -lemma setsum_diff1: "finite A \<Longrightarrow>
2.436 -  (setsum f (A - {a}) :: ('a::ab_group_add)) =
2.437 -  (if a:A then setsum f A - f a else setsum f A)"
2.438 -by (erule finite_induct) (auto simp add: insert_Diff_if)
2.439 -
2.440 -lemma setsum_diff1'[rule_format]:
2.441 -  "finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x)"
2.442 -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))"])
2.444 -done
2.445 -
2.446 -lemma setsum_diff1_ring: assumes "finite A" "a \<in> A"
2.447 -  shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)"
2.448 -unfolding setsum_diff1'[OF assms] by auto
2.449 -
2.450 -(* By Jeremy Siek: *)
2.451 -
2.452 -lemma setsum_diff_nat:
2.453 -assumes "finite B" and "B \<subseteq> A"
2.454 -shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
2.455 -using assms
2.456 -proof induct
2.457 -  show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
2.458 -next
2.459 -  fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
2.460 -    and xFinA: "insert x F \<subseteq> A"
2.461 -    and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
2.462 -  from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
2.463 -  from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
2.464 -    by (simp add: setsum_diff1_nat)
2.465 -  from xFinA have "F \<subseteq> A" by simp
2.466 -  with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
2.467 -  with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
2.468 -    by simp
2.469 -  from xnotinF have "A - insert x F = (A - F) - {x}" by auto
2.470 -  with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
2.471 -    by simp
2.472 -  from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
2.473 -  with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
2.474 -    by simp
2.475 -  thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
2.476 -qed
2.477 -
2.478 -lemma setsum_diff:
2.479 -  assumes le: "finite A" "B \<subseteq> A"
2.480 -  shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
2.481 -proof -
2.482 -  from le have finiteB: "finite B" using finite_subset by auto
2.483 -  show ?thesis using finiteB le
2.484 -  proof induct
2.485 -    case empty
2.486 -    thus ?case by auto
2.487 -  next
2.488 -    case (insert x F)
2.489 -    thus ?case using le finiteB
2.490 -      by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
2.491 -  qed
2.492 -qed
2.493 -
2.494 -lemma setsum_mono:
2.495 -  assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, ordered_ab_semigroup_add}))"
2.496 -  shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
2.497 -proof (cases "finite K")
2.498 -  case True
2.499 -  thus ?thesis using le
2.500 -  proof induct
2.501 -    case empty
2.502 -    thus ?case by simp
2.503 -  next
2.504 -    case insert
2.505 -    thus ?case using add_mono by fastsimp
2.506 -  qed
2.507 -next
2.508 -  case False
2.509 -  thus ?thesis
2.510 -    by (simp add: setsum_def)
2.511 -qed
2.512 -
2.513 -lemma setsum_strict_mono:
2.515 -  assumes "finite A"  "A \<noteq> {}"
2.516 -    and "!!x. x:A \<Longrightarrow> f x < g x"
2.517 -  shows "setsum f A < setsum g A"
2.518 -  using prems
2.519 -proof (induct rule: finite_ne_induct)
2.520 -  case singleton thus ?case by simp
2.521 -next
2.522 -  case insert thus ?case by (auto simp: add_strict_mono)
2.523 -qed
2.524 -
2.525 -lemma setsum_negf:
2.526 -  "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
2.527 -proof (cases "finite A")
2.528 -  case True thus ?thesis by (induct set: finite) auto
2.529 -next
2.530 -  case False thus ?thesis by (simp add: setsum_def)
2.531 -qed
2.532 -
2.533 -lemma setsum_subtractf:
2.534 -  "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
2.535 -    setsum f A - setsum g A"
2.536 -proof (cases "finite A")
2.537 -  case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
2.538 -next
2.539 -  case False thus ?thesis by (simp add: setsum_def)
2.540 -qed
2.541 -
2.542 -lemma setsum_nonneg:
2.544 -  shows "0 \<le> setsum f A"
2.545 -proof (cases "finite A")
2.546 -  case True thus ?thesis using nn
2.547 -  proof induct
2.548 -    case empty then show ?case by simp
2.549 -  next
2.550 -    case (insert x F)
2.551 -    then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
2.552 -    with insert show ?case by simp
2.553 -  qed
2.554 -next
2.555 -  case False thus ?thesis by (simp add: setsum_def)
2.556 -qed
2.557 -
2.558 -lemma setsum_nonpos:
2.560 -  shows "setsum f A \<le> 0"
2.561 -proof (cases "finite A")
2.562 -  case True thus ?thesis using np
2.563 -  proof induct
2.564 -    case empty then show ?case by simp
2.565 -  next
2.566 -    case (insert x F)
2.567 -    then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
2.568 -    with insert show ?case by simp
2.569 -  qed
2.570 -next
2.571 -  case False thus ?thesis by (simp add: setsum_def)
2.572 -qed
2.573 -
2.574 -lemma setsum_mono2:
2.576 -assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
2.577 -shows "setsum f A \<le> setsum f B"
2.578 -proof -
2.579 -  have "setsum f A \<le> setsum f A + setsum f (B-A)"
2.581 -  also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
2.582 -    by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
2.583 -  also have "A \<union> (B-A) = B" using sub by blast
2.584 -  finally show ?thesis .
2.585 -qed
2.586 -
2.587 -lemma setsum_mono3: "finite B ==> A <= B ==>
2.588 -    ALL x: B - A.
2.590 -        setsum f A <= setsum f B"
2.591 -  apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
2.592 -  apply (erule ssubst)
2.593 -  apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
2.594 -  apply simp
2.596 -  apply (erule setsum_nonneg)
2.597 -  apply (subst setsum_Un_disjoint [THEN sym])
2.598 -  apply (erule finite_subset, assumption)
2.599 -  apply (rule finite_subset)
2.600 -  prefer 2
2.601 -  apply assumption
2.602 -  apply (auto simp add: sup_absorb2)
2.603 -done
2.604 -
2.605 -lemma setsum_right_distrib:
2.606 -  fixes f :: "'a => ('b::semiring_0)"
2.607 -  shows "r * setsum f A = setsum (%n. r * f n) A"
2.608 -proof (cases "finite A")
2.609 -  case True
2.610 -  thus ?thesis
2.611 -  proof induct
2.612 -    case empty thus ?case by simp
2.613 -  next
2.614 -    case (insert x A) thus ?case by (simp add: right_distrib)
2.615 -  qed
2.616 -next
2.617 -  case False thus ?thesis by (simp add: setsum_def)
2.618 -qed
2.619 -
2.620 -lemma setsum_left_distrib:
2.621 -  "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
2.622 -proof (cases "finite A")
2.623 -  case True
2.624 -  then show ?thesis
2.625 -  proof induct
2.626 -    case empty thus ?case by simp
2.627 -  next
2.628 -    case (insert x A) thus ?case by (simp add: left_distrib)
2.629 -  qed
2.630 -next
2.631 -  case False thus ?thesis by (simp add: setsum_def)
2.632 -qed
2.633 -
2.634 -lemma setsum_divide_distrib:
2.635 -  "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
2.636 -proof (cases "finite A")
2.637 -  case True
2.638 -  then show ?thesis
2.639 -  proof induct
2.640 -    case empty thus ?case by simp
2.641 -  next
2.642 -    case (insert x A) thus ?case by (simp add: add_divide_distrib)
2.643 -  qed
2.644 -next
2.645 -  case False thus ?thesis by (simp add: setsum_def)
2.646 -qed
2.647 -
2.648 -lemma setsum_abs[iff]:
2.649 -  fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
2.650 -  shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
2.651 -proof (cases "finite A")
2.652 -  case True
2.653 -  thus ?thesis
2.654 -  proof induct
2.655 -    case empty thus ?case by simp
2.656 -  next
2.657 -    case (insert x A)
2.658 -    thus ?case by (auto intro: abs_triangle_ineq order_trans)
2.659 -  qed
2.660 -next
2.661 -  case False thus ?thesis by (simp add: setsum_def)
2.662 -qed
2.663 -
2.664 -lemma setsum_abs_ge_zero[iff]:
2.665 -  fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
2.666 -  shows "0 \<le> setsum (%i. abs(f i)) A"
2.667 -proof (cases "finite A")
2.668 -  case True
2.669 -  thus ?thesis
2.670 -  proof induct
2.671 -    case empty thus ?case by simp
2.672 -  next
2.673 -    case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg)
2.674 -  qed
2.675 -next
2.676 -  case False thus ?thesis by (simp add: setsum_def)
2.677 -qed
2.678 -
2.679 -lemma abs_setsum_abs[simp]:
2.680 -  fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
2.681 -  shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
2.682 -proof (cases "finite A")
2.683 -  case True
2.684 -  thus ?thesis
2.685 -  proof induct
2.686 -    case empty thus ?case by simp
2.687 -  next
2.688 -    case (insert a A)
2.689 -    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
2.690 -    also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
2.691 -    also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
2.692 -      by (simp del: abs_of_nonneg)
2.693 -    also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
2.694 -    finally show ?case .
2.695 -  qed
2.696 -next
2.697 -  case False thus ?thesis by (simp add: setsum_def)
2.698 -qed
2.699 -
2.700 -
2.701 -lemma setsum_Plus:
2.702 -  fixes A :: "'a set" and B :: "'b set"
2.703 -  assumes fin: "finite A" "finite B"
2.704 -  shows "setsum f (A <+> B) = setsum (f \<circ> Inl) A + setsum (f \<circ> Inr) B"
2.705 -proof -
2.706 -  have "A <+> B = Inl ` A \<union> Inr ` B" by auto
2.707 -  moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)"
2.708 -    by(auto intro: finite_imageI)
2.709 -  moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto
2.710 -  moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI)
2.711 -  ultimately show ?thesis using fin by(simp add: setsum_Un_disjoint setsum_reindex)
2.712 -qed
2.713 -
2.714 -
2.715 -text {* Commuting outer and inner summation *}
2.716 -
2.717 -lemma swap_inj_on:
2.718 -  "inj_on (%(i, j). (j, i)) (A \<times> B)"
2.719 -  by (unfold inj_on_def) fast
2.720 -
2.721 -lemma swap_product:
2.722 -  "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
2.723 -  by (simp add: split_def image_def) blast
2.724 -
2.725 -lemma setsum_commute:
2.726 -  "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
2.728 -  have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
2.729 -    (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
2.730 -    (is "?s = _")
2.731 -    apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on)
2.732 -    apply (simp add: split_def)
2.733 -    done
2.734 -  also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
2.735 -    (is "_ = ?t")
2.736 -    apply (simp add: swap_product)
2.737 -    done
2.738 -  finally show "?s = ?t" .
2.739 -qed
2.740 -
2.741 -lemma setsum_product:
2.742 -  fixes f :: "'a => ('b::semiring_0)"
2.743 -  shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
2.744 -  by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
2.745 -
2.746 -lemma setsum_mult_setsum_if_inj:
2.747 -fixes f :: "'a => ('b::semiring_0)"
2.748 -shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==>
2.749 -  setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}"
2.750 -by(auto simp: setsum_product setsum_cartesian_product
2.751 -        intro!:  setsum_reindex_cong[symmetric])
2.752 -
2.753 -
2.754 -subsection {* Generalized product over a set *}
2.755 -
2.756 -definition setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
2.757 -where "setprod f A == if finite A then fold_image (op *) f 1 A else 1"
2.758 -
2.759 -abbreviation
2.760 -  Setprod  ("\<Prod>_" [1000] 999) where
2.761 -  "\<Prod>A == setprod (%x. x) A"
2.762 -
2.763 -syntax
2.764 -  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
2.765 -syntax (xsymbols)
2.766 -  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
2.767 -syntax (HTML output)
2.768 -  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
2.769 -
2.770 -translations -- {* Beware of argument permutation! *}
2.771 -  "PROD i:A. b" == "CONST setprod (%i. b) A"
2.772 -  "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A"
2.773 -
2.774 -text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
2.775 - @{text"\<Prod>x|P. e"}. *}
2.776 -
2.777 -syntax
2.778 -  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
2.779 -syntax (xsymbols)
2.780 -  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
2.781 -syntax (HTML output)
2.782 -  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
2.783 -
2.784 -translations
2.785 -  "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
2.786 -  "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
2.787 -
2.788 -
2.789 -lemma setprod_empty [simp]: "setprod f {} = 1"
2.790 -by (auto simp add: setprod_def)
2.791 -
2.792 -lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
2.793 -    setprod f (insert a A) = f a * setprod f A"
2.795 -
2.796 -lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
2.798 -
2.799 -lemma setprod_reindex:
2.800 -   "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
2.801 -by(auto simp: setprod_def fold_image_reindex dest!:finite_imageD)
2.802 -
2.803 -lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
2.804 -by (auto simp add: setprod_reindex)
2.805 -
2.806 -lemma setprod_cong:
2.807 -  "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
2.808 -by(fastsimp simp: setprod_def intro: fold_image_cong)
2.809 -
2.810 -lemma strong_setprod_cong[cong]:
2.811 -  "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
2.812 -by(fastsimp simp: simp_implies_def setprod_def intro: fold_image_cong)
2.813 -
2.814 -lemma setprod_reindex_cong: "inj_on f A ==>
2.815 -    B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
2.816 -by (frule setprod_reindex, simp)
2.817 -
2.818 -lemma strong_setprod_reindex_cong: assumes i: "inj_on f A"
2.819 -  and B: "B = f ` A" and eq: "\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x"
2.820 -  shows "setprod h B = setprod g A"
2.821 -proof-
2.822 -    have "setprod h B = setprod (h o f) A"
2.823 -      by (simp add: B setprod_reindex[OF i, of h])
2.824 -    then show ?thesis apply simp
2.825 -      apply (rule setprod_cong)
2.826 -      apply simp
2.827 -      by (simp add: eq)
2.828 -qed
2.829 -
2.830 -lemma setprod_Un_one:
2.831 -  assumes fS: "finite S" and fT: "finite T"
2.832 -  and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
2.833 -  shows "setprod f (S \<union> T) = setprod f S  * setprod f T"
2.834 -  using fS fT
2.835 -  apply (simp add: setprod_def)
2.836 -  apply (rule fold_image_Un_one)
2.837 -  using I0 by auto
2.838 -
2.839 -
2.840 -lemma setprod_1: "setprod (%i. 1) A = 1"
2.841 -apply (case_tac "finite A")
2.842 -apply (erule finite_induct, auto simp add: mult_ac)
2.843 -done
2.844 -
2.845 -lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
2.846 -apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
2.847 -apply (erule ssubst, rule setprod_1)
2.848 -apply (rule setprod_cong, auto)
2.849 -done
2.850 -
2.851 -lemma setprod_Un_Int: "finite A ==> finite B
2.852 -    ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
2.854 -
2.855 -lemma setprod_Un_disjoint: "finite A ==> finite B
2.856 -  ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
2.857 -by (subst setprod_Un_Int [symmetric], auto)
2.858 -
2.859 -lemma setprod_mono_one_left:
2.860 -  assumes fT: "finite T" and ST: "S \<subseteq> T"
2.861 -  and z: "\<forall>i \<in> T - S. f i = 1"
2.862 -  shows "setprod f S = setprod f T"
2.863 -proof-
2.864 -  have eq: "T = S \<union> (T - S)" using ST by blast
2.865 -  have d: "S \<inter> (T - S) = {}" using ST by blast
2.866 -  from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
2.867 -  show ?thesis
2.868 -  by (simp add: setprod_Un_disjoint[OF f d, unfolded eq[symmetric]] setprod_1'[OF z])
2.869 -qed
2.870 -
2.871 -lemmas setprod_mono_one_right = setprod_mono_one_left [THEN sym]
2.872 -
2.873 -lemma setprod_delta:
2.874 -  assumes fS: "finite S"
2.875 -  shows "setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
2.876 -proof-
2.877 -  let ?f = "(\<lambda>k. if k=a then b k else 1)"
2.878 -  {assume a: "a \<notin> S"
2.879 -    hence "\<forall> k\<in> S. ?f k = 1" by simp
2.880 -    hence ?thesis  using a by (simp add: setprod_1 cong add: setprod_cong) }
2.881 -  moreover
2.882 -  {assume a: "a \<in> S"
2.883 -    let ?A = "S - {a}"
2.884 -    let ?B = "{a}"
2.885 -    have eq: "S = ?A \<union> ?B" using a by blast
2.886 -    have dj: "?A \<inter> ?B = {}" by simp
2.887 -    from fS have fAB: "finite ?A" "finite ?B" by auto
2.888 -    have fA1: "setprod ?f ?A = 1" apply (rule setprod_1') by auto
2.889 -    have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
2.890 -      using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
2.891 -      by simp
2.892 -    then have ?thesis  using a by (simp add: fA1 cong add: setprod_cong cong del: if_weak_cong)}
2.893 -  ultimately show ?thesis by blast
2.894 -qed
2.895 -
2.896 -lemma setprod_delta':
2.897 -  assumes fS: "finite S" shows
2.898 -  "setprod (\<lambda>k. if a = k then b k else 1) S =
2.899 -     (if a\<in> S then b a else 1)"
2.900 -  using setprod_delta[OF fS, of a b, symmetric]
2.901 -  by (auto intro: setprod_cong)
2.902 -
2.903 -
2.904 -lemma setprod_UN_disjoint:
2.905 -    "finite I ==> (ALL i:I. finite (A i)) ==>
2.906 -        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
2.907 -      setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
2.908 -by(simp add: setprod_def fold_image_UN_disjoint cong: setprod_cong)
2.909 -
2.910 -lemma setprod_Union_disjoint:
2.911 -  "[| (ALL A:C. finite A);
2.912 -      (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
2.913 -   ==> setprod f (Union C) = setprod (setprod f) C"
2.914 -apply (cases "finite C")
2.915 - prefer 2 apply (force dest: finite_UnionD simp add: setprod_def)
2.916 -  apply (frule setprod_UN_disjoint [of C id f])
2.917 - apply (unfold Union_def id_def, assumption+)
2.918 -done
2.919 -
2.920 -lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
2.921 -    (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
2.922 -    (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
2.923 -by(simp add:setprod_def fold_image_Sigma split_def cong:setprod_cong)
2.924 -
2.925 -text{*Here we can eliminate the finiteness assumptions, by cases.*}
2.926 -lemma setprod_cartesian_product:
2.927 -     "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
2.928 -apply (cases "finite A")
2.929 - apply (cases "finite B")
2.930 -  apply (simp add: setprod_Sigma)
2.931 - apply (cases "A={}", simp)
2.932 - apply (simp add: setprod_1)
2.933 -apply (auto simp add: setprod_def
2.934 -            dest: finite_cartesian_productD1 finite_cartesian_productD2)
2.935 -done
2.936 -
2.937 -lemma setprod_timesf:
2.938 -     "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
2.940 -
2.941 -
2.942 -subsubsection {* Properties in more restricted classes of structures *}
2.943 -
2.944 -lemma setprod_eq_1_iff [simp]:
2.945 -  "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
2.946 -by (induct set: finite) auto
2.947 -
2.948 -lemma setprod_zero:
2.949 -     "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
2.950 -apply (induct set: finite, force, clarsimp)
2.951 -apply (erule disjE, auto)
2.952 -done
2.953 -
2.954 -lemma setprod_nonneg [rule_format]:
2.955 -   "(ALL x: A. (0::'a::linordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
2.956 -by (cases "finite A", induct set: finite, simp_all add: mult_nonneg_nonneg)
2.957 -
2.958 -lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x)
2.959 -  --> 0 < setprod f A"
2.960 -by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos)
2.961 -
2.962 -lemma setprod_zero_iff[simp]: "finite A ==>
2.963 -  (setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) =
2.964 -  (EX x: A. f x = 0)"
2.965 -by (erule finite_induct, auto simp:no_zero_divisors)
2.966 -
2.967 -lemma setprod_pos_nat:
2.968 -  "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
2.969 -using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
2.970 -
2.971 -lemma setprod_pos_nat_iff[simp]:
2.972 -  "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
2.973 -using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
2.974 -
2.975 -lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
2.976 -  (setprod f (A Un B) :: 'a ::{field})
2.977 -   = setprod f A * setprod f B / setprod f (A Int B)"
2.978 -by (subst setprod_Un_Int [symmetric], auto)
2.979 -
2.980 -lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
2.981 -  (setprod f (A - {a}) :: 'a :: {field}) =
2.982 -  (if a:A then setprod f A / f a else setprod f A)"
2.983 -by (erule finite_induct) (auto simp add: insert_Diff_if)
2.984 -
2.985 -lemma setprod_inversef:
2.986 -  fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}"
2.987 -  shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)"
2.988 -by (erule finite_induct) auto
2.989 -
2.990 -lemma setprod_dividef:
2.991 -  fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}"
2.992 -  shows "finite A
2.993 -    ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
2.994 -apply (subgoal_tac
2.995 -         "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
2.996 -apply (erule ssubst)
2.997 -apply (subst divide_inverse)
2.998 -apply (subst setprod_timesf)
2.999 -apply (subst setprod_inversef, assumption+, rule refl)
2.1000 -apply (rule setprod_cong, rule refl)
2.1001 -apply (subst divide_inverse, auto)
2.1002 -done
2.1003 -
2.1004 -lemma setprod_dvd_setprod [rule_format]:
2.1005 -    "(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A"
2.1006 -  apply (cases "finite A")
2.1007 -  apply (induct set: finite)
2.1008 -  apply (auto simp add: dvd_def)
2.1009 -  apply (rule_tac x = "k * ka" in exI)
2.1010 -  apply (simp add: algebra_simps)
2.1011 -done
2.1012 -
2.1013 -lemma setprod_dvd_setprod_subset:
2.1014 -  "finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B"
2.1015 -  apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)")
2.1016 -  apply (unfold dvd_def, blast)
2.1017 -  apply (subst setprod_Un_disjoint [symmetric])
2.1018 -  apply (auto elim: finite_subset intro: setprod_cong)
2.1019 -done
2.1020 -
2.1021 -lemma setprod_dvd_setprod_subset2:
2.1022 -  "finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow>
2.1023 -      setprod f A dvd setprod g B"
2.1024 -  apply (rule dvd_trans)
2.1025 -  apply (rule setprod_dvd_setprod, erule (1) bspec)
2.1026 -  apply (erule (1) setprod_dvd_setprod_subset)
2.1027 -done
2.1028 -
2.1029 -lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow>
2.1030 -    (f i ::'a::comm_semiring_1) dvd setprod f A"
2.1031 -by (induct set: finite) (auto intro: dvd_mult)
2.1032 -
2.1033 -lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow>
2.1034 -    (d::'a::comm_semiring_1) dvd (SUM x : A. f x)"
2.1035 -  apply (cases "finite A")
2.1036 -  apply (induct set: finite)
2.1037 -  apply auto
2.1038 -done
2.1039 -
2.1040 -lemma setprod_mono:
2.1041 -  fixes f :: "'a \<Rightarrow> 'b\<Colon>linordered_semidom"
2.1042 -  assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i"
2.1043 -  shows "setprod f A \<le> setprod g A"
2.1044 -proof (cases "finite A")
2.1045 -  case True
2.1046 -  hence ?thesis "setprod f A \<ge> 0" using subset_refl[of A]
2.1047 -  proof (induct A rule: finite_subset_induct)
2.1048 -    case (insert a F)
2.1049 -    thus "setprod f (insert a F) \<le> setprod g (insert a F)" "0 \<le> setprod f (insert a F)"
2.1050 -      unfolding setprod_insert[OF insert(1,3)]
2.1051 -      using assms[rule_format,OF insert(2)] insert
2.1052 -      by (auto intro: mult_mono mult_nonneg_nonneg)
2.1053 -  qed auto
2.1054 -  thus ?thesis by simp
2.1055 -qed auto
2.1056 -
2.1057 -lemma abs_setprod:
2.1058 -  fixes f :: "'a \<Rightarrow> 'b\<Colon>{linordered_field,abs}"
2.1059 -  shows "abs (setprod f A) = setprod (\<lambda>x. abs (f x)) A"
2.1060 -proof (cases "finite A")
2.1061 -  case True thus ?thesis
2.1062 -    by induct (auto simp add: field_simps abs_mult)
2.1063 -qed auto
2.1064 -
2.1065 -
2.1066 -subsection {* Finite cardinality *}
2.1067 -
2.1068 -text {* This definition, although traditional, is ugly to work with:
2.1069 -@{text "card A == LEAST n. EX f. A = {f i | i. i < n}"}.
2.1070 -But now that we have @{text setsum} things are easy:
2.1071 -*}
2.1072 -
2.1073 -definition card :: "'a set \<Rightarrow> nat" where
2.1074 -  "card A = setsum (\<lambda>x. 1) A"
2.1075 -
2.1076 -lemmas card_eq_setsum = card_def
2.1077 -
2.1078 -lemma card_empty [simp]: "card {} = 0"
2.1079 -  by (simp add: card_def)
2.1080 -
2.1081 -lemma card_insert_disjoint [simp]:
2.1082 -  "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
2.1083 -  by (simp add: card_def)
2.1084 -
2.1085 -lemma card_insert_if:
2.1086 -  "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
2.1087 -  by (simp add: insert_absorb)
2.1088 -
2.1089 -lemma card_infinite [simp]: "~ finite A ==> card A = 0"
2.1090 -  by (simp add: card_def)
2.1091 -
2.1092 -lemma card_ge_0_finite:
2.1093 -  "card A > 0 \<Longrightarrow> finite A"
2.1094 -  by (rule ccontr) simp
2.1095 -
2.1096 -lemma card_0_eq [simp,noatp]: "finite A ==> (card A = 0) = (A = {})"
2.1097 -  apply auto
2.1098 -  apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
2.1099 -  done
2.1100 -
2.1101 -lemma finite_UNIV_card_ge_0:
2.1102 -  "finite (UNIV :: 'a set) \<Longrightarrow> card (UNIV :: 'a set) > 0"
2.1103 -  by (rule ccontr) simp
2.1104 -
2.1105 -lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
2.1106 -  by auto
2.1107 -
2.1108 -lemma card_gt_0_iff: "(0 < card A) = (A \<noteq> {} & finite A)"
2.1109 -  by (simp add: neq0_conv [symmetric] card_eq_0_iff)
2.1110 -
2.1111 -lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
2.1112 -apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
2.1113 -apply(simp del:insert_Diff_single)
2.1114 -done
2.1115 -
2.1116 -lemma card_Diff_singleton:
2.1117 -  "finite A ==> x: A ==> card (A - {x}) = card A - 1"
2.1118 -by (simp add: card_Suc_Diff1 [symmetric])
2.1119 -
2.1120 -lemma card_Diff_singleton_if:
2.1121 -  "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
2.1123 -
2.1124 -lemma card_Diff_insert[simp]:
2.1125 -assumes "finite A" and "a:A" and "a ~: B"
2.1126 -shows "card(A - insert a B) = card(A - B) - 1"
2.1127 -proof -
2.1128 -  have "A - insert a B = (A - B) - {a}" using assms by blast
2.1129 -  then show ?thesis using assms by(simp add:card_Diff_singleton)
2.1130 -qed
2.1131 -
2.1132 -lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
2.1133 -by (simp add: card_insert_if card_Suc_Diff1 del:card_Diff_insert)
2.1134 -
2.1135 -lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
2.1137 -
2.1138 -lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
2.1139 -by (simp add: card_def setsum_mono2)
2.1140 -
2.1141 -lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
2.1142 -apply (induct set: finite, simp, clarify)
2.1143 -apply (subgoal_tac "finite A & A - {x} <= F")
2.1144 - prefer 2 apply (blast intro: finite_subset, atomize)
2.1145 -apply (drule_tac x = "A - {x}" in spec)
2.1147 -apply (case_tac "card A", auto)
2.1148 -done
2.1149 -
2.1150 -lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
2.1151 -apply (simp add: psubset_eq linorder_not_le [symmetric])
2.1152 -apply (blast dest: card_seteq)
2.1153 -done
2.1154 -
2.1155 -lemma card_Un_Int: "finite A ==> finite B
2.1156 -    ==> card A + card B = card (A Un B) + card (A Int B)"
2.1158 -
2.1159 -lemma card_Un_disjoint: "finite A ==> finite B
2.1160 -    ==> A Int B = {} ==> card (A Un B) = card A + card B"
2.1162 -
2.1163 -lemma card_Diff_subset:
2.1164 -  "finite B ==> B <= A ==> card (A - B) = card A - card B"
2.1166 -
2.1167 -lemma card_Diff_subset_Int:
2.1168 -  assumes AB: "finite (A \<inter> B)" shows "card (A - B) = card A - card (A \<inter> B)"
2.1169 -proof -
2.1170 -  have "A - B = A - A \<inter> B" by auto
2.1171 -  thus ?thesis
2.1172 -    by (simp add: card_Diff_subset AB)
2.1173 -qed
2.1174 -
2.1175 -lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
2.1176 -apply (rule Suc_less_SucD)
2.1177 -apply (simp add: card_Suc_Diff1 del:card_Diff_insert)
2.1178 -done
2.1179 -
2.1180 -lemma card_Diff2_less:
2.1181 -  "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
2.1182 -apply (case_tac "x = y")
2.1183 - apply (simp add: card_Diff1_less del:card_Diff_insert)
2.1184 -apply (rule less_trans)
2.1185 - prefer 2 apply (auto intro!: card_Diff1_less simp del:card_Diff_insert)
2.1186 -done
2.1187 -
2.1188 -lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
2.1189 -apply (case_tac "x : A")
2.1190 - apply (simp_all add: card_Diff1_less less_imp_le)
2.1191 -done
2.1192 -
2.1193 -lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
2.1194 -by (erule psubsetI, blast)
2.1195 -
2.1196 -lemma insert_partition:
2.1197 -  "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
2.1198 -  \<Longrightarrow> x \<inter> \<Union> F = {}"
2.1199 -by auto
2.1200 -
2.1201 -lemma finite_psubset_induct[consumes 1, case_names psubset]:
2.1202 -  assumes "finite A" and "!!A. finite A \<Longrightarrow> (!!B. finite B \<Longrightarrow> B \<subset> A \<Longrightarrow> P(B)) \<Longrightarrow> P(A)" shows "P A"
2.1203 -using assms(1)
2.1204 -proof (induct A rule: measure_induct_rule[where f=card])
2.1205 -  case (less A)
2.1206 -  show ?case
2.1207 -  proof(rule assms(2)[OF less(2)])
2.1208 -    fix B assume "finite B" "B \<subset> A"
2.1209 -    show "P B" by(rule less(1)[OF psubset_card_mono[OF less(2) `B \<subset> A`] `finite B`])
2.1210 -  qed
2.1211 -qed
2.1212 -
2.1213 -text{* main cardinality theorem *}
2.1214 -lemma card_partition [rule_format]:
2.1215 -  "finite C ==>
2.1216 -     finite (\<Union> C) -->
2.1217 -     (\<forall>c\<in>C. card c = k) -->
2.1218 -     (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->
2.1219 -     k * card(C) = card (\<Union> C)"
2.1220 -apply (erule finite_induct, simp)
2.1221 -apply (simp add: card_Un_disjoint insert_partition
2.1222 -       finite_subset [of _ "\<Union> (insert x F)"])
2.1223 -done
2.1224 -
2.1225 -lemma card_eq_UNIV_imp_eq_UNIV:
2.1226 -  assumes fin: "finite (UNIV :: 'a set)"
2.1227 -  and card: "card A = card (UNIV :: 'a set)"
2.1228 -  shows "A = (UNIV :: 'a set)"
2.1229 -proof
2.1230 -  show "A \<subseteq> UNIV" by simp
2.1231 -  show "UNIV \<subseteq> A"
2.1232 -  proof
2.1233 -    fix x
2.1234 -    show "x \<in> A"
2.1235 -    proof (rule ccontr)
2.1236 -      assume "x \<notin> A"
2.1237 -      then have "A \<subset> UNIV" by auto
2.1238 -      with fin have "card A < card (UNIV :: 'a set)" by (fact psubset_card_mono)
2.1239 -      with card show False by simp
2.1240 -    qed
2.1241 -  qed
2.1242 -qed
2.1243 -
2.1244 -text{*The form of a finite set of given cardinality*}
2.1245 -
2.1246 -lemma card_eq_SucD:
2.1247 -assumes "card A = Suc k"
2.1248 -shows "\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={})"
2.1249 -proof -
2.1250 -  have fin: "finite A" using assms by (auto intro: ccontr)
2.1251 -  moreover have "card A \<noteq> 0" using assms by auto
2.1252 -  ultimately obtain b where b: "b \<in> A" by auto
2.1253 -  show ?thesis
2.1254 -  proof (intro exI conjI)
2.1255 -    show "A = insert b (A-{b})" using b by blast
2.1256 -    show "b \<notin> A - {b}" by blast
2.1257 -    show "card (A - {b}) = k" and "k = 0 \<longrightarrow> A - {b} = {}"
2.1258 -      using assms b fin by(fastsimp dest:mk_disjoint_insert)+
2.1259 -  qed
2.1260 -qed
2.1261 -
2.1262 -lemma card_Suc_eq:
2.1263 -  "(card A = Suc k) =
2.1264 -   (\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={}))"
2.1265 -apply(rule iffI)
2.1266 - apply(erule card_eq_SucD)
2.1267 -apply(auto)
2.1268 -apply(subst card_insert)
2.1269 - apply(auto intro:ccontr)
2.1270 -done
2.1271 -
2.1272 -lemma finite_fun_UNIVD2:
2.1273 -  assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
2.1274 -  shows "finite (UNIV :: 'b set)"
2.1275 -proof -
2.1276 -  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))"
2.1277 -    by(rule finite_imageI)
2.1278 -  moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary)"
2.1279 -    by(rule UNIV_eq_I) auto
2.1280 -  ultimately show "finite (UNIV :: 'b set)" by simp
2.1281 -qed
2.1282 -
2.1283 -lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
2.1284 -apply (cases "finite A")
2.1285 -apply (erule finite_induct)
2.1286 -apply (auto simp add: algebra_simps)
2.1287 -done
2.1288 -
2.1289 -lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
2.1290 -apply (erule finite_induct)
2.1291 -apply auto
2.1292 -done
2.1293 -
2.1294 -lemma setprod_gen_delta:
2.1295 -  assumes fS: "finite S"
2.1296 -  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)"
2.1297 -proof-
2.1298 -  let ?f = "(\<lambda>k. if k=a then b k else c)"
2.1299 -  {assume a: "a \<notin> S"
2.1300 -    hence "\<forall> k\<in> S. ?f k = c" by simp
2.1301 -    hence ?thesis  using a setprod_constant[OF fS, of c] by (simp add: setprod_1 cong add: setprod_cong) }
2.1302 -  moreover
2.1303 -  {assume a: "a \<in> S"
2.1304 -    let ?A = "S - {a}"
2.1305 -    let ?B = "{a}"
2.1306 -    have eq: "S = ?A \<union> ?B" using a by blast
2.1307 -    have dj: "?A \<inter> ?B = {}" by simp
2.1308 -    from fS have fAB: "finite ?A" "finite ?B" by auto
2.1309 -    have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
2.1310 -      apply (rule setprod_cong) by auto
2.1311 -    have cA: "card ?A = card S - 1" using fS a by auto
2.1312 -    have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
2.1313 -    have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
2.1314 -      using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
2.1315 -      by simp
2.1316 -    then have ?thesis using a cA
2.1317 -      by (simp add: fA1 ring_simps cong add: setprod_cong cong del: if_weak_cong)}
2.1318 -  ultimately show ?thesis by blast
2.1319 -qed
2.1320 -
2.1321 -
2.1322 -lemma setsum_bounded:
2.1323 -  assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
2.1324 -  shows "setsum f A \<le> of_nat(card A) * K"
2.1325 -proof (cases "finite A")
2.1326 -  case True
2.1327 -  thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
2.1328 -next
2.1329 -  case False thus ?thesis by (simp add: setsum_def)
2.1330 -qed
2.1331 -
2.1332 -
2.1333 -lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
2.1334 -  unfolding UNIV_unit by simp
2.1335 -
2.1336 -
2.1337 -subsubsection {* Cardinality of unions *}
2.1338 -
2.1339 -lemma card_UN_disjoint:
2.1340 -  "finite I ==> (ALL i:I. finite (A i)) ==>
2.1341 -   (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {})
2.1342 -   ==> card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
2.1343 -apply (simp add: card_def del: setsum_constant)
2.1344 -apply (subgoal_tac
2.1345 -         "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
2.1346 -apply (simp add: setsum_UN_disjoint del: setsum_constant)
2.1347 -apply (simp cong: setsum_cong)
2.1348 -done
2.1349 -
2.1350 -lemma card_Union_disjoint:
2.1351 -  "finite C ==> (ALL A:C. finite A) ==>
2.1352 -   (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
2.1353 -   ==> card (Union C) = setsum card C"
2.1354 -apply (frule card_UN_disjoint [of C id])
2.1355 -apply (unfold Union_def id_def, assumption+)
2.1356 -done
2.1357 -
2.1358 -
2.1359 -subsubsection {* Cardinality of image *}
2.1360 -
2.1361 -text{*The image of a finite set can be expressed using @{term fold_image}.*}
2.1362 -lemma image_eq_fold_image:
2.1363 -  "finite A ==> f ` A = fold_image (op Un) (%x. {f x}) {} A"
2.1364 -proof (induct rule: finite_induct)
2.1365 -  case empty then show ?case by simp
2.1366 -next
2.1367 -  interpret ab_semigroup_mult "op Un"
2.1368 -    proof qed auto
2.1369 -  case insert
2.1370 -  then show ?case by simp
2.1371 -qed
2.1372 -
2.1373 -lemma card_image_le: "finite A ==> card (f ` A) <= card A"
2.1374 -apply (induct set: finite)
2.1375 - apply simp
2.1376 -apply (simp add: le_SucI card_insert_if)
2.1377 -done
2.1378 -
2.1379 -lemma card_image: "inj_on f A ==> card (f ` A) = card A"
2.1380 -by(simp add:card_def setsum_reindex o_def del:setsum_constant)
2.1381 -
2.1382 -lemma bij_betw_same_card: "bij_betw f A B \<Longrightarrow> card A = card B"
2.1383 -by(auto simp: card_image bij_betw_def)
2.1384 -
2.1385 -lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
2.1386 -by (simp add: card_seteq card_image)
2.1387 -
2.1388 -lemma eq_card_imp_inj_on:
2.1389 -  "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
2.1390 -apply (induct rule:finite_induct)
2.1391 -apply simp
2.1392 -apply(frule card_image_le[where f = f])
2.1394 -done
2.1395 -
2.1396 -lemma inj_on_iff_eq_card:
2.1397 -  "finite A ==> inj_on f A = (card(f ` A) = card A)"
2.1398 -by(blast intro: card_image eq_card_imp_inj_on)
2.1399 -
2.1400 -
2.1401 -lemma card_inj_on_le:
2.1402 -  "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
2.1403 -apply (subgoal_tac "finite A")
2.1404 - apply (force intro: card_mono simp add: card_image [symmetric])
2.1405 -apply (blast intro: finite_imageD dest: finite_subset)
2.1406 -done
2.1407 -
2.1408 -lemma card_bij_eq:
2.1409 -  "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
2.1410 -     finite A; finite B |] ==> card A = card B"
2.1411 -by (auto intro: le_antisym card_inj_on_le)
2.1412 -
2.1413 -
2.1414 -subsubsection {* Cardinality of products *}
2.1415 -
2.1416 -(*
2.1417 -lemma SigmaI_insert: "y \<notin> A ==>
2.1418 -  (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
2.1419 -  by auto
2.1420 -*)
2.1421 -
2.1422 -lemma card_SigmaI [simp]:
2.1423 -  "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
2.1424 -  \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
2.1426 -
2.1427 -lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
2.1428 -apply (cases "finite A")
2.1429 -apply (cases "finite B")
2.1430 -apply (auto simp add: card_eq_0_iff
2.1431 -            dest: finite_cartesian_productD1 finite_cartesian_productD2)
2.1432 -done
2.1433 -
2.1434 -lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
2.1436 -
2.1437 -
2.1438 -subsubsection {* Cardinality of sums *}
2.1439 -
2.1440 -lemma card_Plus:
2.1441 -  assumes "finite A" and "finite B"
2.1442 -  shows "card (A <+> B) = card A + card B"
2.1443 -proof -
2.1444 -  have "Inl`A \<inter> Inr`B = {}" by fast
2.1445 -  with assms show ?thesis
2.1446 -    unfolding Plus_def
2.1447 -    by (simp add: card_Un_disjoint card_image)
2.1448 -qed
2.1449 -
2.1450 -lemma card_Plus_conv_if:
2.1451 -  "card (A <+> B) = (if finite A \<and> finite B then card(A) + card(B) else 0)"
2.1452 -by(auto simp: card_def setsum_Plus simp del: setsum_constant)
2.1453 -
2.1454 -
2.1455 -subsubsection {* Cardinality of the Powerset *}
2.1456 -
2.1457 -lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
2.1458 -apply (induct set: finite)
2.1459 - apply (simp_all add: Pow_insert)
2.1460 -apply (subst card_Un_disjoint, blast)
2.1461 -  apply (blast intro: finite_imageI, blast)
2.1462 -apply (subgoal_tac "inj_on (insert x) (Pow F)")
2.1463 - apply (simp add: card_image Pow_insert)
2.1464 -apply (unfold inj_on_def)
2.1465 -apply (blast elim!: equalityE)
2.1466 -done
2.1467 -
2.1468 -text {* Relates to equivalence classes.  Based on a theorem of F. Kammüller.  *}
2.1469 -
2.1470 -lemma dvd_partition:
2.1471 -  "finite (Union C) ==>
2.1472 -    ALL c : C. k dvd card c ==>
2.1473 -    (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
2.1474 -  k dvd card (Union C)"
2.1475 -apply(frule finite_UnionD)
2.1476 -apply(rotate_tac -1)
2.1477 -apply (induct set: finite, simp_all, clarify)
2.1478 -apply (subst card_Un_disjoint)
2.1479 -   apply (auto simp add: disjoint_eq_subset_Compl)
2.1480 -done
2.1481 -
2.1482 -
2.1483 -subsubsection {* Relating injectivity and surjectivity *}
2.1484 -
2.1485 -lemma finite_surj_inj: "finite(A) \<Longrightarrow> A <= f`A \<Longrightarrow> inj_on f A"
2.1486 -apply(rule eq_card_imp_inj_on, assumption)
2.1487 -apply(frule finite_imageI)
2.1488 -apply(drule (1) card_seteq)
2.1489 - apply(erule card_image_le)
2.1490 -apply simp
2.1491 -done
2.1492 -
2.1493 -lemma finite_UNIV_surj_inj: fixes f :: "'a \<Rightarrow> 'a"
2.1494 -shows "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
2.1495 -by (blast intro: finite_surj_inj subset_UNIV dest:surj_range)
2.1496 -
2.1497 -lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a"
2.1498 -shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
2.1499 -by(fastsimp simp:surj_def dest!: endo_inj_surj)
2.1500 -
2.1501 -corollary infinite_UNIV_nat[iff]: "~finite(UNIV::nat set)"
2.1502 -proof
2.1503 -  assume "finite(UNIV::nat set)"
2.1504 -  with finite_UNIV_inj_surj[of Suc]
2.1505 -  show False by simp (blast dest: Suc_neq_Zero surjD)
2.1506 -qed
2.1507 -
2.1508 -(* Often leads to bogus ATP proofs because of reduced type information, hence noatp *)
2.1509 -lemma infinite_UNIV_char_0[noatp]:
2.1510 -  "\<not> finite (UNIV::'a::semiring_char_0 set)"
2.1511 -proof
2.1512 -  assume "finite (UNIV::'a set)"
2.1513 -  with subset_UNIV have "finite (range of_nat::'a set)"
2.1514 -    by (rule finite_subset)
2.1515 -  moreover have "inj (of_nat::nat \<Rightarrow> 'a)"
2.1516 -    by (simp add: inj_on_def)
2.1517 -  ultimately have "finite (UNIV::nat set)"
2.1518 -    by (rule finite_imageD)
2.1519 -  then show "False"
2.1520 -    by simp
2.1521 -qed
2.1522
2.1523  subsection{* A fold functional for non-empty sets *}
2.1524
2.1525 @@ -2811,561 +1354,6 @@
2.1526  qed
2.1527
2.1528
2.1529 -subsubsection {* Fold1 in lattices with @{const inf} and @{const sup} *}
2.1530 -
2.1531 -text{*
2.1532 -  As an application of @{text fold1} we define infimum
2.1533 -  and supremum in (not necessarily complete!) lattices
2.1534 -  over (non-empty) sets by means of @{text fold1}.
2.1535 -*}
2.1536 -
2.1537 -context semilattice_inf
2.1538 -begin
2.1539 -
2.1540 -lemma below_fold1_iff:
2.1541 -  assumes "finite A" "A \<noteq> {}"
2.1542 -  shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
2.1543 -proof -
2.1544 -  interpret ab_semigroup_idem_mult inf
2.1545 -    by (rule ab_semigroup_idem_mult_inf)
2.1546 -  show ?thesis using assms by (induct rule: finite_ne_induct) simp_all
2.1547 -qed
2.1548 -
2.1549 -lemma fold1_belowI:
2.1550 -  assumes "finite A"
2.1551 -    and "a \<in> A"
2.1552 -  shows "fold1 inf A \<le> a"
2.1553 -proof -
2.1554 -  from assms have "A \<noteq> {}" by auto
2.1555 -  from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
2.1556 -  proof (induct rule: finite_ne_induct)
2.1557 -    case singleton thus ?case by simp
2.1558 -  next
2.1559 -    interpret ab_semigroup_idem_mult inf
2.1560 -      by (rule ab_semigroup_idem_mult_inf)
2.1561 -    case (insert x F)
2.1562 -    from insert(5) have "a = x \<or> a \<in> F" by simp
2.1563 -    thus ?case
2.1564 -    proof
2.1565 -      assume "a = x" thus ?thesis using insert
2.1566 -        by (simp add: mult_ac)
2.1567 -    next
2.1568 -      assume "a \<in> F"
2.1569 -      hence bel: "fold1 inf F \<le> a" by (rule insert)
2.1570 -      have "inf (fold1 inf (insert x F)) a = inf x (inf (fold1 inf F) a)"
2.1571 -        using insert by (simp add: mult_ac)
2.1572 -      also have "inf (fold1 inf F) a = fold1 inf F"
2.1573 -        using bel by (auto intro: antisym)
2.1574 -      also have "inf x \<dots> = fold1 inf (insert x F)"
2.1575 -        using insert by (simp add: mult_ac)
2.1576 -      finally have aux: "inf (fold1 inf (insert x F)) a = fold1 inf (insert x F)" .
2.1577 -      moreover have "inf (fold1 inf (insert x F)) a \<le> a" by simp
2.1578 -      ultimately show ?thesis by simp
2.1579 -    qed
2.1580 -  qed
2.1581 -qed
2.1582 -
2.1583 -end
2.1584 -
2.1585 -context lattice
2.1586 -begin
2.1587 -
2.1588 -definition
2.1589 -  Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900)
2.1590 -where
2.1591 -  "Inf_fin = fold1 inf"
2.1592 -
2.1593 -definition
2.1594 -  Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900)
2.1595 -where
2.1596 -  "Sup_fin = fold1 sup"
2.1597 -
2.1598 -lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A"
2.1599 -apply(unfold Sup_fin_def Inf_fin_def)
2.1600 -apply(subgoal_tac "EX a. a:A")
2.1601 -prefer 2 apply blast
2.1602 -apply(erule exE)
2.1603 -apply(rule order_trans)
2.1604 -apply(erule (1) fold1_belowI)
2.1605 -apply(erule (1) semilattice_inf.fold1_belowI [OF dual_semilattice])
2.1606 -done
2.1607 -
2.1608 -lemma sup_Inf_absorb [simp]:
2.1609 -  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^bsub>fin\<^esub>A) = a"
2.1610 -apply(subst sup_commute)
2.1611 -apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI)
2.1612 -done
2.1613 -
2.1614 -lemma inf_Sup_absorb [simp]:
2.1615 -  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a"
2.1616 -by (simp add: Sup_fin_def inf_absorb1
2.1617 -  semilattice_inf.fold1_belowI [OF dual_semilattice])
2.1618 -
2.1619 -end
2.1620 -
2.1621 -context distrib_lattice
2.1622 -begin
2.1623 -
2.1624 -lemma sup_Inf1_distrib:
2.1625 -  assumes "finite A"
2.1626 -    and "A \<noteq> {}"
2.1627 -  shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
2.1628 -proof -
2.1629 -  interpret ab_semigroup_idem_mult inf
2.1630 -    by (rule ab_semigroup_idem_mult_inf)
2.1631 -  from assms show ?thesis
2.1632 -    by (simp add: Inf_fin_def image_def
2.1633 -      hom_fold1_commute [where h="sup x", OF sup_inf_distrib1])
2.1634 -        (rule arg_cong [where f="fold1 inf"], blast)
2.1635 -qed
2.1636 -
2.1637 -lemma sup_Inf2_distrib:
2.1638 -  assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
2.1639 -  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}"
2.1640 -using A proof (induct rule: finite_ne_induct)
2.1641 -  case singleton thus ?case
2.1642 -    by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
2.1643 -next
2.1644 -  interpret ab_semigroup_idem_mult inf
2.1645 -    by (rule ab_semigroup_idem_mult_inf)
2.1646 -  case (insert x A)
2.1647 -  have finB: "finite {sup x b |b. b \<in> B}"
2.1648 -    by(rule finite_surj[where f = "sup x", OF B(1)], auto)
2.1649 -  have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
2.1650 -  proof -
2.1651 -    have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
2.1652 -      by blast
2.1653 -    thus ?thesis by(simp add: insert(1) B(1))
2.1654 -  qed
2.1655 -  have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
2.1656 -  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)"
2.1657 -    using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def])
2.1658 -  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)
2.1659 -  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})"
2.1660 -    using insert by(simp add:sup_Inf1_distrib[OF B])
2.1661 -  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})"
2.1662 -    (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M")
2.1663 -    using B insert
2.1664 -    by (simp add: Inf_fin_def fold1_Un2 [OF finB _ finAB ne])
2.1665 -  also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
2.1666 -    by blast
2.1667 -  finally show ?case .
2.1668 -qed
2.1669 -
2.1670 -lemma inf_Sup1_distrib:
2.1671 -  assumes "finite A" and "A \<noteq> {}"
2.1672 -  shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
2.1673 -proof -
2.1674 -  interpret ab_semigroup_idem_mult sup
2.1675 -    by (rule ab_semigroup_idem_mult_sup)
2.1676 -  from assms show ?thesis
2.1677 -    by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1])
2.1678 -      (rule arg_cong [where f="fold1 sup"], blast)
2.1679 -qed
2.1680 -
2.1681 -lemma inf_Sup2_distrib:
2.1682 -  assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
2.1683 -  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}"
2.1684 -using A proof (induct rule: finite_ne_induct)
2.1685 -  case singleton thus ?case
2.1686 -    by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def])
2.1687 -next
2.1688 -  case (insert x A)
2.1689 -  have finB: "finite {inf x b |b. b \<in> B}"
2.1690 -    by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
2.1691 -  have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
2.1692 -  proof -
2.1693 -    have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
2.1694 -      by blast
2.1695 -    thus ?thesis by(simp add: insert(1) B(1))
2.1696 -  qed
2.1697 -  have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
2.1698 -  interpret ab_semigroup_idem_mult sup
2.1699 -    by (rule ab_semigroup_idem_mult_sup)
2.1700 -  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)"
2.1701 -    using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
2.1702 -  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)
2.1703 -  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})"
2.1704 -    using insert by(simp add:inf_Sup1_distrib[OF B])
2.1705 -  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})"
2.1706 -    (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M")
2.1707 -    using B insert
2.1708 -    by (simp add: Sup_fin_def fold1_Un2 [OF finB _ finAB ne])
2.1709 -  also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
2.1710 -    by blast
2.1711 -  finally show ?case .
2.1712 -qed
2.1713 -
2.1714 -end
2.1715 -
2.1716 -
2.1717 -subsubsection {* Fold1 in linear orders with @{const min} and @{const max} *}
2.1718 -
2.1719 -text{*
2.1720 -  As an application of @{text fold1} we define minimum
2.1721 -  and maximum in (not necessarily complete!) linear orders
2.1722 -  over (non-empty) sets by means of @{text fold1}.
2.1723 -*}
2.1724 -
2.1725 -context linorder
2.1726 -begin
2.1727 -
2.1728 -lemma ab_semigroup_idem_mult_min:
2.1729 -  "ab_semigroup_idem_mult min"
2.1730 -  proof qed (auto simp add: min_def)
2.1731 -
2.1732 -lemma ab_semigroup_idem_mult_max:
2.1733 -  "ab_semigroup_idem_mult max"
2.1734 -  proof qed (auto simp add: max_def)
2.1735 -
2.1736 -lemma max_lattice:
2.1737 -  "semilattice_inf (op \<ge>) (op >) max"
2.1738 -  by (fact min_max.dual_semilattice)
2.1739 -
2.1740 -lemma dual_max:
2.1741 -  "ord.max (op \<ge>) = min"
2.1742 -  by (auto simp add: ord.max_def_raw min_def expand_fun_eq)
2.1743 -
2.1744 -lemma dual_min:
2.1745 -  "ord.min (op \<ge>) = max"
2.1746 -  by (auto simp add: ord.min_def_raw max_def expand_fun_eq)
2.1747 -
2.1748 -lemma strict_below_fold1_iff:
2.1749 -  assumes "finite A" and "A \<noteq> {}"
2.1750 -  shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
2.1751 -proof -
2.1752 -  interpret ab_semigroup_idem_mult min
2.1753 -    by (rule ab_semigroup_idem_mult_min)
2.1754 -  from assms show ?thesis
2.1755 -  by (induct rule: finite_ne_induct)
2.1757 -qed
2.1758 -
2.1759 -lemma fold1_below_iff:
2.1760 -  assumes "finite A" and "A \<noteq> {}"
2.1761 -  shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
2.1762 -proof -
2.1763 -  interpret ab_semigroup_idem_mult min
2.1764 -    by (rule ab_semigroup_idem_mult_min)
2.1765 -  from assms show ?thesis
2.1766 -  by (induct rule: finite_ne_induct)
2.1767 -    (simp_all add: fold1_insert min_le_iff_disj)
2.1768 -qed
2.1769 -
2.1770 -lemma fold1_strict_below_iff:
2.1771 -  assumes "finite A" and "A \<noteq> {}"
2.1772 -  shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
2.1773 -proof -
2.1774 -  interpret ab_semigroup_idem_mult min
2.1775 -    by (rule ab_semigroup_idem_mult_min)
2.1776 -  from assms show ?thesis
2.1777 -  by (induct rule: finite_ne_induct)
2.1778 -    (simp_all add: fold1_insert min_less_iff_disj)
2.1779 -qed
2.1780 -
2.1781 -lemma fold1_antimono:
2.1782 -  assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
2.1783 -  shows "fold1 min B \<le> fold1 min A"
2.1784 -proof cases
2.1785 -  assume "A = B" thus ?thesis by simp
2.1786 -next
2.1787 -  interpret ab_semigroup_idem_mult min
2.1788 -    by (rule ab_semigroup_idem_mult_min)
2.1789 -  assume "A \<noteq> B"
2.1790 -  have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
2.1791 -  have "fold1 min B = fold1 min (A \<union> (B-A))" by(subst B)(rule refl)
2.1792 -  also have "\<dots> = min (fold1 min A) (fold1 min (B-A))"
2.1793 -  proof -
2.1794 -    have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
2.1795 -    moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`]) (* by(blast intro:finite_Diff prems) fails *)
2.1796 -    moreover have "(B-A) \<noteq> {}" using prems by blast
2.1797 -    moreover have "A Int (B-A) = {}" using prems by blast
2.1798 -    ultimately show ?thesis using `A \<noteq> {}` by (rule_tac fold1_Un)
2.1799 -  qed
2.1800 -  also have "\<dots> \<le> fold1 min A" by (simp add: min_le_iff_disj)
2.1801 -  finally show ?thesis .
2.1802 -qed
2.1803 -
2.1804 -definition
2.1805 -  Min :: "'a set \<Rightarrow> 'a"
2.1806 -where
2.1807 -  "Min = fold1 min"
2.1808 -
2.1809 -definition
2.1810 -  Max :: "'a set \<Rightarrow> 'a"
2.1811 -where
2.1812 -  "Max = fold1 max"
2.1813 -
2.1814 -lemmas Min_singleton [simp] = fold1_singleton_def [OF Min_def]
2.1815 -lemmas Max_singleton [simp] = fold1_singleton_def [OF Max_def]
2.1816 -
2.1817 -lemma Min_insert [simp]:
2.1818 -  assumes "finite A" and "A \<noteq> {}"
2.1819 -  shows "Min (insert x A) = min x (Min A)"
2.1820 -proof -
2.1821 -  interpret ab_semigroup_idem_mult min
2.1822 -    by (rule ab_semigroup_idem_mult_min)
2.1823 -  from assms show ?thesis by (rule fold1_insert_idem_def [OF Min_def])
2.1824 -qed
2.1825 -
2.1826 -lemma Max_insert [simp]:
2.1827 -  assumes "finite A" and "A \<noteq> {}"
2.1828 -  shows "Max (insert x A) = max x (Max A)"
2.1829 -proof -
2.1830 -  interpret ab_semigroup_idem_mult max
2.1831 -    by (rule ab_semigroup_idem_mult_max)
2.1832 -  from assms show ?thesis by (rule fold1_insert_idem_def [OF Max_def])
2.1833 -qed
2.1834 -
2.1835 -lemma Min_in [simp]:
2.1836 -  assumes "finite A" and "A \<noteq> {}"
2.1837 -  shows "Min A \<in> A"
2.1838 -proof -
2.1839 -  interpret ab_semigroup_idem_mult min
2.1840 -    by (rule ab_semigroup_idem_mult_min)
2.1841 -  from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def)
2.1842 -qed
2.1843 -
2.1844 -lemma Max_in [simp]:
2.1845 -  assumes "finite A" and "A \<noteq> {}"
2.1846 -  shows "Max A \<in> A"
2.1847 -proof -
2.1848 -  interpret ab_semigroup_idem_mult max
2.1849 -    by (rule ab_semigroup_idem_mult_max)
2.1850 -  from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
2.1851 -qed
2.1852 -
2.1853 -lemma Min_Un:
2.1854 -  assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
2.1855 -  shows "Min (A \<union> B) = min (Min A) (Min B)"
2.1856 -proof -
2.1857 -  interpret ab_semigroup_idem_mult min
2.1858 -    by (rule ab_semigroup_idem_mult_min)
2.1859 -  from assms show ?thesis
2.1860 -    by (simp add: Min_def fold1_Un2)
2.1861 -qed
2.1862 -
2.1863 -lemma Max_Un:
2.1864 -  assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
2.1865 -  shows "Max (A \<union> B) = max (Max A) (Max B)"
2.1866 -proof -
2.1867 -  interpret ab_semigroup_idem_mult max
2.1868 -    by (rule ab_semigroup_idem_mult_max)
2.1869 -  from assms show ?thesis
2.1870 -    by (simp add: Max_def fold1_Un2)
2.1871 -qed
2.1872 -
2.1873 -lemma hom_Min_commute:
2.1874 -  assumes "\<And>x y. h (min x y) = min (h x) (h y)"
2.1875 -    and "finite N" and "N \<noteq> {}"
2.1876 -  shows "h (Min N) = Min (h ` N)"
2.1877 -proof -
2.1878 -  interpret ab_semigroup_idem_mult min
2.1879 -    by (rule ab_semigroup_idem_mult_min)
2.1880 -  from assms show ?thesis
2.1881 -    by (simp add: Min_def hom_fold1_commute)
2.1882 -qed
2.1883 -
2.1884 -lemma hom_Max_commute:
2.1885 -  assumes "\<And>x y. h (max x y) = max (h x) (h y)"
2.1886 -    and "finite N" and "N \<noteq> {}"
2.1887 -  shows "h (Max N) = Max (h ` N)"
2.1888 -proof -
2.1889 -  interpret ab_semigroup_idem_mult max
2.1890 -    by (rule ab_semigroup_idem_mult_max)
2.1891 -  from assms show ?thesis
2.1892 -    by (simp add: Max_def hom_fold1_commute [of h])
2.1893 -qed
2.1894 -
2.1895 -lemma Min_le [simp]:
2.1896 -  assumes "finite A" and "x \<in> A"
2.1897 -  shows "Min A \<le> x"
2.1898 -  using assms by (simp add: Min_def min_max.fold1_belowI)
2.1899 -
2.1900 -lemma Max_ge [simp]:
2.1901 -  assumes "finite A" and "x \<in> A"
2.1902 -  shows "x \<le> Max A"
2.1903 -proof -
2.1904 -  interpret semilattice_inf "op \<ge>" "op >" max
2.1905 -    by (rule max_lattice)
2.1906 -  from assms show ?thesis by (simp add: Max_def fold1_belowI)
2.1907 -qed
2.1908 -
2.1909 -lemma Min_ge_iff [simp, noatp]:
2.1910 -  assumes "finite A" and "A \<noteq> {}"
2.1911 -  shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
2.1912 -  using assms by (simp add: Min_def min_max.below_fold1_iff)
2.1913 -
2.1914 -lemma Max_le_iff [simp, noatp]:
2.1915 -  assumes "finite A" and "A \<noteq> {}"
2.1916 -  shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
2.1917 -proof -
2.1918 -  interpret semilattice_inf "op \<ge>" "op >" max
2.1919 -    by (rule max_lattice)
2.1920 -  from assms show ?thesis by (simp add: Max_def below_fold1_iff)
2.1921 -qed
2.1922 -
2.1923 -lemma Min_gr_iff [simp, noatp]:
2.1924 -  assumes "finite A" and "A \<noteq> {}"
2.1925 -  shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
2.1926 -  using assms by (simp add: Min_def strict_below_fold1_iff)
2.1927 -
2.1928 -lemma Max_less_iff [simp, noatp]:
2.1929 -  assumes "finite A" and "A \<noteq> {}"
2.1930 -  shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
2.1931 -proof -
2.1932 -  interpret dual: linorder "op \<ge>" "op >"
2.1933 -    by (rule dual_linorder)
2.1934 -  from assms show ?thesis
2.1935 -    by (simp add: Max_def dual.strict_below_fold1_iff [folded dual.dual_max])
2.1936 -qed
2.1937 -
2.1938 -lemma Min_le_iff [noatp]:
2.1939 -  assumes "finite A" and "A \<noteq> {}"
2.1940 -  shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
2.1941 -  using assms by (simp add: Min_def fold1_below_iff)
2.1942 -
2.1943 -lemma Max_ge_iff [noatp]:
2.1944 -  assumes "finite A" and "A \<noteq> {}"
2.1945 -  shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
2.1946 -proof -
2.1947 -  interpret dual: linorder "op \<ge>" "op >"
2.1948 -    by (rule dual_linorder)
2.1949 -  from assms show ?thesis
2.1950 -    by (simp add: Max_def dual.fold1_below_iff [folded dual.dual_max])
2.1951 -qed
2.1952 -
2.1953 -lemma Min_less_iff [noatp]:
2.1954 -  assumes "finite A" and "A \<noteq> {}"
2.1955 -  shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
2.1956 -  using assms by (simp add: Min_def fold1_strict_below_iff)
2.1957 -
2.1958 -lemma Max_gr_iff [noatp]:
2.1959 -  assumes "finite A" and "A \<noteq> {}"
2.1960 -  shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
2.1961 -proof -
2.1962 -  interpret dual: linorder "op \<ge>" "op >"
2.1963 -    by (rule dual_linorder)
2.1964 -  from assms show ?thesis
2.1965 -    by (simp add: Max_def dual.fold1_strict_below_iff [folded dual.dual_max])
2.1966 -qed
2.1967 -
2.1968 -lemma Min_eqI:
2.1969 -  assumes "finite A"
2.1970 -  assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
2.1971 -    and "x \<in> A"
2.1972 -  shows "Min A = x"
2.1973 -proof (rule antisym)
2.1974 -  from `x \<in> A` have "A \<noteq> {}" by auto
2.1975 -  with assms show "Min A \<ge> x" by simp
2.1976 -next
2.1977 -  from assms show "x \<ge> Min A" by simp
2.1978 -qed
2.1979 -
2.1980 -lemma Max_eqI:
2.1981 -  assumes "finite A"
2.1982 -  assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
2.1983 -    and "x \<in> A"
2.1984 -  shows "Max A = x"
2.1985 -proof (rule antisym)
2.1986 -  from `x \<in> A` have "A \<noteq> {}" by auto
2.1987 -  with assms show "Max A \<le> x" by simp
2.1988 -next
2.1989 -  from assms show "x \<le> Max A" by simp
2.1990 -qed
2.1991 -
2.1992 -lemma Min_antimono:
2.1993 -  assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
2.1994 -  shows "Min N \<le> Min M"
2.1995 -  using assms by (simp add: Min_def fold1_antimono)
2.1996 -
2.1997 -lemma Max_mono:
2.1998 -  assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
2.1999 -  shows "Max M \<le> Max N"
2.2000 -proof -
2.2001 -  interpret dual: linorder "op \<ge>" "op >"
2.2002 -    by (rule dual_linorder)
2.2003 -  from assms show ?thesis
2.2004 -    by (simp add: Max_def dual.fold1_antimono [folded dual.dual_max])
2.2005 -qed
2.2006 -
2.2007 -lemma finite_linorder_max_induct[consumes 1, case_names empty insert]:
2.2008 - "finite A \<Longrightarrow> P {} \<Longrightarrow>
2.2009 -  (!!b A. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
2.2010 -  \<Longrightarrow> P A"
2.2011 -proof (induct rule: finite_psubset_induct)
2.2012 -  fix A :: "'a set"
2.2013 -  assume IH: "!! B. finite B \<Longrightarrow> B < A \<Longrightarrow> P {} \<Longrightarrow>
2.2014 -                 (!!b A. finite A \<Longrightarrow> (\<forall>a\<in>A. a<b) \<Longrightarrow> P A \<Longrightarrow> P (insert b A))
2.2015 -                  \<Longrightarrow> P B"
2.2016 -  and "finite A" and "P {}"
2.2017 -  and step: "!!b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
2.2018 -  show "P A"
2.2019 -  proof (cases "A = {}")
2.2020 -    assume "A = {}" thus "P A" using `P {}` by simp
2.2021 -  next
2.2022 -    let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B"
2.2023 -    assume "A \<noteq> {}"
2.2024 -    with `finite A` have "Max A : A" by auto
2.2025 -    hence A: "?A = A" using insert_Diff_single insert_absorb by auto
2.2026 -    moreover have "finite ?B" using `finite A` by simp
2.2027 -    ultimately have "P ?B" using `P {}` step IH[of ?B] by blast
2.2028 -    moreover have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastsimp
2.2029 -    ultimately show "P A" using A insert_Diff_single step[OF `finite ?B`] by fastsimp
2.2030 -  qed
2.2031 -qed
2.2032 -
2.2033 -lemma finite_linorder_min_induct[consumes 1, case_names empty insert]:
2.2034 - "\<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"
2.2035 -by(rule linorder.finite_linorder_max_induct[OF dual_linorder])
2.2036 -
2.2037 -end
2.2038 -
2.2040 -begin
2.2041 -
2.2043 -  fixes k
2.2044 -  assumes "finite N" and "N \<noteq> {}"
2.2045 -  shows "k + Min N = Min {k + m | m. m \<in> N}"
2.2046 -proof -
2.2047 -  have "\<And>x y. k + min x y = min (k + x) (k + y)"
2.2048 -    by (simp add: min_def not_le)
2.2049 -      (blast intro: antisym less_imp_le add_left_mono)
2.2050 -  with assms show ?thesis
2.2051 -    using hom_Min_commute [of "plus k" N]
2.2052 -    by simp (blast intro: arg_cong [where f = Min])
2.2053 -qed
2.2054 -
2.2056 -  fixes k
2.2057 -  assumes "finite N" and "N \<noteq> {}"
2.2058 -  shows "k + Max N = Max {k + m | m. m \<in> N}"
2.2059 -proof -
2.2060 -  have "\<And>x y. k + max x y = max (k + x) (k + y)"
2.2061 -    by (simp add: max_def not_le)
2.2062 -      (blast intro: antisym less_imp_le add_left_mono)
2.2063 -  with assms show ?thesis
2.2064 -    using hom_Max_commute [of "plus k" N]
2.2065 -    by simp (blast intro: arg_cong [where f = Max])
2.2066 -qed
2.2067 -
2.2068 -end
2.2069 -
2.2071 -begin
2.2072 -
2.2073 -lemma minus_Max_eq_Min [simp]:
2.2074 -  "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Max S) = Min (uminus ` S)"
2.2075 -  by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min)
2.2076 -
2.2077 -lemma minus_Min_eq_Max [simp]:
2.2078 -  "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Min S) = Max (uminus ` S)"
2.2079 -  by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max)
2.2080 -
2.2081 -end
2.2082 -
2.2083 -
2.2084  subsection {* Expressing set operations via @{const fold} *}
2.2085
2.2086  lemma (in fun_left_comm) fun_left_comm_apply:
2.2087 @@ -3445,32 +1433,6 @@
2.2088    shows "Sup A = fold sup bot A"
2.2089    using assms sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2)
2.2090
2.2091 -lemma Inf_fin_Inf:
2.2092 -  assumes "finite A" and "A \<noteq> {}"
2.2093 -  shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
2.2094 -proof -
2.2095 -  interpret ab_semigroup_idem_mult inf
2.2096 -    by (rule ab_semigroup_idem_mult_inf)
2.2097 -  from `A \<noteq> {}` obtain b B where "A = insert b B" by auto
2.2098 -  moreover with `finite A` have "finite B" by simp
2.2099 -  ultimately show ?thesis
2.2100 -  by (simp add: Inf_fin_def fold1_eq_fold_idem inf_Inf_fold_inf [symmetric])
2.2102 -qed
2.2103 -
2.2104 -lemma Sup_fin_Sup:
2.2105 -  assumes "finite A" and "A \<noteq> {}"
2.2106 -  shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
2.2107 -proof -
2.2108 -  interpret ab_semigroup_idem_mult sup
2.2109 -    by (rule ab_semigroup_idem_mult_sup)
2.2110 -  from `A \<noteq> {}` obtain b B where "A = insert b B" by auto
2.2111 -  moreover with `finite A` have "finite B" by simp
2.2112 -  ultimately show ?thesis
2.2113 -  by (simp add: Sup_fin_def fold1_eq_fold_idem sup_Sup_fold_sup [symmetric])
2.2115 -qed
2.2116 -
2.2117  lemma inf_INFI_fold_inf:
2.2118    assumes "finite A"
2.2119    shows "inf B (INFI A f) = fold (\<lambda>A. inf (f A)) B A" (is "?inf = ?fold")
2.2120 @@ -3505,4 +1467,127 @@
2.2121
2.2122  end
2.2123
2.2124 +
2.2125 +subsection {* Locales as mini-packages *}
2.2126 +
2.2127 +locale folding =
2.2128 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
2.2129 +  fixes F :: "'a set \<Rightarrow> 'b \<Rightarrow> 'b"
2.2130 +  assumes commute_comp: "f x \<circ> f y = f y \<circ> f x"
2.2131 +  assumes eq_fold: "F A s = Finite_Set.fold f s A"
2.2132 +begin
2.2133 +
2.2134 +lemma fun_left_commute:
2.2135 +  "f x (f y s) = f y (f x s)"
2.2136 +  using commute_comp [of x y] by (simp add: expand_fun_eq)
2.2137 +
2.2138 +lemma fun_left_comm:
2.2139 +  "fun_left_comm f"
2.2140 +proof
2.2141 +qed (fact fun_left_commute)
2.2142 +
2.2143 +lemma empty [simp]:
2.2144 +  "F {} = id"
2.2145 +  by (simp add: eq_fold expand_fun_eq)
2.2146 +
2.2147 +lemma insert [simp]:
2.2148 +  assumes "finite A" and "x \<notin> A"
2.2149 +  shows "F (insert x A) = F A \<circ> f x"
2.2150 +proof -
2.2151 +  interpret fun_left_comm f by (fact fun_left_comm)
2.2152 +  from fold_insert2 assms
2.2153 +  have "\<And>s. Finite_Set.fold f s (insert x A) = Finite_Set.fold f (f x s) A" .
2.2154 +  then show ?thesis by (simp add: eq_fold expand_fun_eq)
2.2155 +qed
2.2156 +
2.2157 +lemma remove:
2.2158 +  assumes "finite A" and "x \<in> A"
2.2159 +  shows "F A = F (A - {x}) \<circ> f x"
2.2160 +proof -
2.2161 +  from `x \<in> A` obtain B where A: "A = insert x B" and "x \<notin> B"
2.2162 +    by (auto dest: mk_disjoint_insert)
2.2163 +  moreover from `finite A` this have "finite B" by simp
2.2164 +  ultimately show ?thesis by simp
2.2165 +qed
2.2166 +
2.2167 +lemma insert_remove:
2.2168 +  assumes "finite A"
2.2169 +  shows "F (insert x A) = F (A - {x}) \<circ> f x"
2.2170 +proof (cases "x \<in> A")
2.2171 +  case True with assms show ?thesis by (simp add: remove insert_absorb)
2.2172 +next
2.2173 +  case False with assms show ?thesis by simp
2.2174 +qed
2.2175 +
2.2176 +lemma commute_comp':
2.2177 +  assumes "finite A"
2.2178 +  shows "f x \<circ> F A = F A \<circ> f x"
2.2179 +proof (rule ext)
2.2180 +  fix s
2.2181 +  from assms show "(f x \<circ> F A) s = (F A \<circ> f x) s"
2.2182 +    by (induct A arbitrary: s) (simp_all add: fun_left_commute)
2.2183 +qed
2.2184 +
2.2185 +lemma fun_left_commute':
2.2186 +  assumes "finite A"
2.2187 +  shows "f x (F A s) = F A (f x s)"
2.2188 +  using commute_comp' assms by (simp add: expand_fun_eq)
2.2189 +
2.2190 +lemma union:
2.2191 +  assumes "finite A" and "finite B"
2.2192 +  and "A \<inter> B = {}"
2.2193 +  shows "F (A \<union> B) = F A \<circ> F B"
2.2194 +using `finite A` `A \<inter> B = {}` proof (induct A)
2.2195 +  case empty show ?case by simp
2.2196 +next
2.2197 +  case (insert x A)
2.2198 +  then have "A \<inter> B = {}" by auto
2.2199 +  with insert(3) have "F (A \<union> B) = F A \<circ> F B" .
2.2200 +  moreover from insert have "x \<notin> B" by simp
2.2201 +  moreover from `finite A` `finite B` have fin: "finite (A \<union> B)" by simp
2.2202 +  moreover from `x \<notin> A` `x \<notin> B` have "x \<notin> A \<union> B" by simp
2.2203 +  ultimately show ?case by (simp add: fun_left_commute')
2.2204 +qed
2.2205 +
2.2206  end
2.2207 +
2.2208 +locale folding_idem = folding +
2.2209 +  assumes idem_comp: "f x \<circ> f x = f x"
2.2210 +begin
2.2211 +
2.2212 +declare insert [simp del]
2.2213 +
2.2214 +lemma fun_idem:
2.2215 +  "f x (f x s) = f x s"
2.2216 +  using idem_comp [of x] by (simp add: expand_fun_eq)
2.2217 +
2.2218 +lemma fun_left_comm_idem:
2.2219 +  "fun_left_comm_idem f"
2.2220 +proof
2.2221 +qed (fact fun_left_commute fun_idem)+
2.2222 +
2.2223 +lemma insert_idem [simp]:
2.2224 +  assumes "finite A"
2.2225 +  shows "F (insert x A) = F A \<circ> f x"
2.2226 +proof -
2.2227 +  interpret fun_left_comm_idem f by (fact fun_left_comm_idem)
2.2228 +  from fold_insert_idem2 assms
2.2229 +  have "\<And>s. Finite_Set.fold f s (insert x A) = Finite_Set.fold f (f x s) A" .
2.2230 +  then show ?thesis by (simp add: eq_fold expand_fun_eq)
2.2231 +qed
2.2232 +
2.2233 +lemma union_idem:
2.2234 +  assumes "finite A" and "finite B"
2.2235 +  shows "F (A \<union> B) = F A \<circ> F B"
2.2236 +using `finite A` proof (induct A)
2.2237 +  case empty show ?case by simp
2.2238 +next
2.2239 +  case (insert x A)
2.2240 +  from insert(3) have "F (A \<union> B) = F A \<circ> F B" .
2.2241 +  moreover from `finite A` `finite B` have fin: "finite (A \<union> B)" by simp
2.2242 +  ultimately show ?case by (simp add: fun_left_commute')
2.2243 +qed
2.2244 +
2.2245 +end
2.2246 +
2.2247 +end
```
```     3.1 --- a/src/HOL/IsaMakefile	Wed Mar 10 08:04:50 2010 +0100
3.2 +++ b/src/HOL/IsaMakefile	Wed Mar 10 16:53:27 2010 +0100
3.3 @@ -142,6 +142,7 @@
3.4  	@\$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false \$(OUT)/Pure HOL-Base
3.5
3.6  PLAIN_DEPENDENCIES = \$(BASE_DEPENDENCIES)\
3.7 +  Big_Operators.thy \
3.8    Complete_Lattice.thy \
3.9    Datatype.thy \
3.10    Extraction.thy \
```
```     4.1 --- a/src/HOL/Option.thy	Wed Mar 10 08:04:50 2010 +0100
4.2 +++ b/src/HOL/Option.thy	Wed Mar 10 16:53:27 2010 +0100
4.3 @@ -5,7 +5,7 @@
4.4  header {* Datatype option *}
4.5
4.6  theory Option
4.7 -imports Datatype Finite_Set
4.8 +imports Datatype
4.9  begin
4.10
4.11  datatype 'a option = None | Some 'a
4.12 @@ -33,13 +33,6 @@
4.13  lemma UNIV_option_conv: "UNIV = insert None (range Some)"
4.14  by(auto intro: classical)
4.15
4.16 -lemma finite_option_UNIV[simp]:
4.17 -  "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
4.18 -by(auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
4.19 -
4.20 -instance option :: (finite) finite proof
4.22 -
4.23
4.24  subsubsection {* Operations *}
4.25
```
```     5.1 --- a/src/HOL/Wellfounded.thy	Wed Mar 10 08:04:50 2010 +0100
5.2 +++ b/src/HOL/Wellfounded.thy	Wed Mar 10 16:53:27 2010 +0100
5.3 @@ -8,7 +8,7 @@