src/metis/normalForms.sml

731 fun sub_cnf f con defs (a, b) =
733       val (defs, a) = f defs a
734       val (defs, b) = f defs b
737       (defs, tm)
740 fun def_step (defs, tm) =
741   case List.find (fn (_, b) => b = tm) defs of NONE
742     => let val g = genvar bool in ((g, tm) :: defs, g) end
743   | SOME (v, _) => (defs, v);
745 fun gen_cnf defs tm =
747     def_step (sub_cnf gen_cnf conjunction defs (dest_conj tm))
749     def_step (sub_cnf gen_cnf disjunction defs (dest_disj tm))
751     def_step (sub_cnf gen_cnf beq defs (dest_beq tm))
753     (defs, tm);
755 fun disj_cnf defs tm =
756   if is_disj tm then sub_cnf disj_cnf disjunction defs (dest_disj tm)
757   else gen_cnf defs tm;
759 fun conj_cnf defs tm =
760   if is_conj tm then sub_cnf conj_cnf conjunction defs (dest_conj tm)
761   else disj_cnf defs tm;
782     val (defs, tm) = conj_cnf [] tm
783     val (vs, eqs) = unzip (map (fn (v, d) => (v, mk_eq (v, d))) (rev defs))
786     (defs, tm)
791     val (defs, tm) = gen_def_cnf tm
793     val th = QCONV (funpow (length defs) push ALL_CONV) tm
1128   fun mk_def defs vs tm =
1132       case List.find (aconv def_tm o fst) defs of
1137           (defs, vs, tm, def, NONE)
1145           val defs = (def_tm,(vs,tm,def)) :: defs
1147           (defs, vs, tm, def, SOME def_th)
1163   fun rename defs vs tm =
1166       val (defs,vs,tm,def,def_th) = mk_def defs vs tm
1169       (defs, CONV_RULE (TOP_DEPTH_CONV convish), def_th)
1183   fun extract_bools (defs,th,acc) =
1186       val (defs,rule,vth) = rename defs vs tm
1189       (defs, rule th, acc)
1193 fun extract_lambdas (defs,th,acc) =
1196     val (defs,rule,vth) = rename defs vs tm
1199     (defs, rule th, acc)
1228 fun min_cnf_prep defs acc [] = (defs, rev acc)
1229   | min_cnf_prep defs acc (th :: ths) =
1234     val (defs,th,bs) = repeat extract_bools (defs,th,[])
1235     val (defs,th,ls) = repeat extract_lambdas (defs,th,[])
1238     min_cnf_prep defs (th :: acc) ths
1346 fun min_cnf_norm defs acc [] = (defs, rev acc)
1347   | min_cnf_norm defs acc (th :: ths) =
1362         val (defs,rule,dth) = rename defs vs tm
1365         min_cnf_norm defs acc (rule th :: ths)
1368       min_cnf_norm defs (simple_cnf_rule th :: acc) ths
1375     val defs = []
1376     val (defs,ths) = min_cnf_prep defs [] ths
1377     val (defs,ths) = min_cnf_norm defs [] ths
1378     val cs = map (lhs o hd o hyp o #3 o snd) defs