1.1 --- a/NEWS	Tue Mar 27 12:42:54 2012 +0200
     1.2 +++ b/NEWS	Tue Mar 27 14:49:56 2012 +0200
     1.3 @@ -136,6 +136,16 @@
     1.4  
     1.5  * New type synonym 'a rel = ('a * 'a) set
     1.6  
     1.7 +* Theory Divides: Discontinued redundant theorems about div and mod.
     1.8 +INCOMPATIBILITY, use the corresponding generic theorems instead.
     1.9 +
    1.10 +  DIVISION_BY_ZERO ~> div_by_0, mod_by_0
    1.11 +  zdiv_self ~> div_self
    1.12 +  zmod_self ~> mod_self
    1.13 +  zdiv_zero ~> div_0
    1.14 +  zmod_zero ~> mod_0
    1.15 +  zmod_zdiv_trivial ~> mod_div_trivial
    1.16 +
    1.17  * More default pred/set conversions on a couple of relation operations
    1.18  and predicates.  Consolidation of some relation theorems:
    1.19  

     2.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Tue Mar 27 12:42:54 2012 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Tue Mar 27 14:49:56 2012 +0200
     2.3 @@ -1392,7 +1392,7 @@
     2.4      have "c div c\<le> l div c"
     2.5        by (simp add: zdiv_mono1[OF clel cp])
     2.6      then have ldcp:"0 < l div c" 
     2.7 -      by (simp add: zdiv_self[OF cnz])
     2.8 +      by (simp add: div_self[OF cnz])
     2.9      have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    2.10      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
    2.11        by simp
    2.12 @@ -1410,7 +1410,7 @@
    2.13      have "c div c\<le> l div c"
    2.14        by (simp add: zdiv_mono1[OF clel cp])
    2.15      then have ldcp:"0 < l div c" 
    2.16 -      by (simp add: zdiv_self[OF cnz])
    2.17 +      by (simp add: div_self[OF cnz])
    2.18      have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    2.19      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
    2.20        by simp
    2.21 @@ -1428,7 +1428,7 @@
    2.22      have "c div c\<le> l div c"
    2.23        by (simp add: zdiv_mono1[OF clel cp])
    2.24      then have ldcp:"0 < l div c" 
    2.25 -      by (simp add: zdiv_self[OF cnz])
    2.26 +      by (simp add: div_self[OF cnz])
    2.27      have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    2.28      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
    2.29        by simp
    2.30 @@ -1446,7 +1446,7 @@
    2.31      have "c div c\<le> l div c"
    2.32        by (simp add: zdiv_mono1[OF clel cp])
    2.33      then have ldcp:"0 < l div c" 
    2.34 -      by (simp add: zdiv_self[OF cnz])
    2.35 +      by (simp add: div_self[OF cnz])
    2.36      have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    2.37      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
    2.38        by simp
    2.39 @@ -1466,7 +1466,7 @@
    2.40      have "c div c\<le> l div c"
    2.41        by (simp add: zdiv_mono1[OF clel cp])
    2.42      then have ldcp:"0 < l div c" 
    2.43 -      by (simp add: zdiv_self[OF cnz])
    2.44 +      by (simp add: div_self[OF cnz])
    2.45      have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    2.46      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
    2.47        by simp
    2.48 @@ -1484,7 +1484,7 @@
    2.49      have "c div c\<le> l div c"
    2.50        by (simp add: zdiv_mono1[OF clel cp])
    2.51      then have ldcp:"0 < l div c" 
    2.52 -      by (simp add: zdiv_self[OF cnz])
    2.53 +      by (simp add: div_self[OF cnz])
    2.54      have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    2.55      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
    2.56        by simp
    2.57 @@ -1502,7 +1502,7 @@
    2.58      have "c div c\<le> l div c"
    2.59        by (simp add: zdiv_mono1[OF clel cp])
    2.60      then have ldcp:"0 < l div c" 
    2.61 -      by (simp add: zdiv_self[OF cnz])
    2.62 +      by (simp add: div_self[OF cnz])
    2.63      have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    2.64      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
    2.65        by simp
    2.66 @@ -1519,7 +1519,7 @@
    2.67      have "c div c\<le> l div c"
    2.68        by (simp add: zdiv_mono1[OF clel cp])
    2.69      then have ldcp:"0 < l div c" 
    2.70 -      by (simp add: zdiv_self[OF cnz])
    2.71 +      by (simp add: div_self[OF cnz])
    2.72      have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    2.73      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
    2.74        by simp

     3.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Tue Mar 27 12:42:54 2012 +0200
     3.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Tue Mar 27 14:49:56 2012 +0200
     3.3 @@ -726,7 +726,7 @@
     3.4          have gpdd: "?g' dvd n" by simp
     3.5          have gpdgp: "?g' dvd ?g'" by simp
     3.6          from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" .
     3.7 -        from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]]
     3.8 +        from zdiv_mono1[OF g'n g'p, simplified div_self[OF gp0]]
     3.9          have "n div ?g' >0" by simp
    3.10          hence ?thesis using assms g1 g'1
    3.11            by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0 simpnum_numbound0) }

     4.1 --- a/src/HOL/Decision_Procs/MIR.thy	Tue Mar 27 12:42:54 2012 +0200
     4.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Tue Mar 27 14:49:56 2012 +0200
     4.3 @@ -1000,7 +1000,7 @@
     4.4          have gpdd: "?g' dvd n" by simp
     4.5          have gpdgp: "?g' dvd ?g'" by simp
     4.6          from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" .
     4.7 -        from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]]
     4.8 +        from zdiv_mono1[OF g'n g'p, simplified div_self[OF gp0]]
     4.9          have "n div ?g' >0" by simp
    4.10          hence ?thesis using assms g1 g'1
    4.11            by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0)}
    4.12 @@ -1138,7 +1138,7 @@
    4.13        have "Ifm bs (Dvd (fst (simpdvd d t)) (snd(simpdvd d t))) = Ifm bs (Dvd (d div ?g') ?tt)"
    4.14          by (simp add: simpdvd_def Let_def)
    4.15        also have "\<dots> = (real d rdvd (Inum bs t))"
    4.16 -        using rdvd_reduce[OF gpdd gpdgp g'p, where t="?t", simplified zdiv_self[OF gp0]] 
    4.17 +        using rdvd_reduce[OF gpdd gpdgp g'p, where t="?t", simplified div_self[OF gp0]] 
    4.18            th2[symmetric] by simp
    4.19        finally have ?thesis by simp  }
    4.20      ultimately have ?thesis by blast
    4.21 @@ -2420,7 +2420,7 @@
    4.22      have "c div c\<le> l div c"
    4.23        by (simp add: zdiv_mono1[OF clel cp])
    4.24      then have ldcp:"0 < l div c" 
    4.25 -      by (simp add: zdiv_self[OF cnz])
    4.26 +      by (simp add: div_self[OF cnz])
    4.27      have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    4.28      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
    4.29        by simp
    4.30 @@ -2438,7 +2438,7 @@
    4.31      have "c div c\<le> l div c"
    4.32        by (simp add: zdiv_mono1[OF clel cp])
    4.33      then have ldcp:"0 < l div c" 
    4.34 -      by (simp add: zdiv_self[OF cnz])
    4.35 +      by (simp add: div_self[OF cnz])
    4.36      have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    4.37      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
    4.38        by simp
    4.39 @@ -2456,7 +2456,7 @@
    4.40      have "c div c\<le> l div c"
    4.41        by (simp add: zdiv_mono1[OF clel cp])
    4.42      then have ldcp:"0 < l div c" 
    4.43 -      by (simp add: zdiv_self[OF cnz])
    4.44 +      by (simp add: div_self[OF cnz])
    4.45      have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    4.46      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
    4.47        by simp
    4.48 @@ -2474,7 +2474,7 @@
    4.49      have "c div c\<le> l div c"
    4.50        by (simp add: zdiv_mono1[OF clel cp])
    4.51      then have ldcp:"0 < l div c" 
    4.52 -      by (simp add: zdiv_self[OF cnz])
    4.53 +      by (simp add: div_self[OF cnz])
    4.54      have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    4.55      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
    4.56        by simp
    4.57 @@ -2492,7 +2492,7 @@
    4.58      have "c div c\<le> l div c"
    4.59        by (simp add: zdiv_mono1[OF clel cp])
    4.60      then have ldcp:"0 < l div c" 
    4.61 -      by (simp add: zdiv_self[OF cnz])
    4.62 +      by (simp add: div_self[OF cnz])
    4.63      have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    4.64      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
    4.65        by simp
    4.66 @@ -2510,7 +2510,7 @@
    4.67      have "c div c\<le> l div c"
    4.68        by (simp add: zdiv_mono1[OF clel cp])
    4.69      then have ldcp:"0 < l div c" 
    4.70 -      by (simp add: zdiv_self[OF cnz])
    4.71 +      by (simp add: div_self[OF cnz])
    4.72      have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    4.73      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
    4.74        by simp
    4.75 @@ -2528,7 +2528,7 @@
    4.76      have "c div c\<le> l div c"
    4.77        by (simp add: zdiv_mono1[OF clel cp])
    4.78      then have ldcp:"0 < l div c" 
    4.79 -      by (simp add: zdiv_self[OF cnz])
    4.80 +      by (simp add: div_self[OF cnz])
    4.81      have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    4.82      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
    4.83        by simp
    4.84 @@ -2545,7 +2545,7 @@
    4.85      have "c div c\<le> l div c"
    4.86        by (simp add: zdiv_mono1[OF clel cp])
    4.87      then have ldcp:"0 < l div c" 
    4.88 -      by (simp add: zdiv_self[OF cnz])
    4.89 +      by (simp add: div_self[OF cnz])
    4.90      have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
    4.91      hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
    4.92        by simp
    4.93 @@ -3970,7 +3970,7 @@
    4.94          by (simp add: numgcd_def)
    4.95        from `c > 0` have th': "c\<noteq>0" by auto
    4.96        from `c > 0` have cp: "c \<ge> 0" by simp
    4.97 -      from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
    4.98 +      from zdiv_mono2[OF cp th1 th, simplified div_self[OF th']]
    4.99        have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
   4.100      }
   4.101      with Lt a have ?case
   4.102 @@ -3994,7 +3994,7 @@
   4.103          by (simp add: numgcd_def)
   4.104        from `c > 0` have th': "c\<noteq>0" by auto
   4.105        from `c > 0` have cp: "c \<ge> 0" by simp
   4.106 -      from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
   4.107 +      from zdiv_mono2[OF cp th1 th, simplified div_self[OF th']]
   4.108        have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
   4.109      }
   4.110      with Le a have ?case
   4.111 @@ -4018,7 +4018,7 @@
   4.112          by (simp add: numgcd_def)
   4.113        from `c > 0` have th': "c\<noteq>0" by auto
   4.114        from `c > 0` have cp: "c \<ge> 0" by simp
   4.115 -      from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
   4.116 +      from zdiv_mono2[OF cp th1 th, simplified div_self[OF th']]
   4.117        have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
   4.118      }
   4.119      with Gt a have ?case
   4.120 @@ -4042,7 +4042,7 @@
   4.121          by (simp add: numgcd_def)
   4.122        from `c > 0` have th': "c\<noteq>0" by auto
   4.123        from `c > 0` have cp: "c \<ge> 0" by simp
   4.124 -      from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
   4.125 +      from zdiv_mono2[OF cp th1 th, simplified div_self[OF th']]
   4.126        have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
   4.127      }
   4.128      with Ge a have ?case
   4.129 @@ -4066,7 +4066,7 @@
   4.130          by (simp add: numgcd_def)
   4.131        from `c > 0` have th': "c\<noteq>0" by auto
   4.132        from `c > 0` have cp: "c \<ge> 0" by simp
   4.133 -      from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
   4.134 +      from zdiv_mono2[OF cp th1 th, simplified div_self[OF th']]
   4.135        have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
   4.136      }
   4.137      with Eq a have ?case
   4.138 @@ -4090,7 +4090,7 @@
   4.139          by (simp add: numgcd_def)
   4.140        from `c > 0` have th': "c\<noteq>0" by auto
   4.141        from `c > 0` have cp: "c \<ge> 0" by simp
   4.142 -      from zdiv_mono2[OF cp th1 th, simplified zdiv_self[OF th']]
   4.143 +      from zdiv_mono2[OF cp th1 th, simplified div_self[OF th']]
   4.144        have "0 < c div numgcd (CN 0 c (simpnum e))" by simp
   4.145      }
   4.146      with NEq a have ?case

     5.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Tue Mar 27 12:42:54 2012 +0200
     5.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Tue Mar 27 14:49:56 2012 +0200
     5.3 @@ -73,10 +73,9 @@
     5.4        addsimps [refl,mod_add_eq, mod_add_left_eq,
     5.5            mod_add_right_eq,
     5.6            nat_div_add_eq, int_div_add_eq,
     5.7 -          @{thm mod_self}, @{thm "zmod_self"},
     5.8 -          @{thm mod_by_0}, @{thm div_by_0},
     5.9 -          @{thm "zdiv_zero"}, @{thm "zmod_zero"}, @{thm "div_0"}, @{thm "mod_0"},
    5.10 -          @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
    5.11 +          @{thm mod_self},
    5.12 +          @{thm div_by_0}, @{thm mod_by_0}, @{thm div_0}, @{thm mod_0},
    5.13 +          @{thm div_by_1}, @{thm mod_by_1}, @{thm div_1}, @{thm mod_1},
    5.14            Suc_eq_plus1]
    5.15        addsimps @{thms add_ac}
    5.16        addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]

     6.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Tue Mar 27 12:42:54 2012 +0200
     6.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Tue Mar 27 14:49:56 2012 +0200
     6.3 @@ -38,8 +38,6 @@
     6.4  val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
     6.5  val nat_div_add_eq = @{thm div_add1_eq} RS sym;
     6.6  val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
     6.7 -val ZDIVISION_BY_ZERO_MOD = @{thm DIVISION_BY_ZERO} RS conjunct2;
     6.8 -val ZDIVISION_BY_ZERO_DIV = @{thm DIVISION_BY_ZERO} RS conjunct1;
     6.9  
    6.10  fun prepare_for_linr sg q fm = 
    6.11    let

     7.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Tue Mar 27 12:42:54 2012 +0200
     7.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Tue Mar 27 14:49:56 2012 +0200
     7.3 @@ -54,8 +54,6 @@
     7.4  val mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym;
     7.5  val nat_div_add_eq = @{thm "div_add1_eq"} RS sym;
     7.6  val int_div_add_eq = @{thm "zdiv_zadd1_eq"} RS sym;
     7.7 -val ZDIVISION_BY_ZERO_MOD = @{thm "DIVISION_BY_ZERO"} RS conjunct2;
     7.8 -val ZDIVISION_BY_ZERO_DIV = @{thm "DIVISION_BY_ZERO"} RS conjunct1;
     7.9  
    7.10  fun prepare_for_mir thy q fm = 
    7.11    let
    7.12 @@ -96,8 +94,8 @@
    7.13      (* Some simpsets for dealing with mod div abs and nat*)
    7.14      val mod_div_simpset = HOL_basic_ss 
    7.15                          addsimps [refl, mod_add_eq, 
    7.16 -                                  @{thm "mod_self"}, @{thm "zmod_self"},
    7.17 -                                  @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},
    7.18 +                                  @{thm mod_self},
    7.19 +                                  @{thm div_0}, @{thm mod_0},
    7.20                                    @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
    7.21                                    @{thm "Suc_eq_plus1"}]
    7.22                          addsimps @{thms add_ac}

     8.1 --- a/src/HOL/Divides.thy	Tue Mar 27 12:42:54 2012 +0200
     8.2 +++ b/src/HOL/Divides.thy	Tue Mar 27 14:49:56 2012 +0200
     8.3 @@ -1403,12 +1403,6 @@
     8.4      by (rule div_int_unique, auto simp add: divmod_int_rel_def)
     8.5  qed
     8.6  
     8.7 -text{*Arbitrary definitions for division by zero.  Useful to simplify 
     8.8 -    certain equations.*}
     8.9 -
    8.10 -lemma DIVISION_BY_ZERO [simp]: "a div (0::int) = 0 & a mod (0::int) = a"
    8.11 -  by simp (* FIXME: delete *)
    8.12 -
    8.13  text{*Basic laws about division and remainder*}
    8.14  
    8.15  lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
    8.16 @@ -1552,51 +1546,11 @@
    8.17    unfolding zmod_zminus2_eq_if by auto 
    8.18  
    8.19  
    8.20 -subsubsection {* Division of a Number by Itself *}
    8.21 -
    8.22 -lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 \<le> q"
    8.23 -apply (subgoal_tac "0 < a*q")
    8.24 - apply (simp add: zero_less_mult_iff, arith)
    8.25 -done
    8.26 -
    8.27 -lemma self_quotient_aux2: "[| (0::int) < a; a = r + a*q; 0 \<le> r |] ==> q \<le> 1"
    8.28 -apply (subgoal_tac "0 \<le> a* (1-q) ")
    8.29 - apply (simp add: zero_le_mult_iff)
    8.30 -apply (simp add: right_diff_distrib)
    8.31 -done
    8.32 -
    8.33 -lemma self_quotient: "[| divmod_int_rel a a (q, r); a \<noteq> 0 |] ==> q = 1"
    8.34 -apply (simp add: split_ifs divmod_int_rel_def linorder_neq_iff)
    8.35 -apply (rule order_antisym, safe, simp_all)
    8.36 -apply (rule_tac [3] a = "-a" and r = "-r" in self_quotient_aux1)
    8.37 -apply (rule_tac a = "-a" and r = "-r" in self_quotient_aux2)
    8.38 -apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: add_commute)+
    8.39 -done
    8.40 -
    8.41 -lemma self_remainder: "[| divmod_int_rel a a (q, r); a \<noteq> 0 |] ==> r = 0"
    8.42 -apply (frule (1) self_quotient)
    8.43 -apply (simp add: divmod_int_rel_def)
    8.44 -done
    8.45 -
    8.46 -lemma zdiv_self [simp]: "a \<noteq> 0 ==> a div a = (1::int)"
    8.47 -  by (fact div_self) (* FIXME: delete *)
    8.48 -
    8.49 -(*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *)
    8.50 -lemma zmod_self [simp]: "a mod a = (0::int)"
    8.51 -  by (fact mod_self) (* FIXME: delete *)
    8.52 -
    8.53 -
    8.54  subsubsection {* Computation of Division and Remainder *}
    8.55  
    8.56 -lemma zdiv_zero [simp]: "(0::int) div b = 0"
    8.57 -  by (fact div_0) (* FIXME: delete *)
    8.58 -
    8.59  lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
    8.60  by (simp add: div_int_def divmod_int_def)
    8.61  
    8.62 -lemma zmod_zero [simp]: "(0::int) mod b = 0"
    8.63 -  by (fact mod_0) (* FIXME: delete *)
    8.64 -
    8.65  lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
    8.66  by (simp add: mod_int_def divmod_int_def)
    8.67  
    8.68 @@ -1841,9 +1795,6 @@
    8.69  lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)"
    8.70    by (fact mod_mult_right_eq) (* FIXME: delete *)
    8.71  
    8.72 -lemma zmod_zdiv_trivial: "(a mod b) div b = (0::int)"
    8.73 -  by (fact mod_div_trivial) (* FIXME: delete *)
    8.74 -
    8.75  text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
    8.76  
    8.77  lemma zadd1_lemma:
    8.78 @@ -2235,14 +2186,14 @@
    8.79  
    8.80  lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
    8.81    using zmod_zdiv_equality[where a="m" and b="n"]
    8.82 -  by (simp add: algebra_simps)
    8.83 +  by (simp add: algebra_simps) (* FIXME: generalize *)
    8.84  
    8.85  lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
    8.86  apply (induct "y", auto)
    8.87 -apply (rule zmod_zmult1_eq [THEN trans])
    8.88 +apply (rule mod_mult_right_eq [THEN trans])
    8.89  apply (simp (no_asm_simp))
    8.90  apply (rule mod_mult_eq [symmetric])
    8.91 -done
    8.92 +done (* FIXME: generalize *)
    8.93  
    8.94  lemma zdiv_int: "int (a div b) = (int a) div (int b)"
    8.95  apply (subst split_div, auto)
    8.96 @@ -2290,7 +2241,7 @@
    8.97  lemmas zmod_simps =
    8.98    mod_add_left_eq  [symmetric]
    8.99    mod_add_right_eq [symmetric]
   8.100 -  zmod_zmult1_eq   [symmetric]
   8.101 +  mod_mult_right_eq[symmetric]
   8.102    mod_mult_left_eq [symmetric]
   8.103    zpower_zmod
   8.104    zminus_zmod zdiff_zmod_left zdiff_zmod_right

     9.1 --- a/src/HOL/Groebner_Basis.thy	Tue Mar 27 12:42:54 2012 +0200
     9.2 +++ b/src/HOL/Groebner_Basis.thy	Tue Mar 27 14:49:56 2012 +0200
     9.3 @@ -50,16 +50,16 @@
     9.4  declare dvd_eq_mod_eq_0[symmetric, algebra]
     9.5  declare mod_div_trivial[algebra]
     9.6  declare mod_mod_trivial[algebra]
     9.7 -declare conjunct1[OF DIVISION_BY_ZERO, algebra]
     9.8 -declare conjunct2[OF DIVISION_BY_ZERO, algebra]
     9.9 +declare div_by_0[algebra]
    9.10 +declare mod_by_0[algebra]
    9.11  declare zmod_zdiv_equality[symmetric,algebra]
    9.12  declare zdiv_zmod_equality[symmetric, algebra]
    9.13  declare zdiv_zminus_zminus[algebra]
    9.14  declare zmod_zminus_zminus[algebra]
    9.15  declare zdiv_zminus2[algebra]
    9.16  declare zmod_zminus2[algebra]
    9.17 -declare zdiv_zero[algebra]
    9.18 -declare zmod_zero[algebra]
    9.19 +declare div_0[algebra]
    9.20 +declare mod_0[algebra]
    9.21  declare mod_by_1[algebra]
    9.22  declare div_by_1[algebra]
    9.23  declare zmod_minus1_right[algebra]

    10.1 --- a/src/HOL/Presburger.thy	Tue Mar 27 12:42:54 2012 +0200
    10.2 +++ b/src/HOL/Presburger.thy	Tue Mar 27 14:49:56 2012 +0200
    10.3 @@ -396,8 +396,6 @@
    10.4  declare mod_1[presburger] 
    10.5  declare mod_0[presburger]
    10.6  declare mod_by_1[presburger]
    10.7 -declare zmod_zero[presburger]
    10.8 -declare zmod_self[presburger]
    10.9  declare mod_self[presburger]
   10.10  declare mod_by_0[presburger]
   10.11  declare mod_div_trivial[presburger]

    11.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Tue Mar 27 12:42:54 2012 +0200
    11.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Tue Mar 27 14:49:56 2012 +0200
    11.3 @@ -802,9 +802,7 @@
    11.4      [@{thm "dvd_eq_mod_eq_0"},
    11.5       @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 
    11.6       @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
    11.7 -  @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"}, 
    11.8 -     @{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, 
    11.9 -     @{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, 
   11.10 +  @ [@{thm "mod_self"}, @{thm "mod_by_0"}, @{thm "div_by_0"},
   11.11       @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, 
   11.12       @{thm "mod_1"}, @{thm "Suc_eq_plus1"}]
   11.13    @ @{thms add_ac}