# HG changeset patch # User paulson # Date 1158142821 -7200 # Node ID 756c4f1fd04c42645f4b7ee947f968a9dbaf8c5c # Parent 4b0fdb18ea9abce5ecbea2bf67f42850bcee4ceb Extended the blacklist with higher-order theorems. Restructured. Added checks to ensure that no higher-order clauses are output in first-order mode. diff -r 4b0fdb18ea9a -r 756c4f1fd04c src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Wed Sep 13 12:18:36 2006 +0200 +++ b/src/HOL/Tools/res_atp.ML Wed Sep 13 12:20:21 2006 +0200 @@ -303,16 +303,13 @@ FIXME: this blacklist needs to be maintained using theory data and added to using an attribute.*) val blacklist = ref - ["Datatype.unit.split_asm", (*These "unit" thms cause unsound proofs*) - (*Datatype.unit.nchotomy is caught automatically*) - "Datatype.unit.induct", + ["Datatype.prod.size", + "Datatype.unit.induct", (*"unit" thms cause unsound proofs; unit.nchotomy is caught automatically*) "Datatype.unit.inducts", + "Datatype.unit.split_asm", "Datatype.unit.split", "Datatype.unit.splits", - "Datatype.prod.size", - "Divides.dvd_0_left_iff", - "Finite_Set.card_0_eq", "Finite_Set.card_infinite", "Finite_Set.Max_ge", @@ -329,22 +326,19 @@ "Finite_Set.min_max.below_inf_sup_Inf_Sup.sup_Inf_absorb", "Finite_Set.min.f_below_strict_below.below_f_conv", (*duplicates in Orderings.*) "Finite_Set.min.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*) - + "Fun.vimage_image_eq", (*involves an existential quantifier*) + "HOL.split_if_asm", (*splitting theorem*) "HOL.split_if", (*splitting theorem*) - "HOL.split_if_asm", (*splitting theorem*) - + "IntDef.abs_split", "IntDef.Integ.Abs_Integ_inject", "IntDef.Integ.Abs_Integ_inverse", - "IntDef.abs_split", "IntDiv.zdvd_0_left", - "List.append_eq_append_conv", "List.hd_Cons_tl", (*Says everything is [] or Cons. Probably prolific.*) "List.in_listsD", "List.in_listsI", "List.lists.Cons", "List.listsE", - "Nat.less_one", (*not directional? obscure*) "Nat.not_gr0", "Nat.one_eq_mult_iff", (*duplicate by symmetry*) @@ -369,7 +363,6 @@ "NatSimprocs.mult_less_cancel_right_number_of", (*excessive case analysis*) "NatSimprocs.zero_le_divide_iff_number_of", (*excessive case analysis*) "NatSimprocs.zero_less_divide_iff_number_of", - "OrderedGroup.abs_0_eq", (*duplicate by symmetry*) "OrderedGroup.diff_eq_0_iff_eq", (*prolific?*) "OrderedGroup.join_0_eq_0", @@ -377,9 +370,8 @@ "OrderedGroup.pprt_eq_0", (*obscure*) "OrderedGroup.pprt_eq_id", (*obscure*) "OrderedGroup.pprt_mono", (*obscure*) + "Orderings.split_max", (*splitting theorem*) "Orderings.split_min", (*splitting theorem*) - "Orderings.split_max", (*splitting theorem*) - "Parity.even_nat_power", (*obscure, somewhat prolilfic*) "Parity.power_eq_0_iff_number_of", "Parity.power_le_zero_eq_number_of", (*obscure and prolific*) @@ -387,15 +379,16 @@ "Parity.zero_le_power_eq_number_of", (*obscure and prolific*) "Parity.zero_less_power_eq_number_of", (*obscure and prolific*) "Power.zero_less_power_abs_iff", - "Product_Type.unit_abs_eta_conv", - "Product_Type.unit_induct", - + "Product_Type.split_eta_SetCompr", (*involves an existential quantifier*) "Product_Type.split_paired_Ball_Sigma", (*splitting theorem*) "Product_Type.split_paired_Bex_Sigma", (*splitting theorem*) + "Product_Type.split_split_asm", (*splitting theorem*) "Product_Type.split_split", (*splitting theorem*) - "Product_Type.split_split_asm", (*splitting theorem*) - + "Product_Type.unit_abs_eta_conv", + "Product_Type.unit_induct", "Relation.diagI", + "Relation.Domain_def", (*involves an existential quantifier*) + "Relation.Image_def", (*involves an existential quantifier*) "Relation.ImageI", "Ring_and_Field.divide_cancel_left", (*fields are seldom used & often prolific*) "Ring_and_Field.divide_cancel_right", @@ -422,15 +415,20 @@ "Ring_and_Field.less_divide_eq_1_neg", (*obscure and prolific*) "Ring_and_Field.less_divide_eq_1_pos", (*obscure and prolific*) "Ring_and_Field.one_eq_divide_iff", (*duplicate by symmetry*) - "Set.disjoint_insert", - "Set.insert_disjoint", - "Set.Inter_UNIV_conv", "Set.ball_simps", "Set.bex_simps", (*quantifier rewriting: useless*) + "Set.Collect_bex_eq", (*involves an existential quantifier*) + "Set.Collect_ex_eq", (*involves an existential quantifier*) "Set.Diff_eq_empty_iff", (*redundant with paramodulation*) "Set.Diff_insert0", - "Set.empty_Union_conv", (*redundant with paramodulation*) - "Set.Int_UNIV", (*redundant with paramodulation*) - "Set.Inter_iff", (*We already have InterI, InterE*) + "Set.disjoint_insert", + "Set.empty_Union_conv", (*redundant with paramodulation*) + "Set.full_SetCompr_eq", (*involves an existential quantifier*) + "Set.image_Collect", (*involves an existential quantifier*) + "Set.image_def", (*involves an existential quantifier*) + "Set.insert_disjoint", + "Set.Int_UNIV", (*redundant with paramodulation*) + "Set.Inter_iff", (*We already have InterI, InterE*) + "Set.Inter_UNIV_conv", "Set.psubsetE", (*too prolific and obscure*) "Set.psubsetI", "Set.singleton_insert_inj_eq'", @@ -438,6 +436,7 @@ "Set.singletonD", (*these two duplicate some "insert" lemmas*) "Set.singletonI", "Set.Un_empty", (*redundant with paramodulation*) + "Set.UNION_def", (*involves an existential quantifier*) "Set.Union_empty_conv", (*redundant with paramodulation*) "Set.Union_iff", (*We already have UnionI, UnionE*) "SetInterval.atLeastAtMost_iff", (*obscure and prolific*) @@ -565,7 +564,6 @@ let val nthm = name ^ ": " ^ (string_of_thm thm) 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); @@ -605,24 +603,25 @@ in filter ok thms end else thms; + (***************************************************************) (* ATP invocation methods setup *) (***************************************************************) -(**** prover-specific format: TPTP ****) - - fun cnf_hyps_thms ctxt = let val ths = Assumption.prems_of ctxt in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end; - -(**** write to files ****) - +(*Translation mode can be auto-detected, or forced to be first-order or higher-order*) datatype mode = Auto | Fol | Hol; val linkup_logic_mode = ref Auto; +(*Ensures that no higher-order theorems "leak out"*) +fun restrict_to_logic logic cls = + if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o #1) cls + else cls; + fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas = if is_fol_logic logic then ResClause.tptp_write_file goals filename (axioms, classrels, arities) @@ -639,25 +638,26 @@ |> ResAxioms.assume_abstract_list |> Meson.finish_cnf val hyp_cls = cnf_hyps_thms ctxt val goal_cls = conj_cls@hyp_cls + val logic = case mode of + Auto => problem_logic_goals [map prop_of goal_cls] + | Fol => FOL + | Hol => HOL val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms val user_lemmas_names = map #1 user_rules val cla_simp_atp_clauses = included_thms |> blacklist_filter |> make_unique |> ResAxioms.cnf_rules_pairs + |> restrict_to_logic logic val user_cls = ResAxioms.cnf_rules_pairs user_rules val thy = ProofContext.theory_of ctxt val axclauses = get_relevant_clauses thy cla_simp_atp_clauses user_cls (map prop_of goal_cls) - val prob_logic = case mode of - Auto => problem_logic_goals [map prop_of goal_cls] - | Fol => FOL - | Hol => HOL - val keep_types = if is_fol_logic prob_logic then !fol_keep_types else is_typed_hol () + val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol () val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else [] val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else [] val writer = if dfg then dfg_writer else tptp_writer val file = atp_input_file() in - (writer prob_logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names; + (writer logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names; Output.debug ("Writing to " ^ file); file) end; @@ -751,24 +751,23 @@ fun write_problem_files probfile (ctxt,th) = let val goals = Thm.prems_of th val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals)) - val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt [] - val cla_simp_atp_clauses = included_thms |> blacklist_filter - |> make_unique |> ResAxioms.cnf_rules_pairs - val white_cls = ResAxioms.cnf_rules_pairs white_thms - val _ = Output.debug ("clauses = " ^ Int.toString(length cla_simp_atp_clauses)) val thy = ProofContext.theory_of ctxt fun get_neg_subgoals [] _ = [] - | get_neg_subgoals (gl::gls) n = - let val axclauses = get_relevant_clauses thy cla_simp_atp_clauses - white_cls [gl] (*relevant to goal*) - in - (neg_clauses th n, axclauses) :: get_neg_subgoals gls (n+1) - end - val goal_pairs = get_neg_subgoals goals 1 + | get_neg_subgoals (gl::gls) n = neg_clauses th n :: get_neg_subgoals gls (n+1) + val goal_cls = get_neg_subgoals goals 1 val logic = case !linkup_logic_mode of - Auto => problem_logic_goals (map ((map prop_of) o #1) goal_pairs) + Auto => problem_logic_goals (map ((map prop_of)) goal_cls) | Fol => FOL | Hol => HOL + val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt [] + val included_cls = included_thms |> blacklist_filter + |> make_unique |> ResAxioms.cnf_rules_pairs + |> restrict_to_logic logic + val white_cls = ResAxioms.cnf_rules_pairs white_thms + (*clauses relevant to goal gl*) + val axcls_list = map (fn gl => get_relevant_clauses thy included_cls white_cls [gl]) + goals + val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls)) val keep_types = if is_fol_logic logic then !ResClause.keep_types else is_typed_hol () val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy @@ -779,12 +778,12 @@ else [] val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses)) val writer = if !prover = "spass" then dfg_writer else tptp_writer - fun write_all [] _ = [] - | write_all ((ccls,axcls)::subgoals) k = + fun write_all [] [] _ = [] + | write_all (ccls::ccls_list) (axcls::axcls_list) k = (writer logic ccls (probfile k) (axcls,classrel_clauses,arity_clauses) [], probfile k) - :: write_all subgoals (k+1) - val (clnames::_, filenames) = ListPair.unzip (write_all goal_pairs 1) + :: write_all ccls_list axcls_list (k+1) + val (clnames::_, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1) val thm_names = Array.fromList clnames val _ = if !Output.show_debug_msgs then trace_array "thm_names" thm_names else ()