--- a/NEWS Sun Oct 16 09:31:05 2016 +0200
+++ b/NEWS Sun Oct 16 09:31:05 2016 +0200
@@ -272,6 +272,8 @@
minus_mod_eq_div2 ~> minus_mod_eq_mult_div
div_mod_equality' ~> minus_mod_eq_div_mult [symmetric]
mod_div_equality' ~> minus_div_mult_eq_mod [symmetric]
+ div_1 ~> div_by_Suc_0
+ mod_1 ~> mod_by_Suc_0
INCOMPATIBILITY.
* Dedicated syntax LENGTH('a) for length of types.
--- a/src/HOL/Decision_Procs/cooper_tac.ML Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Sun Oct 16 09:31:05 2016 +0200
@@ -50,7 +50,7 @@
div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
mod_self
div_by_0 mod_by_0 div_0 mod_0
- div_by_1 mod_by_1 div_1 mod_1
+ div_by_1 mod_by_1 div_by_Suc_0 mod_by_Suc_0
Suc_eq_plus1}
addsimps @{thms ac_simps}
addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
--- a/src/HOL/Decision_Procs/mir_tac.ML Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Sun Oct 16 09:31:05 2016 +0200
@@ -74,7 +74,7 @@
addsimps [refl, mod_add_eq,
@{thm mod_self},
@{thm div_0}, @{thm mod_0},
- @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
+ @{thm div_by_1}, @{thm mod_by_1}, @{thm div_by_Suc_0}, @{thm mod_by_Suc_0},
@{thm "Suc_eq_plus1"}]
addsimps @{thms add.assoc add.commute add.left_commute}
addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
--- a/src/HOL/Divides.thy Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Divides.thy Sun Oct 16 09:31:05 2016 +0200
@@ -1117,7 +1117,7 @@
lemma mod_if: "m mod (n::nat) = (if m < n then m else (m - n) mod n)"
by (simp add: le_mod_geq)
-lemma mod_1 [simp]: "m mod Suc 0 = 0"
+lemma mod_by_Suc_0 [simp]: "m mod Suc 0 = 0"
by (induct m) (simp_all add: mod_geq)
(* a simple rearrangement of div_mult_mod_eq: *)
@@ -1196,7 +1196,7 @@
subsubsection \<open>Further Facts about Quotient and Remainder\<close>
-lemma div_1 [simp]:
+lemma div_by_Suc_0 [simp]:
"m div Suc 0 = m"
using div_by_1 [of m] by simp
--- a/src/HOL/Presburger.thy Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Presburger.thy Sun Oct 16 09:31:05 2016 +0200
@@ -411,7 +411,7 @@
\<close> "Cooper's algorithm for Presburger arithmetic"
declare dvd_eq_mod_eq_0 [symmetric, presburger]
-declare mod_1 [presburger]
+declare mod_by_Suc_0 [presburger]
declare mod_0 [presburger]
declare mod_by_1 [presburger]
declare mod_self [presburger]
--- a/src/HOL/Tools/Qelim/cooper.ML Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Sun Oct 16 09:31:05 2016 +0200
@@ -829,8 +829,8 @@
@{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"},
@{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
@ [@{thm "mod_self"}, @{thm "mod_by_0"}, @{thm "div_by_0"},
- @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"},
- @{thm "mod_1"}, @{thm "Suc_eq_plus1"}]
+ @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"},
+ @{thm "div_by_Suc_0"}, @{thm "mod_by_Suc_0"}, @{thm "Suc_eq_plus1"}]
@ @{thms ac_simps}
addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}])
val splits_ss =
--- a/src/HOL/Tools/nat_numeral_simprocs.ML Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Sun Oct 16 09:31:05 2016 +0200
@@ -350,7 +350,7 @@
(** Final simplification for the CancelFactor simprocs **)
val simplify_one = Arith_Data.simplify_meta_eq
- [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}];
+ [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_Suc_0}, @{thm numeral_1_eq_Suc_0}];
fun cancel_simplify_meta_eq ctxt cancel_th th =
simplify_one ctxt (([th, cancel_th]) MRS trans);