1.1 --- a/src/HOL/Tools/SMT2/z3_new_isar.ML	Thu May 22 04:12:06 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT2/z3_new_isar.ML	Thu May 22 05:23:50 2014 +0200
     1.3 @@ -84,8 +84,8 @@
     1.4    Term.map_abs_vars (perhaps (try Name.dest_skolem))
     1.5    #> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T))))
     1.6  
     1.7 -fun atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t fact_ts prem_ids conjecture_id fact_ids
     1.8 -    proof =
     1.9 +fun atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids conjecture_id
    1.10 +    fact_helper_ids proof =
    1.11    let
    1.12      val thy = Proof_Context.theory_of ctxt
    1.13  
    1.14 @@ -108,12 +108,12 @@
    1.15          (case rule of
    1.16            Z3_New_Proof.Asserted =>
    1.17            let
    1.18 -            val ss = the_list (AList.lookup (op =) fact_ids id)
    1.19 +            val ss = the_list (AList.lookup (op =) fact_helper_ids id)
    1.20              val name0 = (sid ^ "a", ss)
    1.21  
    1.22              val (role0, concl0) =
    1.23                (case ss of
    1.24 -                [s] => (Axiom, the (AList.lookup (op =) fact_ts s))
    1.25 +                [s] => (Axiom, the (AList.lookup (op =) fact_helper_ts s))
    1.26                | _ =>
    1.27                  if id = conjecture_id then
    1.28                    (Conjecture, concl_t)

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu May 22 04:12:06 2014 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu May 22 05:23:50 2014 +0200
     2.3 @@ -129,8 +129,7 @@
     2.4           ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} =>
     2.5                     print_used_facts used_facts used_from
     2.6                   | _ => ())
     2.7 -      |> spy
     2.8 -         ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
     2.9 +      |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
    2.10        |> (fn {outcome, preplay, message, message_tail, ...} =>
    2.11               (if outcome = SOME ATP_Proof.TimedOut then timeoutN
    2.12                else if is_some outcome then noneN
    2.13 @@ -143,13 +142,12 @@
    2.14              really_go ()
    2.15            else
    2.16              (really_go ()
    2.17 -             handle ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n")
    2.18 -                  | exn =>
    2.19 -                    if Exn.is_interrupt exn then
    2.20 -                      reraise exn
    2.21 -                    else
    2.22 -                      (unknownN, fn () => "Internal error:\n" ^
    2.23 -                                          Runtime.exn_message exn ^ "\n"))
    2.24 +             handle
    2.25 +               ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n")
    2.26 +             | exn =>
    2.27 +               if Exn.is_interrupt exn then reraise exn
    2.28 +               else (unknownN, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n"))
    2.29 +
    2.30          val _ =
    2.31            (* The "expect" argument is deliberately ignored if the prover is
    2.32               missing so that the "Metis_Examples" can be processed on any
    2.33 @@ -175,9 +173,7 @@
    2.34        let
    2.35          val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()
    2.36          val outcome =
    2.37 -          if outcome_code = someN orelse mode = Normal then
    2.38 -            quote name ^ ": " ^ message ()
    2.39 -          else ""
    2.40 +          if outcome_code = someN orelse mode = Normal then quote name ^ ": " ^ message () else ""
    2.41          val _ =
    2.42            if outcome <> "" andalso is_some output_result then
    2.43              the output_result outcome
    2.44 @@ -274,9 +270,8 @@
    2.45              if mode = Auto_Try then
    2.46                (unknownN, state)
    2.47                |> fold (fn prover => fn accum as (outcome_code, _) =>
    2.48 -                          if outcome_code = someN then accum
    2.49 -                          else launch problem prover)
    2.50 -                      provers
    2.51 +                  if outcome_code = someN then accum else launch problem prover)
    2.52 +                provers
    2.53              else
    2.54                provers
    2.55                |> (if blocking then Par_List.map else map) (launch problem #> fst)

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu May 22 04:12:06 2014 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu May 22 05:23:50 2014 +0200
     3.3 @@ -73,16 +73,11 @@
     3.4  fun add_line_pass1 (line as (name, role, t, rule, [])) lines =
     3.5      (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or
     3.6         definitions. *)
     3.7 -    if role = Conjecture orelse role = Negated_Conjecture then
     3.8 -      line :: lines
     3.9 -    else if is_True_prop t then
    3.10 -      map (replace_dependencies_in_line (name, [])) lines
    3.11 -    else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then
    3.12 -      line :: lines
    3.13 -    else if role = Axiom then
    3.14 -      lines (* axioms (facts) need no proof lines *)
    3.15 -    else
    3.16 -      map (replace_dependencies_in_line (name, [])) lines
    3.17 +    if role = Conjecture orelse role = Negated_Conjecture then line :: lines
    3.18 +    else if is_True_prop t then map (replace_dependencies_in_line (name, [])) lines
    3.19 +    else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then line :: lines
    3.20 +    else if role = Axiom then lines (* axioms (facts) need no proof lines *)
    3.21 +    else map (replace_dependencies_in_line (name, [])) lines
    3.22    | add_line_pass1 line lines = line :: lines
    3.23  
    3.24  fun add_lines_pass2 res _ [] = rev res
    3.25 @@ -364,7 +359,9 @@
    3.26            SOME s => s
    3.27          | NONE =>
    3.28            if isar_proofs = SOME true then "\nWarning: Isar proof construction failed." else "")
    3.29 -  in one_line_proof ^ isar_proof end
    3.30 +  in
    3.31 +    one_line_proof ^ isar_proof
    3.32 +  end
    3.33  
    3.34  fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) =
    3.35    (case play of

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu May 22 04:12:06 2014 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu May 22 05:23:50 2014 +0200
     4.3 @@ -63,8 +63,8 @@
     4.4       message_tail : string}
     4.5  
     4.6    type prover =
     4.7 -    params -> ((string * string list) list -> string -> minimize_command)
     4.8 -    -> prover_problem -> prover_result
     4.9 +    params -> ((string * string list) list -> string -> minimize_command) -> prover_problem ->
    4.10 +    prover_result
    4.11  
    4.12    val SledgehammerN : string
    4.13    val str_of_mode : mode -> string
    4.14 @@ -76,8 +76,7 @@
    4.15    val is_atp : theory -> string -> bool
    4.16    val bunch_of_proof_methods : bool -> bool -> string -> proof_method list
    4.17    val is_fact_chained : (('a * stature) * 'b) -> bool
    4.18 -  val filter_used_facts :
    4.19 -    bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
    4.20 +  val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
    4.21      ((''a * stature) * 'b) list
    4.22    val play_one_line_proof : mode -> bool -> Time.time -> ((string * 'a) * thm) list ->
    4.23      Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome
    4.24 @@ -294,8 +293,7 @@
    4.25        sort_strings (SMT2_Config.available_solvers_of ctxt)
    4.26        |> List.partition (String.isPrefix remote_prefix)
    4.27    in
    4.28 -    Output.urgent_message ("Supported provers: " ^
    4.29 -                           commas (local_provers @ remote_provers) ^ ".")
    4.30 +    Output.urgent_message ("Supported provers: " ^ commas (local_provers @ remote_provers) ^ ".")
    4.31    end
    4.32  
    4.33  fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover"

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu May 22 04:12:06 2014 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu May 22 05:23:50 2014 +0200
     5.3 @@ -242,15 +242,22 @@
     5.4               SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
     5.5           fn preplay =>
     5.6              let
     5.7 -              val fact_ids =
     5.8 -                map (fn (id, th) => (id, short_thm_name ctxt th)) helper_ids @
     5.9 -                map (fn (id, ((name, _), _)) => (id, name)) fact_ids
    5.10 -              val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t
    5.11 -                (map (fn ((s, _), th) => (s, prop_of th)) used_named_facts) prem_ids conjecture_id
    5.12 -                fact_ids z3_proof
    5.13 -              val isar_params =
    5.14 -                K (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
    5.15 +              fun isar_params () =
    5.16 +                let
    5.17 +                  val fact_helper_ts =
    5.18 +                    map (fn (_, th) => (short_thm_name ctxt th, prop_of th)) helper_ids @
    5.19 +                    map (fn ((s, _), th) => (s, prop_of th)) used_named_facts
    5.20 +                  val fact_helper_ids =
    5.21 +                    map (fn (id, th) => (id, short_thm_name ctxt th)) helper_ids @
    5.22 +                    map (fn (id, ((name, _), _)) => (id, name)) fact_ids
    5.23 +
    5.24 +                  val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts
    5.25 +                    concl_t fact_helper_ts prem_ids conjecture_id fact_helper_ids z3_proof
    5.26 +                in
    5.27 +                  (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
    5.28                     minimize <> SOME false, atp_proof, goal)
    5.29 +                end
    5.30 +
    5.31                val one_line_params =
    5.32                  (preplay, proof_banner mode name, used_facts,
    5.33                   choose_minimize_command thy params minimize_command name preplay, subgoal,