src/Pure/deriv.ML
changeset 28288 09c812966e7f
equal deleted inserted replaced
28287:c86fa4e0aedb 28288:09c812966e7f
       
     1 (*  Title:      Pure/deriv.ML
       
     2     ID:         $Id$
       
     3     Author:     Makarius
       
     4 
       
     5 Abstract derivations based on raw proof terms.
       
     6 *)
       
     7 
       
     8 signature DERIV =
       
     9 sig
       
    10   type T
       
    11   val oracle_of: T -> bool
       
    12   val proof_of: T -> Proofterm.proof
       
    13   val uncond_rule: (Proofterm.proof -> Proofterm.proof) -> T -> T
       
    14   val rule0: Proofterm.proof -> T
       
    15   val rule1: (Proofterm.proof -> Proofterm.proof) -> T -> T
       
    16   val rule2: (Proofterm.proof -> Proofterm.proof -> Proofterm.proof) -> T -> T -> T
       
    17   val oracle: string -> term -> T
       
    18 end;
       
    19 
       
    20 structure Deriv: DERIV =
       
    21 struct
       
    22 
       
    23 datatype T = Der of bool * Proofterm.proof;
       
    24 
       
    25 fun oracle_of (Der (ora, _)) = ora;
       
    26 fun proof_of (Der (_, proof)) = proof;
       
    27 
       
    28 fun uncond_rule f (Der (ora, prf)) = Der (ora, f prf);
       
    29 
       
    30 fun rule0 prf = Der (Proofterm.infer_derivs' I (false, prf));
       
    31 fun rule1 f (Der der) = Der (Proofterm.infer_derivs' f der);
       
    32 fun rule2 f (Der der1) (Der der2) = Der (Proofterm.infer_derivs f der1 der2);
       
    33 
       
    34 fun oracle name prop = Der (true, Proofterm.oracle_proof name prop);
       
    35 
       
    36 end;