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