# HG changeset patch # User paulson # Date 1116404651 -7200 # Node ID bc916036cf8482d5cc9991583e0e63d0210d1659 # Parent c71031d7988ce92e513670ee4e942d69a2e15494 new cnf function taking Skolemization theorems as an extra argument diff -r c71031d7988c -r bc916036cf84 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Wed May 18 10:23:47 2005 +0200 +++ b/src/HOL/Tools/meson.ML Wed May 18 10:24:11 2005 +0200 @@ -14,6 +14,7 @@ signature BASIC_MESON = sig val size_of_subgoals : thm -> int + val make_cnf : thm list -> thm -> thm list val make_nnf : thm -> thm val skolemize : thm -> thm val make_clauses : thm list -> thm list @@ -122,32 +123,43 @@ radixstring(26, "A", !name_ref)) in read_instantiate [("x", newname)] sth end; +(*Used with METAHYPS below. There is one assumption, which gets bound to prem + and then normalized via function nf. The normal form is given to resolve_tac, + presumably to instantiate a Boolean variable.*) fun resop nf [prem] = resolve_tac (nf prem) 1; -(*Conjunctive normal form, detecting tautologies early. - Strips universal quantifiers and breaks up conjunctions. *) -fun cnf_aux seen (th,ths) = - if taut_lits (literals(prop_of th) @ seen) - then ths (*tautology ignored*) - else if not (has_consts ["All","op &"] (prop_of th)) - then th::ths (*no work to do, terminate*) - else (*conjunction?*) - cnf_aux seen (th RS conjunct1, - cnf_aux seen (th RS conjunct2, ths)) - handle THM _ => (*universal quant?*) - cnf_aux seen (freeze_spec th, ths) - handle THM _ => (*disjunction?*) - let val tac = - (METAHYPS (resop (cnf_nil seen)) 1) THEN - (fn st' => st' |> +(*Conjunctive normal form, adding clauses from th in front of ths (for foldr). + Detects tautologies early, with "seen" holding the other literals of a clause. + Strips universal quantifiers and breaks up conjunctions. + Eliminates existential quantifiers using skoths: Skolemization theorems.*) +fun cnf skoths (th,ths) = + let fun cnf_aux seen (th,ths) = + if taut_lits (literals(prop_of th) @ seen) + then ths (*tautology ignored*) + else if not (has_consts ["All","Ex","op &"] (prop_of th)) + then th::ths (*no work to do, terminate*) + else (*conjunction?*) + cnf_aux seen (th RS conjunct1, + cnf_aux seen (th RS conjunct2, ths)) + handle THM _ => (*universal quantifier?*) + cnf_aux seen (freeze_spec th, ths) + handle THM _ => (*existential quantifier? Insert Skolem functions.*) + cnf_aux seen (tryres (th,skoths), ths) + handle THM _ => (*disjunction?*) + let val tac = + (METAHYPS (resop (cnf_nil seen)) 1) THEN + (fn st' => st' |> METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1) - in Seq.list_of (tac (th RS disj_forward)) @ ths end -and cnf_nil seen th = (cnf_aux seen (th,[])) + in Seq.list_of (tac (th RS disj_forward)) @ ths end + and cnf_nil seen th = (cnf_aux seen (th,[])) + in + name_ref := 19; (*It's safe to reset this in a top-level call to cnf*) + (cnf skoths (th RS conjunct1, cnf skoths (th RS conjunct2, ths)) + handle THM _ => (*not a conjunction*) cnf_aux [] (th, ths)) + end; -(*Top-level call to cnf -- it's safe to reset name_ref*) -fun cnf (th,ths) = - (name_ref := 19; cnf (th RS conjunct1, cnf (th RS conjunct2, ths)) - handle THM _ => (*not a conjunction*) cnf_aux [] (th, ths)); +fun make_cnf skoths th = cnf skoths (th, []); + (**** Removal of duplicate literals ****) @@ -332,7 +344,7 @@ (*Make clauses from a list of theorems, previously Skolemized and put into nnf. The resulting clauses are HOL disjunctions.*) fun make_clauses ths = - (sort_clauses (map (generalize o nodups) (foldr cnf [] ths))); + (sort_clauses (map (generalize o nodups) (foldr (cnf[]) [] ths))); (*Convert a list of clauses to (contrapositive) Horn clauses*)