if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
authorblanchet
Thu Aug 26 14:58:45 2010 +0200 (2010-08-26)
changeset 3881971c9f61516cd
parent 38818 61cf050f8b2e
child 38820 d0f98bd81a85
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 14:05:22 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 14:58:45 2010 +0200
     1.3 @@ -108,24 +108,24 @@
     1.4  val abs_name = "Sledgehammer.abs"
     1.5  val skolem_prefix = "Sledgehammer.sko"
     1.6  
     1.7 -(* Add a pseudoconstant to the table, but a [] entry means a standard
     1.8 -   connective, which we ignore.*)
     1.9 -fun add_pseudoconst_to_table also_skolem (c, ctyps) =
    1.10 -  if also_skolem orelse not (String.isPrefix skolem_prefix c) then
    1.11 -    Symtab.map_default (c, [ctyps])
    1.12 -                       (fn [] => [] | ctypss => insert (op =) ctyps ctypss)
    1.13 -  else
    1.14 -    I
    1.15 -
    1.16 -fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
    1.17 -
    1.18 -val flip = Option.map not
    1.19  (* These are typically simplified away by "Meson.presimplify". *)
    1.20  val boring_consts =
    1.21    [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}]
    1.22  
    1.23 +(* Add a pseudoconstant to the table, but a [] entry means a standard
    1.24 +   connective, which we ignore.*)
    1.25 +fun add_pseudoconst_to_table also_skolem (c, Ts) =
    1.26 +  if member (op =) boring_consts c orelse
    1.27 +     (not also_skolem andalso String.isPrefix skolem_prefix c) then
    1.28 +    I
    1.29 +  else
    1.30 +    Symtab.map_default (c, [Ts]) (fn Tss => insert (op =) Ts Tss)
    1.31 +
    1.32 +fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
    1.33 +
    1.34  fun get_pseudoconsts thy also_skolems pos ts =
    1.35    let
    1.36 +    val flip = Option.map not
    1.37      (* We include free variables, as well as constants, to handle locales. For
    1.38         each quantifiers that must necessarily be skolemized by the ATP, we
    1.39         introduce a fresh constant to simulate the effect of Skolemization. *)
    1.40 @@ -179,10 +179,7 @@
    1.41        | (t0 as Const (_, @{typ bool})) $ t1 =>
    1.42          do_term t0 #> do_formula pos t1  (* theory constant *)
    1.43        | _ => do_term t
    1.44 -  in
    1.45 -    Symtab.empty |> fold (Symtab.update o rpair []) boring_consts
    1.46 -                 |> fold (do_formula pos) ts
    1.47 -  end
    1.48 +  in Symtab.empty |> fold (do_formula pos) ts end
    1.49  
    1.50  (*Inserts a dummy "constant" referring to the theory name, so that relevance
    1.51    takes the given theory into account.*)
    1.52 @@ -295,12 +292,12 @@
    1.53      in if Real.isFinite res then res else 0.0 end
    1.54  *)
    1.55  
    1.56 -fun pseudoconsts_of_term thy t =
    1.57 +fun pseudoconsts_in_axiom thy t =
    1.58    Symtab.fold (fn (x, ys) => fold (fn y => cons (x, y)) ys)
    1.59                (get_pseudoconsts thy true (SOME true) [t]) []
    1.60  fun pair_consts_axiom theory_relevant thy axiom =
    1.61    (axiom, axiom |> snd |> theory_const_prop_of theory_relevant
    1.62 -                |> pseudoconsts_of_term thy)
    1.63 +                |> pseudoconsts_in_axiom thy)
    1.64  
    1.65  type annotated_thm =
    1.66    (((unit -> string) * locality) * thm) * (string * pseudotype list) list
    1.67 @@ -330,6 +327,14 @@
    1.68      (accepts, more_rejects @ rejects)
    1.69    end
    1.70  
    1.71 +fun if_empty_replace_with_locality thy axioms loc tab =
    1.72 +  if Symtab.is_empty tab then
    1.73 +    get_pseudoconsts thy false (SOME false)
    1.74 +        (map_filter (fn ((_, loc'), th) =>
    1.75 +                        if loc' = loc then SOME (prop_of th) else NONE) axioms)
    1.76 +  else
    1.77 +    tab
    1.78 +
    1.79  (* FUDGE *)
    1.80  val threshold_divisor = 2.0
    1.81  val ridiculous_threshold = 0.1
    1.82 @@ -339,8 +344,12 @@
    1.83                       ({add, del, ...} : relevance_override) axioms goal_ts =
    1.84    let
    1.85      val thy = ProofContext.theory_of ctxt
    1.86 -    val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
    1.87 -                         Symtab.empty
    1.88 +    val const_tab =
    1.89 +      fold (count_axiom_consts theory_relevant thy) axioms Symtab.empty
    1.90 +    val goal_const_tab =
    1.91 +      get_pseudoconsts thy false (SOME false) goal_ts
    1.92 +      |> fold (if_empty_replace_with_locality thy axioms)
    1.93 +              [Chained, Local, Theory]
    1.94      val add_thms = maps (ProofContext.get_fact ctxt) add
    1.95      val del_thms = maps (ProofContext.get_fact ctxt) del
    1.96      val max_max_imperfect =
    1.97 @@ -434,8 +443,7 @@
    1.98    in
    1.99      axioms |> filter_out (member Thm.eq_thm del_thms o snd)
   1.100             |> map (rpair NONE o pair_consts_axiom theory_relevant thy)
   1.101 -           |> iter 0 max_relevant threshold0
   1.102 -                   (get_pseudoconsts thy false (SOME false) goal_ts) []
   1.103 +           |> iter 0 max_relevant threshold0 goal_const_tab []
   1.104             |> tap (fn res => trace_msg (fn () =>
   1.105                                  "Total relevant: " ^ Int.toString (length res)))
   1.106    end