src/ZF/ZF.ML
changeset 9211 6236c5285bd8
parent 9180 3bda56c0d70d
child 9907 473a6604da94
     1.1 --- a/src/ZF/ZF.ML	Fri Jun 30 12:49:11 2000 +0200
     1.2 +++ b/src/ZF/ZF.ML	Fri Jun 30 12:51:30 2000 +0200
     1.3 @@ -15,21 +15,21 @@
     1.4  
     1.5  (*** Bounded universal quantifier ***)
     1.6  
     1.7 -qed_goalw "ballI" ZF.thy [Ball_def]
     1.8 -    "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)"
     1.9 - (fn prems=> [ (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ]);
    1.10 +val prems= Goalw [Ball_def] 
    1.11 +    "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)";
    1.12 +by (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ;
    1.13 +qed "ballI";
    1.14  
    1.15 -qed_goalw "bspec" ZF.thy [Ball_def]
    1.16 -    "[| ALL x:A. P(x);  x: A |] ==> P(x)"
    1.17 - (fn major::prems=>
    1.18 -  [ (rtac (major RS spec RS mp) 1),
    1.19 -    (resolve_tac prems 1) ]);
    1.20 +Goalw [Ball_def] "[| ALL x:A. P(x);  x: A |] ==> P(x)";
    1.21 +by (etac (spec RS mp) 1);
    1.22 +by (assume_tac 1) ;
    1.23 +qed "bspec";
    1.24  
    1.25 -qed_goalw "ballE" ZF.thy [Ball_def]
    1.26 -    "[| ALL x:A. P(x);  P(x) ==> Q;  x~:A ==> Q |] ==> Q"
    1.27 - (fn major::prems=>
    1.28 -  [ (rtac (major RS allE) 1),
    1.29 -    (REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ]);
    1.30 +val major::prems= Goalw [Ball_def] 
    1.31 +    "[| ALL x:A. P(x);  P(x) ==> Q;  x~:A ==> Q |] ==> Q";
    1.32 +by (rtac (major RS allE) 1);
    1.33 +by (REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ;
    1.34 +qed "ballE";
    1.35  
    1.36  (*Used in the datatype package*)
    1.37  Goal "[| x: A;  ALL x:A. P(x) |] ==> P(x)";
    1.38 @@ -57,9 +57,10 @@
    1.39  Addsimps [ball_triv];
    1.40  
    1.41  (*Congruence rule for rewriting*)
    1.42 -qed_goalw "ball_cong" ZF.thy [Ball_def]
    1.43 -    "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==> Ball(A,P) <-> Ball(A',P')"
    1.44 - (fn prems=> [ (simp_tac (FOL_ss addsimps prems) 1) ]);
    1.45 +val prems= Goalw [Ball_def] 
    1.46 +    "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==> Ball(A,P) <-> Ball(A',P')";
    1.47 +by (simp_tac (FOL_ss addsimps prems) 1) ;
    1.48 +qed "ball_cong";
    1.49  
    1.50  (*** Bounded existential quantifier ***)
    1.51  
    1.52 @@ -78,12 +79,12 @@
    1.53  by (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ;
    1.54  qed "bexCI";
    1.55  
    1.56 -qed_goalw "bexE" ZF.thy [Bex_def]
    1.57 +val major::prems= Goalw [Bex_def] 
    1.58      "[| EX x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q \
    1.59 -\    |] ==> Q"
    1.60 - (fn major::prems=>
    1.61 -  [ (rtac (major RS exE) 1),
    1.62 -    (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ]);
    1.63 +\    |] ==> Q";
    1.64 +by (rtac (major RS exE) 1);
    1.65 +by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ;
    1.66 +qed "bexE";
    1.67  
    1.68  AddIs  [bexI];  
    1.69  AddSEs [bexE];
    1.70 @@ -94,32 +95,34 @@
    1.71  qed "bex_triv";
    1.72  Addsimps [bex_triv];
    1.73  
    1.74 -qed_goalw "bex_cong" ZF.thy [Bex_def]
    1.75 +val prems= Goalw [Bex_def] 
    1.76      "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) \
    1.77 -\    |] ==> Bex(A,P) <-> Bex(A',P')"
    1.78 - (fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1) ]);
    1.79 +\    |] ==> Bex(A,P) <-> Bex(A',P')";
    1.80 +by (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1) ;
    1.81 +qed "bex_cong";
    1.82  
    1.83  Addcongs [ball_cong, bex_cong];
    1.84  
    1.85  
    1.86  (*** Rules for subsets ***)
    1.87  
    1.88 -qed_goalw "subsetI" ZF.thy [subset_def]
    1.89 -    "(!!x. x:A ==> x:B) ==> A <= B"
    1.90 - (fn prems=> [ (REPEAT (ares_tac (prems @ [ballI]) 1)) ]);
    1.91 +val prems= Goalw [subset_def] 
    1.92 +    "(!!x. x:A ==> x:B) ==> A <= B";
    1.93 +by (REPEAT (ares_tac (prems @ [ballI]) 1)) ;
    1.94 +qed "subsetI";
    1.95  
    1.96  (*Rule in Modus Ponens style [was called subsetE] *)
    1.97 -qed_goalw "subsetD" ZF.thy [subset_def] "[| A <= B;  c:A |] ==> c:B"
    1.98 - (fn major::prems=>
    1.99 -  [ (rtac (major RS bspec) 1),
   1.100 -    (resolve_tac prems 1) ]);
   1.101 +Goalw [subset_def]  "[| A <= B;  c:A |] ==> c:B";
   1.102 +by (etac bspec 1);
   1.103 +by (assume_tac 1) ;
   1.104 +qed "subsetD";
   1.105  
   1.106  (*Classical elimination rule*)
   1.107 -qed_goalw "subsetCE" ZF.thy [subset_def]
   1.108 -    "[| A <= B;  c~:A ==> P;  c:B ==> P |] ==> P"
   1.109 - (fn major::prems=>
   1.110 -  [ (rtac (major RS ballE) 1),
   1.111 -    (REPEAT (eresolve_tac prems 1)) ]);
   1.112 +val major::prems= Goalw [subset_def] 
   1.113 +    "[| A <= B;  c~:A ==> P;  c:B ==> P |] ==> P";
   1.114 +by (rtac (major RS ballE) 1);
   1.115 +by (REPEAT (eresolve_tac prems 1)) ;
   1.116 +qed "subsetCE";
   1.117  
   1.118  AddSIs [subsetI];
   1.119  AddEs  [subsetCE, subsetD];
   1.120 @@ -155,9 +158,10 @@
   1.121  qed "subset_trans";
   1.122  
   1.123  (*Useful for proving A<=B by rewriting in some cases*)
   1.124 -qed_goalw "subset_iff" ZF.thy [subset_def,Ball_def]
   1.125 -     "A<=B <-> (ALL x. x:A --> x:B)"
   1.126 - (fn _=> [ (rtac iff_refl 1) ]);
   1.127 +Goalw [subset_def,Ball_def] 
   1.128 +     "A<=B <-> (ALL x. x:A --> x:B)";
   1.129 +by (rtac iff_refl 1) ;
   1.130 +qed "subset_iff";
   1.131  
   1.132  
   1.133  (*** Rules for equality ***)
   1.134 @@ -199,12 +203,12 @@
   1.135  
   1.136  (*** Rules for Replace -- the derived form of replacement ***)
   1.137  
   1.138 -qed_goalw "Replace_iff" ZF.thy [Replace_def]
   1.139 -    "b : {y. x:A, P(x,y)}  <->  (EX x:A. P(x,b) & (ALL y. P(x,y) --> y=b))"
   1.140 - (fn _=>
   1.141 -  [ (rtac (replacement RS iff_trans) 1),
   1.142 -    (REPEAT (ares_tac [refl,bex_cong,iffI,ballI,allI,conjI,impI,ex1I] 1
   1.143 -        ORELSE eresolve_tac [conjE, spec RS mp, ex1_functional] 1)) ]);
   1.144 +Goalw [Replace_def] 
   1.145 +    "b : {y. x:A, P(x,y)}  <->  (EX x:A. P(x,b) & (ALL y. P(x,y) --> y=b))";
   1.146 +by (rtac (replacement RS iff_trans) 1);
   1.147 +by (REPEAT (ares_tac [refl,bex_cong,iffI,ballI,allI,conjI,impI,ex1I] 1 
   1.148 +     ORELSE eresolve_tac [conjE, spec RS mp, ex1_functional] 1)) ;
   1.149 +qed "Replace_iff";
   1.150  
   1.151  (*Introduction; there must be a unique y such that P(x,y), namely y=b. *)
   1.152  val prems = Goal
   1.153 @@ -249,9 +253,9 @@
   1.154  
   1.155  (*** Rules for RepFun ***)
   1.156  
   1.157 -qed_goalw "RepFunI" ZF.thy [RepFun_def]
   1.158 -    "!!a A. a : A ==> f(a) : {f(x). x:A}"
   1.159 - (fn _ => [ (REPEAT (ares_tac [ReplaceI,refl] 1)) ]);
   1.160 +Goalw [RepFun_def] "a : A ==> f(a) : {f(x). x:A}";
   1.161 +by (REPEAT (ares_tac [ReplaceI,refl] 1)) ;
   1.162 +qed "RepFunI";
   1.163  
   1.164  (*Useful for coinduction proofs*)
   1.165  Goal "[| b=f(a);  a : A |] ==> b : {f(x). x:A}";
   1.166 @@ -259,26 +263,27 @@
   1.167  by (etac RepFunI 1) ;
   1.168  qed "RepFun_eqI";
   1.169  
   1.170 -qed_goalw "RepFunE" ZF.thy [RepFun_def]
   1.171 +val major::prems= Goalw [RepFun_def] 
   1.172      "[| b : {f(x). x:A};  \
   1.173  \       !!x.[| x:A;  b=f(x) |] ==> P |] ==> \
   1.174 -\    P"
   1.175 - (fn major::prems=>
   1.176 -  [ (rtac (major RS ReplaceE) 1),
   1.177 -    (REPEAT (ares_tac prems 1)) ]);
   1.178 +\    P";
   1.179 +by (rtac (major RS ReplaceE) 1);
   1.180 +by (REPEAT (ares_tac prems 1)) ;
   1.181 +qed "RepFunE";
   1.182  
   1.183  AddIs  [RepFun_eqI];  
   1.184  AddSEs [RepFunE];
   1.185  
   1.186 -qed_goalw "RepFun_cong" ZF.thy [RepFun_def]
   1.187 -    "[| A=B;  !!x. x:B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)"
   1.188 - (fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]);
   1.189 +val prems= Goalw [RepFun_def] 
   1.190 +    "[| A=B;  !!x. x:B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)";
   1.191 +by (simp_tac (simpset() addsimps prems) 1) ;
   1.192 +qed "RepFun_cong";
   1.193  
   1.194  Addcongs [RepFun_cong];
   1.195  
   1.196 -qed_goalw "RepFun_iff" ZF.thy [Bex_def]
   1.197 -    "b : {f(x). x:A} <-> (EX x:A. b=f(x))"
   1.198 - (fn _ => [(Blast_tac 1)]);
   1.199 +Goalw [Bex_def] "b : {f(x). x:A} <-> (EX x:A. b=f(x))";
   1.200 +by (Blast_tac 1);
   1.201 +qed "RepFun_iff";
   1.202  
   1.203  Goal "{x. x:A} = A";
   1.204  by (Blast_tac 1);
   1.205 @@ -289,9 +294,9 @@
   1.206  (*** Rules for Collect -- forming a subset by separation ***)
   1.207  
   1.208  (*Separation is derivable from Replacement*)
   1.209 -qed_goalw "separation" ZF.thy [Collect_def]
   1.210 -    "a : {x:A. P(x)} <-> a:A & P(a)"
   1.211 - (fn _=> [(Blast_tac 1)]);
   1.212 +Goalw [Collect_def] "a : {x:A. P(x)} <-> a:A & P(a)";
   1.213 +by (Blast_tac 1);
   1.214 +qed "separation";
   1.215  
   1.216  Addsimps [separation];
   1.217  
   1.218 @@ -315,9 +320,10 @@
   1.219  by (assume_tac 1) ;
   1.220  qed "CollectD2";
   1.221  
   1.222 -qed_goalw "Collect_cong" ZF.thy [Collect_def] 
   1.223 -    "[| A=B;  !!x. x:B ==> P(x) <-> Q(x) |] ==> Collect(A,P) = Collect(B,Q)"
   1.224 - (fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]);
   1.225 +val prems= Goalw [Collect_def]  
   1.226 +    "[| A=B;  !!x. x:B ==> P(x) <-> Q(x) |] ==> Collect(A,P) = Collect(B,Q)";
   1.227 +by (simp_tac (simpset() addsimps prems) 1) ;
   1.228 +qed "Collect_cong";
   1.229  
   1.230  AddSIs [CollectI];
   1.231  AddSEs [CollectE];
   1.232 @@ -341,9 +347,10 @@
   1.233  (*** Rules for Unions of families ***)
   1.234  (* UN x:A. B(x) abbreviates Union({B(x). x:A}) *)
   1.235  
   1.236 -qed_goalw "UN_iff" ZF.thy [Bex_def]
   1.237 -    "b : (UN x:A. B(x)) <-> (EX x:A. b : B(x))"
   1.238 - (fn _=> [ Simp_tac 1, Blast_tac 1 ]);
   1.239 +Goalw [Bex_def] "b : (UN x:A. B(x)) <-> (EX x:A. b : B(x))";
   1.240 +by (Simp_tac 1);
   1.241 +by (Blast_tac 1) ;
   1.242 +qed "UN_iff";
   1.243  
   1.244  Addsimps [UN_iff];
   1.245  
   1.246 @@ -377,9 +384,11 @@
   1.247  (*** Rules for Inter ***)
   1.248  
   1.249  (*Not obviously useful towards proving InterI, InterD, InterE*)
   1.250 -qed_goalw "Inter_iff" ZF.thy [Inter_def,Ball_def]
   1.251 -    "A : Inter(C) <-> (ALL x:C. A: x) & (EX x. x:C)"
   1.252 - (fn _=> [ Simp_tac 1, Blast_tac 1 ]);
   1.253 +Goalw [Inter_def,Ball_def] 
   1.254 +    "A : Inter(C) <-> (ALL x:C. A: x) & (EX x. x:C)";
   1.255 +by (Simp_tac 1);
   1.256 +by (Blast_tac 1) ;
   1.257 +qed "Inter_iff";
   1.258  
   1.259  (* Intersection is well-behaved only if the family is non-empty! *)
   1.260  val prems = Goal
   1.261 @@ -390,16 +399,16 @@
   1.262  
   1.263  (*A "destruct" rule -- every B in C contains A as an element, but
   1.264    A:B can hold when B:C does not!  This rule is analogous to "spec". *)
   1.265 -qed_goalw "InterD" ZF.thy [Inter_def]
   1.266 -    "!!C. [| A : Inter(C);  B : C |] ==> A : B"
   1.267 - (fn _=> [(Blast_tac 1)]);
   1.268 +Goalw [Inter_def] "[| A : Inter(C);  B : C |] ==> A : B";
   1.269 +by (Blast_tac 1);
   1.270 +qed "InterD";
   1.271  
   1.272  (*"Classical" elimination rule -- does not require exhibiting B:C *)
   1.273 -qed_goalw "InterE" ZF.thy [Inter_def]
   1.274 -    "[| A : Inter(C);  B~:C ==> R;  A:B ==> R |] ==> R"
   1.275 - (fn major::prems=>
   1.276 -  [ (rtac (major RS CollectD2 RS ballE) 1),
   1.277 -    (REPEAT (eresolve_tac prems 1)) ]);
   1.278 +val major::prems= Goalw [Inter_def] 
   1.279 +    "[| A : Inter(C);  B~:C ==> R;  A:B ==> R |] ==> R";
   1.280 +by (rtac (major RS CollectD2 RS ballE) 1);
   1.281 +by (REPEAT (eresolve_tac prems 1)) ;
   1.282 +qed "InterE";
   1.283  
   1.284  AddSIs [InterI];
   1.285  AddEs  [InterD, InterE];
   1.286 @@ -407,9 +416,10 @@
   1.287  (*** Rules for Intersections of families ***)
   1.288  (* INT x:A. B(x) abbreviates Inter({B(x). x:A}) *)
   1.289  
   1.290 -qed_goalw "INT_iff" ZF.thy [Inter_def]
   1.291 -    "b : (INT x:A. B(x)) <-> (ALL x:A. b : B(x)) & (EX x. x:A)"
   1.292 - (fn _=> [ Simp_tac 1, Best_tac 1 ]);
   1.293 +Goalw [Inter_def] "b : (INT x:A. B(x)) <-> (ALL x:A. b : B(x)) & (EX x. x:A)";
   1.294 +by (Simp_tac 1);
   1.295 +by (Best_tac 1) ;
   1.296 +qed "INT_iff";
   1.297  
   1.298  val prems = Goal
   1.299      "[| !!x. x: A ==> b: B(x);  a: A |] ==> b: (INT x:A. B(x))";