src/Pure/deriv.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/deriv.ML	Thu Sep 18 14:06:56 2008 +0200
@@ -0,0 +1,36 @@
+(*  Title:      Pure/deriv.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Abstract derivations based on raw proof terms.
+*)
+
+signature DERIV =
+sig
+  type T
+  val oracle_of: T -> bool
+  val proof_of: T -> Proofterm.proof
+  val uncond_rule: (Proofterm.proof -> Proofterm.proof) -> T -> T
+  val rule0: Proofterm.proof -> T
+  val rule1: (Proofterm.proof -> Proofterm.proof) -> T -> T
+  val rule2: (Proofterm.proof -> Proofterm.proof -> Proofterm.proof) -> T -> T -> T
+  val oracle: string -> term -> T
+end;
+
+structure Deriv: DERIV =
+struct
+
+datatype T = Der of bool * Proofterm.proof;
+
+fun oracle_of (Der (ora, _)) = ora;
+fun proof_of (Der (_, proof)) = proof;
+
+fun uncond_rule f (Der (ora, prf)) = Der (ora, f prf);
+
+fun rule0 prf = Der (Proofterm.infer_derivs' I (false, prf));
+fun rule1 f (Der der) = Der (Proofterm.infer_derivs' f der);
+fun rule2 f (Der der1) (Der der2) = Der (Proofterm.infer_derivs f der1 der2);
+
+fun oracle name prop = Der (true, Proofterm.oracle_proof name prop);
+
+end;