1.1 --- a/src/HOL/Sledgehammer.thy	Fri Mar 14 11:05:45 2014 +0100
     1.2 +++ b/src/HOL/Sledgehammer.thy	Fri Mar 14 11:15:46 2014 +0100
     1.3 @@ -34,13 +34,4 @@
     1.4  ML_file "Tools/Sledgehammer/sledgehammer.ML"
     1.5  ML_file "Tools/Sledgehammer/sledgehammer_commands.ML"
     1.6  
     1.7 -definition plus1 where "plus1 x = x + (1::int)"
     1.8 -
     1.9 -ML {* print_depth 1000 *}
    1.10 -
    1.11 -lemma "map plus1 [0] = [1]"
    1.12 -sledgehammer [z3_new, isar_proofs = true, mepo, debug, dont_preplay, dont_minimize, dont_try0_isar]
    1.13 -(add: plus1_def)
    1.14 -oops
    1.15 -
    1.16  end

     2.1 --- a/src/HOL/Tools/SMT2/smt2_solver.ML	Fri Mar 14 11:05:45 2014 +0100
     2.2 +++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Fri Mar 14 11:15:46 2014 +0100
     2.3 @@ -26,14 +26,13 @@
     2.4    val add_solver: solver_config -> theory -> theory
     2.5    val solver_name_of: Proof.context -> string
     2.6    val available_solvers_of: Proof.context -> string list
     2.7 -  val apply_solver: Proof.context -> (int option * thm) list ->
     2.8 -    ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm
     2.9    val default_max_relevant: Proof.context -> string -> int
    2.10  
    2.11    (*filter*)
    2.12    val smt2_filter: Proof.context -> thm -> ('a * (int option * thm)) list -> int -> Time.time ->
    2.13 -    {outcome: SMT2_Failure.failure option, conjecture_id: int, helper_ids: (int * thm) list,
    2.14 -     fact_ids: (int * ('a * thm)) list, z3_proof: Z3_New_Proof.z3_step list}
    2.15 +    {outcome: SMT2_Failure.failure option, rewrite_rules: thm list, conjecture_id: int,
    2.16 +     helper_ids: (int * thm) list, fact_ids: (int * ('a * thm)) list,
    2.17 +     z3_proof: Z3_New_Proof.z3_step list}
    2.18  
    2.19    (*tactic*)
    2.20    val smt2_tac: Proof.context -> thm list -> int -> tactic
    2.21 @@ -239,7 +238,7 @@
    2.22      val wthms = map (apsnd (check_topsort ctxt)) wthms0
    2.23      val (name, {command, finish, ...}) = name_and_info_of ctxt
    2.24      val (output, replay_data) = invoke name command (SMT2_Normalize.normalize ctxt wthms) ctxt
    2.25 -  in finish ctxt replay_data output end
    2.26 +  in (finish ctxt replay_data output, replay_data) end
    2.27  
    2.28  val default_max_relevant = #default_max_relevant oo get_info
    2.29  val can_filter = #can_filter o snd o name_and_info_of 
    2.30 @@ -275,12 +274,11 @@
    2.31    in
    2.32      wthms
    2.33      |> apply_solver ctxt
    2.34 -    |> fst
    2.35 -    |> (fn (iidths0, z3_proof) =>
    2.36 -      let
    2.37 -        val iidths = if can_filter ctxt then iidths0 else map (apsnd (apfst (K no_id))) iwthms
    2.38 +    |> (fn (((iidths0, z3_proof), _), {rewrite_rules, ...}) =>
    2.39 +      let val iidths = if can_filter ctxt then iidths0 else map (apsnd (apfst (K no_id))) iwthms
    2.40        in
    2.41 -        {outcome = NONE, 
    2.42 +        {outcome = NONE,
    2.43 +         rewrite_rules = rewrite_rules,
    2.44           conjecture_id =
    2.45             the_default no_id (Option.map fst (AList.lookup (op =) iidths conjecture_i)),
    2.46           helper_ids = map_filter (try (fn (~1, idth) => idth)) iidths,
    2.47 @@ -289,8 +287,8 @@
    2.48           z3_proof = z3_proof}
    2.49        end)
    2.50    end
    2.51 -  handle SMT2_Failure.SMT fail => {outcome = SOME fail, conjecture_id = no_id, helper_ids = [],
    2.52 -    fact_ids = [], z3_proof = []}
    2.53 +  handle SMT2_Failure.SMT fail => {outcome = SOME fail, rewrite_rules = [], conjecture_id = no_id,
    2.54 +    helper_ids = [], fact_ids = [], z3_proof = []}
    2.55  
    2.56  
    2.57  (* SMT tactic *)
    2.58 @@ -307,6 +305,7 @@
    2.59    fun solve ctxt wfacts =
    2.60      wfacts
    2.61      |> apply_solver ctxt
    2.62 +    |> fst
    2.63      |>> apfst (trace_assumptions ctxt wfacts)
    2.64      |> snd
    2.65  

     3.1 --- a/src/HOL/Tools/SMT2/z3_new_isar.ML	Fri Mar 14 11:05:45 2014 +0100
     3.2 +++ b/src/HOL/Tools/SMT2/z3_new_isar.ML	Fri Mar 14 11:15:46 2014 +0100
     3.3 @@ -8,8 +8,8 @@
     3.4  sig
     3.5    type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
     3.6  
     3.7 -  val atp_proof_of_z3_proof: theory -> int -> (int * string) list -> Z3_New_Proof.z3_step list ->
     3.8 -    (term, string) atp_step list
     3.9 +  val atp_proof_of_z3_proof: theory -> thm list -> int -> (int * string) list ->
    3.10 +    Z3_New_Proof.z3_step list -> (term, string) atp_step list
    3.11  end;
    3.12  
    3.13  structure Z3_New_Isar: Z3_NEW_ISAR =
    3.14 @@ -76,13 +76,14 @@
    3.15  
    3.16  fun simplify_line (name, role, t, rule, deps) = (name, role, simplify_prop t, rule, deps)
    3.17  
    3.18 -fun atp_proof_of_z3_proof thy conjecture_id fact_ids proof =
    3.19 +fun atp_proof_of_z3_proof thy rewrite_rules conjecture_id fact_ids proof =
    3.20    let
    3.21      fun step_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) =
    3.22        let
    3.23          fun step_name_of id = (string_of_int id, the_list (AList.lookup (op =) fact_ids id))
    3.24  
    3.25          val name as (_, ss) = step_name_of id
    3.26 +
    3.27          val role =
    3.28            (case rule of
    3.29              Z3_New_Proof.Asserted =>
    3.30 @@ -94,9 +95,13 @@
    3.31            | Z3_New_Proof.Skolemize => Lemma
    3.32            | Z3_New_Proof.Th_Lemma _ => Lemma
    3.33            | _ => Plain)
    3.34 +
    3.35 +        val concl' = concl
    3.36 +          |> Raw_Simplifier.rewrite_term thy rewrite_rules []
    3.37 +          |> Object_Logic.atomize_term thy
    3.38 +          |> HOLogic.mk_Trueprop
    3.39        in
    3.40 -        (name, role, HOLogic.mk_Trueprop (Object_Logic.atomize_term thy concl),
    3.41 -         Z3_New_Proof.string_of_rule rule, map step_name_of prems)
    3.42 +        (name, role, concl', Z3_New_Proof.string_of_rule rule, map step_name_of prems)
    3.43        end
    3.44    in
    3.45      proof

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

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri Mar 14 11:05:45 2014 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri Mar 14 11:15:46 2014 +0100
     5.3 @@ -161,7 +161,8 @@
     5.4                reraise exn
     5.5              else
     5.6                {outcome = SOME (SMT2_Failure.Other_Failure (ML_Compiler.exn_message exn)),
     5.7 -               conjecture_id = ~1, helper_ids = [], fact_ids = [], z3_proof = []}
     5.8 +               rewrite_rules = [], conjecture_id = ~1, helper_ids = [], fact_ids = [],
     5.9 +               z3_proof = []}
    5.10  
    5.11          val death = Timer.checkRealTimer timer
    5.12          val outcome0 = if is_none outcome0 then SOME outcome else outcome0
    5.13 @@ -226,8 +227,9 @@
    5.14        end
    5.15  
    5.16      val weighted_factss = map (apsnd weight_facts) factss
    5.17 -    val {outcome, filter_result = {conjecture_id, helper_ids, fact_ids, z3_proof, ...},
    5.18 -         used_from, run_time} = smt2_filter_loop name params state goal subgoal weighted_factss
    5.19 +    val {outcome, filter_result = {conjecture_id, rewrite_rules, helper_ids, fact_ids, z3_proof,
    5.20 +           ...}, used_from, run_time} =
    5.21 +      smt2_filter_loop name params state goal subgoal weighted_factss
    5.22      val used_named_facts = map snd fact_ids
    5.23      val used_facts = map fst used_named_facts
    5.24      val outcome = Option.map failure_of_smt2_failure outcome
    5.25 @@ -243,7 +245,8 @@
    5.26                val fact_ids =
    5.27                  map (fn (id, th) => (id, short_thm_name ctxt th)) helper_ids @
    5.28                  map (fn (id, ((name, _), _)) => (id, name)) fact_ids
    5.29 -              val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy conjecture_id fact_ids z3_proof
    5.30 +              val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy rewrite_rules conjecture_id
    5.31 +                fact_ids z3_proof
    5.32                val isar_params =
    5.33                  K (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
    5.34                     minimize <> SOME false, atp_proof, goal)