# HG changeset patch
# User haftmann
# Date 1476603065 -7200
# Node ID e7102c40783c65850518f0dcf6a3ab85bc58ec29
# Parent  aee949f6642dffa565ecc74e42330190309e44e4
clarified theorem names

diff -r aee949f6642d -r e7102c40783c NEWS
--- 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.
diff -r aee949f6642d -r e7102c40783c src/HOL/Decision_Procs/cooper_tac.ML
--- 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}]
diff -r aee949f6642d -r e7102c40783c src/HOL/Decision_Procs/mir_tac.ML
--- 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}]
diff -r aee949f6642d -r e7102c40783c src/HOL/Divides.thy
--- 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
 
diff -r aee949f6642d -r e7102c40783c src/HOL/Presburger.thy
--- 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]
diff -r aee949f6642d -r e7102c40783c src/HOL/Tools/Qelim/cooper.ML
--- 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 =
diff -r aee949f6642d -r e7102c40783c src/HOL/Tools/nat_numeral_simprocs.ML
--- 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);