author haftmann Sun Dec 15 15:10:14 2013 +0100 (2013-12-15) changeset 54744 1e7f2d296e19 parent 54743 b9ae4a2f615b child 54745 46e441e61ff5
more algebraic terminology for theories about big operators
 src/Doc/Main/Main_Doc.thy file | annotate | diff | revisions src/HOL/Big_Operators.thy file | annotate | diff | revisions src/HOL/Equiv_Relations.thy file | annotate | diff | revisions src/HOL/Groups_Big.thy file | annotate | diff | revisions src/HOL/Hilbert_Choice.thy file | annotate | diff | revisions src/HOL/Lattices_Big.thy file | annotate | diff | revisions
     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.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.176 -apply (subst UNION_disjoint, simp, simp)
2.177 - apply blast
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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.2130 -begin
2.2131 -
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.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.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.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.184 +apply (subst UNION_disjoint, simp, simp)
4.185 + apply blast
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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.770 +begin
6.771 +
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.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.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