Metis/src/Normalize.sml

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