1.1 --- a/src/HOL/Divides.thy	Tue Mar 27 09:44:56 2012 +0200
     1.2 +++ b/src/HOL/Divides.thy	Tue Mar 27 09:54:39 2012 +0200
     1.3 @@ -535,7 +535,7 @@
     1.4    by (auto simp add: divmod_nat_def intro: theI elim: divmod_nat_rel_unique)
     1.5  qed
     1.6  
     1.7 -lemma divmod_nat_eq:
     1.8 +lemma divmod_nat_unique:
     1.9    assumes "divmod_nat_rel m n qr" 
    1.10    shows "divmod_nat m n = qr"
    1.11    using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
    1.12 @@ -561,22 +561,22 @@
    1.13    "divmod_nat m n = (m div n, m mod n)"
    1.14    by (simp add: prod_eq_iff)
    1.15  
    1.16 -lemma div_eq:
    1.17 +lemma div_nat_unique:
    1.18    assumes "divmod_nat_rel m n (q, r)" 
    1.19    shows "m div n = q"
    1.20 -  using assms by (auto dest!: divmod_nat_eq simp add: prod_eq_iff)
    1.21 -
    1.22 -lemma mod_eq:
    1.23 +  using assms by (auto dest!: divmod_nat_unique simp add: prod_eq_iff)
    1.24 +
    1.25 +lemma mod_nat_unique:
    1.26    assumes "divmod_nat_rel m n (q, r)" 
    1.27    shows "m mod n = r"
    1.28 -  using assms by (auto dest!: divmod_nat_eq simp add: prod_eq_iff)
    1.29 +  using assms by (auto dest!: divmod_nat_unique simp add: prod_eq_iff)
    1.30  
    1.31  lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
    1.32    using divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod)
    1.33  
    1.34  lemma divmod_nat_zero:
    1.35    "divmod_nat m 0 = (0, m)"
    1.36 -proof (rule divmod_nat_eq)
    1.37 +proof (rule divmod_nat_unique)
    1.38    show "divmod_nat_rel m 0 (0, m)"
    1.39      unfolding divmod_nat_rel_def by simp
    1.40  qed
    1.41 @@ -584,7 +584,7 @@
    1.42  lemma divmod_nat_base:
    1.43    assumes "m < n"
    1.44    shows "divmod_nat m n = (0, m)"
    1.45 -proof (rule divmod_nat_eq)
    1.46 +proof (rule divmod_nat_unique)
    1.47    show "divmod_nat_rel m n (0, m)"
    1.48      unfolding divmod_nat_rel_def using assms by simp
    1.49  qed
    1.50 @@ -592,7 +592,7 @@
    1.51  lemma divmod_nat_step:
    1.52    assumes "0 < n" and "n \<le> m"
    1.53    shows "divmod_nat m n = (Suc ((m - n) div n), (m - n) mod n)"
    1.54 -proof (rule divmod_nat_eq)
    1.55 +proof (rule divmod_nat_unique)
    1.56    have "divmod_nat_rel (m - n) n ((m - n) div n, (m - n) mod n)"
    1.57      by (rule divmod_nat_rel)
    1.58    thus "divmod_nat_rel m n (Suc ((m - n) div n), (m - n) mod n)"
    1.59 @@ -656,7 +656,7 @@
    1.60          by (auto simp add: divmod_nat_rel_def) (simp_all add: algebra_simps)
    1.61        moreover from divmod_nat_rel have "divmod_nat_rel n q (n div q, n mod q)" .
    1.62        ultimately have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))" .
    1.63 -      then show ?thesis by (simp add: div_eq)
    1.64 +      then show ?thesis by (simp add: div_nat_unique)
    1.65      qed
    1.66    qed simp_all
    1.67  qed
    1.68 @@ -757,7 +757,7 @@
    1.69  
    1.70  lemma div_mult1_eq:
    1.71    "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"
    1.72 -by (blast intro: divmod_nat_rel [THEN divmod_nat_rel_mult1_eq, THEN div_eq])
    1.73 +by (blast intro: divmod_nat_rel_mult1_eq [THEN div_nat_unique] divmod_nat_rel)
    1.74  
    1.75  lemma divmod_nat_rel_add1_eq:
    1.76    "divmod_nat_rel a c (aq, ar) \<Longrightarrow> divmod_nat_rel b c (bq, br)
    1.77 @@ -767,7 +767,7 @@
    1.78  (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
    1.79  lemma div_add1_eq:
    1.80    "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
    1.81 -by (blast intro: divmod_nat_rel_add1_eq [THEN div_eq] divmod_nat_rel)
    1.82 +by (blast intro: divmod_nat_rel_add1_eq [THEN div_nat_unique] divmod_nat_rel)
    1.83  
    1.84  lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
    1.85    apply (cut_tac m = q and n = c in mod_less_divisor)
    1.86 @@ -782,10 +782,10 @@
    1.87  by (auto simp add: mult_ac divmod_nat_rel_def add_mult_distrib2 [symmetric] mod_lemma)
    1.88  
    1.89  lemma div_mult2_eq: "a div (b*c) = (a div b) div (c::nat)"
    1.90 -by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_eq])
    1.91 +by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])
    1.92  
    1.93  lemma mod_mult2_eq: "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)"
    1.94 -by (auto simp add: mult_commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_eq])
    1.95 +by (auto simp add: mult_commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_nat_unique])
    1.96  
    1.97  
    1.98  subsubsection {* Further Facts about Quotient and Remainder *}