src/HOL/Divides.thy
 changeset 47142 d64fa2ca54b8 parent 47141 02d6b816e4b3 child 47159 978c00c20a59
```     1.1 --- a/src/HOL/Divides.thy	Tue Mar 27 12:42:54 2012 +0200
1.2 +++ b/src/HOL/Divides.thy	Tue Mar 27 14:49:56 2012 +0200
1.3 @@ -1403,12 +1403,6 @@
1.4      by (rule div_int_unique, auto simp add: divmod_int_rel_def)
1.5  qed
1.6
1.7 -text{*Arbitrary definitions for division by zero.  Useful to simplify
1.8 -    certain equations.*}
1.9 -
1.10 -lemma DIVISION_BY_ZERO [simp]: "a div (0::int) = 0 & a mod (0::int) = a"
1.11 -  by simp (* FIXME: delete *)
1.12 -
1.13  text{*Basic laws about division and remainder*}
1.14
1.15  lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
1.16 @@ -1552,51 +1546,11 @@
1.17    unfolding zmod_zminus2_eq_if by auto
1.18
1.19
1.20 -subsubsection {* Division of a Number by Itself *}
1.21 -
1.22 -lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 \<le> q"
1.23 -apply (subgoal_tac "0 < a*q")
1.24 - apply (simp add: zero_less_mult_iff, arith)
1.25 -done
1.26 -
1.27 -lemma self_quotient_aux2: "[| (0::int) < a; a = r + a*q; 0 \<le> r |] ==> q \<le> 1"
1.28 -apply (subgoal_tac "0 \<le> a* (1-q) ")
1.29 - apply (simp add: zero_le_mult_iff)
1.31 -done
1.32 -
1.33 -lemma self_quotient: "[| divmod_int_rel a a (q, r); a \<noteq> 0 |] ==> q = 1"
1.34 -apply (simp add: split_ifs divmod_int_rel_def linorder_neq_iff)
1.35 -apply (rule order_antisym, safe, simp_all)
1.36 -apply (rule_tac [3] a = "-a" and r = "-r" in self_quotient_aux1)
1.37 -apply (rule_tac a = "-a" and r = "-r" in self_quotient_aux2)
1.39 -done
1.40 -
1.41 -lemma self_remainder: "[| divmod_int_rel a a (q, r); a \<noteq> 0 |] ==> r = 0"
1.42 -apply (frule (1) self_quotient)
1.44 -done
1.45 -
1.46 -lemma zdiv_self [simp]: "a \<noteq> 0 ==> a div a = (1::int)"
1.47 -  by (fact div_self) (* FIXME: delete *)
1.48 -
1.49 -(*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *)
1.50 -lemma zmod_self [simp]: "a mod a = (0::int)"
1.51 -  by (fact mod_self) (* FIXME: delete *)
1.52 -
1.53 -
1.54  subsubsection {* Computation of Division and Remainder *}
1.55
1.56 -lemma zdiv_zero [simp]: "(0::int) div b = 0"
1.57 -  by (fact div_0) (* FIXME: delete *)
1.58 -
1.59  lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
1.60  by (simp add: div_int_def divmod_int_def)
1.61
1.62 -lemma zmod_zero [simp]: "(0::int) mod b = 0"
1.63 -  by (fact mod_0) (* FIXME: delete *)
1.64 -
1.65  lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
1.66  by (simp add: mod_int_def divmod_int_def)
1.67
1.68 @@ -1841,9 +1795,6 @@
1.69  lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)"
1.70    by (fact mod_mult_right_eq) (* FIXME: delete *)
1.71
1.72 -lemma zmod_zdiv_trivial: "(a mod b) div b = (0::int)"
1.73 -  by (fact mod_div_trivial) (* FIXME: delete *)
1.74 -
1.75  text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
1.76
1.78 @@ -2235,14 +2186,14 @@
1.79
1.80  lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
1.81    using zmod_zdiv_equality[where a="m" and b="n"]
1.82 -  by (simp add: algebra_simps)
1.83 +  by (simp add: algebra_simps) (* FIXME: generalize *)
1.84
1.85  lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
1.86  apply (induct "y", auto)
1.87 -apply (rule zmod_zmult1_eq [THEN trans])
1.88 +apply (rule mod_mult_right_eq [THEN trans])
1.89  apply (simp (no_asm_simp))
1.90  apply (rule mod_mult_eq [symmetric])
1.91 -done
1.92 +done (* FIXME: generalize *)
1.93
1.94  lemma zdiv_int: "int (a div b) = (int a) div (int b)"
1.95  apply (subst split_div, auto)
1.96 @@ -2290,7 +2241,7 @@
1.97  lemmas zmod_simps =