--- a/src/HOL/Tools/cnf.ML Wed Jan 22 22:22:19 2025 +0100
+++ b/src/HOL/Tools/cnf.ML Wed Jan 22 22:37:38 2025 +0100
@@ -104,9 +104,6 @@
(Seq.hd (REPEAT_DETERM (resolve_tac ctxt @{thms cnf.clause2raw_not_disj} i) thm))
(* moves all premises to hyps, i.e. "[...] |- A1 ==> ... ==> An ==> B" *)
(* becomes "[..., A1, ..., An] |- B" *)
- fun prems_to_hyps thm =
- fold (fn cprem => fn thm' =>
- Thm.implies_elim thm' (Thm.assume cprem)) (Thm.cprems_of thm) thm
in
(* [...] |- ~(x1 | ... | xn) ==> False *)
(@{thm cnf.clause2raw_notE} OF [clause])
@@ -115,7 +112,7 @@
(* [...] |- x1' ==> ... ==> xn' ==> False *)
|> Seq.hd o TRYALL (resolve_tac ctxt @{thms cnf.clause2raw_not_not})
(* [..., x1', ..., xn'] |- False *)
- |> prems_to_hyps
+ |> Thm.assume_prems ~1
end;
(* ------------------------------------------------------------------------- *)
--- a/src/Pure/more_thm.ML Wed Jan 22 22:22:19 2025 +0100
+++ b/src/Pure/more_thm.ML Wed Jan 22 22:37:38 2025 +0100
@@ -63,6 +63,7 @@
val check_shyps: Proof.context -> thm -> thm
val weaken_sorts': Proof.context -> cterm -> cterm
val elim_implies: thm -> thm -> thm
+ val assume_prems: int -> thm -> thm
val forall_intr_name: string * cterm -> thm -> thm
val forall_elim_var: int -> thm -> thm
val forall_elim_vars: int -> thm -> thm
@@ -334,6 +335,12 @@
fun elim_implies thA thAB = Thm.implies_elim thAB thA;
+(* assume_prems: shift at most n premises into hyps, where n < 0 means infinity *)
+
+fun assume_prems n th =
+ fold (elim_implies o Thm.assume) (Thm.take_cprems_of n th) th;
+
+
(* forall_intr_name *)
fun forall_intr_name (a, x) th =