use 'simp add:' syntax in Sledgehammer rather than 'using'
authorblanchet
Fri May 16 19:13:50 2014 +0200 (2014-05-16)
changeset 56983132142089ea6
parent 56982 51d4189d95cf
child 56984 d20f19f54789
use 'simp add:' syntax in Sledgehammer rather than 'using'
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 16 19:13:50 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 16 19:13:50 2014 +0200
     1.3 @@ -295,7 +295,7 @@
     1.4          fun str_of_preplay_outcome outcome =
     1.5            if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
     1.6          fun str_of_meth l meth =
     1.7 -          string_of_proof_method meth ^ " " ^
     1.8 +          string_of_proof_method [] meth ^ " " ^
     1.9            str_of_preplay_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)
    1.10          fun comment_of l = map (str_of_meth l) #> commas
    1.11  
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri May 16 19:13:50 2014 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri May 16 19:13:50 2014 +0200
     2.3 @@ -248,18 +248,13 @@
     2.4              |> maybe_quote),
     2.5         ctxt |> Variable.auto_fixes term)
     2.6  
     2.7 -    fun with_facts none _ [] [] = none
     2.8 -      | with_facts _ some ls ss = some (space_implode " " (map string_of_label ls @ ss))
     2.9 -
    2.10 -    val using_facts = with_facts "" (enclose "using " " ")
    2.11 -
    2.12 -    fun maybe_paren s = s |> String.isSubstring " " s ? enclose "(" ")"
    2.13 -    fun by_facts meth ls ss =
    2.14 -      "by " ^ with_facts (maybe_paren meth) (enclose ("(" ^ meth ^ " ") ")") ls ss
    2.15 +    fun using_facts [] [] = ""
    2.16 +      | using_facts ls ss = enclose "using " " " (space_implode " " (map string_of_label ls @ ss))
    2.17  
    2.18      fun is_direct_method (Metis_Method _) = true
    2.19        | is_direct_method Meson_Method = true
    2.20        | is_direct_method SMT2_Method = true
    2.21 +      | is_direct_method Simp_Method = true
    2.22        | is_direct_method _ = false
    2.23  
    2.24      (* Local facts are always passed via "using", which affects "meson" and "metis". This is
    2.25 @@ -269,7 +264,7 @@
    2.26      fun of_method ls ss meth =
    2.27        let val direct = is_direct_method meth in
    2.28          using_facts ls (if direct then [] else ss) ^
    2.29 -        by_facts (string_of_proof_method meth) [] (if direct then ss else [])
    2.30 +        "by " ^ string_of_proof_method (if direct then ss else []) meth
    2.31        end
    2.32  
    2.33      fun of_free (s, T) =
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Fri May 16 19:13:50 2014 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Fri May 16 19:13:50 2014 +0200
     3.3 @@ -33,7 +33,7 @@
     3.4    type one_line_params =
     3.5      (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
     3.6  
     3.7 -  val string_of_proof_method : proof_method -> string
     3.8 +  val string_of_proof_method : string list -> proof_method -> string
     3.9    val tac_of_proof_method : Proof.context -> bool -> thm list * thm list -> proof_method -> int ->
    3.10      tactic
    3.11    val string_of_play_outcome : play_outcome -> string
    3.12 @@ -72,23 +72,30 @@
    3.13  type one_line_params =
    3.14    (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
    3.15  
    3.16 -fun string_of_proof_method meth =
    3.17 -  (case meth of
    3.18 -    Metis_Method (NONE, NONE) => "metis"
    3.19 -  | Metis_Method (type_enc_opt, lam_trans_opt) =>
    3.20 -    "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
    3.21 -  | Meson_Method => "meson"
    3.22 -  | SMT2_Method => "smt2"
    3.23 -  | SATx_Method => "satx"
    3.24 -  | Blast_Method => "blast"
    3.25 -  | Simp_Method => "simp"
    3.26 -  | Simp_Size_Method => "simp add: size_ne_size_imp_ne"
    3.27 -  | Auto_Method => "auto"
    3.28 -  | Fastforce_Method => "fastforce"
    3.29 -  | Force_Method => "force"
    3.30 -  | Linarith_Method => "linarith"
    3.31 -  | Presburger_Method => "presburger"
    3.32 -  | Algebra_Method => "algebra")
    3.33 +fun maybe_paren s = s |> not (Symbol_Pos.is_identifier s) ? enclose "(" ")"
    3.34 +
    3.35 +fun string_of_proof_method ss meth =
    3.36 +  let
    3.37 +    val meth_s =
    3.38 +      (case meth of
    3.39 +        Metis_Method (NONE, NONE) => "metis"
    3.40 +      | Metis_Method (type_enc_opt, lam_trans_opt) =>
    3.41 +        "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
    3.42 +      | Meson_Method => "meson"
    3.43 +      | SMT2_Method => "smt2"
    3.44 +      | SATx_Method => "satx"
    3.45 +      | Blast_Method => "blast"
    3.46 +      | Simp_Method => if null ss then "simp" else "simp add:"
    3.47 +      | Simp_Size_Method => "simp add: size_ne_size_imp_ne"
    3.48 +      | Auto_Method => "auto"
    3.49 +      | Fastforce_Method => "fastforce"
    3.50 +      | Force_Method => "force"
    3.51 +      | Linarith_Method => "linarith"
    3.52 +      | Presburger_Method => "presburger"
    3.53 +      | Algebra_Method => "algebra")
    3.54 +  in
    3.55 +    maybe_paren (space_implode " " (meth_s :: ss))
    3.56 +  end
    3.57  
    3.58  fun tac_of_proof_method ctxt debug (local_facts, global_facts) meth =
    3.59    Method.insert_tac local_facts THEN'
    3.60 @@ -98,12 +105,12 @@
    3.61        (lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts
    3.62    | Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts
    3.63    | SMT2_Method => SMT2_Solver.smt2_tac ctxt global_facts
    3.64 +  | Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts)
    3.65    | _ =>
    3.66      Method.insert_tac global_facts THEN'
    3.67      (case meth of
    3.68        SATx_Method => SAT.satx_tac ctxt
    3.69      | Blast_Method => blast_tac ctxt
    3.70 -    | Simp_Method => Simplifier.asm_full_simp_tac ctxt
    3.71      | Simp_Size_Method =>
    3.72        Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
    3.73      | Auto_Method => K (Clasimp.auto_tac ctxt)
    3.74 @@ -128,27 +135,14 @@
    3.75    | play_outcome_ord (_, Play_Timed_Out _) = GREATER
    3.76    | play_outcome_ord (Play_Failed, Play_Failed) = EQUAL
    3.77  
    3.78 -(* FIXME: Various bugs, esp. with "unfolding"
    3.79 -fun unusing_chained_facts _ 0 = ""
    3.80 -  | unusing_chained_facts used_chaineds num_chained =
    3.81 -    if length used_chaineds = num_chained then ""
    3.82 -    else if null used_chaineds then "(* using no facts *) "
    3.83 -    else "(* using only " ^ space_implode " " used_chaineds ^ " *) "
    3.84 -*)
    3.85 -
    3.86  fun apply_on_subgoal _ 1 = "by "
    3.87    | apply_on_subgoal 1 _ = "apply "
    3.88    | apply_on_subgoal i n =
    3.89      "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
    3.90  
    3.91 -fun command_call name [] =
    3.92 -    name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
    3.93 -  | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
    3.94 -
    3.95  (* FIXME *)
    3.96 -fun proof_method_command meth i n used_chaineds num_chained ss =
    3.97 -  (* unusing_chained_facts used_chaineds num_chained ^ *)
    3.98 -  apply_on_subgoal i n ^ command_call (string_of_proof_method meth) ss
    3.99 +fun proof_method_command meth i n _(*used_chaineds*) _(*num_chained*) ss =
   3.100 +  apply_on_subgoal i n ^ string_of_proof_method ss meth
   3.101  
   3.102  fun try_command_line banner play command =
   3.103    let val s = string_of_play_outcome play in
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri May 16 19:13:50 2014 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri May 16 19:13:50 2014 +0200
     4.3 @@ -230,7 +230,7 @@
     4.4              let
     4.5                val _ =
     4.6                  if verbose then
     4.7 -                  Output.urgent_message ("Trying \"" ^ string_of_proof_method meth ^
     4.8 +                  Output.urgent_message ("Trying \"" ^ string_of_proof_method [] meth ^
     4.9                      "\" for " ^ string_of_time timeout ^ "...")
    4.10                  else
    4.11                    ()
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri May 16 19:13:50 2014 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri May 16 19:13:50 2014 +0200
     5.3 @@ -221,6 +221,8 @@
     5.4      val thy = Proof.theory_of state
     5.5      val ctxt = Proof.context_of state
     5.6  
     5.7 +    val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
     5.8 +
     5.9      fun weight_facts facts =
    5.10        let val num_facts = length facts in
    5.11          map (weight_smt2_fact ctxt num_facts) (facts ~~ (0 upto num_facts - 1))
    5.12 @@ -245,8 +247,8 @@
    5.13                val fact_ids =
    5.14                  map (fn (id, th) => (id, short_thm_name ctxt th)) helper_ids @
    5.15                  map (fn (id, ((name, _), _)) => (id, name)) fact_ids
    5.16 -              val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy rewrite_rules prem_ids conjecture_id
    5.17 -                fact_ids z3_proof
    5.18 +              val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t
    5.19 +                prem_ids conjecture_id fact_ids z3_proof
    5.20                val isar_params =
    5.21                  K (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
    5.22                     minimize <> SOME false, atp_proof, goal)