src/ZF/ZF.ML
changeset 664 ba39b4984f5a
parent 516 1957113f0d7d
child 688 4dddc8d0c384
equal deleted inserted replaced
663:dc3f0582e839 664:ba39b4984f5a
    33   val equalityE		: thm
    33   val equalityE		: thm
    34   val equalityI		: thm
    34   val equalityI		: thm
    35   val equality_iffI	: thm
    35   val equality_iffI	: thm
    36   val equals0D		: thm
    36   val equals0D		: thm
    37   val equals0I		: thm
    37   val equals0I		: thm
    38   val ex1_functional	: thm
       
    39   val InterD		: thm
    38   val InterD		: thm
    40   val InterE		: thm
    39   val InterE		: thm
    41   val InterI		: thm
    40   val InterI		: thm
    42   val Inter_iff 	: thm
    41   val Inter_iff 	: thm
    43   val INT_E		: thm
    42   val INT_E		: thm
   231     (REPEAT (resolve_tac (refl::prems) 1)) ]);
   230     (REPEAT (resolve_tac (refl::prems) 1)) ]);
   232 
   231 
   233 
   232 
   234 (*** Rules for Replace -- the derived form of replacement ***)
   233 (*** Rules for Replace -- the derived form of replacement ***)
   235 
   234 
   236 val ex1_functional = prove_goal ZF.thy
       
   237     "[| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
       
   238  (fn prems=>
       
   239   [ (cut_facts_tac prems 1),
       
   240     (best_tac FOL_dup_cs 1) ]);
       
   241 
       
   242 val Replace_iff = prove_goalw ZF.thy [Replace_def]
   235 val Replace_iff = prove_goalw ZF.thy [Replace_def]
   243     "b : {y. x:A, P(x,y)}  <->  (EX x:A. P(x,b) & (ALL y. P(x,y) --> y=b))"
   236     "b : {y. x:A, P(x,y)}  <->  (EX x:A. P(x,b) & (ALL y. P(x,y) --> y=b))"
   244  (fn _=>
   237  (fn _=>
   245   [ (rtac (replacement RS iff_trans) 1),
   238   [ (rtac (replacement RS iff_trans) 1),
   246     (REPEAT (ares_tac [refl,bex_cong,iffI,ballI,allI,conjI,impI,ex1I] 1
   239     (REPEAT (ares_tac [refl,bex_cong,iffI,ballI,allI,conjI,impI,ex1I] 1