--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Aug 01 23:58:42 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Aug 02 00:15:08 2014 +0200
@@ -93,28 +93,34 @@
map (replace_dependencies_in_line (name, [])) lines
| add_line_pass1 line lines = line :: lines
-fun add_lines_pass2 res _ [] = rev res
- | add_lines_pass2 res (prev as (prev_name, prev_norm_t))
- ((line as (name, role, t, rule, deps)) :: lines) =
+fun normalize role t =
+ t |> role = Conjecture ? (HOLogic.dest_Trueprop #> s_not #> HOLogic.mk_Trueprop)
+
+fun add_lines_pass2 res [] = rev res
+ | add_lines_pass2 res ((line as (name, role, t, rule, deps)) :: lines) =
let
- val norm_t = t |> role = Conjecture ? (HOLogic.dest_Trueprop #> s_not #> HOLogic.mk_Trueprop)
+ val norm_t = normalize role t
+ val is_duplicate =
+ exists (fn (prev_name, prev_role, prev_t, _, _) =>
+ member (op =) deps prev_name andalso
+ Term.aconv_untyped (normalize prev_role prev_t, norm_t))
+ res
fun looks_boring () =
- t aconv @{prop True} orelse t aconv @{prop False} orelse norm_t aconv prev_norm_t orelse
- length deps < 2
+ t aconv @{prop True} orelse t aconv @{prop False} orelse length deps < 2
fun is_skolemizing_line (_, _, _, rule', deps') =
is_skolemize_rule rule' andalso member (op =) deps' name
fun is_before_skolemize_rule () = exists is_skolemizing_line lines
in
- if (Term.aconv_untyped (prev_norm_t, norm_t) andalso member (op =) deps prev_name) orelse
+ if is_duplicate orelse
(role = Plain andalso not (is_skolemize_rule rule) andalso
not (is_arith_rule rule) andalso not (is_datatype_rule rule) andalso
not (null lines) andalso looks_boring () andalso not (is_before_skolemize_rule ())) then
- add_lines_pass2 res prev (map (replace_dependencies_in_line (name, deps)) lines)
+ add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines)
else
- add_lines_pass2 (line :: res) (name, norm_t) lines
+ add_lines_pass2 (line :: res) lines
end
type isar_params =
@@ -165,7 +171,7 @@
val atp_proof =
fold_rev add_line_pass1 atp_proof []
- |> add_lines_pass2 [] (("", []), Term.dummy)
+ |> add_lines_pass2 []
val conjs =
map_filter (fn (name, role, _, _, _) =>