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.14    by (simp_all add: unit_factor_nat_def)
    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.48      by (simp add: modulo_nat_def)
    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.59 -qed (simp_all add: unit_factor_nat_def)
    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.161 +       (simp_all add: of_nat_mult [symmetric] of_nat_add [symmetric]
   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.233 +      (simp add: mod_greater_zero_iff_not_dvd)
   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