1section \<open>Extending FOL by a modified version of HOL set theory\<close> 2 3theory Set 4imports FOL 5begin 6 7declare [[eta_contract]] 8 9typedecl 'a set 10instance set :: ("term") "term" .. 11 12 13subsection \<open>Set comprehension and membership\<close> 14 15axiomatization Collect :: "['a \<Rightarrow> o] \<Rightarrow> 'a set" 16 and mem :: "['a, 'a set] \<Rightarrow> o" (infixl ":" 50) 17where mem_Collect_iff: "(a : Collect(P)) \<longleftrightarrow> P(a)" 18 and set_extension: "A = B \<longleftrightarrow> (ALL x. x:A \<longleftrightarrow> x:B)" 19 20syntax 21 "_Coll" :: "[idt, o] \<Rightarrow> 'a set" ("(1{_./ _})") 22translations 23 "{x. P}" == "CONST Collect(\<lambda>x. P)" 24 25lemma CollectI: "P(a) \<Longrightarrow> a : {x. P(x)}" 26 apply (rule mem_Collect_iff [THEN iffD2]) 27 apply assumption 28 done 29 30lemma CollectD: "a : {x. P(x)} \<Longrightarrow> P(a)" 31 apply (erule mem_Collect_iff [THEN iffD1]) 32 done 33 34lemmas CollectE = CollectD [elim_format] 35 36lemma set_ext: "(\<And>x. x:A \<longleftrightarrow> x:B) \<Longrightarrow> A = B" 37 apply (rule set_extension [THEN iffD2]) 38 apply simp 39 done 40 41 42subsection \<open>Bounded quantifiers\<close> 43 44definition Ball :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> o" 45 where "Ball(A, P) == ALL x. x:A \<longrightarrow> P(x)" 46 47definition Bex :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> o" 48 where "Bex(A, P) == EX x. x:A \<and> P(x)" 49 50syntax 51 "_Ball" :: "[idt, 'a set, o] \<Rightarrow> o" ("(ALL _:_./ _)" [0, 0, 0] 10) 52 "_Bex" :: "[idt, 'a set, o] \<Rightarrow> o" ("(EX _:_./ _)" [0, 0, 0] 10) 53translations 54 "ALL x:A. P" == "CONST Ball(A, \<lambda>x. P)" 55 "EX x:A. P" == "CONST Bex(A, \<lambda>x. P)" 56 57lemma ballI: "(\<And>x. x:A \<Longrightarrow> P(x)) \<Longrightarrow> ALL x:A. P(x)" 58 by (simp add: Ball_def) 59 60lemma bspec: "\<lbrakk>ALL x:A. P(x); x:A\<rbrakk> \<Longrightarrow> P(x)" 61 by (simp add: Ball_def) 62 63lemma ballE: "\<lbrakk>ALL x:A. P(x); P(x) \<Longrightarrow> Q; \<not> x:A \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" 64 unfolding Ball_def by blast 65 66lemma bexI: "\<lbrakk>P(x); x:A\<rbrakk> \<Longrightarrow> EX x:A. P(x)" 67 unfolding Bex_def by blast 68 69lemma bexCI: "\<lbrakk>EX x:A. \<not>P(x) \<Longrightarrow> P(a); a:A\<rbrakk> \<Longrightarrow> EX x:A. P(x)" 70 unfolding Bex_def by blast 71 72lemma bexE: "\<lbrakk>EX x:A. P(x); \<And>x. \<lbrakk>x:A; P(x)\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" 73 unfolding Bex_def by blast 74 75(*Trival rewrite rule; (! x:A.P)=P holds only if A is nonempty!*) 76lemma ball_rew: "(ALL x:A. True) \<longleftrightarrow> True" 77 by (blast intro: ballI) 78 79subsubsection \<open>Congruence rules\<close> 80 81lemma ball_cong: 82 "\<lbrakk>A = A'; \<And>x. x:A' \<Longrightarrow> P(x) \<longleftrightarrow> P'(x)\<rbrakk> \<Longrightarrow> 83 (ALL x:A. P(x)) \<longleftrightarrow> (ALL x:A'. P'(x))" 84 by (blast intro: ballI elim: ballE) 85 86lemma bex_cong: 87 "\<lbrakk>A = A'; \<And>x. x:A' \<Longrightarrow> P(x) \<longleftrightarrow> P'(x)\<rbrakk> \<Longrightarrow> 88 (EX x:A. P(x)) \<longleftrightarrow> (EX x:A'. P'(x))" 89 by (blast intro: bexI elim: bexE) 90 91 92subsection \<open>Further operations\<close> 93 94definition subset :: "['a set, 'a set] \<Rightarrow> o" (infixl "<=" 50) 95 where "A <= B == ALL x:A. x:B" 96 97definition mono :: "['a set \<Rightarrow> 'b set] \<Rightarrow> o" 98 where "mono(f) == (ALL A B. A <= B \<longrightarrow> f(A) <= f(B))" 99 100definition singleton :: "'a \<Rightarrow> 'a set" ("{_}") 101 where "{a} == {x. x=a}" 102 103definition empty :: "'a set" ("{}") 104 where "{} == {x. False}" 105 106definition Un :: "['a set, 'a set] \<Rightarrow> 'a set" (infixl "Un" 65) 107 where "A Un B == {x. x:A | x:B}" 108 109definition Int :: "['a set, 'a set] \<Rightarrow> 'a set" (infixl "Int" 70) 110 where "A Int B == {x. x:A \<and> x:B}" 111 112definition Compl :: "('a set) \<Rightarrow> 'a set" 113 where "Compl(A) == {x. \<not>x:A}" 114 115 116subsection \<open>Big Intersection / Union\<close> 117 118definition INTER :: "['a set, 'a \<Rightarrow> 'b set] \<Rightarrow> 'b set" 119 where "INTER(A, B) == {y. ALL x:A. y: B(x)}" 120 121definition UNION :: "['a set, 'a \<Rightarrow> 'b set] \<Rightarrow> 'b set" 122 where "UNION(A, B) == {y. EX x:A. y: B(x)}" 123 124syntax 125 "_INTER" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set" ("(INT _:_./ _)" [0, 0, 0] 10) 126 "_UNION" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set" ("(UN _:_./ _)" [0, 0, 0] 10) 127translations 128 "INT x:A. B" == "CONST INTER(A, \<lambda>x. B)" 129 "UN x:A. B" == "CONST UNION(A, \<lambda>x. B)" 130 131definition Inter :: "(('a set)set) \<Rightarrow> 'a set" 132 where "Inter(S) == (INT x:S. x)" 133 134definition Union :: "(('a set)set) \<Rightarrow> 'a set" 135 where "Union(S) == (UN x:S. x)" 136 137 138subsection \<open>Rules for subsets\<close> 139 140lemma subsetI: "(\<And>x. x:A \<Longrightarrow> x:B) \<Longrightarrow> A <= B" 141 unfolding subset_def by (blast intro: ballI) 142 143(*Rule in Modus Ponens style*) 144lemma subsetD: "\<lbrakk>A <= B; c:A\<rbrakk> \<Longrightarrow> c:B" 145 unfolding subset_def by (blast elim: ballE) 146 147(*Classical elimination rule*) 148lemma subsetCE: "\<lbrakk>A <= B; \<not>(c:A) \<Longrightarrow> P; c:B \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 149 by (blast dest: subsetD) 150 151lemma subset_refl: "A <= A" 152 by (blast intro: subsetI) 153 154lemma subset_trans: "\<lbrakk>A <= B; B <= C\<rbrakk> \<Longrightarrow> A <= C" 155 by (blast intro: subsetI dest: subsetD) 156 157 158subsection \<open>Rules for equality\<close> 159 160(*Anti-symmetry of the subset relation*) 161lemma subset_antisym: "\<lbrakk>A <= B; B <= A\<rbrakk> \<Longrightarrow> A = B" 162 by (blast intro: set_ext dest: subsetD) 163 164lemmas equalityI = subset_antisym 165 166(* Equality rules from ZF set theory -- are they appropriate here? *) 167lemma equalityD1: "A = B \<Longrightarrow> A<=B" 168 and equalityD2: "A = B \<Longrightarrow> B<=A" 169 by (simp_all add: subset_refl) 170 171lemma equalityE: "\<lbrakk>A = B; \<lbrakk>A <= B; B <= A\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 172 by (simp add: subset_refl) 173 174lemma equalityCE: "\<lbrakk>A = B; \<lbrakk>c:A; c:B\<rbrakk> \<Longrightarrow> P; \<lbrakk>\<not> c:A; \<not> c:B\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 175 by (blast elim: equalityE subsetCE) 176 177lemma trivial_set: "{x. x:A} = A" 178 by (blast intro: equalityI subsetI CollectI dest: CollectD) 179 180 181subsection \<open>Rules for binary union\<close> 182 183lemma UnI1: "c:A \<Longrightarrow> c : A Un B" 184 and UnI2: "c:B \<Longrightarrow> c : A Un B" 185 unfolding Un_def by (blast intro: CollectI)+ 186 187(*Classical introduction rule: no commitment to A vs B*) 188lemma UnCI: "(\<not>c:B \<Longrightarrow> c:A) \<Longrightarrow> c : A Un B" 189 by (blast intro: UnI1 UnI2) 190 191lemma UnE: "\<lbrakk>c : A Un B; c:A \<Longrightarrow> P; c:B \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 192 unfolding Un_def by (blast dest: CollectD) 193 194 195subsection \<open>Rules for small intersection\<close> 196 197lemma IntI: "\<lbrakk>c:A; c:B\<rbrakk> \<Longrightarrow> c : A Int B" 198 unfolding Int_def by (blast intro: CollectI) 199 200lemma IntD1: "c : A Int B \<Longrightarrow> c:A" 201 and IntD2: "c : A Int B \<Longrightarrow> c:B" 202 unfolding Int_def by (blast dest: CollectD)+ 203 204lemma IntE: "\<lbrakk>c : A Int B; \<lbrakk>c:A; c:B\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 205 by (blast dest: IntD1 IntD2) 206 207 208subsection \<open>Rules for set complement\<close> 209 210lemma ComplI: "(c:A \<Longrightarrow> False) \<Longrightarrow> c : Compl(A)" 211 unfolding Compl_def by (blast intro: CollectI) 212 213(*This form, with negated conclusion, works well with the Classical prover. 214 Negated assumptions behave like formulae on the right side of the notional 215 turnstile...*) 216lemma ComplD: "c : Compl(A) \<Longrightarrow> \<not>c:A" 217 unfolding Compl_def by (blast dest: CollectD) 218 219lemmas ComplE = ComplD [elim_format] 220 221 222subsection \<open>Empty sets\<close> 223 224lemma empty_eq: "{x. False} = {}" 225 by (simp add: empty_def) 226 227lemma emptyD: "a : {} \<Longrightarrow> P" 228 unfolding empty_def by (blast dest: CollectD) 229 230lemmas emptyE = emptyD [elim_format] 231 232lemma not_emptyD: 233 assumes "\<not> A={}" 234 shows "EX x. x:A" 235proof - 236 have "\<not> (EX x. x:A) \<Longrightarrow> A = {}" 237 by (rule equalityI) (blast intro!: subsetI elim!: emptyD)+ 238 with assms show ?thesis by blast 239qed 240 241 242subsection \<open>Singleton sets\<close> 243 244lemma singletonI: "a : {a}" 245 unfolding singleton_def by (blast intro: CollectI) 246 247lemma singletonD: "b : {a} \<Longrightarrow> b=a" 248 unfolding singleton_def by (blast dest: CollectD) 249 250lemmas singletonE = singletonD [elim_format] 251 252 253subsection \<open>Unions of families\<close> 254 255(*The order of the premises presupposes that A is rigid; b may be flexible*) 256lemma UN_I: "\<lbrakk>a:A; b: B(a)\<rbrakk> \<Longrightarrow> b: (UN x:A. B(x))" 257 unfolding UNION_def by (blast intro: bexI CollectI) 258 259lemma UN_E: "\<lbrakk>b : (UN x:A. B(x)); \<And>x. \<lbrakk>x:A; b: B(x)\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" 260 unfolding UNION_def by (blast dest: CollectD elim: bexE) 261 262lemma UN_cong: "\<lbrakk>A = B; \<And>x. x:B \<Longrightarrow> C(x) = D(x)\<rbrakk> \<Longrightarrow> (UN x:A. C(x)) = (UN x:B. D(x))" 263 by (simp add: UNION_def cong: bex_cong) 264 265 266subsection \<open>Intersections of families\<close> 267 268lemma INT_I: "(\<And>x. x:A \<Longrightarrow> b: B(x)) \<Longrightarrow> b : (INT x:A. B(x))" 269 unfolding INTER_def by (blast intro: CollectI ballI) 270 271lemma INT_D: "\<lbrakk>b : (INT x:A. B(x)); a:A\<rbrakk> \<Longrightarrow> b: B(a)" 272 unfolding INTER_def by (blast dest: CollectD bspec) 273 274(*"Classical" elimination rule -- does not require proving X:C *) 275lemma INT_E: "\<lbrakk>b : (INT x:A. B(x)); b: B(a) \<Longrightarrow> R; \<not> a:A \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" 276 unfolding INTER_def by (blast dest: CollectD bspec) 277 278lemma INT_cong: "\<lbrakk>A = B; \<And>x. x:B \<Longrightarrow> C(x) = D(x)\<rbrakk> \<Longrightarrow> (INT x:A. C(x)) = (INT x:B. D(x))" 279 by (simp add: INTER_def cong: ball_cong) 280 281 282subsection \<open>Rules for Unions\<close> 283 284(*The order of the premises presupposes that C is rigid; A may be flexible*) 285lemma UnionI: "\<lbrakk>X:C; A:X\<rbrakk> \<Longrightarrow> A : Union(C)" 286 unfolding Union_def by (blast intro: UN_I) 287 288lemma UnionE: "\<lbrakk>A : Union(C); \<And>X. \<lbrakk> A:X; X:C\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" 289 unfolding Union_def by (blast elim: UN_E) 290 291 292subsection \<open>Rules for Inter\<close> 293 294lemma InterI: "(\<And>X. X:C \<Longrightarrow> A:X) \<Longrightarrow> A : Inter(C)" 295 unfolding Inter_def by (blast intro: INT_I) 296 297(*A "destruct" rule -- every X in C contains A as an element, but 298 A:X can hold when X:C does not! This rule is analogous to "spec". *) 299lemma InterD: "\<lbrakk>A : Inter(C); X:C\<rbrakk> \<Longrightarrow> A:X" 300 unfolding Inter_def by (blast dest: INT_D) 301 302(*"Classical" elimination rule -- does not require proving X:C *) 303lemma InterE: "\<lbrakk>A : Inter(C); A:X \<Longrightarrow> R; \<not> X:C \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" 304 unfolding Inter_def by (blast elim: INT_E) 305 306 307section \<open>Derived rules involving subsets; Union and Intersection as lattice operations\<close> 308 309subsection \<open>Big Union -- least upper bound of a set\<close> 310 311lemma Union_upper: "B:A \<Longrightarrow> B <= Union(A)" 312 by (blast intro: subsetI UnionI) 313 314lemma Union_least: "(\<And>X. X:A \<Longrightarrow> X<=C) \<Longrightarrow> Union(A) <= C" 315 by (blast intro: subsetI dest: subsetD elim: UnionE) 316 317 318subsection \<open>Big Intersection -- greatest lower bound of a set\<close> 319 320lemma Inter_lower: "B:A \<Longrightarrow> Inter(A) <= B" 321 by (blast intro: subsetI dest: InterD) 322 323lemma Inter_greatest: "(\<And>X. X:A \<Longrightarrow> C<=X) \<Longrightarrow> C <= Inter(A)" 324 by (blast intro: subsetI InterI dest: subsetD) 325 326 327subsection \<open>Finite Union -- the least upper bound of 2 sets\<close> 328 329lemma Un_upper1: "A <= A Un B" 330 by (blast intro: subsetI UnI1) 331 332lemma Un_upper2: "B <= A Un B" 333 by (blast intro: subsetI UnI2) 334 335lemma Un_least: "\<lbrakk>A<=C; B<=C\<rbrakk> \<Longrightarrow> A Un B <= C" 336 by (blast intro: subsetI elim: UnE dest: subsetD) 337 338 339subsection \<open>Finite Intersection -- the greatest lower bound of 2 sets\<close> 340 341lemma Int_lower1: "A Int B <= A" 342 by (blast intro: subsetI elim: IntE) 343 344lemma Int_lower2: "A Int B <= B" 345 by (blast intro: subsetI elim: IntE) 346 347lemma Int_greatest: "\<lbrakk>C<=A; C<=B\<rbrakk> \<Longrightarrow> C <= A Int B" 348 by (blast intro: subsetI IntI dest: subsetD) 349 350 351subsection \<open>Monotonicity\<close> 352 353lemma monoI: "(\<And>A B. A <= B \<Longrightarrow> f(A) <= f(B)) \<Longrightarrow> mono(f)" 354 unfolding mono_def by blast 355 356lemma monoD: "\<lbrakk>mono(f); A <= B\<rbrakk> \<Longrightarrow> f(A) <= f(B)" 357 unfolding mono_def by blast 358 359lemma mono_Un: "mono(f) \<Longrightarrow> f(A) Un f(B) <= f(A Un B)" 360 by (blast intro: Un_least dest: monoD intro: Un_upper1 Un_upper2) 361 362lemma mono_Int: "mono(f) \<Longrightarrow> f(A Int B) <= f(A) Int f(B)" 363 by (blast intro: Int_greatest dest: monoD intro: Int_lower1 Int_lower2) 364 365 366subsection \<open>Automated reasoning setup\<close> 367 368lemmas [intro!] = ballI subsetI InterI INT_I CollectI ComplI IntI UnCI singletonI 369 and [intro] = bexI UnionI UN_I 370 and [elim!] = bexE UnionE UN_E CollectE ComplE IntE UnE emptyE singletonE 371 and [elim] = ballE InterD InterE INT_D INT_E subsetD subsetCE 372 373lemma mem_rews: 374 "(a : A Un B) \<longleftrightarrow> (a:A | a:B)" 375 "(a : A Int B) \<longleftrightarrow> (a:A \<and> a:B)" 376 "(a : Compl(B)) \<longleftrightarrow> (\<not>a:B)" 377 "(a : {b}) \<longleftrightarrow> (a=b)" 378 "(a : {}) \<longleftrightarrow> False" 379 "(a : {x. P(x)}) \<longleftrightarrow> P(a)" 380 by blast+ 381 382lemmas [simp] = trivial_set empty_eq mem_rews 383 and [cong] = ball_cong bex_cong INT_cong UN_cong 384 385 386section \<open>Equalities involving union, intersection, inclusion, etc.\<close> 387 388subsection \<open>Binary Intersection\<close> 389 390lemma Int_absorb: "A Int A = A" 391 by (blast intro: equalityI) 392 393lemma Int_commute: "A Int B = B Int A" 394 by (blast intro: equalityI) 395 396lemma Int_assoc: "(A Int B) Int C = A Int (B Int C)" 397 by (blast intro: equalityI) 398 399lemma Int_Un_distrib: "(A Un B) Int C = (A Int C) Un (B Int C)" 400 by (blast intro: equalityI) 401 402lemma subset_Int_eq: "(A<=B) \<longleftrightarrow> (A Int B = A)" 403 by (blast intro: equalityI elim: equalityE) 404 405 406subsection \<open>Binary Union\<close> 407 408lemma Un_absorb: "A Un A = A" 409 by (blast intro: equalityI) 410 411lemma Un_commute: "A Un B = B Un A" 412 by (blast intro: equalityI) 413 414lemma Un_assoc: "(A Un B) Un C = A Un (B Un C)" 415 by (blast intro: equalityI) 416 417lemma Un_Int_distrib: "(A Int B) Un C = (A Un C) Int (B Un C)" 418 by (blast intro: equalityI) 419 420lemma Un_Int_crazy: 421 "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)" 422 by (blast intro: equalityI) 423 424lemma subset_Un_eq: "(A<=B) \<longleftrightarrow> (A Un B = B)" 425 by (blast intro: equalityI elim: equalityE) 426 427 428subsection \<open>Simple properties of \<open>Compl\<close> -- complement of a set\<close> 429 430lemma Compl_disjoint: "A Int Compl(A) = {x. False}" 431 by (blast intro: equalityI) 432 433lemma Compl_partition: "A Un Compl(A) = {x. True}" 434 by (blast intro: equalityI) 435 436lemma double_complement: "Compl(Compl(A)) = A" 437 by (blast intro: equalityI) 438 439lemma Compl_Un: "Compl(A Un B) = Compl(A) Int Compl(B)" 440 by (blast intro: equalityI) 441 442lemma Compl_Int: "Compl(A Int B) = Compl(A) Un Compl(B)" 443 by (blast intro: equalityI) 444 445lemma Compl_UN: "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))" 446 by (blast intro: equalityI) 447 448lemma Compl_INT: "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))" 449 by (blast intro: equalityI) 450 451(*Halmos, Naive Set Theory, page 16.*) 452lemma Un_Int_assoc_eq: "((A Int B) Un C = A Int (B Un C)) \<longleftrightarrow> (C<=A)" 453 by (blast intro: equalityI elim: equalityE) 454 455 456subsection \<open>Big Union and Intersection\<close> 457 458lemma Union_Un_distrib: "Union(A Un B) = Union(A) Un Union(B)" 459 by (blast intro: equalityI) 460 461lemma Union_disjoint: 462 "(Union(C) Int A = {x. False}) \<longleftrightarrow> (ALL B:C. B Int A = {x. False})" 463 by (blast intro: equalityI elim: equalityE) 464 465lemma Inter_Un_distrib: "Inter(A Un B) = Inter(A) Int Inter(B)" 466 by (blast intro: equalityI) 467 468 469subsection \<open>Unions and Intersections of Families\<close> 470 471lemma UN_eq: "(UN x:A. B(x)) = Union({Y. EX x:A. Y=B(x)})" 472 by (blast intro: equalityI) 473 474(*Look: it has an EXISTENTIAL quantifier*) 475lemma INT_eq: "(INT x:A. B(x)) = Inter({Y. EX x:A. Y=B(x)})" 476 by (blast intro: equalityI) 477 478lemma Int_Union_image: "A Int Union(B) = (UN C:B. A Int C)" 479 by (blast intro: equalityI) 480 481lemma Un_Inter_image: "A Un Inter(B) = (INT C:B. A Un C)" 482 by (blast intro: equalityI) 483 484 485section \<open>Monotonicity of various operations\<close> 486 487lemma Union_mono: "A<=B \<Longrightarrow> Union(A) <= Union(B)" 488 by blast 489 490lemma Inter_anti_mono: "B <= A \<Longrightarrow> Inter(A) <= Inter(B)" 491 by blast 492 493lemma UN_mono: "\<lbrakk>A <= B; \<And>x. x:A \<Longrightarrow> f(x)<=g(x)\<rbrakk> \<Longrightarrow> (UN x:A. f(x)) <= (UN x:B. g(x))" 494 by blast 495 496lemma INT_anti_mono: "\<lbrakk>B <= A; \<And>x. x:A \<Longrightarrow> f(x) <= g(x)\<rbrakk> \<Longrightarrow> (INT x:A. f(x)) <= (INT x:A. g(x))" 497 by blast 498 499lemma Un_mono: "\<lbrakk>A <= C; B <= D\<rbrakk> \<Longrightarrow> A Un B <= C Un D" 500 by blast 501 502lemma Int_mono: "\<lbrakk>A <= C; B <= D\<rbrakk> \<Longrightarrow> A Int B <= C Int D" 503 by blast 504 505lemma Compl_anti_mono: "A <= B \<Longrightarrow> Compl(B) <= Compl(A)" 506 by blast 507 508end 509