getting rid of qed_goal
authorpaulson
Mon Jul 19 15:19:11 1999 +0200 (1999-07-19)
changeset 703053934985426a
parent 7029 08d4eb8500dd
child 7031 972b5f62f476
getting rid of qed_goal
src/HOL/HOL.ML
src/HOL/NatDef.ML
src/HOL/Option.ML
     1.1 --- a/src/HOL/HOL.ML	Mon Jul 19 15:18:16 1999 +0200
     1.2 +++ b/src/HOL/HOL.ML	Mon Jul 19 15:19:11 1999 +0200
     1.3 @@ -29,13 +29,12 @@
     1.4          a = b
     1.5          |   |
     1.6          c = d   *)
     1.7 -qed_goal "box_equals" HOL.thy
     1.8 -    "[| a=b;  a=c;  b=d |] ==> c=d"  
     1.9 - (fn prems=>
    1.10 -  [ (rtac trans 1),
    1.11 -    (rtac trans 1),
    1.12 -    (rtac sym 1),
    1.13 -    (REPEAT (resolve_tac prems 1)) ]);
    1.14 +Goal "[| a=b;  a=c;  b=d |] ==> c=d";
    1.15 +by (rtac trans 1);
    1.16 +by (rtac trans 1);
    1.17 +by (rtac sym 1);
    1.18 +by (REPEAT (assume_tac 1)) ;
    1.19 +qed "box_equals";
    1.20  
    1.21  
    1.22  (** Congruence rules for meta-application **)
    1.23 @@ -58,9 +57,10 @@
    1.24  (** Equality of booleans -- iff **)
    1.25  section "iff";
    1.26  
    1.27 -qed_goal "iffI" HOL.thy
    1.28 -   "[| P ==> Q;  Q ==> P |] ==> P=Q"
    1.29 - (fn prems=> [ (REPEAT (ares_tac (prems@[impI, iff RS mp RS mp]) 1)) ]);
    1.30 +val prems = Goal
    1.31 +   "[| P ==> Q;  Q ==> P |] ==> P=Q";
    1.32 +by (REPEAT (ares_tac (prems@[impI, iff RS mp RS mp]) 1));
    1.33 +qed "iffI";
    1.34  
    1.35  qed_goal "iffD2" HOL.thy "[| P=Q; Q |] ==> P"
    1.36   (fn prems =>
    1.37 @@ -81,7 +81,7 @@
    1.38  section "True";
    1.39  
    1.40  qed_goalw "TrueI" HOL.thy [True_def] "True"
    1.41 -  (fn _ => [rtac refl 1]);
    1.42 +  (fn _ => [(rtac refl 1)]);
    1.43  
    1.44  qed_goal "eqTrueI" HOL.thy "P ==> P=True" 
    1.45   (fn prems => [REPEAT(resolve_tac ([iffI,TrueI]@prems) 1)]);
    1.46 @@ -94,19 +94,19 @@
    1.47  section "!";
    1.48  
    1.49  qed_goalw "allI" HOL.thy [All_def] "(!!x::'a. P(x)) ==> !x. P(x)"
    1.50 - (fn prems => [resolve_tac (prems RL [eqTrueI RS ext]) 1]);
    1.51 + (fn prems => [(resolve_tac (prems RL [eqTrueI RS ext]) 1)]);
    1.52  
    1.53  qed_goalw "spec" HOL.thy [All_def] "! x::'a. P(x) ==> P(x)"
    1.54   (fn prems => [rtac eqTrueE 1, resolve_tac (prems RL [fun_cong]) 1]);
    1.55  
    1.56 -qed_goal "allE" HOL.thy "[| !x. P(x);  P(x) ==> R |] ==> R"
    1.57 - (fn major::prems=>
    1.58 -  [ (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ]);
    1.59 +val major::prems= goal HOL.thy "[| !x. P(x);  P(x) ==> R |] ==> R";
    1.60 +by (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ;
    1.61 +qed "allE";
    1.62  
    1.63 -qed_goal "all_dupE" HOL.thy 
    1.64 -    "[| ! x. P(x);  [| P(x); ! x. P(x) |] ==> R |] ==> R"
    1.65 - (fn prems =>
    1.66 -  [ (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ]);
    1.67 +val prems = goal HOL.thy 
    1.68 +    "[| ! x. P(x);  [| P(x); ! x. P(x) |] ==> R |] ==> R";
    1.69 +by (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ;
    1.70 +qed "all_dupE";
    1.71  
    1.72  
    1.73  (** False ** Depends upon spec; it is impossible to do propositional logic
    1.74 @@ -127,10 +127,10 @@
    1.75   (fn prems=> [rtac impI 1, eresolve_tac prems 1]);
    1.76  
    1.77  qed_goal "False_not_True" HOL.thy "False ~= True"
    1.78 -  (K [rtac notI 1, etac False_neq_True 1]);
    1.79 +  (fn _ => [rtac notI 1, etac False_neq_True 1]);
    1.80  
    1.81  qed_goal "True_not_False" HOL.thy "True ~= False"
    1.82 -  (K [rtac notI 1, dtac sym 1, etac False_neq_True 1]);
    1.83 +  (fn _ => [rtac notI 1, dtac sym 1, etac False_neq_True 1]);
    1.84  
    1.85  qed_goalw "notE" HOL.thy [not_def] "[| ~P;  P |] ==> R"
    1.86   (fn prems => [rtac (prems MRS mp RS FalseE) 1]);
    1.87 @@ -144,21 +144,24 @@
    1.88  (** Implication **)
    1.89  section "-->";
    1.90  
    1.91 -qed_goal "impE" HOL.thy "[| P-->Q;  P;  Q ==> R |] ==> R"
    1.92 - (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
    1.93 +val prems = Goal "[| P-->Q;  P;  Q ==> R |] ==> R";
    1.94 +by (REPEAT (resolve_tac (prems@[mp]) 1));
    1.95 +qed "impE";
    1.96  
    1.97  (* Reduces Q to P-->Q, allowing substitution in P. *)
    1.98 -qed_goal "rev_mp" HOL.thy "[| P;  P --> Q |] ==> Q"
    1.99 - (fn prems=>  [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
   1.100 +Goal "[| P;  P --> Q |] ==> Q";
   1.101 +by (REPEAT (ares_tac [mp] 1)) ;
   1.102 +qed "rev_mp";
   1.103  
   1.104 -qed_goal "contrapos" HOL.thy "[| ~Q;  P==>Q |] ==> ~P"
   1.105 - (fn [major,minor]=> 
   1.106 -  [ (rtac (major RS notE RS notI) 1), 
   1.107 -    (etac minor 1) ]);
   1.108 +val [major,minor] = Goal "[| ~Q;  P==>Q |] ==> ~P";
   1.109 +by (rtac (major RS notE RS notI) 1);
   1.110 +by (etac minor 1) ;
   1.111 +qed "contrapos";
   1.112  
   1.113 -qed_goal "rev_contrapos" HOL.thy "[| P==>Q; ~Q |] ==> ~P"
   1.114 - (fn [major,minor]=> 
   1.115 -  [ (rtac (minor RS contrapos) 1), (etac major 1) ]);
   1.116 +val [major,minor] = Goal "[| P==>Q; ~Q |] ==> ~P";
   1.117 +by (rtac (minor RS contrapos) 1);
   1.118 +by (etac major 1) ;
   1.119 +qed "rev_contrapos";
   1.120  
   1.121  (* ~(?t = ?s) ==> ~(?s = ?t) *)
   1.122  bind_thm("not_sym", sym COMP rev_contrapos);
   1.123 @@ -226,21 +229,25 @@
   1.124  val ccontr = FalseE RS classical;
   1.125  
   1.126  (*Double negation law*)
   1.127 -qed_goal "notnotD" HOL.thy "~~P ==> P"
   1.128 - (fn [major]=>
   1.129 -  [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
   1.130 +Goal "~~P ==> P";
   1.131 +by (rtac classical 1);
   1.132 +by (etac notE 1);
   1.133 +by (assume_tac 1);
   1.134 +qed "notnotD";
   1.135  
   1.136 -qed_goal "contrapos2" HOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [
   1.137 -        rtac classical 1,
   1.138 -        dtac p2 1,
   1.139 -        etac notE 1,
   1.140 -        rtac p1 1]);
   1.141 +val [p1,p2] = Goal "[| Q; ~ P ==> ~ Q |] ==> P";
   1.142 +by (rtac classical 1);
   1.143 +by (dtac p2 1);
   1.144 +by (etac notE 1);
   1.145 +by (rtac p1 1);
   1.146 +qed "contrapos2";
   1.147  
   1.148 -qed_goal "swap2" HOL.thy "[| P;  Q ==> ~ P |] ==> ~ Q" (fn [p1,p2] => [
   1.149 -        rtac notI 1,
   1.150 -        dtac p2 1,
   1.151 -        etac notE 1,
   1.152 -        rtac p1 1]);
   1.153 +val [p1,p2] = Goal "[| P;  Q ==> ~ P |] ==> ~ Q";
   1.154 +by (rtac notI 1);
   1.155 +by (dtac p2 1);
   1.156 +by (etac notE 1);
   1.157 +by (rtac p1 1);
   1.158 +qed "swap2";
   1.159  
   1.160  (** Unique existence **)
   1.161  section "?!";
   1.162 @@ -251,10 +258,11 @@
   1.163    [REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]);
   1.164  
   1.165  (*Sometimes easier to use: the premises have no shared variables.  Safe!*)
   1.166 -qed_goal "ex_ex1I" HOL.thy
   1.167 -    "[| ? x. P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> ?! x. P(x)"
   1.168 - (fn [ex,eq] => [ (rtac (ex RS exE) 1),
   1.169 -                  (REPEAT (ares_tac [ex1I,eq] 1)) ]);
   1.170 +val [ex,eq] = Goal
   1.171 +    "[| ? x. P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> ?! x. P(x)";
   1.172 +by (rtac (ex RS exE) 1);
   1.173 +by (REPEAT (ares_tac [ex1I,eq] 1)) ;
   1.174 +qed "ex_ex1I";
   1.175  
   1.176  qed_goalw "ex1E" HOL.thy [Ex1_def]
   1.177      "[| ?! x. P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R |] ==> R"
   1.178 @@ -272,90 +280,102 @@
   1.179  section "@";
   1.180  
   1.181  (*Easier to apply than selectI: conclusion has only one occurrence of P*)
   1.182 -qed_goal "selectI2" HOL.thy
   1.183 -    "[| P a;  !!x. P x ==> Q x |] ==> Q (@x. P x)"
   1.184 - (fn prems => [ resolve_tac prems 1, 
   1.185 -                rtac selectI 1, 
   1.186 -                resolve_tac prems 1 ]);
   1.187 +val prems = Goal
   1.188 +    "[| P a;  !!x. P x ==> Q x |] ==> Q (@x. P x)";
   1.189 +by (resolve_tac prems 1);
   1.190 +by (rtac selectI 1);
   1.191 +by (resolve_tac prems 1) ;
   1.192 +qed "selectI2";
   1.193  
   1.194  (*Easier to apply than selectI2 if witness ?a comes from an EX-formula*)
   1.195  qed_goal "selectI2EX" HOL.thy
   1.196    "[| ? a. P a; !!x. P x ==> Q x |] ==> Q (Eps P)"
   1.197  (fn [major,minor] => [rtac (major RS exE) 1, etac selectI2 1, etac minor 1]);
   1.198  
   1.199 -qed_goal "select_equality" HOL.thy
   1.200 -    "[| P a;  !!x. P x ==> x=a |] ==> (@x. P x) = a"
   1.201 - (fn prems => [ rtac selectI2 1, 
   1.202 -                REPEAT (ares_tac prems 1) ]);
   1.203 -
   1.204 -qed_goalw "select1_equality" HOL.thy [Ex1_def]
   1.205 -  "!!P. [| ?!x. P x; P a |] ==> (@x. P x) = a" (K [
   1.206 -	  rtac select_equality 1, atac 1,
   1.207 -          etac exE 1, etac conjE 1,
   1.208 -          rtac allE 1, atac 1,
   1.209 -          etac impE 1, atac 1, etac ssubst 1,
   1.210 -          etac allE 1, etac impE 1, atac 1, etac ssubst 1,
   1.211 -          rtac refl 1]);
   1.212 +val prems = Goal
   1.213 +    "[| P a;  !!x. P x ==> x=a |] ==> (@x. P x) = a";
   1.214 +by (rtac selectI2 1);
   1.215 +by (REPEAT (ares_tac prems 1)) ;
   1.216 +qed "select_equality";
   1.217  
   1.218 -qed_goal "select_eq_Ex" HOL.thy "P (@ x. P x) =  (? x. P x)" (K [
   1.219 -        rtac iffI 1,
   1.220 -        etac exI 1,
   1.221 -        etac exE 1,
   1.222 -        etac selectI 1]);
   1.223 +Goalw [Ex1_def] "[| ?!x. P x; P a |] ==> (@x. P x) = a";
   1.224 +by (rtac select_equality 1);
   1.225 +by (atac 1);
   1.226 +by (etac exE 1);
   1.227 +by (etac conjE 1);
   1.228 +by (rtac allE 1);
   1.229 +by (atac 1);
   1.230 +by (etac impE 1);
   1.231 +by (atac 1);
   1.232 +by (etac ssubst 1);
   1.233 +by (etac allE 1);
   1.234 +by (etac mp 1);
   1.235 +by (atac 1);
   1.236 +qed "select1_equality";
   1.237  
   1.238 -qed_goal "Eps_eq" HOL.thy "(@y. y=x) = x" (K [
   1.239 -	rtac select_equality 1,
   1.240 -	rtac refl 1,
   1.241 -	atac 1]);
   1.242 +Goal "P (@ x. P x) =  (? x. P x)";
   1.243 +by (rtac iffI 1);
   1.244 +by (etac exI 1);
   1.245 +by (etac exE 1);
   1.246 +by (etac selectI 1);
   1.247 +qed "select_eq_Ex";
   1.248  
   1.249 -qed_goal "Eps_sym_eq" HOL.thy "(Eps (op = x)) = x" (K [
   1.250 -	rtac select_equality 1,
   1.251 -	rtac refl 1,
   1.252 -	etac sym 1]);
   1.253 +Goal "(@y. y=x) = x";
   1.254 +by (rtac select_equality 1);
   1.255 +by (rtac refl 1);
   1.256 +by (atac 1);
   1.257 +qed "Eps_eq";
   1.258 +
   1.259 +Goal "(Eps (op = x)) = x";
   1.260 +by (rtac select_equality 1);
   1.261 +by (rtac refl 1);
   1.262 +by (etac sym 1);
   1.263 +qed "Eps_sym_eq";
   1.264  
   1.265  (** Classical intro rules for disjunction and existential quantifiers *)
   1.266  section "classical intro rules";
   1.267  
   1.268 -qed_goal "disjCI" HOL.thy "(~Q ==> P) ==> P|Q"
   1.269 - (fn prems=>
   1.270 -  [ (rtac classical 1),
   1.271 -    (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
   1.272 -    (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
   1.273 +val prems= Goal "(~Q ==> P) ==> P|Q";
   1.274 +by (rtac classical 1);
   1.275 +by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));
   1.276 +by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ;
   1.277 +qed "disjCI";
   1.278  
   1.279 -qed_goal "excluded_middle" HOL.thy "~P | P"
   1.280 - (fn _ => [ (REPEAT (ares_tac [disjCI] 1)) ]);
   1.281 +Goal "~P | P";
   1.282 +by (REPEAT (ares_tac [disjCI] 1)) ;
   1.283 +qed "excluded_middle";
   1.284  
   1.285  (*For disjunctive case analysis*)
   1.286  fun excluded_middle_tac sP =
   1.287      res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
   1.288  
   1.289  (*Classical implies (-->) elimination. *)
   1.290 -qed_goal "impCE" HOL.thy "[| P-->Q; ~P ==> R; Q ==> R |] ==> R" 
   1.291 - (fn major::prems=>
   1.292 -  [ rtac (excluded_middle RS disjE) 1,
   1.293 -    REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1))]);
   1.294 +val major::prems = Goal "[| P-->Q; ~P ==> R; Q ==> R |] ==> R";
   1.295 +by (rtac (excluded_middle RS disjE) 1);
   1.296 +by (REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1)));
   1.297 +qed "impCE";
   1.298  
   1.299  (*This version of --> elimination works on Q before P.  It works best for
   1.300    those cases in which P holds "almost everywhere".  Can't install as
   1.301    default: would break old proofs.*)
   1.302 -qed_goal "impCE'" thy 
   1.303 -    "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R"
   1.304 - (fn major::prems=>
   1.305 -  [ (resolve_tac [excluded_middle RS disjE] 1),
   1.306 -    (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
   1.307 +val major::prems = Goal
   1.308 +    "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R";
   1.309 +by (resolve_tac [excluded_middle RS disjE] 1);
   1.310 +by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ;
   1.311 +qed "impCE'";
   1.312  
   1.313  (*Classical <-> elimination. *)
   1.314 -qed_goal "iffCE" HOL.thy
   1.315 -    "[| P=Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
   1.316 - (fn major::prems =>
   1.317 -  [ (rtac (major RS iffE) 1),
   1.318 -    (REPEAT (DEPTH_SOLVE_1 
   1.319 -        (eresolve_tac ([asm_rl,impCE,notE]@prems) 1))) ]);
   1.320 +val major::prems = Goal
   1.321 +    "[| P=Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R";
   1.322 +by (rtac (major RS iffE) 1);
   1.323 +by (REPEAT (DEPTH_SOLVE_1 
   1.324 +	    (eresolve_tac ([asm_rl,impCE,notE]@prems) 1)));
   1.325 +qed "iffCE";
   1.326  
   1.327 -qed_goal "exCI" HOL.thy "(! x. ~P(x) ==> P(a)) ==> ? x. P(x)"
   1.328 - (fn prems=>
   1.329 -  [ (rtac ccontr 1),
   1.330 -    (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1))  ]);
   1.331 +val prems = Goal "(! x. ~P(x) ==> P(a)) ==> ? x. P(x)";
   1.332 +by (rtac ccontr 1);
   1.333 +by (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1))  ;
   1.334 +qed "exCI";
   1.335  
   1.336  
   1.337  (* case distinction *)
   1.338 @@ -425,7 +445,7 @@
   1.339  
   1.340  local
   1.341  
   1.342 -fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (K (normalize_thm [RSspec, RSmp]))) x;
   1.343 +fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (fn _ => (normalize_thm [RSspec, RSmp]))) x;
   1.344  
   1.345  in
   1.346  
     2.1 --- a/src/HOL/NatDef.ML	Mon Jul 19 15:18:16 1999 +0200
     2.2 +++ b/src/HOL/NatDef.ML	Mon Jul 19 15:19:11 1999 +0200
     2.3 @@ -235,16 +235,14 @@
     2.4  by (Blast_tac 1);
     2.5  qed "nat_neq_iff";
     2.6  
     2.7 -qed_goal "nat_less_cases" thy 
     2.8 -   "[| (m::nat)<n ==> P n m; m=n ==> P n m; n<m ==> P n m |] ==> P n m"
     2.9 -( fn [major,eqCase,lessCase] =>
    2.10 -        [
    2.11 -        (rtac (less_linear RS disjE) 1),
    2.12 -        (etac disjE 2),
    2.13 -        (etac lessCase 1),
    2.14 -        (etac (sym RS eqCase) 1),
    2.15 -        (etac major 1)
    2.16 -        ]);
    2.17 +val [major,eqCase,lessCase] = Goal 
    2.18 +   "[| (m::nat)<n ==> P n m; m=n ==> P n m; n<m ==> P n m |] ==> P n m";
    2.19 +by (rtac (less_linear RS disjE) 1);
    2.20 +by (etac disjE 2);
    2.21 +by (etac lessCase 1);
    2.22 +by (etac (sym RS eqCase) 1);
    2.23 +by (etac major 1);
    2.24 +qed "nat_less_cases";
    2.25  
    2.26  
    2.27  (** Inductive (?) properties **)
     3.1 --- a/src/HOL/Option.ML	Mon Jul 19 15:18:16 1999 +0200
     3.2 +++ b/src/HOL/Option.ML	Mon Jul 19 15:19:11 1999 +0200
     3.3 @@ -5,77 +5,92 @@
     3.4  
     3.5  Derived rules
     3.6  *)
     3.7 -open Option;
     3.8  
     3.9 -qed_goal "not_None_eq" thy "(x ~= None) = (? y. x = Some y)"
    3.10 -	(K [induct_tac "x" 1, Auto_tac]);
    3.11 +Goal "(x ~= None) = (? y. x = Some y)";
    3.12 +by (induct_tac "x" 1);
    3.13 +by Auto_tac;
    3.14 +qed "not_None_eq";
    3.15  AddIffs[not_None_eq];
    3.16  
    3.17 -qed_goal "not_Some_eq" thy "(!y. x ~= Some y) = (x = None)"
    3.18 -	(K [induct_tac "x" 1, Auto_tac]);
    3.19 +Goal "(!y. x ~= Some y) = (x = None)";
    3.20 +by (induct_tac "x" 1);
    3.21 +by Auto_tac;
    3.22 +qed "not_Some_eq";
    3.23  AddIffs[not_Some_eq];
    3.24  
    3.25  
    3.26  section "case analysis in premises";
    3.27  
    3.28 -val optionE = prove_goal thy 
    3.29 -	"[| opt = None ==> P;  !!x. opt = Some x ==> P |] ==> P" (fn prems => [
    3.30 -	case_tac "opt = None" 1,
    3.31 -	 eresolve_tac prems 1,
    3.32 -	dtac (not_None_eq RS iffD1) 1,
    3.33 -	etac exE 1,
    3.34 -	eresolve_tac prems 1]);
    3.35 -fun optionE_tac s = res_inst_tac [("opt",s)] optionE THEN_ALL_NEW hyp_subst_tac;
    3.36 +val prems = Goal
    3.37 +	"[| opt = None ==> P;  !!x. opt = Some x ==> P |] ==> P";
    3.38 +by (case_tac "opt = None" 1);
    3.39 +by (eresolve_tac prems 1);
    3.40 +by (dtac (not_None_eq RS iffD1) 1);
    3.41 +by (etac exE 1);
    3.42 +by (eresolve_tac prems 1);
    3.43 +qed "optionE";
    3.44  
    3.45 -qed_goal "option_caseE" thy "[|case x of None => P | Some y => Q y; \
    3.46 -\                  [|x = None;   P  |] ==> R; \
    3.47 -\             !!y. [|x = Some y; Q y|] ==> R|] ==> R" (fn prems => [
    3.48 -	cut_facts_tac prems 1,
    3.49 -	res_inst_tac [("opt","x")] optionE 1,
    3.50 -	 forward_tac prems 1,
    3.51 -	  forward_tac prems 3, 
    3.52 -	   Auto_tac]);
    3.53 -fun option_case_tac i = EVERY [
    3.54 -	etac option_caseE i,
    3.55 -	 hyp_subst_tac (i+1),
    3.56 -	hyp_subst_tac i];
    3.57 +val prems = Goal
    3.58 +     "[| case x of None => P | Some y => Q y; \
    3.59 +\        [| x = None;   P  |] ==> R; \
    3.60 +\        !!y. [|x = Some y; Q y|] ==> R|] ==> R";
    3.61 +by (cut_facts_tac prems 1);
    3.62 +by (res_inst_tac [("opt","x")] optionE 1);
    3.63 +by (forward_tac prems 1);
    3.64 +by (forward_tac prems 3);
    3.65 +by Auto_tac;
    3.66 +qed "option_caseE";
    3.67  
    3.68  
    3.69  section "the";
    3.70  
    3.71 -qed_goalw "the_Some" thy [the_def]
    3.72 -	"the (Some x) = x" (K [Simp_tac 1]);
    3.73 +Goalw [the_def] "the (Some x) = x";
    3.74 +by (Simp_tac 1);
    3.75 +qed "the_Some";
    3.76 +
    3.77  Addsimps [the_Some];
    3.78  
    3.79  
    3.80  
    3.81  section "option_map";
    3.82  
    3.83 -qed_goalw "option_map_None" thy [option_map_def] 
    3.84 -	"option_map f None = None" (K [Simp_tac 1]);
    3.85 -qed_goalw "option_map_Some" thy [option_map_def] 
    3.86 -	"option_map f (Some x) = Some (f x)" (K [Simp_tac 1]);
    3.87 +Goalw [option_map_def] "option_map f None = None";
    3.88 +by (Simp_tac 1);
    3.89 +qed "option_map_None";
    3.90 +
    3.91 +Goalw [option_map_def] "option_map f (Some x) = Some (f x)";
    3.92 +by (Simp_tac 1);
    3.93 +qed "option_map_Some";
    3.94 +
    3.95  Addsimps [option_map_None, option_map_Some];
    3.96  
    3.97 -val option_map_eq_Some = prove_goalw thy [option_map_def]
    3.98 -	"(option_map f xo = Some y) = (? z. xo = Some z & f z = y)" 
    3.99 - (K [asm_full_simp_tac (simpset() addsplits [option.split]) 1]);
   3.100 +Goalw [option_map_def]
   3.101 +    "(option_map f xo = Some y) = (? z. xo = Some z & f z = y)";
   3.102 +by (asm_full_simp_tac (simpset() addsplits [option.split]) 1);
   3.103 +qed "option_map_eq_Some";
   3.104  AddIffs[option_map_eq_Some];
   3.105  
   3.106  
   3.107  section "o2s";
   3.108  
   3.109 -qed_goal "ospec" thy 
   3.110 -	"!!x. [| !x:o2s A. P x; A = Some x |] ==> P x" (K [Auto_tac]);
   3.111 +Goal "[| !x:o2s A. P x; A = Some x |] ==> P x";
   3.112 +by Auto_tac;
   3.113 +qed "ospec";
   3.114  AddDs[ospec];
   3.115 +
   3.116  claset_ref() := claset() addSD2 ("ospec", ospec);
   3.117  
   3.118  
   3.119 -val elem_o2s = prove_goal thy "!!X. x : o2s xo = (xo = Some x)"
   3.120 - (K [optionE_tac "xo" 1, Auto_tac]);
   3.121 +Goal "x : o2s xo = (xo = Some x)";
   3.122 +by (exhaust_tac "xo" 1);
   3.123 +by Auto_tac;
   3.124 +qed "elem_o2s";
   3.125  AddIffs [elem_o2s];
   3.126  
   3.127 -val o2s_empty_eq = prove_goal thy "(o2s xo = {}) = (xo = None)"
   3.128 - (K [optionE_tac "xo" 1, Auto_tac]);
   3.129 +Goal "(o2s xo = {}) = (xo = None)";
   3.130 +by (exhaust_tac "xo" 1);
   3.131 +by Auto_tac;
   3.132 +qed "o2s_empty_eq";
   3.133 +
   3.134  Addsimps [o2s_empty_eq];
   3.135