# HG changeset patch # User wenzelm # Date 1737472935 -3600 # Node ID da3c3948a39c6a76cdf9d92a882be69d2e05e0ee # Parent cb8f396dd39f87084d5c43b2ab85f616d3463bb6 clarified signature: more uniform cterm operations, without context; diff -r cb8f396dd39f -r da3c3948a39c src/HOL/Decision_Procs/Dense_Linear_Order.thy --- 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>\Trueprop\ + (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>\Trueprop\ + (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>\Trueprop\ + (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>\Trueprop\ + (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>\Trueprop\ + (HOLogic.mk_judgment (Thm.apply \<^cterm>\Not\ (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>\Trueprop\ + (HOLogic.mk_judgment (Thm.apply \<^cterm>\Not\ (Thm.apply (Thm.apply ceq c) cz))) val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI val rth = Thm.implies_elim diff -r cb8f396dd39f -r da3c3948a39c src/HOL/Import/import_rule.ML --- 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>\Trueprop\ -val assume_thm = Thm.trivial o Thm.apply \<^cterm>\Trueprop\ +val make_thm = Skip_Proof.make_thm_cterm o HOLogic.mk_judgment +val assume_thm = Thm.trivial o HOLogic.mk_judgment (* import file *) diff -r cb8f396dd39f -r da3c3948a39c src/HOL/Library/Sum_of_Squares/positivstellensatz.ML --- 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>\Trueprop\ (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>\Trueprop\ (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>\Trueprop\ 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 diff -r cb8f396dd39f -r da3c3948a39c src/HOL/Library/old_recdef.ML --- 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>\Trueprop\, _) $ _ => true - | _ => false); - -fun mk_prop ct = if is_Trueprop ct then ct else Thm.apply \<^cterm>\Trueprop\ 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; diff -r cb8f396dd39f -r da3c3948a39c src/HOL/Tools/Argo/argo_tactic.ML --- 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>\Trueprop\ 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>\Not\ (Thm.apply \<^cterm>\Not\ (Thm.dest_arg ct))) + let val cu = HOLogic.mk_judgment (Thm.apply \<^cterm>\Not\ (Thm.apply \<^cterm>\Not\ (Thm.dest_arg ct))) in (discharge (Thm.assume cu) dneg_rule, [(~i, cu)]) end diff -r cb8f396dd39f -r da3c3948a39c src/HOL/Tools/BNF/bnf_lfp_countable.ML --- 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; diff -r cb8f396dd39f -r da3c3948a39c src/HOL/Tools/Lifting/lifting_def.ML --- 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 diff -r cb8f396dd39f -r da3c3948a39c src/HOL/Tools/Meson/meson_clausify.ML --- 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>\HOL\ 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>\fun\, [_, 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 diff -r cb8f396dd39f -r da3c3948a39c src/HOL/Tools/Qelim/cooper.ML --- 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>\Trueprop\ (Thm.apply \<^cterm>\Not\ + (HOLogic.mk_judgment (Thm.apply \<^cterm>\Not\ (Thm.apply (Thm.apply \<^cterm>\(=) :: int => _\ (Numeral.mk_cnumber \<^ctyp>\int\ x)) \<^cterm>\0::int\))) 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>\Trueprop\ + (HOLogic.mk_judgment (Thm.apply (Thm.apply dvdc (Numeral.mk_cnumber \<^ctyp>\int\ 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>\Trueprop\ + (HOLogic.mk_judgment (Thm.apply (Thm.apply \<^cterm>\(<) :: int => _\ \<^cterm>\0::int\) 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>\False\ 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>\HOL.implies\ p) q) qs q) - val g = Thm.apply (Thm.apply \<^cterm>\(==>)\ (Thm.apply \<^cterm>\Trueprop\ ng)) p' + val g = Thm.apply (Thm.apply \<^cterm>\(==>)\ (HOLogic.mk_judgment ng)) p' val ntac = (case qs of [] => q aconvc \<^cterm>\False\ | _ => false) in diff -r cb8f396dd39f -r da3c3948a39c src/HOL/Tools/SMT/smt_normalize.ML --- 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>\False\ + val (cpfalse, cfalse) = `HOLogic.mk_judgment \<^cterm>\False\ fun inst f ct thm = let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm)) diff -r cb8f396dd39f -r da3c3948a39c src/HOL/Tools/SMT/smt_replay.ML --- 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 diff -r cb8f396dd39f -r da3c3948a39c src/HOL/Tools/SMT/smt_util.ML --- 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>\Trueprop\ - -fun dest_cprop ct = - (case Thm.term_of ct of - \<^Const_>\Trueprop for _\ => Thm.dest_arg ct - | _ => raise CTERM ("not a property", [ct])) - val equals = mk_const_pat \<^theory> \<^const_name>\Pure.eq\ Thm.dest_ctyp0 fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu diff -r cb8f396dd39f -r da3c3948a39c src/HOL/Tools/coinduction.ML --- 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 = diff -r cb8f396dd39f -r da3c3948a39c src/HOL/Tools/groebner.ML --- 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>\Trueprop\ l)) - val ctabr = mk_conj_tab (Thm.assume (Thm.apply \<^cterm>\Trueprop\ 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>\Trueprop\ 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>\Trueprop\ 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>\False\ then Thm.assume (Thm.apply \<^cterm>\Trueprop\ tm) else + if Thm.term_of tm aconv \<^Const>\False\ 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>\Trueprop\ 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>\Trueprop\ tm) + in Thm.implies_intr (HOLogic.mk_judgment tm) (Thm.equal_elim (Drule.arg_cong_rule \<^cterm>\Trueprop\ (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>\Trueprop\ tm) + in Thm.implies_intr (HOLogic.mk_judgment tm) (Thm.equal_elim (Drule.arg_cong_rule \<^cterm>\Trueprop\ (eqF_intr th4)) (HOLogic.mk_obj_eq (Thm.reflexive l))) end diff -r cb8f396dd39f -r da3c3948a39c src/HOL/Tools/hologic.ML --- 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_>\Trueprop for P\ = P | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); +fun is_Trueprop \<^Const_>\Trueprop for _\ = 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_>\Trueprop for _\ => 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>\Trueprop\; -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>\P and Q in lemma (open) \P \ Q \ P \ Q\ by (rule conjI)\ 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>\P and Q in lemma (open) \P \ Q \ P\ by (rule conjunct1)\ thPQ; @@ -218,9 +231,9 @@ Thm.implies_elim \<^instantiate>\P and Q in lemma (open) \P \ Q \ Q\ by (rule conjunct2)\ 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>\conj\; val disj = \<^Const>\disj\; diff -r cb8f396dd39f -r da3c3948a39c src/HOL/Tools/numeral_simprocs.ML --- 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>\HOL\ HOLogic.Trueprop) + val Tp_Eq = Thm.reflexive \<^cterm>\Trueprop\ 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>\Trueprop\ (Thm.apply \<^cterm>\Not\ + (HOLogic.mk_judgment (Thm.apply \<^cterm>\Not\ (Thm.apply (Thm.apply eq t) z))) in Thm.equal_elim (Thm.symmetric th) TrueI end