src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
changeset 37566 9ca40dff25bd
parent 37552 6034aac65143
child 37567 02e4ccd512b6
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 12:15:49 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 15:01:35 2010 +0200
     1.3 @@ -18,18 +18,9 @@
     1.4    val use_natural_form : bool Unsynchronized.ref
     1.5    val name_thms_pair_from_ref :
     1.6      Proof.context -> thm list -> Facts.ref -> string * thm list
     1.7 -  val tvar_classes_of_terms : term list -> string list
     1.8 -  val tfree_classes_of_terms : term list -> string list
     1.9 -  val type_consts_of_terms : theory -> term list -> string list
    1.10 -  val is_quasi_fol_theorem : theory -> thm -> bool
    1.11    val relevant_facts :
    1.12      bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override
    1.13      -> Proof.context * (thm list * 'a) -> thm list -> cnf_thm list
    1.14 -  val prepare_clauses :
    1.15 -    bool -> thm list -> cnf_thm list -> cnf_thm list -> theory
    1.16 -    -> string vector
    1.17 -       * (hol_clause list * hol_clause list * hol_clause list
    1.18 -          * hol_clause list * classrel_clause list * arity_clause list)
    1.19  end;
    1.20  
    1.21  structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
    1.22 @@ -392,10 +383,6 @@
    1.23  
    1.24  (*** retrieve lemmas and filter them ***)
    1.25  
    1.26 -(*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
    1.27 -
    1.28 -fun setinsert (x,s) = Symtab.update (x,()) s;
    1.29 -
    1.30  (*Reject theorems with names like "List.filter.filter_list_def" or
    1.31    "Accessible_Part.acc.defs", as these are definitions arising from packages.*)
    1.32  fun is_package_def a =
    1.33 @@ -406,16 +393,7 @@
    1.34       String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a
    1.35    end;
    1.36  
    1.37 -fun mk_clause_table xs =
    1.38 -  fold (Termtab.update o `(prop_of o fst)) xs Termtab.empty
    1.39 -
    1.40 -fun make_unique xs =
    1.41 -  Termtab.fold (cons o snd) (mk_clause_table xs) []
    1.42 -
    1.43 -(* Remove existing axiom clauses from the conjecture clauses, as this can
    1.44 -   dramatically boost an ATP's performance (for some reason). *)
    1.45 -fun subtract_cls ax_clauses =
    1.46 -  filter_out (Termtab.defined (mk_clause_table ax_clauses) o prop_of)
    1.47 +fun make_unique xs = Termtab.fold (cons o snd) (make_clause_table xs) []
    1.48  
    1.49  val exists_sledgehammer_const =
    1.50    exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) o prop_of
    1.51 @@ -491,48 +469,9 @@
    1.52  
    1.53  
    1.54  (***************************************************************)
    1.55 -(* Type Classes Present in the Axiom or Conjecture Clauses     *)
    1.56 -(***************************************************************)
    1.57 -
    1.58 -fun add_classes (sorts, cset) = List.foldl setinsert cset (flat sorts);
    1.59 -
    1.60 -(*Remove this trivial type class*)
    1.61 -fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
    1.62 -
    1.63 -fun tvar_classes_of_terms ts =
    1.64 -  let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
    1.65 -  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
    1.66 -
    1.67 -fun tfree_classes_of_terms ts =
    1.68 -  let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
    1.69 -  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
    1.70 -
    1.71 -(*fold type constructors*)
    1.72 -fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
    1.73 -  | fold_type_consts _ _ x = x;
    1.74 -
    1.75 -(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
    1.76 -fun add_type_consts_in_term thy =
    1.77 -  let
    1.78 -    val const_typargs = Sign.const_typargs thy
    1.79 -    fun aux (Const cT) = fold (fold_type_consts setinsert) (const_typargs cT)
    1.80 -      | aux (Abs (_, _, u)) = aux u
    1.81 -      | aux (Const (@{const_name skolem_id}, _) $ _) = I
    1.82 -      | aux (t $ u) = aux t #> aux u
    1.83 -      | aux _ = I
    1.84 -  in aux end
    1.85 -
    1.86 -fun type_consts_of_terms thy ts =
    1.87 -  Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
    1.88 -
    1.89 -
    1.90 -(***************************************************************)
    1.91  (* ATP invocation methods setup                                *)
    1.92  (***************************************************************)
    1.93  
    1.94 -fun is_quasi_fol_theorem thy =
    1.95 -  Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] o prop_of
    1.96 -
    1.97  (**** Predicates to detect unwanted clauses (prolific or likely to cause
    1.98        unsoundness) ****)
    1.99  
   1.100 @@ -581,8 +520,6 @@
   1.101      (has_typed_var dangerous_types t orelse
   1.102       forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t)))
   1.103  
   1.104 -fun is_fol_goal thy = forall (Meson.is_fol_term thy) o map prop_of
   1.105 -
   1.106  fun relevant_facts full_types respect_no_atp relevance_threshold
   1.107                     relevance_convergence defs_relevant max_new theory_relevant
   1.108                     (relevance_override as {add, del, only})
   1.109 @@ -591,7 +528,7 @@
   1.110      val thy = ProofContext.theory_of ctxt
   1.111      val add_thms = maps (ProofContext.get_fact ctxt) add
   1.112      val has_override = not (null add) orelse not (null del)
   1.113 -    val is_FO = is_fol_goal thy goal_cls
   1.114 +    val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls
   1.115      val axioms =
   1.116        checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
   1.117            (map (name_thms_pair_from_ref ctxt chained_ths) add @
   1.118 @@ -611,70 +548,4 @@
   1.119      |> sort (prod_ord string_ord int_ord o pairself (fst o snd))
   1.120    end
   1.121  
   1.122 -(** Helper clauses **)
   1.123 -
   1.124 -fun count_combterm (CombConst ((c, _), _, _)) =
   1.125 -    Symtab.map_entry c (Integer.add 1)
   1.126 -  | count_combterm (CombVar _) = I
   1.127 -  | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
   1.128 -fun count_literal (Literal (_, t)) = count_combterm t
   1.129 -fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
   1.130 -
   1.131 -fun raw_cnf_rules_pairs ps = map (fn (name, thm) => (thm, ((name, 0), thm))) ps
   1.132 -fun cnf_helper_thms thy raw =
   1.133 -  map (`Thm.get_name_hint)
   1.134 -  #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
   1.135 -
   1.136 -val optional_helpers =
   1.137 -  [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
   1.138 -   (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
   1.139 -   (["c_COMBS"], (false, @{thms COMBS_def}))]
   1.140 -val optional_typed_helpers =
   1.141 -  [(["c_True", "c_False"], (true, @{thms True_or_False})),
   1.142 -   (["c_If"], (true, @{thms if_True if_False True_or_False}))]
   1.143 -val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
   1.144 -
   1.145 -val init_counters =
   1.146 -  Symtab.make (maps (maps (map (rpair 0) o fst))
   1.147 -                    [optional_helpers, optional_typed_helpers])
   1.148 -
   1.149 -fun get_helper_clauses thy is_FO full_types conjectures axcls =
   1.150 -  let
   1.151 -    val axclauses = map snd (make_axiom_clauses thy axcls)
   1.152 -    val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
   1.153 -    fun is_needed c = the (Symtab.lookup ct c) > 0
   1.154 -    val cnfs =
   1.155 -      (optional_helpers
   1.156 -       |> full_types ? append optional_typed_helpers
   1.157 -       |> maps (fn (ss, (raw, ths)) =>
   1.158 -                   if exists is_needed ss then cnf_helper_thms thy raw ths
   1.159 -                   else []))
   1.160 -      @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
   1.161 -  in map snd (make_axiom_clauses thy cnfs) end
   1.162 -
   1.163 -(* prepare for passing to writer,
   1.164 -   create additional clauses based on the information from extra_cls *)
   1.165 -fun prepare_clauses full_types goal_cls axcls extra_cls thy =
   1.166 -  let
   1.167 -    val is_FO = is_fol_goal thy goal_cls
   1.168 -    val ccls = subtract_cls extra_cls goal_cls
   1.169 -    val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
   1.170 -    val ccltms = map prop_of ccls
   1.171 -    and axtms = map (prop_of o #1) extra_cls
   1.172 -    val subs = tfree_classes_of_terms ccltms
   1.173 -    and supers = tvar_classes_of_terms axtms
   1.174 -    and tycons = type_consts_of_terms thy (ccltms @ axtms)
   1.175 -    (*TFrees in conjecture clauses; TVars in axiom clauses*)
   1.176 -    val conjectures = make_conjecture_clauses thy ccls
   1.177 -    val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls)
   1.178 -    val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls)
   1.179 -    val helper_clauses =
   1.180 -      get_helper_clauses thy is_FO full_types conjectures extra_cls
   1.181 -    val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   1.182 -    val classrel_clauses = make_classrel_clauses thy subs supers'
   1.183 -  in
   1.184 -    (Vector.fromList clnames,
   1.185 -      (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
   1.186 -  end
   1.187 -
   1.188  end;