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