src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
changeset 60252 2c468c062589
parent 59058 a78612c67ec0
child 60305 7d278b0617d3
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sun May 03 18:14:11 2015 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sun May 03 22:15:29 2015 +0200
     1.3 @@ -34,6 +34,7 @@
     1.4      ((string * stature) list * (proof_method * play_outcome)) * string * int * int
     1.5  
     1.6    val is_proof_method_direct : proof_method -> bool
     1.7 +  val proof_method_distinguishes_chained_and_direct : proof_method -> bool
     1.8    val string_of_proof_method : Proof.context -> string list -> proof_method -> string
     1.9    val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
    1.10    val thms_influence_proof_method : Proof.context -> proof_method -> thm list -> bool
    1.11 @@ -80,6 +81,10 @@
    1.12    | is_proof_method_direct Simp_Size_Method = true
    1.13    | is_proof_method_direct _ = false
    1.14  
    1.15 +fun proof_method_distinguishes_chained_and_direct Simp_Method = true
    1.16 +  | proof_method_distinguishes_chained_and_direct Simp_Size_Method = true
    1.17 +  | proof_method_distinguishes_chained_and_direct _ = false
    1.18 +
    1.19  fun is_proof_method_multi_goal Auto_Method = true
    1.20    | is_proof_method_multi_goal _ = false
    1.21  
    1.22 @@ -163,8 +168,14 @@
    1.23    | apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
    1.24  
    1.25  (* FIXME *)
    1.26 -fun proof_method_command ctxt meth i n _(*used_chaineds*) _(*num_chained*) ss =
    1.27 -  let val (indirect_ss, direct_ss) = if is_proof_method_direct meth then ([], ss) else (ss, []) in
    1.28 +fun proof_method_command ctxt meth i n used_chaineds _(*num_chained*) extras =
    1.29 +  let
    1.30 +    val (indirect_ss, direct_ss) =
    1.31 +      if is_proof_method_direct meth then
    1.32 +        ([], extras |> proof_method_distinguishes_chained_and_direct meth ? append used_chaineds)
    1.33 +      else
    1.34 +        (extras, [])
    1.35 +  in
    1.36      (if null indirect_ss then "" else "using " ^ space_implode " " indirect_ss ^ " ") ^
    1.37      apply_on_subgoal i n ^ string_of_proof_method ctxt direct_ss meth ^
    1.38      (if is_proof_method_multi_goal meth andalso n <> 1 then "[1]" else "")