src/HOL/Divides.thy
changeset 64635 255741c5f862
parent 64630 96015aecfeba
child 64715 33d5fa0ce6e5
     1.1 --- a/src/HOL/Divides.thy	Thu Dec 22 08:43:30 2016 +0100
     1.2 +++ b/src/HOL/Divides.thy	Thu Dec 22 10:42:08 2016 +0100
     1.3 @@ -828,18 +828,18 @@
     1.4    @{term "q::nat"}(uotient) and @{term "r::nat"}(emainder).
     1.5  \<close>
     1.6  
     1.7 -definition divmod_nat_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where
     1.8 -  "divmod_nat_rel m n qr \<longleftrightarrow>
     1.9 -    m = fst qr * n + snd qr \<and>
    1.10 -      (if n = 0 then fst qr = 0 else if n > 0 then 0 \<le> snd qr \<and> snd qr < n else n < snd qr \<and> snd qr \<le> 0)"
    1.11 -
    1.12 -text \<open>@{const divmod_nat_rel} is total:\<close>
    1.13 -
    1.14 -qualified lemma divmod_nat_rel_ex:
    1.15 -  obtains q r where "divmod_nat_rel m n (q, r)"
    1.16 +inductive eucl_rel_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool"
    1.17 +  where eucl_rel_nat_by0: "eucl_rel_nat m 0 (0, m)"
    1.18 +  | eucl_rel_natI: "r < n \<Longrightarrow> m = q * n + r \<Longrightarrow> eucl_rel_nat m n (q, r)"
    1.19 +
    1.20 +text \<open>@{const eucl_rel_nat} is total:\<close>
    1.21 +
    1.22 +qualified lemma eucl_rel_nat_ex:
    1.23 +  obtains q r where "eucl_rel_nat m n (q, r)"
    1.24  proof (cases "n = 0")
    1.25 -  case True  with that show thesis
    1.26 -    by (auto simp add: divmod_nat_rel_def)
    1.27 +  case True
    1.28 +  with that eucl_rel_nat_by0 show thesis
    1.29 +    by blast
    1.30  next
    1.31    case False
    1.32    have "\<exists>q r. m = q * n + r \<and> r < n"
    1.33 @@ -864,74 +864,92 @@
    1.34        with \<open>n \<noteq> 0\<close> show ?thesis by blast
    1.35      qed
    1.36    qed
    1.37 -  with that show thesis
    1.38 -    using \<open>n \<noteq> 0\<close> by (auto simp add: divmod_nat_rel_def)
    1.39 +  with that \<open>n \<noteq> 0\<close> eucl_rel_natI show thesis
    1.40 +    by blast
    1.41  qed
    1.42  
    1.43 -text \<open>@{const divmod_nat_rel} is injective:\<close>
    1.44 -
    1.45 -qualified lemma divmod_nat_rel_unique:
    1.46 -  assumes "divmod_nat_rel m n qr"
    1.47 -    and "divmod_nat_rel m n qr'"
    1.48 -  shows "qr = qr'"
    1.49 +text \<open>@{const eucl_rel_nat} is injective:\<close>
    1.50 +
    1.51 +qualified lemma eucl_rel_nat_unique_div:
    1.52 +  assumes "eucl_rel_nat m n (q, r)"
    1.53 +    and "eucl_rel_nat m n (q', r')"
    1.54 +  shows "q = q'"
    1.55  proof (cases "n = 0")
    1.56    case True with assms show ?thesis
    1.57 -    by (cases qr, cases qr')
    1.58 -      (simp add: divmod_nat_rel_def)
    1.59 +    by (auto elim: eucl_rel_nat.cases)
    1.60  next
    1.61    case False
    1.62 -  have aux: "\<And>q r q' r'. q' * n + r' = q * n + r \<Longrightarrow> r < n \<Longrightarrow> q' \<le> (q::nat)"
    1.63 -  apply (rule leI)
    1.64 -  apply (subst less_iff_Suc_add)
    1.65 -  apply (auto simp add: add_mult_distrib)
    1.66 -  done
    1.67 -  from \<open>n \<noteq> 0\<close> assms have *: "fst qr = fst qr'"
    1.68 -    by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym split: if_splits)
    1.69 -  with assms have "snd qr = snd qr'"
    1.70 -    by (simp add: divmod_nat_rel_def)
    1.71 -  with * show ?thesis by (cases qr, cases qr') simp
    1.72 +  have *: "q' \<le> q" if "q' * n + r' = q * n + r" "r < n" for q r q' r' :: nat
    1.73 +  proof (rule ccontr)
    1.74 +    assume "\<not> q' \<le> q"
    1.75 +    then have "q < q'"
    1.76 +      by (simp add: not_le)
    1.77 +    with that show False
    1.78 +      by (auto simp add: less_iff_Suc_add algebra_simps)
    1.79 +  qed
    1.80 +  from \<open>n \<noteq> 0\<close> assms show ?thesis
    1.81 +    by (auto intro: order_antisym elim: eucl_rel_nat.cases dest: * sym split: if_splits)
    1.82 +qed
    1.83 +
    1.84 +qualified lemma eucl_rel_nat_unique_mod:
    1.85 +  assumes "eucl_rel_nat m n (q, r)"
    1.86 +    and "eucl_rel_nat m n (q', r')"
    1.87 +  shows "r = r'"
    1.88 +proof -
    1.89 +  from assms have "q' = q"
    1.90 +    by (auto intro: eucl_rel_nat_unique_div)
    1.91 +  with assms show ?thesis
    1.92 +    by (auto elim!: eucl_rel_nat.cases)
    1.93  qed
    1.94  
    1.95  text \<open>
    1.96    We instantiate divisibility on the natural numbers by
    1.97 -  means of @{const divmod_nat_rel}:
    1.98 +  means of @{const eucl_rel_nat}:
    1.99  \<close>
   1.100  
   1.101  qualified definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
   1.102 -  "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
   1.103 -
   1.104 -qualified lemma divmod_nat_rel_divmod_nat:
   1.105 -  "divmod_nat_rel m n (divmod_nat m n)"
   1.106 +  "divmod_nat m n = (THE qr. eucl_rel_nat m n qr)"
   1.107 +
   1.108 +qualified lemma eucl_rel_nat_divmod_nat:
   1.109 +  "eucl_rel_nat m n (divmod_nat m n)"
   1.110  proof -
   1.111 -  from divmod_nat_rel_ex
   1.112 -    obtain qr where rel: "divmod_nat_rel m n qr" .
   1.113 +  from eucl_rel_nat_ex
   1.114 +    obtain q r where rel: "eucl_rel_nat m n (q, r)" .
   1.115    then show ?thesis
   1.116 -  by (auto simp add: divmod_nat_def intro: theI elim: divmod_nat_rel_unique)
   1.117 +    by (auto simp add: divmod_nat_def intro: theI
   1.118 +      elim: eucl_rel_nat_unique_div eucl_rel_nat_unique_mod)
   1.119  qed
   1.120  
   1.121  qualified lemma divmod_nat_unique:
   1.122 -  assumes "divmod_nat_rel m n qr"
   1.123 -  shows "divmod_nat m n = qr"
   1.124 -  using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
   1.125 -
   1.126 -qualified lemma divmod_nat_zero: "divmod_nat m 0 = (0, m)"
   1.127 -  by (simp add: divmod_nat_unique divmod_nat_rel_def)
   1.128 -
   1.129 -qualified lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)"
   1.130 -  by (simp add: divmod_nat_unique divmod_nat_rel_def)
   1.131 -
   1.132 -qualified lemma divmod_nat_base: "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
   1.133 -  by (simp add: divmod_nat_unique divmod_nat_rel_def)
   1.134 +  "divmod_nat m n = (q, r)" if "eucl_rel_nat m n (q, r)"
   1.135 +  using that
   1.136 +  by (auto simp add: divmod_nat_def intro: eucl_rel_nat_divmod_nat elim: eucl_rel_nat_unique_div eucl_rel_nat_unique_mod)
   1.137 +
   1.138 +qualified lemma divmod_nat_zero:
   1.139 +  "divmod_nat m 0 = (0, m)"
   1.140 +  by (rule divmod_nat_unique) (fact eucl_rel_nat_by0)
   1.141 +
   1.142 +qualified lemma divmod_nat_zero_left:
   1.143 +  "divmod_nat 0 n = (0, 0)"
   1.144 +  by (rule divmod_nat_unique) 
   1.145 +    (cases n, auto intro: eucl_rel_nat_by0 eucl_rel_natI)
   1.146 +
   1.147 +qualified lemma divmod_nat_base:
   1.148 +  "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
   1.149 +  by (rule divmod_nat_unique) 
   1.150 +    (cases n, auto intro: eucl_rel_nat_by0 eucl_rel_natI)
   1.151  
   1.152  qualified lemma divmod_nat_step:
   1.153    assumes "0 < n" and "n \<le> m"
   1.154 -  shows "divmod_nat m n = apfst Suc (divmod_nat (m - n) n)"
   1.155 +  shows "divmod_nat m n =
   1.156 +    (Suc (fst (divmod_nat (m - n) n)), snd (divmod_nat (m - n) n))"
   1.157  proof (rule divmod_nat_unique)
   1.158 -  have "divmod_nat_rel (m - n) n (divmod_nat (m - n) n)"
   1.159 -    by (fact divmod_nat_rel_divmod_nat)
   1.160 -  then show "divmod_nat_rel m n (apfst Suc (divmod_nat (m - n) n))"
   1.161 -    unfolding divmod_nat_rel_def using assms
   1.162 -      by (auto split: if_splits simp add: algebra_simps)
   1.163 +  have "eucl_rel_nat (m - n) n (divmod_nat (m - n) n)"
   1.164 +    by (fact eucl_rel_nat_divmod_nat)
   1.165 +  then show "eucl_rel_nat m n (Suc
   1.166 +    (fst (divmod_nat (m - n) n)), snd (divmod_nat (m - n) n))"
   1.167 +    using assms
   1.168 +      by (auto split: if_splits intro: eucl_rel_natI elim!: eucl_rel_nat.cases simp add: algebra_simps)
   1.169  qed
   1.170  
   1.171  end
   1.172 @@ -969,19 +987,19 @@
   1.173    by (simp add: prod_eq_iff)
   1.174  
   1.175  lemma div_nat_unique:
   1.176 -  assumes "divmod_nat_rel m n (q, r)"
   1.177 +  assumes "eucl_rel_nat m n (q, r)"
   1.178    shows "m div n = q"
   1.179    using assms
   1.180    by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
   1.181  
   1.182  lemma mod_nat_unique:
   1.183 -  assumes "divmod_nat_rel m n (q, r)"
   1.184 +  assumes "eucl_rel_nat m n (q, r)"
   1.185    shows "m mod n = r"
   1.186    using assms
   1.187    by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
   1.188  
   1.189 -lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
   1.190 -  using Divides.divmod_nat_rel_divmod_nat
   1.191 +lemma eucl_rel_nat: "eucl_rel_nat m n (m div n, m mod n)"
   1.192 +  using Divides.eucl_rel_nat_divmod_nat
   1.193    by (simp add: divmod_nat_div_mod)
   1.194  
   1.195  text \<open>The ''recursion'' equations for @{const divide} and @{const modulo}\<close>
   1.196 @@ -1014,22 +1032,21 @@
   1.197    fixes m n :: nat
   1.198    assumes "n > 0"
   1.199    shows "m mod n < n"
   1.200 -  using assms divmod_nat_rel [of m n] unfolding divmod_nat_rel_def
   1.201 -  by (auto split: if_splits)
   1.202 +  using assms eucl_rel_nat [of m n]
   1.203 +    by (auto elim: eucl_rel_nat.cases)
   1.204  
   1.205  lemma mod_le_divisor [simp]:
   1.206    fixes m n :: nat
   1.207    assumes "n > 0"
   1.208    shows "m mod n \<le> n"
   1.209 -proof (rule less_imp_le)
   1.210 -  from assms show "m mod n < n"
   1.211 -    by simp
   1.212 -qed
   1.213 +  using assms eucl_rel_nat [of m n]
   1.214 +    by (auto elim: eucl_rel_nat.cases)
   1.215  
   1.216  instance proof
   1.217    fix m n :: nat
   1.218    show "m div n * n + m mod n = m"
   1.219 -    using divmod_nat_rel [of m n] by (simp add: divmod_nat_rel_def)
   1.220 +    using eucl_rel_nat [of m n]
   1.221 +    by (auto elim: eucl_rel_nat.cases)
   1.222  next
   1.223    fix n :: nat show "n div 0 = 0"
   1.224      by (simp add: div_nat_def Divides.divmod_nat_zero)
   1.225 @@ -1037,7 +1054,7 @@
   1.226    fix m n :: nat
   1.227    assume "n \<noteq> 0"
   1.228    then show "m * n div n = m"
   1.229 -    by (auto simp add: divmod_nat_rel_def intro: div_nat_unique [of _ _ _ 0])
   1.230 +    by (auto intro!: eucl_rel_natI div_nat_unique [of _ _ _ 0])
   1.231  qed (simp_all add: unit_factor_nat_def)
   1.232  
   1.233  end
   1.234 @@ -1051,11 +1068,20 @@
   1.235  next
   1.236    fix m n q :: nat
   1.237    assume "m \<noteq> 0"
   1.238 -  then have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))"
   1.239 -    using div_mult_mod_eq [of n q]
   1.240 -    by (auto simp add: divmod_nat_rel_def algebra_simps distrib_left [symmetric] simp del: distrib_left)
   1.241 -  then show "(m * n) div (m * q) = n div q"
   1.242 -    by (rule div_nat_unique)
   1.243 +  show "(m * n) div (m * q) = n div q"
   1.244 +  proof (cases "q = 0")
   1.245 +    case True
   1.246 +    then show ?thesis
   1.247 +      by simp
   1.248 +  next
   1.249 +    case False
   1.250 +    show ?thesis
   1.251 +    proof (rule div_nat_unique [of _ _ _ "m * (n mod q)"])
   1.252 +      show "eucl_rel_nat (m * n) (m * q) (n div q, m * (n mod q))"
   1.253 +        by (rule eucl_rel_natI)
   1.254 +          (use \<open>m \<noteq> 0\<close> \<open>q \<noteq> 0\<close> div_mult_mod_eq [of n q] in \<open>auto simp add: algebra_simps distrib_left [symmetric]\<close>)
   1.255 +    qed          
   1.256 +  qed
   1.257  qed
   1.258  
   1.259  lemma div_by_Suc_0 [simp]:
   1.260 @@ -1187,31 +1213,33 @@
   1.261  
   1.262  subsubsection \<open>Quotient and Remainder\<close>
   1.263  
   1.264 -lemma divmod_nat_rel_mult1_eq:
   1.265 -  "divmod_nat_rel b c (q, r)
   1.266 -   \<Longrightarrow> divmod_nat_rel (a * b) c (a * q + a * r div c, a * r mod c)"
   1.267 -by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)
   1.268 -
   1.269  lemma div_mult1_eq:
   1.270    "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"
   1.271 -by (blast intro: divmod_nat_rel_mult1_eq [THEN div_nat_unique] divmod_nat_rel)
   1.272 -
   1.273 -lemma divmod_nat_rel_add1_eq:
   1.274 -  "divmod_nat_rel a c (aq, ar) \<Longrightarrow> divmod_nat_rel b c (bq, br)
   1.275 -   \<Longrightarrow> divmod_nat_rel (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
   1.276 -by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)
   1.277 +  by (cases "c = 0")
   1.278 +     (auto simp add: algebra_simps distrib_left [symmetric]
   1.279 +     intro!: div_nat_unique [of _ _ _ "(a * (b mod c)) mod c"] eucl_rel_natI)
   1.280 +
   1.281 +lemma eucl_rel_nat_add1_eq:
   1.282 +  "eucl_rel_nat a c (aq, ar) \<Longrightarrow> eucl_rel_nat b c (bq, br)
   1.283 +   \<Longrightarrow> eucl_rel_nat (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
   1.284 +  by (auto simp add: split_ifs algebra_simps elim!: eucl_rel_nat.cases intro: eucl_rel_nat_by0 eucl_rel_natI)
   1.285  
   1.286  (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
   1.287  lemma div_add1_eq:
   1.288 -  "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
   1.289 -by (blast intro: divmod_nat_rel_add1_eq [THEN div_nat_unique] divmod_nat_rel)
   1.290 -
   1.291 -lemma divmod_nat_rel_mult2_eq:
   1.292 -  assumes "divmod_nat_rel a b (q, r)"
   1.293 -  shows "divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
   1.294 -proof -
   1.295 -  { assume "r < b" and "0 < c"
   1.296 -    then have "b * (q mod c) + r < b * c"
   1.297 +  "(a + b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
   1.298 +by (blast intro: eucl_rel_nat_add1_eq [THEN div_nat_unique] eucl_rel_nat)
   1.299 +
   1.300 +lemma eucl_rel_nat_mult2_eq:
   1.301 +  assumes "eucl_rel_nat a b (q, r)"
   1.302 +  shows "eucl_rel_nat a (b * c) (q div c, b *(q mod c) + r)"
   1.303 +proof (cases "c = 0")
   1.304 +  case True
   1.305 +  with assms show ?thesis
   1.306 +    by (auto intro: eucl_rel_nat_by0 elim!: eucl_rel_nat.cases simp add: ac_simps)
   1.307 +next
   1.308 +  case False
   1.309 +  { assume "r < b"
   1.310 +    with False have "b * (q mod c) + r < b * c"
   1.311        apply (cut_tac m = q and n = c in mod_less_divisor)
   1.312        apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
   1.313        apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
   1.314 @@ -1219,15 +1247,15 @@
   1.315        done
   1.316      then have "r + b * (q mod c) < b * c"
   1.317        by (simp add: ac_simps)
   1.318 -  } with assms show ?thesis
   1.319 -    by (auto simp add: divmod_nat_rel_def algebra_simps add_mult_distrib2 [symmetric])
   1.320 +  } with assms False show ?thesis
   1.321 +    by (auto simp add: algebra_simps add_mult_distrib2 [symmetric] elim!: eucl_rel_nat.cases intro: eucl_rel_nat.intros)
   1.322  qed
   1.323  
   1.324  lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
   1.325 -by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])
   1.326 +by (force simp add: eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN div_nat_unique])
   1.327  
   1.328  lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
   1.329 -by (auto simp add: mult.commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_nat_unique])
   1.330 +by (auto simp add: mult.commute eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN mod_nat_unique])
   1.331  
   1.332  instantiation nat :: semiring_numeral_div
   1.333  begin
   1.334 @@ -1386,8 +1414,8 @@
   1.335    from A B show ?lhs ..
   1.336  next
   1.337    assume P: ?lhs
   1.338 -  then have "divmod_nat_rel m n (q, m - n * q)"
   1.339 -    unfolding divmod_nat_rel_def by (auto simp add: ac_simps)
   1.340 +  then have "eucl_rel_nat m n (q, m - n * q)"
   1.341 +    by (auto intro: eucl_rel_natI simp add: ac_simps)
   1.342    then have "m div n = q"
   1.343      by (rule div_nat_unique)
   1.344    then show ?rhs by simp
   1.345 @@ -1673,9 +1701,19 @@
   1.346  context
   1.347  begin
   1.348  
   1.349 -definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" \<comment> \<open>definition of quotient and remainder\<close>
   1.350 -  where "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
   1.351 -    (if 0 < b then 0 \<le> r \<and> r < b else if b < 0 then b < r \<and> r \<le> 0 else q = 0))"
   1.352 +inductive eucl_rel_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool"
   1.353 +  where eucl_rel_int_by0: "eucl_rel_int k 0 (0, k)"
   1.354 +  | eucl_rel_int_dividesI: "l \<noteq> 0 \<Longrightarrow> k = q * l \<Longrightarrow> eucl_rel_int k l (q, 0)"
   1.355 +  | eucl_rel_int_remainderI: "sgn r = sgn l \<Longrightarrow> \<bar>r\<bar> < \<bar>l\<bar>
   1.356 +      \<Longrightarrow> k = q * l + r \<Longrightarrow> eucl_rel_int k l (q, r)"
   1.357 +
   1.358 +lemma eucl_rel_int_iff:    
   1.359 +  "eucl_rel_int k l (q, r) \<longleftrightarrow> 
   1.360 +    k = l * q + r \<and>
   1.361 +     (if 0 < l then 0 \<le> r \<and> r < l else if l < 0 then l < r \<and> r \<le> 0 else q = 0)"
   1.362 +  by (cases "r = 0")
   1.363 +    (auto elim!: eucl_rel_int.cases intro: eucl_rel_int_by0 eucl_rel_int_dividesI eucl_rel_int_remainderI
   1.364 +    simp add: ac_simps sgn_1_pos sgn_1_neg)
   1.365  
   1.366  lemma unique_quotient_lemma:
   1.367    "b * q' + r' \<le> b * q + r \<Longrightarrow> 0 \<le> r' \<Longrightarrow> r' < b \<Longrightarrow> r < b \<Longrightarrow> q' \<le> (q::int)"
   1.368 @@ -1694,17 +1732,17 @@
   1.369    by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma) auto
   1.370  
   1.371  lemma unique_quotient:
   1.372 -  "divmod_int_rel a b (q, r) \<Longrightarrow> divmod_int_rel a b (q', r') \<Longrightarrow> q = q'"
   1.373 -apply (simp add: divmod_int_rel_def linorder_neq_iff split: if_split_asm)
   1.374 -apply (blast intro: order_antisym
   1.375 -             dest: order_eq_refl [THEN unique_quotient_lemma]
   1.376 -             order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
   1.377 -done
   1.378 +  "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> q = q'"
   1.379 +  apply (simp add: eucl_rel_int_iff linorder_neq_iff split: if_split_asm)
   1.380 +  apply (blast intro: order_antisym
   1.381 +    dest: order_eq_refl [THEN unique_quotient_lemma]
   1.382 +    order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
   1.383 +  done
   1.384  
   1.385  lemma unique_remainder:
   1.386 -  "divmod_int_rel a b (q, r) \<Longrightarrow> divmod_int_rel a b (q', r') \<Longrightarrow> r = r'"
   1.387 +  "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> r = r'"
   1.388  apply (subgoal_tac "q = q'")
   1.389 - apply (simp add: divmod_int_rel_def)
   1.390 + apply (simp add: eucl_rel_int_iff)
   1.391  apply (blast intro: unique_quotient)
   1.392  done
   1.393  
   1.394 @@ -1733,12 +1771,12 @@
   1.395        then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
   1.396        else sgn l * (\<bar>l\<bar> - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
   1.397  
   1.398 -lemma divmod_int_rel:
   1.399 -  "divmod_int_rel k l (k div l, k mod l)"
   1.400 +lemma eucl_rel_int:
   1.401 +  "eucl_rel_int k l (k div l, k mod l)"
   1.402  proof (cases k rule: int_cases3)
   1.403    case zero
   1.404    then show ?thesis
   1.405 -    by (simp add: divmod_int_rel_def divide_int_def modulo_int_def)
   1.406 +    by (simp add: eucl_rel_int_iff divide_int_def modulo_int_def)
   1.407  next
   1.408    case (pos n)
   1.409    then show ?thesis
   1.410 @@ -1746,7 +1784,7 @@
   1.411      by (cases l rule: int_cases3)
   1.412        (auto simp del: of_nat_mult of_nat_add
   1.413          simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
   1.414 -        divmod_int_rel_def divide_int_def modulo_int_def int_dvd_iff)
   1.415 +        eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
   1.416  next
   1.417    case (neg n)
   1.418    then show ?thesis
   1.419 @@ -1754,29 +1792,29 @@
   1.420      by (cases l rule: int_cases3)
   1.421        (auto simp del: of_nat_mult of_nat_add
   1.422          simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
   1.423 -        divmod_int_rel_def divide_int_def modulo_int_def int_dvd_iff)
   1.424 +        eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
   1.425  qed
   1.426  
   1.427  lemma divmod_int_unique:
   1.428 -  assumes "divmod_int_rel k l (q, r)"
   1.429 +  assumes "eucl_rel_int k l (q, r)"
   1.430    shows div_int_unique: "k div l = q" and mod_int_unique: "k mod l = r"
   1.431 -  using assms divmod_int_rel [of k l]
   1.432 +  using assms eucl_rel_int [of k l]
   1.433    using unique_quotient [of k l] unique_remainder [of k l]
   1.434    by auto
   1.435  
   1.436  instance proof
   1.437    fix k l :: int
   1.438    show "k div l * l + k mod l = k"
   1.439 -    using divmod_int_rel [of k l]
   1.440 -    unfolding divmod_int_rel_def by (simp add: ac_simps)
   1.441 +    using eucl_rel_int [of k l]
   1.442 +    unfolding eucl_rel_int_iff by (simp add: ac_simps)
   1.443  next
   1.444    fix k :: int show "k div 0 = 0"
   1.445 -    by (rule div_int_unique, simp add: divmod_int_rel_def)
   1.446 +    by (rule div_int_unique, simp add: eucl_rel_int_iff)
   1.447  next
   1.448    fix k l :: int
   1.449    assume "l \<noteq> 0"
   1.450    then show "k * l div l = k"
   1.451 -    by (auto simp add: divmod_int_rel_def ac_simps intro: div_int_unique [of _ _ _ 0])
   1.452 +    by (auto simp add: eucl_rel_int_iff ac_simps intro: div_int_unique [of _ _ _ 0])
   1.453  qed (simp_all add: sgn_mult mult_sgn_abs abs_sgn_eq)
   1.454  
   1.455  end
   1.456 @@ -1789,23 +1827,23 @@
   1.457  proof
   1.458    fix k l s :: int
   1.459    assume "l \<noteq> 0"
   1.460 -  then have "divmod_int_rel (k + s * l) l (s + k div l, k mod l)"
   1.461 -    using divmod_int_rel [of k l]
   1.462 -    unfolding divmod_int_rel_def by (auto simp: algebra_simps)
   1.463 +  then have "eucl_rel_int (k + s * l) l (s + k div l, k mod l)"
   1.464 +    using eucl_rel_int [of k l]
   1.465 +    unfolding eucl_rel_int_iff by (auto simp: algebra_simps)
   1.466    then show "(k + s * l) div l = s + k div l"
   1.467      by (rule div_int_unique)
   1.468  next
   1.469    fix k l s :: int
   1.470    assume "s \<noteq> 0"
   1.471 -  have "\<And>q r. divmod_int_rel k l (q, r)
   1.472 -    \<Longrightarrow> divmod_int_rel (s * k) (s * l) (q, s * r)"
   1.473 -    unfolding divmod_int_rel_def
   1.474 +  have "\<And>q r. eucl_rel_int k l (q, r)
   1.475 +    \<Longrightarrow> eucl_rel_int (s * k) (s * l) (q, s * r)"
   1.476 +    unfolding eucl_rel_int_iff
   1.477      by (rule linorder_cases [of 0 l])
   1.478        (use \<open>s \<noteq> 0\<close> in \<open>auto simp: algebra_simps
   1.479        mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
   1.480        mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff\<close>)
   1.481 -  then have "divmod_int_rel (s * k) (s * l) (k div l, s * (k mod l))"
   1.482 -    using divmod_int_rel [of k l] .
   1.483 +  then have "eucl_rel_int (s * k) (s * l) (k div l, s * (k mod l))"
   1.484 +    using eucl_rel_int [of k l] .
   1.485    then show "(s * k) div (s * l) = k div l"
   1.486      by (rule div_int_unique)
   1.487  qed
   1.488 @@ -1839,15 +1877,15 @@
   1.489    by (simp add: modulo_int_def int_dvd_iff)
   1.490  
   1.491  lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
   1.492 -  using divmod_int_rel [of a b]
   1.493 -  by (auto simp add: divmod_int_rel_def prod_eq_iff)
   1.494 +  using eucl_rel_int [of a b]
   1.495 +  by (auto simp add: eucl_rel_int_iff prod_eq_iff)
   1.496  
   1.497  lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
   1.498     and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]
   1.499  
   1.500  lemma neg_mod_conj: "b < (0::int) \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b"
   1.501 -  using divmod_int_rel [of a b]
   1.502 -  by (auto simp add: divmod_int_rel_def prod_eq_iff)
   1.503 +  using eucl_rel_int [of a b]
   1.504 +  by (auto simp add: eucl_rel_int_iff prod_eq_iff)
   1.505  
   1.506  lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
   1.507     and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
   1.508 @@ -1857,34 +1895,34 @@
   1.509  
   1.510  lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
   1.511  apply (rule div_int_unique)
   1.512 -apply (auto simp add: divmod_int_rel_def)
   1.513 +apply (auto simp add: eucl_rel_int_iff)
   1.514  done
   1.515  
   1.516  lemma div_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a div b = 0"
   1.517  apply (rule div_int_unique)
   1.518 -apply (auto simp add: divmod_int_rel_def)
   1.519 +apply (auto simp add: eucl_rel_int_iff)
   1.520  done
   1.521  
   1.522  lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a div b = -1"
   1.523  apply (rule div_int_unique)
   1.524 -apply (auto simp add: divmod_int_rel_def)
   1.525 +apply (auto simp add: eucl_rel_int_iff)
   1.526  done
   1.527  
   1.528  (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
   1.529  
   1.530  lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"
   1.531  apply (rule_tac q = 0 in mod_int_unique)
   1.532 -apply (auto simp add: divmod_int_rel_def)
   1.533 +apply (auto simp add: eucl_rel_int_iff)
   1.534  done
   1.535  
   1.536  lemma mod_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a mod b = a"
   1.537  apply (rule_tac q = 0 in mod_int_unique)
   1.538 -apply (auto simp add: divmod_int_rel_def)
   1.539 +apply (auto simp add: eucl_rel_int_iff)
   1.540  done
   1.541  
   1.542  lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"
   1.543  apply (rule_tac q = "-1" in mod_int_unique)
   1.544 -apply (auto simp add: divmod_int_rel_def)
   1.545 +apply (auto simp add: eucl_rel_int_iff)
   1.546  done
   1.547  
   1.548  text\<open>There is no \<open>mod_neg_pos_trivial\<close>.\<close>
   1.549 @@ -1893,22 +1931,22 @@
   1.550  subsubsection \<open>Laws for div and mod with Unary Minus\<close>
   1.551  
   1.552  lemma zminus1_lemma:
   1.553 -     "divmod_int_rel a b (q, r) ==> b \<noteq> 0
   1.554 -      ==> divmod_int_rel (-a) b (if r=0 then -q else -q - 1,
   1.555 +     "eucl_rel_int a b (q, r) ==> b \<noteq> 0
   1.556 +      ==> eucl_rel_int (-a) b (if r=0 then -q else -q - 1,
   1.557                            if r=0 then 0 else b-r)"
   1.558 -by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_diff_distrib)
   1.559 +by (force simp add: split_ifs eucl_rel_int_iff linorder_neq_iff right_diff_distrib)
   1.560  
   1.561  
   1.562  lemma zdiv_zminus1_eq_if:
   1.563       "b \<noteq> (0::int)
   1.564        ==> (-a) div b =
   1.565            (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
   1.566 -by (blast intro: divmod_int_rel [THEN zminus1_lemma, THEN div_int_unique])
   1.567 +by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN div_int_unique])
   1.568  
   1.569  lemma zmod_zminus1_eq_if:
   1.570       "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
   1.571  apply (case_tac "b = 0", simp)
   1.572 -apply (blast intro: divmod_int_rel [THEN zminus1_lemma, THEN mod_int_unique])
   1.573 +apply (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN mod_int_unique])
   1.574  done
   1.575  
   1.576  lemma zmod_zminus1_not_zero:
   1.577 @@ -2022,27 +2060,27 @@
   1.578  text\<open>proving (a*b) div c = a * (b div c) + a * (b mod c)\<close>
   1.579  
   1.580  lemma zmult1_lemma:
   1.581 -     "[| divmod_int_rel b c (q, r) |]
   1.582 -      ==> divmod_int_rel (a * b) c (a*q + a*r div c, a*r mod c)"
   1.583 -by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left ac_simps)
   1.584 +     "[| eucl_rel_int b c (q, r) |]
   1.585 +      ==> eucl_rel_int (a * b) c (a*q + a*r div c, a*r mod c)"
   1.586 +by (auto simp add: split_ifs eucl_rel_int_iff linorder_neq_iff distrib_left ac_simps)
   1.587  
   1.588  lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
   1.589  apply (case_tac "c = 0", simp)
   1.590 -apply (blast intro: divmod_int_rel [THEN zmult1_lemma, THEN div_int_unique])
   1.591 +apply (blast intro: eucl_rel_int [THEN zmult1_lemma, THEN div_int_unique])
   1.592  done
   1.593  
   1.594  text\<open>proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c)\<close>
   1.595  
   1.596  lemma zadd1_lemma:
   1.597 -     "[| divmod_int_rel a c (aq, ar);  divmod_int_rel b c (bq, br) |]
   1.598 -      ==> divmod_int_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
   1.599 -by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left)
   1.600 +     "[| eucl_rel_int a c (aq, ar);  eucl_rel_int b c (bq, br) |]
   1.601 +      ==> eucl_rel_int (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
   1.602 +by (force simp add: split_ifs eucl_rel_int_iff linorder_neq_iff distrib_left)
   1.603  
   1.604  (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
   1.605  lemma zdiv_zadd1_eq:
   1.606       "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
   1.607  apply (case_tac "c = 0", simp)
   1.608 -apply (blast intro: zadd1_lemma [OF divmod_int_rel divmod_int_rel] div_int_unique)
   1.609 +apply (blast intro: zadd1_lemma [OF eucl_rel_int eucl_rel_int] div_int_unique)
   1.610  done
   1.611  
   1.612  lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
   1.613 @@ -2095,9 +2133,9 @@
   1.614  apply simp
   1.615  done
   1.616  
   1.617 -lemma zmult2_lemma: "[| divmod_int_rel a b (q, r); 0 < c |]
   1.618 -      ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
   1.619 -by (auto simp add: mult.assoc divmod_int_rel_def linorder_neq_iff
   1.620 +lemma zmult2_lemma: "[| eucl_rel_int a b (q, r); 0 < c |]
   1.621 +      ==> eucl_rel_int a (b * c) (q div c, b*(q mod c) + r)"
   1.622 +by (auto simp add: mult.assoc eucl_rel_int_iff linorder_neq_iff
   1.623                     zero_less_mult_iff distrib_left [symmetric]
   1.624                     zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: if_split_asm)
   1.625  
   1.626 @@ -2105,14 +2143,14 @@
   1.627    fixes a b c :: int
   1.628    shows "0 \<le> c \<Longrightarrow> a div (b * c) = (a div b) div c"
   1.629  apply (case_tac "b = 0", simp)
   1.630 -apply (force simp add: le_less divmod_int_rel [THEN zmult2_lemma, THEN div_int_unique])
   1.631 +apply (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN div_int_unique])
   1.632  done
   1.633  
   1.634  lemma zmod_zmult2_eq:
   1.635    fixes a b c :: int
   1.636    shows "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
   1.637  apply (case_tac "b = 0", simp)
   1.638 -apply (force simp add: le_less divmod_int_rel [THEN zmult2_lemma, THEN mod_int_unique])
   1.639 +apply (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN mod_int_unique])
   1.640  done
   1.641  
   1.642  lemma div_pos_geq:
   1.643 @@ -2199,27 +2237,27 @@
   1.644  
   1.645  subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
   1.646  
   1.647 -lemma pos_divmod_int_rel_mult_2:
   1.648 +lemma pos_eucl_rel_int_mult_2:
   1.649    assumes "0 \<le> b"
   1.650 -  assumes "divmod_int_rel a b (q, r)"
   1.651 -  shows "divmod_int_rel (1 + 2*a) (2*b) (q, 1 + 2*r)"
   1.652 -  using assms unfolding divmod_int_rel_def by auto
   1.653 -
   1.654 -lemma neg_divmod_int_rel_mult_2:
   1.655 +  assumes "eucl_rel_int a b (q, r)"
   1.656 +  shows "eucl_rel_int (1 + 2*a) (2*b) (q, 1 + 2*r)"
   1.657 +  using assms unfolding eucl_rel_int_iff by auto
   1.658 +
   1.659 +lemma neg_eucl_rel_int_mult_2:
   1.660    assumes "b \<le> 0"
   1.661 -  assumes "divmod_int_rel (a + 1) b (q, r)"
   1.662 -  shows "divmod_int_rel (1 + 2*a) (2*b) (q, 2*r - 1)"
   1.663 -  using assms unfolding divmod_int_rel_def by auto
   1.664 +  assumes "eucl_rel_int (a + 1) b (q, r)"
   1.665 +  shows "eucl_rel_int (1 + 2*a) (2*b) (q, 2*r - 1)"
   1.666 +  using assms unfolding eucl_rel_int_iff by auto
   1.667  
   1.668  text\<open>computing div by shifting\<close>
   1.669  
   1.670  lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
   1.671 -  using pos_divmod_int_rel_mult_2 [OF _ divmod_int_rel]
   1.672 +  using pos_eucl_rel_int_mult_2 [OF _ eucl_rel_int]
   1.673    by (rule div_int_unique)
   1.674  
   1.675  lemma neg_zdiv_mult_2:
   1.676    assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
   1.677 -  using neg_divmod_int_rel_mult_2 [OF A divmod_int_rel]
   1.678 +  using neg_eucl_rel_int_mult_2 [OF A eucl_rel_int]
   1.679    by (rule div_int_unique)
   1.680  
   1.681  (* FIXME: add rules for negative numerals *)
   1.682 @@ -2240,14 +2278,14 @@
   1.683    fixes a b :: int
   1.684    assumes "0 \<le> a"
   1.685    shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"
   1.686 -  using pos_divmod_int_rel_mult_2 [OF assms divmod_int_rel]
   1.687 +  using pos_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
   1.688    by (rule mod_int_unique)
   1.689  
   1.690  lemma neg_zmod_mult_2:
   1.691    fixes a b :: int
   1.692    assumes "a \<le> 0"
   1.693    shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"
   1.694 -  using neg_divmod_int_rel_mult_2 [OF assms divmod_int_rel]
   1.695 +  using neg_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
   1.696    by (rule mod_int_unique)
   1.697  
   1.698  (* FIXME: add rules for negative numerals *)
   1.699 @@ -2452,19 +2490,19 @@
   1.700  text \<open>Simplify expresions in which div and mod combine numerical constants\<close>
   1.701  
   1.702  lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
   1.703 -  by (rule div_int_unique [of a b q r]) (simp add: divmod_int_rel_def)
   1.704 +  by (rule div_int_unique [of a b q r]) (simp add: eucl_rel_int_iff)
   1.705  
   1.706  lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
   1.707    by (rule div_int_unique [of a b q r],
   1.708 -    simp add: divmod_int_rel_def)
   1.709 +    simp add: eucl_rel_int_iff)
   1.710  
   1.711  lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
   1.712    by (rule mod_int_unique [of a b q r],
   1.713 -    simp add: divmod_int_rel_def)
   1.714 +    simp add: eucl_rel_int_iff)
   1.715  
   1.716  lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
   1.717    by (rule mod_int_unique [of a b q r],
   1.718 -    simp add: divmod_int_rel_def)
   1.719 +    simp add: eucl_rel_int_iff)
   1.720  
   1.721  lemma abs_div: "(y::int) dvd x \<Longrightarrow> \<bar>x div y\<bar> = \<bar>x\<bar> div \<bar>y\<bar>"
   1.722  by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)