merged
authorbulwahn
Tue Mar 27 15:34:04 2012 +0200 (2012-03-27)
changeset 471449bfc32fc7ced
parent 47143 212f7a975d49
parent 47142 d64fa2ca54b8
child 47145 ffc6d6267a88
merged
     1.1 --- a/NEWS	Tue Mar 27 14:14:46 2012 +0200
     1.2 +++ b/NEWS	Tue Mar 27 15:34:04 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 14:14:46 2012 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Tue Mar 27 15:34:04 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 14:14:46 2012 +0200
     3.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Tue Mar 27 15:34:04 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 14:14:46 2012 +0200
     4.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Tue Mar 27 15:34:04 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 14:14:46 2012 +0200
     5.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Tue Mar 27 15:34:04 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 14:14:46 2012 +0200
     6.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Tue Mar 27 15:34:04 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 14:14:46 2012 +0200
     7.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Tue Mar 27 15:34:04 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 14:14:46 2012 +0200
     8.2 +++ b/src/HOL/Divides.thy	Tue Mar 27 15:34:04 2012 +0200
     8.3 @@ -535,7 +535,7 @@
     8.4    by (auto simp add: divmod_nat_def intro: theI elim: divmod_nat_rel_unique)
     8.5  qed
     8.6  
     8.7 -lemma divmod_nat_eq:
     8.8 +lemma divmod_nat_unique:
     8.9    assumes "divmod_nat_rel m n qr" 
    8.10    shows "divmod_nat m n = qr"
    8.11    using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
    8.12 @@ -561,58 +561,36 @@
    8.13    "divmod_nat m n = (m div n, m mod n)"
    8.14    by (simp add: prod_eq_iff)
    8.15  
    8.16 -lemma div_eq:
    8.17 +lemma div_nat_unique:
    8.18    assumes "divmod_nat_rel m n (q, r)" 
    8.19    shows "m div n = q"
    8.20 -  using assms by (auto dest!: divmod_nat_eq simp add: prod_eq_iff)
    8.21 -
    8.22 -lemma mod_eq:
    8.23 +  using assms by (auto dest!: divmod_nat_unique simp add: prod_eq_iff)
    8.24 +
    8.25 +lemma mod_nat_unique:
    8.26    assumes "divmod_nat_rel m n (q, r)" 
    8.27    shows "m mod n = r"
    8.28 -  using assms by (auto dest!: divmod_nat_eq simp add: prod_eq_iff)
    8.29 +  using assms by (auto dest!: divmod_nat_unique simp add: prod_eq_iff)
    8.30  
    8.31  lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
    8.32    using divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod)
    8.33  
    8.34 -lemma divmod_nat_zero:
    8.35 -  "divmod_nat m 0 = (0, m)"
    8.36 -proof -
    8.37 -  from divmod_nat_rel [of m 0] show ?thesis
    8.38 -    unfolding divmod_nat_div_mod divmod_nat_rel_def by simp
    8.39 -qed
    8.40 -
    8.41 -lemma divmod_nat_base:
    8.42 -  assumes "m < n"
    8.43 -  shows "divmod_nat m n = (0, m)"
    8.44 -proof -
    8.45 -  from divmod_nat_rel [of m n] show ?thesis
    8.46 -    unfolding divmod_nat_div_mod divmod_nat_rel_def
    8.47 -    using assms by (cases "m div n = 0")
    8.48 -      (auto simp add: gr0_conv_Suc [of "m div n"])
    8.49 -qed
    8.50 +lemma divmod_nat_zero: "divmod_nat m 0 = (0, m)"
    8.51 +  by (simp add: divmod_nat_unique divmod_nat_rel_def)
    8.52 +
    8.53 +lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)"
    8.54 +  by (simp add: divmod_nat_unique divmod_nat_rel_def)
    8.55 +
    8.56 +lemma divmod_nat_base: "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
    8.57 +  by (simp add: divmod_nat_unique divmod_nat_rel_def)
    8.58  
    8.59  lemma divmod_nat_step:
    8.60    assumes "0 < n" and "n \<le> m"
    8.61    shows "divmod_nat m n = (Suc ((m - n) div n), (m - n) mod n)"
    8.62 -proof -
    8.63 -  from divmod_nat_rel have divmod_nat_m_n: "divmod_nat_rel m n (m div n, m mod n)" .
    8.64 -  with assms have m_div_n: "m div n \<ge> 1"
    8.65 -    by (cases "m div n") (auto simp add: divmod_nat_rel_def)
    8.66 -  have "divmod_nat_rel (m - n) n (m div n - Suc 0, m mod n)"
    8.67 -  proof -
    8.68 -    from assms have
    8.69 -      "n \<noteq> 0"
    8.70 -      "\<And>k. m = Suc k * n + m mod n ==> m - n = (Suc k - Suc 0) * n + m mod n"
    8.71 -      by simp_all
    8.72 -    then show ?thesis using assms divmod_nat_m_n 
    8.73 -      by (cases "m div n")
    8.74 -         (simp_all only: divmod_nat_rel_def fst_conv snd_conv, simp_all)
    8.75 -  qed
    8.76 -  with divmod_nat_eq have "divmod_nat (m - n) n = (m div n - Suc 0, m mod n)" by simp
    8.77 -  moreover from divmod_nat_div_mod have "divmod_nat (m - n) n = ((m - n) div n, (m - n) mod n)" .
    8.78 -  ultimately have "m div n = Suc ((m - n) div n)"
    8.79 -    and "m mod n = (m - n) mod n" using m_div_n by simp_all
    8.80 -  then show ?thesis using divmod_nat_div_mod by simp
    8.81 +proof (rule divmod_nat_unique)
    8.82 +  have "divmod_nat_rel (m - n) n ((m - n) div n, (m - n) mod n)"
    8.83 +    by (rule divmod_nat_rel)
    8.84 +  thus "divmod_nat_rel m n (Suc ((m - n) div n), (m - n) mod n)"
    8.85 +    unfolding divmod_nat_rel_def using assms by auto
    8.86  qed
    8.87  
    8.88  text {* The ''recursion'' equations for @{const div} and @{const mod} *}
    8.89 @@ -641,40 +619,30 @@
    8.90    shows "m mod n = (m - n) mod n"
    8.91    using assms divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
    8.92  
    8.93 -instance proof -
    8.94 -  have [simp]: "\<And>n::nat. n div 0 = 0"
    8.95 +instance proof
    8.96 +  fix m n :: nat
    8.97 +  show "m div n * n + m mod n = m"
    8.98 +    using divmod_nat_rel [of m n] by (simp add: divmod_nat_rel_def)
    8.99 +next
   8.100 +  fix m n q :: nat
   8.101 +  assume "n \<noteq> 0"
   8.102 +  then show "(q + m * n) div n = m + q div n"
   8.103 +    by (induct m) (simp_all add: le_div_geq)
   8.104 +next
   8.105 +  fix m n q :: nat
   8.106 +  assume "m \<noteq> 0"
   8.107 +  hence "\<And>a b. divmod_nat_rel n q (a, b) \<Longrightarrow> divmod_nat_rel (m * n) (m * q) (a, m * b)"
   8.108 +    unfolding divmod_nat_rel_def
   8.109 +    by (auto split: split_if_asm, simp_all add: algebra_simps)
   8.110 +  moreover from divmod_nat_rel have "divmod_nat_rel n q (n div q, n mod q)" .
   8.111 +  ultimately have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))" .
   8.112 +  thus "(m * n) div (m * q) = n div q" by (rule div_nat_unique)
   8.113 +next
   8.114 +  fix n :: nat show "n div 0 = 0"
   8.115      by (simp add: div_nat_def divmod_nat_zero)
   8.116 -  have [simp]: "\<And>n::nat. 0 div n = 0"
   8.117 -  proof -
   8.118 -    fix n :: nat
   8.119 -    show "0 div n = 0"
   8.120 -      by (cases "n = 0") simp_all
   8.121 -  qed
   8.122 -  show "OFCLASS(nat, semiring_div_class)" proof
   8.123 -    fix m n :: nat
   8.124 -    show "m div n * n + m mod n = m"
   8.125 -      using divmod_nat_rel [of m n] by (simp add: divmod_nat_rel_def)
   8.126 -  next
   8.127 -    fix m n q :: nat
   8.128 -    assume "n \<noteq> 0"
   8.129 -    then show "(q + m * n) div n = m + q div n"
   8.130 -      by (induct m) (simp_all add: le_div_geq)
   8.131 -  next
   8.132 -    fix m n q :: nat
   8.133 -    assume "m \<noteq> 0"
   8.134 -    then show "(m * n) div (m * q) = n div q"
   8.135 -    proof (cases "n \<noteq> 0 \<and> q \<noteq> 0")
   8.136 -      case False then show ?thesis by auto
   8.137 -    next
   8.138 -      case True with `m \<noteq> 0`
   8.139 -        have "m > 0" and "n > 0" and "q > 0" by auto
   8.140 -      then have "\<And>a b. divmod_nat_rel n q (a, b) \<Longrightarrow> divmod_nat_rel (m * n) (m * q) (a, m * b)"
   8.141 -        by (auto simp add: divmod_nat_rel_def) (simp_all add: algebra_simps)
   8.142 -      moreover from divmod_nat_rel have "divmod_nat_rel n q (n div q, n mod q)" .
   8.143 -      ultimately have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))" .
   8.144 -      then show ?thesis by (simp add: div_eq)
   8.145 -    qed
   8.146 -  qed simp_all
   8.147 +next
   8.148 +  fix n :: nat show "0 div n = 0"
   8.149 +    by (simp add: div_nat_def divmod_nat_zero_left)
   8.150  qed
   8.151  
   8.152  end
   8.153 @@ -745,19 +713,14 @@
   8.154  by (induct m) (simp_all add: mod_geq)
   8.155  
   8.156  lemma mod_mult_distrib: "(m mod n) * (k\<Colon>nat) = (m * k) mod (n * k)"
   8.157 -  apply (cases "n = 0", simp)
   8.158 -  apply (cases "k = 0", simp)
   8.159 -  apply (induct m rule: nat_less_induct)
   8.160 -  apply (subst mod_if, simp)
   8.161 -  apply (simp add: mod_geq diff_mult_distrib)
   8.162 -  done
   8.163 +  by (fact mod_mult_mult2 [symmetric]) (* FIXME: generalize *)
   8.164  
   8.165  lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)"
   8.166 -by (simp add: mult_commute [of k] mod_mult_distrib)
   8.167 +  by (fact mod_mult_mult1 [symmetric]) (* FIXME: generalize *)
   8.168  
   8.169  (* a simple rearrangement of mod_div_equality: *)
   8.170  lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
   8.171 -by (cut_tac a = m and b = n in mod_div_equality2, arith)
   8.172 +  using mod_div_equality2 [of n m] by arith
   8.173  
   8.174  lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
   8.175    apply (drule mod_less_divisor [where m = m])
   8.176 @@ -773,7 +736,7 @@
   8.177  
   8.178  lemma div_mult1_eq:
   8.179    "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"
   8.180 -by (blast intro: divmod_nat_rel [THEN divmod_nat_rel_mult1_eq, THEN div_eq])
   8.181 +by (blast intro: divmod_nat_rel_mult1_eq [THEN div_nat_unique] divmod_nat_rel)
   8.182  
   8.183  lemma divmod_nat_rel_add1_eq:
   8.184    "divmod_nat_rel a c (aq, ar) \<Longrightarrow> divmod_nat_rel b c (bq, br)
   8.185 @@ -783,7 +746,7 @@
   8.186  (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
   8.187  lemma div_add1_eq:
   8.188    "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
   8.189 -by (blast intro: divmod_nat_rel_add1_eq [THEN div_eq] divmod_nat_rel)
   8.190 +by (blast intro: divmod_nat_rel_add1_eq [THEN div_nat_unique] divmod_nat_rel)
   8.191  
   8.192  lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
   8.193    apply (cut_tac m = q and n = c in mod_less_divisor)
   8.194 @@ -798,10 +761,10 @@
   8.195  by (auto simp add: mult_ac divmod_nat_rel_def add_mult_distrib2 [symmetric] mod_lemma)
   8.196  
   8.197  lemma div_mult2_eq: "a div (b*c) = (a div b) div (c::nat)"
   8.198 -by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_eq])
   8.199 +by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])
   8.200  
   8.201  lemma mod_mult2_eq: "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)"
   8.202 -by (auto simp add: mult_commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_eq])
   8.203 +by (auto simp add: mult_commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_nat_unique])
   8.204  
   8.205  
   8.206  subsubsection {* Further Facts about Quotient and Remainder *}
   8.207 @@ -850,9 +813,9 @@
   8.208  done
   8.209  
   8.210  (* Similar for "less than" *)
   8.211 -lemma div_less_dividend [rule_format]:
   8.212 -     "!!n::nat. 1<n ==> 0 < m --> m div n < m"
   8.213 -apply (induct_tac m rule: nat_less_induct)
   8.214 +lemma div_less_dividend [simp]:
   8.215 +  "\<lbrakk>(1::nat) < n; 0 < m\<rbrakk> \<Longrightarrow> m div n < m"
   8.216 +apply (induct m rule: nat_less_induct)
   8.217  apply (rename_tac "m")
   8.218  apply (case_tac "m<n", simp)
   8.219  apply (subgoal_tac "0<n")
   8.220 @@ -865,8 +828,6 @@
   8.221    apply (simp_all)
   8.222  done
   8.223  
   8.224 -declare div_less_dividend [simp]
   8.225 -
   8.226  text{*A fact for the mutilated chess board*}
   8.227  lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
   8.228  apply (case_tac "n=0", simp)
   8.229 @@ -995,23 +956,11 @@
   8.230  qed
   8.231  
   8.232  theorem mod_div_equality': "(m::nat) mod n = m - (m div n) * n"
   8.233 -  apply (rule_tac P="%x. m mod n = x - (m div n) * n" in
   8.234 -    subst [OF mod_div_equality [of _ n]])
   8.235 -  apply arith
   8.236 -  done
   8.237 -
   8.238 -lemma div_mod_equality':
   8.239 -  fixes m n :: nat
   8.240 -  shows "m div n * n = m - m mod n"
   8.241 -proof -
   8.242 -  have "m mod n \<le> m mod n" ..
   8.243 -  from div_mod_equality have 
   8.244 -    "m div n * n + m mod n - m mod n = m - m mod n" by simp
   8.245 -  with diff_add_assoc [OF `m mod n \<le> m mod n`, of "m div n * n"] have
   8.246 -    "m div n * n + (m mod n - m mod n) = m - m mod n"
   8.247 -    by simp
   8.248 -  then show ?thesis by simp
   8.249 -qed
   8.250 +  using mod_div_equality [of m n] by arith
   8.251 +
   8.252 +lemma div_mod_equality': "(m::nat) div n * n = m - m mod n"
   8.253 +  using mod_div_equality [of m n] by arith
   8.254 +(* FIXME: very similar to mult_div_cancel *)
   8.255  
   8.256  
   8.257  subsubsection {* An ``induction'' law for modulus arithmetic. *}
   8.258 @@ -1103,17 +1052,14 @@
   8.259  qed
   8.260  
   8.261  lemma div2_Suc_Suc [simp]: "Suc (Suc m) div 2 = Suc (m div 2)"
   8.262 -by (auto simp add: numeral_2_eq_2 le_div_geq)
   8.263 +  by (simp add: numeral_2_eq_2 le_div_geq)
   8.264 +
   8.265 +lemma mod2_Suc_Suc [simp]: "Suc (Suc m) mod 2 = m mod 2"
   8.266 +  by (simp add: numeral_2_eq_2 le_mod_geq)
   8.267  
   8.268  lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
   8.269  by (simp add: nat_mult_2 [symmetric])
   8.270  
   8.271 -lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
   8.272 -apply (subgoal_tac "m mod 2 < 2")
   8.273 -apply (erule less_2_cases [THEN disjE])
   8.274 -apply (simp_all (no_asm_simp) add: Let_def mod_Suc)
   8.275 -done
   8.276 -
   8.277  lemma mod2_gr_0 [simp]: "0 < (m\<Colon>nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
   8.278  proof -
   8.279    { fix n :: nat have  "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (cases n) simp_all }
   8.280 @@ -1149,8 +1095,8 @@
   8.281  
   8.282  declare Suc_times_mod_eq [of "numeral w", simp] for w
   8.283  
   8.284 -lemma [simp]: "n div k \<le> (Suc n) div k"
   8.285 -by (simp add: div_le_mono) 
   8.286 +lemma Suc_div_le_mono [simp]: "n div k \<le> (Suc n) div k"
   8.287 +by (simp add: div_le_mono)
   8.288  
   8.289  lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2"
   8.290  by (cases n) simp_all
   8.291 @@ -1187,8 +1133,8 @@
   8.292  
   8.293  definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where
   8.294      --{*definition of quotient and remainder*}
   8.295 -    "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
   8.296 -               (if 0 < b then 0 \<le> r \<and> r < b else b < r \<and> r \<le> 0))"
   8.297 +  "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
   8.298 +    (if 0 < b then 0 \<le> r \<and> r < b else if b < 0 then b < r \<and> r \<le> 0 else q = 0))"
   8.299  
   8.300  definition adjust :: "int \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int" where
   8.301      --{*for the division algorithm*}
   8.302 @@ -1386,42 +1332,87 @@
   8.303  subsubsection {* Existence Shown by Proving the Division Algorithm to be Correct *}
   8.304  
   8.305  (*the case a=0*)
   8.306 -lemma divmod_int_rel_0: "b \<noteq> 0 ==> divmod_int_rel 0 b (0, 0)"
   8.307 +lemma divmod_int_rel_0: "divmod_int_rel 0 b (0, 0)"
   8.308  by (auto simp add: divmod_int_rel_def linorder_neq_iff)
   8.309  
   8.310  lemma posDivAlg_0 [simp]: "posDivAlg 0 b = (0, 0)"
   8.311  by (subst posDivAlg.simps, auto)
   8.312  
   8.313 +lemma posDivAlg_0_right [simp]: "posDivAlg a 0 = (0, a)"
   8.314 +by (subst posDivAlg.simps, auto)
   8.315 +
   8.316  lemma negDivAlg_minus1 [simp]: "negDivAlg -1 b = (-1, b - 1)"
   8.317  by (subst negDivAlg.simps, auto)
   8.318  
   8.319  lemma divmod_int_rel_neg: "divmod_int_rel (-a) (-b) qr ==> divmod_int_rel a b (apsnd uminus qr)"
   8.320 -by (auto simp add: split_ifs divmod_int_rel_def)
   8.321 -
   8.322 -lemma divmod_int_correct: "b \<noteq> 0 ==> divmod_int_rel a b (divmod_int a b)"
   8.323 +by (auto simp add: divmod_int_rel_def)
   8.324 +
   8.325 +lemma divmod_int_correct: "divmod_int_rel a b (divmod_int a b)"
   8.326 +apply (cases "b = 0", simp add: divmod_int_def divmod_int_rel_def)
   8.327  by (force simp add: linorder_neq_iff divmod_int_rel_0 divmod_int_def divmod_int_rel_neg
   8.328                      posDivAlg_correct negDivAlg_correct)
   8.329  
   8.330 -text{*Arbitrary definitions for division by zero.  Useful to simplify 
   8.331 -    certain equations.*}
   8.332 -
   8.333 -lemma DIVISION_BY_ZERO [simp]: "a div (0::int) = 0 & a mod (0::int) = a"
   8.334 -by (simp add: div_int_def mod_int_def divmod_int_def posDivAlg.simps)  
   8.335 -
   8.336 +lemma divmod_int_unique:
   8.337 +  assumes "divmod_int_rel a b qr" 
   8.338 +  shows "divmod_int a b = qr"
   8.339 +  using assms divmod_int_correct [of a b]
   8.340 +  using unique_quotient [of a b] unique_remainder [of a b]
   8.341 +  by (metis pair_collapse)
   8.342 +
   8.343 +lemma divmod_int_rel_div_mod: "divmod_int_rel a b (a div b, a mod b)"
   8.344 +  using divmod_int_correct by (simp add: divmod_int_mod_div)
   8.345 +
   8.346 +lemma div_int_unique: "divmod_int_rel a b (q, r) \<Longrightarrow> a div b = q"
   8.347 +  by (simp add: divmod_int_rel_div_mod [THEN unique_quotient])
   8.348 +
   8.349 +lemma mod_int_unique: "divmod_int_rel a b (q, r) \<Longrightarrow> a mod b = r"
   8.350 +  by (simp add: divmod_int_rel_div_mod [THEN unique_remainder])
   8.351 +
   8.352 +instance int :: ring_div
   8.353 +proof
   8.354 +  fix a b :: int
   8.355 +  show "a div b * b + a mod b = a"
   8.356 +    using divmod_int_rel_div_mod [of a b]
   8.357 +    unfolding divmod_int_rel_def by (simp add: mult_commute)
   8.358 +next
   8.359 +  fix a b c :: int
   8.360 +  assume "b \<noteq> 0"
   8.361 +  hence "divmod_int_rel (a + c * b) b (c + a div b, a mod b)"
   8.362 +    using divmod_int_rel_div_mod [of a b]
   8.363 +    unfolding divmod_int_rel_def by (auto simp: algebra_simps)
   8.364 +  thus "(a + c * b) div b = c + a div b"
   8.365 +    by (rule div_int_unique)
   8.366 +next
   8.367 +  fix a b c :: int
   8.368 +  assume "c \<noteq> 0"
   8.369 +  hence "\<And>q r. divmod_int_rel a b (q, r)
   8.370 +    \<Longrightarrow> divmod_int_rel (c * a) (c * b) (q, c * r)"
   8.371 +    unfolding divmod_int_rel_def
   8.372 +    by - (rule linorder_cases [of 0 b], auto simp: algebra_simps
   8.373 +      mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
   8.374 +      mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff)
   8.375 +  hence "divmod_int_rel (c * a) (c * b) (a div b, c * (a mod b))"
   8.376 +    using divmod_int_rel_div_mod [of a b] .
   8.377 +  thus "(c * a) div (c * b) = a div b"
   8.378 +    by (rule div_int_unique)
   8.379 +next
   8.380 +  fix a :: int show "a div 0 = 0"
   8.381 +    by (rule div_int_unique, simp add: divmod_int_rel_def)
   8.382 +next
   8.383 +  fix a :: int show "0 div a = 0"
   8.384 +    by (rule div_int_unique, auto simp add: divmod_int_rel_def)
   8.385 +qed
   8.386  
   8.387  text{*Basic laws about division and remainder*}
   8.388  
   8.389  lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
   8.390 -apply (case_tac "b = 0", simp)
   8.391 -apply (cut_tac a = a and b = b in divmod_int_correct)
   8.392 -apply (auto simp add: divmod_int_rel_def prod_eq_iff)
   8.393 -done
   8.394 +  by (fact mod_div_equality2 [symmetric])
   8.395  
   8.396  lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k"
   8.397 -by(simp add: zmod_zdiv_equality[symmetric])
   8.398 +  by (fact div_mod_equality2)
   8.399  
   8.400  lemma zdiv_zmod_equality2: "((a div b) * b + (a mod b)) + k = (a::int)+k"
   8.401 -by(simp add: mult_commute zmod_zdiv_equality[symmetric])
   8.402 +  by (fact div_mod_equality)
   8.403  
   8.404  text {* Tool setup *}
   8.405  
   8.406 @@ -1446,18 +1437,16 @@
   8.407  
   8.408  simproc_setup cancel_div_mod_int ("(k::int) + l") = {* K Cancel_Div_Mod_Int.proc *}
   8.409  
   8.410 -lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b"
   8.411 -apply (cut_tac a = a and b = b in divmod_int_correct)
   8.412 -apply (auto simp add: divmod_int_rel_def prod_eq_iff)
   8.413 -done
   8.414 +lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
   8.415 +  using divmod_int_correct [of a b]
   8.416 +  by (auto simp add: divmod_int_rel_def prod_eq_iff)
   8.417  
   8.418  lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
   8.419     and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]
   8.420  
   8.421 -lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b"
   8.422 -apply (cut_tac a = a and b = b in divmod_int_correct)
   8.423 -apply (auto simp add: divmod_int_rel_def prod_eq_iff)
   8.424 -done
   8.425 +lemma neg_mod_conj: "b < (0::int) \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b"
   8.426 +  using divmod_int_correct [of a b]
   8.427 +  by (auto simp add: divmod_int_rel_def prod_eq_iff)
   8.428  
   8.429  lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
   8.430     and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
   8.431 @@ -1465,50 +1454,35 @@
   8.432  
   8.433  subsubsection {* General Properties of div and mod *}
   8.434  
   8.435 -lemma divmod_int_rel_div_mod: "b \<noteq> 0 ==> divmod_int_rel a b (a div b, a mod b)"
   8.436 -apply (cut_tac a = a and b = b in zmod_zdiv_equality)
   8.437 -apply (force simp add: divmod_int_rel_def linorder_neq_iff)
   8.438 -done
   8.439 -
   8.440 -lemma divmod_int_rel_div: "[| divmod_int_rel a b (q, r) |] ==> a div b = q"
   8.441 -apply (cases "b = 0")
   8.442 -apply (simp add: divmod_int_rel_def)
   8.443 -by (simp add: divmod_int_rel_div_mod [THEN unique_quotient])
   8.444 -
   8.445 -lemma divmod_int_rel_mod: "[| divmod_int_rel a b (q, r) |] ==> a mod b = r"
   8.446 -apply (cases "b = 0")
   8.447 -apply (simp add: divmod_int_rel_def)
   8.448 -by (simp add: divmod_int_rel_div_mod [THEN unique_remainder])
   8.449 -
   8.450  lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
   8.451 -apply (rule divmod_int_rel_div)
   8.452 +apply (rule div_int_unique)
   8.453  apply (auto simp add: divmod_int_rel_def)
   8.454  done
   8.455  
   8.456  lemma div_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a div b = 0"
   8.457 -apply (rule divmod_int_rel_div)
   8.458 +apply (rule div_int_unique)
   8.459  apply (auto simp add: divmod_int_rel_def)
   8.460  done
   8.461  
   8.462  lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a div b = -1"
   8.463 -apply (rule divmod_int_rel_div)
   8.464 +apply (rule div_int_unique)
   8.465  apply (auto simp add: divmod_int_rel_def)
   8.466  done
   8.467  
   8.468  (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
   8.469  
   8.470  lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"
   8.471 -apply (rule_tac q = 0 in divmod_int_rel_mod)
   8.472 +apply (rule_tac q = 0 in mod_int_unique)
   8.473  apply (auto simp add: divmod_int_rel_def)
   8.474  done
   8.475  
   8.476  lemma mod_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a mod b = a"
   8.477 -apply (rule_tac q = 0 in divmod_int_rel_mod)
   8.478 +apply (rule_tac q = 0 in mod_int_unique)
   8.479  apply (auto simp add: divmod_int_rel_def)
   8.480  done
   8.481  
   8.482  lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"
   8.483 -apply (rule_tac q = "-1" in divmod_int_rel_mod)
   8.484 +apply (rule_tac q = "-1" in mod_int_unique)
   8.485  apply (auto simp add: divmod_int_rel_def)
   8.486  done
   8.487  
   8.488 @@ -1517,24 +1491,17 @@
   8.489  
   8.490  (*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*)
   8.491  lemma zdiv_zminus_zminus [simp]: "(-a) div (-b) = a div (b::int)"
   8.492 -apply (case_tac "b = 0", simp)
   8.493 -apply (simp add: divmod_int_rel_div_mod [THEN divmod_int_rel_neg, simplified, 
   8.494 -                                 THEN divmod_int_rel_div, THEN sym])
   8.495 -
   8.496 -done
   8.497 +  using div_mult_mult1 [of "-1" a b] by simp (* FIXME: generalize *)
   8.498  
   8.499  (*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*)
   8.500  lemma zmod_zminus_zminus [simp]: "(-a) mod (-b) = - (a mod (b::int))"
   8.501 -apply (case_tac "b = 0", simp)
   8.502 -apply (subst divmod_int_rel_div_mod [THEN divmod_int_rel_neg, simplified, THEN divmod_int_rel_mod],
   8.503 -       auto)
   8.504 -done
   8.505 +  using mod_mult_mult1 [of "-1" a b] by simp (* FIXME: generalize *)
   8.506  
   8.507  
   8.508  subsubsection {* Laws for div and mod with Unary Minus *}
   8.509  
   8.510  lemma zminus1_lemma:
   8.511 -     "divmod_int_rel a b (q, r)
   8.512 +     "divmod_int_rel a b (q, r) ==> b \<noteq> 0
   8.513        ==> divmod_int_rel (-a) b (if r=0 then -q else -q - 1,  
   8.514                            if r=0 then 0 else b-r)"
   8.515  by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_diff_distrib)
   8.516 @@ -1544,12 +1511,12 @@
   8.517       "b \<noteq> (0::int)  
   8.518        ==> (-a) div b =  
   8.519            (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
   8.520 -by (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN divmod_int_rel_div])
   8.521 +by (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN div_int_unique])
   8.522  
   8.523  lemma zmod_zminus1_eq_if:
   8.524       "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
   8.525  apply (case_tac "b = 0", simp)
   8.526 -apply (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN divmod_int_rel_mod])
   8.527 +apply (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN mod_int_unique])
   8.528  done
   8.529  
   8.530  lemma zmod_zminus1_not_zero:
   8.531 @@ -1558,10 +1525,10 @@
   8.532    unfolding zmod_zminus1_eq_if by auto
   8.533  
   8.534  lemma zdiv_zminus2: "a div (-b) = (-a::int) div b"
   8.535 -by (cut_tac a = "-a" in zdiv_zminus_zminus, auto)
   8.536 +  using zdiv_zminus_zminus [of "-a" b] by simp (* FIXME: generalize *)
   8.537  
   8.538  lemma zmod_zminus2: "a mod (-b) = - ((-a::int) mod b)"
   8.539 -by (cut_tac a = "-a" and b = b in zmod_zminus_zminus, auto)
   8.540 +  using zmod_zminus_zminus [of "-a" b] by simp (* FIXME: generalize*)
   8.541  
   8.542  lemma zdiv_zminus2_eq_if:
   8.543       "b \<noteq> (0::int)  
   8.544 @@ -1579,53 +1546,11 @@
   8.545    unfolding zmod_zminus2_eq_if by auto 
   8.546  
   8.547  
   8.548 -subsubsection {* Division of a Number by Itself *}
   8.549 -
   8.550 -lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 \<le> q"
   8.551 -apply (subgoal_tac "0 < a*q")
   8.552 - apply (simp add: zero_less_mult_iff, arith)
   8.553 -done
   8.554 -
   8.555 -lemma self_quotient_aux2: "[| (0::int) < a; a = r + a*q; 0 \<le> r |] ==> q \<le> 1"
   8.556 -apply (subgoal_tac "0 \<le> a* (1-q) ")
   8.557 - apply (simp add: zero_le_mult_iff)
   8.558 -apply (simp add: right_diff_distrib)
   8.559 -done
   8.560 -
   8.561 -lemma self_quotient: "[| divmod_int_rel a a (q, r) |] ==> q = 1"
   8.562 -apply (simp add: split_ifs divmod_int_rel_def linorder_neq_iff)
   8.563 -apply (rule order_antisym, safe, simp_all)
   8.564 -apply (rule_tac [3] a = "-a" and r = "-r" in self_quotient_aux1)
   8.565 -apply (rule_tac a = "-a" and r = "-r" in self_quotient_aux2)
   8.566 -apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: add_commute)+
   8.567 -done
   8.568 -
   8.569 -lemma self_remainder: "[| divmod_int_rel a a (q, r) |] ==> r = 0"
   8.570 -apply (frule self_quotient)
   8.571 -apply (simp add: divmod_int_rel_def)
   8.572 -done
   8.573 -
   8.574 -lemma zdiv_self [simp]: "a \<noteq> 0 ==> a div a = (1::int)"
   8.575 -by (simp add: divmod_int_rel_div_mod [THEN self_quotient])
   8.576 -
   8.577 -(*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *)
   8.578 -lemma zmod_self [simp]: "a mod a = (0::int)"
   8.579 -apply (case_tac "a = 0", simp)
   8.580 -apply (simp add: divmod_int_rel_div_mod [THEN self_remainder])
   8.581 -done
   8.582 -
   8.583 -
   8.584  subsubsection {* Computation of Division and Remainder *}
   8.585  
   8.586 -lemma zdiv_zero [simp]: "(0::int) div b = 0"
   8.587 -by (simp add: div_int_def divmod_int_def)
   8.588 -
   8.589  lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
   8.590  by (simp add: div_int_def divmod_int_def)
   8.591  
   8.592 -lemma zmod_zero [simp]: "(0::int) mod b = 0"
   8.593 -by (simp add: mod_int_def divmod_int_def)
   8.594 -
   8.595  lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
   8.596  by (simp add: mod_int_def divmod_int_def)
   8.597  
   8.598 @@ -1668,18 +1593,18 @@
   8.599  text {*Simplify expresions in which div and mod combine numerical constants*}
   8.600  
   8.601  lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
   8.602 -  by (rule divmod_int_rel_div [of a b q r]) (simp add: divmod_int_rel_def)
   8.603 +  by (rule div_int_unique [of a b q r]) (simp add: divmod_int_rel_def)
   8.604  
   8.605  lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
   8.606 -  by (rule divmod_int_rel_div [of a b q r],
   8.607 +  by (rule div_int_unique [of a b q r],
   8.608      simp add: divmod_int_rel_def)
   8.609  
   8.610  lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
   8.611 -  by (rule divmod_int_rel_mod [of a b q r],
   8.612 +  by (rule mod_int_unique [of a b q r],
   8.613      simp add: divmod_int_rel_def)
   8.614  
   8.615  lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
   8.616 -  by (rule divmod_int_rel_mod [of a b q r],
   8.617 +  by (rule mod_int_unique [of a b q r],
   8.618      simp add: divmod_int_rel_def)
   8.619  
   8.620  (* simprocs adapted from HOL/ex/Binary.thy *)
   8.621 @@ -1742,10 +1667,11 @@
   8.622  apply (cut_tac a = a and b = "-1" in neg_mod_sign)
   8.623  apply (cut_tac [2] a = a and b = "-1" in neg_mod_bound)
   8.624  apply (auto simp del: neg_mod_sign neg_mod_bound)
   8.625 -done
   8.626 +done (* FIXME: generalize *)
   8.627  
   8.628  lemma zdiv_minus1_right [simp]: "a div (-1::int) = -a"
   8.629  by (cut_tac a = a and b = "-1" in zmod_zdiv_equality, auto)
   8.630 +(* FIXME: generalize *)
   8.631  
   8.632  (** The last remaining special cases for constant arithmetic:
   8.633      1 div z and 1 mod z **)
   8.634 @@ -1863,18 +1789,11 @@
   8.635  
   8.636  lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
   8.637  apply (case_tac "c = 0", simp)
   8.638 -apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN divmod_int_rel_div])
   8.639 +apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN div_int_unique])
   8.640  done
   8.641  
   8.642  lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)"
   8.643 -apply (case_tac "c = 0", simp)
   8.644 -apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN divmod_int_rel_mod])
   8.645 -done
   8.646 -
   8.647 -lemma zmod_zdiv_trivial: "(a mod b) div b = (0::int)"
   8.648 -apply (case_tac "b = 0", simp)
   8.649 -apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
   8.650 -done
   8.651 +  by (fact mod_mult_right_eq) (* FIXME: delete *)
   8.652  
   8.653  text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
   8.654  
   8.655 @@ -1887,36 +1806,9 @@
   8.656  lemma zdiv_zadd1_eq:
   8.657       "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
   8.658  apply (case_tac "c = 0", simp)
   8.659 -apply (blast intro: zadd1_lemma [OF divmod_int_rel_div_mod divmod_int_rel_div_mod] divmod_int_rel_div)
   8.660 +apply (blast intro: zadd1_lemma [OF divmod_int_rel_div_mod divmod_int_rel_div_mod] div_int_unique)
   8.661  done
   8.662  
   8.663 -instance int :: ring_div
   8.664 -proof
   8.665 -  fix a b c :: int
   8.666 -  assume not0: "b \<noteq> 0"
   8.667 -  show "(a + c * b) div b = c + a div b"
   8.668 -    unfolding zdiv_zadd1_eq [of a "c * b"] using not0 
   8.669 -      by (simp add: zmod_zmult1_eq zmod_zdiv_trivial zdiv_zmult1_eq)
   8.670 -next
   8.671 -  fix a b c :: int
   8.672 -  assume "a \<noteq> 0"
   8.673 -  then show "(a * b) div (a * c) = b div c"
   8.674 -  proof (cases "b \<noteq> 0 \<and> c \<noteq> 0")
   8.675 -    case False then show ?thesis by auto
   8.676 -  next
   8.677 -    case True then have "b \<noteq> 0" and "c \<noteq> 0" by auto
   8.678 -    with `a \<noteq> 0`
   8.679 -    have "\<And>q r. divmod_int_rel b c (q, r) \<Longrightarrow> divmod_int_rel (a * b) (a * c) (q, a * r)"
   8.680 -      apply (auto simp add: divmod_int_rel_def) 
   8.681 -      apply (auto simp add: algebra_simps)
   8.682 -      apply (auto simp add: zero_less_mult_iff zero_le_mult_iff mult_le_0_iff mult_commute [of a] mult_less_cancel_right)
   8.683 -      done
   8.684 -    moreover with `c \<noteq> 0` divmod_int_rel_div_mod have "divmod_int_rel b c (b div c, b mod c)" by auto
   8.685 -    ultimately have "divmod_int_rel (a * b) (a * c) (b div c, a * (b mod c))" .
   8.686 -    from this show ?thesis by (rule divmod_int_rel_div)
   8.687 -  qed
   8.688 -qed auto
   8.689 -
   8.690  lemma posDivAlg_div_mod:
   8.691    assumes "k \<ge> 0"
   8.692    and "l \<ge> 0"
   8.693 @@ -1927,7 +1819,7 @@
   8.694    case False with assms posDivAlg_correct
   8.695      have "divmod_int_rel k l (fst (posDivAlg k l), snd (posDivAlg k l))"
   8.696      by simp
   8.697 -  from divmod_int_rel_div [OF this] divmod_int_rel_mod [OF this]
   8.698 +  from div_int_unique [OF this] mod_int_unique [OF this]
   8.699    show ?thesis by simp
   8.700  qed
   8.701  
   8.702 @@ -1940,7 +1832,7 @@
   8.703    from assms negDivAlg_correct
   8.704      have "divmod_int_rel k l (fst (negDivAlg k l), snd (negDivAlg k l))"
   8.705      by simp
   8.706 -  from divmod_int_rel_div [OF this] divmod_int_rel_mod [OF this]
   8.707 +  from div_int_unique [OF this] mod_int_unique [OF this]
   8.708    show ?thesis by simp
   8.709  qed
   8.710  
   8.711 @@ -1952,8 +1844,7 @@
   8.712  
   8.713  lemma zmod_zdiv_equality':
   8.714    "(m\<Colon>int) mod n = m - (m div n) * n"
   8.715 -  by (rule_tac P="%x. m mod n = x - (m div n) * n" in subst [OF mod_div_equality [of _ n]])
   8.716 -    arith
   8.717 +  using mod_div_equality [of m n] by arith
   8.718  
   8.719  
   8.720  subsubsection {* Proving  @{term "a div (b*c) = (a div b) div c"} *}
   8.721 @@ -2003,17 +1894,17 @@
   8.722        ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
   8.723  by (auto simp add: mult_ac divmod_int_rel_def linorder_neq_iff
   8.724                     zero_less_mult_iff right_distrib [symmetric] 
   8.725 -                   zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4)
   8.726 +                   zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: split_if_asm)
   8.727  
   8.728  lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"
   8.729  apply (case_tac "b = 0", simp)
   8.730 -apply (force simp add: divmod_int_rel_div_mod [THEN zmult2_lemma, THEN divmod_int_rel_div])
   8.731 +apply (force simp add: divmod_int_rel_div_mod [THEN zmult2_lemma, THEN div_int_unique])
   8.732  done
   8.733  
   8.734  lemma zmod_zmult2_eq:
   8.735       "(0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b"
   8.736  apply (case_tac "b = 0", simp)
   8.737 -apply (force simp add: divmod_int_rel_div_mod [THEN zmult2_lemma, THEN divmod_int_rel_mod])
   8.738 +apply (force simp add: divmod_int_rel_div_mod [THEN zmult2_lemma, THEN mod_int_unique])
   8.739  done
   8.740  
   8.741  lemma div_pos_geq:
   8.742 @@ -2295,14 +2186,14 @@
   8.743  
   8.744  lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
   8.745    using zmod_zdiv_equality[where a="m" and b="n"]
   8.746 -  by (simp add: algebra_simps)
   8.747 +  by (simp add: algebra_simps) (* FIXME: generalize *)
   8.748  
   8.749  lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
   8.750  apply (induct "y", auto)
   8.751 -apply (rule zmod_zmult1_eq [THEN trans])
   8.752 +apply (rule mod_mult_right_eq [THEN trans])
   8.753  apply (simp (no_asm_simp))
   8.754  apply (rule mod_mult_eq [symmetric])
   8.755 -done
   8.756 +done (* FIXME: generalize *)
   8.757  
   8.758  lemma zdiv_int: "int (a div b) = (int a) div (int b)"
   8.759  apply (subst split_div, auto)
   8.760 @@ -2350,7 +2241,7 @@
   8.761  lemmas zmod_simps =
   8.762    mod_add_left_eq  [symmetric]
   8.763    mod_add_right_eq [symmetric]
   8.764 -  zmod_zmult1_eq   [symmetric]
   8.765 +  mod_mult_right_eq[symmetric]
   8.766    mod_mult_left_eq [symmetric]
   8.767    zpower_zmod
   8.768    zminus_zmod zdiff_zmod_left zdiff_zmod_right
     9.1 --- a/src/HOL/Groebner_Basis.thy	Tue Mar 27 14:14:46 2012 +0200
     9.2 +++ b/src/HOL/Groebner_Basis.thy	Tue Mar 27 15:34:04 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 14:14:46 2012 +0200
    10.2 +++ b/src/HOL/Presburger.thy	Tue Mar 27 15:34:04 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 14:14:46 2012 +0200
    11.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Tue Mar 27 15:34:04 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}