src/Pure/deriv.ML
author wenzelm
Thu, 18 Sep 2008 14:06:56 +0200
changeset 28288 09c812966e7f
permissions -rw-r--r--
added deriv.ML: Abstract derivations based on raw proof terms.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28288
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/deriv.ML
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
     4
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
     5
Abstract derivations based on raw proof terms.
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
     6
*)
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
     7
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
     8
signature DERIV =
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
     9
sig
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    10
  type T
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    11
  val oracle_of: T -> bool
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    12
  val proof_of: T -> Proofterm.proof
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    13
  val uncond_rule: (Proofterm.proof -> Proofterm.proof) -> T -> T
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    14
  val rule0: Proofterm.proof -> T
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    15
  val rule1: (Proofterm.proof -> Proofterm.proof) -> T -> T
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    16
  val rule2: (Proofterm.proof -> Proofterm.proof -> Proofterm.proof) -> T -> T -> T
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    17
  val oracle: string -> term -> T
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    18
end;
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    19
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    20
structure Deriv: DERIV =
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    21
struct
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    22
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    23
datatype T = Der of bool * Proofterm.proof;
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    24
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    25
fun oracle_of (Der (ora, _)) = ora;
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    26
fun proof_of (Der (_, proof)) = proof;
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    27
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    28
fun uncond_rule f (Der (ora, prf)) = Der (ora, f prf);
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    29
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    30
fun rule0 prf = Der (Proofterm.infer_derivs' I (false, prf));
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    31
fun rule1 f (Der der) = Der (Proofterm.infer_derivs' f der);
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    32
fun rule2 f (Der der1) (Der der2) = Der (Proofterm.infer_derivs f der1 der2);
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    33
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    34
fun oracle name prop = Der (true, Proofterm.oracle_proof name prop);
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    35
09c812966e7f added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
diff changeset
    36
end;