--- a/src/FOL/ex/Prolog.thy Tue Jul 01 20:51:26 2025 +0200
+++ b/src/FOL/ex/Prolog.thy Thu Jul 03 15:28:31 2025 +0200
@@ -64,7 +64,7 @@
(*backtracking version*)
ML \<open>
fun prolog_tac ctxt =
- DEPTH_FIRST (has_fewer_prems 1) (resolve_tac ctxt @{thms rules} 1)
+ DEPTH_FIRST Thm.no_prems (resolve_tac ctxt @{thms rules} 1)
\<close>
schematic_goal \<open>rev(?x, a:b:c:Nil)\<close>
--- a/src/FOL/intprover.ML Tue Jul 01 20:51:26 2025 +0200
+++ b/src/FOL/intprover.ML Thu Jul 03 15:28:31 2025 +0200
@@ -90,11 +90,11 @@
(*Slower but smarter than fast_tac*)
fun best_tac ctxt =
- SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1));
+ SELECT_GOAL (BEST_FIRST (Thm.no_prems, size_of_thm) (step_tac ctxt 1));
(*Uses all_dupE: allows multiple use of universal assumptions. VERY slow.*)
fun best_dup_tac ctxt =
- SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_dup_tac ctxt 1));
+ SELECT_GOAL (BEST_FIRST (Thm.no_prems, size_of_thm) (step_dup_tac ctxt 1));
end;
--- a/src/FOLP/classical.ML Tue Jul 01 20:51:26 2025 +0200
+++ b/src/FOLP/classical.ML Thu Jul 03 15:28:31 2025 +0200
@@ -174,7 +174,7 @@
(*Slower but smarter than fast_tac*)
fun best_tac ctxt cs =
- SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac ctxt cs 1));
+ SELECT_GOAL (BEST_FIRST (Thm.no_prems, sizef) (step_tac ctxt cs 1));
(*Using a "safe" rule to instantiate variables is unsafe. This tactic
allows backtracking from "safe" rules to "unsafe" rules here.*)
--- a/src/FOLP/intprover.ML Tue Jul 01 20:51:26 2025 +0200
+++ b/src/FOLP/intprover.ML Thu Jul 03 15:28:31 2025 +0200
@@ -72,6 +72,6 @@
(*Slower but smarter than fast_tac*)
fun best_tac ctxt =
- SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1));
+ SELECT_GOAL (BEST_FIRST (Thm.no_prems, size_of_thm) (step_tac ctxt 1));
end;
--- a/src/HOL/Nominal/nominal_datatype.ML Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Thu Jul 03 15:28:31 2025 +0200
@@ -588,7 +588,7 @@
(fn ctxt =>
resolve_tac ctxt [exI] 1 THEN
resolve_tac ctxt @{thms CollectI} 1 THEN
- QUIET_BREADTH_FIRST (has_fewer_prems 1)
+ QUIET_BREADTH_FIRST Thm.no_prems
(resolve_tac ctxt rep_intrs 1))) thy |> (fn ((_, r), thy) =>
let
val permT = mk_permT
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Thu Jul 03 15:28:31 2025 +0200
@@ -603,7 +603,7 @@
val pulled_tac_result = Seq.pull tac_result
val tac_failed =
is_none pulled_tac_result orelse
- not (has_fewer_prems 1 (fst (the pulled_tac_result)))
+ not (Thm.no_prems (fst (the pulled_tac_result)))
in
if tac_failed then (wittler THEN' ASAP wittler tac) i st
else tac_result
--- a/src/HOL/Tools/Meson/meson.ML Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Thu Jul 03 15:28:31 2025 +0200
@@ -685,10 +685,10 @@
discrimination as to their size! With BEST_FIRST, fails for problem 41.*)
fun best_prolog_tac ctxt sizef horns =
- BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac ctxt horns 1);
+ BEST_FIRST (Thm.no_prems, sizef) (prolog_step_tac ctxt horns 1);
fun depth_prolog_tac ctxt horns =
- DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac ctxt horns 1);
+ DEPTH_FIRST Thm.no_prems (prolog_step_tac ctxt horns 1);
(*Return all negative clauses, as possible goal clauses*)
fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
@@ -717,7 +717,7 @@
MESON all_tac (make_clauses ctxt)
(fn cls =>
THEN_BEST_FIRST (resolve_tac ctxt (gocls cls) 1)
- (has_fewer_prems 1, sizef)
+ (Thm.no_prems, sizef)
(prolog_step_tac ctxt (make_horns cls) 1))
ctxt
@@ -746,7 +746,7 @@
end;
fun iter_deepen_prolog_tac ctxt horns =
- ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' ctxt horns);
+ ITER_DEEPEN iter_deepen_limit Thm.no_prems (prolog_step_tac' ctxt horns);
fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON all_tac (make_clauses ctxt)
(fn cls =>
@@ -761,7 +761,7 @@
["clauses:"] @ map (Thm.string_of_thm ctxt) horns))
in
THEN_ITER_DEEPEN iter_deepen_limit
- (resolve_tac ctxt goes 1) (has_fewer_prems 1) (prolog_step_tac' ctxt horns)
+ (resolve_tac ctxt goes 1) Thm.no_prems (prolog_step_tac' ctxt horns)
end));
fun meson_tac ctxt ths =
--- a/src/Provers/classical.ML Tue Jul 01 20:51:26 2025 +0200
+++ b/src/Provers/classical.ML Thu Jul 03 15:28:31 2025 +0200
@@ -287,7 +287,7 @@
fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Thm.string_of_thm ctxt th);
fun make_elim ctxt th =
- if has_fewer_prems 1 th then bad_thm ctxt "Ill-formed destruction rule" th
+ if Thm.no_prems th then bad_thm ctxt "Ill-formed destruction rule" th
else Tactic.make_elim th;
fun warn_thm ctxt msg th =
@@ -423,7 +423,7 @@
fun addSE w ctxt th (cs as CS {safeEs, ...}) =
let
- val _ = has_fewer_prems 1 th andalso bad_thm ctxt "Ill-formed elimination rule" th;
+ val _ = Thm.no_prems th andalso bad_thm ctxt "Ill-formed elimination rule" th;
val th' = classical_rule ctxt (flat_rule ctxt th);
val rl = (th', []);
val r = trim_context (th, rl, rl);
@@ -446,7 +446,7 @@
fun addE w ctxt th (cs as CS {unsafeEs, ...}) =
let
- val _ = has_fewer_prems 1 th andalso bad_thm ctxt "Ill-formed elimination rule" th;
+ val _ = Thm.no_prems th andalso bad_thm ctxt "Ill-formed elimination rule" th;
val th' = classical_rule ctxt (flat_rule ctxt th);
val dup_th' = dup_elim ctxt th' handle THM _ => bad_thm ctxt "Ill-formed elimination rule" th;
val r = trim_context (th, (th', []), (dup_th', []));
@@ -804,12 +804,12 @@
(*Slower but smarter than fast_tac*)
fun best_tac ctxt =
Object_Logic.atomize_prems_tac ctxt THEN'
- SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac ctxt 1));
+ SELECT_GOAL (BEST_FIRST (Thm.no_prems, Data.sizef) (step_tac ctxt 1));
(*even a bit smarter than best_tac*)
fun first_best_tac ctxt =
Object_Logic.atomize_prems_tac ctxt THEN'
- SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac ctxt)));
+ SELECT_GOAL (BEST_FIRST (Thm.no_prems, Data.sizef) (FIRSTGOAL (step_tac ctxt)));
fun slow_tac ctxt =
Object_Logic.atomize_prems_tac ctxt THEN'
@@ -817,7 +817,7 @@
fun slow_best_tac ctxt =
Object_Logic.atomize_prems_tac ctxt THEN'
- SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac ctxt 1));
+ SELECT_GOAL (BEST_FIRST (Thm.no_prems, Data.sizef) (slow_step_tac ctxt 1));
(***ASTAR with weight weight_ASTAR, by Norbert Voelker*)
@@ -827,13 +827,13 @@
fun astar_tac ctxt =
Object_Logic.atomize_prems_tac ctxt THEN'
SELECT_GOAL
- (ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev)
+ (ASTAR (Thm.no_prems, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev)
(step_tac ctxt 1));
fun slow_astar_tac ctxt =
Object_Logic.atomize_prems_tac ctxt THEN'
SELECT_GOAL
- (ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev)
+ (ASTAR (Thm.no_prems, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev)
(slow_step_tac ctxt 1));
--- a/src/Pure/search.ML Tue Jul 01 20:51:26 2025 +0200
+++ b/src/Pure/search.ML Thu Jul 03 15:28:31 2025 +0200
@@ -52,10 +52,10 @@
fun has_fewer_prems n rule = Thm.nprems_of rule < n;
(*Apply a tactic if subgoals remain, else do nothing.*)
-val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac;
+val IF_UNSOLVED = COND Thm.no_prems all_tac;
(*Force a tactic to solve its goal completely, otherwise fail *)
-fun SOLVE tac = tac THEN COND (has_fewer_prems 1) all_tac no_tac;
+fun SOLVE tac = tac THEN COND Thm.no_prems all_tac no_tac;
(*Execute tac1, but only execute tac2 if there are at least as many subgoals
as before. This ensures that tac2 is only applied to an outcome of tac1.*)
@@ -72,7 +72,7 @@
| n => DEPTH_FIRST (has_fewer_prems n) tac);
(*Uses depth-first search to solve ALL subgoals*)
-val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1);
+val DEPTH_SOLVE = DEPTH_FIRST Thm.no_prems;
--- a/src/Sequents/modal.ML Tue Jul 01 20:51:26 2025 +0200
+++ b/src/Sequents/modal.ML Thu Jul 03 15:28:31 2025 +0200
@@ -83,7 +83,7 @@
rewrite_goals_tac ctxt Modal_Rule.rewrite_rls THEN solven_tac ctxt d 1;
fun step_tac ctxt n =
- COND (has_fewer_prems 1) all_tac
+ COND Thm.no_prems all_tac
(DETERM(fres_safe_tac ctxt n) ORELSE
(fres_unsafe_tac ctxt n APPEND fres_bound_tac ctxt n));
--- a/src/Sequents/prover.ML Tue Jul 01 20:51:26 2025 +0200
+++ b/src/Sequents/prover.ML Thu Jul 03 15:28:31 2025 +0200
@@ -223,7 +223,7 @@
SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
fun best_tac ctxt =
- SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1));
+ SELECT_GOAL (BEST_FIRST (Thm.no_prems, size_of_thm) (step_tac ctxt 1));
val _ = Theory.setup
(Method.setup \<^binding>\<open>safe\<close> (method safe_tac) "" #>