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 +val prems = Goal
1.204 + "[| P a; !!x. P x ==> x=a |] ==> (@x. P x) = a";
1.205 +by (rtac selectI2 1);
1.206 +by (REPEAT (ares_tac prems 1)) ;
1.207 +qed "select_equality";
1.208
1.209 -qed_goalw "select1_equality" HOL.thy [Ex1_def]
1.210 - "!!P. [| ?!x. P x; P a |] ==> (@x. P x) = a" (K [
1.211 - rtac select_equality 1, atac 1,
1.212 - etac exE 1, etac conjE 1,
1.213 - rtac allE 1, atac 1,
1.214 - etac impE 1, atac 1, etac ssubst 1,
1.215 - etac allE 1, etac impE 1, atac 1, etac ssubst 1,
1.216 - rtac refl 1]);
1.217 +Goalw [Ex1_def] "[| ?!x. P x; P a |] ==> (@x. P x) = a";
1.218 +by (rtac select_equality 1);
1.219 +by (atac 1);
1.220 +by (etac exE 1);
1.221 +by (etac conjE 1);
1.222 +by (rtac allE 1);
1.223 +by (atac 1);
1.224 +by (etac impE 1);
1.225 +by (atac 1);
1.226 +by (etac ssubst 1);
1.227 +by (etac allE 1);
1.228 +by (etac mp 1);
1.229 +by (atac 1);
1.230 +qed "select1_equality";
1.231
1.232 -qed_goal "select_eq_Ex" HOL.thy "P (@ x. P x) = (? x. P x)" (K [
1.233 - rtac iffI 1,
1.234 - etac exI 1,
1.235 - etac exE 1,
1.236 - etac selectI 1]);
1.237 +Goal "P (@ x. P x) = (? x. P x)";
1.238 +by (rtac iffI 1);
1.239 +by (etac exI 1);
1.240 +by (etac exE 1);
1.241 +by (etac selectI 1);
1.242 +qed "select_eq_Ex";
1.243
1.244 -qed_goal "Eps_eq" HOL.thy "(@y. y=x) = x" (K [
1.245 - rtac select_equality 1,
1.246 - rtac refl 1,
1.247 - atac 1]);
1.248 +Goal "(@y. y=x) = x";
1.249 +by (rtac select_equality 1);
1.250 +by (rtac refl 1);
1.251 +by (atac 1);
1.252 +qed "Eps_eq";
1.253
1.254 -qed_goal "Eps_sym_eq" HOL.thy "(Eps (op = x)) = x" (K [
1.255 - rtac select_equality 1,
1.256 - rtac refl 1,
1.257 - etac sym 1]);
1.258 +Goal "(Eps (op = x)) = x";
1.259 +by (rtac select_equality 1);
1.260 +by (rtac refl 1);
1.261 +by (etac sym 1);
1.262 +qed "Eps_sym_eq";
1.263
1.264 (** Classical intro rules for disjunction and existential quantifiers *)
1.265 section "classical intro rules";
1.266
1.267 -qed_goal "disjCI" HOL.thy "(~Q ==> P) ==> P|Q"
1.268 - (fn prems=>
1.269 - [ (rtac classical 1),
1.270 - (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
1.271 - (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
1.272 +val prems= Goal "(~Q ==> P) ==> P|Q";
1.273 +by (rtac classical 1);
1.274 +by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));
1.275 +by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ;
1.276 +qed "disjCI";
1.277
1.278 -qed_goal "excluded_middle" HOL.thy "~P | P"
1.279 - (fn _ => [ (REPEAT (ares_tac [disjCI] 1)) ]);
1.280 +Goal "~P | P";
1.281 +by (REPEAT (ares_tac [disjCI] 1)) ;
1.282 +qed "excluded_middle";
1.283
1.284 (*For disjunctive case analysis*)
1.285 fun excluded_middle_tac sP =
1.286 res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
1.287
1.288 (*Classical implies (-->) elimination. *)
1.289 -qed_goal "impCE" HOL.thy "[| P-->Q; ~P ==> R; Q ==> R |] ==> R"
1.290 - (fn major::prems=>
1.291 - [ rtac (excluded_middle RS disjE) 1,
1.292 - REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1))]);
1.293 +val major::prems = Goal "[| P-->Q; ~P ==> R; Q ==> R |] ==> R";
1.294 +by (rtac (excluded_middle RS disjE) 1);
1.295 +by (REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1)));
1.296 +qed "impCE";
1.297
1.298 (*This version of --> elimination works on Q before P. It works best for
1.299 those cases in which P holds "almost everywhere". Can't install as
1.300 default: would break old proofs.*)
1.301 -qed_goal "impCE'" thy
1.302 - "[| P-->Q; Q ==> R; ~P ==> R |] ==> R"
1.303 - (fn major::prems=>
1.304 - [ (resolve_tac [excluded_middle RS disjE] 1),
1.305 - (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
1.306 +val major::prems = Goal
1.307 + "[| P-->Q; Q ==> R; ~P ==> R |] ==> R";
1.308 +by (resolve_tac [excluded_middle RS disjE] 1);
1.309 +by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ;
1.310 +qed "impCE'";
1.311
1.312 (*Classical <-> elimination. *)
1.313 -qed_goal "iffCE" HOL.thy
1.314 - "[| P=Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R"
1.315 - (fn major::prems =>
1.316 - [ (rtac (major RS iffE) 1),
1.317 - (REPEAT (DEPTH_SOLVE_1
1.318 - (eresolve_tac ([asm_rl,impCE,notE]@prems) 1))) ]);
1.319 +val major::prems = Goal
1.320 + "[| P=Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R";
1.321 +by (rtac (major RS iffE) 1);
1.322 +by (REPEAT (DEPTH_SOLVE_1
1.323 + (eresolve_tac ([asm_rl,impCE,notE]@prems) 1)));
1.324 +qed "iffCE";
1.325
1.326 -qed_goal "exCI" HOL.thy "(! x. ~P(x) ==> P(a)) ==> ? x. P(x)"
1.327 - (fn prems=>
1.328 - [ (rtac ccontr 1),
1.329 - (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1)) ]);
1.330 +val prems = Goal "(! x. ~P(x) ==> P(a)) ==> ? x. P(x)";
1.331 +by (rtac ccontr 1);
1.332 +by (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1)) ;
1.333 +qed "exCI";
1.334
1.335
1.336 (* case distinction *)
1.337 @@ -425,7 +445,7 @@
1.338
1.339 local
1.340
1.341 -fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (K (normalize_thm [RSspec, RSmp]))) x;
1.342 +fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (fn _ => (normalize_thm [RSspec, RSmp]))) x;
1.343
1.344 in
1.345
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