1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sun Dec 15 18:01:38 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sun Dec 15 18:01:38 2013 +0100
     1.3 @@ -22,7 +22,7 @@
     1.4      Proof.context -> bool option -> (unit -> isar_params) -> int -> one_line_params -> string
     1.5  end;
     1.6  
     1.7 -structure Sledgehammer_Reconstruct (* ### : SLEDGEHAMMER_RECONSTRUCT *) =
     1.8 +structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT =
     1.9  struct
    1.10  
    1.11  open ATP_Util
    1.12 @@ -53,7 +53,7 @@
    1.13  val e_skolemize_rule = "skolemize"
    1.14  val vampire_skolemisation_rule = "skolemisation"
    1.15  (* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *)
    1.16 -val z3_skolemize_rule = "skolemize"
    1.17 +val z3_skolemize_rule = "sk"
    1.18  val z3_hypothesis_rule = "hypothesis"
    1.19  val z3_lemma_rule = "lemma"
    1.20  val z3_intro_def_rule = "intro-def"
    1.21 @@ -253,8 +253,11 @@
    1.22      val one_line_proof = one_line_proof_text 0 one_line_params
    1.23      val do_preplay = preplay_timeout <> SOME Time.zeroTime
    1.24  
    1.25 -    fun get_role keep_role ((num, _), role, t, _, _) =
    1.26 -      if keep_role role then SOME (raw_label_of_num num, t) else NONE
    1.27 +    val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
    1.28 +    fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
    1.29 +
    1.30 +    fun get_role keep_role ((num, _), role, t, rule, _) =
    1.31 +      if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE
    1.32  
    1.33      fun isar_proof_of () =
    1.34        let
    1.35 @@ -270,10 +273,14 @@
    1.36            map_filter (fn (name, role, _, _, _) =>
    1.37                if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE)
    1.38              atp_proof
    1.39 -        val assms = map_filter (get_role (curry (op =) Hypothesis)) atp_proof
    1.40 +        val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof
    1.41          val lems =
    1.42            map_filter (get_role (curry (op =) Lemma)) atp_proof
    1.43 -          |> map (fn (l, t) => Prove ([], [], l, maybe_mk_Trueprop t, [], (([], []), ArithM)))
    1.44 +          |> map (fn ((l, t), rule) =>
    1.45 +            if is_skolemize_rule rule then
    1.46 +              Prove ([], skolems_of t, l, maybe_mk_Trueprop t, [], (([], []), MetisM))
    1.47 +            else
    1.48 +              Prove ([], [], l, maybe_mk_Trueprop t, [], (([], []), ArithM)))
    1.49  
    1.50          val bot = atp_proof |> List.last |> #1
    1.51  
    1.52 @@ -318,9 +325,6 @@
    1.53              end
    1.54              |> HOLogic.mk_Trueprop |> close_form
    1.55  
    1.56 -        val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
    1.57 -        fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
    1.58 -
    1.59          fun maybe_show outer c =
    1.60            (outer andalso length c = 1 andalso subset (op =) (c, conjs)) ? cons Show
    1.61  
    1.62 @@ -344,19 +348,16 @@
    1.63                  (case gamma of
    1.64                    [g] =>
    1.65                    if is_clause_skolemize_rule g andalso is_clause_tainted g then
    1.66 -                    let
    1.67 -                      val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum)
    1.68 -                    in
    1.69 +                    let val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum) in
    1.70                        isar_steps outer (SOME l) [prove [subproof] (no_facts, MetisM)] []
    1.71                      end
    1.72                    else
    1.73                      do_rest l (prove [] by)
    1.74                  | _ => do_rest l (prove [] by))
    1.75                else
    1.76 -                if is_clause_skolemize_rule c then
    1.77 -                  do_rest l (Prove ([], skolems_of t, l, t, [], by))
    1.78 -                else
    1.79 -                  do_rest l (prove [] by)
    1.80 +                (if is_clause_skolemize_rule c then Prove ([], skolems_of t, l, t, [], by)
    1.81 +                 else prove [] by)
    1.82 +                |> do_rest l
    1.83              end
    1.84            | isar_steps outer predecessor accum (Cases cases :: infs) =
    1.85              let
    1.86 @@ -386,11 +387,11 @@
    1.87          val (preplay_interface as {overall_preplay_stats, ...}, isar_proof) =
    1.88            refute_graph
    1.89  (*
    1.90 -          |> tap (tracing o prefix "REFUTE GRAPH: " o string_of_refute_graph)
    1.91 +          |> tap (tracing o prefix "Refute graph: " o string_of_refute_graph)
    1.92  *)
    1.93            |> redirect_graph axioms tainted bot
    1.94  (*
    1.95 -          |> tap (tracing o prefix "DIRECT PROOF: " o string_of_direct_proof)
    1.96 +          |> tap (tracing o prefix "Direct proof: " o string_of_direct_proof)
    1.97  *)
    1.98            |> isar_proof_of_direct_proof
    1.99            |> postprocess_remove_unreferenced_steps I