src/HOL/Finite_Set.thy
changeset 35719 99b6152aedf5
parent 35577 43b93e294522
child 35722 69419a09a7ff
     1.1 --- a/src/HOL/Finite_Set.thy	Wed Mar 10 08:04:50 2010 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Wed Mar 10 16:53:27 2010 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Finite sets *}
     1.5  
     1.6  theory Finite_Set
     1.7 -imports Power Product_Type Sum_Type
     1.8 +imports Power Option
     1.9  begin
    1.10  
    1.11  subsection {* Definition and basic properties *}
    1.12 @@ -527,17 +527,24 @@
    1.13  lemma UNIV_unit [noatp]:
    1.14    "UNIV = {()}" by auto
    1.15  
    1.16 -instance unit :: finite
    1.17 -  by default (simp add: UNIV_unit)
    1.18 +instance unit :: finite proof
    1.19 +qed (simp add: UNIV_unit)
    1.20  
    1.21  lemma UNIV_bool [noatp]:
    1.22    "UNIV = {False, True}" by auto
    1.23  
    1.24 -instance bool :: finite
    1.25 -  by default (simp add: UNIV_bool)
    1.26 +instance bool :: finite proof
    1.27 +qed (simp add: UNIV_bool)
    1.28 +
    1.29 +instance * :: (finite, finite) finite proof
    1.30 +qed (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
    1.31  
    1.32 -instance * :: (finite, finite) finite
    1.33 -  by default (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
    1.34 +lemma finite_option_UNIV [simp]:
    1.35 +  "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
    1.36 +  by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
    1.37 +
    1.38 +instance option :: (finite) finite proof
    1.39 +qed (simp add: UNIV_option_conv)
    1.40  
    1.41  lemma inj_graph: "inj (%f. {(x, y). y = f x})"
    1.42    by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
    1.43 @@ -556,8 +563,8 @@
    1.44    qed
    1.45  qed
    1.46  
    1.47 -instance "+" :: (finite, finite) finite
    1.48 -  by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
    1.49 +instance "+" :: (finite, finite) finite proof
    1.50 +qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
    1.51  
    1.52  
    1.53  subsection {* A fold functional for finite sets *}
    1.54 @@ -1053,1470 +1060,6 @@
    1.55  
    1.56  end
    1.57  
    1.58 -subsection {* Generalized summation over a set *}
    1.59 -
    1.60 -interpretation comm_monoid_add: comm_monoid_mult "op +" "0::'a::comm_monoid_add"
    1.61 -  proof qed (auto intro: add_assoc add_commute)
    1.62 -
    1.63 -definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
    1.64 -where "setsum f A == if finite A then fold_image (op +) f 0 A else 0"
    1.65 -
    1.66 -abbreviation
    1.67 -  Setsum  ("\<Sum>_" [1000] 999) where
    1.68 -  "\<Sum>A == setsum (%x. x) A"
    1.69 -
    1.70 -text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
    1.71 -written @{text"\<Sum>x\<in>A. e"}. *}
    1.72 -
    1.73 -syntax
    1.74 -  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
    1.75 -syntax (xsymbols)
    1.76 -  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
    1.77 -syntax (HTML output)
    1.78 -  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
    1.79 -
    1.80 -translations -- {* Beware of argument permutation! *}
    1.81 -  "SUM i:A. b" == "CONST setsum (%i. b) A"
    1.82 -  "\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
    1.83 -
    1.84 -text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
    1.85 - @{text"\<Sum>x|P. e"}. *}
    1.86 -
    1.87 -syntax
    1.88 -  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
    1.89 -syntax (xsymbols)
    1.90 -  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
    1.91 -syntax (HTML output)
    1.92 -  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
    1.93 -
    1.94 -translations
    1.95 -  "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
    1.96 -  "\<Sum>x|P. t" => "CONST setsum (%x. t) {x. P}"
    1.97 -
    1.98 -print_translation {*
    1.99 -let
   1.100 -  fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
   1.101 -        if x <> y then raise Match
   1.102 -        else
   1.103 -          let
   1.104 -            val x' = Syntax.mark_bound x;
   1.105 -            val t' = subst_bound (x', t);
   1.106 -            val P' = subst_bound (x', P);
   1.107 -          in Syntax.const @{syntax_const "_qsetsum"} $ Syntax.mark_bound x $ P' $ t' end
   1.108 -    | setsum_tr' _ = raise Match;
   1.109 -in [(@{const_syntax setsum}, setsum_tr')] end
   1.110 -*}
   1.111 -
   1.112 -
   1.113 -lemma setsum_empty [simp]: "setsum f {} = 0"
   1.114 -by (simp add: setsum_def)
   1.115 -
   1.116 -lemma setsum_insert [simp]:
   1.117 -  "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   1.118 -by (simp add: setsum_def)
   1.119 -
   1.120 -lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0"
   1.121 -by (simp add: setsum_def)
   1.122 -
   1.123 -lemma setsum_reindex:
   1.124 -     "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
   1.125 -by(auto simp add: setsum_def comm_monoid_add.fold_image_reindex dest!:finite_imageD)
   1.126 -
   1.127 -lemma setsum_reindex_id:
   1.128 -     "inj_on f B ==> setsum f B = setsum id (f ` B)"
   1.129 -by (auto simp add: setsum_reindex)
   1.130 -
   1.131 -lemma setsum_reindex_nonzero: 
   1.132 -  assumes fS: "finite S"
   1.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"
   1.134 -  shows "setsum h (f ` S) = setsum (h o f) S"
   1.135 -using nz
   1.136 -proof(induct rule: finite_induct[OF fS])
   1.137 -  case 1 thus ?case by simp
   1.138 -next
   1.139 -  case (2 x F) 
   1.140 -  {assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto
   1.141 -    then obtain y where y: "y \<in> F" "f x = f y" by auto 
   1.142 -    from "2.hyps" y have xy: "x \<noteq> y" by auto
   1.143 -    
   1.144 -    from "2.prems"[of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp
   1.145 -    have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto
   1.146 -    also have "\<dots> = setsum (h o f) (insert x F)" 
   1.147 -      unfolding setsum_insert[OF `finite F` `x\<notin>F`]
   1.148 -      using h0 
   1.149 -      apply simp
   1.150 -      apply (rule "2.hyps"(3))
   1.151 -      apply (rule_tac y="y" in  "2.prems")
   1.152 -      apply simp_all
   1.153 -      done
   1.154 -    finally have ?case .}
   1.155 -  moreover
   1.156 -  {assume fxF: "f x \<notin> f ` F"
   1.157 -    have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)" 
   1.158 -      using fxF "2.hyps" by simp 
   1.159 -    also have "\<dots> = setsum (h o f) (insert x F)"
   1.160 -      unfolding setsum_insert[OF `finite F` `x\<notin>F`]
   1.161 -      apply simp
   1.162 -      apply (rule cong[OF refl[of "op + (h (f x))"]])
   1.163 -      apply (rule "2.hyps"(3))
   1.164 -      apply (rule_tac y="y" in  "2.prems")
   1.165 -      apply simp_all
   1.166 -      done
   1.167 -    finally have ?case .}
   1.168 -  ultimately show ?case by blast
   1.169 -qed
   1.170 -
   1.171 -lemma setsum_cong:
   1.172 -  "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
   1.173 -by(fastsimp simp: setsum_def intro: comm_monoid_add.fold_image_cong)
   1.174 -
   1.175 -lemma strong_setsum_cong[cong]:
   1.176 -  "A = B ==> (!!x. x:B =simp=> f x = g x)
   1.177 -   ==> setsum (%x. f x) A = setsum (%x. g x) B"
   1.178 -by(fastsimp simp: simp_implies_def setsum_def intro: comm_monoid_add.fold_image_cong)
   1.179 -
   1.180 -lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A"
   1.181 -by (rule setsum_cong[OF refl], auto)
   1.182 -
   1.183 -lemma setsum_reindex_cong:
   1.184 -   "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|] 
   1.185 -    ==> setsum h B = setsum g A"
   1.186 -by (simp add: setsum_reindex cong: setsum_cong)
   1.187 -
   1.188 -
   1.189 -lemma setsum_0[simp]: "setsum (%i. 0) A = 0"
   1.190 -apply (clarsimp simp: setsum_def)
   1.191 -apply (erule finite_induct, auto)
   1.192 -done
   1.193 -
   1.194 -lemma setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0"
   1.195 -by(simp add:setsum_cong)
   1.196 -
   1.197 -lemma setsum_Un_Int: "finite A ==> finite B ==>
   1.198 -  setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
   1.199 -  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   1.200 -by(simp add: setsum_def comm_monoid_add.fold_image_Un_Int [symmetric])
   1.201 -
   1.202 -lemma setsum_Un_disjoint: "finite A ==> finite B
   1.203 -  ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
   1.204 -by (subst setsum_Un_Int [symmetric], auto)
   1.205 -
   1.206 -lemma setsum_mono_zero_left: 
   1.207 -  assumes fT: "finite T" and ST: "S \<subseteq> T"
   1.208 -  and z: "\<forall>i \<in> T - S. f i = 0"
   1.209 -  shows "setsum f S = setsum f T"
   1.210 -proof-
   1.211 -  have eq: "T = S \<union> (T - S)" using ST by blast
   1.212 -  have d: "S \<inter> (T - S) = {}" using ST by blast
   1.213 -  from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
   1.214 -  show ?thesis 
   1.215 -  by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
   1.216 -qed
   1.217 -
   1.218 -lemma setsum_mono_zero_right: 
   1.219 -  "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. f i = 0 \<Longrightarrow> setsum f T = setsum f S"
   1.220 -by(blast intro!: setsum_mono_zero_left[symmetric])
   1.221 -
   1.222 -lemma setsum_mono_zero_cong_left: 
   1.223 -  assumes fT: "finite T" and ST: "S \<subseteq> T"
   1.224 -  and z: "\<forall>i \<in> T - S. g i = 0"
   1.225 -  and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
   1.226 -  shows "setsum f S = setsum g T"
   1.227 -proof-
   1.228 -  have eq: "T = S \<union> (T - S)" using ST by blast
   1.229 -  have d: "S \<inter> (T - S) = {}" using ST by blast
   1.230 -  from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
   1.231 -  show ?thesis 
   1.232 -    using fg by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z])
   1.233 -qed
   1.234 -
   1.235 -lemma setsum_mono_zero_cong_right: 
   1.236 -  assumes fT: "finite T" and ST: "S \<subseteq> T"
   1.237 -  and z: "\<forall>i \<in> T - S. f i = 0"
   1.238 -  and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
   1.239 -  shows "setsum f T = setsum g S"
   1.240 -using setsum_mono_zero_cong_left[OF fT ST z] fg[symmetric] by auto 
   1.241 -
   1.242 -lemma setsum_delta: 
   1.243 -  assumes fS: "finite S"
   1.244 -  shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
   1.245 -proof-
   1.246 -  let ?f = "(\<lambda>k. if k=a then b k else 0)"
   1.247 -  {assume a: "a \<notin> S"
   1.248 -    hence "\<forall> k\<in> S. ?f k = 0" by simp
   1.249 -    hence ?thesis  using a by simp}
   1.250 -  moreover 
   1.251 -  {assume a: "a \<in> S"
   1.252 -    let ?A = "S - {a}"
   1.253 -    let ?B = "{a}"
   1.254 -    have eq: "S = ?A \<union> ?B" using a by blast 
   1.255 -    have dj: "?A \<inter> ?B = {}" by simp
   1.256 -    from fS have fAB: "finite ?A" "finite ?B" by auto  
   1.257 -    have "setsum ?f S = setsum ?f ?A + setsum ?f ?B"
   1.258 -      using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
   1.259 -      by simp
   1.260 -    then have ?thesis  using a by simp}
   1.261 -  ultimately show ?thesis by blast
   1.262 -qed
   1.263 -lemma setsum_delta': 
   1.264 -  assumes fS: "finite S" shows 
   1.265 -  "setsum (\<lambda>k. if a = k then b k else 0) S = 
   1.266 -     (if a\<in> S then b a else 0)"
   1.267 -  using setsum_delta[OF fS, of a b, symmetric] 
   1.268 -  by (auto intro: setsum_cong)
   1.269 -
   1.270 -lemma setsum_restrict_set:
   1.271 -  assumes fA: "finite A"
   1.272 -  shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A"
   1.273 -proof-
   1.274 -  from fA have fab: "finite (A \<inter> B)" by auto
   1.275 -  have aba: "A \<inter> B \<subseteq> A" by blast
   1.276 -  let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0"
   1.277 -  from setsum_mono_zero_left[OF fA aba, of ?g]
   1.278 -  show ?thesis by simp
   1.279 -qed
   1.280 -
   1.281 -lemma setsum_cases:
   1.282 -  assumes fA: "finite A"
   1.283 -  shows "setsum (\<lambda>x. if P x then f x else g x) A =
   1.284 -         setsum f (A \<inter> {x. P x}) + setsum g (A \<inter> - {x. P x})"
   1.285 -proof-
   1.286 -  have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}" 
   1.287 -          "(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}" 
   1.288 -    by blast+
   1.289 -  from fA 
   1.290 -  have f: "finite (A \<inter> {x. P x})" "finite (A \<inter> -{x. P x})" by auto
   1.291 -  let ?g = "\<lambda>x. if P x then f x else g x"
   1.292 -  from setsum_Un_disjoint[OF f a(2), of ?g] a(1)
   1.293 -  show ?thesis by simp
   1.294 -qed
   1.295 -
   1.296 -
   1.297 -(*But we can't get rid of finite I. If infinite, although the rhs is 0, 
   1.298 -  the lhs need not be, since UNION I A could still be finite.*)
   1.299 -lemma setsum_UN_disjoint:
   1.300 -    "finite I ==> (ALL i:I. finite (A i)) ==>
   1.301 -        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   1.302 -      setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
   1.303 -by(simp add: setsum_def comm_monoid_add.fold_image_UN_disjoint cong: setsum_cong)
   1.304 -
   1.305 -text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
   1.306 -directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
   1.307 -lemma setsum_Union_disjoint:
   1.308 -  "[| (ALL A:C. finite A);
   1.309 -      (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
   1.310 -   ==> setsum f (Union C) = setsum (setsum f) C"
   1.311 -apply (cases "finite C") 
   1.312 - prefer 2 apply (force dest: finite_UnionD simp add: setsum_def)
   1.313 -  apply (frule setsum_UN_disjoint [of C id f])
   1.314 - apply (unfold Union_def id_def, assumption+)
   1.315 -done
   1.316 -
   1.317 -(*But we can't get rid of finite A. If infinite, although the lhs is 0, 
   1.318 -  the rhs need not be, since SIGMA A B could still be finite.*)
   1.319 -lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
   1.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)"
   1.321 -by(simp add:setsum_def comm_monoid_add.fold_image_Sigma split_def cong:setsum_cong)
   1.322 -
   1.323 -text{*Here we can eliminate the finiteness assumptions, by cases.*}
   1.324 -lemma setsum_cartesian_product: 
   1.325 -   "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)"
   1.326 -apply (cases "finite A") 
   1.327 - apply (cases "finite B") 
   1.328 -  apply (simp add: setsum_Sigma)
   1.329 - apply (cases "A={}", simp)
   1.330 - apply (simp) 
   1.331 -apply (auto simp add: setsum_def
   1.332 -            dest: finite_cartesian_productD1 finite_cartesian_productD2) 
   1.333 -done
   1.334 -
   1.335 -lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
   1.336 -by(simp add:setsum_def comm_monoid_add.fold_image_distrib)
   1.337 -
   1.338 -
   1.339 -subsubsection {* Properties in more restricted classes of structures *}
   1.340 -
   1.341 -lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   1.342 -apply (case_tac "finite A")
   1.343 - prefer 2 apply (simp add: setsum_def)
   1.344 -apply (erule rev_mp)
   1.345 -apply (erule finite_induct, auto)
   1.346 -done
   1.347 -
   1.348 -lemma setsum_eq_0_iff [simp]:
   1.349 -    "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   1.350 -by (induct set: finite) auto
   1.351 -
   1.352 -lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
   1.353 -  (setsum f A = Suc 0) = (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
   1.354 -apply(erule finite_induct)
   1.355 -apply (auto simp add:add_is_1)
   1.356 -done
   1.357 -
   1.358 -lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
   1.359 -
   1.360 -lemma setsum_Un_nat: "finite A ==> finite B ==>
   1.361 -  (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   1.362 -  -- {* For the natural numbers, we have subtraction. *}
   1.363 -by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
   1.364 -
   1.365 -lemma setsum_Un: "finite A ==> finite B ==>
   1.366 -  (setsum f (A Un B) :: 'a :: ab_group_add) =
   1.367 -   setsum f A + setsum f B - setsum f (A Int B)"
   1.368 -by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
   1.369 -
   1.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"
   1.371 -  apply (induct set: finite)
   1.372 -  apply simp by auto
   1.373 -
   1.374 -lemma (in comm_monoid_mult) fold_image_Un_one:
   1.375 -  assumes fS: "finite S" and fT: "finite T"
   1.376 -  and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
   1.377 -  shows "fold_image (op *) f 1 (S \<union> T) = fold_image (op *) f 1 S * fold_image (op *) f 1 T"
   1.378 -proof-
   1.379 -  have "fold_image op * f 1 (S \<inter> T) = 1" 
   1.380 -    apply (rule fold_image_1)
   1.381 -    using fS fT I0 by auto 
   1.382 -  with fold_image_Un_Int[OF fS fT] show ?thesis by simp
   1.383 -qed
   1.384 -
   1.385 -lemma setsum_eq_general_reverses:
   1.386 -  assumes fS: "finite S" and fT: "finite T"
   1.387 -  and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
   1.388 -  and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x"
   1.389 -  shows "setsum f S = setsum g T"
   1.390 -  apply (simp add: setsum_def fS fT)
   1.391 -  apply (rule comm_monoid_add.fold_image_eq_general_inverses[OF fS])
   1.392 -  apply (erule kh)
   1.393 -  apply (erule hk)
   1.394 -  done
   1.395 -
   1.396 -
   1.397 -
   1.398 -lemma setsum_Un_zero:  
   1.399 -  assumes fS: "finite S" and fT: "finite T"
   1.400 -  and I0: "\<forall>x \<in> S\<inter>T. f x = 0"
   1.401 -  shows "setsum f (S \<union> T) = setsum f S  + setsum f T"
   1.402 -  using fS fT
   1.403 -  apply (simp add: setsum_def)
   1.404 -  apply (rule comm_monoid_add.fold_image_Un_one)
   1.405 -  using I0 by auto
   1.406 -
   1.407 -
   1.408 -lemma setsum_UNION_zero: 
   1.409 -  assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T"
   1.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"
   1.411 -  shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S"
   1.412 -  using fSS f0
   1.413 -proof(induct rule: finite_induct[OF fS])
   1.414 -  case 1 thus ?case by simp
   1.415 -next
   1.416 -  case (2 T F)
   1.417 -  then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F" 
   1.418 -    and H: "setsum f (\<Union> F) = setsum (setsum f) F" by auto
   1.419 -  from fTF have fUF: "finite (\<Union>F)" by auto
   1.420 -  from "2.prems" TF fTF
   1.421 -  show ?case 
   1.422 -    by (auto simp add: H[symmetric] intro: setsum_Un_zero[OF fTF(1) fUF, of f])
   1.423 -qed
   1.424 -
   1.425 -
   1.426 -lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
   1.427 -  (if a:A then setsum f A - f a else setsum f A)"
   1.428 -apply (case_tac "finite A")
   1.429 - prefer 2 apply (simp add: setsum_def)
   1.430 -apply (erule finite_induct)
   1.431 - apply (auto simp add: insert_Diff_if)
   1.432 -apply (drule_tac a = a in mk_disjoint_insert, auto)
   1.433 -done
   1.434 -
   1.435 -lemma setsum_diff1: "finite A \<Longrightarrow>
   1.436 -  (setsum f (A - {a}) :: ('a::ab_group_add)) =
   1.437 -  (if a:A then setsum f A - f a else setsum f A)"
   1.438 -by (erule finite_induct) (auto simp add: insert_Diff_if)
   1.439 -
   1.440 -lemma setsum_diff1'[rule_format]:
   1.441 -  "finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x)"
   1.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))"])
   1.443 -apply (auto simp add: insert_Diff_if add_ac)
   1.444 -done
   1.445 -
   1.446 -lemma setsum_diff1_ring: assumes "finite A" "a \<in> A"
   1.447 -  shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)"
   1.448 -unfolding setsum_diff1'[OF assms] by auto
   1.449 -
   1.450 -(* By Jeremy Siek: *)
   1.451 -
   1.452 -lemma setsum_diff_nat: 
   1.453 -assumes "finite B" and "B \<subseteq> A"
   1.454 -shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
   1.455 -using assms
   1.456 -proof induct
   1.457 -  show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
   1.458 -next
   1.459 -  fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
   1.460 -    and xFinA: "insert x F \<subseteq> A"
   1.461 -    and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
   1.462 -  from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
   1.463 -  from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
   1.464 -    by (simp add: setsum_diff1_nat)
   1.465 -  from xFinA have "F \<subseteq> A" by simp
   1.466 -  with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
   1.467 -  with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
   1.468 -    by simp
   1.469 -  from xnotinF have "A - insert x F = (A - F) - {x}" by auto
   1.470 -  with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
   1.471 -    by simp
   1.472 -  from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
   1.473 -  with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
   1.474 -    by simp
   1.475 -  thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
   1.476 -qed
   1.477 -
   1.478 -lemma setsum_diff:
   1.479 -  assumes le: "finite A" "B \<subseteq> A"
   1.480 -  shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
   1.481 -proof -
   1.482 -  from le have finiteB: "finite B" using finite_subset by auto
   1.483 -  show ?thesis using finiteB le
   1.484 -  proof induct
   1.485 -    case empty
   1.486 -    thus ?case by auto
   1.487 -  next
   1.488 -    case (insert x F)
   1.489 -    thus ?case using le finiteB 
   1.490 -      by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
   1.491 -  qed
   1.492 -qed
   1.493 -
   1.494 -lemma setsum_mono:
   1.495 -  assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, ordered_ab_semigroup_add}))"
   1.496 -  shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
   1.497 -proof (cases "finite K")
   1.498 -  case True
   1.499 -  thus ?thesis using le
   1.500 -  proof induct
   1.501 -    case empty
   1.502 -    thus ?case by simp
   1.503 -  next
   1.504 -    case insert
   1.505 -    thus ?case using add_mono by fastsimp
   1.506 -  qed
   1.507 -next
   1.508 -  case False
   1.509 -  thus ?thesis
   1.510 -    by (simp add: setsum_def)
   1.511 -qed
   1.512 -
   1.513 -lemma setsum_strict_mono:
   1.514 -  fixes f :: "'a \<Rightarrow> 'b::{ordered_cancel_ab_semigroup_add,comm_monoid_add}"
   1.515 -  assumes "finite A"  "A \<noteq> {}"
   1.516 -    and "!!x. x:A \<Longrightarrow> f x < g x"
   1.517 -  shows "setsum f A < setsum g A"
   1.518 -  using prems
   1.519 -proof (induct rule: finite_ne_induct)
   1.520 -  case singleton thus ?case by simp
   1.521 -next
   1.522 -  case insert thus ?case by (auto simp: add_strict_mono)
   1.523 -qed
   1.524 -
   1.525 -lemma setsum_negf:
   1.526 -  "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
   1.527 -proof (cases "finite A")
   1.528 -  case True thus ?thesis by (induct set: finite) auto
   1.529 -next
   1.530 -  case False thus ?thesis by (simp add: setsum_def)
   1.531 -qed
   1.532 -
   1.533 -lemma setsum_subtractf:
   1.534 -  "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
   1.535 -    setsum f A - setsum g A"
   1.536 -proof (cases "finite A")
   1.537 -  case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
   1.538 -next
   1.539 -  case False thus ?thesis by (simp add: setsum_def)
   1.540 -qed
   1.541 -
   1.542 -lemma setsum_nonneg:
   1.543 -  assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
   1.544 -  shows "0 \<le> setsum f A"
   1.545 -proof (cases "finite A")
   1.546 -  case True thus ?thesis using nn
   1.547 -  proof induct
   1.548 -    case empty then show ?case by simp
   1.549 -  next
   1.550 -    case (insert x F)
   1.551 -    then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
   1.552 -    with insert show ?case by simp
   1.553 -  qed
   1.554 -next
   1.555 -  case False thus ?thesis by (simp add: setsum_def)
   1.556 -qed
   1.557 -
   1.558 -lemma setsum_nonpos:
   1.559 -  assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{ordered_ab_semigroup_add,comm_monoid_add})"
   1.560 -  shows "setsum f A \<le> 0"
   1.561 -proof (cases "finite A")
   1.562 -  case True thus ?thesis using np
   1.563 -  proof induct
   1.564 -    case empty then show ?case by simp
   1.565 -  next
   1.566 -    case (insert x F)
   1.567 -    then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
   1.568 -    with insert show ?case by simp
   1.569 -  qed
   1.570 -next
   1.571 -  case False thus ?thesis by (simp add: setsum_def)
   1.572 -qed
   1.573 -
   1.574 -lemma setsum_mono2:
   1.575 -fixes f :: "'a \<Rightarrow> 'b :: {ordered_ab_semigroup_add_imp_le,comm_monoid_add}"
   1.576 -assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
   1.577 -shows "setsum f A \<le> setsum f B"
   1.578 -proof -
   1.579 -  have "setsum f A \<le> setsum f A + setsum f (B-A)"
   1.580 -    by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
   1.581 -  also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
   1.582 -    by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
   1.583 -  also have "A \<union> (B-A) = B" using sub by blast
   1.584 -  finally show ?thesis .
   1.585 -qed
   1.586 -
   1.587 -lemma setsum_mono3: "finite B ==> A <= B ==> 
   1.588 -    ALL x: B - A. 
   1.589 -      0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==>
   1.590 -        setsum f A <= setsum f B"
   1.591 -  apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
   1.592 -  apply (erule ssubst)
   1.593 -  apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
   1.594 -  apply simp
   1.595 -  apply (rule add_left_mono)
   1.596 -  apply (erule setsum_nonneg)
   1.597 -  apply (subst setsum_Un_disjoint [THEN sym])
   1.598 -  apply (erule finite_subset, assumption)
   1.599 -  apply (rule finite_subset)
   1.600 -  prefer 2
   1.601 -  apply assumption
   1.602 -  apply (auto simp add: sup_absorb2)
   1.603 -done
   1.604 -
   1.605 -lemma setsum_right_distrib: 
   1.606 -  fixes f :: "'a => ('b::semiring_0)"
   1.607 -  shows "r * setsum f A = setsum (%n. r * f n) 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) thus ?case by (simp add: right_distrib)
   1.615 -  qed
   1.616 -next
   1.617 -  case False thus ?thesis by (simp add: setsum_def)
   1.618 -qed
   1.619 -
   1.620 -lemma setsum_left_distrib:
   1.621 -  "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
   1.622 -proof (cases "finite A")
   1.623 -  case True
   1.624 -  then show ?thesis
   1.625 -  proof induct
   1.626 -    case empty thus ?case by simp
   1.627 -  next
   1.628 -    case (insert x A) thus ?case by (simp add: left_distrib)
   1.629 -  qed
   1.630 -next
   1.631 -  case False thus ?thesis by (simp add: setsum_def)
   1.632 -qed
   1.633 -
   1.634 -lemma setsum_divide_distrib:
   1.635 -  "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
   1.636 -proof (cases "finite A")
   1.637 -  case True
   1.638 -  then show ?thesis
   1.639 -  proof induct
   1.640 -    case empty thus ?case by simp
   1.641 -  next
   1.642 -    case (insert x A) thus ?case by (simp add: add_divide_distrib)
   1.643 -  qed
   1.644 -next
   1.645 -  case False thus ?thesis by (simp add: setsum_def)
   1.646 -qed
   1.647 -
   1.648 -lemma setsum_abs[iff]: 
   1.649 -  fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   1.650 -  shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
   1.651 -proof (cases "finite A")
   1.652 -  case True
   1.653 -  thus ?thesis
   1.654 -  proof induct
   1.655 -    case empty thus ?case by simp
   1.656 -  next
   1.657 -    case (insert x A)
   1.658 -    thus ?case by (auto intro: abs_triangle_ineq order_trans)
   1.659 -  qed
   1.660 -next
   1.661 -  case False thus ?thesis by (simp add: setsum_def)
   1.662 -qed
   1.663 -
   1.664 -lemma setsum_abs_ge_zero[iff]: 
   1.665 -  fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   1.666 -  shows "0 \<le> setsum (%i. abs(f i)) A"
   1.667 -proof (cases "finite A")
   1.668 -  case True
   1.669 -  thus ?thesis
   1.670 -  proof induct
   1.671 -    case empty thus ?case by simp
   1.672 -  next
   1.673 -    case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg)
   1.674 -  qed
   1.675 -next
   1.676 -  case False thus ?thesis by (simp add: setsum_def)
   1.677 -qed
   1.678 -
   1.679 -lemma abs_setsum_abs[simp]: 
   1.680 -  fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   1.681 -  shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
   1.682 -proof (cases "finite A")
   1.683 -  case True
   1.684 -  thus ?thesis
   1.685 -  proof induct
   1.686 -    case empty thus ?case by simp
   1.687 -  next
   1.688 -    case (insert a A)
   1.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
   1.690 -    also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
   1.691 -    also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
   1.692 -      by (simp del: abs_of_nonneg)
   1.693 -    also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
   1.694 -    finally show ?case .
   1.695 -  qed
   1.696 -next
   1.697 -  case False thus ?thesis by (simp add: setsum_def)
   1.698 -qed
   1.699 -
   1.700 -
   1.701 -lemma setsum_Plus:
   1.702 -  fixes A :: "'a set" and B :: "'b set"
   1.703 -  assumes fin: "finite A" "finite B"
   1.704 -  shows "setsum f (A <+> B) = setsum (f \<circ> Inl) A + setsum (f \<circ> Inr) B"
   1.705 -proof -
   1.706 -  have "A <+> B = Inl ` A \<union> Inr ` B" by auto
   1.707 -  moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)"
   1.708 -    by(auto intro: finite_imageI)
   1.709 -  moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto
   1.710 -  moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI)
   1.711 -  ultimately show ?thesis using fin by(simp add: setsum_Un_disjoint setsum_reindex)
   1.712 -qed
   1.713 -
   1.714 -
   1.715 -text {* Commuting outer and inner summation *}
   1.716 -
   1.717 -lemma swap_inj_on:
   1.718 -  "inj_on (%(i, j). (j, i)) (A \<times> B)"
   1.719 -  by (unfold inj_on_def) fast
   1.720 -
   1.721 -lemma swap_product:
   1.722 -  "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
   1.723 -  by (simp add: split_def image_def) blast
   1.724 -
   1.725 -lemma setsum_commute:
   1.726 -  "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
   1.727 -proof (simp add: setsum_cartesian_product)
   1.728 -  have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
   1.729 -    (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
   1.730 -    (is "?s = _")
   1.731 -    apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on)
   1.732 -    apply (simp add: split_def)
   1.733 -    done
   1.734 -  also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
   1.735 -    (is "_ = ?t")
   1.736 -    apply (simp add: swap_product)
   1.737 -    done
   1.738 -  finally show "?s = ?t" .
   1.739 -qed
   1.740 -
   1.741 -lemma setsum_product:
   1.742 -  fixes f :: "'a => ('b::semiring_0)"
   1.743 -  shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
   1.744 -  by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
   1.745 -
   1.746 -lemma setsum_mult_setsum_if_inj:
   1.747 -fixes f :: "'a => ('b::semiring_0)"
   1.748 -shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==>
   1.749 -  setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}"
   1.750 -by(auto simp: setsum_product setsum_cartesian_product
   1.751 -        intro!:  setsum_reindex_cong[symmetric])
   1.752 -
   1.753 -
   1.754 -subsection {* Generalized product over a set *}
   1.755 -
   1.756 -definition setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult"
   1.757 -where "setprod f A == if finite A then fold_image (op *) f 1 A else 1"
   1.758 -
   1.759 -abbreviation
   1.760 -  Setprod  ("\<Prod>_" [1000] 999) where
   1.761 -  "\<Prod>A == setprod (%x. x) A"
   1.762 -
   1.763 -syntax
   1.764 -  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
   1.765 -syntax (xsymbols)
   1.766 -  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
   1.767 -syntax (HTML output)
   1.768 -  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
   1.769 -
   1.770 -translations -- {* Beware of argument permutation! *}
   1.771 -  "PROD i:A. b" == "CONST setprod (%i. b) A" 
   1.772 -  "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A" 
   1.773 -
   1.774 -text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
   1.775 - @{text"\<Prod>x|P. e"}. *}
   1.776 -
   1.777 -syntax
   1.778 -  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
   1.779 -syntax (xsymbols)
   1.780 -  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
   1.781 -syntax (HTML output)
   1.782 -  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
   1.783 -
   1.784 -translations
   1.785 -  "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
   1.786 -  "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
   1.787 -
   1.788 -
   1.789 -lemma setprod_empty [simp]: "setprod f {} = 1"
   1.790 -by (auto simp add: setprod_def)
   1.791 -
   1.792 -lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
   1.793 -    setprod f (insert a A) = f a * setprod f A"
   1.794 -by (simp add: setprod_def)
   1.795 -
   1.796 -lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
   1.797 -by (simp add: setprod_def)
   1.798 -
   1.799 -lemma setprod_reindex:
   1.800 -   "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
   1.801 -by(auto simp: setprod_def fold_image_reindex dest!:finite_imageD)
   1.802 -
   1.803 -lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
   1.804 -by (auto simp add: setprod_reindex)
   1.805 -
   1.806 -lemma setprod_cong:
   1.807 -  "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
   1.808 -by(fastsimp simp: setprod_def intro: fold_image_cong)
   1.809 -
   1.810 -lemma strong_setprod_cong[cong]:
   1.811 -  "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
   1.812 -by(fastsimp simp: simp_implies_def setprod_def intro: fold_image_cong)
   1.813 -
   1.814 -lemma setprod_reindex_cong: "inj_on f A ==>
   1.815 -    B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
   1.816 -by (frule setprod_reindex, simp)
   1.817 -
   1.818 -lemma strong_setprod_reindex_cong: assumes i: "inj_on f A"
   1.819 -  and B: "B = f ` A" and eq: "\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x"
   1.820 -  shows "setprod h B = setprod g A"
   1.821 -proof-
   1.822 -    have "setprod h B = setprod (h o f) A"
   1.823 -      by (simp add: B setprod_reindex[OF i, of h])
   1.824 -    then show ?thesis apply simp
   1.825 -      apply (rule setprod_cong)
   1.826 -      apply simp
   1.827 -      by (simp add: eq)
   1.828 -qed
   1.829 -
   1.830 -lemma setprod_Un_one:  
   1.831 -  assumes fS: "finite S" and fT: "finite T"
   1.832 -  and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
   1.833 -  shows "setprod f (S \<union> T) = setprod f S  * setprod f T"
   1.834 -  using fS fT
   1.835 -  apply (simp add: setprod_def)
   1.836 -  apply (rule fold_image_Un_one)
   1.837 -  using I0 by auto
   1.838 -
   1.839 -
   1.840 -lemma setprod_1: "setprod (%i. 1) A = 1"
   1.841 -apply (case_tac "finite A")
   1.842 -apply (erule finite_induct, auto simp add: mult_ac)
   1.843 -done
   1.844 -
   1.845 -lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
   1.846 -apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
   1.847 -apply (erule ssubst, rule setprod_1)
   1.848 -apply (rule setprod_cong, auto)
   1.849 -done
   1.850 -
   1.851 -lemma setprod_Un_Int: "finite A ==> finite B
   1.852 -    ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
   1.853 -by(simp add: setprod_def fold_image_Un_Int[symmetric])
   1.854 -
   1.855 -lemma setprod_Un_disjoint: "finite A ==> finite B
   1.856 -  ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
   1.857 -by (subst setprod_Un_Int [symmetric], auto)
   1.858 -
   1.859 -lemma setprod_mono_one_left: 
   1.860 -  assumes fT: "finite T" and ST: "S \<subseteq> T"
   1.861 -  and z: "\<forall>i \<in> T - S. f i = 1"
   1.862 -  shows "setprod f S = setprod f T"
   1.863 -proof-
   1.864 -  have eq: "T = S \<union> (T - S)" using ST by blast
   1.865 -  have d: "S \<inter> (T - S) = {}" using ST by blast
   1.866 -  from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset)
   1.867 -  show ?thesis
   1.868 -  by (simp add: setprod_Un_disjoint[OF f d, unfolded eq[symmetric]] setprod_1'[OF z])
   1.869 -qed
   1.870 -
   1.871 -lemmas setprod_mono_one_right = setprod_mono_one_left [THEN sym]
   1.872 -
   1.873 -lemma setprod_delta: 
   1.874 -  assumes fS: "finite S"
   1.875 -  shows "setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
   1.876 -proof-
   1.877 -  let ?f = "(\<lambda>k. if k=a then b k else 1)"
   1.878 -  {assume a: "a \<notin> S"
   1.879 -    hence "\<forall> k\<in> S. ?f k = 1" by simp
   1.880 -    hence ?thesis  using a by (simp add: setprod_1 cong add: setprod_cong) }
   1.881 -  moreover 
   1.882 -  {assume a: "a \<in> S"
   1.883 -    let ?A = "S - {a}"
   1.884 -    let ?B = "{a}"
   1.885 -    have eq: "S = ?A \<union> ?B" using a by blast 
   1.886 -    have dj: "?A \<inter> ?B = {}" by simp
   1.887 -    from fS have fAB: "finite ?A" "finite ?B" by auto  
   1.888 -    have fA1: "setprod ?f ?A = 1" apply (rule setprod_1') by auto
   1.889 -    have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
   1.890 -      using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
   1.891 -      by simp
   1.892 -    then have ?thesis  using a by (simp add: fA1 cong add: setprod_cong cong del: if_weak_cong)}
   1.893 -  ultimately show ?thesis by blast
   1.894 -qed
   1.895 -
   1.896 -lemma setprod_delta': 
   1.897 -  assumes fS: "finite S" shows 
   1.898 -  "setprod (\<lambda>k. if a = k then b k else 1) S = 
   1.899 -     (if a\<in> S then b a else 1)"
   1.900 -  using setprod_delta[OF fS, of a b, symmetric] 
   1.901 -  by (auto intro: setprod_cong)
   1.902 -
   1.903 -
   1.904 -lemma setprod_UN_disjoint:
   1.905 -    "finite I ==> (ALL i:I. finite (A i)) ==>
   1.906 -        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   1.907 -      setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
   1.908 -by(simp add: setprod_def fold_image_UN_disjoint cong: setprod_cong)
   1.909 -
   1.910 -lemma setprod_Union_disjoint:
   1.911 -  "[| (ALL A:C. finite A);
   1.912 -      (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |] 
   1.913 -   ==> setprod f (Union C) = setprod (setprod f) C"
   1.914 -apply (cases "finite C") 
   1.915 - prefer 2 apply (force dest: finite_UnionD simp add: setprod_def)
   1.916 -  apply (frule setprod_UN_disjoint [of C id f])
   1.917 - apply (unfold Union_def id_def, assumption+)
   1.918 -done
   1.919 -
   1.920 -lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
   1.921 -    (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
   1.922 -    (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
   1.923 -by(simp add:setprod_def fold_image_Sigma split_def cong:setprod_cong)
   1.924 -
   1.925 -text{*Here we can eliminate the finiteness assumptions, by cases.*}
   1.926 -lemma setprod_cartesian_product: 
   1.927 -     "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
   1.928 -apply (cases "finite A") 
   1.929 - apply (cases "finite B") 
   1.930 -  apply (simp add: setprod_Sigma)
   1.931 - apply (cases "A={}", simp)
   1.932 - apply (simp add: setprod_1) 
   1.933 -apply (auto simp add: setprod_def
   1.934 -            dest: finite_cartesian_productD1 finite_cartesian_productD2) 
   1.935 -done
   1.936 -
   1.937 -lemma setprod_timesf:
   1.938 -     "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
   1.939 -by(simp add:setprod_def fold_image_distrib)
   1.940 -
   1.941 -
   1.942 -subsubsection {* Properties in more restricted classes of structures *}
   1.943 -
   1.944 -lemma setprod_eq_1_iff [simp]:
   1.945 -  "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
   1.946 -by (induct set: finite) auto
   1.947 -
   1.948 -lemma setprod_zero:
   1.949 -     "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
   1.950 -apply (induct set: finite, force, clarsimp)
   1.951 -apply (erule disjE, auto)
   1.952 -done
   1.953 -
   1.954 -lemma setprod_nonneg [rule_format]:
   1.955 -   "(ALL x: A. (0::'a::linordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
   1.956 -by (cases "finite A", induct set: finite, simp_all add: mult_nonneg_nonneg)
   1.957 -
   1.958 -lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x)
   1.959 -  --> 0 < setprod f A"
   1.960 -by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos)
   1.961 -
   1.962 -lemma setprod_zero_iff[simp]: "finite A ==> 
   1.963 -  (setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) =
   1.964 -  (EX x: A. f x = 0)"
   1.965 -by (erule finite_induct, auto simp:no_zero_divisors)
   1.966 -
   1.967 -lemma setprod_pos_nat:
   1.968 -  "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
   1.969 -using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
   1.970 -
   1.971 -lemma setprod_pos_nat_iff[simp]:
   1.972 -  "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
   1.973 -using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
   1.974 -
   1.975 -lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
   1.976 -  (setprod f (A Un B) :: 'a ::{field})
   1.977 -   = setprod f A * setprod f B / setprod f (A Int B)"
   1.978 -by (subst setprod_Un_Int [symmetric], auto)
   1.979 -
   1.980 -lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
   1.981 -  (setprod f (A - {a}) :: 'a :: {field}) =
   1.982 -  (if a:A then setprod f A / f a else setprod f A)"
   1.983 -by (erule finite_induct) (auto simp add: insert_Diff_if)
   1.984 -
   1.985 -lemma setprod_inversef: 
   1.986 -  fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}"
   1.987 -  shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)"
   1.988 -by (erule finite_induct) auto
   1.989 -
   1.990 -lemma setprod_dividef:
   1.991 -  fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}"
   1.992 -  shows "finite A
   1.993 -    ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
   1.994 -apply (subgoal_tac
   1.995 -         "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
   1.996 -apply (erule ssubst)
   1.997 -apply (subst divide_inverse)
   1.998 -apply (subst setprod_timesf)
   1.999 -apply (subst setprod_inversef, assumption+, rule refl)
  1.1000 -apply (rule setprod_cong, rule refl)
  1.1001 -apply (subst divide_inverse, auto)
  1.1002 -done
  1.1003 -
  1.1004 -lemma setprod_dvd_setprod [rule_format]: 
  1.1005 -    "(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A"
  1.1006 -  apply (cases "finite A")
  1.1007 -  apply (induct set: finite)
  1.1008 -  apply (auto simp add: dvd_def)
  1.1009 -  apply (rule_tac x = "k * ka" in exI)
  1.1010 -  apply (simp add: algebra_simps)
  1.1011 -done
  1.1012 -
  1.1013 -lemma setprod_dvd_setprod_subset:
  1.1014 -  "finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B"
  1.1015 -  apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)")
  1.1016 -  apply (unfold dvd_def, blast)
  1.1017 -  apply (subst setprod_Un_disjoint [symmetric])
  1.1018 -  apply (auto elim: finite_subset intro: setprod_cong)
  1.1019 -done
  1.1020 -
  1.1021 -lemma setprod_dvd_setprod_subset2:
  1.1022 -  "finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow> 
  1.1023 -      setprod f A dvd setprod g B"
  1.1024 -  apply (rule dvd_trans)
  1.1025 -  apply (rule setprod_dvd_setprod, erule (1) bspec)
  1.1026 -  apply (erule (1) setprod_dvd_setprod_subset)
  1.1027 -done
  1.1028 -
  1.1029 -lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow> 
  1.1030 -    (f i ::'a::comm_semiring_1) dvd setprod f A"
  1.1031 -by (induct set: finite) (auto intro: dvd_mult)
  1.1032 -
  1.1033 -lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow> 
  1.1034 -    (d::'a::comm_semiring_1) dvd (SUM x : A. f x)"
  1.1035 -  apply (cases "finite A")
  1.1036 -  apply (induct set: finite)
  1.1037 -  apply auto
  1.1038 -done
  1.1039 -
  1.1040 -lemma setprod_mono:
  1.1041 -  fixes f :: "'a \<Rightarrow> 'b\<Colon>linordered_semidom"
  1.1042 -  assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i"
  1.1043 -  shows "setprod f A \<le> setprod g A"
  1.1044 -proof (cases "finite A")
  1.1045 -  case True
  1.1046 -  hence ?thesis "setprod f A \<ge> 0" using subset_refl[of A]
  1.1047 -  proof (induct A rule: finite_subset_induct)
  1.1048 -    case (insert a F)
  1.1049 -    thus "setprod f (insert a F) \<le> setprod g (insert a F)" "0 \<le> setprod f (insert a F)"
  1.1050 -      unfolding setprod_insert[OF insert(1,3)]
  1.1051 -      using assms[rule_format,OF insert(2)] insert
  1.1052 -      by (auto intro: mult_mono mult_nonneg_nonneg)
  1.1053 -  qed auto
  1.1054 -  thus ?thesis by simp
  1.1055 -qed auto
  1.1056 -
  1.1057 -lemma abs_setprod:
  1.1058 -  fixes f :: "'a \<Rightarrow> 'b\<Colon>{linordered_field,abs}"
  1.1059 -  shows "abs (setprod f A) = setprod (\<lambda>x. abs (f x)) A"
  1.1060 -proof (cases "finite A")
  1.1061 -  case True thus ?thesis
  1.1062 -    by induct (auto simp add: field_simps abs_mult)
  1.1063 -qed auto
  1.1064 -
  1.1065 -
  1.1066 -subsection {* Finite cardinality *}
  1.1067 -
  1.1068 -text {* This definition, although traditional, is ugly to work with:
  1.1069 -@{text "card A == LEAST n. EX f. A = {f i | i. i < n}"}.
  1.1070 -But now that we have @{text setsum} things are easy:
  1.1071 -*}
  1.1072 -
  1.1073 -definition card :: "'a set \<Rightarrow> nat" where
  1.1074 -  "card A = setsum (\<lambda>x. 1) A"
  1.1075 -
  1.1076 -lemmas card_eq_setsum = card_def
  1.1077 -
  1.1078 -lemma card_empty [simp]: "card {} = 0"
  1.1079 -  by (simp add: card_def)
  1.1080 -
  1.1081 -lemma card_insert_disjoint [simp]:
  1.1082 -  "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
  1.1083 -  by (simp add: card_def)
  1.1084 -
  1.1085 -lemma card_insert_if:
  1.1086 -  "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
  1.1087 -  by (simp add: insert_absorb)
  1.1088 -
  1.1089 -lemma card_infinite [simp]: "~ finite A ==> card A = 0"
  1.1090 -  by (simp add: card_def)
  1.1091 -
  1.1092 -lemma card_ge_0_finite:
  1.1093 -  "card A > 0 \<Longrightarrow> finite A"
  1.1094 -  by (rule ccontr) simp
  1.1095 -
  1.1096 -lemma card_0_eq [simp,noatp]: "finite A ==> (card A = 0) = (A = {})"
  1.1097 -  apply auto
  1.1098 -  apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
  1.1099 -  done
  1.1100 -
  1.1101 -lemma finite_UNIV_card_ge_0:
  1.1102 -  "finite (UNIV :: 'a set) \<Longrightarrow> card (UNIV :: 'a set) > 0"
  1.1103 -  by (rule ccontr) simp
  1.1104 -
  1.1105 -lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
  1.1106 -  by auto
  1.1107 -
  1.1108 -lemma card_gt_0_iff: "(0 < card A) = (A \<noteq> {} & finite A)"
  1.1109 -  by (simp add: neq0_conv [symmetric] card_eq_0_iff) 
  1.1110 -
  1.1111 -lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
  1.1112 -apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
  1.1113 -apply(simp del:insert_Diff_single)
  1.1114 -done
  1.1115 -
  1.1116 -lemma card_Diff_singleton:
  1.1117 -  "finite A ==> x: A ==> card (A - {x}) = card A - 1"
  1.1118 -by (simp add: card_Suc_Diff1 [symmetric])
  1.1119 -
  1.1120 -lemma card_Diff_singleton_if:
  1.1121 -  "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)"
  1.1122 -by (simp add: card_Diff_singleton)
  1.1123 -
  1.1124 -lemma card_Diff_insert[simp]:
  1.1125 -assumes "finite A" and "a:A" and "a ~: B"
  1.1126 -shows "card(A - insert a B) = card(A - B) - 1"
  1.1127 -proof -
  1.1128 -  have "A - insert a B = (A - B) - {a}" using assms by blast
  1.1129 -  then show ?thesis using assms by(simp add:card_Diff_singleton)
  1.1130 -qed
  1.1131 -
  1.1132 -lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))"
  1.1133 -by (simp add: card_insert_if card_Suc_Diff1 del:card_Diff_insert)
  1.1134 -
  1.1135 -lemma card_insert_le: "finite A ==> card A <= card (insert x A)"
  1.1136 -by (simp add: card_insert_if)
  1.1137 -
  1.1138 -lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
  1.1139 -by (simp add: card_def setsum_mono2)
  1.1140 -
  1.1141 -lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
  1.1142 -apply (induct set: finite, simp, clarify)
  1.1143 -apply (subgoal_tac "finite A & A - {x} <= F")
  1.1144 - prefer 2 apply (blast intro: finite_subset, atomize)
  1.1145 -apply (drule_tac x = "A - {x}" in spec)
  1.1146 -apply (simp add: card_Diff_singleton_if split add: split_if_asm)
  1.1147 -apply (case_tac "card A", auto)
  1.1148 -done
  1.1149 -
  1.1150 -lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B"
  1.1151 -apply (simp add: psubset_eq linorder_not_le [symmetric])
  1.1152 -apply (blast dest: card_seteq)
  1.1153 -done
  1.1154 -
  1.1155 -lemma card_Un_Int: "finite A ==> finite B
  1.1156 -    ==> card A + card B = card (A Un B) + card (A Int B)"
  1.1157 -by(simp add:card_def setsum_Un_Int)
  1.1158 -
  1.1159 -lemma card_Un_disjoint: "finite A ==> finite B
  1.1160 -    ==> A Int B = {} ==> card (A Un B) = card A + card B"
  1.1161 -by (simp add: card_Un_Int)
  1.1162 -
  1.1163 -lemma card_Diff_subset:
  1.1164 -  "finite B ==> B <= A ==> card (A - B) = card A - card B"
  1.1165 -by(simp add:card_def setsum_diff_nat)
  1.1166 -
  1.1167 -lemma card_Diff_subset_Int:
  1.1168 -  assumes AB: "finite (A \<inter> B)" shows "card (A - B) = card A - card (A \<inter> B)"
  1.1169 -proof -
  1.1170 -  have "A - B = A - A \<inter> B" by auto
  1.1171 -  thus ?thesis
  1.1172 -    by (simp add: card_Diff_subset AB) 
  1.1173 -qed
  1.1174 -
  1.1175 -lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
  1.1176 -apply (rule Suc_less_SucD)
  1.1177 -apply (simp add: card_Suc_Diff1 del:card_Diff_insert)
  1.1178 -done
  1.1179 -
  1.1180 -lemma card_Diff2_less:
  1.1181 -  "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A"
  1.1182 -apply (case_tac "x = y")
  1.1183 - apply (simp add: card_Diff1_less del:card_Diff_insert)
  1.1184 -apply (rule less_trans)
  1.1185 - prefer 2 apply (auto intro!: card_Diff1_less simp del:card_Diff_insert)
  1.1186 -done
  1.1187 -
  1.1188 -lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A"
  1.1189 -apply (case_tac "x : A")
  1.1190 - apply (simp_all add: card_Diff1_less less_imp_le)
  1.1191 -done
  1.1192 -
  1.1193 -lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
  1.1194 -by (erule psubsetI, blast)
  1.1195 -
  1.1196 -lemma insert_partition:
  1.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>
  1.1198 -  \<Longrightarrow> x \<inter> \<Union> F = {}"
  1.1199 -by auto
  1.1200 -
  1.1201 -lemma finite_psubset_induct[consumes 1, case_names psubset]:
  1.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"
  1.1203 -using assms(1)
  1.1204 -proof (induct A rule: measure_induct_rule[where f=card])
  1.1205 -  case (less A)
  1.1206 -  show ?case
  1.1207 -  proof(rule assms(2)[OF less(2)])
  1.1208 -    fix B assume "finite B" "B \<subset> A"
  1.1209 -    show "P B" by(rule less(1)[OF psubset_card_mono[OF less(2) `B \<subset> A`] `finite B`])
  1.1210 -  qed
  1.1211 -qed
  1.1212 -
  1.1213 -text{* main cardinality theorem *}
  1.1214 -lemma card_partition [rule_format]:
  1.1215 -  "finite C ==>
  1.1216 -     finite (\<Union> C) -->
  1.1217 -     (\<forall>c\<in>C. card c = k) -->
  1.1218 -     (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->
  1.1219 -     k * card(C) = card (\<Union> C)"
  1.1220 -apply (erule finite_induct, simp)
  1.1221 -apply (simp add: card_Un_disjoint insert_partition 
  1.1222 -       finite_subset [of _ "\<Union> (insert x F)"])
  1.1223 -done
  1.1224 -
  1.1225 -lemma card_eq_UNIV_imp_eq_UNIV:
  1.1226 -  assumes fin: "finite (UNIV :: 'a set)"
  1.1227 -  and card: "card A = card (UNIV :: 'a set)"
  1.1228 -  shows "A = (UNIV :: 'a set)"
  1.1229 -proof
  1.1230 -  show "A \<subseteq> UNIV" by simp
  1.1231 -  show "UNIV \<subseteq> A"
  1.1232 -  proof
  1.1233 -    fix x
  1.1234 -    show "x \<in> A"
  1.1235 -    proof (rule ccontr)
  1.1236 -      assume "x \<notin> A"
  1.1237 -      then have "A \<subset> UNIV" by auto
  1.1238 -      with fin have "card A < card (UNIV :: 'a set)" by (fact psubset_card_mono)
  1.1239 -      with card show False by simp
  1.1240 -    qed
  1.1241 -  qed
  1.1242 -qed
  1.1243 -
  1.1244 -text{*The form of a finite set of given cardinality*}
  1.1245 -
  1.1246 -lemma card_eq_SucD:
  1.1247 -assumes "card A = Suc k"
  1.1248 -shows "\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={})"
  1.1249 -proof -
  1.1250 -  have fin: "finite A" using assms by (auto intro: ccontr)
  1.1251 -  moreover have "card A \<noteq> 0" using assms by auto
  1.1252 -  ultimately obtain b where b: "b \<in> A" by auto
  1.1253 -  show ?thesis
  1.1254 -  proof (intro exI conjI)
  1.1255 -    show "A = insert b (A-{b})" using b by blast
  1.1256 -    show "b \<notin> A - {b}" by blast
  1.1257 -    show "card (A - {b}) = k" and "k = 0 \<longrightarrow> A - {b} = {}"
  1.1258 -      using assms b fin by(fastsimp dest:mk_disjoint_insert)+
  1.1259 -  qed
  1.1260 -qed
  1.1261 -
  1.1262 -lemma card_Suc_eq:
  1.1263 -  "(card A = Suc k) =
  1.1264 -   (\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={}))"
  1.1265 -apply(rule iffI)
  1.1266 - apply(erule card_eq_SucD)
  1.1267 -apply(auto)
  1.1268 -apply(subst card_insert)
  1.1269 - apply(auto intro:ccontr)
  1.1270 -done
  1.1271 -
  1.1272 -lemma finite_fun_UNIVD2:
  1.1273 -  assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
  1.1274 -  shows "finite (UNIV :: 'b set)"
  1.1275 -proof -
  1.1276 -  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))"
  1.1277 -    by(rule finite_imageI)
  1.1278 -  moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary)"
  1.1279 -    by(rule UNIV_eq_I) auto
  1.1280 -  ultimately show "finite (UNIV :: 'b set)" by simp
  1.1281 -qed
  1.1282 -
  1.1283 -lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
  1.1284 -apply (cases "finite A")
  1.1285 -apply (erule finite_induct)
  1.1286 -apply (auto simp add: algebra_simps)
  1.1287 -done
  1.1288 -
  1.1289 -lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
  1.1290 -apply (erule finite_induct)
  1.1291 -apply auto
  1.1292 -done
  1.1293 -
  1.1294 -lemma setprod_gen_delta:
  1.1295 -  assumes fS: "finite S"
  1.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)"
  1.1297 -proof-
  1.1298 -  let ?f = "(\<lambda>k. if k=a then b k else c)"
  1.1299 -  {assume a: "a \<notin> S"
  1.1300 -    hence "\<forall> k\<in> S. ?f k = c" by simp
  1.1301 -    hence ?thesis  using a setprod_constant[OF fS, of c] by (simp add: setprod_1 cong add: setprod_cong) }
  1.1302 -  moreover 
  1.1303 -  {assume a: "a \<in> S"
  1.1304 -    let ?A = "S - {a}"
  1.1305 -    let ?B = "{a}"
  1.1306 -    have eq: "S = ?A \<union> ?B" using a by blast 
  1.1307 -    have dj: "?A \<inter> ?B = {}" by simp
  1.1308 -    from fS have fAB: "finite ?A" "finite ?B" by auto  
  1.1309 -    have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
  1.1310 -      apply (rule setprod_cong) by auto
  1.1311 -    have cA: "card ?A = card S - 1" using fS a by auto
  1.1312 -    have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
  1.1313 -    have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
  1.1314 -      using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
  1.1315 -      by simp
  1.1316 -    then have ?thesis using a cA
  1.1317 -      by (simp add: fA1 ring_simps cong add: setprod_cong cong del: if_weak_cong)}
  1.1318 -  ultimately show ?thesis by blast
  1.1319 -qed
  1.1320 -
  1.1321 -
  1.1322 -lemma setsum_bounded:
  1.1323 -  assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
  1.1324 -  shows "setsum f A \<le> of_nat(card A) * K"
  1.1325 -proof (cases "finite A")
  1.1326 -  case True
  1.1327 -  thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
  1.1328 -next
  1.1329 -  case False thus ?thesis by (simp add: setsum_def)
  1.1330 -qed
  1.1331 -
  1.1332 -
  1.1333 -lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
  1.1334 -  unfolding UNIV_unit by simp
  1.1335 -
  1.1336 -
  1.1337 -subsubsection {* Cardinality of unions *}
  1.1338 -
  1.1339 -lemma card_UN_disjoint:
  1.1340 -  "finite I ==> (ALL i:I. finite (A i)) ==>
  1.1341 -   (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {})
  1.1342 -   ==> card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
  1.1343 -apply (simp add: card_def del: setsum_constant)
  1.1344 -apply (subgoal_tac
  1.1345 -         "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
  1.1346 -apply (simp add: setsum_UN_disjoint del: setsum_constant)
  1.1347 -apply (simp cong: setsum_cong)
  1.1348 -done
  1.1349 -
  1.1350 -lemma card_Union_disjoint:
  1.1351 -  "finite C ==> (ALL A:C. finite A) ==>
  1.1352 -   (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
  1.1353 -   ==> card (Union C) = setsum card C"
  1.1354 -apply (frule card_UN_disjoint [of C id])
  1.1355 -apply (unfold Union_def id_def, assumption+)
  1.1356 -done
  1.1357 -
  1.1358 -
  1.1359 -subsubsection {* Cardinality of image *}
  1.1360 -
  1.1361 -text{*The image of a finite set can be expressed using @{term fold_image}.*}
  1.1362 -lemma image_eq_fold_image:
  1.1363 -  "finite A ==> f ` A = fold_image (op Un) (%x. {f x}) {} A"
  1.1364 -proof (induct rule: finite_induct)
  1.1365 -  case empty then show ?case by simp
  1.1366 -next
  1.1367 -  interpret ab_semigroup_mult "op Un"
  1.1368 -    proof qed auto
  1.1369 -  case insert 
  1.1370 -  then show ?case by simp
  1.1371 -qed
  1.1372 -
  1.1373 -lemma card_image_le: "finite A ==> card (f ` A) <= card A"
  1.1374 -apply (induct set: finite)
  1.1375 - apply simp
  1.1376 -apply (simp add: le_SucI card_insert_if)
  1.1377 -done
  1.1378 -
  1.1379 -lemma card_image: "inj_on f A ==> card (f ` A) = card A"
  1.1380 -by(simp add:card_def setsum_reindex o_def del:setsum_constant)
  1.1381 -
  1.1382 -lemma bij_betw_same_card: "bij_betw f A B \<Longrightarrow> card A = card B"
  1.1383 -by(auto simp: card_image bij_betw_def)
  1.1384 -
  1.1385 -lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
  1.1386 -by (simp add: card_seteq card_image)
  1.1387 -
  1.1388 -lemma eq_card_imp_inj_on:
  1.1389 -  "[| finite A; card(f ` A) = card A |] ==> inj_on f A"
  1.1390 -apply (induct rule:finite_induct)
  1.1391 -apply simp
  1.1392 -apply(frule card_image_le[where f = f])
  1.1393 -apply(simp add:card_insert_if split:if_splits)
  1.1394 -done
  1.1395 -
  1.1396 -lemma inj_on_iff_eq_card:
  1.1397 -  "finite A ==> inj_on f A = (card(f ` A) = card A)"
  1.1398 -by(blast intro: card_image eq_card_imp_inj_on)
  1.1399 -
  1.1400 -
  1.1401 -lemma card_inj_on_le:
  1.1402 -  "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B"
  1.1403 -apply (subgoal_tac "finite A") 
  1.1404 - apply (force intro: card_mono simp add: card_image [symmetric])
  1.1405 -apply (blast intro: finite_imageD dest: finite_subset) 
  1.1406 -done
  1.1407 -
  1.1408 -lemma card_bij_eq:
  1.1409 -  "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
  1.1410 -     finite A; finite B |] ==> card A = card B"
  1.1411 -by (auto intro: le_antisym card_inj_on_le)
  1.1412 -
  1.1413 -
  1.1414 -subsubsection {* Cardinality of products *}
  1.1415 -
  1.1416 -(*
  1.1417 -lemma SigmaI_insert: "y \<notin> A ==>
  1.1418 -  (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
  1.1419 -  by auto
  1.1420 -*)
  1.1421 -
  1.1422 -lemma card_SigmaI [simp]:
  1.1423 -  "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
  1.1424 -  \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  1.1425 -by(simp add:card_def setsum_Sigma del:setsum_constant)
  1.1426 -
  1.1427 -lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
  1.1428 -apply (cases "finite A") 
  1.1429 -apply (cases "finite B") 
  1.1430 -apply (auto simp add: card_eq_0_iff
  1.1431 -            dest: finite_cartesian_productD1 finite_cartesian_productD2)
  1.1432 -done
  1.1433 -
  1.1434 -lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
  1.1435 -by (simp add: card_cartesian_product)
  1.1436 -
  1.1437 -
  1.1438 -subsubsection {* Cardinality of sums *}
  1.1439 -
  1.1440 -lemma card_Plus:
  1.1441 -  assumes "finite A" and "finite B"
  1.1442 -  shows "card (A <+> B) = card A + card B"
  1.1443 -proof -
  1.1444 -  have "Inl`A \<inter> Inr`B = {}" by fast
  1.1445 -  with assms show ?thesis
  1.1446 -    unfolding Plus_def
  1.1447 -    by (simp add: card_Un_disjoint card_image)
  1.1448 -qed
  1.1449 -
  1.1450 -lemma card_Plus_conv_if:
  1.1451 -  "card (A <+> B) = (if finite A \<and> finite B then card(A) + card(B) else 0)"
  1.1452 -by(auto simp: card_def setsum_Plus simp del: setsum_constant)
  1.1453 -
  1.1454 -
  1.1455 -subsubsection {* Cardinality of the Powerset *}
  1.1456 -
  1.1457 -lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
  1.1458 -apply (induct set: finite)
  1.1459 - apply (simp_all add: Pow_insert)
  1.1460 -apply (subst card_Un_disjoint, blast)
  1.1461 -  apply (blast intro: finite_imageI, blast)
  1.1462 -apply (subgoal_tac "inj_on (insert x) (Pow F)")
  1.1463 - apply (simp add: card_image Pow_insert)
  1.1464 -apply (unfold inj_on_def)
  1.1465 -apply (blast elim!: equalityE)
  1.1466 -done
  1.1467 -
  1.1468 -text {* Relates to equivalence classes.  Based on a theorem of F. Kammüller.  *}
  1.1469 -
  1.1470 -lemma dvd_partition:
  1.1471 -  "finite (Union C) ==>
  1.1472 -    ALL c : C. k dvd card c ==>
  1.1473 -    (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
  1.1474 -  k dvd card (Union C)"
  1.1475 -apply(frule finite_UnionD)
  1.1476 -apply(rotate_tac -1)
  1.1477 -apply (induct set: finite, simp_all, clarify)
  1.1478 -apply (subst card_Un_disjoint)
  1.1479 -   apply (auto simp add: disjoint_eq_subset_Compl)
  1.1480 -done
  1.1481 -
  1.1482 -
  1.1483 -subsubsection {* Relating injectivity and surjectivity *}
  1.1484 -
  1.1485 -lemma finite_surj_inj: "finite(A) \<Longrightarrow> A <= f`A \<Longrightarrow> inj_on f A"
  1.1486 -apply(rule eq_card_imp_inj_on, assumption)
  1.1487 -apply(frule finite_imageI)
  1.1488 -apply(drule (1) card_seteq)
  1.1489 - apply(erule card_image_le)
  1.1490 -apply simp
  1.1491 -done
  1.1492 -
  1.1493 -lemma finite_UNIV_surj_inj: fixes f :: "'a \<Rightarrow> 'a"
  1.1494 -shows "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
  1.1495 -by (blast intro: finite_surj_inj subset_UNIV dest:surj_range)
  1.1496 -
  1.1497 -lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a"
  1.1498 -shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
  1.1499 -by(fastsimp simp:surj_def dest!: endo_inj_surj)
  1.1500 -
  1.1501 -corollary infinite_UNIV_nat[iff]: "~finite(UNIV::nat set)"
  1.1502 -proof
  1.1503 -  assume "finite(UNIV::nat set)"
  1.1504 -  with finite_UNIV_inj_surj[of Suc]
  1.1505 -  show False by simp (blast dest: Suc_neq_Zero surjD)
  1.1506 -qed
  1.1507 -
  1.1508 -(* Often leads to bogus ATP proofs because of reduced type information, hence noatp *)
  1.1509 -lemma infinite_UNIV_char_0[noatp]:
  1.1510 -  "\<not> finite (UNIV::'a::semiring_char_0 set)"
  1.1511 -proof
  1.1512 -  assume "finite (UNIV::'a set)"
  1.1513 -  with subset_UNIV have "finite (range of_nat::'a set)"
  1.1514 -    by (rule finite_subset)
  1.1515 -  moreover have "inj (of_nat::nat \<Rightarrow> 'a)"
  1.1516 -    by (simp add: inj_on_def)
  1.1517 -  ultimately have "finite (UNIV::nat set)"
  1.1518 -    by (rule finite_imageD)
  1.1519 -  then show "False"
  1.1520 -    by simp
  1.1521 -qed
  1.1522  
  1.1523  subsection{* A fold functional for non-empty sets *}
  1.1524  
  1.1525 @@ -2811,561 +1354,6 @@
  1.1526  qed
  1.1527  
  1.1528  
  1.1529 -subsubsection {* Fold1 in lattices with @{const inf} and @{const sup} *}
  1.1530 -
  1.1531 -text{*
  1.1532 -  As an application of @{text fold1} we define infimum
  1.1533 -  and supremum in (not necessarily complete!) lattices
  1.1534 -  over (non-empty) sets by means of @{text fold1}.
  1.1535 -*}
  1.1536 -
  1.1537 -context semilattice_inf
  1.1538 -begin
  1.1539 -
  1.1540 -lemma below_fold1_iff:
  1.1541 -  assumes "finite A" "A \<noteq> {}"
  1.1542 -  shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
  1.1543 -proof -
  1.1544 -  interpret ab_semigroup_idem_mult inf
  1.1545 -    by (rule ab_semigroup_idem_mult_inf)
  1.1546 -  show ?thesis using assms by (induct rule: finite_ne_induct) simp_all
  1.1547 -qed
  1.1548 -
  1.1549 -lemma fold1_belowI:
  1.1550 -  assumes "finite A"
  1.1551 -    and "a \<in> A"
  1.1552 -  shows "fold1 inf A \<le> a"
  1.1553 -proof -
  1.1554 -  from assms have "A \<noteq> {}" by auto
  1.1555 -  from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
  1.1556 -  proof (induct rule: finite_ne_induct)
  1.1557 -    case singleton thus ?case by simp
  1.1558 -  next
  1.1559 -    interpret ab_semigroup_idem_mult inf
  1.1560 -      by (rule ab_semigroup_idem_mult_inf)
  1.1561 -    case (insert x F)
  1.1562 -    from insert(5) have "a = x \<or> a \<in> F" by simp
  1.1563 -    thus ?case
  1.1564 -    proof
  1.1565 -      assume "a = x" thus ?thesis using insert
  1.1566 -        by (simp add: mult_ac)
  1.1567 -    next
  1.1568 -      assume "a \<in> F"
  1.1569 -      hence bel: "fold1 inf F \<le> a" by (rule insert)
  1.1570 -      have "inf (fold1 inf (insert x F)) a = inf x (inf (fold1 inf F) a)"
  1.1571 -        using insert by (simp add: mult_ac)
  1.1572 -      also have "inf (fold1 inf F) a = fold1 inf F"
  1.1573 -        using bel by (auto intro: antisym)
  1.1574 -      also have "inf x \<dots> = fold1 inf (insert x F)"
  1.1575 -        using insert by (simp add: mult_ac)
  1.1576 -      finally have aux: "inf (fold1 inf (insert x F)) a = fold1 inf (insert x F)" .
  1.1577 -      moreover have "inf (fold1 inf (insert x F)) a \<le> a" by simp
  1.1578 -      ultimately show ?thesis by simp
  1.1579 -    qed
  1.1580 -  qed
  1.1581 -qed
  1.1582 -
  1.1583 -end
  1.1584 -
  1.1585 -context lattice
  1.1586 -begin
  1.1587 -
  1.1588 -definition
  1.1589 -  Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900)
  1.1590 -where
  1.1591 -  "Inf_fin = fold1 inf"
  1.1592 -
  1.1593 -definition
  1.1594 -  Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900)
  1.1595 -where
  1.1596 -  "Sup_fin = fold1 sup"
  1.1597 -
  1.1598 -lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A"
  1.1599 -apply(unfold Sup_fin_def Inf_fin_def)
  1.1600 -apply(subgoal_tac "EX a. a:A")
  1.1601 -prefer 2 apply blast
  1.1602 -apply(erule exE)
  1.1603 -apply(rule order_trans)
  1.1604 -apply(erule (1) fold1_belowI)
  1.1605 -apply(erule (1) semilattice_inf.fold1_belowI [OF dual_semilattice])
  1.1606 -done
  1.1607 -
  1.1608 -lemma sup_Inf_absorb [simp]:
  1.1609 -  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^bsub>fin\<^esub>A) = a"
  1.1610 -apply(subst sup_commute)
  1.1611 -apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI)
  1.1612 -done
  1.1613 -
  1.1614 -lemma inf_Sup_absorb [simp]:
  1.1615 -  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a"
  1.1616 -by (simp add: Sup_fin_def inf_absorb1
  1.1617 -  semilattice_inf.fold1_belowI [OF dual_semilattice])
  1.1618 -
  1.1619 -end
  1.1620 -
  1.1621 -context distrib_lattice
  1.1622 -begin
  1.1623 -
  1.1624 -lemma sup_Inf1_distrib:
  1.1625 -  assumes "finite A"
  1.1626 -    and "A \<noteq> {}"
  1.1627 -  shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
  1.1628 -proof -
  1.1629 -  interpret ab_semigroup_idem_mult inf
  1.1630 -    by (rule ab_semigroup_idem_mult_inf)
  1.1631 -  from assms show ?thesis
  1.1632 -    by (simp add: Inf_fin_def image_def
  1.1633 -      hom_fold1_commute [where h="sup x", OF sup_inf_distrib1])
  1.1634 -        (rule arg_cong [where f="fold1 inf"], blast)
  1.1635 -qed
  1.1636 -
  1.1637 -lemma sup_Inf2_distrib:
  1.1638 -  assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  1.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}"
  1.1640 -using A proof (induct rule: finite_ne_induct)
  1.1641 -  case singleton thus ?case
  1.1642 -    by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
  1.1643 -next
  1.1644 -  interpret ab_semigroup_idem_mult inf
  1.1645 -    by (rule ab_semigroup_idem_mult_inf)
  1.1646 -  case (insert x A)
  1.1647 -  have finB: "finite {sup x b |b. b \<in> B}"
  1.1648 -    by(rule finite_surj[where f = "sup x", OF B(1)], auto)
  1.1649 -  have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
  1.1650 -  proof -
  1.1651 -    have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
  1.1652 -      by blast
  1.1653 -    thus ?thesis by(simp add: insert(1) B(1))
  1.1654 -  qed
  1.1655 -  have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  1.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)"
  1.1657 -    using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def])
  1.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)
  1.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})"
  1.1660 -    using insert by(simp add:sup_Inf1_distrib[OF B])
  1.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})"
  1.1662 -    (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M")
  1.1663 -    using B insert
  1.1664 -    by (simp add: Inf_fin_def fold1_Un2 [OF finB _ finAB ne])
  1.1665 -  also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
  1.1666 -    by blast
  1.1667 -  finally show ?case .
  1.1668 -qed
  1.1669 -
  1.1670 -lemma inf_Sup1_distrib:
  1.1671 -  assumes "finite A" and "A \<noteq> {}"
  1.1672 -  shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
  1.1673 -proof -
  1.1674 -  interpret ab_semigroup_idem_mult sup
  1.1675 -    by (rule ab_semigroup_idem_mult_sup)
  1.1676 -  from assms show ?thesis
  1.1677 -    by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1])
  1.1678 -      (rule arg_cong [where f="fold1 sup"], blast)
  1.1679 -qed
  1.1680 -
  1.1681 -lemma inf_Sup2_distrib:
  1.1682 -  assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  1.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}"
  1.1684 -using A proof (induct rule: finite_ne_induct)
  1.1685 -  case singleton thus ?case
  1.1686 -    by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def])
  1.1687 -next
  1.1688 -  case (insert x A)
  1.1689 -  have finB: "finite {inf x b |b. b \<in> B}"
  1.1690 -    by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
  1.1691 -  have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
  1.1692 -  proof -
  1.1693 -    have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
  1.1694 -      by blast
  1.1695 -    thus ?thesis by(simp add: insert(1) B(1))
  1.1696 -  qed
  1.1697 -  have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  1.1698 -  interpret ab_semigroup_idem_mult sup
  1.1699 -    by (rule ab_semigroup_idem_mult_sup)
  1.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)"
  1.1701 -    using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
  1.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)
  1.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})"
  1.1704 -    using insert by(simp add:inf_Sup1_distrib[OF B])
  1.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})"
  1.1706 -    (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M")
  1.1707 -    using B insert
  1.1708 -    by (simp add: Sup_fin_def fold1_Un2 [OF finB _ finAB ne])
  1.1709 -  also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
  1.1710 -    by blast
  1.1711 -  finally show ?case .
  1.1712 -qed
  1.1713 -
  1.1714 -end
  1.1715 -
  1.1716 -
  1.1717 -subsubsection {* Fold1 in linear orders with @{const min} and @{const max} *}
  1.1718 -
  1.1719 -text{*
  1.1720 -  As an application of @{text fold1} we define minimum
  1.1721 -  and maximum in (not necessarily complete!) linear orders
  1.1722 -  over (non-empty) sets by means of @{text fold1}.
  1.1723 -*}
  1.1724 -
  1.1725 -context linorder
  1.1726 -begin
  1.1727 -
  1.1728 -lemma ab_semigroup_idem_mult_min:
  1.1729 -  "ab_semigroup_idem_mult min"
  1.1730 -  proof qed (auto simp add: min_def)
  1.1731 -
  1.1732 -lemma ab_semigroup_idem_mult_max:
  1.1733 -  "ab_semigroup_idem_mult max"
  1.1734 -  proof qed (auto simp add: max_def)
  1.1735 -
  1.1736 -lemma max_lattice:
  1.1737 -  "semilattice_inf (op \<ge>) (op >) max"
  1.1738 -  by (fact min_max.dual_semilattice)
  1.1739 -
  1.1740 -lemma dual_max:
  1.1741 -  "ord.max (op \<ge>) = min"
  1.1742 -  by (auto simp add: ord.max_def_raw min_def expand_fun_eq)
  1.1743 -
  1.1744 -lemma dual_min:
  1.1745 -  "ord.min (op \<ge>) = max"
  1.1746 -  by (auto simp add: ord.min_def_raw max_def expand_fun_eq)
  1.1747 -
  1.1748 -lemma strict_below_fold1_iff:
  1.1749 -  assumes "finite A" and "A \<noteq> {}"
  1.1750 -  shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
  1.1751 -proof -
  1.1752 -  interpret ab_semigroup_idem_mult min
  1.1753 -    by (rule ab_semigroup_idem_mult_min)
  1.1754 -  from assms show ?thesis
  1.1755 -  by (induct rule: finite_ne_induct)
  1.1756 -    (simp_all add: fold1_insert)
  1.1757 -qed
  1.1758 -
  1.1759 -lemma fold1_below_iff:
  1.1760 -  assumes "finite A" and "A \<noteq> {}"
  1.1761 -  shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
  1.1762 -proof -
  1.1763 -  interpret ab_semigroup_idem_mult min
  1.1764 -    by (rule ab_semigroup_idem_mult_min)
  1.1765 -  from assms show ?thesis
  1.1766 -  by (induct rule: finite_ne_induct)
  1.1767 -    (simp_all add: fold1_insert min_le_iff_disj)
  1.1768 -qed
  1.1769 -
  1.1770 -lemma fold1_strict_below_iff:
  1.1771 -  assumes "finite A" and "A \<noteq> {}"
  1.1772 -  shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
  1.1773 -proof -
  1.1774 -  interpret ab_semigroup_idem_mult min
  1.1775 -    by (rule ab_semigroup_idem_mult_min)
  1.1776 -  from assms show ?thesis
  1.1777 -  by (induct rule: finite_ne_induct)
  1.1778 -    (simp_all add: fold1_insert min_less_iff_disj)
  1.1779 -qed
  1.1780 -
  1.1781 -lemma fold1_antimono:
  1.1782 -  assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
  1.1783 -  shows "fold1 min B \<le> fold1 min A"
  1.1784 -proof cases
  1.1785 -  assume "A = B" thus ?thesis by simp
  1.1786 -next
  1.1787 -  interpret ab_semigroup_idem_mult min
  1.1788 -    by (rule ab_semigroup_idem_mult_min)
  1.1789 -  assume "A \<noteq> B"
  1.1790 -  have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
  1.1791 -  have "fold1 min B = fold1 min (A \<union> (B-A))" by(subst B)(rule refl)
  1.1792 -  also have "\<dots> = min (fold1 min A) (fold1 min (B-A))"
  1.1793 -  proof -
  1.1794 -    have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
  1.1795 -    moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`]) (* by(blast intro:finite_Diff prems) fails *)
  1.1796 -    moreover have "(B-A) \<noteq> {}" using prems by blast
  1.1797 -    moreover have "A Int (B-A) = {}" using prems by blast
  1.1798 -    ultimately show ?thesis using `A \<noteq> {}` by (rule_tac fold1_Un)
  1.1799 -  qed
  1.1800 -  also have "\<dots> \<le> fold1 min A" by (simp add: min_le_iff_disj)
  1.1801 -  finally show ?thesis .
  1.1802 -qed
  1.1803 -
  1.1804 -definition
  1.1805 -  Min :: "'a set \<Rightarrow> 'a"
  1.1806 -where
  1.1807 -  "Min = fold1 min"
  1.1808 -
  1.1809 -definition
  1.1810 -  Max :: "'a set \<Rightarrow> 'a"
  1.1811 -where
  1.1812 -  "Max = fold1 max"
  1.1813 -
  1.1814 -lemmas Min_singleton [simp] = fold1_singleton_def [OF Min_def]
  1.1815 -lemmas Max_singleton [simp] = fold1_singleton_def [OF Max_def]
  1.1816 -
  1.1817 -lemma Min_insert [simp]:
  1.1818 -  assumes "finite A" and "A \<noteq> {}"
  1.1819 -  shows "Min (insert x A) = min x (Min 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 show ?thesis by (rule fold1_insert_idem_def [OF Min_def])
  1.1824 -qed
  1.1825 -
  1.1826 -lemma Max_insert [simp]:
  1.1827 -  assumes "finite A" and "A \<noteq> {}"
  1.1828 -  shows "Max (insert x A) = max x (Max 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 show ?thesis by (rule fold1_insert_idem_def [OF Max_def])
  1.1833 -qed
  1.1834 -
  1.1835 -lemma Min_in [simp]:
  1.1836 -  assumes "finite A" and "A \<noteq> {}"
  1.1837 -  shows "Min A \<in> A"
  1.1838 -proof -
  1.1839 -  interpret ab_semigroup_idem_mult min
  1.1840 -    by (rule ab_semigroup_idem_mult_min)
  1.1841 -  from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def)
  1.1842 -qed
  1.1843 -
  1.1844 -lemma Max_in [simp]:
  1.1845 -  assumes "finite A" and "A \<noteq> {}"
  1.1846 -  shows "Max A \<in> A"
  1.1847 -proof -
  1.1848 -  interpret ab_semigroup_idem_mult max
  1.1849 -    by (rule ab_semigroup_idem_mult_max)
  1.1850 -  from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
  1.1851 -qed
  1.1852 -
  1.1853 -lemma Min_Un:
  1.1854 -  assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
  1.1855 -  shows "Min (A \<union> B) = min (Min A) (Min B)"
  1.1856 -proof -
  1.1857 -  interpret ab_semigroup_idem_mult min
  1.1858 -    by (rule ab_semigroup_idem_mult_min)
  1.1859 -  from assms show ?thesis
  1.1860 -    by (simp add: Min_def fold1_Un2)
  1.1861 -qed
  1.1862 -
  1.1863 -lemma Max_Un:
  1.1864 -  assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
  1.1865 -  shows "Max (A \<union> B) = max (Max A) (Max B)"
  1.1866 -proof -
  1.1867 -  interpret ab_semigroup_idem_mult max
  1.1868 -    by (rule ab_semigroup_idem_mult_max)
  1.1869 -  from assms show ?thesis
  1.1870 -    by (simp add: Max_def fold1_Un2)
  1.1871 -qed
  1.1872 -
  1.1873 -lemma hom_Min_commute:
  1.1874 -  assumes "\<And>x y. h (min x y) = min (h x) (h y)"
  1.1875 -    and "finite N" and "N \<noteq> {}"
  1.1876 -  shows "h (Min N) = Min (h ` N)"
  1.1877 -proof -
  1.1878 -  interpret ab_semigroup_idem_mult min
  1.1879 -    by (rule ab_semigroup_idem_mult_min)
  1.1880 -  from assms show ?thesis
  1.1881 -    by (simp add: Min_def hom_fold1_commute)
  1.1882 -qed
  1.1883 -
  1.1884 -lemma hom_Max_commute:
  1.1885 -  assumes "\<And>x y. h (max x y) = max (h x) (h y)"
  1.1886 -    and "finite N" and "N \<noteq> {}"
  1.1887 -  shows "h (Max N) = Max (h ` N)"
  1.1888 -proof -
  1.1889 -  interpret ab_semigroup_idem_mult max
  1.1890 -    by (rule ab_semigroup_idem_mult_max)
  1.1891 -  from assms show ?thesis
  1.1892 -    by (simp add: Max_def hom_fold1_commute [of h])
  1.1893 -qed
  1.1894 -
  1.1895 -lemma Min_le [simp]:
  1.1896 -  assumes "finite A" and "x \<in> A"
  1.1897 -  shows "Min A \<le> x"
  1.1898 -  using assms by (simp add: Min_def min_max.fold1_belowI)
  1.1899 -
  1.1900 -lemma Max_ge [simp]:
  1.1901 -  assumes "finite A" and "x \<in> A"
  1.1902 -  shows "x \<le> Max A"
  1.1903 -proof -
  1.1904 -  interpret semilattice_inf "op \<ge>" "op >" max
  1.1905 -    by (rule max_lattice)
  1.1906 -  from assms show ?thesis by (simp add: Max_def fold1_belowI)
  1.1907 -qed
  1.1908 -
  1.1909 -lemma Min_ge_iff [simp, noatp]:
  1.1910 -  assumes "finite A" and "A \<noteq> {}"
  1.1911 -  shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
  1.1912 -  using assms by (simp add: Min_def min_max.below_fold1_iff)
  1.1913 -
  1.1914 -lemma Max_le_iff [simp, noatp]:
  1.1915 -  assumes "finite A" and "A \<noteq> {}"
  1.1916 -  shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
  1.1917 -proof -
  1.1918 -  interpret semilattice_inf "op \<ge>" "op >" max
  1.1919 -    by (rule max_lattice)
  1.1920 -  from assms show ?thesis by (simp add: Max_def below_fold1_iff)
  1.1921 -qed
  1.1922 -
  1.1923 -lemma Min_gr_iff [simp, noatp]:
  1.1924 -  assumes "finite A" and "A \<noteq> {}"
  1.1925 -  shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
  1.1926 -  using assms by (simp add: Min_def strict_below_fold1_iff)
  1.1927 -
  1.1928 -lemma Max_less_iff [simp, noatp]:
  1.1929 -  assumes "finite A" and "A \<noteq> {}"
  1.1930 -  shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
  1.1931 -proof -
  1.1932 -  interpret dual: linorder "op \<ge>" "op >"
  1.1933 -    by (rule dual_linorder)
  1.1934 -  from assms show ?thesis
  1.1935 -    by (simp add: Max_def dual.strict_below_fold1_iff [folded dual.dual_max])
  1.1936 -qed
  1.1937 -
  1.1938 -lemma Min_le_iff [noatp]:
  1.1939 -  assumes "finite A" and "A \<noteq> {}"
  1.1940 -  shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
  1.1941 -  using assms by (simp add: Min_def fold1_below_iff)
  1.1942 -
  1.1943 -lemma Max_ge_iff [noatp]:
  1.1944 -  assumes "finite A" and "A \<noteq> {}"
  1.1945 -  shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
  1.1946 -proof -
  1.1947 -  interpret dual: linorder "op \<ge>" "op >"
  1.1948 -    by (rule dual_linorder)
  1.1949 -  from assms show ?thesis
  1.1950 -    by (simp add: Max_def dual.fold1_below_iff [folded dual.dual_max])
  1.1951 -qed
  1.1952 -
  1.1953 -lemma Min_less_iff [noatp]:
  1.1954 -  assumes "finite A" and "A \<noteq> {}"
  1.1955 -  shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
  1.1956 -  using assms by (simp add: Min_def fold1_strict_below_iff)
  1.1957 -
  1.1958 -lemma Max_gr_iff [noatp]:
  1.1959 -  assumes "finite A" and "A \<noteq> {}"
  1.1960 -  shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
  1.1961 -proof -
  1.1962 -  interpret dual: linorder "op \<ge>" "op >"
  1.1963 -    by (rule dual_linorder)
  1.1964 -  from assms show ?thesis
  1.1965 -    by (simp add: Max_def dual.fold1_strict_below_iff [folded dual.dual_max])
  1.1966 -qed
  1.1967 -
  1.1968 -lemma Min_eqI:
  1.1969 -  assumes "finite A"
  1.1970 -  assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
  1.1971 -    and "x \<in> A"
  1.1972 -  shows "Min A = x"
  1.1973 -proof (rule antisym)
  1.1974 -  from `x \<in> A` have "A \<noteq> {}" by auto
  1.1975 -  with assms show "Min A \<ge> x" by simp
  1.1976 -next
  1.1977 -  from assms show "x \<ge> Min A" by simp
  1.1978 -qed
  1.1979 -
  1.1980 -lemma Max_eqI:
  1.1981 -  assumes "finite A"
  1.1982 -  assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
  1.1983 -    and "x \<in> A"
  1.1984 -  shows "Max A = x"
  1.1985 -proof (rule antisym)
  1.1986 -  from `x \<in> A` have "A \<noteq> {}" by auto
  1.1987 -  with assms show "Max A \<le> x" by simp
  1.1988 -next
  1.1989 -  from assms show "x \<le> Max A" by simp
  1.1990 -qed
  1.1991 -
  1.1992 -lemma Min_antimono:
  1.1993 -  assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
  1.1994 -  shows "Min N \<le> Min M"
  1.1995 -  using assms by (simp add: Min_def fold1_antimono)
  1.1996 -
  1.1997 -lemma Max_mono:
  1.1998 -  assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
  1.1999 -  shows "Max M \<le> Max N"
  1.2000 -proof -
  1.2001 -  interpret dual: linorder "op \<ge>" "op >"
  1.2002 -    by (rule dual_linorder)
  1.2003 -  from assms show ?thesis
  1.2004 -    by (simp add: Max_def dual.fold1_antimono [folded dual.dual_max])
  1.2005 -qed
  1.2006 -
  1.2007 -lemma finite_linorder_max_induct[consumes 1, case_names empty insert]:
  1.2008 - "finite A \<Longrightarrow> P {} \<Longrightarrow>
  1.2009 -  (!!b A. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
  1.2010 -  \<Longrightarrow> P A"
  1.2011 -proof (induct rule: finite_psubset_induct)
  1.2012 -  fix A :: "'a set"
  1.2013 -  assume IH: "!! B. finite B \<Longrightarrow> B < A \<Longrightarrow> P {} \<Longrightarrow>
  1.2014 -                 (!!b A. finite A \<Longrightarrow> (\<forall>a\<in>A. a<b) \<Longrightarrow> P A \<Longrightarrow> P (insert b A))
  1.2015 -                  \<Longrightarrow> P B"
  1.2016 -  and "finite A" and "P {}"
  1.2017 -  and step: "!!b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
  1.2018 -  show "P A"
  1.2019 -  proof (cases "A = {}")
  1.2020 -    assume "A = {}" thus "P A" using `P {}` by simp
  1.2021 -  next
  1.2022 -    let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B"
  1.2023 -    assume "A \<noteq> {}"
  1.2024 -    with `finite A` have "Max A : A" by auto
  1.2025 -    hence A: "?A = A" using insert_Diff_single insert_absorb by auto
  1.2026 -    moreover have "finite ?B" using `finite A` by simp
  1.2027 -    ultimately have "P ?B" using `P {}` step IH[of ?B] by blast
  1.2028 -    moreover have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastsimp
  1.2029 -    ultimately show "P A" using A insert_Diff_single step[OF `finite ?B`] by fastsimp
  1.2030 -  qed
  1.2031 -qed
  1.2032 -
  1.2033 -lemma finite_linorder_min_induct[consumes 1, case_names empty insert]:
  1.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"
  1.2035 -by(rule linorder.finite_linorder_max_induct[OF dual_linorder])
  1.2036 -
  1.2037 -end
  1.2038 -
  1.2039 -context linordered_ab_semigroup_add
  1.2040 -begin
  1.2041 -
  1.2042 -lemma add_Min_commute:
  1.2043 -  fixes k
  1.2044 -  assumes "finite N" and "N \<noteq> {}"
  1.2045 -  shows "k + Min N = Min {k + m | m. m \<in> N}"
  1.2046 -proof -
  1.2047 -  have "\<And>x y. k + min x y = min (k + x) (k + y)"
  1.2048 -    by (simp add: min_def not_le)
  1.2049 -      (blast intro: antisym less_imp_le add_left_mono)
  1.2050 -  with assms show ?thesis
  1.2051 -    using hom_Min_commute [of "plus k" N]
  1.2052 -    by simp (blast intro: arg_cong [where f = Min])
  1.2053 -qed
  1.2054 -
  1.2055 -lemma add_Max_commute:
  1.2056 -  fixes k
  1.2057 -  assumes "finite N" and "N \<noteq> {}"
  1.2058 -  shows "k + Max N = Max {k + m | m. m \<in> N}"
  1.2059 -proof -
  1.2060 -  have "\<And>x y. k + max x y = max (k + x) (k + y)"
  1.2061 -    by (simp add: max_def not_le)
  1.2062 -      (blast intro: antisym less_imp_le add_left_mono)
  1.2063 -  with assms show ?thesis
  1.2064 -    using hom_Max_commute [of "plus k" N]
  1.2065 -    by simp (blast intro: arg_cong [where f = Max])
  1.2066 -qed
  1.2067 -
  1.2068 -end
  1.2069 -
  1.2070 -context linordered_ab_group_add
  1.2071 -begin
  1.2072 -
  1.2073 -lemma minus_Max_eq_Min [simp]:
  1.2074 -  "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Max S) = Min (uminus ` S)"
  1.2075 -  by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min)
  1.2076 -
  1.2077 -lemma minus_Min_eq_Max [simp]:
  1.2078 -  "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Min S) = Max (uminus ` S)"
  1.2079 -  by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max)
  1.2080 -
  1.2081 -end
  1.2082 -
  1.2083 -
  1.2084  subsection {* Expressing set operations via @{const fold} *}
  1.2085  
  1.2086  lemma (in fun_left_comm) fun_left_comm_apply:
  1.2087 @@ -3445,32 +1433,6 @@
  1.2088    shows "Sup A = fold sup bot A"
  1.2089    using assms sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2)
  1.2090  
  1.2091 -lemma Inf_fin_Inf:
  1.2092 -  assumes "finite A" and "A \<noteq> {}"
  1.2093 -  shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
  1.2094 -proof -
  1.2095 -  interpret ab_semigroup_idem_mult inf
  1.2096 -    by (rule ab_semigroup_idem_mult_inf)
  1.2097 -  from `A \<noteq> {}` obtain b B where "A = insert b B" by auto
  1.2098 -  moreover with `finite A` have "finite B" by simp
  1.2099 -  ultimately show ?thesis  
  1.2100 -  by (simp add: Inf_fin_def fold1_eq_fold_idem inf_Inf_fold_inf [symmetric])
  1.2101 -    (simp add: Inf_fold_inf)
  1.2102 -qed
  1.2103 -
  1.2104 -lemma Sup_fin_Sup:
  1.2105 -  assumes "finite A" and "A \<noteq> {}"
  1.2106 -  shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
  1.2107 -proof -
  1.2108 -  interpret ab_semigroup_idem_mult sup
  1.2109 -    by (rule ab_semigroup_idem_mult_sup)
  1.2110 -  from `A \<noteq> {}` obtain b B where "A = insert b B" by auto
  1.2111 -  moreover with `finite A` have "finite B" by simp
  1.2112 -  ultimately show ?thesis  
  1.2113 -  by (simp add: Sup_fin_def fold1_eq_fold_idem sup_Sup_fold_sup [symmetric])
  1.2114 -    (simp add: Sup_fold_sup)
  1.2115 -qed
  1.2116 -
  1.2117  lemma inf_INFI_fold_inf:
  1.2118    assumes "finite A"
  1.2119    shows "inf B (INFI A f) = fold (\<lambda>A. inf (f A)) B A" (is "?inf = ?fold") 
  1.2120 @@ -3505,4 +1467,127 @@
  1.2121  
  1.2122  end
  1.2123  
  1.2124 +
  1.2125 +subsection {* Locales as mini-packages *}
  1.2126 +
  1.2127 +locale folding =
  1.2128 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
  1.2129 +  fixes F :: "'a set \<Rightarrow> 'b \<Rightarrow> 'b"
  1.2130 +  assumes commute_comp: "f x \<circ> f y = f y \<circ> f x"
  1.2131 +  assumes eq_fold: "F A s = Finite_Set.fold f s A"
  1.2132 +begin
  1.2133 +
  1.2134 +lemma fun_left_commute:
  1.2135 +  "f x (f y s) = f y (f x s)"
  1.2136 +  using commute_comp [of x y] by (simp add: expand_fun_eq)
  1.2137 +
  1.2138 +lemma fun_left_comm:
  1.2139 +  "fun_left_comm f"
  1.2140 +proof
  1.2141 +qed (fact fun_left_commute)
  1.2142 +
  1.2143 +lemma empty [simp]:
  1.2144 +  "F {} = id"
  1.2145 +  by (simp add: eq_fold expand_fun_eq)
  1.2146 +
  1.2147 +lemma insert [simp]:
  1.2148 +  assumes "finite A" and "x \<notin> A"
  1.2149 +  shows "F (insert x A) = F A \<circ> f x"
  1.2150 +proof -
  1.2151 +  interpret fun_left_comm f by (fact fun_left_comm)
  1.2152 +  from fold_insert2 assms
  1.2153 +  have "\<And>s. Finite_Set.fold f s (insert x A) = Finite_Set.fold f (f x s) A" .
  1.2154 +  then show ?thesis by (simp add: eq_fold expand_fun_eq)
  1.2155 +qed
  1.2156 +
  1.2157 +lemma remove:
  1.2158 +  assumes "finite A" and "x \<in> A"
  1.2159 +  shows "F A = F (A - {x}) \<circ> f x"
  1.2160 +proof -
  1.2161 +  from `x \<in> A` obtain B where A: "A = insert x B" and "x \<notin> B"
  1.2162 +    by (auto dest: mk_disjoint_insert)
  1.2163 +  moreover from `finite A` this have "finite B" by simp
  1.2164 +  ultimately show ?thesis by simp
  1.2165 +qed
  1.2166 +
  1.2167 +lemma insert_remove:
  1.2168 +  assumes "finite A"
  1.2169 +  shows "F (insert x A) = F (A - {x}) \<circ> f x"
  1.2170 +proof (cases "x \<in> A")
  1.2171 +  case True with assms show ?thesis by (simp add: remove insert_absorb)
  1.2172 +next
  1.2173 +  case False with assms show ?thesis by simp
  1.2174 +qed
  1.2175 +
  1.2176 +lemma commute_comp':
  1.2177 +  assumes "finite A"
  1.2178 +  shows "f x \<circ> F A = F A \<circ> f x"
  1.2179 +proof (rule ext)
  1.2180 +  fix s
  1.2181 +  from assms show "(f x \<circ> F A) s = (F A \<circ> f x) s"
  1.2182 +    by (induct A arbitrary: s) (simp_all add: fun_left_commute)
  1.2183 +qed
  1.2184 +
  1.2185 +lemma fun_left_commute':
  1.2186 +  assumes "finite A"
  1.2187 +  shows "f x (F A s) = F A (f x s)"
  1.2188 +  using commute_comp' assms by (simp add: expand_fun_eq)
  1.2189 +
  1.2190 +lemma union:
  1.2191 +  assumes "finite A" and "finite B"
  1.2192 +  and "A \<inter> B = {}"
  1.2193 +  shows "F (A \<union> B) = F A \<circ> F B"
  1.2194 +using `finite A` `A \<inter> B = {}` proof (induct A)
  1.2195 +  case empty show ?case by simp
  1.2196 +next
  1.2197 +  case (insert x A)
  1.2198 +  then have "A \<inter> B = {}" by auto
  1.2199 +  with insert(3) have "F (A \<union> B) = F A \<circ> F B" .
  1.2200 +  moreover from insert have "x \<notin> B" by simp
  1.2201 +  moreover from `finite A` `finite B` have fin: "finite (A \<union> B)" by simp
  1.2202 +  moreover from `x \<notin> A` `x \<notin> B` have "x \<notin> A \<union> B" by simp
  1.2203 +  ultimately show ?case by (simp add: fun_left_commute')
  1.2204 +qed
  1.2205 +
  1.2206  end
  1.2207 +
  1.2208 +locale folding_idem = folding +
  1.2209 +  assumes idem_comp: "f x \<circ> f x = f x"
  1.2210 +begin
  1.2211 +
  1.2212 +declare insert [simp del]
  1.2213 +
  1.2214 +lemma fun_idem:
  1.2215 +  "f x (f x s) = f x s"
  1.2216 +  using idem_comp [of x] by (simp add: expand_fun_eq)
  1.2217 +
  1.2218 +lemma fun_left_comm_idem:
  1.2219 +  "fun_left_comm_idem f"
  1.2220 +proof
  1.2221 +qed (fact fun_left_commute fun_idem)+
  1.2222 +
  1.2223 +lemma insert_idem [simp]:
  1.2224 +  assumes "finite A"
  1.2225 +  shows "F (insert x A) = F A \<circ> f x"
  1.2226 +proof -
  1.2227 +  interpret fun_left_comm_idem f by (fact fun_left_comm_idem)
  1.2228 +  from fold_insert_idem2 assms
  1.2229 +  have "\<And>s. Finite_Set.fold f s (insert x A) = Finite_Set.fold f (f x s) A" .
  1.2230 +  then show ?thesis by (simp add: eq_fold expand_fun_eq)
  1.2231 +qed
  1.2232 +
  1.2233 +lemma union_idem:
  1.2234 +  assumes "finite A" and "finite B"
  1.2235 +  shows "F (A \<union> B) = F A \<circ> F B"
  1.2236 +using `finite A` proof (induct A)
  1.2237 +  case empty show ?case by simp
  1.2238 +next
  1.2239 +  case (insert x A)
  1.2240 +  from insert(3) have "F (A \<union> B) = F A \<circ> F B" .
  1.2241 +  moreover from `finite A` `finite B` have fin: "finite (A \<union> B)" by simp
  1.2242 +  ultimately show ?case by (simp add: fun_left_commute')
  1.2243 +qed
  1.2244 +
  1.2245 +end
  1.2246 +
  1.2247 +end