--- a/src/HOL/Groups.thy Thu Aug 08 11:40:42 2019 +0200
+++ b/src/HOL/Groups.thy Thu Aug 08 12:11:40 2019 +0200
@@ -993,6 +993,29 @@
end
+locale group_cancel
+begin
+
+lemma add1: "(A::'a::comm_monoid_add) \<equiv> k + a \<Longrightarrow> A + b \<equiv> k + (a + b)"
+ by (simp only: ac_simps)
+
+lemma add2: "(B::'a::comm_monoid_add) \<equiv> k + b \<Longrightarrow> a + B \<equiv> k + (a + b)"
+ by (simp only: ac_simps)
+
+lemma sub1: "(A::'a::ab_group_add) \<equiv> k + a \<Longrightarrow> A - b \<equiv> k + (a - b)"
+ by (simp only: add_diff_eq)
+
+lemma sub2: "(B::'a::ab_group_add) \<equiv> k + b \<Longrightarrow> a - B \<equiv> - k + (a - b)"
+ by (simp only: minus_add diff_conv_add_uminus ac_simps)
+
+lemma neg1: "(A::'a::ab_group_add) \<equiv> k + a \<Longrightarrow> - A \<equiv> - k + - a"
+ by (simp only: minus_add_distrib)
+
+lemma rule0: "(a::'a::comm_monoid_add) \<equiv> a + 0"
+ by (simp only: add_0_right)
+
+end
+
ML_file \<open>Tools/group_cancel.ML\<close>
simproc_setup group_cancel_add ("a + b::'a::ab_group_add") =
--- a/src/HOL/Lattices.thy Thu Aug 08 11:40:42 2019 +0200
+++ b/src/HOL/Lattices.thy Thu Aug 08 12:11:40 2019 +0200
@@ -693,6 +693,29 @@
end
+locale boolean_algebra_cancel
+begin
+
+lemma sup1: "(A::'a::semilattice_sup) \<equiv> sup k a \<Longrightarrow> sup A b \<equiv> sup k (sup a b)"
+ by (simp only: ac_simps)
+
+lemma sup2: "(B::'a::semilattice_sup) \<equiv> sup k b \<Longrightarrow> sup a B \<equiv> sup k (sup a b)"
+ by (simp only: ac_simps)
+
+lemma sup0: "(a::'a::bounded_semilattice_sup_bot) \<equiv> sup a bot"
+ by simp
+
+lemma inf1: "(A::'a::semilattice_inf) \<equiv> inf k a \<Longrightarrow> inf A b \<equiv> inf k (inf a b)"
+ by (simp only: ac_simps)
+
+lemma inf2: "(B::'a::semilattice_inf) \<equiv> inf k b \<Longrightarrow> inf a B \<equiv> inf k (inf a b)"
+ by (simp only: ac_simps)
+
+lemma inf0: "(a::'a::bounded_semilattice_inf_top) \<equiv> inf a top"
+ by simp
+
+end
+
ML_file \<open>Tools/boolean_algebra_cancel.ML\<close>
simproc_setup boolean_algebra_cancel_sup ("sup a b::'a::boolean_algebra") =
--- a/src/HOL/Nat.thy Thu Aug 08 11:40:42 2019 +0200
+++ b/src/HOL/Nat.thy Thu Aug 08 12:11:40 2019 +0200
@@ -1887,6 +1887,23 @@
shows "u = s"
using assms(2,1) by (rule trans)
+locale nat_arith
+begin
+
+lemma add1: "(A::'a::comm_monoid_add) \<equiv> k + a \<Longrightarrow> A + b \<equiv> k + (a + b)"
+ by (simp only: ac_simps)
+
+lemma add2: "(B::'a::comm_monoid_add) \<equiv> k + b \<Longrightarrow> a + B \<equiv> k + (a + b)"
+ by (simp only: ac_simps)
+
+lemma suc1: "A == k + a \<Longrightarrow> Suc A \<equiv> k + Suc a"
+ by (simp only: add_Suc_right)
+
+lemma rule0: "(a::'a::comm_monoid_add) \<equiv> a + 0"
+ by (simp only: add_0_right)
+
+end
+
ML_file \<open>Tools/nat_arith.ML\<close>
simproc_setup nateq_cancel_sums
--- a/src/HOL/Tools/boolean_algebra_cancel.ML Thu Aug 08 11:40:42 2019 +0200
+++ b/src/HOL/Tools/boolean_algebra_cancel.ML Thu Aug 08 12:11:40 2019 +0200
@@ -13,27 +13,18 @@
structure Boolean_Algebra_Cancel: BOOLEAN_ALGEBRA_CANCEL =
struct
-val sup1 = @{lemma "(A::'a::semilattice_sup) == sup k a ==> sup A b == sup k (sup a b)"
- by (simp only: ac_simps)}
-val sup2 = @{lemma "(B::'a::semilattice_sup) == sup k b ==> sup a B == sup k (sup a b)"
- by (simp only: ac_simps)}
-val sup0 = @{lemma "(a::'a::bounded_semilattice_sup_bot) == sup a bot" by (simp)}
-
-val inf1 = @{lemma "(A::'a::semilattice_inf) == inf k a ==> inf A b == inf k (inf a b)"
- by (simp only: ac_simps)}
-val inf2 = @{lemma "(B::'a::semilattice_inf) == inf k b ==> inf a B == inf k (inf a b)"
- by (simp only: ac_simps)}
-val inf0 = @{lemma "(a::'a::bounded_semilattice_inf_top) == inf a top" by (simp)}
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) =
if sup then
- add_atoms sup pos (sup1::path) x #> add_atoms sup pos (sup2::path) y
+ 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) =
if not sup then
- add_atoms sup pos (inf1::path) x #> add_atoms sup pos (inf2::path) y
+ 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
@@ -59,7 +50,8 @@
fun cancel_conv sup rule ct =
let
- val rule0 = if sup then sup0 else inf0
+ val rule0 =
+ if sup then @{thm boolean_algebra_cancel.sup0} else @{thm boolean_algebra_cancel.inf0}
fun cancel1_conv (pos, lpath, rpath) =
let
val lconv = move_to_front rule0 lpath
--- a/src/HOL/Tools/group_cancel.ML Thu Aug 08 11:40:42 2019 +0200
+++ b/src/HOL/Tools/group_cancel.ML Thu Aug 08 12:11:40 2019 +0200
@@ -18,30 +18,20 @@
structure Group_Cancel: GROUP_CANCEL =
struct
-val add1 = @{lemma "(A::'a::comm_monoid_add) == k + a ==> A + b == k + (a + b)"
- by (simp only: ac_simps)}
-val add2 = @{lemma "(B::'a::comm_monoid_add) == k + b ==> a + B == k + (a + b)"
- by (simp only: ac_simps)}
-val sub1 = @{lemma "(A::'a::ab_group_add) == k + a ==> A - b == k + (a - b)"
- by (simp only: add_diff_eq)}
-val sub2 = @{lemma "(B::'a::ab_group_add) == k + b ==> a - B == - k + (a - b)"
- by (simp only: minus_add diff_conv_add_uminus ac_simps)}
-val neg1 = @{lemma "(A::'a::ab_group_add) == k + a ==> - A == - k + - a"
- by (simp only: minus_add_distrib)}
-val rule0 = @{lemma "(a::'a::comm_monoid_add) == a + 0"
- by (simp only: add_0_right)}
val minus_minus = mk_meta_eq @{thm minus_minus}
fun move_to_front path = Conv.every_conv
- [Conv.rewr_conv (Library.foldl (op RS) (rule0, path)),
+ [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) =
- add_atoms pos (add1::path) x #> add_atoms pos (add2::path) y
+ 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 (sub1::path) x #> add_atoms (not pos) (sub2::path) y
+ 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 (not pos) (neg1::path) x
+ add_atoms (not pos) (@{thm group_cancel.neg1}::path) x
| add_atoms _ _ (Const (\<^const_name>\<open>Groups.zero\<close>, _)) = I
| add_atoms pos path x = cons ((pos, x), path)
--- a/src/HOL/Tools/nat_arith.ML Thu Aug 08 11:40:42 2019 +0200
+++ b/src/HOL/Tools/nat_arith.ML Thu Aug 08 12:11:40 2019 +0200
@@ -15,25 +15,17 @@
structure Nat_Arith: NAT_ARITH =
struct
-val add1 = @{lemma "(A::'a::comm_monoid_add) == k + a ==> A + b == k + (a + b)"
- by (simp only: ac_simps)}
-val add2 = @{lemma "(B::'a::comm_monoid_add) == k + b ==> a + B == k + (a + b)"
- by (simp only: ac_simps)}
-val suc1 = @{lemma "A == k + a ==> Suc A == k + Suc a"
- by (simp only: add_Suc_right)}
-val rule0 = @{lemma "(a::'a::comm_monoid_add) == a + 0"
- by (simp only: add_0_right)}
-
val norm_rules = map mk_meta_eq @{thms add_0_left add_0_right}
fun move_to_front ctxt path = Conv.every_conv
- [Conv.rewr_conv (Library.foldl (op RS) (rule0, path)),
+ [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) =
- add_atoms (add1::path) x #> add_atoms (add2::path) y
+ 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 (suc1::path) x
+ add_atoms (@{thm nat_arith.suc1}::path) x
| add_atoms _ (Const (\<^const_name>\<open>Groups.zero\<close>, _)) = I
| add_atoms path x = cons (x, path)