# HG changeset patch
# User wenzelm
# Date 1737577905 -3600
# Node ID 4652c6b36ee8e3a604fd046371a7ff48c65a137d
# Parent  1c482e216d84f842765621f6d86bfac97dc532f3
tuned signature: more explicit operations;

diff -r 1c482e216d84 -r 4652c6b36ee8 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Wed Jan 22 19:34:04 2025 +0100
+++ b/src/Pure/logic.ML	Wed Jan 22 21:31:45 2025 +0100
@@ -23,6 +23,7 @@
   val list_implies: term list * term -> term
   val strip_imp_prems: term -> term list
   val strip_imp_concl: term -> term
+  val take_imp_prems: int -> term -> term list
   val strip_prems: int * term list * term -> term list * term
   val count_prems: term -> int
   val no_prems: term -> bool
@@ -200,6 +201,11 @@
 fun strip_imp_concl (Const("Pure.imp", _) $ A $ B) = strip_imp_concl B
   | strip_imp_concl A = A : term;
 
+(* take at most n prems, where n < 0 means infinity *)
+fun take_imp_prems 0 _ = []
+  | take_imp_prems n (Const ("Pure.imp", _) $ A $ B) = A :: take_imp_prems (n - 1) B
+  | take_imp_prems _ _ = [];
+
 (*Strip and return premises: (i, [], A1\<Longrightarrow>...Ai\<Longrightarrow>B)
     goes to   ([Ai, A(i-1),...,A1] , B)         (REVERSED)
   if  i<0 or else i too big then raises  TERM*)
diff -r 1c482e216d84 -r 4652c6b36ee8 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Jan 22 19:34:04 2025 +0100
+++ b/src/Pure/thm.ML	Wed Jan 22 21:31:45 2025 +0100
@@ -76,13 +76,16 @@
   val tpairs_of: thm -> (term * term) list
   val concl_of: thm -> term
   val prems_of: thm -> term list
+  val take_prems_of: int -> thm -> term list
   val nprems_of: thm -> int
   val no_prems: thm -> bool
+  val prem_of: thm -> int -> term
   val major_prem_of: thm -> term
   val cprop_of: thm -> cterm
   val cprem_of: thm -> int -> cterm
   val cconcl_of: thm -> cterm
   val cprems_of: thm -> cterm list
+  val take_cprems_of: int -> thm -> cterm list
   val chyps_of: thm -> cterm list
   val thm_ord: thm ord
   exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option
@@ -519,11 +522,15 @@
 
 val concl_of = Logic.strip_imp_concl o prop_of;
 val prems_of = Logic.strip_imp_prems o prop_of;
+fun take_prems_of n = Logic.take_imp_prems n o prop_of;
 val nprems_of = Logic.count_prems o prop_of;
 val no_prems = Logic.no_prems o prop_of;
 
+fun prem_of th i =
+  Logic.nth_prem (i, prop_of th) handle TERM _ => raise THM ("prem_of", i, [th]);
+
 fun major_prem_of th =
-  (case prems_of th of
+  (case take_prems_of 1 th of
     prem :: _ => Logic.strip_assums_concl prem
   | [] => raise THM ("major_prem_of: rule with no premises", 0, [th]));
 
@@ -541,6 +548,10 @@
   map (fn t => Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = t})
     (prems_of th);
 
+fun take_cprems_of n (th as Thm (_, {cert, maxidx, shyps, ...})) =
+  map (fn t => Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = t})
+    (take_prems_of n th);
+
 fun chyps_of (Thm (_, {cert, shyps, hyps, ...})) =
   map (fn t => Cterm {cert = cert, maxidx = ~1, T = propT, sorts = shyps, t = t}) hyps;