src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
changeset 37501 b5440c78ed3f
parent 37500 7587b6e63454
child 37502 a8f7b25d5478
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Jun 22 16:23:29 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Jun 22 16:40:36 2010 +0200
     1.3 @@ -255,17 +255,12 @@
     1.4        end
     1.5    end;
     1.6  
     1.7 -fun cnf_for_facts ctxt =
     1.8 -  let val thy = ProofContext.theory_of ctxt in
     1.9 -    maps (maps (cnf_axiom thy) o ProofContext.get_fact ctxt)
    1.10 -  end
    1.11 -
    1.12  fun relevant_clauses ctxt relevance_convergence defs_relevant max_new
    1.13                       ({add, del, ...} : relevance_override) ctab =
    1.14    let
    1.15      val thy = ProofContext.theory_of ctxt
    1.16 -    val add_thms = cnf_for_facts ctxt add
    1.17 -    val del_thms = cnf_for_facts ctxt del
    1.18 +    val add_thms = maps (ProofContext.get_fact ctxt) add
    1.19 +    val del_thms = maps (ProofContext.get_fact ctxt) del
    1.20      fun iter threshold rel_consts =
    1.21        let
    1.22          fun relevant ([], _) [] = []  (* Nothing added this iteration *)
    1.23 @@ -283,11 +278,11 @@
    1.24                    (more_rejects @ rejects)
    1.25              end
    1.26            | relevant (newrels, rejects)
    1.27 -                     ((ax as (clsthm as (thm, ((name, n), _)), consts_typs)) ::
    1.28 -                      axs) =
    1.29 +                     ((ax as (clsthm as (thm, ((name, n), orig_th)),
    1.30 +                              consts_typs)) :: axs) =
    1.31              let
    1.32 -              val weight = if member Thm.eq_thm add_thms thm then 1.0
    1.33 -                           else if member Thm.eq_thm del_thms thm then 0.0
    1.34 +              val weight = if member Thm.eq_thm add_thms orig_th then 1.0
    1.35 +                           else if member Thm.eq_thm del_thms orig_th then 0.0
    1.36                             else clause_weight ctab rel_consts consts_typs
    1.37              in
    1.38                if weight >= threshold orelse
    1.39 @@ -525,12 +520,10 @@
    1.40      (has_typed_var dangerous_types t orelse
    1.41       forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t)))
    1.42  
    1.43 -fun is_dangerous_theorem full_types add_thms thm =
    1.44 -  not (member Thm.eq_thm add_thms thm) andalso
    1.45 -  is_dangerous_term full_types (prop_of thm)
    1.46 -
    1.47  fun remove_dangerous_clauses full_types add_thms =
    1.48 -  filter_out (is_dangerous_theorem full_types add_thms o fst)
    1.49 +  filter_out (fn (cnf_th, (_, orig_th)) =>
    1.50 +                 not (member Thm.eq_thm add_thms orig_th) andalso
    1.51 +                 is_dangerous_term full_types (prop_of cnf_th))
    1.52  
    1.53  fun is_fol_goal thy = forall (Meson.is_fol_term thy) o map prop_of
    1.54  
    1.55 @@ -552,8 +545,11 @@
    1.56          |> cnf_rules_pairs thy
    1.57          |> not has_override ? make_unique
    1.58          |> not only ? restrict_to_logic thy is_FO
    1.59 -        |> (if only then I
    1.60 -            else remove_dangerous_clauses full_types (cnf_for_facts ctxt add))
    1.61 +        |> (if only then
    1.62 +              I
    1.63 +            else
    1.64 +              remove_dangerous_clauses full_types
    1.65 +                                       (maps (ProofContext.get_fact ctxt) add))
    1.66      in
    1.67        relevance_filter ctxt relevance_threshold relevance_convergence
    1.68                         defs_relevant max_new theory_relevant relevance_override