Extended the blacklist with higher-order theorems. Restructured. Added checks to
authorpaulson
Wed Sep 13 12:20:21 2006 +0200 (2006-09-13)
changeset 20526756c4f1fd04c
parent 20525 4b0fdb18ea9a
child 20527 958ec4833d87
Extended the blacklist with higher-order theorems. Restructured. Added checks to
ensure that no higher-order clauses are output in first-order mode.
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Sep 13 12:18:36 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Sep 13 12:20:21 2006 +0200
     1.3 @@ -303,16 +303,13 @@
     1.4    FIXME: this blacklist needs to be maintained using theory data and added to using
     1.5    an attribute.*)
     1.6  val blacklist = ref
     1.7 -  ["Datatype.unit.split_asm",         (*These  "unit" thms cause unsound proofs*)
     1.8 -                               (*Datatype.unit.nchotomy is caught automatically*)
     1.9 -   "Datatype.unit.induct",
    1.10 +  ["Datatype.prod.size",
    1.11 +   "Datatype.unit.induct", (*"unit" thms cause unsound proofs; unit.nchotomy is caught automatically*)
    1.12     "Datatype.unit.inducts",
    1.13 +   "Datatype.unit.split_asm", 
    1.14     "Datatype.unit.split",
    1.15     "Datatype.unit.splits",
    1.16 -   "Datatype.prod.size",
    1.17 -
    1.18     "Divides.dvd_0_left_iff",
    1.19 -
    1.20     "Finite_Set.card_0_eq",
    1.21     "Finite_Set.card_infinite",
    1.22     "Finite_Set.Max_ge",
    1.23 @@ -329,22 +326,19 @@
    1.24     "Finite_Set.min_max.below_inf_sup_Inf_Sup.sup_Inf_absorb", 
    1.25     "Finite_Set.min.f_below_strict_below.below_f_conv",        (*duplicates in Orderings.*)
    1.26     "Finite_Set.min.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
    1.27 -   
    1.28 +   "Fun.vimage_image_eq",   (*involves an existential quantifier*)
    1.29 +   "HOL.split_if_asm",     (*splitting theorem*)
    1.30     "HOL.split_if",         (*splitting theorem*)
    1.31 -   "HOL.split_if_asm",     (*splitting theorem*)
    1.32 -
    1.33 +   "IntDef.abs_split",
    1.34     "IntDef.Integ.Abs_Integ_inject",
    1.35     "IntDef.Integ.Abs_Integ_inverse",
    1.36 -   "IntDef.abs_split",
    1.37     "IntDiv.zdvd_0_left",
    1.38 -   
    1.39     "List.append_eq_append_conv",
    1.40     "List.hd_Cons_tl",   (*Says everything is [] or Cons. Probably prolific.*)
    1.41     "List.in_listsD",
    1.42     "List.in_listsI",
    1.43     "List.lists.Cons",
    1.44     "List.listsE",
    1.45 -
    1.46     "Nat.less_one", (*not directional? obscure*)
    1.47     "Nat.not_gr0",
    1.48     "Nat.one_eq_mult_iff", (*duplicate by symmetry*)
    1.49 @@ -369,7 +363,6 @@
    1.50     "NatSimprocs.mult_less_cancel_right_number_of", (*excessive case analysis*)
    1.51     "NatSimprocs.zero_le_divide_iff_number_of", (*excessive case analysis*)
    1.52     "NatSimprocs.zero_less_divide_iff_number_of",
    1.53 -
    1.54     "OrderedGroup.abs_0_eq", (*duplicate by symmetry*)
    1.55     "OrderedGroup.diff_eq_0_iff_eq", (*prolific?*)
    1.56     "OrderedGroup.join_0_eq_0",
    1.57 @@ -377,9 +370,8 @@
    1.58     "OrderedGroup.pprt_eq_0",   (*obscure*)
    1.59     "OrderedGroup.pprt_eq_id",   (*obscure*)
    1.60     "OrderedGroup.pprt_mono",   (*obscure*)
    1.61 +   "Orderings.split_max",      (*splitting theorem*)
    1.62     "Orderings.split_min",      (*splitting theorem*)
    1.63 -   "Orderings.split_max",      (*splitting theorem*)
    1.64 -
    1.65     "Parity.even_nat_power",   (*obscure, somewhat prolilfic*)
    1.66     "Parity.power_eq_0_iff_number_of",
    1.67     "Parity.power_le_zero_eq_number_of",   (*obscure and prolific*)
    1.68 @@ -387,15 +379,16 @@
    1.69     "Parity.zero_le_power_eq_number_of",   (*obscure and prolific*)
    1.70     "Parity.zero_less_power_eq_number_of",   (*obscure and prolific*)
    1.71     "Power.zero_less_power_abs_iff",
    1.72 -   "Product_Type.unit_abs_eta_conv",
    1.73 -   "Product_Type.unit_induct",
    1.74 -
    1.75 +   "Product_Type.split_eta_SetCompr",   (*involves an existential quantifier*)
    1.76     "Product_Type.split_paired_Ball_Sigma",     (*splitting theorem*)
    1.77     "Product_Type.split_paired_Bex_Sigma",      (*splitting theorem*)
    1.78 +   "Product_Type.split_split_asm",             (*splitting theorem*)
    1.79     "Product_Type.split_split",                 (*splitting theorem*)
    1.80 -   "Product_Type.split_split_asm",             (*splitting theorem*)
    1.81 -
    1.82 +   "Product_Type.unit_abs_eta_conv",
    1.83 +   "Product_Type.unit_induct",
    1.84     "Relation.diagI",
    1.85 +   "Relation.Domain_def",   (*involves an existential quantifier*)
    1.86 +   "Relation.Image_def",   (*involves an existential quantifier*)
    1.87     "Relation.ImageI",
    1.88     "Ring_and_Field.divide_cancel_left", (*fields are seldom used & often prolific*)
    1.89     "Ring_and_Field.divide_cancel_right",
    1.90 @@ -422,15 +415,20 @@
    1.91     "Ring_and_Field.less_divide_eq_1_neg", (*obscure and prolific*)
    1.92     "Ring_and_Field.less_divide_eq_1_pos", (*obscure and prolific*)
    1.93     "Ring_and_Field.one_eq_divide_iff",  (*duplicate by symmetry*)
    1.94 -   "Set.disjoint_insert",
    1.95 -   "Set.insert_disjoint",
    1.96 -   "Set.Inter_UNIV_conv",
    1.97     "Set.ball_simps", "Set.bex_simps",   (*quantifier rewriting: useless*)
    1.98 +   "Set.Collect_bex_eq",   (*involves an existential quantifier*)
    1.99 +   "Set.Collect_ex_eq",   (*involves an existential quantifier*)
   1.100     "Set.Diff_eq_empty_iff", (*redundant with paramodulation*)
   1.101     "Set.Diff_insert0",
   1.102 -   "Set.empty_Union_conv", (*redundant with paramodulation*)
   1.103 -   "Set.Int_UNIV", (*redundant with paramodulation*)
   1.104 -   "Set.Inter_iff",              (*We already have InterI, InterE*)
   1.105 +   "Set.disjoint_insert",
   1.106 +   "Set.empty_Union_conv",   (*redundant with paramodulation*)
   1.107 +   "Set.full_SetCompr_eq",   (*involves an existential quantifier*)
   1.108 +   "Set.image_Collect",      (*involves an existential quantifier*)
   1.109 +   "Set.image_def",          (*involves an existential quantifier*)
   1.110 +   "Set.insert_disjoint",
   1.111 +   "Set.Int_UNIV",  (*redundant with paramodulation*)
   1.112 +   "Set.Inter_iff", (*We already have InterI, InterE*)
   1.113 +   "Set.Inter_UNIV_conv",
   1.114     "Set.psubsetE",    (*too prolific and obscure*)
   1.115     "Set.psubsetI",
   1.116     "Set.singleton_insert_inj_eq'",
   1.117 @@ -438,6 +436,7 @@
   1.118     "Set.singletonD",  (*these two duplicate some "insert" lemmas*)
   1.119     "Set.singletonI",
   1.120     "Set.Un_empty", (*redundant with paramodulation*)
   1.121 +   "Set.UNION_def",   (*involves an existential quantifier*)
   1.122     "Set.Union_empty_conv", (*redundant with paramodulation*)
   1.123     "Set.Union_iff",              (*We already have UnionI, UnionE*)
   1.124     "SetInterval.atLeastAtMost_iff", (*obscure and prolific*)
   1.125 @@ -565,7 +564,6 @@
   1.126        let val nthm = name ^ ": " ^ (string_of_thm thm)
   1.127        in Output.debug nthm; display_thms nthms  end;
   1.128   
   1.129 -
   1.130  fun all_facts_of ctxt =
   1.131    FactIndex.find (ProofContext.fact_index_of ctxt) ([], [])
   1.132    |> maps #2 |> map (`Thm.name_of_thm);
   1.133 @@ -605,24 +603,25 @@
   1.134        in  filter ok thms  end
   1.135    else thms;
   1.136  
   1.137 +
   1.138  (***************************************************************)
   1.139  (* ATP invocation methods setup                                *)
   1.140  (***************************************************************)
   1.141  
   1.142 -(**** prover-specific format: TPTP ****)
   1.143 -
   1.144 -
   1.145  fun cnf_hyps_thms ctxt = 
   1.146      let val ths = Assumption.prems_of ctxt
   1.147      in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end;
   1.148  
   1.149 -
   1.150 -(**** write to files ****)
   1.151 -
   1.152 +(*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
   1.153  datatype mode = Auto | Fol | Hol;
   1.154  
   1.155  val linkup_logic_mode = ref Auto;
   1.156  
   1.157 +(*Ensures that no higher-order theorems "leak out"*)
   1.158 +fun restrict_to_logic logic cls =
   1.159 +  if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o #1) cls 
   1.160 +	                else cls;
   1.161 +
   1.162  fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas =
   1.163      if is_fol_logic logic 
   1.164      then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
   1.165 @@ -639,25 +638,26 @@
   1.166                           |> ResAxioms.assume_abstract_list |> Meson.finish_cnf
   1.167  	val hyp_cls = cnf_hyps_thms ctxt
   1.168  	val goal_cls = conj_cls@hyp_cls
   1.169 +	val logic = case mode of 
   1.170 +                            Auto => problem_logic_goals [map prop_of goal_cls]
   1.171 +			  | Fol => FOL
   1.172 +			  | Hol => HOL
   1.173  	val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
   1.174  	val user_lemmas_names = map #1 user_rules
   1.175  	val cla_simp_atp_clauses = included_thms |> blacklist_filter
   1.176  	                             |> make_unique |> ResAxioms.cnf_rules_pairs
   1.177 +                                     |> restrict_to_logic logic 
   1.178  	val user_cls = ResAxioms.cnf_rules_pairs user_rules
   1.179  	val thy = ProofContext.theory_of ctxt
   1.180  	val axclauses = get_relevant_clauses thy cla_simp_atp_clauses
   1.181  	                            user_cls (map prop_of goal_cls)
   1.182 -	val prob_logic = case mode of 
   1.183 -                            Auto => problem_logic_goals [map prop_of goal_cls]
   1.184 -			  | Fol => FOL
   1.185 -			  | Hol => HOL
   1.186 -	val keep_types = if is_fol_logic prob_logic then !fol_keep_types else is_typed_hol ()
   1.187 +	val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
   1.188  	val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
   1.189  	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
   1.190          val writer = if dfg then dfg_writer else tptp_writer 
   1.191  	val file = atp_input_file()
   1.192      in
   1.193 -	(writer prob_logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
   1.194 +	(writer logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
   1.195  	 Output.debug ("Writing to " ^ file);
   1.196  	 file)
   1.197      end;
   1.198 @@ -751,24 +751,23 @@
   1.199  fun write_problem_files probfile (ctxt,th)  =
   1.200    let val goals = Thm.prems_of th
   1.201        val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
   1.202 -      val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
   1.203 -      val cla_simp_atp_clauses = included_thms |> blacklist_filter
   1.204 -                                   |> make_unique |> ResAxioms.cnf_rules_pairs 
   1.205 -      val white_cls = ResAxioms.cnf_rules_pairs white_thms
   1.206 -      val _ = Output.debug ("clauses = " ^ Int.toString(length cla_simp_atp_clauses))
   1.207        val thy = ProofContext.theory_of ctxt
   1.208        fun get_neg_subgoals [] _ = []
   1.209 -        | get_neg_subgoals (gl::gls) n =
   1.210 -	      let val axclauses = get_relevant_clauses thy cla_simp_atp_clauses
   1.211 -	                            white_cls [gl]  (*relevant to goal*)
   1.212 -	      in
   1.213 -		  (neg_clauses th n, axclauses) :: get_neg_subgoals gls (n+1)
   1.214 -	      end
   1.215 -      val goal_pairs = get_neg_subgoals goals 1
   1.216 +        | get_neg_subgoals (gl::gls) n = neg_clauses th n :: get_neg_subgoals gls (n+1)
   1.217 +      val goal_cls = get_neg_subgoals goals 1
   1.218        val logic = case !linkup_logic_mode of
   1.219 -		Auto => problem_logic_goals (map ((map prop_of) o #1) goal_pairs)
   1.220 +		Auto => problem_logic_goals (map ((map prop_of)) goal_cls)
   1.221  	      | Fol => FOL
   1.222  	      | Hol => HOL
   1.223 +      val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
   1.224 +      val included_cls = included_thms |> blacklist_filter
   1.225 +                                       |> make_unique |> ResAxioms.cnf_rules_pairs 
   1.226 +                                       |> restrict_to_logic logic 
   1.227 +      val white_cls = ResAxioms.cnf_rules_pairs white_thms
   1.228 +      (*clauses relevant to goal gl*)
   1.229 +      val axcls_list = map (fn gl => get_relevant_clauses thy included_cls white_cls [gl])
   1.230 +                           goals
   1.231 +      val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls))
   1.232        val keep_types = if is_fol_logic logic then !ResClause.keep_types 
   1.233                         else is_typed_hol ()
   1.234        val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy
   1.235 @@ -779,12 +778,12 @@
   1.236                            else []
   1.237        val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
   1.238        val writer = if !prover = "spass" then dfg_writer else tptp_writer 
   1.239 -      fun write_all [] _ = []
   1.240 -	| write_all ((ccls,axcls)::subgoals) k =
   1.241 +      fun write_all [] [] _ = []
   1.242 +	| write_all (ccls::ccls_list) (axcls::axcls_list) k =
   1.243  	   (writer logic ccls (probfile k) (axcls,classrel_clauses,arity_clauses) [],
   1.244  	    probfile k) 
   1.245 -	   :: write_all subgoals (k+1)
   1.246 -      val (clnames::_, filenames) = ListPair.unzip (write_all goal_pairs 1)
   1.247 +	   :: write_all ccls_list axcls_list (k+1)
   1.248 +      val (clnames::_, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
   1.249        val thm_names = Array.fromList clnames
   1.250        val _ = if !Output.show_debug_msgs 
   1.251                then trace_array "thm_names" thm_names else ()