# HG changeset patch # User wenzelm # Date 1222177732 -7200 # Node ID 7e803c3923420be931108649afcf832be29b65e0 # Parent e6a5fa9f1e415c5fe818b152ccb81c01e009fa20 added dest_deriv, removed external type deriv; misc tuning of internal deriv; more substantial promise/fulfill; promise_ord: reverse order on serial numbers; removed unused is_named; get_name: unfinished proof term; diff -r e6a5fa9f1e41 -r 7e803c392342 src/Pure/thm.ML --- a/src/Pure/thm.ML Tue Sep 23 15:48:51 2008 +0200 +++ b/src/Pure/thm.ML Tue Sep 23 15:48:52 2008 +0200 @@ -37,7 +37,6 @@ val ctyp_of_term: cterm -> ctyp (*theorems*) - type deriv type thm type conv = cterm -> thm type attribute = Context.generic * thm -> Context.generic * thm @@ -60,8 +59,6 @@ exception THM of string * int * thm list val theory_of_thm: thm -> theory val prop_of: thm -> term - val oracle_of: thm -> bool - val proof_of: thm -> Proofterm.proof val tpairs_of: thm -> (term * term) list val concl_of: thm -> term val prems_of: thm -> term list @@ -113,9 +110,6 @@ val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq - val promise: thm Future.T -> cterm -> thm - val extern_oracles: theory -> xstring list - val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory end; signature THM = @@ -131,6 +125,11 @@ val adjust_maxidx_cterm: int -> cterm -> cterm val capply: cterm -> cterm -> cterm val cabs: cterm -> cterm -> cterm + val dest_deriv: thm -> + {oracle: bool, + proof: Proofterm.proof, + promises: (serial * (thm Future.T * theory * sort list * term)) list} + val oracle_of: thm -> bool val major_prem_of: thm -> term val no_prems: thm -> bool val terms_of_tpairs: (term * term) list -> term list @@ -151,6 +150,11 @@ val varifyT: thm -> thm val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm val freezeT: thm -> thm + val promise: thm Future.T -> cterm -> thm + val fulfill: thm -> thm + val proof_of: thm -> Proofterm.proof + val extern_oracles: theory -> xstring list + val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory end; structure Thm: THM = @@ -337,19 +341,21 @@ (*** Derivations and Theorems ***) -abstype deriv = Deriv of - {oracle: bool, (*oracle occurrence flag*) - proof: Pt.proof, (*proof term*) - promises: (serial * (theory * thm Future.T)) list} (*promised derivations*) -and thm = Thm of - deriv * (*derivation*) - {thy_ref: theory_ref, (*dynamic reference to theory*) - tags: Properties.T, (*additional annotations/comments*) - maxidx: int, (*maximum index of any Var or TVar*) - shyps: sort list, (*sort hypotheses as ordered list*) - hyps: term list, (*hypotheses as ordered list*) - tpairs: (term * term) list, (*flex-flex pairs*) - prop: term} (*conclusion*) +abstype thm = Thm of + deriv * (*derivation*) + {thy_ref: theory_ref, (*dynamic reference to theory*) + tags: Properties.T, (*additional annotations/comments*) + maxidx: int, (*maximum index of any Var or TVar*) + shyps: sort list, (*sort hypotheses as ordered list*) + hyps: term list, (*hypotheses as ordered list*) + tpairs: (term * term) list, (*flex-flex pairs*) + prop: term} (*conclusion*) +and deriv = Deriv of + {oracle: bool, (*oracle occurrence flag*) + proof: Pt.proof, (*proof term*) + promises: (serial * promise) list} (*promised derivations*) +and promise = Promise of + thm Future.T * theory * sort list * term with type conv = cterm -> thm; @@ -395,13 +401,16 @@ (* basic components *) +fun dest_deriv (Thm (Deriv {oracle, proof, promises}, _)) = + {oracle = oracle, proof = proof, promises = map (fn (i, Promise args) => (i, args)) promises}; + +fun oracle_of (Thm (Deriv {oracle, ...}, _)) = oracle; + val theory_of_thm = Theory.deref o #thy_ref o rep_thm; val maxidx_of = #maxidx o rep_thm; fun maxidx_thm th i = Int.max (maxidx_of th, i); val hyps_of = #hyps o rep_thm; val prop_of = #prop o rep_thm; -fun oracle_of (Thm (Deriv {oracle, ...}, _)) = oracle; (* FIXME finish proof *) -fun proof_of (Thm (Deriv {proof, ...}, _)) = proof; (* FIXME finish proof *) val tpairs_of = #tpairs o rep_thm; val concl_of = Logic.strip_imp_concl o prop_of; @@ -492,30 +501,33 @@ (** derivations **) -local +(* type deriv *) fun make_deriv oracle promises proof = Deriv {oracle = oracle, promises = promises, proof = proof}; val empty_deriv = make_deriv false [] Pt.min_proof; -fun add_oracles false = K I - | add_oracles true = Pt.oracles_of_proof; + +(* type promise *) -in +fun promise_ord ((i, Promise _), (j, Promise _)) = int_ord (j, i); + + +(* inference rules *) fun deriv_rule2 f (Deriv {oracle = ora1, promises = ps1, proof = prf1}) (Deriv {oracle = ora2, promises = ps2, proof = prf2}) = let val ora = ora1 orelse ora2; - val ps = OrdList.union (int_ord o pairself #1) ps1 ps2; + val ps = OrdList.union promise_ord ps1 ps2; val prf = (case ! Pt.proofs of 2 => f prf1 prf2 | 1 => MinProof (([], [], []) |> Pt.mk_min_proof prf1 |> Pt.mk_min_proof prf2) | 0 => - if ora then MinProof ([], [], [] |> add_oracles ora1 prf1 |> add_oracles ora2 prf2) + if ora then MinProof ([], [], [] |> Pt.add_oracles ora1 prf1 |> Pt.add_oracles ora2 prf2) else Pt.min_proof | i => error ("Illegal level of detail for proof objects: " ^ string_of_int i)); in make_deriv ora ps prf end; @@ -523,17 +535,6 @@ fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv; fun deriv_rule0 prf = deriv_rule1 I (make_deriv false [] prf); -fun deriv_oracle name prop = - make_deriv true [] (Pt.oracle_proof name prop); - -fun deriv_promise i thy future prop = - make_deriv false [(i, (thy, future))] (Pt.promise_proof i prop); - -fun deriv_uncond_rule f (Deriv {oracle, promises, proof}) = - make_deriv oracle promises (f proof); - -end; - (** Axioms **) @@ -576,18 +577,16 @@ (* official name and additional tags *) -fun get_name th = Pt.get_name (hyps_of th) (prop_of th) (proof_of th); (*finished proof!*) - -fun is_named (Thm (Deriv {proof, ...}, _)) = Pt.is_named proof; +fun get_name (Thm (Deriv {proof, ...}, {hyps, prop, ...})) = Pt.get_name hyps prop proof; -fun put_name name (thm as Thm (der, args as {thy_ref, hyps, prop, tpairs, ...})) = - let - val _ = null tpairs orelse - raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]); - val thy = Theory.deref thy_ref; - val der' = deriv_uncond_rule (Pt.thm_proof thy name hyps prop) der; - val _ = Theory.check_thy thy; - in Thm (der', args) end; +fun put_name name thm = + let + val Thm (Deriv {oracle, promises, proof}, args as {thy_ref, hyps, prop, tpairs, ...}) = thm; + val _ = null tpairs orelse raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]); + val thy = Theory.deref thy_ref; + val der' = make_deriv oracle promises (Pt.thm_proof thy name hyps prop proof); + val _ = Theory.check_thy thy; + in Thm (der', args) end; val get_tags = #tags o rep_thm; @@ -1606,6 +1605,8 @@ (*** Promises ***) +(* promise *) + fun promise future ct = let val {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = rep_cterm ct; @@ -1613,7 +1614,7 @@ val _ = T <> propT andalso raise CTERM ("promise: prop expected", [ct]); val i = serial (); in - Thm (deriv_promise i thy future prop, + Thm (make_deriv false [(i, Promise (future, thy, sorts, prop))] (Pt.promise_proof i prop), {thy_ref = thy_ref, tags = [], maxidx = maxidx, @@ -1623,6 +1624,34 @@ prop = prop}) end; +fun check_promise (i, Promise (future, thy1, shyps1, prop1)) = + let + val thm = transfer thy1 (Future.join future); + val _ = Theory.check_thy thy1; + fun err msg = raise THM ("check_promise: " ^ msg, 0, [thm]); + + val Thm (Deriv {oracle, proof, promises}, {shyps, hyps, tpairs, prop, ...}) = thm; + val _ = null promises orelse err "illegal nested promises"; + val _ = shyps = shyps1 orelse err "bad shyps"; + val _ = null hyps orelse err "bad hyps"; + val _ = null tpairs orelse err "bad tpairs"; + val _ = prop aconv prop1 orelse err "bad prop"; + in (oracle, (i, proof)) end; + + +(* fulfill *) + +fun fulfill (thm as Thm (Deriv {oracle, proof, promises}, args)) = + let + val _ = Future.join_results (map (fn (_, Promise (future, _, _, _)) => future) promises); + val results = map check_promise promises; + + val ora = oracle orelse exists #1 results; + val prf = Pt.fulfill (fold (Inttab.update o #2) results Inttab.empty) proof; + in Thm (make_deriv ora [] prf, args) end; + +val proof_of = fulfill #> (fn Thm (Deriv {proof, ...}, _) => proof); + (*** Oracles ***) @@ -1634,7 +1663,7 @@ if T <> propT then raise THM ("Oracle's result must have type prop: " ^ name, 0, []) else - Thm (deriv_oracle name prop, + Thm (make_deriv true [] (Pt.oracle_proof name prop), {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2), tags = [], maxidx = maxidx,