split off theory Big_Operators from theory Finite_Set
authorhaftmann
Wed Mar 10 16:53:27 2010 +0100 (2010-03-10)
changeset 3571999b6152aedf5
parent 35686 abf91fba0a70
child 35720 3fc79186a2f6
split off theory Big_Operators from theory Finite_Set
src/HOL/Big_Operators.thy
src/HOL/Finite_Set.thy
src/HOL/IsaMakefile
src/HOL/Option.thy
src/HOL/Wellfounded.thy
     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.17 +interpretation comm_monoid_add: comm_monoid_mult "op +" "0::'a::comm_monoid_add"
    1.18 +  proof qed (auto intro: add_assoc add_commute)
    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.71 +by (simp add: setsum_def)
    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.75 +by (simp add: setsum_def)
    1.76 +
    1.77 +lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0"
    1.78 +by (simp add: setsum_def)
    1.79 +
    1.80 +lemma setsum_reindex:
    1.81 +     "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
    1.82 +by(auto simp add: setsum_def comm_monoid_add.fold_image_reindex dest!:finite_imageD)
    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.152 +by(simp add:setsum_cong)
   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.157 +by(simp add: setsum_def comm_monoid_add.fold_image_Un_Int [symmetric])
   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.260 +by(simp add: setsum_def comm_monoid_add.fold_image_UN_disjoint cong: setsum_cong)
   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.278 +by(simp add:setsum_def comm_monoid_add.fold_image_Sigma split_def cong:setsum_cong)
   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.293 +by(simp add:setsum_def comm_monoid_add.fold_image_distrib)
   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.312 +apply (auto simp add:add_is_1)
   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.361 +  apply (rule comm_monoid_add.fold_image_Un_one)
   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.400 +apply (auto simp add: insert_Diff_if add_ac)
   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.471 +  fixes f :: "'a \<Rightarrow> 'b::{ordered_cancel_ab_semigroup_add,comm_monoid_add}"
   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.500 +  assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
   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.516 +  assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{ordered_ab_semigroup_add,comm_monoid_add})"
   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.532 +fixes f :: "'a \<Rightarrow> 'b :: {ordered_ab_semigroup_add_imp_le,comm_monoid_add}"
   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.537 +    by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
   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.546 +      0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==>
   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.552 +  apply (rule add_left_mono)
   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.684 +proof (simp add: setsum_cartesian_product)
   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.751 +by (simp add: setprod_def)
   1.752 +
   1.753 +lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
   1.754 +by (simp add: setprod_def)
   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.810 +by(simp add: setprod_def fold_image_Un_Int[symmetric])
   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.896 +by(simp add:setprod_def fold_image_distrib)
   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.1079 +by (simp add: card_Diff_singleton)
  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.1093 +by (simp add: card_insert_if)
  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.1103 +apply (simp add: card_Diff_singleton_if split add: split_if_asm)
  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.1114 +by(simp add:card_def setsum_Un_Int)
  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.1118 +by (simp add: card_Un_Int)
  1.1119 +
  1.1120 +lemma card_Diff_subset:
  1.1121 +  "finite B ==> B <= A ==> card (A - B) = card A - card B"
  1.1122 +by(simp add:card_def setsum_diff_nat)
  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.1350 +apply(simp add:card_insert_if split:if_splits)
  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.1382 +by(simp add:card_def setsum_Sigma del:setsum_constant)
  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.1392 +by (simp add: card_cartesian_product)
  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.1680 +    (simp add: Inf_fold_inf)
  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.1693 +    (simp add: Sup_fold_sup)
  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.1738 +    (simp_all add: fold1_insert)
  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.2021 +context linordered_ab_semigroup_add
  1.2022 +begin
  1.2023 +
  1.2024 +lemma add_Min_commute:
  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.2037 +lemma add_Max_commute:
  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.2052 +context linordered_ab_group_add
  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.19 +qed (simp add: UNIV_unit)
    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.27 +qed (simp add: UNIV_bool)
    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.39 +qed (simp add: UNIV_option_conv)
    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.60 -interpretation comm_monoid_add: comm_monoid_mult "op +" "0::'a::comm_monoid_add"
    2.61 -  proof qed (auto intro: add_assoc add_commute)
    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.114 -by (simp add: setsum_def)
   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.118 -by (simp add: setsum_def)
   2.119 -
   2.120 -lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0"
   2.121 -by (simp add: setsum_def)
   2.122 -
   2.123 -lemma setsum_reindex:
   2.124 -     "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
   2.125 -by(auto simp add: setsum_def comm_monoid_add.fold_image_reindex dest!:finite_imageD)
   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.195 -by(simp add:setsum_cong)
   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.200 -by(simp add: setsum_def comm_monoid_add.fold_image_Un_Int [symmetric])
   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.303 -by(simp add: setsum_def comm_monoid_add.fold_image_UN_disjoint cong: setsum_cong)
   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.321 -by(simp add:setsum_def comm_monoid_add.fold_image_Sigma split_def cong:setsum_cong)
   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.336 -by(simp add:setsum_def comm_monoid_add.fold_image_distrib)
   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.355 -apply (auto simp add:add_is_1)
   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.404 -  apply (rule comm_monoid_add.fold_image_Un_one)
   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.443 -apply (auto simp add: insert_Diff_if add_ac)
   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.514 -  fixes f :: "'a \<Rightarrow> 'b::{ordered_cancel_ab_semigroup_add,comm_monoid_add}"
   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.543 -  assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
   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.559 -  assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{ordered_ab_semigroup_add,comm_monoid_add})"
   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.575 -fixes f :: "'a \<Rightarrow> 'b :: {ordered_ab_semigroup_add_imp_le,comm_monoid_add}"
   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.580 -    by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
   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.589 -      0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==>
   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.595 -  apply (rule add_left_mono)
   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.727 -proof (simp add: setsum_cartesian_product)
   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.794 -by (simp add: setprod_def)
   2.795 -
   2.796 -lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
   2.797 -by (simp add: setprod_def)
   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.853 -by(simp add: setprod_def fold_image_Un_Int[symmetric])
   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.939 -by(simp add:setprod_def fold_image_distrib)
   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.1122 -by (simp add: card_Diff_singleton)
  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.1136 -by (simp add: card_insert_if)
  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.1146 -apply (simp add: card_Diff_singleton_if split add: split_if_asm)
  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.1157 -by(simp add:card_def setsum_Un_Int)
  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.1161 -by (simp add: card_Un_Int)
  2.1162 -
  2.1163 -lemma card_Diff_subset:
  2.1164 -  "finite B ==> B <= A ==> card (A - B) = card A - card B"
  2.1165 -by(simp add:card_def setsum_diff_nat)
  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.1393 -apply(simp add:card_insert_if split:if_splits)
  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.1425 -by(simp add:card_def setsum_Sigma del:setsum_constant)
  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.1435 -by (simp add: card_cartesian_product)
  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.1756 -    (simp_all add: fold1_insert)
  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.2039 -context linordered_ab_semigroup_add
  2.2040 -begin
  2.2041 -
  2.2042 -lemma add_Min_commute:
  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.2055 -lemma add_Max_commute:
  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.2070 -context linordered_ab_group_add
  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.2101 -    (simp add: Inf_fold_inf)
  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.2114 -    (simp add: Sup_fold_sup)
  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.21 -qed (simp add: UNIV_option_conv)
    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 @@
     5.4  header {*Well-founded Recursion*}
     5.5  
     5.6  theory Wellfounded
     5.7 -imports Finite_Set Transitive_Closure
     5.8 +imports Transitive_Closure Big_Operators
     5.9  uses ("Tools/Function/size.ML")
    5.10  begin
    5.11