# HG changeset patch
# User blanchet
# Date 1394791544 -3600
# Node ID fc937e7ef4c64c7b79b613793206d4d13438a0b6
# Parent  e03c0f6ad1b6be9e502da0f0014dff55156322ac
more simplification of trivial steps

diff -r e03c0f6ad1b6 -r fc937e7ef4c6 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Fri Mar 14 11:05:37 2014 +0100
+++ b/src/HOL/Sledgehammer.thy	Fri Mar 14 11:05:44 2014 +0100
@@ -34,4 +34,13 @@
 ML_file "Tools/Sledgehammer/sledgehammer.ML"
 ML_file "Tools/Sledgehammer/sledgehammer_commands.ML"
 
+definition plus1 where "plus1 x = x + (1::int)"
+
+ML {* print_depth 1000 *}
+
+lemma "map plus1 [0] = [1]"
+sledgehammer [z3_new, isar_proofs = true, mepo, debug, dont_preplay, dont_minimize, dont_try0_isar]
+(add: plus1_def)
+oops
+
 end
diff -r e03c0f6ad1b6 -r fc937e7ef4c6 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Fri Mar 14 11:05:37 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML	Fri Mar 14 11:05:44 2014 +0100
@@ -305,7 +305,7 @@
   | s_iff (t1, @{const True}) = t1
   | s_iff (@{const False}, t2) = s_not t2
   | s_iff (t1, @{const False}) = s_not t1
-  | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
+  | s_iff (t1, t2) = if t1 aconv t2 then @{const True} else HOLogic.eq_const HOLogic.boolT $ t1 $ t2
 
 fun close_form t =
   fold (fn ((s, i), T) => fn t' =>
diff -r e03c0f6ad1b6 -r fc937e7ef4c6 src/HOL/Tools/SMT2/z3_new_isar.ML
--- a/src/HOL/Tools/SMT2/z3_new_isar.ML	Fri Mar 14 11:05:37 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_isar.ML	Fri Mar 14 11:05:44 2014 +0100
@@ -68,6 +68,8 @@
   | simplify_prop (@{const disj} $ t $ u) = s_disj (simplify_prop t, simplify_prop u)
   | simplify_prop (@{const implies} $ t $ u) = s_imp (simplify_prop t, simplify_prop u)
   | simplify_prop (@{const HOL.eq (bool)} $ t $ u) = s_iff (simplify_prop t, simplify_prop u)
+  | simplify_prop (t as Const (@{const_name HOL.eq}, _) $ u $ v) =
+    if u aconv v then @{const True} else t
   | simplify_prop (t $ u) = simplify_prop t $ simplify_prop u
   | simplify_prop (Abs (s, T, t)) = Abs (s, T, simplify_prop t)
   | simplify_prop t = t
diff -r e03c0f6ad1b6 -r fc937e7ef4c6 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Mar 14 11:05:37 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Mar 14 11:05:44 2014 +0100
@@ -68,20 +68,20 @@
 fun add_fact_of_dependencies [(_, ss as _ :: _)] = apsnd (union (op =) ss)
   | add_fact_of_dependencies names = apfst (insert (op =) (label_of_clause names))
 
-(* No "real" literals means only type information (tfree_tcs, clsrel, or clsarity). *)
-fun is_only_type_information t = t aconv @{prop True}
+fun is_True_prop t = t aconv @{prop True}
 
 (* Discard facts; consolidate adjacent lines that prove the same formula, since they differ only in
    type information. *)
 fun add_line_pass1 (line as (name, role, t, rule, [])) lines =
     (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or
        definitions. *)
-    if role = Lemma orelse role = Conjecture orelse role = Negated_Conjecture orelse
-       role = Hypothesis orelse is_arith_rule rule then
+    if role = Conjecture orelse role = Negated_Conjecture then
       line :: lines
+    else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then
+      lines |> not (is_True_prop t) ? cons line
     else if role = Axiom then
       (* Facts are not proof lines. *)
-      lines |> is_only_type_information t ? map (replace_dependencies_in_line (name, []))
+      lines |> is_True_prop t ? map (replace_dependencies_in_line (name, []))
     else
       map (replace_dependencies_in_line (name, [])) lines
   | add_line_pass1 line lines = line :: lines
@@ -92,8 +92,8 @@
       val is_last_line = null lines
 
       fun looks_interesting () =
-        not (is_only_type_information t) andalso null (Term.add_tvars t [])
-        andalso length deps >= 2 andalso not (can the_single lines)
+        not (is_True_prop t) andalso null (Term.add_tvars t []) andalso length deps >= 2 andalso
+        not (can the_single lines)
 
       fun is_skolemizing_line (_, _, _, rule', deps') =
         is_skolemize_rule rule' andalso member (op =) deps' name