--- a/src/HOL/HOL.thy Thu Mar 27 11:20:59 2025 +0100
+++ b/src/HOL/HOL.thy Thu Mar 27 13:30:16 2025 +0100
@@ -5,7 +5,7 @@
section \<open>The basis of Higher-Order Logic\<close>
theory HOL
-imports Pure Tools.Code_Generator
+imports Pure Try0 Tools.Code_Generator
keywords
"try" "solve_direct" "quickcheck" "print_coercions" "print_claset"
"print_induct_rules" :: diag and
--- a/src/HOL/Sledgehammer.thy Thu Mar 27 11:20:59 2025 +0100
+++ b/src/HOL/Sledgehammer.thy Thu Mar 27 13:30:16 2025 +0100
@@ -7,7 +7,7 @@
section \<open>Sledgehammer: Isabelle--ATP Linkup\<close>
theory Sledgehammer
-imports Presburger SMT Try0
+imports Presburger SMT Try0_HOL
keywords
"sledgehammer" :: diag and
"sledgehammer_params" :: thy_decl
--- a/src/HOL/Tools/Nunchaku/nunchaku_commands.ML Thu Mar 27 11:20:59 2025 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_commands.ML Thu Mar 27 13:30:16 2025 +0100
@@ -246,7 +246,7 @@
fun run_chaku override_params mode i state0 =
let
- val state = Proof.map_contexts (Try0.silence_methods false) state0;
+ val state = Proof.map_contexts (Try0_Util.silence_methods false) state0;
val thy = Proof.theory_of state;
val ctxt = Proof.context_of state;
val _ = List.app check_raw_param override_params;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Mar 27 11:20:59 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Mar 27 13:30:16 2025 +0100
@@ -292,7 +292,7 @@
fun default_params thy = get_params Normal thy o map (apsnd single)
val silence_state =
- Proof.map_contexts (Try0.silence_methods false #> Config.put SMT_Config.verbose false)
+ Proof.map_contexts (Try0_Util.silence_methods false #> Config.put SMT_Config.verbose false)
(* Sledgehammer the given subgoal *)
--- a/src/HOL/Tools/try0.ML Thu Mar 27 11:20:59 2025 +0100
+++ b/src/HOL/Tools/try0.ML Thu Mar 27 13:30:16 2025 +0100
@@ -6,6 +6,8 @@
signature TRY0 =
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
@@ -16,14 +18,21 @@
val register_proof_method : string -> proof_method_options -> proof_method -> unit
val get_proof_method : string -> proof_method option
+ datatype mode = Auto_Try | Try | Normal
+ val generic_try0 : mode -> Time.time option -> tagged_xref list -> Proof.state ->
+ (bool * (string * string list)) * result list
val try0 : Time.time option -> tagged_xref list -> Proof.state -> result list
-
- val silence_methods : bool -> Proof.context -> Proof.context
end
structure Try0 : TRY0 =
struct
+fun serial_commas _ [] = ["??"]
+ | serial_commas _ [s] = [s]
+ | serial_commas conj [s1, s2] = [s1, conj, s2]
+ | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
+ | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss;
+
val noneN = "none"
datatype mode = Auto_Try | Try | Normal
@@ -112,7 +121,7 @@
in
if mode = Normal then
let val names = map quote proof_method_names in
- writeln ("Trying " ^ implode_space (Try.serial_commas "and" names) ^ "...")
+ writeln ("Trying " ^ implode_space (serial_commas "and" names) ^ "...")
end
else
();
@@ -161,20 +170,4 @@
Outer_Syntax.command \<^command_keyword>\<open>try0\<close> "try a combination of proof methods"
(Scan.optional parse_attrs [] #>> try0_trans)
-val _ =
- Try.tool_setup
- {name = "try0", weight = 30, auto_option = \<^system_option>\<open>auto_methods\<close>,
- body = fn auto => fst o generic_try0 (if auto then Auto_Try else Try) NONE []}
-
-(* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification
- bound exceeded" warnings and the like. *)
-fun silence_methods debug =
- Config.put Metis_Tactic.verbose debug
- #> not debug ? (fn ctxt =>
- ctxt
- |> Simplifier_Trace.disable
- |> Context_Position.set_visible false
- |> Config.put Unify.unify_trace false
- |> Config.put Argo_Tactic.trace "none")
-
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/try0_util.ML Thu Mar 27 13:30:16 2025 +0100
@@ -0,0 +1,35 @@
+(* Title: HOL/Tools/try0_hol.ML
+ Author: Jasmin Blanchette, LMU Muenchen
+ Author: Martin Desharnais, LMU Muenchen
+ Author: Fabian Huch, TU Muenchen
+
+General-purpose functions used by Try0.
+*)
+
+signature TRY0_UTIL =
+sig
+ val silence_methods : bool -> Proof.context -> Proof.context
+ val string_of_xref : Try0.xref -> string
+end
+
+structure Try0_Util : TRY0_UTIL = struct
+
+(* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification
+ bound exceeded" warnings and the like. *)
+fun silence_methods debug =
+ Config.put Metis_Tactic.verbose debug
+ #> not debug ? (fn ctxt =>
+ ctxt
+ |> Simplifier_Trace.disable
+ |> Context_Position.set_visible false
+ |> Config.put Unify.unify_trace false
+ |> Config.put Argo_Tactic.trace "none")
+
+fun string_of_xref ((xref, args) : Try0.xref) =
+ (case xref of
+ Facts.Fact literal => literal |> Symbol_Pos.explode0 |> Symbol_Pos.implode |> cartouche
+ | _ =>
+ Facts.string_of_ref xref) ^ implode
+ (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args)
+
+end
\ No newline at end of file
--- a/src/HOL/Try0.thy Thu Mar 27 11:20:59 2025 +0100
+++ b/src/HOL/Try0.thy Thu Mar 27 13:30:16 2025 +0100
@@ -5,127 +5,10 @@
*)
theory Try0
- imports Presburger
+ imports Pure
keywords "try0" :: diag
begin
ML_file \<open>Tools/try0.ML\<close>
-ML \<open>
-local
-
-fun string_of_xref ((xref, args) : Try0.xref) =
- (case xref of
- Facts.Fact literal => literal |> Symbol_Pos.explode0 |> Symbol_Pos.implode |> cartouche
- | _ =>
- Facts.string_of_ref xref) ^ implode
- (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args)
-
-fun add_attr_text (tagged : Try0.tagged_xref list) (tag, src) s =
- let
- val fs = tagged |> filter (fn (_, tags) => member (op =) tags tag) |> map (string_of_xref o fst)
- 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
- |> filter Token.is_proper
- |> Scan.read Token.stopper Method.parse
- |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source")
-
-fun run_tac timeout_opt tac st =
- let val with_timeout =
- (case timeout_opt of SOME timeout => Timeout.apply_physical timeout | NONE => I)
- in with_timeout (Seq.pull o tac) st |> Option.map fst end
-
-val num_goals = Thm.nprems_of o #goal o Proof.goal
-
-fun apply_recursive recurse elapsed0 timeout_opt apply st =
- (case Timing.timing (Option.join o try (run_tac timeout_opt apply)) st of
- ({elapsed, ...}, SOME st') =>
- if recurse andalso num_goals st' > 0 andalso num_goals st' < num_goals st then
- let val timeout_opt1 = (Option.map (fn timeout => timeout - elapsed) timeout_opt)
- in apply_recursive recurse (elapsed0 + elapsed) timeout_opt1 apply st' end
- else (elapsed0 + elapsed, st')
- |_ => (elapsed0, st))
-
-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 = []
-
-(* name * (run_if_auto_try * (all_goals * tags)) *)
-val raw_named_methods =
- [("simp", (true, (false, simp_attrs))),
- ("auto", (true, (true, full_attrs))),
- ("blast", (true, (false, clas_attrs))),
- ("metis", (true, (false, metis_attrs))),
- ("argo", (true, (false, no_attrs))),
- ("linarith", (true, (false, no_attrs))),
- ("presburger", (true, (false, no_attrs))),
- ("algebra", (true, (false, no_attrs))),
- ("fast", (false, (false, clas_attrs))),
- ("fastforce", (false, (false, full_attrs))),
- ("force", (false, (false, full_attrs))),
- ("meson", (false, (false, metis_attrs))),
- ("satx", (false, (false, no_attrs))),
- ("order", (true, (false, no_attrs)))]
-
-fun apply_raw_named_method name (all_goals, attrs) timeout_opt tagged st :
- Try0.result option =
- let
- val st = Proof.map_contexts (Try0.silence_methods false) 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 text =
- name ^ attrs
- |> parse_method ctxt
- |> Method.method_cmd ctxt
- |> Method.Basic
- |> (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
- 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
- val num_after = num_goals st'
- val select = "[" ^ string_of_int (num_before - num_after) ^ "]"
- val unused = implode_space (unused |> map string_of_xref)
- val command =
- (if unused <> "" then "using " ^ unused ^ " " else "") ^
- (if num_after = 0 then "by " else "apply ") ^
- (name ^ attrs |> attrs <> "" ? enclose "(" ")") ^
- (if multiple_goals andalso num_after > 0 then select else "")
- in
- if num_before > num_after then
- SOME {name = name, command = command, time = time, state = st'}
- else NONE
- end
-
-in
-
-val () = raw_named_methods
- |> List.app (fn (name, (run_if_auto_try, raw_method)) =>
- let val meth : Try0.proof_method = apply_raw_named_method name raw_method in
- Try0.register_proof_method name {run_if_auto_try = run_if_auto_try} meth
- handle Symtab.DUP _ => ()
- end)
-
-end
-\<close>
-
end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Try0_HOL.thy Thu Mar 27 13:30:16 2025 +0100
@@ -0,0 +1,131 @@
+(* Title: HOL/Try0_HOL.thy
+ Author: Jasmin Blanchette, LMU Muenchen
+ Author: Martin Desharnais, LMU Muenchen
+ Author: Fabian Huch, TU Muenchen
+*)
+theory Try0_HOL
+ imports Try0 Presburger
+begin
+
+
+ML_file \<open>Tools/try0_util.ML\<close>
+
+ML \<open>
+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 []}
+\<close>
+
+ML \<open>
+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 (Try0_Util.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
+ |> filter Token.is_proper
+ |> Scan.read Token.stopper Method.parse
+ |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source")
+
+fun run_tac timeout_opt tac st =
+ let val with_timeout =
+ (case timeout_opt of SOME timeout => Timeout.apply_physical timeout | NONE => I)
+ in with_timeout (Seq.pull o tac) st |> Option.map fst end
+
+val num_goals = Thm.nprems_of o #goal o Proof.goal
+
+fun apply_recursive recurse elapsed0 timeout_opt apply st =
+ (case Timing.timing (Option.join o try (run_tac timeout_opt apply)) st of
+ ({elapsed, ...}, SOME st') =>
+ if recurse andalso num_goals st' > 0 andalso num_goals st' < num_goals st then
+ let val timeout_opt1 = (Option.map (fn timeout => timeout - elapsed) timeout_opt)
+ in apply_recursive recurse (elapsed0 + elapsed) timeout_opt1 apply st' end
+ else (elapsed0 + elapsed, st')
+ |_ => (elapsed0, st))
+
+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 = []
+
+(* name * (run_if_auto_try * (all_goals * tags)) *)
+val raw_named_methods =
+ [("simp", (true, (false, simp_attrs))),
+ ("auto", (true, (true, full_attrs))),
+ ("blast", (true, (false, clas_attrs))),
+ ("metis", (true, (false, metis_attrs))),
+ ("argo", (true, (false, no_attrs))),
+ ("linarith", (true, (false, no_attrs))),
+ ("presburger", (true, (false, no_attrs))),
+ ("algebra", (true, (false, no_attrs))),
+ ("fast", (false, (false, clas_attrs))),
+ ("fastforce", (false, (false, full_attrs))),
+ ("force", (false, (false, full_attrs))),
+ ("meson", (false, (false, metis_attrs))),
+ ("satx", (false, (false, no_attrs))),
+ ("order", (true, (false, no_attrs)))]
+
+fun apply_raw_named_method name (all_goals, attrs) timeout_opt tagged st :
+ Try0.result option =
+ let
+ val st = Proof.map_contexts (Try0_Util.silence_methods false) 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 text =
+ name ^ attrs
+ |> parse_method ctxt
+ |> Method.method_cmd ctxt
+ |> Method.Basic
+ |> (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
+ 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
+ val num_after = num_goals st'
+ val select = "[" ^ string_of_int (num_before - num_after) ^ "]"
+ val unused = implode_space (unused |> map Try0_Util.string_of_xref)
+ val command =
+ (if unused <> "" then "using " ^ unused ^ " " else "") ^
+ (if num_after = 0 then "by " else "apply ") ^
+ (name ^ attrs |> attrs <> "" ? enclose "(" ")") ^
+ (if multiple_goals andalso num_after > 0 then select else "")
+ in
+ if num_before > num_after then
+ SOME {name = name, command = command, time = time, state = st'}
+ else NONE
+ end
+
+in
+
+val () = raw_named_methods
+ |> List.app (fn (name, (run_if_auto_try, raw_method)) =>
+ let val meth : Try0.proof_method = apply_raw_named_method name raw_method in
+ Try0.register_proof_method name {run_if_auto_try = run_if_auto_try} meth
+ handle Symtab.DUP _ => ()
+ end)
+
+end
+\<close>
+
+end
\ No newline at end of file
--- a/src/Tools/try.ML Thu Mar 27 11:20:59 2025 +0100
+++ b/src/Tools/try.ML Thu Mar 27 13:30:16 2025 +0100
@@ -20,11 +20,7 @@
(* helpers *)
-fun serial_commas _ [] = ["??"]
- | serial_commas _ [s] = [s]
- | serial_commas conj [s1, s2] = [s1, conj, s2]
- | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
- | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss;
+val serial_commas = Try0.serial_commas
(* configuration *)