author bulwahn Tue Mar 27 15:34:04 2012 +0200 (2012-03-27) changeset 47144 9bfc32fc7ced 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}
```