src/ZF/equalities.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/equalities
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 *)
     7 
     8 header{*Basic Equalities and Inclusions*}
     9 
    10 theory equalities imports pair begin
    11 
    12 text{*These cover union, intersection, converse, domain, range, etc.  Philippe
    13 de Groote proved many of the inclusions.*}
    14 
    15 lemma in_mono: "A\<subseteq>B ==> x\<in>A --> x\<in>B"
    16 by blast
    17 
    18 lemma the_eq_0 [simp]: "(THE x. False) = 0"
    19 by (blast intro: the_0)
    20 
    21 subsection{*Bounded Quantifiers*}
    22 text {* \medskip 
    23 
    24   The following are not added to the default simpset because
    25   (a) they duplicate the body and (b) there are no similar rules for @{text Int}.*}
    26 
    27 lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) <-> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))";
    28   by blast
    29 
    30 lemma bex_Un: "(\<exists>x \<in> A\<union>B. P(x)) <-> (\<exists>x \<in> A. P(x)) | (\<exists>x \<in> B. P(x))";
    31   by blast
    32 
    33 lemma ball_UN: "(\<forall>z \<in> (\<Union>x\<in>A. B(x)). P(z)) <-> (\<forall>x\<in>A. \<forall>z \<in> B(x). P(z))"
    34   by blast
    35 
    36 lemma bex_UN: "(\<exists>z \<in> (\<Union>x\<in>A. B(x)). P(z)) <-> (\<exists>x\<in>A. \<exists>z\<in>B(x). P(z))"
    37   by blast
    38 
    39 subsection{*Converse of a Relation*}
    40 
    41 lemma converse_iff [simp]: "<a,b>\<in> converse(r) <-> <b,a>\<in>r"
    42 by (unfold converse_def, blast)
    43 
    44 lemma converseI [intro!]: "<a,b>\<in>r ==> <b,a>\<in>converse(r)"
    45 by (unfold converse_def, blast)
    46 
    47 lemma converseD: "<a,b> \<in> converse(r) ==> <b,a> \<in> r"
    48 by (unfold converse_def, blast)
    49 
    50 lemma converseE [elim!]:
    51     "[| yx \<in> converse(r);   
    52         !!x y. [| yx=<y,x>;  <x,y>\<in>r |] ==> P |]
    53      ==> P"
    54 by (unfold converse_def, blast) 
    55 
    56 lemma converse_converse: "r\<subseteq>Sigma(A,B) ==> converse(converse(r)) = r"
    57 by blast
    58 
    59 lemma converse_type: "r\<subseteq>A*B ==> converse(r)\<subseteq>B*A"
    60 by blast
    61 
    62 lemma converse_prod [simp]: "converse(A*B) = B*A"
    63 by blast
    64 
    65 lemma converse_empty [simp]: "converse(0) = 0"
    66 by blast
    67 
    68 lemma converse_subset_iff:
    69      "A \<subseteq> Sigma(X,Y) ==> converse(A) \<subseteq> converse(B) <-> A \<subseteq> B"
    70 by blast
    71 
    72 
    73 subsection{*Finite Set Constructions Using @{term cons}*}
    74 
    75 lemma cons_subsetI: "[| a\<in>C; B\<subseteq>C |] ==> cons(a,B) \<subseteq> C"
    76 by blast
    77 
    78 lemma subset_consI: "B \<subseteq> cons(a,B)"
    79 by blast
    80 
    81 lemma cons_subset_iff [iff]: "cons(a,B)\<subseteq>C <-> a\<in>C & B\<subseteq>C"
    82 by blast
    83 
    84 (*A safe special case of subset elimination, adding no new variables 
    85   [| cons(a,B) \<subseteq> C; [| a \<in> C; B \<subseteq> C |] ==> R |] ==> R *)
    86 lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE, standard]
    87 
    88 lemma subset_empty_iff: "A\<subseteq>0 <-> A=0"
    89 by blast
    90 
    91 lemma subset_cons_iff: "C\<subseteq>cons(a,B) <-> C\<subseteq>B | (a\<in>C & C-{a} \<subseteq> B)"
    92 by blast
    93 
    94 (* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*)
    95 lemma cons_eq: "{a} Un B = cons(a,B)"
    96 by blast
    97 
    98 lemma cons_commute: "cons(a, cons(b, C)) = cons(b, cons(a, C))"
    99 by blast
   100 
   101 lemma cons_absorb: "a: B ==> cons(a,B) = B"
   102 by blast
   103 
   104 lemma cons_Diff: "a: B ==> cons(a, B-{a}) = B"
   105 by blast
   106 
   107 lemma Diff_cons_eq: "cons(a,B) - C = (if a\<in>C then B-C else cons(a,B-C))" 
   108 by auto
   109 
   110 lemma equal_singleton [rule_format]: "[| a: C;  \<forall>y\<in>C. y=b |] ==> C = {b}"
   111 by blast
   112 
   113 lemma [simp]: "cons(a,cons(a,B)) = cons(a,B)"
   114 by blast
   115 
   116 (** singletons **)
   117 
   118 lemma singleton_subsetI: "a\<in>C ==> {a} \<subseteq> C"
   119 by blast
   120 
   121 lemma singleton_subsetD: "{a} \<subseteq> C  ==>  a\<in>C"
   122 by blast
   123 
   124 
   125 (** succ **)
   126 
   127 lemma subset_succI: "i \<subseteq> succ(i)"
   128 by blast
   129 
   130 (*But if j is an ordinal or is transitive, then i\<in>j implies i\<subseteq>j! 
   131   See ordinal/Ord_succ_subsetI*)
   132 lemma succ_subsetI: "[| i\<in>j;  i\<subseteq>j |] ==> succ(i)\<subseteq>j"
   133 by (unfold succ_def, blast)
   134 
   135 lemma succ_subsetE:
   136     "[| succ(i) \<subseteq> j;  [| i\<in>j;  i\<subseteq>j |] ==> P |] ==> P"
   137 by (unfold succ_def, blast) 
   138 
   139 lemma succ_subset_iff: "succ(a) \<subseteq> B <-> (a \<subseteq> B & a \<in> B)"
   140 by (unfold succ_def, blast)
   141 
   142 
   143 subsection{*Binary Intersection*}
   144 
   145 (** Intersection is the greatest lower bound of two sets **)
   146 
   147 lemma Int_subset_iff: "C \<subseteq> A Int B <-> C \<subseteq> A & C \<subseteq> B"
   148 by blast
   149 
   150 lemma Int_lower1: "A Int B \<subseteq> A"
   151 by blast
   152 
   153 lemma Int_lower2: "A Int B \<subseteq> B"
   154 by blast
   155 
   156 lemma Int_greatest: "[| C\<subseteq>A;  C\<subseteq>B |] ==> C \<subseteq> A Int B"
   157 by blast
   158 
   159 lemma Int_cons: "cons(a,B) Int C \<subseteq> cons(a, B Int C)"
   160 by blast
   161 
   162 lemma Int_absorb [simp]: "A Int A = A"
   163 by blast
   164 
   165 lemma Int_left_absorb: "A Int (A Int B) = A Int B"
   166 by blast
   167 
   168 lemma Int_commute: "A Int B = B Int A"
   169 by blast
   170 
   171 lemma Int_left_commute: "A Int (B Int C) = B Int (A Int C)"
   172 by blast
   173 
   174 lemma Int_assoc: "(A Int B) Int C  =  A Int (B Int C)"
   175 by blast
   176 
   177 (*Intersection is an AC-operator*)
   178 lemmas Int_ac= Int_assoc Int_left_absorb Int_commute Int_left_commute
   179 
   180 lemma Int_absorb1: "B \<subseteq> A ==> A \<inter> B = B"
   181   by blast
   182 
   183 lemma Int_absorb2: "A \<subseteq> B ==> A \<inter> B = A"
   184   by blast
   185 
   186 lemma Int_Un_distrib: "A Int (B Un C) = (A Int B) Un (A Int C)"
   187 by blast
   188 
   189 lemma Int_Un_distrib2: "(B Un C) Int A = (B Int A) Un (C Int A)"
   190 by blast
   191 
   192 lemma subset_Int_iff: "A\<subseteq>B <-> A Int B = A"
   193 by (blast elim!: equalityE)
   194 
   195 lemma subset_Int_iff2: "A\<subseteq>B <-> B Int A = A"
   196 by (blast elim!: equalityE)
   197 
   198 lemma Int_Diff_eq: "C\<subseteq>A ==> (A-B) Int C = C-B"
   199 by blast
   200 
   201 lemma Int_cons_left:
   202      "cons(a,A) Int B = (if a \<in> B then cons(a, A Int B) else A Int B)"
   203 by auto
   204 
   205 lemma Int_cons_right:
   206      "A Int cons(a, B) = (if a \<in> A then cons(a, A Int B) else A Int B)"
   207 by auto
   208 
   209 lemma cons_Int_distrib: "cons(x, A \<inter> B) = cons(x, A) \<inter> cons(x, B)"
   210 by auto
   211 
   212 subsection{*Binary Union*}
   213 
   214 (** Union is the least upper bound of two sets *)
   215 
   216 lemma Un_subset_iff: "A Un B \<subseteq> C <-> A \<subseteq> C & B \<subseteq> C"
   217 by blast
   218 
   219 lemma Un_upper1: "A \<subseteq> A Un B"
   220 by blast
   221 
   222 lemma Un_upper2: "B \<subseteq> A Un B"
   223 by blast
   224 
   225 lemma Un_least: "[| A\<subseteq>C;  B\<subseteq>C |] ==> A Un B \<subseteq> C"
   226 by blast
   227 
   228 lemma Un_cons: "cons(a,B) Un C = cons(a, B Un C)"
   229 by blast
   230 
   231 lemma Un_absorb [simp]: "A Un A = A"
   232 by blast
   233 
   234 lemma Un_left_absorb: "A Un (A Un B) = A Un B"
   235 by blast
   236 
   237 lemma Un_commute: "A Un B = B Un A"
   238 by blast
   239 
   240 lemma Un_left_commute: "A Un (B Un C) = B Un (A Un C)"
   241 by blast
   242 
   243 lemma Un_assoc: "(A Un B) Un C  =  A Un (B Un C)"
   244 by blast
   245 
   246 (*Union is an AC-operator*)
   247 lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute
   248 
   249 lemma Un_absorb1: "A \<subseteq> B ==> A \<union> B = B"
   250   by blast
   251 
   252 lemma Un_absorb2: "B \<subseteq> A ==> A \<union> B = A"
   253   by blast
   254 
   255 lemma Un_Int_distrib: "(A Int B) Un C  =  (A Un C) Int (B Un C)"
   256 by blast
   257 
   258 lemma subset_Un_iff: "A\<subseteq>B <-> A Un B = B"
   259 by (blast elim!: equalityE)
   260 
   261 lemma subset_Un_iff2: "A\<subseteq>B <-> B Un A = B"
   262 by (blast elim!: equalityE)
   263 
   264 lemma Un_empty [iff]: "(A Un B = 0) <-> (A = 0 & B = 0)"
   265 by blast
   266 
   267 lemma Un_eq_Union: "A Un B = Union({A, B})"
   268 by blast
   269 
   270 subsection{*Set Difference*}
   271 
   272 lemma Diff_subset: "A-B \<subseteq> A"
   273 by blast
   274 
   275 lemma Diff_contains: "[| C\<subseteq>A;  C Int B = 0 |] ==> C \<subseteq> A-B"
   276 by blast
   277 
   278 lemma subset_Diff_cons_iff: "B \<subseteq> A - cons(c,C)  <->  B\<subseteq>A-C & c ~: B"
   279 by blast
   280 
   281 lemma Diff_cancel: "A - A = 0"
   282 by blast
   283 
   284 lemma Diff_triv: "A  Int B = 0 ==> A - B = A"
   285 by blast
   286 
   287 lemma empty_Diff [simp]: "0 - A = 0"
   288 by blast
   289 
   290 lemma Diff_0 [simp]: "A - 0 = A"
   291 by blast
   292 
   293 lemma Diff_eq_0_iff: "A - B = 0 <-> A \<subseteq> B"
   294 by (blast elim: equalityE)
   295 
   296 (*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
   297 lemma Diff_cons: "A - cons(a,B) = A - B - {a}"
   298 by blast
   299 
   300 (*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
   301 lemma Diff_cons2: "A - cons(a,B) = A - {a} - B"
   302 by blast
   303 
   304 lemma Diff_disjoint: "A Int (B-A) = 0"
   305 by blast
   306 
   307 lemma Diff_partition: "A\<subseteq>B ==> A Un (B-A) = B"
   308 by blast
   309 
   310 lemma subset_Un_Diff: "A \<subseteq> B Un (A - B)"
   311 by blast
   312 
   313 lemma double_complement: "[| A\<subseteq>B; B\<subseteq>C |] ==> B-(C-A) = A"
   314 by blast
   315 
   316 lemma double_complement_Un: "(A Un B) - (B-A) = A"
   317 by blast
   318 
   319 lemma Un_Int_crazy: 
   320  "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)"
   321 apply blast
   322 done
   323 
   324 lemma Diff_Un: "A - (B Un C) = (A-B) Int (A-C)"
   325 by blast
   326 
   327 lemma Diff_Int: "A - (B Int C) = (A-B) Un (A-C)"
   328 by blast
   329 
   330 lemma Un_Diff: "(A Un B) - C = (A - C) Un (B - C)"
   331 by blast
   332 
   333 lemma Int_Diff: "(A Int B) - C = A Int (B - C)"
   334 by blast
   335 
   336 lemma Diff_Int_distrib: "C Int (A-B) = (C Int A) - (C Int B)"
   337 by blast
   338 
   339 lemma Diff_Int_distrib2: "(A-B) Int C = (A Int C) - (B Int C)"
   340 by blast
   341 
   342 (*Halmos, Naive Set Theory, page 16.*)
   343 lemma Un_Int_assoc_iff: "(A Int B) Un C = A Int (B Un C)  <->  C\<subseteq>A"
   344 by (blast elim!: equalityE)
   345 
   346 
   347 subsection{*Big Union and Intersection*}
   348 
   349 (** Big Union is the least upper bound of a set  **)
   350 
   351 lemma Union_subset_iff: "Union(A) \<subseteq> C <-> (\<forall>x\<in>A. x \<subseteq> C)"
   352 by blast
   353 
   354 lemma Union_upper: "B\<in>A ==> B \<subseteq> Union(A)"
   355 by blast
   356 
   357 lemma Union_least: "[| !!x. x\<in>A ==> x\<subseteq>C |] ==> Union(A) \<subseteq> C"
   358 by blast
   359 
   360 lemma Union_cons [simp]: "Union(cons(a,B)) = a Un Union(B)"
   361 by blast
   362 
   363 lemma Union_Un_distrib: "Union(A Un B) = Union(A) Un Union(B)"
   364 by blast
   365 
   366 lemma Union_Int_subset: "Union(A Int B) \<subseteq> Union(A) Int Union(B)"
   367 by blast
   368 
   369 lemma Union_disjoint: "Union(C) Int A = 0 <-> (\<forall>B\<in>C. B Int A = 0)"
   370 by (blast elim!: equalityE)
   371 
   372 lemma Union_empty_iff: "Union(A) = 0 <-> (\<forall>B\<in>A. B=0)"
   373 by blast
   374 
   375 lemma Int_Union2: "Union(B) Int A = (\<Union>C\<in>B. C Int A)"
   376 by blast
   377 
   378 (** Big Intersection is the greatest lower bound of a nonempty set **)
   379 
   380 lemma Inter_subset_iff: "A\<noteq>0  ==>  C \<subseteq> Inter(A) <-> (\<forall>x\<in>A. C \<subseteq> x)"
   381 by blast
   382 
   383 lemma Inter_lower: "B\<in>A ==> Inter(A) \<subseteq> B"
   384 by blast
   385 
   386 lemma Inter_greatest: "[| A\<noteq>0;  !!x. x\<in>A ==> C\<subseteq>x |] ==> C \<subseteq> Inter(A)"
   387 by blast
   388 
   389 (** Intersection of a family of sets  **)
   390 
   391 lemma INT_lower: "x\<in>A ==> (\<Inter>x\<in>A. B(x)) \<subseteq> B(x)"
   392 by blast
   393 
   394 lemma INT_greatest: "[| A\<noteq>0;  !!x. x\<in>A ==> C\<subseteq>B(x) |] ==> C \<subseteq> (\<Inter>x\<in>A. B(x))"
   395 by force
   396 
   397 lemma Inter_0 [simp]: "Inter(0) = 0"
   398 by (unfold Inter_def, blast)
   399 
   400 lemma Inter_Un_subset:
   401      "[| z\<in>A; z\<in>B |] ==> Inter(A) Un Inter(B) \<subseteq> Inter(A Int B)"
   402 by blast
   403 
   404 (* A good challenge: Inter is ill-behaved on the empty set *)
   405 lemma Inter_Un_distrib:
   406      "[| A\<noteq>0;  B\<noteq>0 |] ==> Inter(A Un B) = Inter(A) Int Inter(B)"
   407 by blast
   408 
   409 lemma Union_singleton: "Union({b}) = b"
   410 by blast
   411 
   412 lemma Inter_singleton: "Inter({b}) = b"
   413 by blast
   414 
   415 lemma Inter_cons [simp]:
   416      "Inter(cons(a,B)) = (if B=0 then a else a Int Inter(B))"
   417 by force
   418 
   419 subsection{*Unions and Intersections of Families*}
   420 
   421 lemma subset_UN_iff_eq: "A \<subseteq> (\<Union>i\<in>I. B(i)) <-> A = (\<Union>i\<in>I. A Int B(i))"
   422 by (blast elim!: equalityE)
   423 
   424 lemma UN_subset_iff: "(\<Union>x\<in>A. B(x)) \<subseteq> C <-> (\<forall>x\<in>A. B(x) \<subseteq> C)"
   425 by blast
   426 
   427 lemma UN_upper: "x\<in>A ==> B(x) \<subseteq> (\<Union>x\<in>A. B(x))"
   428 by (erule RepFunI [THEN Union_upper])
   429 
   430 lemma UN_least: "[| !!x. x\<in>A ==> B(x)\<subseteq>C |] ==> (\<Union>x\<in>A. B(x)) \<subseteq> C"
   431 by blast
   432 
   433 lemma Union_eq_UN: "Union(A) = (\<Union>x\<in>A. x)"
   434 by blast
   435 
   436 lemma Inter_eq_INT: "Inter(A) = (\<Inter>x\<in>A. x)"
   437 by (unfold Inter_def, blast)
   438 
   439 lemma UN_0 [simp]: "(\<Union>i\<in>0. A(i)) = 0"
   440 by blast
   441 
   442 lemma UN_singleton: "(\<Union>x\<in>A. {x}) = A"
   443 by blast
   444 
   445 lemma UN_Un: "(\<Union>i\<in> A Un B. C(i)) = (\<Union>i\<in> A. C(i)) Un (\<Union>i\<in>B. C(i))"
   446 by blast
   447 
   448 lemma INT_Un: "(\<Inter>i\<in>I Un J. A(i)) = 
   449                (if I=0 then \<Inter>j\<in>J. A(j)  
   450                        else if J=0 then \<Inter>i\<in>I. A(i)  
   451                        else ((\<Inter>i\<in>I. A(i)) Int  (\<Inter>j\<in>J. A(j))))"
   452 by (simp, blast intro!: equalityI)
   453 
   454 lemma UN_UN_flatten: "(\<Union>x \<in> (\<Union>y\<in>A. B(y)). C(x)) = (\<Union>y\<in>A. \<Union>x\<in> B(y). C(x))"
   455 by blast
   456 
   457 (*Halmos, Naive Set Theory, page 35.*)
   458 lemma Int_UN_distrib: "B Int (\<Union>i\<in>I. A(i)) = (\<Union>i\<in>I. B Int A(i))"
   459 by blast
   460 
   461 lemma Un_INT_distrib: "I\<noteq>0 ==> B Un (\<Inter>i\<in>I. A(i)) = (\<Inter>i\<in>I. B Un A(i))"
   462 by auto
   463 
   464 lemma Int_UN_distrib2:
   465      "(\<Union>i\<in>I. A(i)) Int (\<Union>j\<in>J. B(j)) = (\<Union>i\<in>I. \<Union>j\<in>J. A(i) Int B(j))"
   466 by blast
   467 
   468 lemma Un_INT_distrib2: "[| I\<noteq>0;  J\<noteq>0 |] ==>  
   469       (\<Inter>i\<in>I. A(i)) Un (\<Inter>j\<in>J. B(j)) = (\<Inter>i\<in>I. \<Inter>j\<in>J. A(i) Un B(j))"
   470 by auto
   471 
   472 lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A=0 then 0 else c)"
   473 by force
   474 
   475 lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A=0 then 0 else c)"
   476 by force
   477 
   478 lemma UN_RepFun [simp]: "(\<Union>y\<in> RepFun(A,f). B(y)) = (\<Union>x\<in>A. B(f(x)))"
   479 by blast
   480 
   481 lemma INT_RepFun [simp]: "(\<Inter>x\<in>RepFun(A,f). B(x))    = (\<Inter>a\<in>A. B(f(a)))"
   482 by (auto simp add: Inter_def)
   483 
   484 lemma INT_Union_eq:
   485      "0 ~: A ==> (\<Inter>x\<in> Union(A). B(x)) = (\<Inter>y\<in>A. \<Inter>x\<in>y. B(x))"
   486 apply (subgoal_tac "\<forall>x\<in>A. x~=0")
   487  prefer 2 apply blast
   488 apply (force simp add: Inter_def ball_conj_distrib) 
   489 done
   490 
   491 lemma INT_UN_eq:
   492      "(\<forall>x\<in>A. B(x) ~= 0)  
   493       ==> (\<Inter>z\<in> (\<Union>x\<in>A. B(x)). C(z)) = (\<Inter>x\<in>A. \<Inter>z\<in> B(x). C(z))"
   494 apply (subst INT_Union_eq, blast)
   495 apply (simp add: Inter_def)
   496 done
   497 
   498 
   499 (** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
   500     Union of a family of unions **)
   501 
   502 lemma UN_Un_distrib:
   503      "(\<Union>i\<in>I. A(i) Un B(i)) = (\<Union>i\<in>I. A(i))  Un  (\<Union>i\<in>I. B(i))"
   504 by blast
   505 
   506 lemma INT_Int_distrib:
   507      "I\<noteq>0 ==> (\<Inter>i\<in>I. A(i) Int B(i)) = (\<Inter>i\<in>I. A(i)) Int (\<Inter>i\<in>I. B(i))"
   508 by (blast elim!: not_emptyE)
   509 
   510 lemma UN_Int_subset:
   511      "(\<Union>z\<in>I Int J. A(z)) \<subseteq> (\<Union>z\<in>I. A(z)) Int (\<Union>z\<in>J. A(z))"
   512 by blast
   513 
   514 (** Devlin, page 12, exercise 5: Complements **)
   515 
   516 lemma Diff_UN: "I\<noteq>0 ==> B - (\<Union>i\<in>I. A(i)) = (\<Inter>i\<in>I. B - A(i))"
   517 by (blast elim!: not_emptyE)
   518 
   519 lemma Diff_INT: "I\<noteq>0 ==> B - (\<Inter>i\<in>I. A(i)) = (\<Union>i\<in>I. B - A(i))"
   520 by (blast elim!: not_emptyE)
   521 
   522 
   523 (** Unions and Intersections with General Sum **)
   524 
   525 (*Not suitable for rewriting: LOOPS!*)
   526 lemma Sigma_cons1: "Sigma(cons(a,B), C) = ({a}*C(a)) Un Sigma(B,C)"
   527 by blast
   528 
   529 (*Not suitable for rewriting: LOOPS!*)
   530 lemma Sigma_cons2: "A * cons(b,B) = A*{b} Un A*B"
   531 by blast
   532 
   533 lemma Sigma_succ1: "Sigma(succ(A), B) = ({A}*B(A)) Un Sigma(A,B)"
   534 by blast
   535 
   536 lemma Sigma_succ2: "A * succ(B) = A*{B} Un A*B"
   537 by blast
   538 
   539 lemma SUM_UN_distrib1:
   540      "(\<Sigma> x \<in> (\<Union>y\<in>A. C(y)). B(x)) = (\<Union>y\<in>A. \<Sigma> x\<in>C(y). B(x))"
   541 by blast
   542 
   543 lemma SUM_UN_distrib2:
   544      "(\<Sigma> i\<in>I. \<Union>j\<in>J. C(i,j)) = (\<Union>j\<in>J. \<Sigma> i\<in>I. C(i,j))"
   545 by blast
   546 
   547 lemma SUM_Un_distrib1:
   548      "(\<Sigma> i\<in>I Un J. C(i)) = (\<Sigma> i\<in>I. C(i)) Un (\<Sigma> j\<in>J. C(j))"
   549 by blast
   550 
   551 lemma SUM_Un_distrib2:
   552      "(\<Sigma> i\<in>I. A(i) Un B(i)) = (\<Sigma> i\<in>I. A(i)) Un (\<Sigma> i\<in>I. B(i))"
   553 by blast
   554 
   555 (*First-order version of the above, for rewriting*)
   556 lemma prod_Un_distrib2: "I * (A Un B) = I*A Un I*B"
   557 by (rule SUM_Un_distrib2)
   558 
   559 lemma SUM_Int_distrib1:
   560      "(\<Sigma> i\<in>I Int J. C(i)) = (\<Sigma> i\<in>I. C(i)) Int (\<Sigma> j\<in>J. C(j))"
   561 by blast
   562 
   563 lemma SUM_Int_distrib2:
   564      "(\<Sigma> i\<in>I. A(i) Int B(i)) = (\<Sigma> i\<in>I. A(i)) Int (\<Sigma> i\<in>I. B(i))"
   565 by blast
   566 
   567 (*First-order version of the above, for rewriting*)
   568 lemma prod_Int_distrib2: "I * (A Int B) = I*A Int I*B"
   569 by (rule SUM_Int_distrib2)
   570 
   571 (*Cf Aczel, Non-Well-Founded Sets, page 115*)
   572 lemma SUM_eq_UN: "(\<Sigma> i\<in>I. A(i)) = (\<Union>i\<in>I. {i} * A(i))"
   573 by blast
   574 
   575 lemma times_subset_iff:
   576      "(A'*B' \<subseteq> A*B) <-> (A' = 0 | B' = 0 | (A'\<subseteq>A) & (B'\<subseteq>B))"
   577 by blast
   578 
   579 lemma Int_Sigma_eq:
   580      "(\<Sigma> x \<in> A'. B'(x)) Int (\<Sigma> x \<in> A. B(x)) = (\<Sigma> x \<in> A' Int A. B'(x) Int B(x))"
   581 by blast
   582 
   583 (** Domain **)
   584 
   585 lemma domain_iff: "a: domain(r) <-> (EX y. <a,y>\<in> r)"
   586 by (unfold domain_def, blast)
   587 
   588 lemma domainI [intro]: "<a,b>\<in> r ==> a: domain(r)"
   589 by (unfold domain_def, blast)
   590 
   591 lemma domainE [elim!]:
   592     "[| a \<in> domain(r);  !!y. <a,y>\<in> r ==> P |] ==> P"
   593 by (unfold domain_def, blast)
   594 
   595 lemma domain_subset: "domain(Sigma(A,B)) \<subseteq> A"
   596 by blast
   597 
   598 lemma domain_of_prod: "b\<in>B ==> domain(A*B) = A"
   599 by blast
   600 
   601 lemma domain_0 [simp]: "domain(0) = 0"
   602 by blast
   603 
   604 lemma domain_cons [simp]: "domain(cons(<a,b>,r)) = cons(a, domain(r))"
   605 by blast
   606 
   607 lemma domain_Un_eq [simp]: "domain(A Un B) = domain(A) Un domain(B)"
   608 by blast
   609 
   610 lemma domain_Int_subset: "domain(A Int B) \<subseteq> domain(A) Int domain(B)"
   611 by blast
   612 
   613 lemma domain_Diff_subset: "domain(A) - domain(B) \<subseteq> domain(A - B)"
   614 by blast
   615 
   616 lemma domain_UN: "domain(\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. domain(B(x)))"
   617 by blast
   618 
   619 lemma domain_Union: "domain(Union(A)) = (\<Union>x\<in>A. domain(x))"
   620 by blast
   621 
   622 
   623 (** Range **)
   624 
   625 lemma rangeI [intro]: "<a,b>\<in> r ==> b \<in> range(r)"
   626 apply (unfold range_def)
   627 apply (erule converseI [THEN domainI])
   628 done
   629 
   630 lemma rangeE [elim!]: "[| b \<in> range(r);  !!x. <x,b>\<in> r ==> P |] ==> P"
   631 by (unfold range_def, blast)
   632 
   633 lemma range_subset: "range(A*B) \<subseteq> B"
   634 apply (unfold range_def)
   635 apply (subst converse_prod)
   636 apply (rule domain_subset)
   637 done
   638 
   639 lemma range_of_prod: "a\<in>A ==> range(A*B) = B"
   640 by blast
   641 
   642 lemma range_0 [simp]: "range(0) = 0"
   643 by blast
   644 
   645 lemma range_cons [simp]: "range(cons(<a,b>,r)) = cons(b, range(r))"
   646 by blast
   647 
   648 lemma range_Un_eq [simp]: "range(A Un B) = range(A) Un range(B)"
   649 by blast
   650 
   651 lemma range_Int_subset: "range(A Int B) \<subseteq> range(A) Int range(B)"
   652 by blast
   653 
   654 lemma range_Diff_subset: "range(A) - range(B) \<subseteq> range(A - B)"
   655 by blast
   656 
   657 lemma domain_converse [simp]: "domain(converse(r)) = range(r)"
   658 by blast
   659 
   660 lemma range_converse [simp]: "range(converse(r)) = domain(r)"
   661 by blast
   662 
   663 
   664 (** Field **)
   665 
   666 lemma fieldI1: "<a,b>\<in> r ==> a \<in> field(r)"
   667 by (unfold field_def, blast)
   668 
   669 lemma fieldI2: "<a,b>\<in> r ==> b \<in> field(r)"
   670 by (unfold field_def, blast)
   671 
   672 lemma fieldCI [intro]: 
   673     "(~ <c,a>\<in>r ==> <a,b>\<in> r) ==> a \<in> field(r)"
   674 apply (unfold field_def, blast)
   675 done
   676 
   677 lemma fieldE [elim!]: 
   678      "[| a \<in> field(r);   
   679          !!x. <a,x>\<in> r ==> P;   
   680          !!x. <x,a>\<in> r ==> P        |] ==> P"
   681 by (unfold field_def, blast)
   682 
   683 lemma field_subset: "field(A*B) \<subseteq> A Un B"
   684 by blast
   685 
   686 lemma domain_subset_field: "domain(r) \<subseteq> field(r)"
   687 apply (unfold field_def)
   688 apply (rule Un_upper1)
   689 done
   690 
   691 lemma range_subset_field: "range(r) \<subseteq> field(r)"
   692 apply (unfold field_def)
   693 apply (rule Un_upper2)
   694 done
   695 
   696 lemma domain_times_range: "r \<subseteq> Sigma(A,B) ==> r \<subseteq> domain(r)*range(r)"
   697 by blast
   698 
   699 lemma field_times_field: "r \<subseteq> Sigma(A,B) ==> r \<subseteq> field(r)*field(r)"
   700 by blast
   701 
   702 lemma relation_field_times_field: "relation(r) ==> r \<subseteq> field(r)*field(r)"
   703 by (simp add: relation_def, blast) 
   704 
   705 lemma field_of_prod: "field(A*A) = A"
   706 by blast
   707 
   708 lemma field_0 [simp]: "field(0) = 0"
   709 by blast
   710 
   711 lemma field_cons [simp]: "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))"
   712 by blast
   713 
   714 lemma field_Un_eq [simp]: "field(A Un B) = field(A) Un field(B)"
   715 by blast
   716 
   717 lemma field_Int_subset: "field(A Int B) \<subseteq> field(A) Int field(B)"
   718 by blast
   719 
   720 lemma field_Diff_subset: "field(A) - field(B) \<subseteq> field(A - B)"
   721 by blast
   722 
   723 lemma field_converse [simp]: "field(converse(r)) = field(r)"
   724 by blast
   725 
   726 (** The Union of a set of relations is a relation -- Lemma for fun_Union **)
   727 lemma rel_Union: "(\<forall>x\<in>S. EX A B. x \<subseteq> A*B) ==>   
   728                   Union(S) \<subseteq> domain(Union(S)) * range(Union(S))"
   729 by blast
   730 
   731 (** The Union of 2 relations is a relation (Lemma for fun_Un)  **)
   732 lemma rel_Un: "[| r \<subseteq> A*B;  s \<subseteq> C*D |] ==> (r Un s) \<subseteq> (A Un C) * (B Un D)"
   733 by blast
   734 
   735 lemma domain_Diff_eq: "[| <a,c> \<in> r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)"
   736 by blast
   737 
   738 lemma range_Diff_eq: "[| <c,b> \<in> r; c~=a |] ==> range(r-{<a,b>}) = range(r)"
   739 by blast
   740 
   741 
   742 subsection{*Image of a Set under a Function or Relation*}
   743 
   744 lemma image_iff: "b \<in> r``A <-> (\<exists>x\<in>A. <x,b>\<in>r)"
   745 by (unfold image_def, blast)
   746 
   747 lemma image_singleton_iff: "b \<in> r``{a} <-> <a,b>\<in>r"
   748 by (rule image_iff [THEN iff_trans], blast)
   749 
   750 lemma imageI [intro]: "[| <a,b>\<in> r;  a\<in>A |] ==> b \<in> r``A"
   751 by (unfold image_def, blast)
   752 
   753 lemma imageE [elim!]: 
   754     "[| b: r``A;  !!x.[| <x,b>\<in> r;  x\<in>A |] ==> P |] ==> P"
   755 by (unfold image_def, blast)
   756 
   757 lemma image_subset: "r \<subseteq> A*B ==> r``C \<subseteq> B"
   758 by blast
   759 
   760 lemma image_0 [simp]: "r``0 = 0"
   761 by blast
   762 
   763 lemma image_Un [simp]: "r``(A Un B) = (r``A) Un (r``B)"
   764 by blast
   765 
   766 lemma image_UN: "r `` (\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. r `` B(x))"
   767 by blast
   768 
   769 lemma Collect_image_eq:
   770      "{z \<in> Sigma(A,B). P(z)} `` C = (\<Union>x \<in> A. {y \<in> B(x). x \<in> C & P(<x,y>)})"
   771 by blast
   772 
   773 lemma image_Int_subset: "r``(A Int B) \<subseteq> (r``A) Int (r``B)"
   774 by blast
   775 
   776 lemma image_Int_square_subset: "(r Int A*A)``B \<subseteq> (r``B) Int A"
   777 by blast
   778 
   779 lemma image_Int_square: "B\<subseteq>A ==> (r Int A*A)``B = (r``B) Int A"
   780 by blast
   781 
   782 
   783 (*Image laws for special relations*)
   784 lemma image_0_left [simp]: "0``A = 0"
   785 by blast
   786 
   787 lemma image_Un_left: "(r Un s)``A = (r``A) Un (s``A)"
   788 by blast
   789 
   790 lemma image_Int_subset_left: "(r Int s)``A \<subseteq> (r``A) Int (s``A)"
   791 by blast
   792 
   793 
   794 subsection{*Inverse Image of a Set under a Function or Relation*}
   795 
   796 lemma vimage_iff: 
   797     "a \<in> r-``B <-> (\<exists>y\<in>B. <a,y>\<in>r)"
   798 by (unfold vimage_def image_def converse_def, blast)
   799 
   800 lemma vimage_singleton_iff: "a \<in> r-``{b} <-> <a,b>\<in>r"
   801 by (rule vimage_iff [THEN iff_trans], blast)
   802 
   803 lemma vimageI [intro]: "[| <a,b>\<in> r;  b\<in>B |] ==> a \<in> r-``B"
   804 by (unfold vimage_def, blast)
   805 
   806 lemma vimageE [elim!]: 
   807     "[| a: r-``B;  !!x.[| <a,x>\<in> r;  x\<in>B |] ==> P |] ==> P"
   808 apply (unfold vimage_def, blast)
   809 done
   810 
   811 lemma vimage_subset: "r \<subseteq> A*B ==> r-``C \<subseteq> A"
   812 apply (unfold vimage_def)
   813 apply (erule converse_type [THEN image_subset])
   814 done
   815 
   816 lemma vimage_0 [simp]: "r-``0 = 0"
   817 by blast
   818 
   819 lemma vimage_Un [simp]: "r-``(A Un B) = (r-``A) Un (r-``B)"
   820 by blast
   821 
   822 lemma vimage_Int_subset: "r-``(A Int B) \<subseteq> (r-``A) Int (r-``B)"
   823 by blast
   824 
   825 (*NOT suitable for rewriting*)
   826 lemma vimage_eq_UN: "f -``B = (\<Union>y\<in>B. f-``{y})"
   827 by blast
   828 
   829 lemma function_vimage_Int:
   830      "function(f) ==> f-``(A Int B) = (f-``A)  Int  (f-``B)"
   831 by (unfold function_def, blast)
   832 
   833 lemma function_vimage_Diff: "function(f) ==> f-``(A-B) = (f-``A) - (f-``B)"
   834 by (unfold function_def, blast)
   835 
   836 lemma function_image_vimage: "function(f) ==> f `` (f-`` A) \<subseteq> A"
   837 by (unfold function_def, blast)
   838 
   839 lemma vimage_Int_square_subset: "(r Int A*A)-``B \<subseteq> (r-``B) Int A"
   840 by blast
   841 
   842 lemma vimage_Int_square: "B\<subseteq>A ==> (r Int A*A)-``B = (r-``B) Int A"
   843 by blast
   844 
   845 
   846 
   847 (*Invese image laws for special relations*)
   848 lemma vimage_0_left [simp]: "0-``A = 0"
   849 by blast
   850 
   851 lemma vimage_Un_left: "(r Un s)-``A = (r-``A) Un (s-``A)"
   852 by blast
   853 
   854 lemma vimage_Int_subset_left: "(r Int s)-``A \<subseteq> (r-``A) Int (s-``A)"
   855 by blast
   856 
   857 
   858 (** Converse **)
   859 
   860 lemma converse_Un [simp]: "converse(A Un B) = converse(A) Un converse(B)"
   861 by blast
   862 
   863 lemma converse_Int [simp]: "converse(A Int B) = converse(A) Int converse(B)"
   864 by blast
   865 
   866 lemma converse_Diff [simp]: "converse(A - B) = converse(A) - converse(B)"
   867 by blast
   868 
   869 lemma converse_UN [simp]: "converse(\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. converse(B(x)))"
   870 by blast
   871 
   872 (*Unfolding Inter avoids using excluded middle on A=0*)
   873 lemma converse_INT [simp]:
   874      "converse(\<Inter>x\<in>A. B(x)) = (\<Inter>x\<in>A. converse(B(x)))"
   875 apply (unfold Inter_def, blast)
   876 done
   877 
   878 
   879 subsection{*Powerset Operator*}
   880 
   881 lemma Pow_0 [simp]: "Pow(0) = {0}"
   882 by blast
   883 
   884 lemma Pow_insert: "Pow (cons(a,A)) = Pow(A) Un {cons(a,X) . X: Pow(A)}"
   885 apply (rule equalityI, safe)
   886 apply (erule swap)
   887 apply (rule_tac a = "x-{a}" in RepFun_eqI, auto) 
   888 done
   889 
   890 lemma Un_Pow_subset: "Pow(A) Un Pow(B) \<subseteq> Pow(A Un B)"
   891 by blast
   892 
   893 lemma UN_Pow_subset: "(\<Union>x\<in>A. Pow(B(x))) \<subseteq> Pow(\<Union>x\<in>A. B(x))"
   894 by blast
   895 
   896 lemma subset_Pow_Union: "A \<subseteq> Pow(Union(A))"
   897 by blast
   898 
   899 lemma Union_Pow_eq [simp]: "Union(Pow(A)) = A"
   900 by blast
   901 
   902 lemma Union_Pow_iff: "Union(A) \<in> Pow(B) <-> A \<in> Pow(Pow(B))"
   903 by blast
   904 
   905 lemma Pow_Int_eq [simp]: "Pow(A Int B) = Pow(A) Int Pow(B)"
   906 by blast
   907 
   908 lemma Pow_INT_eq: "A\<noteq>0 ==> Pow(\<Inter>x\<in>A. B(x)) = (\<Inter>x\<in>A. Pow(B(x)))"
   909 by (blast elim!: not_emptyE)
   910 
   911 
   912 subsection{*RepFun*}
   913 
   914 lemma RepFun_subset: "[| !!x. x\<in>A ==> f(x) \<in> B |] ==> {f(x). x\<in>A} \<subseteq> B"
   915 by blast
   916 
   917 lemma RepFun_eq_0_iff [simp]: "{f(x).x\<in>A}=0 <-> A=0"
   918 by blast
   919 
   920 lemma RepFun_constant [simp]: "{c. x\<in>A} = (if A=0 then 0 else {c})"
   921 by force
   922 
   923 
   924 subsection{*Collect*}
   925 
   926 lemma Collect_subset: "Collect(A,P) \<subseteq> A"
   927 by blast
   928 
   929 lemma Collect_Un: "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)"
   930 by blast
   931 
   932 lemma Collect_Int: "Collect(A Int B, P) = Collect(A,P) Int Collect(B,P)"
   933 by blast
   934 
   935 lemma Collect_Diff: "Collect(A - B, P) = Collect(A,P) - Collect(B,P)"
   936 by blast
   937 
   938 lemma Collect_cons: "{x\<in>cons(a,B). P(x)} =  
   939       (if P(a) then cons(a, {x\<in>B. P(x)}) else {x\<in>B. P(x)})"
   940 by (simp, blast)
   941 
   942 lemma Int_Collect_self_eq: "A Int Collect(A,P) = Collect(A,P)"
   943 by blast
   944 
   945 lemma Collect_Collect_eq [simp]:
   946      "Collect(Collect(A,P), Q) = Collect(A, %x. P(x) & Q(x))"
   947 by blast
   948 
   949 lemma Collect_Int_Collect_eq:
   950      "Collect(A,P) Int Collect(A,Q) = Collect(A, %x. P(x) & Q(x))"
   951 by blast
   952 
   953 lemma Collect_Union_eq [simp]:
   954      "Collect(\<Union>x\<in>A. B(x), P) = (\<Union>x\<in>A. Collect(B(x), P))"
   955 by blast
   956 
   957 lemma Collect_Int_left: "{x\<in>A. P(x)} Int B = {x \<in> A Int B. P(x)}"
   958 by blast
   959 
   960 lemma Collect_Int_right: "A Int {x\<in>B. P(x)} = {x \<in> A Int B. P(x)}"
   961 by blast
   962 
   963 lemma Collect_disj_eq: "{x\<in>A. P(x) | Q(x)} = Collect(A, P) Un Collect(A, Q)"
   964 by blast
   965 
   966 lemma Collect_conj_eq: "{x\<in>A. P(x) & Q(x)} = Collect(A, P) Int Collect(A, Q)"
   967 by blast
   968 
   969 lemmas subset_SIs = subset_refl cons_subsetI subset_consI 
   970                     Union_least UN_least Un_least 
   971                     Inter_greatest Int_greatest RepFun_subset
   972                     Un_upper1 Un_upper2 Int_lower1 Int_lower2
   973 
   974 (*First, ML bindings from the old file subset.ML*)
   975 ML
   976 {*
   977 val cons_subsetI = thm "cons_subsetI";
   978 val subset_consI = thm "subset_consI";
   979 val cons_subset_iff = thm "cons_subset_iff";
   980 val cons_subsetE = thm "cons_subsetE";
   981 val subset_empty_iff = thm "subset_empty_iff";
   982 val subset_cons_iff = thm "subset_cons_iff";
   983 val subset_succI = thm "subset_succI";
   984 val succ_subsetI = thm "succ_subsetI";
   985 val succ_subsetE = thm "succ_subsetE";
   986 val succ_subset_iff = thm "succ_subset_iff";
   987 val singleton_subsetI = thm "singleton_subsetI";
   988 val singleton_subsetD = thm "singleton_subsetD";
   989 val Union_subset_iff = thm "Union_subset_iff";
   990 val Union_upper = thm "Union_upper";
   991 val Union_least = thm "Union_least";
   992 val subset_UN_iff_eq = thm "subset_UN_iff_eq";
   993 val UN_subset_iff = thm "UN_subset_iff";
   994 val UN_upper = thm "UN_upper";
   995 val UN_least = thm "UN_least";
   996 val Inter_subset_iff = thm "Inter_subset_iff";
   997 val Inter_lower = thm "Inter_lower";
   998 val Inter_greatest = thm "Inter_greatest";
   999 val INT_lower = thm "INT_lower";
  1000 val INT_greatest = thm "INT_greatest";
  1001 val Un_subset_iff = thm "Un_subset_iff";
  1002 val Un_upper1 = thm "Un_upper1";
  1003 val Un_upper2 = thm "Un_upper2";
  1004 val Un_least = thm "Un_least";
  1005 val Int_subset_iff = thm "Int_subset_iff";
  1006 val Int_lower1 = thm "Int_lower1";
  1007 val Int_lower2 = thm "Int_lower2";
  1008 val Int_greatest = thm "Int_greatest";
  1009 val Diff_subset = thm "Diff_subset";
  1010 val Diff_contains = thm "Diff_contains";
  1011 val subset_Diff_cons_iff = thm "subset_Diff_cons_iff";
  1012 val Collect_subset = thm "Collect_subset";
  1013 val RepFun_subset = thm "RepFun_subset";
  1014 
  1015 val subset_SIs = thms "subset_SIs";
  1016 
  1017 val subset_cs = claset() 
  1018     delrules [subsetI, subsetCE]
  1019     addSIs subset_SIs
  1020     addIs  [Union_upper, Inter_lower]
  1021     addSEs [cons_subsetE];
  1022 *}
  1023 (*subset_cs is a claset for subset reasoning*)
  1024 
  1025 ML
  1026 {*
  1027 val ZF_cs = claset() delrules [equalityI];
  1028 
  1029 val in_mono = thm "in_mono";
  1030 val conj_mono = thm "conj_mono";
  1031 val disj_mono = thm "disj_mono";
  1032 val imp_mono = thm "imp_mono";
  1033 val imp_refl = thm "imp_refl";
  1034 val ex_mono = thm "ex_mono";
  1035 val all_mono = thm "all_mono";
  1036 
  1037 val converse_iff = thm "converse_iff";
  1038 val converseI = thm "converseI";
  1039 val converseD = thm "converseD";
  1040 val converseE = thm "converseE";
  1041 val converse_converse = thm "converse_converse";
  1042 val converse_type = thm "converse_type";
  1043 val converse_prod = thm "converse_prod";
  1044 val converse_empty = thm "converse_empty";
  1045 val converse_subset_iff = thm "converse_subset_iff";
  1046 val domain_iff = thm "domain_iff";
  1047 val domainI = thm "domainI";
  1048 val domainE = thm "domainE";
  1049 val domain_subset = thm "domain_subset";
  1050 val rangeI = thm "rangeI";
  1051 val rangeE = thm "rangeE";
  1052 val range_subset = thm "range_subset";
  1053 val fieldI1 = thm "fieldI1";
  1054 val fieldI2 = thm "fieldI2";
  1055 val fieldCI = thm "fieldCI";
  1056 val fieldE = thm "fieldE";
  1057 val field_subset = thm "field_subset";
  1058 val domain_subset_field = thm "domain_subset_field";
  1059 val range_subset_field = thm "range_subset_field";
  1060 val domain_times_range = thm "domain_times_range";
  1061 val field_times_field = thm "field_times_field";
  1062 val image_iff = thm "image_iff";
  1063 val image_singleton_iff = thm "image_singleton_iff";
  1064 val imageI = thm "imageI";
  1065 val imageE = thm "imageE";
  1066 val image_subset = thm "image_subset";
  1067 val vimage_iff = thm "vimage_iff";
  1068 val vimage_singleton_iff = thm "vimage_singleton_iff";
  1069 val vimageI = thm "vimageI";
  1070 val vimageE = thm "vimageE";
  1071 val vimage_subset = thm "vimage_subset";
  1072 val rel_Union = thm "rel_Union";
  1073 val rel_Un = thm "rel_Un";
  1074 val domain_Diff_eq = thm "domain_Diff_eq";
  1075 val range_Diff_eq = thm "range_Diff_eq";
  1076 val cons_eq = thm "cons_eq";
  1077 val cons_commute = thm "cons_commute";
  1078 val cons_absorb = thm "cons_absorb";
  1079 val cons_Diff = thm "cons_Diff";
  1080 val equal_singleton = thm "equal_singleton";
  1081 val Int_cons = thm "Int_cons";
  1082 val Int_absorb = thm "Int_absorb";
  1083 val Int_left_absorb = thm "Int_left_absorb";
  1084 val Int_commute = thm "Int_commute";
  1085 val Int_left_commute = thm "Int_left_commute";
  1086 val Int_assoc = thm "Int_assoc";
  1087 val Int_Un_distrib = thm "Int_Un_distrib";
  1088 val Int_Un_distrib2 = thm "Int_Un_distrib2";
  1089 val subset_Int_iff = thm "subset_Int_iff";
  1090 val subset_Int_iff2 = thm "subset_Int_iff2";
  1091 val Int_Diff_eq = thm "Int_Diff_eq";
  1092 val Int_cons_left = thm "Int_cons_left";
  1093 val Int_cons_right = thm "Int_cons_right";
  1094 val Un_cons = thm "Un_cons";
  1095 val Un_absorb = thm "Un_absorb";
  1096 val Un_left_absorb = thm "Un_left_absorb";
  1097 val Un_commute = thm "Un_commute";
  1098 val Un_left_commute = thm "Un_left_commute";
  1099 val Un_assoc = thm "Un_assoc";
  1100 val Un_Int_distrib = thm "Un_Int_distrib";
  1101 val subset_Un_iff = thm "subset_Un_iff";
  1102 val subset_Un_iff2 = thm "subset_Un_iff2";
  1103 val Un_empty = thm "Un_empty";
  1104 val Un_eq_Union = thm "Un_eq_Union";
  1105 val Diff_cancel = thm "Diff_cancel";
  1106 val Diff_triv = thm "Diff_triv";
  1107 val empty_Diff = thm "empty_Diff";
  1108 val Diff_0 = thm "Diff_0";
  1109 val Diff_eq_0_iff = thm "Diff_eq_0_iff";
  1110 val Diff_cons = thm "Diff_cons";
  1111 val Diff_cons2 = thm "Diff_cons2";
  1112 val Diff_disjoint = thm "Diff_disjoint";
  1113 val Diff_partition = thm "Diff_partition";
  1114 val subset_Un_Diff = thm "subset_Un_Diff";
  1115 val double_complement = thm "double_complement";
  1116 val double_complement_Un = thm "double_complement_Un";
  1117 val Un_Int_crazy = thm "Un_Int_crazy";
  1118 val Diff_Un = thm "Diff_Un";
  1119 val Diff_Int = thm "Diff_Int";
  1120 val Un_Diff = thm "Un_Diff";
  1121 val Int_Diff = thm "Int_Diff";
  1122 val Diff_Int_distrib = thm "Diff_Int_distrib";
  1123 val Diff_Int_distrib2 = thm "Diff_Int_distrib2";
  1124 val Un_Int_assoc_iff = thm "Un_Int_assoc_iff";
  1125 val Union_cons = thm "Union_cons";
  1126 val Union_Un_distrib = thm "Union_Un_distrib";
  1127 val Union_Int_subset = thm "Union_Int_subset";
  1128 val Union_disjoint = thm "Union_disjoint";
  1129 val Union_empty_iff = thm "Union_empty_iff";
  1130 val Int_Union2 = thm "Int_Union2";
  1131 val Inter_0 = thm "Inter_0";
  1132 val Inter_Un_subset = thm "Inter_Un_subset";
  1133 val Inter_Un_distrib = thm "Inter_Un_distrib";
  1134 val Union_singleton = thm "Union_singleton";
  1135 val Inter_singleton = thm "Inter_singleton";
  1136 val Inter_cons = thm "Inter_cons";
  1137 val Union_eq_UN = thm "Union_eq_UN";
  1138 val Inter_eq_INT = thm "Inter_eq_INT";
  1139 val UN_0 = thm "UN_0";
  1140 val UN_singleton = thm "UN_singleton";
  1141 val UN_Un = thm "UN_Un";
  1142 val INT_Un = thm "INT_Un";
  1143 val UN_UN_flatten = thm "UN_UN_flatten";
  1144 val Int_UN_distrib = thm "Int_UN_distrib";
  1145 val Un_INT_distrib = thm "Un_INT_distrib";
  1146 val Int_UN_distrib2 = thm "Int_UN_distrib2";
  1147 val Un_INT_distrib2 = thm "Un_INT_distrib2";
  1148 val UN_constant = thm "UN_constant";
  1149 val INT_constant = thm "INT_constant";
  1150 val UN_RepFun = thm "UN_RepFun";
  1151 val INT_RepFun = thm "INT_RepFun";
  1152 val INT_Union_eq = thm "INT_Union_eq";
  1153 val INT_UN_eq = thm "INT_UN_eq";
  1154 val UN_Un_distrib = thm "UN_Un_distrib";
  1155 val INT_Int_distrib = thm "INT_Int_distrib";
  1156 val UN_Int_subset = thm "UN_Int_subset";
  1157 val Diff_UN = thm "Diff_UN";
  1158 val Diff_INT = thm "Diff_INT";
  1159 val Sigma_cons1 = thm "Sigma_cons1";
  1160 val Sigma_cons2 = thm "Sigma_cons2";
  1161 val Sigma_succ1 = thm "Sigma_succ1";
  1162 val Sigma_succ2 = thm "Sigma_succ2";
  1163 val SUM_UN_distrib1 = thm "SUM_UN_distrib1";
  1164 val SUM_UN_distrib2 = thm "SUM_UN_distrib2";
  1165 val SUM_Un_distrib1 = thm "SUM_Un_distrib1";
  1166 val SUM_Un_distrib2 = thm "SUM_Un_distrib2";
  1167 val prod_Un_distrib2 = thm "prod_Un_distrib2";
  1168 val SUM_Int_distrib1 = thm "SUM_Int_distrib1";
  1169 val SUM_Int_distrib2 = thm "SUM_Int_distrib2";
  1170 val prod_Int_distrib2 = thm "prod_Int_distrib2";
  1171 val SUM_eq_UN = thm "SUM_eq_UN";
  1172 val domain_of_prod = thm "domain_of_prod";
  1173 val domain_0 = thm "domain_0";
  1174 val domain_cons = thm "domain_cons";
  1175 val domain_Un_eq = thm "domain_Un_eq";
  1176 val domain_Int_subset = thm "domain_Int_subset";
  1177 val domain_Diff_subset = thm "domain_Diff_subset";
  1178 val domain_converse = thm "domain_converse";
  1179 val domain_UN = thm "domain_UN";
  1180 val domain_Union = thm "domain_Union";
  1181 val range_of_prod = thm "range_of_prod";
  1182 val range_0 = thm "range_0";
  1183 val range_cons = thm "range_cons";
  1184 val range_Un_eq = thm "range_Un_eq";
  1185 val range_Int_subset = thm "range_Int_subset";
  1186 val range_Diff_subset = thm "range_Diff_subset";
  1187 val range_converse = thm "range_converse";
  1188 val field_of_prod = thm "field_of_prod";
  1189 val field_0 = thm "field_0";
  1190 val field_cons = thm "field_cons";
  1191 val field_Un_eq = thm "field_Un_eq";
  1192 val field_Int_subset = thm "field_Int_subset";
  1193 val field_Diff_subset = thm "field_Diff_subset";
  1194 val field_converse = thm "field_converse";
  1195 val image_0 = thm "image_0";
  1196 val image_Un = thm "image_Un";
  1197 val image_Int_subset = thm "image_Int_subset";
  1198 val image_Int_square_subset = thm "image_Int_square_subset";
  1199 val image_Int_square = thm "image_Int_square";
  1200 val image_0_left = thm "image_0_left";
  1201 val image_Un_left = thm "image_Un_left";
  1202 val image_Int_subset_left = thm "image_Int_subset_left";
  1203 val vimage_0 = thm "vimage_0";
  1204 val vimage_Un = thm "vimage_Un";
  1205 val vimage_Int_subset = thm "vimage_Int_subset";
  1206 val vimage_eq_UN = thm "vimage_eq_UN";
  1207 val function_vimage_Int = thm "function_vimage_Int";
  1208 val function_vimage_Diff = thm "function_vimage_Diff";
  1209 val function_image_vimage = thm "function_image_vimage";
  1210 val vimage_Int_square_subset = thm "vimage_Int_square_subset";
  1211 val vimage_Int_square = thm "vimage_Int_square";
  1212 val vimage_0_left = thm "vimage_0_left";
  1213 val vimage_Un_left = thm "vimage_Un_left";
  1214 val vimage_Int_subset_left = thm "vimage_Int_subset_left";
  1215 val converse_Un = thm "converse_Un";
  1216 val converse_Int = thm "converse_Int";
  1217 val converse_Diff = thm "converse_Diff";
  1218 val converse_UN = thm "converse_UN";
  1219 val converse_INT = thm "converse_INT";
  1220 val Pow_0 = thm "Pow_0";
  1221 val Pow_insert = thm "Pow_insert";
  1222 val Un_Pow_subset = thm "Un_Pow_subset";
  1223 val UN_Pow_subset = thm "UN_Pow_subset";
  1224 val subset_Pow_Union = thm "subset_Pow_Union";
  1225 val Union_Pow_eq = thm "Union_Pow_eq";
  1226 val Union_Pow_iff = thm "Union_Pow_iff";
  1227 val Pow_Int_eq = thm "Pow_Int_eq";
  1228 val Pow_INT_eq = thm "Pow_INT_eq";
  1229 val RepFun_eq_0_iff = thm "RepFun_eq_0_iff";
  1230 val RepFun_constant = thm "RepFun_constant";
  1231 val Collect_Un = thm "Collect_Un";
  1232 val Collect_Int = thm "Collect_Int";
  1233 val Collect_Diff = thm "Collect_Diff";
  1234 val Collect_cons = thm "Collect_cons";
  1235 val Int_Collect_self_eq = thm "Int_Collect_self_eq";
  1236 val Collect_Collect_eq = thm "Collect_Collect_eq";
  1237 val Collect_Int_Collect_eq = thm "Collect_Int_Collect_eq";
  1238 val Collect_disj_eq = thm "Collect_disj_eq";
  1239 val Collect_conj_eq = thm "Collect_conj_eq";
  1240 
  1241 val Int_ac = thms "Int_ac";
  1242 val Un_ac = thms "Un_ac";
  1243 val Int_absorb1 = thm "Int_absorb1";
  1244 val Int_absorb2 = thm "Int_absorb2";
  1245 val Un_absorb1 = thm "Un_absorb1";
  1246 val Un_absorb2 = thm "Un_absorb2";
  1247 *}
  1248  
  1249 end
  1250