--- a/src/HOL/Try0_HOL.thy Thu Mar 27 13:30:16 2025 +0100
+++ b/src/HOL/Try0_HOL.thy Thu Mar 27 13:40:33 2025 +0100
@@ -20,38 +20,6 @@
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")]
@@ -75,52 +43,11 @@
("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
+ |> List.app (fn (name, (run_if_auto_try, (all_goals, tags))) =>
+ let val meth : Try0.proof_method = Try0_Util.apply_raw_named_method name all_goals tags in
Try0.register_proof_method name {run_if_auto_try = run_if_auto_try} meth
handle Symtab.DUP _ => ()
end)