--- a/src/Pure/logic.ML Tue May 31 11:53:20 2005 +0200
+++ b/src/Pure/logic.ML Tue May 31 11:53:21 2005 +0200
@@ -22,6 +22,7 @@
val strip_imp_concl : term -> term
val strip_prems : int * term list * term -> term list * term
val count_prems : term * int -> int
+ val nth_prem : int * term -> term
val mk_conjunction : term * term -> term
val mk_conjunction_list: term list -> term
val strip_horn : term -> term list * term
@@ -112,10 +113,15 @@
strip_prems (i-1, A::As, B)
| strip_prems (_, As, A) = raise TERM("strip_prems", A::As);
-(*Count premises -- quicker than (length ostrip_prems) *)
+(*Count premises -- quicker than (length o strip_prems) *)
fun count_prems (Const("==>", _) $ A $ B, n) = count_prems (B,n+1)
| count_prems (_,n) = n;
+(*Select Ai from A1 ==>...Ai==>B*)
+fun nth_prem (1, Const ("==>", _) $ A $ _) = A
+ | nth_prem (i, Const ("==>", _) $ _ $ B) = nth_prem (i - 1, B)
+ | nth_prem (_, A) = raise TERM ("nth_prem", [A]);
+
(*strip a proof state (Horn clause):
B1 ==> ... Bn ==> C goes to ([B1, ..., Bn], C) *)
fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);