1.1 --- a/src/HOL/Divides.thy	Tue Mar 27 11:41:16 2012 +0200
     1.2 +++ b/src/HOL/Divides.thy	Tue Mar 27 11:45:02 2012 +0200
     1.3 @@ -1420,41 +1420,41 @@
     1.4  apply (force simp add: divmod_int_rel_def linorder_neq_iff)
     1.5  done
     1.6  
     1.7 -lemma divmod_int_rel_div: "[| divmod_int_rel a b (q, r) |] ==> a div b = q"
     1.8 +lemma div_int_unique: "[| divmod_int_rel a b (q, r) |] ==> a div b = q"
     1.9  by (simp add: divmod_int_rel_div_mod [THEN unique_quotient])
    1.10  
    1.11 -lemma divmod_int_rel_mod: "[| divmod_int_rel a b (q, r) |] ==> a mod b = r"
    1.12 +lemma mod_int_unique: "[| divmod_int_rel a b (q, r) |] ==> a mod b = r"
    1.13  by (simp add: divmod_int_rel_div_mod [THEN unique_remainder])
    1.14  
    1.15  lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
    1.16 -apply (rule divmod_int_rel_div)
    1.17 +apply (rule div_int_unique)
    1.18  apply (auto simp add: divmod_int_rel_def)
    1.19  done
    1.20  
    1.21  lemma div_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a div b = 0"
    1.22 -apply (rule divmod_int_rel_div)
    1.23 +apply (rule div_int_unique)
    1.24  apply (auto simp add: divmod_int_rel_def)
    1.25  done
    1.26  
    1.27  lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a div b = -1"
    1.28 -apply (rule divmod_int_rel_div)
    1.29 +apply (rule div_int_unique)
    1.30  apply (auto simp add: divmod_int_rel_def)
    1.31  done
    1.32  
    1.33  (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
    1.34  
    1.35  lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"
    1.36 -apply (rule_tac q = 0 in divmod_int_rel_mod)
    1.37 +apply (rule_tac q = 0 in mod_int_unique)
    1.38  apply (auto simp add: divmod_int_rel_def)
    1.39  done
    1.40  
    1.41  lemma mod_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a mod b = a"
    1.42 -apply (rule_tac q = 0 in divmod_int_rel_mod)
    1.43 +apply (rule_tac q = 0 in mod_int_unique)
    1.44  apply (auto simp add: divmod_int_rel_def)
    1.45  done
    1.46  
    1.47  lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"
    1.48 -apply (rule_tac q = "-1" in divmod_int_rel_mod)
    1.49 +apply (rule_tac q = "-1" in mod_int_unique)
    1.50  apply (auto simp add: divmod_int_rel_def)
    1.51  done
    1.52  
    1.53 @@ -1464,13 +1464,13 @@
    1.54  (*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*)
    1.55  lemma zdiv_zminus_zminus [simp]: "(-a) div (-b) = a div (b::int)"
    1.56  apply (simp add: divmod_int_rel_div_mod [THEN divmod_int_rel_neg, simplified, 
    1.57 -                                 THEN divmod_int_rel_div, THEN sym])
    1.58 +                                 THEN div_int_unique, THEN sym])
    1.59  
    1.60  done
    1.61  
    1.62  (*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*)
    1.63  lemma zmod_zminus_zminus [simp]: "(-a) mod (-b) = - (a mod (b::int))"
    1.64 -apply (subst divmod_int_rel_div_mod [THEN divmod_int_rel_neg, simplified, THEN divmod_int_rel_mod],
    1.65 +apply (subst divmod_int_rel_div_mod [THEN divmod_int_rel_neg, simplified, THEN mod_int_unique],
    1.66         auto)
    1.67  done
    1.68  
    1.69 @@ -1488,12 +1488,12 @@
    1.70       "b \<noteq> (0::int)  
    1.71        ==> (-a) div b =  
    1.72            (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
    1.73 -by (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN divmod_int_rel_div])
    1.74 +by (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN div_int_unique])
    1.75  
    1.76  lemma zmod_zminus1_eq_if:
    1.77       "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
    1.78  apply (case_tac "b = 0", simp)
    1.79 -apply (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN divmod_int_rel_mod])
    1.80 +apply (blast intro: divmod_int_rel_div_mod [THEN zminus1_lemma, THEN mod_int_unique])
    1.81  done
    1.82  
    1.83  lemma zmod_zminus1_not_zero:
    1.84 @@ -1612,18 +1612,18 @@
    1.85  text {*Simplify expresions in which div and mod combine numerical constants*}
    1.86  
    1.87  lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
    1.88 -  by (rule divmod_int_rel_div [of a b q r]) (simp add: divmod_int_rel_def)
    1.89 +  by (rule div_int_unique [of a b q r]) (simp add: divmod_int_rel_def)
    1.90  
    1.91  lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
    1.92 -  by (rule divmod_int_rel_div [of a b q r],
    1.93 +  by (rule div_int_unique [of a b q r],
    1.94      simp add: divmod_int_rel_def)
    1.95  
    1.96  lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
    1.97 -  by (rule divmod_int_rel_mod [of a b q r],
    1.98 +  by (rule mod_int_unique [of a b q r],
    1.99      simp add: divmod_int_rel_def)
   1.100  
   1.101  lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
   1.102 -  by (rule divmod_int_rel_mod [of a b q r],
   1.103 +  by (rule mod_int_unique [of a b q r],
   1.104      simp add: divmod_int_rel_def)
   1.105  
   1.106  (* simprocs adapted from HOL/ex/Binary.thy *)
   1.107 @@ -1807,12 +1807,12 @@
   1.108  
   1.109  lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
   1.110  apply (case_tac "c = 0", simp)
   1.111 -apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN divmod_int_rel_div])
   1.112 +apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN div_int_unique])
   1.113  done
   1.114  
   1.115  lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)"
   1.116  apply (case_tac "c = 0", simp)
   1.117 -apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN divmod_int_rel_mod])
   1.118 +apply (blast intro: divmod_int_rel_div_mod [THEN zmult1_lemma, THEN mod_int_unique])
   1.119  done
   1.120  
   1.121  lemma zmod_zdiv_trivial: "(a mod b) div b = (0::int)"
   1.122 @@ -1831,7 +1831,7 @@
   1.123  lemma zdiv_zadd1_eq:
   1.124       "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
   1.125  apply (case_tac "c = 0", simp)
   1.126 -apply (blast intro: zadd1_lemma [OF divmod_int_rel_div_mod divmod_int_rel_div_mod] divmod_int_rel_div)
   1.127 +apply (blast intro: zadd1_lemma [OF divmod_int_rel_div_mod divmod_int_rel_div_mod] div_int_unique)
   1.128  done
   1.129  
   1.130  instance int :: ring_div
   1.131 @@ -1857,7 +1857,7 @@
   1.132        done
   1.133      moreover with `c \<noteq> 0` divmod_int_rel_div_mod have "divmod_int_rel b c (b div c, b mod c)" by auto
   1.134      ultimately have "divmod_int_rel (a * b) (a * c) (b div c, a * (b mod c))" .
   1.135 -    from this show ?thesis by (rule divmod_int_rel_div)
   1.136 +    from this show ?thesis by (rule div_int_unique)
   1.137    qed
   1.138  qed auto
   1.139  
   1.140 @@ -1871,7 +1871,7 @@
   1.141    case False with assms posDivAlg_correct
   1.142      have "divmod_int_rel k l (fst (posDivAlg k l), snd (posDivAlg k l))"
   1.143      by simp
   1.144 -  from divmod_int_rel_div [OF this] divmod_int_rel_mod [OF this]
   1.145 +  from div_int_unique [OF this] mod_int_unique [OF this]
   1.146    show ?thesis by simp
   1.147  qed
   1.148  
   1.149 @@ -1884,7 +1884,7 @@
   1.150    from assms negDivAlg_correct
   1.151      have "divmod_int_rel k l (fst (negDivAlg k l), snd (negDivAlg k l))"
   1.152      by simp
   1.153 -  from divmod_int_rel_div [OF this] divmod_int_rel_mod [OF this]
   1.154 +  from div_int_unique [OF this] mod_int_unique [OF this]
   1.155    show ?thesis by simp
   1.156  qed
   1.157  
   1.158 @@ -1951,13 +1951,13 @@
   1.159  
   1.160  lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"
   1.161  apply (case_tac "b = 0", simp)
   1.162 -apply (force simp add: divmod_int_rel_div_mod [THEN zmult2_lemma, THEN divmod_int_rel_div])
   1.163 +apply (force simp add: divmod_int_rel_div_mod [THEN zmult2_lemma, THEN div_int_unique])
   1.164  done
   1.165  
   1.166  lemma zmod_zmult2_eq:
   1.167       "(0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b"
   1.168  apply (case_tac "b = 0", simp)
   1.169 -apply (force simp add: divmod_int_rel_div_mod [THEN zmult2_lemma, THEN divmod_int_rel_mod])
   1.170 +apply (force simp add: divmod_int_rel_div_mod [THEN zmult2_lemma, THEN mod_int_unique])
   1.171  done
   1.172  
   1.173  lemma div_pos_geq: