1.1 --- a/src/Pure/thm.ML Thu Jun 03 22:54:33 2010 +0200
1.2 +++ b/src/Pure/thm.ML Thu Jun 03 23:17:57 2010 +0200
1.3 @@ -156,9 +156,6 @@
1.4 structure Thm: THM =
1.5 struct
1.6
1.7 -structure Pt = Proofterm;
1.8 -
1.9 -
1.10 (*** Certified terms and types ***)
1.11
1.12 (** certified types **)
1.13 @@ -349,7 +346,7 @@
1.14 prop: term} (*conclusion*)
1.15 and deriv = Deriv of
1.16 {promises: (serial * thm future) OrdList.T,
1.17 - body: Pt.proof_body}
1.18 + body: Proofterm.proof_body}
1.19 with
1.20
1.21 type conv = cterm -> thm;
1.22 @@ -486,7 +483,7 @@
1.23 fun make_deriv promises oracles thms proof =
1.24 Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}};
1.25
1.26 -val empty_deriv = make_deriv [] [] [] Pt.MinProof;
1.27 +val empty_deriv = make_deriv [] [] [] Proofterm.MinProof;
1.28
1.29
1.30 (* inference rules *)
1.31 @@ -498,10 +495,10 @@
1.32 (Deriv {promises = ps2, body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) =
1.33 let
1.34 val ps = OrdList.union promise_ord ps1 ps2;
1.35 - val oras = Pt.merge_oracles oras1 oras2;
1.36 - val thms = Pt.merge_thms thms1 thms2;
1.37 + val oras = Proofterm.merge_oracles oras1 oras2;
1.38 + val thms = Proofterm.merge_thms thms1 thms2;
1.39 val prf =
1.40 - (case ! Pt.proofs of
1.41 + (case ! Proofterm.proofs of
1.42 2 => f prf1 prf2
1.43 | 1 => MinProof
1.44 | 0 => MinProof
1.45 @@ -520,14 +517,14 @@
1.46 fun raw_body (Thm (Deriv {body, ...}, _)) = body;
1.47
1.48 fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
1.49 - Pt.fulfill_norm_proof (Theory.deref thy_ref)
1.50 + Proofterm.fulfill_norm_proof (Theory.deref thy_ref)
1.51 (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
1.52 and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));
1.53
1.54 -val join_proofs = Pt.join_bodies o map fulfill_body;
1.55 +val join_proofs = Proofterm.join_bodies o map fulfill_body;
1.56
1.57 -fun proof_body_of thm = (Pt.join_bodies [raw_body thm]; fulfill_body thm);
1.58 -val proof_of = Pt.proof_of o proof_body_of;
1.59 +fun proof_body_of thm = (Proofterm.join_bodies [raw_body thm]; fulfill_body thm);
1.60 +val proof_of = Proofterm.proof_of o proof_body_of;
1.61
1.62
1.63 (* derivation status *)
1.64 @@ -537,7 +534,7 @@
1.65 val ps = map (Future.peek o snd) promises;
1.66 val bodies = body ::
1.67 map_filter (fn SOME (Exn.Result th) => SOME (raw_body th) | _ => NONE) ps;
1.68 - val {oracle, unfinished, failed} = Pt.status_of bodies;
1.69 + val {oracle, unfinished, failed} = Proofterm.status_of bodies;
1.70 in
1.71 {oracle = oracle,
1.72 unfinished = unfinished orelse exists is_none ps,
1.73 @@ -571,7 +568,7 @@
1.74 val i = serial ();
1.75 val future = future_thm |> Future.map (future_result i thy sorts prop);
1.76 in
1.77 - Thm (make_deriv [(i, future)] [] [] (Pt.promise_proof thy i prop),
1.78 + Thm (make_deriv [(i, future)] [] [] (Proofterm.promise_proof thy i prop),
1.79 {thy_ref = thy_ref,
1.80 tags = [],
1.81 maxidx = maxidx,
1.82 @@ -585,7 +582,7 @@
1.83 (* closed derivations with official name *)
1.84
1.85 fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
1.86 - Pt.get_name shyps hyps prop (Pt.proof_of body);
1.87 + Proofterm.get_name shyps hyps prop (Proofterm.proof_of body);
1.88
1.89 fun name_derivation name (thm as Thm (der, args)) =
1.90 let
1.91 @@ -595,7 +592,7 @@
1.92
1.93 val ps = map (apsnd (Future.map proof_body_of)) promises;
1.94 val thy = Theory.deref thy_ref;
1.95 - val (pthm, proof) = Pt.thm_proof thy name shyps hyps prop ps body;
1.96 + val (pthm, proof) = Proofterm.thm_proof thy name shyps hyps prop ps body;
1.97 val der' = make_deriv [] [] [pthm] proof;
1.98 val _ = Theory.check_thy thy;
1.99 in Thm (der', args) end;
1.100 @@ -610,7 +607,7 @@
1.101 Symtab.lookup (Theory.axiom_table thy) name
1.102 |> Option.map (fn prop =>
1.103 let
1.104 - val der = deriv_rule0 (Pt.axm_proof name prop);
1.105 + val der = deriv_rule0 (Proofterm.axm_proof name prop);
1.106 val maxidx = maxidx_of_term prop;
1.107 val shyps = Sorts.insert_term prop [];
1.108 in
1.109 @@ -640,7 +637,7 @@
1.110 fun norm_proof (Thm (der, args as {thy_ref, ...})) =
1.111 let
1.112 val thy = Theory.deref thy_ref;
1.113 - val der' = deriv_rule1 (Pt.rew_proof thy) der;
1.114 + val der' = deriv_rule1 (Proofterm.rew_proof thy) der;
1.115 val _ = Theory.check_thy thy;
1.116 in Thm (der', args) end;
1.117
1.118 @@ -666,7 +663,7 @@
1.119 raise THM ("assume: prop", 0, [])
1.120 else if maxidx <> ~1 then
1.121 raise THM ("assume: variables", maxidx, [])
1.122 - else Thm (deriv_rule0 (Pt.Hyp prop),
1.123 + else Thm (deriv_rule0 (Proofterm.Hyp prop),
1.124 {thy_ref = thy_ref,
1.125 tags = [],
1.126 maxidx = ~1,
1.127 @@ -689,7 +686,7 @@
1.128 if T <> propT then
1.129 raise THM ("implies_intr: assumptions must have type prop", 0, [th])
1.130 else
1.131 - Thm (deriv_rule1 (Pt.implies_intr_proof A) der,
1.132 + Thm (deriv_rule1 (Proofterm.implies_intr_proof A) der,
1.133 {thy_ref = merge_thys1 ct th,
1.134 tags = [],
1.135 maxidx = Int.max (maxidxA, maxidx),
1.136 @@ -714,7 +711,7 @@
1.137 case prop of
1.138 Const ("==>", _) $ A $ B =>
1.139 if A aconv propA then
1.140 - Thm (deriv_rule2 (curry Pt.%%) der derA,
1.141 + Thm (deriv_rule2 (curry Proofterm.%%) der derA,
1.142 {thy_ref = merge_thys2 thAB thA,
1.143 tags = [],
1.144 maxidx = Int.max (maxA, maxidx),
1.145 @@ -738,7 +735,7 @@
1.146 (th as Thm (der, {maxidx, shyps, hyps, tpairs, prop, ...})) =
1.147 let
1.148 fun result a =
1.149 - Thm (deriv_rule1 (Pt.forall_intr_proof x a) der,
1.150 + Thm (deriv_rule1 (Proofterm.forall_intr_proof x a) der,
1.151 {thy_ref = merge_thys1 ct th,
1.152 tags = [],
1.153 maxidx = maxidx,
1.154 @@ -770,7 +767,7 @@
1.155 if T <> qary then
1.156 raise THM ("forall_elim: type mismatch", 0, [th])
1.157 else
1.158 - Thm (deriv_rule1 (Pt.% o rpair (SOME t)) der,
1.159 + Thm (deriv_rule1 (Proofterm.% o rpair (SOME t)) der,
1.160 {thy_ref = merge_thys1 ct th,
1.161 tags = [],
1.162 maxidx = Int.max (maxidx, maxt),
1.163 @@ -787,7 +784,7 @@
1.164 t == t
1.165 *)
1.166 fun reflexive (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
1.167 - Thm (deriv_rule0 Pt.reflexive,
1.168 + Thm (deriv_rule0 Proofterm.reflexive,
1.169 {thy_ref = thy_ref,
1.170 tags = [],
1.171 maxidx = maxidx,
1.172 @@ -804,7 +801,7 @@
1.173 fun symmetric (th as Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
1.174 (case prop of
1.175 (eq as Const ("==", _)) $ t $ u =>
1.176 - Thm (deriv_rule1 Pt.symmetric der,
1.177 + Thm (deriv_rule1 Proofterm.symmetric der,
1.178 {thy_ref = thy_ref,
1.179 tags = [],
1.180 maxidx = maxidx,
1.181 @@ -831,7 +828,7 @@
1.182 ((eq as Const ("==", Type (_, [T, _]))) $ t1 $ u, Const ("==", _) $ u' $ t2) =>
1.183 if not (u aconv u') then err "middle term"
1.184 else
1.185 - Thm (deriv_rule2 (Pt.transitive u T) der1 der2,
1.186 + Thm (deriv_rule2 (Proofterm.transitive u T) der1 der2,
1.187 {thy_ref = merge_thys2 th1 th2,
1.188 tags = [],
1.189 maxidx = Int.max (max1, max2),
1.190 @@ -853,7 +850,7 @@
1.191 (case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt)
1.192 | _ => raise THM ("beta_conversion: not a redex", 0, []));
1.193 in
1.194 - Thm (deriv_rule0 Pt.reflexive,
1.195 + Thm (deriv_rule0 Proofterm.reflexive,
1.196 {thy_ref = thy_ref,
1.197 tags = [],
1.198 maxidx = maxidx,
1.199 @@ -864,7 +861,7 @@
1.200 end;
1.201
1.202 fun eta_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
1.203 - Thm (deriv_rule0 Pt.reflexive,
1.204 + Thm (deriv_rule0 Proofterm.reflexive,
1.205 {thy_ref = thy_ref,
1.206 tags = [],
1.207 maxidx = maxidx,
1.208 @@ -874,7 +871,7 @@
1.209 prop = Logic.mk_equals (t, Envir.eta_contract t)});
1.210
1.211 fun eta_long_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
1.212 - Thm (deriv_rule0 Pt.reflexive,
1.213 + Thm (deriv_rule0 Proofterm.reflexive,
1.214 {thy_ref = thy_ref,
1.215 tags = [],
1.216 maxidx = maxidx,
1.217 @@ -896,7 +893,7 @@
1.218 val (t, u) = Logic.dest_equals prop
1.219 handle TERM _ => raise THM ("abstract_rule: premise not an equality", 0, [th]);
1.220 val result =
1.221 - Thm (deriv_rule1 (Pt.abstract_rule x a) der,
1.222 + Thm (deriv_rule1 (Proofterm.abstract_rule x a) der,
1.223 {thy_ref = thy_ref,
1.224 tags = [],
1.225 maxidx = maxidx,
1.226 @@ -939,7 +936,7 @@
1.227 (Const ("==", Type ("fun", [fT, _])) $ f $ g,
1.228 Const ("==", Type ("fun", [tT, _])) $ t $ u) =>
1.229 (chktypes fT tT;
1.230 - Thm (deriv_rule2 (Pt.combination f g t u fT) der1 der2,
1.231 + Thm (deriv_rule2 (Proofterm.combination f g t u fT) der1 der2,
1.232 {thy_ref = merge_thys2 th1 th2,
1.233 tags = [],
1.234 maxidx = Int.max (max1, max2),
1.235 @@ -966,7 +963,7 @@
1.236 case (prop1, prop2) of
1.237 (Const("==>", _) $ A $ B, Const("==>", _) $ B' $ A') =>
1.238 if A aconv A' andalso B aconv B' then
1.239 - Thm (deriv_rule2 (Pt.equal_intr A B) der1 der2,
1.240 + Thm (deriv_rule2 (Proofterm.equal_intr A B) der1 der2,
1.241 {thy_ref = merge_thys2 th1 th2,
1.242 tags = [],
1.243 maxidx = Int.max (max1, max2),
1.244 @@ -994,7 +991,7 @@
1.245 case prop1 of
1.246 Const ("==", _) $ A $ B =>
1.247 if prop2 aconv A then
1.248 - Thm (deriv_rule2 (Pt.equal_elim A B) der1 der2,
1.249 + Thm (deriv_rule2 (Proofterm.equal_elim A B) der1 der2,
1.250 {thy_ref = merge_thys2 th1 th2,
1.251 tags = [],
1.252 maxidx = Int.max (max1, max2),
1.253 @@ -1024,7 +1021,7 @@
1.254 val tpairs' = tpairs |> map (pairself (Envir.norm_term env))
1.255 (*remove trivial tpairs, of the form t==t*)
1.256 |> filter_out (op aconv);
1.257 - val der' = deriv_rule1 (Pt.norm_proof' env) der;
1.258 + val der' = deriv_rule1 (Proofterm.norm_proof' env) der;
1.259 val prop' = Envir.norm_term env prop;
1.260 val maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop');
1.261 val shyps = Envir.insert_sorts env shyps;
1.262 @@ -1064,7 +1061,7 @@
1.263 val tpairs' = map (pairself gen) tpairs;
1.264 val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop');
1.265 in
1.266 - Thm (deriv_rule1 (Pt.generalize (tfrees, frees) idx) der,
1.267 + Thm (deriv_rule1 (Proofterm.generalize (tfrees, frees) idx) der,
1.268 {thy_ref = thy_ref,
1.269 tags = [],
1.270 maxidx = maxidx',
1.271 @@ -1135,7 +1132,8 @@
1.272 val (tpairs', maxidx') =
1.273 fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1;
1.274 in
1.275 - Thm (deriv_rule1 (fn d => Pt.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der,
1.276 + Thm (deriv_rule1
1.277 + (fn d => Proofterm.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der,
1.278 {thy_ref = thy_ref',
1.279 tags = [],
1.280 maxidx = maxidx',
1.281 @@ -1168,7 +1166,7 @@
1.282 if T <> propT then
1.283 raise THM ("trivial: the term must have type prop", 0, [])
1.284 else
1.285 - Thm (deriv_rule0 (Pt.AbsP ("H", NONE, Pt.PBound 0)),
1.286 + Thm (deriv_rule0 (Proofterm.AbsP ("H", NONE, Proofterm.PBound 0)),
1.287 {thy_ref = thy_ref,
1.288 tags = [],
1.289 maxidx = maxidx,
1.290 @@ -1190,7 +1188,7 @@
1.291 val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_of_class (T, c));
1.292 in
1.293 if Sign.of_sort thy (T, [c]) then
1.294 - Thm (deriv_rule0 (Pt.OfClass (T, c)),
1.295 + Thm (deriv_rule0 (Proofterm.OfClass (T, c)),
1.296 {thy_ref = Theory.check_thy thy,
1.297 tags = [],
1.298 maxidx = maxidx,
1.299 @@ -1215,7 +1213,8 @@
1.300 |> Sorts.minimal_sorts algebra;
1.301 val shyps' = fold (Sorts.insert_sort o #2) present extra';
1.302 in
1.303 - Thm (deriv_rule_unconditional (Pt.strip_shyps_proof algebra present witnessed extra') der,
1.304 + Thm (deriv_rule_unconditional
1.305 + (Proofterm.strip_shyps_proof algebra present witnessed extra') der,
1.306 {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx,
1.307 shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
1.308 end;
1.309 @@ -1234,7 +1233,8 @@
1.310
1.311 val ps = map (apsnd (Future.map proof_body_of)) promises;
1.312 val thy = Theory.deref thy_ref;
1.313 - val (pthm as (_, (_, prop', _)), proof) = Pt.unconstrain_thm_proof thy shyps prop ps body;
1.314 + val (pthm as (_, (_, prop', _)), proof) =
1.315 + Proofterm.unconstrain_thm_proof thy shyps prop ps body;
1.316 val der' = make_deriv [] [] [pthm] proof;
1.317 val _ = Theory.check_thy thy;
1.318 in
1.319 @@ -1256,7 +1256,7 @@
1.320 val (al, prop2) = Type.varify_global tfrees prop1;
1.321 val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
1.322 in
1.323 - (al, Thm (deriv_rule1 (Pt.varify_proof prop tfrees) der,
1.324 + (al, Thm (deriv_rule1 (Proofterm.varify_proof prop tfrees) der,
1.325 {thy_ref = thy_ref,
1.326 tags = [],
1.327 maxidx = Int.max (0, maxidx),
1.328 @@ -1275,7 +1275,7 @@
1.329 val prop2 = Type.legacy_freeze prop1;
1.330 val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
1.331 in
1.332 - Thm (deriv_rule1 (Pt.legacy_freezeT prop1) der,
1.333 + Thm (deriv_rule1 (Proofterm.legacy_freezeT prop1) der,
1.334 {thy_ref = thy_ref,
1.335 tags = [],
1.336 maxidx = maxidx_of_term prop2,
1.337 @@ -1308,7 +1308,7 @@
1.338 in
1.339 if T <> propT then raise THM ("lift_rule: the term must have type prop", 0, [])
1.340 else
1.341 - Thm (deriv_rule1 (Pt.lift_proof gprop inc prop) der,
1.342 + Thm (deriv_rule1 (Proofterm.lift_proof gprop inc prop) der,
1.343 {thy_ref = merge_thys1 goal orule,
1.344 tags = [],
1.345 maxidx = maxidx + inc,
1.346 @@ -1322,7 +1322,7 @@
1.347 if i < 0 then raise THM ("negative increment", 0, [thm])
1.348 else if i = 0 then thm
1.349 else
1.350 - Thm (deriv_rule1 (Pt.incr_indexes i) der,
1.351 + Thm (deriv_rule1 (Proofterm.incr_indexes i) der,
1.352 {thy_ref = thy_ref,
1.353 tags = [],
1.354 maxidx = maxidx + i,
1.355 @@ -1339,8 +1339,8 @@
1.356 val (tpairs, Bs, Bi, C) = dest_state (state, i);
1.357 fun newth n (env, tpairs) =
1.358 Thm (deriv_rule1
1.359 - ((if Envir.is_empty env then I else (Pt.norm_proof' env)) o
1.360 - Pt.assumption_proof Bs Bi n) der,
1.361 + ((if Envir.is_empty env then I else (Proofterm.norm_proof' env)) o
1.362 + Proofterm.assumption_proof Bs Bi n) der,
1.363 {tags = [],
1.364 maxidx = Envir.maxidx_of env,
1.365 shyps = Envir.insert_sorts env shyps,
1.366 @@ -1377,7 +1377,7 @@
1.367 (case find_index (fn asm => Pattern.aeconv (asm, concl)) asms of
1.368 ~1 => raise THM ("eq_assumption", 0, [state])
1.369 | n =>
1.370 - Thm (deriv_rule1 (Pt.assumption_proof Bs Bi (n + 1)) der,
1.371 + Thm (deriv_rule1 (Proofterm.assumption_proof Bs Bi (n + 1)) der,
1.372 {thy_ref = thy_ref,
1.373 tags = [],
1.374 maxidx = maxidx,
1.375 @@ -1406,7 +1406,7 @@
1.376 in list_all (params, Logic.list_implies (qs @ ps, concl)) end
1.377 else raise THM ("rotate_rule", k, [state]);
1.378 in
1.379 - Thm (deriv_rule1 (Pt.rotate_proof Bs Bi m) der,
1.380 + Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi m) der,
1.381 {thy_ref = thy_ref,
1.382 tags = [],
1.383 maxidx = maxidx,
1.384 @@ -1437,7 +1437,7 @@
1.385 in Logic.list_implies (fixed_prems @ qs @ ps, concl) end
1.386 else raise THM ("permute_prems: k", k, [rl]);
1.387 in
1.388 - Thm (deriv_rule1 (Pt.permute_prems_proof prems j m) der,
1.389 + Thm (deriv_rule1 (Proofterm.permute_prems_proof prems j m) der,
1.390 {thy_ref = thy_ref,
1.391 tags = [],
1.392 maxidx = maxidx,
1.393 @@ -1605,10 +1605,10 @@
1.394 Thm (deriv_rule2
1.395 ((if Envir.is_empty env then I
1.396 else if Envir.above env smax then
1.397 - (fn f => fn der => f (Pt.norm_proof' env der))
1.398 + (fn f => fn der => f (Proofterm.norm_proof' env der))
1.399 else
1.400 - curry op oo (Pt.norm_proof' env))
1.401 - (Pt.bicompose_proof flatten Bs oldAs As A n (nlift+1))) rder' sder,
1.402 + curry op oo (Proofterm.norm_proof' env))
1.403 + (Proofterm.bicompose_proof flatten Bs oldAs As A n (nlift+1))) rder' sder,
1.404 {tags = [],
1.405 maxidx = Envir.maxidx_of env,
1.406 shyps = Envir.insert_sorts env (Sorts.union rshyps sshyps),
1.407 @@ -1624,7 +1624,7 @@
1.408 let val (As1, rder') =
1.409 if not lifted then (As0, rder)
1.410 else (map (rename_bvars(dpairs,tpairs,B)) As0,
1.411 - deriv_rule1 (Pt.map_proof_terms
1.412 + deriv_rule1 (Proofterm.map_proof_terms
1.413 (rename_bvars (dpairs, tpairs, Bound 0)) I) rder);
1.414 in (map (if flatten then (Logic.flatten_params n) else I) As1, As1, rder', n)
1.415 handle TERM _ =>
1.416 @@ -1711,7 +1711,7 @@
1.417 if T <> propT then
1.418 raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
1.419 else
1.420 - let val (ora, prf) = Pt.oracle_proof name prop in
1.421 + let val (ora, prf) = Proofterm.oracle_proof name prop in
1.422 Thm (make_deriv [] [ora] [] prf,
1.423 {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
1.424 tags = [],