author blanchet Wed May 16 18:16:51 2012 +0200 (2012-05-16) changeset 47933 4e8e0245e8be parent 47932 ce4178e037a7 child 47934 08d7aff8c7e6
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
```     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed May 16 18:16:51 2012 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed May 16 18:16:51 2012 +0200
1.3 @@ -362,6 +362,12 @@
1.4    if (not also_skolem andalso String.isPrefix skolem_prefix s) then I
1.5    else Symtab.map_default (s, [p]) (insert (op =) p)
1.6
1.7 +(* Set constants tend to pull in too many irrelevant facts. We limit the damage
1.8 +   by treating them more or less as if they were built-in but add their
1.9 +   axiomatization at the end. *)
1.10 +val set_consts = [@{const_name Collect}, @{const_name Set.member}]
1.11 +val set_thms = @{thms Collect_mem_eq mem_Collect_eq}
1.12 +
1.13  fun add_pconsts_in_term thy is_built_in_const also_skolems pos =
1.14    let
1.15      val flip = Option.map not
1.16 @@ -369,16 +375,19 @@
1.17         each quantifiers that must necessarily be skolemized by the automatic
1.18         prover, we introduce a fresh constant to simulate the effect of
1.19         Skolemization. *)
1.20 -    fun do_const const x ts =
1.21 +    fun do_const const ext_arg (x as (s, _)) ts =
1.22        let val (built_in, ts) = is_built_in_const x ts in
1.23 -        (not built_in
1.24 -         ? add_pconst_to_table also_skolems (rich_pconst thy const x))
1.25 -        #> fold (do_term false) ts
1.26 +        if member (op =) set_consts s then
1.27 +          fold (do_term ext_arg) ts
1.28 +        else
1.29 +          (not built_in
1.30 +           ? add_pconst_to_table also_skolems (rich_pconst thy const x))
1.31 +          #> fold (do_term false) ts
1.32        end
1.33      and do_term ext_arg t =
1.34        case strip_comb t of
1.35 -        (Const x, ts) => do_const true x ts
1.36 -      | (Free x, ts) => do_const false x ts
1.37 +        (Const x, ts) => do_const true ext_arg x ts
1.38 +      | (Free x, ts) => do_const false ext_arg x ts
1.39        | (Abs (_, T, t'), ts) =>
1.40          ((null ts andalso not ext_arg)
1.41           (* Since lambdas on the right-hand side of equalities are usually
1.42 @@ -750,6 +759,14 @@
1.43        ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
1.44         (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
1.45        |> take max_relevant
1.46 +    fun uses_const s t =
1.47 +      fold_aterms (curry (fn (Const (s', _), false) => s' = s | (_, b) => b)) t
1.48 +                  false
1.49 +    fun uses_const_anywhere accepts s =
1.50 +      exists (uses_const s o prop_of o snd) accepts orelse
1.51 +      exists (uses_const s) (concl_t :: hyp_ts)
1.52 +    fun add_set_const_thms accepts =
1.53 +      exists (uses_const_anywhere accepts) set_consts ? append set_thms
1.54      fun insert_into_facts accepts [] = accepts
1.55        | insert_into_facts accepts ths =
1.56          let
1.57 @@ -761,6 +778,7 @@
1.58          in bef @ add @ after end
1.59      fun insert_special_facts accepts =
1.60         [] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext}