1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Mon Dec 16 09:48:26 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Mon Dec 16 12:02:28 2013 +0100
     1.3 @@ -104,17 +104,17 @@
     1.4  
     1.5  fun tac_of_method method type_enc lam_trans ctxt facts =
     1.6    (case method of
     1.7 -    MetisM => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts
     1.8 -  | MesonM => Meson.meson_tac ctxt facts
     1.9 +    Metis_Method => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts
    1.10 +  | Meson_Method => Meson.meson_tac ctxt facts
    1.11    | _ =>
    1.12      Method.insert_tac facts THEN'
    1.13      (case method of
    1.14 -      SimpM => Simplifier.asm_full_simp_tac ctxt
    1.15 -    | AutoM => K (Clasimp.auto_tac ctxt)
    1.16 -    | FastforceM => Clasimp.fast_force_tac ctxt
    1.17 -    | ForceM => Clasimp.force_tac ctxt
    1.18 -    | ArithM => Arith_Data.arith_tac ctxt
    1.19 -    | BlastM => blast_tac ctxt
    1.20 +      Simp_Method => Simplifier.asm_full_simp_tac ctxt
    1.21 +    | Auto_Method => K (Clasimp.auto_tac ctxt)
    1.22 +    | Fastforce_Method => Clasimp.fast_force_tac ctxt
    1.23 +    | Force_Method => Clasimp.force_tac ctxt
    1.24 +    | Arith_Method => Arith_Data.arith_tac ctxt
    1.25 +    | Blast_Method => blast_tac ctxt
    1.26      | _ => raise Fail "Sledgehammer_Preplay: tac_of_method"))
    1.27  
    1.28  (* main function for preplaying Isar steps; may throw exceptions *)

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Mon Dec 16 09:48:26 2013 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Mon Dec 16 12:02:28 2013 +0100
     2.3 @@ -174,20 +174,20 @@
     2.4  
     2.5      fun by_method meth = "by " ^
     2.6        (case meth of
     2.7 -        SimpM => "simp"
     2.8 -      | AutoM => "auto"
     2.9 -      | FastforceM => "fastforce"
    2.10 -      | ForceM => "force"
    2.11 -      | ArithM => "arith"
    2.12 -      | BlastM => "blast"
    2.13 -      | MesonM => "meson"
    2.14 +        Simp_Method => "simp"
    2.15 +      | Auto_Method => "auto"
    2.16 +      | Fastforce_Method => "fastforce"
    2.17 +      | Force_Method => "force"
    2.18 +      | Arith_Method => "arith"
    2.19 +      | Blast_Method => "blast"
    2.20 +      | Meson_Method => "meson"
    2.21        | _ => raise Fail "Sledgehammer_Print: by_method")
    2.22  
    2.23      fun using_facts [] [] = ""
    2.24        | using_facts ls ss =
    2.25            "using " ^ space_implode " " (map string_of_label ls @ ss) ^ " "
    2.26  
    2.27 -    fun of_method ls ss MetisM =
    2.28 +    fun of_method ls ss Metis_Method =
    2.29          reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 (ls, ss)
    2.30        | of_method ls ss meth = using_facts ls ss ^ by_method meth
    2.31  
    2.32 @@ -254,21 +254,16 @@
    2.33        | add_step ind (step as Prove (qs, xs, l, t, subproofs, (facts, meth))) =
    2.34          (case xs of
    2.35            [] => (* have *)
    2.36 -            add_step_pre ind qs subproofs
    2.37 -            #> add_suffix (of_prove qs (length subproofs) ^ " ")
    2.38 -            #> add_step_post ind l t facts meth ""
    2.39 +          add_step_pre ind qs subproofs
    2.40 +          #> add_suffix (of_prove qs (length subproofs) ^ " ")
    2.41 +          #> add_step_post ind l t facts meth ""
    2.42          | _ => (* obtain *)
    2.43 -            add_step_pre ind qs subproofs
    2.44 -            #> add_suffix (of_obtain qs (length subproofs) ^ " ")
    2.45 -            #> add_frees xs
    2.46 -            #> add_suffix " where "
    2.47 -            (* The new skolemizer puts the arguments in the same order as the ATPs (E and Vampire --
    2.48 -               but see also "atp_proof_reconstruct.ML" regarding Vampire). *)
    2.49 -            #> add_step_post ind l t facts meth
    2.50 -                 (if use_metis_new_skolem step then
    2.51 -                    "using [[metis_new_skolem]] "
    2.52 -                  else
    2.53 -                    ""))
    2.54 +          add_step_pre ind qs subproofs
    2.55 +          #> add_suffix (of_obtain qs (length subproofs) ^ " ")
    2.56 +          #> add_frees xs
    2.57 +          #> add_suffix " where "
    2.58 +          #> add_step_post ind l t facts meth
    2.59 +               (if use_metis_new_skolem step then "using [[metis_new_skolem]] " else ""))
    2.60  
    2.61      and add_steps ind = fold (add_step ind)
    2.62  
    2.63 @@ -278,7 +273,7 @@
    2.64      (* One-step Metis proofs are pointless; better use the one-liner directly. *)
    2.65      (case proof of
    2.66        Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *)
    2.67 -    | Proof ([], [], [Prove (_, [], _, _, [], (_, MetisM))]) => ""
    2.68 +    | Proof ([], [], [Prove (_, [], _, _, [], (_, Metis_Method))]) => ""
    2.69      | _ =>
    2.70        (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
    2.71        of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Mon Dec 16 09:48:26 2013 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Mon Dec 16 12:02:28 2013 +0100
     3.3 @@ -20,14 +20,8 @@
     3.4      Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
     3.5        (facts * proof_method)
     3.6    and proof_method =
     3.7 -    MetisM |
     3.8 -    SimpM |
     3.9 -    AutoM |
    3.10 -    FastforceM |
    3.11 -    ForceM |
    3.12 -    ArithM |
    3.13 -    BlastM |
    3.14 -    MesonM
    3.15 +    Metis_Method | Simp_Method | Auto_Method | Fastforce_Method | Force_Method | Arith_Method |
    3.16 +    Blast_Method | Meson_Method
    3.17  
    3.18    val no_label : label
    3.19    val no_facts : facts
    3.20 @@ -49,8 +43,7 @@
    3.21    val use_metis_new_skolem : isar_step -> bool
    3.22  
    3.23    val fold_isar_step : (isar_step -> 'a -> 'a) -> isar_step -> 'a -> 'a
    3.24 -  val fold_isar_steps :
    3.25 -    (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a
    3.26 +  val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a
    3.27  
    3.28    val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
    3.29  
    3.30 @@ -78,14 +71,8 @@
    3.31    Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
    3.32      (facts * proof_method)
    3.33  and proof_method =
    3.34 -  MetisM |
    3.35 -  SimpM |
    3.36 -  AutoM |
    3.37 -  FastforceM |
    3.38 -  ForceM |
    3.39 -  ArithM |
    3.40 -  BlastM |
    3.41 -  MesonM
    3.42 +  Metis_Method | Simp_Method | Auto_Method | Fastforce_Method | Force_Method | Arith_Method |
    3.43 +  Blast_Method | Meson_Method
    3.44  
    3.45  val no_label = ("", ~1)
    3.46  val no_facts = ([],[])
    3.47 @@ -112,24 +99,25 @@
    3.48  fun proof_method_of_step (Prove (_, _, _, _, _, (_, method))) = SOME method
    3.49    | proof_method_of_step _ = NONE
    3.50  
    3.51 +(* The new skolemizer puts the arguments in the same order as the ATPs (E and Vampire -- but see
    3.52 +   also "atp_proof_reconstruct.ML" concerning Vampire). *)
    3.53  fun use_metis_new_skolem (Prove (_, xs, _, _, _, (_, meth))) =
    3.54 -    meth = MetisM andalso exists (fn (_, T) => length (binder_types T) > 1) xs
    3.55 +    meth = Metis_Method andalso exists (fn (_, T) => length (binder_types T) > 1) xs
    3.56    | use_metis_new_skolem _ = false
    3.57  
    3.58  fun fold_isar_steps f = fold (fold_isar_step f)
    3.59 -and fold_isar_step f step s =
    3.60 -  fold (steps_of_proof #> fold_isar_steps f)
    3.61 -       (these (subproofs_of_step step)) s
    3.62 -    |> f step
    3.63 +and fold_isar_step f step =
    3.64 +  fold (steps_of_proof #> fold_isar_steps f) (these (subproofs_of_step step))
    3.65 +  #> f step
    3.66  
    3.67 -fun map_isar_steps f proof =
    3.68 +fun map_isar_steps f =
    3.69    let
    3.70      fun do_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map do_step steps)
    3.71      and do_step (step as Let _) = f step
    3.72        | do_step (Prove (qs, xs, l, t, subproofs, by)) =
    3.73          f (Prove (qs, xs, l, t, map do_proof subproofs, by))
    3.74    in
    3.75 -    do_proof proof
    3.76 +    do_proof
    3.77    end
    3.78  
    3.79  val add_proof_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I)

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Dec 16 09:48:26 2013 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Dec 16 12:02:28 2013 +0100
     4.3 @@ -288,9 +288,9 @@
     4.4            |> map (fn ((l, t), rule) =>
     4.5              let
     4.6                val (skos, meth) =
     4.7 -                if is_skolemize_rule rule then (skolems_of t, MetisM)
     4.8 -                else if is_arith_rule rule then ([], ArithM)
     4.9 -                else ([], AutoM)
    4.10 +                if is_skolemize_rule rule then (skolems_of t, Metis_Method)
    4.11 +                else if is_arith_rule rule then ([], Arith_Method)
    4.12 +                else ([], Auto_Method)
    4.13              in
    4.14                Prove ([], skos, l, t, [], (([], []), meth))
    4.15              end)
    4.16 @@ -340,7 +340,7 @@
    4.17              accum
    4.18              |> (if tainted = [] then
    4.19                    cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
    4.20 -                               ((the_list predecessor, []), MetisM)))
    4.21 +                               ((the_list predecessor, []), Metis_Method)))
    4.22                  else
    4.23                    I)
    4.24              |> rev
    4.25 @@ -355,7 +355,7 @@
    4.26                fun do_rest l step = isar_steps outer (SOME l) (step :: accum) infs
    4.27  
    4.28                val deps = fold add_fact_of_dependencies gamma no_facts
    4.29 -              val meth = if is_arith_rule rule then ArithM else MetisM
    4.30 +              val meth = if is_arith_rule rule then Arith_Method else Metis_Method
    4.31                val by = (deps, meth)
    4.32              in
    4.33                if is_clause_tainted c then
    4.34 @@ -363,15 +363,13 @@
    4.35                    [g] =>
    4.36                    if skolem andalso is_clause_tainted g then
    4.37                      let val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum) in
    4.38 -                      isar_steps outer (SOME l) [prove [subproof] (no_facts, MetisM)] []
    4.39 +                      isar_steps outer (SOME l) [prove [subproof] (no_facts, Metis_Method)] []
    4.40                      end
    4.41                    else
    4.42                      do_rest l (prove [] by)
    4.43                  | _ => do_rest l (prove [] by))
    4.44                else
    4.45 -                (if skolem then Prove ([], skolems_of t, l, t, [], by)
    4.46 -                 else prove [] by)
    4.47 -                |> do_rest l
    4.48 +                do_rest l (if skolem then Prove ([], skolems_of t, l, t, [], by) else prove [] by)
    4.49              end
    4.50            | isar_steps outer predecessor accum (Cases cases :: infs) =
    4.51              let
    4.52 @@ -383,14 +381,14 @@
    4.53                val step =
    4.54                  Prove (maybe_show outer c [], [], l, t,
    4.55                    map isar_case (filter_out (null o snd) cases),
    4.56 -                  ((the_list predecessor, []), MetisM))
    4.57 +                  ((the_list predecessor, []), Metis_Method))
    4.58              in
    4.59                isar_steps outer (SOME l) (step :: accum) infs
    4.60              end
    4.61          and isar_proof outer fix assms lems infs =
    4.62            Proof (fix, assms, lems @ isar_steps outer NONE [] infs)
    4.63  
    4.64 -        (* 60 seconds seems like a good interpreation of "no timeout" *)
    4.65 +        (* 60 seconds seems like a reasonable interpreation of "no timeout" *)
    4.66          val preplay_timeout = preplay_timeout |> the_default (seconds 60.0)
    4.67  
    4.68          val (preplay_interface as {overall_preplay_stats, ...}, isar_proof) =

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML	Mon Dec 16 09:48:26 2013 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML	Mon Dec 16 12:02:28 2013 +0100
     5.3 @@ -21,7 +21,9 @@
     5.4  open Sledgehammer_Proof
     5.5  open Sledgehammer_Preplay
     5.6  
     5.7 -val variant_methods = [SimpM, AutoM, ArithM, FastforceM, BlastM, ForceM, MetisM, MesonM]
     5.8 +val variant_methods =
     5.9 +  [Simp_Method, Auto_Method, Arith_Method, Fastforce_Method, Blast_Method, Force_Method,
    5.10 +   Metis_Method, Meson_Method]
    5.11  
    5.12  fun variants_of_step (Let _) = raise Fail "Sledgehammer_Try0: variants_of_step"
    5.13    | variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, meth))) =