# HG changeset patch # User wenzelm # Date 1737581858 -3600 # Node ID 33616e13e17273ab9bfec9db0fd273ad8fededf9 # Parent 6f2bcdfa9a1940cb4b5dd6cf44b8771f364a7500 tuned signature: more operations; diff -r 6f2bcdfa9a19 -r 33616e13e172 src/HOL/Tools/cnf.ML --- 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; (* ------------------------------------------------------------------------- *) diff -r 6f2bcdfa9a19 -r 33616e13e172 src/Pure/more_thm.ML --- 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 =