1(* ========================================================================= *)
2(* INTERFACE TO THE LCF-STYLE LOGICAL KERNEL, PLUS SOME DERIVED RULES        *)
3(* Copyright (c) 2001-2004 Joe Hurd.                                         *)
4(* ========================================================================= *)
5
6signature mlibThm =
7sig
8
9type 'a pp = 'a mlibUseful.pp
10
11include mlibKernel
12
13(* Annotated primitive inferences *)
14datatype inference' =
15  Axiom'    of formula list
16| Refl'     of term
17| Assume'   of formula
18| Inst'     of subst * thm
19| Factor'   of thm
20| Resolve'  of formula * thm * thm
21| Equality' of formula * int list * term * bool * thm
22
23val primitive_inference : inference' -> thm
24
25(* User-friendly destructors *)
26val clause    : thm -> formula list
27val inference : thm -> inference'
28val proof     : thm -> (thm * inference') list
29
30val dest_axiom : thm -> formula list
31val is_axiom   : thm -> bool
32
33(* Theorem operations *)
34val thm_compare : thm * thm -> order
35val thm_map     : (thm * 'a list -> 'a) -> thm -> 'a
36val thm_foldr   : (thm * 'a -> 'a) -> 'a -> thm -> 'a
37
38(* Contradictions and units *)
39val is_contradiction : thm -> bool
40val dest_unit        : thm -> formula
41val is_unit          : thm -> bool
42val dest_unit_eq     : thm -> term * term
43val is_unit_eq       : thm -> bool
44
45(* Derived rules and theorems *)
46val CONTR          : formula -> thm -> thm
47val WEAKEN         : formula list -> thm -> thm
48val FRESH_VARS     : thm -> thm
49val FRESH_VARSL    : thm list -> thm list
50val UNIT_SQUASH    : thm -> thm
51val REFLEXIVITY    : thm
52val SYMMETRY       : thm
53val TRANSITIVITY   : thm
54val FUN_CONGRUENCE : string * int -> thm
55val REL_CONGRUENCE : string * int -> thm
56val SYM            : formula -> thm -> thm
57val EQ_FACTOR      : thm -> thm
58val REWR           : thm * bool -> thm * formula * int list -> thm
59val DEPTH1         : (term->thm*term*bool) -> thm * formula -> thm * formula
60val DEPTH          : (term->thm*term*bool) -> thm -> thm
61
62(* Converting to clauses *)
63val axiomatize : formula -> thm list
64val eq_axioms  : formula -> thm list
65val clauses    : formula -> {thms : thm list, hyps : thm list}
66
67(* Pretty-printing of theorems and inferences *)
68val pp_thm               : thm pp
69val pp_inference         : inference pp
70val pp_inference'        : inference' pp
71val pp_proof             : (thm * inference') list pp
72val thm_to_string'       : int -> thm -> string        (* purely functional *)
73val inference_to_string' : int -> inference' -> string
74val proof_to_string'     : int -> (thm * inference') list -> string
75val thm_to_string        : thm -> string               (* uses !LINE_LENGTH *)
76val inference_to_string  : inference' -> string
77val proof_to_string      : (thm * inference') list -> string
78
79end
80