src/HOL/Big_Operators.thy
 author haftmann Tue Mar 26 21:53:56 2013 +0100 (2013-03-26) changeset 51546 2e26df807dc7 parent 51540 eea5c4ca4a0e child 51586 7c59fe17f495 permissions -rw-r--r--
more uniform style for interpretation and sublocale declarations
 haftmann@35719 ` 1` ```(* Title: HOL/Big_Operators.thy ``` wenzelm@12396 ` 2` ``` Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel ``` avigad@16775 ` 3` ``` with contributions by Jeremy Avigad ``` wenzelm@12396 ` 4` ```*) ``` wenzelm@12396 ` 5` haftmann@35719 ` 6` ```header {* Big operators and finite (non-empty) sets *} ``` haftmann@26041 ` 7` haftmann@35719 ` 8` ```theory Big_Operators ``` haftmann@51489 ` 9` ```imports Finite_Set Option Metis ``` haftmann@26041 ` 10` ```begin ``` haftmann@26041 ` 11` haftmann@35816 ` 12` ```subsection {* Generic monoid operation over a set *} ``` haftmann@35816 ` 13` haftmann@35816 ` 14` ```no_notation times (infixl "*" 70) ``` haftmann@35816 ` 15` ```no_notation Groups.one ("1") ``` haftmann@35816 ` 16` haftmann@51489 ` 17` ```locale comm_monoid_set = comm_monoid ``` haftmann@51489 ` 18` ```begin ``` haftmann@35816 ` 19` haftmann@51489 ` 20` ```definition F :: "('b \ 'a) \ 'b set \ 'a" ``` haftmann@51489 ` 21` ```where ``` haftmann@51489 ` 22` ``` eq_fold: "F g A = Finite_Set.fold (f \ g) 1 A" ``` haftmann@35816 ` 23` haftmann@35816 ` 24` ```lemma infinite [simp]: ``` haftmann@35816 ` 25` ``` "\ finite A \ F g A = 1" ``` haftmann@51489 ` 26` ``` by (simp add: eq_fold) ``` haftmann@51489 ` 27` haftmann@51489 ` 28` ```lemma empty [simp]: ``` haftmann@51489 ` 29` ``` "F g {} = 1" ``` haftmann@51489 ` 30` ``` by (simp add: eq_fold) ``` haftmann@51489 ` 31` haftmann@51489 ` 32` ```lemma insert [simp]: ``` haftmann@51489 ` 33` ``` assumes "finite A" and "x \ A" ``` haftmann@51489 ` 34` ``` shows "F g (insert x A) = g x * F g A" ``` haftmann@51489 ` 35` ```proof - ``` haftmann@51489 ` 36` ``` interpret comp_fun_commute f ``` haftmann@51489 ` 37` ``` by default (simp add: fun_eq_iff left_commute) ``` haftmann@51489 ` 38` ``` interpret comp_fun_commute "f \ g" ``` haftmann@51489 ` 39` ``` by (rule comp_comp_fun_commute) ``` haftmann@51489 ` 40` ``` from assms show ?thesis by (simp add: eq_fold) ``` haftmann@51489 ` 41` ```qed ``` haftmann@51489 ` 42` haftmann@51489 ` 43` ```lemma remove: ``` haftmann@51489 ` 44` ``` assumes "finite A" and "x \ A" ``` haftmann@51489 ` 45` ``` shows "F g A = g x * F g (A - {x})" ``` haftmann@51489 ` 46` ```proof - ``` haftmann@51489 ` 47` ``` from `x \ A` obtain B where A: "A = insert x B" and "x \ B" ``` haftmann@51489 ` 48` ``` by (auto dest: mk_disjoint_insert) ``` haftmann@51489 ` 49` ``` moreover from `finite A` this have "finite B" by simp ``` haftmann@51489 ` 50` ``` ultimately show ?thesis by simp ``` haftmann@51489 ` 51` ```qed ``` haftmann@51489 ` 52` haftmann@51489 ` 53` ```lemma insert_remove: ``` haftmann@51489 ` 54` ``` assumes "finite A" ``` haftmann@51489 ` 55` ``` shows "F g (insert x A) = g x * F g (A - {x})" ``` haftmann@51489 ` 56` ``` using assms by (cases "x \ A") (simp_all add: remove insert_absorb) ``` haftmann@51489 ` 57` haftmann@51489 ` 58` ```lemma neutral: ``` haftmann@51489 ` 59` ``` assumes "\x\A. g x = 1" ``` haftmann@51489 ` 60` ``` shows "F g A = 1" ``` haftmann@51489 ` 61` ```proof (cases "finite A") ``` haftmann@51489 ` 62` ``` case True from `finite A` assms show ?thesis by (induct A) simp_all ``` haftmann@51489 ` 63` ```next ``` haftmann@51489 ` 64` ``` case False then show ?thesis by simp ``` haftmann@51489 ` 65` ```qed ``` haftmann@35816 ` 66` haftmann@51489 ` 67` ```lemma neutral_const [simp]: ``` haftmann@51489 ` 68` ``` "F (\_. 1) A = 1" ``` haftmann@51489 ` 69` ``` by (simp add: neutral) ``` haftmann@51489 ` 70` haftmann@51489 ` 71` ```lemma union_inter: ``` haftmann@51489 ` 72` ``` assumes "finite A" and "finite B" ``` haftmann@51489 ` 73` ``` shows "F g (A \ B) * F g (A \ B) = F g A * F g B" ``` haftmann@51489 ` 74` ``` -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *} ``` haftmann@51489 ` 75` ```using assms proof (induct A) ``` haftmann@51489 ` 76` ``` case empty then show ?case by simp ``` hoelzl@42986 ` 77` ```next ``` haftmann@51489 ` 78` ``` case (insert x A) then show ?case ``` haftmann@51489 ` 79` ``` by (auto simp add: insert_absorb Int_insert_left commute [of _ "g x"] assoc left_commute) ``` haftmann@51489 ` 80` ```qed ``` haftmann@51489 ` 81` haftmann@51489 ` 82` ```corollary union_inter_neutral: ``` haftmann@51489 ` 83` ``` assumes "finite A" and "finite B" ``` haftmann@51489 ` 84` ``` and I0: "\x \ A \ B. g x = 1" ``` haftmann@51489 ` 85` ``` shows "F g (A \ B) = F g A * F g B" ``` haftmann@51489 ` 86` ``` using assms by (simp add: union_inter [symmetric] neutral) ``` haftmann@51489 ` 87` haftmann@51489 ` 88` ```corollary union_disjoint: ``` haftmann@51489 ` 89` ``` assumes "finite A" and "finite B" ``` haftmann@51489 ` 90` ``` assumes "A \ B = {}" ``` haftmann@51489 ` 91` ``` shows "F g (A \ B) = F g A * F g B" ``` haftmann@51489 ` 92` ``` using assms by (simp add: union_inter_neutral) ``` haftmann@51489 ` 93` haftmann@51489 ` 94` ```lemma subset_diff: ``` haftmann@51489 ` 95` ``` "B \ A \ finite A \ F g A = F g (A - B) * F g B" ``` haftmann@51489 ` 96` ``` by (metis Diff_partition union_disjoint Diff_disjoint finite_Un inf_commute sup_commute) ``` haftmann@51489 ` 97` haftmann@51489 ` 98` ```lemma reindex: ``` haftmann@51489 ` 99` ``` assumes "inj_on h A" ``` haftmann@51489 ` 100` ``` shows "F g (h ` A) = F (g \ h) A" ``` haftmann@51489 ` 101` ```proof (cases "finite A") ``` haftmann@51489 ` 102` ``` case True ``` haftmann@51489 ` 103` ``` interpret comp_fun_commute f ``` haftmann@51489 ` 104` ``` by default (simp add: fun_eq_iff left_commute) ``` haftmann@51489 ` 105` ``` interpret comp_fun_commute "f \ g" ``` haftmann@51489 ` 106` ``` by (rule comp_comp_fun_commute) ``` haftmann@51489 ` 107` ``` from assms `finite A` show ?thesis by (simp add: eq_fold fold_image comp_assoc) ``` haftmann@51489 ` 108` ```next ``` haftmann@51489 ` 109` ``` case False with assms have "\ finite (h ` A)" by (blast dest: finite_imageD) ``` haftmann@51489 ` 110` ``` with False show ?thesis by simp ``` hoelzl@42986 ` 111` ```qed ``` hoelzl@42986 ` 112` haftmann@51489 ` 113` ```lemma cong: ``` haftmann@51489 ` 114` ``` assumes "A = B" ``` haftmann@51489 ` 115` ``` assumes g_h: "\x. x \ B \ g x = h x" ``` haftmann@51489 ` 116` ``` shows "F g A = F h B" ``` haftmann@51489 ` 117` ```proof (cases "finite A") ``` haftmann@51489 ` 118` ``` case True ``` haftmann@51489 ` 119` ``` then have "\C. C \ A \ (\x\C. g x = h x) \ F g C = F h C" ``` haftmann@51489 ` 120` ``` proof induct ``` haftmann@51489 ` 121` ``` case empty then show ?case by simp ``` haftmann@51489 ` 122` ``` next ``` haftmann@51489 ` 123` ``` case (insert x F) then show ?case apply - ``` haftmann@51489 ` 124` ``` apply (simp add: subset_insert_iff, clarify) ``` haftmann@51489 ` 125` ``` apply (subgoal_tac "finite C") ``` haftmann@51489 ` 126` ``` prefer 2 apply (blast dest: finite_subset [rotated]) ``` haftmann@51489 ` 127` ``` apply (subgoal_tac "C = insert x (C - {x})") ``` haftmann@51489 ` 128` ``` prefer 2 apply blast ``` haftmann@51489 ` 129` ``` apply (erule ssubst) ``` haftmann@51489 ` 130` ``` apply (simp add: Ball_def del: insert_Diff_single) ``` haftmann@51489 ` 131` ``` done ``` haftmann@51489 ` 132` ``` qed ``` haftmann@51489 ` 133` ``` with `A = B` g_h show ?thesis by simp ``` haftmann@51489 ` 134` ```next ``` haftmann@51489 ` 135` ``` case False ``` haftmann@51489 ` 136` ``` with `A = B` show ?thesis by simp ``` haftmann@51489 ` 137` ```qed ``` nipkow@48849 ` 138` haftmann@51489 ` 139` ```lemma strong_cong [cong]: ``` haftmann@51489 ` 140` ``` assumes "A = B" "\x. x \ B =simp=> g x = h x" ``` haftmann@51489 ` 141` ``` shows "F (\x. g x) A = F (\x. h x) B" ``` haftmann@51489 ` 142` ``` by (rule cong) (insert assms, simp_all add: simp_implies_def) ``` haftmann@51489 ` 143` haftmann@51489 ` 144` ```lemma UNION_disjoint: ``` haftmann@51489 ` 145` ``` assumes "finite I" and "\i\I. finite (A i)" ``` haftmann@51489 ` 146` ``` and "\i\I. \j\I. i \ j \ A i \ A j = {}" ``` haftmann@51489 ` 147` ``` shows "F g (UNION I A) = F (\x. F g (A x)) I" ``` haftmann@51489 ` 148` ```apply (insert assms) ``` haftmann@51489 ` 149` ```apply (induct rule: finite_induct) ``` haftmann@51489 ` 150` ```apply simp ``` haftmann@51489 ` 151` ```apply atomize ``` haftmann@51489 ` 152` ```apply (subgoal_tac "\i\Fa. x \ i") ``` haftmann@51489 ` 153` ``` prefer 2 apply blast ``` haftmann@51489 ` 154` ```apply (subgoal_tac "A x Int UNION Fa A = {}") ``` haftmann@51489 ` 155` ``` prefer 2 apply blast ``` haftmann@51489 ` 156` ```apply (simp add: union_disjoint) ``` haftmann@51489 ` 157` ```done ``` haftmann@51489 ` 158` haftmann@51489 ` 159` ```lemma Union_disjoint: ``` haftmann@51489 ` 160` ``` assumes "\A\C. finite A" "\A\C. \B\C. A \ B \ A \ B = {}" ``` haftmann@51489 ` 161` ``` shows "F g (Union C) = F (F g) C" ``` haftmann@51489 ` 162` ```proof cases ``` haftmann@51489 ` 163` ``` assume "finite C" ``` haftmann@51489 ` 164` ``` from UNION_disjoint [OF this assms] ``` haftmann@51489 ` 165` ``` show ?thesis ``` haftmann@51489 ` 166` ``` by (simp add: SUP_def) ``` haftmann@51489 ` 167` ```qed (auto dest: finite_UnionD intro: infinite) ``` nipkow@48821 ` 168` haftmann@51489 ` 169` ```lemma distrib: ``` haftmann@51489 ` 170` ``` "F (\x. g x * h x) A = F g A * F h A" ``` haftmann@51489 ` 171` ```proof (cases "finite A") ``` haftmann@51489 ` 172` ``` case False then show ?thesis by simp ``` haftmann@51489 ` 173` ```next ``` haftmann@51489 ` 174` ``` case True then show ?thesis by (rule finite_induct) (simp_all add: assoc commute left_commute) ``` haftmann@51489 ` 175` ```qed ``` haftmann@51489 ` 176` haftmann@51489 ` 177` ```lemma Sigma: ``` haftmann@51489 ` 178` ``` "finite A \ \x\A. finite (B x) \ F (\x. F (g x) (B x)) A = F (split g) (SIGMA x:A. B x)" ``` haftmann@51489 ` 179` ```apply (subst Sigma_def) ``` haftmann@51489 ` 180` ```apply (subst UNION_disjoint, assumption, simp) ``` haftmann@51489 ` 181` ``` apply blast ``` haftmann@51489 ` 182` ```apply (rule cong) ``` haftmann@51489 ` 183` ```apply rule ``` haftmann@51489 ` 184` ```apply (simp add: fun_eq_iff) ``` haftmann@51489 ` 185` ```apply (subst UNION_disjoint, simp, simp) ``` haftmann@51489 ` 186` ``` apply blast ``` haftmann@51489 ` 187` ```apply (simp add: comp_def) ``` haftmann@51489 ` 188` ```done ``` haftmann@51489 ` 189` haftmann@51489 ` 190` ```lemma related: ``` haftmann@51489 ` 191` ``` assumes Re: "R 1 1" ``` haftmann@51489 ` 192` ``` and Rop: "\x1 y1 x2 y2. R x1 x2 \ R y1 y2 \ R (x1 * y1) (x2 * y2)" ``` haftmann@51489 ` 193` ``` and fS: "finite S" and Rfg: "\x\S. R (h x) (g x)" ``` haftmann@51489 ` 194` ``` shows "R (F h S) (F g S)" ``` haftmann@51489 ` 195` ``` using fS by (rule finite_subset_induct) (insert assms, auto) ``` nipkow@48849 ` 196` haftmann@51489 ` 197` ```lemma eq_general: ``` haftmann@51489 ` 198` ``` assumes h: "\y\S'. \!x. x \ S \ h x = y" ``` haftmann@51489 ` 199` ``` and f12: "\x\S. h x \ S' \ f2 (h x) = f1 x" ``` haftmann@51489 ` 200` ``` shows "F f1 S = F f2 S'" ``` haftmann@51489 ` 201` ```proof- ``` haftmann@51489 ` 202` ``` from h f12 have hS: "h ` S = S'" by blast ``` haftmann@51489 ` 203` ``` {fix x y assume H: "x \ S" "y \ S" "h x = h y" ``` haftmann@51489 ` 204` ``` from f12 h H have "x = y" by auto } ``` haftmann@51489 ` 205` ``` hence hinj: "inj_on h S" unfolding inj_on_def Ex1_def by blast ``` haftmann@51489 ` 206` ``` from f12 have th: "\x. x \ S \ (f2 \ h) x = f1 x" by auto ``` haftmann@51489 ` 207` ``` from hS have "F f2 S' = F f2 (h ` S)" by simp ``` haftmann@51489 ` 208` ``` also have "\ = F (f2 o h) S" using reindex [OF hinj, of f2] . ``` haftmann@51489 ` 209` ``` also have "\ = F f1 S " using th cong [of _ _ "f2 o h" f1] ``` haftmann@51489 ` 210` ``` by blast ``` haftmann@51489 ` 211` ``` finally show ?thesis .. ``` haftmann@51489 ` 212` ```qed ``` nipkow@48849 ` 213` haftmann@51489 ` 214` ```lemma eq_general_reverses: ``` haftmann@51489 ` 215` ``` assumes kh: "\y. y \ T \ k y \ S \ h (k y) = y" ``` haftmann@51489 ` 216` ``` and hk: "\x. x \ S \ h x \ T \ k (h x) = x \ g (h x) = j x" ``` haftmann@51489 ` 217` ``` shows "F j S = F g T" ``` haftmann@51489 ` 218` ``` (* metis solves it, but not yet available here *) ``` haftmann@51489 ` 219` ``` apply (rule eq_general [of T S h g j]) ``` haftmann@51489 ` 220` ``` apply (rule ballI) ``` haftmann@51489 ` 221` ``` apply (frule kh) ``` haftmann@51489 ` 222` ``` apply (rule ex1I[]) ``` haftmann@51489 ` 223` ``` apply blast ``` haftmann@51489 ` 224` ``` apply clarsimp ``` haftmann@51489 ` 225` ``` apply (drule hk) apply simp ``` haftmann@51489 ` 226` ``` apply (rule sym) ``` haftmann@51489 ` 227` ``` apply (erule conjunct1[OF conjunct2[OF hk]]) ``` haftmann@51489 ` 228` ``` apply (rule ballI) ``` haftmann@51489 ` 229` ``` apply (drule hk) ``` haftmann@51489 ` 230` ``` apply blast ``` haftmann@51489 ` 231` ``` done ``` haftmann@51489 ` 232` haftmann@51489 ` 233` ```lemma mono_neutral_cong_left: ``` nipkow@48849 ` 234` ``` assumes "finite T" and "S \ T" and "\i \ T - S. h i = 1" ``` nipkow@48849 ` 235` ``` and "\x. x \ S \ g x = h x" shows "F g S = F h T" ``` nipkow@48849 ` 236` ```proof- ``` nipkow@48849 ` 237` ``` have eq: "T = S \ (T - S)" using `S \ T` by blast ``` nipkow@48849 ` 238` ``` have d: "S \ (T - S) = {}" using `S \ T` by blast ``` nipkow@48849 ` 239` ``` from `finite T` `S \ T` have f: "finite S" "finite (T - S)" ``` nipkow@48849 ` 240` ``` by (auto intro: finite_subset) ``` nipkow@48849 ` 241` ``` show ?thesis using assms(4) ``` haftmann@51489 ` 242` ``` by (simp add: union_disjoint [OF f d, unfolded eq [symmetric]] neutral [OF assms(3)]) ``` nipkow@48849 ` 243` ```qed ``` nipkow@48849 ` 244` haftmann@51489 ` 245` ```lemma mono_neutral_cong_right: ``` nipkow@48850 ` 246` ``` "\ finite T; S \ T; \i \ T - S. g i = 1; \x. x \ S \ g x = h x \ ``` nipkow@48850 ` 247` ``` \ F g T = F h S" ``` haftmann@51489 ` 248` ``` by (auto intro!: mono_neutral_cong_left [symmetric]) ``` nipkow@48849 ` 249` haftmann@51489 ` 250` ```lemma mono_neutral_left: ``` nipkow@48849 ` 251` ``` "\ finite T; S \ T; \i \ T - S. g i = 1 \ \ F g S = F g T" ``` haftmann@51489 ` 252` ``` by (blast intro: mono_neutral_cong_left) ``` nipkow@48849 ` 253` haftmann@51489 ` 254` ```lemma mono_neutral_right: ``` nipkow@48850 ` 255` ``` "\ finite T; S \ T; \i \ T - S. g i = 1 \ \ F g T = F g S" ``` haftmann@51489 ` 256` ``` by (blast intro!: mono_neutral_left [symmetric]) ``` nipkow@48849 ` 257` haftmann@51489 ` 258` ```lemma delta: ``` nipkow@48849 ` 259` ``` assumes fS: "finite S" ``` haftmann@51489 ` 260` ``` shows "F (\k. if k = a then b k else 1) S = (if a \ S then b a else 1)" ``` nipkow@48849 ` 261` ```proof- ``` nipkow@48849 ` 262` ``` let ?f = "(\k. if k=a then b k else 1)" ``` nipkow@48849 ` 263` ``` { assume a: "a \ S" ``` nipkow@48849 ` 264` ``` hence "\k\S. ?f k = 1" by simp ``` nipkow@48849 ` 265` ``` hence ?thesis using a by simp } ``` nipkow@48849 ` 266` ``` moreover ``` nipkow@48849 ` 267` ``` { assume a: "a \ S" ``` nipkow@48849 ` 268` ``` let ?A = "S - {a}" ``` nipkow@48849 ` 269` ``` let ?B = "{a}" ``` nipkow@48849 ` 270` ``` have eq: "S = ?A \ ?B" using a by blast ``` nipkow@48849 ` 271` ``` have dj: "?A \ ?B = {}" by simp ``` nipkow@48849 ` 272` ``` from fS have fAB: "finite ?A" "finite ?B" by auto ``` nipkow@48849 ` 273` ``` have "F ?f S = F ?f ?A * F ?f ?B" ``` haftmann@51489 ` 274` ``` using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]] ``` nipkow@48849 ` 275` ``` by simp ``` haftmann@51489 ` 276` ``` then have ?thesis using a by simp } ``` nipkow@48849 ` 277` ``` ultimately show ?thesis by blast ``` nipkow@48849 ` 278` ```qed ``` nipkow@48849 ` 279` haftmann@51489 ` 280` ```lemma delta': ``` haftmann@51489 ` 281` ``` assumes fS: "finite S" ``` haftmann@51489 ` 282` ``` shows "F (\k. if a = k then b k else 1) S = (if a \ S then b a else 1)" ``` haftmann@51489 ` 283` ``` using delta [OF fS, of a b, symmetric] by (auto intro: cong) ``` nipkow@48893 ` 284` hoelzl@42986 ` 285` ```lemma If_cases: ``` hoelzl@42986 ` 286` ``` fixes P :: "'b \ bool" and g h :: "'b \ 'a" ``` hoelzl@42986 ` 287` ``` assumes fA: "finite A" ``` hoelzl@42986 ` 288` ``` shows "F (\x. if P x then h x else g x) A = ``` haftmann@51489 ` 289` ``` F h (A \ {x. P x}) * F g (A \ - {x. P x})" ``` haftmann@51489 ` 290` ```proof - ``` hoelzl@42986 ` 291` ``` have a: "A = A \ {x. P x} \ A \ -{x. P x}" ``` hoelzl@42986 ` 292` ``` "(A \ {x. P x}) \ (A \ -{x. P x}) = {}" ``` hoelzl@42986 ` 293` ``` by blast+ ``` hoelzl@42986 ` 294` ``` from fA ``` hoelzl@42986 ` 295` ``` have f: "finite (A \ {x. P x})" "finite (A \ -{x. P x})" by auto ``` hoelzl@42986 ` 296` ``` let ?g = "\x. if P x then h x else g x" ``` haftmann@51489 ` 297` ``` from union_disjoint [OF f a(2), of ?g] a(1) ``` hoelzl@42986 ` 298` ``` show ?thesis ``` haftmann@51489 ` 299` ``` by (subst (1 2) cong) simp_all ``` hoelzl@42986 ` 300` ```qed ``` hoelzl@42986 ` 301` haftmann@51489 ` 302` ```lemma cartesian_product: ``` haftmann@51489 ` 303` ``` "F (\x. F (g x) B) A = F (split g) (A <*> B)" ``` haftmann@51489 ` 304` ```apply (rule sym) ``` haftmann@51489 ` 305` ```apply (cases "finite A") ``` haftmann@51489 ` 306` ``` apply (cases "finite B") ``` haftmann@51489 ` 307` ``` apply (simp add: Sigma) ``` haftmann@51489 ` 308` ``` apply (cases "A={}", simp) ``` haftmann@51489 ` 309` ``` apply simp ``` haftmann@51489 ` 310` ```apply (auto intro: infinite dest: finite_cartesian_productD2) ``` haftmann@51489 ` 311` ```apply (cases "B = {}") apply (auto intro: infinite dest: finite_cartesian_productD1) ``` haftmann@51489 ` 312` ```done ``` haftmann@51489 ` 313` haftmann@35816 ` 314` ```end ``` haftmann@35816 ` 315` haftmann@35816 ` 316` ```notation times (infixl "*" 70) ``` haftmann@35816 ` 317` ```notation Groups.one ("1") ``` haftmann@35816 ` 318` haftmann@35816 ` 319` nipkow@15402 ` 320` ```subsection {* Generalized summation over a set *} ``` nipkow@15402 ` 321` haftmann@51489 ` 322` ```definition (in comm_monoid_add) setsum :: "('b \ 'a) \ 'b set \ 'a" ``` haftmann@51489 ` 323` ```where ``` haftmann@51489 ` 324` ``` "setsum = comm_monoid_set.F plus 0" ``` haftmann@26041 ` 325` haftmann@51489 ` 326` ```sublocale comm_monoid_add < setsum!: comm_monoid_set plus 0 ``` haftmann@51489 ` 327` ```where ``` haftmann@51546 ` 328` ``` "comm_monoid_set.F plus 0 = setsum" ``` haftmann@51489 ` 329` ```proof - ``` haftmann@51489 ` 330` ``` show "comm_monoid_set plus 0" .. ``` haftmann@51489 ` 331` ``` then interpret setsum!: comm_monoid_set plus 0 . ``` haftmann@51546 ` 332` ``` from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule ``` haftmann@51489 ` 333` ```qed ``` nipkow@15402 ` 334` wenzelm@19535 ` 335` ```abbreviation ``` haftmann@51489 ` 336` ``` Setsum ("\_" [1000] 999) where ``` haftmann@51489 ` 337` ``` "\A \ setsum (%x. x) A" ``` wenzelm@19535 ` 338` nipkow@15402 ` 339` ```text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is ``` nipkow@15402 ` 340` ```written @{text"\x\A. e"}. *} ``` nipkow@15402 ` 341` nipkow@15402 ` 342` ```syntax ``` paulson@17189 ` 343` ``` "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3SUM _:_. _)" [0, 51, 10] 10) ``` nipkow@15402 ` 344` ```syntax (xsymbols) ``` paulson@17189 ` 345` ``` "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\_\_. _)" [0, 51, 10] 10) ``` nipkow@15402 ` 346` ```syntax (HTML output) ``` paulson@17189 ` 347` ``` "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\_\_. _)" [0, 51, 10] 10) ``` nipkow@15402 ` 348` nipkow@15402 ` 349` ```translations -- {* Beware of argument permutation! *} ``` nipkow@28853 ` 350` ``` "SUM i:A. b" == "CONST setsum (%i. b) A" ``` nipkow@28853 ` 351` ``` "\i\A. b" == "CONST setsum (%i. b) A" ``` nipkow@15402 ` 352` nipkow@15402 ` 353` ```text{* Instead of @{term"\x\{x. P}. e"} we introduce the shorter ``` nipkow@15402 ` 354` ``` @{text"\x|P. e"}. *} ``` nipkow@15402 ` 355` nipkow@15402 ` 356` ```syntax ``` paulson@17189 ` 357` ``` "_qsetsum" :: "pttrn \ bool \ 'a \ 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10) ``` nipkow@15402 ` 358` ```syntax (xsymbols) ``` paulson@17189 ` 359` ``` "_qsetsum" :: "pttrn \ bool \ 'a \ 'a" ("(3\_ | (_)./ _)" [0,0,10] 10) ``` nipkow@15402 ` 360` ```syntax (HTML output) ``` paulson@17189 ` 361` ``` "_qsetsum" :: "pttrn \ bool \ 'a \ 'a" ("(3\_ | (_)./ _)" [0,0,10] 10) ``` nipkow@15402 ` 362` nipkow@15402 ` 363` ```translations ``` nipkow@28853 ` 364` ``` "SUM x|P. t" => "CONST setsum (%x. t) {x. P}" ``` nipkow@28853 ` 365` ``` "\x|P. t" => "CONST setsum (%x. t) {x. P}" ``` nipkow@15402 ` 366` nipkow@15402 ` 367` ```print_translation {* ``` nipkow@15402 ` 368` ```let ``` wenzelm@35115 ` 369` ``` fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) \$ Abs (y, Ty, P)] = ``` wenzelm@35115 ` 370` ``` if x <> y then raise Match ``` wenzelm@35115 ` 371` ``` else ``` wenzelm@35115 ` 372` ``` let ``` wenzelm@49660 ` 373` ``` val x' = Syntax_Trans.mark_bound_body (x, Tx); ``` wenzelm@35115 ` 374` ``` val t' = subst_bound (x', t); ``` wenzelm@35115 ` 375` ``` val P' = subst_bound (x', P); ``` wenzelm@49660 ` 376` ``` in ``` wenzelm@49660 ` 377` ``` Syntax.const @{syntax_const "_qsetsum"} \$ Syntax_Trans.mark_bound_abs (x, Tx) \$ P' \$ t' ``` wenzelm@49660 ` 378` ``` end ``` wenzelm@35115 ` 379` ``` | setsum_tr' _ = raise Match; ``` wenzelm@35115 ` 380` ```in [(@{const_syntax setsum}, setsum_tr')] end ``` nipkow@15402 ` 381` ```*} ``` nipkow@15402 ` 382` haftmann@51489 ` 383` ```text {* TODO These are candidates for generalization *} ``` nipkow@15402 ` 384` haftmann@51489 ` 385` ```context comm_monoid_add ``` haftmann@51489 ` 386` ```begin ``` nipkow@15402 ` 387` haftmann@51489 ` 388` ```lemma setsum_reindex_id: ``` haftmann@35816 ` 389` ``` "inj_on f B ==> setsum f B = setsum id (f ` B)" ``` haftmann@51489 ` 390` ``` by (simp add: setsum.reindex) ``` nipkow@15402 ` 391` haftmann@51489 ` 392` ```lemma setsum_reindex_nonzero: ``` chaieb@29674 ` 393` ``` assumes fS: "finite S" ``` haftmann@51489 ` 394` ``` and nz: "\x y. x \ S \ y \ S \ x \ y \ f x = f y \ h (f x) = 0" ``` haftmann@51489 ` 395` ``` shows "setsum h (f ` S) = setsum (h \ f) S" ``` haftmann@51489 ` 396` ```using nz proof (induct rule: finite_induct [OF fS]) ``` chaieb@29674 ` 397` ``` case 1 thus ?case by simp ``` chaieb@29674 ` 398` ```next ``` chaieb@29674 ` 399` ``` case (2 x F) ``` nipkow@48849 ` 400` ``` { assume fxF: "f x \ f ` F" hence "\y \ F . f y = f x" by auto ``` chaieb@29674 ` 401` ``` then obtain y where y: "y \ F" "f x = f y" by auto ``` chaieb@29674 ` 402` ``` from "2.hyps" y have xy: "x \ y" by auto ``` haftmann@51489 ` 403` ``` from "2.prems" [of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp ``` chaieb@29674 ` 404` ``` have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto ``` chaieb@29674 ` 405` ``` also have "\ = setsum (h o f) (insert x F)" ``` haftmann@35816 ` 406` ``` unfolding setsum.insert[OF `finite F` `x\F`] ``` haftmann@35816 ` 407` ``` using h0 ``` haftmann@51489 ` 408` ``` apply (simp cong del: setsum.strong_cong) ``` chaieb@29674 ` 409` ``` apply (rule "2.hyps"(3)) ``` chaieb@29674 ` 410` ``` apply (rule_tac y="y" in "2.prems") ``` chaieb@29674 ` 411` ``` apply simp_all ``` chaieb@29674 ` 412` ``` done ``` nipkow@48849 ` 413` ``` finally have ?case . } ``` chaieb@29674 ` 414` ``` moreover ``` nipkow@48849 ` 415` ``` { assume fxF: "f x \ f ` F" ``` chaieb@29674 ` 416` ``` have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)" ``` chaieb@29674 ` 417` ``` using fxF "2.hyps" by simp ``` chaieb@29674 ` 418` ``` also have "\ = setsum (h o f) (insert x F)" ``` haftmann@35816 ` 419` ``` unfolding setsum.insert[OF `finite F` `x\F`] ``` haftmann@51489 ` 420` ``` apply (simp cong del: setsum.strong_cong) ``` haftmann@35816 ` 421` ``` apply (rule cong [OF refl [of "op + (h (f x))"]]) ``` chaieb@29674 ` 422` ``` apply (rule "2.hyps"(3)) ``` chaieb@29674 ` 423` ``` apply (rule_tac y="y" in "2.prems") ``` chaieb@29674 ` 424` ``` apply simp_all ``` chaieb@29674 ` 425` ``` done ``` nipkow@48849 ` 426` ``` finally have ?case . } ``` chaieb@29674 ` 427` ``` ultimately show ?case by blast ``` chaieb@29674 ` 428` ```qed ``` chaieb@29674 ` 429` haftmann@51489 ` 430` ```lemma setsum_cong2: ``` haftmann@51489 ` 431` ``` "(\x. x \ A \ f x = g x) \ setsum f A = setsum g A" ``` haftmann@51489 ` 432` ``` by (auto intro: setsum.cong) ``` nipkow@15554 ` 433` nipkow@48849 ` 434` ```lemma setsum_reindex_cong: ``` nipkow@28853 ` 435` ``` "[|inj_on f A; B = f ` A; !!a. a:A \ g a = h (f a)|] ``` nipkow@28853 ` 436` ``` ==> setsum h B = setsum g A" ``` haftmann@51489 ` 437` ``` by (simp add: setsum.reindex) ``` chaieb@29674 ` 438` chaieb@30260 ` 439` ```lemma setsum_restrict_set: ``` chaieb@30260 ` 440` ``` assumes fA: "finite A" ``` chaieb@30260 ` 441` ``` shows "setsum f (A \ B) = setsum (\x. if x \ B then f x else 0) A" ``` chaieb@30260 ` 442` ```proof- ``` chaieb@30260 ` 443` ``` from fA have fab: "finite (A \ B)" by auto ``` chaieb@30260 ` 444` ``` have aba: "A \ B \ A" by blast ``` chaieb@30260 ` 445` ``` let ?g = "\x. if x \ A\B then f x else 0" ``` haftmann@51489 ` 446` ``` from setsum.mono_neutral_left [OF fA aba, of ?g] ``` chaieb@30260 ` 447` ``` show ?thesis by simp ``` chaieb@30260 ` 448` ```qed ``` chaieb@30260 ` 449` nipkow@15402 ` 450` ```lemma setsum_Union_disjoint: ``` hoelzl@44937 ` 451` ``` assumes "\A\C. finite A" "\A\C. \B\C. A \ B \ A Int B = {}" ``` hoelzl@44937 ` 452` ``` shows "setsum f (Union C) = setsum (setsum f) C" ``` haftmann@51489 ` 453` ``` using assms by (fact setsum.Union_disjoint) ``` nipkow@15402 ` 454` haftmann@51489 ` 455` ```lemma setsum_cartesian_product: ``` haftmann@51489 ` 456` ``` "(\x\A. (\y\B. f x y)) = (\(x,y) \ A <*> B. f x y)" ``` haftmann@51489 ` 457` ``` by (fact setsum.cartesian_product) ``` nipkow@15402 ` 458` haftmann@51489 ` 459` ```lemma setsum_UNION_zero: ``` nipkow@48893 ` 460` ``` assumes fS: "finite S" and fSS: "\T \ S. finite T" ``` nipkow@48893 ` 461` ``` and f0: "\T1 T2 x. T1\S \ T2\S \ T1 \ T2 \ x \ T1 \ x \ T2 \ f x = 0" ``` nipkow@48893 ` 462` ``` shows "setsum f (\S) = setsum (\T. setsum f T) S" ``` nipkow@48893 ` 463` ``` using fSS f0 ``` nipkow@48893 ` 464` ```proof(induct rule: finite_induct[OF fS]) ``` nipkow@48893 ` 465` ``` case 1 thus ?case by simp ``` nipkow@48893 ` 466` ```next ``` nipkow@48893 ` 467` ``` case (2 T F) ``` nipkow@48893 ` 468` ``` then have fTF: "finite T" "\T\F. finite T" "finite F" and TF: "T \ F" ``` nipkow@48893 ` 469` ``` and H: "setsum f (\ F) = setsum (setsum f) F" by auto ``` nipkow@48893 ` 470` ``` from fTF have fUF: "finite (\F)" by auto ``` nipkow@48893 ` 471` ``` from "2.prems" TF fTF ``` nipkow@48893 ` 472` ``` show ?case ``` haftmann@51489 ` 473` ``` by (auto simp add: H [symmetric] intro: setsum.union_inter_neutral [OF fTF(1) fUF, of f]) ``` haftmann@51489 ` 474` ```qed ``` haftmann@51489 ` 475` haftmann@51489 ` 476` ```text {* Commuting outer and inner summation *} ``` haftmann@51489 ` 477` haftmann@51489 ` 478` ```lemma setsum_commute: ``` haftmann@51489 ` 479` ``` "(\i\A. \j\B. f i j) = (\j\B. \i\A. f i j)" ``` haftmann@51489 ` 480` ```proof (simp add: setsum_cartesian_product) ``` haftmann@51489 ` 481` ``` have "(\(x,y) \ A <*> B. f x y) = ``` haftmann@51489 ` 482` ``` (\(y,x) \ (%(i, j). (j, i)) ` (A \ B). f x y)" ``` haftmann@51489 ` 483` ``` (is "?s = _") ``` haftmann@51489 ` 484` ``` apply (simp add: setsum.reindex [where h = "%(i, j). (j, i)"] swap_inj_on) ``` haftmann@51489 ` 485` ``` apply (simp add: split_def) ``` haftmann@51489 ` 486` ``` done ``` haftmann@51489 ` 487` ``` also have "... = (\(y,x)\B \ A. f x y)" ``` haftmann@51489 ` 488` ``` (is "_ = ?t") ``` haftmann@51489 ` 489` ``` apply (simp add: swap_product) ``` haftmann@51489 ` 490` ``` done ``` haftmann@51489 ` 491` ``` finally show "?s = ?t" . ``` haftmann@51489 ` 492` ```qed ``` haftmann@51489 ` 493` haftmann@51489 ` 494` ```lemma setsum_Plus: ``` haftmann@51489 ` 495` ``` fixes A :: "'a set" and B :: "'b set" ``` haftmann@51489 ` 496` ``` assumes fin: "finite A" "finite B" ``` haftmann@51489 ` 497` ``` shows "setsum f (A <+> B) = setsum (f \ Inl) A + setsum (f \ Inr) B" ``` haftmann@51489 ` 498` ```proof - ``` haftmann@51489 ` 499` ``` have "A <+> B = Inl ` A \ Inr ` B" by auto ``` haftmann@51489 ` 500` ``` moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)" ``` haftmann@51489 ` 501` ``` by auto ``` haftmann@51489 ` 502` ``` moreover have "Inl ` A \ Inr ` B = ({} :: ('a + 'b) set)" by auto ``` haftmann@51489 ` 503` ``` moreover have "inj_on (Inl :: 'a \ 'a + 'b) A" "inj_on (Inr :: 'b \ 'a + 'b) B" by(auto intro: inj_onI) ``` haftmann@51489 ` 504` ``` ultimately show ?thesis using fin by(simp add: setsum.union_disjoint setsum.reindex) ``` nipkow@48893 ` 505` ```qed ``` nipkow@48893 ` 506` haftmann@51489 ` 507` ```end ``` haftmann@51489 ` 508` haftmann@51489 ` 509` ```text {* TODO These are legacy *} ``` haftmann@51489 ` 510` haftmann@51489 ` 511` ```lemma setsum_empty: ``` haftmann@51489 ` 512` ``` "setsum f {} = 0" ``` haftmann@51489 ` 513` ``` by (fact setsum.empty) ``` haftmann@51489 ` 514` haftmann@51489 ` 515` ```lemma setsum_insert: ``` haftmann@51489 ` 516` ``` "finite F ==> a \ F ==> setsum f (insert a F) = f a + setsum f F" ``` haftmann@51489 ` 517` ``` by (fact setsum.insert) ``` haftmann@51489 ` 518` haftmann@51489 ` 519` ```lemma setsum_infinite: ``` haftmann@51489 ` 520` ``` "~ finite A ==> setsum f A = 0" ``` haftmann@51489 ` 521` ``` by (fact setsum.infinite) ``` haftmann@51489 ` 522` haftmann@51489 ` 523` ```lemma setsum_reindex: ``` haftmann@51489 ` 524` ``` "inj_on f B \ setsum h (f ` B) = setsum (h \ f) B" ``` haftmann@51489 ` 525` ``` by (fact setsum.reindex) ``` haftmann@51489 ` 526` haftmann@51489 ` 527` ```lemma setsum_cong: ``` haftmann@51489 ` 528` ``` "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B" ``` haftmann@51489 ` 529` ``` by (fact setsum.cong) ``` haftmann@51489 ` 530` haftmann@51489 ` 531` ```lemma strong_setsum_cong: ``` haftmann@51489 ` 532` ``` "A = B ==> (!!x. x:B =simp=> f x = g x) ``` haftmann@51489 ` 533` ``` ==> setsum (%x. f x) A = setsum (%x. g x) B" ``` haftmann@51489 ` 534` ``` by (fact setsum.strong_cong) ``` haftmann@51489 ` 535` haftmann@51489 ` 536` ```lemmas setsum_0 = setsum.neutral_const ``` haftmann@51489 ` 537` ```lemmas setsum_0' = setsum.neutral ``` haftmann@51489 ` 538` haftmann@51489 ` 539` ```lemma setsum_Un_Int: "finite A ==> finite B ==> ``` haftmann@51489 ` 540` ``` setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B" ``` haftmann@51489 ` 541` ``` -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *} ``` haftmann@51489 ` 542` ``` by (fact setsum.union_inter) ``` haftmann@51489 ` 543` haftmann@51489 ` 544` ```lemma setsum_Un_disjoint: "finite A ==> finite B ``` haftmann@51489 ` 545` ``` ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B" ``` haftmann@51489 ` 546` ``` by (fact setsum.union_disjoint) ``` haftmann@51489 ` 547` haftmann@51489 ` 548` ```lemma setsum_subset_diff: "\ B \ A; finite A \ \ ``` haftmann@51489 ` 549` ``` setsum f A = setsum f (A - B) + setsum f B" ``` haftmann@51489 ` 550` ``` by (fact setsum.subset_diff) ``` haftmann@51489 ` 551` haftmann@51489 ` 552` ```lemma setsum_mono_zero_left: ``` haftmann@51489 ` 553` ``` "\ finite T; S \ T; \i \ T - S. f i = 0 \ \ setsum f S = setsum f T" ``` haftmann@51489 ` 554` ``` by (fact setsum.mono_neutral_left) ``` haftmann@51489 ` 555` haftmann@51489 ` 556` ```lemmas setsum_mono_zero_right = setsum.mono_neutral_right ``` haftmann@51489 ` 557` haftmann@51489 ` 558` ```lemma setsum_mono_zero_cong_left: ``` haftmann@51489 ` 559` ``` "\ finite T; S \ T; \i \ T - S. g i = 0; \x. x \ S \ f x = g x \ ``` haftmann@51489 ` 560` ``` \ setsum f S = setsum g T" ``` haftmann@51489 ` 561` ``` by (fact setsum.mono_neutral_cong_left) ``` haftmann@51489 ` 562` haftmann@51489 ` 563` ```lemmas setsum_mono_zero_cong_right = setsum.mono_neutral_cong_right ``` haftmann@51489 ` 564` haftmann@51489 ` 565` ```lemma setsum_delta: "finite S \ ``` haftmann@51489 ` 566` ``` setsum (\k. if k=a then b k else 0) S = (if a \ S then b a else 0)" ``` haftmann@51489 ` 567` ``` by (fact setsum.delta) ``` haftmann@51489 ` 568` haftmann@51489 ` 569` ```lemma setsum_delta': "finite S \ ``` haftmann@51489 ` 570` ``` setsum (\k. if a = k then b k else 0) S = (if a\ S then b a else 0)" ``` haftmann@51489 ` 571` ``` by (fact setsum.delta') ``` haftmann@51489 ` 572` haftmann@51489 ` 573` ```lemma setsum_cases: ``` haftmann@51489 ` 574` ``` assumes "finite A" ``` haftmann@51489 ` 575` ``` shows "setsum (\x. if P x then f x else g x) A = ``` haftmann@51489 ` 576` ``` setsum f (A \ {x. P x}) + setsum g (A \ - {x. P x})" ``` haftmann@51489 ` 577` ``` using assms by (fact setsum.If_cases) ``` haftmann@51489 ` 578` haftmann@51489 ` 579` ```(*But we can't get rid of finite I. If infinite, although the rhs is 0, ``` haftmann@51489 ` 580` ``` the lhs need not be, since UNION I A could still be finite.*) ``` haftmann@51489 ` 581` ```lemma setsum_UN_disjoint: ``` haftmann@51489 ` 582` ``` assumes "finite I" and "ALL i:I. finite (A i)" ``` haftmann@51489 ` 583` ``` and "ALL i:I. ALL j:I. i \ j --> A i Int A j = {}" ``` haftmann@51489 ` 584` ``` shows "setsum f (UNION I A) = (\i\I. setsum f (A i))" ``` haftmann@51489 ` 585` ``` using assms by (fact setsum.UNION_disjoint) ``` haftmann@51489 ` 586` haftmann@51489 ` 587` ```(*But we can't get rid of finite A. If infinite, although the lhs is 0, ``` haftmann@51489 ` 588` ``` the rhs need not be, since SIGMA A B could still be finite.*) ``` haftmann@51489 ` 589` ```lemma setsum_Sigma: ``` haftmann@51489 ` 590` ``` assumes "finite A" and "ALL x:A. finite (B x)" ``` haftmann@51489 ` 591` ``` shows "(\x\A. (\y\B x. f x y)) = (\(x,y)\(SIGMA x:A. B x). f x y)" ``` haftmann@51489 ` 592` ``` using assms by (fact setsum.Sigma) ``` haftmann@51489 ` 593` haftmann@51489 ` 594` ```lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)" ``` haftmann@51489 ` 595` ``` by (fact setsum.distrib) ``` haftmann@51489 ` 596` haftmann@51489 ` 597` ```lemma setsum_Un_zero: ``` haftmann@51489 ` 598` ``` "\ finite S; finite T; \x \ S\T. f x = 0 \ \ ``` haftmann@51489 ` 599` ``` setsum f (S \ T) = setsum f S + setsum f T" ``` haftmann@51489 ` 600` ``` by (fact setsum.union_inter_neutral) ``` haftmann@51489 ` 601` haftmann@51489 ` 602` ```lemma setsum_eq_general_reverses: ``` haftmann@51489 ` 603` ``` assumes fS: "finite S" and fT: "finite T" ``` haftmann@51489 ` 604` ``` and kh: "\y. y \ T \ k y \ S \ h (k y) = y" ``` haftmann@51489 ` 605` ``` and hk: "\x. x \ S \ h x \ T \ k (h x) = x \ g (h x) = f x" ``` haftmann@51489 ` 606` ``` shows "setsum f S = setsum g T" ``` haftmann@51489 ` 607` ``` using kh hk by (fact setsum.eq_general_reverses) ``` haftmann@51489 ` 608` nipkow@15402 ` 609` nipkow@15402 ` 610` ```subsubsection {* Properties in more restricted classes of structures *} ``` nipkow@15402 ` 611` nipkow@15402 ` 612` ```lemma setsum_Un: "finite A ==> finite B ==> ``` nipkow@28853 ` 613` ``` (setsum f (A Un B) :: 'a :: ab_group_add) = ``` nipkow@28853 ` 614` ``` setsum f A + setsum f B - setsum f (A Int B)" ``` nipkow@29667 ` 615` ```by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps) ``` nipkow@15402 ` 616` haftmann@49715 ` 617` ```lemma setsum_Un2: ``` haftmann@49715 ` 618` ``` assumes "finite (A \ B)" ``` haftmann@49715 ` 619` ``` shows "setsum f (A \ B) = setsum f (A - B) + setsum f (B - A) + setsum f (A \ B)" ``` haftmann@49715 ` 620` ```proof - ``` haftmann@49715 ` 621` ``` have "A \ B = A - B \ (B - A) \ A \ B" ``` haftmann@49715 ` 622` ``` by auto ``` haftmann@49715 ` 623` ``` with assms show ?thesis by simp (subst setsum_Un_disjoint, auto)+ ``` haftmann@49715 ` 624` ```qed ``` haftmann@49715 ` 625` nipkow@15402 ` 626` ```lemma setsum_diff1: "finite A \ ``` nipkow@15402 ` 627` ``` (setsum f (A - {a}) :: ('a::ab_group_add)) = ``` nipkow@15402 ` 628` ``` (if a:A then setsum f A - f a else setsum f A)" ``` nipkow@28853 ` 629` ```by (erule finite_induct) (auto simp add: insert_Diff_if) ``` nipkow@28853 ` 630` nipkow@15402 ` 631` ```lemma setsum_diff: ``` nipkow@15402 ` 632` ``` assumes le: "finite A" "B \ A" ``` nipkow@15402 ` 633` ``` shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))" ``` nipkow@15402 ` 634` ```proof - ``` nipkow@15402 ` 635` ``` from le have finiteB: "finite B" using finite_subset by auto ``` nipkow@15402 ` 636` ``` show ?thesis using finiteB le ``` wenzelm@21575 ` 637` ``` proof induct ``` wenzelm@19535 ` 638` ``` case empty ``` wenzelm@19535 ` 639` ``` thus ?case by auto ``` wenzelm@19535 ` 640` ``` next ``` wenzelm@19535 ` 641` ``` case (insert x F) ``` wenzelm@19535 ` 642` ``` thus ?case using le finiteB ``` wenzelm@19535 ` 643` ``` by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb) ``` nipkow@15402 ` 644` ``` qed ``` wenzelm@19535 ` 645` ```qed ``` nipkow@15402 ` 646` nipkow@15402 ` 647` ```lemma setsum_mono: ``` haftmann@35028 ` 648` ``` assumes le: "\i. i\K \ f (i::'a) \ ((g i)::('b::{comm_monoid_add, ordered_ab_semigroup_add}))" ``` nipkow@15402 ` 649` ``` shows "(\i\K. f i) \ (\i\K. g i)" ``` nipkow@15402 ` 650` ```proof (cases "finite K") ``` nipkow@15402 ` 651` ``` case True ``` nipkow@15402 ` 652` ``` thus ?thesis using le ``` wenzelm@19535 ` 653` ``` proof induct ``` nipkow@15402 ` 654` ``` case empty ``` nipkow@15402 ` 655` ``` thus ?case by simp ``` nipkow@15402 ` 656` ``` next ``` nipkow@15402 ` 657` ``` case insert ``` nipkow@44890 ` 658` ``` thus ?case using add_mono by fastforce ``` nipkow@15402 ` 659` ``` qed ``` nipkow@15402 ` 660` ```next ``` haftmann@51489 ` 661` ``` case False then show ?thesis by simp ``` nipkow@15402 ` 662` ```qed ``` nipkow@15402 ` 663` nipkow@15554 ` 664` ```lemma setsum_strict_mono: ``` haftmann@35028 ` 665` ``` fixes f :: "'a \ 'b::{ordered_cancel_ab_semigroup_add,comm_monoid_add}" ``` wenzelm@19535 ` 666` ``` assumes "finite A" "A \ {}" ``` wenzelm@19535 ` 667` ``` and "!!x. x:A \ f x < g x" ``` wenzelm@19535 ` 668` ``` shows "setsum f A < setsum g A" ``` wenzelm@41550 ` 669` ``` using assms ``` nipkow@15554 ` 670` ```proof (induct rule: finite_ne_induct) ``` nipkow@15554 ` 671` ``` case singleton thus ?case by simp ``` nipkow@15554 ` 672` ```next ``` nipkow@15554 ` 673` ``` case insert thus ?case by (auto simp: add_strict_mono) ``` nipkow@15554 ` 674` ```qed ``` nipkow@15554 ` 675` nipkow@46699 ` 676` ```lemma setsum_strict_mono_ex1: ``` nipkow@46699 ` 677` ```fixes f :: "'a \ 'b::{comm_monoid_add, ordered_cancel_ab_semigroup_add}" ``` nipkow@46699 ` 678` ```assumes "finite A" and "ALL x:A. f x \ g x" and "EX a:A. f a < g a" ``` nipkow@46699 ` 679` ```shows "setsum f A < setsum g A" ``` nipkow@46699 ` 680` ```proof- ``` nipkow@46699 ` 681` ``` from assms(3) obtain a where a: "a:A" "f a < g a" by blast ``` nipkow@46699 ` 682` ``` have "setsum f A = setsum f ((A-{a}) \ {a})" ``` nipkow@46699 ` 683` ``` by(simp add:insert_absorb[OF `a:A`]) ``` nipkow@46699 ` 684` ``` also have "\ = setsum f (A-{a}) + setsum f {a}" ``` nipkow@46699 ` 685` ``` using `finite A` by(subst setsum_Un_disjoint) auto ``` nipkow@46699 ` 686` ``` also have "setsum f (A-{a}) \ setsum g (A-{a})" ``` nipkow@46699 ` 687` ``` by(rule setsum_mono)(simp add: assms(2)) ``` nipkow@46699 ` 688` ``` also have "setsum f {a} < setsum g {a}" using a by simp ``` nipkow@46699 ` 689` ``` also have "setsum g (A - {a}) + setsum g {a} = setsum g((A-{a}) \ {a})" ``` nipkow@46699 ` 690` ``` using `finite A` by(subst setsum_Un_disjoint[symmetric]) auto ``` nipkow@46699 ` 691` ``` also have "\ = setsum g A" by(simp add:insert_absorb[OF `a:A`]) ``` nipkow@46699 ` 692` ``` finally show ?thesis by (metis add_right_mono add_strict_left_mono) ``` nipkow@46699 ` 693` ```qed ``` nipkow@46699 ` 694` nipkow@15535 ` 695` ```lemma setsum_negf: ``` wenzelm@19535 ` 696` ``` "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A" ``` nipkow@15535 ` 697` ```proof (cases "finite A") ``` berghofe@22262 ` 698` ``` case True thus ?thesis by (induct set: finite) auto ``` nipkow@15535 ` 699` ```next ``` haftmann@51489 ` 700` ``` case False thus ?thesis by simp ``` nipkow@15535 ` 701` ```qed ``` nipkow@15402 ` 702` nipkow@15535 ` 703` ```lemma setsum_subtractf: ``` wenzelm@19535 ` 704` ``` "setsum (%x. ((f x)::'a::ab_group_add) - g x) A = ``` wenzelm@19535 ` 705` ``` setsum f A - setsum g A" ``` nipkow@15535 ` 706` ```proof (cases "finite A") ``` nipkow@15535 ` 707` ``` case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf) ``` nipkow@15535 ` 708` ```next ``` haftmann@51489 ` 709` ``` case False thus ?thesis by simp ``` nipkow@15535 ` 710` ```qed ``` nipkow@15402 ` 711` nipkow@15535 ` 712` ```lemma setsum_nonneg: ``` haftmann@35028 ` 713` ``` assumes nn: "\x\A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \ f x" ``` wenzelm@19535 ` 714` ``` shows "0 \ setsum f A" ``` nipkow@15535 ` 715` ```proof (cases "finite A") ``` nipkow@15535 ` 716` ``` case True thus ?thesis using nn ``` wenzelm@21575 ` 717` ``` proof induct ``` wenzelm@19535 ` 718` ``` case empty then show ?case by simp ``` wenzelm@19535 ` 719` ``` next ``` wenzelm@19535 ` 720` ``` case (insert x F) ``` wenzelm@19535 ` 721` ``` then have "0 + 0 \ f x + setsum f F" by (blast intro: add_mono) ``` wenzelm@19535 ` 722` ``` with insert show ?case by simp ``` wenzelm@19535 ` 723` ``` qed ``` nipkow@15535 ` 724` ```next ``` haftmann@51489 ` 725` ``` case False thus ?thesis by simp ``` nipkow@15535 ` 726` ```qed ``` nipkow@15402 ` 727` nipkow@15535 ` 728` ```lemma setsum_nonpos: ``` haftmann@35028 ` 729` ``` assumes np: "\x\A. f x \ (0::'a::{ordered_ab_semigroup_add,comm_monoid_add})" ``` wenzelm@19535 ` 730` ``` shows "setsum f A \ 0" ``` nipkow@15535 ` 731` ```proof (cases "finite A") ``` nipkow@15535 ` 732` ``` case True thus ?thesis using np ``` wenzelm@21575 ` 733` ``` proof induct ``` wenzelm@19535 ` 734` ``` case empty then show ?case by simp ``` wenzelm@19535 ` 735` ``` next ``` wenzelm@19535 ` 736` ``` case (insert x F) ``` wenzelm@19535 ` 737` ``` then have "f x + setsum f F \ 0 + 0" by (blast intro: add_mono) ``` wenzelm@19535 ` 738` ``` with insert show ?case by simp ``` wenzelm@19535 ` 739` ``` qed ``` nipkow@15535 ` 740` ```next ``` haftmann@51489 ` 741` ``` case False thus ?thesis by simp ``` nipkow@15535 ` 742` ```qed ``` nipkow@15402 ` 743` hoelzl@36622 ` 744` ```lemma setsum_nonneg_leq_bound: ``` hoelzl@36622 ` 745` ``` fixes f :: "'a \ 'b::{ordered_ab_group_add}" ``` hoelzl@36622 ` 746` ``` assumes "finite s" "\i. i \ s \ f i \ 0" "(\i \ s. f i) = B" "i \ s" ``` hoelzl@36622 ` 747` ``` shows "f i \ B" ``` hoelzl@36622 ` 748` ```proof - ``` hoelzl@36622 ` 749` ``` have "0 \ (\ i \ s - {i}. f i)" and "0 \ f i" ``` hoelzl@36622 ` 750` ``` using assms by (auto intro!: setsum_nonneg) ``` hoelzl@36622 ` 751` ``` moreover ``` hoelzl@36622 ` 752` ``` have "(\ i \ s - {i}. f i) + f i = B" ``` hoelzl@36622 ` 753` ``` using assms by (simp add: setsum_diff1) ``` hoelzl@36622 ` 754` ``` ultimately show ?thesis by auto ``` hoelzl@36622 ` 755` ```qed ``` hoelzl@36622 ` 756` hoelzl@36622 ` 757` ```lemma setsum_nonneg_0: ``` hoelzl@36622 ` 758` ``` fixes f :: "'a \ 'b::{ordered_ab_group_add}" ``` hoelzl@36622 ` 759` ``` assumes "finite s" and pos: "\ i. i \ s \ f i \ 0" ``` hoelzl@36622 ` 760` ``` and "(\ i \ s. f i) = 0" and i: "i \ s" ``` hoelzl@36622 ` 761` ``` shows "f i = 0" ``` hoelzl@36622 ` 762` ``` using setsum_nonneg_leq_bound[OF assms] pos[OF i] by auto ``` hoelzl@36622 ` 763` nipkow@15539 ` 764` ```lemma setsum_mono2: ``` haftmann@36303 ` 765` ```fixes f :: "'a \ 'b :: ordered_comm_monoid_add" ``` nipkow@15539 ` 766` ```assumes fin: "finite B" and sub: "A \ B" and nn: "\b. b \ B-A \ 0 \ f b" ``` nipkow@15539 ` 767` ```shows "setsum f A \ setsum f B" ``` nipkow@15539 ` 768` ```proof - ``` nipkow@15539 ` 769` ``` have "setsum f A \ setsum f A + setsum f (B-A)" ``` nipkow@15539 ` 770` ``` by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def) ``` nipkow@15539 ` 771` ``` also have "\ = setsum f (A \ (B-A))" using fin finite_subset[OF sub fin] ``` nipkow@15539 ` 772` ``` by (simp add:setsum_Un_disjoint del:Un_Diff_cancel) ``` nipkow@15539 ` 773` ``` also have "A \ (B-A) = B" using sub by blast ``` nipkow@15539 ` 774` ``` finally show ?thesis . ``` nipkow@15539 ` 775` ```qed ``` nipkow@15542 ` 776` avigad@16775 ` 777` ```lemma setsum_mono3: "finite B ==> A <= B ==> ``` avigad@16775 ` 778` ``` ALL x: B - A. ``` haftmann@35028 ` 779` ``` 0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==> ``` avigad@16775 ` 780` ``` setsum f A <= setsum f B" ``` avigad@16775 ` 781` ``` apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)") ``` avigad@16775 ` 782` ``` apply (erule ssubst) ``` avigad@16775 ` 783` ``` apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)") ``` avigad@16775 ` 784` ``` apply simp ``` avigad@16775 ` 785` ``` apply (rule add_left_mono) ``` avigad@16775 ` 786` ``` apply (erule setsum_nonneg) ``` avigad@16775 ` 787` ``` apply (subst setsum_Un_disjoint [THEN sym]) ``` avigad@16775 ` 788` ``` apply (erule finite_subset, assumption) ``` avigad@16775 ` 789` ``` apply (rule finite_subset) ``` avigad@16775 ` 790` ``` prefer 2 ``` avigad@16775 ` 791` ``` apply assumption ``` haftmann@32698 ` 792` ``` apply (auto simp add: sup_absorb2) ``` avigad@16775 ` 793` ```done ``` avigad@16775 ` 794` ballarin@19279 ` 795` ```lemma setsum_right_distrib: ``` huffman@22934 ` 796` ``` fixes f :: "'a => ('b::semiring_0)" ``` nipkow@15402 ` 797` ``` shows "r * setsum f A = setsum (%n. r * f n) A" ``` nipkow@15402 ` 798` ```proof (cases "finite A") ``` nipkow@15402 ` 799` ``` case True ``` nipkow@15402 ` 800` ``` thus ?thesis ``` wenzelm@21575 ` 801` ``` proof induct ``` nipkow@15402 ` 802` ``` case empty thus ?case by simp ``` nipkow@15402 ` 803` ``` next ``` webertj@49962 ` 804` ``` case (insert x A) thus ?case by (simp add: distrib_left) ``` nipkow@15402 ` 805` ``` qed ``` nipkow@15402 ` 806` ```next ``` haftmann@51489 ` 807` ``` case False thus ?thesis by simp ``` nipkow@15402 ` 808` ```qed ``` nipkow@15402 ` 809` ballarin@17149 ` 810` ```lemma setsum_left_distrib: ``` huffman@22934 ` 811` ``` "setsum f A * (r::'a::semiring_0) = (\n\A. f n * r)" ``` ballarin@17149 ` 812` ```proof (cases "finite A") ``` ballarin@17149 ` 813` ``` case True ``` ballarin@17149 ` 814` ``` then show ?thesis ``` ballarin@17149 ` 815` ``` proof induct ``` ballarin@17149 ` 816` ``` case empty thus ?case by simp ``` ballarin@17149 ` 817` ``` next ``` webertj@49962 ` 818` ``` case (insert x A) thus ?case by (simp add: distrib_right) ``` ballarin@17149 ` 819` ``` qed ``` ballarin@17149 ` 820` ```next ``` haftmann@51489 ` 821` ``` case False thus ?thesis by simp ``` ballarin@17149 ` 822` ```qed ``` ballarin@17149 ` 823` ballarin@17149 ` 824` ```lemma setsum_divide_distrib: ``` ballarin@17149 ` 825` ``` "setsum f A / (r::'a::field) = (\n\A. f n / r)" ``` ballarin@17149 ` 826` ```proof (cases "finite A") ``` ballarin@17149 ` 827` ``` case True ``` ballarin@17149 ` 828` ``` then show ?thesis ``` ballarin@17149 ` 829` ``` proof induct ``` ballarin@17149 ` 830` ``` case empty thus ?case by simp ``` ballarin@17149 ` 831` ``` next ``` ballarin@17149 ` 832` ``` case (insert x A) thus ?case by (simp add: add_divide_distrib) ``` ballarin@17149 ` 833` ``` qed ``` ballarin@17149 ` 834` ```next ``` haftmann@51489 ` 835` ``` case False thus ?thesis by simp ``` ballarin@17149 ` 836` ```qed ``` ballarin@17149 ` 837` nipkow@15535 ` 838` ```lemma setsum_abs[iff]: ``` haftmann@35028 ` 839` ``` fixes f :: "'a => ('b::ordered_ab_group_add_abs)" ``` nipkow@15402 ` 840` ``` shows "abs (setsum f A) \ setsum (%i. abs(f i)) A" ``` nipkow@15535 ` 841` ```proof (cases "finite A") ``` nipkow@15535 ` 842` ``` case True ``` nipkow@15535 ` 843` ``` thus ?thesis ``` wenzelm@21575 ` 844` ``` proof induct ``` nipkow@15535 ` 845` ``` case empty thus ?case by simp ``` nipkow@15535 ` 846` ``` next ``` nipkow@15535 ` 847` ``` case (insert x A) ``` nipkow@15535 ` 848` ``` thus ?case by (auto intro: abs_triangle_ineq order_trans) ``` nipkow@15535 ` 849` ``` qed ``` nipkow@15402 ` 850` ```next ``` haftmann@51489 ` 851` ``` case False thus ?thesis by simp ``` nipkow@15402 ` 852` ```qed ``` nipkow@15402 ` 853` nipkow@15535 ` 854` ```lemma setsum_abs_ge_zero[iff]: ``` haftmann@35028 ` 855` ``` fixes f :: "'a => ('b::ordered_ab_group_add_abs)" ``` nipkow@15402 ` 856` ``` shows "0 \ setsum (%i. abs(f i)) A" ``` nipkow@15535 ` 857` ```proof (cases "finite A") ``` nipkow@15535 ` 858` ``` case True ``` nipkow@15535 ` 859` ``` thus ?thesis ``` wenzelm@21575 ` 860` ``` proof induct ``` nipkow@15535 ` 861` ``` case empty thus ?case by simp ``` nipkow@15535 ` 862` ``` next ``` huffman@36977 ` 863` ``` case (insert x A) thus ?case by auto ``` nipkow@15535 ` 864` ``` qed ``` nipkow@15402 ` 865` ```next ``` haftmann@51489 ` 866` ``` case False thus ?thesis by simp ``` nipkow@15402 ` 867` ```qed ``` nipkow@15402 ` 868` nipkow@15539 ` 869` ```lemma abs_setsum_abs[simp]: ``` haftmann@35028 ` 870` ``` fixes f :: "'a => ('b::ordered_ab_group_add_abs)" ``` nipkow@15539 ` 871` ``` shows "abs (\a\A. abs(f a)) = (\a\A. abs(f a))" ``` nipkow@15539 ` 872` ```proof (cases "finite A") ``` nipkow@15539 ` 873` ``` case True ``` nipkow@15539 ` 874` ``` thus ?thesis ``` wenzelm@21575 ` 875` ``` proof induct ``` nipkow@15539 ` 876` ``` case empty thus ?case by simp ``` nipkow@15539 ` 877` ``` next ``` nipkow@15539 ` 878` ``` case (insert a A) ``` nipkow@15539 ` 879` ``` hence "\\a\insert a A. \f a\\ = \\f a\ + (\a\A. \f a\)\" by simp ``` nipkow@15539 ` 880` ``` also have "\ = \\f a\ + \\a\A. \f a\\\" using insert by simp ``` avigad@16775 ` 881` ``` also have "\ = \f a\ + \\a\A. \f a\\" ``` avigad@16775 ` 882` ``` by (simp del: abs_of_nonneg) ``` nipkow@15539 ` 883` ``` also have "\ = (\a\insert a A. \f a\)" using insert by simp ``` nipkow@15539 ` 884` ``` finally show ?case . ``` nipkow@15539 ` 885` ``` qed ``` nipkow@15539 ` 886` ```next ``` haftmann@51489 ` 887` ``` case False thus ?thesis by simp ``` nipkow@31080 ` 888` ```qed ``` nipkow@31080 ` 889` haftmann@51489 ` 890` ```lemma setsum_diff1'[rule_format]: ``` haftmann@51489 ` 891` ``` "finite A \ a \ A \ (\ x \ A. f x) = f a + (\ x \ (A - {a}). f x)" ``` haftmann@51489 ` 892` ```apply (erule finite_induct[where F=A and P="% A. (a \ A \ (\ x \ A. f x) = f a + (\ x \ (A - {a}). f x))"]) ``` haftmann@51489 ` 893` ```apply (auto simp add: insert_Diff_if add_ac) ``` haftmann@51489 ` 894` ```done ``` ballarin@17149 ` 895` haftmann@51489 ` 896` ```lemma setsum_diff1_ring: assumes "finite A" "a \ A" ``` haftmann@51489 ` 897` ``` shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)" ``` haftmann@51489 ` 898` ```unfolding setsum_diff1'[OF assms] by auto ``` ballarin@17149 ` 899` ballarin@19279 ` 900` ```lemma setsum_product: ``` huffman@22934 ` 901` ``` fixes f :: "'a => ('b::semiring_0)" ``` ballarin@19279 ` 902` ``` shows "setsum f A * setsum g B = (\i\A. \j\B. f i * g j)" ``` ballarin@19279 ` 903` ``` by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute) ``` ballarin@19279 ` 904` nipkow@34223 ` 905` ```lemma setsum_mult_setsum_if_inj: ``` nipkow@34223 ` 906` ```fixes f :: "'a => ('b::semiring_0)" ``` nipkow@34223 ` 907` ```shows "inj_on (%(a,b). f a * g b) (A \ B) ==> ``` nipkow@34223 ` 908` ``` setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}" ``` nipkow@34223 ` 909` ```by(auto simp: setsum_product setsum_cartesian_product ``` nipkow@34223 ` 910` ``` intro!: setsum_reindex_cong[symmetric]) ``` nipkow@34223 ` 911` haftmann@51489 ` 912` ```lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a" ``` haftmann@51489 ` 913` ```apply (case_tac "finite A") ``` haftmann@51489 ` 914` ``` prefer 2 apply simp ``` haftmann@51489 ` 915` ```apply (erule rev_mp) ``` haftmann@51489 ` 916` ```apply (erule finite_induct, auto) ``` haftmann@51489 ` 917` ```done ``` haftmann@51489 ` 918` haftmann@51489 ` 919` ```lemma setsum_eq_0_iff [simp]: ``` haftmann@51489 ` 920` ``` "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))" ``` haftmann@51489 ` 921` ``` by (induct set: finite) auto ``` haftmann@51489 ` 922` haftmann@51489 ` 923` ```lemma setsum_eq_Suc0_iff: "finite A \ ``` haftmann@51489 ` 924` ``` setsum f A = Suc 0 \ (EX a:A. f a = Suc 0 & (ALL b:A. a\b \ f b = 0))" ``` haftmann@51489 ` 925` ```apply(erule finite_induct) ``` haftmann@51489 ` 926` ```apply (auto simp add:add_is_1) ``` haftmann@51489 ` 927` ```done ``` haftmann@51489 ` 928` haftmann@51489 ` 929` ```lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]] ``` haftmann@51489 ` 930` haftmann@51489 ` 931` ```lemma setsum_Un_nat: "finite A ==> finite B ==> ``` haftmann@51489 ` 932` ``` (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)" ``` haftmann@51489 ` 933` ``` -- {* For the natural numbers, we have subtraction. *} ``` haftmann@51489 ` 934` ```by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps) ``` haftmann@51489 ` 935` haftmann@51489 ` 936` ```lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) = ``` haftmann@51489 ` 937` ``` (if a:A then setsum f A - f a else setsum f A)" ``` haftmann@51489 ` 938` ```apply (case_tac "finite A") ``` haftmann@51489 ` 939` ``` prefer 2 apply simp ``` haftmann@51489 ` 940` ```apply (erule finite_induct) ``` haftmann@51489 ` 941` ``` apply (auto simp add: insert_Diff_if) ``` haftmann@51489 ` 942` ```apply (drule_tac a = a in mk_disjoint_insert, auto) ``` haftmann@51489 ` 943` ```done ``` haftmann@51489 ` 944` haftmann@51489 ` 945` ```lemma setsum_diff_nat: ``` haftmann@51489 ` 946` ```assumes "finite B" and "B \ A" ``` haftmann@51489 ` 947` ```shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)" ``` haftmann@51489 ` 948` ```using assms ``` haftmann@51489 ` 949` ```proof induct ``` haftmann@51489 ` 950` ``` show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp ``` haftmann@51489 ` 951` ```next ``` haftmann@51489 ` 952` ``` fix F x assume finF: "finite F" and xnotinF: "x \ F" ``` haftmann@51489 ` 953` ``` and xFinA: "insert x F \ A" ``` haftmann@51489 ` 954` ``` and IH: "F \ A \ setsum f (A - F) = setsum f A - setsum f F" ``` haftmann@51489 ` 955` ``` from xnotinF xFinA have xinAF: "x \ (A - F)" by simp ``` haftmann@51489 ` 956` ``` from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x" ``` haftmann@51489 ` 957` ``` by (simp add: setsum_diff1_nat) ``` haftmann@51489 ` 958` ``` from xFinA have "F \ A" by simp ``` haftmann@51489 ` 959` ``` with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp ``` haftmann@51489 ` 960` ``` with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x" ``` haftmann@51489 ` 961` ``` by simp ``` haftmann@51489 ` 962` ``` from xnotinF have "A - insert x F = (A - F) - {x}" by auto ``` haftmann@51489 ` 963` ``` with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x" ``` haftmann@51489 ` 964` ``` by simp ``` haftmann@51489 ` 965` ``` from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp ``` haftmann@51489 ` 966` ``` with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" ``` haftmann@51489 ` 967` ``` by simp ``` haftmann@51489 ` 968` ``` thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp ``` haftmann@51489 ` 969` ```qed ``` haftmann@51489 ` 970` haftmann@51489 ` 971` haftmann@51489 ` 972` ```subsubsection {* Cardinality as special case of @{const setsum} *} ``` haftmann@51489 ` 973` haftmann@51489 ` 974` ```lemma card_eq_setsum: ``` haftmann@51489 ` 975` ``` "card A = setsum (\x. 1) A" ``` haftmann@51489 ` 976` ```proof - ``` haftmann@51489 ` 977` ``` have "plus \ (\_. Suc 0) = (\_. Suc)" ``` haftmann@51489 ` 978` ``` by (simp add: fun_eq_iff) ``` haftmann@51489 ` 979` ``` then have "Finite_Set.fold (plus \ (\_. Suc 0)) = Finite_Set.fold (\_. Suc)" ``` haftmann@51489 ` 980` ``` by (rule arg_cong) ``` haftmann@51489 ` 981` ``` then have "Finite_Set.fold (plus \ (\_. Suc 0)) 0 A = Finite_Set.fold (\_. Suc) 0 A" ``` haftmann@51489 ` 982` ``` by (blast intro: fun_cong) ``` haftmann@51489 ` 983` ``` then show ?thesis by (simp add: card.eq_fold setsum.eq_fold) ``` haftmann@51489 ` 984` ```qed ``` haftmann@51489 ` 985` haftmann@51489 ` 986` ```lemma setsum_constant [simp]: ``` haftmann@51489 ` 987` ``` "(\x \ A. y) = of_nat (card A) * y" ``` haftmann@35722 ` 988` ```apply (cases "finite A") ``` haftmann@35722 ` 989` ```apply (erule finite_induct) ``` haftmann@35722 ` 990` ```apply (auto simp add: algebra_simps) ``` haftmann@35722 ` 991` ```done ``` haftmann@35722 ` 992` haftmann@35722 ` 993` ```lemma setsum_bounded: ``` haftmann@35722 ` 994` ``` assumes le: "\i. i\A \ f i \ (K::'a::{semiring_1, ordered_ab_semigroup_add})" ``` haftmann@51489 ` 995` ``` shows "setsum f A \ of_nat (card A) * K" ``` haftmann@35722 ` 996` ```proof (cases "finite A") ``` haftmann@35722 ` 997` ``` case True ``` haftmann@35722 ` 998` ``` thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp ``` haftmann@35722 ` 999` ```next ``` haftmann@51489 ` 1000` ``` case False thus ?thesis by simp ``` haftmann@35722 ` 1001` ```qed ``` haftmann@35722 ` 1002` haftmann@35722 ` 1003` ```lemma card_UN_disjoint: ``` haftmann@46629 ` 1004` ``` assumes "finite I" and "\i\I. finite (A i)" ``` haftmann@46629 ` 1005` ``` and "\i\I. \j\I. i \ j \ A i \ A j = {}" ``` haftmann@46629 ` 1006` ``` shows "card (UNION I A) = (\i\I. card(A i))" ``` haftmann@46629 ` 1007` ```proof - ``` haftmann@46629 ` 1008` ``` have "(\i\I. card (A i)) = (\i\I. \x\A i. 1)" by simp ``` haftmann@46629 ` 1009` ``` with assms show ?thesis by (simp add: card_eq_setsum setsum_UN_disjoint del: setsum_constant) ``` haftmann@46629 ` 1010` ```qed ``` haftmann@35722 ` 1011` haftmann@35722 ` 1012` ```lemma card_Union_disjoint: ``` haftmann@35722 ` 1013` ``` "finite C ==> (ALL A:C. finite A) ==> ``` haftmann@35722 ` 1014` ``` (ALL A:C. ALL B:C. A \ B --> A Int B = {}) ``` haftmann@35722 ` 1015` ``` ==> card (Union C) = setsum card C" ``` haftmann@35722 ` 1016` ```apply (frule card_UN_disjoint [of C id]) ``` hoelzl@44937 ` 1017` ```apply (simp_all add: SUP_def id_def) ``` haftmann@35722 ` 1018` ```done ``` haftmann@35722 ` 1019` haftmann@35722 ` 1020` haftmann@35722 ` 1021` ```subsubsection {* Cardinality of products *} ``` haftmann@35722 ` 1022` haftmann@35722 ` 1023` ```lemma card_SigmaI [simp]: ``` haftmann@35722 ` 1024` ``` "\ finite A; ALL a:A. finite (B a) \ ``` haftmann@35722 ` 1025` ``` \ card (SIGMA x: A. B x) = (\a\A. card (B a))" ``` haftmann@35722 ` 1026` ```by(simp add: card_eq_setsum setsum_Sigma del:setsum_constant) ``` haftmann@35722 ` 1027` haftmann@35722 ` 1028` ```(* ``` haftmann@35722 ` 1029` ```lemma SigmaI_insert: "y \ A ==> ``` haftmann@35722 ` 1030` ``` (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \ (SIGMA x: A. B x))" ``` haftmann@35722 ` 1031` ``` by auto ``` haftmann@35722 ` 1032` ```*) ``` haftmann@35722 ` 1033` haftmann@35722 ` 1034` ```lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)" ``` haftmann@35722 ` 1035` ``` by (cases "finite A \ finite B") ``` haftmann@35722 ` 1036` ``` (auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2) ``` haftmann@35722 ` 1037` haftmann@35722 ` 1038` ```lemma card_cartesian_product_singleton: "card({x} <*> A) = card(A)" ``` haftmann@35722 ` 1039` ```by (simp add: card_cartesian_product) ``` haftmann@35722 ` 1040` ballarin@17149 ` 1041` nipkow@15402 ` 1042` ```subsection {* Generalized product over a set *} ``` nipkow@15402 ` 1043` haftmann@51489 ` 1044` ```definition (in comm_monoid_mult) setprod :: "('b \ 'a) \ 'b set \ 'a" ``` haftmann@51489 ` 1045` ```where ``` haftmann@51489 ` 1046` ``` "setprod = comm_monoid_set.F times 1" ``` haftmann@35816 ` 1047` haftmann@51489 ` 1048` ```sublocale comm_monoid_mult < setprod!: comm_monoid_set times 1 ``` haftmann@51489 ` 1049` ```where ``` haftmann@51546 ` 1050` ``` "comm_monoid_set.F times 1 = setprod" ``` haftmann@51489 ` 1051` ```proof - ``` haftmann@51489 ` 1052` ``` show "comm_monoid_set times 1" .. ``` haftmann@51489 ` 1053` ``` then interpret setprod!: comm_monoid_set times 1 . ``` haftmann@51546 ` 1054` ``` from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule ``` haftmann@51489 ` 1055` ```qed ``` nipkow@15402 ` 1056` wenzelm@19535 ` 1057` ```abbreviation ``` haftmann@51489 ` 1058` ``` Setprod ("\_" [1000] 999) where ``` haftmann@51489 ` 1059` ``` "\A \ setprod (\x. x) A" ``` wenzelm@19535 ` 1060` nipkow@15402 ` 1061` ```syntax ``` paulson@17189 ` 1062` ``` "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3PROD _:_. _)" [0, 51, 10] 10) ``` nipkow@15402 ` 1063` ```syntax (xsymbols) ``` paulson@17189 ` 1064` ``` "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3\_\_. _)" [0, 51, 10] 10) ``` nipkow@15402 ` 1065` ```syntax (HTML output) ``` paulson@17189 ` 1066` ``` "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3\_\_. _)" [0, 51, 10] 10) ``` nipkow@16550 ` 1067` nipkow@16550 ` 1068` ```translations -- {* Beware of argument permutation! *} ``` nipkow@28853 ` 1069` ``` "PROD i:A. b" == "CONST setprod (%i. b) A" ``` nipkow@28853 ` 1070` ``` "\i\A. b" == "CONST setprod (%i. b) A" ``` nipkow@16550 ` 1071` nipkow@16550 ` 1072` ```text{* Instead of @{term"\x\{x. P}. e"} we introduce the shorter ``` nipkow@16550 ` 1073` ``` @{text"\x|P. e"}. *} ``` nipkow@16550 ` 1074` nipkow@16550 ` 1075` ```syntax ``` paulson@17189 ` 1076` ``` "_qsetprod" :: "pttrn \ bool \ 'a \ 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10) ``` nipkow@16550 ` 1077` ```syntax (xsymbols) ``` paulson@17189 ` 1078` ``` "_qsetprod" :: "pttrn \ bool \ 'a \ 'a" ("(3\_ | (_)./ _)" [0,0,10] 10) ``` nipkow@16550 ` 1079` ```syntax (HTML output) ``` paulson@17189 ` 1080` ``` "_qsetprod" :: "pttrn \ bool \ 'a \ 'a" ("(3\_ | (_)./ _)" [0,0,10] 10) ``` nipkow@16550 ` 1081` nipkow@15402 ` 1082` ```translations ``` nipkow@28853 ` 1083` ``` "PROD x|P. t" => "CONST setprod (%x. t) {x. P}" ``` nipkow@28853 ` 1084` ``` "\x|P. t" => "CONST setprod (%x. t) {x. P}" ``` nipkow@16550 ` 1085` haftmann@51489 ` 1086` ```text {* TODO These are candidates for generalization *} ``` haftmann@51489 ` 1087` haftmann@51489 ` 1088` ```context comm_monoid_mult ``` haftmann@51489 ` 1089` ```begin ``` haftmann@51489 ` 1090` haftmann@51489 ` 1091` ```lemma setprod_reindex_id: ``` haftmann@51489 ` 1092` ``` "inj_on f B ==> setprod f B = setprod id (f ` B)" ``` haftmann@51489 ` 1093` ``` by (auto simp add: setprod.reindex) ``` haftmann@51489 ` 1094` haftmann@51489 ` 1095` ```lemma setprod_reindex_cong: ``` haftmann@51489 ` 1096` ``` "inj_on f A ==> B = f ` A ==> g = h \ f ==> setprod h B = setprod g A" ``` haftmann@51489 ` 1097` ``` by (frule setprod.reindex, simp) ``` haftmann@51489 ` 1098` haftmann@51489 ` 1099` ```lemma strong_setprod_reindex_cong: ``` haftmann@51489 ` 1100` ``` assumes i: "inj_on f A" ``` haftmann@51489 ` 1101` ``` and B: "B = f ` A" and eq: "\x. x \ A \ g x = (h \ f) x" ``` haftmann@51489 ` 1102` ``` shows "setprod h B = setprod g A" ``` haftmann@51489 ` 1103` ```proof- ``` haftmann@51489 ` 1104` ``` have "setprod h B = setprod (h o f) A" ``` haftmann@51489 ` 1105` ``` by (simp add: B setprod.reindex [OF i, of h]) ``` haftmann@51489 ` 1106` ``` then show ?thesis apply simp ``` haftmann@51489 ` 1107` ``` apply (rule setprod.cong) ``` haftmann@51489 ` 1108` ``` apply simp ``` haftmann@51489 ` 1109` ``` by (simp add: eq) ``` haftmann@51489 ` 1110` ```qed ``` haftmann@51489 ` 1111` haftmann@51489 ` 1112` ```lemma setprod_Union_disjoint: ``` haftmann@51489 ` 1113` ``` assumes "\A\C. finite A" "\A\C. \B\C. A \ B \ A Int B = {}" ``` haftmann@51489 ` 1114` ``` shows "setprod f (Union C) = setprod (setprod f) C" ``` haftmann@51489 ` 1115` ``` using assms by (fact setprod.Union_disjoint) ``` haftmann@51489 ` 1116` haftmann@51489 ` 1117` ```text{*Here we can eliminate the finiteness assumptions, by cases.*} ``` haftmann@51489 ` 1118` ```lemma setprod_cartesian_product: ``` haftmann@51489 ` 1119` ``` "(\x\A. (\y\ B. f x y)) = (\(x,y)\(A <*> B). f x y)" ``` haftmann@51489 ` 1120` ``` by (fact setprod.cartesian_product) ``` haftmann@51489 ` 1121` haftmann@51489 ` 1122` ```lemma setprod_Un2: ``` haftmann@51489 ` 1123` ``` assumes "finite (A \ B)" ``` haftmann@51489 ` 1124` ``` shows "setprod f (A \ B) = setprod f (A - B) * setprod f (B - A) * setprod f (A \ B)" ``` haftmann@51489 ` 1125` ```proof - ``` haftmann@51489 ` 1126` ``` have "A \ B = A - B \ (B - A) \ A \ B" ``` haftmann@51489 ` 1127` ``` by auto ``` haftmann@51489 ` 1128` ``` with assms show ?thesis by simp (subst setprod.union_disjoint, auto)+ ``` haftmann@51489 ` 1129` ```qed ``` haftmann@51489 ` 1130` haftmann@51489 ` 1131` ```end ``` haftmann@51489 ` 1132` haftmann@51489 ` 1133` ```text {* TODO These are legacy *} ``` haftmann@51489 ` 1134` haftmann@35816 ` 1135` ```lemma setprod_empty: "setprod f {} = 1" ``` haftmann@35816 ` 1136` ``` by (fact setprod.empty) ``` nipkow@15402 ` 1137` haftmann@35816 ` 1138` ```lemma setprod_insert: "[| finite A; a \ A |] ==> ``` nipkow@15402 ` 1139` ``` setprod f (insert a A) = f a * setprod f A" ``` haftmann@35816 ` 1140` ``` by (fact setprod.insert) ``` nipkow@15402 ` 1141` haftmann@35816 ` 1142` ```lemma setprod_infinite: "~ finite A ==> setprod f A = 1" ``` haftmann@35816 ` 1143` ``` by (fact setprod.infinite) ``` paulson@15409 ` 1144` nipkow@15402 ` 1145` ```lemma setprod_reindex: ``` haftmann@51489 ` 1146` ``` "inj_on f B ==> setprod h (f ` B) = setprod (h \ f) B" ``` haftmann@51489 ` 1147` ``` by (fact setprod.reindex) ``` nipkow@15402 ` 1148` nipkow@15402 ` 1149` ```lemma setprod_cong: ``` nipkow@15402 ` 1150` ``` "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B" ``` haftmann@51489 ` 1151` ``` by (fact setprod.cong) ``` nipkow@15402 ` 1152` nipkow@48849 ` 1153` ```lemma strong_setprod_cong: ``` berghofe@16632 ` 1154` ``` "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B" ``` haftmann@51489 ` 1155` ``` by (fact setprod.strong_cong) ``` nipkow@15402 ` 1156` haftmann@51489 ` 1157` ```lemma setprod_Un_one: ``` haftmann@51489 ` 1158` ``` "\ finite S; finite T; \x \ S\T. f x = 1 \ ``` haftmann@51489 ` 1159` ``` \ setprod f (S \ T) = setprod f S * setprod f T" ``` haftmann@51489 ` 1160` ``` by (fact setprod.union_inter_neutral) ``` chaieb@29674 ` 1161` haftmann@51489 ` 1162` ```lemmas setprod_1 = setprod.neutral_const ``` haftmann@51489 ` 1163` ```lemmas setprod_1' = setprod.neutral ``` nipkow@15402 ` 1164` nipkow@15402 ` 1165` ```lemma setprod_Un_Int: "finite A ==> finite B ``` nipkow@15402 ` 1166` ``` ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B" ``` haftmann@51489 ` 1167` ``` by (fact setprod.union_inter) ``` nipkow@15402 ` 1168` nipkow@15402 ` 1169` ```lemma setprod_Un_disjoint: "finite A ==> finite B ``` nipkow@15402 ` 1170` ``` ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B" ``` haftmann@51489 ` 1171` ``` by (fact setprod.union_disjoint) ``` nipkow@48849 ` 1172` nipkow@48849 ` 1173` ```lemma setprod_subset_diff: "\ B \ A; finite A \ \ ``` nipkow@48849 ` 1174` ``` setprod f A = setprod f (A - B) * setprod f B" ``` haftmann@51489 ` 1175` ``` by (fact setprod.subset_diff) ``` nipkow@15402 ` 1176` nipkow@48849 ` 1177` ```lemma setprod_mono_one_left: ``` nipkow@48849 ` 1178` ``` "\ finite T; S \ T; \i \ T - S. f i = 1 \ \ setprod f S = setprod f T" ``` haftmann@51489 ` 1179` ``` by (fact setprod.mono_neutral_left) ``` nipkow@30837 ` 1180` haftmann@51489 ` 1181` ```lemmas setprod_mono_one_right = setprod.mono_neutral_right ``` nipkow@30837 ` 1182` nipkow@48849 ` 1183` ```lemma setprod_mono_one_cong_left: ``` nipkow@48849 ` 1184` ``` "\ finite T; S \ T; \i \ T - S. g i = 1; \x. x \ S \ f x = g x \ ``` nipkow@48849 ` 1185` ``` \ setprod f S = setprod g T" ``` haftmann@51489 ` 1186` ``` by (fact setprod.mono_neutral_cong_left) ``` nipkow@48849 ` 1187` haftmann@51489 ` 1188` ```lemmas setprod_mono_one_cong_right = setprod.mono_neutral_cong_right ``` chaieb@29674 ` 1189` nipkow@48849 ` 1190` ```lemma setprod_delta: "finite S \ ``` nipkow@48849 ` 1191` ``` setprod (\k. if k=a then b k else 1) S = (if a \ S then b a else 1)" ``` haftmann@51489 ` 1192` ``` by (fact setprod.delta) ``` chaieb@29674 ` 1193` nipkow@48849 ` 1194` ```lemma setprod_delta': "finite S \ ``` nipkow@48849 ` 1195` ``` setprod (\k. if a = k then b k else 1) S = (if a\ S then b a else 1)" ``` haftmann@51489 ` 1196` ``` by (fact setprod.delta') ``` chaieb@29674 ` 1197` nipkow@15402 ` 1198` ```lemma setprod_UN_disjoint: ``` nipkow@15402 ` 1199` ``` "finite I ==> (ALL i:I. finite (A i)) ==> ``` nipkow@15402 ` 1200` ``` (ALL i:I. ALL j:I. i \ j --> A i Int A j = {}) ==> ``` nipkow@15402 ` 1201` ``` setprod f (UNION I A) = setprod (%i. setprod f (A i)) I" ``` haftmann@51489 ` 1202` ``` by (fact setprod.UNION_disjoint) ``` nipkow@15402 ` 1203` nipkow@15402 ` 1204` ```lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==> ``` nipkow@16550 ` 1205` ``` (\x\A. (\y\ B x. f x y)) = ``` paulson@17189 ` 1206` ``` (\(x,y)\(SIGMA x:A. B x). f x y)" ``` haftmann@51489 ` 1207` ``` by (fact setprod.Sigma) ``` nipkow@15402 ` 1208` haftmann@51489 ` 1209` ```lemma setprod_timesf: "setprod (\x. f x * g x) A = setprod f A * setprod g A" ``` haftmann@51489 ` 1210` ``` by (fact setprod.distrib) ``` nipkow@15402 ` 1211` nipkow@15402 ` 1212` nipkow@15402 ` 1213` ```subsubsection {* Properties in more restricted classes of structures *} ``` nipkow@15402 ` 1214` nipkow@15402 ` 1215` ```lemma setprod_zero: ``` huffman@23277 ` 1216` ``` "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0" ``` nipkow@28853 ` 1217` ```apply (induct set: finite, force, clarsimp) ``` nipkow@28853 ` 1218` ```apply (erule disjE, auto) ``` nipkow@28853 ` 1219` ```done ``` nipkow@15402 ` 1220` haftmann@51489 ` 1221` ```lemma setprod_zero_iff[simp]: "finite A ==> ``` haftmann@51489 ` 1222` ``` (setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) = ``` haftmann@51489 ` 1223` ``` (EX x: A. f x = 0)" ``` haftmann@51489 ` 1224` ```by (erule finite_induct, auto simp:no_zero_divisors) ``` haftmann@51489 ` 1225` haftmann@51489 ` 1226` ```lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \ 0) ==> ``` haftmann@51489 ` 1227` ``` (setprod f (A Un B) :: 'a ::{field}) ``` haftmann@51489 ` 1228` ``` = setprod f A * setprod f B / setprod f (A Int B)" ``` haftmann@51489 ` 1229` ```by (subst setprod_Un_Int [symmetric], auto) ``` haftmann@51489 ` 1230` nipkow@15402 ` 1231` ```lemma setprod_nonneg [rule_format]: ``` haftmann@35028 ` 1232` ``` "(ALL x: A. (0::'a::linordered_semidom) \ f x) --> 0 \ setprod f A" ``` huffman@30841 ` 1233` ```by (cases "finite A", induct set: finite, simp_all add: mult_nonneg_nonneg) ``` huffman@30841 ` 1234` haftmann@35028 ` 1235` ```lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x) ``` nipkow@28853 ` 1236` ``` --> 0 < setprod f A" ``` huffman@30841 ` 1237` ```by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos) ``` nipkow@15402 ` 1238` nipkow@15402 ` 1239` ```lemma setprod_diff1: "finite A ==> f a \ 0 ==> ``` nipkow@28853 ` 1240` ``` (setprod f (A - {a}) :: 'a :: {field}) = ``` nipkow@28853 ` 1241` ``` (if a:A then setprod f A / f a else setprod f A)" ``` haftmann@36303 ` 1242` ``` by (erule finite_induct) (auto simp add: insert_Diff_if) ``` nipkow@15402 ` 1243` paulson@31906 ` 1244` ```lemma setprod_inversef: ``` haftmann@36409 ` 1245` ``` fixes f :: "'b \ 'a::field_inverse_zero" ``` paulson@31906 ` 1246` ``` shows "finite A ==> setprod (inverse \ f) A = inverse (setprod f A)" ``` nipkow@28853 ` 1247` ```by (erule finite_induct) auto ``` nipkow@15402 ` 1248` nipkow@15402 ` 1249` ```lemma setprod_dividef: ``` haftmann@36409 ` 1250` ``` fixes f :: "'b \ 'a::field_inverse_zero" ``` wenzelm@31916 ` 1251` ``` shows "finite A ``` nipkow@28853 ` 1252` ``` ==> setprod (%x. f x / g x) A = setprod f A / setprod g A" ``` nipkow@28853 ` 1253` ```apply (subgoal_tac ``` nipkow@15402 ` 1254` ``` "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \ g) x) A") ``` nipkow@28853 ` 1255` ```apply (erule ssubst) ``` nipkow@28853 ` 1256` ```apply (subst divide_inverse) ``` nipkow@28853 ` 1257` ```apply (subst setprod_timesf) ``` nipkow@28853 ` 1258` ```apply (subst setprod_inversef, assumption+, rule refl) ``` nipkow@28853 ` 1259` ```apply (rule setprod_cong, rule refl) ``` nipkow@28853 ` 1260` ```apply (subst divide_inverse, auto) ``` nipkow@28853 ` 1261` ```done ``` nipkow@28853 ` 1262` nipkow@29925 ` 1263` ```lemma setprod_dvd_setprod [rule_format]: ``` nipkow@29925 ` 1264` ``` "(ALL x : A. f x dvd g x) \ setprod f A dvd setprod g A" ``` nipkow@29925 ` 1265` ``` apply (cases "finite A") ``` nipkow@29925 ` 1266` ``` apply (induct set: finite) ``` nipkow@29925 ` 1267` ``` apply (auto simp add: dvd_def) ``` nipkow@29925 ` 1268` ``` apply (rule_tac x = "k * ka" in exI) ``` nipkow@29925 ` 1269` ``` apply (simp add: algebra_simps) ``` nipkow@29925 ` 1270` ```done ``` nipkow@29925 ` 1271` nipkow@29925 ` 1272` ```lemma setprod_dvd_setprod_subset: ``` nipkow@29925 ` 1273` ``` "finite B \ A <= B \ setprod f A dvd setprod f B" ``` nipkow@29925 ` 1274` ``` apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)") ``` nipkow@29925 ` 1275` ``` apply (unfold dvd_def, blast) ``` nipkow@29925 ` 1276` ``` apply (subst setprod_Un_disjoint [symmetric]) ``` nipkow@29925 ` 1277` ``` apply (auto elim: finite_subset intro: setprod_cong) ``` nipkow@29925 ` 1278` ```done ``` nipkow@29925 ` 1279` nipkow@29925 ` 1280` ```lemma setprod_dvd_setprod_subset2: ``` nipkow@29925 ` 1281` ``` "finite B \ A <= B \ ALL x : A. (f x::'a::comm_semiring_1) dvd g x \ ``` nipkow@29925 ` 1282` ``` setprod f A dvd setprod g B" ``` nipkow@29925 ` 1283` ``` apply (rule dvd_trans) ``` nipkow@29925 ` 1284` ``` apply (rule setprod_dvd_setprod, erule (1) bspec) ``` nipkow@29925 ` 1285` ``` apply (erule (1) setprod_dvd_setprod_subset) ``` nipkow@29925 ` 1286` ```done ``` nipkow@29925 ` 1287` nipkow@29925 ` 1288` ```lemma dvd_setprod: "finite A \ i:A \ ``` nipkow@29925 ` 1289` ``` (f i ::'a::comm_semiring_1) dvd setprod f A" ``` nipkow@29925 ` 1290` ```by (induct set: finite) (auto intro: dvd_mult) ``` nipkow@29925 ` 1291` nipkow@29925 ` 1292` ```lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \ ``` nipkow@29925 ` 1293` ``` (d::'a::comm_semiring_1) dvd (SUM x : A. f x)" ``` nipkow@29925 ` 1294` ``` apply (cases "finite A") ``` nipkow@29925 ` 1295` ``` apply (induct set: finite) ``` nipkow@29925 ` 1296` ``` apply auto ``` nipkow@29925 ` 1297` ```done ``` nipkow@29925 ` 1298` hoelzl@35171 ` 1299` ```lemma setprod_mono: ``` hoelzl@35171 ` 1300` ``` fixes f :: "'a \ 'b\linordered_semidom" ``` hoelzl@35171 ` 1301` ``` assumes "\i\A. 0 \ f i \ f i \ g i" ``` hoelzl@35171 ` 1302` ``` shows "setprod f A \ setprod g A" ``` hoelzl@35171 ` 1303` ```proof (cases "finite A") ``` hoelzl@35171 ` 1304` ``` case True ``` hoelzl@35171 ` 1305` ``` hence ?thesis "setprod f A \ 0" using subset_refl[of A] ``` hoelzl@35171 ` 1306` ``` proof (induct A rule: finite_subset_induct) ``` hoelzl@35171 ` 1307` ``` case (insert a F) ``` hoelzl@35171 ` 1308` ``` thus "setprod f (insert a F) \ setprod g (insert a F)" "0 \ setprod f (insert a F)" ``` hoelzl@35171 ` 1309` ``` unfolding setprod_insert[OF insert(1,3)] ``` hoelzl@35171 ` 1310` ``` using assms[rule_format,OF insert(2)] insert ``` hoelzl@35171 ` 1311` ``` by (auto intro: mult_mono mult_nonneg_nonneg) ``` hoelzl@35171 ` 1312` ``` qed auto ``` hoelzl@35171 ` 1313` ``` thus ?thesis by simp ``` hoelzl@35171 ` 1314` ```qed auto ``` hoelzl@35171 ` 1315` hoelzl@35171 ` 1316` ```lemma abs_setprod: ``` hoelzl@35171 ` 1317` ``` fixes f :: "'a \ 'b\{linordered_field,abs}" ``` hoelzl@35171 ` 1318` ``` shows "abs (setprod f A) = setprod (\x. abs (f x)) A" ``` hoelzl@35171 ` 1319` ```proof (cases "finite A") ``` hoelzl@35171 ` 1320` ``` case True thus ?thesis ``` huffman@35216 ` 1321` ``` by induct (auto simp add: field_simps abs_mult) ``` hoelzl@35171 ` 1322` ```qed auto ``` hoelzl@35171 ` 1323` haftmann@31017 ` 1324` ```lemma setprod_constant: "finite A ==> (\x\ A. (y::'a::{comm_monoid_mult})) = y^(card A)" ``` nipkow@28853 ` 1325` ```apply (erule finite_induct) ``` huffman@35216 ` 1326` ```apply auto ``` nipkow@28853 ` 1327` ```done ``` nipkow@15402 ` 1328` chaieb@29674 ` 1329` ```lemma setprod_gen_delta: ``` chaieb@29674 ` 1330` ``` assumes fS: "finite S" ``` haftmann@51489 ` 1331` ``` shows "setprod (\k. if k=a then b k else c) S = (if a \ S then (b a ::'a::comm_monoid_mult) * c^ (card S - 1) else c^ card S)" ``` chaieb@29674 ` 1332` ```proof- ``` chaieb@29674 ` 1333` ``` let ?f = "(\k. if k=a then b k else c)" ``` chaieb@29674 ` 1334` ``` {assume a: "a \ S" ``` chaieb@29674 ` 1335` ``` hence "\ k\ S. ?f k = c" by simp ``` nipkow@48849 ` 1336` ``` hence ?thesis using a setprod_constant[OF fS, of c] by simp } ``` chaieb@29674 ` 1337` ``` moreover ``` chaieb@29674 ` 1338` ``` {assume a: "a \ S" ``` chaieb@29674 ` 1339` ``` let ?A = "S - {a}" ``` chaieb@29674 ` 1340` ``` let ?B = "{a}" ``` chaieb@29674 ` 1341` ``` have eq: "S = ?A \ ?B" using a by blast ``` chaieb@29674 ` 1342` ``` have dj: "?A \ ?B = {}" by simp ``` chaieb@29674 ` 1343` ``` from fS have fAB: "finite ?A" "finite ?B" by auto ``` chaieb@29674 ` 1344` ``` have fA0:"setprod ?f ?A = setprod (\i. c) ?A" ``` chaieb@29674 ` 1345` ``` apply (rule setprod_cong) by auto ``` chaieb@29674 ` 1346` ``` have cA: "card ?A = card S - 1" using fS a by auto ``` chaieb@29674 ` 1347` ``` have fA1: "setprod ?f ?A = c ^ card ?A" unfolding fA0 apply (rule setprod_constant) using fS by auto ``` chaieb@29674 ` 1348` ``` have "setprod ?f ?A * setprod ?f ?B = setprod ?f S" ``` chaieb@29674 ` 1349` ``` using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] ``` chaieb@29674 ` 1350` ``` by simp ``` chaieb@29674 ` 1351` ``` then have ?thesis using a cA ``` haftmann@36349 ` 1352` ``` by (simp add: fA1 field_simps cong add: setprod_cong cong del: if_weak_cong)} ``` chaieb@29674 ` 1353` ``` ultimately show ?thesis by blast ``` chaieb@29674 ` 1354` ```qed ``` chaieb@29674 ` 1355` haftmann@51489 ` 1356` ```lemma setprod_eq_1_iff [simp]: ``` haftmann@51489 ` 1357` ``` "finite F ==> setprod f F = 1 \ (ALL a:F. f a = (1::nat))" ``` haftmann@51489 ` 1358` ``` by (induct set: finite) auto ``` chaieb@29674 ` 1359` haftmann@51489 ` 1360` ```lemma setprod_pos_nat: ``` haftmann@51489 ` 1361` ``` "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0" ``` haftmann@51489 ` 1362` ```using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric]) ``` haftmann@51489 ` 1363` haftmann@51489 ` 1364` ```lemma setprod_pos_nat_iff[simp]: ``` haftmann@51489 ` 1365` ``` "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))" ``` haftmann@51489 ` 1366` ```using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric]) ``` haftmann@51489 ` 1367` haftmann@51489 ` 1368` haftmann@51489 ` 1369` ```subsection {* Generic lattice operations over a set *} ``` haftmann@35816 ` 1370` haftmann@35816 ` 1371` ```no_notation times (infixl "*" 70) ``` haftmann@35816 ` 1372` ```no_notation Groups.one ("1") ``` haftmann@35816 ` 1373` haftmann@51489 ` 1374` haftmann@51489 ` 1375` ```subsubsection {* Without neutral element *} ``` haftmann@51489 ` 1376` haftmann@51489 ` 1377` ```locale semilattice_set = semilattice ``` haftmann@51489 ` 1378` ```begin ``` haftmann@51489 ` 1379` haftmann@51489 ` 1380` ```definition F :: "'a set \ 'a" ``` haftmann@51489 ` 1381` ```where ``` haftmann@51489 ` 1382` ``` eq_fold': "F A = the (Finite_Set.fold (\x y. Some (case y of None \ x | Some z \ f x z)) None A)" ``` haftmann@51489 ` 1383` haftmann@51489 ` 1384` ```lemma eq_fold: ``` haftmann@51489 ` 1385` ``` assumes "finite A" ``` haftmann@51489 ` 1386` ``` shows "F (insert x A) = Finite_Set.fold f x A" ``` haftmann@51489 ` 1387` ```proof (rule sym) ``` haftmann@51489 ` 1388` ``` let ?f = "\x y. Some (case y of None \ x | Some z \ f x z)" ``` haftmann@51489 ` 1389` ``` interpret comp_fun_idem f ``` haftmann@51489 ` 1390` ``` by default (simp_all add: fun_eq_iff left_commute) ``` haftmann@51489 ` 1391` ``` interpret comp_fun_idem "?f" ``` haftmann@51489 ` 1392` ``` by default (simp_all add: fun_eq_iff commute left_commute split: option.split) ``` haftmann@51489 ` 1393` ``` from assms show "Finite_Set.fold f x A = F (insert x A)" ``` haftmann@51489 ` 1394` ``` proof induct ``` haftmann@51489 ` 1395` ``` case empty then show ?case by (simp add: eq_fold') ``` haftmann@51489 ` 1396` ``` next ``` haftmann@51489 ` 1397` ``` case (insert y B) then show ?case by (simp add: insert_commute [of x] eq_fold') ``` haftmann@51489 ` 1398` ``` qed ``` haftmann@51489 ` 1399` ```qed ``` haftmann@51489 ` 1400` haftmann@51489 ` 1401` ```lemma singleton [simp]: ``` haftmann@51489 ` 1402` ``` "F {x} = x" ``` haftmann@51489 ` 1403` ``` by (simp add: eq_fold) ``` haftmann@51489 ` 1404` haftmann@51489 ` 1405` ```lemma insert_not_elem: ``` haftmann@51489 ` 1406` ``` assumes "finite A" and "x \ A" and "A \ {}" ``` haftmann@51489 ` 1407` ``` shows "F (insert x A) = x * F A" ``` haftmann@51489 ` 1408` ```proof - ``` haftmann@51489 ` 1409` ``` interpret comp_fun_idem f ``` haftmann@51489 ` 1410` ``` by default (simp_all add: fun_eq_iff left_commute) ``` haftmann@51489 ` 1411` ``` from `A \ {}` obtain b where "b \ A" by blast ``` haftmann@51489 ` 1412` ``` then obtain B where *: "A = insert b B" "b \ B" by (blast dest: mk_disjoint_insert) ``` haftmann@51489 ` 1413` ``` with `finite A` and `x \ A` ``` haftmann@51489 ` 1414` ``` have "finite (insert x B)" and "b \ insert x B" by auto ``` haftmann@51489 ` 1415` ``` then have "F (insert b (insert x B)) = x * F (insert b B)" ``` haftmann@51489 ` 1416` ``` by (simp add: eq_fold) ``` haftmann@51489 ` 1417` ``` then show ?thesis by (simp add: * insert_commute) ``` haftmann@51489 ` 1418` ```qed ``` haftmann@51489 ` 1419` haftmann@51489 ` 1420` ```lemma subsumption: ``` haftmann@51489 ` 1421` ``` assumes "finite A" and "x \ A" ``` haftmann@51489 ` 1422` ``` shows "x * F A = F A" ``` haftmann@51489 ` 1423` ```proof - ``` haftmann@51489 ` 1424` ``` from assms have "A \ {}" by auto ``` haftmann@51489 ` 1425` ``` with `finite A` show ?thesis using `x \ A` ``` haftmann@51489 ` 1426` ``` by (induct A rule: finite_ne_induct) (auto simp add: ac_simps insert_not_elem) ``` haftmann@51489 ` 1427` ```qed ``` haftmann@51489 ` 1428` haftmann@51489 ` 1429` ```lemma insert [simp]: ``` haftmann@51489 ` 1430` ``` assumes "finite A" and "A \ {}" ``` haftmann@51489 ` 1431` ``` shows "F (insert x A) = x * F A" ``` haftmann@51489 ` 1432` ``` using assms by (cases "x \ A") (simp_all add: insert_absorb subsumption insert_not_elem) ``` haftmann@51489 ` 1433` haftmann@51489 ` 1434` ```lemma union: ``` haftmann@51489 ` 1435` ``` assumes "finite A" "A \ {}" and "finite B" "B \ {}" ``` haftmann@51489 ` 1436` ``` shows "F (A \ B) = F A * F B" ``` haftmann@51489 ` 1437` ``` using assms by (induct A rule: finite_ne_induct) (simp_all add: ac_simps) ``` haftmann@51489 ` 1438` haftmann@51489 ` 1439` ```lemma remove: ``` haftmann@51489 ` 1440` ``` assumes "finite A" and "x \ A" ``` haftmann@51489 ` 1441` ``` shows "F A = (if A - {x} = {} then x else x * F (A - {x}))" ``` haftmann@51489 ` 1442` ```proof - ``` haftmann@51489 ` 1443` ``` from assms obtain B where "A = insert x B" and "x \ B" by (blast dest: mk_disjoint_insert) ``` haftmann@51489 ` 1444` ``` with assms show ?thesis by simp ``` haftmann@51489 ` 1445` ```qed ``` haftmann@51489 ` 1446` haftmann@51489 ` 1447` ```lemma insert_remove: ``` haftmann@51489 ` 1448` ``` assumes "finite A" ``` haftmann@51489 ` 1449` ``` shows "F (insert x A) = (if A - {x} = {} then x else x * F (A - {x}))" ``` haftmann@51489 ` 1450` ``` using assms by (cases "x \ A") (simp_all add: insert_absorb remove) ``` haftmann@51489 ` 1451` haftmann@51489 ` 1452` ```lemma subset: ``` haftmann@51489 ` 1453` ``` assumes "finite A" "B \ {}" and "B \ A" ``` haftmann@51489 ` 1454` ``` shows "F B * F A = F A" ``` haftmann@51489 ` 1455` ```proof - ``` haftmann@51489 ` 1456` ``` from assms have "A \ {}" and "finite B" by (auto dest: finite_subset) ``` haftmann@51489 ` 1457` ``` with assms show ?thesis by (simp add: union [symmetric] Un_absorb1) ``` haftmann@51489 ` 1458` ```qed ``` haftmann@51489 ` 1459` haftmann@51489 ` 1460` ```lemma closed: ``` haftmann@51489 ` 1461` ``` assumes "finite A" "A \ {}" and elem: "\x y. x * y \ {x, y}" ``` haftmann@51489 ` 1462` ``` shows "F A \ A" ``` haftmann@51489 ` 1463` ```using `finite A` `A \ {}` proof (induct rule: finite_ne_induct) ``` haftmann@51489 ` 1464` ``` case singleton then show ?case by simp ``` haftmann@51489 ` 1465` ```next ``` haftmann@51489 ` 1466` ``` case insert with elem show ?case by force ``` haftmann@51489 ` 1467` ```qed ``` haftmann@51489 ` 1468` haftmann@51489 ` 1469` ```lemma hom_commute: ``` haftmann@51489 ` 1470` ``` assumes hom: "\x y. h (x * y) = h x * h y" ``` haftmann@51489 ` 1471` ``` and N: "finite N" "N \ {}" ``` haftmann@51489 ` 1472` ``` shows "h (F N) = F (h ` N)" ``` haftmann@51489 ` 1473` ```using N proof (induct rule: finite_ne_induct) ``` haftmann@51489 ` 1474` ``` case singleton thus ?case by simp ``` haftmann@51489 ` 1475` ```next ``` haftmann@51489 ` 1476` ``` case (insert n N) ``` haftmann@51489 ` 1477` ``` then have "h (F (insert n N)) = h (n * F N)" by simp ``` haftmann@51489 ` 1478` ``` also have "\ = h n * h (F N)" by (rule hom) ``` haftmann@51489 ` 1479` ``` also have "h (F N) = F (h ` N)" by (rule insert) ``` haftmann@51489 ` 1480` ``` also have "h n * \ = F (insert (h n) (h ` N))" ``` haftmann@51489 ` 1481` ``` using insert by simp ``` haftmann@51489 ` 1482` ``` also have "insert (h n) (h ` N) = h ` insert n N" by simp ``` haftmann@51489 ` 1483` ``` finally show ?case . ``` haftmann@51489 ` 1484` ```qed ``` haftmann@51489 ` 1485` haftmann@51489 ` 1486` ```end ``` haftmann@51489 ` 1487` haftmann@51489 ` 1488` ```locale semilattice_order_set = semilattice_order + semilattice_set ``` haftmann@51489 ` 1489` ```begin ``` haftmann@51489 ` 1490` haftmann@51489 ` 1491` ```lemma bounded_iff: ``` haftmann@51489 ` 1492` ``` assumes "finite A" and "A \ {}" ``` haftmann@51489 ` 1493` ``` shows "x \ F A \ (\a\A. x \ a)" ``` haftmann@51489 ` 1494` ``` using assms by (induct rule: finite_ne_induct) (simp_all add: bounded_iff) ``` haftmann@51489 ` 1495` haftmann@51489 ` 1496` ```lemma boundedI: ``` haftmann@51489 ` 1497` ``` assumes "finite A" ``` haftmann@51489 ` 1498` ``` assumes "A \ {}" ``` haftmann@51489 ` 1499` ``` assumes "\a. a \ A \ x \ a" ``` haftmann@51489 ` 1500` ``` shows "x \ F A" ``` haftmann@51489 ` 1501` ``` using assms by (simp add: bounded_iff) ``` haftmann@51489 ` 1502` haftmann@51489 ` 1503` ```lemma boundedE: ``` haftmann@51489 ` 1504` ``` assumes "finite A" and "A \ {}" and "x \ F A" ``` haftmann@51489 ` 1505` ``` obtains "\a. a \ A \ x \ a" ``` haftmann@51489 ` 1506` ``` using assms by (simp add: bounded_iff) ``` haftmann@35816 ` 1507` haftmann@51489 ` 1508` ```lemma coboundedI: ``` haftmann@51489 ` 1509` ``` assumes "finite A" ``` haftmann@51489 ` 1510` ``` and "a \ A" ``` haftmann@51489 ` 1511` ``` shows "F A \ a" ``` haftmann@51489 ` 1512` ```proof - ``` haftmann@51489 ` 1513` ``` from assms have "A \ {}" by auto ``` haftmann@51489 ` 1514` ``` from `finite A` `A \ {}` `a \ A` show ?thesis ``` haftmann@51489 ` 1515` ``` proof (induct rule: finite_ne_induct) ``` haftmann@51489 ` 1516` ``` case singleton thus ?case by (simp add: refl) ``` haftmann@51489 ` 1517` ``` next ``` haftmann@51489 ` 1518` ``` case (insert x B) ``` haftmann@51489 ` 1519` ``` from insert have "a = x \ a \ B" by simp ``` haftmann@51489 ` 1520` ``` then show ?case using insert by (auto intro: coboundedI2) ``` haftmann@51489 ` 1521` ``` qed ``` haftmann@51489 ` 1522` ```qed ``` haftmann@51489 ` 1523` haftmann@51489 ` 1524` ```lemma antimono: ``` haftmann@51489 ` 1525` ``` assumes "A \ B" and "A \ {}" and "finite B" ``` haftmann@51489 ` 1526` ``` shows "F B \ F A" ``` haftmann@51489 ` 1527` ```proof (cases "A = B") ``` haftmann@51489 ` 1528` ``` case True then show ?thesis by (simp add: refl) ``` haftmann@51489 ` 1529` ```next ``` haftmann@51489 ` 1530` ``` case False ``` haftmann@51489 ` 1531` ``` have B: "B = A \ (B - A)" using `A \ B` by blast ``` haftmann@51489 ` 1532` ``` then have "F B = F (A \ (B - A))" by simp ``` haftmann@51489 ` 1533` ``` also have "\ = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset) ``` haftmann@51489 ` 1534` ``` also have "\ \ F A" by simp ``` haftmann@51489 ` 1535` ``` finally show ?thesis . ``` haftmann@51489 ` 1536` ```qed ``` haftmann@51489 ` 1537` haftmann@51489 ` 1538` ```end ``` haftmann@51489 ` 1539` haftmann@51489 ` 1540` haftmann@51489 ` 1541` ```subsubsection {* With neutral element *} ``` haftmann@51489 ` 1542` haftmann@51489 ` 1543` ```locale semilattice_neutr_set = semilattice_neutr ``` haftmann@51489 ` 1544` ```begin ``` haftmann@51489 ` 1545` haftmann@51489 ` 1546` ```definition F :: "'a set \ 'a" ``` haftmann@51489 ` 1547` ```where ``` haftmann@51489 ` 1548` ``` eq_fold: "F A = Finite_Set.fold f 1 A" ``` haftmann@51489 ` 1549` haftmann@51489 ` 1550` ```lemma infinite [simp]: ``` haftmann@51489 ` 1551` ``` "\ finite A \ F A = 1" ``` haftmann@51489 ` 1552` ``` by (simp add: eq_fold) ``` haftmann@51489 ` 1553` haftmann@51489 ` 1554` ```lemma empty [simp]: ``` haftmann@51489 ` 1555` ``` "F {} = 1" ``` haftmann@51489 ` 1556` ``` by (simp add: eq_fold) ``` haftmann@51489 ` 1557` haftmann@51489 ` 1558` ```lemma insert [simp]: ``` haftmann@51489 ` 1559` ``` assumes "finite A" ``` haftmann@51489 ` 1560` ``` shows "F (insert x A) = x * F A" ``` haftmann@51489 ` 1561` ```proof - ``` haftmann@51489 ` 1562` ``` interpret comp_fun_idem f ``` haftmann@51489 ` 1563` ``` by default (simp_all add: fun_eq_iff left_commute) ``` haftmann@51489 ` 1564` ``` from assms show ?thesis by (simp add: eq_fold) ``` haftmann@51489 ` 1565` ```qed ``` haftmann@51489 ` 1566` haftmann@51489 ` 1567` ```lemma subsumption: ``` haftmann@51489 ` 1568` ``` assumes "finite A" and "x \ A" ``` haftmann@51489 ` 1569` ``` shows "x * F A = F A" ``` haftmann@51489 ` 1570` ```proof - ``` haftmann@51489 ` 1571` ``` from assms have "A \ {}" by auto ``` haftmann@51489 ` 1572` ``` with `finite A` show ?thesis using `x \ A` ``` haftmann@51489 ` 1573` ``` by (induct A rule: finite_ne_induct) (auto simp add: ac_simps) ``` haftmann@51489 ` 1574` ```qed ``` haftmann@51489 ` 1575` haftmann@51489 ` 1576` ```lemma union: ``` haftmann@51489 ` 1577` ``` assumes "finite A" and "finite B" ``` haftmann@51489 ` 1578` ``` shows "F (A \ B) = F A * F B" ``` haftmann@51489 ` 1579` ``` using assms by (induct A) (simp_all add: ac_simps) ``` haftmann@51489 ` 1580` haftmann@51489 ` 1581` ```lemma remove: ``` haftmann@51489 ` 1582` ``` assumes "finite A" and "x \ A" ``` haftmann@51489 ` 1583` ``` shows "F A = x * F (A - {x})" ``` haftmann@51489 ` 1584` ```proof - ``` haftmann@51489 ` 1585` ``` from assms obtain B where "A = insert x B" and "x \ B" by (blast dest: mk_disjoint_insert) ``` haftmann@51489 ` 1586` ``` with assms show ?thesis by simp ``` haftmann@51489 ` 1587` ```qed ``` haftmann@51489 ` 1588` haftmann@51489 ` 1589` ```lemma insert_remove: ``` haftmann@51489 ` 1590` ``` assumes "finite A" ``` haftmann@51489 ` 1591` ``` shows "F (insert x A) = x * F (A - {x})" ``` haftmann@51489 ` 1592` ``` using assms by (cases "x \ A") (simp_all add: insert_absorb remove) ``` haftmann@51489 ` 1593` haftmann@51489 ` 1594` ```lemma subset: ``` haftmann@51489 ` 1595` ``` assumes "finite A" and "B \ A" ``` haftmann@51489 ` 1596` ``` shows "F B * F A = F A" ``` haftmann@51489 ` 1597` ```proof - ``` haftmann@51489 ` 1598` ``` from assms have "finite B" by (auto dest: finite_subset) ``` haftmann@51489 ` 1599` ``` with assms show ?thesis by (simp add: union [symmetric] Un_absorb1) ``` haftmann@51489 ` 1600` ```qed ``` haftmann@51489 ` 1601` haftmann@51489 ` 1602` ```lemma closed: ``` haftmann@51489 ` 1603` ``` assumes "finite A" "A \ {}" and elem: "\x y. x * y \ {x, y}" ``` haftmann@51489 ` 1604` ``` shows "F A \ A" ``` haftmann@51489 ` 1605` ```using `finite A` `A \ {}` proof (induct rule: finite_ne_induct) ``` haftmann@51489 ` 1606` ``` case singleton then show ?case by simp ``` haftmann@51489 ` 1607` ```next ``` haftmann@51489 ` 1608` ``` case insert with elem show ?case by force ``` haftmann@51489 ` 1609` ```qed ``` haftmann@51489 ` 1610` haftmann@51489 ` 1611` ```end ``` haftmann@51489 ` 1612` haftmann@51489 ` 1613` ```locale semilattice_order_neutr_set = semilattice_neutr_order + semilattice_neutr_set ``` haftmann@51489 ` 1614` ```begin ``` haftmann@51489 ` 1615` haftmann@51489 ` 1616` ```lemma bounded_iff: ``` haftmann@51489 ` 1617` ``` assumes "finite A" ``` haftmann@51489 ` 1618` ``` shows "x \ F A \ (\a\A. x \ a)" ``` haftmann@51489 ` 1619` ``` using assms by (induct A) (simp_all add: bounded_iff) ``` haftmann@51489 ` 1620` haftmann@51489 ` 1621` ```lemma boundedI: ``` haftmann@51489 ` 1622` ``` assumes "finite A" ``` haftmann@51489 ` 1623` ``` assumes "\a. a \ A \ x \ a" ``` haftmann@51489 ` 1624` ``` shows "x \ F A" ``` haftmann@51489 ` 1625` ``` using assms by (simp add: bounded_iff) ``` haftmann@51489 ` 1626` haftmann@51489 ` 1627` ```lemma boundedE: ``` haftmann@51489 ` 1628` ``` assumes "finite A" and "x \ F A" ``` haftmann@51489 ` 1629` ``` obtains "\a. a \ A \ x \ a" ``` haftmann@51489 ` 1630` ``` using assms by (simp add: bounded_iff) ``` haftmann@51489 ` 1631` haftmann@51489 ` 1632` ```lemma coboundedI: ``` haftmann@51489 ` 1633` ``` assumes "finite A" ``` haftmann@51489 ` 1634` ``` and "a \ A" ``` haftmann@51489 ` 1635` ``` shows "F A \ a" ``` haftmann@51489 ` 1636` ```proof - ``` haftmann@51489 ` 1637` ``` from assms have "A \ {}" by auto ``` haftmann@51489 ` 1638` ``` from `finite A` `A \ {}` `a \ A` show ?thesis ``` haftmann@51489 ` 1639` ``` proof (induct rule: finite_ne_induct) ``` haftmann@51489 ` 1640` ``` case singleton thus ?case by (simp add: refl) ``` haftmann@51489 ` 1641` ``` next ``` haftmann@51489 ` 1642` ``` case (insert x B) ``` haftmann@51489 ` 1643` ``` from insert have "a = x \ a \ B" by simp ``` haftmann@51489 ` 1644` ``` then show ?case using insert by (auto intro: coboundedI2) ``` haftmann@51489 ` 1645` ``` qed ``` haftmann@51489 ` 1646` ```qed ``` haftmann@51489 ` 1647` haftmann@51489 ` 1648` ```lemma antimono: ``` haftmann@51489 ` 1649` ``` assumes "A \ B" and "finite B" ``` haftmann@51489 ` 1650` ``` shows "F B \ F A" ``` haftmann@51489 ` 1651` ```proof (cases "A = B") ``` haftmann@51489 ` 1652` ``` case True then show ?thesis by (simp add: refl) ``` haftmann@51489 ` 1653` ```next ``` haftmann@51489 ` 1654` ``` case False ``` haftmann@51489 ` 1655` ``` have B: "B = A \ (B - A)" using `A \ B` by blast ``` haftmann@51489 ` 1656` ``` then have "F B = F (A \ (B - A))" by simp ``` haftmann@51489 ` 1657` ``` also have "\ = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset) ``` haftmann@51489 ` 1658` ``` also have "\ \ F A" by simp ``` haftmann@51489 ` 1659` ``` finally show ?thesis . ``` haftmann@51489 ` 1660` ```qed ``` haftmann@51489 ` 1661` haftmann@51489 ` 1662` ```end ``` haftmann@35816 ` 1663` haftmann@35816 ` 1664` ```notation times (infixl "*" 70) ``` haftmann@35816 ` 1665` ```notation Groups.one ("1") ``` haftmann@22917 ` 1666` haftmann@35816 ` 1667` haftmann@51489 ` 1668` ```subsection {* Lattice operations on finite sets *} ``` haftmann@35816 ` 1669` haftmann@51489 ` 1670` ```text {* ``` haftmann@51489 ` 1671` ``` For historic reasons, there is the sublocale dependency from @{class distrib_lattice} ``` haftmann@51489 ` 1672` ``` to @{class linorder}. This is badly designed: both should depend on a common abstract ``` haftmann@51489 ` 1673` ``` distributive lattice rather than having this non-subclass dependecy between two ``` haftmann@51489 ` 1674` ``` classes. But for the moment we have to live with it. This forces us to setup ``` haftmann@51489 ` 1675` ``` this sublocale dependency simultaneously with the lattice operations on finite ``` haftmann@51489 ` 1676` ``` sets, to avoid garbage. ``` haftmann@51489 ` 1677` ```*} ``` haftmann@22917 ` 1678` haftmann@51489 ` 1679` ```definition (in semilattice_inf) Inf_fin :: "'a set \ 'a" ("\\<^bsub>fin\<^esub>_" [900] 900) ``` haftmann@51489 ` 1680` ```where ``` haftmann@51489 ` 1681` ``` "Inf_fin = semilattice_set.F inf" ``` haftmann@26041 ` 1682` haftmann@51489 ` 1683` ```definition (in semilattice_sup) Sup_fin :: "'a set \ 'a" ("\\<^bsub>fin\<^esub>_" [900] 900) ``` haftmann@51489 ` 1684` ```where ``` haftmann@51489 ` 1685` ``` "Sup_fin = semilattice_set.F sup" ``` haftmann@35816 ` 1686` haftmann@51489 ` 1687` ```definition (in linorder) Min :: "'a set \ 'a" ``` haftmann@51489 ` 1688` ```where ``` haftmann@51489 ` 1689` ``` "Min = semilattice_set.F min" ``` haftmann@35816 ` 1690` haftmann@51489 ` 1691` ```definition (in linorder) Max :: "'a set \ 'a" ``` haftmann@51489 ` 1692` ```where ``` haftmann@51489 ` 1693` ``` "Max = semilattice_set.F max" ``` haftmann@51489 ` 1694` haftmann@51540 ` 1695` ```sublocale linorder < Min!: semilattice_order_set min less_eq less ``` haftmann@51540 ` 1696` ``` + Max!: semilattice_order_set max greater_eq greater ``` haftmann@51540 ` 1697` ```where ``` haftmann@51540 ` 1698` ``` "semilattice_set.F min = Min" ``` haftmann@51540 ` 1699` ``` and "semilattice_set.F max = Max" ``` haftmann@51540 ` 1700` ```proof - ``` haftmann@51540 ` 1701` ``` show "semilattice_order_set min less_eq less" by default (auto simp add: min_def) ``` haftmann@51540 ` 1702` ``` then interpret Min!: semilattice_order_set min less_eq less. ``` haftmann@51540 ` 1703` ``` show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def) ``` haftmann@51540 ` 1704` ``` then interpret Max!: semilattice_order_set max greater_eq greater . ``` haftmann@51540 ` 1705` ``` from Min_def show "semilattice_set.F min = Min" by rule ``` haftmann@51540 ` 1706` ``` from Max_def show "semilattice_set.F max = Max" by rule ``` haftmann@51540 ` 1707` ```qed ``` haftmann@51540 ` 1708` haftmann@51540 ` 1709` haftmann@51489 ` 1710` ```text {* An aside: @{const min}/@{const max} on linear orders as special case of @{const inf}/@{const sup} *} ``` haftmann@35816 ` 1711` haftmann@51489 ` 1712` ```sublocale linorder < min_max!: distrib_lattice min less_eq less max ``` haftmann@51489 ` 1713` ```where ``` haftmann@51489 ` 1714` ``` "semilattice_inf.Inf_fin min = Min" ``` haftmann@51489 ` 1715` ``` and "semilattice_sup.Sup_fin max = Max" ``` haftmann@26041 ` 1716` ```proof - ``` haftmann@51489 ` 1717` ``` show "class.distrib_lattice min less_eq less max" ``` haftmann@51489 ` 1718` ``` proof ``` haftmann@51489 ` 1719` ``` fix x y z ``` haftmann@51489 ` 1720` ``` show "max x (min y z) = min (max x y) (max x z)" ``` haftmann@51489 ` 1721` ``` by (auto simp add: min_def max_def) ``` haftmann@51489 ` 1722` ``` qed (auto simp add: min_def max_def not_le less_imp_le) ``` haftmann@51489 ` 1723` ``` then interpret min_max!: distrib_lattice min less_eq less max . ``` haftmann@51489 ` 1724` ``` show "semilattice_inf.Inf_fin min = Min" ``` haftmann@51489 ` 1725` ``` by (simp only: min_max.Inf_fin_def Min_def) ``` haftmann@51489 ` 1726` ``` show "semilattice_sup.Sup_fin max = Max" ``` haftmann@51489 ` 1727` ``` by (simp only: min_max.Sup_fin_def Max_def) ``` haftmann@26041 ` 1728` ```qed ``` haftmann@26041 ` 1729` haftmann@51489 ` 1730` ```lemmas le_maxI1 = min_max.sup_ge1 ``` haftmann@51489 ` 1731` ```lemmas le_maxI2 = min_max.sup_ge2 ``` haftmann@51489 ` 1732` ``` ``` haftmann@51489 ` 1733` ```lemmas min_ac = min_max.inf_assoc min_max.inf_commute ``` haftmann@51540 ` 1734` ``` min.left_commute ``` haftmann@51489 ` 1735` haftmann@51489 ` 1736` ```lemmas max_ac = min_max.sup_assoc min_max.sup_commute ``` haftmann@51540 ` 1737` ``` max.left_commute ``` haftmann@51489 ` 1738` haftmann@51489 ` 1739` haftmann@51489 ` 1740` ```text {* Lattice operations proper *} ``` haftmann@51489 ` 1741` haftmann@51489 ` 1742` ```sublocale semilattice_inf < Inf_fin!: semilattice_order_set inf less_eq less ``` haftmann@51489 ` 1743` ```where ``` haftmann@51546 ` 1744` ``` "semilattice_set.F inf = Inf_fin" ``` haftmann@26757 ` 1745` ```proof - ``` haftmann@51489 ` 1746` ``` show "semilattice_order_set inf less_eq less" .. ``` haftmann@51489 ` 1747` ``` then interpret Inf_fin!: semilattice_order_set inf less_eq less. ``` haftmann@51546 ` 1748` ``` from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule ``` haftmann@26041 ` 1749` ```qed ``` haftmann@26041 ` 1750` haftmann@51489 ` 1751` ```sublocale semilattice_sup < Sup_fin!: semilattice_order_set sup greater_eq greater ``` haftmann@51489 ` 1752` ```where ``` haftmann@51546 ` 1753` ``` "semilattice_set.F sup = Sup_fin" ``` haftmann@51489 ` 1754` ```proof - ``` haftmann@51489 ` 1755` ``` show "semilattice_order_set sup greater_eq greater" .. ``` haftmann@51489 ` 1756` ``` then interpret Sup_fin!: semilattice_order_set sup greater_eq greater . ``` haftmann@51546 ` 1757` ``` from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule ``` haftmann@51489 ` 1758` ```qed ``` haftmann@35816 ` 1759` haftmann@51489 ` 1760` haftmann@51540 ` 1761` ```text {* An aside again: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin} *} ``` haftmann@51540 ` 1762` haftmann@51540 ` 1763` ```lemma Inf_fin_Min: ``` haftmann@51540 ` 1764` ``` "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \ 'a)" ``` haftmann@51540 ` 1765` ``` by (simp add: Inf_fin_def Min_def inf_min) ``` haftmann@51540 ` 1766` haftmann@51540 ` 1767` ```lemma Sup_fin_Max: ``` haftmann@51540 ` 1768` ``` "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \ 'a)" ``` haftmann@51540 ` 1769` ``` by (simp add: Sup_fin_def Max_def sup_max) ``` haftmann@51540 ` 1770` haftmann@51540 ` 1771` haftmann@51540 ` 1772` haftmann@51489 ` 1773` ```subsection {* Infimum and Supremum over non-empty sets *} ``` haftmann@22917 ` 1774` haftmann@51489 ` 1775` ```text {* ``` haftmann@51489 ` 1776` ``` After this non-regular bootstrap, things continue canonically. ``` haftmann@51489 ` 1777` ```*} ``` haftmann@35816 ` 1778` haftmann@35816 ` 1779` ```context lattice ``` haftmann@35816 ` 1780` ```begin ``` haftmann@25062 ` 1781` wenzelm@31916 ` 1782` ```lemma Inf_le_Sup [simp]: "\ finite A; A \ {} \ \ \\<^bsub>fin\<^esub>A \ \\<^bsub>fin\<^esub>A" ``` nipkow@15500 ` 1783` ```apply(subgoal_tac "EX a. a:A") ``` nipkow@15500 ` 1784` ```prefer 2 apply blast ``` nipkow@15500 ` 1785` ```apply(erule exE) ``` haftmann@22388 ` 1786` ```apply(rule order_trans) ``` haftmann@51489 ` 1787` ```apply(erule (1) Inf_fin.coboundedI) ``` haftmann@51489 ` 1788` ```apply(erule (1) Sup_fin.coboundedI) ``` nipkow@15500 ` 1789` ```done ``` nipkow@15500 ` 1790` haftmann@24342 ` 1791` ```lemma sup_Inf_absorb [simp]: ``` wenzelm@31916 ` 1792` ``` "finite A \ a \ A \ sup a (\\<^bsub>fin\<^esub>A) = a" ``` nipkow@15512 ` 1793` ```apply(subst sup_commute) ``` haftmann@51489 ` 1794` ```apply(simp add: sup_absorb2 Inf_fin.coboundedI) ``` nipkow@15504 ` 1795` ```done ``` nipkow@15504 ` 1796` haftmann@24342 ` 1797` ```lemma inf_Sup_absorb [simp]: ``` wenzelm@31916 ` 1798` ``` "finite A \ a \ A \ inf a (\\<^bsub>fin\<^esub>A) = a" ``` haftmann@51489 ` 1799` ```by (simp add: inf_absorb1 Sup_fin.coboundedI) ``` haftmann@24342 ` 1800` haftmann@24342 ` 1801` ```end ``` haftmann@24342 ` 1802` haftmann@24342 ` 1803` ```context distrib_lattice ``` haftmann@24342 ` 1804` ```begin ``` haftmann@24342 ` 1805` haftmann@24342 ` 1806` ```lemma sup_Inf1_distrib: ``` haftmann@26041 ` 1807` ``` assumes "finite A" ``` haftmann@26041 ` 1808` ``` and "A \ {}" ``` wenzelm@31916 ` 1809` ``` shows "sup x (\\<^bsub>fin\<^esub>A) = \\<^bsub>fin\<^esub>{sup x a|a. a \ A}" ``` haftmann@51489 ` 1810` ```using assms by (simp add: image_def Inf_fin.hom_commute [where h="sup x", OF sup_inf_distrib1]) ``` haftmann@51489 ` 1811` ``` (rule arg_cong [where f="Inf_fin"], blast) ``` nipkow@18423 ` 1812` haftmann@24342 ` 1813` ```lemma sup_Inf2_distrib: ``` haftmann@24342 ` 1814` ``` assumes A: "finite A" "A \ {}" and B: "finite B" "B \ {}" ``` wenzelm@31916 ` 1815` ``` shows "sup (\\<^bsub>fin\<^esub>A) (\\<^bsub>fin\<^esub>B) = \\<^bsub>fin\<^esub>{sup a b|a b. a \ A \ b \ B}" ``` haftmann@24342 ` 1816` ```using A proof (induct rule: finite_ne_induct) ``` haftmann@51489 ` 1817` ``` case singleton then show ?case ``` wenzelm@41550 ` 1818` ``` by (simp add: sup_Inf1_distrib [OF B]) ``` nipkow@15500 ` 1819` ```next ``` nipkow@15500 ` 1820` ``` case (insert x A) ``` haftmann@25062 ` 1821` ``` have finB: "finite {sup x b |b. b \ B}" ``` haftmann@51489 ` 1822` ``` by (rule finite_surj [where f = "sup x", OF B(1)], auto) ``` haftmann@25062 ` 1823` ``` have finAB: "finite {sup a b |a b. a \ A \ b \ B}" ``` nipkow@15500 ` 1824` ``` proof - ``` haftmann@25062 ` 1825` ``` have "{sup a b |a b. a \ A \ b \ B} = (UN a:A. UN b:B. {sup a b})" ``` nipkow@15500 ` 1826` ``` by blast ``` berghofe@15517 ` 1827` ``` thus ?thesis by(simp add: insert(1) B(1)) ``` nipkow@15500 ` 1828` ``` qed ``` haftmann@25062 ` 1829` ``` have ne: "{sup a b |a b. a \ A \ b \ B} \ {}" using insert B by blast ``` wenzelm@31916 ` 1830` ``` have "sup (\\<^bsub>fin\<^esub>(insert x A)) (\\<^bsub>fin\<^esub>B) = sup (inf x (\\<^bsub>fin\<^esub>A)) (\\<^bsub>fin\<^esub>B)" ``` wenzelm@41550 ` 1831` ``` using insert by simp ``` wenzelm@31916 ` 1832` ``` also have "\ = inf (sup x (\\<^bsub>fin\<^esub>B)) (sup (\\<^bsub>fin\<^esub>A) (\\<^bsub>fin\<^esub>B))" by(rule sup_inf_distrib2) ``` wenzelm@31916 ` 1833` ``` also have "\ = inf (\\<^bsub>fin\<^esub>{sup x b|b. b \ B}) (\\<^bsub>fin\<^esub>{sup a b|a b. a \ A \ b \ B})" ``` nipkow@15500 ` 1834` ``` using insert by(simp add:sup_Inf1_distrib[OF B]) ``` wenzelm@31916 ` 1835` ``` also have "\ = \\<^bsub>fin\<^esub>({sup x b |b. b \ B} \ {sup a b |a b. a \ A \ b \ B})" ``` wenzelm@31916 ` 1836` ``` (is "_ = \\<^bsub>fin\<^esub>?M") ``` nipkow@15500 ` 1837` ``` using B insert ``` haftmann@51489 ` 1838` ``` by (simp add: Inf_fin.union [OF finB _ finAB ne]) ``` haftmann@25062 ` 1839` ``` also have "?M = {sup a b |a b. a \ insert x A \ b \ B}" ``` nipkow@15500 ` 1840` ``` by blast ``` nipkow@15500 ` 1841` ``` finally show ?case . ``` nipkow@15500 ` 1842` ```qed ``` nipkow@15500 ` 1843` haftmann@24342 ` 1844` ```lemma inf_Sup1_distrib: ``` haftmann@26041 ` 1845` ``` assumes "finite A" and "A \ {}" ``` wenzelm@31916 ` 1846` ``` shows "inf x (\\<^bsub>fin\<^esub>A) = \\<^bsub>fin\<^esub>{inf x a|a. a \ A}" ``` haftmann@51489 ` 1847` ```using assms by (simp add: image_def Sup_fin.hom_commute [where h="inf x", OF inf_sup_distrib1]) ``` haftmann@51489 ` 1848` ``` (rule arg_cong [where f="Sup_fin"], blast) ``` nipkow@18423 ` 1849` haftmann@24342 ` 1850` ```lemma inf_Sup2_distrib: ``` haftmann@24342 ` 1851` ``` assumes A: "finite A" "A \ {}" and B: "finite B" "B \ {}" ``` wenzelm@31916 ` 1852` ``` shows "inf (\\<^bsub>fin\<^esub>A) (\\<^bsub>fin\<^esub>B) = \\<^bsub>fin\<^esub>{inf a b|a b. a \ A \ b \ B}" ``` haftmann@24342 ` 1853` ```using A proof (induct rule: finite_ne_induct) ``` nipkow@18423 ` 1854` ``` case singleton thus ?case ``` huffman@44921 ` 1855` ``` by(simp add: inf_Sup1_distrib [OF B]) ``` nipkow@18423 ` 1856` ```next ``` nipkow@18423 ` 1857` ``` case (insert x A) ``` haftmann@25062 ` 1858` ``` have finB: "finite {inf x b |b. b \ B}" ``` haftmann@25062 ` 1859` ``` by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto) ``` haftmann@25062 ` 1860` ``` have finAB: "finite {inf a b |a b. a \ A \ b \ B}" ``` nipkow@18423 ` 1861` ``` proof - ``` haftmann@25062 ` 1862` ``` have "{inf a b |a b. a \ A \ b \ B} = (UN a:A. UN b:B. {inf a b})" ``` nipkow@18423 ` 1863` ``` by blast ``` nipkow@18423 ` 1864` ``` thus ?thesis by(simp add: insert(1) B(1)) ``` nipkow@18423 ` 1865` ``` qed ``` haftmann@25062 ` 1866` ``` have ne: "{inf a b |a b. a \ A \ b \ B} \ {}" using insert B by blast ``` wenzelm@31916 ` 1867` ``` have "inf (\\<^bsub>fin\<^esub>(insert x A)) (\\<^bsub>fin\<^esub>B) = inf (sup x (\\<^bsub>fin\<^esub>A)) (\\<^bsub>fin\<^esub>B)" ``` wenzelm@41550 ` 1868` ``` using insert by simp ``` wenzelm@31916 ` 1869` ``` also have "\ = sup (inf x (\\<^bsub>fin\<^esub>B)) (inf (\\<^bsub>fin\<^esub>A) (\\<^bsub>fin\<^esub>B))" by(rule inf_sup_distrib2) ``` wenzelm@31916 ` 1870` ``` also have "\ = sup (\\<^bsub>fin\<^esub>{inf x b|b. b \ B}) (\\<^bsub>fin\<^esub>{inf a b|a b. a \ A \ b \ B})" ``` nipkow@18423 ` 1871` ``` using insert by(simp add:inf_Sup1_distrib[OF B]) ``` wenzelm@31916 ` 1872` ``` also have "\ = \\<^bsub>fin\<^esub>({inf x b |b. b \ B} \ {inf a b |a b. a \ A \ b \ B})" ``` wenzelm@31916 ` 1873` ``` (is "_ = \\<^bsub>fin\<^esub>?M") ``` nipkow@18423 ` 1874` ``` using B insert ``` haftmann@51489 ` 1875` ``` by (simp add: Sup_fin.union [OF finB _ finAB ne]) ``` haftmann@25062 ` 1876` ``` also have "?M = {inf a b |a b. a \ insert x A \ b \ B}" ``` nipkow@18423 ` 1877` ``` by blast ``` nipkow@18423 ` 1878` ``` finally show ?case . ``` nipkow@18423 ` 1879` ```qed ``` nipkow@18423 ` 1880` haftmann@24342 ` 1881` ```end ``` haftmann@24342 ` 1882` haftmann@35719 ` 1883` ```context complete_lattice ``` haftmann@35719 ` 1884` ```begin ``` haftmann@35719 ` 1885` haftmann@35719 ` 1886` ```lemma Inf_fin_Inf: ``` haftmann@35719 ` 1887` ``` assumes "finite A" and "A \ {}" ``` haftmann@35719 ` 1888` ``` shows "\\<^bsub>fin\<^esub>A = Inf A" ``` haftmann@35719 ` 1889` ```proof - ``` haftmann@51489 ` 1890` ``` from assms obtain b B where "A = insert b B" and "finite B" by auto ``` haftmann@51489 ` 1891` ``` then show ?thesis ``` haftmann@51489 ` 1892` ``` by (simp add: Inf_fin.eq_fold inf_Inf_fold_inf inf.commute [of b]) ``` haftmann@35719 ` 1893` ```qed ``` haftmann@35719 ` 1894` haftmann@35719 ` 1895` ```lemma Sup_fin_Sup: ``` haftmann@35719 ` 1896` ``` assumes "finite A" and "A \ {}" ``` haftmann@35719 ` 1897` ``` shows "\\<^bsub>fin\<^esub>A = Sup A" ``` haftmann@35719 ` 1898` ```proof - ``` haftmann@51489 ` 1899` ``` from assms obtain b B where "A = insert b B" and "finite B" by auto ``` haftmann@51489 ` 1900` ``` then show ?thesis ``` haftmann@51489 ` 1901` ``` by (simp add: Sup_fin.eq_fold sup_Sup_fold_sup sup.commute [of b]) ``` haftmann@35719 ` 1902` ```qed ``` haftmann@35719 ` 1903` haftmann@35719 ` 1904` ```end ``` haftmann@35719 ` 1905` haftmann@22917 ` 1906` haftmann@51489 ` 1907` ```subsection {* Minimum and Maximum over non-empty sets *} ``` haftmann@22917 ` 1908` haftmann@24342 ` 1909` ```context linorder ``` haftmann@22917 ` 1910` ```begin ``` haftmann@22917 ` 1911` haftmann@26041 ` 1912` ```lemma dual_min: ``` haftmann@51489 ` 1913` ``` "ord.min greater_eq = max" ``` wenzelm@46904 ` 1914` ``` by (auto simp add: ord.min_def max_def fun_eq_iff) ``` haftmann@26041 ` 1915` haftmann@51489 ` 1916` ```lemma dual_max: ``` haftmann@51489 ` 1917` ``` "ord.max greater_eq = min" ``` haftmann@51489 ` 1918` ``` by (auto simp add: ord.max_def min_def fun_eq_iff) ``` haftmann@51489 ` 1919` haftmann@51489 ` 1920` ```lemma dual_Min: ``` haftmann@51489 ` 1921` ``` "linorder.Min greater_eq = Max" ``` haftmann@26041 ` 1922` ```proof - ``` haftmann@51489 ` 1923` ``` interpret dual!: linorder greater_eq greater by (fact dual_linorder) ``` haftmann@51489 ` 1924` ``` show ?thesis by (simp add: dual.Min_def dual_min Max_def) ``` haftmann@26041 ` 1925` ```qed ``` haftmann@26041 ` 1926` haftmann@51489 ` 1927` ```lemma dual_Max: ``` haftmann@51489 ` 1928` ``` "linorder.Max greater_eq = Min" ``` haftmann@26041 ` 1929` ```proof - ``` haftmann@51489 ` 1930` ``` interpret dual!: linorder greater_eq greater by (fact dual_linorder) ``` haftmann@51489 ` 1931` ``` show ?thesis by (simp add: dual.Max_def dual_max Min_def) ``` haftmann@26041 ` 1932` ```qed ``` haftmann@26041 ` 1933` haftmann@51540 ` 1934` ```lemmas Min_singleton = Min.singleton ``` haftmann@51540 ` 1935` ```lemmas Max_singleton = Max.singleton ``` haftmann@51540 ` 1936` ```lemmas Min_insert = Min.insert ``` haftmann@51540 ` 1937` ```lemmas Max_insert = Max.insert ``` haftmann@51540 ` 1938` ```lemmas Min_Un = Min.union ``` haftmann@51540 ` 1939` ```lemmas Max_Un = Max.union ``` haftmann@51540 ` 1940` ```lemmas hom_Min_commute = Min.hom_commute ``` haftmann@51540 ` 1941` ```lemmas hom_Max_commute = Max.hom_commute ``` haftmann@26041 ` 1942` paulson@24427 ` 1943` ```lemma Min_in [simp]: ``` haftmann@26041 ` 1944` ``` assumes "finite A" and "A \ {}" ``` haftmann@26041 ` 1945` ``` shows "Min A \ A" ``` haftmann@51540 ` 1946` ``` using assms by (auto simp add: min_def Min.closed) ``` nipkow@15392 ` 1947` paulson@24427 ` 1948` ```lemma Max_in [simp]: ``` haftmann@26041 ` 1949` ``` assumes "finite A" and "A \ {}" ``` haftmann@26041 ` 1950` ``` shows "Max A \ A" ``` haftmann@51540 ` 1951` ``` using assms by (auto simp add: max_def Max.closed) ``` haftmann@26041 ` 1952` haftmann@26041 ` 1953` ```lemma Min_le [simp]: ``` haftmann@26757 ` 1954` ``` assumes "finite A" and "x \ A" ``` haftmann@26041 ` 1955` ``` shows "Min A \ x" ``` haftmann@51540 ` 1956` ``` using assms by (fact Min.coboundedI) ``` haftmann@26041 ` 1957` haftmann@26041 ` 1958` ```lemma Max_ge [simp]: ``` haftmann@26757 ` 1959` ``` assumes "finite A" and "x \ A" ``` haftmann@26041 ` 1960` ``` shows "x \ Max A" ``` haftmann@51540 ` 1961` ``` using assms by (fact Max.coboundedI) ``` haftmann@26041 ` 1962` haftmann@30325 ` 1963` ```lemma Min_eqI: ``` haftmann@30325 ` 1964` ``` assumes "finite A" ``` haftmann@30325 ` 1965` ``` assumes "\y. y \ A \ y \ x" ``` haftmann@30325 ` 1966` ``` and "x \ A" ``` haftmann@30325 ` 1967` ``` shows "Min A = x" ``` haftmann@30325 ` 1968` ```proof (rule antisym) ``` haftmann@30325 ` 1969` ``` from `x \ A` have "A \ {}" by auto ``` haftmann@30325 ` 1970` ``` with assms show "Min A \ x" by simp ``` haftmann@30325 ` 1971` ```next ``` haftmann@30325 ` 1972` ``` from assms show "x \ Min A" by simp ``` haftmann@30325 ` 1973` ```qed ``` haftmann@30325 ` 1974` haftmann@30325 ` 1975` ```lemma Max_eqI: ``` haftmann@30325 ` 1976` ``` assumes "finite A" ``` haftmann@30325 ` 1977` ``` assumes "\y. y \ A \ y \ x" ``` haftmann@30325 ` 1978` ``` and "x \ A" ``` haftmann@30325 ` 1979` ``` shows "Max A = x" ``` haftmann@30325 ` 1980` ```proof (rule antisym) ``` haftmann@30325 ` 1981` ``` from `x \ A` have "A \ {}" by auto ``` haftmann@30325 ` 1982` ``` with assms show "Max A \ x" by simp ``` haftmann@30325 ` 1983` ```next ``` haftmann@30325 ` 1984` ``` from assms show "x \ Max A" by simp ``` haftmann@30325 ` 1985` ```qed ``` haftmann@30325 ` 1986` haftmann@51489 ` 1987` ```lemma Min_ge_iff [simp, no_atp]: ``` haftmann@51489 ` 1988` ``` assumes "finite A" and "A \ {}" ``` haftmann@51489 ` 1989` ``` shows "x \ Min A \ (\a\A. x \ a)" ``` haftmann@51540 ` 1990` ``` using assms by (fact Min.bounded_iff) ``` haftmann@51489 ` 1991` haftmann@51489 ` 1992` ```lemma Max_le_iff [simp, no_atp]: ``` haftmann@51489 ` 1993` ``` assumes "finite A" and "A \ {}" ``` haftmann@51489 ` 1994` ``` shows "Max A \ x \ (\a\A. a \ x)" ``` haftmann@51540 ` 1995` ``` using assms by (fact Max.bounded_iff) ``` haftmann@51489 ` 1996` haftmann@51489 ` 1997` ```lemma Min_gr_iff [simp, no_atp]: ``` haftmann@51489 ` 1998` ``` assumes "finite A" and "A \ {}" ``` haftmann@51489 ` 1999` ``` shows "x < Min A \ (\a\A. x < a)" ``` haftmann@51489 ` 2000` ``` using assms by (induct rule: finite_ne_induct) simp_all ``` haftmann@51489 ` 2001` haftmann@51489 ` 2002` ```lemma Max_less_iff [simp, no_atp]: ``` haftmann@51489 ` 2003` ``` assumes "finite A" and "A \ {}" ``` haftmann@51489 ` 2004` ``` shows "Max A < x \ (\a\A. a < x)" ``` haftmann@51489 ` 2005` ``` using assms by (induct rule: finite_ne_induct) simp_all ``` haftmann@51489 ` 2006` haftmann@51489 ` 2007` ```lemma Min_le_iff [no_atp]: ``` haftmann@51489 ` 2008` ``` assumes "finite A" and "A \ {}" ``` haftmann@51489 ` 2009` ``` shows "Min A \ x \ (\a\A. a \ x)" ``` haftmann@51489 ` 2010` ``` using assms by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj) ``` haftmann@51489 ` 2011` haftmann@51489 ` 2012` ```lemma Max_ge_iff [no_atp]: ``` haftmann@51489 ` 2013` ``` assumes "finite A" and "A \ {}" ``` haftmann@51489 ` 2014` ``` shows "x \ Max A \ (\a\A. x \ a)" ``` haftmann@51489 ` 2015` ``` using assms by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj) ``` haftmann@51489 ` 2016` haftmann@51489 ` 2017` ```lemma Min_less_iff [no_atp]: ``` haftmann@51489 ` 2018` ``` assumes "finite A" and "A \ {}" ``` haftmann@51489 ` 2019` ``` shows "Min A < x \ (\a\A. a < x)" ``` haftmann@51489 ` 2020` ``` using assms by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj) ``` haftmann@51489 ` 2021` haftmann@51489 ` 2022` ```lemma Max_gr_iff [no_atp]: ``` haftmann@51489 ` 2023` ``` assumes "finite A" and "A \ {}" ``` haftmann@51489 ` 2024` ``` shows "x < Max A \ (\a\A. x < a)" ``` haftmann@51489 ` 2025` ``` using assms by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj) ``` haftmann@51489 ` 2026` haftmann@26041 ` 2027` ```lemma Min_antimono: ``` haftmann@26041 ` 2028` ``` assumes "M \ N" and "M \ {}" and "finite N" ``` haftmann@26041 ` 2029` ``` shows "Min N \ Min M" ``` haftmann@51540 ` 2030` ``` using assms by (fact Min.antimono) ``` haftmann@26041 ` 2031` haftmann@26041 ` 2032` ```lemma Max_mono: ``` haftmann@26041 ` 2033` ``` assumes "M \ N" and "M \ {}" and "finite N" ``` haftmann@26041 ` 2034` ``` shows "Max M \ Max N" ``` haftmann@51540 ` 2035` ``` using assms by (fact Max.antimono) ``` haftmann@51489 ` 2036` haftmann@51489 ` 2037` ```lemma mono_Min_commute: ``` haftmann@51489 ` 2038` ``` assumes "mono f" ``` haftmann@51489 ` 2039` ``` assumes "finite A" and "A \ {}" ``` haftmann@51489 ` 2040` ``` shows "f (Min A) = Min (f ` A)" ``` haftmann@51489 ` 2041` ```proof (rule linorder_class.Min_eqI [symmetric]) ``` haftmann@51489 ` 2042` ``` from `finite A` show "finite (f ` A)" by simp ``` haftmann@51489 ` 2043` ``` from assms show "f (Min A) \ f ` A" by simp ``` haftmann@51489 ` 2044` ``` fix x ``` haftmann@51489 ` 2045` ``` assume "x \ f ` A" ``` haftmann@51489 ` 2046` ``` then obtain y where "y \ A" and "x = f y" .. ``` haftmann@51489 ` 2047` ``` with assms have "Min A \ y" by auto ``` haftmann@51489 ` 2048` ``` with `mono f` have "f (Min A) \ f y" by (rule monoE) ``` haftmann@51489 ` 2049` ``` with `x = f y` show "f (Min A) \ x" by simp ``` haftmann@51489 ` 2050` ```qed ``` haftmann@22917 ` 2051` haftmann@51489 ` 2052` ```lemma mono_Max_commute: ``` haftmann@51489 ` 2053` ``` assumes "mono f" ``` haftmann@51489 ` 2054` ``` assumes "finite A" and "A \ {}" ``` haftmann@51489 ` 2055` ``` shows "f (Max A) = Max (f ` A)" ``` haftmann@51489 ` 2056` ```proof (rule linorder_class.Max_eqI [symmetric]) ``` haftmann@51489 ` 2057` ``` from `finite A` show "finite (f ` A)" by simp ``` haftmann@51489 ` 2058` ``` from assms show "f (Max A) \ f ` A" by simp ``` haftmann@51489 ` 2059` ``` fix x ``` haftmann@51489 ` 2060` ``` assume "x \ f ` A" ``` haftmann@51489 ` 2061` ``` then obtain y where "y \ A" and "x = f y" .. ``` haftmann@51489 ` 2062` ``` with assms have "y \ Max A" by auto ``` haftmann@51489 ` 2063` ``` with `mono f` have "f y \ f (Max A)" by (rule monoE) ``` haftmann@51489 ` 2064` ``` with `x = f y` show "x \ f (Max A)" by simp ``` haftmann@51489 ` 2065` ```qed ``` haftmann@51489 ` 2066` haftmann@51489 ` 2067` ```lemma finite_linorder_max_induct [consumes 1, case_names empty insert]: ``` haftmann@51489 ` 2068` ``` assumes fin: "finite A" ``` haftmann@51489 ` 2069` ``` and empty: "P {}" ``` haftmann@51489 ` 2070` ``` and insert: "\b A. finite A \ \a\A. a < b \ P A \ P (insert b A)" ``` haftmann@51489 ` 2071` ``` shows "P A" ``` urbanc@36079 ` 2072` ```using fin empty insert ``` nipkow@32006 ` 2073` ```proof (induct rule: finite_psubset_induct) ``` urbanc@36079 ` 2074` ``` case (psubset A) ``` urbanc@36079 ` 2075` ``` have IH: "\B. \B < A; P {}; (\A b. \finite A; \a\A. a \ P (insert b A))\ \ P B" by fact ``` urbanc@36079 ` 2076` ``` have fin: "finite A" by fact ``` urbanc@36079 ` 2077` ``` have empty: "P {}" by fact ``` urbanc@36079 ` 2078` ``` have step: "\b A. \finite A; \a\A. a < b; P A\ \ P (insert b A)" by fact ``` krauss@26748 ` 2079` ``` show "P A" ``` haftmann@26757 ` 2080` ``` proof (cases "A = {}") ``` urbanc@36079 ` 2081` ``` assume "A = {}" ``` urbanc@36079 ` 2082` ``` then show "P A" using `P {}` by simp ``` krauss@26748 ` 2083` ``` next ``` urbanc@36079 ` 2084` ``` let ?B = "A - {Max A}" ``` urbanc@36079 ` 2085` ``` let ?A = "insert (Max A) ?B" ``` urbanc@36079 ` 2086` ``` have "finite ?B" using `finite A` by simp ``` krauss@26748 ` 2087` ``` assume "A \ {}" ``` krauss@26748 ` 2088` ``` with `finite A` have "Max A : A" by auto ``` urbanc@36079 ` 2089` ``` then have A: "?A = A" using insert_Diff_single insert_absorb by auto ``` haftmann@51489 ` 2090` ``` then have "P ?B" using `P {}` step IH [of ?B] by blast ``` urbanc@36079 ` 2091` ``` moreover ``` nipkow@44890 ` 2092` ``` have "\a\?B. a < Max A" using Max_ge [OF `finite A`] by fastforce ``` haftmann@51489 ` 2093` ``` ultimately show "P A" using A insert_Diff_single step [OF `finite ?B`] by fastforce ``` krauss@26748 ` 2094` ``` qed ``` krauss@26748 ` 2095` ```qed ``` krauss@26748 ` 2096` haftmann@51489 ` 2097` ```lemma finite_linorder_min_induct [consumes 1, case_names empty insert]: ``` haftmann@51489 ` 2098` ``` "\finite A; P {}; \b A. \finite A; \a\A. b < a; P A\ \ P (insert b A)\ \ P A" ``` haftmann@51489 ` 2099` ``` by (rule linorder.finite_linorder_max_induct [OF dual_linorder]) ``` nipkow@32006 ` 2100` haftmann@22917 ` 2101` ```end ``` haftmann@22917 ` 2102` haftmann@35028 ` 2103` ```context linordered_ab_semigroup_add ``` haftmann@22917 ` 2104` ```begin ``` haftmann@22917 ` 2105` haftmann@22917 ` 2106` ```lemma add_Min_commute: ``` haftmann@22917 ` 2107` ``` fixes k ``` haftmann@25062 ` 2108` ``` assumes "finite N" and "N \ {}" ``` haftmann@25062 ` 2109` ``` shows "k + Min N = Min {k + m | m. m \ N}" ``` haftmann@25062 ` 2110` ```proof - ``` haftmann@25062 ` 2111` ``` have "\x y. k + min x y = min (k + x) (k + y)" ``` haftmann@25062 ` 2112` ``` by (simp add: min_def not_le) ``` haftmann@25062 ` 2113` ``` (blast intro: antisym less_imp_le add_left_mono) ``` haftmann@25062 ` 2114` ``` with assms show ?thesis ``` haftmann@25062 ` 2115` ``` using hom_Min_commute [of "plus k" N] ``` haftmann@25062 ` 2116` ``` by simp (blast intro: arg_cong [where f = Min]) ``` haftmann@25062 ` 2117` ```qed ``` haftmann@22917 ` 2118` haftmann@22917 ` 2119` ```lemma add_Max_commute: ``` haftmann@22917 ` 2120` ``` fixes k ``` haftmann@25062 ` 2121` ``` assumes "finite N" and "N \ {}" ``` haftmann@25062 ` 2122` ``` shows "k + Max N = Max {k + m | m. m \ N}" ``` haftmann@25062 ` 2123` ```proof - ``` haftmann@25062 ` 2124` ``` have "\x y. k + max x y = max (k + x) (k + y)" ``` haftmann@25062 ` 2125` ``` by (simp add: max_def not_le) ``` haftmann@25062 ` 2126` ``` (blast intro: antisym less_imp_le add_left_mono) ``` haftmann@25062 ` 2127` ``` with assms show ?thesis ``` haftmann@25062 ` 2128` ``` using hom_Max_commute [of "plus k" N] ``` haftmann@25062 ` 2129` ``` by simp (blast intro: arg_cong [where f = Max]) ``` haftmann@25062 ` 2130` ```qed ``` haftmann@22917 ` 2131` haftmann@22917 ` 2132` ```end ``` haftmann@22917 ` 2133` haftmann@35034 ` 2134` ```context linordered_ab_group_add ``` haftmann@35034 ` 2135` ```begin ``` haftmann@35034 ` 2136` haftmann@35034 ` 2137` ```lemma minus_Max_eq_Min [simp]: ``` haftmann@51489 ` 2138` ``` "finite S \ S \ {} \ - Max S = Min (uminus ` S)" ``` haftmann@35034 ` 2139` ``` by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min) ``` haftmann@35034 ` 2140` haftmann@35034 ` 2141` ```lemma minus_Min_eq_Max [simp]: ``` haftmann@51489 ` 2142` ``` "finite S \ S \ {} \ - Min S = Max (uminus ` S)" ``` haftmann@35034 ` 2143` ``` by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max) ``` haftmann@35034 ` 2144` haftmann@35034 ` 2145` ```end ``` haftmann@35034 ` 2146` haftmann@51540 ` 2147` ```context complete_linorder ``` haftmann@51540 ` 2148` ```begin ``` haftmann@51540 ` 2149` haftmann@51540 ` 2150` ```lemma Min_Inf: ``` haftmann@51540 ` 2151` ``` assumes "finite A" and "A \ {}" ``` haftmann@51540 ` 2152` ``` shows "Min A = Inf A" ``` haftmann@51540 ` 2153` ```proof - ``` haftmann@51540 ` 2154` ``` from assms obtain b B where "A = insert b B" and "finite B" by auto ``` haftmann@51540 ` 2155` ``` then show ?thesis ``` haftmann@51540 ` 2156` ``` by (simp add: Min.eq_fold complete_linorder_inf_min [symmetric] inf_Inf_fold_inf inf.commute [of b]) ``` haftmann@51540 ` 2157` ```qed ``` haftmann@51540 ` 2158` haftmann@51540 ` 2159` ```lemma Max_Sup: ``` haftmann@51540 ` 2160` ``` assumes "finite A" and "A \ {}" ``` haftmann@51540 ` 2161` ``` shows "Max A = Sup A" ``` haftmann@51540 ` 2162` ```proof - ``` haftmann@51540 ` 2163` ``` from assms obtain b B where "A = insert b B" and "finite B" by auto ``` haftmann@51540 ` 2164` ``` then show ?thesis ``` haftmann@51540 ` 2165` ``` by (simp add: Max.eq_fold complete_linorder_sup_max [symmetric] sup_Sup_fold_sup sup.commute [of b]) ``` haftmann@51540 ` 2166` ```qed ``` haftmann@51540 ` 2167` haftmann@25571 ` 2168` ```end ``` haftmann@51263 ` 2169` haftmann@51540 ` 2170` ```end ``` haftmann@51540 ` 2171`