1.1 --- a/src/Pure/thm.ML Sat Nov 15 21:31:23 2008 +0100
1.2 +++ b/src/Pure/thm.ML Sat Nov 15 21:31:25 2008 +0100
1.3 @@ -121,11 +121,6 @@
1.4 val adjust_maxidx_cterm: int -> cterm -> cterm
1.5 val capply: cterm -> cterm -> cterm
1.6 val cabs: cterm -> cterm -> cterm
1.7 - val rep_deriv: thm ->
1.8 - {oracle: bool,
1.9 - proof: Proofterm.proof,
1.10 - promises: (serial * thm Future.T) OrdList.T}
1.11 - val oracle_of: thm -> bool
1.12 val major_prem_of: thm -> term
1.13 val no_prems: thm -> bool
1.14 val terms_of_tpairs: (term * term) list -> term list
1.15 @@ -153,7 +148,7 @@
1.16 val freezeT: thm -> thm
1.17 val join_futures: theory -> unit
1.18 val future: (unit -> thm) -> cterm -> thm
1.19 - val proof_of: thm -> Proofterm.proof
1.20 + val proof_of: thm -> proof_body
1.21 val extern_oracles: theory -> xstring list
1.22 val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
1.23 end;
1.24 @@ -350,9 +345,9 @@
1.25 tpairs: (term * term) list, (*flex-flex pairs*)
1.26 prop: term} (*conclusion*)
1.27 and deriv = Deriv of
1.28 - {oracle: bool, (*oracle occurrence flag*)
1.29 - proof: Pt.proof, (*proof term*)
1.30 - promises: (serial * thm Future.T) OrdList.T}; (*promised derivations*)
1.31 + {all_promises: (serial * thm Future.T) OrdList.T,
1.32 + promises: (serial * thm Future.T) OrdList.T,
1.33 + body: Pt.proof_body};
1.34
1.35 type conv = cterm -> thm;
1.36
1.37 @@ -399,8 +394,8 @@
1.38
1.39 (* basic components *)
1.40
1.41 -fun rep_deriv (Thm (Deriv args, _)) = args;
1.42 -val oracle_of = #oracle o rep_deriv;
1.43 +fun deriv_of (Thm (Deriv der, _)) = der;
1.44 +val proof_term_of = Proofterm.proof_of o #body o deriv_of;
1.45
1.46 val theory_of_thm = Theory.deref o #thy_ref o rep_thm;
1.47 val maxidx_of = #maxidx o rep_thm;
1.48 @@ -508,10 +503,12 @@
1.49
1.50 (** derivations **)
1.51
1.52 -fun make_deriv oracle promises proof =
1.53 - Deriv {oracle = oracle, promises = promises, proof = proof};
1.54 +fun make_deriv all_promises promises oracles thms proof =
1.55 + Deriv {all_promises = all_promises, promises = promises,
1.56 + body = PBody {oracles = oracles, thms = thms, proof = proof}};
1.57
1.58 -val empty_deriv = make_deriv false [] Pt.min_proof;
1.59 +val closed_deriv = make_deriv [] [] [] [];
1.60 +val empty_deriv = closed_deriv Pt.MinProof;
1.61
1.62
1.63 (* inference rules *)
1.64 @@ -519,23 +516,25 @@
1.65 fun promise_ord ((i, _), (j, _)) = int_ord (j, i);
1.66
1.67 fun deriv_rule2 f
1.68 - (Deriv {oracle = ora1, promises = ps1, proof = prf1})
1.69 - (Deriv {oracle = ora2, promises = ps2, proof = prf2}) =
1.70 + (Deriv {all_promises = all_ps1, promises = ps1,
1.71 + body = PBody {oracles = oras1, thms = thms1, proof = prf1}})
1.72 + (Deriv {all_promises = all_ps2, promises = ps2,
1.73 + body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) =
1.74 let
1.75 - val ora = ora1 orelse ora2;
1.76 + val all_ps = OrdList.union promise_ord all_ps1 all_ps2;
1.77 val ps = OrdList.union promise_ord ps1 ps2;
1.78 + val oras = Pt.merge_oracles oras1 oras2;
1.79 + val thms = Pt.merge_thms thms1 thms2;
1.80 val prf =
1.81 (case ! Pt.proofs of
1.82 2 => f prf1 prf2
1.83 - | 1 => MinProof (([], [], []) |> Pt.mk_min_proof prf1 |> Pt.mk_min_proof prf2)
1.84 - | 0 =>
1.85 - if ora then MinProof ([], [], [] |> Pt.add_oracles ora1 prf1 |> Pt.add_oracles ora2 prf2)
1.86 - else Pt.min_proof
1.87 + | 1 => MinProof
1.88 + | 0 => MinProof
1.89 | i => error ("Illegal level of detail for proof objects: " ^ string_of_int i));
1.90 - in make_deriv ora ps prf end;
1.91 + in make_deriv all_ps ps oras thms prf end;
1.92
1.93 fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv;
1.94 -fun deriv_rule0 prf = deriv_rule1 I (make_deriv false [] prf);
1.95 +fun deriv_rule0 prf = deriv_rule1 I (closed_deriv prf);
1.96
1.97
1.98
1.99 @@ -573,19 +572,7 @@
1.100 map (fn s => (s, axiom thy s)) (Symtab.keys (Theory.axiom_table thy));
1.101
1.102
1.103 -(* official name and additional tags *)
1.104 -
1.105 -fun get_name (Thm (Deriv {proof, ...}, {hyps, prop, ...})) = Pt.get_name hyps prop proof;
1.106 -
1.107 -fun put_name name thm =
1.108 - let
1.109 - val Thm (Deriv {oracle, promises, proof}, args as {thy_ref, hyps, prop, tpairs, ...}) = thm;
1.110 - val _ = null tpairs orelse raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]);
1.111 - val thy = Theory.deref thy_ref;
1.112 - val der' = make_deriv oracle promises (Pt.thm_proof thy name hyps prop proof);
1.113 - val _ = Theory.check_thy thy;
1.114 - in Thm (der', args) end;
1.115 -
1.116 +(* tags *)
1.117
1.118 val get_tags = #tags o rep_thm;
1.119
1.120 @@ -1641,12 +1628,12 @@
1.121 val _ = Theory.check_thy orig_thy;
1.122 fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
1.123
1.124 - val Thm (Deriv {promises, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
1.125 + val Thm (Deriv {all_promises, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
1.126 val _ = prop aconv orig_prop orelse err "bad prop";
1.127 val _ = null tpairs orelse err "bad tpairs";
1.128 val _ = null hyps orelse err "bad hyps";
1.129 val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
1.130 - val _ = forall (fn (j, _) => j < i) promises orelse err "bad dependencies";
1.131 + val _ = forall (fn (j, _) => j < i) all_promises orelse err "bad dependencies";
1.132 in thm end;
1.133
1.134 fun future make_result ct =
1.135 @@ -1658,8 +1645,9 @@
1.136 val i = serial ();
1.137 val future = Future.fork_background (future_result i thy sorts prop o make_result);
1.138 val _ = add_future thy future;
1.139 + val promises = [(i, future)];
1.140 in
1.141 - Thm (make_deriv false [(i, future)] (Pt.promise_proof i prop),
1.142 + Thm (make_deriv promises promises [] [] (Pt.promise_proof i prop),
1.143 {thy_ref = thy_ref,
1.144 tags = [],
1.145 maxidx = maxidx,
1.146 @@ -1670,18 +1658,34 @@
1.147 end;
1.148
1.149
1.150 -(* join_deriv *)
1.151 +(* fulfilled proof *)
1.152
1.153 -fun join_deriv (thm as Thm (Deriv {oracle, proof, promises}, args)) =
1.154 +fun proof_of thm =
1.155 let
1.156 - val _ = Exn.release_all (Future.join_results (rev (map #2 promises)));
1.157 - val results = map (apsnd Future.join) promises;
1.158 - val proofs = fold (fn (i, Thm (Deriv {proof = prf, ...}, _)) => Inttab.update (i, prf))
1.159 - results Inttab.empty;
1.160 - val ora = oracle orelse exists (oracle_of o #2) results;
1.161 - in Thm (make_deriv ora [] (Pt.fulfill proofs proof), args) end;
1.162 + val {all_promises, promises, body} = deriv_of thm;
1.163 + val _ = Exn.release_all (map (Future.join_result o #2) (rev all_promises));
1.164 + val ps = map (apsnd (Lazy.value o proof_term_of o Future.join)) promises;
1.165 + in Pt.fulfill_proof ps body end;
1.166
1.167 -val proof_of = join_deriv #> (fn Thm (Deriv {proof, ...}, _) => proof);
1.168 +
1.169 +(* closed derivations with official name *)
1.170 +
1.171 +fun get_name thm =
1.172 + Pt.get_name (hyps_of thm) (prop_of thm) (proof_term_of thm);
1.173 +
1.174 +fun put_name name (thm as Thm (der, args)) =
1.175 + let
1.176 + val Deriv {all_promises, promises, body} = der;
1.177 + val {thy_ref, hyps, prop, tpairs, ...} = args;
1.178 + val _ = null tpairs orelse raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]);
1.179 +
1.180 + val ps =
1.181 + map (apsnd (fn future => Lazy.lazy (fn () => proof_term_of (Future.join future)))) promises;
1.182 + val thy = Theory.deref thy_ref;
1.183 + val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
1.184 + val der' = make_deriv [] [] [] [pthm] proof;
1.185 + val _ = Theory.check_thy thy;
1.186 + in Thm (der', args) end;
1.187
1.188
1.189
1.190 @@ -1694,14 +1698,16 @@
1.191 if T <> propT then
1.192 raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
1.193 else
1.194 - Thm (make_deriv true [] (Pt.oracle_proof name prop),
1.195 - {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
1.196 - tags = [],
1.197 - maxidx = maxidx,
1.198 - shyps = sorts,
1.199 - hyps = [],
1.200 - tpairs = [],
1.201 - prop = prop})
1.202 + let val prf = Pt.oracle_proof name prop in
1.203 + Thm (make_deriv [] [] (Pt.make_oracles prf) [] prf,
1.204 + {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
1.205 + tags = [],
1.206 + maxidx = maxidx,
1.207 + shyps = sorts,
1.208 + hyps = [],
1.209 + tpairs = [],
1.210 + prop = prop})
1.211 + end
1.212 end;
1.213
1.214