Lines Matching defs:fm
41 | simplify1 (Not (Not fm)) = fm
61 | simplify1 (fm as Forall (x, p)) = if mem x (FV p) then fm else p
62 | simplify1 (fm as Exists (x, p)) = if mem x (FV p) then fm else p
63 | simplify1 fm = fm;
72 | simplify fm = fm;
85 | nnf fm = fm
95 | nnf' fm = Not fm;
101 fun pullquants fm =
102 (case fm of
103 And (Forall (x,p), Forall (y,q)) => pullquant_2 fm Forall And x y p q
104 | Or (Exists (x,p), Exists (y,q)) => pullquant_2 fm Exists Or x y p q
105 | And (Forall (x,p), q) => pullquant_l fm Forall And x p q
106 | And (p, Forall (x,q)) => pullquant_r fm Forall And x p q
107 | Or (Forall (x,p), q) => pullquant_l fm Forall Or x p q
108 | Or (p, Forall (x,q)) => pullquant_r fm Forall Or x p q
109 | And (Exists (x,p), q) => pullquant_l fm Exists And x p q
110 | And (p, Exists (x,q)) => pullquant_r fm Exists And x p q
111 | Or (Exists (x,p), q) => pullquant_l fm Exists Or x p q
112 | Or (p, Exists (x,q)) => pullquant_r fm Exists Or x p q
113 | _ => fm)
114 and pullquant_l fm Q C x p q =
116 val x' = variant x (FV fm)
120 and pullquant_r fm Q C x p q =
122 val x' = variant x (FV fm)
126 and pullquant_2 fm Q C x y p q =
128 val x' = variant x (FV fm)
138 | prenex fm = fm;
156 | skolem _ fm = fm
165 fun skolemize fm = skolem (function_names fm) fm;
191 | push fm = [[fm]];
195 | simpcnf fm = List.filter (non tautologous) (push fm);
222 val fm = list_mk_conj fms
223 val rels = relations fm
224 val funs = functions fm