src/Pure/thm.ML
changeset 32725 57e29093ecfb
parent 32590 95f4f08f950f
child 32726 a900d3cd47cc
     1.1 --- a/src/Pure/thm.ML	Mon Sep 28 12:09:18 2009 +0200
     1.2 +++ b/src/Pure/thm.ML	Mon Sep 28 12:09:55 2009 +0200
     1.3 @@ -124,6 +124,13 @@
     1.4    val hyps_of: thm -> term list
     1.5    val no_prems: thm -> bool
     1.6    val major_prem_of: thm -> term
     1.7 +  val join_proofs: thm list -> unit
     1.8 +  val proof_body_of: thm -> proof_body
     1.9 +  val proof_of: thm -> proof
    1.10 +  val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
    1.11 +  val future: thm future -> cterm -> thm
    1.12 +  val get_name: thm -> string
    1.13 +  val put_name: string -> thm -> thm
    1.14    val axiom: theory -> string -> thm
    1.15    val axioms_of: theory -> (string * thm) list
    1.16    val get_tags: thm -> Properties.T
    1.17 @@ -142,13 +149,6 @@
    1.18    val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
    1.19    val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
    1.20    val rename_boundvars: term -> term -> thm -> thm
    1.21 -  val join_proofs: thm list -> unit
    1.22 -  val proof_body_of: thm -> proof_body
    1.23 -  val proof_of: thm -> proof
    1.24 -  val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
    1.25 -  val future: thm future -> cterm -> thm
    1.26 -  val get_name: thm -> string
    1.27 -  val put_name: string -> thm -> thm
    1.28    val extern_oracles: theory -> xstring list
    1.29    val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
    1.30  end;
    1.31 @@ -505,7 +505,7 @@
    1.32  
    1.33  
    1.34  
    1.35 -(** derivations **)
    1.36 +(** derivations and promised proofs **)
    1.37  
    1.38  fun make_deriv promises oracles thms proof =
    1.39    Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}};
    1.40 @@ -536,6 +536,93 @@
    1.41  fun deriv_rule0 prf = deriv_rule1 I (make_deriv [] [] [] prf);
    1.42  
    1.43  
    1.44 +(* fulfilled proofs *)
    1.45 +
    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_proof (Theory.deref thy_ref)
    1.50 +    (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
    1.51 +and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));
    1.52 +
    1.53 +val join_proofs = Pt.join_bodies o map fulfill_body;
    1.54 +
    1.55 +fun proof_body_of thm = (Pt.join_bodies [raw_body thm]; fulfill_body thm);
    1.56 +val proof_of = Pt.proof_of o proof_body_of;
    1.57 +
    1.58 +
    1.59 +(* derivation status *)
    1.60 +
    1.61 +fun status_of (Thm (Deriv {promises, body}, _)) =
    1.62 +  let
    1.63 +    val ps = map (Future.peek o snd) promises;
    1.64 +    val bodies = body ::
    1.65 +      map_filter (fn SOME (Exn.Result th) => SOME (raw_body th) | _ => NONE) ps;
    1.66 +    val {oracle, unfinished, failed} = Pt.status_of bodies;
    1.67 +  in
    1.68 +   {oracle = oracle,
    1.69 +    unfinished = unfinished orelse exists is_none ps,
    1.70 +    failed = failed orelse exists (fn SOME (Exn.Exn _) => true | _ => false) ps}
    1.71 +  end;
    1.72 +
    1.73 +
    1.74 +(* future rule *)
    1.75 +
    1.76 +fun future_result i orig_thy orig_shyps orig_prop raw_thm =
    1.77 +  let
    1.78 +    val _ = Theory.check_thy orig_thy;
    1.79 +    val thm = strip_shyps (transfer orig_thy raw_thm);
    1.80 +    val _ = Theory.check_thy orig_thy;
    1.81 +    fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
    1.82 +
    1.83 +    val Thm (Deriv {promises, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
    1.84 +    val _ = prop aconv orig_prop orelse err "bad prop";
    1.85 +    val _ = null tpairs orelse err "bad tpairs";
    1.86 +    val _ = null hyps orelse err "bad hyps";
    1.87 +    val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
    1.88 +    val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies";
    1.89 +    val _ = fulfill_bodies (map #2 promises);
    1.90 +  in thm end;
    1.91 +
    1.92 +fun future future_thm ct =
    1.93 +  let
    1.94 +    val Cterm {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = ct;
    1.95 +    val thy = Context.reject_draft (Theory.deref thy_ref);
    1.96 +    val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
    1.97 +
    1.98 +    val i = serial ();
    1.99 +    val future = future_thm |> Future.map (future_result i thy sorts prop);
   1.100 +  in
   1.101 +    Thm (make_deriv [(i, future)] [] [] (Pt.promise_proof thy i prop),
   1.102 +     {thy_ref = thy_ref,
   1.103 +      tags = [],
   1.104 +      maxidx = maxidx,
   1.105 +      shyps = sorts,
   1.106 +      hyps = [],
   1.107 +      tpairs = [],
   1.108 +      prop = prop})
   1.109 +  end;
   1.110 +
   1.111 +
   1.112 +(* closed derivations with official name *)
   1.113 +
   1.114 +fun get_name thm =
   1.115 +  Pt.get_name (hyps_of thm) (prop_of thm) (Pt.proof_of (raw_body thm));
   1.116 +
   1.117 +fun put_name name (thm as Thm (der, args)) =
   1.118 +  let
   1.119 +    val Deriv {promises, body} = der;
   1.120 +    val {thy_ref, hyps, prop, tpairs, ...} = args;
   1.121 +    val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
   1.122 +
   1.123 +    val ps = map (apsnd (Future.map proof_body_of)) promises;
   1.124 +    val thy = Theory.deref thy_ref;
   1.125 +    val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
   1.126 +    val der' = make_deriv [] [] [pthm] proof;
   1.127 +    val _ = Theory.check_thy thy;
   1.128 +  in Thm (der', args) end;
   1.129 +
   1.130 +
   1.131  
   1.132  (** Axioms **)
   1.133  
   1.134 @@ -1610,96 +1697,6 @@
   1.135  
   1.136  
   1.137  
   1.138 -(*** Future theorems -- proofs with promises ***)
   1.139 -
   1.140 -(* fulfilled proofs *)
   1.141 -
   1.142 -fun raw_body (Thm (Deriv {body, ...}, _)) = body;
   1.143 -
   1.144 -fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
   1.145 -  Pt.fulfill_proof (Theory.deref thy_ref)
   1.146 -    (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
   1.147 -and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));
   1.148 -
   1.149 -val join_proofs = Pt.join_bodies o map fulfill_body;
   1.150 -
   1.151 -fun proof_body_of thm = (Pt.join_bodies [raw_body thm]; fulfill_body thm);
   1.152 -val proof_of = Pt.proof_of o proof_body_of;
   1.153 -
   1.154 -
   1.155 -(* derivation status *)
   1.156 -
   1.157 -fun status_of (Thm (Deriv {promises, body}, _)) =
   1.158 -  let
   1.159 -    val ps = map (Future.peek o snd) promises;
   1.160 -    val bodies = body ::
   1.161 -      map_filter (fn SOME (Exn.Result th) => SOME (raw_body th) | _ => NONE) ps;
   1.162 -    val {oracle, unfinished, failed} = Pt.status_of bodies;
   1.163 -  in
   1.164 -   {oracle = oracle,
   1.165 -    unfinished = unfinished orelse exists is_none ps,
   1.166 -    failed = failed orelse exists (fn SOME (Exn.Exn _) => true | _ => false) ps}
   1.167 -  end;
   1.168 -
   1.169 -
   1.170 -(* future rule *)
   1.171 -
   1.172 -fun future_result i orig_thy orig_shyps orig_prop raw_thm =
   1.173 -  let
   1.174 -    val _ = Theory.check_thy orig_thy;
   1.175 -    val thm = strip_shyps (transfer orig_thy raw_thm);
   1.176 -    val _ = Theory.check_thy orig_thy;
   1.177 -    fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
   1.178 -
   1.179 -    val Thm (Deriv {promises, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
   1.180 -    val _ = prop aconv orig_prop orelse err "bad prop";
   1.181 -    val _ = null tpairs orelse err "bad tpairs";
   1.182 -    val _ = null hyps orelse err "bad hyps";
   1.183 -    val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
   1.184 -    val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies";
   1.185 -    val _ = fulfill_bodies (map #2 promises);
   1.186 -  in thm end;
   1.187 -
   1.188 -fun future future_thm ct =
   1.189 -  let
   1.190 -    val Cterm {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = ct;
   1.191 -    val thy = Context.reject_draft (Theory.deref thy_ref);
   1.192 -    val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
   1.193 -
   1.194 -    val i = serial ();
   1.195 -    val future = future_thm |> Future.map (future_result i thy sorts prop);
   1.196 -  in
   1.197 -    Thm (make_deriv [(i, future)] [] [] (Pt.promise_proof thy i prop),
   1.198 -     {thy_ref = thy_ref,
   1.199 -      tags = [],
   1.200 -      maxidx = maxidx,
   1.201 -      shyps = sorts,
   1.202 -      hyps = [],
   1.203 -      tpairs = [],
   1.204 -      prop = prop})
   1.205 -  end;
   1.206 -
   1.207 -
   1.208 -(* closed derivations with official name *)
   1.209 -
   1.210 -fun get_name thm =
   1.211 -  Pt.get_name (hyps_of thm) (prop_of thm) (Pt.proof_of (raw_body thm));
   1.212 -
   1.213 -fun put_name name (thm as Thm (der, args)) =
   1.214 -  let
   1.215 -    val Deriv {promises, body} = der;
   1.216 -    val {thy_ref, hyps, prop, tpairs, ...} = args;
   1.217 -    val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
   1.218 -
   1.219 -    val ps = map (apsnd (Future.map proof_body_of)) promises;
   1.220 -    val thy = Theory.deref thy_ref;
   1.221 -    val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
   1.222 -    val der' = make_deriv [] [] [pthm] proof;
   1.223 -    val _ = Theory.check_thy thy;
   1.224 -  in Thm (der', args) end;
   1.225 -
   1.226 -
   1.227 -
   1.228  (*** Oracles ***)
   1.229  
   1.230  (* oracle rule *)