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