src/Pure/thm.ML
changeset 28804 5d3b1df16353
parent 28675 fb68c0767004
child 28814 463c9e9111ae
     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 +
   1.168 +(* closed derivations with official name *)
   1.169 +
   1.170 +fun get_name thm =
   1.171 +  Pt.get_name (hyps_of thm) (prop_of thm) (proof_term_of thm);
   1.172  
   1.173 -val proof_of = join_deriv #> (fn Thm (Deriv {proof, ...}, _) => proof);
   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