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.30 -apply (simp add: right_diff_distrib)
    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.38 -apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: add_commute)+
    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.43 -apply (simp add: divmod_int_rel_def)
    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.77  lemma zadd1_lemma:
    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 =
    1.98    mod_add_left_eq  [symmetric]
    1.99    mod_add_right_eq [symmetric]
   1.100 -  zmod_zmult1_eq   [symmetric]
   1.101 +  mod_mult_right_eq[symmetric]
   1.102    mod_mult_left_eq [symmetric]
   1.103    zpower_zmod
   1.104    zminus_zmod zdiff_zmod_left zdiff_zmod_right