Lines Matching defs:inf
913 fun parentsInference inf =
914 case inf of
925 fun parentsThm (Thm (_,inf)) = parentsInference inf;
929 fun destThm (Thm (fm,inf)) = (toFormula fm, inf);
956 val (fm,inf) = destThm th
960 val acc = (fm,inf,fms) :: acc
977 fun toStringInference inf =
978 case inf of
1127 fun simp fm inf =
1128 case simp_sub fm inf of
1129 NONE => simp_top fm inf
1130 | SOME (fm,inf) => try_simp_top fm inf
1132 and try_simp_top fm inf =
1133 case simp_top fm inf of
1134 NONE => SOME (fm,inf)
1137 and simp_top fm inf =
1145 val inf = th :: inf
1147 try_simp_top fm inf
1155 val inf = th :: inf
1157 try_simp_top fm inf
1165 val inf = th :: inf
1167 try_simp_top fm inf
1174 val inf = th :: inf
1176 try_simp_top fm inf
1179 and simp_sub fm inf =
1182 (case simp_set s inf of
1184 | SOME (l,inf) => SOME (AndList l, inf))
1186 (case simp_set s inf of
1188 | SOME (l,inf) => SOME (OrList l, inf))
1190 (case simp_set s inf of
1192 | SOME (l,inf) => SOME (XorPolarityList (p,l), inf))
1194 (case simp f inf of
1196 | SOME (f,inf) => SOME (ExistsSet (n,f), inf))
1198 (case simp f inf of
1200 | SOME (f,inf) => SOME (ForallSet (n,f), inf))
1203 and simp_set s inf =
1205 val (changed,l,inf) = Set.foldr simp_set_elt (false,[],inf) s
1207 if changed then SOME (l,inf) else NONE
1210 and simp_set_elt (fm,(changed,l,inf)) =
1211 case simp fm inf of
1212 NONE => (changed, fm :: l, inf)
1213 | SOME (fm,inf) => (true, fm :: l, inf)
1219 val inf = Simplify (th,ths)
1221 Thm (fm,inf)
1264 val inf = Definition (rel,fm)
1268 Thm (fm,inf)
1289 fun def_cnf_clause inf (fm,acc) =
1292 val th = Thm (fm,inf)
1344 val inf = Clausify th
1348 | False => def_cnf_inconsistent (Thm (fm,inf))
1351 val inf = Conjunct (Thm (fm,inf))
1352 val cls = Set.foldl (def_cnf_clause inf) cls s
1356 | fm => def_cnf (def_cnf_clause inf (fm,cls)) simp ths