src/ZF/upair.thy
author wenzelm
Tue Jul 31 19:40:22 2007 +0200 (2007-07-31)
changeset 24091 109f19a13872
parent 16417 9bc16273c2d4
child 24893 b8ef7afe3a6b
permissions -rw-r--r--
added Tools/lin_arith.ML;
     1 (*  Title:      ZF/upair.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Observe the order of dependence:
     7     Upair is defined in terms of Replace
     8     Un is defined in terms of Upair and Union (similarly for Int)
     9     cons is defined in terms of Upair and Un
    10     Ordered pairs and descriptions are defined using cons ("set notation")
    11 *)
    12 
    13 header{*Unordered Pairs*}
    14 
    15 theory upair imports ZF
    16 uses "Tools/typechk.ML" begin
    17 
    18 setup TypeCheck.setup
    19 
    20 lemma atomize_ball [symmetric, rulify]:
    21      "(!!x. x:A ==> P(x)) == Trueprop (ALL x:A. P(x))"
    22 by (simp add: Ball_def atomize_all atomize_imp)
    23 
    24 
    25 subsection{*Unordered Pairs: constant @{term Upair}*}
    26 
    27 lemma Upair_iff [simp]: "c : Upair(a,b) <-> (c=a | c=b)"
    28 by (unfold Upair_def, blast)
    29 
    30 lemma UpairI1: "a : Upair(a,b)"
    31 by simp
    32 
    33 lemma UpairI2: "b : Upair(a,b)"
    34 by simp
    35 
    36 lemma UpairE: "[| a : Upair(b,c);  a=b ==> P;  a=c ==> P |] ==> P"
    37 by (simp, blast)
    38 
    39 subsection{*Rules for Binary Union, Defined via @{term Upair}*}
    40 
    41 lemma Un_iff [simp]: "c : A Un B <-> (c:A | c:B)"
    42 apply (simp add: Un_def)
    43 apply (blast intro: UpairI1 UpairI2 elim: UpairE)
    44 done
    45 
    46 lemma UnI1: "c : A ==> c : A Un B"
    47 by simp
    48 
    49 lemma UnI2: "c : B ==> c : A Un B"
    50 by simp
    51 
    52 declare UnI1 [elim?]  UnI2 [elim?]
    53 
    54 lemma UnE [elim!]: "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P"
    55 by (simp, blast)
    56 
    57 (*Stronger version of the rule above*)
    58 lemma UnE': "[| c : A Un B;  c:A ==> P;  [| c:B;  c~:A |] ==> P |] ==> P"
    59 by (simp, blast)
    60 
    61 (*Classical introduction rule: no commitment to A vs B*)
    62 lemma UnCI [intro!]: "(c ~: B ==> c : A) ==> c : A Un B"
    63 by (simp, blast)
    64 
    65 subsection{*Rules for Binary Intersection, Defined via @{term Upair}*}
    66 
    67 lemma Int_iff [simp]: "c : A Int B <-> (c:A & c:B)"
    68 apply (unfold Int_def)
    69 apply (blast intro: UpairI1 UpairI2 elim: UpairE)
    70 done
    71 
    72 lemma IntI [intro!]: "[| c : A;  c : B |] ==> c : A Int B"
    73 by simp
    74 
    75 lemma IntD1: "c : A Int B ==> c : A"
    76 by simp
    77 
    78 lemma IntD2: "c : A Int B ==> c : B"
    79 by simp
    80 
    81 lemma IntE [elim!]: "[| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P"
    82 by simp
    83 
    84 
    85 subsection{*Rules for Set Difference, Defined via @{term Upair}*}
    86 
    87 lemma Diff_iff [simp]: "c : A-B <-> (c:A & c~:B)"
    88 by (unfold Diff_def, blast)
    89 
    90 lemma DiffI [intro!]: "[| c : A;  c ~: B |] ==> c : A - B"
    91 by simp
    92 
    93 lemma DiffD1: "c : A - B ==> c : A"
    94 by simp
    95 
    96 lemma DiffD2: "c : A - B ==> c ~: B"
    97 by simp
    98 
    99 lemma DiffE [elim!]: "[| c : A - B;  [| c:A; c~:B |] ==> P |] ==> P"
   100 by simp
   101 
   102 
   103 subsection{*Rules for @{term cons}*}
   104 
   105 lemma cons_iff [simp]: "a : cons(b,A) <-> (a=b | a:A)"
   106 apply (unfold cons_def)
   107 apply (blast intro: UpairI1 UpairI2 elim: UpairE)
   108 done
   109 
   110 (*risky as a typechecking rule, but solves otherwise unconstrained goals of
   111 the form x : ?A*)
   112 lemma consI1 [simp,TC]: "a : cons(a,B)"
   113 by simp
   114 
   115 
   116 lemma consI2: "a : B ==> a : cons(b,B)"
   117 by simp
   118 
   119 lemma consE [elim!]: "[| a : cons(b,A);  a=b ==> P;  a:A ==> P |] ==> P"
   120 by (simp, blast)
   121 
   122 (*Stronger version of the rule above*)
   123 lemma consE':
   124     "[| a : cons(b,A);  a=b ==> P;  [| a:A;  a~=b |] ==> P |] ==> P"
   125 by (simp, blast)
   126 
   127 (*Classical introduction rule*)
   128 lemma consCI [intro!]: "(a~:B ==> a=b) ==> a: cons(b,B)"
   129 by (simp, blast)
   130 
   131 lemma cons_not_0 [simp]: "cons(a,B) ~= 0"
   132 by (blast elim: equalityE)
   133 
   134 lemmas cons_neq_0 = cons_not_0 [THEN notE, standard]
   135 
   136 declare cons_not_0 [THEN not_sym, simp]
   137 
   138 
   139 subsection{*Singletons*}
   140 
   141 lemma singleton_iff: "a : {b} <-> a=b"
   142 by simp
   143 
   144 lemma singletonI [intro!]: "a : {a}"
   145 by (rule consI1)
   146 
   147 lemmas singletonE = singleton_iff [THEN iffD1, elim_format, standard, elim!]
   148 
   149 
   150 subsection{*Descriptions*}
   151 
   152 lemma the_equality [intro]:
   153     "[| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
   154 apply (unfold the_def) 
   155 apply (fast dest: subst)
   156 done
   157 
   158 (* Only use this if you already know EX!x. P(x) *)
   159 lemma the_equality2: "[| EX! x. P(x);  P(a) |] ==> (THE x. P(x)) = a"
   160 by blast
   161 
   162 lemma theI: "EX! x. P(x) ==> P(THE x. P(x))"
   163 apply (erule ex1E)
   164 apply (subst the_equality)
   165 apply (blast+)
   166 done
   167 
   168 (*the_cong is no longer necessary: if (ALL y.P(y)<->Q(y)) then 
   169   (THE x.P(x))  rewrites to  (THE x. Q(x))  *)
   170 
   171 (*If it's "undefined", it's zero!*)
   172 lemma the_0: "~ (EX! x. P(x)) ==> (THE x. P(x))=0"
   173 apply (unfold the_def)
   174 apply (blast elim!: ReplaceE)
   175 done
   176 
   177 (*Easier to apply than theI: conclusion has only one occurrence of P*)
   178 lemma theI2:
   179     assumes p1: "~ Q(0) ==> EX! x. P(x)"
   180         and p2: "!!x. P(x) ==> Q(x)"
   181     shows "Q(THE x. P(x))"
   182 apply (rule classical)
   183 apply (rule p2)
   184 apply (rule theI)
   185 apply (rule classical)
   186 apply (rule p1)
   187 apply (erule the_0 [THEN subst], assumption)
   188 done
   189 
   190 lemma the_eq_trivial [simp]: "(THE x. x = a) = a"
   191 by blast
   192 
   193 lemma the_eq_trivial2 [simp]: "(THE x. a = x) = a"
   194 by blast
   195 
   196 
   197 subsection{*Conditional Terms: @{text "if-then-else"}*}
   198 
   199 lemma if_true [simp]: "(if True then a else b) = a"
   200 by (unfold if_def, blast)
   201 
   202 lemma if_false [simp]: "(if False then a else b) = b"
   203 by (unfold if_def, blast)
   204 
   205 (*Never use with case splitting, or if P is known to be true or false*)
   206 lemma if_cong:
   207     "[| P<->Q;  Q ==> a=c;  ~Q ==> b=d |]  
   208      ==> (if P then a else b) = (if Q then c else d)"
   209 by (simp add: if_def cong add: conj_cong)
   210 
   211 (*Prevents simplification of x and y: faster and allows the execution
   212   of functional programs. NOW THE DEFAULT.*)
   213 lemma if_weak_cong: "P<->Q ==> (if P then x else y) = (if Q then x else y)"
   214 by simp
   215 
   216 (*Not needed for rewriting, since P would rewrite to True anyway*)
   217 lemma if_P: "P ==> (if P then a else b) = a"
   218 by (unfold if_def, blast)
   219 
   220 (*Not needed for rewriting, since P would rewrite to False anyway*)
   221 lemma if_not_P: "~P ==> (if P then a else b) = b"
   222 by (unfold if_def, blast)
   223 
   224 lemma split_if [split]:
   225      "P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
   226 by (case_tac Q, simp_all)
   227 
   228 (** Rewrite rules for boolean case-splitting: faster than 
   229 	addsplits[split_if]
   230 **)
   231 
   232 lemmas split_if_eq1 = split_if [of "%x. x = b", standard]
   233 lemmas split_if_eq2 = split_if [of "%x. a = x", standard]
   234 
   235 lemmas split_if_mem1 = split_if [of "%x. x : b", standard]
   236 lemmas split_if_mem2 = split_if [of "%x. a : x", standard]
   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) <-> P & a:x | ~P & a:y"
   242 by simp
   243 
   244 lemma if_type [TC]:
   245     "[| P ==> a: A;  ~P ==> b: 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) <-> (~((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:b;  ~P ==> b: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: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 ~: 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:A ==> a ~= A"
   279 by (blast elim!: mem_irrefl)
   280 
   281 lemma eq_imp_not_mem: "a=A ==> a ~: A"
   282 by (blast intro: elim: mem_irrefl)
   283 
   284 subsection{*Rules for Successor*}
   285 
   286 lemma succ_iff: "i : succ(j) <-> i=j | i:j"
   287 by (unfold succ_def, blast)
   288 
   289 lemma succI1 [simp]: "i : succ(i)"
   290 by (simp add: succ_iff)
   291 
   292 lemma succI2: "i : j ==> i : succ(j)"
   293 by (simp add: succ_iff)
   294 
   295 lemma succE [elim!]: 
   296     "[| i : succ(j);  i=j ==> P;  i:j ==> P |] ==> P"
   297 apply (simp add: succ_iff, blast) 
   298 done
   299 
   300 (*Classical introduction rule*)
   301 lemma succCI [intro!]: "(i~:j ==> i=j) ==> i: succ(j)"
   302 by (simp add: succ_iff, blast)
   303 
   304 lemma succ_not_0 [simp]: "succ(n) ~= 0"
   305 by (blast elim!: equalityE)
   306 
   307 lemmas succ_neq_0 = succ_not_0 [THEN notE, standard, elim!]
   308 
   309 declare succ_not_0 [THEN not_sym, simp]
   310 declare sym [THEN succ_neq_0, elim!]
   311 
   312 (* succ(c) <= B ==> c : B *)
   313 lemmas succ_subsetD = succI1 [THEN [2] subsetD]
   314 
   315 (* succ(b) ~= b *)
   316 lemmas succ_neq_self = succI1 [THEN mem_imp_not_eq, THEN not_sym, standard]
   317 
   318 lemma succ_inject_iff [simp]: "succ(m) = succ(n) <-> m=n"
   319 by (blast elim: mem_asym elim!: equalityE)
   320 
   321 lemmas succ_inject = succ_inject_iff [THEN iffD1, standard, dest!]
   322 
   323 
   324 subsection{*Miniscoping of the Bounded Universal Quantifier*}
   325 
   326 lemma ball_simps1:
   327      "(ALL x:A. P(x) & Q)   <-> (ALL x:A. P(x)) & (A=0 | Q)"
   328      "(ALL x:A. P(x) | Q)   <-> ((ALL x:A. P(x)) | Q)"
   329      "(ALL x:A. P(x) --> Q) <-> ((EX x:A. P(x)) --> Q)"
   330      "(~(ALL x:A. P(x))) <-> (EX x:A. ~P(x))"
   331      "(ALL x:0.P(x)) <-> True"
   332      "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i. P(x))"
   333      "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B. P(x))"
   334      "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))"
   335      "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))" 
   336 by blast+
   337 
   338 lemma ball_simps2:
   339      "(ALL x:A. P & Q(x))   <-> (A=0 | P) & (ALL x:A. Q(x))"
   340      "(ALL x:A. P | Q(x))   <-> (P | (ALL x:A. Q(x)))"
   341      "(ALL x:A. P --> Q(x)) <-> (P --> (ALL x:A. Q(x)))"
   342 by blast+
   343 
   344 lemma ball_simps3:
   345      "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))"
   346 by blast+
   347 
   348 lemmas ball_simps [simp] = ball_simps1 ball_simps2 ball_simps3
   349 
   350 lemma ball_conj_distrib:
   351     "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))"
   352 by blast
   353 
   354 
   355 subsection{*Miniscoping of the Bounded Existential Quantifier*}
   356 
   357 lemma bex_simps1:
   358      "(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)"
   359      "(EX x:A. P(x) | Q) <-> (EX x:A. P(x)) | (A~=0 & Q)"
   360      "(EX x:A. P(x) --> Q) <-> ((ALL x:A. P(x)) --> (A~=0 & Q))"
   361      "(EX x:0.P(x)) <-> False"
   362      "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i. P(x))"
   363      "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))"
   364      "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))"
   365      "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y.  P(x))"
   366      "(~(EX x:A. P(x))) <-> (ALL x:A. ~P(x))"
   367 by blast+
   368 
   369 lemma bex_simps2:
   370      "(EX x:A. P & Q(x)) <-> (P & (EX x:A. Q(x)))"
   371      "(EX x:A. P | Q(x)) <-> (A~=0 & P) | (EX x:A. Q(x))"
   372      "(EX x:A. P --> Q(x)) <-> ((A=0 | P) --> (EX x:A. Q(x)))"
   373 by blast+
   374 
   375 lemma bex_simps3:
   376      "(EX x:Collect(A,Q).P(x)) <-> (EX x: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     "(EX x:A. P(x) | Q(x)) <-> ((EX x:A. P(x)) | (EX x: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]: "(EX x:A. x=a) <-> (a:A)"
   389 by blast
   390 
   391 lemma bex_triv_one_point2 [simp]: "(EX x:A. a=x) <-> (a:A)"
   392 by blast
   393 
   394 lemma bex_one_point1 [simp]: "(EX x:A. x=a & P(x)) <-> (a:A & P(a))"
   395 by blast
   396 
   397 lemma bex_one_point2 [simp]: "(EX x:A. a=x & P(x)) <-> (a:A & P(a))"
   398 by blast
   399 
   400 lemma ball_one_point1 [simp]: "(ALL x:A. x=a --> P(x)) <-> (a:A --> P(a))"
   401 by blast
   402 
   403 lemma ball_one_point2 [simp]: "(ALL x:A. a=x --> P(x)) <-> (a:A --> 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:0, R(x,y)} = 0"
   412      "{x:0. P(x)} = 0"
   413      "{x: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      "(UN x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, UN x:C. B(x)))"
   424      "(UN x:C. A(x) Un B')   = (if C=0 then 0 else (UN x:C. A(x)) Un B')"
   425      "(UN x:C. A' Un B(x))   = (if C=0 then 0 else A' Un (UN x:C. B(x)))"
   426      "(UN x:C. A(x) Int B')  = ((UN x:C. A(x)) Int B')"
   427      "(UN x:C. A' Int B(x))  = (A' Int (UN x:C. B(x)))"
   428      "(UN x:C. A(x) - B')    = ((UN x:C. A(x)) - B')"
   429      "(UN x:C. A' - B(x))    = (if C=0 then 0 else A' - (INT x:C. B(x)))"
   430 apply (simp_all add: Inter_def) 
   431 apply (blast intro!: equalityI )+
   432 done
   433 
   434 lemma UN_simps2:
   435       "(UN x: Union(A). B(x)) = (UN y:A. UN x:y. B(x))"
   436       "(UN z: (UN x:A. B(x)). C(z)) = (UN  x:A. UN z: B(x). C(z))"
   437       "(UN x: RepFun(A,f). B(x))     = (UN a: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      "(UN x:C. A(x)) Un B   = (if C=0 then B else (UN x:C. A(x) Un B))"
   446      "((UN x:C. A(x)) Int B) = (UN x:C. A(x) Int B)"
   447      "((UN x:C. A(x)) - B) = (UN x:C. A(x) - B)"
   448 apply simp_all 
   449 apply blast+
   450 done
   451 
   452 lemma UN_extend_simps2:
   453      "cons(a, UN x:C. B(x)) = (if C=0 then {a} else (UN x:C. cons(a, B(x))))"
   454      "A Un (UN x:C. B(x))   = (if C=0 then A else (UN x:C. A Un B(x)))"
   455      "(A Int (UN x:C. B(x))) = (UN x:C. A Int B(x))"
   456      "A - (INT x:C. B(x))    = (if C=0 then A else (UN x:C. A - B(x)))"
   457      "(UN y:A. UN x:y. B(x)) = (UN x: Union(A). B(x))"
   458      "(UN a:A. B(f(a))) = (UN x: 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      "(UN  x:A. UN z: B(x). C(z)) = (UN z: (UN x: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      "(INT x:C. A(x) Int B) = (INT x:C. A(x)) Int B"
   474      "(INT x:C. A(x) - B)   = (INT x:C. A(x)) - B"
   475      "(INT x:C. A(x) Un B)  = (if C=0 then 0 else (INT x:C. A(x)) Un B)"
   476 by (simp_all add: Inter_def, blast+)
   477 
   478 lemma INT_simps2:
   479      "(INT x:C. A Int B(x)) = A Int (INT x:C. B(x))"
   480      "(INT x:C. A - B(x))   = (if C=0 then 0 else A - (UN x:C. B(x)))"
   481      "(INT x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, INT x:C. B(x)))"
   482      "(INT x:C. A Un B(x))  = (if C=0 then 0 else A Un (INT x: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      "(INT x:C. A(x)) Int B = (INT x:C. A(x) Int B)"
   494      "(INT x:C. A(x)) - B = (INT x:C. A(x) - B)"
   495      "(INT x:C. A(x)) Un B  = (if C=0 then B else (INT x:C. A(x) Un B))"
   496 apply (simp_all add: Inter_def, blast+)
   497 done
   498 
   499 lemma INT_extend_simps2:
   500      "A Int (INT x:C. B(x)) = (INT x:C. A Int B(x))"
   501      "A - (UN x:C. B(x))   = (if C=0 then A else (INT x:C. A - B(x)))"
   502      "cons(a, INT x:C. B(x)) = (if C=0 then {a} else (INT x:C. cons(a, B(x))))"
   503      "A Un (INT x:C. B(x))  = (if C=0 then A else (INT x:C. A Un 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 Un A = A"
   518      "A Un 0 = A"
   519      "0 Int A = 0"
   520      "A Int 0 = 0"
   521      "0 - A = 0"
   522      "A - 0 = A"
   523      "Union(0) = 0"
   524      "Union(cons(b,A)) = b Un Union(A)"
   525      "Inter({b}) = b"
   526 by blast+
   527 
   528 
   529 ML
   530 {*
   531 val Upair_iff = thm "Upair_iff";
   532 val UpairI1 = thm "UpairI1";
   533 val UpairI2 = thm "UpairI2";
   534 val UpairE = thm "UpairE";
   535 val Un_iff = thm "Un_iff";
   536 val UnI1 = thm "UnI1";
   537 val UnI2 = thm "UnI2";
   538 val UnE = thm "UnE";
   539 val UnE' = thm "UnE'";
   540 val UnCI = thm "UnCI";
   541 val Int_iff = thm "Int_iff";
   542 val IntI = thm "IntI";
   543 val IntD1 = thm "IntD1";
   544 val IntD2 = thm "IntD2";
   545 val IntE = thm "IntE";
   546 val Diff_iff = thm "Diff_iff";
   547 val DiffI = thm "DiffI";
   548 val DiffD1 = thm "DiffD1";
   549 val DiffD2 = thm "DiffD2";
   550 val DiffE = thm "DiffE";
   551 val cons_iff = thm "cons_iff";
   552 val consI1 = thm "consI1";
   553 val consI2 = thm "consI2";
   554 val consE = thm "consE";
   555 val consE' = thm "consE'";
   556 val consCI = thm "consCI";
   557 val cons_not_0 = thm "cons_not_0";
   558 val cons_neq_0 = thm "cons_neq_0";
   559 val singleton_iff = thm "singleton_iff";
   560 val singletonI = thm "singletonI";
   561 val singletonE = thm "singletonE";
   562 val the_equality = thm "the_equality";
   563 val the_equality2 = thm "the_equality2";
   564 val theI = thm "theI";
   565 val the_0 = thm "the_0";
   566 val theI2 = thm "theI2";
   567 val if_true = thm "if_true";
   568 val if_false = thm "if_false";
   569 val if_cong = thm "if_cong";
   570 val if_weak_cong = thm "if_weak_cong";
   571 val if_P = thm "if_P";
   572 val if_not_P = thm "if_not_P";
   573 val split_if = thm "split_if";
   574 val split_if_eq1 = thm "split_if_eq1";
   575 val split_if_eq2 = thm "split_if_eq2";
   576 val split_if_mem1 = thm "split_if_mem1";
   577 val split_if_mem2 = thm "split_if_mem2";
   578 val if_iff = thm "if_iff";
   579 val if_type = thm "if_type";
   580 val mem_asym = thm "mem_asym";
   581 val mem_irrefl = thm "mem_irrefl";
   582 val mem_not_refl = thm "mem_not_refl";
   583 val mem_imp_not_eq = thm "mem_imp_not_eq";
   584 val succ_iff = thm "succ_iff";
   585 val succI1 = thm "succI1";
   586 val succI2 = thm "succI2";
   587 val succE = thm "succE";
   588 val succCI = thm "succCI";
   589 val succ_not_0 = thm "succ_not_0";
   590 val succ_neq_0 = thm "succ_neq_0";
   591 val succ_subsetD = thm "succ_subsetD";
   592 val succ_neq_self = thm "succ_neq_self";
   593 val succ_inject_iff = thm "succ_inject_iff";
   594 val succ_inject = thm "succ_inject";
   595 
   596 val split_ifs = thms "split_ifs";
   597 val ball_simps = thms "ball_simps";
   598 val bex_simps = thms "bex_simps";
   599 
   600 val ball_conj_distrib = thm "ball_conj_distrib";
   601 val bex_disj_distrib = thm "bex_disj_distrib";
   602 val bex_triv_one_point1 = thm "bex_triv_one_point1";
   603 val bex_triv_one_point2 = thm "bex_triv_one_point2";
   604 val bex_one_point1 = thm "bex_one_point1";
   605 val bex_one_point2 = thm "bex_one_point2";
   606 val ball_one_point1 = thm "ball_one_point1";
   607 val ball_one_point2 = thm "ball_one_point2";
   608 
   609 val Rep_simps = thms "Rep_simps";
   610 val misc_simps = thms "misc_simps";
   611 
   612 val UN_simps = thms "UN_simps";
   613 val INT_simps = thms "INT_simps";
   614 
   615 val UN_extend_simps = thms "UN_extend_simps";
   616 val INT_extend_simps = thms "INT_extend_simps";
   617 *}
   618 
   619 end