# HG changeset patch # User blanchet # Date 1406930322 -7200 # Node ID 6c4ab6f0a6fcaa13c69d29ba87469fecd5f41606 # Parent 5ef0531d9db2f5f74bbee9b7d915c833558ad3c2 normalize conjectures vs. negated conjectures when comparing terms diff -r 5ef0531d9db2 -r 6c4ab6f0a6fc src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Aug 01 23:33:43 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Aug 01 23:58:42 2014 +0200 @@ -94,22 +94,27 @@ | add_line_pass1 line lines = line :: lines fun add_lines_pass2 res _ [] = rev res - | add_lines_pass2 res prev_t ((line as (name, role, t, rule, deps)) :: lines) = + | add_lines_pass2 res (prev as (prev_name, prev_norm_t)) + ((line as (name, role, t, rule, deps)) :: lines) = let + val norm_t = t |> role = Conjecture ? (HOLogic.dest_Trueprop #> s_not #> HOLogic.mk_Trueprop) + fun looks_boring () = - t aconv @{prop True} orelse t aconv @{prop False} orelse t aconv prev_t orelse + t aconv @{prop True} orelse t aconv @{prop False} orelse norm_t aconv prev_norm_t 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 role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse - is_datatype_rule rule orelse null lines orelse not (looks_boring ()) orelse - is_before_skolemize_rule () then - add_lines_pass2 (line :: res) t lines + if (Term.aconv_untyped (prev_norm_t, norm_t) andalso member (op =) deps prev_name) 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) else - add_lines_pass2 res prev_t (map (replace_dependencies_in_line (name, deps)) lines) + add_lines_pass2 (line :: res) (name, norm_t) lines end type isar_params = @@ -160,7 +165,7 @@ val atp_proof = fold_rev add_line_pass1 atp_proof [] - |> add_lines_pass2 [] Term.dummy + |> add_lines_pass2 [] (("", []), Term.dummy) val conjs = map_filter (fn (name, role, _, _, _) =>