proper bootstrap of HOL theory and packages;
authorwenzelm
Wed Aug 25 20:49:02 1999 +0200 (1999-08-25)
changeset 7357d0e16da40ea2
parent 7356 1714c91b8729
child 7358 9e95b846ad42
proper bootstrap of HOL theory and packages;
src/HOL/HOL.ML
src/HOL/HOL.thy
src/HOL/HOL_lemmas.ML
src/HOL/Inductive.thy
src/HOL/IsaMakefile
src/HOL/Ord.thy
src/HOL/ROOT.ML
src/HOL/Recdef.thy
src/HOL/Record.thy
src/HOL/blastdata.ML
src/HOL/cladata.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/HOL.ML	Wed Aug 25 20:46:40 1999 +0200
     1.2 +++ b/src/HOL/HOL.ML	Wed Aug 25 20:49:02 1999 +0200
     1.3 @@ -1,456 +1,31 @@
     1.4 -(*  Title:      HOL/HOL.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Tobias Nipkow
     1.7 -    Copyright   1991  University of Cambridge
     1.8  
     1.9 -Derived rules from Appendix of Mike Gordons HOL Report, Cambridge TR 68 
    1.10 -*)
    1.11 -
    1.12 -
    1.13 -(** Equality **)
    1.14 -section "=";
    1.15 -
    1.16 -qed_goal "sym" HOL.thy "s=t ==> t=s"
    1.17 - (fn prems => [cut_facts_tac prems 1, etac subst 1, rtac refl 1]);
    1.18 -
    1.19 -(*calling "standard" reduces maxidx to 0*)
    1.20 -bind_thm ("ssubst", (sym RS subst));
    1.21 -
    1.22 -qed_goal "trans" HOL.thy "[| r=s; s=t |] ==> r=t"
    1.23 - (fn prems =>
    1.24 -        [rtac subst 1, resolve_tac prems 1, resolve_tac prems 1]);
    1.25 -
    1.26 -val prems = goal thy "(A == B) ==> A = B";
    1.27 -by (rewrite_goals_tac prems);
    1.28 -by (rtac refl 1);
    1.29 -qed "def_imp_eq";
    1.30 -
    1.31 -(*Useful with eresolve_tac for proving equalties from known equalities.
    1.32 -        a = b
    1.33 -        |   |
    1.34 -        c = d   *)
    1.35 -Goal "[| a=b;  a=c;  b=d |] ==> c=d";
    1.36 -by (rtac trans 1);
    1.37 -by (rtac trans 1);
    1.38 -by (rtac sym 1);
    1.39 -by (REPEAT (assume_tac 1)) ;
    1.40 -qed "box_equals";
    1.41 -
    1.42 -
    1.43 -(** Congruence rules for meta-application **)
    1.44 -section "Congruence";
    1.45 -
    1.46 -(*similar to AP_THM in Gordon's HOL*)
    1.47 -qed_goal "fun_cong" HOL.thy "(f::'a=>'b) = g ==> f(x)=g(x)"
    1.48 -  (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
    1.49 -
    1.50 -(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
    1.51 -qed_goal "arg_cong" HOL.thy "x=y ==> f(x)=f(y)"
    1.52 - (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
    1.53 -
    1.54 -qed_goal "cong" HOL.thy
    1.55 -   "[| f = g; (x::'a) = y |] ==> f(x) = g(y)"
    1.56 - (fn [prem1,prem2] =>
    1.57 -   [rtac (prem1 RS subst) 1, rtac (prem2 RS subst) 1, rtac refl 1]);
    1.58 -
    1.59 -
    1.60 -(** Equality of booleans -- iff **)
    1.61 -section "iff";
    1.62 -
    1.63 -val prems = Goal
    1.64 -   "[| P ==> Q;  Q ==> P |] ==> P=Q";
    1.65 -by (REPEAT (ares_tac (prems@[impI, iff RS mp RS mp]) 1));
    1.66 -qed "iffI";
    1.67 -
    1.68 -qed_goal "iffD2" HOL.thy "[| P=Q; Q |] ==> P"
    1.69 - (fn prems =>
    1.70 -        [rtac ssubst 1, resolve_tac prems 1, resolve_tac prems 1]);
    1.71 -
    1.72 -qed_goal "rev_iffD2" HOL.thy "!!P. [| Q; P=Q |] ==> P"
    1.73 - (fn _ => [etac iffD2 1, assume_tac 1]);
    1.74 -
    1.75 -bind_thm ("iffD1", sym RS iffD2);
    1.76 -bind_thm ("rev_iffD1", sym RSN (2, rev_iffD2));
    1.77 -
    1.78 -qed_goal "iffE" HOL.thy
    1.79 -    "[| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R"
    1.80 - (fn [p1,p2] => [REPEAT(ares_tac([p1 RS iffD2, p1 RS iffD1, p2, impI])1)]);
    1.81 -
    1.82 -
    1.83 -(** True **)
    1.84 -section "True";
    1.85 -
    1.86 -qed_goalw "TrueI" HOL.thy [True_def] "True"
    1.87 -  (fn _ => [(rtac refl 1)]);
    1.88 -
    1.89 -qed_goal "eqTrueI" HOL.thy "P ==> P=True" 
    1.90 - (fn prems => [REPEAT(resolve_tac ([iffI,TrueI]@prems) 1)]);
    1.91 -
    1.92 -qed_goal "eqTrueE" HOL.thy "P=True ==> P" 
    1.93 - (fn prems => [REPEAT(resolve_tac (prems@[TrueI,iffD2]) 1)]);
    1.94 -
    1.95 -
    1.96 -(** Universal quantifier **)
    1.97 -section "!";
    1.98 -
    1.99 -qed_goalw "allI" HOL.thy [All_def] "(!!x::'a. P(x)) ==> !x. P(x)"
   1.100 - (fn prems => [(resolve_tac (prems RL [eqTrueI RS ext]) 1)]);
   1.101 -
   1.102 -qed_goalw "spec" HOL.thy [All_def] "! x::'a. P(x) ==> P(x)"
   1.103 - (fn prems => [rtac eqTrueE 1, resolve_tac (prems RL [fun_cong]) 1]);
   1.104 -
   1.105 -val major::prems= goal HOL.thy "[| !x. P(x);  P(x) ==> R |] ==> R";
   1.106 -by (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ;
   1.107 -qed "allE";
   1.108 -
   1.109 -val prems = goal HOL.thy 
   1.110 -    "[| ! x. P(x);  [| P(x); ! x. P(x) |] ==> R |] ==> R";
   1.111 -by (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ;
   1.112 -qed "all_dupE";
   1.113 -
   1.114 -
   1.115 -(** False ** Depends upon spec; it is impossible to do propositional logic
   1.116 -             before quantifiers! **)
   1.117 -section "False";
   1.118 -
   1.119 -qed_goalw "FalseE" HOL.thy [False_def] "False ==> P"
   1.120 - (fn [major] => [rtac (major RS spec) 1]);
   1.121 -
   1.122 -qed_goal "False_neq_True" HOL.thy "False=True ==> P"
   1.123 - (fn [prem] => [rtac (prem RS eqTrueE RS FalseE) 1]);
   1.124 -
   1.125 -
   1.126 -(** Negation **)
   1.127 -section "~";
   1.128 -
   1.129 -qed_goalw "notI" HOL.thy [not_def] "(P ==> False) ==> ~P"
   1.130 - (fn prems=> [rtac impI 1, eresolve_tac prems 1]);
   1.131 -
   1.132 -qed_goal "False_not_True" HOL.thy "False ~= True"
   1.133 -  (fn _ => [rtac notI 1, etac False_neq_True 1]);
   1.134 -
   1.135 -qed_goal "True_not_False" HOL.thy "True ~= False"
   1.136 -  (fn _ => [rtac notI 1, dtac sym 1, etac False_neq_True 1]);
   1.137 -
   1.138 -qed_goalw "notE" HOL.thy [not_def] "[| ~P;  P |] ==> R"
   1.139 - (fn prems => [rtac (prems MRS mp RS FalseE) 1]);
   1.140 -
   1.141 -bind_thm ("classical2", notE RS notI);
   1.142 -
   1.143 -qed_goal "rev_notE" HOL.thy "!!P R. [| P; ~P |] ==> R"
   1.144 - (fn _ => [REPEAT (ares_tac [notE] 1)]);
   1.145 -
   1.146 -
   1.147 -(** Implication **)
   1.148 -section "-->";
   1.149 -
   1.150 -val prems = Goal "[| P-->Q;  P;  Q ==> R |] ==> R";
   1.151 -by (REPEAT (resolve_tac (prems@[mp]) 1));
   1.152 -qed "impE";
   1.153 -
   1.154 -(* Reduces Q to P-->Q, allowing substitution in P. *)
   1.155 -Goal "[| P;  P --> Q |] ==> Q";
   1.156 -by (REPEAT (ares_tac [mp] 1)) ;
   1.157 -qed "rev_mp";
   1.158 -
   1.159 -val [major,minor] = Goal "[| ~Q;  P==>Q |] ==> ~P";
   1.160 -by (rtac (major RS notE RS notI) 1);
   1.161 -by (etac minor 1) ;
   1.162 -qed "contrapos";
   1.163 -
   1.164 -val [major,minor] = Goal "[| P==>Q; ~Q |] ==> ~P";
   1.165 -by (rtac (minor RS contrapos) 1);
   1.166 -by (etac major 1) ;
   1.167 -qed "rev_contrapos";
   1.168 -
   1.169 -(* ~(?t = ?s) ==> ~(?s = ?t) *)
   1.170 -bind_thm("not_sym", sym COMP rev_contrapos);
   1.171 -
   1.172 -
   1.173 -(** Existential quantifier **)
   1.174 -section "?";
   1.175 -
   1.176 -qed_goalw "exI" HOL.thy [Ex_def] "P x ==> ? x::'a. P x"
   1.177 - (fn prems => [rtac selectI 1, resolve_tac prems 1]);
   1.178 -
   1.179 -qed_goalw "exE" HOL.thy [Ex_def]
   1.180 -  "[| ? x::'a. P(x); !!x. P(x) ==> Q |] ==> Q"
   1.181 -  (fn prems => [REPEAT(resolve_tac prems 1)]);
   1.182 -
   1.183 -
   1.184 -(** Conjunction **)
   1.185 -section "&";
   1.186 -
   1.187 -qed_goalw "conjI" HOL.thy [and_def] "[| P; Q |] ==> P&Q"
   1.188 - (fn prems =>
   1.189 -  [REPEAT (resolve_tac (prems@[allI,impI]) 1 ORELSE etac (mp RS mp) 1)]);
   1.190 -
   1.191 -qed_goalw "conjunct1" HOL.thy [and_def] "[| P & Q |] ==> P"
   1.192 - (fn prems =>
   1.193 -   [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
   1.194 -
   1.195 -qed_goalw "conjunct2" HOL.thy [and_def] "[| P & Q |] ==> Q"
   1.196 - (fn prems =>
   1.197 -   [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
   1.198 -
   1.199 -qed_goal "conjE" HOL.thy "[| P&Q;  [| P; Q |] ==> R |] ==> R"
   1.200 - (fn prems =>
   1.201 -         [cut_facts_tac prems 1, resolve_tac prems 1,
   1.202 -          etac conjunct1 1, etac conjunct2 1]);
   1.203 -
   1.204 -qed_goal "context_conjI" HOL.thy  "[| P; P ==> Q |] ==> P & Q"
   1.205 - (fn prems => [REPEAT(resolve_tac (conjI::prems) 1)]);
   1.206 -
   1.207 -
   1.208 -(** Disjunction *)
   1.209 -section "|";
   1.210 -
   1.211 -qed_goalw "disjI1" HOL.thy [or_def] "P ==> P|Q"
   1.212 - (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
   1.213 -
   1.214 -qed_goalw "disjI2" HOL.thy [or_def] "Q ==> P|Q"
   1.215 - (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
   1.216 -
   1.217 -qed_goalw "disjE" HOL.thy [or_def] "[| P | Q; P ==> R; Q ==> R |] ==> R"
   1.218 - (fn [a1,a2,a3] =>
   1.219 -        [rtac (mp RS mp) 1, rtac spec 1, rtac a1 1,
   1.220 -         rtac (a2 RS impI) 1, assume_tac 1, rtac (a3 RS impI) 1, assume_tac 1]);
   1.221 -
   1.222 -
   1.223 -(** CCONTR -- classical logic **)
   1.224 -section "classical logic";
   1.225 -
   1.226 -qed_goalw "classical" HOL.thy [not_def]  "(~P ==> P) ==> P"
   1.227 - (fn [prem] =>
   1.228 -   [rtac (True_or_False RS (disjE RS eqTrueE)) 1,  assume_tac 1,
   1.229 -    rtac (impI RS prem RS eqTrueI) 1,
   1.230 -    etac subst 1,  assume_tac 1]);
   1.231 -
   1.232 -val ccontr = FalseE RS classical;
   1.233 -
   1.234 -(*Double negation law*)
   1.235 -Goal "~~P ==> P";
   1.236 -by (rtac classical 1);
   1.237 -by (etac notE 1);
   1.238 -by (assume_tac 1);
   1.239 -qed "notnotD";
   1.240 -
   1.241 -val [p1,p2] = Goal "[| Q; ~ P ==> ~ Q |] ==> P";
   1.242 -by (rtac classical 1);
   1.243 -by (dtac p2 1);
   1.244 -by (etac notE 1);
   1.245 -by (rtac p1 1);
   1.246 -qed "contrapos2";
   1.247 -
   1.248 -val [p1,p2] = Goal "[| P;  Q ==> ~ P |] ==> ~ Q";
   1.249 -by (rtac notI 1);
   1.250 -by (dtac p2 1);
   1.251 -by (etac notE 1);
   1.252 -by (rtac p1 1);
   1.253 -qed "swap2";
   1.254 -
   1.255 -(** Unique existence **)
   1.256 -section "?!";
   1.257 -
   1.258 -qed_goalw "ex1I" HOL.thy [Ex1_def]
   1.259 -            "[| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
   1.260 - (fn prems =>
   1.261 -  [REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]);
   1.262 -
   1.263 -(*Sometimes easier to use: the premises have no shared variables.  Safe!*)
   1.264 -val [ex,eq] = Goal
   1.265 -    "[| ? x. P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> ?! x. P(x)";
   1.266 -by (rtac (ex RS exE) 1);
   1.267 -by (REPEAT (ares_tac [ex1I,eq] 1)) ;
   1.268 -qed "ex_ex1I";
   1.269 -
   1.270 -qed_goalw "ex1E" HOL.thy [Ex1_def]
   1.271 -    "[| ?! x. P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R |] ==> R"
   1.272 - (fn major::prems =>
   1.273 -  [rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);
   1.274 -
   1.275 -Goal "?! x. P x ==> ? x. P x";
   1.276 -by (etac ex1E 1);
   1.277 -by (rtac exI 1);
   1.278 -by (assume_tac 1);
   1.279 -qed "ex1_implies_ex";
   1.280 -
   1.281 -
   1.282 -(** Select: Hilbert's Epsilon-operator **)
   1.283 -section "@";
   1.284 -
   1.285 -(*Easier to apply than selectI: conclusion has only one occurrence of P*)
   1.286 -val prems = Goal
   1.287 -    "[| P a;  !!x. P x ==> Q x |] ==> Q (@x. P x)";
   1.288 -by (resolve_tac prems 1);
   1.289 -by (rtac selectI 1);
   1.290 -by (resolve_tac prems 1) ;
   1.291 -qed "selectI2";
   1.292 -
   1.293 -(*Easier to apply than selectI2 if witness ?a comes from an EX-formula*)
   1.294 -qed_goal "selectI2EX" HOL.thy
   1.295 -  "[| ? a. P a; !!x. P x ==> Q x |] ==> Q (Eps P)"
   1.296 -(fn [major,minor] => [rtac (major RS exE) 1, etac selectI2 1, etac minor 1]);
   1.297 -
   1.298 -val prems = Goal
   1.299 -    "[| P a;  !!x. P x ==> x=a |] ==> (@x. P x) = a";
   1.300 -by (rtac selectI2 1);
   1.301 -by (REPEAT (ares_tac prems 1)) ;
   1.302 -qed "select_equality";
   1.303 -
   1.304 -Goalw [Ex1_def] "[| ?!x. P x; P a |] ==> (@x. P x) = a";
   1.305 -by (rtac select_equality 1);
   1.306 -by (atac 1);
   1.307 -by (etac exE 1);
   1.308 -by (etac conjE 1);
   1.309 -by (rtac allE 1);
   1.310 -by (atac 1);
   1.311 -by (etac impE 1);
   1.312 -by (atac 1);
   1.313 -by (etac ssubst 1);
   1.314 -by (etac allE 1);
   1.315 -by (etac mp 1);
   1.316 -by (atac 1);
   1.317 -qed "select1_equality";
   1.318 -
   1.319 -Goal "P (@ x. P x) =  (? x. P x)";
   1.320 -by (rtac iffI 1);
   1.321 -by (etac exI 1);
   1.322 -by (etac exE 1);
   1.323 -by (etac selectI 1);
   1.324 -qed "select_eq_Ex";
   1.325 -
   1.326 -Goal "(@y. y=x) = x";
   1.327 -by (rtac select_equality 1);
   1.328 -by (rtac refl 1);
   1.329 -by (atac 1);
   1.330 -qed "Eps_eq";
   1.331 -
   1.332 -Goal "(Eps (op = x)) = x";
   1.333 -by (rtac select_equality 1);
   1.334 -by (rtac refl 1);
   1.335 -by (etac sym 1);
   1.336 -qed "Eps_sym_eq";
   1.337 -
   1.338 -(** Classical intro rules for disjunction and existential quantifiers *)
   1.339 -section "classical intro rules";
   1.340 -
   1.341 -val prems= Goal "(~Q ==> P) ==> P|Q";
   1.342 -by (rtac classical 1);
   1.343 -by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));
   1.344 -by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ;
   1.345 -qed "disjCI";
   1.346 -
   1.347 -Goal "~P | P";
   1.348 -by (REPEAT (ares_tac [disjCI] 1)) ;
   1.349 -qed "excluded_middle";
   1.350 -
   1.351 -(*For disjunctive case analysis*)
   1.352 -fun excluded_middle_tac sP =
   1.353 -    res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
   1.354 -
   1.355 -(*Classical implies (-->) elimination. *)
   1.356 -val major::prems = Goal "[| P-->Q; ~P ==> R; Q ==> R |] ==> R";
   1.357 -by (rtac (excluded_middle RS disjE) 1);
   1.358 -by (REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1)));
   1.359 -qed "impCE";
   1.360 -
   1.361 -(*This version of --> elimination works on Q before P.  It works best for
   1.362 -  those cases in which P holds "almost everywhere".  Can't install as
   1.363 -  default: would break old proofs.*)
   1.364 -val major::prems = Goal
   1.365 -    "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R";
   1.366 -by (resolve_tac [excluded_middle RS disjE] 1);
   1.367 -by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ;
   1.368 -qed "impCE'";
   1.369 -
   1.370 -(*Classical <-> elimination. *)
   1.371 -val major::prems = Goal
   1.372 -    "[| P=Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R";
   1.373 -by (rtac (major RS iffE) 1);
   1.374 -by (REPEAT (DEPTH_SOLVE_1 
   1.375 -	    (eresolve_tac ([asm_rl,impCE,notE]@prems) 1)));
   1.376 -qed "iffCE";
   1.377 -
   1.378 -val prems = Goal "(! x. ~P(x) ==> P(a)) ==> ? x. P(x)";
   1.379 -by (rtac ccontr 1);
   1.380 -by (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1))  ;
   1.381 -qed "exCI";
   1.382 -
   1.383 -
   1.384 -(* case distinction *)
   1.385 -
   1.386 -qed_goal "case_split_thm" HOL.thy "[| P ==> Q; ~P ==> Q |] ==> Q"
   1.387 -  (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1,
   1.388 -                  etac p2 1, etac p1 1]);
   1.389 -
   1.390 -fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
   1.391 -
   1.392 -
   1.393 -(** Standard abbreviations **)
   1.394 -
   1.395 -(*Apply an equality or definition ONCE.
   1.396 -  Fails unless the substitution has an effect*)
   1.397 -fun stac th = 
   1.398 -  let val th' = th RS def_imp_eq handle THM _ => th
   1.399 -  in  CHANGED_GOAL (rtac (th' RS ssubst))
   1.400 -  end;
   1.401 -
   1.402 -fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
   1.403 -
   1.404 -
   1.405 -(** strip ! and --> from proved goal while preserving !-bound var names **)
   1.406 -
   1.407 -local
   1.408 -
   1.409 -(* Use XXX to avoid forall_intr failing because of duplicate variable name *)
   1.410 -val myspec = read_instantiate [("P","?XXX")] spec;
   1.411 -val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec;
   1.412 -val cvx = cterm_of (#sign(rep_thm myspec)) vx;
   1.413 -val aspec = forall_intr cvx myspec;
   1.414 -
   1.415 -in
   1.416 -
   1.417 -fun RSspec th =
   1.418 -  (case concl_of th of
   1.419 -     _ $ (Const("All",_) $ Abs(a,_,_)) =>
   1.420 -         let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),vxT))
   1.421 -         in th RS forall_elim ca aspec end
   1.422 -  | _ => raise THM("RSspec",0,[th]));
   1.423 -
   1.424 -fun RSmp th =
   1.425 -  (case concl_of th of
   1.426 -     _ $ (Const("op -->",_)$_$_) => th RS mp
   1.427 -  | _ => raise THM("RSmp",0,[th]));
   1.428 -
   1.429 -fun normalize_thm funs =
   1.430 -  let fun trans [] th = th
   1.431 -	| trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
   1.432 -  in zero_var_indexes o trans funs end;
   1.433 -
   1.434 -fun qed_spec_mp name =
   1.435 -  let val thm = normalize_thm [RSspec,RSmp] (result())
   1.436 -  in ThmDatabase.ml_store_thm(name, thm) end;
   1.437 -
   1.438 -fun qed_goal_spec_mp name thy s p = 
   1.439 -	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
   1.440 -
   1.441 -fun qed_goalw_spec_mp name thy defs s p = 
   1.442 -	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
   1.443 -
   1.444 +structure HOL =
   1.445 +struct
   1.446 +  val thy = the_context ();
   1.447 +  val plusI = plusI;
   1.448 +  val minusI = minusI;
   1.449 +  val timesI = timesI;
   1.450 +  val powerI = powerI;
   1.451 +  val eq_reflection = eq_reflection;
   1.452 +  val refl = refl;
   1.453 +  val subst = subst;
   1.454 +  val ext = ext;
   1.455 +  val selectI = selectI;
   1.456 +  val impI = impI;
   1.457 +  val mp = mp;
   1.458 +  val True_def = True_def;
   1.459 +  val All_def = All_def;
   1.460 +  val Ex_def = Ex_def;
   1.461 +  val False_def = False_def;
   1.462 +  val not_def = not_def;
   1.463 +  val and_def = and_def;
   1.464 +  val or_def = or_def;
   1.465 +  val Ex1_def = Ex1_def;
   1.466 +  val iff = iff;
   1.467 +  val True_or_False = True_or_False;
   1.468 +  val Let_def = Let_def;
   1.469 +  val if_def = if_def;
   1.470 +  val arbitrary_def = arbitrary_def;
   1.471  end;
   1.472  
   1.473 -
   1.474 -(* attributes *)
   1.475 -
   1.476 -local
   1.477 -
   1.478 -fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (fn _ => (normalize_thm [RSspec, RSmp]))) x;
   1.479 -
   1.480 -in
   1.481 -
   1.482 -val hol_setup =
   1.483 - [Attrib.add_attributes
   1.484 -  [("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]];
   1.485 -
   1.486 -end;
   1.487 +open HOL;
     2.1 --- a/src/HOL/HOL.thy	Wed Aug 25 20:46:40 1999 +0200
     2.2 +++ b/src/HOL/HOL.thy	Wed Aug 25 20:49:02 1999 +0200
     2.3 @@ -6,72 +6,63 @@
     2.4  Higher-Order Logic.
     2.5  *)
     2.6  
     2.7 -HOL = CPure +
     2.8 +theory HOL = CPure
     2.9 +files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML"):
    2.10  
    2.11  
    2.12  (** Core syntax **)
    2.13  
    2.14  global
    2.15  
    2.16 -classes
    2.17 -  term < logic
    2.18 +classes "term" < logic
    2.19 +defaultsort "term"
    2.20  
    2.21 -default
    2.22 -  term
    2.23 -
    2.24 -types
    2.25 -  bool
    2.26 +typedecl bool
    2.27  
    2.28  arities
    2.29 -  fun :: (term, term) term
    2.30 -  bool :: term
    2.31 +  bool :: "term"
    2.32 +  fun :: ("term", "term") "term"
    2.33  
    2.34  
    2.35  consts
    2.36  
    2.37    (* Constants *)
    2.38  
    2.39 -  Trueprop      :: bool => prop                     ("(_)" 5)
    2.40 -  Not           :: bool => bool                     ("~ _" [40] 40)
    2.41 -  True, False   :: bool
    2.42 -  If            :: [bool, 'a, 'a] => 'a   ("(if (_)/ then (_)/ else (_))" 10)
    2.43 +  Trueprop      :: "bool => prop"                   ("(_)" 5)
    2.44 +  Not           :: "bool => bool"                   ("~ _" [40] 40)
    2.45 +  True          :: bool
    2.46 +  False         :: bool
    2.47 +  If            :: "[bool, 'a, 'a] => 'a"           ("(if (_)/ then (_)/ else (_))" 10)
    2.48    arbitrary     :: 'a
    2.49  
    2.50    (* Binders *)
    2.51  
    2.52 -  Eps           :: ('a => bool) => 'a
    2.53 -  All           :: ('a => bool) => bool             (binder "ALL " 10)
    2.54 -  Ex            :: ('a => bool) => bool             (binder "EX " 10)
    2.55 -  Ex1           :: ('a => bool) => bool             (binder "EX! " 10)
    2.56 -  Let           :: ['a, 'a => 'b] => 'b
    2.57 +  Eps           :: "('a => bool) => 'a"
    2.58 +  All           :: "('a => bool) => bool"           (binder "ALL " 10)
    2.59 +  Ex            :: "('a => bool) => bool"           (binder "EX " 10)
    2.60 +  Ex1           :: "('a => bool) => bool"           (binder "EX! " 10)
    2.61 +  Let           :: "['a, 'a => 'b] => 'b"
    2.62  
    2.63    (* Infixes *)
    2.64  
    2.65 -  "="           :: ['a, 'a] => bool                 (infixl 50)
    2.66 -  "&"           :: [bool, bool] => bool             (infixr 35)
    2.67 -  "|"           :: [bool, bool] => bool             (infixr 30)
    2.68 -  "-->"         :: [bool, bool] => bool             (infixr 25)
    2.69 +  "="           :: "['a, 'a] => bool"               (infixl 50)
    2.70 +  &             :: "[bool, bool] => bool"           (infixr 35)
    2.71 +  "|"           :: "[bool, bool] => bool"           (infixr 30)
    2.72 +  -->           :: "[bool, bool] => bool"           (infixr 25)
    2.73  
    2.74  
    2.75  (* Overloaded Constants *)
    2.76  
    2.77 -axclass
    2.78 -  plus < term
    2.79 -
    2.80 -axclass
    2.81 -  minus < term
    2.82 -
    2.83 -axclass
    2.84 -  times < term
    2.85 -
    2.86 -axclass
    2.87 -  power < term
    2.88 +axclass plus < "term"
    2.89 +axclass minus < "term"
    2.90 +axclass times < "term"
    2.91 +axclass power < "term"
    2.92  
    2.93  consts
    2.94 -  "+"           :: ['a::plus, 'a]  => 'a            (infixl 65)
    2.95 -  "-"           :: ['a::minus, 'a] => 'a            (infixl 65)
    2.96 -  uminus        :: ['a::minus] => 'a                ("- _" [81] 80)
    2.97 -  "*"           :: ['a::times, 'a] => 'a            (infixl 70)
    2.98 +  "+"           :: "['a::plus, 'a]  => 'a"          (infixl 65)
    2.99 +  -             :: "['a::minus, 'a] => 'a"          (infixl 65)
   2.100 +  uminus        :: "['a::minus] => 'a"              ("- _" [81] 80)
   2.101 +  "*"           :: "['a::times, 'a] => 'a"          (infixl 70)
   2.102    (*See Nat.thy for "^"*)
   2.103  
   2.104  
   2.105 @@ -83,22 +74,22 @@
   2.106    case_syn  cases_syn
   2.107  
   2.108  syntax
   2.109 -  "~="          :: ['a, 'a] => bool                 (infixl 50)
   2.110 -  "_Eps"        :: [pttrn, bool] => 'a              ("(3SOME _./ _)" [0, 10] 10)
   2.111 +  ~=            :: "['a, 'a] => bool"                    (infixl 50)
   2.112 +  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3SOME _./ _)" [0, 10] 10)
   2.113  
   2.114    (* Let expressions *)
   2.115  
   2.116 -  "_bind"       :: [pttrn, 'a] => letbind           ("(2_ =/ _)" 10)
   2.117 -  ""            :: letbind => letbinds              ("_")
   2.118 -  "_binds"      :: [letbind, letbinds] => letbinds  ("_;/ _")
   2.119 -  "_Let"        :: [letbinds, 'a] => 'a             ("(let (_)/ in (_))" 10)
   2.120 +  "_bind"       :: "[pttrn, 'a] => letbind"              ("(2_ =/ _)" 10)
   2.121 +  ""            :: "letbind => letbinds"                 ("_")
   2.122 +  "_binds"      :: "[letbind, letbinds] => letbinds"     ("_;/ _")
   2.123 +  "_Let"        :: "[letbinds, 'a] => 'a"                ("(let (_)/ in (_))" 10)
   2.124  
   2.125    (* Case expressions *)
   2.126  
   2.127 -  "@case"       :: ['a, cases_syn] => 'b            ("(case _ of/ _)" 10)
   2.128 -  "@case1"      :: ['a, 'b] => case_syn             ("(2_ =>/ _)" 10)
   2.129 -  ""            :: case_syn => cases_syn            ("_")
   2.130 -  "@case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ | _")
   2.131 +  "@case"       :: "['a, cases_syn] => 'b"               ("(case _ of/ _)" 10)
   2.132 +  "@case1"      :: "['a, 'b] => case_syn"                ("(2_ =>/ _)" 10)
   2.133 +  ""            :: "case_syn => cases_syn"               ("_")
   2.134 +  "@case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ | _")
   2.135  
   2.136  translations
   2.137    "x ~= y"                == "~ (x = y)"
   2.138 @@ -107,37 +98,37 @@
   2.139    "let x = a in e"        == "Let a (%x. e)"
   2.140  
   2.141  syntax ("" output)
   2.142 -  "op ="        :: ['a, 'a] => bool                 ("(_ =/ _)" [51, 51] 50)
   2.143 -  "op ~="       :: ['a, 'a] => bool                 ("(_ ~=/ _)" [51, 51] 50)
   2.144 +  "op ="        :: "['a, 'a] => bool"                    ("(_ =/ _)" [51, 51] 50)
   2.145 +  "op ~="       :: "['a, 'a] => bool"                    ("(_ ~=/ _)" [51, 51] 50)
   2.146  
   2.147  syntax (symbols)
   2.148 -  Not           :: bool => bool                     ("\\<not> _" [40] 40)
   2.149 -  "op &"        :: [bool, bool] => bool             (infixr "\\<and>" 35)
   2.150 -  "op |"        :: [bool, bool] => bool             (infixr "\\<or>" 30)
   2.151 -  "op -->"      :: [bool, bool] => bool             (infixr "\\<midarrow>\\<rightarrow>" 25)
   2.152 -  "op o"        :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl "\\<circ>" 55)
   2.153 -  "op ~="       :: ['a, 'a] => bool                 (infixl "\\<noteq>" 50)
   2.154 -  "_Eps"        :: [pttrn, bool] => 'a              ("(3\\<epsilon>_./ _)" [0, 10] 10)
   2.155 -  "ALL "        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
   2.156 -  "EX "         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
   2.157 -  "EX! "        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
   2.158 -  "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<Rightarrow>/ _)" 10)
   2.159 -(*"@case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ \\<orelse> _")*)
   2.160 +  Not           :: "bool => bool"                        ("\\<not> _" [40] 40)
   2.161 +  "op &"        :: "[bool, bool] => bool"                (infixr "\\<and>" 35)
   2.162 +  "op |"        :: "[bool, bool] => bool"                (infixr "\\<or>" 30)
   2.163 +  "op -->"      :: "[bool, bool] => bool"                (infixr "\\<midarrow>\\<rightarrow>" 25)
   2.164 +  "op o"        :: "['b => 'c, 'a => 'b, 'a] => 'c"      (infixl "\\<circ>" 55)
   2.165 +  "op ~="       :: "['a, 'a] => bool"                    (infixl "\\<noteq>" 50)
   2.166 +  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\\<epsilon>_./ _)" [0, 10] 10)
   2.167 +  "ALL "        :: "[idts, bool] => bool"                ("(3\\<forall>_./ _)" [0, 10] 10)
   2.168 +  "EX "         :: "[idts, bool] => bool"                ("(3\\<exists>_./ _)" [0, 10] 10)
   2.169 +  "EX! "        :: "[idts, bool] => bool"                ("(3\\<exists>!_./ _)" [0, 10] 10)
   2.170 +  "@case1"      :: "['a, 'b] => case_syn"                ("(2_ \\<Rightarrow>/ _)" 10)
   2.171 +(*"@case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \\<orelse> _")*)
   2.172  
   2.173  syntax (symbols output)
   2.174 -  "op ~="       :: ['a, 'a] => bool                 ("(_ \\<noteq>/ _)" [51, 51] 50)
   2.175 +  "op ~="       :: "['a, 'a] => bool"                    ("(_ \\<noteq>/ _)" [51, 51] 50)
   2.176  
   2.177  syntax (xsymbols)
   2.178 -  "op -->"      :: [bool, bool] => bool             (infixr "\\<longrightarrow>" 25)
   2.179 +  "op -->"      :: "[bool, bool] => bool"                (infixr "\\<longrightarrow>" 25)
   2.180  
   2.181  syntax (HTML output)
   2.182 -  Not           :: bool => bool                     ("\\<not> _" [40] 40)
   2.183 +  Not           :: "bool => bool"                        ("\\<not> _" [40] 40)
   2.184  
   2.185  syntax (HOL)
   2.186 -  "_Eps"        :: [pttrn, bool] => 'a              ("(3@ _./ _)" [0, 10] 10)
   2.187 -  "ALL "        :: [idts, bool] => bool             ("(3! _./ _)" [0, 10] 10)
   2.188 -  "EX "         :: [idts, bool] => bool             ("(3? _./ _)" [0, 10] 10)
   2.189 -  "EX! "        :: [idts, bool] => bool             ("(3?! _./ _)" [0, 10] 10)
   2.190 +  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3@ _./ _)" [0, 10] 10)
   2.191 +  "ALL "        :: "[idts, bool] => bool"                ("(3! _./ _)" [0, 10] 10)
   2.192 +  "EX "         :: "[idts, bool] => bool"                ("(3? _./ _)" [0, 10] 10)
   2.193 +  "EX! "        :: "[idts, bool] => bool"                ("(3?! _./ _)" [0, 10] 10)
   2.194  
   2.195  
   2.196  
   2.197 @@ -145,57 +136,59 @@
   2.198  
   2.199  local
   2.200  
   2.201 -rules
   2.202 +axioms
   2.203  
   2.204 -  eq_reflection "(x=y) ==> (x==y)"
   2.205 +  eq_reflection: "(x=y) ==> (x==y)"
   2.206  
   2.207    (* Basic Rules *)
   2.208  
   2.209 -  refl          "t = (t::'a)"
   2.210 -  subst         "[| s = t; P(s) |] ==> P(t::'a)"
   2.211 +  refl:         "t = (t::'a)"
   2.212 +  subst:        "[| s = t; P(s) |] ==> P(t::'a)"
   2.213  
   2.214    (*Extensionality is built into the meta-logic, and this rule expresses
   2.215      a related property.  It is an eta-expanded version of the traditional
   2.216      rule, and similar to the ABS rule of HOL.*)
   2.217 -  ext           "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
   2.218 +  ext:          "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
   2.219  
   2.220 -  selectI       "P (x::'a) ==> P (@x. P x)"
   2.221 +  selectI:      "P (x::'a) ==> P (@x. P x)"
   2.222  
   2.223 -  impI          "(P ==> Q) ==> P-->Q"
   2.224 -  mp            "[| P-->Q;  P |] ==> Q"
   2.225 +  impI:         "(P ==> Q) ==> P-->Q"
   2.226 +  mp:           "[| P-->Q;  P |] ==> Q"
   2.227  
   2.228  defs
   2.229  
   2.230 -  True_def      "True      == ((%x::bool. x) = (%x. x))"
   2.231 -  All_def       "All(P)    == (P = (%x. True))"
   2.232 -  Ex_def        "Ex(P)     == P(@x. P(x))"
   2.233 -  False_def     "False     == (!P. P)"
   2.234 -  not_def       "~ P       == P-->False"
   2.235 -  and_def       "P & Q     == !R. (P-->Q-->R) --> R"
   2.236 -  or_def        "P | Q     == !R. (P-->R) --> (Q-->R) --> R"
   2.237 -  Ex1_def       "Ex1(P)    == ? x. P(x) & (! y. P(y) --> y=x)"
   2.238 +  True_def:     "True      == ((%x::bool. x) = (%x. x))"
   2.239 +  All_def:      "All(P)    == (P = (%x. True))"
   2.240 +  Ex_def:       "Ex(P)     == P(@x. P(x))"
   2.241 +  False_def:    "False     == (!P. P)"
   2.242 +  not_def:      "~ P       == P-->False"
   2.243 +  and_def:      "P & Q     == !R. (P-->Q-->R) --> R"
   2.244 +  or_def:       "P | Q     == !R. (P-->R) --> (Q-->R) --> R"
   2.245 +  Ex1_def:      "Ex1(P)    == ? x. P(x) & (! y. P(y) --> y=x)"
   2.246  
   2.247 -rules
   2.248 +axioms
   2.249    (* Axioms *)
   2.250  
   2.251 -  iff           "(P-->Q) --> (Q-->P) --> (P=Q)"
   2.252 -  True_or_False "(P=True) | (P=False)"
   2.253 +  iff:          "(P-->Q) --> (Q-->P) --> (P=Q)"
   2.254 +  True_or_False:  "(P=True) | (P=False)"
   2.255  
   2.256  defs
   2.257    (*misc definitions*)
   2.258 -  Let_def       "Let s f == f(s)"
   2.259 -  if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
   2.260 +  Let_def:      "Let s f == f(s)"
   2.261 +  if_def:       "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
   2.262  
   2.263    (*arbitrary is completely unspecified, but is made to appear as a
   2.264      definition syntactically*)
   2.265 -  arbitrary_def "False ==> arbitrary == (@x. False)"
   2.266 +  arbitrary_def:  "False ==> arbitrary == (@x. False)"
   2.267  
   2.268  
   2.269  
   2.270 -(** initial HOL theory setup **)
   2.271 +(* theory and package setup *)
   2.272  
   2.273 -setup Simplifier.setup
   2.274 -setup ClasetThyData.setup
   2.275 +use "HOL_lemmas.ML"	setup attrib_setup
   2.276 +use "cladata.ML"	setup Classical.setup setup clasetup
   2.277 +use "blastdata.ML"	setup Blast.setup
   2.278 +use "simpdata.ML"	setup Simplifier.setup setup simpsetup setup Clasimp.setup
   2.279  
   2.280  
   2.281  end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/HOL_lemmas.ML	Wed Aug 25 20:49:02 1999 +0200
     3.3 @@ -0,0 +1,484 @@
     3.4 +(*  Title:      HOL/HOL_lemmas.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Tobias Nipkow
     3.7 +    Copyright   1991  University of Cambridge
     3.8 +
     3.9 +Derived rules from Appendix of Mike Gordons HOL Report, Cambridge TR 68.
    3.10 +*)
    3.11 +
    3.12 +(* ML bindings *)
    3.13 +
    3.14 +val plusI = thm "plusI";
    3.15 +val minusI = thm "minusI";
    3.16 +val timesI = thm "timesI";
    3.17 +val powerI = thm "powerI";
    3.18 +val eq_reflection = thm "eq_reflection";
    3.19 +val refl = thm "refl";
    3.20 +val subst = thm "subst";
    3.21 +val ext = thm "ext";
    3.22 +val selectI = thm "selectI";
    3.23 +val impI = thm "impI";
    3.24 +val mp = thm "mp";
    3.25 +val True_def = thm "True_def";
    3.26 +val All_def = thm "All_def";
    3.27 +val Ex_def = thm "Ex_def";
    3.28 +val False_def = thm "False_def";
    3.29 +val not_def = thm "not_def";
    3.30 +val and_def = thm "and_def";
    3.31 +val or_def = thm "or_def";
    3.32 +val Ex1_def = thm "Ex1_def";
    3.33 +val iff = thm "iff";
    3.34 +val True_or_False = thm "True_or_False";
    3.35 +val Let_def = thm "Let_def";
    3.36 +val if_def = thm "if_def";
    3.37 +val arbitrary_def = thm "arbitrary_def";
    3.38 +
    3.39 +
    3.40 +(** Equality **)
    3.41 +section "=";
    3.42 +
    3.43 +qed_goal "sym" (the_context ()) "s=t ==> t=s"
    3.44 + (fn prems => [cut_facts_tac prems 1, etac subst 1, rtac refl 1]);
    3.45 +
    3.46 +(*calling "standard" reduces maxidx to 0*)
    3.47 +bind_thm ("ssubst", (sym RS subst));
    3.48 +
    3.49 +qed_goal "trans" (the_context ()) "[| r=s; s=t |] ==> r=t"
    3.50 + (fn prems =>
    3.51 +        [rtac subst 1, resolve_tac prems 1, resolve_tac prems 1]);
    3.52 +
    3.53 +val prems = goal (the_context ()) "(A == B) ==> A = B";
    3.54 +by (rewrite_goals_tac prems);
    3.55 +by (rtac refl 1);
    3.56 +qed "def_imp_eq";
    3.57 +
    3.58 +(*Useful with eresolve_tac for proving equalties from known equalities.
    3.59 +        a = b
    3.60 +        |   |
    3.61 +        c = d   *)
    3.62 +Goal "[| a=b;  a=c;  b=d |] ==> c=d";
    3.63 +by (rtac trans 1);
    3.64 +by (rtac trans 1);
    3.65 +by (rtac sym 1);
    3.66 +by (REPEAT (assume_tac 1)) ;
    3.67 +qed "box_equals";
    3.68 +
    3.69 +
    3.70 +(** Congruence rules for meta-application **)
    3.71 +section "Congruence";
    3.72 +
    3.73 +(*similar to AP_THM in Gordon's HOL*)
    3.74 +qed_goal "fun_cong" (the_context ()) "(f::'a=>'b) = g ==> f(x)=g(x)"
    3.75 +  (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
    3.76 +
    3.77 +(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
    3.78 +qed_goal "arg_cong" (the_context ()) "x=y ==> f(x)=f(y)"
    3.79 + (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
    3.80 +
    3.81 +qed_goal "cong" (the_context ())
    3.82 +   "[| f = g; (x::'a) = y |] ==> f(x) = g(y)"
    3.83 + (fn [prem1,prem2] =>
    3.84 +   [rtac (prem1 RS subst) 1, rtac (prem2 RS subst) 1, rtac refl 1]);
    3.85 +
    3.86 +
    3.87 +(** Equality of booleans -- iff **)
    3.88 +section "iff";
    3.89 +
    3.90 +val prems = Goal
    3.91 +   "[| P ==> Q;  Q ==> P |] ==> P=Q";
    3.92 +by (REPEAT (ares_tac (prems@[impI, iff RS mp RS mp]) 1));
    3.93 +qed "iffI";
    3.94 +
    3.95 +qed_goal "iffD2" (the_context ()) "[| P=Q; Q |] ==> P"
    3.96 + (fn prems =>
    3.97 +        [rtac ssubst 1, resolve_tac prems 1, resolve_tac prems 1]);
    3.98 +
    3.99 +qed_goal "rev_iffD2" (the_context ()) "!!P. [| Q; P=Q |] ==> P"
   3.100 + (fn _ => [etac iffD2 1, assume_tac 1]);
   3.101 +
   3.102 +bind_thm ("iffD1", sym RS iffD2);
   3.103 +bind_thm ("rev_iffD1", sym RSN (2, rev_iffD2));
   3.104 +
   3.105 +qed_goal "iffE" (the_context ())
   3.106 +    "[| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R"
   3.107 + (fn [p1,p2] => [REPEAT(ares_tac([p1 RS iffD2, p1 RS iffD1, p2, impI])1)]);
   3.108 +
   3.109 +
   3.110 +(** True **)
   3.111 +section "True";
   3.112 +
   3.113 +qed_goalw "TrueI" (the_context ()) [True_def] "True"
   3.114 +  (fn _ => [(rtac refl 1)]);
   3.115 +
   3.116 +qed_goal "eqTrueI" (the_context ()) "P ==> P=True" 
   3.117 + (fn prems => [REPEAT(resolve_tac ([iffI,TrueI]@prems) 1)]);
   3.118 +
   3.119 +qed_goal "eqTrueE" (the_context ()) "P=True ==> P" 
   3.120 + (fn prems => [REPEAT(resolve_tac (prems@[TrueI,iffD2]) 1)]);
   3.121 +
   3.122 +
   3.123 +(** Universal quantifier **)
   3.124 +section "!";
   3.125 +
   3.126 +qed_goalw "allI" (the_context ()) [All_def] "(!!x::'a. P(x)) ==> !x. P(x)"
   3.127 + (fn prems => [(resolve_tac (prems RL [eqTrueI RS ext]) 1)]);
   3.128 +
   3.129 +qed_goalw "spec" (the_context ()) [All_def] "! x::'a. P(x) ==> P(x)"
   3.130 + (fn prems => [rtac eqTrueE 1, resolve_tac (prems RL [fun_cong]) 1]);
   3.131 +
   3.132 +val major::prems= goal (the_context ()) "[| !x. P(x);  P(x) ==> R |] ==> R";
   3.133 +by (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ;
   3.134 +qed "allE";
   3.135 +
   3.136 +val prems = goal (the_context ()) 
   3.137 +    "[| ! x. P(x);  [| P(x); ! x. P(x) |] ==> R |] ==> R";
   3.138 +by (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ;
   3.139 +qed "all_dupE";
   3.140 +
   3.141 +
   3.142 +(** False ** Depends upon spec; it is impossible to do propositional logic
   3.143 +             before quantifiers! **)
   3.144 +section "False";
   3.145 +
   3.146 +qed_goalw "FalseE" (the_context ()) [False_def] "False ==> P"
   3.147 + (fn [major] => [rtac (major RS spec) 1]);
   3.148 +
   3.149 +qed_goal "False_neq_True" (the_context ()) "False=True ==> P"
   3.150 + (fn [prem] => [rtac (prem RS eqTrueE RS FalseE) 1]);
   3.151 +
   3.152 +
   3.153 +(** Negation **)
   3.154 +section "~";
   3.155 +
   3.156 +qed_goalw "notI" (the_context ()) [not_def] "(P ==> False) ==> ~P"
   3.157 + (fn prems=> [rtac impI 1, eresolve_tac prems 1]);
   3.158 +
   3.159 +qed_goal "False_not_True" (the_context ()) "False ~= True"
   3.160 +  (fn _ => [rtac notI 1, etac False_neq_True 1]);
   3.161 +
   3.162 +qed_goal "True_not_False" (the_context ()) "True ~= False"
   3.163 +  (fn _ => [rtac notI 1, dtac sym 1, etac False_neq_True 1]);
   3.164 +
   3.165 +qed_goalw "notE" (the_context ()) [not_def] "[| ~P;  P |] ==> R"
   3.166 + (fn prems => [rtac (prems MRS mp RS FalseE) 1]);
   3.167 +
   3.168 +bind_thm ("classical2", notE RS notI);
   3.169 +
   3.170 +qed_goal "rev_notE" (the_context ()) "!!P R. [| P; ~P |] ==> R"
   3.171 + (fn _ => [REPEAT (ares_tac [notE] 1)]);
   3.172 +
   3.173 +
   3.174 +(** Implication **)
   3.175 +section "-->";
   3.176 +
   3.177 +val prems = Goal "[| P-->Q;  P;  Q ==> R |] ==> R";
   3.178 +by (REPEAT (resolve_tac (prems@[mp]) 1));
   3.179 +qed "impE";
   3.180 +
   3.181 +(* Reduces Q to P-->Q, allowing substitution in P. *)
   3.182 +Goal "[| P;  P --> Q |] ==> Q";
   3.183 +by (REPEAT (ares_tac [mp] 1)) ;
   3.184 +qed "rev_mp";
   3.185 +
   3.186 +val [major,minor] = Goal "[| ~Q;  P==>Q |] ==> ~P";
   3.187 +by (rtac (major RS notE RS notI) 1);
   3.188 +by (etac minor 1) ;
   3.189 +qed "contrapos";
   3.190 +
   3.191 +val [major,minor] = Goal "[| P==>Q; ~Q |] ==> ~P";
   3.192 +by (rtac (minor RS contrapos) 1);
   3.193 +by (etac major 1) ;
   3.194 +qed "rev_contrapos";
   3.195 +
   3.196 +(* ~(?t = ?s) ==> ~(?s = ?t) *)
   3.197 +bind_thm("not_sym", sym COMP rev_contrapos);
   3.198 +
   3.199 +
   3.200 +(** Existential quantifier **)
   3.201 +section "?";
   3.202 +
   3.203 +qed_goalw "exI" (the_context ()) [Ex_def] "P x ==> ? x::'a. P x"
   3.204 + (fn prems => [rtac selectI 1, resolve_tac prems 1]);
   3.205 +
   3.206 +qed_goalw "exE" (the_context ()) [Ex_def]
   3.207 +  "[| ? x::'a. P(x); !!x. P(x) ==> Q |] ==> Q"
   3.208 +  (fn prems => [REPEAT(resolve_tac prems 1)]);
   3.209 +
   3.210 +
   3.211 +(** Conjunction **)
   3.212 +section "&";
   3.213 +
   3.214 +qed_goalw "conjI" (the_context ()) [and_def] "[| P; Q |] ==> P&Q"
   3.215 + (fn prems =>
   3.216 +  [REPEAT (resolve_tac (prems@[allI,impI]) 1 ORELSE etac (mp RS mp) 1)]);
   3.217 +
   3.218 +qed_goalw "conjunct1" (the_context ()) [and_def] "[| P & Q |] ==> P"
   3.219 + (fn prems =>
   3.220 +   [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
   3.221 +
   3.222 +qed_goalw "conjunct2" (the_context ()) [and_def] "[| P & Q |] ==> Q"
   3.223 + (fn prems =>
   3.224 +   [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
   3.225 +
   3.226 +qed_goal "conjE" (the_context ()) "[| P&Q;  [| P; Q |] ==> R |] ==> R"
   3.227 + (fn prems =>
   3.228 +         [cut_facts_tac prems 1, resolve_tac prems 1,
   3.229 +          etac conjunct1 1, etac conjunct2 1]);
   3.230 +
   3.231 +qed_goal "context_conjI" (the_context ())  "[| P; P ==> Q |] ==> P & Q"
   3.232 + (fn prems => [REPEAT(resolve_tac (conjI::prems) 1)]);
   3.233 +
   3.234 +
   3.235 +(** Disjunction *)
   3.236 +section "|";
   3.237 +
   3.238 +qed_goalw "disjI1" (the_context ()) [or_def] "P ==> P|Q"
   3.239 + (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
   3.240 +
   3.241 +qed_goalw "disjI2" (the_context ()) [or_def] "Q ==> P|Q"
   3.242 + (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
   3.243 +
   3.244 +qed_goalw "disjE" (the_context ()) [or_def] "[| P | Q; P ==> R; Q ==> R |] ==> R"
   3.245 + (fn [a1,a2,a3] =>
   3.246 +        [rtac (mp RS mp) 1, rtac spec 1, rtac a1 1,
   3.247 +         rtac (a2 RS impI) 1, assume_tac 1, rtac (a3 RS impI) 1, assume_tac 1]);
   3.248 +
   3.249 +
   3.250 +(** CCONTR -- classical logic **)
   3.251 +section "classical logic";
   3.252 +
   3.253 +qed_goalw "classical" (the_context ()) [not_def]  "(~P ==> P) ==> P"
   3.254 + (fn [prem] =>
   3.255 +   [rtac (True_or_False RS (disjE RS eqTrueE)) 1,  assume_tac 1,
   3.256 +    rtac (impI RS prem RS eqTrueI) 1,
   3.257 +    etac subst 1,  assume_tac 1]);
   3.258 +
   3.259 +val ccontr = FalseE RS classical;
   3.260 +
   3.261 +(*Double negation law*)
   3.262 +Goal "~~P ==> P";
   3.263 +by (rtac classical 1);
   3.264 +by (etac notE 1);
   3.265 +by (assume_tac 1);
   3.266 +qed "notnotD";
   3.267 +
   3.268 +val [p1,p2] = Goal "[| Q; ~ P ==> ~ Q |] ==> P";
   3.269 +by (rtac classical 1);
   3.270 +by (dtac p2 1);
   3.271 +by (etac notE 1);
   3.272 +by (rtac p1 1);
   3.273 +qed "contrapos2";
   3.274 +
   3.275 +val [p1,p2] = Goal "[| P;  Q ==> ~ P |] ==> ~ Q";
   3.276 +by (rtac notI 1);
   3.277 +by (dtac p2 1);
   3.278 +by (etac notE 1);
   3.279 +by (rtac p1 1);
   3.280 +qed "swap2";
   3.281 +
   3.282 +(** Unique existence **)
   3.283 +section "?!";
   3.284 +
   3.285 +qed_goalw "ex1I" (the_context ()) [Ex1_def]
   3.286 +            "[| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
   3.287 + (fn prems =>
   3.288 +  [REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]);
   3.289 +
   3.290 +(*Sometimes easier to use: the premises have no shared variables.  Safe!*)
   3.291 +val [ex,eq] = Goal
   3.292 +    "[| ? x. P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> ?! x. P(x)";
   3.293 +by (rtac (ex RS exE) 1);
   3.294 +by (REPEAT (ares_tac [ex1I,eq] 1)) ;
   3.295 +qed "ex_ex1I";
   3.296 +
   3.297 +qed_goalw "ex1E" (the_context ()) [Ex1_def]
   3.298 +    "[| ?! x. P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R |] ==> R"
   3.299 + (fn major::prems =>
   3.300 +  [rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);
   3.301 +
   3.302 +Goal "?! x. P x ==> ? x. P x";
   3.303 +by (etac ex1E 1);
   3.304 +by (rtac exI 1);
   3.305 +by (assume_tac 1);
   3.306 +qed "ex1_implies_ex";
   3.307 +
   3.308 +
   3.309 +(** Select: Hilbert's Epsilon-operator **)
   3.310 +section "@";
   3.311 +
   3.312 +(*Easier to apply than selectI: conclusion has only one occurrence of P*)
   3.313 +val prems = Goal
   3.314 +    "[| P a;  !!x. P x ==> Q x |] ==> Q (@x. P x)";
   3.315 +by (resolve_tac prems 1);
   3.316 +by (rtac selectI 1);
   3.317 +by (resolve_tac prems 1) ;
   3.318 +qed "selectI2";
   3.319 +
   3.320 +(*Easier to apply than selectI2 if witness ?a comes from an EX-formula*)
   3.321 +qed_goal "selectI2EX" (the_context ())
   3.322 +  "[| ? a. P a; !!x. P x ==> Q x |] ==> Q (Eps P)"
   3.323 +(fn [major,minor] => [rtac (major RS exE) 1, etac selectI2 1, etac minor 1]);
   3.324 +
   3.325 +val prems = Goal
   3.326 +    "[| P a;  !!x. P x ==> x=a |] ==> (@x. P x) = a";
   3.327 +by (rtac selectI2 1);
   3.328 +by (REPEAT (ares_tac prems 1)) ;
   3.329 +qed "select_equality";
   3.330 +
   3.331 +Goalw [Ex1_def] "[| ?!x. P x; P a |] ==> (@x. P x) = a";
   3.332 +by (rtac select_equality 1);
   3.333 +by (atac 1);
   3.334 +by (etac exE 1);
   3.335 +by (etac conjE 1);
   3.336 +by (rtac allE 1);
   3.337 +by (atac 1);
   3.338 +by (etac impE 1);
   3.339 +by (atac 1);
   3.340 +by (etac ssubst 1);
   3.341 +by (etac allE 1);
   3.342 +by (etac mp 1);
   3.343 +by (atac 1);
   3.344 +qed "select1_equality";
   3.345 +
   3.346 +Goal "P (@ x. P x) =  (? x. P x)";
   3.347 +by (rtac iffI 1);
   3.348 +by (etac exI 1);
   3.349 +by (etac exE 1);
   3.350 +by (etac selectI 1);
   3.351 +qed "select_eq_Ex";
   3.352 +
   3.353 +Goal "(@y. y=x) = x";
   3.354 +by (rtac select_equality 1);
   3.355 +by (rtac refl 1);
   3.356 +by (atac 1);
   3.357 +qed "Eps_eq";
   3.358 +
   3.359 +Goal "(Eps (op = x)) = x";
   3.360 +by (rtac select_equality 1);
   3.361 +by (rtac refl 1);
   3.362 +by (etac sym 1);
   3.363 +qed "Eps_sym_eq";
   3.364 +
   3.365 +(** Classical intro rules for disjunction and existential quantifiers *)
   3.366 +section "classical intro rules";
   3.367 +
   3.368 +val prems= Goal "(~Q ==> P) ==> P|Q";
   3.369 +by (rtac classical 1);
   3.370 +by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));
   3.371 +by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ;
   3.372 +qed "disjCI";
   3.373 +
   3.374 +Goal "~P | P";
   3.375 +by (REPEAT (ares_tac [disjCI] 1)) ;
   3.376 +qed "excluded_middle";
   3.377 +
   3.378 +(*For disjunctive case analysis*)
   3.379 +fun excluded_middle_tac sP =
   3.380 +    res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
   3.381 +
   3.382 +(*Classical implies (-->) elimination. *)
   3.383 +val major::prems = Goal "[| P-->Q; ~P ==> R; Q ==> R |] ==> R";
   3.384 +by (rtac (excluded_middle RS disjE) 1);
   3.385 +by (REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1)));
   3.386 +qed "impCE";
   3.387 +
   3.388 +(*This version of --> elimination works on Q before P.  It works best for
   3.389 +  those cases in which P holds "almost everywhere".  Can't install as
   3.390 +  default: would break old proofs.*)
   3.391 +val major::prems = Goal
   3.392 +    "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R";
   3.393 +by (resolve_tac [excluded_middle RS disjE] 1);
   3.394 +by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ;
   3.395 +qed "impCE'";
   3.396 +
   3.397 +(*Classical <-> elimination. *)
   3.398 +val major::prems = Goal
   3.399 +    "[| P=Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R";
   3.400 +by (rtac (major RS iffE) 1);
   3.401 +by (REPEAT (DEPTH_SOLVE_1 
   3.402 +	    (eresolve_tac ([asm_rl,impCE,notE]@prems) 1)));
   3.403 +qed "iffCE";
   3.404 +
   3.405 +val prems = Goal "(! x. ~P(x) ==> P(a)) ==> ? x. P(x)";
   3.406 +by (rtac ccontr 1);
   3.407 +by (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1))  ;
   3.408 +qed "exCI";
   3.409 +
   3.410 +
   3.411 +(* case distinction *)
   3.412 +
   3.413 +qed_goal "case_split_thm" (the_context ()) "[| P ==> Q; ~P ==> Q |] ==> Q"
   3.414 +  (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1,
   3.415 +                  etac p2 1, etac p1 1]);
   3.416 +
   3.417 +fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
   3.418 +
   3.419 +
   3.420 +(** Standard abbreviations **)
   3.421 +
   3.422 +(*Apply an equality or definition ONCE.
   3.423 +  Fails unless the substitution has an effect*)
   3.424 +fun stac th = 
   3.425 +  let val th' = th RS def_imp_eq handle THM _ => th
   3.426 +  in  CHANGED_GOAL (rtac (th' RS ssubst))
   3.427 +  end;
   3.428 +
   3.429 +fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
   3.430 +
   3.431 +
   3.432 +(** strip ! and --> from proved goal while preserving !-bound var names **)
   3.433 +
   3.434 +local
   3.435 +
   3.436 +(* Use XXX to avoid forall_intr failing because of duplicate variable name *)
   3.437 +val myspec = read_instantiate [("P","?XXX")] spec;
   3.438 +val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec;
   3.439 +val cvx = cterm_of (#sign(rep_thm myspec)) vx;
   3.440 +val aspec = forall_intr cvx myspec;
   3.441 +
   3.442 +in
   3.443 +
   3.444 +fun RSspec th =
   3.445 +  (case concl_of th of
   3.446 +     _ $ (Const("All",_) $ Abs(a,_,_)) =>
   3.447 +         let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),vxT))
   3.448 +         in th RS forall_elim ca aspec end
   3.449 +  | _ => raise THM("RSspec",0,[th]));
   3.450 +
   3.451 +fun RSmp th =
   3.452 +  (case concl_of th of
   3.453 +     _ $ (Const("op -->",_)$_$_) => th RS mp
   3.454 +  | _ => raise THM("RSmp",0,[th]));
   3.455 +
   3.456 +fun normalize_thm funs =
   3.457 +  let fun trans [] th = th
   3.458 +	| trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
   3.459 +  in zero_var_indexes o trans funs end;
   3.460 +
   3.461 +fun qed_spec_mp name =
   3.462 +  let val thm = normalize_thm [RSspec,RSmp] (result())
   3.463 +  in ThmDatabase.ml_store_thm(name, thm) end;
   3.464 +
   3.465 +fun qed_goal_spec_mp name thy s p = 
   3.466 +	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
   3.467 +
   3.468 +fun qed_goalw_spec_mp name thy defs s p = 
   3.469 +	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
   3.470 +
   3.471 +end;
   3.472 +
   3.473 +
   3.474 +(* attributes *)
   3.475 +
   3.476 +local
   3.477 +
   3.478 +fun gen_rulify x =
   3.479 +  Attrib.no_args (Drule.rule_attribute (fn _ => (normalize_thm [RSspec, RSmp]))) x;
   3.480 +
   3.481 +in
   3.482 +
   3.483 +val attrib_setup =
   3.484 + [Attrib.add_attributes
   3.485 +  [("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]];
   3.486 +
   3.487 +end;
     4.1 --- a/src/HOL/Inductive.thy	Wed Aug 25 20:46:40 1999 +0200
     4.2 +++ b/src/HOL/Inductive.thy	Wed Aug 25 20:49:02 1999 +0200
     4.3 @@ -1,5 +1,6 @@
     4.4  
     4.5 -Inductive = Gfp + Prod + Sum +
     4.6 +theory Inductive = Gfp + Prod + Sum
     4.7 +files "Tools/inductive_package.ML":
     4.8  
     4.9  setup InductivePackage.setup
    4.10  
     5.1 --- a/src/HOL/IsaMakefile	Wed Aug 25 20:46:40 1999 +0200
     5.2 +++ b/src/HOL/IsaMakefile	Wed Aug 25 20:49:02 1999 +0200
     5.3 @@ -32,9 +32,9 @@
     5.4  	@cd $(SRC)/Pure; $(ISATOOL) make Pure
     5.5  
     5.6  $(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \
     5.7 -  $(SRC)/Provers/Arith/cancel_sums.ML \
     5.8 -  $(SRC)/Provers/Arith/assoc_fold.ML \
     5.9 -  $(SRC)/Provers/Arith/combine_coeff.ML \
    5.10 +  $(SRC)/Provers/Arith/cancel_sums.ML		\
    5.11 +  $(SRC)/Provers/Arith/assoc_fold.ML		\
    5.12 +  $(SRC)/Provers/Arith/combine_coeff.ML		\
    5.13    $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
    5.14    $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
    5.15    $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
    5.16 @@ -47,24 +47,25 @@
    5.17    $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml Arith.ML Arith.thy \
    5.18    Calculation.thy Datatype.thy Divides.ML Divides.thy Finite.ML \
    5.19    Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \
    5.20 -  Inductive.thy Integ/Bin.ML Integ/Bin.thy Integ/Equiv.ML \
    5.21 -  Integ/Equiv.thy Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML \
    5.22 -  Integ/Int.thy Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML \
    5.23 -  Integ/NatBin.thy Integ/simproc.ML Lfp.ML Lfp.thy List.ML List.thy \
    5.24 -  Main.thy Map.ML Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy \
    5.25 -  Numeral.thy Option.ML Option.thy Ord.ML Ord.thy Power.ML Power.thy \
    5.26 -  Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
    5.27 -  Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy String.thy \
    5.28 -  SVC_Oracle.ML SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML \
    5.29 -  Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
    5.30 -  Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
    5.31 -  Tools/induct_method.ML Tools/inductive_package.ML \
    5.32 -  Tools/numeral_syntax.ML Tools/primrec_package.ML \
    5.33 -  Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.ML \
    5.34 -  Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
    5.35 -  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy cladata.ML \
    5.36 -  equalities.ML equalities.thy hologic.ML mono.ML mono.thy simpdata.ML \
    5.37 -  subset.ML subset.thy thy_syntax.ML
    5.38 +  HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
    5.39 +  Integ/Equiv.ML Integ/Equiv.thy Integ/IntDef.ML Integ/IntDef.thy \
    5.40 +  Integ/Int.ML Integ/Int.thy Integ/IntDiv.ML Integ/IntDiv.thy \
    5.41 +  Integ/NatBin.ML Integ/NatBin.thy Integ/simproc.ML Lfp.ML Lfp.thy \
    5.42 +  List.ML List.thy Main.thy Map.ML Map.thy Nat.ML Nat.thy NatDef.ML \
    5.43 +  NatDef.thy Numeral.thy Option.ML Option.thy Ord.ML Ord.thy Power.ML \
    5.44 +  Power.thy Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML \
    5.45 +  RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \
    5.46 +  String.thy SVC_Oracle.ML SVC_Oracle.thy Sum.ML Sum.thy \
    5.47 +  Tools/datatype_aux.ML Tools/datatype_abs_proofs.ML \
    5.48 +  Tools/datatype_package.ML Tools/datatype_prop.ML \
    5.49 +  Tools/datatype_rep_proofs.ML Tools/induct_method.ML \
    5.50 +  Tools/inductive_package.ML Tools/numeral_syntax.ML \
    5.51 +  Tools/primrec_package.ML Tools/recdef_package.ML \
    5.52 +  Tools/record_package.ML Tools/svc_funcs.ML Tools/typedef_package.ML \
    5.53 +  Trancl.ML Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML \
    5.54 +  WF.thy WF_Rel.ML WF_Rel.thy blastdata.ML cladata.ML equalities.ML \
    5.55 +  equalities.thy hologic.ML mono.ML mono.thy simpdata.ML subset.ML \
    5.56 +  subset.thy thy_syntax.ML
    5.57  	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
    5.58  
    5.59  
     6.1 --- a/src/HOL/Ord.thy	Wed Aug 25 20:46:40 1999 +0200
     6.2 +++ b/src/HOL/Ord.thy	Wed Aug 25 20:49:02 1999 +0200
     6.3 @@ -8,13 +8,6 @@
     6.4  
     6.5  Ord = HOL +
     6.6  
     6.7 -(*FIXME move to HOL.thy*)
     6.8 -setup hol_setup
     6.9 -setup Classical.setup
    6.10 -setup Blast.setup
    6.11 -setup Clasimp.setup
    6.12 -setup simpdata_setup
    6.13 -
    6.14  
    6.15  axclass
    6.16    ord < term
     7.1 --- a/src/HOL/ROOT.ML	Wed Aug 25 20:46:40 1999 +0200
     7.2 +++ b/src/HOL/ROOT.ML	Wed Aug 25 20:49:02 1999 +0200
     7.3 @@ -15,6 +15,7 @@
     7.4  (*old-style theory syntax*)
     7.5  use "~~/src/Pure/section_utils.ML";
     7.6  use "thy_syntax.ML";
     7.7 +use "hologic.ML";
     7.8  
     7.9  use "~~/src/Provers/simplifier.ML";
    7.10  use "~~/src/Provers/split_paired_all.ML";
    7.11 @@ -29,24 +30,14 @@
    7.12  use "~~/src/Provers/Arith/abel_cancel.ML";
    7.13  use "~~/src/Provers/Arith/assoc_fold.ML";
    7.14  use "~~/src/Provers/quantifier1.ML";
    7.15 +use "~~/src/Provers/Arith/combine_coeff.ML";
    7.16  
    7.17 -use_thy "HOL";
    7.18 -use "hologic.ML";
    7.19 -use "~~/src/Provers/Arith/combine_coeff.ML";
    7.20 -use "cladata.ML";
    7.21 -use "simpdata.ML";
    7.22 -
    7.23 -use_thy "Ord";
    7.24  use_thy "subset";
    7.25  use "Tools/typedef_package.ML";
    7.26 -use_thy "Sum";
    7.27 -use_thy "Gfp";
    7.28  
    7.29 +use_thy "Inductive";
    7.30  use_thy "NatDef";
    7.31  
    7.32 -use "Tools/inductive_package.ML";
    7.33 -use_thy "Inductive";
    7.34 -
    7.35  use "Tools/datatype_aux.ML";
    7.36  use "Tools/datatype_prop.ML";
    7.37  use "Tools/datatype_rep_proofs.ML";
    7.38 @@ -54,20 +45,13 @@
    7.39  use "Tools/datatype_package.ML";
    7.40  use "Tools/primrec_package.ML";
    7.41  use_thy "Datatype";
    7.42 -use_thy "Numeral";
    7.43 -
    7.44 -use "Tools/record_package.ML";
    7.45 -use_thy "Record";
    7.46  
    7.47  (*TFL: recursive function definitions*)
    7.48  use_thy "WF_Rel";
    7.49 -cd "../TFL";
    7.50 -use "sys.sml";
    7.51 -cd "../HOL";
    7.52 -use "Tools/recdef_package.ML";
    7.53 -use "Tools/induct_method.ML";
    7.54 +cd "../TFL"; use "sys.sml"; cd "../HOL";
    7.55  use_thy "Recdef";
    7.56  
    7.57 +use_thy "Numeral";
    7.58  cd "Integ";
    7.59  use_thy "IntDef";
    7.60  use "simproc.ML";
     8.1 --- a/src/HOL/Recdef.thy	Wed Aug 25 20:46:40 1999 +0200
     8.2 +++ b/src/HOL/Recdef.thy	Wed Aug 25 20:49:02 1999 +0200
     8.3 @@ -1,5 +1,6 @@
     8.4  
     8.5 -Recdef = WF_Rel +
     8.6 +theory Recdef = WF_Rel
     8.7 +files "Tools/recdef_package.ML" "Tools/induct_method.ML":
     8.8  
     8.9  setup RecdefPackage.setup
    8.10  setup InductMethod.setup
     9.1 --- a/src/HOL/Record.thy	Wed Aug 25 20:46:40 1999 +0200
     9.2 +++ b/src/HOL/Record.thy	Wed Aug 25 20:49:02 1999 +0200
     9.3 @@ -6,7 +6,8 @@
     9.4  Tools/record_package.ML for the actual implementation.
     9.5  *)
     9.6  
     9.7 -Record = Datatype +
     9.8 +theory Record = Datatype
     9.9 +files "Tools/record_package.ML":
    9.10  
    9.11  
    9.12  (* concrete syntax *)
    9.13 @@ -42,8 +43,9 @@
    9.14  
    9.15  (* type class for record extensions *)
    9.16  
    9.17 -axclass more < term
    9.18 +axclass more < "term"
    9.19  instance unit :: more
    9.20 +  by intro_classes
    9.21  
    9.22  
    9.23  (* initialize the package *)
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/blastdata.ML	Wed Aug 25 20:49:02 1999 +0200
    10.3 @@ -0,0 +1,34 @@
    10.4 +
    10.5 +(*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
    10.6 +val major::prems = goal (the_context ())
    10.7 +    "[| ?! x. P(x);                                              \
    10.8 +\       !!x. [| P(x);  ALL y y'. P(y) & P(y') --> y=y' |] ==> R  \
    10.9 +\    |] ==> R";
   10.10 +by (rtac (major RS ex1E) 1);
   10.11 +by (REPEAT (ares_tac (allI::prems) 1));
   10.12 +by (etac (dup_elim allE) 1);
   10.13 +by (Fast_tac 1);
   10.14 +qed "alt_ex1E";
   10.15 +
   10.16 +AddSEs [alt_ex1E];
   10.17 +
   10.18 +(*** Applying BlastFun to create Blast_tac ***)
   10.19 +structure Blast_Data = 
   10.20 +  struct
   10.21 +  type claset	= Classical.claset
   10.22 +  val notE	= notE
   10.23 +  val ccontr	= ccontr
   10.24 +  val contr_tac = Classical.contr_tac
   10.25 +  val dup_intr	= Classical.dup_intr
   10.26 +  val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
   10.27 +  val claset	= Classical.claset
   10.28 +  val rep_cs    = Classical.rep_cs
   10.29 +  val cla_modifiers = Classical.cla_modifiers;
   10.30 +  val cla_meth' = Classical.cla_meth'
   10.31 +  end;
   10.32 +
   10.33 +structure Blast = BlastFun(Blast_Data);
   10.34 +Blast.overloaded ("op =", domain_type);	(*overloading of equality as iff*)
   10.35 +
   10.36 +val Blast_tac = Blast.Blast_tac
   10.37 +and blast_tac = Blast.blast_tac;
    11.1 --- a/src/HOL/cladata.ML	Wed Aug 25 20:46:40 1999 +0200
    11.2 +++ b/src/HOL/cladata.ML	Wed Aug 25 20:49:02 1999 +0200
    11.3 @@ -22,7 +22,7 @@
    11.4    val rev_mp = rev_mp
    11.5    val subst = subst
    11.6    val sym = sym
    11.7 -  val thin_refl = prove_goal HOL.thy 
    11.8 +  val thin_refl = prove_goal (the_context ())
    11.9  		  "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
   11.10    end;
   11.11  
   11.12 @@ -40,7 +40,8 @@
   11.13    end;
   11.14  
   11.15  structure Classical = ClassicalFun(Classical_Data);
   11.16 -open Classical;
   11.17 +structure BasicClassical: BASIC_CLASSICAL = Classical;
   11.18 +open BasicClassical;
   11.19  
   11.20  (*Propositional rules*)
   11.21  val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
   11.22 @@ -50,38 +51,4 @@
   11.23  val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, select_equality] 
   11.24                       addSEs [exE] addEs [allE];
   11.25  
   11.26 -claset_ref() := HOL_cs;
   11.27 -
   11.28 -(*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
   11.29 -val major::prems = goal thy
   11.30 -    "[| ?! x. P(x);                                              \
   11.31 -\       !!x. [| P(x);  ALL y y'. P(y) & P(y') --> y=y' |] ==> R  \
   11.32 -\    |] ==> R";
   11.33 -by (rtac (major RS ex1E) 1);
   11.34 -by (REPEAT (ares_tac (allI::prems) 1));
   11.35 -by (etac (dup_elim allE) 1);
   11.36 -by (Fast_tac 1);
   11.37 -qed "alt_ex1E";
   11.38 -
   11.39 -AddSEs [alt_ex1E];
   11.40 -
   11.41 -(*** Applying BlastFun to create Blast_tac ***)
   11.42 -structure Blast_Data = 
   11.43 -  struct
   11.44 -  type claset	= Classical.claset
   11.45 -  val notE	= notE
   11.46 -  val ccontr	= ccontr
   11.47 -  val contr_tac = Classical.contr_tac
   11.48 -  val dup_intr	= Classical.dup_intr
   11.49 -  val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
   11.50 -  val claset	= Classical.claset
   11.51 -  val rep_cs    = Classical.rep_cs
   11.52 -  val cla_modifiers = Classical.cla_modifiers;
   11.53 -  val cla_meth' = Classical.cla_meth'
   11.54 -  end;
   11.55 -
   11.56 -structure Blast = BlastFun(Blast_Data);
   11.57 -Blast.overloaded ("op =", domain_type);	(*overloading of equality as iff*)
   11.58 -
   11.59 -val Blast_tac = Blast.Blast_tac
   11.60 -and blast_tac = Blast.blast_tac;
   11.61 +val clasetup = [fn thy => (claset_ref_of thy := HOL_cs; thy)];
    12.1 --- a/src/HOL/simpdata.ML	Wed Aug 25 20:46:40 1999 +0200
    12.2 +++ b/src/HOL/simpdata.ML	Wed Aug 25 20:49:02 1999 +0200
    12.3 @@ -89,14 +89,14 @@
    12.4  end;
    12.5  
    12.6  
    12.7 -val [prem] = goal HOL.thy "x==y ==> x=y";
    12.8 +val [prem] = goal (the_context ()) "x==y ==> x=y";
    12.9  by (rewtac prem);
   12.10  by (rtac refl 1);
   12.11  qed "meta_eq_to_obj_eq";
   12.12  
   12.13  local
   12.14  
   12.15 -  fun prover s = prove_goal HOL.thy s (fn _ => [(Blast_tac 1)]);
   12.16 +  fun prover s = prove_goal (the_context ()) s (fn _ => [(Blast_tac 1)]);
   12.17  
   12.18  in
   12.19  
   12.20 @@ -157,7 +157,7 @@
   12.21  
   12.22  
   12.23  val imp_cong = impI RSN
   12.24 -    (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
   12.25 +    (2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
   12.26          (fn _=> [(Blast_tac 1)]) RS mp RS mp);
   12.27  
   12.28  (*Miniscoping: pushing in existential quantifiers*)
   12.29 @@ -182,10 +182,10 @@
   12.30  (* elimination of existential quantifiers in assumptions *)
   12.31  
   12.32  val ex_all_equiv =
   12.33 -  let val lemma1 = prove_goal HOL.thy
   12.34 +  let val lemma1 = prove_goal (the_context ())
   12.35          "(? x. P(x) ==> PROP Q) ==> (!!x. P(x) ==> PROP Q)"
   12.36          (fn prems => [resolve_tac prems 1, etac exI 1]);
   12.37 -      val lemma2 = prove_goalw HOL.thy [Ex_def]
   12.38 +      val lemma2 = prove_goalw (the_context ()) [Ex_def]
   12.39          "(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)"
   12.40          (fn prems => [(REPEAT(resolve_tac prems 1))])
   12.41    in equal_intr lemma1 lemma2 end;
   12.42 @@ -194,13 +194,13 @@
   12.43  
   12.44  (* Elimination of True from asumptions: *)
   12.45  
   12.46 -val True_implies_equals = prove_goal HOL.thy
   12.47 +val True_implies_equals = prove_goal (the_context ())
   12.48   "(True ==> PROP P) == PROP P"
   12.49  (fn _ => [rtac equal_intr_rule 1, atac 2,
   12.50            METAHYPS (fn prems => resolve_tac prems 1) 1,
   12.51            rtac TrueI 1]);
   12.52  
   12.53 -fun prove nm thm  = qed_goal nm HOL.thy thm (fn _ => [(Blast_tac 1)]);
   12.54 +fun prove nm thm  = qed_goal nm (the_context ()) thm (fn _ => [(Blast_tac 1)]);
   12.55  
   12.56  prove "conj_commute" "(P&Q) = (Q&P)";
   12.57  prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))";
   12.58 @@ -255,19 +255,19 @@
   12.59  (* '&' congruence rule: not included by default!
   12.60     May slow rewrite proofs down by as much as 50% *)
   12.61  
   12.62 -let val th = prove_goal HOL.thy 
   12.63 +let val th = prove_goal (the_context ()) 
   12.64                  "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"
   12.65                  (fn _=> [(Blast_tac 1)])
   12.66  in  bind_thm("conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
   12.67  
   12.68 -let val th = prove_goal HOL.thy 
   12.69 +let val th = prove_goal (the_context ()) 
   12.70                  "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))"
   12.71                  (fn _=> [(Blast_tac 1)])
   12.72  in  bind_thm("rev_conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
   12.73  
   12.74  (* '|' congruence rule: not included by default! *)
   12.75  
   12.76 -let val th = prove_goal HOL.thy 
   12.77 +let val th = prove_goal (the_context ()) 
   12.78                  "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))"
   12.79                  (fn _=> [(Blast_tac 1)])
   12.80  in  bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
   12.81 @@ -358,10 +358,10 @@
   12.82  
   12.83  local
   12.84  val ex_pattern =
   12.85 -  Thm.read_cterm (Theory.sign_of HOL.thy) ("EX x. P(x) & Q(x)",HOLogic.boolT)
   12.86 +  Thm.read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x) & Q(x)",HOLogic.boolT)
   12.87  
   12.88  val all_pattern =
   12.89 -  Thm.read_cterm (Theory.sign_of HOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
   12.90 +  Thm.read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
   12.91  
   12.92  in
   12.93  val defEX_regroup =
   12.94 @@ -478,7 +478,7 @@
   12.95  
   12.96  
   12.97  (*For expand_case_tac*)
   12.98 -val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
   12.99 +val prems = goal (the_context ()) "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
  12.100  by (case_tac "P" 1);
  12.101  by (ALLGOALS (asm_simp_tac (HOL_ss addsimps prems)));
  12.102  val expand_case = result();
  12.103 @@ -491,9 +491,8 @@
  12.104      Simp_tac i;
  12.105  
  12.106  
  12.107 -(* install implicit simpset *)
  12.108 -
  12.109 -simpset_ref() := HOL_ss addcongs [if_weak_cong];
  12.110 +(* default simpset *)
  12.111 +val simpsetup = [fn thy => (simpset_ref_of thy := HOL_ss addcongs [if_weak_cong]; thy)];
  12.112  
  12.113  
  12.114  (*** integration of simplifier with classical reasoner ***)