1(* ========================================================================= *) 2(* FIRST ORDER LOGIC FORMULAS *) 3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6signature Formula = 7sig 8 9(* ------------------------------------------------------------------------- *) 10(* A type of first order logic formulas. *) 11(* ------------------------------------------------------------------------- *) 12 13datatype formula = 14 True 15 | False 16 | Atom of Atom.atom 17 | Not of formula 18 | And of formula * formula 19 | Or of formula * formula 20 | Imp of formula * formula 21 | Iff of formula * formula 22 | Forall of Term.var * formula 23 | Exists of Term.var * formula 24 25(* ------------------------------------------------------------------------- *) 26(* Constructors and destructors. *) 27(* ------------------------------------------------------------------------- *) 28 29(* Booleans *) 30 31val mkBoolean : bool -> formula 32 33val destBoolean : formula -> bool 34 35val isBoolean : formula -> bool 36 37val isTrue : formula -> bool 38 39val isFalse : formula -> bool 40 41(* Functions *) 42 43val functions : formula -> NameAritySet.set 44 45val functionNames : formula -> NameSet.set 46 47(* Relations *) 48 49val relations : formula -> NameAritySet.set 50 51val relationNames : formula -> NameSet.set 52 53(* Atoms *) 54 55val destAtom : formula -> Atom.atom 56 57val isAtom : formula -> bool 58 59(* Negations *) 60 61val destNeg : formula -> formula 62 63val isNeg : formula -> bool 64 65val stripNeg : formula -> int * formula 66 67(* Conjunctions *) 68 69val listMkConj : formula list -> formula 70 71val stripConj : formula -> formula list 72 73val flattenConj : formula -> formula list 74 75(* Disjunctions *) 76 77val listMkDisj : formula list -> formula 78 79val stripDisj : formula -> formula list 80 81val flattenDisj : formula -> formula list 82 83(* Equivalences *) 84 85val listMkEquiv : formula list -> formula 86 87val stripEquiv : formula -> formula list 88 89val flattenEquiv : formula -> formula list 90 91(* Universal quantification *) 92 93val destForall : formula -> Term.var * formula 94 95val isForall : formula -> bool 96 97val listMkForall : Term.var list * formula -> formula 98 99val setMkForall : NameSet.set * formula -> formula 100 101val stripForall : formula -> Term.var list * formula 102 103(* Existential quantification *) 104 105val destExists : formula -> Term.var * formula 106 107val isExists : formula -> bool 108 109val listMkExists : Term.var list * formula -> formula 110 111val setMkExists : NameSet.set * formula -> formula 112 113val stripExists : formula -> Term.var list * formula 114 115(* ------------------------------------------------------------------------- *) 116(* The size of a formula in symbols. *) 117(* ------------------------------------------------------------------------- *) 118 119val symbols : formula -> int 120 121(* ------------------------------------------------------------------------- *) 122(* A total comparison function for formulas. *) 123(* ------------------------------------------------------------------------- *) 124 125val compare : formula * formula -> order 126 127val equal : formula -> formula -> bool 128 129(* ------------------------------------------------------------------------- *) 130(* Free variables. *) 131(* ------------------------------------------------------------------------- *) 132 133val freeIn : Term.var -> formula -> bool 134 135val freeVars : formula -> NameSet.set 136 137val freeVarsList : formula list -> NameSet.set 138 139val specialize : formula -> formula 140 141val generalize : formula -> formula 142 143(* ------------------------------------------------------------------------- *) 144(* Substitutions. *) 145(* ------------------------------------------------------------------------- *) 146 147val subst : Subst.subst -> formula -> formula 148 149(* ------------------------------------------------------------------------- *) 150(* The equality relation. *) 151(* ------------------------------------------------------------------------- *) 152 153val mkEq : Term.term * Term.term -> formula 154 155val destEq : formula -> Term.term * Term.term 156 157val isEq : formula -> bool 158 159val mkNeq : Term.term * Term.term -> formula 160 161val destNeq : formula -> Term.term * Term.term 162 163val isNeq : formula -> bool 164 165val mkRefl : Term.term -> formula 166 167val destRefl : formula -> Term.term 168 169val isRefl : formula -> bool 170 171val sym : formula -> formula (* raises Error if given a refl *) 172 173val lhs : formula -> Term.term 174 175val rhs : formula -> Term.term 176 177(* ------------------------------------------------------------------------- *) 178(* Splitting goals. *) 179(* ------------------------------------------------------------------------- *) 180 181val splitGoal : formula -> formula list 182 183(* ------------------------------------------------------------------------- *) 184(* Parsing and pretty-printing. *) 185(* ------------------------------------------------------------------------- *) 186 187type quotation = formula Parse.quotation 188 189val pp : formula Print.pp 190 191val toString : formula -> string 192 193val fromString : string -> formula 194 195val parse : quotation -> formula 196 197end 198