clarified theorem names
authorhaftmann
Sun Oct 16 09:31:05 2016 +0200 (2016-10-16)
changeset 64244e7102c40783c
parent 64243 aee949f6642d
child 64245 3d00821444fc
clarified theorem names
NEWS
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/Divides.thy
src/HOL/Presburger.thy
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/nat_numeral_simprocs.ML
     1.1 --- a/NEWS	Sun Oct 16 09:31:05 2016 +0200
     1.2 +++ b/NEWS	Sun Oct 16 09:31:05 2016 +0200
     1.3 @@ -272,6 +272,8 @@
     1.4      minus_mod_eq_div2 ~> minus_mod_eq_mult_div
     1.5      div_mod_equality' ~> minus_mod_eq_div_mult [symmetric]
     1.6      mod_div_equality' ~> minus_div_mult_eq_mod [symmetric]
     1.7 +    div_1 ~> div_by_Suc_0
     1.8 +    mod_1 ~> mod_by_Suc_0
     1.9  INCOMPATIBILITY.
    1.10  
    1.11  * Dedicated syntax LENGTH('a) for length of types.
     2.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Sun Oct 16 09:31:05 2016 +0200
     2.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sun Oct 16 09:31:05 2016 +0200
     2.3 @@ -50,7 +50,7 @@
     2.4            div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
     2.5            mod_self
     2.6            div_by_0 mod_by_0 div_0 mod_0
     2.7 -          div_by_1 mod_by_1 div_1 mod_1
     2.8 +          div_by_1 mod_by_1 div_by_Suc_0 mod_by_Suc_0
     2.9            Suc_eq_plus1}
    2.10        addsimps @{thms ac_simps}
    2.11        addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
     3.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Sun Oct 16 09:31:05 2016 +0200
     3.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Sun Oct 16 09:31:05 2016 +0200
     3.3 @@ -74,7 +74,7 @@
     3.4                          addsimps [refl, mod_add_eq, 
     3.5                                    @{thm mod_self},
     3.6                                    @{thm div_0}, @{thm mod_0},
     3.7 -                                  @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
     3.8 +                                  @{thm div_by_1}, @{thm mod_by_1}, @{thm div_by_Suc_0}, @{thm mod_by_Suc_0},
     3.9                                    @{thm "Suc_eq_plus1"}]
    3.10                          addsimps @{thms add.assoc add.commute add.left_commute}
    3.11                          addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
     4.1 --- a/src/HOL/Divides.thy	Sun Oct 16 09:31:05 2016 +0200
     4.2 +++ b/src/HOL/Divides.thy	Sun Oct 16 09:31:05 2016 +0200
     4.3 @@ -1117,7 +1117,7 @@
     4.4  lemma mod_if: "m mod (n::nat) = (if m < n then m else (m - n) mod n)"
     4.5  by (simp add: le_mod_geq)
     4.6  
     4.7 -lemma mod_1 [simp]: "m mod Suc 0 = 0"
     4.8 +lemma mod_by_Suc_0 [simp]: "m mod Suc 0 = 0"
     4.9  by (induct m) (simp_all add: mod_geq)
    4.10  
    4.11  (* a simple rearrangement of div_mult_mod_eq: *)
    4.12 @@ -1196,7 +1196,7 @@
    4.13  
    4.14  subsubsection \<open>Further Facts about Quotient and Remainder\<close>
    4.15  
    4.16 -lemma div_1 [simp]:
    4.17 +lemma div_by_Suc_0 [simp]:
    4.18    "m div Suc 0 = m"
    4.19    using div_by_1 [of m] by simp
    4.20  
     5.1 --- a/src/HOL/Presburger.thy	Sun Oct 16 09:31:05 2016 +0200
     5.2 +++ b/src/HOL/Presburger.thy	Sun Oct 16 09:31:05 2016 +0200
     5.3 @@ -411,7 +411,7 @@
     5.4  \<close> "Cooper's algorithm for Presburger arithmetic"
     5.5  
     5.6  declare dvd_eq_mod_eq_0 [symmetric, presburger]
     5.7 -declare mod_1 [presburger] 
     5.8 +declare mod_by_Suc_0 [presburger] 
     5.9  declare mod_0 [presburger]
    5.10  declare mod_by_1 [presburger]
    5.11  declare mod_self [presburger]
     6.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sun Oct 16 09:31:05 2016 +0200
     6.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sun Oct 16 09:31:05 2016 +0200
     6.3 @@ -829,8 +829,8 @@
     6.4         @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 
     6.5         @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
     6.6      @ [@{thm "mod_self"}, @{thm "mod_by_0"}, @{thm "div_by_0"},
     6.7 -       @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, 
     6.8 -       @{thm "mod_1"}, @{thm "Suc_eq_plus1"}]
     6.9 +       @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"},
    6.10 +       @{thm "div_by_Suc_0"}, @{thm "mod_by_Suc_0"}, @{thm "Suc_eq_plus1"}]
    6.11      @ @{thms ac_simps}
    6.12     addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}])
    6.13  val splits_ss =
     7.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Sun Oct 16 09:31:05 2016 +0200
     7.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Sun Oct 16 09:31:05 2016 +0200
     7.3 @@ -350,7 +350,7 @@
     7.4  
     7.5  (** Final simplification for the CancelFactor simprocs **)
     7.6  val simplify_one = Arith_Data.simplify_meta_eq  
     7.7 -  [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}];
     7.8 +  [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_Suc_0}, @{thm numeral_1_eq_Suc_0}];
     7.9  
    7.10  fun cancel_simplify_meta_eq ctxt cancel_th th =
    7.11      simplify_one ctxt (([th, cancel_th]) MRS trans);