--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Tue Jan 21 16:12:27 2025 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Tue Jan 21 16:22:15 2025 +0100
@@ -930,7 +930,7 @@
val cz = Thm.dest_arg ct
val neg = cr < @0
val cthp = Simplifier.rewrite ctxt
- (Thm.apply \<^cterm>\<open>Trueprop\<close>
+ (HOLogic.mk_judgment
(if neg then Thm.apply (Thm.apply clt c) cz
else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
@@ -953,7 +953,7 @@
val cz = Thm.dest_arg ct
val neg = cr < @0
val cthp = Simplifier.rewrite ctxt
- (Thm.apply \<^cterm>\<open>Trueprop\<close>
+ (HOLogic.mk_judgment
(if neg then Thm.apply (Thm.apply clt c) cz
else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
@@ -975,7 +975,7 @@
val cz = Thm.dest_arg ct
val neg = cr < @0
val cthp = Simplifier.rewrite ctxt
- (Thm.apply \<^cterm>\<open>Trueprop\<close>
+ (HOLogic.mk_judgment
(if neg then Thm.apply (Thm.apply clt c) cz
else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
@@ -1000,7 +1000,7 @@
val cz = Thm.dest_arg ct
val neg = cr < @0
val cthp = Simplifier.rewrite ctxt
- (Thm.apply \<^cterm>\<open>Trueprop\<close>
+ (HOLogic.mk_judgment
(if neg then Thm.apply (Thm.apply clt c) cz
else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
@@ -1019,7 +1019,7 @@
val ceq = Thm.dest_fun2 ct
val cz = Thm.dest_arg ct
val cthp = Simplifier.rewrite ctxt
- (Thm.apply \<^cterm>\<open>Trueprop\<close>
+ (HOLogic.mk_judgment
(Thm.apply \<^cterm>\<open>Not\<close> (Thm.apply (Thm.apply ceq c) cz)))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
val th = Thm.implies_elim
@@ -1041,7 +1041,7 @@
val ceq = Thm.dest_fun2 ct
val cz = Thm.dest_arg ct
val cthp = Simplifier.rewrite ctxt
- (Thm.apply \<^cterm>\<open>Trueprop\<close>
+ (HOLogic.mk_judgment
(Thm.apply \<^cterm>\<open>Not\<close> (Thm.apply (Thm.apply ceq c) cz)))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
val rth = Thm.implies_elim
--- a/src/HOL/Import/import_rule.ML Tue Jan 21 16:12:27 2025 +0100
+++ b/src/HOL/Import/import_rule.ML Tue Jan 21 16:22:15 2025 +0100
@@ -339,8 +339,8 @@
| NONE => Sign.full_bname thy (#isabelle (make_name c)))
in Thm.global_cterm_of thy (Const (d, Thm.typ_of ty)) end
-val make_thm = Skip_Proof.make_thm_cterm o Thm.apply \<^cterm>\<open>Trueprop\<close>
-val assume_thm = Thm.trivial o Thm.apply \<^cterm>\<open>Trueprop\<close>
+val make_thm = Skip_Proof.make_thm_cterm o HOLogic.mk_judgment
+val assume_thm = Thm.trivial o HOLogic.mk_judgment
(* import file *)
--- a/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Tue Jan 21 16:12:27 2025 +0100
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Tue Jan 21 16:22:15 2025 +0100
@@ -461,10 +461,10 @@
let
val (th1, cert1) =
overall (Left::cert_choice) dun
- (Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.dest_arg1 ct))::oths)
+ (Thm.assume (HOLogic.mk_judgment (Thm.dest_arg1 ct))::oths)
val (th2, cert2) =
overall (Right::cert_choice) dun
- (Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.dest_arg ct))::oths)
+ (Thm.assume (HOLogic.mk_judgment (Thm.dest_arg ct))::oths)
in (disj_cases th th1 th2, Branch (cert1, cert2)) end
else overall cert_choice (th::dun) oths
end
@@ -572,7 +572,7 @@
val (th2, certs) = overall [] [] [specl avs (Thm.assume (Thm.rhs_of th1))]
val th3 =
fold simple_choose evs
- (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> bod))) th2)
+ (prove_hyp (Thm.equal_elim th1 (Thm.assume (HOLogic.mk_judgment bod))) th2)
in (Drule.implies_intr_hyps (prove_hyp (Thm.equal_elim th0 (Thm.assume not_A)) th3), certs)
end
in
--- a/src/HOL/Library/old_recdef.ML Tue Jan 21 16:12:27 2025 +0100
+++ b/src/HOL/Library/old_recdef.ML Tue Jan 21 16:22:15 2025 +0100
@@ -896,13 +896,8 @@
* Going into and out of prop
*---------------------------------------------------------------------------*)
-fun is_Trueprop ct =
- (case Thm.term_of ct of
- Const (\<^const_name>\<open>Trueprop\<close>, _) $ _ => true
- | _ => false);
-
-fun mk_prop ct = if is_Trueprop ct then ct else Thm.apply \<^cterm>\<open>Trueprop\<close> ct;
-fun drop_prop ct = if is_Trueprop ct then Thm.dest_arg ct else ct;
+fun mk_prop ct = if HOLogic.is_judgment ct then ct else HOLogic.mk_judgment ct;
+fun drop_prop ct = if HOLogic.is_judgment ct then Thm.dest_arg ct else ct;
end;
--- a/src/HOL/Tools/Argo/argo_tactic.ML Tue Jan 21 16:12:27 2025 +0100
+++ b/src/HOL/Tools/Argo/argo_tactic.ML Tue Jan 21 16:22:15 2025 +0100
@@ -286,10 +286,8 @@
SOME t => t
| NONE => raise Fail "bad expression")
-fun as_prop ct = Thm.apply \<^cterm>\<open>Trueprop\<close> ct
-
fun cterm_of ctxt cons e = Thm.cterm_of ctxt (term_of (ctxt, cons) e)
-fun cprop_of ctxt cons e = as_prop (cterm_of ctxt cons e)
+fun cprop_of ctxt cons e = HOLogic.mk_judgment (cterm_of ctxt cons e)
(* generic proof tools *)
@@ -299,7 +297,7 @@
fun discharges thm rules = [thm] RL rules
fun under_assumption f ct =
- let val cprop = as_prop ct
+ let val cprop = HOLogic.mk_judgment ct
in Thm.implies_intr cprop (f (Thm.assume cprop)) end
@@ -537,7 +535,7 @@
fun replay_hyp i ct =
if i < 0 then (Thm.assume ct, [(~i, ct)])
else
- let val cu = as_prop (Thm.apply \<^cterm>\<open>Not\<close> (Thm.apply \<^cterm>\<open>Not\<close> (Thm.dest_arg ct)))
+ let val cu = HOLogic.mk_judgment (Thm.apply \<^cterm>\<open>Not\<close> (Thm.apply \<^cterm>\<open>Not\<close> (Thm.dest_arg ct)))
in (discharge (Thm.assume cu) dneg_rule, [(~i, cu)]) end
--- a/src/HOL/Tools/BNF/bnf_lfp_countable.ML Tue Jan 21 16:12:27 2025 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_countable.ML Tue Jan 21 16:22:15 2025 +0100
@@ -176,7 +176,7 @@
Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} =>
mk_encode_injectives_tac ctxt ns induct nchotomys injectss rec_thmss map_comps'
inj_map_strongs')
- |> HOLogic.conj_elims ctxt
+ |> HOLogic.conj_elims
|> Proof_Context.export names_ctxt ctxt
|> map (Thm.close_derivation \<^here>)
end;
--- a/src/HOL/Tools/Lifting/lifting_def.ML Tue Jan 21 16:12:27 2025 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Tue Jan 21 16:22:15 2025 +0100
@@ -222,8 +222,7 @@
val typ = Thm.typ_of_cterm rel
val POS_const = Thm.cterm_of ctxt (mk_POS typ)
val var = Thm.cterm_of ctxt (Var (("X", Thm.maxidx_of_cterm rel + 1), typ))
- val goal =
- Thm.apply (Thm.cterm_of ctxt HOLogic.Trueprop) (Thm.apply (Thm.apply POS_const rel) var)
+ val goal = HOLogic.mk_judgment (Thm.apply (Thm.apply POS_const rel) var)
in
[Lifting_Term.merge_transfer_relations ctxt goal, thm] MRSL @{thm POS_apply}
end
--- a/src/HOL/Tools/Meson/meson_clausify.ML Tue Jan 21 16:12:27 2025 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Tue Jan 21 16:22:15 2025 +0100
@@ -184,9 +184,6 @@
(* A type variable of sort "{}" will make "abstraction" fail. *)
TrueI)
-(*cterms are used throughout for efficiency*)
-val cTrueprop = Thm.cterm_of \<^theory_context>\<open>HOL\<close> HOLogic.Trueprop;
-
(*Given an abstraction over n variables, replace the bound variables by free
ones. Return the body, along with the list of free variables.*)
fun c_variant_abs_multi (ct0, vars) =
@@ -208,10 +205,10 @@
Const (_, Type (\<^type_name>\<open>fun\<close>, [_, T])) => T
| _ => raise TERM ("old_skolem_theorem_of_def: expected \"Eps\"", [hilbert])
val cex = Thm.cterm_of ctxt (HOLogic.exists_const T)
- val ex_tm = Thm.apply cTrueprop (Thm.apply cex cabs)
+ val ex_tm = HOLogic.mk_judgment (Thm.apply cex cabs)
val conc =
Drule.list_comb (rhs, frees)
- |> Drule.beta_conv cabs |> Thm.apply cTrueprop
+ |> Drule.beta_conv cabs |> HOLogic.mk_judgment
fun tacf [prem] =
rewrite_goals_tac ctxt @{thms skolem_def [abs_def]}
THEN resolve_tac ctxt
--- a/src/HOL/Tools/Qelim/cooper.ML Tue Jan 21 16:12:27 2025 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML Tue Jan 21 16:22:15 2025 +0100
@@ -376,7 +376,7 @@
let
val th =
Simplifier.rewrite (put_simpset lin_ss ctxt)
- (Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.apply \<^cterm>\<open>Not\<close>
+ (HOLogic.mk_judgment (Thm.apply \<^cterm>\<open>Not\<close>
(Thm.apply (Thm.apply \<^cterm>\<open>(=) :: int => _\<close> (Numeral.mk_cnumber \<^ctyp>\<open>int\<close> x))
\<^cterm>\<open>0::int\<close>)))
in Thm.equal_elim (Thm.symmetric th) TrueI end;
@@ -469,7 +469,7 @@
let
val th =
Simplifier.rewrite (put_simpset lin_ss ctxt)
- (Thm.apply \<^cterm>\<open>Trueprop\<close>
+ (HOLogic.mk_judgment
(Thm.apply (Thm.apply dvdc (Numeral.mk_cnumber \<^ctyp>\<open>int\<close> x)) cd))
in Thm.equal_elim (Thm.symmetric th) TrueI end;
val dvd =
@@ -481,7 +481,7 @@
end
val dp =
let val th = Simplifier.rewrite (put_simpset lin_ss ctxt)
- (Thm.apply \<^cterm>\<open>Trueprop\<close>
+ (HOLogic.mk_judgment
(Thm.apply (Thm.apply \<^cterm>\<open>(<) :: int => _\<close> \<^cterm>\<open>0::int\<close>) cd))
in Thm.equal_elim (Thm.symmetric th) TrueI end;
(* A and B set *)
@@ -736,7 +736,7 @@
val q = if P c then c else \<^cterm>\<open>False\<close>
val ng = fold_rev (fn (a,v) => fn t => Thm.apply a (Thm.lambda v t)) qvs
(fold_rev (fn p => fn q => Thm.apply (Thm.apply \<^cterm>\<open>HOL.implies\<close> p) q) qs q)
- val g = Thm.apply (Thm.apply \<^cterm>\<open>(==>)\<close> (Thm.apply \<^cterm>\<open>Trueprop\<close> ng)) p'
+ val g = Thm.apply (Thm.apply \<^cterm>\<open>(==>)\<close> (HOLogic.mk_judgment ng)) p'
val ntac = (case qs of [] => q aconvc \<^cterm>\<open>False\<close>
| _ => false)
in
--- a/src/HOL/Tools/SMT/smt_normalize.ML Tue Jan 21 16:12:27 2025 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Tue Jan 21 16:22:15 2025 +0100
@@ -31,7 +31,7 @@
(** instantiate elimination rules **)
local
- val (cpfalse, cfalse) = `SMT_Util.mk_cprop \<^cterm>\<open>False\<close>
+ val (cpfalse, cfalse) = `HOLogic.mk_judgment \<^cterm>\<open>False\<close>
fun inst f ct thm =
let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
--- a/src/HOL/Tools/SMT/smt_replay.ML Tue Jan 21 16:12:27 2025 +0100
+++ b/src/HOL/Tools/SMT/smt_replay.ML Tue Jan 21 16:22:15 2025 +0100
@@ -80,7 +80,7 @@
(* proof combinators *)
fun under_assumption f ct =
- let val ct' = SMT_Util.mk_cprop ct in Thm.implies_intr ct' (f (Thm.assume ct')) end
+ let val ct' = HOLogic.mk_judgment ct in Thm.implies_intr ct' (f (Thm.assume ct')) end
fun discharge p pq = Thm.implies_elim pq p
--- a/src/HOL/Tools/SMT/smt_util.ML Tue Jan 21 16:12:27 2025 +0100
+++ b/src/HOL/Tools/SMT/smt_util.ML Tue Jan 21 16:22:15 2025 +0100
@@ -51,8 +51,6 @@
val dest_all_cabs: cterm -> Proof.context -> cterm * Proof.context
val dest_cbinder: cterm -> Proof.context -> cterm * Proof.context
val dest_all_cbinders: cterm -> Proof.context -> cterm * Proof.context
- val mk_cprop: cterm -> cterm
- val dest_cprop: cterm -> cterm
val mk_cequals: cterm -> cterm -> cterm
val term_of: cterm -> term
val prop_of: thm -> term
@@ -201,13 +199,6 @@
val dest_all_cbinders = repeat_yield (try o dest_cbinder)
-val mk_cprop = Thm.apply \<^cterm>\<open>Trueprop\<close>
-
-fun dest_cprop ct =
- (case Thm.term_of ct of
- \<^Const_>\<open>Trueprop for _\<close> => Thm.dest_arg ct
- | _ => raise CTERM ("not a property", [ct]))
-
val equals = mk_const_pat \<^theory> \<^const_name>\<open>Pure.eq\<close> Thm.dest_ctyp0
fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu
--- a/src/HOL/Tools/coinduction.ML Tue Jan 21 16:12:27 2025 +0100
+++ b/src/HOL/Tools/coinduction.ML Tue Jan 21 16:22:15 2025 +0100
@@ -106,7 +106,7 @@
[] => all_tac
| inv :: case_prems =>
let
- val (init, last) = funpow_yield (p + e - 1) (HOLogic.conj_elim ctxt) inv;
+ val (init, last) = funpow_yield (p + e - 1) HOLogic.conj_elim inv;
val inv_thms = init @ [last];
val eqs = take e inv_thms;
fun is_local_var t =
--- a/src/HOL/Tools/groebner.ML Tue Jan 21 16:12:27 2025 +0100
+++ b/src/HOL/Tools/groebner.ML Tue Jan 21 16:22:15 2025 +0100
@@ -455,8 +455,8 @@
fun conj_ac_rule eq =
let
val (l,r) = Thm.dest_equals eq
- val ctabl = mk_conj_tab (Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> l))
- val ctabr = mk_conj_tab (Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> r))
+ val ctabl = mk_conj_tab (Thm.assume (HOLogic.mk_judgment l))
+ val ctabr = mk_conj_tab (Thm.assume (HOLogic.mk_judgment r))
fun tabl c = the (Termtab.lookup ctabl (Thm.term_of c))
fun tabr c = the (Termtab.lookup ctabr (Thm.term_of c))
val thl = prove_conj tabl (conjuncts r) |> implies_intr_hyps
@@ -485,7 +485,7 @@
| _ => error "" (* FIXME ? *)
fun simple_choose ctxt v th =
- choose v (Thm.assume ((Thm.apply \<^cterm>\<open>Trueprop\<close> o mk_ex ctxt v)
+ choose v (Thm.assume ((HOLogic.mk_judgment o mk_ex ctxt v)
(Thm.dest_arg (hd (Thm.chyps_of th))))) th
@@ -502,7 +502,7 @@
val (p0,q0) = Thm.dest_binop t
val (vs',P) = strip_exists p0
val (vs,_) = strip_exists q0
- val th = Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> P)
+ val th = Thm.assume (HOLogic.mk_judgment P)
val th1 = implies_intr_hyps (fold (simple_choose ctxt) vs' (fold mkexi vs th))
val th2 = implies_intr_hyps (fold (simple_choose ctxt) vs (fold mkexi vs' th))
val p = (Thm.dest_arg o Thm.dest_arg1 o Thm.cprop_of) th1
@@ -662,23 +662,23 @@
fun mk_add th1 = Thm.combination (Drule.arg_cong_rule ring_add_tm th1);
fun refute ctxt tm =
- if Thm.term_of tm aconv \<^Const>\<open>False\<close> then Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> tm) else
+ if Thm.term_of tm aconv \<^Const>\<open>False\<close> then Thm.assume (HOLogic.mk_judgment tm) else
((let
val (nths0,eths0) =
List.partition (is_neg o concl)
- (HOLogic.conj_elims ctxt (Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> tm)))
+ (HOLogic.conj_elims (Thm.assume (HOLogic.mk_judgment tm)))
val nths = filter (is_eq o Thm.dest_arg o concl) nths0
val eths = filter (is_eq o concl) eths0
in
if null eths then
let
- val th1 = end_itlist (fn th1 => fn th2 => idom_rule ctxt (HOLogic.conj_intr ctxt th1 th2)) nths
+ val th1 = end_itlist (fn th1 => fn th2 => idom_rule ctxt (HOLogic.conj_intr th1 th2)) nths
val th2 =
Conv.fconv_rule
((Conv.arg_conv #> Conv.arg_conv) (Conv.binop_conv ring_normalize_conv)) th1
val conc = th2 |> concl |> Thm.dest_arg
val (l,_) = conc |> dest_eq
- in Thm.implies_intr (Thm.apply \<^cterm>\<open>Trueprop\<close> tm)
+ in Thm.implies_intr (HOLogic.mk_judgment tm)
(Thm.equal_elim (Drule.arg_cong_rule \<^cterm>\<open>Trueprop\<close> (eqF_intr th2))
(HOLogic.mk_obj_eq (Thm.reflexive l)))
end
@@ -692,13 +692,13 @@
end
else
let
- val nth = end_itlist (fn th1 => fn th2 => idom_rule ctxt (HOLogic.conj_intr ctxt th1 th2)) nths
+ val nth = end_itlist (fn th1 => fn th2 => idom_rule ctxt (HOLogic.conj_intr th1 th2)) nths
val (vars,pol::pols) =
grobify_equations(list_mk_conj(Thm.dest_arg(concl nth)::map concl eths))
val (deg,l,cert) = grobner_strong vars pols pol
val th1 =
Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv) (Conv.binop_conv ring_normalize_conv)) nth
- val th2 = funpow deg (idom_rule ctxt o HOLogic.conj_intr ctxt th1) neq_01
+ val th2 = funpow deg (idom_rule ctxt o HOLogic.conj_intr th1) neq_01
in (vars,l,cert,th2)
end)
val cert_pos = map (fn (i,p) => (i,filter (fn (c,_) => c > @0) p)) cert
@@ -713,12 +713,12 @@
(nth eths i |> mk_meta_eq)) pols)
val th1 = thm_fn herts_pos
val th2 = thm_fn herts_neg
- val th3 = HOLogic.conj_intr ctxt (HOLogic.mk_obj_eq (mk_add (Thm.symmetric th1) th2)) noteqth
+ val th3 = HOLogic.conj_intr (HOLogic.mk_obj_eq (mk_add (Thm.symmetric th1) th2)) noteqth
val th4 =
Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv o Conv.binop_conv) ring_normalize_conv)
(neq_rule l th3)
val (l, _) = dest_eq(Thm.dest_arg(concl th4))
- in Thm.implies_intr (Thm.apply \<^cterm>\<open>Trueprop\<close> tm)
+ in Thm.implies_intr (HOLogic.mk_judgment tm)
(Thm.equal_elim (Drule.arg_cong_rule \<^cterm>\<open>Trueprop\<close> (eqF_intr th4))
(HOLogic.mk_obj_eq (Thm.reflexive l)))
end
--- a/src/HOL/Tools/hologic.ML Tue Jan 21 16:12:27 2025 +0100
+++ b/src/HOL/Tools/hologic.ML Tue Jan 21 16:22:15 2025 +0100
@@ -14,7 +14,11 @@
val Trueprop: term
val mk_Trueprop: term -> term
val dest_Trueprop: term -> term
+ val is_Trueprop: term -> bool
val Trueprop_conv: conv -> conv
+ val mk_judgment: cterm -> cterm
+ val is_judgment: cterm -> bool
+ val dest_judgment: cterm -> cterm
val mk_induct_forall: typ -> term
val mk_setT: typ -> typ
val dest_setT: typ -> typ
@@ -25,9 +29,9 @@
val mk_set: typ -> term list -> term
val dest_set: term -> term list
val mk_UNIV: typ -> term
- val conj_intr: Proof.context -> thm -> thm -> thm
- val conj_elim: Proof.context -> thm -> thm * thm
- val conj_elims: Proof.context -> thm -> thm list
+ val conj_intr: thm -> thm -> thm
+ val conj_elim: thm -> thm * thm
+ val conj_elims: thm -> thm list
val conj: term
val disj: term
val imp: term
@@ -195,22 +199,31 @@
fun dest_Trueprop \<^Const_>\<open>Trueprop for P\<close> = P
| dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
+fun is_Trueprop \<^Const_>\<open>Trueprop for _\<close> = true
+ | is_Trueprop _ = false;
+
+val is_judgment = is_Trueprop o Thm.term_of;
+
fun Trueprop_conv cv ct =
- (case Thm.term_of ct of
- \<^Const_>\<open>Trueprop for _\<close> => Conv.arg_conv cv ct
- | _ => raise CTERM ("Trueprop_conv", [ct]))
+ if is_judgment ct then Conv.arg_conv cv ct
+ else raise CTERM ("Trueprop_conv", [ct]);
+val mk_judgment = Thm.apply \<^cterm>\<open>Trueprop\<close>;
-fun conj_intr ctxt thP thQ =
+fun dest_judgment ct =
+ if is_judgment ct then Thm.dest_arg ct
+ else raise CTERM ("dest_judgment", [ct]);
+
+fun conj_intr thP thQ =
let
- val (P, Q) = apply2 (Object_Logic.dest_judgment ctxt o Thm.cprop_of) (thP, thQ)
+ val (P, Q) = apply2 (dest_judgment o Thm.cprop_of) (thP, thQ)
handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]);
val rule = \<^instantiate>\<open>P and Q in lemma (open) \<open>P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q\<close> by (rule conjI)\<close>
in Drule.implies_elim_list rule [thP, thQ] end;
-fun conj_elim ctxt thPQ =
+fun conj_elim thPQ =
let
- val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment ctxt (Thm.cprop_of thPQ))
+ val (P, Q) = Thm.dest_binop (dest_judgment (Thm.cprop_of thPQ))
handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]);
val thP =
Thm.implies_elim \<^instantiate>\<open>P and Q in lemma (open) \<open>P \<and> Q \<Longrightarrow> P\<close> by (rule conjunct1)\<close> thPQ;
@@ -218,9 +231,9 @@
Thm.implies_elim \<^instantiate>\<open>P and Q in lemma (open) \<open>P \<and> Q \<Longrightarrow> Q\<close> by (rule conjunct2)\<close> thPQ;
in (thP, thQ) end;
-fun conj_elims ctxt th =
- let val (th1, th2) = conj_elim ctxt th
- in conj_elims ctxt th1 @ conj_elims ctxt th2 end handle THM _ => [th];
+fun conj_elims th =
+ let val (th1, th2) = conj_elim th
+ in conj_elims th1 @ conj_elims th2 end handle THM _ => [th];
val conj = \<^Const>\<open>conj\<close>;
val disj = \<^Const>\<open>disj\<close>;
--- a/src/HOL/Tools/numeral_simprocs.ML Tue Jan 21 16:12:27 2025 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML Tue Jan 21 16:22:15 2025 +0100
@@ -471,7 +471,7 @@
simplify_one ctxt (([th, cancel_th]) MRS trans);
local
- val Tp_Eq = Thm.reflexive (Thm.cterm_of \<^theory_context>\<open>HOL\<close> HOLogic.Trueprop)
+ val Tp_Eq = Thm.reflexive \<^cterm>\<open>Trueprop\<close>
fun Eq_True_elim Eq =
Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI}
in
@@ -593,7 +593,7 @@
val eq = Thm.instantiate_cterm (TVars.make1 (type_tvar, T), Vars.empty) geq
val th =
Simplifier.rewrite (ctxt addsimps @{thms simp_thms})
- (Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.apply \<^cterm>\<open>Not\<close>
+ (HOLogic.mk_judgment (Thm.apply \<^cterm>\<open>Not\<close>
(Thm.apply (Thm.apply eq t) z)))
in Thm.equal_elim (Thm.symmetric th) TrueI end