# HG changeset patch # User paulson # Date 1150386647 -7200 # Node ID 7c7e15b271454a02312bf2c4eac69ab24a4db75d # Parent 7546dafb3fc6f77b03fb7849532ebcaaaddc4f63 the "all_theorems" option and some fixes diff -r 7546dafb3fc6 -r 7c7e15b27145 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Thu Jun 15 17:50:30 2006 +0200 +++ b/src/HOL/Tools/meson.ML Thu Jun 15 17:50:47 2006 +0200 @@ -123,7 +123,8 @@ in exists taut_poslit poslits orelse exists (fn t => mem_term (t, neglits)) (HOLogic.false_const :: poslits) - end; + end + handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*) (*** To remove trivial negated equality literals from clauses ***) @@ -154,11 +155,20 @@ (*Simplify a clause by applying reflexivity to its negated equality literals*) fun refl_clause th = let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th)) - in zero_var_indexes (refl_clause_aux neqs th) end; + in zero_var_indexes (refl_clause_aux neqs th) end + handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*) (*** The basic CNF transformation ***) +(*Estimate the number of clauses in order to detect infeasible theorems*) +fun nclauses (Const("Trueprop",_) $ t) = nclauses t + | nclauses (Const("op &",_) $ t $ u) = nclauses t + nclauses u + | nclauses (Const("Ex", _) $ Abs (_,_,t)) = nclauses t + | nclauses (Const("All",_) $ Abs (_,_,t)) = nclauses t + | nclauses (Const("op |",_) $ t $ u) = nclauses t * nclauses u + | nclauses _ = 1; (* literal *) + (*Replaces universally quantified variables by FREE variables -- because assumptions may not contain scheme variables. Later, call "generalize". *) fun freeze_spec th = @@ -179,7 +189,7 @@ Eliminates existential quantifiers using skoths: Skolemization theorems.*) fun cnf skoths (th,ths) = let fun cnf_aux (th,ths) = - if has_meta_conn (prop_of th) then ths (*meta-level: ignore*) + if has_meta_conn (prop_of th) then ths (*meta-level: ignore*) else if not (has_consts ["All","Ex","op &"] (prop_of th)) then th::ths (*no work to do, terminate*) else case head_of (HOLogic.dest_Trueprop (concl_of th)) of @@ -199,7 +209,9 @@ | _ => (*no work to do*) th::ths and cnf_nil th = cnf_aux (th,[]) in - cnf_aux (th,ths) + if nclauses (concl_of th) > 20 + then (Output.debug ("cnf is ignoring: " ^ string_of_thm th); ths) + else cnf_aux (th,ths) end; (*Convert all suitable free variables to schematic variables, @@ -379,15 +391,18 @@ which are needed to avoid the various one-point theorems from generating junk clauses.*) val tag_True = thm "tag_True"; val tag_False = thm "tag_False"; -val nnf_simps = [Ex1_def,Ball_def,Bex_def,tag_True,tag_False] +val nnf_simps = + [simp_implies_def, Ex1_def, Ball_def, Bex_def, tag_True, tag_False, if_True, + if_False, if_cancel, if_eq_cancel, cases_simp]; +val nnf_extra_simps = + thms"split_ifs" @ ex_simps @ all_simps @ simp_thms; val nnf_ss = - HOL_basic_ss addsimps - (nnf_simps @ [if_True, if_False, if_cancel, if_eq_cancel, cases_simp] @ - thms"split_ifs" @ ex_simps @ all_simps @ simp_thms) - addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc]; + HOL_basic_ss addsimps nnf_extra_simps + addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc]; -fun make_nnf th = th |> simplify nnf_ss +fun make_nnf th = th |> rewrite_rule (map safe_mk_meta_eq nnf_simps) + |> simplify nnf_ss (*But this doesn't simplify premises...*) |> make_nnf1 (*Pull existential quantifiers to front. This accomplishes Skolemization for diff -r 7546dafb3fc6 -r 7c7e15b27145 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Thu Jun 15 17:50:30 2006 +0200 +++ b/src/HOL/Tools/res_atp.ML Thu Jun 15 17:50:47 2006 +0200 @@ -39,10 +39,12 @@ val run_relevance_filter: bool ref val run_blacklist_filter: bool ref val invoke_atp_ml : ProofContext.context * thm -> unit + val add_all : unit -> unit val add_claset : unit -> unit val add_simpset : unit -> unit val add_clasimp : unit -> unit val add_atpset : unit -> unit + val rm_all : unit -> unit val rm_claset : unit -> unit val rm_simpset : unit -> unit val rm_atpset : unit -> unit @@ -133,13 +135,16 @@ else error ("No such directory: " ^ !destdir) end; +val include_all = ref false; val include_simpset = ref false; val include_claset = ref false; val include_atpset = ref true; +val add_all = (fn () => include_all:=true); val add_simpset = (fn () => include_simpset:=true); val add_claset = (fn () => include_claset:=true); val add_clasimp = (fn () => (include_simpset:=true;include_claset:=true)); val add_atpset = (fn () => include_atpset:=true); +val rm_all = (fn () => include_all:=false); val rm_simpset = (fn () => include_simpset:=false); val rm_claset = (fn () => include_claset:=false); val rm_clasimp = (fn () => (include_simpset:=false;include_claset:=false)); @@ -512,47 +517,55 @@ in Output.debug nthm; display_thms nthms end; +fun all_facts_of ctxt = + FactIndex.find (ProofContext.fact_index_of ctxt) ([], []) + |> maps #2 |> map (`Thm.name_of_thm); + (* get lemmas from claset, simpset, atpset and extra supplied rules *) fun get_clasimp_atp_lemmas ctxt user_thms = - let val claset_thms = - if !include_claset then - map put_name_pair (ResAxioms.claset_rules_of_ctxt ctxt) - else [] - val simpset_thms = - if !include_simpset then - map put_name_pair (ResAxioms.simpset_rules_of_ctxt ctxt) - else [] - val atpset_thms = - if !include_atpset then - map put_name_pair (ResAxioms.atpset_rules_of_ctxt ctxt) - else [] - val _ = if !Output.show_debug_msgs then (Output.debug "ATP theorems: "; display_thms atpset_thms) else () - val user_rules = - case user_thms of (*use whitelist if there are no user-supplied rules*) - [] => map (put_name_pair o ResAxioms.pairname) (!whitelist) - | _ => map put_name_pair user_thms - in - (claset_thms, simpset_thms, atpset_thms, user_rules) - end; + let val included_thms = + if !include_all + then (tap (fn ths => Output.debug ("Including all " ^ Int.toString (length ths) ^ + " theorems")) + (all_facts_of ctxt @ PureThy.all_thms_of (ProofContext.theory_of ctxt))) + else + let val claset_thms = + if !include_claset then ResAxioms.claset_rules_of_ctxt ctxt + else [] + val simpset_thms = + if !include_simpset then ResAxioms.simpset_rules_of_ctxt ctxt + else [] + val atpset_thms = + if !include_atpset then ResAxioms.atpset_rules_of_ctxt ctxt + else [] + val _ = if !Output.show_debug_msgs + then (Output.debug "ATP theorems: "; display_thms atpset_thms) + else () + in claset_thms @ simpset_thms @ atpset_thms end + val user_rules = map (put_name_pair o ResAxioms.pairname) + (if null user_thms then !whitelist else user_thms) + in + (map put_name_pair included_thms, user_rules) + end; (* remove lemmas that are banned from the backlist *) fun blacklist_filter thms = - if !run_blacklist_filter then - let val banned = make_banned_test (map #1 thms) - fun ok (a,_) = not (banned a) - in - filter ok thms - end - else - thms; + if !run_blacklist_filter then + let val banned = make_banned_test (map #1 thms) + fun ok (a,_) = not (banned a) + in filter ok thms end + else thms; (* filter axiom clauses, but keep supplied clauses and clauses in whitelist *) fun get_relevant_clauses ctxt cls_thms white_cls goals = - let val cls_thms_list = make_unique (mk_clause_table 2200) (List.concat (white_cls@cls_thms)) - val relevant_cls_thms_list = if !run_relevance_filter then ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_thms_list goals else cls_thms_list - in - insert_thms (List.concat white_cls) relevant_cls_thms_list - end; + let val cls_thms_list = make_unique (mk_clause_table 2200) (List.concat (white_cls@cls_thms)) + val relevant_cls_thms_list = + if !run_relevance_filter + then ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_thms_list goals + else cls_thms_list + in + insert_thms (List.concat white_cls) relevant_cls_thms_list + end; (***************************************************************) (* ATP invocation methods setup *) @@ -587,8 +600,8 @@ let val conj_cls = make_clauses conjectures val hyp_cls = cnf_hyps_thms ctxt val goal_cls = conj_cls@hyp_cls - val (cla_thms,simp_thms,atp_thms,user_rules) = get_clasimp_atp_lemmas ctxt (map ResAxioms.pairname user_thms) - val rm_black_cls = blacklist_filter (cla_thms@simp_thms@atp_thms) + val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms + val rm_black_cls = blacklist_filter included_thms val cla_simp_atp_clauses = ResAxioms.cnf_rules_pairs rm_black_cls val user_cls = ResAxioms.cnf_rules_pairs user_rules val axclauses_as_thms = get_relevant_clauses ctxt cla_simp_atp_clauses user_cls (map prop_of goal_cls) @@ -685,8 +698,8 @@ fun write_problem_files pf (ctxt,th) = let val goals = Thm.prems_of th val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals)) - val (cla_thms,simp_thms,atp_thms,white_thms) = get_clasimp_atp_lemmas ctxt [] - val rm_blacklist_cls = blacklist_filter (cla_thms@simp_thms@atp_thms) + val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt [] + val rm_blacklist_cls = blacklist_filter included_thms val cla_simp_atp_clauses = ResAxioms.cnf_rules_pairs rm_blacklist_cls val axclauses = get_relevant_clauses ctxt cla_simp_atp_clauses (ResAxioms.cnf_rules_pairs white_thms) goals val _ = Output.debug ("claset, simprules and atprules total clauses = " ^ diff -r 7546dafb3fc6 -r 7c7e15b27145 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Thu Jun 15 17:50:30 2006 +0200 +++ b/src/HOL/Tools/res_axioms.ML Thu Jun 15 17:50:47 2006 +0200 @@ -44,88 +44,65 @@ exception ELIMR2FOL of string; -(* functions used to construct a formula *) - -fun make_disjs [x] = x - | make_disjs (x :: xs) = HOLogic.mk_disj(x, make_disjs xs) - -fun make_conjs [x] = x - | make_conjs (x :: xs) = HOLogic.mk_conj(x, make_conjs xs) - fun add_EX tm [] = tm | add_EX tm ((x,xtp)::xs) = add_EX (HOLogic.exists_const xtp $ Abs(x,xtp,tm)) xs; -fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) (Const("Trueprop",_) $ Free(q,_)) = (p = q) +(*Checks for the premise ~P when the conclusion is P.*) +fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) + (Const("Trueprop",_) $ Free(q,_)) = (p = q) | is_neg _ _ = false; - -exception STRIP_CONCL; - - +(*FIXME: What if dest_Trueprop fails?*) fun strip_concl' prems bvs (Const ("==>",_) $ P $ Q) = - let val P' = HOLogic.dest_Trueprop P - val prems' = P'::prems - in - strip_concl' prems' bvs Q - end + strip_concl' (HOLogic.dest_Trueprop P :: prems) bvs Q | strip_concl' prems bvs P = let val P' = HOLogic.Not $ (HOLogic.dest_Trueprop P) - in - add_EX (make_conjs (P'::prems)) bvs - end; - + in add_EX (foldr1 HOLogic.mk_conj (P'::prems)) bvs end; fun strip_concl prems bvs concl (Const ("all", _) $ Abs (x,xtp,body)) = strip_concl prems ((x,xtp)::bvs) concl body | strip_concl prems bvs concl (Const ("==>",_) $ P $ Q) = if (is_neg P concl) then (strip_concl' prems bvs Q) else strip_concl (HOLogic.dest_Trueprop P::prems) bvs concl Q - | strip_concl prems bvs concl _ = add_EX (make_conjs prems) bvs; + | strip_concl prems bvs concl _ = add_EX (foldr1 HOLogic.mk_conj prems) bvs; - -fun trans_elim (main,others,concl) = - let val others' = map (strip_concl [] [] concl) others - val disjs = make_disjs others' +fun trans_elim (major,minors,concl) = + let val disjs = foldr1 HOLogic.mk_disj (map (strip_concl [] [] concl) minors) in - HOLogic.mk_imp (HOLogic.dest_Trueprop main, disjs) + HOLogic.mk_imp (HOLogic.dest_Trueprop major, disjs) end; - -(* aux function of elim2Fol, take away predicate variable. *) -fun elimR2Fol_aux prems concl = - let val nprems = length prems - val main = hd prems - in - if (nprems = 1) then HOLogic.Not $ (HOLogic.dest_Trueprop main) - else trans_elim (main, tl prems, concl) - end; - - (* convert an elim rule into an equivalent formula, of type term. *) fun elimR2Fol elimR = - let val elimR' = Drule.freeze_all elimR - val (prems,concl) = (prems_of elimR', concl_of elimR') - in - case concl of Const("Trueprop",_) $ Free(_,Type("bool",[])) - => HOLogic.mk_Trueprop (elimR2Fol_aux prems concl) - | Free(x,Type("prop",[])) => HOLogic.mk_Trueprop(elimR2Fol_aux prems concl) - | _ => raise ELIMR2FOL("Not an elimination rule!") - end; - + let val elimR' = Drule.freeze_all elimR + val (prems,concl) = (prems_of elimR', concl_of elimR') + val _ = case concl of + Const("Trueprop",_) $ Free(_,Type("bool",[])) => () + | Free(_, Type("prop",[])) => () + | _ => raise ELIMR2FOL "elimR2Fol: Not an elimination rule!" + val th = case prems of + [] => raise ELIMR2FOL "elimR2Fol: No premises!" + | [major] => HOLogic.Not $ (HOLogic.dest_Trueprop major) + | major::minors => trans_elim (major, minors, concl) + in HOLogic.mk_Trueprop th end + handle exn => + (warning ("elimR2Fol raised exception " ^ Toplevel.exn_message exn); + concl_of elimR); (* check if a rule is an elim rule *) fun is_elimR th = - case (concl_of th) of (Const ("Trueprop", _) $ Var (idx,_)) => true - | Var(indx,Type("prop",[])) => true - | _ => false; + case concl_of th of Const ("Trueprop", _) $ Var _ => true + | Var(_,Type("prop",[])) => true + | _ => false; (* convert an elim-rule into an equivalent theorem that does not have the predicate variable. Leave other theorems unchanged.*) fun transform_elim th = if is_elimR th then - let val tm = elimR2Fol th - val ctm = cterm_of (sign_of_thm th) tm + let val ctm = cterm_of (sign_of_thm th) (elimR2Fol th) in Goal.prove_raw [] ctm (fn _ => elimRule_tac th) end + handle exn => (warning ("transform_elim failed: " ^ Toplevel.exn_message exn ^ + " for theorem " ^ string_of_thm th); th) else th; @@ -303,12 +280,12 @@ (*Exported function to convert Isabelle theorems into axiom clauses*) -fun cnf_axiom_g cnf (name,th) = +fun cnf_axiom (name,th) = case name of - "" => cnf th (*no name, so can't cache*) + "" => skolem_thm th (*no name, so can't cache*) | s => case Symtab.lookup (!clause_cache) s of NONE => - let val cls = cnf th + let val cls = skolem_thm th in change clause_cache (Symtab.update (s, (th, cls))); cls end | SOME(th',cls) => if eq_thm(th,th') then cls @@ -319,15 +296,10 @@ fun pairname th = (Thm.name_of_thm th, th); - -val cnf_axiom = cnf_axiom_g skolem_thm; - - fun meta_cnf_axiom th = map Meson.make_meta_clause (cnf_axiom (pairname th)); - (**** Extract and Clausify theorems from a theory's claset and simpset ****) (*Preserve the name of "th" after the transformation "f"*) @@ -374,34 +346,27 @@ (**** Translate a set of classical/simplifier rules into CNF (still as type "thm") ****) -(* classical rules *) -fun cnf_rules_g cnf_axiom [] err_list = ([],err_list) - | cnf_rules_g cnf_axiom ((name,th) :: ths) err_list = - let val (ts,es) = cnf_rules_g cnf_axiom ths err_list +(* classical rules: works for both FOL and HOL *) +fun cnf_rules [] err_list = ([],err_list) + | cnf_rules ((name,th) :: ths) err_list = + let val (ts,es) = cnf_rules ths err_list in (cnf_axiom (name,th) :: ts,es) handle _ => (ts, (th::es)) end; - -(*works for both FOL and HOL*) -val cnf_rules = cnf_rules_g cnf_axiom; - -fun cnf_rules_pairs_aux [] = [] - | cnf_rules_pairs_aux ((name,th)::ths) = - let val ts = cnf_rules_pairs_aux ths - fun pair_name_cls k (n, []) = [] - | pair_name_cls k (n, cls::clss) = - (cls, (n,k))::(pair_name_cls (k+1) (n, clss)) - in - (pair_name_cls 0 (name, cnf_axiom(name,th)))::ts - handle THM _ => ts | ResClause.CLAUSE _ => ts | ResHolClause.LAM2COMB _ => ts - end; +fun pair_name_cls k (n, []) = [] + | pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss) + +fun cnf_rules_pairs_aux pairs [] = pairs + | cnf_rules_pairs_aux pairs ((name,th)::ths) = + let val pairs' = (pair_name_cls 0 (name, cnf_axiom(name,th))) :: pairs + handle THM _ => pairs | ResClause.CLAUSE _ => pairs + | ResHolClause.LAM2COMB _ => pairs + in cnf_rules_pairs_aux pairs' ths end; - -fun cnf_rules_pairs thms = rev (cnf_rules_pairs_aux thms); +val cnf_rules_pairs = cnf_rules_pairs_aux []; (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****) - (*These should include any plausibly-useful theorems, especially if they need Skolem functions. FIXME: this list is VERY INCOMPLETE*) val default_initial_thms = map pairname