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}