--- a/src/HOL/Tools/groebner.ML Sun Aug 18 14:22:21 2024 +0200
+++ b/src/HOL/Tools/groebner.ML Sun Aug 18 14:40:49 2024 +0200
@@ -349,23 +349,23 @@
fun refute_disj rfn tm =
case Thm.term_of tm of
- Const(\<^const_name>\<open>HOL.disj\<close>,_)$_$_ =>
+ \<^Const_>\<open>disj for _ _\<close> =>
Drule.compose
(refute_disj rfn (Thm.dest_arg tm), 2,
Drule.compose (refute_disj rfn (Thm.dest_arg1 tm), 2, disjE))
| _ => rfn tm ;
-val notnotD = @{thm notnotD};
fun mk_binop ct x y = Thm.apply (Thm.apply ct x) y
fun is_neg t =
- case Thm.term_of t of
- (Const(\<^const_name>\<open>Not\<close>,_)$_) => true
- | _ => false;
+ case Thm.term_of t of
+ \<^Const_>\<open>Not for _\<close> => true
+ | _ => false;
+
fun is_eq t =
- case Thm.term_of t of
- (Const(\<^const_name>\<open>HOL.eq\<close>,_)$_$_) => true
-| _ => false;
+ case Thm.term_of t of
+ \<^Const_>\<open>HOL.eq _ for _ _\<close> => true
+ | _ => false;
fun end_itlist f l =
case l of
@@ -392,9 +392,9 @@
end;
fun is_forall t =
- case Thm.term_of t of
- (Const(\<^const_name>\<open>All\<close>,_)$Abs(_,_,_)) => true
-| _ => false;
+ case Thm.term_of t of
+ \<^Const_>\<open>All _ for \<open>Abs _\<close>\<close> => true
+ | _ => false;
val nnf_simps = @{thms nnf_simps};
@@ -436,21 +436,21 @@
(* FIXME : copied from cqe.ML -- complex QE*)
fun conjuncts ct =
- case Thm.term_of ct of
- \<^term>\<open>HOL.conj\<close>$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
-| _ => [ct];
+ case Thm.term_of ct of
+ \<^Const_>\<open>conj for _ _\<close> => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
+ | _ => [ct];
fun fold1 f = foldr1 (uncurry f);
fun mk_conj_tab th =
- let fun h acc th =
- case Thm.prop_of th of
- \<^term>\<open>Trueprop\<close>$(\<^term>\<open>HOL.conj\<close>$_$_) =>
- h (h acc (th RS conjunct2)) (th RS conjunct1)
- | \<^term>\<open>Trueprop\<close>$p => (p,th)::acc
-in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
+ let fun h acc th =
+ case Thm.prop_of th of
+ \<^Const_>\<open>Trueprop for \<^Const_>\<open>conj for _ _\<close>\<close> =>
+ h (h acc (th RS conjunct2)) (th RS conjunct1)
+ | \<^Const_>\<open>Trueprop for p\<close> => (p,th)::acc
+ in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
-fun is_conj (\<^term>\<open>HOL.conj\<close>$_$_) = true
+fun is_conj \<^Const_>\<open>conj for _ _\<close> = true
| is_conj _ = false;
fun prove_conj tab cjs =
@@ -474,11 +474,11 @@
(* Conversion for the equivalence of existential statements where
EX quantifiers are rearranged differently *)
-fun ext ctxt T = Thm.cterm_of ctxt (Const (\<^const_name>\<open>Ex\<close>, (T --> \<^typ>\<open>bool\<close>) --> \<^typ>\<open>bool\<close>))
+fun ext ctxt T = Thm.cterm_of ctxt \<^Const>\<open>Ex T\<close>
fun mk_ex ctxt v t = Thm.apply (ext ctxt (Thm.typ_of_cterm v)) (Thm.lambda v t)
fun choose v th th' = case Thm.concl_of th of
- \<^term>\<open>Trueprop\<close> $ (Const(\<^const_name>\<open>Ex\<close>,_)$_) =>
+ \<^Const_>\<open>Trueprop for \<^Const_>\<open>Ex _ for _\<close>\<close> =>
let
val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th
val T = Thm.dest_ctyp0 (Thm.ctyp_of_cterm p)
@@ -488,7 +488,7 @@
(Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.apply p v))
val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
in Thm.implies_elim (Thm.implies_elim th0 th) th1 end
-| _ => error "" (* FIXME ? *)
+ | _ => error "" (* FIXME ? *)
fun simple_choose ctxt v th =
choose v (Thm.assume ((Thm.apply \<^cterm>\<open>Trueprop\<close> o mk_ex ctxt v)
@@ -734,7 +734,7 @@
fun mk_forall x p =
let
val T = Thm.typ_of_cterm x;
- val all = Thm.cterm_of ctxt (Const (\<^const_name>\<open>All\<close>, (T --> \<^typ>\<open>bool\<close>) --> \<^typ>\<open>bool\<close>))
+ val all = Thm.cterm_of ctxt \<^Const>\<open>All T\<close>
in Thm.apply all (Thm.lambda x p) end
val avs = Cterms.build (Drule.add_frees_cterm tm)
val P' = fold mk_forall (Cterms.list_set_rev avs) tm
@@ -753,7 +753,7 @@
(Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps [not_ex RS sym])
(th2 |> Thm.cprop_of)) th2
in specl (Cterms.list_set_rev avs)
- ([[[HOLogic.mk_obj_eq th1, th3 RS PFalse'] MRS trans] MRS PFalse] MRS notnotD)
+ ([[[HOLogic.mk_obj_eq th1, th3 RS PFalse'] MRS trans] MRS PFalse] MRS @{thm notnotD})
end
end
fun ideal tms tm ord =
@@ -890,18 +890,18 @@
fun find_term tm ctxt =
(case Thm.term_of tm of
- Const (\<^const_name>\<open>HOL.eq\<close>, T) $ _ $ _ =>
- if domain_type T = HOLogic.boolT then find_args tm ctxt
+ \<^Const_>\<open>HOL.eq T for _ _\<close> =>
+ if T = \<^Type>\<open>bool\<close> then find_args tm ctxt
else (Thm.dest_arg tm, ctxt)
- | Const (\<^const_name>\<open>Not\<close>, _) $ _ => find_term (Thm.dest_arg tm) ctxt
- | Const (\<^const_name>\<open>All\<close>, _) $ _ => find_body (Thm.dest_arg tm) ctxt
- | Const (\<^const_name>\<open>Ex\<close>, _) $ _ => find_body (Thm.dest_arg tm) ctxt
- | Const (\<^const_name>\<open>HOL.conj\<close>, _) $ _ $ _ => find_args tm ctxt
- | Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ _ => find_args tm ctxt
- | Const (\<^const_name>\<open>HOL.implies\<close>, _) $ _ $ _ => find_args tm ctxt
- | \<^term>\<open>Pure.imp\<close> $_$_ => find_args tm ctxt
+ | \<^Const_>\<open>Not for _\<close> => find_term (Thm.dest_arg tm) ctxt
+ | \<^Const_>\<open>All _ for _\<close> => find_body (Thm.dest_arg tm) ctxt
+ | \<^Const_>\<open>Ex _ for _\<close> => find_body (Thm.dest_arg tm) ctxt
+ | \<^Const_>\<open>conj for _ _\<close> => find_args tm ctxt
+ | \<^Const_>\<open>disj for _ _\<close> => find_args tm ctxt
+ | \<^Const_>\<open>implies for _ _\<close> => find_args tm ctxt
+ | \<^Const_>\<open>Pure.imp for _ _\<close> => find_args tm ctxt
| Const("(==)",_)$_$_ => find_args tm ctxt (* FIXME proper const name *)
- | \<^term>\<open>Trueprop\<close>$_ => find_term (Thm.dest_arg tm) ctxt
+ | \<^Const_>\<open>Trueprop for _\<close> => find_term (Thm.dest_arg tm) ctxt
| _ => raise TERM ("find_term", []))
and find_args tm ctxt =
let val (t, u) = Thm.dest_binop tm
@@ -942,9 +942,11 @@
| THM _ => no_tac);
local
- fun lhs t = case Thm.term_of t of
- Const(\<^const_name>\<open>HOL.eq\<close>,_)$_$_ => Thm.dest_arg1 t
- | _=> raise CTERM ("ideal_tac - lhs",[t])
+ fun lhs t =
+ case Thm.term_of t of
+ \<^Const_>\<open>HOL.eq _ for _ _\<close> => Thm.dest_arg1 t
+ | _=> raise CTERM ("ideal_tac - lhs",[t])
+
fun exitac _ NONE = no_tac
| exitac ctxt (SOME y) =
resolve_tac ctxt [Thm.instantiate' [SOME (Thm.ctyp_of_cterm y)] [NONE,SOME y] exI] 1
--- a/src/HOL/Tools/semiring_normalizer.ML Sun Aug 18 14:22:21 2024 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML Sun Aug 18 14:40:49 2024 +0200
@@ -128,17 +128,17 @@
let
fun numeral_is_const ct =
case Thm.term_of ct of
- Const (\<^const_name>\<open>Rings.divide\<close>,_) $ a $ b =>
- can HOLogic.dest_number a andalso can HOLogic.dest_number b
- | Const (\<^const_name>\<open>Fields.inverse\<close>,_)$t => can HOLogic.dest_number t
- | t => can HOLogic.dest_number t
- fun dest_const ct = ((case Thm.term_of ct of
- Const (\<^const_name>\<open>Rings.divide\<close>,_) $ a $ b=>
- Rat.make (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
- | Const (\<^const_name>\<open>Fields.inverse\<close>,_)$t =>
- Rat.inv (Rat.of_int (snd (HOLogic.dest_number t)))
- | t => Rat.of_int (snd (HOLogic.dest_number t)))
- handle TERM _ => error "ring_dest_const")
+ \<^Const_>\<open>divide _ for a b\<close> =>
+ can HOLogic.dest_number a andalso can HOLogic.dest_number b
+ | \<^Const_>\<open>inverse _ for t\<close> => can HOLogic.dest_number t
+ | t => can HOLogic.dest_number t
+ fun dest_const ct =
+ (case Thm.term_of ct of
+ \<^Const_>\<open>divide _ for a b\<close> =>
+ Rat.make (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
+ | \<^Const_>\<open>inverse _ for t\<close> => Rat.inv (Rat.of_int (snd (HOLogic.dest_number t)))
+ | t => Rat.of_int (snd (HOLogic.dest_number t)))
+ handle TERM _ => error "ring_dest_const"
fun mk_const cT x =
let val (a, b) = Rat.dest x
in if b = 1 then Numeral.mk_cnumber cT a