1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 16:18:40 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 17:27:29 2010 +0200
     1.3 @@ -101,8 +101,7 @@
     1.4  
     1.5  fun string_for_pseudoconst (s, []) = s
     1.6    | string_for_pseudoconst (s, Ts) = s ^ string_for_pseudotypes Ts
     1.7 -fun string_for_super_pseudoconst (s, [[]]) = s
     1.8 -  | string_for_super_pseudoconst (s, Tss) =
     1.9 +fun string_for_super_pseudoconst (s, Tss) =
    1.10      s ^ "{" ^ commas (map string_for_pseudotypes Tss) ^ "}"
    1.11  
    1.12  val abs_name = "Sledgehammer.abs"
    1.13 @@ -229,10 +228,9 @@
    1.14  (**** Actual Filtering Code ****)
    1.15  
    1.16  (*The frequency of a constant is the sum of those of all instances of its type.*)
    1.17 -fun pseudoconst_freq match const_tab (c, cts) =
    1.18 -  CTtab.fold (fn (cts', m) => match (cts, cts') ? Integer.add m)
    1.19 +fun pseudoconst_freq match const_tab (c, Ts) =
    1.20 +  CTtab.fold (fn (Ts', m) => match (Ts, Ts') ? Integer.add m)
    1.21               (the (Symtab.lookup const_tab c)) 0
    1.22 -  handle Option.Option => 0
    1.23  
    1.24  
    1.25  (* A surprising number of theorems contain only a few significant constants.
    1.26 @@ -247,15 +245,20 @@
    1.27  fun irrel_log n = Math.ln (Real.fromInt n + 19.0) / 6.4
    1.28  
    1.29  (* FUDGE *)
    1.30 -val abs_weight = 2.0
    1.31 -val skolem_weight = 0.5
    1.32 +val abs_rel_weight = 0.5
    1.33 +val abs_irrel_weight = 2.0
    1.34 +val skolem_rel_weight = 2.0  (* impossible *)
    1.35 +val skolem_irrel_weight = 0.5
    1.36  
    1.37  (* Computes a constant's weight, as determined by its frequency. *)
    1.38 -val rel_weight = rel_log oo pseudoconst_freq match_pseudotypes
    1.39 -fun irrel_weight const_tab (c as (s, _)) =
    1.40 +fun generic_weight abs_weight skolem_weight logx f const_tab (c as (s, _)) =
    1.41    if s = abs_name then abs_weight
    1.42    else if String.isPrefix skolem_prefix s then skolem_weight
    1.43 -  else irrel_log (pseudoconst_freq (match_pseudotypes o swap) const_tab c)
    1.44 +  else logx (pseudoconst_freq (match_pseudotypes o f) const_tab c)
    1.45 +
    1.46 +val rel_weight = generic_weight abs_rel_weight skolem_rel_weight rel_log I
    1.47 +val irrel_weight = generic_weight abs_irrel_weight skolem_irrel_weight irrel_log
    1.48 +                                  swap
    1.49  
    1.50  (* FUDGE *)
    1.51  fun locality_multiplier General = 1.0
    1.52 @@ -508,12 +511,17 @@
    1.53  val exists_sledgehammer_const =
    1.54    exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
    1.55  
    1.56 -fun is_strange_theorem th =
    1.57 +fun is_metastrange_theorem th =
    1.58    case head_of (concl_of th) of
    1.59        Const (a, _) => (a <> @{const_name Trueprop} andalso
    1.60                         a <> @{const_name "=="})
    1.61      | _ => false
    1.62  
    1.63 +fun is_that_fact th =
    1.64 +  String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
    1.65 +  andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
    1.66 +                           | _ => false) (prop_of th)
    1.67 +
    1.68  val type_has_top_sort =
    1.69    exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
    1.70  
    1.71 @@ -583,7 +591,7 @@
    1.72    let val t = prop_of thm in
    1.73      is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
    1.74      is_dangerous_term full_types t orelse exists_sledgehammer_const t orelse
    1.75 -    is_strange_theorem thm
    1.76 +    is_metastrange_theorem thm orelse is_that_fact thm
    1.77    end
    1.78  
    1.79  fun all_name_thms_pairs ctxt reserved full_types add_thms chained_ths =