proof_body/pthm: removed redundant types field;
authorwenzelm
Sun Nov 16 22:12:41 2008 +0100 (2008-11-16)
changeset 2881580bb72a0f577
parent 28814 463c9e9111ae
child 28816 d651b0b15835
proof_body/pthm: removed redundant types field;
fold_proof_atoms: unified recursive case with fold_body_thms;
tuned signature;
src/Pure/proofterm.ML
     1.1 --- a/src/Pure/proofterm.ML	Sun Nov 16 20:03:42 2008 +0100
     1.2 +++ b/src/Pure/proofterm.ML	Sun Nov 16 22:12:41 2008 +0100
     1.3 @@ -25,7 +25,7 @@
     1.4     | PThm of serial * ((string * term * typ list option) * proof_body Lazy.T)
     1.5    and proof_body = PBody of
     1.6      {oracles: (string * term) OrdList.T,
     1.7 -     thms: (serial * ((string * term * typ list option) * proof_body Lazy.T)) OrdList.T,
     1.8 +     thms: (serial * (string * term * proof_body Lazy.T)) OrdList.T,
     1.9       proof: proof}
    1.10  
    1.11    val %> : proof * term -> proof
    1.12 @@ -35,19 +35,16 @@
    1.13  sig
    1.14    include BASIC_PROOFTERM
    1.15  
    1.16 -  val proof_of: proof_body -> proof
    1.17 +  type oracle = string * term
    1.18 +  type pthm = serial * (string * term * proof_body Lazy.T)
    1.19    val force_body: proof_body Lazy.T ->
    1.20 -   {oracles: (string * term) OrdList.T,
    1.21 -    thms: (serial * ((string * term * typ list option) * proof_body Lazy.T)) OrdList.T,
    1.22 -    proof: proof}
    1.23 +    {oracles: oracle OrdList.T, thms: pthm OrdList.T, proof: proof}
    1.24    val force_proof: proof_body Lazy.T -> proof
    1.25 -  val fold_body_thms: ((string * term * typ list option) * proof_body -> 'a -> 'a) ->
    1.26 -    proof_body list -> 'a -> 'a
    1.27 +  val proof_of: proof_body -> proof
    1.28 +  val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
    1.29    val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
    1.30  
    1.31 -  type oracle = string * term
    1.32    val oracle_ord: oracle * oracle -> order
    1.33 -  type pthm = serial * ((string * term * typ list option) * proof_body Lazy.T)
    1.34    val thm_ord: pthm * pthm -> order
    1.35    val make_proof_body: proof -> proof_body
    1.36    val merge_oracles: oracle OrdList.T -> oracle OrdList.T -> oracle OrdList.T
    1.37 @@ -149,9 +146,12 @@
    1.38   | PThm of serial * ((string * term * typ list option) * proof_body Lazy.T)
    1.39  and proof_body = PBody of
    1.40    {oracles: (string * term) OrdList.T,
    1.41 -   thms: (serial * ((string * term * typ list option) * proof_body Lazy.T)) OrdList.T,
    1.42 +   thms: (serial * (string * term * proof_body Lazy.T)) OrdList.T,
    1.43     proof: proof};
    1.44  
    1.45 +type oracle = string * term;
    1.46 +type pthm = serial * (string * term * proof_body Lazy.T);
    1.47 +
    1.48  val force_body = Lazy.force #> (fn PBody args => args);
    1.49  val force_proof = #proof o force_body;
    1.50  
    1.51 @@ -162,13 +162,13 @@
    1.52  
    1.53  fun fold_body_thms f =
    1.54    let
    1.55 -    fun app (PBody {thms, ...}) = thms |> fold (fn (i, (stmt, body)) => fn (x, seen) =>
    1.56 +    fun app (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
    1.57        if Inttab.defined seen i then (x, seen)
    1.58        else
    1.59          let
    1.60            val body' = Lazy.force body;
    1.61            val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
    1.62 -        in (f (stmt, body') x', seen') end);
    1.63 +        in (f (name, prop, body') x', seen') end);
    1.64    in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
    1.65  
    1.66  fun fold_proof_atoms all f =
    1.67 @@ -180,29 +180,23 @@
    1.68        | app (prf as PThm (i, (_, body))) = (fn (x, seen) =>
    1.69            if Inttab.defined seen i then (x, seen)
    1.70            else
    1.71 -            let val res = (f prf x, Inttab.update (i, ()) seen)
    1.72 -            in if all then app (force_proof body) res else res
    1.73 -          end)
    1.74 +            let val (x', seen') =
    1.75 +              (if all then app (force_proof body) else I) (x, Inttab.update (i, ()) seen)
    1.76 +            in (f prf x', seen') end)
    1.77        | app prf = (fn (x, seen) => (f prf x, seen));
    1.78    in fn prfs => fn x => #1 (fold app prfs (x, Inttab.empty)) end;
    1.79  
    1.80  
    1.81 -(* atom kinds *)
    1.82 -
    1.83 -type oracle = string * term;
    1.84 -val oracle_ord = prod_ord fast_string_ord Term.fast_term_ord;
    1.85 +(* proof body *)
    1.86  
    1.87 -type pthm = serial * ((string * term * typ list option) * proof_body Lazy.T);
    1.88 +val oracle_ord = prod_ord fast_string_ord Term.fast_term_ord;
    1.89  fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i);
    1.90  
    1.91 -
    1.92 -(* proof body *)
    1.93 -
    1.94  fun make_body prf =
    1.95    let
    1.96      val (oracles, thms) = fold_proof_atoms false
    1.97        (fn Oracle (s, prop, _) => apfst (cons (s, prop))
    1.98 -        | PThm thm => apsnd (cons thm)
    1.99 +        | PThm (i, ((name, prop, _), body)) => apsnd (cons (i, (name, prop, body)))
   1.100          | _ => I) [prf] ([], []);
   1.101    in (OrdList.make oracle_ord oracles, OrdList.make thm_ord thms) end;
   1.102  
   1.103 @@ -217,7 +211,7 @@
   1.104  val merge_thms = OrdList.union thm_ord;
   1.105  
   1.106  fun merge_body (oracles1, thms1) (oracles2, thms2) =
   1.107 - (merge_oracles oracles1 oracles2, merge_thms thms1 thms2);
   1.108 +  (merge_oracles oracles1 oracles2, merge_thms thms1 thms2);
   1.109  
   1.110  
   1.111  (***** proof objects with different levels of detail *****)
   1.112 @@ -1226,20 +1220,19 @@
   1.113          #4 (shrink_proof thy [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)))
   1.114        else MinProof;
   1.115  
   1.116 -    fun new_prf () = (serial (), ((name, prop, NONE),
   1.117 -      Lazy.lazy (fn () =>
   1.118 -        fulfill_proof promises (PBody {oracles = oracles0, thms = thms0, proof = proof0}))));
   1.119 +    fun new_prf () = (serial (), name, prop, Lazy.lazy (fn () =>
   1.120 +      fulfill_proof promises (PBody {oracles = oracles0, thms = thms0, proof = proof0})));
   1.121  
   1.122 -    val head =
   1.123 +    val (i, name, prop, body') =
   1.124        (case strip_combt (fst (strip_combP prf)) of
   1.125          (PThm (i, ((old_name, prop', NONE), body')), args') =>
   1.126 -          if (old_name = "" orelse old_name = name) andalso
   1.127 -             prop = prop' andalso args = args'
   1.128 -          then (i, ((name, prop, NONE), body'))
   1.129 +          if (old_name = "" orelse old_name = name) andalso prop = prop' andalso args = args'
   1.130 +          then (i, name, prop, body')
   1.131            else new_prf ()
   1.132 -      | _ => new_prf ())
   1.133 +      | _ => new_prf ());
   1.134 +    val head = PThm (i, ((name, prop, NONE), body'));
   1.135    in
   1.136 -    (head, proof_combP (proof_combt' (PThm head, args), map Hyp hyps))
   1.137 +    ((i, (name, prop, body')), proof_combP (proof_combt' (head, args), map Hyp hyps))
   1.138    end;
   1.139  
   1.140  fun get_name hyps prop prf =