improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
authorblanchet
Sun May 03 22:15:29 2015 +0200 (2015-05-03)
changeset 602522c468c062589
parent 60251 98754695b421
child 60253 478795f6e78a
improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun May 03 18:14:11 2015 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun May 03 22:15:29 2015 +0200
     1.3 @@ -55,6 +55,8 @@
     1.4     del : (Facts.ref * Token.src list) list,
     1.5     only : bool}
     1.6  
     1.7 +val local_thisN = Long_Name.localN ^ Long_Name.separator ^ Auto_Bind.thisN
     1.8 +
     1.9  (* gracefully handle huge background theories *)
    1.10  val max_facts_for_duplicates = 50000
    1.11  val max_facts_for_complex_check = 25000
    1.12 @@ -499,7 +501,7 @@
    1.13                 else
    1.14                   let
    1.15                     fun get_name () =
    1.16 -                     if name0 = "" then
    1.17 +                     if name0 = "" orelse name0 = local_thisN then
    1.18                         backquote_thm ctxt th
    1.19                       else
    1.20                         let val short_name = Facts.extern ctxt facts name0 in
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sun May 03 18:14:11 2015 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sun May 03 22:15:29 2015 +0200
     2.3 @@ -34,6 +34,7 @@
     2.4      ((string * stature) list * (proof_method * play_outcome)) * string * int * int
     2.5  
     2.6    val is_proof_method_direct : proof_method -> bool
     2.7 +  val proof_method_distinguishes_chained_and_direct : proof_method -> bool
     2.8    val string_of_proof_method : Proof.context -> string list -> proof_method -> string
     2.9    val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
    2.10    val thms_influence_proof_method : Proof.context -> proof_method -> thm list -> bool
    2.11 @@ -80,6 +81,10 @@
    2.12    | is_proof_method_direct Simp_Size_Method = true
    2.13    | is_proof_method_direct _ = false
    2.14  
    2.15 +fun proof_method_distinguishes_chained_and_direct Simp_Method = true
    2.16 +  | proof_method_distinguishes_chained_and_direct Simp_Size_Method = true
    2.17 +  | proof_method_distinguishes_chained_and_direct _ = false
    2.18 +
    2.19  fun is_proof_method_multi_goal Auto_Method = true
    2.20    | is_proof_method_multi_goal _ = false
    2.21  
    2.22 @@ -163,8 +168,14 @@
    2.23    | apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
    2.24  
    2.25  (* FIXME *)
    2.26 -fun proof_method_command ctxt meth i n _(*used_chaineds*) _(*num_chained*) ss =
    2.27 -  let val (indirect_ss, direct_ss) = if is_proof_method_direct meth then ([], ss) else (ss, []) in
    2.28 +fun proof_method_command ctxt meth i n used_chaineds _(*num_chained*) extras =
    2.29 +  let
    2.30 +    val (indirect_ss, direct_ss) =
    2.31 +      if is_proof_method_direct meth then
    2.32 +        ([], extras |> proof_method_distinguishes_chained_and_direct meth ? append used_chaineds)
    2.33 +      else
    2.34 +        (extras, [])
    2.35 +  in
    2.36      (if null indirect_ss then "" else "using " ^ space_implode " " indirect_ss ^ " ") ^
    2.37      apply_on_subgoal i n ^ string_of_proof_method ctxt direct_ss meth ^
    2.38      (if is_proof_method_multi_goal meth andalso n <> 1 then "[1]" else "")