src/HOL/Library/Set_Algebras.thy
 author blanchet Wed Sep 24 15:45:55 2014 +0200 (2014-09-24) changeset 58425 246985c6b20b parent 57514 bdc2c6b40bf2 child 58881 b9556a055632 permissions -rw-r--r--
simpler proof
 haftmann@38622 ` 1` ```(* Title: HOL/Library/Set_Algebras.thy ``` haftmann@38622 ` 2` ``` Author: Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM ``` avigad@16908 ` 3` ```*) ``` avigad@16908 ` 4` haftmann@38622 ` 5` ```header {* Algebraic operations on sets *} ``` avigad@16908 ` 6` haftmann@38622 ` 7` ```theory Set_Algebras ``` haftmann@30738 ` 8` ```imports Main ``` avigad@16908 ` 9` ```begin ``` avigad@16908 ` 10` wenzelm@19736 ` 11` ```text {* ``` wenzelm@56899 ` 12` ``` This library lifts operations like addition and multiplication to ``` haftmann@38622 ` 13` ``` sets. It was designed to support asymptotic calculations. See the ``` haftmann@38622 ` 14` ``` comments at the top of theory @{text BigO}. ``` avigad@16908 ` 15` ```*} ``` avigad@16908 ` 16` krauss@47443 ` 17` ```instantiation set :: (plus) plus ``` krauss@47443 ` 18` ```begin ``` krauss@47443 ` 19` krauss@47443 ` 20` ```definition plus_set :: "'a::plus set \ 'a set \ 'a set" where ``` krauss@47443 ` 21` ``` set_plus_def: "A + B = {c. \a\A. \b\B. c = a + b}" ``` krauss@47443 ` 22` krauss@47443 ` 23` ```instance .. ``` krauss@47443 ` 24` krauss@47443 ` 25` ```end ``` krauss@47443 ` 26` krauss@47443 ` 27` ```instantiation set :: (times) times ``` krauss@47443 ` 28` ```begin ``` krauss@47443 ` 29` krauss@47443 ` 30` ```definition times_set :: "'a::times set \ 'a set \ 'a set" where ``` krauss@47443 ` 31` ``` set_times_def: "A * B = {c. \a\A. \b\B. c = a * b}" ``` krauss@47443 ` 32` krauss@47443 ` 33` ```instance .. ``` krauss@47443 ` 34` krauss@47443 ` 35` ```end ``` krauss@47443 ` 36` krauss@47443 ` 37` ```instantiation set :: (zero) zero ``` krauss@47443 ` 38` ```begin ``` krauss@47443 ` 39` krauss@47443 ` 40` ```definition ``` wenzelm@56899 ` 41` ``` set_zero[simp]: "(0::'a::zero set) = {0}" ``` krauss@47443 ` 42` krauss@47443 ` 43` ```instance .. ``` krauss@47443 ` 44` krauss@47443 ` 45` ```end ``` wenzelm@56899 ` 46` krauss@47443 ` 47` ```instantiation set :: (one) one ``` krauss@47443 ` 48` ```begin ``` krauss@47443 ` 49` krauss@47443 ` 50` ```definition ``` wenzelm@56899 ` 51` ``` set_one[simp]: "(1::'a::one set) = {1}" ``` krauss@47443 ` 52` krauss@47443 ` 53` ```instance .. ``` krauss@47443 ` 54` krauss@47443 ` 55` ```end ``` haftmann@25594 ` 56` haftmann@38622 ` 57` ```definition elt_set_plus :: "'a::plus \ 'a set \ 'a set" (infixl "+o" 70) where ``` haftmann@38622 ` 58` ``` "a +o B = {c. \b\B. c = a + b}" ``` avigad@16908 ` 59` haftmann@38622 ` 60` ```definition elt_set_times :: "'a::times \ 'a set \ 'a set" (infixl "*o" 80) where ``` haftmann@38622 ` 61` ``` "a *o B = {c. \b\B. c = a * b}" ``` haftmann@25594 ` 62` haftmann@38622 ` 63` ```abbreviation (input) elt_set_eq :: "'a \ 'a set \ bool" (infix "=o" 50) where ``` haftmann@38622 ` 64` ``` "x =o A \ x \ A" ``` haftmann@25594 ` 65` krauss@47443 ` 66` ```instance set :: (semigroup_add) semigroup_add ``` wenzelm@56899 ` 67` ``` by default (force simp add: set_plus_def add.assoc) ``` haftmann@25594 ` 68` krauss@47443 ` 69` ```instance set :: (ab_semigroup_add) ab_semigroup_add ``` wenzelm@56899 ` 70` ``` by default (force simp add: set_plus_def add.commute) ``` haftmann@25594 ` 71` krauss@47443 ` 72` ```instance set :: (monoid_add) monoid_add ``` wenzelm@56899 ` 73` ``` by default (simp_all add: set_plus_def) ``` haftmann@25594 ` 74` krauss@47443 ` 75` ```instance set :: (comm_monoid_add) comm_monoid_add ``` wenzelm@56899 ` 76` ``` by default (simp_all add: set_plus_def) ``` avigad@16908 ` 77` krauss@47443 ` 78` ```instance set :: (semigroup_mult) semigroup_mult ``` wenzelm@56899 ` 79` ``` by default (force simp add: set_times_def mult.assoc) ``` avigad@16908 ` 80` krauss@47443 ` 81` ```instance set :: (ab_semigroup_mult) ab_semigroup_mult ``` wenzelm@56899 ` 82` ``` by default (force simp add: set_times_def mult.commute) ``` avigad@16908 ` 83` krauss@47443 ` 84` ```instance set :: (monoid_mult) monoid_mult ``` wenzelm@56899 ` 85` ``` by default (simp_all add: set_times_def) ``` avigad@16908 ` 86` krauss@47443 ` 87` ```instance set :: (comm_monoid_mult) comm_monoid_mult ``` wenzelm@56899 ` 88` ``` by default (simp_all add: set_times_def) ``` avigad@16908 ` 89` wenzelm@56899 ` 90` ```lemma set_plus_intro [intro]: "a \ C \ b \ D \ a + b \ C + D" ``` berghofe@26814 ` 91` ``` by (auto simp add: set_plus_def) ``` avigad@16908 ` 92` huffman@53596 ` 93` ```lemma set_plus_elim: ``` huffman@53596 ` 94` ``` assumes "x \ A + B" ``` huffman@53596 ` 95` ``` obtains a b where "x = a + b" and "a \ A" and "b \ B" ``` huffman@53596 ` 96` ``` using assms unfolding set_plus_def by fast ``` huffman@53596 ` 97` wenzelm@56899 ` 98` ```lemma set_plus_intro2 [intro]: "b \ C \ a + b \ a +o C" ``` wenzelm@19736 ` 99` ``` by (auto simp add: elt_set_plus_def) ``` avigad@16908 ` 100` wenzelm@56899 ` 101` ```lemma set_plus_rearrange: ``` wenzelm@56899 ` 102` ``` "((a::'a::comm_monoid_add) +o C) + (b +o D) = (a + b) +o (C + D)" ``` haftmann@57514 ` 103` ``` apply (auto simp add: elt_set_plus_def set_plus_def ac_simps) ``` wenzelm@19736 ` 104` ``` apply (rule_tac x = "ba + bb" in exI) ``` haftmann@57514 ` 105` ``` apply (auto simp add: ac_simps) ``` avigad@16908 ` 106` ``` apply (rule_tac x = "aa + a" in exI) ``` haftmann@57514 ` 107` ``` apply (auto simp add: ac_simps) ``` wenzelm@19736 ` 108` ``` done ``` avigad@16908 ` 109` wenzelm@56899 ` 110` ```lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) = (a + b) +o C" ``` haftmann@57512 ` 111` ``` by (auto simp add: elt_set_plus_def add.assoc) ``` avigad@16908 ` 112` wenzelm@56899 ` 113` ```lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) + C = a +o (B + C)" ``` berghofe@26814 ` 114` ``` apply (auto simp add: elt_set_plus_def set_plus_def) ``` haftmann@57514 ` 115` ``` apply (blast intro: ac_simps) ``` avigad@16908 ` 116` ``` apply (rule_tac x = "a + aa" in exI) ``` avigad@16908 ` 117` ``` apply (rule conjI) ``` wenzelm@19736 ` 118` ``` apply (rule_tac x = "aa" in bexI) ``` wenzelm@19736 ` 119` ``` apply auto ``` avigad@16908 ` 120` ``` apply (rule_tac x = "ba" in bexI) ``` haftmann@57514 ` 121` ``` apply (auto simp add: ac_simps) ``` wenzelm@19736 ` 122` ``` done ``` avigad@16908 ` 123` wenzelm@56899 ` 124` ```theorem set_plus_rearrange4: "C + ((a::'a::comm_monoid_add) +o D) = a +o (C + D)" ``` haftmann@57514 ` 125` ``` apply (auto simp add: elt_set_plus_def set_plus_def ac_simps) ``` wenzelm@19736 ` 126` ``` apply (rule_tac x = "aa + ba" in exI) ``` haftmann@57514 ` 127` ``` apply (auto simp add: ac_simps) ``` wenzelm@19736 ` 128` ``` done ``` avigad@16908 ` 129` avigad@16908 ` 130` ```theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2 ``` avigad@16908 ` 131` ``` set_plus_rearrange3 set_plus_rearrange4 ``` avigad@16908 ` 132` wenzelm@56899 ` 133` ```lemma set_plus_mono [intro!]: "C \ D \ a +o C \ a +o D" ``` wenzelm@19736 ` 134` ``` by (auto simp add: elt_set_plus_def) ``` avigad@16908 ` 135` wenzelm@56899 ` 136` ```lemma set_plus_mono2 [intro]: "(C::'a::plus set) \ D \ E \ F \ C + E \ D + F" ``` berghofe@26814 ` 137` ``` by (auto simp add: set_plus_def) ``` avigad@16908 ` 138` wenzelm@56899 ` 139` ```lemma set_plus_mono3 [intro]: "a \ C \ a +o D \ C + D" ``` berghofe@26814 ` 140` ``` by (auto simp add: elt_set_plus_def set_plus_def) ``` avigad@16908 ` 141` wenzelm@56899 ` 142` ```lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) \ C \ a +o D \ D + C" ``` haftmann@57514 ` 143` ``` by (auto simp add: elt_set_plus_def set_plus_def ac_simps) ``` avigad@16908 ` 144` wenzelm@56899 ` 145` ```lemma set_plus_mono5: "a \ C \ B \ D \ a +o B \ C + D" ``` wenzelm@56899 ` 146` ``` apply (subgoal_tac "a +o B \ a +o D") ``` wenzelm@19736 ` 147` ``` apply (erule order_trans) ``` wenzelm@19736 ` 148` ``` apply (erule set_plus_mono3) ``` avigad@16908 ` 149` ``` apply (erule set_plus_mono) ``` wenzelm@19736 ` 150` ``` done ``` avigad@16908 ` 151` wenzelm@56899 ` 152` ```lemma set_plus_mono_b: "C \ D \ x \ a +o C \ x \ a +o D" ``` avigad@16908 ` 153` ``` apply (frule set_plus_mono) ``` avigad@16908 ` 154` ``` apply auto ``` wenzelm@19736 ` 155` ``` done ``` avigad@16908 ` 156` wenzelm@56899 ` 157` ```lemma set_plus_mono2_b: "C \ D \ E \ F \ x \ C + E \ x \ D + F" ``` avigad@16908 ` 158` ``` apply (frule set_plus_mono2) ``` wenzelm@19736 ` 159` ``` prefer 2 ``` wenzelm@19736 ` 160` ``` apply force ``` avigad@16908 ` 161` ``` apply assumption ``` wenzelm@19736 ` 162` ``` done ``` avigad@16908 ` 163` wenzelm@56899 ` 164` ```lemma set_plus_mono3_b: "a \ C \ x \ a +o D \ x \ C + D" ``` avigad@16908 ` 165` ``` apply (frule set_plus_mono3) ``` avigad@16908 ` 166` ``` apply auto ``` wenzelm@19736 ` 167` ``` done ``` avigad@16908 ` 168` wenzelm@56899 ` 169` ```lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C \ x \ a +o D \ x \ D + C" ``` avigad@16908 ` 170` ``` apply (frule set_plus_mono4) ``` avigad@16908 ` 171` ``` apply auto ``` wenzelm@19736 ` 172` ``` done ``` avigad@16908 ` 173` avigad@16908 ` 174` ```lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C" ``` wenzelm@19736 ` 175` ``` by (auto simp add: elt_set_plus_def) ``` avigad@16908 ` 176` wenzelm@56899 ` 177` ```lemma set_zero_plus2: "(0::'a::comm_monoid_add) \ A \ B \ A + B" ``` huffman@44142 ` 178` ``` apply (auto simp add: set_plus_def) ``` avigad@16908 ` 179` ``` apply (rule_tac x = 0 in bexI) ``` wenzelm@19736 ` 180` ``` apply (rule_tac x = x in bexI) ``` haftmann@57514 ` 181` ``` apply (auto simp add: ac_simps) ``` wenzelm@19736 ` 182` ``` done ``` avigad@16908 ` 183` wenzelm@56899 ` 184` ```lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C \ (a - b) \ C" ``` haftmann@57514 ` 185` ``` by (auto simp add: elt_set_plus_def ac_simps) ``` avigad@16908 ` 186` wenzelm@56899 ` 187` ```lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C \ a \ b +o C" ``` haftmann@57514 ` 188` ``` apply (auto simp add: elt_set_plus_def ac_simps) ``` avigad@16908 ` 189` ``` apply (subgoal_tac "a = (a + - b) + b") ``` haftmann@54230 ` 190` ``` apply (rule bexI, assumption) ``` haftmann@57514 ` 191` ``` apply (auto simp add: ac_simps) ``` wenzelm@19736 ` 192` ``` done ``` avigad@16908 ` 193` wenzelm@56899 ` 194` ```lemma set_minus_plus: "(a::'a::ab_group_add) - b \ C \ a \ b +o C" ``` wenzelm@56899 ` 195` ``` by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus) ``` avigad@16908 ` 196` wenzelm@56899 ` 197` ```lemma set_times_intro [intro]: "a \ C \ b \ D \ a * b \ C * D" ``` berghofe@26814 ` 198` ``` by (auto simp add: set_times_def) ``` avigad@16908 ` 199` huffman@53596 ` 200` ```lemma set_times_elim: ``` huffman@53596 ` 201` ``` assumes "x \ A * B" ``` huffman@53596 ` 202` ``` obtains a b where "x = a * b" and "a \ A" and "b \ B" ``` huffman@53596 ` 203` ``` using assms unfolding set_times_def by fast ``` huffman@53596 ` 204` wenzelm@56899 ` 205` ```lemma set_times_intro2 [intro!]: "b \ C \ a * b \ a *o C" ``` wenzelm@19736 ` 206` ``` by (auto simp add: elt_set_times_def) ``` avigad@16908 ` 207` wenzelm@56899 ` 208` ```lemma set_times_rearrange: ``` wenzelm@56899 ` 209` ``` "((a::'a::comm_monoid_mult) *o C) * (b *o D) = (a * b) *o (C * D)" ``` berghofe@26814 ` 210` ``` apply (auto simp add: elt_set_times_def set_times_def) ``` wenzelm@19736 ` 211` ``` apply (rule_tac x = "ba * bb" in exI) ``` haftmann@57514 ` 212` ``` apply (auto simp add: ac_simps) ``` avigad@16908 ` 213` ``` apply (rule_tac x = "aa * a" in exI) ``` haftmann@57514 ` 214` ``` apply (auto simp add: ac_simps) ``` wenzelm@19736 ` 215` ``` done ``` avigad@16908 ` 216` wenzelm@56899 ` 217` ```lemma set_times_rearrange2: ``` wenzelm@56899 ` 218` ``` "(a::'a::semigroup_mult) *o (b *o C) = (a * b) *o C" ``` haftmann@57512 ` 219` ``` by (auto simp add: elt_set_times_def mult.assoc) ``` avigad@16908 ` 220` wenzelm@56899 ` 221` ```lemma set_times_rearrange3: ``` wenzelm@56899 ` 222` ``` "((a::'a::semigroup_mult) *o B) * C = a *o (B * C)" ``` berghofe@26814 ` 223` ``` apply (auto simp add: elt_set_times_def set_times_def) ``` haftmann@57514 ` 224` ``` apply (blast intro: ac_simps) ``` avigad@16908 ` 225` ``` apply (rule_tac x = "a * aa" in exI) ``` avigad@16908 ` 226` ``` apply (rule conjI) ``` wenzelm@19736 ` 227` ``` apply (rule_tac x = "aa" in bexI) ``` wenzelm@19736 ` 228` ``` apply auto ``` avigad@16908 ` 229` ``` apply (rule_tac x = "ba" in bexI) ``` haftmann@57514 ` 230` ``` apply (auto simp add: ac_simps) ``` wenzelm@19736 ` 231` ``` done ``` avigad@16908 ` 232` wenzelm@56899 ` 233` ```theorem set_times_rearrange4: ``` wenzelm@56899 ` 234` ``` "C * ((a::'a::comm_monoid_mult) *o D) = a *o (C * D)" ``` haftmann@57514 ` 235` ``` apply (auto simp add: elt_set_times_def set_times_def ac_simps) ``` wenzelm@19736 ` 236` ``` apply (rule_tac x = "aa * ba" in exI) ``` haftmann@57514 ` 237` ``` apply (auto simp add: ac_simps) ``` wenzelm@19736 ` 238` ``` done ``` avigad@16908 ` 239` avigad@16908 ` 240` ```theorems set_times_rearranges = set_times_rearrange set_times_rearrange2 ``` avigad@16908 ` 241` ``` set_times_rearrange3 set_times_rearrange4 ``` avigad@16908 ` 242` wenzelm@56899 ` 243` ```lemma set_times_mono [intro]: "C \ D \ a *o C \ a *o D" ``` wenzelm@19736 ` 244` ``` by (auto simp add: elt_set_times_def) ``` avigad@16908 ` 245` wenzelm@56899 ` 246` ```lemma set_times_mono2 [intro]: "(C::'a::times set) \ D \ E \ F \ C * E \ D * F" ``` berghofe@26814 ` 247` ``` by (auto simp add: set_times_def) ``` avigad@16908 ` 248` wenzelm@56899 ` 249` ```lemma set_times_mono3 [intro]: "a \ C \ a *o D \ C * D" ``` berghofe@26814 ` 250` ``` by (auto simp add: elt_set_times_def set_times_def) ``` avigad@16908 ` 251` wenzelm@56899 ` 252` ```lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C \ a *o D \ D * C" ``` haftmann@57514 ` 253` ``` by (auto simp add: elt_set_times_def set_times_def ac_simps) ``` avigad@16908 ` 254` wenzelm@56899 ` 255` ```lemma set_times_mono5: "a \ C \ B \ D \ a *o B \ C * D" ``` wenzelm@56899 ` 256` ``` apply (subgoal_tac "a *o B \ a *o D") ``` wenzelm@19736 ` 257` ``` apply (erule order_trans) ``` wenzelm@19736 ` 258` ``` apply (erule set_times_mono3) ``` avigad@16908 ` 259` ``` apply (erule set_times_mono) ``` wenzelm@19736 ` 260` ``` done ``` avigad@16908 ` 261` wenzelm@56899 ` 262` ```lemma set_times_mono_b: "C \ D \ x \ a *o C \ x \ a *o D" ``` avigad@16908 ` 263` ``` apply (frule set_times_mono) ``` avigad@16908 ` 264` ``` apply auto ``` wenzelm@19736 ` 265` ``` done ``` avigad@16908 ` 266` wenzelm@56899 ` 267` ```lemma set_times_mono2_b: "C \ D \ E \ F \ x \ C * E \ x \ D * F" ``` avigad@16908 ` 268` ``` apply (frule set_times_mono2) ``` wenzelm@19736 ` 269` ``` prefer 2 ``` wenzelm@19736 ` 270` ``` apply force ``` avigad@16908 ` 271` ``` apply assumption ``` wenzelm@19736 ` 272` ``` done ``` avigad@16908 ` 273` wenzelm@56899 ` 274` ```lemma set_times_mono3_b: "a \ C \ x \ a *o D \ x \ C * D" ``` avigad@16908 ` 275` ``` apply (frule set_times_mono3) ``` avigad@16908 ` 276` ``` apply auto ``` wenzelm@19736 ` 277` ``` done ``` avigad@16908 ` 278` wenzelm@56899 ` 279` ```lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) \ C \ x \ a *o D \ x \ D * C" ``` avigad@16908 ` 280` ``` apply (frule set_times_mono4) ``` avigad@16908 ` 281` ``` apply auto ``` wenzelm@19736 ` 282` ``` done ``` avigad@16908 ` 283` avigad@16908 ` 284` ```lemma set_one_times [simp]: "(1::'a::comm_monoid_mult) *o C = C" ``` wenzelm@19736 ` 285` ``` by (auto simp add: elt_set_times_def) ``` avigad@16908 ` 286` wenzelm@56899 ` 287` ```lemma set_times_plus_distrib: ``` wenzelm@56899 ` 288` ``` "(a::'a::semiring) *o (b +o C) = (a * b) +o (a *o C)" ``` nipkow@23477 ` 289` ``` by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs) ``` avigad@16908 ` 290` wenzelm@56899 ` 291` ```lemma set_times_plus_distrib2: ``` wenzelm@56899 ` 292` ``` "(a::'a::semiring) *o (B + C) = (a *o B) + (a *o C)" ``` berghofe@26814 ` 293` ``` apply (auto simp add: set_plus_def elt_set_times_def ring_distribs) ``` wenzelm@19736 ` 294` ``` apply blast ``` avigad@16908 ` 295` ``` apply (rule_tac x = "b + bb" in exI) ``` nipkow@23477 ` 296` ``` apply (auto simp add: ring_distribs) ``` wenzelm@19736 ` 297` ``` done ``` avigad@16908 ` 298` wenzelm@56899 ` 299` ```lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) * D \ a *o D + C * D" ``` huffman@44142 ` 300` ``` apply (auto simp add: ``` berghofe@26814 ` 301` ``` elt_set_plus_def elt_set_times_def set_times_def ``` berghofe@26814 ` 302` ``` set_plus_def ring_distribs) ``` avigad@16908 ` 303` ``` apply auto ``` wenzelm@19736 ` 304` ``` done ``` avigad@16908 ` 305` wenzelm@19380 ` 306` ```theorems set_times_plus_distribs = ``` wenzelm@19380 ` 307` ``` set_times_plus_distrib ``` avigad@16908 ` 308` ``` set_times_plus_distrib2 ``` avigad@16908 ` 309` wenzelm@56899 ` 310` ```lemma set_neg_intro: "(a::'a::ring_1) \ (- 1) *o C \ - a \ C" ``` wenzelm@19736 ` 311` ``` by (auto simp add: elt_set_times_def) ``` avigad@16908 ` 312` wenzelm@56899 ` 313` ```lemma set_neg_intro2: "(a::'a::ring_1) \ C \ - a \ (- 1) *o C" ``` wenzelm@19736 ` 314` ``` by (auto simp add: elt_set_times_def) ``` wenzelm@19736 ` 315` huffman@53596 ` 316` ```lemma set_plus_image: "S + T = (\(x, y). x + y) ` (S \ T)" ``` nipkow@44890 ` 317` ``` unfolding set_plus_def by (fastforce simp: image_iff) ``` hoelzl@40887 ` 318` huffman@53596 ` 319` ```lemma set_times_image: "S * T = (\(x, y). x * y) ` (S \ T)" ``` huffman@53596 ` 320` ``` unfolding set_times_def by (fastforce simp: image_iff) ``` huffman@53596 ` 321` wenzelm@56899 ` 322` ```lemma finite_set_plus: "finite s \ finite t \ finite (s + t)" ``` wenzelm@56899 ` 323` ``` unfolding set_plus_image by simp ``` huffman@53596 ` 324` wenzelm@56899 ` 325` ```lemma finite_set_times: "finite s \ finite t \ finite (s * t)" ``` wenzelm@56899 ` 326` ``` unfolding set_times_image by simp ``` huffman@53596 ` 327` hoelzl@40887 ` 328` ```lemma set_setsum_alt: ``` hoelzl@40887 ` 329` ``` assumes fin: "finite I" ``` krauss@47444 ` 330` ``` shows "setsum S I = {setsum s I |s. \i\I. s i \ S i}" ``` hoelzl@40887 ` 331` ``` (is "_ = ?setsum I") ``` wenzelm@56899 ` 332` ``` using fin ``` wenzelm@56899 ` 333` ```proof induct ``` wenzelm@56899 ` 334` ``` case empty ``` wenzelm@56899 ` 335` ``` then show ?case by simp ``` wenzelm@56899 ` 336` ```next ``` hoelzl@40887 ` 337` ``` case (insert x F) ``` krauss@47445 ` 338` ``` have "setsum S (insert x F) = S x + ?setsum F" ``` hoelzl@40887 ` 339` ``` using insert.hyps by auto ``` wenzelm@56899 ` 340` ``` also have "\ = {s x + setsum s F |s. \ i\insert x F. s i \ S i}" ``` hoelzl@40887 ` 341` ``` unfolding set_plus_def ``` hoelzl@40887 ` 342` ``` proof safe ``` wenzelm@56899 ` 343` ``` fix y s ``` wenzelm@56899 ` 344` ``` assume "y \ S x" "\i\F. s i \ S i" ``` hoelzl@40887 ` 345` ``` then show "\s'. y + setsum s F = s' x + setsum s' F \ (\i\insert x F. s' i \ S i)" ``` hoelzl@40887 ` 346` ``` using insert.hyps ``` hoelzl@40887 ` 347` ``` by (intro exI[of _ "\i. if i \ F then s i else y"]) (auto simp add: set_plus_def) ``` hoelzl@40887 ` 348` ``` qed auto ``` hoelzl@40887 ` 349` ``` finally show ?case ``` hoelzl@40887 ` 350` ``` using insert.hyps by auto ``` wenzelm@56899 ` 351` ```qed ``` hoelzl@40887 ` 352` hoelzl@40887 ` 353` ```lemma setsum_set_cond_linear: ``` wenzelm@56899 ` 354` ``` fixes f :: "'a::comm_monoid_add set \ 'b::comm_monoid_add set" ``` krauss@47445 ` 355` ``` assumes [intro!]: "\A B. P A \ P B \ P (A + B)" "P {0}" ``` krauss@47445 ` 356` ``` and f: "\A B. P A \ P B \ f (A + B) = f A + f B" "f {0} = {0}" ``` hoelzl@40887 ` 357` ``` assumes all: "\i. i \ I \ P (S i)" ``` krauss@47444 ` 358` ``` shows "f (setsum S I) = setsum (f \ S) I" ``` wenzelm@56899 ` 359` ```proof (cases "finite I") ``` wenzelm@56899 ` 360` ``` case True ``` wenzelm@56899 ` 361` ``` from this all show ?thesis ``` hoelzl@40887 ` 362` ``` proof induct ``` wenzelm@56899 ` 363` ``` case empty ``` wenzelm@56899 ` 364` ``` then show ?case by (auto intro!: f) ``` wenzelm@56899 ` 365` ``` next ``` hoelzl@40887 ` 366` ``` case (insert x F) ``` krauss@47444 ` 367` ``` from `finite F` `\i. i \ insert x F \ P (S i)` have "P (setsum S F)" ``` hoelzl@40887 ` 368` ``` by induct auto ``` hoelzl@40887 ` 369` ``` with insert show ?case ``` hoelzl@40887 ` 370` ``` by (simp, subst f) auto ``` wenzelm@56899 ` 371` ``` qed ``` wenzelm@56899 ` 372` ```next ``` wenzelm@56899 ` 373` ``` case False ``` wenzelm@56899 ` 374` ``` then show ?thesis by (auto intro!: f) ``` wenzelm@56899 ` 375` ```qed ``` hoelzl@40887 ` 376` hoelzl@40887 ` 377` ```lemma setsum_set_linear: ``` wenzelm@56899 ` 378` ``` fixes f :: "'a::comm_monoid_add set \ 'b::comm_monoid_add set" ``` krauss@47445 ` 379` ``` assumes "\A B. f(A) + f(B) = f(A + B)" "f {0} = {0}" ``` krauss@47444 ` 380` ``` shows "f (setsum S I) = setsum (f \ S) I" ``` hoelzl@40887 ` 381` ``` using setsum_set_cond_linear[of "\x. True" f I S] assms by auto ``` hoelzl@40887 ` 382` krauss@47446 ` 383` ```lemma set_times_Un_distrib: ``` krauss@47446 ` 384` ``` "A * (B \ C) = A * B \ A * C" ``` krauss@47446 ` 385` ``` "(A \ B) * C = A * C \ B * C" ``` wenzelm@56899 ` 386` ``` by (auto simp: set_times_def) ``` krauss@47446 ` 387` krauss@47446 ` 388` ```lemma set_times_UNION_distrib: ``` wenzelm@56899 ` 389` ``` "A * UNION I M = (\i\I. A * M i)" ``` wenzelm@56899 ` 390` ``` "UNION I M * A = (\i\I. M i * A)" ``` wenzelm@56899 ` 391` ``` by (auto simp: set_times_def) ``` krauss@47446 ` 392` avigad@16908 ` 393` ```end ```