author | wenzelm |
Thu, 18 Sep 2008 14:06:56 +0200 | |
changeset 28288 | 09c812966e7f |
permissions | -rw-r--r-- |
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; |