more algebraic terminology for theories about big operators
authorhaftmann
Sun Dec 15 15:10:14 2013 +0100 (2013-12-15)
changeset 547441e7f2d296e19
parent 54743 b9ae4a2f615b
child 54745 46e441e61ff5
more algebraic terminology for theories about big operators
src/Doc/Main/Main_Doc.thy
src/HOL/Big_Operators.thy
src/HOL/Equiv_Relations.thy
src/HOL/Groups_Big.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Lattices_Big.thy
     1.1 --- a/src/Doc/Main/Main_Doc.thy	Sat Dec 14 20:46:36 2013 +0100
     1.2 +++ b/src/Doc/Main/Main_Doc.thy	Sun Dec 15 15:10:14 2013 +0100
     1.3 @@ -407,8 +407,8 @@
     1.4  @{const Finite_Set.finite} & @{term_type_only Finite_Set.finite "'a set\<Rightarrow>bool"}\\
     1.5  @{const Finite_Set.card} & @{term_type_only Finite_Set.card "'a set => nat"}\\
     1.6  @{const Finite_Set.fold} & @{term_type_only Finite_Set.fold "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"}\\
     1.7 -@{const Big_Operators.setsum} & @{term_type_only Big_Operators.setsum "('a => 'b) => 'a set => 'b::comm_monoid_add"}\\
     1.8 -@{const Big_Operators.setprod} & @{term_type_only Big_Operators.setprod "('a => 'b) => 'a set => 'b::comm_monoid_mult"}\\
     1.9 +@{const Groups_Big.setsum} & @{term_type_only Groups_Big.setsum "('a => 'b) => 'a set => 'b::comm_monoid_add"}\\
    1.10 +@{const Groups_Big.setprod} & @{term_type_only Groups_Big.setprod "('a => 'b) => 'a set => 'b::comm_monoid_mult"}\\
    1.11  \end{supertabular}
    1.12  
    1.13  
     2.1 --- a/src/HOL/Big_Operators.thy	Sat Dec 14 20:46:36 2013 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,2193 +0,0 @@
     2.4 -(*  Title:      HOL/Big_Operators.thy
     2.5 -    Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     2.6 -                with contributions by Jeremy Avigad
     2.7 -*)
     2.8 -
     2.9 -header {* Big operators and finite (non-empty) sets *}
    2.10 -
    2.11 -theory Big_Operators
    2.12 -imports Finite_Set Metis
    2.13 -begin
    2.14 -
    2.15 -subsection {* Generic monoid operation over a set *}
    2.16 -
    2.17 -no_notation times (infixl "*" 70)
    2.18 -no_notation Groups.one ("1")
    2.19 -
    2.20 -locale comm_monoid_set = comm_monoid
    2.21 -begin
    2.22 -
    2.23 -interpretation comp_fun_commute f
    2.24 -  by default (simp add: fun_eq_iff left_commute)
    2.25 -
    2.26 -interpretation comp_fun_commute "f \<circ> g"
    2.27 -  by (rule comp_comp_fun_commute)
    2.28 -
    2.29 -definition F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
    2.30 -where
    2.31 -  eq_fold: "F g A = Finite_Set.fold (f \<circ> g) 1 A"
    2.32 -
    2.33 -lemma infinite [simp]:
    2.34 -  "\<not> finite A \<Longrightarrow> F g A = 1"
    2.35 -  by (simp add: eq_fold)
    2.36 -
    2.37 -lemma empty [simp]:
    2.38 -  "F g {} = 1"
    2.39 -  by (simp add: eq_fold)
    2.40 -
    2.41 -lemma insert [simp]:
    2.42 -  assumes "finite A" and "x \<notin> A"
    2.43 -  shows "F g (insert x A) = g x * F g A"
    2.44 -  using assms by (simp add: eq_fold)
    2.45 -
    2.46 -lemma remove:
    2.47 -  assumes "finite A" and "x \<in> A"
    2.48 -  shows "F g A = g x * F g (A - {x})"
    2.49 -proof -
    2.50 -  from `x \<in> A` obtain B where A: "A = insert x B" and "x \<notin> B"
    2.51 -    by (auto dest: mk_disjoint_insert)
    2.52 -  moreover from `finite A` A have "finite B" by simp
    2.53 -  ultimately show ?thesis by simp
    2.54 -qed
    2.55 -
    2.56 -lemma insert_remove:
    2.57 -  assumes "finite A"
    2.58 -  shows "F g (insert x A) = g x * F g (A - {x})"
    2.59 -  using assms by (cases "x \<in> A") (simp_all add: remove insert_absorb)
    2.60 -
    2.61 -lemma neutral:
    2.62 -  assumes "\<forall>x\<in>A. g x = 1"
    2.63 -  shows "F g A = 1"
    2.64 -  using assms by (induct A rule: infinite_finite_induct) simp_all
    2.65 -
    2.66 -lemma neutral_const [simp]:
    2.67 -  "F (\<lambda>_. 1) A = 1"
    2.68 -  by (simp add: neutral)
    2.69 -
    2.70 -lemma union_inter:
    2.71 -  assumes "finite A" and "finite B"
    2.72 -  shows "F g (A \<union> B) * F g (A \<inter> B) = F g A * F g B"
    2.73 -  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
    2.74 -using assms proof (induct A)
    2.75 -  case empty then show ?case by simp
    2.76 -next
    2.77 -  case (insert x A) then show ?case
    2.78 -    by (auto simp add: insert_absorb Int_insert_left commute [of _ "g x"] assoc left_commute)
    2.79 -qed
    2.80 -
    2.81 -corollary union_inter_neutral:
    2.82 -  assumes "finite A" and "finite B"
    2.83 -  and I0: "\<forall>x \<in> A \<inter> B. g x = 1"
    2.84 -  shows "F g (A \<union> B) = F g A * F g B"
    2.85 -  using assms by (simp add: union_inter [symmetric] neutral)
    2.86 -
    2.87 -corollary union_disjoint:
    2.88 -  assumes "finite A" and "finite B"
    2.89 -  assumes "A \<inter> B = {}"
    2.90 -  shows "F g (A \<union> B) = F g A * F g B"
    2.91 -  using assms by (simp add: union_inter_neutral)
    2.92 -
    2.93 -lemma subset_diff:
    2.94 -  "B \<subseteq> A \<Longrightarrow> finite A \<Longrightarrow> F g A = F g (A - B) * F g B"
    2.95 -  by (metis Diff_partition union_disjoint Diff_disjoint finite_Un inf_commute sup_commute)
    2.96 -
    2.97 -lemma reindex:
    2.98 -  assumes "inj_on h A"
    2.99 -  shows "F g (h ` A) = F (g \<circ> h) A"
   2.100 -proof (cases "finite A")
   2.101 -  case True
   2.102 -  with assms show ?thesis by (simp add: eq_fold fold_image comp_assoc)
   2.103 -next
   2.104 -  case False with assms have "\<not> finite (h ` A)" by (blast dest: finite_imageD)
   2.105 -  with False show ?thesis by simp
   2.106 -qed
   2.107 -
   2.108 -lemma cong:
   2.109 -  assumes "A = B"
   2.110 -  assumes g_h: "\<And>x. x \<in> B \<Longrightarrow> g x = h x"
   2.111 -  shows "F g A = F h B"
   2.112 -proof (cases "finite A")
   2.113 -  case True
   2.114 -  then have "\<And>C. C \<subseteq> A \<longrightarrow> (\<forall>x\<in>C. g x = h x) \<longrightarrow> F g C = F h C"
   2.115 -  proof induct
   2.116 -    case empty then show ?case by simp
   2.117 -  next
   2.118 -    case (insert x F) then show ?case apply -
   2.119 -    apply (simp add: subset_insert_iff, clarify)
   2.120 -    apply (subgoal_tac "finite C")
   2.121 -      prefer 2 apply (blast dest: finite_subset [rotated])
   2.122 -    apply (subgoal_tac "C = insert x (C - {x})")
   2.123 -      prefer 2 apply blast
   2.124 -    apply (erule ssubst)
   2.125 -    apply (simp add: Ball_def del: insert_Diff_single)
   2.126 -    done
   2.127 -  qed
   2.128 -  with `A = B` g_h show ?thesis by simp
   2.129 -next
   2.130 -  case False
   2.131 -  with `A = B` show ?thesis by simp
   2.132 -qed
   2.133 -
   2.134 -lemma strong_cong [cong]:
   2.135 -  assumes "A = B" "\<And>x. x \<in> B =simp=> g x = h x"
   2.136 -  shows "F (\<lambda>x. g x) A = F (\<lambda>x. h x) B"
   2.137 -  by (rule cong) (insert assms, simp_all add: simp_implies_def)
   2.138 -
   2.139 -lemma UNION_disjoint:
   2.140 -  assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
   2.141 -  and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
   2.142 -  shows "F g (UNION I A) = F (\<lambda>x. F g (A x)) I"
   2.143 -apply (insert assms)
   2.144 -apply (induct rule: finite_induct)
   2.145 -apply simp
   2.146 -apply atomize
   2.147 -apply (subgoal_tac "\<forall>i\<in>Fa. x \<noteq> i")
   2.148 - prefer 2 apply blast
   2.149 -apply (subgoal_tac "A x Int UNION Fa A = {}")
   2.150 - prefer 2 apply blast
   2.151 -apply (simp add: union_disjoint)
   2.152 -done
   2.153 -
   2.154 -lemma Union_disjoint:
   2.155 -  assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {}"
   2.156 -  shows "F g (Union C) = F (F g) C"
   2.157 -proof cases
   2.158 -  assume "finite C"
   2.159 -  from UNION_disjoint [OF this assms]
   2.160 -  show ?thesis
   2.161 -    by (simp add: SUP_def)
   2.162 -qed (auto dest: finite_UnionD intro: infinite)
   2.163 -
   2.164 -lemma distrib:
   2.165 -  "F (\<lambda>x. g x * h x) A = F g A * F h A"
   2.166 -  using assms by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute)
   2.167 -
   2.168 -lemma Sigma:
   2.169 -  "finite A \<Longrightarrow> \<forall>x\<in>A. finite (B x) \<Longrightarrow> F (\<lambda>x. F (g x) (B x)) A = F (split g) (SIGMA x:A. B x)"
   2.170 -apply (subst Sigma_def)
   2.171 -apply (subst UNION_disjoint, assumption, simp)
   2.172 - apply blast
   2.173 -apply (rule cong)
   2.174 -apply rule
   2.175 -apply (simp add: fun_eq_iff)
   2.176 -apply (subst UNION_disjoint, simp, simp)
   2.177 - apply blast
   2.178 -apply (simp add: comp_def)
   2.179 -done
   2.180 -
   2.181 -lemma related: 
   2.182 -  assumes Re: "R 1 1" 
   2.183 -  and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)" 
   2.184 -  and fS: "finite S" and Rfg: "\<forall>x\<in>S. R (h x) (g x)"
   2.185 -  shows "R (F h S) (F g S)"
   2.186 -  using fS by (rule finite_subset_induct) (insert assms, auto)
   2.187 -
   2.188 -lemma eq_general:
   2.189 -  assumes h: "\<forall>y\<in>S'. \<exists>!x. x \<in> S \<and> h x = y" 
   2.190 -  and f12:  "\<forall>x\<in>S. h x \<in> S' \<and> f2 (h x) = f1 x"
   2.191 -  shows "F f1 S = F f2 S'"
   2.192 -proof-
   2.193 -  from h f12 have hS: "h ` S = S'" by blast
   2.194 -  {fix x y assume H: "x \<in> S" "y \<in> S" "h x = h y"
   2.195 -    from f12 h H  have "x = y" by auto }
   2.196 -  hence hinj: "inj_on h S" unfolding inj_on_def Ex1_def by blast
   2.197 -  from f12 have th: "\<And>x. x \<in> S \<Longrightarrow> (f2 \<circ> h) x = f1 x" by auto 
   2.198 -  from hS have "F f2 S' = F f2 (h ` S)" by simp
   2.199 -  also have "\<dots> = F (f2 o h) S" using reindex [OF hinj, of f2] .
   2.200 -  also have "\<dots> = F f1 S " using th cong [of _ _ "f2 o h" f1]
   2.201 -    by blast
   2.202 -  finally show ?thesis ..
   2.203 -qed
   2.204 -
   2.205 -lemma eq_general_reverses:
   2.206 -  assumes kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
   2.207 -  and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = j x"
   2.208 -  shows "F j S = F g T"
   2.209 -  (* metis solves it, but not yet available here *)
   2.210 -  apply (rule eq_general [of T S h g j])
   2.211 -  apply (rule ballI)
   2.212 -  apply (frule kh)
   2.213 -  apply (rule ex1I[])
   2.214 -  apply blast
   2.215 -  apply clarsimp
   2.216 -  apply (drule hk) apply simp
   2.217 -  apply (rule sym)
   2.218 -  apply (erule conjunct1[OF conjunct2[OF hk]])
   2.219 -  apply (rule ballI)
   2.220 -  apply (drule hk)
   2.221 -  apply blast
   2.222 -  done
   2.223 -
   2.224 -lemma mono_neutral_cong_left:
   2.225 -  assumes "finite T" and "S \<subseteq> T" and "\<forall>i \<in> T - S. h i = 1"
   2.226 -  and "\<And>x. x \<in> S \<Longrightarrow> g x = h x" shows "F g S = F h T"
   2.227 -proof-
   2.228 -  have eq: "T = S \<union> (T - S)" using `S \<subseteq> T` by blast
   2.229 -  have d: "S \<inter> (T - S) = {}" using `S \<subseteq> T` by blast
   2.230 -  from `finite T` `S \<subseteq> T` have f: "finite S" "finite (T - S)"
   2.231 -    by (auto intro: finite_subset)
   2.232 -  show ?thesis using assms(4)
   2.233 -    by (simp add: union_disjoint [OF f d, unfolded eq [symmetric]] neutral [OF assms(3)])
   2.234 -qed
   2.235 -
   2.236 -lemma mono_neutral_cong_right:
   2.237 -  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1; \<And>x. x \<in> S \<Longrightarrow> g x = h x \<rbrakk>
   2.238 -   \<Longrightarrow> F g T = F h S"
   2.239 -  by (auto intro!: mono_neutral_cong_left [symmetric])
   2.240 -
   2.241 -lemma mono_neutral_left:
   2.242 -  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g S = F g T"
   2.243 -  by (blast intro: mono_neutral_cong_left)
   2.244 -
   2.245 -lemma mono_neutral_right:
   2.246 -  "\<lbrakk> finite T;  S \<subseteq> T;  \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g T = F g S"
   2.247 -  by (blast intro!: mono_neutral_left [symmetric])
   2.248 -
   2.249 -lemma delta: 
   2.250 -  assumes fS: "finite S"
   2.251 -  shows "F (\<lambda>k. if k = a then b k else 1) S = (if a \<in> S then b a else 1)"
   2.252 -proof-
   2.253 -  let ?f = "(\<lambda>k. if k=a then b k else 1)"
   2.254 -  { assume a: "a \<notin> S"
   2.255 -    hence "\<forall>k\<in>S. ?f k = 1" by simp
   2.256 -    hence ?thesis  using a by simp }
   2.257 -  moreover
   2.258 -  { assume a: "a \<in> S"
   2.259 -    let ?A = "S - {a}"
   2.260 -    let ?B = "{a}"
   2.261 -    have eq: "S = ?A \<union> ?B" using a by blast 
   2.262 -    have dj: "?A \<inter> ?B = {}" by simp
   2.263 -    from fS have fAB: "finite ?A" "finite ?B" by auto  
   2.264 -    have "F ?f S = F ?f ?A * F ?f ?B"
   2.265 -      using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]]
   2.266 -      by simp
   2.267 -    then have ?thesis using a by simp }
   2.268 -  ultimately show ?thesis by blast
   2.269 -qed
   2.270 -
   2.271 -lemma delta': 
   2.272 -  assumes fS: "finite S"
   2.273 -  shows "F (\<lambda>k. if a = k then b k else 1) S = (if a \<in> S then b a else 1)"
   2.274 -  using delta [OF fS, of a b, symmetric] by (auto intro: cong)
   2.275 -
   2.276 -lemma If_cases:
   2.277 -  fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
   2.278 -  assumes fA: "finite A"
   2.279 -  shows "F (\<lambda>x. if P x then h x else g x) A =
   2.280 -    F h (A \<inter> {x. P x}) * F g (A \<inter> - {x. P x})"
   2.281 -proof -
   2.282 -  have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}" 
   2.283 -          "(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}" 
   2.284 -    by blast+
   2.285 -  from fA 
   2.286 -  have f: "finite (A \<inter> {x. P x})" "finite (A \<inter> -{x. P x})" by auto
   2.287 -  let ?g = "\<lambda>x. if P x then h x else g x"
   2.288 -  from union_disjoint [OF f a(2), of ?g] a(1)
   2.289 -  show ?thesis
   2.290 -    by (subst (1 2) cong) simp_all
   2.291 -qed
   2.292 -
   2.293 -lemma cartesian_product:
   2.294 -   "F (\<lambda>x. F (g x) B) A = F (split g) (A <*> B)"
   2.295 -apply (rule sym)
   2.296 -apply (cases "finite A") 
   2.297 - apply (cases "finite B") 
   2.298 -  apply (simp add: Sigma)
   2.299 - apply (cases "A={}", simp)
   2.300 - apply simp
   2.301 -apply (auto intro: infinite dest: finite_cartesian_productD2)
   2.302 -apply (cases "B = {}") apply (auto intro: infinite dest: finite_cartesian_productD1)
   2.303 -done
   2.304 -
   2.305 -end
   2.306 -
   2.307 -notation times (infixl "*" 70)
   2.308 -notation Groups.one ("1")
   2.309 -
   2.310 -
   2.311 -subsection {* Generalized summation over a set *}
   2.312 -
   2.313 -context comm_monoid_add
   2.314 -begin
   2.315 -
   2.316 -definition setsum :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
   2.317 -where
   2.318 -  "setsum = comm_monoid_set.F plus 0"
   2.319 -
   2.320 -sublocale setsum!: comm_monoid_set plus 0
   2.321 -where
   2.322 -  "comm_monoid_set.F plus 0 = setsum"
   2.323 -proof -
   2.324 -  show "comm_monoid_set plus 0" ..
   2.325 -  then interpret setsum!: comm_monoid_set plus 0 .
   2.326 -  from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
   2.327 -qed
   2.328 -
   2.329 -abbreviation
   2.330 -  Setsum ("\<Sum>_" [1000] 999) where
   2.331 -  "\<Sum>A \<equiv> setsum (%x. x) A"
   2.332 -
   2.333 -end
   2.334 -
   2.335 -text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
   2.336 -written @{text"\<Sum>x\<in>A. e"}. *}
   2.337 -
   2.338 -syntax
   2.339 -  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
   2.340 -syntax (xsymbols)
   2.341 -  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   2.342 -syntax (HTML output)
   2.343 -  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   2.344 -
   2.345 -translations -- {* Beware of argument permutation! *}
   2.346 -  "SUM i:A. b" == "CONST setsum (%i. b) A"
   2.347 -  "\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
   2.348 -
   2.349 -text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
   2.350 - @{text"\<Sum>x|P. e"}. *}
   2.351 -
   2.352 -syntax
   2.353 -  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
   2.354 -syntax (xsymbols)
   2.355 -  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   2.356 -syntax (HTML output)
   2.357 -  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   2.358 -
   2.359 -translations
   2.360 -  "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
   2.361 -  "\<Sum>x|P. t" => "CONST setsum (%x. t) {x. P}"
   2.362 -
   2.363 -print_translation {*
   2.364 -let
   2.365 -  fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
   2.366 -        if x <> y then raise Match
   2.367 -        else
   2.368 -          let
   2.369 -            val x' = Syntax_Trans.mark_bound_body (x, Tx);
   2.370 -            val t' = subst_bound (x', t);
   2.371 -            val P' = subst_bound (x', P);
   2.372 -          in
   2.373 -            Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
   2.374 -          end
   2.375 -    | setsum_tr' _ = raise Match;
   2.376 -in [(@{const_syntax setsum}, K setsum_tr')] end
   2.377 -*}
   2.378 -
   2.379 -text {* TODO These are candidates for generalization *}
   2.380 -
   2.381 -context comm_monoid_add
   2.382 -begin
   2.383 -
   2.384 -lemma setsum_reindex_id: 
   2.385 -  "inj_on f B ==> setsum f B = setsum id (f ` B)"
   2.386 -  by (simp add: setsum.reindex)
   2.387 -
   2.388 -lemma setsum_reindex_nonzero:
   2.389 -  assumes fS: "finite S"
   2.390 -  and nz: "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x = f y \<Longrightarrow> h (f x) = 0"
   2.391 -  shows "setsum h (f ` S) = setsum (h \<circ> f) S"
   2.392 -using nz proof (induct rule: finite_induct [OF fS])
   2.393 -  case 1 thus ?case by simp
   2.394 -next
   2.395 -  case (2 x F) 
   2.396 -  { assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto
   2.397 -    then obtain y where y: "y \<in> F" "f x = f y" by auto 
   2.398 -    from "2.hyps" y have xy: "x \<noteq> y" by auto
   2.399 -    from "2.prems" [of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp
   2.400 -    have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto
   2.401 -    also have "\<dots> = setsum (h o f) (insert x F)" 
   2.402 -      unfolding setsum.insert[OF `finite F` `x\<notin>F`]
   2.403 -      using h0
   2.404 -      apply (simp cong del: setsum.strong_cong)
   2.405 -      apply (rule "2.hyps"(3))
   2.406 -      apply (rule_tac y="y" in  "2.prems")
   2.407 -      apply simp_all
   2.408 -      done
   2.409 -    finally have ?case . }
   2.410 -  moreover
   2.411 -  { assume fxF: "f x \<notin> f ` F"
   2.412 -    have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)" 
   2.413 -      using fxF "2.hyps" by simp 
   2.414 -    also have "\<dots> = setsum (h o f) (insert x F)"
   2.415 -      unfolding setsum.insert[OF `finite F` `x\<notin>F`]
   2.416 -      apply (simp cong del: setsum.strong_cong)
   2.417 -      apply (rule cong [OF refl [of "op + (h (f x))"]])
   2.418 -      apply (rule "2.hyps"(3))
   2.419 -      apply (rule_tac y="y" in  "2.prems")
   2.420 -      apply simp_all
   2.421 -      done
   2.422 -    finally have ?case . }
   2.423 -  ultimately show ?case by blast
   2.424 -qed
   2.425 -
   2.426 -lemma setsum_cong2:
   2.427 -  "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> setsum f A = setsum g A"
   2.428 -  by (auto intro: setsum.cong)
   2.429 -
   2.430 -lemma setsum_reindex_cong:
   2.431 -   "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|] 
   2.432 -    ==> setsum h B = setsum g A"
   2.433 -  by (simp add: setsum.reindex)
   2.434 -
   2.435 -lemma setsum_restrict_set:
   2.436 -  assumes fA: "finite A"
   2.437 -  shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A"
   2.438 -proof-
   2.439 -  from fA have fab: "finite (A \<inter> B)" by auto
   2.440 -  have aba: "A \<inter> B \<subseteq> A" by blast
   2.441 -  let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0"
   2.442 -  from setsum.mono_neutral_left [OF fA aba, of ?g]
   2.443 -  show ?thesis by simp
   2.444 -qed
   2.445 -
   2.446 -lemma setsum_Union_disjoint:
   2.447 -  assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}"
   2.448 -  shows "setsum f (Union C) = setsum (setsum f) C"
   2.449 -  using assms by (fact setsum.Union_disjoint)
   2.450 -
   2.451 -lemma setsum_cartesian_product:
   2.452 -  "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)"
   2.453 -  by (fact setsum.cartesian_product)
   2.454 -
   2.455 -lemma setsum_UNION_zero:
   2.456 -  assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T"
   2.457 -  and f0: "\<And>T1 T2 x. T1\<in>S \<Longrightarrow> T2\<in>S \<Longrightarrow> T1 \<noteq> T2 \<Longrightarrow> x \<in> T1 \<Longrightarrow> x \<in> T2 \<Longrightarrow> f x = 0"
   2.458 -  shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S"
   2.459 -  using fSS f0
   2.460 -proof(induct rule: finite_induct[OF fS])
   2.461 -  case 1 thus ?case by simp
   2.462 -next
   2.463 -  case (2 T F)
   2.464 -  then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F" 
   2.465 -    and H: "setsum f (\<Union> F) = setsum (setsum f) F" by auto
   2.466 -  from fTF have fUF: "finite (\<Union>F)" by auto
   2.467 -  from "2.prems" TF fTF
   2.468 -  show ?case 
   2.469 -    by (auto simp add: H [symmetric] intro: setsum.union_inter_neutral [OF fTF(1) fUF, of f])
   2.470 -qed
   2.471 -
   2.472 -text {* Commuting outer and inner summation *}
   2.473 -
   2.474 -lemma setsum_commute:
   2.475 -  "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
   2.476 -proof (simp add: setsum_cartesian_product)
   2.477 -  have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
   2.478 -    (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
   2.479 -    (is "?s = _")
   2.480 -    apply (simp add: setsum.reindex [where h = "%(i, j). (j, i)"] swap_inj_on)
   2.481 -    apply (simp add: split_def)
   2.482 -    done
   2.483 -  also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
   2.484 -    (is "_ = ?t")
   2.485 -    apply (simp add: swap_product)
   2.486 -    done
   2.487 -  finally show "?s = ?t" .
   2.488 -qed
   2.489 -
   2.490 -lemma setsum_Plus:
   2.491 -  fixes A :: "'a set" and B :: "'b set"
   2.492 -  assumes fin: "finite A" "finite B"
   2.493 -  shows "setsum f (A <+> B) = setsum (f \<circ> Inl) A + setsum (f \<circ> Inr) B"
   2.494 -proof -
   2.495 -  have "A <+> B = Inl ` A \<union> Inr ` B" by auto
   2.496 -  moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)"
   2.497 -    by auto
   2.498 -  moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto
   2.499 -  moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI)
   2.500 -  ultimately show ?thesis using fin by(simp add: setsum.union_disjoint setsum.reindex)
   2.501 -qed
   2.502 -
   2.503 -end
   2.504 -
   2.505 -text {* TODO These are legacy *}
   2.506 -
   2.507 -lemma setsum_empty:
   2.508 -  "setsum f {} = 0"
   2.509 -  by (fact setsum.empty)
   2.510 -
   2.511 -lemma setsum_insert:
   2.512 -  "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   2.513 -  by (fact setsum.insert)
   2.514 -
   2.515 -lemma setsum_infinite:
   2.516 -  "~ finite A ==> setsum f A = 0"
   2.517 -  by (fact setsum.infinite)
   2.518 -
   2.519 -lemma setsum_reindex:
   2.520 -  "inj_on f B \<Longrightarrow> setsum h (f ` B) = setsum (h \<circ> f) B"
   2.521 -  by (fact setsum.reindex)
   2.522 -
   2.523 -lemma setsum_cong:
   2.524 -  "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
   2.525 -  by (fact setsum.cong)
   2.526 -
   2.527 -lemma strong_setsum_cong:
   2.528 -  "A = B ==> (!!x. x:B =simp=> f x = g x)
   2.529 -   ==> setsum (%x. f x) A = setsum (%x. g x) B"
   2.530 -  by (fact setsum.strong_cong)
   2.531 -
   2.532 -lemmas setsum_0 = setsum.neutral_const
   2.533 -lemmas setsum_0' = setsum.neutral
   2.534 -
   2.535 -lemma setsum_Un_Int: "finite A ==> finite B ==>
   2.536 -  setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
   2.537 -  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   2.538 -  by (fact setsum.union_inter)
   2.539 -
   2.540 -lemma setsum_Un_disjoint: "finite A ==> finite B
   2.541 -  ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
   2.542 -  by (fact setsum.union_disjoint)
   2.543 -
   2.544 -lemma setsum_subset_diff: "\<lbrakk> B \<subseteq> A; finite A \<rbrakk> \<Longrightarrow>
   2.545 -    setsum f A = setsum f (A - B) + setsum f B"
   2.546 -  by (fact setsum.subset_diff)
   2.547 -
   2.548 -lemma setsum_mono_zero_left: 
   2.549 -  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. f i = 0 \<rbrakk> \<Longrightarrow> setsum f S = setsum f T"
   2.550 -  by (fact setsum.mono_neutral_left)
   2.551 -
   2.552 -lemmas setsum_mono_zero_right = setsum.mono_neutral_right
   2.553 -
   2.554 -lemma setsum_mono_zero_cong_left: 
   2.555 -  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 0; \<And>x. x \<in> S \<Longrightarrow> f x = g x \<rbrakk>
   2.556 -  \<Longrightarrow> setsum f S = setsum g T"
   2.557 -  by (fact setsum.mono_neutral_cong_left)
   2.558 -
   2.559 -lemmas setsum_mono_zero_cong_right = setsum.mono_neutral_cong_right
   2.560 -
   2.561 -lemma setsum_delta: "finite S \<Longrightarrow>
   2.562 -  setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
   2.563 -  by (fact setsum.delta)
   2.564 -
   2.565 -lemma setsum_delta': "finite S \<Longrightarrow>
   2.566 -  setsum (\<lambda>k. if a = k then b k else 0) S = (if a\<in> S then b a else 0)"
   2.567 -  by (fact setsum.delta')
   2.568 -
   2.569 -lemma setsum_cases:
   2.570 -  assumes "finite A"
   2.571 -  shows "setsum (\<lambda>x. if P x then f x else g x) A =
   2.572 -         setsum f (A \<inter> {x. P x}) + setsum g (A \<inter> - {x. P x})"
   2.573 -  using assms by (fact setsum.If_cases)
   2.574 -
   2.575 -(*But we can't get rid of finite I. If infinite, although the rhs is 0, 
   2.576 -  the lhs need not be, since UNION I A could still be finite.*)
   2.577 -lemma setsum_UN_disjoint:
   2.578 -  assumes "finite I" and "ALL i:I. finite (A i)"
   2.579 -    and "ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}"
   2.580 -  shows "setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
   2.581 -  using assms by (fact setsum.UNION_disjoint)
   2.582 -
   2.583 -(*But we can't get rid of finite A. If infinite, although the lhs is 0, 
   2.584 -  the rhs need not be, since SIGMA A B could still be finite.*)
   2.585 -lemma setsum_Sigma:
   2.586 -  assumes "finite A" and  "ALL x:A. finite (B x)"
   2.587 -  shows "(\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
   2.588 -  using assms by (fact setsum.Sigma)
   2.589 -
   2.590 -lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
   2.591 -  by (fact setsum.distrib)
   2.592 -
   2.593 -lemma setsum_Un_zero:  
   2.594 -  "\<lbrakk> finite S; finite T; \<forall>x \<in> S\<inter>T. f x = 0 \<rbrakk> \<Longrightarrow>
   2.595 -  setsum f (S \<union> T) = setsum f S + setsum f T"
   2.596 -  by (fact setsum.union_inter_neutral)
   2.597 -
   2.598 -lemma setsum_eq_general_reverses:
   2.599 -  assumes fS: "finite S" and fT: "finite T"
   2.600 -  and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
   2.601 -  and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x"
   2.602 -  shows "setsum f S = setsum g T"
   2.603 -  using kh hk by (fact setsum.eq_general_reverses)
   2.604 -
   2.605 -
   2.606 -subsubsection {* Properties in more restricted classes of structures *}
   2.607 -
   2.608 -lemma setsum_Un: "finite A ==> finite B ==>
   2.609 -  (setsum f (A Un B) :: 'a :: ab_group_add) =
   2.610 -   setsum f A + setsum f B - setsum f (A Int B)"
   2.611 -by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
   2.612 -
   2.613 -lemma setsum_Un2:
   2.614 -  assumes "finite (A \<union> B)"
   2.615 -  shows "setsum f (A \<union> B) = setsum f (A - B) + setsum f (B - A) + setsum f (A \<inter> B)"
   2.616 -proof -
   2.617 -  have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
   2.618 -    by auto
   2.619 -  with assms show ?thesis by simp (subst setsum_Un_disjoint, auto)+
   2.620 -qed
   2.621 -
   2.622 -lemma setsum_diff1: "finite A \<Longrightarrow>
   2.623 -  (setsum f (A - {a}) :: ('a::ab_group_add)) =
   2.624 -  (if a:A then setsum f A - f a else setsum f A)"
   2.625 -by (erule finite_induct) (auto simp add: insert_Diff_if)
   2.626 -
   2.627 -lemma setsum_diff:
   2.628 -  assumes le: "finite A" "B \<subseteq> A"
   2.629 -  shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
   2.630 -proof -
   2.631 -  from le have finiteB: "finite B" using finite_subset by auto
   2.632 -  show ?thesis using finiteB le
   2.633 -  proof induct
   2.634 -    case empty
   2.635 -    thus ?case by auto
   2.636 -  next
   2.637 -    case (insert x F)
   2.638 -    thus ?case using le finiteB 
   2.639 -      by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
   2.640 -  qed
   2.641 -qed
   2.642 -
   2.643 -lemma setsum_mono:
   2.644 -  assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, ordered_ab_semigroup_add}))"
   2.645 -  shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
   2.646 -proof (cases "finite K")
   2.647 -  case True
   2.648 -  thus ?thesis using le
   2.649 -  proof induct
   2.650 -    case empty
   2.651 -    thus ?case by simp
   2.652 -  next
   2.653 -    case insert
   2.654 -    thus ?case using add_mono by fastforce
   2.655 -  qed
   2.656 -next
   2.657 -  case False then show ?thesis by simp
   2.658 -qed
   2.659 -
   2.660 -lemma setsum_strict_mono:
   2.661 -  fixes f :: "'a \<Rightarrow> 'b::{ordered_cancel_ab_semigroup_add,comm_monoid_add}"
   2.662 -  assumes "finite A"  "A \<noteq> {}"
   2.663 -    and "!!x. x:A \<Longrightarrow> f x < g x"
   2.664 -  shows "setsum f A < setsum g A"
   2.665 -  using assms
   2.666 -proof (induct rule: finite_ne_induct)
   2.667 -  case singleton thus ?case by simp
   2.668 -next
   2.669 -  case insert thus ?case by (auto simp: add_strict_mono)
   2.670 -qed
   2.671 -
   2.672 -lemma setsum_strict_mono_ex1:
   2.673 -fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_cancel_ab_semigroup_add}"
   2.674 -assumes "finite A" and "ALL x:A. f x \<le> g x" and "EX a:A. f a < g a"
   2.675 -shows "setsum f A < setsum g A"
   2.676 -proof-
   2.677 -  from assms(3) obtain a where a: "a:A" "f a < g a" by blast
   2.678 -  have "setsum f A = setsum f ((A-{a}) \<union> {a})"
   2.679 -    by(simp add:insert_absorb[OF `a:A`])
   2.680 -  also have "\<dots> = setsum f (A-{a}) + setsum f {a}"
   2.681 -    using `finite A` by(subst setsum_Un_disjoint) auto
   2.682 -  also have "setsum f (A-{a}) \<le> setsum g (A-{a})"
   2.683 -    by(rule setsum_mono)(simp add: assms(2))
   2.684 -  also have "setsum f {a} < setsum g {a}" using a by simp
   2.685 -  also have "setsum g (A - {a}) + setsum g {a} = setsum g((A-{a}) \<union> {a})"
   2.686 -    using `finite A` by(subst setsum_Un_disjoint[symmetric]) auto
   2.687 -  also have "\<dots> = setsum g A" by(simp add:insert_absorb[OF `a:A`])
   2.688 -  finally show ?thesis by (metis add_right_mono add_strict_left_mono)
   2.689 -qed
   2.690 -
   2.691 -lemma setsum_negf:
   2.692 -  "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
   2.693 -proof (cases "finite A")
   2.694 -  case True thus ?thesis by (induct set: finite) auto
   2.695 -next
   2.696 -  case False thus ?thesis by simp
   2.697 -qed
   2.698 -
   2.699 -lemma setsum_subtractf:
   2.700 -  "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
   2.701 -    setsum f A - setsum g A"
   2.702 -  using setsum_addf [of f "- g" A] by (simp add: setsum_negf)
   2.703 -
   2.704 -lemma setsum_nonneg:
   2.705 -  assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
   2.706 -  shows "0 \<le> setsum f A"
   2.707 -proof (cases "finite A")
   2.708 -  case True thus ?thesis using nn
   2.709 -  proof induct
   2.710 -    case empty then show ?case by simp
   2.711 -  next
   2.712 -    case (insert x F)
   2.713 -    then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
   2.714 -    with insert show ?case by simp
   2.715 -  qed
   2.716 -next
   2.717 -  case False thus ?thesis by simp
   2.718 -qed
   2.719 -
   2.720 -lemma setsum_nonpos:
   2.721 -  assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{ordered_ab_semigroup_add,comm_monoid_add})"
   2.722 -  shows "setsum f A \<le> 0"
   2.723 -proof (cases "finite A")
   2.724 -  case True thus ?thesis using np
   2.725 -  proof induct
   2.726 -    case empty then show ?case by simp
   2.727 -  next
   2.728 -    case (insert x F)
   2.729 -    then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
   2.730 -    with insert show ?case by simp
   2.731 -  qed
   2.732 -next
   2.733 -  case False thus ?thesis by simp
   2.734 -qed
   2.735 -
   2.736 -lemma setsum_nonneg_leq_bound:
   2.737 -  fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
   2.738 -  assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s"
   2.739 -  shows "f i \<le> B"
   2.740 -proof -
   2.741 -  have "0 \<le> (\<Sum> i \<in> s - {i}. f i)" and "0 \<le> f i"
   2.742 -    using assms by (auto intro!: setsum_nonneg)
   2.743 -  moreover
   2.744 -  have "(\<Sum> i \<in> s - {i}. f i) + f i = B"
   2.745 -    using assms by (simp add: setsum_diff1)
   2.746 -  ultimately show ?thesis by auto
   2.747 -qed
   2.748 -
   2.749 -lemma setsum_nonneg_0:
   2.750 -  fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
   2.751 -  assumes "finite s" and pos: "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
   2.752 -  and "(\<Sum> i \<in> s. f i) = 0" and i: "i \<in> s"
   2.753 -  shows "f i = 0"
   2.754 -  using setsum_nonneg_leq_bound[OF assms] pos[OF i] by auto
   2.755 -
   2.756 -lemma setsum_mono2:
   2.757 -fixes f :: "'a \<Rightarrow> 'b :: ordered_comm_monoid_add"
   2.758 -assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
   2.759 -shows "setsum f A \<le> setsum f B"
   2.760 -proof -
   2.761 -  have "setsum f A \<le> setsum f A + setsum f (B-A)"
   2.762 -    by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
   2.763 -  also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
   2.764 -    by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
   2.765 -  also have "A \<union> (B-A) = B" using sub by blast
   2.766 -  finally show ?thesis .
   2.767 -qed
   2.768 -
   2.769 -lemma setsum_mono3: "finite B ==> A <= B ==> 
   2.770 -    ALL x: B - A. 
   2.771 -      0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==>
   2.772 -        setsum f A <= setsum f B"
   2.773 -  apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
   2.774 -  apply (erule ssubst)
   2.775 -  apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
   2.776 -  apply simp
   2.777 -  apply (rule add_left_mono)
   2.778 -  apply (erule setsum_nonneg)
   2.779 -  apply (subst setsum_Un_disjoint [THEN sym])
   2.780 -  apply (erule finite_subset, assumption)
   2.781 -  apply (rule finite_subset)
   2.782 -  prefer 2
   2.783 -  apply assumption
   2.784 -  apply (auto simp add: sup_absorb2)
   2.785 -done
   2.786 -
   2.787 -lemma setsum_right_distrib: 
   2.788 -  fixes f :: "'a => ('b::semiring_0)"
   2.789 -  shows "r * setsum f A = setsum (%n. r * f n) A"
   2.790 -proof (cases "finite A")
   2.791 -  case True
   2.792 -  thus ?thesis
   2.793 -  proof induct
   2.794 -    case empty thus ?case by simp
   2.795 -  next
   2.796 -    case (insert x A) thus ?case by (simp add: distrib_left)
   2.797 -  qed
   2.798 -next
   2.799 -  case False thus ?thesis by simp
   2.800 -qed
   2.801 -
   2.802 -lemma setsum_left_distrib:
   2.803 -  "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
   2.804 -proof (cases "finite A")
   2.805 -  case True
   2.806 -  then show ?thesis
   2.807 -  proof induct
   2.808 -    case empty thus ?case by simp
   2.809 -  next
   2.810 -    case (insert x A) thus ?case by (simp add: distrib_right)
   2.811 -  qed
   2.812 -next
   2.813 -  case False thus ?thesis by simp
   2.814 -qed
   2.815 -
   2.816 -lemma setsum_divide_distrib:
   2.817 -  "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
   2.818 -proof (cases "finite A")
   2.819 -  case True
   2.820 -  then show ?thesis
   2.821 -  proof induct
   2.822 -    case empty thus ?case by simp
   2.823 -  next
   2.824 -    case (insert x A) thus ?case by (simp add: add_divide_distrib)
   2.825 -  qed
   2.826 -next
   2.827 -  case False thus ?thesis by simp
   2.828 -qed
   2.829 -
   2.830 -lemma setsum_abs[iff]: 
   2.831 -  fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   2.832 -  shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
   2.833 -proof (cases "finite A")
   2.834 -  case True
   2.835 -  thus ?thesis
   2.836 -  proof induct
   2.837 -    case empty thus ?case by simp
   2.838 -  next
   2.839 -    case (insert x A)
   2.840 -    thus ?case by (auto intro: abs_triangle_ineq order_trans)
   2.841 -  qed
   2.842 -next
   2.843 -  case False thus ?thesis by simp
   2.844 -qed
   2.845 -
   2.846 -lemma setsum_abs_ge_zero[iff]: 
   2.847 -  fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   2.848 -  shows "0 \<le> setsum (%i. abs(f i)) A"
   2.849 -proof (cases "finite A")
   2.850 -  case True
   2.851 -  thus ?thesis
   2.852 -  proof induct
   2.853 -    case empty thus ?case by simp
   2.854 -  next
   2.855 -    case (insert x A) thus ?case by auto
   2.856 -  qed
   2.857 -next
   2.858 -  case False thus ?thesis by simp
   2.859 -qed
   2.860 -
   2.861 -lemma abs_setsum_abs[simp]: 
   2.862 -  fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   2.863 -  shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
   2.864 -proof (cases "finite A")
   2.865 -  case True
   2.866 -  thus ?thesis
   2.867 -  proof induct
   2.868 -    case empty thus ?case by simp
   2.869 -  next
   2.870 -    case (insert a A)
   2.871 -    hence "\<bar>\<Sum>a\<in>insert a A. \<bar>f a\<bar>\<bar> = \<bar>\<bar>f a\<bar> + (\<Sum>a\<in>A. \<bar>f a\<bar>)\<bar>" by simp
   2.872 -    also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
   2.873 -    also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
   2.874 -      by (simp del: abs_of_nonneg)
   2.875 -    also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
   2.876 -    finally show ?case .
   2.877 -  qed
   2.878 -next
   2.879 -  case False thus ?thesis by simp
   2.880 -qed
   2.881 -
   2.882 -lemma setsum_diff1'[rule_format]:
   2.883 -  "finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x)"
   2.884 -apply (erule finite_induct[where F=A and P="% A. (a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x))"])
   2.885 -apply (auto simp add: insert_Diff_if add_ac)
   2.886 -done
   2.887 -
   2.888 -lemma setsum_diff1_ring: assumes "finite A" "a \<in> A"
   2.889 -  shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)"
   2.890 -unfolding setsum_diff1'[OF assms] by auto
   2.891 -
   2.892 -lemma setsum_product:
   2.893 -  fixes f :: "'a => ('b::semiring_0)"
   2.894 -  shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
   2.895 -  by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
   2.896 -
   2.897 -lemma setsum_mult_setsum_if_inj:
   2.898 -fixes f :: "'a => ('b::semiring_0)"
   2.899 -shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==>
   2.900 -  setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}"
   2.901 -by(auto simp: setsum_product setsum_cartesian_product
   2.902 -        intro!:  setsum_reindex_cong[symmetric])
   2.903 -
   2.904 -lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   2.905 -apply (case_tac "finite A")
   2.906 - prefer 2 apply simp
   2.907 -apply (erule rev_mp)
   2.908 -apply (erule finite_induct, auto)
   2.909 -done
   2.910 -
   2.911 -lemma setsum_eq_0_iff [simp]:
   2.912 -  "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   2.913 -  by (induct set: finite) auto
   2.914 -
   2.915 -lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
   2.916 -  setsum f A = Suc 0 \<longleftrightarrow> (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
   2.917 -apply(erule finite_induct)
   2.918 -apply (auto simp add:add_is_1)
   2.919 -done
   2.920 -
   2.921 -lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
   2.922 -
   2.923 -lemma setsum_Un_nat: "finite A ==> finite B ==>
   2.924 -  (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   2.925 -  -- {* For the natural numbers, we have subtraction. *}
   2.926 -by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
   2.927 -
   2.928 -lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
   2.929 -  (if a:A then setsum f A - f a else setsum f A)"
   2.930 -apply (case_tac "finite A")
   2.931 - prefer 2 apply simp
   2.932 -apply (erule finite_induct)
   2.933 - apply (auto simp add: insert_Diff_if)
   2.934 -apply (drule_tac a = a in mk_disjoint_insert, auto)
   2.935 -done
   2.936 -
   2.937 -lemma setsum_diff_nat: 
   2.938 -assumes "finite B" and "B \<subseteq> A"
   2.939 -shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
   2.940 -using assms
   2.941 -proof induct
   2.942 -  show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
   2.943 -next
   2.944 -  fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
   2.945 -    and xFinA: "insert x F \<subseteq> A"
   2.946 -    and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
   2.947 -  from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
   2.948 -  from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
   2.949 -    by (simp add: setsum_diff1_nat)
   2.950 -  from xFinA have "F \<subseteq> A" by simp
   2.951 -  with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
   2.952 -  with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
   2.953 -    by simp
   2.954 -  from xnotinF have "A - insert x F = (A - F) - {x}" by auto
   2.955 -  with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
   2.956 -    by simp
   2.957 -  from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
   2.958 -  with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
   2.959 -    by simp
   2.960 -  thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
   2.961 -qed
   2.962 -
   2.963 -lemma setsum_comp_morphism:
   2.964 -  assumes "h 0 = 0" and "\<And>x y. h (x + y) = h x + h y"
   2.965 -  shows "setsum (h \<circ> g) A = h (setsum g A)"
   2.966 -proof (cases "finite A")
   2.967 -  case False then show ?thesis by (simp add: assms)
   2.968 -next
   2.969 -  case True then show ?thesis by (induct A) (simp_all add: assms)
   2.970 -qed
   2.971 -
   2.972 -
   2.973 -subsubsection {* Cardinality as special case of @{const setsum} *}
   2.974 -
   2.975 -lemma card_eq_setsum:
   2.976 -  "card A = setsum (\<lambda>x. 1) A"
   2.977 -proof -
   2.978 -  have "plus \<circ> (\<lambda>_. Suc 0) = (\<lambda>_. Suc)"
   2.979 -    by (simp add: fun_eq_iff)
   2.980 -  then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) = Finite_Set.fold (\<lambda>_. Suc)"
   2.981 -    by (rule arg_cong)
   2.982 -  then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) 0 A = Finite_Set.fold (\<lambda>_. Suc) 0 A"
   2.983 -    by (blast intro: fun_cong)
   2.984 -  then show ?thesis by (simp add: card.eq_fold setsum.eq_fold)
   2.985 -qed
   2.986 -
   2.987 -lemma setsum_constant [simp]:
   2.988 -  "(\<Sum>x \<in> A. y) = of_nat (card A) * y"
   2.989 -apply (cases "finite A")
   2.990 -apply (erule finite_induct)
   2.991 -apply (auto simp add: algebra_simps)
   2.992 -done
   2.993 -
   2.994 -lemma setsum_bounded:
   2.995 -  assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
   2.996 -  shows "setsum f A \<le> of_nat (card A) * K"
   2.997 -proof (cases "finite A")
   2.998 -  case True
   2.999 -  thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
  2.1000 -next
  2.1001 -  case False thus ?thesis by simp
  2.1002 -qed
  2.1003 -
  2.1004 -lemma card_UN_disjoint:
  2.1005 -  assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
  2.1006 -    and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
  2.1007 -  shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
  2.1008 -proof -
  2.1009 -  have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)" by simp
  2.1010 -  with assms show ?thesis by (simp add: card_eq_setsum setsum_UN_disjoint del: setsum_constant)
  2.1011 -qed
  2.1012 -
  2.1013 -lemma card_Union_disjoint:
  2.1014 -  "finite C ==> (ALL A:C. finite A) ==>
  2.1015 -   (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
  2.1016 -   ==> card (Union C) = setsum card C"
  2.1017 -apply (frule card_UN_disjoint [of C id])
  2.1018 -apply (simp_all add: SUP_def id_def)
  2.1019 -done
  2.1020 -
  2.1021 -
  2.1022 -subsubsection {* Cardinality of products *}
  2.1023 -
  2.1024 -lemma card_SigmaI [simp]:
  2.1025 -  "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
  2.1026 -  \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  2.1027 -by(simp add: card_eq_setsum setsum_Sigma del:setsum_constant)
  2.1028 -
  2.1029 -(*
  2.1030 -lemma SigmaI_insert: "y \<notin> A ==>
  2.1031 -  (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
  2.1032 -  by auto
  2.1033 -*)
  2.1034 -
  2.1035 -lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
  2.1036 -  by (cases "finite A \<and> finite B")
  2.1037 -    (auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2)
  2.1038 -
  2.1039 -lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
  2.1040 -by (simp add: card_cartesian_product)
  2.1041 -
  2.1042 -
  2.1043 -subsection {* Generalized product over a set *}
  2.1044 -
  2.1045 -context comm_monoid_mult
  2.1046 -begin
  2.1047 -
  2.1048 -definition setprod :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
  2.1049 -where
  2.1050 -  "setprod = comm_monoid_set.F times 1"
  2.1051 -
  2.1052 -sublocale setprod!: comm_monoid_set times 1
  2.1053 -where
  2.1054 -  "comm_monoid_set.F times 1 = setprod"
  2.1055 -proof -
  2.1056 -  show "comm_monoid_set times 1" ..
  2.1057 -  then interpret setprod!: comm_monoid_set times 1 .
  2.1058 -  from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
  2.1059 -qed
  2.1060 -
  2.1061 -abbreviation
  2.1062 -  Setprod ("\<Prod>_" [1000] 999) where
  2.1063 -  "\<Prod>A \<equiv> setprod (\<lambda>x. x) A"
  2.1064 -
  2.1065 -end
  2.1066 -
  2.1067 -syntax
  2.1068 -  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
  2.1069 -syntax (xsymbols)
  2.1070 -  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  2.1071 -syntax (HTML output)
  2.1072 -  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  2.1073 -
  2.1074 -translations -- {* Beware of argument permutation! *}
  2.1075 -  "PROD i:A. b" == "CONST setprod (%i. b) A" 
  2.1076 -  "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A" 
  2.1077 -
  2.1078 -text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
  2.1079 - @{text"\<Prod>x|P. e"}. *}
  2.1080 -
  2.1081 -syntax
  2.1082 -  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
  2.1083 -syntax (xsymbols)
  2.1084 -  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  2.1085 -syntax (HTML output)
  2.1086 -  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  2.1087 -
  2.1088 -translations
  2.1089 -  "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
  2.1090 -  "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
  2.1091 -
  2.1092 -text {* TODO These are candidates for generalization *}
  2.1093 -
  2.1094 -context comm_monoid_mult
  2.1095 -begin
  2.1096 -
  2.1097 -lemma setprod_reindex_id:
  2.1098 -  "inj_on f B ==> setprod f B = setprod id (f ` B)"
  2.1099 -  by (auto simp add: setprod.reindex)
  2.1100 -
  2.1101 -lemma setprod_reindex_cong:
  2.1102 -  "inj_on f A ==> B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
  2.1103 -  by (frule setprod.reindex, simp)
  2.1104 -
  2.1105 -lemma strong_setprod_reindex_cong:
  2.1106 -  assumes i: "inj_on f A"
  2.1107 -  and B: "B = f ` A" and eq: "\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x"
  2.1108 -  shows "setprod h B = setprod g A"
  2.1109 -proof-
  2.1110 -  have "setprod h B = setprod (h o f) A"
  2.1111 -    by (simp add: B setprod.reindex [OF i, of h])
  2.1112 -  then show ?thesis apply simp
  2.1113 -    apply (rule setprod.cong)
  2.1114 -    apply simp
  2.1115 -    by (simp add: eq)
  2.1116 -qed
  2.1117 -
  2.1118 -lemma setprod_Union_disjoint:
  2.1119 -  assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}" 
  2.1120 -  shows "setprod f (Union C) = setprod (setprod f) C"
  2.1121 -  using assms by (fact setprod.Union_disjoint)
  2.1122 -
  2.1123 -text{*Here we can eliminate the finiteness assumptions, by cases.*}
  2.1124 -lemma setprod_cartesian_product:
  2.1125 -  "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
  2.1126 -  by (fact setprod.cartesian_product)
  2.1127 -
  2.1128 -lemma setprod_Un2:
  2.1129 -  assumes "finite (A \<union> B)"
  2.1130 -  shows "setprod f (A \<union> B) = setprod f (A - B) * setprod f (B - A) * setprod f (A \<inter> B)"
  2.1131 -proof -
  2.1132 -  have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
  2.1133 -    by auto
  2.1134 -  with assms show ?thesis by simp (subst setprod.union_disjoint, auto)+
  2.1135 -qed
  2.1136 -
  2.1137 -end
  2.1138 -
  2.1139 -text {* TODO These are legacy *}
  2.1140 -
  2.1141 -lemma setprod_empty: "setprod f {} = 1"
  2.1142 -  by (fact setprod.empty)
  2.1143 -
  2.1144 -lemma setprod_insert: "[| finite A; a \<notin> A |] ==>
  2.1145 -    setprod f (insert a A) = f a * setprod f A"
  2.1146 -  by (fact setprod.insert)
  2.1147 -
  2.1148 -lemma setprod_infinite: "~ finite A ==> setprod f A = 1"
  2.1149 -  by (fact setprod.infinite)
  2.1150 -
  2.1151 -lemma setprod_reindex:
  2.1152 -  "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
  2.1153 -  by (fact setprod.reindex)
  2.1154 -
  2.1155 -lemma setprod_cong:
  2.1156 -  "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
  2.1157 -  by (fact setprod.cong)
  2.1158 -
  2.1159 -lemma strong_setprod_cong:
  2.1160 -  "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
  2.1161 -  by (fact setprod.strong_cong)
  2.1162 -
  2.1163 -lemma setprod_Un_one:
  2.1164 -  "\<lbrakk> finite S; finite T; \<forall>x \<in> S\<inter>T. f x = 1 \<rbrakk>
  2.1165 -  \<Longrightarrow> setprod f (S \<union> T) = setprod f S  * setprod f T"
  2.1166 -  by (fact setprod.union_inter_neutral)
  2.1167 -
  2.1168 -lemmas setprod_1 = setprod.neutral_const
  2.1169 -lemmas setprod_1' = setprod.neutral
  2.1170 -
  2.1171 -lemma setprod_Un_Int: "finite A ==> finite B
  2.1172 -    ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
  2.1173 -  by (fact setprod.union_inter)
  2.1174 -
  2.1175 -lemma setprod_Un_disjoint: "finite A ==> finite B
  2.1176 -  ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
  2.1177 -  by (fact setprod.union_disjoint)
  2.1178 -
  2.1179 -lemma setprod_subset_diff: "\<lbrakk> B \<subseteq> A; finite A \<rbrakk> \<Longrightarrow>
  2.1180 -    setprod f A = setprod f (A - B) * setprod f B"
  2.1181 -  by (fact setprod.subset_diff)
  2.1182 -
  2.1183 -lemma setprod_mono_one_left:
  2.1184 -  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. f i = 1 \<rbrakk> \<Longrightarrow> setprod f S = setprod f T"
  2.1185 -  by (fact setprod.mono_neutral_left)
  2.1186 -
  2.1187 -lemmas setprod_mono_one_right = setprod.mono_neutral_right
  2.1188 -
  2.1189 -lemma setprod_mono_one_cong_left: 
  2.1190 -  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1; \<And>x. x \<in> S \<Longrightarrow> f x = g x \<rbrakk>
  2.1191 -  \<Longrightarrow> setprod f S = setprod g T"
  2.1192 -  by (fact setprod.mono_neutral_cong_left)
  2.1193 -
  2.1194 -lemmas setprod_mono_one_cong_right = setprod.mono_neutral_cong_right
  2.1195 -
  2.1196 -lemma setprod_delta: "finite S \<Longrightarrow>
  2.1197 -  setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
  2.1198 -  by (fact setprod.delta)
  2.1199 -
  2.1200 -lemma setprod_delta': "finite S \<Longrightarrow>
  2.1201 -  setprod (\<lambda>k. if a = k then b k else 1) S = (if a\<in> S then b a else 1)"
  2.1202 -  by (fact setprod.delta')
  2.1203 -
  2.1204 -lemma setprod_UN_disjoint:
  2.1205 -    "finite I ==> (ALL i:I. finite (A i)) ==>
  2.1206 -        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  2.1207 -      setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
  2.1208 -  by (fact setprod.UNION_disjoint)
  2.1209 -
  2.1210 -lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  2.1211 -    (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
  2.1212 -    (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
  2.1213 -  by (fact setprod.Sigma)
  2.1214 -
  2.1215 -lemma setprod_timesf: "setprod (\<lambda>x. f x * g x) A = setprod f A * setprod g A"
  2.1216 -  by (fact setprod.distrib)
  2.1217 -
  2.1218 -
  2.1219 -subsubsection {* Properties in more restricted classes of structures *}
  2.1220 -
  2.1221 -lemma setprod_zero:
  2.1222 -     "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
  2.1223 -apply (induct set: finite, force, clarsimp)
  2.1224 -apply (erule disjE, auto)
  2.1225 -done
  2.1226 -
  2.1227 -lemma setprod_zero_iff[simp]: "finite A ==> 
  2.1228 -  (setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) =
  2.1229 -  (EX x: A. f x = 0)"
  2.1230 -by (erule finite_induct, auto simp:no_zero_divisors)
  2.1231 -
  2.1232 -lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
  2.1233 -  (setprod f (A Un B) :: 'a ::{field})
  2.1234 -   = setprod f A * setprod f B / setprod f (A Int B)"
  2.1235 -by (subst setprod_Un_Int [symmetric], auto)
  2.1236 -
  2.1237 -lemma setprod_nonneg [rule_format]:
  2.1238 -   "(ALL x: A. (0::'a::linordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
  2.1239 -by (cases "finite A", induct set: finite, simp_all add: mult_nonneg_nonneg)
  2.1240 -
  2.1241 -lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x)
  2.1242 -  --> 0 < setprod f A"
  2.1243 -by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos)
  2.1244 -
  2.1245 -lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
  2.1246 -  (setprod f (A - {a}) :: 'a :: {field}) =
  2.1247 -  (if a:A then setprod f A / f a else setprod f A)"
  2.1248 -  by (erule finite_induct) (auto simp add: insert_Diff_if)
  2.1249 -
  2.1250 -lemma setprod_inversef: 
  2.1251 -  fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
  2.1252 -  shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)"
  2.1253 -by (erule finite_induct) auto
  2.1254 -
  2.1255 -lemma setprod_dividef:
  2.1256 -  fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
  2.1257 -  shows "finite A
  2.1258 -    ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
  2.1259 -apply (subgoal_tac
  2.1260 -         "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
  2.1261 -apply (erule ssubst)
  2.1262 -apply (subst divide_inverse)
  2.1263 -apply (subst setprod_timesf)
  2.1264 -apply (subst setprod_inversef, assumption+, rule refl)
  2.1265 -apply (rule setprod_cong, rule refl)
  2.1266 -apply (subst divide_inverse, auto)
  2.1267 -done
  2.1268 -
  2.1269 -lemma setprod_dvd_setprod [rule_format]: 
  2.1270 -    "(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A"
  2.1271 -  apply (cases "finite A")
  2.1272 -  apply (induct set: finite)
  2.1273 -  apply (auto simp add: dvd_def)
  2.1274 -  apply (rule_tac x = "k * ka" in exI)
  2.1275 -  apply (simp add: algebra_simps)
  2.1276 -done
  2.1277 -
  2.1278 -lemma setprod_dvd_setprod_subset:
  2.1279 -  "finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B"
  2.1280 -  apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)")
  2.1281 -  apply (unfold dvd_def, blast)
  2.1282 -  apply (subst setprod_Un_disjoint [symmetric])
  2.1283 -  apply (auto elim: finite_subset intro: setprod_cong)
  2.1284 -done
  2.1285 -
  2.1286 -lemma setprod_dvd_setprod_subset2:
  2.1287 -  "finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow> 
  2.1288 -      setprod f A dvd setprod g B"
  2.1289 -  apply (rule dvd_trans)
  2.1290 -  apply (rule setprod_dvd_setprod, erule (1) bspec)
  2.1291 -  apply (erule (1) setprod_dvd_setprod_subset)
  2.1292 -done
  2.1293 -
  2.1294 -lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow> 
  2.1295 -    (f i ::'a::comm_semiring_1) dvd setprod f A"
  2.1296 -by (induct set: finite) (auto intro: dvd_mult)
  2.1297 -
  2.1298 -lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow> 
  2.1299 -    (d::'a::comm_semiring_1) dvd (SUM x : A. f x)"
  2.1300 -  apply (cases "finite A")
  2.1301 -  apply (induct set: finite)
  2.1302 -  apply auto
  2.1303 -done
  2.1304 -
  2.1305 -lemma setprod_mono:
  2.1306 -  fixes f :: "'a \<Rightarrow> 'b\<Colon>linordered_semidom"
  2.1307 -  assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i"
  2.1308 -  shows "setprod f A \<le> setprod g A"
  2.1309 -proof (cases "finite A")
  2.1310 -  case True
  2.1311 -  hence ?thesis "setprod f A \<ge> 0" using subset_refl[of A]
  2.1312 -  proof (induct A rule: finite_subset_induct)
  2.1313 -    case (insert a F)
  2.1314 -    thus "setprod f (insert a F) \<le> setprod g (insert a F)" "0 \<le> setprod f (insert a F)"
  2.1315 -      unfolding setprod_insert[OF insert(1,3)]
  2.1316 -      using assms[rule_format,OF insert(2)] insert
  2.1317 -      by (auto intro: mult_mono mult_nonneg_nonneg)
  2.1318 -  qed auto
  2.1319 -  thus ?thesis by simp
  2.1320 -qed auto
  2.1321 -
  2.1322 -lemma abs_setprod:
  2.1323 -  fixes f :: "'a \<Rightarrow> 'b\<Colon>{linordered_field,abs}"
  2.1324 -  shows "abs (setprod f A) = setprod (\<lambda>x. abs (f x)) A"
  2.1325 -proof (cases "finite A")
  2.1326 -  case True thus ?thesis
  2.1327 -    by induct (auto simp add: field_simps abs_mult)
  2.1328 -qed auto
  2.1329 -
  2.1330 -lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
  2.1331 -apply (erule finite_induct)
  2.1332 -apply auto
  2.1333 -done
  2.1334 -
  2.1335 -lemma setprod_gen_delta:
  2.1336 -  assumes fS: "finite S"
  2.1337 -  shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::comm_monoid_mult) * c^ (card S - 1) else c^ card S)"
  2.1338 -proof-
  2.1339 -  let ?f = "(\<lambda>k. if k=a then b k else c)"
  2.1340 -  {assume a: "a \<notin> S"
  2.1341 -    hence "\<forall> k\<in> S. ?f k = c" by simp
  2.1342 -    hence ?thesis  using a setprod_constant[OF fS, of c] by simp }
  2.1343 -  moreover 
  2.1344 -  {assume a: "a \<in> S"
  2.1345 -    let ?A = "S - {a}"
  2.1346 -    let ?B = "{a}"
  2.1347 -    have eq: "S = ?A \<union> ?B" using a by blast 
  2.1348 -    have dj: "?A \<inter> ?B = {}" by simp
  2.1349 -    from fS have fAB: "finite ?A" "finite ?B" by auto  
  2.1350 -    have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
  2.1351 -      apply (rule setprod_cong) by auto
  2.1352 -    have cA: "card ?A = card S - 1" using fS a by auto
  2.1353 -    have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
  2.1354 -    have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
  2.1355 -      using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
  2.1356 -      by simp
  2.1357 -    then have ?thesis using a cA
  2.1358 -      by (simp add: fA1 field_simps cong add: setprod_cong cong del: if_weak_cong)}
  2.1359 -  ultimately show ?thesis by blast
  2.1360 -qed
  2.1361 -
  2.1362 -lemma setprod_eq_1_iff [simp]:
  2.1363 -  "finite F ==> setprod f F = 1 \<longleftrightarrow> (ALL a:F. f a = (1::nat))"
  2.1364 -  by (induct set: finite) auto
  2.1365 -
  2.1366 -lemma setprod_pos_nat:
  2.1367 -  "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
  2.1368 -using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
  2.1369 -
  2.1370 -lemma setprod_pos_nat_iff[simp]:
  2.1371 -  "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
  2.1372 -using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
  2.1373 -
  2.1374 -
  2.1375 -subsection {* Generic lattice operations over a set *}
  2.1376 -
  2.1377 -no_notation times (infixl "*" 70)
  2.1378 -no_notation Groups.one ("1")
  2.1379 -
  2.1380 -
  2.1381 -subsubsection {* Without neutral element *}
  2.1382 -
  2.1383 -locale semilattice_set = semilattice
  2.1384 -begin
  2.1385 -
  2.1386 -interpretation comp_fun_idem f
  2.1387 -  by default (simp_all add: fun_eq_iff left_commute)
  2.1388 -
  2.1389 -definition F :: "'a set \<Rightarrow> 'a"
  2.1390 -where
  2.1391 -  eq_fold': "F A = the (Finite_Set.fold (\<lambda>x y. Some (case y of None \<Rightarrow> x | Some z \<Rightarrow> f x z)) None A)"
  2.1392 -
  2.1393 -lemma eq_fold:
  2.1394 -  assumes "finite A"
  2.1395 -  shows "F (insert x A) = Finite_Set.fold f x A"
  2.1396 -proof (rule sym)
  2.1397 -  let ?f = "\<lambda>x y. Some (case y of None \<Rightarrow> x | Some z \<Rightarrow> f x z)"
  2.1398 -  interpret comp_fun_idem "?f"
  2.1399 -    by default (simp_all add: fun_eq_iff commute left_commute split: option.split)
  2.1400 -  from assms show "Finite_Set.fold f x A = F (insert x A)"
  2.1401 -  proof induct
  2.1402 -    case empty then show ?case by (simp add: eq_fold')
  2.1403 -  next
  2.1404 -    case (insert y B) then show ?case by (simp add: insert_commute [of x] eq_fold')
  2.1405 -  qed
  2.1406 -qed
  2.1407 -
  2.1408 -lemma singleton [simp]:
  2.1409 -  "F {x} = x"
  2.1410 -  by (simp add: eq_fold)
  2.1411 -
  2.1412 -lemma insert_not_elem:
  2.1413 -  assumes "finite A" and "x \<notin> A" and "A \<noteq> {}"
  2.1414 -  shows "F (insert x A) = x * F A"
  2.1415 -proof -
  2.1416 -  from `A \<noteq> {}` obtain b where "b \<in> A" by blast
  2.1417 -  then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)
  2.1418 -  with `finite A` and `x \<notin> A`
  2.1419 -    have "finite (insert x B)" and "b \<notin> insert x B" by auto
  2.1420 -  then have "F (insert b (insert x B)) = x * F (insert b B)"
  2.1421 -    by (simp add: eq_fold)
  2.1422 -  then show ?thesis by (simp add: * insert_commute)
  2.1423 -qed
  2.1424 -
  2.1425 -lemma in_idem:
  2.1426 -  assumes "finite A" and "x \<in> A"
  2.1427 -  shows "x * F A = F A"
  2.1428 -proof -
  2.1429 -  from assms have "A \<noteq> {}" by auto
  2.1430 -  with `finite A` show ?thesis using `x \<in> A`
  2.1431 -    by (induct A rule: finite_ne_induct) (auto simp add: ac_simps insert_not_elem)
  2.1432 -qed
  2.1433 -
  2.1434 -lemma insert [simp]:
  2.1435 -  assumes "finite A" and "A \<noteq> {}"
  2.1436 -  shows "F (insert x A) = x * F A"
  2.1437 -  using assms by (cases "x \<in> A") (simp_all add: insert_absorb in_idem insert_not_elem)
  2.1438 -
  2.1439 -lemma union:
  2.1440 -  assumes "finite A" "A \<noteq> {}" and "finite B" "B \<noteq> {}"
  2.1441 -  shows "F (A \<union> B) = F A * F B"
  2.1442 -  using assms by (induct A rule: finite_ne_induct) (simp_all add: ac_simps)
  2.1443 -
  2.1444 -lemma remove:
  2.1445 -  assumes "finite A" and "x \<in> A"
  2.1446 -  shows "F A = (if A - {x} = {} then x else x * F (A - {x}))"
  2.1447 -proof -
  2.1448 -  from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
  2.1449 -  with assms show ?thesis by simp
  2.1450 -qed
  2.1451 -
  2.1452 -lemma insert_remove:
  2.1453 -  assumes "finite A"
  2.1454 -  shows "F (insert x A) = (if A - {x} = {} then x else x * F (A - {x}))"
  2.1455 -  using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
  2.1456 -
  2.1457 -lemma subset:
  2.1458 -  assumes "finite A" "B \<noteq> {}" and "B \<subseteq> A"
  2.1459 -  shows "F B * F A = F A"
  2.1460 -proof -
  2.1461 -  from assms have "A \<noteq> {}" and "finite B" by (auto dest: finite_subset)
  2.1462 -  with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
  2.1463 -qed
  2.1464 -
  2.1465 -lemma closed:
  2.1466 -  assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
  2.1467 -  shows "F A \<in> A"
  2.1468 -using `finite A` `A \<noteq> {}` proof (induct rule: finite_ne_induct)
  2.1469 -  case singleton then show ?case by simp
  2.1470 -next
  2.1471 -  case insert with elem show ?case by force
  2.1472 -qed
  2.1473 -
  2.1474 -lemma hom_commute:
  2.1475 -  assumes hom: "\<And>x y. h (x * y) = h x * h y"
  2.1476 -  and N: "finite N" "N \<noteq> {}"
  2.1477 -  shows "h (F N) = F (h ` N)"
  2.1478 -using N proof (induct rule: finite_ne_induct)
  2.1479 -  case singleton thus ?case by simp
  2.1480 -next
  2.1481 -  case (insert n N)
  2.1482 -  then have "h (F (insert n N)) = h (n * F N)" by simp
  2.1483 -  also have "\<dots> = h n * h (F N)" by (rule hom)
  2.1484 -  also have "h (F N) = F (h ` N)" by (rule insert)
  2.1485 -  also have "h n * \<dots> = F (insert (h n) (h ` N))"
  2.1486 -    using insert by simp
  2.1487 -  also have "insert (h n) (h ` N) = h ` insert n N" by simp
  2.1488 -  finally show ?case .
  2.1489 -qed
  2.1490 -
  2.1491 -end
  2.1492 -
  2.1493 -locale semilattice_order_set = semilattice_order + semilattice_set
  2.1494 -begin
  2.1495 -
  2.1496 -lemma bounded_iff:
  2.1497 -  assumes "finite A" and "A \<noteq> {}"
  2.1498 -  shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
  2.1499 -  using assms by (induct rule: finite_ne_induct) (simp_all add: bounded_iff)
  2.1500 -
  2.1501 -lemma boundedI:
  2.1502 -  assumes "finite A"
  2.1503 -  assumes "A \<noteq> {}"
  2.1504 -  assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
  2.1505 -  shows "x \<preceq> F A"
  2.1506 -  using assms by (simp add: bounded_iff)
  2.1507 -
  2.1508 -lemma boundedE:
  2.1509 -  assumes "finite A" and "A \<noteq> {}" and "x \<preceq> F A"
  2.1510 -  obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
  2.1511 -  using assms by (simp add: bounded_iff)
  2.1512 -
  2.1513 -lemma coboundedI:
  2.1514 -  assumes "finite A"
  2.1515 -    and "a \<in> A"
  2.1516 -  shows "F A \<preceq> a"
  2.1517 -proof -
  2.1518 -  from assms have "A \<noteq> {}" by auto
  2.1519 -  from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
  2.1520 -  proof (induct rule: finite_ne_induct)
  2.1521 -    case singleton thus ?case by (simp add: refl)
  2.1522 -  next
  2.1523 -    case (insert x B)
  2.1524 -    from insert have "a = x \<or> a \<in> B" by simp
  2.1525 -    then show ?case using insert by (auto intro: coboundedI2)
  2.1526 -  qed
  2.1527 -qed
  2.1528 -
  2.1529 -lemma antimono:
  2.1530 -  assumes "A \<subseteq> B" and "A \<noteq> {}" and "finite B"
  2.1531 -  shows "F B \<preceq> F A"
  2.1532 -proof (cases "A = B")
  2.1533 -  case True then show ?thesis by (simp add: refl)
  2.1534 -next
  2.1535 -  case False
  2.1536 -  have B: "B = A \<union> (B - A)" using `A \<subseteq> B` by blast
  2.1537 -  then have "F B = F (A \<union> (B - A))" by simp
  2.1538 -  also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
  2.1539 -  also have "\<dots> \<preceq> F A" by simp
  2.1540 -  finally show ?thesis .
  2.1541 -qed
  2.1542 -
  2.1543 -end
  2.1544 -
  2.1545 -
  2.1546 -subsubsection {* With neutral element *}
  2.1547 -
  2.1548 -locale semilattice_neutr_set = semilattice_neutr
  2.1549 -begin
  2.1550 -
  2.1551 -interpretation comp_fun_idem f
  2.1552 -  by default (simp_all add: fun_eq_iff left_commute)
  2.1553 -
  2.1554 -definition F :: "'a set \<Rightarrow> 'a"
  2.1555 -where
  2.1556 -  eq_fold: "F A = Finite_Set.fold f 1 A"
  2.1557 -
  2.1558 -lemma infinite [simp]:
  2.1559 -  "\<not> finite A \<Longrightarrow> F A = 1"
  2.1560 -  by (simp add: eq_fold)
  2.1561 -
  2.1562 -lemma empty [simp]:
  2.1563 -  "F {} = 1"
  2.1564 -  by (simp add: eq_fold)
  2.1565 -
  2.1566 -lemma insert [simp]:
  2.1567 -  assumes "finite A"
  2.1568 -  shows "F (insert x A) = x * F A"
  2.1569 -  using assms by (simp add: eq_fold)
  2.1570 -
  2.1571 -lemma in_idem:
  2.1572 -  assumes "finite A" and "x \<in> A"
  2.1573 -  shows "x * F A = F A"
  2.1574 -proof -
  2.1575 -  from assms have "A \<noteq> {}" by auto
  2.1576 -  with `finite A` show ?thesis using `x \<in> A`
  2.1577 -    by (induct A rule: finite_ne_induct) (auto simp add: ac_simps)
  2.1578 -qed
  2.1579 -
  2.1580 -lemma union:
  2.1581 -  assumes "finite A" and "finite B"
  2.1582 -  shows "F (A \<union> B) = F A * F B"
  2.1583 -  using assms by (induct A) (simp_all add: ac_simps)
  2.1584 -
  2.1585 -lemma remove:
  2.1586 -  assumes "finite A" and "x \<in> A"
  2.1587 -  shows "F A = x * F (A - {x})"
  2.1588 -proof -
  2.1589 -  from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
  2.1590 -  with assms show ?thesis by simp
  2.1591 -qed
  2.1592 -
  2.1593 -lemma insert_remove:
  2.1594 -  assumes "finite A"
  2.1595 -  shows "F (insert x A) = x * F (A - {x})"
  2.1596 -  using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
  2.1597 -
  2.1598 -lemma subset:
  2.1599 -  assumes "finite A" and "B \<subseteq> A"
  2.1600 -  shows "F B * F A = F A"
  2.1601 -proof -
  2.1602 -  from assms have "finite B" by (auto dest: finite_subset)
  2.1603 -  with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
  2.1604 -qed
  2.1605 -
  2.1606 -lemma closed:
  2.1607 -  assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
  2.1608 -  shows "F A \<in> A"
  2.1609 -using `finite A` `A \<noteq> {}` proof (induct rule: finite_ne_induct)
  2.1610 -  case singleton then show ?case by simp
  2.1611 -next
  2.1612 -  case insert with elem show ?case by force
  2.1613 -qed
  2.1614 -
  2.1615 -end
  2.1616 -
  2.1617 -locale semilattice_order_neutr_set = semilattice_neutr_order + semilattice_neutr_set
  2.1618 -begin
  2.1619 -
  2.1620 -lemma bounded_iff:
  2.1621 -  assumes "finite A"
  2.1622 -  shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
  2.1623 -  using assms by (induct A) (simp_all add: bounded_iff)
  2.1624 -
  2.1625 -lemma boundedI:
  2.1626 -  assumes "finite A"
  2.1627 -  assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
  2.1628 -  shows "x \<preceq> F A"
  2.1629 -  using assms by (simp add: bounded_iff)
  2.1630 -
  2.1631 -lemma boundedE:
  2.1632 -  assumes "finite A" and "x \<preceq> F A"
  2.1633 -  obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
  2.1634 -  using assms by (simp add: bounded_iff)
  2.1635 -
  2.1636 -lemma coboundedI:
  2.1637 -  assumes "finite A"
  2.1638 -    and "a \<in> A"
  2.1639 -  shows "F A \<preceq> a"
  2.1640 -proof -
  2.1641 -  from assms have "A \<noteq> {}" by auto
  2.1642 -  from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
  2.1643 -  proof (induct rule: finite_ne_induct)
  2.1644 -    case singleton thus ?case by (simp add: refl)
  2.1645 -  next
  2.1646 -    case (insert x B)
  2.1647 -    from insert have "a = x \<or> a \<in> B" by simp
  2.1648 -    then show ?case using insert by (auto intro: coboundedI2)
  2.1649 -  qed
  2.1650 -qed
  2.1651 -
  2.1652 -lemma antimono:
  2.1653 -  assumes "A \<subseteq> B" and "finite B"
  2.1654 -  shows "F B \<preceq> F A"
  2.1655 -proof (cases "A = B")
  2.1656 -  case True then show ?thesis by (simp add: refl)
  2.1657 -next
  2.1658 -  case False
  2.1659 -  have B: "B = A \<union> (B - A)" using `A \<subseteq> B` by blast
  2.1660 -  then have "F B = F (A \<union> (B - A))" by simp
  2.1661 -  also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
  2.1662 -  also have "\<dots> \<preceq> F A" by simp
  2.1663 -  finally show ?thesis .
  2.1664 -qed
  2.1665 -
  2.1666 -end
  2.1667 -
  2.1668 -notation times (infixl "*" 70)
  2.1669 -notation Groups.one ("1")
  2.1670 -
  2.1671 -
  2.1672 -subsection {* Lattice operations on finite sets *}
  2.1673 -
  2.1674 -text {*
  2.1675 -  For historic reasons, there is the sublocale dependency from @{class distrib_lattice}
  2.1676 -  to @{class linorder}.  This is badly designed: both should depend on a common abstract
  2.1677 -  distributive lattice rather than having this non-subclass dependecy between two
  2.1678 -  classes.  But for the moment we have to live with it.  This forces us to setup
  2.1679 -  this sublocale dependency simultaneously with the lattice operations on finite
  2.1680 -  sets, to avoid garbage.
  2.1681 -*}
  2.1682 -
  2.1683 -definition (in semilattice_inf) Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
  2.1684 -where
  2.1685 -  "Inf_fin = semilattice_set.F inf"
  2.1686 -
  2.1687 -definition (in semilattice_sup) Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
  2.1688 -where
  2.1689 -  "Sup_fin = semilattice_set.F sup"
  2.1690 -
  2.1691 -context linorder
  2.1692 -begin
  2.1693 -
  2.1694 -definition Min :: "'a set \<Rightarrow> 'a"
  2.1695 -where
  2.1696 -  "Min = semilattice_set.F min"
  2.1697 -
  2.1698 -definition Max :: "'a set \<Rightarrow> 'a"
  2.1699 -where
  2.1700 -  "Max = semilattice_set.F max"
  2.1701 -
  2.1702 -sublocale Min!: semilattice_order_set min less_eq less
  2.1703 -  + Max!: semilattice_order_set max greater_eq greater
  2.1704 -where
  2.1705 -  "semilattice_set.F min = Min"
  2.1706 -  and "semilattice_set.F max = Max"
  2.1707 -proof -
  2.1708 -  show "semilattice_order_set min less_eq less" by default (auto simp add: min_def)
  2.1709 -  then interpret Min!: semilattice_order_set min less_eq less .
  2.1710 -  show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def)
  2.1711 -  then interpret Max!: semilattice_order_set max greater_eq greater .
  2.1712 -  from Min_def show "semilattice_set.F min = Min" by rule
  2.1713 -  from Max_def show "semilattice_set.F max = Max" by rule
  2.1714 -qed
  2.1715 -
  2.1716 -
  2.1717 -text {* An aside: @{const min}/@{const max} on linear orders as special case of @{const inf}/@{const sup} *}
  2.1718 -
  2.1719 -sublocale min_max!: distrib_lattice min less_eq less max
  2.1720 -where
  2.1721 -  "semilattice_inf.Inf_fin min = Min"
  2.1722 -  and "semilattice_sup.Sup_fin max = Max"
  2.1723 -proof -
  2.1724 -  show "class.distrib_lattice min less_eq less max"
  2.1725 -  proof
  2.1726 -    fix x y z
  2.1727 -    show "max x (min y z) = min (max x y) (max x z)"
  2.1728 -      by (auto simp add: min_def max_def)
  2.1729 -  qed (auto simp add: min_def max_def not_le less_imp_le)
  2.1730 -  then interpret min_max!: distrib_lattice min less_eq less max .
  2.1731 -  show "semilattice_inf.Inf_fin min = Min"
  2.1732 -    by (simp only: min_max.Inf_fin_def Min_def)
  2.1733 -  show "semilattice_sup.Sup_fin max = Max"
  2.1734 -    by (simp only: min_max.Sup_fin_def Max_def)
  2.1735 -qed
  2.1736 -
  2.1737 -lemmas le_maxI1 = min_max.sup_ge1
  2.1738 -lemmas le_maxI2 = min_max.sup_ge2
  2.1739 - 
  2.1740 -lemmas min_ac = min_max.inf_assoc min_max.inf_commute
  2.1741 -  min.left_commute
  2.1742 -
  2.1743 -lemmas max_ac = min_max.sup_assoc min_max.sup_commute
  2.1744 -  max.left_commute
  2.1745 -
  2.1746 -end
  2.1747 -
  2.1748 -
  2.1749 -text {* Lattice operations proper *}
  2.1750 -
  2.1751 -sublocale semilattice_inf < Inf_fin!: semilattice_order_set inf less_eq less
  2.1752 -where
  2.1753 -  "semilattice_set.F inf = Inf_fin"
  2.1754 -proof -
  2.1755 -  show "semilattice_order_set inf less_eq less" ..
  2.1756 -  then interpret Inf_fin!: semilattice_order_set inf less_eq less .
  2.1757 -  from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule
  2.1758 -qed
  2.1759 -
  2.1760 -sublocale semilattice_sup < Sup_fin!: semilattice_order_set sup greater_eq greater
  2.1761 -where
  2.1762 -  "semilattice_set.F sup = Sup_fin"
  2.1763 -proof -
  2.1764 -  show "semilattice_order_set sup greater_eq greater" ..
  2.1765 -  then interpret Sup_fin!: semilattice_order_set sup greater_eq greater .
  2.1766 -  from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule
  2.1767 -qed
  2.1768 -
  2.1769 -
  2.1770 -text {* An aside again: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin} *}
  2.1771 -
  2.1772 -lemma Inf_fin_Min:
  2.1773 -  "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)"
  2.1774 -  by (simp add: Inf_fin_def Min_def inf_min)
  2.1775 -
  2.1776 -lemma Sup_fin_Max:
  2.1777 -  "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)"
  2.1778 -  by (simp add: Sup_fin_def Max_def sup_max)
  2.1779 -
  2.1780 -
  2.1781 -
  2.1782 -subsection {* Infimum and Supremum over non-empty sets *}
  2.1783 -
  2.1784 -text {*
  2.1785 -  After this non-regular bootstrap, things continue canonically.
  2.1786 -*}
  2.1787 -
  2.1788 -context lattice
  2.1789 -begin
  2.1790 -
  2.1791 -lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA"
  2.1792 -apply(subgoal_tac "EX a. a:A")
  2.1793 -prefer 2 apply blast
  2.1794 -apply(erule exE)
  2.1795 -apply(rule order_trans)
  2.1796 -apply(erule (1) Inf_fin.coboundedI)
  2.1797 -apply(erule (1) Sup_fin.coboundedI)
  2.1798 -done
  2.1799 -
  2.1800 -lemma sup_Inf_absorb [simp]:
  2.1801 -  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) = a"
  2.1802 -apply(subst sup_commute)
  2.1803 -apply(simp add: sup_absorb2 Inf_fin.coboundedI)
  2.1804 -done
  2.1805 -
  2.1806 -lemma inf_Sup_absorb [simp]:
  2.1807 -  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) = a"
  2.1808 -by (simp add: inf_absorb1 Sup_fin.coboundedI)
  2.1809 -
  2.1810 -end
  2.1811 -
  2.1812 -context distrib_lattice
  2.1813 -begin
  2.1814 -
  2.1815 -lemma sup_Inf1_distrib:
  2.1816 -  assumes "finite A"
  2.1817 -    and "A \<noteq> {}"
  2.1818 -  shows "sup x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup x a|a. a \<in> A}"
  2.1819 -using assms by (simp add: image_def Inf_fin.hom_commute [where h="sup x", OF sup_inf_distrib1])
  2.1820 -  (rule arg_cong [where f="Inf_fin"], blast)
  2.1821 -
  2.1822 -lemma sup_Inf2_distrib:
  2.1823 -  assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  2.1824 -  shows "sup (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB) = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup a b|a b. a \<in> A \<and> b \<in> B}"
  2.1825 -using A proof (induct rule: finite_ne_induct)
  2.1826 -  case singleton then show ?case
  2.1827 -    by (simp add: sup_Inf1_distrib [OF B])
  2.1828 -next
  2.1829 -  case (insert x A)
  2.1830 -  have finB: "finite {sup x b |b. b \<in> B}"
  2.1831 -    by (rule finite_surj [where f = "sup x", OF B(1)], auto)
  2.1832 -  have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
  2.1833 -  proof -
  2.1834 -    have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
  2.1835 -      by blast
  2.1836 -    thus ?thesis by(simp add: insert(1) B(1))
  2.1837 -  qed
  2.1838 -  have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  2.1839 -  have "sup (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n(insert x A)) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB) = sup (inf x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA)) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB)"
  2.1840 -    using insert by simp
  2.1841 -  also have "\<dots> = inf (sup x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB)) (sup (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB))" by(rule sup_inf_distrib2)
  2.1842 -  also have "\<dots> = inf (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup x b|b. b \<in> B}) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup a b|a b. a \<in> A \<and> b \<in> B})"
  2.1843 -    using insert by(simp add:sup_Inf1_distrib[OF B])
  2.1844 -  also have "\<dots> = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n({sup x b |b. b \<in> B} \<union> {sup a b |a b. a \<in> A \<and> b \<in> B})"
  2.1845 -    (is "_ = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n?M")
  2.1846 -    using B insert
  2.1847 -    by (simp add: Inf_fin.union [OF finB _ finAB ne])
  2.1848 -  also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
  2.1849 -    by blast
  2.1850 -  finally show ?case .
  2.1851 -qed
  2.1852 -
  2.1853 -lemma inf_Sup1_distrib:
  2.1854 -  assumes "finite A" and "A \<noteq> {}"
  2.1855 -  shows "inf x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) = \<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf x a|a. a \<in> A}"
  2.1856 -using assms by (simp add: image_def Sup_fin.hom_commute [where h="inf x", OF inf_sup_distrib1])
  2.1857 -  (rule arg_cong [where f="Sup_fin"], blast)
  2.1858 -
  2.1859 -lemma inf_Sup2_distrib:
  2.1860 -  assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
  2.1861 -  shows "inf (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB) = \<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf a b|a b. a \<in> A \<and> b \<in> B}"
  2.1862 -using A proof (induct rule: finite_ne_induct)
  2.1863 -  case singleton thus ?case
  2.1864 -    by(simp add: inf_Sup1_distrib [OF B])
  2.1865 -next
  2.1866 -  case (insert x A)
  2.1867 -  have finB: "finite {inf x b |b. b \<in> B}"
  2.1868 -    by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
  2.1869 -  have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
  2.1870 -  proof -
  2.1871 -    have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
  2.1872 -      by blast
  2.1873 -    thus ?thesis by(simp add: insert(1) B(1))
  2.1874 -  qed
  2.1875 -  have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
  2.1876 -  have "inf (\<Squnion>\<^sub>f\<^sub>i\<^sub>n(insert x A)) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB) = inf (sup x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA)) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB)"
  2.1877 -    using insert by simp
  2.1878 -  also have "\<dots> = sup (inf x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB)) (inf (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB))" by(rule inf_sup_distrib2)
  2.1879 -  also have "\<dots> = sup (\<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf x b|b. b \<in> B}) (\<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf a b|a b. a \<in> A \<and> b \<in> B})"
  2.1880 -    using insert by(simp add:inf_Sup1_distrib[OF B])
  2.1881 -  also have "\<dots> = \<Squnion>\<^sub>f\<^sub>i\<^sub>n({inf x b |b. b \<in> B} \<union> {inf a b |a b. a \<in> A \<and> b \<in> B})"
  2.1882 -    (is "_ = \<Squnion>\<^sub>f\<^sub>i\<^sub>n?M")
  2.1883 -    using B insert
  2.1884 -    by (simp add: Sup_fin.union [OF finB _ finAB ne])
  2.1885 -  also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
  2.1886 -    by blast
  2.1887 -  finally show ?case .
  2.1888 -qed
  2.1889 -
  2.1890 -end
  2.1891 -
  2.1892 -context complete_lattice
  2.1893 -begin
  2.1894 -
  2.1895 -lemma Inf_fin_Inf:
  2.1896 -  assumes "finite A" and "A \<noteq> {}"
  2.1897 -  shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA = Inf A"
  2.1898 -proof -
  2.1899 -  from assms obtain b B where "A = insert b B" and "finite B" by auto
  2.1900 -  then show ?thesis
  2.1901 -    by (simp add: Inf_fin.eq_fold inf_Inf_fold_inf inf.commute [of b])
  2.1902 -qed
  2.1903 -
  2.1904 -lemma Sup_fin_Sup:
  2.1905 -  assumes "finite A" and "A \<noteq> {}"
  2.1906 -  shows "\<Squnion>\<^sub>f\<^sub>i\<^sub>nA = Sup A"
  2.1907 -proof -
  2.1908 -  from assms obtain b B where "A = insert b B" and "finite B" by auto
  2.1909 -  then show ?thesis
  2.1910 -    by (simp add: Sup_fin.eq_fold sup_Sup_fold_sup sup.commute [of b])
  2.1911 -qed
  2.1912 -
  2.1913 -end
  2.1914 -
  2.1915 -
  2.1916 -subsection {* Minimum and Maximum over non-empty sets *}
  2.1917 -
  2.1918 -context linorder
  2.1919 -begin
  2.1920 -
  2.1921 -lemma dual_min:
  2.1922 -  "ord.min greater_eq = max"
  2.1923 -  by (auto simp add: ord.min_def max_def fun_eq_iff)
  2.1924 -
  2.1925 -lemma dual_max:
  2.1926 -  "ord.max greater_eq = min"
  2.1927 -  by (auto simp add: ord.max_def min_def fun_eq_iff)
  2.1928 -
  2.1929 -lemma dual_Min:
  2.1930 -  "linorder.Min greater_eq = Max"
  2.1931 -proof -
  2.1932 -  interpret dual!: linorder greater_eq greater by (fact dual_linorder)
  2.1933 -  show ?thesis by (simp add: dual.Min_def dual_min Max_def)
  2.1934 -qed
  2.1935 -
  2.1936 -lemma dual_Max:
  2.1937 -  "linorder.Max greater_eq = Min"
  2.1938 -proof -
  2.1939 -  interpret dual!: linorder greater_eq greater by (fact dual_linorder)
  2.1940 -  show ?thesis by (simp add: dual.Max_def dual_max Min_def)
  2.1941 -qed
  2.1942 -
  2.1943 -lemmas Min_singleton = Min.singleton
  2.1944 -lemmas Max_singleton = Max.singleton
  2.1945 -lemmas Min_insert = Min.insert
  2.1946 -lemmas Max_insert = Max.insert
  2.1947 -lemmas Min_Un = Min.union
  2.1948 -lemmas Max_Un = Max.union
  2.1949 -lemmas hom_Min_commute = Min.hom_commute
  2.1950 -lemmas hom_Max_commute = Max.hom_commute
  2.1951 -
  2.1952 -lemma Min_in [simp]:
  2.1953 -  assumes "finite A" and "A \<noteq> {}"
  2.1954 -  shows "Min A \<in> A"
  2.1955 -  using assms by (auto simp add: min_def Min.closed)
  2.1956 -
  2.1957 -lemma Max_in [simp]:
  2.1958 -  assumes "finite A" and "A \<noteq> {}"
  2.1959 -  shows "Max A \<in> A"
  2.1960 -  using assms by (auto simp add: max_def Max.closed)
  2.1961 -
  2.1962 -lemma Min_le [simp]:
  2.1963 -  assumes "finite A" and "x \<in> A"
  2.1964 -  shows "Min A \<le> x"
  2.1965 -  using assms by (fact Min.coboundedI)
  2.1966 -
  2.1967 -lemma Max_ge [simp]:
  2.1968 -  assumes "finite A" and "x \<in> A"
  2.1969 -  shows "x \<le> Max A"
  2.1970 -  using assms by (fact Max.coboundedI)
  2.1971 -
  2.1972 -lemma Min_eqI:
  2.1973 -  assumes "finite A"
  2.1974 -  assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
  2.1975 -    and "x \<in> A"
  2.1976 -  shows "Min A = x"
  2.1977 -proof (rule antisym)
  2.1978 -  from `x \<in> A` have "A \<noteq> {}" by auto
  2.1979 -  with assms show "Min A \<ge> x" by simp
  2.1980 -next
  2.1981 -  from assms show "x \<ge> Min A" by simp
  2.1982 -qed
  2.1983 -
  2.1984 -lemma Max_eqI:
  2.1985 -  assumes "finite A"
  2.1986 -  assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
  2.1987 -    and "x \<in> A"
  2.1988 -  shows "Max A = x"
  2.1989 -proof (rule antisym)
  2.1990 -  from `x \<in> A` have "A \<noteq> {}" by auto
  2.1991 -  with assms show "Max A \<le> x" by simp
  2.1992 -next
  2.1993 -  from assms show "x \<le> Max A" by simp
  2.1994 -qed
  2.1995 -
  2.1996 -context
  2.1997 -  fixes A :: "'a set"
  2.1998 -  assumes fin_nonempty: "finite A" "A \<noteq> {}"
  2.1999 -begin
  2.2000 -
  2.2001 -lemma Min_ge_iff [simp]:
  2.2002 -  "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
  2.2003 -  using fin_nonempty by (fact Min.bounded_iff)
  2.2004 -
  2.2005 -lemma Max_le_iff [simp]:
  2.2006 -  "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
  2.2007 -  using fin_nonempty by (fact Max.bounded_iff)
  2.2008 -
  2.2009 -lemma Min_gr_iff [simp]:
  2.2010 -  "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
  2.2011 -  using fin_nonempty  by (induct rule: finite_ne_induct) simp_all
  2.2012 -
  2.2013 -lemma Max_less_iff [simp]:
  2.2014 -  "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
  2.2015 -  using fin_nonempty by (induct rule: finite_ne_induct) simp_all
  2.2016 -
  2.2017 -lemma Min_le_iff:
  2.2018 -  "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
  2.2019 -  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj)
  2.2020 -
  2.2021 -lemma Max_ge_iff:
  2.2022 -  "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
  2.2023 -  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj)
  2.2024 -
  2.2025 -lemma Min_less_iff:
  2.2026 -  "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
  2.2027 -  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj)
  2.2028 -
  2.2029 -lemma Max_gr_iff:
  2.2030 -  "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
  2.2031 -  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj)
  2.2032 -
  2.2033 -end
  2.2034 -
  2.2035 -lemma Min_antimono:
  2.2036 -  assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
  2.2037 -  shows "Min N \<le> Min M"
  2.2038 -  using assms by (fact Min.antimono)
  2.2039 -
  2.2040 -lemma Max_mono:
  2.2041 -  assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
  2.2042 -  shows "Max M \<le> Max N"
  2.2043 -  using assms by (fact Max.antimono)
  2.2044 -
  2.2045 -lemma mono_Min_commute:
  2.2046 -  assumes "mono f"
  2.2047 -  assumes "finite A" and "A \<noteq> {}"
  2.2048 -  shows "f (Min A) = Min (f ` A)"
  2.2049 -proof (rule linorder_class.Min_eqI [symmetric])
  2.2050 -  from `finite A` show "finite (f ` A)" by simp
  2.2051 -  from assms show "f (Min A) \<in> f ` A" by simp
  2.2052 -  fix x
  2.2053 -  assume "x \<in> f ` A"
  2.2054 -  then obtain y where "y \<in> A" and "x = f y" ..
  2.2055 -  with assms have "Min A \<le> y" by auto
  2.2056 -  with `mono f` have "f (Min A) \<le> f y" by (rule monoE)
  2.2057 -  with `x = f y` show "f (Min A) \<le> x" by simp
  2.2058 -qed
  2.2059 -
  2.2060 -lemma mono_Max_commute:
  2.2061 -  assumes "mono f"
  2.2062 -  assumes "finite A" and "A \<noteq> {}"
  2.2063 -  shows "f (Max A) = Max (f ` A)"
  2.2064 -proof (rule linorder_class.Max_eqI [symmetric])
  2.2065 -  from `finite A` show "finite (f ` A)" by simp
  2.2066 -  from assms show "f (Max A) \<in> f ` A" by simp
  2.2067 -  fix x
  2.2068 -  assume "x \<in> f ` A"
  2.2069 -  then obtain y where "y \<in> A" and "x = f y" ..
  2.2070 -  with assms have "y \<le> Max A" by auto
  2.2071 -  with `mono f` have "f y \<le> f (Max A)" by (rule monoE)
  2.2072 -  with `x = f y` show "x \<le> f (Max A)" by simp
  2.2073 -qed
  2.2074 -
  2.2075 -lemma finite_linorder_max_induct [consumes 1, case_names empty insert]:
  2.2076 -  assumes fin: "finite A"
  2.2077 -  and empty: "P {}" 
  2.2078 -  and insert: "\<And>b A. finite A \<Longrightarrow> \<forall>a\<in>A. a < b \<Longrightarrow> P A \<Longrightarrow> P (insert b A)"
  2.2079 -  shows "P A"
  2.2080 -using fin empty insert
  2.2081 -proof (induct rule: finite_psubset_induct)
  2.2082 -  case (psubset A)
  2.2083 -  have IH: "\<And>B. \<lbrakk>B < A; P {}; (\<And>A b. \<lbrakk>finite A; \<forall>a\<in>A. a<b; P A\<rbrakk> \<Longrightarrow> P (insert b A))\<rbrakk> \<Longrightarrow> P B" by fact 
  2.2084 -  have fin: "finite A" by fact 
  2.2085 -  have empty: "P {}" by fact
  2.2086 -  have step: "\<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)" by fact
  2.2087 -  show "P A"
  2.2088 -  proof (cases "A = {}")
  2.2089 -    assume "A = {}" 
  2.2090 -    then show "P A" using `P {}` by simp
  2.2091 -  next
  2.2092 -    let ?B = "A - {Max A}" 
  2.2093 -    let ?A = "insert (Max A) ?B"
  2.2094 -    have "finite ?B" using `finite A` by simp
  2.2095 -    assume "A \<noteq> {}"
  2.2096 -    with `finite A` have "Max A : A" by auto
  2.2097 -    then have A: "?A = A" using insert_Diff_single insert_absorb by auto
  2.2098 -    then have "P ?B" using `P {}` step IH [of ?B] by blast
  2.2099 -    moreover 
  2.2100 -    have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastforce
  2.2101 -    ultimately show "P A" using A insert_Diff_single step [OF `finite ?B`] by fastforce
  2.2102 -  qed
  2.2103 -qed
  2.2104 -
  2.2105 -lemma finite_linorder_min_induct [consumes 1, case_names empty insert]:
  2.2106 -  "\<lbrakk>finite A; P {}; \<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. b < a; P A\<rbrakk> \<Longrightarrow> P (insert b A)\<rbrakk> \<Longrightarrow> P A"
  2.2107 -  by (rule linorder.finite_linorder_max_induct [OF dual_linorder])
  2.2108 -
  2.2109 -lemma Least_Min:
  2.2110 -  assumes "finite {a. P a}" and "\<exists>a. P a"
  2.2111 -  shows "(LEAST a. P a) = Min {a. P a}"
  2.2112 -proof -
  2.2113 -  { fix A :: "'a set"
  2.2114 -    assume A: "finite A" "A \<noteq> {}"
  2.2115 -    have "(LEAST a. a \<in> A) = Min A"
  2.2116 -    using A proof (induct A rule: finite_ne_induct)
  2.2117 -      case singleton show ?case by (rule Least_equality) simp_all
  2.2118 -    next
  2.2119 -      case (insert a A)
  2.2120 -      have "(LEAST b. b = a \<or> b \<in> A) = min a (LEAST a. a \<in> A)"
  2.2121 -        by (auto intro!: Least_equality simp add: min_def not_le Min_le_iff insert.hyps dest!: less_imp_le)
  2.2122 -      with insert show ?case by simp
  2.2123 -    qed
  2.2124 -  } from this [of "{a. P a}"] assms show ?thesis by simp
  2.2125 -qed
  2.2126 -
  2.2127 -end
  2.2128 -
  2.2129 -context linordered_ab_semigroup_add
  2.2130 -begin
  2.2131 -
  2.2132 -lemma add_Min_commute:
  2.2133 -  fixes k
  2.2134 -  assumes "finite N" and "N \<noteq> {}"
  2.2135 -  shows "k + Min N = Min {k + m | m. m \<in> N}"
  2.2136 -proof -
  2.2137 -  have "\<And>x y. k + min x y = min (k + x) (k + y)"
  2.2138 -    by (simp add: min_def not_le)
  2.2139 -      (blast intro: antisym less_imp_le add_left_mono)
  2.2140 -  with assms show ?thesis
  2.2141 -    using hom_Min_commute [of "plus k" N]
  2.2142 -    by simp (blast intro: arg_cong [where f = Min])
  2.2143 -qed
  2.2144 -
  2.2145 -lemma add_Max_commute:
  2.2146 -  fixes k
  2.2147 -  assumes "finite N" and "N \<noteq> {}"
  2.2148 -  shows "k + Max N = Max {k + m | m. m \<in> N}"
  2.2149 -proof -
  2.2150 -  have "\<And>x y. k + max x y = max (k + x) (k + y)"
  2.2151 -    by (simp add: max_def not_le)
  2.2152 -      (blast intro: antisym less_imp_le add_left_mono)
  2.2153 -  with assms show ?thesis
  2.2154 -    using hom_Max_commute [of "plus k" N]
  2.2155 -    by simp (blast intro: arg_cong [where f = Max])
  2.2156 -qed
  2.2157 -
  2.2158 -end
  2.2159 -
  2.2160 -context linordered_ab_group_add
  2.2161 -begin
  2.2162 -
  2.2163 -lemma minus_Max_eq_Min [simp]:
  2.2164 -  "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Max S = Min (uminus ` S)"
  2.2165 -  by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min)
  2.2166 -
  2.2167 -lemma minus_Min_eq_Max [simp]:
  2.2168 -  "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Min S = Max (uminus ` S)"
  2.2169 -  by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max)
  2.2170 -
  2.2171 -end
  2.2172 -
  2.2173 -context complete_linorder
  2.2174 -begin
  2.2175 -
  2.2176 -lemma Min_Inf:
  2.2177 -  assumes "finite A" and "A \<noteq> {}"
  2.2178 -  shows "Min A = Inf A"
  2.2179 -proof -
  2.2180 -  from assms obtain b B where "A = insert b B" and "finite B" by auto
  2.2181 -  then show ?thesis
  2.2182 -    by (simp add: Min.eq_fold complete_linorder_inf_min [symmetric] inf_Inf_fold_inf inf.commute [of b])
  2.2183 -qed
  2.2184 -
  2.2185 -lemma Max_Sup:
  2.2186 -  assumes "finite A" and "A \<noteq> {}"
  2.2187 -  shows "Max A = Sup A"
  2.2188 -proof -
  2.2189 -  from assms obtain b B where "A = insert b B" and "finite B" by auto
  2.2190 -  then show ?thesis
  2.2191 -    by (simp add: Max.eq_fold complete_linorder_sup_max [symmetric] sup_Sup_fold_sup sup.commute [of b])
  2.2192 -qed
  2.2193 -
  2.2194 -end
  2.2195 -
  2.2196 -end
     3.1 --- a/src/HOL/Equiv_Relations.thy	Sat Dec 14 20:46:36 2013 +0100
     3.2 +++ b/src/HOL/Equiv_Relations.thy	Sun Dec 15 15:10:14 2013 +0100
     3.3 @@ -5,7 +5,7 @@
     3.4  header {* Equivalence Relations in Higher-Order Set Theory *}
     3.5  
     3.6  theory Equiv_Relations
     3.7 -imports Big_Operators Relation
     3.8 +imports Groups_Big Relation
     3.9  begin
    3.10  
    3.11  subsection {* Equivalence relations -- set version *}
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Groups_Big.thy	Sun Dec 15 15:10:14 2013 +0100
     4.3 @@ -0,0 +1,1379 @@
     4.4 +(*  Title:      HOL/Groups_Big.thy
     4.5 +    Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     4.6 +                with contributions by Jeremy Avigad
     4.7 +*)
     4.8 +
     4.9 +header {* Big sum and product over finite (non-empty) sets *}
    4.10 +
    4.11 +theory Groups_Big
    4.12 +imports Finite_Set
    4.13 +begin
    4.14 +
    4.15 +subsection {* Generic monoid operation over a set *}
    4.16 +
    4.17 +no_notation times (infixl "*" 70)
    4.18 +no_notation Groups.one ("1")
    4.19 +
    4.20 +locale comm_monoid_set = comm_monoid
    4.21 +begin
    4.22 +
    4.23 +interpretation comp_fun_commute f
    4.24 +  by default (simp add: fun_eq_iff left_commute)
    4.25 +
    4.26 +interpretation comp_fun_commute "f \<circ> g"
    4.27 +  by (rule comp_comp_fun_commute)
    4.28 +
    4.29 +definition F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
    4.30 +where
    4.31 +  eq_fold: "F g A = Finite_Set.fold (f \<circ> g) 1 A"
    4.32 +
    4.33 +lemma infinite [simp]:
    4.34 +  "\<not> finite A \<Longrightarrow> F g A = 1"
    4.35 +  by (simp add: eq_fold)
    4.36 +
    4.37 +lemma empty [simp]:
    4.38 +  "F g {} = 1"
    4.39 +  by (simp add: eq_fold)
    4.40 +
    4.41 +lemma insert [simp]:
    4.42 +  assumes "finite A" and "x \<notin> A"
    4.43 +  shows "F g (insert x A) = g x * F g A"
    4.44 +  using assms by (simp add: eq_fold)
    4.45 +
    4.46 +lemma remove:
    4.47 +  assumes "finite A" and "x \<in> A"
    4.48 +  shows "F g A = g x * F g (A - {x})"
    4.49 +proof -
    4.50 +  from `x \<in> A` obtain B where A: "A = insert x B" and "x \<notin> B"
    4.51 +    by (auto dest: mk_disjoint_insert)
    4.52 +  moreover from `finite A` A have "finite B" by simp
    4.53 +  ultimately show ?thesis by simp
    4.54 +qed
    4.55 +
    4.56 +lemma insert_remove:
    4.57 +  assumes "finite A"
    4.58 +  shows "F g (insert x A) = g x * F g (A - {x})"
    4.59 +  using assms by (cases "x \<in> A") (simp_all add: remove insert_absorb)
    4.60 +
    4.61 +lemma neutral:
    4.62 +  assumes "\<forall>x\<in>A. g x = 1"
    4.63 +  shows "F g A = 1"
    4.64 +  using assms by (induct A rule: infinite_finite_induct) simp_all
    4.65 +
    4.66 +lemma neutral_const [simp]:
    4.67 +  "F (\<lambda>_. 1) A = 1"
    4.68 +  by (simp add: neutral)
    4.69 +
    4.70 +lemma union_inter:
    4.71 +  assumes "finite A" and "finite B"
    4.72 +  shows "F g (A \<union> B) * F g (A \<inter> B) = F g A * F g B"
    4.73 +  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
    4.74 +using assms proof (induct A)
    4.75 +  case empty then show ?case by simp
    4.76 +next
    4.77 +  case (insert x A) then show ?case
    4.78 +    by (auto simp add: insert_absorb Int_insert_left commute [of _ "g x"] assoc left_commute)
    4.79 +qed
    4.80 +
    4.81 +corollary union_inter_neutral:
    4.82 +  assumes "finite A" and "finite B"
    4.83 +  and I0: "\<forall>x \<in> A \<inter> B. g x = 1"
    4.84 +  shows "F g (A \<union> B) = F g A * F g B"
    4.85 +  using assms by (simp add: union_inter [symmetric] neutral)
    4.86 +
    4.87 +corollary union_disjoint:
    4.88 +  assumes "finite A" and "finite B"
    4.89 +  assumes "A \<inter> B = {}"
    4.90 +  shows "F g (A \<union> B) = F g A * F g B"
    4.91 +  using assms by (simp add: union_inter_neutral)
    4.92 +
    4.93 +lemma subset_diff:
    4.94 +  assumes "B \<subseteq> A" and "finite A"
    4.95 +  shows "F g A = F g (A - B) * F g B"
    4.96 +proof -
    4.97 +  from assms have "finite (A - B)" by auto
    4.98 +  moreover from assms have "finite B" by (rule finite_subset)
    4.99 +  moreover from assms have "(A - B) \<inter> B = {}" by auto
   4.100 +  ultimately have "F g (A - B \<union> B) = F g (A - B) * F g B" by (rule union_disjoint)
   4.101 +  moreover from assms have "A \<union> B = A" by auto
   4.102 +  ultimately show ?thesis by simp
   4.103 +qed
   4.104 +
   4.105 +lemma reindex:
   4.106 +  assumes "inj_on h A"
   4.107 +  shows "F g (h ` A) = F (g \<circ> h) A"
   4.108 +proof (cases "finite A")
   4.109 +  case True
   4.110 +  with assms show ?thesis by (simp add: eq_fold fold_image comp_assoc)
   4.111 +next
   4.112 +  case False with assms have "\<not> finite (h ` A)" by (blast dest: finite_imageD)
   4.113 +  with False show ?thesis by simp
   4.114 +qed
   4.115 +
   4.116 +lemma cong:
   4.117 +  assumes "A = B"
   4.118 +  assumes g_h: "\<And>x. x \<in> B \<Longrightarrow> g x = h x"
   4.119 +  shows "F g A = F h B"
   4.120 +proof (cases "finite A")
   4.121 +  case True
   4.122 +  then have "\<And>C. C \<subseteq> A \<longrightarrow> (\<forall>x\<in>C. g x = h x) \<longrightarrow> F g C = F h C"
   4.123 +  proof induct
   4.124 +    case empty then show ?case by simp
   4.125 +  next
   4.126 +    case (insert x F) then show ?case apply -
   4.127 +    apply (simp add: subset_insert_iff, clarify)
   4.128 +    apply (subgoal_tac "finite C")
   4.129 +      prefer 2 apply (blast dest: finite_subset [rotated])
   4.130 +    apply (subgoal_tac "C = insert x (C - {x})")
   4.131 +      prefer 2 apply blast
   4.132 +    apply (erule ssubst)
   4.133 +    apply (simp add: Ball_def del: insert_Diff_single)
   4.134 +    done
   4.135 +  qed
   4.136 +  with `A = B` g_h show ?thesis by simp
   4.137 +next
   4.138 +  case False
   4.139 +  with `A = B` show ?thesis by simp
   4.140 +qed
   4.141 +
   4.142 +lemma strong_cong [cong]:
   4.143 +  assumes "A = B" "\<And>x. x \<in> B =simp=> g x = h x"
   4.144 +  shows "F (\<lambda>x. g x) A = F (\<lambda>x. h x) B"
   4.145 +  by (rule cong) (insert assms, simp_all add: simp_implies_def)
   4.146 +
   4.147 +lemma UNION_disjoint:
   4.148 +  assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
   4.149 +  and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
   4.150 +  shows "F g (UNION I A) = F (\<lambda>x. F g (A x)) I"
   4.151 +apply (insert assms)
   4.152 +apply (induct rule: finite_induct)
   4.153 +apply simp
   4.154 +apply atomize
   4.155 +apply (subgoal_tac "\<forall>i\<in>Fa. x \<noteq> i")
   4.156 + prefer 2 apply blast
   4.157 +apply (subgoal_tac "A x Int UNION Fa A = {}")
   4.158 + prefer 2 apply blast
   4.159 +apply (simp add: union_disjoint)
   4.160 +done
   4.161 +
   4.162 +lemma Union_disjoint:
   4.163 +  assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {}"
   4.164 +  shows "F g (Union C) = F (F g) C"
   4.165 +proof cases
   4.166 +  assume "finite C"
   4.167 +  from UNION_disjoint [OF this assms]
   4.168 +  show ?thesis
   4.169 +    by (simp add: SUP_def)
   4.170 +qed (auto dest: finite_UnionD intro: infinite)
   4.171 +
   4.172 +lemma distrib:
   4.173 +  "F (\<lambda>x. g x * h x) A = F g A * F h A"
   4.174 +  using assms by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute)
   4.175 +
   4.176 +lemma Sigma:
   4.177 +  "finite A \<Longrightarrow> \<forall>x\<in>A. finite (B x) \<Longrightarrow> F (\<lambda>x. F (g x) (B x)) A = F (split g) (SIGMA x:A. B x)"
   4.178 +apply (subst Sigma_def)
   4.179 +apply (subst UNION_disjoint, assumption, simp)
   4.180 + apply blast
   4.181 +apply (rule cong)
   4.182 +apply rule
   4.183 +apply (simp add: fun_eq_iff)
   4.184 +apply (subst UNION_disjoint, simp, simp)
   4.185 + apply blast
   4.186 +apply (simp add: comp_def)
   4.187 +done
   4.188 +
   4.189 +lemma related: 
   4.190 +  assumes Re: "R 1 1" 
   4.191 +  and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)" 
   4.192 +  and fS: "finite S" and Rfg: "\<forall>x\<in>S. R (h x) (g x)"
   4.193 +  shows "R (F h S) (F g S)"
   4.194 +  using fS by (rule finite_subset_induct) (insert assms, auto)
   4.195 +
   4.196 +lemma eq_general:
   4.197 +  assumes h: "\<forall>y\<in>S'. \<exists>!x. x \<in> S \<and> h x = y" 
   4.198 +  and f12:  "\<forall>x\<in>S. h x \<in> S' \<and> f2 (h x) = f1 x"
   4.199 +  shows "F f1 S = F f2 S'"
   4.200 +proof-
   4.201 +  from h f12 have hS: "h ` S = S'" by blast
   4.202 +  {fix x y assume H: "x \<in> S" "y \<in> S" "h x = h y"
   4.203 +    from f12 h H  have "x = y" by auto }
   4.204 +  hence hinj: "inj_on h S" unfolding inj_on_def Ex1_def by blast
   4.205 +  from f12 have th: "\<And>x. x \<in> S \<Longrightarrow> (f2 \<circ> h) x = f1 x" by auto 
   4.206 +  from hS have "F f2 S' = F f2 (h ` S)" by simp
   4.207 +  also have "\<dots> = F (f2 o h) S" using reindex [OF hinj, of f2] .
   4.208 +  also have "\<dots> = F f1 S " using th cong [of _ _ "f2 o h" f1]
   4.209 +    by blast
   4.210 +  finally show ?thesis ..
   4.211 +qed
   4.212 +
   4.213 +lemma eq_general_reverses:
   4.214 +  assumes kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
   4.215 +  and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = j x"
   4.216 +  shows "F j S = F g T"
   4.217 +  (* metis solves it, but not yet available here *)
   4.218 +  apply (rule eq_general [of T S h g j])
   4.219 +  apply (rule ballI)
   4.220 +  apply (frule kh)
   4.221 +  apply (rule ex1I[])
   4.222 +  apply blast
   4.223 +  apply clarsimp
   4.224 +  apply (drule hk) apply simp
   4.225 +  apply (rule sym)
   4.226 +  apply (erule conjunct1[OF conjunct2[OF hk]])
   4.227 +  apply (rule ballI)
   4.228 +  apply (drule hk)
   4.229 +  apply blast
   4.230 +  done
   4.231 +
   4.232 +lemma mono_neutral_cong_left:
   4.233 +  assumes "finite T" and "S \<subseteq> T" and "\<forall>i \<in> T - S. h i = 1"
   4.234 +  and "\<And>x. x \<in> S \<Longrightarrow> g x = h x" shows "F g S = F h T"
   4.235 +proof-
   4.236 +  have eq: "T = S \<union> (T - S)" using `S \<subseteq> T` by blast
   4.237 +  have d: "S \<inter> (T - S) = {}" using `S \<subseteq> T` by blast
   4.238 +  from `finite T` `S \<subseteq> T` have f: "finite S" "finite (T - S)"
   4.239 +    by (auto intro: finite_subset)
   4.240 +  show ?thesis using assms(4)
   4.241 +    by (simp add: union_disjoint [OF f d, unfolded eq [symmetric]] neutral [OF assms(3)])
   4.242 +qed
   4.243 +
   4.244 +lemma mono_neutral_cong_right:
   4.245 +  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1; \<And>x. x \<in> S \<Longrightarrow> g x = h x \<rbrakk>
   4.246 +   \<Longrightarrow> F g T = F h S"
   4.247 +  by (auto intro!: mono_neutral_cong_left [symmetric])
   4.248 +
   4.249 +lemma mono_neutral_left:
   4.250 +  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g S = F g T"
   4.251 +  by (blast intro: mono_neutral_cong_left)
   4.252 +
   4.253 +lemma mono_neutral_right:
   4.254 +  "\<lbrakk> finite T;  S \<subseteq> T;  \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g T = F g S"
   4.255 +  by (blast intro!: mono_neutral_left [symmetric])
   4.256 +
   4.257 +lemma delta: 
   4.258 +  assumes fS: "finite S"
   4.259 +  shows "F (\<lambda>k. if k = a then b k else 1) S = (if a \<in> S then b a else 1)"
   4.260 +proof-
   4.261 +  let ?f = "(\<lambda>k. if k=a then b k else 1)"
   4.262 +  { assume a: "a \<notin> S"
   4.263 +    hence "\<forall>k\<in>S. ?f k = 1" by simp
   4.264 +    hence ?thesis  using a by simp }
   4.265 +  moreover
   4.266 +  { assume a: "a \<in> S"
   4.267 +    let ?A = "S - {a}"
   4.268 +    let ?B = "{a}"
   4.269 +    have eq: "S = ?A \<union> ?B" using a by blast 
   4.270 +    have dj: "?A \<inter> ?B = {}" by simp
   4.271 +    from fS have fAB: "finite ?A" "finite ?B" by auto  
   4.272 +    have "F ?f S = F ?f ?A * F ?f ?B"
   4.273 +      using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]]
   4.274 +      by simp
   4.275 +    then have ?thesis using a by simp }
   4.276 +  ultimately show ?thesis by blast
   4.277 +qed
   4.278 +
   4.279 +lemma delta': 
   4.280 +  assumes fS: "finite S"
   4.281 +  shows "F (\<lambda>k. if a = k then b k else 1) S = (if a \<in> S then b a else 1)"
   4.282 +  using delta [OF fS, of a b, symmetric] by (auto intro: cong)
   4.283 +
   4.284 +lemma If_cases:
   4.285 +  fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
   4.286 +  assumes fA: "finite A"
   4.287 +  shows "F (\<lambda>x. if P x then h x else g x) A =
   4.288 +    F h (A \<inter> {x. P x}) * F g (A \<inter> - {x. P x})"
   4.289 +proof -
   4.290 +  have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}" 
   4.291 +          "(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}" 
   4.292 +    by blast+
   4.293 +  from fA 
   4.294 +  have f: "finite (A \<inter> {x. P x})" "finite (A \<inter> -{x. P x})" by auto
   4.295 +  let ?g = "\<lambda>x. if P x then h x else g x"
   4.296 +  from union_disjoint [OF f a(2), of ?g] a(1)
   4.297 +  show ?thesis
   4.298 +    by (subst (1 2) cong) simp_all
   4.299 +qed
   4.300 +
   4.301 +lemma cartesian_product:
   4.302 +   "F (\<lambda>x. F (g x) B) A = F (split g) (A <*> B)"
   4.303 +apply (rule sym)
   4.304 +apply (cases "finite A") 
   4.305 + apply (cases "finite B") 
   4.306 +  apply (simp add: Sigma)
   4.307 + apply (cases "A={}", simp)
   4.308 + apply simp
   4.309 +apply (auto intro: infinite dest: finite_cartesian_productD2)
   4.310 +apply (cases "B = {}") apply (auto intro: infinite dest: finite_cartesian_productD1)
   4.311 +done
   4.312 +
   4.313 +end
   4.314 +
   4.315 +notation times (infixl "*" 70)
   4.316 +notation Groups.one ("1")
   4.317 +
   4.318 +
   4.319 +subsection {* Generalized summation over a set *}
   4.320 +
   4.321 +context comm_monoid_add
   4.322 +begin
   4.323 +
   4.324 +definition setsum :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
   4.325 +where
   4.326 +  "setsum = comm_monoid_set.F plus 0"
   4.327 +
   4.328 +sublocale setsum!: comm_monoid_set plus 0
   4.329 +where
   4.330 +  "comm_monoid_set.F plus 0 = setsum"
   4.331 +proof -
   4.332 +  show "comm_monoid_set plus 0" ..
   4.333 +  then interpret setsum!: comm_monoid_set plus 0 .
   4.334 +  from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
   4.335 +qed
   4.336 +
   4.337 +abbreviation
   4.338 +  Setsum ("\<Sum>_" [1000] 999) where
   4.339 +  "\<Sum>A \<equiv> setsum (%x. x) A"
   4.340 +
   4.341 +end
   4.342 +
   4.343 +text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
   4.344 +written @{text"\<Sum>x\<in>A. e"}. *}
   4.345 +
   4.346 +syntax
   4.347 +  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
   4.348 +syntax (xsymbols)
   4.349 +  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   4.350 +syntax (HTML output)
   4.351 +  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   4.352 +
   4.353 +translations -- {* Beware of argument permutation! *}
   4.354 +  "SUM i:A. b" == "CONST setsum (%i. b) A"
   4.355 +  "\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
   4.356 +
   4.357 +text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
   4.358 + @{text"\<Sum>x|P. e"}. *}
   4.359 +
   4.360 +syntax
   4.361 +  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
   4.362 +syntax (xsymbols)
   4.363 +  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   4.364 +syntax (HTML output)
   4.365 +  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   4.366 +
   4.367 +translations
   4.368 +  "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
   4.369 +  "\<Sum>x|P. t" => "CONST setsum (%x. t) {x. P}"
   4.370 +
   4.371 +print_translation {*
   4.372 +let
   4.373 +  fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
   4.374 +        if x <> y then raise Match
   4.375 +        else
   4.376 +          let
   4.377 +            val x' = Syntax_Trans.mark_bound_body (x, Tx);
   4.378 +            val t' = subst_bound (x', t);
   4.379 +            val P' = subst_bound (x', P);
   4.380 +          in
   4.381 +            Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
   4.382 +          end
   4.383 +    | setsum_tr' _ = raise Match;
   4.384 +in [(@{const_syntax setsum}, K setsum_tr')] end
   4.385 +*}
   4.386 +
   4.387 +text {* TODO These are candidates for generalization *}
   4.388 +
   4.389 +context comm_monoid_add
   4.390 +begin
   4.391 +
   4.392 +lemma setsum_reindex_id: 
   4.393 +  "inj_on f B ==> setsum f B = setsum id (f ` B)"
   4.394 +  by (simp add: setsum.reindex)
   4.395 +
   4.396 +lemma setsum_reindex_nonzero:
   4.397 +  assumes fS: "finite S"
   4.398 +  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"
   4.399 +  shows "setsum h (f ` S) = setsum (h \<circ> f) S"
   4.400 +using nz proof (induct rule: finite_induct [OF fS])
   4.401 +  case 1 thus ?case by simp
   4.402 +next
   4.403 +  case (2 x F) 
   4.404 +  { assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto
   4.405 +    then obtain y where y: "y \<in> F" "f x = f y" by auto 
   4.406 +    from "2.hyps" y have xy: "x \<noteq> y" by auto
   4.407 +    from "2.prems" [of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp
   4.408 +    have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto
   4.409 +    also have "\<dots> = setsum (h o f) (insert x F)" 
   4.410 +      unfolding setsum.insert[OF `finite F` `x\<notin>F`]
   4.411 +      using h0
   4.412 +      apply (simp cong del: setsum.strong_cong)
   4.413 +      apply (rule "2.hyps"(3))
   4.414 +      apply (rule_tac y="y" in  "2.prems")
   4.415 +      apply simp_all
   4.416 +      done
   4.417 +    finally have ?case . }
   4.418 +  moreover
   4.419 +  { assume fxF: "f x \<notin> f ` F"
   4.420 +    have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)" 
   4.421 +      using fxF "2.hyps" by simp 
   4.422 +    also have "\<dots> = setsum (h o f) (insert x F)"
   4.423 +      unfolding setsum.insert[OF `finite F` `x\<notin>F`]
   4.424 +      apply (simp cong del: setsum.strong_cong)
   4.425 +      apply (rule cong [OF refl [of "op + (h (f x))"]])
   4.426 +      apply (rule "2.hyps"(3))
   4.427 +      apply (rule_tac y="y" in  "2.prems")
   4.428 +      apply simp_all
   4.429 +      done
   4.430 +    finally have ?case . }
   4.431 +  ultimately show ?case by blast
   4.432 +qed
   4.433 +
   4.434 +lemma setsum_cong2:
   4.435 +  "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> setsum f A = setsum g A"
   4.436 +  by (auto intro: setsum.cong)
   4.437 +
   4.438 +lemma setsum_reindex_cong:
   4.439 +   "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|] 
   4.440 +    ==> setsum h B = setsum g A"
   4.441 +  by (simp add: setsum.reindex)
   4.442 +
   4.443 +lemma setsum_restrict_set:
   4.444 +  assumes fA: "finite A"
   4.445 +  shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A"
   4.446 +proof-
   4.447 +  from fA have fab: "finite (A \<inter> B)" by auto
   4.448 +  have aba: "A \<inter> B \<subseteq> A" by blast
   4.449 +  let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0"
   4.450 +  from setsum.mono_neutral_left [OF fA aba, of ?g]
   4.451 +  show ?thesis by simp
   4.452 +qed
   4.453 +
   4.454 +lemma setsum_Union_disjoint:
   4.455 +  assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}"
   4.456 +  shows "setsum f (Union C) = setsum (setsum f) C"
   4.457 +  using assms by (fact setsum.Union_disjoint)
   4.458 +
   4.459 +lemma setsum_cartesian_product:
   4.460 +  "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)"
   4.461 +  by (fact setsum.cartesian_product)
   4.462 +
   4.463 +lemma setsum_UNION_zero:
   4.464 +  assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T"
   4.465 +  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"
   4.466 +  shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S"
   4.467 +  using fSS f0
   4.468 +proof(induct rule: finite_induct[OF fS])
   4.469 +  case 1 thus ?case by simp
   4.470 +next
   4.471 +  case (2 T F)
   4.472 +  then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F" 
   4.473 +    and H: "setsum f (\<Union> F) = setsum (setsum f) F" by auto
   4.474 +  from fTF have fUF: "finite (\<Union>F)" by auto
   4.475 +  from "2.prems" TF fTF
   4.476 +  show ?case 
   4.477 +    by (auto simp add: H [symmetric] intro: setsum.union_inter_neutral [OF fTF(1) fUF, of f])
   4.478 +qed
   4.479 +
   4.480 +text {* Commuting outer and inner summation *}
   4.481 +
   4.482 +lemma setsum_commute:
   4.483 +  "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
   4.484 +proof (simp add: setsum_cartesian_product)
   4.485 +  have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
   4.486 +    (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
   4.487 +    (is "?s = _")
   4.488 +    apply (simp add: setsum.reindex [where h = "%(i, j). (j, i)"] swap_inj_on)
   4.489 +    apply (simp add: split_def)
   4.490 +    done
   4.491 +  also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
   4.492 +    (is "_ = ?t")
   4.493 +    apply (simp add: swap_product)
   4.494 +    done
   4.495 +  finally show "?s = ?t" .
   4.496 +qed
   4.497 +
   4.498 +lemma setsum_Plus:
   4.499 +  fixes A :: "'a set" and B :: "'b set"
   4.500 +  assumes fin: "finite A" "finite B"
   4.501 +  shows "setsum f (A <+> B) = setsum (f \<circ> Inl) A + setsum (f \<circ> Inr) B"
   4.502 +proof -
   4.503 +  have "A <+> B = Inl ` A \<union> Inr ` B" by auto
   4.504 +  moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)"
   4.505 +    by auto
   4.506 +  moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto
   4.507 +  moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI)
   4.508 +  ultimately show ?thesis using fin by(simp add: setsum.union_disjoint setsum.reindex)
   4.509 +qed
   4.510 +
   4.511 +end
   4.512 +
   4.513 +text {* TODO These are legacy *}
   4.514 +
   4.515 +lemma setsum_empty:
   4.516 +  "setsum f {} = 0"
   4.517 +  by (fact setsum.empty)
   4.518 +
   4.519 +lemma setsum_insert:
   4.520 +  "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   4.521 +  by (fact setsum.insert)
   4.522 +
   4.523 +lemma setsum_infinite:
   4.524 +  "~ finite A ==> setsum f A = 0"
   4.525 +  by (fact setsum.infinite)
   4.526 +
   4.527 +lemma setsum_reindex:
   4.528 +  "inj_on f B \<Longrightarrow> setsum h (f ` B) = setsum (h \<circ> f) B"
   4.529 +  by (fact setsum.reindex)
   4.530 +
   4.531 +lemma setsum_cong:
   4.532 +  "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
   4.533 +  by (fact setsum.cong)
   4.534 +
   4.535 +lemma strong_setsum_cong:
   4.536 +  "A = B ==> (!!x. x:B =simp=> f x = g x)
   4.537 +   ==> setsum (%x. f x) A = setsum (%x. g x) B"
   4.538 +  by (fact setsum.strong_cong)
   4.539 +
   4.540 +lemmas setsum_0 = setsum.neutral_const
   4.541 +lemmas setsum_0' = setsum.neutral
   4.542 +
   4.543 +lemma setsum_Un_Int: "finite A ==> finite B ==>
   4.544 +  setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
   4.545 +  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   4.546 +  by (fact setsum.union_inter)
   4.547 +
   4.548 +lemma setsum_Un_disjoint: "finite A ==> finite B
   4.549 +  ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
   4.550 +  by (fact setsum.union_disjoint)
   4.551 +
   4.552 +lemma setsum_subset_diff: "\<lbrakk> B \<subseteq> A; finite A \<rbrakk> \<Longrightarrow>
   4.553 +    setsum f A = setsum f (A - B) + setsum f B"
   4.554 +  by (fact setsum.subset_diff)
   4.555 +
   4.556 +lemma setsum_mono_zero_left: 
   4.557 +  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. f i = 0 \<rbrakk> \<Longrightarrow> setsum f S = setsum f T"
   4.558 +  by (fact setsum.mono_neutral_left)
   4.559 +
   4.560 +lemmas setsum_mono_zero_right = setsum.mono_neutral_right
   4.561 +
   4.562 +lemma setsum_mono_zero_cong_left: 
   4.563 +  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 0; \<And>x. x \<in> S \<Longrightarrow> f x = g x \<rbrakk>
   4.564 +  \<Longrightarrow> setsum f S = setsum g T"
   4.565 +  by (fact setsum.mono_neutral_cong_left)
   4.566 +
   4.567 +lemmas setsum_mono_zero_cong_right = setsum.mono_neutral_cong_right
   4.568 +
   4.569 +lemma setsum_delta: "finite S \<Longrightarrow>
   4.570 +  setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
   4.571 +  by (fact setsum.delta)
   4.572 +
   4.573 +lemma setsum_delta': "finite S \<Longrightarrow>
   4.574 +  setsum (\<lambda>k. if a = k then b k else 0) S = (if a\<in> S then b a else 0)"
   4.575 +  by (fact setsum.delta')
   4.576 +
   4.577 +lemma setsum_cases:
   4.578 +  assumes "finite A"
   4.579 +  shows "setsum (\<lambda>x. if P x then f x else g x) A =
   4.580 +         setsum f (A \<inter> {x. P x}) + setsum g (A \<inter> - {x. P x})"
   4.581 +  using assms by (fact setsum.If_cases)
   4.582 +
   4.583 +(*But we can't get rid of finite I. If infinite, although the rhs is 0, 
   4.584 +  the lhs need not be, since UNION I A could still be finite.*)
   4.585 +lemma setsum_UN_disjoint:
   4.586 +  assumes "finite I" and "ALL i:I. finite (A i)"
   4.587 +    and "ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}"
   4.588 +  shows "setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
   4.589 +  using assms by (fact setsum.UNION_disjoint)
   4.590 +
   4.591 +(*But we can't get rid of finite A. If infinite, although the lhs is 0, 
   4.592 +  the rhs need not be, since SIGMA A B could still be finite.*)
   4.593 +lemma setsum_Sigma:
   4.594 +  assumes "finite A" and  "ALL x:A. finite (B x)"
   4.595 +  shows "(\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
   4.596 +  using assms by (fact setsum.Sigma)
   4.597 +
   4.598 +lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
   4.599 +  by (fact setsum.distrib)
   4.600 +
   4.601 +lemma setsum_Un_zero:  
   4.602 +  "\<lbrakk> finite S; finite T; \<forall>x \<in> S\<inter>T. f x = 0 \<rbrakk> \<Longrightarrow>
   4.603 +  setsum f (S \<union> T) = setsum f S + setsum f T"
   4.604 +  by (fact setsum.union_inter_neutral)
   4.605 +
   4.606 +lemma setsum_eq_general_reverses:
   4.607 +  assumes fS: "finite S" and fT: "finite T"
   4.608 +  and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
   4.609 +  and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x"
   4.610 +  shows "setsum f S = setsum g T"
   4.611 +  using kh hk by (fact setsum.eq_general_reverses)
   4.612 +
   4.613 +
   4.614 +subsubsection {* Properties in more restricted classes of structures *}
   4.615 +
   4.616 +lemma setsum_Un: "finite A ==> finite B ==>
   4.617 +  (setsum f (A Un B) :: 'a :: ab_group_add) =
   4.618 +   setsum f A + setsum f B - setsum f (A Int B)"
   4.619 +by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
   4.620 +
   4.621 +lemma setsum_Un2:
   4.622 +  assumes "finite (A \<union> B)"
   4.623 +  shows "setsum f (A \<union> B) = setsum f (A - B) + setsum f (B - A) + setsum f (A \<inter> B)"
   4.624 +proof -
   4.625 +  have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
   4.626 +    by auto
   4.627 +  with assms show ?thesis by simp (subst setsum_Un_disjoint, auto)+
   4.628 +qed
   4.629 +
   4.630 +lemma setsum_diff1: "finite A \<Longrightarrow>
   4.631 +  (setsum f (A - {a}) :: ('a::ab_group_add)) =
   4.632 +  (if a:A then setsum f A - f a else setsum f A)"
   4.633 +by (erule finite_induct) (auto simp add: insert_Diff_if)
   4.634 +
   4.635 +lemma setsum_diff:
   4.636 +  assumes le: "finite A" "B \<subseteq> A"
   4.637 +  shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
   4.638 +proof -
   4.639 +  from le have finiteB: "finite B" using finite_subset by auto
   4.640 +  show ?thesis using finiteB le
   4.641 +  proof induct
   4.642 +    case empty
   4.643 +    thus ?case by auto
   4.644 +  next
   4.645 +    case (insert x F)
   4.646 +    thus ?case using le finiteB 
   4.647 +      by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
   4.648 +  qed
   4.649 +qed
   4.650 +
   4.651 +lemma setsum_mono:
   4.652 +  assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, ordered_ab_semigroup_add}))"
   4.653 +  shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
   4.654 +proof (cases "finite K")
   4.655 +  case True
   4.656 +  thus ?thesis using le
   4.657 +  proof induct
   4.658 +    case empty
   4.659 +    thus ?case by simp
   4.660 +  next
   4.661 +    case insert
   4.662 +    thus ?case using add_mono by fastforce
   4.663 +  qed
   4.664 +next
   4.665 +  case False then show ?thesis by simp
   4.666 +qed
   4.667 +
   4.668 +lemma setsum_strict_mono:
   4.669 +  fixes f :: "'a \<Rightarrow> 'b::{ordered_cancel_ab_semigroup_add,comm_monoid_add}"
   4.670 +  assumes "finite A"  "A \<noteq> {}"
   4.671 +    and "!!x. x:A \<Longrightarrow> f x < g x"
   4.672 +  shows "setsum f A < setsum g A"
   4.673 +  using assms
   4.674 +proof (induct rule: finite_ne_induct)
   4.675 +  case singleton thus ?case by simp
   4.676 +next
   4.677 +  case insert thus ?case by (auto simp: add_strict_mono)
   4.678 +qed
   4.679 +
   4.680 +lemma setsum_strict_mono_ex1:
   4.681 +fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_cancel_ab_semigroup_add}"
   4.682 +assumes "finite A" and "ALL x:A. f x \<le> g x" and "EX a:A. f a < g a"
   4.683 +shows "setsum f A < setsum g A"
   4.684 +proof-
   4.685 +  from assms(3) obtain a where a: "a:A" "f a < g a" by blast
   4.686 +  have "setsum f A = setsum f ((A-{a}) \<union> {a})"
   4.687 +    by(simp add:insert_absorb[OF `a:A`])
   4.688 +  also have "\<dots> = setsum f (A-{a}) + setsum f {a}"
   4.689 +    using `finite A` by(subst setsum_Un_disjoint) auto
   4.690 +  also have "setsum f (A-{a}) \<le> setsum g (A-{a})"
   4.691 +    by(rule setsum_mono)(simp add: assms(2))
   4.692 +  also have "setsum f {a} < setsum g {a}" using a by simp
   4.693 +  also have "setsum g (A - {a}) + setsum g {a} = setsum g((A-{a}) \<union> {a})"
   4.694 +    using `finite A` by(subst setsum_Un_disjoint[symmetric]) auto
   4.695 +  also have "\<dots> = setsum g A" by(simp add:insert_absorb[OF `a:A`])
   4.696 +  finally show ?thesis by (auto simp add: add_right_mono add_strict_left_mono)
   4.697 +qed
   4.698 +
   4.699 +lemma setsum_negf:
   4.700 +  "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
   4.701 +proof (cases "finite A")
   4.702 +  case True thus ?thesis by (induct set: finite) auto
   4.703 +next
   4.704 +  case False thus ?thesis by simp
   4.705 +qed
   4.706 +
   4.707 +lemma setsum_subtractf:
   4.708 +  "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
   4.709 +    setsum f A - setsum g A"
   4.710 +  using setsum_addf [of f "- g" A] by (simp add: setsum_negf)
   4.711 +
   4.712 +lemma setsum_nonneg:
   4.713 +  assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
   4.714 +  shows "0 \<le> setsum f A"
   4.715 +proof (cases "finite A")
   4.716 +  case True thus ?thesis using nn
   4.717 +  proof induct
   4.718 +    case empty then show ?case by simp
   4.719 +  next
   4.720 +    case (insert x F)
   4.721 +    then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
   4.722 +    with insert show ?case by simp
   4.723 +  qed
   4.724 +next
   4.725 +  case False thus ?thesis by simp
   4.726 +qed
   4.727 +
   4.728 +lemma setsum_nonpos:
   4.729 +  assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{ordered_ab_semigroup_add,comm_monoid_add})"
   4.730 +  shows "setsum f A \<le> 0"
   4.731 +proof (cases "finite A")
   4.732 +  case True thus ?thesis using np
   4.733 +  proof induct
   4.734 +    case empty then show ?case by simp
   4.735 +  next
   4.736 +    case (insert x F)
   4.737 +    then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
   4.738 +    with insert show ?case by simp
   4.739 +  qed
   4.740 +next
   4.741 +  case False thus ?thesis by simp
   4.742 +qed
   4.743 +
   4.744 +lemma setsum_nonneg_leq_bound:
   4.745 +  fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
   4.746 +  assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s"
   4.747 +  shows "f i \<le> B"
   4.748 +proof -
   4.749 +  have "0 \<le> (\<Sum> i \<in> s - {i}. f i)" and "0 \<le> f i"
   4.750 +    using assms by (auto intro!: setsum_nonneg)
   4.751 +  moreover
   4.752 +  have "(\<Sum> i \<in> s - {i}. f i) + f i = B"
   4.753 +    using assms by (simp add: setsum_diff1)
   4.754 +  ultimately show ?thesis by auto
   4.755 +qed
   4.756 +
   4.757 +lemma setsum_nonneg_0:
   4.758 +  fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
   4.759 +  assumes "finite s" and pos: "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
   4.760 +  and "(\<Sum> i \<in> s. f i) = 0" and i: "i \<in> s"
   4.761 +  shows "f i = 0"
   4.762 +  using setsum_nonneg_leq_bound[OF assms] pos[OF i] by auto
   4.763 +
   4.764 +lemma setsum_mono2:
   4.765 +fixes f :: "'a \<Rightarrow> 'b :: ordered_comm_monoid_add"
   4.766 +assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
   4.767 +shows "setsum f A \<le> setsum f B"
   4.768 +proof -
   4.769 +  have "setsum f A \<le> setsum f A + setsum f (B-A)"
   4.770 +    by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
   4.771 +  also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
   4.772 +    by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
   4.773 +  also have "A \<union> (B-A) = B" using sub by blast
   4.774 +  finally show ?thesis .
   4.775 +qed
   4.776 +
   4.777 +lemma setsum_mono3: "finite B ==> A <= B ==> 
   4.778 +    ALL x: B - A. 
   4.779 +      0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==>
   4.780 +        setsum f A <= setsum f B"
   4.781 +  apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
   4.782 +  apply (erule ssubst)
   4.783 +  apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
   4.784 +  apply simp
   4.785 +  apply (rule add_left_mono)
   4.786 +  apply (erule setsum_nonneg)
   4.787 +  apply (subst setsum_Un_disjoint [THEN sym])
   4.788 +  apply (erule finite_subset, assumption)
   4.789 +  apply (rule finite_subset)
   4.790 +  prefer 2
   4.791 +  apply assumption
   4.792 +  apply (auto simp add: sup_absorb2)
   4.793 +done
   4.794 +
   4.795 +lemma setsum_right_distrib: 
   4.796 +  fixes f :: "'a => ('b::semiring_0)"
   4.797 +  shows "r * setsum f A = setsum (%n. r * f n) A"
   4.798 +proof (cases "finite A")
   4.799 +  case True
   4.800 +  thus ?thesis
   4.801 +  proof induct
   4.802 +    case empty thus ?case by simp
   4.803 +  next
   4.804 +    case (insert x A) thus ?case by (simp add: distrib_left)
   4.805 +  qed
   4.806 +next
   4.807 +  case False thus ?thesis by simp
   4.808 +qed
   4.809 +
   4.810 +lemma setsum_left_distrib:
   4.811 +  "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
   4.812 +proof (cases "finite A")
   4.813 +  case True
   4.814 +  then show ?thesis
   4.815 +  proof induct
   4.816 +    case empty thus ?case by simp
   4.817 +  next
   4.818 +    case (insert x A) thus ?case by (simp add: distrib_right)
   4.819 +  qed
   4.820 +next
   4.821 +  case False thus ?thesis by simp
   4.822 +qed
   4.823 +
   4.824 +lemma setsum_divide_distrib:
   4.825 +  "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
   4.826 +proof (cases "finite A")
   4.827 +  case True
   4.828 +  then show ?thesis
   4.829 +  proof induct
   4.830 +    case empty thus ?case by simp
   4.831 +  next
   4.832 +    case (insert x A) thus ?case by (simp add: add_divide_distrib)
   4.833 +  qed
   4.834 +next
   4.835 +  case False thus ?thesis by simp
   4.836 +qed
   4.837 +
   4.838 +lemma setsum_abs[iff]: 
   4.839 +  fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   4.840 +  shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
   4.841 +proof (cases "finite A")
   4.842 +  case True
   4.843 +  thus ?thesis
   4.844 +  proof induct
   4.845 +    case empty thus ?case by simp
   4.846 +  next
   4.847 +    case (insert x A)
   4.848 +    thus ?case by (auto intro: abs_triangle_ineq order_trans)
   4.849 +  qed
   4.850 +next
   4.851 +  case False thus ?thesis by simp
   4.852 +qed
   4.853 +
   4.854 +lemma setsum_abs_ge_zero[iff]: 
   4.855 +  fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   4.856 +  shows "0 \<le> setsum (%i. abs(f i)) A"
   4.857 +proof (cases "finite A")
   4.858 +  case True
   4.859 +  thus ?thesis
   4.860 +  proof induct
   4.861 +    case empty thus ?case by simp
   4.862 +  next
   4.863 +    case (insert x A) thus ?case by auto
   4.864 +  qed
   4.865 +next
   4.866 +  case False thus ?thesis by simp
   4.867 +qed
   4.868 +
   4.869 +lemma abs_setsum_abs[simp]: 
   4.870 +  fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   4.871 +  shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
   4.872 +proof (cases "finite A")
   4.873 +  case True
   4.874 +  thus ?thesis
   4.875 +  proof induct
   4.876 +    case empty thus ?case by simp
   4.877 +  next
   4.878 +    case (insert a A)
   4.879 +    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
   4.880 +    also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
   4.881 +    also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
   4.882 +      by (simp del: abs_of_nonneg)
   4.883 +    also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
   4.884 +    finally show ?case .
   4.885 +  qed
   4.886 +next
   4.887 +  case False thus ?thesis by simp
   4.888 +qed
   4.889 +
   4.890 +lemma setsum_diff1'[rule_format]:
   4.891 +  "finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x)"
   4.892 +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))"])
   4.893 +apply (auto simp add: insert_Diff_if add_ac)
   4.894 +done
   4.895 +
   4.896 +lemma setsum_diff1_ring: assumes "finite A" "a \<in> A"
   4.897 +  shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)"
   4.898 +unfolding setsum_diff1'[OF assms] by auto
   4.899 +
   4.900 +lemma setsum_product:
   4.901 +  fixes f :: "'a => ('b::semiring_0)"
   4.902 +  shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
   4.903 +  by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
   4.904 +
   4.905 +lemma setsum_mult_setsum_if_inj:
   4.906 +fixes f :: "'a => ('b::semiring_0)"
   4.907 +shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==>
   4.908 +  setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}"
   4.909 +by(auto simp: setsum_product setsum_cartesian_product
   4.910 +        intro!:  setsum_reindex_cong[symmetric])
   4.911 +
   4.912 +lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   4.913 +apply (case_tac "finite A")
   4.914 + prefer 2 apply simp
   4.915 +apply (erule rev_mp)
   4.916 +apply (erule finite_induct, auto)
   4.917 +done
   4.918 +
   4.919 +lemma setsum_eq_0_iff [simp]:
   4.920 +  "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   4.921 +  by (induct set: finite) auto
   4.922 +
   4.923 +lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
   4.924 +  setsum f A = Suc 0 \<longleftrightarrow> (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
   4.925 +apply(erule finite_induct)
   4.926 +apply (auto simp add:add_is_1)
   4.927 +done
   4.928 +
   4.929 +lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
   4.930 +
   4.931 +lemma setsum_Un_nat: "finite A ==> finite B ==>
   4.932 +  (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   4.933 +  -- {* For the natural numbers, we have subtraction. *}
   4.934 +by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
   4.935 +
   4.936 +lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
   4.937 +  (if a:A then setsum f A - f a else setsum f A)"
   4.938 +apply (case_tac "finite A")
   4.939 + prefer 2 apply simp
   4.940 +apply (erule finite_induct)
   4.941 + apply (auto simp add: insert_Diff_if)
   4.942 +apply (drule_tac a = a in mk_disjoint_insert, auto)
   4.943 +done
   4.944 +
   4.945 +lemma setsum_diff_nat: 
   4.946 +assumes "finite B" and "B \<subseteq> A"
   4.947 +shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
   4.948 +using assms
   4.949 +proof induct
   4.950 +  show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
   4.951 +next
   4.952 +  fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
   4.953 +    and xFinA: "insert x F \<subseteq> A"
   4.954 +    and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
   4.955 +  from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
   4.956 +  from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
   4.957 +    by (simp add: setsum_diff1_nat)
   4.958 +  from xFinA have "F \<subseteq> A" by simp
   4.959 +  with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
   4.960 +  with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
   4.961 +    by simp
   4.962 +  from xnotinF have "A - insert x F = (A - F) - {x}" by auto
   4.963 +  with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
   4.964 +    by simp
   4.965 +  from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
   4.966 +  with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
   4.967 +    by simp
   4.968 +  thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
   4.969 +qed
   4.970 +
   4.971 +lemma setsum_comp_morphism:
   4.972 +  assumes "h 0 = 0" and "\<And>x y. h (x + y) = h x + h y"
   4.973 +  shows "setsum (h \<circ> g) A = h (setsum g A)"
   4.974 +proof (cases "finite A")
   4.975 +  case False then show ?thesis by (simp add: assms)
   4.976 +next
   4.977 +  case True then show ?thesis by (induct A) (simp_all add: assms)
   4.978 +qed
   4.979 +
   4.980 +
   4.981 +subsubsection {* Cardinality as special case of @{const setsum} *}
   4.982 +
   4.983 +lemma card_eq_setsum:
   4.984 +  "card A = setsum (\<lambda>x. 1) A"
   4.985 +proof -
   4.986 +  have "plus \<circ> (\<lambda>_. Suc 0) = (\<lambda>_. Suc)"
   4.987 +    by (simp add: fun_eq_iff)
   4.988 +  then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) = Finite_Set.fold (\<lambda>_. Suc)"
   4.989 +    by (rule arg_cong)
   4.990 +  then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) 0 A = Finite_Set.fold (\<lambda>_. Suc) 0 A"
   4.991 +    by (blast intro: fun_cong)
   4.992 +  then show ?thesis by (simp add: card.eq_fold setsum.eq_fold)
   4.993 +qed
   4.994 +
   4.995 +lemma setsum_constant [simp]:
   4.996 +  "(\<Sum>x \<in> A. y) = of_nat (card A) * y"
   4.997 +apply (cases "finite A")
   4.998 +apply (erule finite_induct)
   4.999 +apply (auto simp add: algebra_simps)
  4.1000 +done
  4.1001 +
  4.1002 +lemma setsum_bounded:
  4.1003 +  assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
  4.1004 +  shows "setsum f A \<le> of_nat (card A) * K"
  4.1005 +proof (cases "finite A")
  4.1006 +  case True
  4.1007 +  thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
  4.1008 +next
  4.1009 +  case False thus ?thesis by simp
  4.1010 +qed
  4.1011 +
  4.1012 +lemma card_UN_disjoint:
  4.1013 +  assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
  4.1014 +    and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
  4.1015 +  shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
  4.1016 +proof -
  4.1017 +  have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)" by simp
  4.1018 +  with assms show ?thesis by (simp add: card_eq_setsum setsum_UN_disjoint del: setsum_constant)
  4.1019 +qed
  4.1020 +
  4.1021 +lemma card_Union_disjoint:
  4.1022 +  "finite C ==> (ALL A:C. finite A) ==>
  4.1023 +   (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
  4.1024 +   ==> card (Union C) = setsum card C"
  4.1025 +apply (frule card_UN_disjoint [of C id])
  4.1026 +apply (simp_all add: SUP_def id_def)
  4.1027 +done
  4.1028 +
  4.1029 +
  4.1030 +subsubsection {* Cardinality of products *}
  4.1031 +
  4.1032 +lemma card_SigmaI [simp]:
  4.1033 +  "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
  4.1034 +  \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  4.1035 +by(simp add: card_eq_setsum setsum_Sigma del:setsum_constant)
  4.1036 +
  4.1037 +(*
  4.1038 +lemma SigmaI_insert: "y \<notin> A ==>
  4.1039 +  (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
  4.1040 +  by auto
  4.1041 +*)
  4.1042 +
  4.1043 +lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
  4.1044 +  by (cases "finite A \<and> finite B")
  4.1045 +    (auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2)
  4.1046 +
  4.1047 +lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
  4.1048 +by (simp add: card_cartesian_product)
  4.1049 +
  4.1050 +
  4.1051 +subsection {* Generalized product over a set *}
  4.1052 +
  4.1053 +context comm_monoid_mult
  4.1054 +begin
  4.1055 +
  4.1056 +definition setprod :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
  4.1057 +where
  4.1058 +  "setprod = comm_monoid_set.F times 1"
  4.1059 +
  4.1060 +sublocale setprod!: comm_monoid_set times 1
  4.1061 +where
  4.1062 +  "comm_monoid_set.F times 1 = setprod"
  4.1063 +proof -
  4.1064 +  show "comm_monoid_set times 1" ..
  4.1065 +  then interpret setprod!: comm_monoid_set times 1 .
  4.1066 +  from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
  4.1067 +qed
  4.1068 +
  4.1069 +abbreviation
  4.1070 +  Setprod ("\<Prod>_" [1000] 999) where
  4.1071 +  "\<Prod>A \<equiv> setprod (\<lambda>x. x) A"
  4.1072 +
  4.1073 +end
  4.1074 +
  4.1075 +syntax
  4.1076 +  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
  4.1077 +syntax (xsymbols)
  4.1078 +  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  4.1079 +syntax (HTML output)
  4.1080 +  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  4.1081 +
  4.1082 +translations -- {* Beware of argument permutation! *}
  4.1083 +  "PROD i:A. b" == "CONST setprod (%i. b) A" 
  4.1084 +  "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A" 
  4.1085 +
  4.1086 +text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
  4.1087 + @{text"\<Prod>x|P. e"}. *}
  4.1088 +
  4.1089 +syntax
  4.1090 +  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
  4.1091 +syntax (xsymbols)
  4.1092 +  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  4.1093 +syntax (HTML output)
  4.1094 +  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  4.1095 +
  4.1096 +translations
  4.1097 +  "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
  4.1098 +  "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
  4.1099 +
  4.1100 +text {* TODO These are candidates for generalization *}
  4.1101 +
  4.1102 +context comm_monoid_mult
  4.1103 +begin
  4.1104 +
  4.1105 +lemma setprod_reindex_id:
  4.1106 +  "inj_on f B ==> setprod f B = setprod id (f ` B)"
  4.1107 +  by (auto simp add: setprod.reindex)
  4.1108 +
  4.1109 +lemma setprod_reindex_cong:
  4.1110 +  "inj_on f A ==> B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
  4.1111 +  by (frule setprod.reindex, simp)
  4.1112 +
  4.1113 +lemma strong_setprod_reindex_cong:
  4.1114 +  assumes i: "inj_on f A"
  4.1115 +  and B: "B = f ` A" and eq: "\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x"
  4.1116 +  shows "setprod h B = setprod g A"
  4.1117 +proof-
  4.1118 +  have "setprod h B = setprod (h o f) A"
  4.1119 +    by (simp add: B setprod.reindex [OF i, of h])
  4.1120 +  then show ?thesis apply simp
  4.1121 +    apply (rule setprod.cong)
  4.1122 +    apply simp
  4.1123 +    by (simp add: eq)
  4.1124 +qed
  4.1125 +
  4.1126 +lemma setprod_Union_disjoint:
  4.1127 +  assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}" 
  4.1128 +  shows "setprod f (Union C) = setprod (setprod f) C"
  4.1129 +  using assms by (fact setprod.Union_disjoint)
  4.1130 +
  4.1131 +text{*Here we can eliminate the finiteness assumptions, by cases.*}
  4.1132 +lemma setprod_cartesian_product:
  4.1133 +  "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
  4.1134 +  by (fact setprod.cartesian_product)
  4.1135 +
  4.1136 +lemma setprod_Un2:
  4.1137 +  assumes "finite (A \<union> B)"
  4.1138 +  shows "setprod f (A \<union> B) = setprod f (A - B) * setprod f (B - A) * setprod f (A \<inter> B)"
  4.1139 +proof -
  4.1140 +  have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
  4.1141 +    by auto
  4.1142 +  with assms show ?thesis by simp (subst setprod.union_disjoint, auto)+
  4.1143 +qed
  4.1144 +
  4.1145 +end
  4.1146 +
  4.1147 +text {* TODO These are legacy *}
  4.1148 +
  4.1149 +lemma setprod_empty: "setprod f {} = 1"
  4.1150 +  by (fact setprod.empty)
  4.1151 +
  4.1152 +lemma setprod_insert: "[| finite A; a \<notin> A |] ==>
  4.1153 +    setprod f (insert a A) = f a * setprod f A"
  4.1154 +  by (fact setprod.insert)
  4.1155 +
  4.1156 +lemma setprod_infinite: "~ finite A ==> setprod f A = 1"
  4.1157 +  by (fact setprod.infinite)
  4.1158 +
  4.1159 +lemma setprod_reindex:
  4.1160 +  "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
  4.1161 +  by (fact setprod.reindex)
  4.1162 +
  4.1163 +lemma setprod_cong:
  4.1164 +  "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
  4.1165 +  by (fact setprod.cong)
  4.1166 +
  4.1167 +lemma strong_setprod_cong:
  4.1168 +  "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
  4.1169 +  by (fact setprod.strong_cong)
  4.1170 +
  4.1171 +lemma setprod_Un_one:
  4.1172 +  "\<lbrakk> finite S; finite T; \<forall>x \<in> S\<inter>T. f x = 1 \<rbrakk>
  4.1173 +  \<Longrightarrow> setprod f (S \<union> T) = setprod f S  * setprod f T"
  4.1174 +  by (fact setprod.union_inter_neutral)
  4.1175 +
  4.1176 +lemmas setprod_1 = setprod.neutral_const
  4.1177 +lemmas setprod_1' = setprod.neutral
  4.1178 +
  4.1179 +lemma setprod_Un_Int: "finite A ==> finite B
  4.1180 +    ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
  4.1181 +  by (fact setprod.union_inter)
  4.1182 +
  4.1183 +lemma setprod_Un_disjoint: "finite A ==> finite B
  4.1184 +  ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
  4.1185 +  by (fact setprod.union_disjoint)
  4.1186 +
  4.1187 +lemma setprod_subset_diff: "\<lbrakk> B \<subseteq> A; finite A \<rbrakk> \<Longrightarrow>
  4.1188 +    setprod f A = setprod f (A - B) * setprod f B"
  4.1189 +  by (fact setprod.subset_diff)
  4.1190 +
  4.1191 +lemma setprod_mono_one_left:
  4.1192 +  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. f i = 1 \<rbrakk> \<Longrightarrow> setprod f S = setprod f T"
  4.1193 +  by (fact setprod.mono_neutral_left)
  4.1194 +
  4.1195 +lemmas setprod_mono_one_right = setprod.mono_neutral_right
  4.1196 +
  4.1197 +lemma setprod_mono_one_cong_left: 
  4.1198 +  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1; \<And>x. x \<in> S \<Longrightarrow> f x = g x \<rbrakk>
  4.1199 +  \<Longrightarrow> setprod f S = setprod g T"
  4.1200 +  by (fact setprod.mono_neutral_cong_left)
  4.1201 +
  4.1202 +lemmas setprod_mono_one_cong_right = setprod.mono_neutral_cong_right
  4.1203 +
  4.1204 +lemma setprod_delta: "finite S \<Longrightarrow>
  4.1205 +  setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
  4.1206 +  by (fact setprod.delta)
  4.1207 +
  4.1208 +lemma setprod_delta': "finite S \<Longrightarrow>
  4.1209 +  setprod (\<lambda>k. if a = k then b k else 1) S = (if a\<in> S then b a else 1)"
  4.1210 +  by (fact setprod.delta')
  4.1211 +
  4.1212 +lemma setprod_UN_disjoint:
  4.1213 +    "finite I ==> (ALL i:I. finite (A i)) ==>
  4.1214 +        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  4.1215 +      setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
  4.1216 +  by (fact setprod.UNION_disjoint)
  4.1217 +
  4.1218 +lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  4.1219 +    (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
  4.1220 +    (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
  4.1221 +  by (fact setprod.Sigma)
  4.1222 +
  4.1223 +lemma setprod_timesf: "setprod (\<lambda>x. f x * g x) A = setprod f A * setprod g A"
  4.1224 +  by (fact setprod.distrib)
  4.1225 +
  4.1226 +
  4.1227 +subsubsection {* Properties in more restricted classes of structures *}
  4.1228 +
  4.1229 +lemma setprod_zero:
  4.1230 +     "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
  4.1231 +apply (induct set: finite, force, clarsimp)
  4.1232 +apply (erule disjE, auto)
  4.1233 +done
  4.1234 +
  4.1235 +lemma setprod_zero_iff[simp]: "finite A ==> 
  4.1236 +  (setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) =
  4.1237 +  (EX x: A. f x = 0)"
  4.1238 +by (erule finite_induct, auto simp:no_zero_divisors)
  4.1239 +
  4.1240 +lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
  4.1241 +  (setprod f (A Un B) :: 'a ::{field})
  4.1242 +   = setprod f A * setprod f B / setprod f (A Int B)"
  4.1243 +by (subst setprod_Un_Int [symmetric], auto)
  4.1244 +
  4.1245 +lemma setprod_nonneg [rule_format]:
  4.1246 +   "(ALL x: A. (0::'a::linordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
  4.1247 +by (cases "finite A", induct set: finite, simp_all add: mult_nonneg_nonneg)
  4.1248 +
  4.1249 +lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x)
  4.1250 +  --> 0 < setprod f A"
  4.1251 +by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos)
  4.1252 +
  4.1253 +lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
  4.1254 +  (setprod f (A - {a}) :: 'a :: {field}) =
  4.1255 +  (if a:A then setprod f A / f a else setprod f A)"
  4.1256 +  by (erule finite_induct) (auto simp add: insert_Diff_if)
  4.1257 +
  4.1258 +lemma setprod_inversef: 
  4.1259 +  fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
  4.1260 +  shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)"
  4.1261 +by (erule finite_induct) auto
  4.1262 +
  4.1263 +lemma setprod_dividef:
  4.1264 +  fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
  4.1265 +  shows "finite A
  4.1266 +    ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
  4.1267 +apply (subgoal_tac
  4.1268 +         "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
  4.1269 +apply (erule ssubst)
  4.1270 +apply (subst divide_inverse)
  4.1271 +apply (subst setprod_timesf)
  4.1272 +apply (subst setprod_inversef, assumption+, rule refl)
  4.1273 +apply (rule setprod_cong, rule refl)
  4.1274 +apply (subst divide_inverse, auto)
  4.1275 +done
  4.1276 +
  4.1277 +lemma setprod_dvd_setprod [rule_format]: 
  4.1278 +    "(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A"
  4.1279 +  apply (cases "finite A")
  4.1280 +  apply (induct set: finite)
  4.1281 +  apply (auto simp add: dvd_def)
  4.1282 +  apply (rule_tac x = "k * ka" in exI)
  4.1283 +  apply (simp add: algebra_simps)
  4.1284 +done
  4.1285 +
  4.1286 +lemma setprod_dvd_setprod_subset:
  4.1287 +  "finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B"
  4.1288 +  apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)")
  4.1289 +  apply (unfold dvd_def, blast)
  4.1290 +  apply (subst setprod_Un_disjoint [symmetric])
  4.1291 +  apply (auto elim: finite_subset intro: setprod_cong)
  4.1292 +done
  4.1293 +
  4.1294 +lemma setprod_dvd_setprod_subset2:
  4.1295 +  "finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow> 
  4.1296 +      setprod f A dvd setprod g B"
  4.1297 +  apply (rule dvd_trans)
  4.1298 +  apply (rule setprod_dvd_setprod, erule (1) bspec)
  4.1299 +  apply (erule (1) setprod_dvd_setprod_subset)
  4.1300 +done
  4.1301 +
  4.1302 +lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow> 
  4.1303 +    (f i ::'a::comm_semiring_1) dvd setprod f A"
  4.1304 +by (induct set: finite) (auto intro: dvd_mult)
  4.1305 +
  4.1306 +lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow> 
  4.1307 +    (d::'a::comm_semiring_1) dvd (SUM x : A. f x)"
  4.1308 +  apply (cases "finite A")
  4.1309 +  apply (induct set: finite)
  4.1310 +  apply auto
  4.1311 +done
  4.1312 +
  4.1313 +lemma setprod_mono:
  4.1314 +  fixes f :: "'a \<Rightarrow> 'b\<Colon>linordered_semidom"
  4.1315 +  assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i"
  4.1316 +  shows "setprod f A \<le> setprod g A"
  4.1317 +proof (cases "finite A")
  4.1318 +  case True
  4.1319 +  hence ?thesis "setprod f A \<ge> 0" using subset_refl[of A]
  4.1320 +  proof (induct A rule: finite_subset_induct)
  4.1321 +    case (insert a F)
  4.1322 +    thus "setprod f (insert a F) \<le> setprod g (insert a F)" "0 \<le> setprod f (insert a F)"
  4.1323 +      unfolding setprod_insert[OF insert(1,3)]
  4.1324 +      using assms[rule_format,OF insert(2)] insert
  4.1325 +      by (auto intro: mult_mono mult_nonneg_nonneg)
  4.1326 +  qed auto
  4.1327 +  thus ?thesis by simp
  4.1328 +qed auto
  4.1329 +
  4.1330 +lemma abs_setprod:
  4.1331 +  fixes f :: "'a \<Rightarrow> 'b\<Colon>{linordered_field,abs}"
  4.1332 +  shows "abs (setprod f A) = setprod (\<lambda>x. abs (f x)) A"
  4.1333 +proof (cases "finite A")
  4.1334 +  case True thus ?thesis
  4.1335 +    by induct (auto simp add: field_simps abs_mult)
  4.1336 +qed auto
  4.1337 +
  4.1338 +lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
  4.1339 +apply (erule finite_induct)
  4.1340 +apply auto
  4.1341 +done
  4.1342 +
  4.1343 +lemma setprod_gen_delta:
  4.1344 +  assumes fS: "finite S"
  4.1345 +  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)"
  4.1346 +proof-
  4.1347 +  let ?f = "(\<lambda>k. if k=a then b k else c)"
  4.1348 +  {assume a: "a \<notin> S"
  4.1349 +    hence "\<forall> k\<in> S. ?f k = c" by simp
  4.1350 +    hence ?thesis  using a setprod_constant[OF fS, of c] by simp }
  4.1351 +  moreover 
  4.1352 +  {assume a: "a \<in> S"
  4.1353 +    let ?A = "S - {a}"
  4.1354 +    let ?B = "{a}"
  4.1355 +    have eq: "S = ?A \<union> ?B" using a by blast 
  4.1356 +    have dj: "?A \<inter> ?B = {}" by simp
  4.1357 +    from fS have fAB: "finite ?A" "finite ?B" by auto  
  4.1358 +    have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
  4.1359 +      apply (rule setprod_cong) by auto
  4.1360 +    have cA: "card ?A = card S - 1" using fS a by auto
  4.1361 +    have fA1: "setprod ?f ?A = c ^ card ?A"  unfolding fA0 apply (rule setprod_constant) using fS by auto
  4.1362 +    have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
  4.1363 +      using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
  4.1364 +      by simp
  4.1365 +    then have ?thesis using a cA
  4.1366 +      by (simp add: fA1 field_simps cong add: setprod_cong cong del: if_weak_cong)}
  4.1367 +  ultimately show ?thesis by blast
  4.1368 +qed
  4.1369 +
  4.1370 +lemma setprod_eq_1_iff [simp]:
  4.1371 +  "finite F ==> setprod f F = 1 \<longleftrightarrow> (ALL a:F. f a = (1::nat))"
  4.1372 +  by (induct set: finite) auto
  4.1373 +
  4.1374 +lemma setprod_pos_nat:
  4.1375 +  "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
  4.1376 +using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
  4.1377 +
  4.1378 +lemma setprod_pos_nat_iff[simp]:
  4.1379 +  "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
  4.1380 +using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
  4.1381 +
  4.1382 +end
     5.1 --- a/src/HOL/Hilbert_Choice.thy	Sat Dec 14 20:46:36 2013 +0100
     5.2 +++ b/src/HOL/Hilbert_Choice.thy	Sun Dec 15 15:10:14 2013 +0100
     5.3 @@ -6,7 +6,7 @@
     5.4  header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
     5.5  
     5.6  theory Hilbert_Choice
     5.7 -imports Nat Wellfounded Big_Operators
     5.8 +imports Nat Wellfounded Lattices_Big Metis
     5.9  keywords "specification" "ax_specification" :: thy_goal
    5.10  begin
    5.11  
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Lattices_Big.thy	Sun Dec 15 15:10:14 2013 +0100
     6.3 @@ -0,0 +1,833 @@
     6.4 +(*  Title:      HOL/Lattices_Big.thy
     6.5 +    Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     6.6 +                with contributions by Jeremy Avigad
     6.7 +*)
     6.8 +
     6.9 +header {* Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets *}
    6.10 +
    6.11 +theory Lattices_Big
    6.12 +imports Finite_Set
    6.13 +begin
    6.14 +
    6.15 +subsection {* Generic lattice operations over a set *}
    6.16 +
    6.17 +no_notation times (infixl "*" 70)
    6.18 +no_notation Groups.one ("1")
    6.19 +
    6.20 +
    6.21 +subsubsection {* Without neutral element *}
    6.22 +
    6.23 +locale semilattice_set = semilattice
    6.24 +begin
    6.25 +
    6.26 +interpretation comp_fun_idem f
    6.27 +  by default (simp_all add: fun_eq_iff left_commute)
    6.28 +
    6.29 +definition F :: "'a set \<Rightarrow> 'a"
    6.30 +where
    6.31 +  eq_fold': "F A = the (Finite_Set.fold (\<lambda>x y. Some (case y of None \<Rightarrow> x | Some z \<Rightarrow> f x z)) None A)"
    6.32 +
    6.33 +lemma eq_fold:
    6.34 +  assumes "finite A"
    6.35 +  shows "F (insert x A) = Finite_Set.fold f x A"
    6.36 +proof (rule sym)
    6.37 +  let ?f = "\<lambda>x y. Some (case y of None \<Rightarrow> x | Some z \<Rightarrow> f x z)"
    6.38 +  interpret comp_fun_idem "?f"
    6.39 +    by default (simp_all add: fun_eq_iff commute left_commute split: option.split)
    6.40 +  from assms show "Finite_Set.fold f x A = F (insert x A)"
    6.41 +  proof induct
    6.42 +    case empty then show ?case by (simp add: eq_fold')
    6.43 +  next
    6.44 +    case (insert y B) then show ?case by (simp add: insert_commute [of x] eq_fold')
    6.45 +  qed
    6.46 +qed
    6.47 +
    6.48 +lemma singleton [simp]:
    6.49 +  "F {x} = x"
    6.50 +  by (simp add: eq_fold)
    6.51 +
    6.52 +lemma insert_not_elem:
    6.53 +  assumes "finite A" and "x \<notin> A" and "A \<noteq> {}"
    6.54 +  shows "F (insert x A) = x * F A"
    6.55 +proof -
    6.56 +  from `A \<noteq> {}` obtain b where "b \<in> A" by blast
    6.57 +  then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)
    6.58 +  with `finite A` and `x \<notin> A`
    6.59 +    have "finite (insert x B)" and "b \<notin> insert x B" by auto
    6.60 +  then have "F (insert b (insert x B)) = x * F (insert b B)"
    6.61 +    by (simp add: eq_fold)
    6.62 +  then show ?thesis by (simp add: * insert_commute)
    6.63 +qed
    6.64 +
    6.65 +lemma in_idem:
    6.66 +  assumes "finite A" and "x \<in> A"
    6.67 +  shows "x * F A = F A"
    6.68 +proof -
    6.69 +  from assms have "A \<noteq> {}" by auto
    6.70 +  with `finite A` show ?thesis using `x \<in> A`
    6.71 +    by (induct A rule: finite_ne_induct) (auto simp add: ac_simps insert_not_elem)
    6.72 +qed
    6.73 +
    6.74 +lemma insert [simp]:
    6.75 +  assumes "finite A" and "A \<noteq> {}"
    6.76 +  shows "F (insert x A) = x * F A"
    6.77 +  using assms by (cases "x \<in> A") (simp_all add: insert_absorb in_idem insert_not_elem)
    6.78 +
    6.79 +lemma union:
    6.80 +  assumes "finite A" "A \<noteq> {}" and "finite B" "B \<noteq> {}"
    6.81 +  shows "F (A \<union> B) = F A * F B"
    6.82 +  using assms by (induct A rule: finite_ne_induct) (simp_all add: ac_simps)
    6.83 +
    6.84 +lemma remove:
    6.85 +  assumes "finite A" and "x \<in> A"
    6.86 +  shows "F A = (if A - {x} = {} then x else x * F (A - {x}))"
    6.87 +proof -
    6.88 +  from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
    6.89 +  with assms show ?thesis by simp
    6.90 +qed
    6.91 +
    6.92 +lemma insert_remove:
    6.93 +  assumes "finite A"
    6.94 +  shows "F (insert x A) = (if A - {x} = {} then x else x * F (A - {x}))"
    6.95 +  using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
    6.96 +
    6.97 +lemma subset:
    6.98 +  assumes "finite A" "B \<noteq> {}" and "B \<subseteq> A"
    6.99 +  shows "F B * F A = F A"
   6.100 +proof -
   6.101 +  from assms have "A \<noteq> {}" and "finite B" by (auto dest: finite_subset)
   6.102 +  with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
   6.103 +qed
   6.104 +
   6.105 +lemma closed:
   6.106 +  assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
   6.107 +  shows "F A \<in> A"
   6.108 +using `finite A` `A \<noteq> {}` proof (induct rule: finite_ne_induct)
   6.109 +  case singleton then show ?case by simp
   6.110 +next
   6.111 +  case insert with elem show ?case by force
   6.112 +qed
   6.113 +
   6.114 +lemma hom_commute:
   6.115 +  assumes hom: "\<And>x y. h (x * y) = h x * h y"
   6.116 +  and N: "finite N" "N \<noteq> {}"
   6.117 +  shows "h (F N) = F (h ` N)"
   6.118 +using N proof (induct rule: finite_ne_induct)
   6.119 +  case singleton thus ?case by simp
   6.120 +next
   6.121 +  case (insert n N)
   6.122 +  then have "h (F (insert n N)) = h (n * F N)" by simp
   6.123 +  also have "\<dots> = h n * h (F N)" by (rule hom)
   6.124 +  also have "h (F N) = F (h ` N)" by (rule insert)
   6.125 +  also have "h n * \<dots> = F (insert (h n) (h ` N))"
   6.126 +    using insert by simp
   6.127 +  also have "insert (h n) (h ` N) = h ` insert n N" by simp
   6.128 +  finally show ?case .
   6.129 +qed
   6.130 +
   6.131 +end
   6.132 +
   6.133 +locale semilattice_order_set = semilattice_order + semilattice_set
   6.134 +begin
   6.135 +
   6.136 +lemma bounded_iff:
   6.137 +  assumes "finite A" and "A \<noteq> {}"
   6.138 +  shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
   6.139 +  using assms by (induct rule: finite_ne_induct) (simp_all add: bounded_iff)
   6.140 +
   6.141 +lemma boundedI:
   6.142 +  assumes "finite A"
   6.143 +  assumes "A \<noteq> {}"
   6.144 +  assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
   6.145 +  shows "x \<preceq> F A"
   6.146 +  using assms by (simp add: bounded_iff)
   6.147 +
   6.148 +lemma boundedE:
   6.149 +  assumes "finite A" and "A \<noteq> {}" and "x \<preceq> F A"
   6.150 +  obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
   6.151 +  using assms by (simp add: bounded_iff)
   6.152 +
   6.153 +lemma coboundedI:
   6.154 +  assumes "finite A"
   6.155 +    and "a \<in> A"
   6.156 +  shows "F A \<preceq> a"
   6.157 +proof -
   6.158 +  from assms have "A \<noteq> {}" by auto
   6.159 +  from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
   6.160 +  proof (induct rule: finite_ne_induct)
   6.161 +    case singleton thus ?case by (simp add: refl)
   6.162 +  next
   6.163 +    case (insert x B)
   6.164 +    from insert have "a = x \<or> a \<in> B" by simp
   6.165 +    then show ?case using insert by (auto intro: coboundedI2)
   6.166 +  qed
   6.167 +qed
   6.168 +
   6.169 +lemma antimono:
   6.170 +  assumes "A \<subseteq> B" and "A \<noteq> {}" and "finite B"
   6.171 +  shows "F B \<preceq> F A"
   6.172 +proof (cases "A = B")
   6.173 +  case True then show ?thesis by (simp add: refl)
   6.174 +next
   6.175 +  case False
   6.176 +  have B: "B = A \<union> (B - A)" using `A \<subseteq> B` by blast
   6.177 +  then have "F B = F (A \<union> (B - A))" by simp
   6.178 +  also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
   6.179 +  also have "\<dots> \<preceq> F A" by simp
   6.180 +  finally show ?thesis .
   6.181 +qed
   6.182 +
   6.183 +end
   6.184 +
   6.185 +
   6.186 +subsubsection {* With neutral element *}
   6.187 +
   6.188 +locale semilattice_neutr_set = semilattice_neutr
   6.189 +begin
   6.190 +
   6.191 +interpretation comp_fun_idem f
   6.192 +  by default (simp_all add: fun_eq_iff left_commute)
   6.193 +
   6.194 +definition F :: "'a set \<Rightarrow> 'a"
   6.195 +where
   6.196 +  eq_fold: "F A = Finite_Set.fold f 1 A"
   6.197 +
   6.198 +lemma infinite [simp]:
   6.199 +  "\<not> finite A \<Longrightarrow> F A = 1"
   6.200 +  by (simp add: eq_fold)
   6.201 +
   6.202 +lemma empty [simp]:
   6.203 +  "F {} = 1"
   6.204 +  by (simp add: eq_fold)
   6.205 +
   6.206 +lemma insert [simp]:
   6.207 +  assumes "finite A"
   6.208 +  shows "F (insert x A) = x * F A"
   6.209 +  using assms by (simp add: eq_fold)
   6.210 +
   6.211 +lemma in_idem:
   6.212 +  assumes "finite A" and "x \<in> A"
   6.213 +  shows "x * F A = F A"
   6.214 +proof -
   6.215 +  from assms have "A \<noteq> {}" by auto
   6.216 +  with `finite A` show ?thesis using `x \<in> A`
   6.217 +    by (induct A rule: finite_ne_induct) (auto simp add: ac_simps)
   6.218 +qed
   6.219 +
   6.220 +lemma union:
   6.221 +  assumes "finite A" and "finite B"
   6.222 +  shows "F (A \<union> B) = F A * F B"
   6.223 +  using assms by (induct A) (simp_all add: ac_simps)
   6.224 +
   6.225 +lemma remove:
   6.226 +  assumes "finite A" and "x \<in> A"
   6.227 +  shows "F A = x * F (A - {x})"
   6.228 +proof -
   6.229 +  from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
   6.230 +  with assms show ?thesis by simp
   6.231 +qed
   6.232 +
   6.233 +lemma insert_remove:
   6.234 +  assumes "finite A"
   6.235 +  shows "F (insert x A) = x * F (A - {x})"
   6.236 +  using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
   6.237 +
   6.238 +lemma subset:
   6.239 +  assumes "finite A" and "B \<subseteq> A"
   6.240 +  shows "F B * F A = F A"
   6.241 +proof -
   6.242 +  from assms have "finite B" by (auto dest: finite_subset)
   6.243 +  with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
   6.244 +qed
   6.245 +
   6.246 +lemma closed:
   6.247 +  assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
   6.248 +  shows "F A \<in> A"
   6.249 +using `finite A` `A \<noteq> {}` proof (induct rule: finite_ne_induct)
   6.250 +  case singleton then show ?case by simp
   6.251 +next
   6.252 +  case insert with elem show ?case by force
   6.253 +qed
   6.254 +
   6.255 +end
   6.256 +
   6.257 +locale semilattice_order_neutr_set = semilattice_neutr_order + semilattice_neutr_set
   6.258 +begin
   6.259 +
   6.260 +lemma bounded_iff:
   6.261 +  assumes "finite A"
   6.262 +  shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
   6.263 +  using assms by (induct A) (simp_all add: bounded_iff)
   6.264 +
   6.265 +lemma boundedI:
   6.266 +  assumes "finite A"
   6.267 +  assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
   6.268 +  shows "x \<preceq> F A"
   6.269 +  using assms by (simp add: bounded_iff)
   6.270 +
   6.271 +lemma boundedE:
   6.272 +  assumes "finite A" and "x \<preceq> F A"
   6.273 +  obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
   6.274 +  using assms by (simp add: bounded_iff)
   6.275 +
   6.276 +lemma coboundedI:
   6.277 +  assumes "finite A"
   6.278 +    and "a \<in> A"
   6.279 +  shows "F A \<preceq> a"
   6.280 +proof -
   6.281 +  from assms have "A \<noteq> {}" by auto
   6.282 +  from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
   6.283 +  proof (induct rule: finite_ne_induct)
   6.284 +    case singleton thus ?case by (simp add: refl)
   6.285 +  next
   6.286 +    case (insert x B)
   6.287 +    from insert have "a = x \<or> a \<in> B" by simp
   6.288 +    then show ?case using insert by (auto intro: coboundedI2)
   6.289 +  qed
   6.290 +qed
   6.291 +
   6.292 +lemma antimono:
   6.293 +  assumes "A \<subseteq> B" and "finite B"
   6.294 +  shows "F B \<preceq> F A"
   6.295 +proof (cases "A = B")
   6.296 +  case True then show ?thesis by (simp add: refl)
   6.297 +next
   6.298 +  case False
   6.299 +  have B: "B = A \<union> (B - A)" using `A \<subseteq> B` by blast
   6.300 +  then have "F B = F (A \<union> (B - A))" by simp
   6.301 +  also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
   6.302 +  also have "\<dots> \<preceq> F A" by simp
   6.303 +  finally show ?thesis .
   6.304 +qed
   6.305 +
   6.306 +end
   6.307 +
   6.308 +notation times (infixl "*" 70)
   6.309 +notation Groups.one ("1")
   6.310 +
   6.311 +
   6.312 +subsection {* Lattice operations on finite sets *}
   6.313 +
   6.314 +text {*
   6.315 +  For historic reasons, there is the sublocale dependency from @{class distrib_lattice}
   6.316 +  to @{class linorder}.  This is badly designed: both should depend on a common abstract
   6.317 +  distributive lattice rather than having this non-subclass dependecy between two
   6.318 +  classes.  But for the moment we have to live with it.  This forces us to setup
   6.319 +  this sublocale dependency simultaneously with the lattice operations on finite
   6.320 +  sets, to avoid garbage.
   6.321 +*}
   6.322 +
   6.323 +definition (in semilattice_inf) Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
   6.324 +where
   6.325 +  "Inf_fin = semilattice_set.F inf"
   6.326 +
   6.327 +definition (in semilattice_sup) Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
   6.328 +where
   6.329 +  "Sup_fin = semilattice_set.F sup"
   6.330 +
   6.331 +context linorder
   6.332 +begin
   6.333 +
   6.334 +definition Min :: "'a set \<Rightarrow> 'a"
   6.335 +where
   6.336 +  "Min = semilattice_set.F min"
   6.337 +
   6.338 +definition Max :: "'a set \<Rightarrow> 'a"
   6.339 +where
   6.340 +  "Max = semilattice_set.F max"
   6.341 +
   6.342 +sublocale Min!: semilattice_order_set min less_eq less
   6.343 +  + Max!: semilattice_order_set max greater_eq greater
   6.344 +where
   6.345 +  "semilattice_set.F min = Min"
   6.346 +  and "semilattice_set.F max = Max"
   6.347 +proof -
   6.348 +  show "semilattice_order_set min less_eq less" by default (auto simp add: min_def)
   6.349 +  then interpret Min!: semilattice_order_set min less_eq less .
   6.350 +  show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def)
   6.351 +  then interpret Max!: semilattice_order_set max greater_eq greater .
   6.352 +  from Min_def show "semilattice_set.F min = Min" by rule
   6.353 +  from Max_def show "semilattice_set.F max = Max" by rule
   6.354 +qed
   6.355 +
   6.356 +
   6.357 +text {* An aside: @{const min}/@{const max} on linear orders as special case of @{const inf}/@{const sup} *}
   6.358 +
   6.359 +sublocale min_max!: distrib_lattice min less_eq less max
   6.360 +where
   6.361 +  "semilattice_inf.Inf_fin min = Min"
   6.362 +  and "semilattice_sup.Sup_fin max = Max"
   6.363 +proof -
   6.364 +  show "class.distrib_lattice min less_eq less max"
   6.365 +  proof
   6.366 +    fix x y z
   6.367 +    show "max x (min y z) = min (max x y) (max x z)"
   6.368 +      by (auto simp add: min_def max_def)
   6.369 +  qed (auto simp add: min_def max_def not_le less_imp_le)
   6.370 +  then interpret min_max!: distrib_lattice min less_eq less max .
   6.371 +  show "semilattice_inf.Inf_fin min = Min"
   6.372 +    by (simp only: min_max.Inf_fin_def Min_def)
   6.373 +  show "semilattice_sup.Sup_fin max = Max"
   6.374 +    by (simp only: min_max.Sup_fin_def Max_def)
   6.375 +qed
   6.376 +
   6.377 +lemmas le_maxI1 = min_max.sup_ge1
   6.378 +lemmas le_maxI2 = min_max.sup_ge2
   6.379 + 
   6.380 +lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   6.381 +  min.left_commute
   6.382 +
   6.383 +lemmas max_ac = min_max.sup_assoc min_max.sup_commute
   6.384 +  max.left_commute
   6.385 +
   6.386 +end
   6.387 +
   6.388 +
   6.389 +text {* Lattice operations proper *}
   6.390 +
   6.391 +sublocale semilattice_inf < Inf_fin!: semilattice_order_set inf less_eq less
   6.392 +where
   6.393 +  "semilattice_set.F inf = Inf_fin"
   6.394 +proof -
   6.395 +  show "semilattice_order_set inf less_eq less" ..
   6.396 +  then interpret Inf_fin!: semilattice_order_set inf less_eq less .
   6.397 +  from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule
   6.398 +qed
   6.399 +
   6.400 +sublocale semilattice_sup < Sup_fin!: semilattice_order_set sup greater_eq greater
   6.401 +where
   6.402 +  "semilattice_set.F sup = Sup_fin"
   6.403 +proof -
   6.404 +  show "semilattice_order_set sup greater_eq greater" ..
   6.405 +  then interpret Sup_fin!: semilattice_order_set sup greater_eq greater .
   6.406 +  from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule
   6.407 +qed
   6.408 +
   6.409 +
   6.410 +text {* An aside again: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin} *}
   6.411 +
   6.412 +lemma Inf_fin_Min:
   6.413 +  "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)"
   6.414 +  by (simp add: Inf_fin_def Min_def inf_min)
   6.415 +
   6.416 +lemma Sup_fin_Max:
   6.417 +  "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)"
   6.418 +  by (simp add: Sup_fin_def Max_def sup_max)
   6.419 +
   6.420 +
   6.421 +
   6.422 +subsection {* Infimum and Supremum over non-empty sets *}
   6.423 +
   6.424 +text {*
   6.425 +  After this non-regular bootstrap, things continue canonically.
   6.426 +*}
   6.427 +
   6.428 +context lattice
   6.429 +begin
   6.430 +
   6.431 +lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA"
   6.432 +apply(subgoal_tac "EX a. a:A")
   6.433 +prefer 2 apply blast
   6.434 +apply(erule exE)
   6.435 +apply(rule order_trans)
   6.436 +apply(erule (1) Inf_fin.coboundedI)
   6.437 +apply(erule (1) Sup_fin.coboundedI)
   6.438 +done
   6.439 +
   6.440 +lemma sup_Inf_absorb [simp]:
   6.441 +  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) = a"
   6.442 +apply(subst sup_commute)
   6.443 +apply(simp add: sup_absorb2 Inf_fin.coboundedI)
   6.444 +done
   6.445 +
   6.446 +lemma inf_Sup_absorb [simp]:
   6.447 +  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) = a"
   6.448 +by (simp add: inf_absorb1 Sup_fin.coboundedI)
   6.449 +
   6.450 +end
   6.451 +
   6.452 +context distrib_lattice
   6.453 +begin
   6.454 +
   6.455 +lemma sup_Inf1_distrib:
   6.456 +  assumes "finite A"
   6.457 +    and "A \<noteq> {}"
   6.458 +  shows "sup x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup x a|a. a \<in> A}"
   6.459 +using assms by (simp add: image_def Inf_fin.hom_commute [where h="sup x", OF sup_inf_distrib1])
   6.460 +  (rule arg_cong [where f="Inf_fin"], blast)
   6.461 +
   6.462 +lemma sup_Inf2_distrib:
   6.463 +  assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
   6.464 +  shows "sup (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB) = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup a b|a b. a \<in> A \<and> b \<in> B}"
   6.465 +using A proof (induct rule: finite_ne_induct)
   6.466 +  case singleton then show ?case
   6.467 +    by (simp add: sup_Inf1_distrib [OF B])
   6.468 +next
   6.469 +  case (insert x A)
   6.470 +  have finB: "finite {sup x b |b. b \<in> B}"
   6.471 +    by (rule finite_surj [where f = "sup x", OF B(1)], auto)
   6.472 +  have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
   6.473 +  proof -
   6.474 +    have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
   6.475 +      by blast
   6.476 +    thus ?thesis by(simp add: insert(1) B(1))
   6.477 +  qed
   6.478 +  have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
   6.479 +  have "sup (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n(insert x A)) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB) = sup (inf x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA)) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB)"
   6.480 +    using insert by simp
   6.481 +  also have "\<dots> = inf (sup x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB)) (sup (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB))" by(rule sup_inf_distrib2)
   6.482 +  also have "\<dots> = inf (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup x b|b. b \<in> B}) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup a b|a b. a \<in> A \<and> b \<in> B})"
   6.483 +    using insert by(simp add:sup_Inf1_distrib[OF B])
   6.484 +  also have "\<dots> = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n({sup x b |b. b \<in> B} \<union> {sup a b |a b. a \<in> A \<and> b \<in> B})"
   6.485 +    (is "_ = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n?M")
   6.486 +    using B insert
   6.487 +    by (simp add: Inf_fin.union [OF finB _ finAB ne])
   6.488 +  also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
   6.489 +    by blast
   6.490 +  finally show ?case .
   6.491 +qed
   6.492 +
   6.493 +lemma inf_Sup1_distrib:
   6.494 +  assumes "finite A" and "A \<noteq> {}"
   6.495 +  shows "inf x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) = \<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf x a|a. a \<in> A}"
   6.496 +using assms by (simp add: image_def Sup_fin.hom_commute [where h="inf x", OF inf_sup_distrib1])
   6.497 +  (rule arg_cong [where f="Sup_fin"], blast)
   6.498 +
   6.499 +lemma inf_Sup2_distrib:
   6.500 +  assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
   6.501 +  shows "inf (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB) = \<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf a b|a b. a \<in> A \<and> b \<in> B}"
   6.502 +using A proof (induct rule: finite_ne_induct)
   6.503 +  case singleton thus ?case
   6.504 +    by(simp add: inf_Sup1_distrib [OF B])
   6.505 +next
   6.506 +  case (insert x A)
   6.507 +  have finB: "finite {inf x b |b. b \<in> B}"
   6.508 +    by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
   6.509 +  have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
   6.510 +  proof -
   6.511 +    have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
   6.512 +      by blast
   6.513 +    thus ?thesis by(simp add: insert(1) B(1))
   6.514 +  qed
   6.515 +  have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
   6.516 +  have "inf (\<Squnion>\<^sub>f\<^sub>i\<^sub>n(insert x A)) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB) = inf (sup x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA)) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB)"
   6.517 +    using insert by simp
   6.518 +  also have "\<dots> = sup (inf x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB)) (inf (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB))" by(rule inf_sup_distrib2)
   6.519 +  also have "\<dots> = sup (\<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf x b|b. b \<in> B}) (\<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf a b|a b. a \<in> A \<and> b \<in> B})"
   6.520 +    using insert by(simp add:inf_Sup1_distrib[OF B])
   6.521 +  also have "\<dots> = \<Squnion>\<^sub>f\<^sub>i\<^sub>n({inf x b |b. b \<in> B} \<union> {inf a b |a b. a \<in> A \<and> b \<in> B})"
   6.522 +    (is "_ = \<Squnion>\<^sub>f\<^sub>i\<^sub>n?M")
   6.523 +    using B insert
   6.524 +    by (simp add: Sup_fin.union [OF finB _ finAB ne])
   6.525 +  also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
   6.526 +    by blast
   6.527 +  finally show ?case .
   6.528 +qed
   6.529 +
   6.530 +end
   6.531 +
   6.532 +context complete_lattice
   6.533 +begin
   6.534 +
   6.535 +lemma Inf_fin_Inf:
   6.536 +  assumes "finite A" and "A \<noteq> {}"
   6.537 +  shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA = Inf A"
   6.538 +proof -
   6.539 +  from assms obtain b B where "A = insert b B" and "finite B" by auto
   6.540 +  then show ?thesis
   6.541 +    by (simp add: Inf_fin.eq_fold inf_Inf_fold_inf inf.commute [of b])
   6.542 +qed
   6.543 +
   6.544 +lemma Sup_fin_Sup:
   6.545 +  assumes "finite A" and "A \<noteq> {}"
   6.546 +  shows "\<Squnion>\<^sub>f\<^sub>i\<^sub>nA = Sup A"
   6.547 +proof -
   6.548 +  from assms obtain b B where "A = insert b B" and "finite B" by auto
   6.549 +  then show ?thesis
   6.550 +    by (simp add: Sup_fin.eq_fold sup_Sup_fold_sup sup.commute [of b])
   6.551 +qed
   6.552 +
   6.553 +end
   6.554 +
   6.555 +
   6.556 +subsection {* Minimum and Maximum over non-empty sets *}
   6.557 +
   6.558 +context linorder
   6.559 +begin
   6.560 +
   6.561 +lemma dual_min:
   6.562 +  "ord.min greater_eq = max"
   6.563 +  by (auto simp add: ord.min_def max_def fun_eq_iff)
   6.564 +
   6.565 +lemma dual_max:
   6.566 +  "ord.max greater_eq = min"
   6.567 +  by (auto simp add: ord.max_def min_def fun_eq_iff)
   6.568 +
   6.569 +lemma dual_Min:
   6.570 +  "linorder.Min greater_eq = Max"
   6.571 +proof -
   6.572 +  interpret dual!: linorder greater_eq greater by (fact dual_linorder)
   6.573 +  show ?thesis by (simp add: dual.Min_def dual_min Max_def)
   6.574 +qed
   6.575 +
   6.576 +lemma dual_Max:
   6.577 +  "linorder.Max greater_eq = Min"
   6.578 +proof -
   6.579 +  interpret dual!: linorder greater_eq greater by (fact dual_linorder)
   6.580 +  show ?thesis by (simp add: dual.Max_def dual_max Min_def)
   6.581 +qed
   6.582 +
   6.583 +lemmas Min_singleton = Min.singleton
   6.584 +lemmas Max_singleton = Max.singleton
   6.585 +lemmas Min_insert = Min.insert
   6.586 +lemmas Max_insert = Max.insert
   6.587 +lemmas Min_Un = Min.union
   6.588 +lemmas Max_Un = Max.union
   6.589 +lemmas hom_Min_commute = Min.hom_commute
   6.590 +lemmas hom_Max_commute = Max.hom_commute
   6.591 +
   6.592 +lemma Min_in [simp]:
   6.593 +  assumes "finite A" and "A \<noteq> {}"
   6.594 +  shows "Min A \<in> A"
   6.595 +  using assms by (auto simp add: min_def Min.closed)
   6.596 +
   6.597 +lemma Max_in [simp]:
   6.598 +  assumes "finite A" and "A \<noteq> {}"
   6.599 +  shows "Max A \<in> A"
   6.600 +  using assms by (auto simp add: max_def Max.closed)
   6.601 +
   6.602 +lemma Min_le [simp]:
   6.603 +  assumes "finite A" and "x \<in> A"
   6.604 +  shows "Min A \<le> x"
   6.605 +  using assms by (fact Min.coboundedI)
   6.606 +
   6.607 +lemma Max_ge [simp]:
   6.608 +  assumes "finite A" and "x \<in> A"
   6.609 +  shows "x \<le> Max A"
   6.610 +  using assms by (fact Max.coboundedI)
   6.611 +
   6.612 +lemma Min_eqI:
   6.613 +  assumes "finite A"
   6.614 +  assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
   6.615 +    and "x \<in> A"
   6.616 +  shows "Min A = x"
   6.617 +proof (rule antisym)
   6.618 +  from `x \<in> A` have "A \<noteq> {}" by auto
   6.619 +  with assms show "Min A \<ge> x" by simp
   6.620 +next
   6.621 +  from assms show "x \<ge> Min A" by simp
   6.622 +qed
   6.623 +
   6.624 +lemma Max_eqI:
   6.625 +  assumes "finite A"
   6.626 +  assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
   6.627 +    and "x \<in> A"
   6.628 +  shows "Max A = x"
   6.629 +proof (rule antisym)
   6.630 +  from `x \<in> A` have "A \<noteq> {}" by auto
   6.631 +  with assms show "Max A \<le> x" by simp
   6.632 +next
   6.633 +  from assms show "x \<le> Max A" by simp
   6.634 +qed
   6.635 +
   6.636 +context
   6.637 +  fixes A :: "'a set"
   6.638 +  assumes fin_nonempty: "finite A" "A \<noteq> {}"
   6.639 +begin
   6.640 +
   6.641 +lemma Min_ge_iff [simp]:
   6.642 +  "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
   6.643 +  using fin_nonempty by (fact Min.bounded_iff)
   6.644 +
   6.645 +lemma Max_le_iff [simp]:
   6.646 +  "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
   6.647 +  using fin_nonempty by (fact Max.bounded_iff)
   6.648 +
   6.649 +lemma Min_gr_iff [simp]:
   6.650 +  "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
   6.651 +  using fin_nonempty  by (induct rule: finite_ne_induct) simp_all
   6.652 +
   6.653 +lemma Max_less_iff [simp]:
   6.654 +  "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
   6.655 +  using fin_nonempty by (induct rule: finite_ne_induct) simp_all
   6.656 +
   6.657 +lemma Min_le_iff:
   6.658 +  "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
   6.659 +  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj)
   6.660 +
   6.661 +lemma Max_ge_iff:
   6.662 +  "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
   6.663 +  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj)
   6.664 +
   6.665 +lemma Min_less_iff:
   6.666 +  "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
   6.667 +  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj)
   6.668 +
   6.669 +lemma Max_gr_iff:
   6.670 +  "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
   6.671 +  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj)
   6.672 +
   6.673 +end
   6.674 +
   6.675 +lemma Min_antimono:
   6.676 +  assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   6.677 +  shows "Min N \<le> Min M"
   6.678 +  using assms by (fact Min.antimono)
   6.679 +
   6.680 +lemma Max_mono:
   6.681 +  assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   6.682 +  shows "Max M \<le> Max N"
   6.683 +  using assms by (fact Max.antimono)
   6.684 +
   6.685 +lemma mono_Min_commute:
   6.686 +  assumes "mono f"
   6.687 +  assumes "finite A" and "A \<noteq> {}"
   6.688 +  shows "f (Min A) = Min (f ` A)"
   6.689 +proof (rule linorder_class.Min_eqI [symmetric])
   6.690 +  from `finite A` show "finite (f ` A)" by simp
   6.691 +  from assms show "f (Min A) \<in> f ` A" by simp
   6.692 +  fix x
   6.693 +  assume "x \<in> f ` A"
   6.694 +  then obtain y where "y \<in> A" and "x = f y" ..
   6.695 +  with assms have "Min A \<le> y" by auto
   6.696 +  with `mono f` have "f (Min A) \<le> f y" by (rule monoE)
   6.697 +  with `x = f y` show "f (Min A) \<le> x" by simp
   6.698 +qed
   6.699 +
   6.700 +lemma mono_Max_commute:
   6.701 +  assumes "mono f"
   6.702 +  assumes "finite A" and "A \<noteq> {}"
   6.703 +  shows "f (Max A) = Max (f ` A)"
   6.704 +proof (rule linorder_class.Max_eqI [symmetric])
   6.705 +  from `finite A` show "finite (f ` A)" by simp
   6.706 +  from assms show "f (Max A) \<in> f ` A" by simp
   6.707 +  fix x
   6.708 +  assume "x \<in> f ` A"
   6.709 +  then obtain y where "y \<in> A" and "x = f y" ..
   6.710 +  with assms have "y \<le> Max A" by auto
   6.711 +  with `mono f` have "f y \<le> f (Max A)" by (rule monoE)
   6.712 +  with `x = f y` show "x \<le> f (Max A)" by simp
   6.713 +qed
   6.714 +
   6.715 +lemma finite_linorder_max_induct [consumes 1, case_names empty insert]:
   6.716 +  assumes fin: "finite A"
   6.717 +  and empty: "P {}" 
   6.718 +  and insert: "\<And>b A. finite A \<Longrightarrow> \<forall>a\<in>A. a < b \<Longrightarrow> P A \<Longrightarrow> P (insert b A)"
   6.719 +  shows "P A"
   6.720 +using fin empty insert
   6.721 +proof (induct rule: finite_psubset_induct)
   6.722 +  case (psubset A)
   6.723 +  have IH: "\<And>B. \<lbrakk>B < A; P {}; (\<And>A b. \<lbrakk>finite A; \<forall>a\<in>A. a<b; P A\<rbrakk> \<Longrightarrow> P (insert b A))\<rbrakk> \<Longrightarrow> P B" by fact 
   6.724 +  have fin: "finite A" by fact 
   6.725 +  have empty: "P {}" by fact
   6.726 +  have step: "\<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)" by fact
   6.727 +  show "P A"
   6.728 +  proof (cases "A = {}")
   6.729 +    assume "A = {}" 
   6.730 +    then show "P A" using `P {}` by simp
   6.731 +  next
   6.732 +    let ?B = "A - {Max A}" 
   6.733 +    let ?A = "insert (Max A) ?B"
   6.734 +    have "finite ?B" using `finite A` by simp
   6.735 +    assume "A \<noteq> {}"
   6.736 +    with `finite A` have "Max A : A" by auto
   6.737 +    then have A: "?A = A" using insert_Diff_single insert_absorb by auto
   6.738 +    then have "P ?B" using `P {}` step IH [of ?B] by blast
   6.739 +    moreover 
   6.740 +    have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastforce
   6.741 +    ultimately show "P A" using A insert_Diff_single step [OF `finite ?B`] by fastforce
   6.742 +  qed
   6.743 +qed
   6.744 +
   6.745 +lemma finite_linorder_min_induct [consumes 1, case_names empty insert]:
   6.746 +  "\<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"
   6.747 +  by (rule linorder.finite_linorder_max_induct [OF dual_linorder])
   6.748 +
   6.749 +lemma Least_Min:
   6.750 +  assumes "finite {a. P a}" and "\<exists>a. P a"
   6.751 +  shows "(LEAST a. P a) = Min {a. P a}"
   6.752 +proof -
   6.753 +  { fix A :: "'a set"
   6.754 +    assume A: "finite A" "A \<noteq> {}"
   6.755 +    have "(LEAST a. a \<in> A) = Min A"
   6.756 +    using A proof (induct A rule: finite_ne_induct)
   6.757 +      case singleton show ?case by (rule Least_equality) simp_all
   6.758 +    next
   6.759 +      case (insert a A)
   6.760 +      have "(LEAST b. b = a \<or> b \<in> A) = min a (LEAST a. a \<in> A)"
   6.761 +        by (auto intro!: Least_equality simp add: min_def not_le Min_le_iff insert.hyps dest!: less_imp_le)
   6.762 +      with insert show ?case by simp
   6.763 +    qed
   6.764 +  } from this [of "{a. P a}"] assms show ?thesis by simp
   6.765 +qed
   6.766 +
   6.767 +end
   6.768 +
   6.769 +context linordered_ab_semigroup_add
   6.770 +begin
   6.771 +
   6.772 +lemma add_Min_commute:
   6.773 +  fixes k
   6.774 +  assumes "finite N" and "N \<noteq> {}"
   6.775 +  shows "k + Min N = Min {k + m | m. m \<in> N}"
   6.776 +proof -
   6.777 +  have "\<And>x y. k + min x y = min (k + x) (k + y)"
   6.778 +    by (simp add: min_def not_le)
   6.779 +      (blast intro: antisym less_imp_le add_left_mono)
   6.780 +  with assms show ?thesis
   6.781 +    using hom_Min_commute [of "plus k" N]
   6.782 +    by simp (blast intro: arg_cong [where f = Min])
   6.783 +qed
   6.784 +
   6.785 +lemma add_Max_commute:
   6.786 +  fixes k
   6.787 +  assumes "finite N" and "N \<noteq> {}"
   6.788 +  shows "k + Max N = Max {k + m | m. m \<in> N}"
   6.789 +proof -
   6.790 +  have "\<And>x y. k + max x y = max (k + x) (k + y)"
   6.791 +    by (simp add: max_def not_le)
   6.792 +      (blast intro: antisym less_imp_le add_left_mono)
   6.793 +  with assms show ?thesis
   6.794 +    using hom_Max_commute [of "plus k" N]
   6.795 +    by simp (blast intro: arg_cong [where f = Max])
   6.796 +qed
   6.797 +
   6.798 +end
   6.799 +
   6.800 +context linordered_ab_group_add
   6.801 +begin
   6.802 +
   6.803 +lemma minus_Max_eq_Min [simp]:
   6.804 +  "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Max S = Min (uminus ` S)"
   6.805 +  by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min)
   6.806 +
   6.807 +lemma minus_Min_eq_Max [simp]:
   6.808 +  "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Min S = Max (uminus ` S)"
   6.809 +  by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max)
   6.810 +
   6.811 +end
   6.812 +
   6.813 +context complete_linorder
   6.814 +begin
   6.815 +
   6.816 +lemma Min_Inf:
   6.817 +  assumes "finite A" and "A \<noteq> {}"
   6.818 +  shows "Min A = Inf A"
   6.819 +proof -
   6.820 +  from assms obtain b B where "A = insert b B" and "finite B" by auto
   6.821 +  then show ?thesis
   6.822 +    by (simp add: Min.eq_fold complete_linorder_inf_min [symmetric] inf_Inf_fold_inf inf.commute [of b])
   6.823 +qed
   6.824 +
   6.825 +lemma Max_Sup:
   6.826 +  assumes "finite A" and "A \<noteq> {}"
   6.827 +  shows "Max A = Sup A"
   6.828 +proof -
   6.829 +  from assms obtain b B where "A = insert b B" and "finite B" by auto
   6.830 +  then show ?thesis
   6.831 +    by (simp add: Max.eq_fold complete_linorder_sup_max [symmetric] sup_Sup_fold_sup sup.commute [of b])
   6.832 +qed
   6.833 +
   6.834 +end
   6.835 +
   6.836 +end