1.1 --- a/src/Pure/thm.ML Tue Sep 23 15:48:51 2008 +0200
1.2 +++ b/src/Pure/thm.ML Tue Sep 23 15:48:52 2008 +0200
1.3 @@ -37,7 +37,6 @@
1.4 val ctyp_of_term: cterm -> ctyp
1.5
1.6 (*theorems*)
1.7 - type deriv
1.8 type thm
1.9 type conv = cterm -> thm
1.10 type attribute = Context.generic * thm -> Context.generic * thm
1.11 @@ -60,8 +59,6 @@
1.12 exception THM of string * int * thm list
1.13 val theory_of_thm: thm -> theory
1.14 val prop_of: thm -> term
1.15 - val oracle_of: thm -> bool
1.16 - val proof_of: thm -> Proofterm.proof
1.17 val tpairs_of: thm -> (term * term) list
1.18 val concl_of: thm -> term
1.19 val prems_of: thm -> term list
1.20 @@ -113,9 +110,6 @@
1.21 val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq
1.22 val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
1.23 val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
1.24 - val promise: thm Future.T -> cterm -> thm
1.25 - val extern_oracles: theory -> xstring list
1.26 - val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
1.27 end;
1.28
1.29 signature THM =
1.30 @@ -131,6 +125,11 @@
1.31 val adjust_maxidx_cterm: int -> cterm -> cterm
1.32 val capply: cterm -> cterm -> cterm
1.33 val cabs: cterm -> cterm -> cterm
1.34 + val dest_deriv: thm ->
1.35 + {oracle: bool,
1.36 + proof: Proofterm.proof,
1.37 + promises: (serial * (thm Future.T * theory * sort list * term)) list}
1.38 + val oracle_of: thm -> bool
1.39 val major_prem_of: thm -> term
1.40 val no_prems: thm -> bool
1.41 val terms_of_tpairs: (term * term) list -> term list
1.42 @@ -151,6 +150,11 @@
1.43 val varifyT: thm -> thm
1.44 val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
1.45 val freezeT: thm -> thm
1.46 + val promise: thm Future.T -> cterm -> thm
1.47 + val fulfill: thm -> thm
1.48 + val proof_of: thm -> Proofterm.proof
1.49 + val extern_oracles: theory -> xstring list
1.50 + val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
1.51 end;
1.52
1.53 structure Thm: THM =
1.54 @@ -337,19 +341,21 @@
1.55
1.56 (*** Derivations and Theorems ***)
1.57
1.58 -abstype deriv = Deriv of
1.59 - {oracle: bool, (*oracle occurrence flag*)
1.60 - proof: Pt.proof, (*proof term*)
1.61 - promises: (serial * (theory * thm Future.T)) list} (*promised derivations*)
1.62 -and thm = Thm of
1.63 - deriv * (*derivation*)
1.64 - {thy_ref: theory_ref, (*dynamic reference to theory*)
1.65 - tags: Properties.T, (*additional annotations/comments*)
1.66 - maxidx: int, (*maximum index of any Var or TVar*)
1.67 - shyps: sort list, (*sort hypotheses as ordered list*)
1.68 - hyps: term list, (*hypotheses as ordered list*)
1.69 - tpairs: (term * term) list, (*flex-flex pairs*)
1.70 - prop: term} (*conclusion*)
1.71 +abstype thm = Thm of
1.72 + deriv * (*derivation*)
1.73 + {thy_ref: theory_ref, (*dynamic reference to theory*)
1.74 + tags: Properties.T, (*additional annotations/comments*)
1.75 + maxidx: int, (*maximum index of any Var or TVar*)
1.76 + shyps: sort list, (*sort hypotheses as ordered list*)
1.77 + hyps: term list, (*hypotheses as ordered list*)
1.78 + tpairs: (term * term) list, (*flex-flex pairs*)
1.79 + prop: term} (*conclusion*)
1.80 +and deriv = Deriv of
1.81 + {oracle: bool, (*oracle occurrence flag*)
1.82 + proof: Pt.proof, (*proof term*)
1.83 + promises: (serial * promise) list} (*promised derivations*)
1.84 +and promise = Promise of
1.85 + thm Future.T * theory * sort list * term
1.86 with
1.87
1.88 type conv = cterm -> thm;
1.89 @@ -395,13 +401,16 @@
1.90
1.91 (* basic components *)
1.92
1.93 +fun dest_deriv (Thm (Deriv {oracle, proof, promises}, _)) =
1.94 + {oracle = oracle, proof = proof, promises = map (fn (i, Promise args) => (i, args)) promises};
1.95 +
1.96 +fun oracle_of (Thm (Deriv {oracle, ...}, _)) = oracle;
1.97 +
1.98 val theory_of_thm = Theory.deref o #thy_ref o rep_thm;
1.99 val maxidx_of = #maxidx o rep_thm;
1.100 fun maxidx_thm th i = Int.max (maxidx_of th, i);
1.101 val hyps_of = #hyps o rep_thm;
1.102 val prop_of = #prop o rep_thm;
1.103 -fun oracle_of (Thm (Deriv {oracle, ...}, _)) = oracle; (* FIXME finish proof *)
1.104 -fun proof_of (Thm (Deriv {proof, ...}, _)) = proof; (* FIXME finish proof *)
1.105 val tpairs_of = #tpairs o rep_thm;
1.106
1.107 val concl_of = Logic.strip_imp_concl o prop_of;
1.108 @@ -492,30 +501,33 @@
1.109
1.110 (** derivations **)
1.111
1.112 -local
1.113 +(* type deriv *)
1.114
1.115 fun make_deriv oracle promises proof =
1.116 Deriv {oracle = oracle, promises = promises, proof = proof};
1.117
1.118 val empty_deriv = make_deriv false [] Pt.min_proof;
1.119
1.120 -fun add_oracles false = K I
1.121 - | add_oracles true = Pt.oracles_of_proof;
1.122
1.123 -in
1.124 +(* type promise *)
1.125 +
1.126 +fun promise_ord ((i, Promise _), (j, Promise _)) = int_ord (j, i);
1.127 +
1.128 +
1.129 +(* inference rules *)
1.130
1.131 fun deriv_rule2 f
1.132 (Deriv {oracle = ora1, promises = ps1, proof = prf1})
1.133 (Deriv {oracle = ora2, promises = ps2, proof = prf2}) =
1.134 let
1.135 val ora = ora1 orelse ora2;
1.136 - val ps = OrdList.union (int_ord o pairself #1) ps1 ps2;
1.137 + val ps = OrdList.union promise_ord ps1 ps2;
1.138 val prf =
1.139 (case ! Pt.proofs of
1.140 2 => f prf1 prf2
1.141 | 1 => MinProof (([], [], []) |> Pt.mk_min_proof prf1 |> Pt.mk_min_proof prf2)
1.142 | 0 =>
1.143 - if ora then MinProof ([], [], [] |> add_oracles ora1 prf1 |> add_oracles ora2 prf2)
1.144 + if ora then MinProof ([], [], [] |> Pt.add_oracles ora1 prf1 |> Pt.add_oracles ora2 prf2)
1.145 else Pt.min_proof
1.146 | i => error ("Illegal level of detail for proof objects: " ^ string_of_int i));
1.147 in make_deriv ora ps prf end;
1.148 @@ -523,17 +535,6 @@
1.149 fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv;
1.150 fun deriv_rule0 prf = deriv_rule1 I (make_deriv false [] prf);
1.151
1.152 -fun deriv_oracle name prop =
1.153 - make_deriv true [] (Pt.oracle_proof name prop);
1.154 -
1.155 -fun deriv_promise i thy future prop =
1.156 - make_deriv false [(i, (thy, future))] (Pt.promise_proof i prop);
1.157 -
1.158 -fun deriv_uncond_rule f (Deriv {oracle, promises, proof}) =
1.159 - make_deriv oracle promises (f proof);
1.160 -
1.161 -end;
1.162 -
1.163
1.164
1.165 (** Axioms **)
1.166 @@ -576,18 +577,16 @@
1.167
1.168 (* official name and additional tags *)
1.169
1.170 -fun get_name th = Pt.get_name (hyps_of th) (prop_of th) (proof_of th); (*finished proof!*)
1.171 +fun get_name (Thm (Deriv {proof, ...}, {hyps, prop, ...})) = Pt.get_name hyps prop proof;
1.172
1.173 -fun is_named (Thm (Deriv {proof, ...}, _)) = Pt.is_named proof;
1.174 -
1.175 -fun put_name name (thm as Thm (der, args as {thy_ref, hyps, prop, tpairs, ...})) =
1.176 - let
1.177 - val _ = null tpairs orelse
1.178 - raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]);
1.179 - val thy = Theory.deref thy_ref;
1.180 - val der' = deriv_uncond_rule (Pt.thm_proof thy name hyps prop) der;
1.181 - val _ = Theory.check_thy thy;
1.182 - in Thm (der', args) end;
1.183 +fun put_name name thm =
1.184 + let
1.185 + val Thm (Deriv {oracle, promises, proof}, args as {thy_ref, hyps, prop, tpairs, ...}) = thm;
1.186 + val _ = null tpairs orelse raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]);
1.187 + val thy = Theory.deref thy_ref;
1.188 + val der' = make_deriv oracle promises (Pt.thm_proof thy name hyps prop proof);
1.189 + val _ = Theory.check_thy thy;
1.190 + in Thm (der', args) end;
1.191
1.192
1.193 val get_tags = #tags o rep_thm;
1.194 @@ -1606,6 +1605,8 @@
1.195
1.196 (*** Promises ***)
1.197
1.198 +(* promise *)
1.199 +
1.200 fun promise future ct =
1.201 let
1.202 val {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = rep_cterm ct;
1.203 @@ -1613,7 +1614,7 @@
1.204 val _ = T <> propT andalso raise CTERM ("promise: prop expected", [ct]);
1.205 val i = serial ();
1.206 in
1.207 - Thm (deriv_promise i thy future prop,
1.208 + Thm (make_deriv false [(i, Promise (future, thy, sorts, prop))] (Pt.promise_proof i prop),
1.209 {thy_ref = thy_ref,
1.210 tags = [],
1.211 maxidx = maxidx,
1.212 @@ -1623,6 +1624,34 @@
1.213 prop = prop})
1.214 end;
1.215
1.216 +fun check_promise (i, Promise (future, thy1, shyps1, prop1)) =
1.217 + let
1.218 + val thm = transfer thy1 (Future.join future);
1.219 + val _ = Theory.check_thy thy1;
1.220 + fun err msg = raise THM ("check_promise: " ^ msg, 0, [thm]);
1.221 +
1.222 + val Thm (Deriv {oracle, proof, promises}, {shyps, hyps, tpairs, prop, ...}) = thm;
1.223 + val _ = null promises orelse err "illegal nested promises";
1.224 + val _ = shyps = shyps1 orelse err "bad shyps";
1.225 + val _ = null hyps orelse err "bad hyps";
1.226 + val _ = null tpairs orelse err "bad tpairs";
1.227 + val _ = prop aconv prop1 orelse err "bad prop";
1.228 + in (oracle, (i, proof)) end;
1.229 +
1.230 +
1.231 +(* fulfill *)
1.232 +
1.233 +fun fulfill (thm as Thm (Deriv {oracle, proof, promises}, args)) =
1.234 + let
1.235 + val _ = Future.join_results (map (fn (_, Promise (future, _, _, _)) => future) promises);
1.236 + val results = map check_promise promises;
1.237 +
1.238 + val ora = oracle orelse exists #1 results;
1.239 + val prf = Pt.fulfill (fold (Inttab.update o #2) results Inttab.empty) proof;
1.240 + in Thm (make_deriv ora [] prf, args) end;
1.241 +
1.242 +val proof_of = fulfill #> (fn Thm (Deriv {proof, ...}, _) => proof);
1.243 +
1.244
1.245
1.246 (*** Oracles ***)
1.247 @@ -1634,7 +1663,7 @@
1.248 if T <> propT then
1.249 raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
1.250 else
1.251 - Thm (deriv_oracle name prop,
1.252 + Thm (make_deriv true [] (Pt.oracle_proof name prop),
1.253 {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
1.254 tags = [],
1.255 maxidx = maxidx,