--- a/src/HOL/Tools/arith_data.ML Sun Aug 18 15:29:03 2024 +0200
+++ b/src/HOL/Tools/arith_data.ML Sun Aug 18 15:29:18 2024 +0200
@@ -57,29 +57,21 @@
fun mk_number T 1 = HOLogic.numeral_const T $ HOLogic.one_const
| mk_number T n = HOLogic.mk_number T n;
-val mk_plus = HOLogic.mk_binop \<^const_name>\<open>Groups.plus\<close>;
-
-fun mk_minus t =
- let val T = Term.fastype_of t
- in Const (\<^const_name>\<open>Groups.uminus\<close>, T --> T) $ t end;
-
(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
fun mk_sum T [] = mk_number T 0
- | mk_sum T [t, u] = mk_plus (t, u)
- | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
+ | mk_sum T [t, u] = \<^Const>\<open>plus T for t u\<close>
+ | mk_sum T (t :: ts) = \<^Const>\<open>plus T for t \<open>mk_sum T ts\<close>\<close>;
(*this version ALWAYS includes a trailing zero*)
fun long_mk_sum T [] = mk_number T 0
- | long_mk_sum T (t :: ts) = mk_plus (t, long_mk_sum T ts);
+ | long_mk_sum T (t :: ts) = \<^Const>\<open>plus T for t \<open>long_mk_sum T ts\<close>\<close>;
(*decompose additions AND subtractions as a sum*)
-fun dest_summing (pos, Const (\<^const_name>\<open>Groups.plus\<close>, _) $ t $ u, ts) =
- dest_summing (pos, t, dest_summing (pos, u, ts))
- | dest_summing (pos, Const (\<^const_name>\<open>Groups.minus\<close>, _) $ t $ u, ts) =
- dest_summing (pos, t, dest_summing (not pos, u, ts))
- | dest_summing (pos, t, ts) = (if pos then t else mk_minus t) :: ts;
+fun dest_summing pos \<^Const_>\<open>plus _ for t u\<close> ts = dest_summing pos t (dest_summing pos u ts)
+ | dest_summing pos \<^Const_>\<open>minus _ for t u\<close> ts = dest_summing pos t (dest_summing (not pos) u ts)
+ | dest_summing pos t ts = (if pos then t else \<^Const>\<open>uminus \<open>fastype_of t\<close> for t\<close>) :: ts;
-fun dest_sum t = dest_summing (true, t, []);
+fun dest_sum t = dest_summing true t [];
(* various auxiliary and legacy *)
--- a/src/HOL/Tools/boolean_algebra_cancel.ML Sun Aug 18 15:29:03 2024 +0200
+++ b/src/HOL/Tools/boolean_algebra_cancel.ML Sun Aug 18 15:29:18 2024 +0200
@@ -16,19 +16,19 @@
fun move_to_front rule path = Conv.rewr_conv (Library.foldl (op RS) (rule, path))
-fun add_atoms sup pos path (t as Const (\<^const_name>\<open>Lattices.sup\<close>, _) $ x $ y) =
+fun add_atoms sup pos path (t as \<^Const_>\<open>sup _ for x y\<close>) =
if sup then
add_atoms sup pos (@{thm boolean_algebra_cancel.sup1}::path) x #>
add_atoms sup pos (@{thm boolean_algebra_cancel.sup2}::path) y
else cons ((pos, t), path)
- | add_atoms sup pos path (t as Const (\<^const_name>\<open>Lattices.inf\<close>, _) $ x $ y) =
+ | add_atoms sup pos path (t as \<^Const_>\<open>inf _ for x y\<close>) =
if not sup then
add_atoms sup pos (@{thm boolean_algebra_cancel.inf1}::path) x #>
add_atoms sup pos (@{thm boolean_algebra_cancel.inf2}::path) y
else cons ((pos, t), path)
- | add_atoms _ _ _ (Const (\<^const_name>\<open>Orderings.bot\<close>, _)) = I
- | add_atoms _ _ _ (Const (\<^const_name>\<open>Orderings.top\<close>, _)) = I
- | add_atoms _ pos path (Const (\<^const_name>\<open>Groups.uminus\<close>, _) $ x) = cons ((not pos, x), path)
+ | add_atoms _ _ _ \<^Const_>\<open>bot _\<close> = I
+ | add_atoms _ _ _ \<^Const_>\<open>top _\<close> = I
+ | add_atoms _ pos path \<^Const_>\<open>uminus _ for x\<close> = cons ((not pos, x), path)
| add_atoms _ pos path x = cons ((pos, x), path);
fun atoms sup pos t = add_atoms sup pos [] t []
--- a/src/HOL/Tools/group_cancel.ML Sun Aug 18 15:29:03 2024 +0200
+++ b/src/HOL/Tools/group_cancel.ML Sun Aug 18 15:29:18 2024 +0200
@@ -24,15 +24,15 @@
[Conv.rewr_conv (Library.foldl (op RS) (@{thm group_cancel.rule0}, path)),
Conv.arg1_conv (Conv.repeat_conv (Conv.rewr_conv minus_minus))]
-fun add_atoms pos path (Const (\<^const_name>\<open>Groups.plus\<close>, _) $ x $ y) =
+fun add_atoms pos path \<^Const_>\<open>plus _ for x y\<close> =
add_atoms pos (@{thm group_cancel.add1}::path) x #>
add_atoms pos (@{thm group_cancel.add2}::path) y
- | add_atoms pos path (Const (\<^const_name>\<open>Groups.minus\<close>, _) $ x $ y) =
+ | add_atoms pos path \<^Const_>\<open>minus _ for x y\<close> =
add_atoms pos (@{thm group_cancel.sub1}::path) x #>
add_atoms (not pos) (@{thm group_cancel.sub2}::path) y
- | add_atoms pos path (Const (\<^const_name>\<open>Groups.uminus\<close>, _) $ x) =
+ | add_atoms pos path \<^Const_>\<open>uminus _ for x\<close> =
add_atoms (not pos) (@{thm group_cancel.neg1}::path) x
- | add_atoms _ _ (Const (\<^const_name>\<open>Groups.zero\<close>, _)) = I
+ | add_atoms _ _ \<^Const_>\<open>Groups.zero _\<close> = I
| add_atoms pos path x = cons ((pos, x), path)
fun atoms t = add_atoms true [] t []
--- a/src/HOL/Tools/nat_arith.ML Sun Aug 18 15:29:03 2024 +0200
+++ b/src/HOL/Tools/nat_arith.ML Sun Aug 18 15:29:18 2024 +0200
@@ -21,12 +21,12 @@
[Conv.rewr_conv (Library.foldl (op RS) (@{thm nat_arith.rule0}, path)),
Conv.arg_conv (Raw_Simplifier.rewrite ctxt false norm_rules)]
-fun add_atoms path (Const (\<^const_name>\<open>Groups.plus\<close>, _) $ x $ y) =
+fun add_atoms path \<^Const_>\<open>plus _ for x y\<close> =
add_atoms (@{thm nat_arith.add1}::path) x #>
add_atoms (@{thm nat_arith.add2}::path) y
- | add_atoms path (Const (\<^const_name>\<open>Nat.Suc\<close>, _) $ x) =
+ | add_atoms path \<^Const_>\<open>Suc for x\<close> =
add_atoms (@{thm nat_arith.suc1}::path) x
- | add_atoms _ (Const (\<^const_name>\<open>Groups.zero\<close>, _)) = I
+ | add_atoms _ \<^Const_>\<open>Groups.zero _\<close> = I
| add_atoms path x = cons (x, path)
fun atoms t = add_atoms [] t []