src/ZF/ZF.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 6 8ce8c4d13d4d
permissions -rw-r--r--
Initial revision
clasohm@0
     1
(*  Title: 	ZF/zf.ML
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
clasohm@0
     4
    Copyright   1992  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Basic introduction and elimination rules for Zermelo-Fraenkel Set Theory 
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
open ZF;
clasohm@0
    10
clasohm@0
    11
signature ZF_LEMMAS = 
clasohm@0
    12
  sig
clasohm@0
    13
  val ballE : thm
clasohm@0
    14
  val ballI : thm
clasohm@0
    15
  val ball_cong : thm
clasohm@0
    16
  val ball_rew : thm
clasohm@0
    17
  val ball_tac : int -> tactic
clasohm@0
    18
  val basic_ZF_congs : thm list
clasohm@0
    19
  val bexCI : thm
clasohm@0
    20
  val bexE : thm
clasohm@0
    21
  val bexI : thm
clasohm@0
    22
  val bex_cong : thm
clasohm@0
    23
  val bspec : thm
clasohm@0
    24
  val CollectD1 : thm
clasohm@0
    25
  val CollectD2 : thm
clasohm@0
    26
  val CollectE : thm
clasohm@0
    27
  val CollectI : thm
clasohm@0
    28
  val Collect_cong : thm
clasohm@0
    29
  val emptyE : thm
clasohm@0
    30
  val empty_subsetI : thm
clasohm@0
    31
  val equalityCE : thm
clasohm@0
    32
  val equalityD1 : thm
clasohm@0
    33
  val equalityD2 : thm
clasohm@0
    34
  val equalityE : thm
clasohm@0
    35
  val equalityI : thm
clasohm@0
    36
  val equality_iffI : thm
clasohm@0
    37
  val equals0D : thm
clasohm@0
    38
  val equals0I : thm
clasohm@0
    39
  val ex1_functional : thm
clasohm@0
    40
  val InterD : thm
clasohm@0
    41
  val InterE : thm
clasohm@0
    42
  val InterI : thm
clasohm@0
    43
  val INT_E : thm
clasohm@0
    44
  val INT_I : thm
clasohm@0
    45
  val lemmas_cs : claset
clasohm@0
    46
  val PowD : thm
clasohm@0
    47
  val PowI : thm
clasohm@0
    48
  val prove_cong_tac : thm list -> int -> tactic
clasohm@0
    49
  val RepFunE : thm
clasohm@0
    50
  val RepFunI : thm
clasohm@0
    51
  val RepFun_eqI : thm
clasohm@0
    52
  val RepFun_cong : thm
clasohm@0
    53
  val ReplaceE : thm
clasohm@0
    54
  val ReplaceI : thm
clasohm@0
    55
  val Replace_iff : thm
clasohm@0
    56
  val Replace_cong : thm
clasohm@0
    57
  val rev_ballE : thm
clasohm@0
    58
  val rev_bspec : thm
clasohm@0
    59
  val rev_subsetD : thm
clasohm@0
    60
  val separation : thm
clasohm@0
    61
  val setup_induction : thm
clasohm@0
    62
  val set_mp_tac : int -> tactic
clasohm@0
    63
  val subsetCE : thm
clasohm@0
    64
  val subsetD : thm
clasohm@0
    65
  val subsetI : thm
clasohm@0
    66
  val subset_refl : thm
clasohm@0
    67
  val subset_trans : thm
clasohm@0
    68
  val UnionE : thm
clasohm@0
    69
  val UnionI : thm
clasohm@0
    70
  val UN_E : thm
clasohm@0
    71
  val UN_I : thm
clasohm@0
    72
  end;
clasohm@0
    73
clasohm@0
    74
clasohm@0
    75
structure ZF_Lemmas : ZF_LEMMAS = 
clasohm@0
    76
struct
clasohm@0
    77
clasohm@0
    78
val basic_ZF_congs = mk_congs ZF.thy 
clasohm@0
    79
    ["op `", "op ``", "op Int", "op Un", "op -", "op <=", "op :", 
clasohm@0
    80
     "Pow", "Union", "Inter", "fst", "snd", "succ", "Pair", "Upair", "cons",
clasohm@0
    81
     "domain", "range", "restrict"];
clasohm@0
    82
clasohm@0
    83
fun prove_cong_tac prems i =
clasohm@0
    84
    REPEAT (ares_tac (prems@[refl]@FOL_congs@basic_ZF_congs) i);
clasohm@0
    85
clasohm@0
    86
(*** Bounded universal quantifier ***)
clasohm@0
    87
clasohm@0
    88
val ballI = prove_goalw ZF.thy [Ball_def]
clasohm@0
    89
    "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)"
clasohm@0
    90
 (fn prems=> [ (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ]);
clasohm@0
    91
clasohm@0
    92
val bspec = prove_goalw ZF.thy [Ball_def]
clasohm@0
    93
    "[| ALL x:A. P(x);  x: A |] ==> P(x)"
clasohm@0
    94
 (fn major::prems=>
clasohm@0
    95
  [ (rtac (major RS spec RS mp) 1),
clasohm@0
    96
    (resolve_tac prems 1) ]);
clasohm@0
    97
clasohm@0
    98
val ballE = prove_goalw ZF.thy [Ball_def]
clasohm@0
    99
    "[| ALL x:A. P(x);  P(x) ==> Q;  ~ x:A ==> Q |] ==> Q"
clasohm@0
   100
 (fn major::prems=>
clasohm@0
   101
  [ (rtac (major RS allE) 1),
clasohm@0
   102
    (REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ]);
clasohm@0
   103
clasohm@0
   104
(*Used in the datatype package*)
clasohm@0
   105
val rev_bspec = prove_goal ZF.thy
clasohm@0
   106
    "!!x A P. [| x: A;  ALL x:A. P(x) |] ==> P(x)"
clasohm@0
   107
 (fn _ =>
clasohm@0
   108
  [ REPEAT (ares_tac [bspec] 1) ]);
clasohm@0
   109
clasohm@0
   110
(*Instantiates x first: better for automatic theorem proving?*)
clasohm@0
   111
val rev_ballE = prove_goal ZF.thy
clasohm@0
   112
    "[| ALL x:A. P(x);  ~ x:A ==> Q;  P(x) ==> Q |] ==> Q"
clasohm@0
   113
 (fn major::prems=>
clasohm@0
   114
  [ (rtac (major RS ballE) 1),
clasohm@0
   115
    (REPEAT (eresolve_tac prems 1)) ]);
clasohm@0
   116
clasohm@0
   117
(*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*)
clasohm@0
   118
val ball_tac = dtac bspec THEN' assume_tac;
clasohm@0
   119
clasohm@0
   120
(*Trival rewrite rule;   (ALL x:A.P)<->P holds only if A is nonempty!*)
clasohm@0
   121
val ball_rew = prove_goal ZF.thy "(ALL x:A. True) <-> True"
clasohm@0
   122
 (fn prems=> [ (REPEAT (ares_tac [TrueI,ballI,iffI] 1)) ]);
clasohm@0
   123
clasohm@0
   124
(*Congruence rule for rewriting*)
clasohm@0
   125
val ball_cong = prove_goalw ZF.thy [Ball_def]
clasohm@0
   126
    "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) \
clasohm@0
   127
\    |] ==> (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))"
clasohm@0
   128
 (fn prems=> [ (prove_cong_tac prems 1) ]);
clasohm@0
   129
clasohm@0
   130
(*** Bounded existential quantifier ***)
clasohm@0
   131
clasohm@0
   132
val bexI = prove_goalw ZF.thy [Bex_def]
clasohm@0
   133
    "[| P(x);  x: A |] ==> EX x:A. P(x)"
clasohm@0
   134
 (fn prems=> [ (REPEAT (ares_tac (prems @ [exI,conjI]) 1)) ]);
clasohm@0
   135
clasohm@0
   136
(*Not of the general form for such rules; ~EX has become ALL~ *)
clasohm@0
   137
val bexCI = prove_goal ZF.thy 
clasohm@0
   138
   "[| ALL x:A. ~P(x) ==> P(a);  a: A |] ==> EX x:A.P(x)"
clasohm@0
   139
 (fn prems=>
clasohm@0
   140
  [ (rtac classical 1),
clasohm@0
   141
    (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]);
clasohm@0
   142
clasohm@0
   143
val bexE = prove_goalw ZF.thy [Bex_def]
clasohm@0
   144
    "[| EX x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q \
clasohm@0
   145
\    |] ==> Q"
clasohm@0
   146
 (fn major::prems=>
clasohm@0
   147
  [ (rtac (major RS exE) 1),
clasohm@0
   148
    (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ]);
clasohm@0
   149
clasohm@0
   150
(*We do not even have (EX x:A. True) <-> True unless A is nonempty!!*)
clasohm@0
   151
clasohm@0
   152
val bex_cong = prove_goalw ZF.thy [Bex_def]
clasohm@0
   153
    "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) \
clasohm@0
   154
\    |] ==> (EX x:A. P(x)) <-> (EX x:A'. P'(x))"
clasohm@0
   155
 (fn prems=> [ (prove_cong_tac prems 1) ]);
clasohm@0
   156
clasohm@0
   157
(*** Rules for subsets ***)
clasohm@0
   158
clasohm@0
   159
val subsetI = prove_goalw ZF.thy [subset_def]
clasohm@0
   160
    "(!!x.x:A ==> x:B) ==> A <= B"
clasohm@0
   161
 (fn prems=> [ (REPEAT (ares_tac (prems @ [ballI]) 1)) ]);
clasohm@0
   162
clasohm@0
   163
(*Rule in Modus Ponens style [was called subsetE] *)
clasohm@0
   164
val subsetD = prove_goalw ZF.thy [subset_def] "[| A <= B;  c:A |] ==> c:B"
clasohm@0
   165
 (fn major::prems=>
clasohm@0
   166
  [ (rtac (major RS bspec) 1),
clasohm@0
   167
    (resolve_tac prems 1) ]);
clasohm@0
   168
clasohm@0
   169
(*Classical elimination rule*)
clasohm@0
   170
val subsetCE = prove_goalw ZF.thy [subset_def]
clasohm@0
   171
    "[| A <= B;  ~(c:A) ==> P;  c:B ==> P |] ==> P"
clasohm@0
   172
 (fn major::prems=>
clasohm@0
   173
  [ (rtac (major RS ballE) 1),
clasohm@0
   174
    (REPEAT (eresolve_tac prems 1)) ]);
clasohm@0
   175
clasohm@0
   176
(*Takes assumptions A<=B; c:A and creates the assumption c:B *)
clasohm@0
   177
val set_mp_tac = dtac subsetD THEN' assume_tac;
clasohm@0
   178
clasohm@0
   179
(*Sometimes useful with premises in this order*)
clasohm@0
   180
val rev_subsetD = prove_goal ZF.thy "!!A B c. [| c:A; A<=B |] ==> c:B"
clasohm@0
   181
 (fn _=> [REPEAT (ares_tac [subsetD] 1)]);
clasohm@0
   182
clasohm@0
   183
val subset_refl = prove_goal ZF.thy "A <= A"
clasohm@0
   184
 (fn _=> [ (rtac subsetI 1), atac 1 ]);
clasohm@0
   185
clasohm@0
   186
val subset_trans = prove_goal ZF.thy "[| A<=B;  B<=C |] ==> A<=C"
clasohm@0
   187
 (fn prems=> [ (REPEAT (ares_tac ([subsetI]@(prems RL [subsetD])) 1)) ]);
clasohm@0
   188
clasohm@0
   189
clasohm@0
   190
(*** Rules for equality ***)
clasohm@0
   191
clasohm@0
   192
(*Anti-symmetry of the subset relation*)
clasohm@0
   193
val equalityI = prove_goal ZF.thy "[| A <= B;  B <= A |] ==> A = B"
clasohm@0
   194
 (fn prems=> [ (REPEAT (resolve_tac (prems@[conjI, extension RS iffD2]) 1)) ]);
clasohm@0
   195
clasohm@0
   196
val equality_iffI = prove_goal ZF.thy "(!!x. x:A <-> x:B) ==> A = B"
clasohm@0
   197
 (fn [prem] =>
clasohm@0
   198
  [ (rtac equalityI 1),
clasohm@0
   199
    (REPEAT (ares_tac [subsetI, prem RS iffD1, prem RS iffD2] 1)) ]);
clasohm@0
   200
clasohm@0
   201
val equalityD1 = prove_goal ZF.thy "A = B ==> A<=B"
clasohm@0
   202
 (fn prems=>
clasohm@0
   203
  [ (rtac (extension RS iffD1 RS conjunct1) 1),
clasohm@0
   204
    (resolve_tac prems 1) ]);
clasohm@0
   205
clasohm@0
   206
val equalityD2 = prove_goal ZF.thy "A = B ==> B<=A"
clasohm@0
   207
 (fn prems=>
clasohm@0
   208
  [ (rtac (extension RS iffD1 RS conjunct2) 1),
clasohm@0
   209
    (resolve_tac prems 1) ]);
clasohm@0
   210
clasohm@0
   211
val equalityE = prove_goal ZF.thy
clasohm@0
   212
    "[| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P"
clasohm@0
   213
 (fn prems=>
clasohm@0
   214
  [ (DEPTH_SOLVE (resolve_tac (prems@[equalityD1,equalityD2]) 1)) ]);
clasohm@0
   215
clasohm@0
   216
val equalityCE = prove_goal ZF.thy
clasohm@0
   217
    "[| A = B;  [| c:A; c:B |] ==> P;  [| ~ c:A; ~ c:B |] ==> P |]  ==>  P"
clasohm@0
   218
 (fn major::prems=>
clasohm@0
   219
  [ (rtac (major RS equalityE) 1),
clasohm@0
   220
    (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)) ]);
clasohm@0
   221
clasohm@0
   222
(*Lemma for creating induction formulae -- for "pattern matching" on p
clasohm@0
   223
  To make the induction hypotheses usable, apply "spec" or "bspec" to
clasohm@0
   224
  put universal quantifiers over the free variables in p. 
clasohm@0
   225
  Would it be better to do subgoal_tac "ALL z. p = f(z) --> R(z)" ??*)
clasohm@0
   226
val setup_induction = prove_goal ZF.thy
clasohm@0
   227
    "[| p: A;  !!z. z: A ==> p=z --> R |] ==> R"
clasohm@0
   228
 (fn prems=>
clasohm@0
   229
  [ (rtac mp 1),
clasohm@0
   230
    (REPEAT (resolve_tac (refl::prems) 1)) ]);
clasohm@0
   231
clasohm@0
   232
clasohm@0
   233
(*** Rules for Replace -- the derived form of replacement ***)
clasohm@0
   234
clasohm@0
   235
val ex1_functional = prove_goal ZF.thy
clasohm@0
   236
    "[| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
clasohm@0
   237
 (fn prems=>
clasohm@0
   238
  [ (cut_facts_tac prems 1),
clasohm@0
   239
    (best_tac FOL_dup_cs 1) ]);
clasohm@0
   240
clasohm@0
   241
val Replace_iff = prove_goalw ZF.thy [Replace_def]
clasohm@0
   242
    "b : {y. x:A, P(x,y)}  <->  (EX x:A. P(x,b) & (ALL y. P(x,y) --> y=b))"
clasohm@0
   243
 (fn _=>
clasohm@0
   244
  [ (rtac (replacement RS iff_trans) 1),
clasohm@0
   245
    (REPEAT (ares_tac [refl,bex_cong,iffI,ballI,allI,conjI,impI,ex1I] 1
clasohm@0
   246
        ORELSE eresolve_tac [conjE, spec RS mp, ex1_functional] 1)) ]);
clasohm@0
   247
clasohm@0
   248
(*Introduction; there must be a unique y such that P(x,y), namely y=b. *)
clasohm@0
   249
val ReplaceI = prove_goal ZF.thy
clasohm@0
   250
    "[| x: A;  P(x,b);  !!y. P(x,y) ==> y=b |] ==> \
clasohm@0
   251
\    b : {y. x:A, P(x,y)}"
clasohm@0
   252
 (fn prems=>
clasohm@0
   253
  [ (rtac (Replace_iff RS iffD2) 1),
clasohm@0
   254
    (REPEAT (ares_tac (prems@[bexI,conjI,allI,impI]) 1)) ]);
clasohm@0
   255
clasohm@0
   256
(*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *)
clasohm@0
   257
val ReplaceE = prove_goal ZF.thy 
clasohm@0
   258
    "[| b : {y. x:A, P(x,y)};  \
clasohm@0
   259
\       !!x. [| x: A;  P(x,b);  ALL y. P(x,y)-->y=b |] ==> R \
clasohm@0
   260
\    |] ==> R"
clasohm@0
   261
 (fn prems=>
clasohm@0
   262
  [ (rtac (Replace_iff RS iffD1 RS bexE) 1),
clasohm@0
   263
    (etac conjE 2),
clasohm@0
   264
    (REPEAT (ares_tac prems 1)) ]);
clasohm@0
   265
clasohm@0
   266
val Replace_cong = prove_goal ZF.thy
clasohm@0
   267
    "[| A=B;  !!x y. x:B ==> P(x,y) <-> Q(x,y) |] ==> \
clasohm@0
   268
\    {y. x:A, P(x,y)} = {y. x:B, Q(x,y)}"
clasohm@0
   269
 (fn prems=>
clasohm@0
   270
   let val substprems = prems RL [subst, ssubst]
clasohm@0
   271
       and iffprems = prems RL [iffD1,iffD2]
clasohm@0
   272
   in [ (rtac equalityI 1),
clasohm@0
   273
	(REPEAT (eresolve_tac (substprems@[asm_rl, ReplaceE, spec RS mp]) 1
clasohm@0
   274
	 ORELSE resolve_tac [subsetI, ReplaceI] 1
clasohm@0
   275
	 ORELSE (resolve_tac iffprems 1 THEN assume_tac 2))) ]
clasohm@0
   276
   end);
clasohm@0
   277
clasohm@0
   278
clasohm@0
   279
(*** Rules for RepFun ***)
clasohm@0
   280
clasohm@0
   281
val RepFunI = prove_goalw ZF.thy [RepFun_def]
clasohm@0
   282
    "!!a A. a : A ==> f(a) : {f(x). x:A}"
clasohm@0
   283
 (fn _ => [ (REPEAT (ares_tac [ReplaceI,refl] 1)) ]);
clasohm@0
   284
clasohm@0
   285
(*Useful for co-induction proofs*)
clasohm@0
   286
val RepFun_eqI = prove_goal ZF.thy
clasohm@0
   287
    "!!b a f. [| b=f(a);  a : A |] ==> b : {f(x). x:A}"
clasohm@0
   288
 (fn _ => [ etac ssubst 1, etac RepFunI 1 ]);
clasohm@0
   289
clasohm@0
   290
val RepFunE = prove_goalw ZF.thy [RepFun_def]
clasohm@0
   291
    "[| b : {f(x). x:A};  \
clasohm@0
   292
\       !!x.[| x:A;  b=f(x) |] ==> P |] ==> \
clasohm@0
   293
\    P"
clasohm@0
   294
 (fn major::prems=>
clasohm@0
   295
  [ (rtac (major RS ReplaceE) 1),
clasohm@0
   296
    (REPEAT (ares_tac prems 1)) ]);
clasohm@0
   297
clasohm@0
   298
val RepFun_cong = prove_goalw ZF.thy [RepFun_def]
clasohm@0
   299
    "[| A=B;  !!x. x:B ==> f(x)=g(x) |] ==> \
clasohm@0
   300
\    {f(x). x:A} = {g(x). x:B}"
clasohm@0
   301
 (fn prems=> [ (prove_cong_tac (prems@[Replace_cong]) 1) ]);
clasohm@0
   302
clasohm@0
   303
clasohm@0
   304
(*** Rules for Collect -- forming a subset by separation ***)
clasohm@0
   305
clasohm@0
   306
(*Separation is derivable from Replacement*)
clasohm@0
   307
val separation = prove_goalw ZF.thy [Collect_def]
clasohm@0
   308
    "a : {x:A. P(x)} <-> a:A & P(a)"
clasohm@0
   309
 (fn _=> [ (fast_tac (FOL_cs addIs  [bexI,ReplaceI] 
clasohm@0
   310
		             addSEs [bexE,ReplaceE]) 1) ]);
clasohm@0
   311
clasohm@0
   312
val CollectI = prove_goal ZF.thy
clasohm@0
   313
    "[| a:A;  P(a) |] ==> a : {x:A. P(x)}"
clasohm@0
   314
 (fn prems=>
clasohm@0
   315
  [ (rtac (separation RS iffD2) 1),
clasohm@0
   316
    (REPEAT (resolve_tac (prems@[conjI]) 1)) ]);
clasohm@0
   317
clasohm@0
   318
val CollectE = prove_goal ZF.thy
clasohm@0
   319
    "[| a : {x:A. P(x)};  [| a:A; P(a) |] ==> R |] ==> R"
clasohm@0
   320
 (fn prems=>
clasohm@0
   321
  [ (rtac (separation RS iffD1 RS conjE) 1),
clasohm@0
   322
    (REPEAT (ares_tac prems 1)) ]);
clasohm@0
   323
clasohm@0
   324
val CollectD1 = prove_goal ZF.thy "a : {x:A. P(x)} ==> a:A"
clasohm@0
   325
 (fn [major]=>
clasohm@0
   326
  [ (rtac (major RS CollectE) 1),
clasohm@0
   327
    (assume_tac 1) ]);
clasohm@0
   328
clasohm@0
   329
val CollectD2 = prove_goal ZF.thy "a : {x:A. P(x)} ==> P(a)"
clasohm@0
   330
 (fn [major]=>
clasohm@0
   331
  [ (rtac (major RS CollectE) 1),
clasohm@0
   332
    (assume_tac 1) ]);
clasohm@0
   333
clasohm@0
   334
val Collect_cong = prove_goalw ZF.thy [Collect_def] 
clasohm@0
   335
    "[| A=B;  !!x. x:B ==> P(x) <-> Q(x) |] ==> \
clasohm@0
   336
\    {x:A. P(x)} = {x:B. Q(x)}"
clasohm@0
   337
 (fn prems=> [ (prove_cong_tac (prems@[Replace_cong]) 1) ]);
clasohm@0
   338
clasohm@0
   339
(*** Rules for Unions ***)
clasohm@0
   340
clasohm@0
   341
(*The order of the premises presupposes that C is rigid; A may be flexible*)
clasohm@0
   342
val UnionI = prove_goal ZF.thy "[| B: C;  A: B |] ==> A: Union(C)"
clasohm@0
   343
 (fn prems=>
clasohm@0
   344
  [ (resolve_tac [union_iff RS iffD2] 1),
clasohm@0
   345
    (REPEAT (resolve_tac (prems @ [bexI]) 1)) ]);
clasohm@0
   346
clasohm@0
   347
val UnionE = prove_goal ZF.thy
clasohm@0
   348
    "[| A : Union(C);  !!B.[| A: B;  B: C |] ==> R |] ==> R"
clasohm@0
   349
 (fn prems=>
clasohm@0
   350
  [ (resolve_tac [union_iff RS iffD1 RS bexE] 1),
clasohm@0
   351
    (REPEAT (ares_tac prems 1)) ]);
clasohm@0
   352
clasohm@0
   353
(*** Rules for Inter ***)
clasohm@0
   354
clasohm@0
   355
(*Not obviously useful towards proving InterI, InterD, InterE*)
clasohm@0
   356
val Inter_iff = prove_goalw ZF.thy [Inter_def,Ball_def]
clasohm@0
   357
    "A : Inter(C) <-> (ALL x:C. A: x) & (EX x. x:C)"
clasohm@0
   358
 (fn _=> [ (rtac (separation RS iff_trans) 1),
clasohm@0
   359
	   (fast_tac (FOL_cs addIs [UnionI] addSEs [UnionE]) 1) ]);
clasohm@0
   360
clasohm@0
   361
(* Intersection is well-behaved only if the family is non-empty! *)
clasohm@0
   362
val InterI = prove_goalw ZF.thy [Inter_def]
clasohm@0
   363
    "[| !!x. x: C ==> A: x;  c:C |] ==> A : Inter(C)"
clasohm@0
   364
 (fn prems=>
clasohm@0
   365
  [ (DEPTH_SOLVE (ares_tac ([CollectI,UnionI,ballI] @ prems) 1)) ]);
clasohm@0
   366
clasohm@0
   367
(*A "destruct" rule -- every B in C contains A as an element, but
clasohm@0
   368
  A:B can hold when B:C does not!  This rule is analogous to "spec". *)
clasohm@0
   369
val InterD = prove_goalw ZF.thy [Inter_def]
clasohm@0
   370
    "[| A : Inter(C);  B : C |] ==> A : B"
clasohm@0
   371
 (fn [major,minor]=>
clasohm@0
   372
  [ (rtac (major RS CollectD2 RS bspec) 1),
clasohm@0
   373
    (rtac minor 1) ]);
clasohm@0
   374
clasohm@0
   375
(*"Classical" elimination rule -- does not require exhibiting B:C *)
clasohm@0
   376
val InterE = prove_goalw ZF.thy [Inter_def]
clasohm@0
   377
    "[| A : Inter(C);  A:B ==> R;  ~ B:C ==> R |] ==> R"
clasohm@0
   378
 (fn major::prems=>
clasohm@0
   379
  [ (rtac (major RS CollectD2 RS ballE) 1),
clasohm@0
   380
    (REPEAT (eresolve_tac prems 1)) ]);
clasohm@0
   381
clasohm@0
   382
(*** Rules for Unions of families ***)
clasohm@0
   383
(* UN x:A. B(x) abbreviates Union({B(x). x:A}) *)
clasohm@0
   384
clasohm@0
   385
(*The order of the premises presupposes that A is rigid; b may be flexible*)
clasohm@0
   386
val UN_I = prove_goal ZF.thy "[| a: A;  b: B(a) |] ==> b: (UN x:A. B(x))"
clasohm@0
   387
 (fn prems=>
clasohm@0
   388
  [ (REPEAT (resolve_tac (prems@[UnionI,RepFunI]) 1)) ]);
clasohm@0
   389
clasohm@0
   390
val UN_E = prove_goal ZF.thy
clasohm@0
   391
    "[| b : (UN x:A. B(x));  !!x.[| x: A;  b: B(x) |] ==> R |] ==> R"
clasohm@0
   392
 (fn major::prems=>
clasohm@0
   393
  [ (rtac (major RS UnionE) 1),
clasohm@0
   394
    (REPEAT (eresolve_tac (prems@[asm_rl, RepFunE, subst]) 1)) ]);
clasohm@0
   395
clasohm@0
   396
clasohm@0
   397
(*** Rules for Intersections of families ***)
clasohm@0
   398
(* INT x:A. B(x) abbreviates Inter({B(x). x:A}) *)
clasohm@0
   399
clasohm@0
   400
val INT_I = prove_goal ZF.thy
clasohm@0
   401
    "[| !!x. x: A ==> b: B(x);  a: A |] ==> b: (INT x:A. B(x))"
clasohm@0
   402
 (fn prems=>
clasohm@0
   403
  [ (REPEAT (ares_tac (prems@[InterI,RepFunI]) 1
clasohm@0
   404
     ORELSE eresolve_tac [RepFunE,ssubst] 1)) ]);
clasohm@0
   405
clasohm@0
   406
val INT_E = prove_goal ZF.thy
clasohm@0
   407
    "[| b : (INT x:A. B(x));  a: A |] ==> b : B(a)"
clasohm@0
   408
 (fn [major,minor]=>
clasohm@0
   409
  [ (rtac (major RS InterD) 1),
clasohm@0
   410
    (rtac (minor RS RepFunI) 1) ]);
clasohm@0
   411
clasohm@0
   412
clasohm@0
   413
(*** Rules for Powersets ***)
clasohm@0
   414
clasohm@0
   415
val PowI = prove_goal ZF.thy "A <= B ==> A : Pow(B)"
clasohm@0
   416
 (fn [prem]=> [ (rtac (prem RS (power_set RS iffD2)) 1) ]);
clasohm@0
   417
clasohm@0
   418
val PowD = prove_goal ZF.thy "A : Pow(B)  ==>  A<=B"
clasohm@0
   419
 (fn [major]=> [ (rtac (major RS (power_set RS iffD1)) 1) ]);
clasohm@0
   420
clasohm@0
   421
clasohm@0
   422
(*** Rules for the empty set ***)
clasohm@0
   423
clasohm@0
   424
(*The set {x:0.False} is empty; by foundation it equals 0 
clasohm@0
   425
  See Suppes, page 21.*)
clasohm@0
   426
val emptyE = prove_goal ZF.thy "a:0 ==> P"
clasohm@0
   427
 (fn [major]=>
clasohm@0
   428
  [ (rtac (foundation RS disjE) 1),
clasohm@0
   429
    (etac (equalityD2 RS subsetD RS CollectD2 RS FalseE) 1),
clasohm@0
   430
    (rtac major 1),
clasohm@0
   431
    (etac bexE 1),
clasohm@0
   432
    (etac (CollectD2 RS FalseE) 1) ]);
clasohm@0
   433
clasohm@0
   434
val empty_subsetI = prove_goal ZF.thy "0 <= A"
clasohm@0
   435
 (fn _ => [ (REPEAT (ares_tac [equalityI,subsetI,emptyE] 1)) ]);
clasohm@0
   436
clasohm@0
   437
val equals0I = prove_goal ZF.thy "[| !!y. y:A ==> False |] ==> A=0"
clasohm@0
   438
 (fn prems=>
clasohm@0
   439
  [ (REPEAT (ares_tac (prems@[empty_subsetI,subsetI,equalityI]) 1 
clasohm@0
   440
      ORELSE eresolve_tac (prems RL [FalseE]) 1)) ]);
clasohm@0
   441
clasohm@0
   442
val equals0D = prove_goal ZF.thy "[| A=0;  a:A |] ==> P"
clasohm@0
   443
 (fn [major,minor]=>
clasohm@0
   444
  [ (rtac (minor RS (major RS equalityD1 RS subsetD RS emptyE)) 1) ]);
clasohm@0
   445
clasohm@0
   446
val lemmas_cs = FOL_cs
clasohm@0
   447
  addSIs [ballI, InterI, CollectI, PowI, subsetI]
clasohm@0
   448
  addIs [bexI, UnionI, ReplaceI, RepFunI]
clasohm@0
   449
  addSEs [bexE, make_elim PowD, UnionE, ReplaceE, RepFunE,
clasohm@0
   450
	  CollectE, emptyE]
clasohm@0
   451
  addEs [rev_ballE, InterD, make_elim InterD, subsetD, subsetCE];
clasohm@0
   452
clasohm@0
   453
end;
clasohm@0
   454
clasohm@0
   455
open ZF_Lemmas;