1(* Title: ZF/upair.thy 2 Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory 3 Copyright 1993 University of Cambridge 4 5Observe the order of dependence: 6 Upair is defined in terms of Replace 7 \<union> is defined in terms of Upair and \<Union>(similarly for Int) 8 cons is defined in terms of Upair and Un 9 Ordered pairs and descriptions are defined using cons ("set notation") 10*) 11 12section\<open>Unordered Pairs\<close> 13 14theory upair 15imports ZF_Base 16keywords "print_tcset" :: diag 17begin 18 19ML_file \<open>Tools/typechk.ML\<close> 20 21lemma atomize_ball [symmetric, rulify]: 22 "(!!x. x \<in> A ==> P(x)) == Trueprop (\<forall>x\<in>A. P(x))" 23by (simp add: Ball_def atomize_all atomize_imp) 24 25 26subsection\<open>Unordered Pairs: constant \<^term>\<open>Upair\<close>\<close> 27 28lemma Upair_iff [simp]: "c \<in> Upair(a,b) \<longleftrightarrow> (c=a | c=b)" 29by (unfold Upair_def, blast) 30 31lemma UpairI1: "a \<in> Upair(a,b)" 32by simp 33 34lemma UpairI2: "b \<in> Upair(a,b)" 35by simp 36 37lemma UpairE: "[| a \<in> Upair(b,c); a=b ==> P; a=c ==> P |] ==> P" 38by (simp, blast) 39 40subsection\<open>Rules for Binary Union, Defined via \<^term>\<open>Upair\<close>\<close> 41 42lemma Un_iff [simp]: "c \<in> A \<union> B \<longleftrightarrow> (c \<in> A | c \<in> B)" 43apply (simp add: Un_def) 44apply (blast intro: UpairI1 UpairI2 elim: UpairE) 45done 46 47lemma UnI1: "c \<in> A ==> c \<in> A \<union> B" 48by simp 49 50lemma UnI2: "c \<in> B ==> c \<in> A \<union> B" 51by simp 52 53declare UnI1 [elim?] UnI2 [elim?] 54 55lemma UnE [elim!]: "[| c \<in> A \<union> B; c \<in> A ==> P; c \<in> B ==> P |] ==> P" 56by (simp, blast) 57 58(*Stronger version of the rule above*) 59lemma UnE': "[| c \<in> A \<union> B; c \<in> A ==> P; [| c \<in> B; c\<notin>A |] ==> P |] ==> P" 60by (simp, blast) 61 62(*Classical introduction rule: no commitment to A vs B*) 63lemma UnCI [intro!]: "(c \<notin> B ==> c \<in> A) ==> c \<in> A \<union> B" 64by (simp, blast) 65 66subsection\<open>Rules for Binary Intersection, Defined via \<^term>\<open>Upair\<close>\<close> 67 68lemma Int_iff [simp]: "c \<in> A \<inter> B \<longleftrightarrow> (c \<in> A & c \<in> B)" 69apply (unfold Int_def) 70apply (blast intro: UpairI1 UpairI2 elim: UpairE) 71done 72 73lemma IntI [intro!]: "[| c \<in> A; c \<in> B |] ==> c \<in> A \<inter> B" 74by simp 75 76lemma IntD1: "c \<in> A \<inter> B ==> c \<in> A" 77by simp 78 79lemma IntD2: "c \<in> A \<inter> B ==> c \<in> B" 80by simp 81 82lemma IntE [elim!]: "[| c \<in> A \<inter> B; [| c \<in> A; c \<in> B |] ==> P |] ==> P" 83by simp 84 85 86subsection\<open>Rules for Set Difference, Defined via \<^term>\<open>Upair\<close>\<close> 87 88lemma Diff_iff [simp]: "c \<in> A-B \<longleftrightarrow> (c \<in> A & c\<notin>B)" 89by (unfold Diff_def, blast) 90 91lemma DiffI [intro!]: "[| c \<in> A; c \<notin> B |] ==> c \<in> A - B" 92by simp 93 94lemma DiffD1: "c \<in> A - B ==> c \<in> A" 95by simp 96 97lemma DiffD2: "c \<in> A - B ==> c \<notin> B" 98by simp 99 100lemma DiffE [elim!]: "[| c \<in> A - B; [| c \<in> A; c\<notin>B |] ==> P |] ==> P" 101by simp 102 103 104subsection\<open>Rules for \<^term>\<open>cons\<close>\<close> 105 106lemma cons_iff [simp]: "a \<in> cons(b,A) \<longleftrightarrow> (a=b | a \<in> A)" 107apply (unfold cons_def) 108apply (blast intro: UpairI1 UpairI2 elim: UpairE) 109done 110 111(*risky as a typechecking rule, but solves otherwise unconstrained goals of 112the form x \<in> ?A*) 113lemma consI1 [simp,TC]: "a \<in> cons(a,B)" 114by simp 115 116 117lemma consI2: "a \<in> B ==> a \<in> cons(b,B)" 118by simp 119 120lemma consE [elim!]: "[| a \<in> cons(b,A); a=b ==> P; a \<in> A ==> P |] ==> P" 121by (simp, blast) 122 123(*Stronger version of the rule above*) 124lemma consE': 125 "[| a \<in> cons(b,A); a=b ==> P; [| a \<in> A; a\<noteq>b |] ==> P |] ==> P" 126by (simp, blast) 127 128(*Classical introduction rule*) 129lemma consCI [intro!]: "(a\<notin>B ==> a=b) ==> a \<in> cons(b,B)" 130by (simp, blast) 131 132lemma cons_not_0 [simp]: "cons(a,B) \<noteq> 0" 133by (blast elim: equalityE) 134 135lemmas cons_neq_0 = cons_not_0 [THEN notE] 136 137declare cons_not_0 [THEN not_sym, simp] 138 139 140subsection\<open>Singletons\<close> 141 142lemma singleton_iff: "a \<in> {b} \<longleftrightarrow> a=b" 143by simp 144 145lemma singletonI [intro!]: "a \<in> {a}" 146by (rule consI1) 147 148lemmas singletonE = singleton_iff [THEN iffD1, elim_format, elim!] 149 150 151subsection\<open>Descriptions\<close> 152 153lemma the_equality [intro]: 154 "[| P(a); !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a" 155apply (unfold the_def) 156apply (fast dest: subst) 157done 158 159(* Only use this if you already know \<exists>!x. P(x) *) 160lemma the_equality2: "[| \<exists>!x. P(x); P(a) |] ==> (THE x. P(x)) = a" 161by blast 162 163lemma theI: "\<exists>!x. P(x) ==> P(THE x. P(x))" 164apply (erule ex1E) 165apply (subst the_equality) 166apply (blast+) 167done 168 169(*No congruence rule is necessary: if @{term"\<forall>y.P(y)\<longleftrightarrow>Q(y)"} then 170 @{term "THE x.P(x)"} rewrites to @{term "THE x.Q(x)"} *) 171 172(*If it's "undefined", it's zero!*) 173lemma the_0: "~ (\<exists>!x. P(x)) ==> (THE x. P(x))=0" 174apply (unfold the_def) 175apply (blast elim!: ReplaceE) 176done 177 178(*Easier to apply than theI: conclusion has only one occurrence of P*) 179lemma theI2: 180 assumes p1: "~ Q(0) ==> \<exists>!x. P(x)" 181 and p2: "!!x. P(x) ==> Q(x)" 182 shows "Q(THE x. P(x))" 183apply (rule classical) 184apply (rule p2) 185apply (rule theI) 186apply (rule classical) 187apply (rule p1) 188apply (erule the_0 [THEN subst], assumption) 189done 190 191lemma the_eq_trivial [simp]: "(THE x. x = a) = a" 192by blast 193 194lemma the_eq_trivial2 [simp]: "(THE x. a = x) = a" 195by blast 196 197 198subsection\<open>Conditional Terms: \<open>if-then-else\<close>\<close> 199 200lemma if_true [simp]: "(if True then a else b) = a" 201by (unfold if_def, blast) 202 203lemma if_false [simp]: "(if False then a else b) = b" 204by (unfold if_def, blast) 205 206(*Never use with case splitting, or if P is known to be true or false*) 207lemma if_cong: 208 "[| P\<longleftrightarrow>Q; Q ==> a=c; ~Q ==> b=d |] 209 ==> (if P then a else b) = (if Q then c else d)" 210by (simp add: if_def cong add: conj_cong) 211 212(*Prevents simplification of x and y \<in> faster and allows the execution 213 of functional programs. NOW THE DEFAULT.*) 214lemma if_weak_cong: "P\<longleftrightarrow>Q ==> (if P then x else y) = (if Q then x else y)" 215by simp 216 217(*Not needed for rewriting, since P would rewrite to True anyway*) 218lemma if_P: "P ==> (if P then a else b) = a" 219by (unfold if_def, blast) 220 221(*Not needed for rewriting, since P would rewrite to False anyway*) 222lemma if_not_P: "~P ==> (if P then a else b) = b" 223by (unfold if_def, blast) 224 225lemma split_if [split]: 226 "P(if Q then x else y) \<longleftrightarrow> ((Q \<longrightarrow> P(x)) & (~Q \<longrightarrow> P(y)))" 227by (case_tac Q, simp_all) 228 229(** Rewrite rules for boolean case-splitting: faster than split_if [split] 230**) 231 232lemmas split_if_eq1 = split_if [of "%x. x = b"] for b 233lemmas split_if_eq2 = split_if [of "%x. a = x"] for a 234 235lemmas split_if_mem1 = split_if [of "%x. x \<in> b"] for b 236lemmas split_if_mem2 = split_if [of "%x. a \<in> x"] for a 237 238lemmas split_ifs = split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2 239 240(*Logically equivalent to split_if_mem2*) 241lemma if_iff: "a: (if P then x else y) \<longleftrightarrow> P & a \<in> x | ~P & a \<in> y" 242by simp 243 244lemma if_type [TC]: 245 "[| P ==> a \<in> A; ~P ==> b \<in> A |] ==> (if P then a else b): A" 246by simp 247 248(** Splitting IFs in the assumptions **) 249 250lemma split_if_asm: "P(if Q then x else y) \<longleftrightarrow> (~((Q & ~P(x)) | (~Q & ~P(y))))" 251by simp 252 253lemmas if_splits = split_if split_if_asm 254 255 256subsection\<open>Consequences of Foundation\<close> 257 258(*was called mem_anti_sym*) 259lemma mem_asym: "[| a \<in> b; ~P ==> b \<in> a |] ==> P" 260apply (rule classical) 261apply (rule_tac A1 = "{a,b}" in foundation [THEN disjE]) 262apply (blast elim!: equalityE)+ 263done 264 265(*was called mem_anti_refl*) 266lemma mem_irrefl: "a \<in> a ==> P" 267by (blast intro: mem_asym) 268 269(*mem_irrefl should NOT be added to default databases: 270 it would be tried on most goals, making proofs slower!*) 271 272lemma mem_not_refl: "a \<notin> a" 273apply (rule notI) 274apply (erule mem_irrefl) 275done 276 277(*Good for proving inequalities by rewriting*) 278lemma mem_imp_not_eq: "a \<in> A ==> a \<noteq> A" 279by (blast elim!: mem_irrefl) 280 281lemma eq_imp_not_mem: "a=A ==> a \<notin> A" 282by (blast intro: elim: mem_irrefl) 283 284subsection\<open>Rules for Successor\<close> 285 286lemma succ_iff: "i \<in> succ(j) \<longleftrightarrow> i=j | i \<in> j" 287by (unfold succ_def, blast) 288 289lemma succI1 [simp]: "i \<in> succ(i)" 290by (simp add: succ_iff) 291 292lemma succI2: "i \<in> j ==> i \<in> succ(j)" 293by (simp add: succ_iff) 294 295lemma succE [elim!]: 296 "[| i \<in> succ(j); i=j ==> P; i \<in> j ==> P |] ==> P" 297apply (simp add: succ_iff, blast) 298done 299 300(*Classical introduction rule*) 301lemma succCI [intro!]: "(i\<notin>j ==> i=j) ==> i \<in> succ(j)" 302by (simp add: succ_iff, blast) 303 304lemma succ_not_0 [simp]: "succ(n) \<noteq> 0" 305by (blast elim!: equalityE) 306 307lemmas succ_neq_0 = succ_not_0 [THEN notE, elim!] 308 309declare succ_not_0 [THEN not_sym, simp] 310declare sym [THEN succ_neq_0, elim!] 311 312(* @{term"succ(c) \<subseteq> B ==> c \<in> B"} *) 313lemmas succ_subsetD = succI1 [THEN [2] subsetD] 314 315(* @{term"succ(b) \<noteq> b"} *) 316lemmas succ_neq_self = succI1 [THEN mem_imp_not_eq, THEN not_sym] 317 318lemma succ_inject_iff [simp]: "succ(m) = succ(n) \<longleftrightarrow> m=n" 319by (blast elim: mem_asym elim!: equalityE) 320 321lemmas succ_inject = succ_inject_iff [THEN iffD1, dest!] 322 323 324subsection\<open>Miniscoping of the Bounded Universal Quantifier\<close> 325 326lemma ball_simps1: 327 "(\<forall>x\<in>A. P(x) & Q) \<longleftrightarrow> (\<forall>x\<in>A. P(x)) & (A=0 | Q)" 328 "(\<forall>x\<in>A. P(x) | Q) \<longleftrightarrow> ((\<forall>x\<in>A. P(x)) | Q)" 329 "(\<forall>x\<in>A. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P(x)) \<longrightarrow> Q)" 330 "(~(\<forall>x\<in>A. P(x))) \<longleftrightarrow> (\<exists>x\<in>A. ~P(x))" 331 "(\<forall>x\<in>0.P(x)) \<longleftrightarrow> True" 332 "(\<forall>x\<in>succ(i).P(x)) \<longleftrightarrow> P(i) & (\<forall>x\<in>i. P(x))" 333 "(\<forall>x\<in>cons(a,B).P(x)) \<longleftrightarrow> P(a) & (\<forall>x\<in>B. P(x))" 334 "(\<forall>x\<in>RepFun(A,f). P(x)) \<longleftrightarrow> (\<forall>y\<in>A. P(f(y)))" 335 "(\<forall>x\<in>\<Union>(A).P(x)) \<longleftrightarrow> (\<forall>y\<in>A. \<forall>x\<in>y. P(x))" 336by blast+ 337 338lemma ball_simps2: 339 "(\<forall>x\<in>A. P & Q(x)) \<longleftrightarrow> (A=0 | P) & (\<forall>x\<in>A. Q(x))" 340 "(\<forall>x\<in>A. P | Q(x)) \<longleftrightarrow> (P | (\<forall>x\<in>A. Q(x)))" 341 "(\<forall>x\<in>A. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x\<in>A. Q(x)))" 342by blast+ 343 344lemma ball_simps3: 345 "(\<forall>x\<in>Collect(A,Q).P(x)) \<longleftrightarrow> (\<forall>x\<in>A. Q(x) \<longrightarrow> P(x))" 346by blast+ 347 348lemmas ball_simps [simp] = ball_simps1 ball_simps2 ball_simps3 349 350lemma ball_conj_distrib: 351 "(\<forall>x\<in>A. P(x) & Q(x)) \<longleftrightarrow> ((\<forall>x\<in>A. P(x)) & (\<forall>x\<in>A. Q(x)))" 352by blast 353 354 355subsection\<open>Miniscoping of the Bounded Existential Quantifier\<close> 356 357lemma bex_simps1: 358 "(\<exists>x\<in>A. P(x) & Q) \<longleftrightarrow> ((\<exists>x\<in>A. P(x)) & Q)" 359 "(\<exists>x\<in>A. P(x) | Q) \<longleftrightarrow> (\<exists>x\<in>A. P(x)) | (A\<noteq>0 & Q)" 360 "(\<exists>x\<in>A. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<forall>x\<in>A. P(x)) \<longrightarrow> (A\<noteq>0 & Q))" 361 "(\<exists>x\<in>0.P(x)) \<longleftrightarrow> False" 362 "(\<exists>x\<in>succ(i).P(x)) \<longleftrightarrow> P(i) | (\<exists>x\<in>i. P(x))" 363 "(\<exists>x\<in>cons(a,B).P(x)) \<longleftrightarrow> P(a) | (\<exists>x\<in>B. P(x))" 364 "(\<exists>x\<in>RepFun(A,f). P(x)) \<longleftrightarrow> (\<exists>y\<in>A. P(f(y)))" 365 "(\<exists>x\<in>\<Union>(A).P(x)) \<longleftrightarrow> (\<exists>y\<in>A. \<exists>x\<in>y. P(x))" 366 "(~(\<exists>x\<in>A. P(x))) \<longleftrightarrow> (\<forall>x\<in>A. ~P(x))" 367by blast+ 368 369lemma bex_simps2: 370 "(\<exists>x\<in>A. P & Q(x)) \<longleftrightarrow> (P & (\<exists>x\<in>A. Q(x)))" 371 "(\<exists>x\<in>A. P | Q(x)) \<longleftrightarrow> (A\<noteq>0 & P) | (\<exists>x\<in>A. Q(x))" 372 "(\<exists>x\<in>A. P \<longrightarrow> Q(x)) \<longleftrightarrow> ((A=0 | P) \<longrightarrow> (\<exists>x\<in>A. Q(x)))" 373by blast+ 374 375lemma bex_simps3: 376 "(\<exists>x\<in>Collect(A,Q).P(x)) \<longleftrightarrow> (\<exists>x\<in>A. Q(x) & P(x))" 377by blast 378 379lemmas bex_simps [simp] = bex_simps1 bex_simps2 bex_simps3 380 381lemma bex_disj_distrib: 382 "(\<exists>x\<in>A. P(x) | Q(x)) \<longleftrightarrow> ((\<exists>x\<in>A. P(x)) | (\<exists>x\<in>A. Q(x)))" 383by blast 384 385 386(** One-point rule for bounded quantifiers: see HOL/Set.ML **) 387 388lemma bex_triv_one_point1 [simp]: "(\<exists>x\<in>A. x=a) \<longleftrightarrow> (a \<in> A)" 389by blast 390 391lemma bex_triv_one_point2 [simp]: "(\<exists>x\<in>A. a=x) \<longleftrightarrow> (a \<in> A)" 392by blast 393 394lemma bex_one_point1 [simp]: "(\<exists>x\<in>A. x=a & P(x)) \<longleftrightarrow> (a \<in> A & P(a))" 395by blast 396 397lemma bex_one_point2 [simp]: "(\<exists>x\<in>A. a=x & P(x)) \<longleftrightarrow> (a \<in> A & P(a))" 398by blast 399 400lemma ball_one_point1 [simp]: "(\<forall>x\<in>A. x=a \<longrightarrow> P(x)) \<longleftrightarrow> (a \<in> A \<longrightarrow> P(a))" 401by blast 402 403lemma ball_one_point2 [simp]: "(\<forall>x\<in>A. a=x \<longrightarrow> P(x)) \<longleftrightarrow> (a \<in> A \<longrightarrow> P(a))" 404by blast 405 406 407subsection\<open>Miniscoping of the Replacement Operator\<close> 408 409text\<open>These cover both \<^term>\<open>Replace\<close> and \<^term>\<open>Collect\<close>\<close> 410lemma Rep_simps [simp]: 411 "{x. y \<in> 0, R(x,y)} = 0" 412 "{x \<in> 0. P(x)} = 0" 413 "{x \<in> A. Q} = (if Q then A else 0)" 414 "RepFun(0,f) = 0" 415 "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))" 416 "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))" 417by (simp_all, blast+) 418 419 420subsection\<open>Miniscoping of Unions\<close> 421 422lemma UN_simps1: 423 "(\<Union>x\<in>C. cons(a, B(x))) = (if C=0 then 0 else cons(a, \<Union>x\<in>C. B(x)))" 424 "(\<Union>x\<in>C. A(x) \<union> B') = (if C=0 then 0 else (\<Union>x\<in>C. A(x)) \<union> B')" 425 "(\<Union>x\<in>C. A' \<union> B(x)) = (if C=0 then 0 else A' \<union> (\<Union>x\<in>C. B(x)))" 426 "(\<Union>x\<in>C. A(x) \<inter> B') = ((\<Union>x\<in>C. A(x)) \<inter> B')" 427 "(\<Union>x\<in>C. A' \<inter> B(x)) = (A' \<inter> (\<Union>x\<in>C. B(x)))" 428 "(\<Union>x\<in>C. A(x) - B') = ((\<Union>x\<in>C. A(x)) - B')" 429 "(\<Union>x\<in>C. A' - B(x)) = (if C=0 then 0 else A' - (\<Inter>x\<in>C. B(x)))" 430apply (simp_all add: Inter_def) 431apply (blast intro!: equalityI )+ 432done 433 434lemma UN_simps2: 435 "(\<Union>x\<in>\<Union>(A). B(x)) = (\<Union>y\<in>A. \<Union>x\<in>y. B(x))" 436 "(\<Union>z\<in>(\<Union>x\<in>A. B(x)). C(z)) = (\<Union>x\<in>A. \<Union>z\<in>B(x). C(z))" 437 "(\<Union>x\<in>RepFun(A,f). B(x)) = (\<Union>a\<in>A. B(f(a)))" 438by blast+ 439 440lemmas UN_simps [simp] = UN_simps1 UN_simps2 441 442text\<open>Opposite of miniscoping: pull the operator out\<close> 443 444lemma UN_extend_simps1: 445 "(\<Union>x\<in>C. A(x)) \<union> B = (if C=0 then B else (\<Union>x\<in>C. A(x) \<union> B))" 446 "((\<Union>x\<in>C. A(x)) \<inter> B) = (\<Union>x\<in>C. A(x) \<inter> B)" 447 "((\<Union>x\<in>C. A(x)) - B) = (\<Union>x\<in>C. A(x) - B)" 448apply simp_all 449apply blast+ 450done 451 452lemma UN_extend_simps2: 453 "cons(a, \<Union>x\<in>C. B(x)) = (if C=0 then {a} else (\<Union>x\<in>C. cons(a, B(x))))" 454 "A \<union> (\<Union>x\<in>C. B(x)) = (if C=0 then A else (\<Union>x\<in>C. A \<union> B(x)))" 455 "(A \<inter> (\<Union>x\<in>C. B(x))) = (\<Union>x\<in>C. A \<inter> B(x))" 456 "A - (\<Inter>x\<in>C. B(x)) = (if C=0 then A else (\<Union>x\<in>C. A - B(x)))" 457 "(\<Union>y\<in>A. \<Union>x\<in>y. B(x)) = (\<Union>x\<in>\<Union>(A). B(x))" 458 "(\<Union>a\<in>A. B(f(a))) = (\<Union>x\<in>RepFun(A,f). B(x))" 459apply (simp_all add: Inter_def) 460apply (blast intro!: equalityI)+ 461done 462 463lemma UN_UN_extend: 464 "(\<Union>x\<in>A. \<Union>z\<in>B(x). C(z)) = (\<Union>z\<in>(\<Union>x\<in>A. B(x)). C(z))" 465by blast 466 467lemmas UN_extend_simps = UN_extend_simps1 UN_extend_simps2 UN_UN_extend 468 469 470subsection\<open>Miniscoping of Intersections\<close> 471 472lemma INT_simps1: 473 "(\<Inter>x\<in>C. A(x) \<inter> B) = (\<Inter>x\<in>C. A(x)) \<inter> B" 474 "(\<Inter>x\<in>C. A(x) - B) = (\<Inter>x\<in>C. A(x)) - B" 475 "(\<Inter>x\<in>C. A(x) \<union> B) = (if C=0 then 0 else (\<Inter>x\<in>C. A(x)) \<union> B)" 476by (simp_all add: Inter_def, blast+) 477 478lemma INT_simps2: 479 "(\<Inter>x\<in>C. A \<inter> B(x)) = A \<inter> (\<Inter>x\<in>C. B(x))" 480 "(\<Inter>x\<in>C. A - B(x)) = (if C=0 then 0 else A - (\<Union>x\<in>C. B(x)))" 481 "(\<Inter>x\<in>C. cons(a, B(x))) = (if C=0 then 0 else cons(a, \<Inter>x\<in>C. B(x)))" 482 "(\<Inter>x\<in>C. A \<union> B(x)) = (if C=0 then 0 else A \<union> (\<Inter>x\<in>C. B(x)))" 483apply (simp_all add: Inter_def) 484apply (blast intro!: equalityI)+ 485done 486 487lemmas INT_simps [simp] = INT_simps1 INT_simps2 488 489text\<open>Opposite of miniscoping: pull the operator out\<close> 490 491 492lemma INT_extend_simps1: 493 "(\<Inter>x\<in>C. A(x)) \<inter> B = (\<Inter>x\<in>C. A(x) \<inter> B)" 494 "(\<Inter>x\<in>C. A(x)) - B = (\<Inter>x\<in>C. A(x) - B)" 495 "(\<Inter>x\<in>C. A(x)) \<union> B = (if C=0 then B else (\<Inter>x\<in>C. A(x) \<union> B))" 496apply (simp_all add: Inter_def, blast+) 497done 498 499lemma INT_extend_simps2: 500 "A \<inter> (\<Inter>x\<in>C. B(x)) = (\<Inter>x\<in>C. A \<inter> B(x))" 501 "A - (\<Union>x\<in>C. B(x)) = (if C=0 then A else (\<Inter>x\<in>C. A - B(x)))" 502 "cons(a, \<Inter>x\<in>C. B(x)) = (if C=0 then {a} else (\<Inter>x\<in>C. cons(a, B(x))))" 503 "A \<union> (\<Inter>x\<in>C. B(x)) = (if C=0 then A else (\<Inter>x\<in>C. A \<union> B(x)))" 504apply (simp_all add: Inter_def) 505apply (blast intro!: equalityI)+ 506done 507 508lemmas INT_extend_simps = INT_extend_simps1 INT_extend_simps2 509 510 511subsection\<open>Other simprules\<close> 512 513 514(*** Miniscoping: pushing in big Unions, Intersections, quantifiers, etc. ***) 515 516lemma misc_simps [simp]: 517 "0 \<union> A = A" 518 "A \<union> 0 = A" 519 "0 \<inter> A = 0" 520 "A \<inter> 0 = 0" 521 "0 - A = 0" 522 "A - 0 = A" 523 "\<Union>(0) = 0" 524 "\<Union>(cons(b,A)) = b \<union> \<Union>(A)" 525 "\<Inter>({b}) = b" 526by blast+ 527 528end 529