src/ZF/upair.thy
 author wenzelm Sun Nov 09 17:04:14 2014 +0100 (2014-11-09) changeset 58957 c9e744ea8a38 parent 58871 c399ae4b836f child 60770 240563fbf41d permissions -rw-r--r--
proper context for match_tac etc.;
```     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     \<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
```
```    12 section{*Unordered Pairs*}
```
```    13
```
```    14 theory upair
```
```    15 imports ZF
```
```    16 keywords "print_tcset" :: diag
```
```    17 begin
```
```    18
```
```    19 ML_file "Tools/typechk.ML"
```
```    20
```
```    21 lemma atomize_ball [symmetric, rulify]:
```
```    22      "(!!x. x \<in> A ==> P(x)) == Trueprop (\<forall>x\<in>A. P(x))"
```
```    23 by (simp add: Ball_def atomize_all atomize_imp)
```
```    24
```
```    25
```
```    26 subsection{*Unordered Pairs: constant @{term Upair}*}
```
```    27
```
```    28 lemma Upair_iff [simp]: "c \<in> Upair(a,b) \<longleftrightarrow> (c=a | c=b)"
```
```    29 by (unfold Upair_def, blast)
```
```    30
```
```    31 lemma UpairI1: "a \<in> Upair(a,b)"
```
```    32 by simp
```
```    33
```
```    34 lemma UpairI2: "b \<in> Upair(a,b)"
```
```    35 by simp
```
```    36
```
```    37 lemma UpairE: "[| a \<in> Upair(b,c);  a=b ==> P;  a=c ==> P |] ==> P"
```
```    38 by (simp, blast)
```
```    39
```
```    40 subsection{*Rules for Binary Union, Defined via @{term Upair}*}
```
```    41
```
```    42 lemma Un_iff [simp]: "c \<in> A \<union> B \<longleftrightarrow> (c \<in> A | c \<in> B)"
```
```    43 apply (simp add: Un_def)
```
```    44 apply (blast intro: UpairI1 UpairI2 elim: UpairE)
```
```    45 done
```
```    46
```
```    47 lemma UnI1: "c \<in> A ==> c \<in> A \<union> B"
```
```    48 by simp
```
```    49
```
```    50 lemma UnI2: "c \<in> B ==> c \<in> A \<union> B"
```
```    51 by simp
```
```    52
```
```    53 declare UnI1 [elim?]  UnI2 [elim?]
```
```    54
```
```    55 lemma UnE [elim!]: "[| c \<in> A \<union> B;  c \<in> A ==> P;  c \<in> B ==> P |] ==> P"
```
```    56 by (simp, blast)
```
```    57
```
```    58 (*Stronger version of the rule above*)
```
```    59 lemma UnE': "[| c \<in> A \<union> B;  c \<in> A ==> P;  [| c \<in> B;  c\<notin>A |] ==> P |] ==> P"
```
```    60 by (simp, blast)
```
```    61
```
```    62 (*Classical introduction rule: no commitment to A vs B*)
```
```    63 lemma UnCI [intro!]: "(c \<notin> B ==> c \<in> A) ==> c \<in> A \<union> B"
```
```    64 by (simp, blast)
```
```    65
```
```    66 subsection{*Rules for Binary Intersection, Defined via @{term Upair}*}
```
```    67
```
```    68 lemma Int_iff [simp]: "c \<in> A \<inter> B \<longleftrightarrow> (c \<in> A & c \<in> B)"
```
```    69 apply (unfold Int_def)
```
```    70 apply (blast intro: UpairI1 UpairI2 elim: UpairE)
```
```    71 done
```
```    72
```
```    73 lemma IntI [intro!]: "[| c \<in> A;  c \<in> B |] ==> c \<in> A \<inter> B"
```
```    74 by simp
```
```    75
```
```    76 lemma IntD1: "c \<in> A \<inter> B ==> c \<in> A"
```
```    77 by simp
```
```    78
```
```    79 lemma IntD2: "c \<in> A \<inter> B ==> c \<in> B"
```
```    80 by simp
```
```    81
```
```    82 lemma IntE [elim!]: "[| c \<in> A \<inter> B;  [| c \<in> A; c \<in> B |] ==> P |] ==> P"
```
```    83 by simp
```
```    84
```
```    85
```
```    86 subsection{*Rules for Set Difference, Defined via @{term Upair}*}
```
```    87
```
```    88 lemma Diff_iff [simp]: "c \<in> A-B \<longleftrightarrow> (c \<in> A & c\<notin>B)"
```
```    89 by (unfold Diff_def, blast)
```
```    90
```
```    91 lemma DiffI [intro!]: "[| c \<in> A;  c \<notin> B |] ==> c \<in> A - B"
```
```    92 by simp
```
```    93
```
```    94 lemma DiffD1: "c \<in> A - B ==> c \<in> A"
```
```    95 by simp
```
```    96
```
```    97 lemma DiffD2: "c \<in> A - B ==> c \<notin> B"
```
```    98 by simp
```
```    99
```
```   100 lemma DiffE [elim!]: "[| c \<in> A - B;  [| c \<in> A; c\<notin>B |] ==> P |] ==> P"
```
```   101 by simp
```
```   102
```
```   103
```
```   104 subsection{*Rules for @{term cons}*}
```
```   105
```
```   106 lemma cons_iff [simp]: "a \<in> cons(b,A) \<longleftrightarrow> (a=b | a \<in> A)"
```
```   107 apply (unfold cons_def)
```
```   108 apply (blast intro: UpairI1 UpairI2 elim: UpairE)
```
```   109 done
```
```   110
```
```   111 (*risky as a typechecking rule, but solves otherwise unconstrained goals of
```
```   112 the form x \<in> ?A*)
```
```   113 lemma consI1 [simp,TC]: "a \<in> cons(a,B)"
```
```   114 by simp
```
```   115
```
```   116
```
```   117 lemma consI2: "a \<in> B ==> a \<in> cons(b,B)"
```
```   118 by simp
```
```   119
```
```   120 lemma consE [elim!]: "[| a \<in> cons(b,A);  a=b ==> P;  a \<in> A ==> P |] ==> P"
```
```   121 by (simp, blast)
```
```   122
```
```   123 (*Stronger version of the rule above*)
```
```   124 lemma consE':
```
```   125     "[| a \<in> cons(b,A);  a=b ==> P;  [| a \<in> A;  a\<noteq>b |] ==> P |] ==> P"
```
```   126 by (simp, blast)
```
```   127
```
```   128 (*Classical introduction rule*)
```
```   129 lemma consCI [intro!]: "(a\<notin>B ==> a=b) ==> a \<in> cons(b,B)"
```
```   130 by (simp, blast)
```
```   131
```
```   132 lemma cons_not_0 [simp]: "cons(a,B) \<noteq> 0"
```
```   133 by (blast elim: equalityE)
```
```   134
```
```   135 lemmas cons_neq_0 = cons_not_0 [THEN notE]
```
```   136
```
```   137 declare cons_not_0 [THEN not_sym, simp]
```
```   138
```
```   139
```
```   140 subsection{*Singletons*}
```
```   141
```
```   142 lemma singleton_iff: "a \<in> {b} \<longleftrightarrow> a=b"
```
```   143 by simp
```
```   144
```
```   145 lemma singletonI [intro!]: "a \<in> {a}"
```
```   146 by (rule consI1)
```
```   147
```
```   148 lemmas singletonE = singleton_iff [THEN iffD1, elim_format, elim!]
```
```   149
```
```   150
```
```   151 subsection{*Descriptions*}
```
```   152
```
```   153 lemma the_equality [intro]:
```
```   154     "[| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
```
```   155 apply (unfold the_def)
```
```   156 apply (fast dest: subst)
```
```   157 done
```
```   158
```
```   159 (* Only use this if you already know EX!x. P(x) *)
```
```   160 lemma the_equality2: "[| EX! x. P(x);  P(a) |] ==> (THE x. P(x)) = a"
```
```   161 by blast
```
```   162
```
```   163 lemma theI: "EX! x. P(x) ==> P(THE x. P(x))"
```
```   164 apply (erule ex1E)
```
```   165 apply (subst the_equality)
```
```   166 apply (blast+)
```
```   167 done
```
```   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!*)
```
```   173 lemma the_0: "~ (EX! x. P(x)) ==> (THE x. P(x))=0"
```
```   174 apply (unfold the_def)
```
```   175 apply (blast elim!: ReplaceE)
```
```   176 done
```
```   177
```
```   178 (*Easier to apply than theI: conclusion has only one occurrence of P*)
```
```   179 lemma theI2:
```
```   180     assumes p1: "~ Q(0) ==> EX! x. P(x)"
```
```   181         and p2: "!!x. P(x) ==> Q(x)"
```
```   182     shows "Q(THE x. P(x))"
```
```   183 apply (rule classical)
```
```   184 apply (rule p2)
```
```   185 apply (rule theI)
```
```   186 apply (rule classical)
```
```   187 apply (rule p1)
```
```   188 apply (erule the_0 [THEN subst], assumption)
```
```   189 done
```
```   190
```
```   191 lemma the_eq_trivial [simp]: "(THE x. x = a) = a"
```
```   192 by blast
```
```   193
```
```   194 lemma the_eq_trivial2 [simp]: "(THE x. a = x) = a"
```
```   195 by blast
```
```   196
```
```   197
```
```   198 subsection{*Conditional Terms: @{text "if-then-else"}*}
```
```   199
```
```   200 lemma if_true [simp]: "(if True then a else b) = a"
```
```   201 by (unfold if_def, blast)
```
```   202
```
```   203 lemma if_false [simp]: "(if False then a else b) = b"
```
```   204 by (unfold if_def, blast)
```
```   205
```
```   206 (*Never use with case splitting, or if P is known to be true or false*)
```
```   207 lemma 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)"
```
```   210 by (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.*)
```
```   214 lemma if_weak_cong: "P\<longleftrightarrow>Q ==> (if P then x else y) = (if Q then x else y)"
```
```   215 by simp
```
```   216
```
```   217 (*Not needed for rewriting, since P would rewrite to True anyway*)
```
```   218 lemma if_P: "P ==> (if P then a else b) = a"
```
```   219 by (unfold if_def, blast)
```
```   220
```
```   221 (*Not needed for rewriting, since P would rewrite to False anyway*)
```
```   222 lemma if_not_P: "~P ==> (if P then a else b) = b"
```
```   223 by (unfold if_def, blast)
```
```   224
```
```   225 lemma split_if [split]:
```
```   226      "P(if Q then x else y) \<longleftrightarrow> ((Q \<longrightarrow> P(x)) & (~Q \<longrightarrow> P(y)))"
```
```   227 by (case_tac Q, simp_all)
```
```   228
```
```   229 (** Rewrite rules for boolean case-splitting: faster than split_if [split]
```
```   230 **)
```
```   231
```
```   232 lemmas split_if_eq1 = split_if [of "%x. x = b"] for b
```
```   233 lemmas split_if_eq2 = split_if [of "%x. a = x"] for x
```
```   234
```
```   235 lemmas split_if_mem1 = split_if [of "%x. x \<in> b"] for b
```
```   236 lemmas split_if_mem2 = split_if [of "%x. a \<in> x"] for x
```
```   237
```
```   238 lemmas split_ifs = split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
```
```   239
```
```   240 (*Logically equivalent to split_if_mem2*)
```
```   241 lemma if_iff: "a: (if P then x else y) \<longleftrightarrow> P & a \<in> x | ~P & a \<in> y"
```
```   242 by simp
```
```   243
```
```   244 lemma if_type [TC]:
```
```   245     "[| P ==> a \<in> A;  ~P ==> b \<in> A |] ==> (if P then a else b): A"
```
```   246 by simp
```
```   247
```
```   248 (** Splitting IFs in the assumptions **)
```
```   249
```
```   250 lemma split_if_asm: "P(if Q then x else y) \<longleftrightarrow> (~((Q & ~P(x)) | (~Q & ~P(y))))"
```
```   251 by simp
```
```   252
```
```   253 lemmas if_splits = split_if split_if_asm
```
```   254
```
```   255
```
```   256 subsection{*Consequences of Foundation*}
```
```   257
```
```   258 (*was called mem_anti_sym*)
```
```   259 lemma mem_asym: "[| a \<in> b;  ~P ==> b \<in> a |] ==> P"
```
```   260 apply (rule classical)
```
```   261 apply (rule_tac A1 = "{a,b}" in foundation [THEN disjE])
```
```   262 apply (blast elim!: equalityE)+
```
```   263 done
```
```   264
```
```   265 (*was called mem_anti_refl*)
```
```   266 lemma mem_irrefl: "a \<in> a ==> P"
```
```   267 by (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
```
```   272 lemma mem_not_refl: "a \<notin> a"
```
```   273 apply (rule notI)
```
```   274 apply (erule mem_irrefl)
```
```   275 done
```
```   276
```
```   277 (*Good for proving inequalities by rewriting*)
```
```   278 lemma mem_imp_not_eq: "a \<in> A ==> a \<noteq> A"
```
```   279 by (blast elim!: mem_irrefl)
```
```   280
```
```   281 lemma eq_imp_not_mem: "a=A ==> a \<notin> A"
```
```   282 by (blast intro: elim: mem_irrefl)
```
```   283
```
```   284 subsection{*Rules for Successor*}
```
```   285
```
```   286 lemma succ_iff: "i \<in> succ(j) \<longleftrightarrow> i=j | i \<in> j"
```
```   287 by (unfold succ_def, blast)
```
```   288
```
```   289 lemma succI1 [simp]: "i \<in> succ(i)"
```
```   290 by (simp add: succ_iff)
```
```   291
```
```   292 lemma succI2: "i \<in> j ==> i \<in> succ(j)"
```
```   293 by (simp add: succ_iff)
```
```   294
```
```   295 lemma succE [elim!]:
```
```   296     "[| i \<in> succ(j);  i=j ==> P;  i \<in> j ==> P |] ==> P"
```
```   297 apply (simp add: succ_iff, blast)
```
```   298 done
```
```   299
```
```   300 (*Classical introduction rule*)
```
```   301 lemma succCI [intro!]: "(i\<notin>j ==> i=j) ==> i \<in> succ(j)"
```
```   302 by (simp add: succ_iff, blast)
```
```   303
```
```   304 lemma succ_not_0 [simp]: "succ(n) \<noteq> 0"
```
```   305 by (blast elim!: equalityE)
```
```   306
```
```   307 lemmas succ_neq_0 = succ_not_0 [THEN notE, elim!]
```
```   308
```
```   309 declare succ_not_0 [THEN not_sym, simp]
```
```   310 declare sym [THEN succ_neq_0, elim!]
```
```   311
```
```   312 (* @{term"succ(c) \<subseteq> B ==> c \<in> B"} *)
```
```   313 lemmas succ_subsetD = succI1 [THEN [2] subsetD]
```
```   314
```
```   315 (* @{term"succ(b) \<noteq> b"} *)
```
```   316 lemmas succ_neq_self = succI1 [THEN mem_imp_not_eq, THEN not_sym]
```
```   317
```
```   318 lemma succ_inject_iff [simp]: "succ(m) = succ(n) \<longleftrightarrow> m=n"
```
```   319 by (blast elim: mem_asym elim!: equalityE)
```
```   320
```
```   321 lemmas succ_inject = succ_inject_iff [THEN iffD1, dest!]
```
```   322
```
```   323
```
```   324 subsection{*Miniscoping of the Bounded Universal Quantifier*}
```
```   325
```
```   326 lemma 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))"
```
```   336 by blast+
```
```   337
```
```   338 lemma 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)))"
```
```   342 by blast+
```
```   343
```
```   344 lemma ball_simps3:
```
```   345      "(\<forall>x\<in>Collect(A,Q).P(x)) \<longleftrightarrow> (\<forall>x\<in>A. Q(x) \<longrightarrow> P(x))"
```
```   346 by blast+
```
```   347
```
```   348 lemmas ball_simps [simp] = ball_simps1 ball_simps2 ball_simps3
```
```   349
```
```   350 lemma 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)))"
```
```   352 by blast
```
```   353
```
```   354
```
```   355 subsection{*Miniscoping of the Bounded Existential Quantifier*}
```
```   356
```
```   357 lemma 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))"
```
```   367 by blast+
```
```   368
```
```   369 lemma 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)))"
```
```   373 by blast+
```
```   374
```
```   375 lemma bex_simps3:
```
```   376      "(\<exists>x\<in>Collect(A,Q).P(x)) \<longleftrightarrow> (\<exists>x\<in>A. Q(x) & P(x))"
```
```   377 by blast
```
```   378
```
```   379 lemmas bex_simps [simp] = bex_simps1 bex_simps2 bex_simps3
```
```   380
```
```   381 lemma 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)))"
```
```   383 by blast
```
```   384
```
```   385
```
```   386 (** One-point rule for bounded quantifiers: see HOL/Set.ML **)
```
```   387
```
```   388 lemma bex_triv_one_point1 [simp]: "(\<exists>x\<in>A. x=a) \<longleftrightarrow> (a \<in> A)"
```
```   389 by blast
```
```   390
```
```   391 lemma bex_triv_one_point2 [simp]: "(\<exists>x\<in>A. a=x) \<longleftrightarrow> (a \<in> A)"
```
```   392 by blast
```
```   393
```
```   394 lemma bex_one_point1 [simp]: "(\<exists>x\<in>A. x=a & P(x)) \<longleftrightarrow> (a \<in> A & P(a))"
```
```   395 by blast
```
```   396
```
```   397 lemma bex_one_point2 [simp]: "(\<exists>x\<in>A. a=x & P(x)) \<longleftrightarrow> (a \<in> A & P(a))"
```
```   398 by blast
```
```   399
```
```   400 lemma ball_one_point1 [simp]: "(\<forall>x\<in>A. x=a \<longrightarrow> P(x)) \<longleftrightarrow> (a \<in> A \<longrightarrow> P(a))"
```
```   401 by blast
```
```   402
```
```   403 lemma ball_one_point2 [simp]: "(\<forall>x\<in>A. a=x \<longrightarrow> P(x)) \<longleftrightarrow> (a \<in> A \<longrightarrow> P(a))"
```
```   404 by blast
```
```   405
```
```   406
```
```   407 subsection{*Miniscoping of the Replacement Operator*}
```
```   408
```
```   409 text{*These cover both @{term Replace} and @{term Collect}*}
```
```   410 lemma 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))"
```
```   417 by (simp_all, blast+)
```
```   418
```
```   419
```
```   420 subsection{*Miniscoping of Unions*}
```
```   421
```
```   422 lemma 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)))"
```
```   430 apply (simp_all add: Inter_def)
```
```   431 apply (blast intro!: equalityI )+
```
```   432 done
```
```   433
```
```   434 lemma 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)))"
```
```   438 by blast+
```
```   439
```
```   440 lemmas UN_simps [simp] = UN_simps1 UN_simps2
```
```   441
```
```   442 text{*Opposite of miniscoping: pull the operator out*}
```
```   443
```
```   444 lemma 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)"
```
```   448 apply simp_all
```
```   449 apply blast+
```
```   450 done
```
```   451
```
```   452 lemma 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))"
```
```   459 apply (simp_all add: Inter_def)
```
```   460 apply (blast intro!: equalityI)+
```
```   461 done
```
```   462
```
```   463 lemma 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))"
```
```   465 by blast
```
```   466
```
```   467 lemmas UN_extend_simps = UN_extend_simps1 UN_extend_simps2 UN_UN_extend
```
```   468
```
```   469
```
```   470 subsection{*Miniscoping of Intersections*}
```
```   471
```
```   472 lemma 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)"
```
```   476 by (simp_all add: Inter_def, blast+)
```
```   477
```
```   478 lemma 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)))"
```
```   483 apply (simp_all add: Inter_def)
```
```   484 apply (blast intro!: equalityI)+
```
```   485 done
```
```   486
```
```   487 lemmas INT_simps [simp] = INT_simps1 INT_simps2
```
```   488
```
```   489 text{*Opposite of miniscoping: pull the operator out*}
```
```   490
```
```   491
```
```   492 lemma 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))"
```
```   496 apply (simp_all add: Inter_def, blast+)
```
```   497 done
```
```   498
```
```   499 lemma 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)))"
```
```   504 apply (simp_all add: Inter_def)
```
```   505 apply (blast intro!: equalityI)+
```
```   506 done
```
```   507
```
```   508 lemmas INT_extend_simps = INT_extend_simps1 INT_extend_simps2
```
```   509
```
```   510
```
```   511 subsection{*Other simprules*}
```
```   512
```
```   513
```
```   514 (*** Miniscoping: pushing in big Unions, Intersections, quantifiers, etc. ***)
```
```   515
```
```   516 lemma 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"
```
```   526 by blast+
```
```   527
```
```   528 end
```