--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Jun 23 16:28:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Jun 23 18:43:50 2010 +0200
@@ -88,42 +88,70 @@
Symtab.map_default (c, [ctyps])
(fn [] => [] | ctypss => insert (op =) ctyps ctypss)
-val fresh_Ex_prefix = "Sledgehammer.Ex."
+val fresh_sko_prefix = "Sledgehammer.Skox."
+
+val flip = Option.map not
-fun get_goal_consts_typs thy goals =
+(* Including equality in this list might be expected to stop rules like
+ subset_antisym from being chosen, but for some reason filtering works better
+ with them listed. The logical signs All, Ex, &, and --> are omitted for CNF
+ because any remaining occurrences must be within comprehensions. *)
+val boring_cnf_consts =
+ [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all},
+ @{const_name "=="}, @{const_name "op |"}, @{const_name Not},
+ @{const_name "op ="}]
+
+fun get_consts_typs thy pos ts =
let
- val use_natural_form = !use_natural_form
(* Free variables are included, as well as constants, to handle locales.
"skolem_id" is included to increase the complexity of theorems containing
Skolem functions. In non-CNF form, "Ex" is included but each occurrence
is considered fresh, to simulate the effect of Skolemization. *)
- fun aux (Const (x as (s, _))) =
- (if s = @{const_name Ex} andalso use_natural_form then
- (gensym fresh_Ex_prefix, [])
- else
- (const_with_typ thy x))
- |> add_const_type_to_table
- | aux (Free x) = add_const_type_to_table (const_with_typ thy x)
- | aux ((t as Const (@{const_name skolem_id}, _)) $ _) = aux t
- | aux (t $ u) = aux t #> aux u
- | aux (Abs (_, _, t)) = aux t
- | aux _ = I
- (* Including equality in this list might be expected to stop rules like
- subset_antisym from being chosen, but for some reason filtering works better
- with them listed. The logical signs All, Ex, &, and --> are omitted for CNF
- because any remaining occurrences must be within comprehensions. *)
- val standard_consts =
- [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all},
- @{const_name "=="}, @{const_name "op |"}, @{const_name Not},
- @{const_name "op ="}] @
- (if use_natural_form then
- [@{const_name All}, @{const_name Ex}, @{const_name "op &"},
- @{const_name "op -->"}]
- else
- [])
+ fun do_term t =
+ case t of
+ Const x => add_const_type_to_table (const_with_typ thy x)
+ | Free x => add_const_type_to_table (const_with_typ thy x)
+ | (t as Const (@{const_name skolem_id}, _)) $ _ => do_term t
+ | t1 $ t2 => do_term t1 #> do_term t2
+ | Abs (_, _, t) => do_term t
+ | _ => I
+ fun do_quantifier sweet_pos pos body_t =
+ do_formula pos body_t
+ #> (if pos = SOME sweet_pos then I
+ else add_const_type_to_table (gensym fresh_sko_prefix, []))
+ and do_equality T t1 t2 =
+ fold (if T = @{typ bool} orelse T = @{typ prop} then do_formula NONE
+ else do_term) [t1, t2]
+ and do_formula pos t =
+ case t of
+ Const (@{const_name all}, _) $ Abs (_, _, body_t) =>
+ do_quantifier false pos body_t
+ | @{const "==>"} $ t1 $ t2 =>
+ do_formula (flip pos) t1 #> do_formula pos t2
+ | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
+ do_equality T t1 t2
+ | @{const Trueprop} $ t1 => do_formula pos t1
+ | @{const Not} $ t1 => do_formula (flip pos) t1
+ | Const (@{const_name All}, _) $ Abs (_, _, body_t) =>
+ do_quantifier false pos body_t
+ | Const (@{const_name Ex}, _) $ Abs (_, _, body_t) =>
+ do_quantifier true pos body_t
+ | @{const "op &"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
+ | @{const "op |"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
+ | @{const "op -->"} $ t1 $ t2 =>
+ do_formula (flip pos) t1 #> do_formula pos t2
+ | Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 =>
+ do_equality T t1 t2
+ | (t0 as Const (_, @{typ bool})) $ t1 =>
+ do_term t0 #> do_formula pos t1 (* theory constant *)
+ | _ => do_term t
in
- Symtab.empty |> fold (Symtab.update o rpair []) standard_consts
- |> fold aux goals
+ Symtab.empty
+ |> (if !use_natural_form then
+ fold (do_formula pos) ts
+ else
+ fold (Symtab.update o rpair []) boring_cnf_consts
+ #> fold do_term ts)
end
(*Inserts a dummy "constant" referring to the theory name, so that relevance
@@ -217,7 +245,7 @@
fun add_expand_pairs (x,ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys;
fun consts_typs_of_term thy t =
- Symtab.fold add_expand_pairs (get_goal_consts_typs thy [t]) []
+ Symtab.fold add_expand_pairs (get_consts_typs thy (SOME false) [t]) []
fun pair_consts_typs_axiom theory_relevant thy axiom =
(axiom, axiom |> appropriate_prop_of theory_relevant
@@ -306,9 +334,11 @@
if weight >= threshold orelse
(defs_relevant andalso
defines thy (#1 clsthm) rel_const_tab) then
- (trace_msg (fn () => name ^ " clause " ^ Int.toString n ^
- " passes: " ^ Real.toString weight);
- relevant ((ax, weight) :: newrels, rejects) axs)
+ (trace_msg (fn () =>
+ name ^ " clause " ^ Int.toString n ^
+ " passes: " ^ Real.toString weight
+ (* ^ " consts: " ^ commas (map fst consts_typs) *));
+ relevant ((ax, weight) :: newrels, rejects) axs)
else
relevant (newrels, ax :: rejects) axs
end
@@ -326,7 +356,7 @@
let
val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
Symtab.empty
- val goal_const_tab = get_goal_consts_typs thy goals
+ val goal_const_tab = get_consts_typs thy (SOME true) goals
val _ =
trace_msg (fn () => "Initial constants: " ^
commas (Symtab.keys goal_const_tab))