src/ZF/OrdQuant.ML
changeset 9211 6236c5285bd8
parent 9180 3bda56c0d70d
child 9907 473a6604da94
     1.1 --- a/src/ZF/OrdQuant.ML	Fri Jun 30 12:49:11 2000 +0200
     1.2 +++ b/src/ZF/OrdQuant.ML	Fri Jun 30 12:51:30 2000 +0200
     1.3 @@ -7,23 +7,23 @@
     1.4  
     1.5  (*** universal quantifier for ordinals ***)
     1.6  
     1.7 -qed_goalw "oallI" thy [oall_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 [oall_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 "oallI";
    1.14  
    1.15 -qed_goalw "ospec" thy [oall_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 [oall_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 "ospec";
    1.24  
    1.25 -qed_goalw "oallE" thy [oall_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 [oall_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 "oallE";
    1.35  
    1.36 -val major::prems= goal thy
    1.37 +val major::prems = Goal
    1.38      "[| ALL x<A. P(x);  ~x<A ==> Q;  P(x) ==> Q |] ==> Q";
    1.39  by (rtac (major RS oallE) 1);
    1.40  by (REPEAT (eresolve_tac prems 1)) ;
    1.41 @@ -35,16 +35,18 @@
    1.42  qed "oall_simp";
    1.43  
    1.44  (*Congruence rule for rewriting*)
    1.45 -qed_goalw "oall_cong" thy [oall_def]
    1.46 -    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |] ==> oall(a,P) <-> oall(a',P')"
    1.47 - (fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]);
    1.48 +val prems = Goalw [oall_def] 
    1.49 +    "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) |] ==> oall(a,P) <-> oall(a',P')";
    1.50 +by (simp_tac (simpset() addsimps prems) 1) ;
    1.51 +qed "oall_cong";
    1.52  
    1.53  
    1.54  (*** existential quantifier for ordinals ***)
    1.55  
    1.56 -qed_goalw "oexI" thy [oex_def]
    1.57 -    "[| P(x);  x<A |] ==> EX x<A. P(x)"
    1.58 - (fn prems=> [ (REPEAT (ares_tac (prems @ [exI,conjI]) 1)) ]);
    1.59 +val prems = Goalw [oex_def] 
    1.60 +    "[| P(x);  x<A |] ==> EX x<A. P(x)";
    1.61 +by (REPEAT (ares_tac (prems @ [exI,conjI]) 1)) ;
    1.62 +qed "oexI";
    1.63  
    1.64  (*Not of the general form for such rules; ~EX has become ALL~ *)
    1.65  val prems = Goal
    1.66 @@ -53,35 +55,36 @@
    1.67  by (REPEAT (ares_tac (prems@[oexI,oallI,notI,notE]) 1)) ;
    1.68  qed "oexCI";
    1.69  
    1.70 -qed_goalw "oexE" thy [oex_def]
    1.71 +val major::prems = Goalw [oex_def] 
    1.72      "[| EX x<A. P(x);  !!x. [| x<A; P(x) |] ==> Q \
    1.73 -\    |] ==> Q"
    1.74 - (fn major::prems=>
    1.75 -  [ (rtac (major RS exE) 1),
    1.76 -    (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ]);
    1.77 +\    |] ==> Q";
    1.78 +by (rtac (major RS exE) 1);
    1.79 +by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ;
    1.80 +qed "oexE";
    1.81  
    1.82 -qed_goalw "oex_cong" thy [oex_def]
    1.83 +val prems = Goalw [oex_def] 
    1.84      "[| a=a';  !!x. x<a' ==> P(x) <-> P'(x) \
    1.85 -\    |] ==> oex(a,P) <-> oex(a',P')"
    1.86 - (fn prems=> [ (simp_tac (simpset() addsimps prems addcongs [conj_cong]) 1) ]);
    1.87 +\    |] ==> oex(a,P) <-> oex(a',P')";
    1.88 +by (simp_tac (simpset() addsimps prems addcongs [conj_cong]) 1) ;
    1.89 +qed "oex_cong";
    1.90  
    1.91  
    1.92  (*** Rules for Ordinal-Indexed Unions ***)
    1.93  
    1.94 -qed_goalw "OUN_I" thy [OUnion_def]
    1.95 -        "!!i. [| a<i;  b: B(a) |] ==> b: (UN z<i. B(z))"
    1.96 - (fn _=> [ fast_tac (claset() addSEs [ltE]) 1 ]);
    1.97 +Goalw [OUnion_def] "[| a<i;  b: B(a) |] ==> b: (UN z<i. B(z))";
    1.98 +by (blast_tac (claset() addSEs [ltE]) 1);
    1.99 +qed "OUN_I";
   1.100  
   1.101 -qed_goalw "OUN_E" thy [OUnion_def]
   1.102 -    "[| b : (UN z<i. B(z));  !!a.[| b: B(a);  a<i |] ==> R |] ==> R"
   1.103 - (fn major::prems=>
   1.104 -  [ (rtac (major RS CollectE) 1),
   1.105 -    (rtac UN_E 1),
   1.106 -    (REPEAT (ares_tac (ltI::prems) 1)) ]);
   1.107 +val major::prems = Goalw [OUnion_def] 
   1.108 +    "[| b : (UN z<i. B(z));  !!a.[| b: B(a);  a<i |] ==> R |] ==> R";
   1.109 +by (rtac (major RS CollectE) 1);
   1.110 +by (rtac UN_E 1);
   1.111 +by (REPEAT (ares_tac (ltI::prems) 1)) ;
   1.112 +qed "OUN_E";
   1.113  
   1.114 -qed_goalw "OUN_iff" thy [oex_def]
   1.115 -    "b : (UN x<i. B(x)) <-> (EX x<i. b : B(x))"
   1.116 - (fn _=> [ (fast_tac (claset() addIs [OUN_I] addSEs [OUN_E]) 1) ]);
   1.117 +Goalw [oex_def] "b : (UN x<i. B(x)) <-> (EX x<i. b : B(x))";
   1.118 +by (fast_tac (claset() addIs [OUN_I] addSEs [OUN_E]) 1) ;
   1.119 +qed "OUN_iff";
   1.120  
   1.121  val prems = Goal
   1.122      "[| i=j;  !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))";