src/HOL/Tools/res_atp.ML
changeset 21431 ef9080e7dbbc
parent 21397 2134b81a0b37
child 21470 7c1b59ddcd56
equal deleted inserted replaced
21430:77651b6d9d6c 21431:ef9080e7dbbc
   313 
   313 
   314 (*** white list and black list of lemmas ***)
   314 (*** white list and black list of lemmas ***)
   315 
   315 
   316 (*The rule subsetI is frequently omitted by the relevance filter.*)
   316 (*The rule subsetI is frequently omitted by the relevance filter.*)
   317 val whitelist = ref [subsetI]; 
   317 val whitelist = ref [subsetI]; 
   318 
   318   
   319 (*Names of theorems and theorem lists to be banned. The final numeric suffix of
   319 (*Names of theorems (not theorem lists! See multi_blacklist above) to be banned. 
   320   theorem lists is first removed.
       
   321 
   320 
   322   These theorems typically produce clauses that are prolific (match too many equality or
   321   These theorems typically produce clauses that are prolific (match too many equality or
   323   membership literals) and relate to seldom-used facts. Some duplicate other rules.
   322   membership literals) and relate to seldom-used facts. Some duplicate other rules.
   324   FIXME: this blacklist needs to be maintained using theory data and added to using
   323   FIXME: this blacklist needs to be maintained using theory data and added to using
   325   an attribute.*)
   324   an attribute.*)
   326 val blacklist = ref
   325 val blacklist = ref
   327   ["Datatype.prod.size",
   326   ["Datatype.prod.size",
   328    "Datatype.unit.exhaust", (*"unit" thms cause unsound proofs; unit.nchotomy is caught automatically*)
       
   329    "Datatype.unit.induct", 
       
   330    "Datatype.unit.inducts",
       
   331    "Datatype.unit.split_asm", 
       
   332    "Datatype.unit.split",
       
   333    "Datatype.unit.splits",
       
   334    "Divides.dvd_0_left_iff",
   327    "Divides.dvd_0_left_iff",
   335    "Finite_Set.card_0_eq",
   328    "Finite_Set.card_0_eq",
   336    "Finite_Set.card_infinite",
   329    "Finite_Set.card_infinite",
   337    "Finite_Set.Max_ge",
   330    "Finite_Set.Max_ge",
   338    "Finite_Set.Max_in",
   331    "Finite_Set.Max_in",
   342    "Finite_Set.max.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
   335    "Finite_Set.max.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
   343    "Finite_Set.Min_ge_iff",
   336    "Finite_Set.Min_ge_iff",
   344    "Finite_Set.Min_gr_iff",
   337    "Finite_Set.Min_gr_iff",
   345    "Finite_Set.Min_in",
   338    "Finite_Set.Min_in",
   346    "Finite_Set.Min_le",
   339    "Finite_Set.Min_le",
   347    "Finite_Set.min_max.below_inf_sup_Inf_Sup.inf_Sup_absorb", 
       
   348    "Finite_Set.min_max.below_inf_sup_Inf_Sup.sup_Inf_absorb", 
       
   349    "Finite_Set.min.f_below_strict_below.below_f_conv",        (*duplicates in Orderings.*)
   340    "Finite_Set.min.f_below_strict_below.below_f_conv",        (*duplicates in Orderings.*)
   350    "Finite_Set.min.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
   341    "Finite_Set.min.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
   351    "Fun.vimage_image_eq",   (*involves an existential quantifier*)
   342    "Fun.vimage_image_eq",   (*involves an existential quantifier*)
   352    "HOL.split_if_asm",     (*splitting theorem*)
   343    "HOL.split_if_asm",     (*splitting theorem*)
   353    "HOL.split_if",         (*splitting theorem*)
   344    "HOL.split_if",         (*splitting theorem*)
   392    "OrderedGroup.pprt_eq_0",   (*obscure*)
   383    "OrderedGroup.pprt_eq_0",   (*obscure*)
   393    "OrderedGroup.pprt_eq_id",   (*obscure*)
   384    "OrderedGroup.pprt_eq_id",   (*obscure*)
   394    "OrderedGroup.pprt_mono",   (*obscure*)
   385    "OrderedGroup.pprt_mono",   (*obscure*)
   395    "Orderings.split_max",      (*splitting theorem*)
   386    "Orderings.split_max",      (*splitting theorem*)
   396    "Orderings.split_min",      (*splitting theorem*)
   387    "Orderings.split_min",      (*splitting theorem*)
   397    "Parity.even_nat_power",   (*obscure, somewhat prolilfic*)
       
   398    "Parity.power_eq_0_iff_number_of",
       
   399    "Parity.power_le_zero_eq_number_of",   (*obscure and prolific*)
       
   400    "Parity.power_less_zero_eq_number_of",
       
   401    "Parity.zero_le_power_eq_number_of",   (*obscure and prolific*)
       
   402    "Parity.zero_less_power_eq_number_of",   (*obscure and prolific*)
       
   403    "Power.zero_less_power_abs_iff",
   388    "Power.zero_less_power_abs_iff",
   404    "Product_Type.split_eta_SetCompr",   (*involves an existential quantifier*)
   389    "Product_Type.split_eta_SetCompr",   (*involves an existential quantifier*)
   405    "Product_Type.split_paired_Ball_Sigma",     (*splitting theorem*)
   390    "Product_Type.split_paired_Ball_Sigma",     (*splitting theorem*)
   406    "Product_Type.split_paired_Bex_Sigma",      (*splitting theorem*)
   391    "Product_Type.split_paired_Bex_Sigma",      (*splitting theorem*)
   407    "Product_Type.split_split_asm",             (*splitting theorem*)
   392    "Product_Type.split_split_asm",             (*splitting theorem*)
   435    "Ring_and_Field.le_divide_eq_1_neg", (*obscure and prolific*)
   420    "Ring_and_Field.le_divide_eq_1_neg", (*obscure and prolific*)
   436    "Ring_and_Field.le_divide_eq_1_pos", (*obscure and prolific*)
   421    "Ring_and_Field.le_divide_eq_1_pos", (*obscure and prolific*)
   437    "Ring_and_Field.less_divide_eq_1_neg", (*obscure and prolific*)
   422    "Ring_and_Field.less_divide_eq_1_neg", (*obscure and prolific*)
   438    "Ring_and_Field.less_divide_eq_1_pos", (*obscure and prolific*)
   423    "Ring_and_Field.less_divide_eq_1_pos", (*obscure and prolific*)
   439    "Ring_and_Field.one_eq_divide_iff",  (*duplicate by symmetry*)
   424    "Ring_and_Field.one_eq_divide_iff",  (*duplicate by symmetry*)
   440    "Set.ball_simps", "Set.bex_simps",   (*quantifier rewriting: useless*)
       
   441    "Set.Collect_bex_eq",   (*involves an existential quantifier*)
   425    "Set.Collect_bex_eq",   (*involves an existential quantifier*)
   442    "Set.Collect_ex_eq",   (*involves an existential quantifier*)
   426    "Set.Collect_ex_eq",   (*involves an existential quantifier*)
   443    "Set.Diff_eq_empty_iff", (*redundant with paramodulation*)
   427    "Set.Diff_eq_empty_iff", (*redundant with paramodulation*)
   444    "Set.Diff_insert0",
   428    "Set.Diff_insert0",
   445    "Set.disjoint_insert",
       
   446    "Set.empty_Union_conv",   (*redundant with paramodulation*)
   429    "Set.empty_Union_conv",   (*redundant with paramodulation*)
   447    "Set.full_SetCompr_eq",   (*involves an existential quantifier*)
   430    "Set.full_SetCompr_eq",   (*involves an existential quantifier*)
   448    "Set.image_Collect",      (*involves an existential quantifier*)
   431    "Set.image_Collect",      (*involves an existential quantifier*)
   449    "Set.image_def",          (*involves an existential quantifier*)
   432    "Set.image_def",          (*involves an existential quantifier*)
   450    "Set.insert_disjoint",
       
   451    "Set.Int_UNIV",  (*redundant with paramodulation*)
   433    "Set.Int_UNIV",  (*redundant with paramodulation*)
   452    "Set.Inter_iff", (*We already have InterI, InterE*)
   434    "Set.Inter_iff", (*We already have InterI, InterE*)
   453    "Set.Inter_UNIV_conv",
       
   454    "Set.psubsetE",    (*too prolific and obscure*)
   435    "Set.psubsetE",    (*too prolific and obscure*)
   455    "Set.psubsetI",
   436    "Set.psubsetI",
   456    "Set.singleton_insert_inj_eq'",
   437    "Set.singleton_insert_inj_eq'",
   457    "Set.singleton_insert_inj_eq",
   438    "Set.singleton_insert_inj_eq",
   458    "Set.singletonD",  (*these two duplicate some "insert" lemmas*)
   439    "Set.singletonD",  (*these two duplicate some "insert" lemmas*)
   488 fun insert_suffixed_names ht x = 
   469 fun insert_suffixed_names ht x = 
   489      (Polyhash.insert ht (x^"_iff1", ()); 
   470      (Polyhash.insert ht (x^"_iff1", ()); 
   490       Polyhash.insert ht (x^"_iff2", ()); 
   471       Polyhash.insert ht (x^"_iff2", ()); 
   491       Polyhash.insert ht (x^"_dest", ())); 
   472       Polyhash.insert ht (x^"_dest", ())); 
   492 
   473 
   493 (*Are all characters in this string digits?*)
   474 (*FIXME: probably redundant now that ALL boolean-valued variables are banned*)
   494 fun all_numeric s = null (String.tokens Char.isDigit s);
       
   495 
       
   496 (*Delete a suffix of the form _\d+*)
       
   497 fun delete_numeric_suffix s =
       
   498   case rev (String.fields (fn c => c = #"_") s) of
       
   499       last::rest => 
       
   500           if all_numeric last 
       
   501           then [s, space_implode "_" (rev rest)]
       
   502           else [s]
       
   503     | [] => [s];
       
   504 
       
   505 fun banned_thmlist s =
   475 fun banned_thmlist s =
   506   (Sign.base_name s) mem_string ["induct","inducts","split","splits","split_asm"];
   476   (Sign.base_name s) mem_string ["induct","inducts","split","splits","split_asm"];
   507 
   477 
   508 (*Reject theorems with names like "List.filter.filter_list_def" or
   478 (*Reject theorems with names like "List.filter.filter_list_def" or
   509   "Accessible_Part.acc.defs", as these are definitions arising from packages.
   479   "Accessible_Part.acc.defs", as these are definitions arising from packages.
   513    String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a;
   483    String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a;
   514 
   484 
   515 fun make_banned_test xs = 
   485 fun make_banned_test xs = 
   516   let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)
   486   let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)
   517                                 (6000, HASH_STRING)
   487                                 (6000, HASH_STRING)
   518       fun banned_aux s = 
   488       fun banned s = 
   519             isSome (Polyhash.peek ht s) orelse banned_thmlist s orelse is_package_def s
   489             isSome (Polyhash.peek ht s) orelse banned_thmlist s orelse is_package_def s
   520       fun banned s = exists banned_aux (delete_numeric_suffix s)
       
   521   in  app (fn x => Polyhash.insert ht (x,())) (!blacklist);
   490   in  app (fn x => Polyhash.insert ht (x,())) (!blacklist);
   522       app (insert_suffixed_names ht) (!blacklist @ xs); 
   491       app (insert_suffixed_names ht) (!blacklist @ xs); 
   523       banned
   492       banned
   524   end;
   493   end;
   525 
   494 
   586     (FactIndex.find (ProofContext.fact_index_of ctxt) ([], []));
   555     (FactIndex.find (ProofContext.fact_index_of ctxt) ([], []));
   587 
   556 
   588 fun multi_name a (th, (n,pairs)) = 
   557 fun multi_name a (th, (n,pairs)) = 
   589   (n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs)
   558   (n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs)
   590 
   559 
   591 fun add_multi_names ((a, []), pairs) = pairs
   560 fun add_multi_names_aux ((a, []), pairs) = pairs
   592   | add_multi_names ((a, [th]), pairs) = (a,th)::pairs
   561   | add_multi_names_aux ((a, [th]), pairs) = (a,th)::pairs
   593   | add_multi_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths);
   562   | add_multi_names_aux ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths);
       
   563 
       
   564 val multi_blacklist =
       
   565   ["Set.ball_simps", "Set.bex_simps",  (*quantifier rewriting: useless*)
       
   566    "Set.disjoint_insert", "Set.insert_disjoint", "Set.Inter_UNIV_conv"];
       
   567 
       
   568 (*Ignore blacklisted theorem lists*)
       
   569 fun add_multi_names ((a, ths), pairs) = 
       
   570   if a mem_string multi_blacklist then pairs
       
   571   else add_multi_names_aux ((a, ths), pairs);
   594 
   572 
   595 fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
   573 fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
   596 
   574 
   597 (*The single theorems go BEFORE the multiple ones*)
   575 (*The single theorems go BEFORE the multiple ones*)
   598 fun name_thm_pairs ctxt = 
   576 fun name_thm_pairs ctxt = 
   629   in
   607   in
   630       (filter check_named included_thms, user_rules)
   608       (filter check_named included_thms, user_rules)
   631   end;
   609   end;
   632 
   610 
   633 (*Remove lemmas that are banned from the backlist. Also remove duplicates. *)
   611 (*Remove lemmas that are banned from the backlist. Also remove duplicates. *)
   634 fun blacklist_filter thms = 
   612 fun blacklist_filter ths = 
   635   if !run_blacklist_filter then 
   613   if !run_blacklist_filter then 
   636       let val _ = Output.debug("blacklist filter gets " ^ Int.toString (length thms) ^ " theorems")
   614       let val _ = Output.debug("blacklist filter gets " ^ Int.toString (length ths) ^ " theorems")
   637           val banned = make_banned_test (map #1 thms)
   615           val banned = make_banned_test (map #1 ths)
   638 	  fun ok (a,_) = not (banned a)
   616 	  fun ok (a,_) = not (banned a)
   639 	  val okthms = filter ok thms
   617 	  val okthms = filter ok ths
   640           val _ = Output.debug("...and returns " ^ Int.toString (length okthms))
   618           val _ = Output.debug("...and returns " ^ Int.toString (length okthms))
   641       in  okthms end
   619       in  okthms end
   642   else thms;
   620   else ths;
   643 
   621 
   644 (***************************************************************)
   622 (***************************************************************)
   645 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
   623 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
   646 (***************************************************************)
   624 (***************************************************************)
   647 
   625 
   695 (*Ensures that no higher-order theorems "leak out"*)
   673 (*Ensures that no higher-order theorems "leak out"*)
   696 fun restrict_to_logic logic cls =
   674 fun restrict_to_logic logic cls =
   697   if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o fst) cls 
   675   if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o fst) cls 
   698 	                else cls;
   676 	                else cls;
   699 
   677 
       
   678 (*True if the term contains a variable whose (atomic) type is in the given list.*)
       
   679 fun has_typed_var tycons = 
       
   680   let fun var_tycon (Var (_, Type(a,_))) = a mem_string tycons
       
   681         | var_tycon _ = false
       
   682   in  exists var_tycon o term_vars  end;
       
   683 
       
   684 (*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and
       
   685   likely to lead to unsound proofs.*)
       
   686 fun remove_finite_types cls =
       
   687   filter (not o has_typed_var ["Product_Type.unit","bool"] o prop_of o fst) cls;
       
   688 
   700 fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas =
   689 fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas =
   701     if is_fol_logic logic 
   690     if is_fol_logic logic 
   702     then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
   691     then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
   703     else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) user_lemmas;
   692     else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) user_lemmas;
   704 
   693 
   711 fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
   700 fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
   712     let val conj_cls = make_clauses conjectures 
   701     let val conj_cls = make_clauses conjectures 
   713                          |> ResAxioms.assume_abstract_list |> Meson.finish_cnf
   702                          |> ResAxioms.assume_abstract_list |> Meson.finish_cnf
   714 	val hyp_cls = cnf_hyps_thms ctxt
   703 	val hyp_cls = cnf_hyps_thms ctxt
   715 	val goal_cls = conj_cls@hyp_cls
   704 	val goal_cls = conj_cls@hyp_cls
       
   705 	val goal_tms = map prop_of goal_cls
   716 	val logic = case mode of 
   706 	val logic = case mode of 
   717                             Auto => problem_logic_goals [map prop_of goal_cls]
   707                             Auto => problem_logic_goals [goal_tms]
   718 			  | Fol => FOL
   708 			  | Fol => FOL
   719 			  | Hol => HOL
   709 			  | Hol => HOL
   720 	val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
   710 	val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
   721 	val cla_simp_atp_clauses = included_thms |> blacklist_filter
   711 	val cla_simp_atp_clauses = included_thms |> blacklist_filter
   722 	                             |> ResAxioms.cnf_rules_pairs |> make_unique 
   712 	                             |> ResAxioms.cnf_rules_pairs |> make_unique 
   723                                      |> restrict_to_logic logic 
   713                                      |> restrict_to_logic logic 
       
   714                                      |> remove_finite_types
   724 	val user_cls = ResAxioms.cnf_rules_pairs user_rules
   715 	val user_cls = ResAxioms.cnf_rules_pairs user_rules
   725 	val thy = ProofContext.theory_of ctxt
   716 	val thy = ProofContext.theory_of ctxt
   726 	val axclauses = get_relevant_clauses thy cla_simp_atp_clauses
   717 	val axclauses = make_unique (get_relevant_clauses thy cla_simp_atp_clauses user_cls goal_tms)
   727 	                            user_cls (map prop_of goal_cls) |> make_unique
       
   728 	val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
   718 	val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
   729         val subs = tfree_classes_of_terms (map prop_of goal_cls)
   719         val subs = tfree_classes_of_terms goal_tms
   730         and axtms = map (prop_of o #1) axclauses
   720         and axtms = map (prop_of o #1) axclauses
   731         val supers = tvar_classes_of_terms axtms
   721         val supers = tvar_classes_of_terms axtms
   732         and tycons = type_consts_of_terms thy axtms
   722         and tycons = type_consts_of_terms thy (goal_tms@axtms)
   733         (*TFrees in conjecture clauses; TVars in axiom clauses*)
   723         (*TFrees in conjecture clauses; TVars in axiom clauses*)
   734         val classrel_clauses = 
   724         val classrel_clauses = 
   735               if keep_types then ResClause.make_classrel_clauses thy subs supers
   725               if keep_types then ResClause.make_classrel_clauses thy subs supers
   736               else []
   726               else []
   737 	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy tycons supers else []
   727 	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy tycons supers else []
   840 	      | Fol => FOL
   830 	      | Fol => FOL
   841 	      | Hol => HOL
   831 	      | Hol => HOL
   842       val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
   832       val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
   843       val included_cls = included_thms |> blacklist_filter
   833       val included_cls = included_thms |> blacklist_filter
   844                                        |> ResAxioms.cnf_rules_pairs |> make_unique 
   834                                        |> ResAxioms.cnf_rules_pairs |> make_unique 
   845                                        |> restrict_to_logic logic 
   835                                        |> restrict_to_logic logic
       
   836                                        |> remove_finite_types
   846       val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls))
   837       val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls))
   847       val white_cls = ResAxioms.cnf_rules_pairs white_thms
   838       val white_cls = ResAxioms.cnf_rules_pairs white_thms
   848       (*clauses relevant to goal gl*)
   839       (*clauses relevant to goal gl*)
   849       val axcls_list = map (fn gl => get_relevant_clauses thy included_cls white_cls [gl])
   840       val axcls_list = map (fn gl => get_relevant_clauses thy included_cls white_cls [gl])
   850                            goals
   841                            goals
   856       fun write_all [] [] _ = []
   847       fun write_all [] [] _ = []
   857 	| write_all (ccls::ccls_list) (axcls::axcls_list) k =
   848 	| write_all (ccls::ccls_list) (axcls::axcls_list) k =
   858             let val fname = probfile k
   849             let val fname = probfile k
   859                 val axcls = make_unique axcls
   850                 val axcls = make_unique axcls
   860                 val ccls = subtract_cls ccls axcls
   851                 val ccls = subtract_cls ccls axcls
   861                 val subs = tfree_classes_of_terms (map prop_of ccls)
   852                 val ccltms = map prop_of ccls
   862                 and axtms = map (prop_of o #1) axcls
   853                 and axtms = map (prop_of o #1) axcls
   863                 val supers = tvar_classes_of_terms axtms
   854                 val subs = tfree_classes_of_terms ccltms
   864                 and tycons = type_consts_of_terms thy axtms
   855                 and supers = tvar_classes_of_terms axtms
       
   856                 and tycons = type_consts_of_terms thy (ccltms@axtms)
   865                 (*TFrees in conjecture clauses; TVars in axiom clauses*)
   857                 (*TFrees in conjecture clauses; TVars in axiom clauses*)
   866                 val classrel_clauses = 
   858                 val classrel_clauses = 
   867                       if keep_types then ResClause.make_classrel_clauses thy subs supers
   859                       if keep_types then ResClause.make_classrel_clauses thy subs supers
   868                       else []
   860                       else []
   869                 val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
   861                 val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))