--- a/src/HOL/HOL.thy Thu Mar 27 14:33:08 2025 +0100
+++ b/src/HOL/HOL.thy Thu Mar 27 16:35:41 2025 +0100
@@ -38,7 +38,7 @@
val _ =
Try.tool_setup
{name = "try0", weight = 30, auto_option = \<^system_option>\<open>auto_methods\<close>,
- body = fn auto => fst o Try0.generic_try0 (if auto then Try0.Auto_Try else Try0.Try) NONE []}
+ body = fn auto => fst o Try0.generic_try0 (if auto then Try0.Auto_Try else Try0.Try) NONE Try0.empty_facts}
\<close>
ML \<open>Plugin_Name.declare_setup \<^binding>\<open>extraction\<close>\<close>
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Thu Mar 27 14:33:08 2025 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Thu Mar 27 16:35:41 2025 +0100
@@ -148,7 +148,7 @@
let
val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy)
in
- case Try0.try0 (SOME (seconds 5.0)) [] state of
+ case Try0.try0 (SOME (seconds 5.0)) Try0.empty_facts state of
[] => (Unsolved, [])
| _ => (Solved, [])
end
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Thu Mar 27 14:33:08 2025 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Thu Mar 27 16:35:41 2025 +0100
@@ -216,7 +216,7 @@
end
-val try0 = not o null o Try0.try0 (SOME (Time.fromSeconds 5)) []
+val try0 = not o null o Try0.try0 (SOME (Time.fromSeconds 5)) Try0.empty_facts
fun make_action ({arguments, timeout, output_dir, ...} : Mirabelle.action_context) =
let
--- a/src/HOL/Tools/Mirabelle/mirabelle_try0.ML Thu Mar 27 14:33:08 2025 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_try0.ML Thu Mar 27 16:35:41 2025 +0100
@@ -12,9 +12,10 @@
fun make_action ({timeout, ...} : Mirabelle.action_context) =
let
val generous_timeout = Time.scale 10.0 timeout
+ val try0 = Try0.try0 (SOME timeout) Try0.empty_facts
fun run ({pre, ...} : Mirabelle.command) =
- if Timeout.apply generous_timeout (not o null o Try0.try0 (SOME timeout) []) pre then
+ if Timeout.apply generous_timeout (not o null o try0) pre then
"succeeded"
else
""
--- a/src/HOL/Tools/try0.ML Thu Mar 27 14:33:08 2025 +0100
+++ b/src/HOL/Tools/try0.ML Thu Mar 27 16:35:41 2025 +0100
@@ -1,5 +1,7 @@
-(* Title: HOL/Tools/try0.ML
- Author: Jasmin Blanchette, TU Muenchen
+(* Title: HOL/Tools/try0.ML
+ Author: Jasmin Blanchette, LMU Muenchen
+ Author: Martin Desharnais, LMU Muenchen
+ Author: Fabian Huch, TU Muenchen
Try a combination of proof methods.
*)
@@ -8,11 +10,18 @@
sig
val serial_commas : string -> string list -> string list
- datatype modifier = Use | Simp | Intro | Elim | Dest
type xref = Facts.ref * Token.src list
- type tagged_xref = xref * modifier list
+
+ type facts =
+ {usings: xref list,
+ simps : xref list,
+ intros : xref list,
+ elims : xref list,
+ dests : xref list}
+ val empty_facts : facts
+
type result = {name: string, command: string, time: Time.time, state: Proof.state}
- type proof_method = Time.time option -> tagged_xref list -> Proof.state -> result option
+ type proof_method = Time.time option -> facts -> Proof.state -> result option
type proof_method_options = {run_if_auto_try: bool}
val register_proof_method : string -> proof_method_options -> proof_method -> unit
@@ -20,9 +29,9 @@
val get_all_proof_method_names : unit -> string list
datatype mode = Auto_Try | Try | Normal
- val generic_try0 : mode -> Time.time option -> tagged_xref list -> Proof.state ->
+ val generic_try0 : mode -> Time.time option -> facts -> Proof.state ->
(bool * (string * string list)) * result list
- val try0 : Time.time option -> tagged_xref list -> Proof.state -> result list
+ val try0 : Time.time option -> facts -> Proof.state -> result list
end
structure Try0 : TRY0 =
@@ -43,9 +52,23 @@
datatype modifier = Use | Simp | Intro | Elim | Dest
type xref = Facts.ref * Token.src list
type tagged_xref = xref * modifier list
+type facts =
+ {usings: xref list,
+ simps : xref list,
+ intros : xref list,
+ elims : xref list,
+ dests : xref list}
+
+val empty_facts: facts = {usings = [], simps = [], intros = [], elims = [], dests = []}
+fun union_facts (left : facts) (right : facts) : facts =
+ {usings = #usings left @ #usings right,
+ simps = #simps left @ #simps right,
+ intros = #intros left @ #intros right,
+ elims = #elims left @ #elims right,
+ dests = #dests left @ #dests right}
type result = {name: string, command: string, time: Time.time, state: Proof.state}
-type proof_method = Time.time option -> tagged_xref list -> Proof.state -> result option
+type proof_method = Time.time option -> facts -> Proof.state -> result option
type proof_method_options = {run_if_auto_try: bool}
val noop_proof_method : proof_method = fn _ => fn _ => fn _ => NONE
@@ -60,7 +83,7 @@
fun register_proof_method name ({run_if_auto_try} : proof_method_options) proof_method =
let
val () = if name = "" then error "Registering unnamed proof method" else ()
- val () = Synchronized.change proof_methods (Symtab.update_new (name, proof_method))
+ val () = Synchronized.change proof_methods (Symtab.update (name, proof_method))
val () =
if run_if_auto_try then
Synchronized.change auto_try_proof_methods_names (Symset.insert name)
@@ -99,9 +122,9 @@
fun time_string time = string_of_int (Time.toMilliseconds time) ^ " ms"
fun tool_time_string (s, time) = s ^ ": " ^ time_string time
-fun generic_try0 mode timeout_opt (tagged : tagged_xref list) st =
+fun generic_try0 mode timeout_opt (facts : facts) st =
let
- fun try_method method = method mode timeout_opt tagged st
+ fun try_method (method : mode -> proof_method) = method mode timeout_opt facts st
fun get_message {command, time, ...} = "Found proof: " ^ Active.sendback_markup_command
command ^ " (" ^ time_string time ^ ")"
val print_step = Option.map (tap (writeln o get_message))
@@ -149,24 +172,28 @@
fun try0 timeout_opt = snd oo generic_try0 Normal timeout_opt
-fun try0_trans tagged =
+fun try0_trans (facts : facts) =
Toplevel.keep_proof
- (ignore o generic_try0 Normal (SOME default_timeout) tagged o Toplevel.proof_of)
+ (ignore o generic_try0 Normal (SOME default_timeout) facts o Toplevel.proof_of)
val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.thm)
val parse_attr =
- Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs >> (map (rpair [Simp]))
- || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs >> (map (rpair [Intro]))
- || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs >> (map (rpair [Elim]))
- || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs >> (map (rpair [Dest]))
+ Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs >> (fn xrefs =>
+ {usings = [], simps = xrefs, intros = [], elims = [], dests = []})
+ || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs >> (fn xrefs =>
+ {usings = [], simps = [], intros = xrefs, elims = [], dests = []})
+ || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs >> (fn xrefs =>
+ {usings = [], simps = [], intros = [], elims = xrefs, dests = []})
+ || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs >> (fn xrefs =>
+ {usings = [], simps = [], intros = [], elims = [], dests = xrefs})
fun parse_attrs x =
(Args.parens parse_attrs
- || Scan.repeat parse_attr >> (fn tagged => fold (curry (op @)) tagged [])) x
+ || Scan.repeat parse_attr >> (fn factss => fold union_facts factss empty_facts)) x
val _ =
Outer_Syntax.command \<^command_keyword>\<open>try0\<close> "try a combination of proof methods"
- (Scan.optional parse_attrs [] #>> try0_trans)
+ (Scan.optional parse_attrs empty_facts #>> try0_trans)
end
--- a/src/HOL/Tools/try0_util.ML Thu Mar 27 14:33:08 2025 +0100
+++ b/src/HOL/Tools/try0_util.ML Thu Mar 27 16:35:41 2025 +0100
@@ -9,13 +9,20 @@
signature TRY0_UTIL =
sig
val string_of_xref : Try0.xref -> string
- val full_attrs : (Try0.modifier * string) list
- val clas_attrs : (Try0.modifier * string) list
- val simp_attrs : (Try0.modifier * string) list
- val metis_attrs : (Try0.modifier * string) list
- val no_attrs : (Try0.modifier * string) list
- val apply_raw_named_method : string -> bool -> (Try0.modifier * string) list ->
- (Proof.context -> Proof.context) -> Time.time option -> Try0.tagged_xref list -> Proof.state ->
+
+ type facts_prefixes =
+ {usings: string,
+ simps : string,
+ intros : string,
+ elims : string,
+ dests : string}
+ val full_attrs : facts_prefixes
+ val clas_attrs : facts_prefixes
+ val simp_attrs : facts_prefixes
+ val metis_attrs : facts_prefixes
+ val no_attrs : facts_prefixes
+ val apply_raw_named_method : string -> bool -> facts_prefixes ->
+ (Proof.context -> Proof.context) -> Time.time option -> Try0.facts -> Proof.state ->
Try0.result option
end
@@ -29,27 +36,25 @@
(map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args)
-val full_attrs = [(Try0.Simp, "simp"), (Try0.Intro, "intro"), (Try0.Elim, "elim"), (Try0.Dest, "dest")]
-val clas_attrs = [(Try0.Intro, "intro"), (Try0.Elim, "elim"), (Try0.Dest, "dest")]
-val simp_attrs = [(Try0.Simp, "add")]
-val metis_attrs = [(Try0.Simp, ""), (Try0.Intro, ""), (Try0.Elim, ""), (Try0.Dest, "")]
-val no_attrs = []
+type facts_prefixes =
+ {usings: string,
+ simps : string,
+ intros : string,
+ elims : string,
+ dests : string}
+
+val no_attrs : facts_prefixes =
+ {usings = "", simps = "", intros = "", elims = "", dests = ""}
+val full_attrs : facts_prefixes =
+ {usings = "", simps = "simp", intros = "intro", elims = "elim", dests = "dest"}
+val clas_attrs : facts_prefixes =
+ {usings = "", simps = "", intros = "intro", elims = "elim", dests = "dest"}
+val simp_attrs : facts_prefixes =
+ {usings = "", simps = "add", intros = "", elims = "", dests = ""}
+val metis_attrs : facts_prefixes = no_attrs
local
-fun add_attr_text (tagged : Try0.tagged_xref list) (tag, src) s =
- let
- val fs = tagged
- |> map_filter (fn (xref, tags) =>
- if member (op =) tags tag then
- SOME (string_of_xref xref)
- else
- NONE)
- in if null fs then s else s ^ " " ^ (if src = "" then "" else src ^ ": ") ^ implode_space fs end
-
-fun attrs_text tags (tagged : Try0.tagged_xref list) =
- "" |> fold (add_attr_text tagged) tags
-
fun parse_method ctxt s =
enclose "(" ")" s
|> Token.explode (Thy_Header.get_keywords' ctxt) Position.start
@@ -75,21 +80,40 @@
in
-fun apply_raw_named_method (name : string) all_goals attrs
- (silence_methods : Proof.context -> Proof.context) timeout_opt (tagged : Try0.tagged_xref list)
+fun apply_raw_named_method (name : string) all_goals (prefixes: facts_prefixes)
+ (silence_methods : Proof.context -> Proof.context) timeout_opt (facts : Try0.facts)
(st : Proof.state) : Try0.result option =
let
val st = Proof.map_contexts silence_methods st
- val unused =
- tagged
- |> filter
- (fn (_, tags) => not (null tags) andalso null (inter (op =) tags (attrs |> map fst)))
- |> map fst
-
- val attrs = attrs_text attrs tagged
-
val ctxt = Proof.context_of st
+ val (unused_simps, simps_attrs) =
+ if #simps prefixes = "" then
+ (#simps facts, "")
+ else
+ ([], " " ^ #simps prefixes ^ ": " ^ space_implode "" (map string_of_xref (#simps facts)))
+
+ val (unused_intros, intros_attrs) =
+ if #intros prefixes = "" then
+ (#intros facts, "")
+ else
+ ([], " " ^ #intros prefixes ^ ": " ^ space_implode "" (map string_of_xref (#intros facts)))
+
+ val (unused_elims, elims_attrs) =
+ if #elims prefixes = "" then
+ (#elims facts, "")
+ else
+ ([], " " ^ #elims prefixes ^ ": " ^ space_implode "" (map string_of_xref (#elims facts)))
+
+ val (unused_dests, dests_attrs) =
+ if #dests prefixes = "" then
+ (#dests facts, "")
+ else
+ ([], " " ^ #dests prefixes ^ ": " ^ space_implode "" (map string_of_xref (#dests facts)))
+
+ val unused = #usings facts @ unused_simps @ unused_intros @ unused_elims @ unused_dests
+
+ val attrs = simps_attrs ^ intros_attrs ^ elims_attrs ^ dests_attrs
val text =
name ^ attrs
|> parse_method ctxt
@@ -98,8 +122,8 @@
|> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m]))
val apply =
- Proof.using [Attrib.eval_thms ctxt unused |> map (rpair [] o single)]
- #> Proof.refine text #> Seq.filter_results
+ Proof.using [Attrib.eval_thms ctxt unused |> map (rpair [] o single)]
+ #> Proof.refine text #> Seq.filter_results
val num_before = num_goals st
val multiple_goals = all_goals andalso num_before > 1
val (time, st') = apply_recursive multiple_goals Time.zeroTime timeout_opt apply st