equal
deleted
inserted
replaced

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; 