src/HOL/Euclidean_Division.thy
 changeset 66816 212a3334e7da parent 66814 a24cde9588bb child 66817 0b12755ccbb2
```     1.1 --- a/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:22 2017 +0200
1.2 +++ b/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:22 2017 +0200
1.3 @@ -704,7 +704,7 @@
1.4
1.5  subsection \<open>Euclidean division on @{typ nat}\<close>
1.6
1.7 -instantiation nat :: unique_euclidean_semiring
1.8 +instantiation nat :: normalization_semidom
1.9  begin
1.10
1.11  definition normalize_nat :: "nat \<Rightarrow> nat"
1.12 @@ -718,15 +718,23 @@
1.13    "unit_factor (Suc n) = 1"
1.15
1.16 +definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
1.17 +  where "m div n = (if n = 0 then 0 else Max {k::nat. k * n \<le> m})"
1.18 +
1.19 +instance
1.20 +  by standard (auto simp add: divide_nat_def ac_simps unit_factor_nat_def intro: Max_eqI)
1.21 +
1.22 +end
1.23 +
1.24 +instantiation nat :: unique_euclidean_semiring
1.25 +begin
1.26 +
1.27  definition euclidean_size_nat :: "nat \<Rightarrow> nat"
1.28    where [simp]: "euclidean_size_nat = id"
1.29
1.30  definition uniqueness_constraint_nat :: "nat \<Rightarrow> nat \<Rightarrow> bool"
1.31    where [simp]: "uniqueness_constraint_nat = \<top>"
1.32
1.33 -definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
1.34 -  where "m div n = (if n = 0 then 0 else Max {k::nat. k * n \<le> m})"
1.35 -
1.36  definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
1.37    where "m mod n = m - (m div n * (n::nat))"
1.38
1.39 @@ -757,15 +765,11 @@
1.40      finally show ?thesis
1.41        using False by (simp add: divide_nat_def ac_simps)
1.42    qed
1.43 -  show "n div 0 = 0"
1.44 -    by (simp add: divide_nat_def)
1.45    have less_eq: "m div n * n \<le> m"
1.46      by (auto simp add: mult_div_unfold ac_simps intro: Max.boundedI)
1.47    then show "m div n * n + m mod n = m"
1.49    assume "n \<noteq> 0"
1.50 -  show "m * n div n = m"
1.51 -    using \<open>n \<noteq> 0\<close> by (auto simp add: divide_nat_def ac_simps intro: Max_eqI)
1.52    show "euclidean_size (m mod n) < euclidean_size n"
1.53    proof -
1.54      have "m < Suc (m div n) * n"
1.55 @@ -805,7 +809,7 @@
1.56      with \<open>n \<noteq> 0\<close> ex fin show ?thesis
1.57        by (auto simp add: divide_nat_def Max_eq_iff)
1.58    qed
1.60 +qed simp_all
1.61
1.62  end
1.63
1.64 @@ -1329,6 +1333,186 @@
1.65  qed
1.66
1.67
1.68 +subsection \<open>Euclidean division on @{typ int}\<close>
1.69 +
1.70 +instantiation int :: normalization_semidom
1.71 +begin
1.72 +
1.73 +definition normalize_int :: "int \<Rightarrow> int"
1.74 +  where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
1.75 +
1.76 +definition unit_factor_int :: "int \<Rightarrow> int"
1.77 +  where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
1.78 +
1.79 +definition divide_int :: "int \<Rightarrow> int \<Rightarrow> int"
1.80 +  where "k div l = (if l = 0 then 0
1.81 +    else if sgn k = sgn l
1.82 +      then int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
1.83 +      else - int (nat \<bar>k\<bar> div nat \<bar>l\<bar> + of_bool (\<not> l dvd k)))"
1.84 +
1.85 +lemma divide_int_unfold:
1.86 +  "(sgn k * int m) div (sgn l * int n) =
1.87 +   (if sgn l = 0 \<or> sgn k = 0 \<or> n = 0 then 0
1.88 +    else if sgn k = sgn l
1.89 +      then int (m div n)
1.90 +      else - int (m div n + of_bool (\<not> n dvd m)))"
1.91 +  by (auto simp add: divide_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
1.92 +    nat_mult_distrib dvd_int_iff)
1.93 +
1.94 +instance proof
1.95 +  fix k :: int show "k div 0 = 0"
1.96 +  by (simp add: divide_int_def)
1.97 +next
1.98 +  fix k l :: int
1.99 +  assume "l \<noteq> 0"
1.100 +  obtain n m and s t where k: "k = sgn s * int n" and l: "l = sgn t * int m"
1.101 +    by (blast intro: int_sgnE elim: that)
1.102 +  then have "k * l = sgn (s * t) * int (n * m)"
1.103 +    by (simp add: ac_simps sgn_mult)
1.104 +  with k l \<open>l \<noteq> 0\<close> show "k * l div l = k"
1.105 +    by (simp only: divide_int_unfold)
1.106 +      (auto simp add: algebra_simps sgn_mult sgn_1_pos sgn_0_0)
1.107 +qed (auto simp add: sgn_mult mult_sgn_abs abs_eq_iff')
1.108 +
1.109 +end
1.110 +
1.111 +instantiation int :: unique_euclidean_ring
1.112 +begin
1.113 +
1.114 +definition euclidean_size_int :: "int \<Rightarrow> nat"
1.115 +  where [simp]: "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
1.116 +
1.117 +definition uniqueness_constraint_int :: "int \<Rightarrow> int \<Rightarrow> bool"
1.118 +  where [simp]: "uniqueness_constraint_int k l \<longleftrightarrow> unit_factor k = unit_factor l"
1.119 +
1.120 +definition modulo_int :: "int \<Rightarrow> int \<Rightarrow> int"
1.121 +  where "k mod l = (if l = 0 then k
1.122 +    else if sgn k = sgn l
1.123 +      then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
1.124 +      else sgn l * (\<bar>l\<bar> * of_bool (\<not> l dvd k) - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
1.125 +
1.126 +lemma modulo_int_unfold:
1.127 +  "(sgn k * int m) mod (sgn l * int n) =
1.128 +   (if sgn l = 0 \<or> sgn k = 0 \<or> n = 0 then sgn k * int m
1.129 +    else if sgn k = sgn l
1.130 +      then sgn l * int (m mod n)
1.131 +      else sgn l * (int (n * of_bool (\<not> n dvd m)) - int (m mod n)))"
1.132 +  by (auto simp add: modulo_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
1.133 +    nat_mult_distrib dvd_int_iff)
1.134 +
1.135 +lemma abs_mod_less:
1.136 +  "\<bar>k mod l\<bar> < \<bar>l\<bar>" if "l \<noteq> 0" for k l :: int
1.137 +proof -
1.138 +  obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m"
1.139 +    by (blast intro: int_sgnE elim: that)
1.140 +  with that show ?thesis
1.141 +    by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg
1.142 +      abs_mult mod_greater_zero_iff_not_dvd)
1.143 +qed
1.144 +
1.145 +lemma sgn_mod:
1.146 +  "sgn (k mod l) = sgn l" if "l \<noteq> 0" "\<not> l dvd k" for k l :: int
1.147 +proof -
1.148 +  obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m"
1.149 +    by (blast intro: int_sgnE elim: that)
1.150 +  with that show ?thesis
1.151 +    by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg
1.152 +      sgn_mult mod_eq_0_iff_dvd int_dvd_iff)
1.153 +qed
1.154 +
1.155 +instance proof
1.156 +  fix k l :: int
1.157 +  obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m"
1.158 +    by (blast intro: int_sgnE elim: that)
1.159 +  then show "k div l * l + k mod l = k"
1.160 +    by (auto simp add: divide_int_unfold modulo_int_unfold algebra_simps dest!: sgn_not_eq_imp)
1.162 +         distrib_left [symmetric] minus_mult_right
1.163 +         del: of_nat_mult minus_mult_right [symmetric])
1.164 +next
1.165 +  fix l q r :: int
1.166 +  obtain n m and s t
1.167 +     where l: "l = sgn s * int n" and q: "q = sgn t * int m"
1.168 +    by (blast intro: int_sgnE elim: that)
1.169 +  assume \<open>l \<noteq> 0\<close>
1.170 +  with l have "s \<noteq> 0" and "n > 0"
1.171 +    by (simp_all add: sgn_0_0)
1.172 +  assume "uniqueness_constraint r l"
1.173 +  moreover have "r = sgn r * \<bar>r\<bar>"
1.174 +    by (simp add: sgn_mult_abs)
1.175 +  moreover define u where "u = nat \<bar>r\<bar>"
1.176 +  ultimately have "r = sgn l * int u"
1.177 +    by simp
1.178 +  with l \<open>n > 0\<close> have r: "r = sgn s * int u"
1.179 +    by (simp add: sgn_mult)
1.180 +  assume "euclidean_size r < euclidean_size l"
1.181 +  with l r \<open>s \<noteq> 0\<close> have "u < n"
1.182 +    by (simp add: abs_mult)
1.183 +  show "(q * l + r) div l = q"
1.184 +  proof (cases "q = 0 \<or> r = 0")
1.185 +    case True
1.186 +    then show ?thesis
1.187 +    proof
1.188 +      assume "q = 0"
1.189 +      then show ?thesis
1.190 +        using l r \<open>u < n\<close> by (simp add: divide_int_unfold)
1.191 +    next
1.192 +      assume "r = 0"
1.193 +      from \<open>r = 0\<close> have *: "q * l + r = sgn (t * s) * int (n * m)"
1.194 +        using q l by (simp add: ac_simps sgn_mult)
1.195 +      from \<open>s \<noteq> 0\<close> \<open>n > 0\<close> show ?thesis
1.196 +        by (simp only: *, simp only: q l divide_int_unfold)
1.197 +          (auto simp add: sgn_mult sgn_0_0 sgn_1_pos)
1.198 +    qed
1.199 +  next
1.200 +    case False
1.201 +    with q r have "t \<noteq> 0" and "m > 0" and "s \<noteq> 0" and "u > 0"
1.202 +      by (simp_all add: sgn_0_0)
1.203 +    moreover from \<open>0 < m\<close> \<open>u < n\<close> have "u \<le> m * n"
1.204 +      using mult_le_less_imp_less [of 1 m u n] by simp
1.205 +    ultimately have *: "q * l + r = sgn (s * t)
1.206 +      * int (if t < 0 then m * n - u else m * n + u)"
1.207 +      using l q r
1.208 +      by (simp add: sgn_mult algebra_simps of_nat_diff)
1.209 +    have "(m * n - u) div n = m - 1" if "u > 0"
1.210 +      using \<open>0 < m\<close> \<open>u < n\<close> that
1.211 +      by (auto intro: div_nat_eqI simp add: algebra_simps)
1.212 +    moreover have "n dvd m * n - u \<longleftrightarrow> n dvd u"
1.213 +      using \<open>u \<le> m * n\<close> dvd_diffD1 [of n "m * n" u]
1.214 +      by auto
1.215 +    ultimately show ?thesis
1.216 +      using \<open>s \<noteq> 0\<close> \<open>m > 0\<close> \<open>u > 0\<close> \<open>u < n\<close> \<open>u \<le> m * n\<close>
1.217 +      by (simp only: *, simp only: l q divide_int_unfold)
1.218 +        (auto simp add: sgn_mult sgn_0_0 sgn_1_pos algebra_simps dest: dvd_imp_le)
1.219 +  qed
1.220 +qed (use mult_le_mono2 [of 1] in \<open>auto simp add: abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>)
1.221 +
1.222 +end
1.223 +
1.224 +lemma pos_mod_bound [simp]:
1.225 +  "k mod l < l" if "l > 0" for k l :: int
1.226 +proof -
1.227 +  obtain m and s where "k = sgn s * int m"
1.228 +    by (blast intro: int_sgnE elim: that)
1.229 +  moreover from that obtain n where "l = sgn 1 * int n"
1.230 +    by (cases l) auto
1.231 +  ultimately show ?thesis
1.232 +    using that by (simp only: modulo_int_unfold)
1.234 +qed
1.235 +
1.236 +lemma pos_mod_sign [simp]:
1.237 +  "0 \<le> k mod l" if "l > 0" for k l :: int
1.238 +proof -
1.239 +  obtain m and s where "k = sgn s * int m"
1.240 +    by (blast intro: int_sgnE elim: that)
1.241 +  moreover from that obtain n where "l = sgn 1 * int n"
1.242 +    by (cases l) auto
1.243 +  ultimately show ?thesis
1.244 +    using that by (simp only: modulo_int_unfold) simp
1.245 +qed
1.246 +
1.247 +
1.248  subsection \<open>Code generation\<close>
1.249
1.250  code_identifier
```