# HG changeset patch # User paulson # Date 1164222487 -3600 # Node ID 7c1b59ddcd56814e9776ce24618c3e5c4d1b5edd # Parent 1e45e9ef327e295e0261e5a24c0a33707f87cc1c Consolidation of code to "blacklist" unhelpful theorems, including record surjectivity properties diff -r 1e45e9ef327e -r 7c1b59ddcd56 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Wed Nov 22 19:55:22 2006 +0100 +++ b/src/HOL/Tools/res_atp.ML Wed Nov 22 20:08:07 2006 +0100 @@ -247,9 +247,11 @@ exception PRED_LG of term; fun pred_lg (t as Const(P,tp)) (lg,seen)= - if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg,insert (op =) t seen) + if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) + else (lg,insert (op =) t seen) | pred_lg (t as Free(P,tp)) (lg,seen) = - if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg,insert (op =) t seen) + if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) + else (lg,insert (op =) t seen) | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, insert (op =) t seen) | pred_lg P _ = raise PRED_LG(P); @@ -275,18 +277,13 @@ end | lits_lg lits (lg,seen) = (lg,seen); -fun dest_disj_aux (Const ("op |", _) $ t $ t') disjs = - dest_disj_aux t (dest_disj_aux t' disjs) +fun dest_disj_aux (Const("Trueprop",_) $ t) disjs = dest_disj_aux t disjs + | dest_disj_aux (Const ("op |", _) $ t $ t') disjs = dest_disj_aux t (dest_disj_aux t' disjs) | dest_disj_aux t disjs = t::disjs; fun dest_disj t = dest_disj_aux t []; -fun logic_of_clause tm (lg,seen) = - let val tm' = HOLogic.dest_Trueprop tm - val disjs = dest_disj tm' - in - lits_lg disjs (lg,seen) - end; +fun logic_of_clause tm = lits_lg (dest_disj tm); fun logic_of_clauses [] (lg,seen) = (lg,seen) | logic_of_clauses (cls::clss) (FOL,seen) = @@ -316,7 +313,7 @@ (*The rule subsetI is frequently omitted by the relevance filter.*) val whitelist = ref [subsetI]; -(*Names of theorems (not theorem lists! See multi_blacklist above) to be banned. +(*Names of theorems (not theorem lists! See multi_blacklist below) to be banned. These theorems typically produce clauses that are prolific (match too many equality or membership literals) and relate to seldom-used facts. Some duplicate other rules. @@ -471,10 +468,6 @@ Polyhash.insert ht (x^"_iff2", ()); Polyhash.insert ht (x^"_dest", ())); -(*FIXME: probably redundant now that ALL boolean-valued variables are banned*) -fun banned_thmlist s = - (Sign.base_name s) mem_string ["induct","inducts","split","splits","split_asm"]; - (*Reject theorems with names like "List.filter.filter_list_def" or "Accessible_Part.acc.defs", as these are definitions arising from packages. FIXME: this will also block definitions within locales*) @@ -486,7 +479,7 @@ let val ht = Polyhash.mkTable (Polyhash.hash_string, op =) (6000, HASH_STRING) fun banned s = - isSome (Polyhash.peek ht s) orelse banned_thmlist s orelse is_package_def s + isSome (Polyhash.peek ht s) orelse is_package_def s in app (fn x => Polyhash.insert ht (x,())) (!blacklist); app (insert_suffixed_names ht) (!blacklist @ xs); banned @@ -505,12 +498,7 @@ fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_term(P,0w0)) | hash_literal P = hashw_term(P,0w0); - -fun get_literals (Const("Trueprop",_)$P) lits = get_literals P lits - | get_literals (Const("op |",_)$P$Q) lits = get_literals Q (get_literals P lits) - | get_literals lit lits = (lit::lits); - -fun hash_term t = Word.toIntX (xor_words (map hash_literal (get_literals t []))); +fun hash_term t = Word.toIntX (xor_words (map hash_literal (dest_disj t))); fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2); @@ -565,9 +553,13 @@ ["Set.ball_simps", "Set.bex_simps", (*quantifier rewriting: useless*) "Set.disjoint_insert", "Set.insert_disjoint", "Set.Inter_UNIV_conv"]; +val multi_base_blacklist = + ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm"]; + (*Ignore blacklisted theorem lists*) fun add_multi_names ((a, ths), pairs) = - if a mem_string multi_blacklist then pairs + if a mem_string multi_blacklist orelse (Sign.base_name a) mem_string multi_base_blacklist + then pairs else add_multi_names_aux ((a, ths), pairs); fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a; @@ -675,16 +667,50 @@ if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o fst) cls else cls; +(**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****) + +(** Too general means, positive equality literal with a variable X as one operand, + when X does not occur properly in the other operand. This rules out clearly + inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **) + +fun occurs ix = + let fun occ(Var (jx,_)) = (ix=jx) + | occ(t1$t2) = occ t1 orelse occ t2 + | occ(Abs(_,_,t)) = occ t + | occ _ = false + in occ end; + +fun is_recordtype T = not (null (RecordPackage.dest_recTs T)); + +(*Unwanted equalities include + (1) those between a variable that does not properly occur in the second operand, + (2) those between a variable and a record, since these seem to be prolific "cases" thms +*) +fun too_general_eqterms (Var (ix,T), t) = not (occurs ix t) orelse is_recordtype T + | too_general_eqterms _ = false; + +fun too_general_equality (Const ("op =", _) $ x $ y) = + too_general_eqterms (x,y) orelse too_general_eqterms(y,x) + | too_general_equality _ = false; + +(* tautologous? *) +fun is_taut (Const ("Trueprop", _) $ Const ("True", _)) = true + | is_taut _ = false; + (*True if the term contains a variable whose (atomic) type is in the given list.*) fun has_typed_var tycons = let fun var_tycon (Var (_, Type(a,_))) = a mem_string tycons | var_tycon _ = false in exists var_tycon o term_vars end; +fun unwanted t = + is_taut t orelse has_typed_var ["Product_Type.unit","bool"] t orelse + forall too_general_equality (dest_disj t); + (*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and likely to lead to unsound proofs.*) -fun remove_finite_types cls = - filter (not o has_typed_var ["Product_Type.unit","bool"] o prop_of o fst) cls; +fun remove_unwanted_clauses cls = + filter (not o unwanted o prop_of o fst) cls; fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas = if is_fol_logic logic @@ -711,7 +737,7 @@ val cla_simp_atp_clauses = included_thms |> blacklist_filter |> ResAxioms.cnf_rules_pairs |> make_unique |> restrict_to_logic logic - |> remove_finite_types + |> remove_unwanted_clauses val user_cls = ResAxioms.cnf_rules_pairs user_rules val thy = ProofContext.theory_of ctxt val axclauses = make_unique (get_relevant_clauses thy cla_simp_atp_clauses user_cls goal_tms) @@ -833,7 +859,7 @@ val included_cls = included_thms |> blacklist_filter |> ResAxioms.cnf_rules_pairs |> make_unique |> restrict_to_logic logic - |> remove_finite_types + |> remove_unwanted_clauses val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls)) val white_cls = ResAxioms.cnf_rules_pairs white_thms (*clauses relevant to goal gl*) diff -r 1e45e9ef327e -r 7c1b59ddcd56 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Wed Nov 22 19:55:22 2006 +0100 +++ b/src/HOL/Tools/res_axioms.ML Wed Nov 22 20:08:07 2006 +0100 @@ -91,14 +91,6 @@ fun transfer_to_ATP_Linkup th = transfer (Theory.deref recon_thy_ref) th handle THM _ => th; -fun is_taut th = - case (prop_of th) of - (Const ("Trueprop", _) $ Const ("True", _)) => true - | _ => false; - -(* remove tautologous clauses *) -val rm_redundant_cls = List.filter (not o is_taut); - (**** SKOLEMIZATION BY INFERENCE (lcp) ****) @@ -467,8 +459,7 @@ (*Skolemize a named theorem, with Skolem functions as additional premises.*) fun skolem_thm th = let val nnfth = to_nnf th - in Meson.make_cnf (skolem_of_nnf nnfth) nnfth - |> assume_abstract_list |> Meson.finish_cnf |> rm_redundant_cls + in Meson.make_cnf (skolem_of_nnf nnfth) nnfth |> assume_abstract_list |> Meson.finish_cnf end handle THM _ => []; @@ -485,7 +476,7 @@ let val (thy',defs) = declare_skofuns cname nnfth thy val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth val (thy'',cnfs') = declare_abstract (thy',cnfs) - in (thy'', rm_redundant_cls (Meson.finish_cnf cnfs')) + in (thy'', Meson.finish_cnf cnfs') end) (SOME (to_nnf th) handle THM _ => NONE) end; diff -r 1e45e9ef327e -r 7c1b59ddcd56 src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Wed Nov 22 19:55:22 2006 +0100 +++ b/src/HOL/Tools/res_clause.ML Wed Nov 22 20:08:07 2006 +0100 @@ -417,35 +417,14 @@ (vss, fs union fss) end; -(** Too general means, positive equality literal with a variable X as one operand, - when X does not occur properly in the other operand. This rules out clearly - inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **) - -fun occurs a (UVar(b,_)) = a=b - | occurs a (Fun (_,_,ts)) = exists (occurs a) ts - -(*Is the first operand a variable that does not properly occur in the second operand?*) -fun too_general_terms (UVar _, UVar _) = false - | too_general_terms (Fun _, _) = false - | too_general_terms (UVar (a,_), t) = not (occurs a t); - -fun too_general_lit (Literal (true, Predicate("equal",_,[x,y]))) = - too_general_terms (x,y) orelse too_general_terms(y,x) - | too_general_lit _ = false; - - (** make axiom and conjecture clauses. **) exception MAKE_CLAUSE; fun make_clause (clause_id, axiom_name, th, kind) = - let val term = prop_of th - val (lits,types_sorts) = literals_of_term term + let val (lits,types_sorts) = literals_of_term (prop_of th) in if forall isFalse lits then error "Problem too trivial for resolution (empty clause)" - else if kind=Axiom andalso forall too_general_lit lits - then (Output.debug ("Omitting " ^ axiom_name ^ ": equalities are too general"); - raise MAKE_CLAUSE) else Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind, literals = lits, types_sorts = types_sorts} end; diff -r 1e45e9ef327e -r 7c1b59ddcd56 src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Wed Nov 22 19:55:22 2006 +0100 +++ b/src/HOL/Tools/res_hol_clause.ML Wed Nov 22 20:08:07 2006 +0100 @@ -418,21 +418,6 @@ fun literals_of_term P = literals_of_term1 ([],[]) P; -fun occurs a (CombVar(b,_)) = a = b - | occurs a (CombApp(t1,t2,_)) = (occurs a t1) orelse (occurs a t2) - | occurs _ _ = false - -fun too_general_terms (CombVar(v,_), t) = not (occurs v t) - | too_general_terms _ = false; - -fun too_general_equality (Literal(true,(Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))))) = - too_general_terms (t1,t2) orelse too_general_terms (t2,t1) - | too_general_equality _ = false; - -(* forbid the literal hBOOL(V) *) -fun too_general_bool (Literal(_,Bool(CombVar _))) = true - | too_general_bool _ = false; - (* making axiom and conjecture clauses *) exception MAKE_CLAUSE fun make_clause(clause_id,axiom_name,kind,thm,is_user) = @@ -443,10 +428,6 @@ in if forall isFalse lits then error "Problem too trivial for resolution (empty clause)" - else if (!typ_level <> T_FULL) andalso kind=Axiom andalso - (forall too_general_equality lits orelse exists too_general_bool lits) - then (Output.debug ("Omitting " ^ axiom_name ^ ": clause is too prolific"); - raise MAKE_CLAUSE) else Clause {clause_id = clause_id, axiom_name = axiom_name, th = thm, kind = kind, literals = lits, ctypes_sorts = ctypes_sorts, @@ -718,16 +699,6 @@ val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname) -(*Simulate the result of conversion to CNF*) -fun pretend_cnf s = (thm s, (s,0)); - -(*These theorems allow the proof of P=Q from P-->Q and Q-->P, so they are necessary for - completeness. Unfortunately, they are very prolific, causing greatly increased runtimes. - They also lead to many unsound proofs. Thus it is well that the "exists too_general_bool" - test deletes them except with the full-typed translation.*) -val iff_thms = [pretend_cnf "ATP_Linkup.iff_positive", - pretend_cnf "ATP_Linkup.iff_negative"]; - fun get_helper_clauses () = let val IK = if !combI_count > 0 orelse !combK_count > 0 then (Output.debug "Include combinator I K"; cnf_helper_thms [comb_I,comb_K]) @@ -746,7 +717,7 @@ else [] val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal] in - make_axiom_clauses (iff_thms @ other @ IK @ BC @ S @ B'C' @ S') [] + make_axiom_clauses (other @ IK @ BC @ S @ B'C' @ S') [] end