1(* ========================================================================= *) 2(* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS *) 3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6signature Rule = 7sig 8 9(* ------------------------------------------------------------------------- *) 10(* An equation consists of two terms (t,u) plus a theorem (stronger than) *) 11(* t = u \/ C. *) 12(* ------------------------------------------------------------------------- *) 13 14type equation = (Term.term * Term.term) * Thm.thm 15 16val ppEquation : equation Print.pp 17 18val equationToString : equation -> string 19 20(* Returns t = u if the equation theorem contains this literal *) 21val equationLiteral : equation -> Literal.literal option 22 23val reflEqn : Term.term -> equation 24 25val symEqn : equation -> equation 26 27val transEqn : equation -> equation -> equation 28 29(* ------------------------------------------------------------------------- *) 30(* A conversion takes a term t and either: *) 31(* 1. Returns a term u together with a theorem (stronger than) t = u \/ C. *) 32(* 2. Raises an Error exception. *) 33(* ------------------------------------------------------------------------- *) 34 35type conv = Term.term -> Term.term * Thm.thm 36 37val allConv : conv 38 39val noConv : conv 40 41val thenConv : conv -> conv -> conv 42 43val orelseConv : conv -> conv -> conv 44 45val tryConv : conv -> conv 46 47val repeatConv : conv -> conv 48 49val firstConv : conv list -> conv 50 51val everyConv : conv list -> conv 52 53val rewrConv : equation -> Term.path -> conv 54 55val pathConv : conv -> Term.path -> conv 56 57val subtermConv : conv -> int -> conv 58 59val subtermsConv : conv -> conv (* All function arguments *) 60 61(* ------------------------------------------------------------------------- *) 62(* Applying a conversion to every subterm, with some traversal strategy. *) 63(* ------------------------------------------------------------------------- *) 64 65val bottomUpConv : conv -> conv 66 67val topDownConv : conv -> conv 68 69val repeatTopDownConv : conv -> conv (* useful for rewriting *) 70 71(* ------------------------------------------------------------------------- *) 72(* A literule (bad pun) takes a literal L and either: *) 73(* 1. Returns a literal L' with a theorem (stronger than) ~L \/ L' \/ C. *) 74(* 2. Raises an Error exception. *) 75(* ------------------------------------------------------------------------- *) 76 77type literule = Literal.literal -> Literal.literal * Thm.thm 78 79val allLiterule : literule 80 81val noLiterule : literule 82 83val thenLiterule : literule -> literule -> literule 84 85val orelseLiterule : literule -> literule -> literule 86 87val tryLiterule : literule -> literule 88 89val repeatLiterule : literule -> literule 90 91val firstLiterule : literule list -> literule 92 93val everyLiterule : literule list -> literule 94 95val rewrLiterule : equation -> Term.path -> literule 96 97val pathLiterule : conv -> Term.path -> literule 98 99val argumentLiterule : conv -> int -> literule 100 101val allArgumentsLiterule : conv -> literule 102 103(* ------------------------------------------------------------------------- *) 104(* A rule takes one theorem and either deduces another or raises an Error *) 105(* exception. *) 106(* ------------------------------------------------------------------------- *) 107 108type rule = Thm.thm -> Thm.thm 109 110val allRule : rule 111 112val noRule : rule 113 114val thenRule : rule -> rule -> rule 115 116val orelseRule : rule -> rule -> rule 117 118val tryRule : rule -> rule 119 120val changedRule : rule -> rule 121 122val repeatRule : rule -> rule 123 124val firstRule : rule list -> rule 125 126val everyRule : rule list -> rule 127 128val literalRule : literule -> Literal.literal -> rule 129 130val rewrRule : equation -> Literal.literal -> Term.path -> rule 131 132val pathRule : conv -> Literal.literal -> Term.path -> rule 133 134val literalsRule : literule -> LiteralSet.set -> rule 135 136val allLiteralsRule : literule -> rule 137 138val convRule : conv -> rule (* All arguments of all literals *) 139 140(* ------------------------------------------------------------------------- *) 141(* *) 142(* --------- reflexivity *) 143(* x = x *) 144(* ------------------------------------------------------------------------- *) 145 146val reflexivityRule : Term.term -> Thm.thm 147 148val reflexivity : Thm.thm 149 150(* ------------------------------------------------------------------------- *) 151(* *) 152(* --------------------- symmetry *) 153(* ~(x = y) \/ y = x *) 154(* ------------------------------------------------------------------------- *) 155 156val symmetryRule : Term.term -> Term.term -> Thm.thm 157 158val symmetry : Thm.thm 159 160(* ------------------------------------------------------------------------- *) 161(* *) 162(* --------------------------------- transitivity *) 163(* ~(x = y) \/ ~(y = z) \/ x = z *) 164(* ------------------------------------------------------------------------- *) 165 166val transitivity : Thm.thm 167 168(* ------------------------------------------------------------------------- *) 169(* *) 170(* ---------------------------------------------- functionCongruence (f,n) *) 171(* ~(x0 = y0) \/ ... \/ ~(x{n-1} = y{n-1}) \/ *) 172(* f x0 ... x{n-1} = f y0 ... y{n-1} *) 173(* ------------------------------------------------------------------------- *) 174 175val functionCongruence : Term.function -> Thm.thm 176 177(* ------------------------------------------------------------------------- *) 178(* *) 179(* ---------------------------------------------- relationCongruence (R,n) *) 180(* ~(x0 = y0) \/ ... \/ ~(x{n-1} = y{n-1}) \/ *) 181(* ~R x0 ... x{n-1} \/ R y0 ... y{n-1} *) 182(* ------------------------------------------------------------------------- *) 183 184val relationCongruence : Atom.relation -> Thm.thm 185 186(* ------------------------------------------------------------------------- *) 187(* x = y \/ C *) 188(* -------------- symEq (x = y) *) 189(* y = x \/ C *) 190(* ------------------------------------------------------------------------- *) 191 192val symEq : Literal.literal -> rule 193 194(* ------------------------------------------------------------------------- *) 195(* ~(x = y) \/ C *) 196(* ----------------- symNeq ~(x = y) *) 197(* ~(y = x) \/ C *) 198(* ------------------------------------------------------------------------- *) 199 200val symNeq : Literal.literal -> rule 201 202(* ------------------------------------------------------------------------- *) 203(* sym (x = y) = symEq (x = y) /\ sym ~(x = y) = symNeq ~(x = y) *) 204(* ------------------------------------------------------------------------- *) 205 206val sym : Literal.literal -> rule 207 208(* ------------------------------------------------------------------------- *) 209(* ~(x = x) \/ C *) 210(* ----------------- removeIrrefl *) 211(* C *) 212(* *) 213(* where all irreflexive equalities. *) 214(* ------------------------------------------------------------------------- *) 215 216val removeIrrefl : rule 217 218(* ------------------------------------------------------------------------- *) 219(* x = y \/ y = x \/ C *) 220(* ----------------------- removeSym *) 221(* x = y \/ C *) 222(* *) 223(* where all duplicate copies of equalities and disequalities are removed. *) 224(* ------------------------------------------------------------------------- *) 225 226val removeSym : rule 227 228(* ------------------------------------------------------------------------- *) 229(* ~(v = t) \/ C *) 230(* ----------------- expandAbbrevs *) 231(* C[t/v] *) 232(* *) 233(* where t must not contain any occurrence of the variable v. *) 234(* ------------------------------------------------------------------------- *) 235 236val expandAbbrevs : rule 237 238(* ------------------------------------------------------------------------- *) 239(* simplify = isTautology + expandAbbrevs + removeSym *) 240(* ------------------------------------------------------------------------- *) 241 242val simplify : Thm.thm -> Thm.thm option 243 244(* ------------------------------------------------------------------------- *) 245(* C *) 246(* -------- freshVars *) 247(* C[s] *) 248(* *) 249(* where s is a renaming substitution chosen so that all of the variables in *) 250(* C are replaced by fresh variables. *) 251(* ------------------------------------------------------------------------- *) 252 253val freshVars : rule 254 255(* ------------------------------------------------------------------------- *) 256(* C *) 257(* ---------------------------- factor *) 258(* C_s_1, C_s_2, ..., C_s_n *) 259(* *) 260(* where each s_i is a substitution that factors C, meaning that the theorem *) 261(* *) 262(* C_s_i = (removeIrrefl o removeSym o Thm.subst s_i) C *) 263(* *) 264(* has fewer literals than C. *) 265(* *) 266(* Also, if s is any substitution that factors C, then one of the s_i will *) 267(* result in a theorem C_s_i that strictly subsumes the theorem C_s. *) 268(* ------------------------------------------------------------------------- *) 269 270val factor' : Thm.clause -> Subst.subst list 271 272val factor : Thm.thm -> Thm.thm list 273 274end 275