undo rewrite rules (e.g. for 'fun_app') in Isar

--- a/src/HOL/Sledgehammer.thy	Fri Mar 14 11:05:45 2014 +0100
+++ b/src/HOL/Sledgehammer.thy	Fri Mar 14 11:15:46 2014 +0100
@@ -34,13 +34,4 @@
 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

--- a/src/HOL/Tools/SMT2/smt2_solver.ML	Fri Mar 14 11:05:45 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Fri Mar 14 11:15:46 2014 +0100
@@ -26,14 +26,13 @@
   val add_solver: solver_config -> theory -> theory
   val solver_name_of: Proof.context -> string
   val available_solvers_of: Proof.context -> string list
-  val apply_solver: Proof.context -> (int option * thm) list ->
-    ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm
   val default_max_relevant: Proof.context -> string -> int
 
   (*filter*)
   val smt2_filter: Proof.context -> thm -> ('a * (int option * thm)) list -> int -> Time.time ->
-    {outcome: SMT2_Failure.failure option, conjecture_id: int, helper_ids: (int * thm) list,
-     fact_ids: (int * ('a * thm)) list, z3_proof: Z3_New_Proof.z3_step list}
+    {outcome: SMT2_Failure.failure option, rewrite_rules: thm list, conjecture_id: int,
+     helper_ids: (int * thm) list, fact_ids: (int * ('a * thm)) list,
+     z3_proof: Z3_New_Proof.z3_step list}
 
   (*tactic*)
   val smt2_tac: Proof.context -> thm list -> int -> tactic
@@ -239,7 +238,7 @@
     val wthms = map (apsnd (check_topsort ctxt)) wthms0
     val (name, {command, finish, ...}) = name_and_info_of ctxt
     val (output, replay_data) = invoke name command (SMT2_Normalize.normalize ctxt wthms) ctxt
-  in finish ctxt replay_data output end
+  in (finish ctxt replay_data output, replay_data) end
 
 val default_max_relevant = #default_max_relevant oo get_info
 val can_filter = #can_filter o snd o name_and_info_of 
@@ -275,12 +274,11 @@
   in
     wthms
     |> apply_solver ctxt
-    |> fst
-    |> (fn (iidths0, z3_proof) =>
-      let
-        val iidths = if can_filter ctxt then iidths0 else map (apsnd (apfst (K no_id))) iwthms
+    |> (fn (((iidths0, z3_proof), _), {rewrite_rules, ...}) =>
+      let val iidths = if can_filter ctxt then iidths0 else map (apsnd (apfst (K no_id))) iwthms
       in
-        {outcome = NONE, 
+        {outcome = NONE,
+         rewrite_rules = rewrite_rules,
          conjecture_id =
            the_default no_id (Option.map fst (AList.lookup (op =) iidths conjecture_i)),
          helper_ids = map_filter (try (fn (~1, idth) => idth)) iidths,
@@ -289,8 +287,8 @@
          z3_proof = z3_proof}
       end)
   end
-  handle SMT2_Failure.SMT fail => {outcome = SOME fail, conjecture_id = no_id, helper_ids = [],
-    fact_ids = [], z3_proof = []}
+  handle SMT2_Failure.SMT fail => {outcome = SOME fail, rewrite_rules = [], conjecture_id = no_id,
+    helper_ids = [], fact_ids = [], z3_proof = []}
 
 
 (* SMT tactic *)
@@ -307,6 +305,7 @@
   fun solve ctxt wfacts =
     wfacts
     |> apply_solver ctxt
+    |> fst
     |>> apfst (trace_assumptions ctxt wfacts)
     |> snd
 

--- a/src/HOL/Tools/SMT2/z3_new_isar.ML	Fri Mar 14 11:05:45 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_isar.ML	Fri Mar 14 11:15:46 2014 +0100
@@ -8,8 +8,8 @@
 sig
   type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
 
-  val atp_proof_of_z3_proof: theory -> int -> (int * string) list -> Z3_New_Proof.z3_step list ->
-    (term, string) atp_step list
+  val atp_proof_of_z3_proof: theory -> thm list -> int -> (int * string) list ->
+    Z3_New_Proof.z3_step list -> (term, string) atp_step list
 end;
 
 structure Z3_New_Isar: Z3_NEW_ISAR =
@@ -76,13 +76,14 @@
 
 fun simplify_line (name, role, t, rule, deps) = (name, role, simplify_prop t, rule, deps)
 
-fun atp_proof_of_z3_proof thy conjecture_id fact_ids proof =
+fun atp_proof_of_z3_proof thy rewrite_rules conjecture_id fact_ids proof =
   let
     fun step_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) =
       let
         fun step_name_of id = (string_of_int id, the_list (AList.lookup (op =) fact_ids id))
 
         val name as (_, ss) = step_name_of id
+
         val role =
           (case rule of
             Z3_New_Proof.Asserted =>
@@ -94,9 +95,13 @@
           | Z3_New_Proof.Skolemize => Lemma
           | Z3_New_Proof.Th_Lemma _ => Lemma
           | _ => Plain)
+
+        val concl' = concl
+          |> Raw_Simplifier.rewrite_term thy rewrite_rules []
+          |> Object_Logic.atomize_term thy
+          |> HOLogic.mk_Trueprop
       in
-        (name, role, HOLogic.mk_Trueprop (Object_Logic.atomize_term thy concl),
-         Z3_New_Proof.string_of_rule rule, map step_name_of prems)
+        (name, role, concl', Z3_New_Proof.string_of_rule rule, map step_name_of prems)
       end
   in
     proof

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Mar 14 11:05:45 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Mar 14 11:15:46 2014 +0100
@@ -89,9 +89,6 @@
 fun add_lines_pass2 res [] = rev res
   | add_lines_pass2 res ((line as (name, role, t, rule, deps)) :: lines) =
     let
-val line as (name, role, t, rule, deps) = (name, role, Term.map_aterms
-  (perhaps (try (fn Free (s, T) => Free (unsuffix "__" s, T)))) t
-  |> Term.map_abs_vars (perhaps (try (unsuffix "__"))), rule, deps) (*###*)
       val is_last_line = null lines
 
       fun looks_interesting () =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri Mar 14 11:05:45 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri Mar 14 11:15:46 2014 +0100
@@ -161,7 +161,8 @@
               reraise exn
             else
               {outcome = SOME (SMT2_Failure.Other_Failure (ML_Compiler.exn_message exn)),
-               conjecture_id = ~1, helper_ids = [], fact_ids = [], z3_proof = []}
+               rewrite_rules = [], conjecture_id = ~1, helper_ids = [], fact_ids = [],
+               z3_proof = []}
 
         val death = Timer.checkRealTimer timer
         val outcome0 = if is_none outcome0 then SOME outcome else outcome0
@@ -226,8 +227,9 @@
       end
 
     val weighted_factss = map (apsnd weight_facts) factss
-    val {outcome, filter_result = {conjecture_id, helper_ids, fact_ids, z3_proof, ...},
-         used_from, run_time} = smt2_filter_loop name params state goal subgoal weighted_factss
+    val {outcome, filter_result = {conjecture_id, rewrite_rules, helper_ids, fact_ids, z3_proof,
+           ...}, used_from, run_time} =
+      smt2_filter_loop name params state goal subgoal weighted_factss
     val used_named_facts = map snd fact_ids
     val used_facts = map fst used_named_facts
     val outcome = Option.map failure_of_smt2_failure outcome
@@ -243,7 +245,8 @@
               val fact_ids =
                 map (fn (id, th) => (id, short_thm_name ctxt th)) helper_ids @
                 map (fn (id, ((name, _), _)) => (id, name)) fact_ids
-              val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy conjecture_id fact_ids z3_proof
+              val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy rewrite_rules conjecture_id
+                fact_ids z3_proof
               val isar_params =
                 K (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
                    minimize <> SOME false, atp_proof, goal)