src/HOL/Library/Set_Idioms.thy
 author haftmann Sun Nov 18 18:07:51 2018 +0000 (7 months ago) changeset 69313 b021008c5397 parent 69004 f6a0c8115e9c child 69325 4b6ddc5989fc permissions -rw-r--r--
removed legacy input syntax
 lp15@69004 ` 1` ```(* Title: HOL/Library/Set_Idioms.thy ``` lp15@69004 ` 2` ``` Author: Lawrence Paulson (but borrowed from HOL Light) ``` lp15@69004 ` 3` ```*) ``` lp15@69004 ` 4` lp15@69004 ` 5` ```section \Set Idioms\ ``` lp15@69004 ` 6` lp15@69004 ` 7` ```theory Set_Idioms ``` lp15@69004 ` 8` ```imports Countable_Set ``` lp15@69004 ` 9` lp15@69004 ` 10` ```begin ``` lp15@69004 ` 11` lp15@69004 ` 12` lp15@69004 ` 13` ```subsection\Idioms for being a suitable union/intersection of something\ ``` lp15@69004 ` 14` lp15@69004 ` 15` ```definition union_of :: "('a set set \ bool) \ ('a set \ bool) \ 'a set \ bool" ``` lp15@69004 ` 16` ``` (infixr "union'_of" 60) ``` lp15@69004 ` 17` ``` where "P union_of Q \ \S. \\. P \ \ \ \ Collect Q \ \\ = S" ``` lp15@69004 ` 18` lp15@69004 ` 19` ```definition intersection_of :: "('a set set \ bool) \ ('a set \ bool) \ 'a set \ bool" ``` lp15@69004 ` 20` ``` (infixr "intersection'_of" 60) ``` lp15@69004 ` 21` ``` where "P intersection_of Q \ \S. \\. P \ \ \ \ Collect Q \ \\ = S" ``` lp15@69004 ` 22` lp15@69004 ` 23` ```definition arbitrary:: "'a set set \ bool" where "arbitrary \ \ True" ``` lp15@69004 ` 24` lp15@69004 ` 25` ```lemma union_of_inc: "\P {S}; Q S\ \ (P union_of Q) S" ``` lp15@69004 ` 26` ``` by (auto simp: union_of_def) ``` lp15@69004 ` 27` lp15@69004 ` 28` ```lemma intersection_of_inc: ``` lp15@69004 ` 29` ``` "\P {S}; Q S\ \ (P intersection_of Q) S" ``` lp15@69004 ` 30` ``` by (auto simp: intersection_of_def) ``` lp15@69004 ` 31` lp15@69004 ` 32` ```lemma union_of_mono: ``` lp15@69004 ` 33` ``` "\(P union_of Q) S; \x. Q x \ Q' x\ \ (P union_of Q') S" ``` lp15@69004 ` 34` ``` by (auto simp: union_of_def) ``` lp15@69004 ` 35` lp15@69004 ` 36` ```lemma intersection_of_mono: ``` lp15@69004 ` 37` ``` "\(P intersection_of Q) S; \x. Q x \ Q' x\ \ (P intersection_of Q') S" ``` lp15@69004 ` 38` ``` by (auto simp: intersection_of_def) ``` lp15@69004 ` 39` lp15@69004 ` 40` ```lemma all_union_of: ``` lp15@69004 ` 41` ``` "(\S. (P union_of Q) S \ R S) \ (\T. P T \ T \ Collect Q \ R(\T))" ``` lp15@69004 ` 42` ``` by (auto simp: union_of_def) ``` lp15@69004 ` 43` lp15@69004 ` 44` ```lemma all_intersection_of: ``` lp15@69004 ` 45` ``` "(\S. (P intersection_of Q) S \ R S) \ (\T. P T \ T \ Collect Q \ R(\T))" ``` lp15@69004 ` 46` ``` by (auto simp: intersection_of_def) ``` lp15@69004 ` 47` lp15@69004 ` 48` ```lemma union_of_empty: ``` lp15@69004 ` 49` ``` "P {} \ (P union_of Q) {}" ``` lp15@69004 ` 50` ``` by (auto simp: union_of_def) ``` lp15@69004 ` 51` lp15@69004 ` 52` ```lemma intersection_of_empty: ``` lp15@69004 ` 53` ``` "P {} \ (P intersection_of Q) UNIV" ``` lp15@69004 ` 54` ``` by (auto simp: intersection_of_def) ``` lp15@69004 ` 55` lp15@69004 ` 56` ```text\ The arbitrary and finite cases\ ``` lp15@69004 ` 57` lp15@69004 ` 58` ```lemma arbitrary_union_of_alt: ``` lp15@69004 ` 59` ``` "(arbitrary union_of Q) S \ (\x \ S. \U. Q U \ x \ U \ U \ S)" ``` lp15@69004 ` 60` ``` (is "?lhs = ?rhs") ``` lp15@69004 ` 61` ```proof ``` lp15@69004 ` 62` ``` assume ?lhs ``` lp15@69004 ` 63` ``` then show ?rhs ``` lp15@69004 ` 64` ``` by (force simp: union_of_def arbitrary_def) ``` lp15@69004 ` 65` ```next ``` lp15@69004 ` 66` ``` assume ?rhs ``` lp15@69004 ` 67` ``` then have "{U. Q U \ U \ S} \ Collect Q" "\{U. Q U \ U \ S} = S" ``` lp15@69004 ` 68` ``` by auto ``` lp15@69004 ` 69` ``` then show ?lhs ``` lp15@69004 ` 70` ``` unfolding union_of_def arbitrary_def by blast ``` lp15@69004 ` 71` ```qed ``` lp15@69004 ` 72` lp15@69004 ` 73` ```lemma arbitrary_union_of_empty [simp]: "(arbitrary union_of P) {}" ``` lp15@69004 ` 74` ``` by (force simp: union_of_def arbitrary_def) ``` lp15@69004 ` 75` lp15@69004 ` 76` ```lemma arbitrary_intersection_of_empty [simp]: ``` lp15@69004 ` 77` ``` "(arbitrary intersection_of P) UNIV" ``` lp15@69004 ` 78` ``` by (force simp: intersection_of_def arbitrary_def) ``` lp15@69004 ` 79` lp15@69004 ` 80` ```lemma arbitrary_union_of_inc: ``` lp15@69004 ` 81` ``` "P S \ (arbitrary union_of P) S" ``` lp15@69004 ` 82` ``` by (force simp: union_of_inc arbitrary_def) ``` lp15@69004 ` 83` lp15@69004 ` 84` ```lemma arbitrary_intersection_of_inc: ``` lp15@69004 ` 85` ``` "P S \ (arbitrary intersection_of P) S" ``` lp15@69004 ` 86` ``` by (force simp: intersection_of_inc arbitrary_def) ``` lp15@69004 ` 87` lp15@69004 ` 88` ```lemma arbitrary_union_of_complement: ``` lp15@69004 ` 89` ``` "(arbitrary union_of P) S \ (arbitrary intersection_of (\S. P(- S))) (- S)" (is "?lhs = ?rhs") ``` lp15@69004 ` 90` ```proof ``` lp15@69004 ` 91` ``` assume ?lhs ``` lp15@69004 ` 92` ``` then obtain \ where "\ \ Collect P" "S = \\" ``` lp15@69004 ` 93` ``` by (auto simp: union_of_def arbitrary_def) ``` lp15@69004 ` 94` ``` then show ?rhs ``` lp15@69004 ` 95` ``` unfolding intersection_of_def arbitrary_def ``` lp15@69004 ` 96` ``` by (rule_tac x="uminus ` \" in exI) auto ``` lp15@69004 ` 97` ```next ``` lp15@69004 ` 98` ``` assume ?rhs ``` lp15@69004 ` 99` ``` then obtain \ where "\ \ {S. P (- S)}" "\\ = - S" ``` lp15@69004 ` 100` ``` by (auto simp: union_of_def intersection_of_def arbitrary_def) ``` lp15@69004 ` 101` ``` then show ?lhs ``` lp15@69004 ` 102` ``` unfolding union_of_def arbitrary_def ``` lp15@69004 ` 103` ``` by (rule_tac x="uminus ` \" in exI) auto ``` lp15@69004 ` 104` ```qed ``` lp15@69004 ` 105` lp15@69004 ` 106` ```lemma arbitrary_intersection_of_complement: ``` lp15@69004 ` 107` ``` "(arbitrary intersection_of P) S \ (arbitrary union_of (\S. P(- S))) (- S)" ``` lp15@69004 ` 108` ``` by (simp add: arbitrary_union_of_complement) ``` lp15@69004 ` 109` lp15@69004 ` 110` ```lemma arbitrary_union_of_idempot [simp]: ``` lp15@69004 ` 111` ``` "arbitrary union_of arbitrary union_of P = arbitrary union_of P" ``` lp15@69004 ` 112` ```proof - ``` lp15@69004 ` 113` ``` have 1: "\\'\Collect P. \\' = \\" if "\ \ {S. \\\Collect P. \\ = S}" for \ ``` lp15@69004 ` 114` ``` proof - ``` lp15@69004 ` 115` ``` let ?\ = "{V. \\. \\Collect P \ V \ \ \ (\S \ \. \\ = S)}" ``` lp15@69004 ` 116` ``` have *: "\x U. \x \ U; U \ \\ \ x \ \?\" ``` lp15@69004 ` 117` ``` using that ``` lp15@69004 ` 118` ``` apply simp ``` lp15@69004 ` 119` ``` apply (drule subsetD, assumption, auto) ``` lp15@69004 ` 120` ``` done ``` lp15@69004 ` 121` ``` show ?thesis ``` lp15@69004 ` 122` ``` apply (rule_tac x="{V. \\. \\Collect P \ V \ \ \ (\S \ \. \\ = S)}" in exI) ``` lp15@69004 ` 123` ``` using that by (blast intro: *) ``` lp15@69004 ` 124` ``` qed ``` lp15@69004 ` 125` ``` have 2: "\\'\{S. \\\Collect P. \\ = S}. \\' = \\" if "\ \ Collect P" for \ ``` lp15@69004 ` 126` ``` by (metis (mono_tags, lifting) union_of_def arbitrary_union_of_inc that) ``` lp15@69004 ` 127` ``` show ?thesis ``` lp15@69004 ` 128` ``` unfolding union_of_def arbitrary_def by (force simp: 1 2) ``` lp15@69004 ` 129` ```qed ``` lp15@69004 ` 130` lp15@69004 ` 131` ```lemma arbitrary_intersection_of_idempot: ``` lp15@69004 ` 132` ``` "arbitrary intersection_of arbitrary intersection_of P = arbitrary intersection_of P" (is "?lhs = ?rhs") ``` lp15@69004 ` 133` ```proof - ``` lp15@69004 ` 134` ``` have "- ?lhs = - ?rhs" ``` lp15@69004 ` 135` ``` unfolding arbitrary_intersection_of_complement by simp ``` lp15@69004 ` 136` ``` then show ?thesis ``` lp15@69004 ` 137` ``` by simp ``` lp15@69004 ` 138` ```qed ``` lp15@69004 ` 139` lp15@69004 ` 140` ```lemma arbitrary_union_of_Union: ``` lp15@69004 ` 141` ``` "(\S. S \ \ \ (arbitrary union_of P) S) \ (arbitrary union_of P) (\\)" ``` lp15@69004 ` 142` ``` by (metis union_of_def arbitrary_def arbitrary_union_of_idempot mem_Collect_eq subsetI) ``` lp15@69004 ` 143` lp15@69004 ` 144` ```lemma arbitrary_union_of_Un: ``` lp15@69004 ` 145` ``` "\(arbitrary union_of P) S; (arbitrary union_of P) T\ ``` lp15@69004 ` 146` ``` \ (arbitrary union_of P) (S \ T)" ``` lp15@69004 ` 147` ``` using arbitrary_union_of_Union [of "{S,T}"] by auto ``` lp15@69004 ` 148` lp15@69004 ` 149` ```lemma arbitrary_intersection_of_Inter: ``` lp15@69004 ` 150` ``` "(\S. S \ \ \ (arbitrary intersection_of P) S) \ (arbitrary intersection_of P) (\\)" ``` lp15@69004 ` 151` ``` by (metis intersection_of_def arbitrary_def arbitrary_intersection_of_idempot mem_Collect_eq subsetI) ``` lp15@69004 ` 152` lp15@69004 ` 153` ```lemma arbitrary_intersection_of_Int: ``` lp15@69004 ` 154` ``` "\(arbitrary intersection_of P) S; (arbitrary intersection_of P) T\ ``` lp15@69004 ` 155` ``` \ (arbitrary intersection_of P) (S \ T)" ``` lp15@69004 ` 156` ``` using arbitrary_intersection_of_Inter [of "{S,T}"] by auto ``` lp15@69004 ` 157` lp15@69004 ` 158` ```lemma arbitrary_union_of_Int_eq: ``` lp15@69004 ` 159` ``` "(\S T. (arbitrary union_of P) S \ (arbitrary union_of P) T ``` lp15@69004 ` 160` ``` \ (arbitrary union_of P) (S \ T)) ``` lp15@69004 ` 161` ``` \ (\S T. P S \ P T \ (arbitrary union_of P) (S \ T))" (is "?lhs = ?rhs") ``` lp15@69004 ` 162` ```proof ``` lp15@69004 ` 163` ``` assume ?lhs ``` lp15@69004 ` 164` ``` then show ?rhs ``` lp15@69004 ` 165` ``` by (simp add: arbitrary_union_of_inc) ``` lp15@69004 ` 166` ```next ``` lp15@69004 ` 167` ``` assume R: ?rhs ``` lp15@69004 ` 168` ``` show ?lhs ``` lp15@69004 ` 169` ``` proof clarify ``` lp15@69004 ` 170` ``` fix S :: "'a set" and T :: "'a set" ``` lp15@69004 ` 171` ``` assume "(arbitrary union_of P) S" and "(arbitrary union_of P) T" ``` lp15@69004 ` 172` ``` then obtain \ \ where *: "\ \ Collect P" "\\ = S" "\ \ Collect P" "\\ = T" ``` lp15@69004 ` 173` ``` by (auto simp: union_of_def) ``` lp15@69004 ` 174` ``` then have "(arbitrary union_of P) (\C\\. \D\\. C \ D)" ``` lp15@69004 ` 175` ``` using R by (blast intro: arbitrary_union_of_Union) ``` lp15@69004 ` 176` ``` then show "(arbitrary union_of P) (S \ T)" ``` lp15@69004 ` 177` ``` by (simp add: Int_UN_distrib2 *) ``` lp15@69004 ` 178` ``` qed ``` lp15@69004 ` 179` ```qed ``` lp15@69004 ` 180` lp15@69004 ` 181` ```lemma arbitrary_intersection_of_Un_eq: ``` lp15@69004 ` 182` ``` "(\S T. (arbitrary intersection_of P) S \ (arbitrary intersection_of P) T ``` lp15@69004 ` 183` ``` \ (arbitrary intersection_of P) (S \ T)) \ ``` lp15@69004 ` 184` ``` (\S T. P S \ P T \ (arbitrary intersection_of P) (S \ T))" ``` lp15@69004 ` 185` ``` apply (simp add: arbitrary_intersection_of_complement) ``` lp15@69004 ` 186` ``` using arbitrary_union_of_Int_eq [of "\S. P (- S)"] ``` lp15@69004 ` 187` ``` by (metis (no_types, lifting) arbitrary_def double_compl union_of_inc) ``` lp15@69004 ` 188` lp15@69004 ` 189` ```lemma finite_union_of_empty [simp]: "(finite union_of P) {}" ``` lp15@69004 ` 190` ``` by (simp add: union_of_empty) ``` lp15@69004 ` 191` lp15@69004 ` 192` ```lemma finite_intersection_of_empty [simp]: "(finite intersection_of P) UNIV" ``` lp15@69004 ` 193` ``` by (simp add: intersection_of_empty) ``` lp15@69004 ` 194` lp15@69004 ` 195` ```lemma finite_union_of_inc: ``` lp15@69004 ` 196` ``` "P S \ (finite union_of P) S" ``` lp15@69004 ` 197` ``` by (simp add: union_of_inc) ``` lp15@69004 ` 198` lp15@69004 ` 199` ```lemma finite_intersection_of_inc: ``` lp15@69004 ` 200` ``` "P S \ (finite intersection_of P) S" ``` lp15@69004 ` 201` ``` by (simp add: intersection_of_inc) ``` lp15@69004 ` 202` lp15@69004 ` 203` ```lemma finite_union_of_complement: ``` lp15@69004 ` 204` ``` "(finite union_of P) S \ (finite intersection_of (\S. P(- S))) (- S)" ``` lp15@69004 ` 205` ``` unfolding union_of_def intersection_of_def ``` lp15@69004 ` 206` ``` apply safe ``` lp15@69004 ` 207` ``` apply (rule_tac x="uminus ` \" in exI, fastforce)+ ``` lp15@69004 ` 208` ``` done ``` lp15@69004 ` 209` lp15@69004 ` 210` ```lemma finite_intersection_of_complement: ``` lp15@69004 ` 211` ``` "(finite intersection_of P) S \ (finite union_of (\S. P(- S))) (- S)" ``` lp15@69004 ` 212` ``` by (simp add: finite_union_of_complement) ``` lp15@69004 ` 213` lp15@69004 ` 214` ```lemma finite_union_of_idempot [simp]: ``` lp15@69004 ` 215` ``` "finite union_of finite union_of P = finite union_of P" ``` lp15@69004 ` 216` ```proof - ``` lp15@69004 ` 217` ``` have "(finite union_of P) S" if S: "(finite union_of finite union_of P) S" for S ``` lp15@69004 ` 218` ``` proof - ``` lp15@69004 ` 219` ``` obtain \ where "finite \" "S = \\" and \: "\U\\. \\. finite \ \ (\ \ Collect P) \ \\ = U" ``` lp15@69004 ` 220` ``` using S unfolding union_of_def by (auto simp: subset_eq) ``` lp15@69004 ` 221` ``` then obtain f where "\U\\. finite (f U) \ (f U \ Collect P) \ \(f U) = U" ``` lp15@69004 ` 222` ``` by metis ``` lp15@69004 ` 223` ``` then show ?thesis ``` lp15@69004 ` 224` ``` unfolding union_of_def \S = \\\ ``` lp15@69004 ` 225` ``` by (rule_tac x = "snd ` Sigma \ f" in exI) (fastforce simp: \finite \\) ``` lp15@69004 ` 226` ``` qed ``` lp15@69004 ` 227` ``` moreover ``` lp15@69004 ` 228` ``` have "(finite union_of finite union_of P) S" if "(finite union_of P) S" for S ``` lp15@69004 ` 229` ``` by (simp add: finite_union_of_inc that) ``` lp15@69004 ` 230` ``` ultimately show ?thesis ``` lp15@69004 ` 231` ``` by force ``` lp15@69004 ` 232` ```qed ``` lp15@69004 ` 233` lp15@69004 ` 234` ```lemma finite_intersection_of_idempot [simp]: ``` lp15@69004 ` 235` ``` "finite intersection_of finite intersection_of P = finite intersection_of P" ``` lp15@69004 ` 236` ``` by (force simp: finite_intersection_of_complement) ``` lp15@69004 ` 237` lp15@69004 ` 238` ```lemma finite_union_of_Union: ``` lp15@69004 ` 239` ``` "\finite \; \S. S \ \ \ (finite union_of P) S\ \ (finite union_of P) (\\)" ``` lp15@69004 ` 240` ``` using finite_union_of_idempot [of P] ``` lp15@69004 ` 241` ``` by (metis mem_Collect_eq subsetI union_of_def) ``` lp15@69004 ` 242` lp15@69004 ` 243` ```lemma finite_union_of_Un: ``` lp15@69004 ` 244` ``` "\(finite union_of P) S; (finite union_of P) T\ \ (finite union_of P) (S \ T)" ``` lp15@69004 ` 245` ``` by (auto simp: union_of_def) ``` lp15@69004 ` 246` lp15@69004 ` 247` ```lemma finite_intersection_of_Inter: ``` lp15@69004 ` 248` ``` "\finite \; \S. S \ \ \ (finite intersection_of P) S\ \ (finite intersection_of P) (\\)" ``` lp15@69004 ` 249` ``` using finite_intersection_of_idempot [of P] ``` lp15@69004 ` 250` ``` by (metis intersection_of_def mem_Collect_eq subsetI) ``` lp15@69004 ` 251` lp15@69004 ` 252` ```lemma finite_intersection_of_Int: ``` lp15@69004 ` 253` ``` "\(finite intersection_of P) S; (finite intersection_of P) T\ ``` lp15@69004 ` 254` ``` \ (finite intersection_of P) (S \ T)" ``` lp15@69004 ` 255` ``` by (auto simp: intersection_of_def) ``` lp15@69004 ` 256` lp15@69004 ` 257` ```lemma finite_union_of_Int_eq: ``` lp15@69004 ` 258` ``` "(\S T. (finite union_of P) S \ (finite union_of P) T \ (finite union_of P) (S \ T)) ``` lp15@69004 ` 259` ``` \ (\S T. P S \ P T \ (finite union_of P) (S \ T))" ``` lp15@69004 ` 260` ```(is "?lhs = ?rhs") ``` lp15@69004 ` 261` ```proof ``` lp15@69004 ` 262` ``` assume ?lhs ``` lp15@69004 ` 263` ``` then show ?rhs ``` lp15@69004 ` 264` ``` by (simp add: finite_union_of_inc) ``` lp15@69004 ` 265` ```next ``` lp15@69004 ` 266` ``` assume R: ?rhs ``` lp15@69004 ` 267` ``` show ?lhs ``` lp15@69004 ` 268` ``` proof clarify ``` lp15@69004 ` 269` ``` fix S :: "'a set" and T :: "'a set" ``` lp15@69004 ` 270` ``` assume "(finite union_of P) S" and "(finite union_of P) T" ``` lp15@69004 ` 271` ``` then obtain \ \ where *: "\ \ Collect P" "\\ = S" "finite \" "\ \ Collect P" "\\ = T" "finite \" ``` lp15@69004 ` 272` ``` by (auto simp: union_of_def) ``` lp15@69004 ` 273` ``` then have "(finite union_of P) (\C\\. \D\\. C \ D)" ``` lp15@69004 ` 274` ``` using R ``` lp15@69004 ` 275` ``` by (blast intro: finite_union_of_Union) ``` lp15@69004 ` 276` ``` then show "(finite union_of P) (S \ T)" ``` lp15@69004 ` 277` ``` by (simp add: Int_UN_distrib2 *) ``` lp15@69004 ` 278` ``` qed ``` lp15@69004 ` 279` ```qed ``` lp15@69004 ` 280` lp15@69004 ` 281` ```lemma finite_intersection_of_Un_eq: ``` lp15@69004 ` 282` ``` "(\S T. (finite intersection_of P) S \ ``` lp15@69004 ` 283` ``` (finite intersection_of P) T ``` lp15@69004 ` 284` ``` \ (finite intersection_of P) (S \ T)) \ ``` lp15@69004 ` 285` ``` (\S T. P S \ P T \ (finite intersection_of P) (S \ T))" ``` lp15@69004 ` 286` ``` apply (simp add: finite_intersection_of_complement) ``` lp15@69004 ` 287` ``` using finite_union_of_Int_eq [of "\S. P (- S)"] ``` lp15@69004 ` 288` ``` by (metis (no_types, lifting) double_compl) ``` lp15@69004 ` 289` lp15@69004 ` 290` lp15@69004 ` 291` ```abbreviation finite' :: "'a set \ bool" ``` lp15@69004 ` 292` ``` where "finite' A \ finite A \ A \ {}" ``` lp15@69004 ` 293` lp15@69004 ` 294` ```lemma finite'_intersection_of_Int: ``` lp15@69004 ` 295` ``` "\(finite' intersection_of P) S; (finite' intersection_of P) T\ ``` lp15@69004 ` 296` ``` \ (finite' intersection_of P) (S \ T)" ``` lp15@69004 ` 297` ``` by (auto simp: intersection_of_def) ``` lp15@69004 ` 298` lp15@69004 ` 299` ```lemma finite'_intersection_of_inc: ``` lp15@69004 ` 300` ``` "P S \ (finite' intersection_of P) S" ``` lp15@69004 ` 301` ``` by (simp add: intersection_of_inc) ``` lp15@69004 ` 302` lp15@69004 ` 303` lp15@69004 ` 304` ```subsection \The ``Relative to'' operator\ ``` lp15@69004 ` 305` lp15@69004 ` 306` ```text\A somewhat cheap but handy way of getting localized forms of various topological concepts ``` lp15@69004 ` 307` ```(open, closed, borel, fsigma, gdelta etc.)\ ``` lp15@69004 ` 308` lp15@69004 ` 309` ```definition relative_to :: "['a set \ bool, 'a set, 'a set] \ bool" (infixl "relative'_to" 55) ``` lp15@69004 ` 310` ``` where "P relative_to S \ \T. \U. P U \ S \ U = T" ``` lp15@69004 ` 311` lp15@69004 ` 312` ```lemma relative_to_UNIV [simp]: "(P relative_to UNIV) S \ P S" ``` lp15@69004 ` 313` ``` by (simp add: relative_to_def) ``` lp15@69004 ` 314` lp15@69004 ` 315` ```lemma relative_to_imp_subset: ``` lp15@69004 ` 316` ``` "(P relative_to S) T \ T \ S" ``` lp15@69004 ` 317` ``` by (auto simp: relative_to_def) ``` lp15@69004 ` 318` lp15@69004 ` 319` ```lemma all_relative_to: "(\S. (P relative_to U) S \ Q S) \ (\S. P S \ Q(U \ S))" ``` lp15@69004 ` 320` ``` by (auto simp: relative_to_def) ``` lp15@69004 ` 321` lp15@69004 ` 322` ```lemma relative_to_inc: ``` lp15@69004 ` 323` ``` "P S \ (P relative_to U) (U \ S)" ``` lp15@69004 ` 324` ``` by (auto simp: relative_to_def) ``` lp15@69004 ` 325` lp15@69004 ` 326` ```lemma relative_to_relative_to [simp]: ``` lp15@69004 ` 327` ``` "P relative_to S relative_to T = P relative_to (S \ T)" ``` lp15@69004 ` 328` ``` unfolding relative_to_def ``` lp15@69004 ` 329` ``` by auto ``` lp15@69004 ` 330` lp15@69004 ` 331` ```lemma relative_to_compl: ``` lp15@69004 ` 332` ``` "S \ U \ ((P relative_to U) (U - S) \ ((\c. P(- c)) relative_to U) S)" ``` lp15@69004 ` 333` ``` unfolding relative_to_def ``` lp15@69004 ` 334` ``` by (metis Diff_Diff_Int Diff_eq double_compl inf.absorb_iff2) ``` lp15@69004 ` 335` lp15@69004 ` 336` ```lemma relative_to_subset: ``` lp15@69004 ` 337` ``` "S \ T \ P S \ (P relative_to T) S" ``` lp15@69004 ` 338` ``` unfolding relative_to_def by auto ``` lp15@69004 ` 339` lp15@69004 ` 340` ```lemma relative_to_subset_trans: ``` lp15@69004 ` 341` ``` "(P relative_to U) S \ S \ T \ T \ U \ (P relative_to T) S" ``` lp15@69004 ` 342` ``` unfolding relative_to_def by auto ``` lp15@69004 ` 343` lp15@69004 ` 344` ```lemma relative_to_mono: ``` lp15@69004 ` 345` ``` "\(P relative_to U) S; \S. P S \ Q S\ \ (Q relative_to U) S" ``` lp15@69004 ` 346` ``` unfolding relative_to_def by auto ``` lp15@69004 ` 347` lp15@69004 ` 348` ```lemma relative_to_subset_inc: "\S \ U; P S\ \ (P relative_to U) S" ``` lp15@69004 ` 349` ``` unfolding relative_to_def by auto ``` lp15@69004 ` 350` lp15@69004 ` 351` ```lemma relative_to_Int: ``` lp15@69004 ` 352` ``` "\(P relative_to S) C; (P relative_to S) D; \X Y. \P X; P Y\ \ P(X \ Y)\ ``` lp15@69004 ` 353` ``` \ (P relative_to S) (C \ D)" ``` lp15@69004 ` 354` ``` unfolding relative_to_def by auto ``` lp15@69004 ` 355` lp15@69004 ` 356` ```lemma relative_to_Un: ``` lp15@69004 ` 357` ``` "\(P relative_to S) C; (P relative_to S) D; \X Y. \P X; P Y\ \ P(X \ Y)\ ``` lp15@69004 ` 358` ``` \ (P relative_to S) (C \ D)" ``` lp15@69004 ` 359` ``` unfolding relative_to_def by auto ``` lp15@69004 ` 360` lp15@69004 ` 361` ```lemma arbitrary_union_of_relative_to: ``` lp15@69004 ` 362` ``` "((arbitrary union_of P) relative_to U) = (arbitrary union_of (P relative_to U))" (is "?lhs = ?rhs") ``` lp15@69004 ` 363` ```proof - ``` lp15@69004 ` 364` ``` have "?rhs S" if L: "?lhs S" for S ``` lp15@69004 ` 365` ``` proof - ``` lp15@69004 ` 366` ``` obtain \ where "S = U \ \\" "\ \ Collect P" ``` lp15@69004 ` 367` ``` using L unfolding relative_to_def union_of_def by auto ``` lp15@69004 ` 368` ``` then show ?thesis ``` lp15@69004 ` 369` ``` unfolding relative_to_def union_of_def arbitrary_def ``` lp15@69004 ` 370` ``` by (rule_tac x="(\X. U \ X) ` \" in exI) auto ``` lp15@69004 ` 371` ``` qed ``` lp15@69004 ` 372` ``` moreover have "?lhs S" if R: "?rhs S" for S ``` lp15@69004 ` 373` ``` proof - ``` lp15@69004 ` 374` ``` obtain \ where "S = \\" "\T\\. \V. P V \ U \ V = T" ``` lp15@69004 ` 375` ``` using R unfolding relative_to_def union_of_def by auto ``` lp15@69004 ` 376` ``` then obtain f where f: "\T. T \ \ \ P (f T)" "\T. T \ \ \ U \ (f T) = T" ``` lp15@69004 ` 377` ``` by metis ``` lp15@69004 ` 378` ``` then have "\\'\Collect P. \\' = UNION \ f" ``` lp15@69004 ` 379` ``` by (metis image_subset_iff mem_Collect_eq) ``` lp15@69004 ` 380` ``` moreover have eq: "U \ UNION \ f = \\" ``` lp15@69004 ` 381` ``` using f by auto ``` lp15@69004 ` 382` ``` ultimately show ?thesis ``` lp15@69004 ` 383` ``` unfolding relative_to_def union_of_def arbitrary_def \S = \\\ ``` lp15@69004 ` 384` ``` by metis ``` lp15@69004 ` 385` ``` qed ``` lp15@69004 ` 386` ``` ultimately show ?thesis ``` lp15@69004 ` 387` ``` by blast ``` lp15@69004 ` 388` ```qed ``` lp15@69004 ` 389` lp15@69004 ` 390` ```lemma finite_union_of_relative_to: ``` lp15@69004 ` 391` ``` "((finite union_of P) relative_to U) = (finite union_of (P relative_to U))" (is "?lhs = ?rhs") ``` lp15@69004 ` 392` ```proof - ``` lp15@69004 ` 393` ``` have "?rhs S" if L: "?lhs S" for S ``` lp15@69004 ` 394` ``` proof - ``` lp15@69004 ` 395` ``` obtain \ where "S = U \ \\" "\ \ Collect P" "finite \" ``` lp15@69004 ` 396` ``` using L unfolding relative_to_def union_of_def by auto ``` lp15@69004 ` 397` ``` then show ?thesis ``` lp15@69004 ` 398` ``` unfolding relative_to_def union_of_def ``` lp15@69004 ` 399` ``` by (rule_tac x="(\X. U \ X) ` \" in exI) auto ``` lp15@69004 ` 400` ``` qed ``` lp15@69004 ` 401` ``` moreover have "?lhs S" if R: "?rhs S" for S ``` lp15@69004 ` 402` ``` proof - ``` lp15@69004 ` 403` ``` obtain \ where "S = \\" "\T\\. \V. P V \ U \ V = T" "finite \" ``` lp15@69004 ` 404` ``` using R unfolding relative_to_def union_of_def by auto ``` lp15@69004 ` 405` ``` then obtain f where f: "\T. T \ \ \ P (f T)" "\T. T \ \ \ U \ (f T) = T" ``` lp15@69004 ` 406` ``` by metis ``` lp15@69004 ` 407` ``` then have "\\'\Collect P. \\' = UNION \ f" ``` lp15@69004 ` 408` ``` by (metis image_subset_iff mem_Collect_eq) ``` lp15@69004 ` 409` ``` moreover have eq: "U \ UNION \ f = \\" ``` lp15@69004 ` 410` ``` using f by auto ``` lp15@69004 ` 411` ``` ultimately show ?thesis ``` lp15@69004 ` 412` ``` using \finite \\ f ``` lp15@69004 ` 413` ``` unfolding relative_to_def union_of_def \S = \\\ ``` lp15@69004 ` 414` ``` by (rule_tac x="UNION \ f" in exI) (metis finite_imageI image_subsetI mem_Collect_eq) ``` lp15@69004 ` 415` ``` qed ``` lp15@69004 ` 416` ``` ultimately show ?thesis ``` lp15@69004 ` 417` ``` by blast ``` lp15@69004 ` 418` ```qed ``` lp15@69004 ` 419` lp15@69004 ` 420` ```lemma countable_union_of_relative_to: ``` lp15@69004 ` 421` ``` "((countable union_of P) relative_to U) = (countable union_of (P relative_to U))" (is "?lhs = ?rhs") ``` lp15@69004 ` 422` ```proof - ``` lp15@69004 ` 423` ``` have "?rhs S" if L: "?lhs S" for S ``` lp15@69004 ` 424` ``` proof - ``` lp15@69004 ` 425` ``` obtain \ where "S = U \ \\" "\ \ Collect P" "countable \" ``` lp15@69004 ` 426` ``` using L unfolding relative_to_def union_of_def by auto ``` lp15@69004 ` 427` ``` then show ?thesis ``` lp15@69004 ` 428` ``` unfolding relative_to_def union_of_def ``` lp15@69004 ` 429` ``` by (rule_tac x="(\X. U \ X) ` \" in exI) auto ``` lp15@69004 ` 430` ``` qed ``` lp15@69004 ` 431` ``` moreover have "?lhs S" if R: "?rhs S" for S ``` lp15@69004 ` 432` ``` proof - ``` lp15@69004 ` 433` ``` obtain \ where "S = \\" "\T\\. \V. P V \ U \ V = T" "countable \" ``` lp15@69004 ` 434` ``` using R unfolding relative_to_def union_of_def by auto ``` lp15@69004 ` 435` ``` then obtain f where f: "\T. T \ \ \ P (f T)" "\T. T \ \ \ U \ (f T) = T" ``` lp15@69004 ` 436` ``` by metis ``` lp15@69004 ` 437` ``` then have "\\'\Collect P. \\' = UNION \ f" ``` lp15@69004 ` 438` ``` by (metis image_subset_iff mem_Collect_eq) ``` lp15@69004 ` 439` ``` moreover have eq: "U \ UNION \ f = \\" ``` lp15@69004 ` 440` ``` using f by auto ``` lp15@69004 ` 441` ``` ultimately show ?thesis ``` lp15@69004 ` 442` ``` using \countable \\ f ``` lp15@69004 ` 443` ``` unfolding relative_to_def union_of_def \S = \\\ ``` lp15@69004 ` 444` ``` by (rule_tac x="UNION \ f" in exI) (metis countable_image image_subsetI mem_Collect_eq) ``` lp15@69004 ` 445` ``` qed ``` lp15@69004 ` 446` ``` ultimately show ?thesis ``` lp15@69004 ` 447` ``` by blast ``` lp15@69004 ` 448` ```qed ``` lp15@69004 ` 449` lp15@69004 ` 450` lp15@69004 ` 451` ```lemma arbitrary_intersection_of_relative_to: ``` lp15@69004 ` 452` ``` "((arbitrary intersection_of P) relative_to U) = ((arbitrary intersection_of (P relative_to U)) relative_to U)" (is "?lhs = ?rhs") ``` lp15@69004 ` 453` ```proof - ``` lp15@69004 ` 454` ``` have "?rhs S" if L: "?lhs S" for S ``` lp15@69004 ` 455` ``` proof - ``` lp15@69004 ` 456` ``` obtain \ where \: "S = U \ \\" "\ \ Collect P" ``` lp15@69004 ` 457` ``` using L unfolding relative_to_def intersection_of_def by auto ``` lp15@69004 ` 458` ``` show ?thesis ``` lp15@69004 ` 459` ``` unfolding relative_to_def intersection_of_def arbitrary_def ``` lp15@69004 ` 460` ``` proof (intro exI conjI) ``` lp15@69004 ` 461` ``` show "U \ (\X\\. U \ X) = S" "(\) U ` \ \ {T. \Ua. P Ua \ U \ Ua = T}" ``` lp15@69004 ` 462` ``` using \ by blast+ ``` lp15@69004 ` 463` ``` qed auto ``` lp15@69004 ` 464` ``` qed ``` lp15@69004 ` 465` ``` moreover have "?lhs S" if R: "?rhs S" for S ``` lp15@69004 ` 466` ``` proof - ``` lp15@69004 ` 467` ``` obtain \ where "S = U \ \\" "\T\\. \V. P V \ U \ V = T" ``` lp15@69004 ` 468` ``` using R unfolding relative_to_def intersection_of_def by auto ``` lp15@69004 ` 469` ``` then obtain f where f: "\T. T \ \ \ P (f T)" "\T. T \ \ \ U \ (f T) = T" ``` lp15@69004 ` 470` ``` by metis ``` haftmann@69313 ` 471` ``` then have "f ` \ \ Collect P" ``` haftmann@69313 ` 472` ``` by auto ``` haftmann@69313 ` 473` ``` moreover have eq: "U \ \(f ` \) = U \ \\" ``` lp15@69004 ` 474` ``` using f by auto ``` lp15@69004 ` 475` ``` ultimately show ?thesis ``` lp15@69004 ` 476` ``` unfolding relative_to_def intersection_of_def arbitrary_def \S = U \ \\\ ``` haftmann@69313 ` 477` ``` by auto ``` lp15@69004 ` 478` ``` qed ``` lp15@69004 ` 479` ``` ultimately show ?thesis ``` lp15@69004 ` 480` ``` by blast ``` lp15@69004 ` 481` ```qed ``` lp15@69004 ` 482` lp15@69004 ` 483` ```lemma finite_intersection_of_relative_to: ``` lp15@69004 ` 484` ``` "((finite intersection_of P) relative_to U) = ((finite intersection_of (P relative_to U)) relative_to U)" (is "?lhs = ?rhs") ``` lp15@69004 ` 485` ```proof - ``` lp15@69004 ` 486` ``` have "?rhs S" if L: "?lhs S" for S ``` lp15@69004 ` 487` ``` proof - ``` lp15@69004 ` 488` ``` obtain \ where \: "S = U \ \\" "\ \ Collect P" "finite \" ``` lp15@69004 ` 489` ``` using L unfolding relative_to_def intersection_of_def by auto ``` lp15@69004 ` 490` ``` show ?thesis ``` lp15@69004 ` 491` ``` unfolding relative_to_def intersection_of_def ``` lp15@69004 ` 492` ``` proof (intro exI conjI) ``` lp15@69004 ` 493` ``` show "U \ (\X\\. U \ X) = S" "(\) U ` \ \ {T. \Ua. P Ua \ U \ Ua = T}" ``` lp15@69004 ` 494` ``` using \ by blast+ ``` lp15@69004 ` 495` ``` show "finite ((\) U ` \)" ``` lp15@69004 ` 496` ``` by (simp add: \finite \\) ``` lp15@69004 ` 497` ``` qed auto ``` lp15@69004 ` 498` ``` qed ``` lp15@69004 ` 499` ``` moreover have "?lhs S" if R: "?rhs S" for S ``` lp15@69004 ` 500` ``` proof - ``` lp15@69004 ` 501` ``` obtain \ where "S = U \ \\" "\T\\. \V. P V \ U \ V = T" "finite \" ``` lp15@69004 ` 502` ``` using R unfolding relative_to_def intersection_of_def by auto ``` lp15@69004 ` 503` ``` then obtain f where f: "\T. T \ \ \ P (f T)" "\T. T \ \ \ U \ (f T) = T" ``` lp15@69004 ` 504` ``` by metis ``` haftmann@69313 ` 505` ``` then have "f ` \ \ Collect P" ``` haftmann@69313 ` 506` ``` by auto ``` haftmann@69313 ` 507` ``` moreover have eq: "U \ \ (f ` \) = U \ \ \" ``` lp15@69004 ` 508` ``` using f by auto ``` lp15@69004 ` 509` ``` ultimately show ?thesis ``` lp15@69004 ` 510` ``` unfolding relative_to_def intersection_of_def \S = U \ \\\ ``` haftmann@69313 ` 511` ``` using \finite \\ ``` haftmann@69313 ` 512` ``` by auto ``` lp15@69004 ` 513` ``` qed ``` lp15@69004 ` 514` ``` ultimately show ?thesis ``` lp15@69004 ` 515` ``` by blast ``` lp15@69004 ` 516` ```qed ``` lp15@69004 ` 517` lp15@69004 ` 518` ```lemma countable_intersection_of_relative_to: ``` lp15@69004 ` 519` ``` "((countable intersection_of P) relative_to U) = ((countable intersection_of (P relative_to U)) relative_to U)" (is "?lhs = ?rhs") ``` lp15@69004 ` 520` ```proof - ``` lp15@69004 ` 521` ``` have "?rhs S" if L: "?lhs S" for S ``` lp15@69004 ` 522` ``` proof - ``` lp15@69004 ` 523` ``` obtain \ where \: "S = U \ \\" "\ \ Collect P" "countable \" ``` lp15@69004 ` 524` ``` using L unfolding relative_to_def intersection_of_def by auto ``` lp15@69004 ` 525` ``` show ?thesis ``` lp15@69004 ` 526` ``` unfolding relative_to_def intersection_of_def ``` lp15@69004 ` 527` ``` proof (intro exI conjI) ``` lp15@69004 ` 528` ``` show "U \ (\X\\. U \ X) = S" "(\) U ` \ \ {T. \Ua. P Ua \ U \ Ua = T}" ``` lp15@69004 ` 529` ``` using \ by blast+ ``` lp15@69004 ` 530` ``` show "countable ((\) U ` \)" ``` lp15@69004 ` 531` ``` by (simp add: \countable \\) ``` lp15@69004 ` 532` ``` qed auto ``` lp15@69004 ` 533` ``` qed ``` lp15@69004 ` 534` ``` moreover have "?lhs S" if R: "?rhs S" for S ``` lp15@69004 ` 535` ``` proof - ``` lp15@69004 ` 536` ``` obtain \ where "S = U \ \\" "\T\\. \V. P V \ U \ V = T" "countable \" ``` lp15@69004 ` 537` ``` using R unfolding relative_to_def intersection_of_def by auto ``` lp15@69004 ` 538` ``` then obtain f where f: "\T. T \ \ \ P (f T)" "\T. T \ \ \ U \ (f T) = T" ``` lp15@69004 ` 539` ``` by metis ``` haftmann@69313 ` 540` ``` then have "f ` \ \ Collect P" ``` haftmann@69313 ` 541` ``` by auto ``` haftmann@69313 ` 542` ``` moreover have eq: "U \ \ (f ` \) = U \ \ \" ``` lp15@69004 ` 543` ``` using f by auto ``` lp15@69004 ` 544` ``` ultimately show ?thesis ``` lp15@69004 ` 545` ``` unfolding relative_to_def intersection_of_def \S = U \ \\\ ``` haftmann@69313 ` 546` ``` using \countable \\ countable_image ``` haftmann@69313 ` 547` ``` by auto ``` lp15@69004 ` 548` ``` qed ``` lp15@69004 ` 549` ``` ultimately show ?thesis ``` lp15@69004 ` 550` ``` by blast ``` lp15@69004 ` 551` ```qed ``` lp15@69004 ` 552` lp15@69004 ` 553` ```end ```