more fundamental definition of div and mod on int
authorhaftmann
Sun Oct 08 22:28:22 2017 +0200 (19 months ago)
changeset 66816212a3334e7da
parent 66815 93c6632ddf44
child 66817 0b12755ccbb2
more fundamental definition of div and mod on int
src/HOL/Divides.thy
src/HOL/Euclidean_Division.thy
src/HOL/GCD.thy
src/HOL/Int.thy
src/HOL/Nat.thy
src/HOL/Parity.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Divides.thy	Sun Oct 08 22:28:22 2017 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sun Oct 08 22:28:22 2017 +0200
     1.3 @@ -326,12 +326,6 @@
     1.4    "m mod n = snd (divmod_nat m n)"
     1.5    by simp_all
     1.6  
     1.7 -
     1.8 -subsection \<open>Division on @{typ int}\<close>
     1.9 -
    1.10 -context
    1.11 -begin
    1.12 -
    1.13  inductive eucl_rel_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool"
    1.14    where eucl_rel_int_by0: "eucl_rel_int k 0 (0, k)"
    1.15    | eucl_rel_int_dividesI: "l \<noteq> 0 \<Longrightarrow> k = q * l \<Longrightarrow> eucl_rel_int k l (q, 0)"
    1.16 @@ -377,31 +371,6 @@
    1.17  apply (blast intro: unique_quotient)
    1.18  done
    1.19  
    1.20 -end
    1.21 -
    1.22 -instantiation int :: "{idom_modulo, normalization_semidom}"
    1.23 -begin
    1.24 -
    1.25 -definition normalize_int :: "int \<Rightarrow> int"
    1.26 -  where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
    1.27 -
    1.28 -definition unit_factor_int :: "int \<Rightarrow> int"
    1.29 -  where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
    1.30 -
    1.31 -definition divide_int :: "int \<Rightarrow> int \<Rightarrow> int"
    1.32 -  where "k div l = (if l = 0 \<or> k = 0 then 0
    1.33 -    else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
    1.34 -      then int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
    1.35 -      else
    1.36 -        if l dvd k then - int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
    1.37 -        else - int (Suc (nat \<bar>k\<bar> div nat \<bar>l\<bar>)))"
    1.38 -
    1.39 -definition modulo_int :: "int \<Rightarrow> int \<Rightarrow> int"
    1.40 -  where "k mod l = (if l = 0 then k else if l dvd k then 0
    1.41 -    else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
    1.42 -      then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
    1.43 -      else sgn l * (\<bar>l\<bar> - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
    1.44 -
    1.45  lemma eucl_rel_int:
    1.46    "eucl_rel_int k l (k div l, k mod l)"
    1.47  proof (cases k rule: int_cases3)
    1.48 @@ -433,42 +402,21 @@
    1.49    using unique_quotient [of k l] unique_remainder [of k l]
    1.50    by auto
    1.51  
    1.52 -instance proof
    1.53 -  fix k l :: int
    1.54 -  show "k div l * l + k mod l = k"
    1.55 -    using eucl_rel_int [of k l]
    1.56 -    unfolding eucl_rel_int_iff by (simp add: ac_simps)
    1.57 -next
    1.58 -  fix k :: int show "k div 0 = 0"
    1.59 -    by (rule div_int_unique, simp add: eucl_rel_int_iff)
    1.60 -next
    1.61 -  fix k l :: int
    1.62 -  assume "l \<noteq> 0"
    1.63 -  then show "k * l div l = k"
    1.64 -    by (auto simp add: eucl_rel_int_iff ac_simps intro: div_int_unique [of _ _ _ 0])
    1.65 -qed (auto simp add: sgn_mult mult_sgn_abs abs_eq_iff')
    1.66 -
    1.67 -end
    1.68 -
    1.69 -lemma is_unit_int:
    1.70 -  "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
    1.71 -  by auto
    1.72 -
    1.73 -lemma zdiv_int:
    1.74 -  "int (a div b) = int a div int b"
    1.75 -  by (simp add: divide_int_def)
    1.76 -
    1.77 -lemma zmod_int:
    1.78 -  "int (a mod b) = int a mod int b"
    1.79 -  by (simp add: modulo_int_def int_dvd_iff)
    1.80 -
    1.81  lemma div_abs_eq_div_nat:
    1.82    "\<bar>k\<bar> div \<bar>l\<bar> = int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)"
    1.83    by (simp add: divide_int_def)
    1.84  
    1.85  lemma mod_abs_eq_div_nat:
    1.86    "\<bar>k\<bar> mod \<bar>l\<bar> = int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)"
    1.87 -  by (simp add: modulo_int_def dvd_int_unfold_dvd_nat)
    1.88 +  by (simp add: modulo_int_def)
    1.89 +
    1.90 +lemma zdiv_int:
    1.91 +  "int (a div b) = int a div int b"
    1.92 +  by (simp add: divide_int_def sgn_1_pos)
    1.93 +
    1.94 +lemma zmod_int:
    1.95 +  "int (a mod b) = int a mod int b"
    1.96 +  by (simp add: modulo_int_def sgn_1_pos)
    1.97  
    1.98  lemma div_sgn_abs_cancel:
    1.99    fixes k l v :: int
   1.100 @@ -493,7 +441,7 @@
   1.101  next
   1.102    case False
   1.103    with assms have "(sgn k * \<bar>k\<bar>) div (sgn l * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
   1.104 -    by (simp add: div_sgn_abs_cancel)
   1.105 +    using div_sgn_abs_cancel [of l k l] by simp
   1.106    then show ?thesis
   1.107      by (simp add: sgn_mult_abs)
   1.108  qed
   1.109 @@ -502,12 +450,14 @@
   1.110    fixes k l :: int
   1.111    assumes "l dvd k"
   1.112    shows "k div l = (sgn k * sgn l) * (\<bar>k\<bar> div \<bar>l\<bar>)"
   1.113 -proof (cases "k = 0")
   1.114 +proof (cases "k = 0 \<or> l = 0")
   1.115    case True
   1.116    then show ?thesis
   1.117 -    by simp
   1.118 +    by auto
   1.119  next
   1.120    case False
   1.121 +  then have "k \<noteq> 0" and "l \<noteq> 0"
   1.122 +    by auto
   1.123    show ?thesis
   1.124    proof (cases "sgn l = sgn k")
   1.125      case True
   1.126 @@ -515,9 +465,12 @@
   1.127        by (simp add: div_eq_sgn_abs)
   1.128    next
   1.129      case False
   1.130 -    with \<open>k \<noteq> 0\<close> assms show ?thesis
   1.131 +    with \<open>k \<noteq> 0\<close> \<open>l \<noteq> 0\<close>
   1.132 +    have "sgn l * sgn k = - 1"
   1.133 +      by (simp add: sgn_if split: if_splits)
   1.134 +    with assms show ?thesis
   1.135        unfolding divide_int_def [of k l]
   1.136 -        by (auto simp add: zdiv_int)
   1.137 +      by (auto simp add: zdiv_int ac_simps)
   1.138    qed
   1.139  qed
   1.140  
   1.141 @@ -529,59 +482,14 @@
   1.142    using assms
   1.143    by (simp only: divide_int_def [of k l], auto simp add: not_less zdiv_int)
   1.144    
   1.145 -lemma sgn_mod:
   1.146 -  fixes k l :: int
   1.147 -  assumes "l \<noteq> 0" "\<not> l dvd k"
   1.148 -  shows "sgn (k mod l) = sgn l"
   1.149 -proof -
   1.150 -  from \<open>\<not> l dvd k\<close>
   1.151 -  have "k mod l \<noteq> 0"
   1.152 -    by (simp add: dvd_eq_mod_eq_0)
   1.153 -  show ?thesis
   1.154 -    using \<open>l \<noteq> 0\<close> \<open>\<not> l dvd k\<close>
   1.155 -    unfolding modulo_int_def [of k l]
   1.156 -    by (auto simp add: sgn_1_pos sgn_1_neg mod_greater_zero_iff_not_dvd nat_dvd_iff not_less
   1.157 -      zless_nat_eq_int_zless [symmetric] elim: nonpos_int_cases)
   1.158 -qed
   1.159 -
   1.160 -lemma abs_mod_less:
   1.161 -  fixes k l :: int
   1.162 -  assumes "l \<noteq> 0"
   1.163 -  shows "\<bar>k mod l\<bar> < \<bar>l\<bar>"
   1.164 -  using assms unfolding modulo_int_def [of k l]
   1.165 -  by (auto simp add: not_less int_dvd_iff mod_greater_zero_iff_not_dvd elim: pos_int_cases neg_int_cases nonneg_int_cases nonpos_int_cases)
   1.166 -
   1.167 -instantiation int :: unique_euclidean_ring
   1.168 -begin
   1.169 -
   1.170 -definition [simp]:
   1.171 -  "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
   1.172 -
   1.173 -definition [simp]:
   1.174 -  "uniqueness_constraint_int (k :: int) l \<longleftrightarrow> unit_factor k = unit_factor l"
   1.175 -  
   1.176 -instance proof
   1.177 -  fix l q r:: int
   1.178 -  assume "uniqueness_constraint r l"
   1.179 -    and "euclidean_size r < euclidean_size l"
   1.180 -  then have "sgn r = sgn l" and "\<bar>r\<bar> < \<bar>l\<bar>"
   1.181 -    by simp_all
   1.182 -  then have "eucl_rel_int (q * l + r) l (q, r)"
   1.183 -    by (rule eucl_rel_int_remainderI) simp
   1.184 -  then show "(q * l + r) div l = q"
   1.185 -    by (rule div_int_unique)
   1.186 -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.187 -
   1.188 -end
   1.189 -
   1.190  text\<open>Basic laws about division and remainder\<close>
   1.191  
   1.192  lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
   1.193    using eucl_rel_int [of a b]
   1.194    by (auto simp add: eucl_rel_int_iff prod_eq_iff)
   1.195  
   1.196 -lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
   1.197 -   and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]
   1.198 +lemmas pos_mod_sign = pos_mod_conj [THEN conjunct1]
   1.199 +   and pos_mod_bound = pos_mod_conj [THEN conjunct2]
   1.200  
   1.201  lemma neg_mod_conj: "b < (0::int) \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b"
   1.202    using eucl_rel_int [of a b]
   1.203 @@ -631,39 +539,6 @@
   1.204  
   1.205  text\<open>There is no \<open>mod_neg_pos_trivial\<close>.\<close>
   1.206  
   1.207 -instance int :: ring_parity
   1.208 -proof
   1.209 -  fix k l :: int
   1.210 -  show "k mod 2 = 1" if "\<not> 2 dvd k"
   1.211 -  proof (rule order_antisym)
   1.212 -    have "0 \<le> k mod 2" and "k mod 2 < 2"
   1.213 -      by auto
   1.214 -    moreover have "k mod 2 \<noteq> 0"
   1.215 -      using that by (simp add: dvd_eq_mod_eq_0)
   1.216 -    ultimately have "0 < k mod 2"
   1.217 -      by (simp only: less_le) simp
   1.218 -    then show "1 \<le> k mod 2"
   1.219 -      by simp
   1.220 -    from \<open>k mod 2 < 2\<close> show "k mod 2 \<le> 1"
   1.221 -      by (simp only: less_le) simp
   1.222 -  qed
   1.223 -qed (simp_all add: dvd_eq_mod_eq_0 divide_int_def)
   1.224 -
   1.225 -lemma even_diff_iff [simp]:
   1.226 -  "even (k - l) \<longleftrightarrow> even (k + l)" for k l :: int
   1.227 -  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
   1.228 -
   1.229 -lemma even_abs_add_iff [simp]:
   1.230 -  "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)" for k l :: int
   1.231 -  by (cases "k \<ge> 0") (simp_all add: ac_simps)
   1.232 -
   1.233 -lemma even_add_abs_iff [simp]:
   1.234 -  "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)" for k l :: int
   1.235 -  using even_abs_add_iff [of l k] by (simp add: ac_simps)
   1.236 -
   1.237 -lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
   1.238 -  by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric])
   1.239 -
   1.240  
   1.241  subsubsection \<open>Laws for div and mod with Unary Minus\<close>
   1.242  
   1.243 @@ -697,14 +572,14 @@
   1.244    by (simp add: mod_eq_0_iff_dvd)
   1.245  
   1.246  lemma zdiv_zminus2_eq_if:
   1.247 -     "b \<noteq> (0::int)
   1.248 +  "b \<noteq> (0::int)
   1.249        ==> a div (-b) =
   1.250            (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
   1.251 -by (simp add: zdiv_zminus1_eq_if div_minus_right)
   1.252 +  by (auto simp add: zdiv_zminus1_eq_if div_minus_right)
   1.253  
   1.254  lemma zmod_zminus2_eq_if:
   1.255 -     "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
   1.256 -by (simp add: zmod_zminus1_eq_if mod_minus_right)
   1.257 +  "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
   1.258 +  by (auto simp add: zmod_zminus1_eq_if mod_minus_right)
   1.259  
   1.260  
   1.261  subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
   1.262 @@ -1161,11 +1036,17 @@
   1.263  
   1.264  lemma minus_numeral_mod_numeral [simp]:
   1.265    "- numeral m mod numeral n = adjust_mod (numeral n) (snd (divmod m n) :: int)"
   1.266 -proof -
   1.267 -  have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
   1.268 -    using that by (simp only: snd_divmod modulo_int_def) auto
   1.269 +proof (cases "snd (divmod m n) = (0::int)")
   1.270 +  case True
   1.271    then show ?thesis
   1.272 -    by (auto simp add: split_def Let_def adjust_div_def divides_aux_def modulo_int_def)
   1.273 +    by (simp add: mod_eq_0_iff_dvd divides_aux_def)
   1.274 +next
   1.275 +  case False
   1.276 +  then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
   1.277 +    by (simp only: snd_divmod modulo_int_def) auto
   1.278 +  then show ?thesis
   1.279 +    by (simp add: divides_aux_def adjust_div_def)
   1.280 +      (simp add: divides_aux_def modulo_int_def)
   1.281  qed
   1.282  
   1.283  lemma numeral_div_minus_numeral [simp]:
   1.284 @@ -1179,11 +1060,17 @@
   1.285    
   1.286  lemma numeral_mod_minus_numeral [simp]:
   1.287    "numeral m mod - numeral n = - adjust_mod (numeral n) (snd (divmod m n) :: int)"
   1.288 -proof -
   1.289 -  have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
   1.290 -    using that by (simp only: snd_divmod modulo_int_def) auto
   1.291 +proof (cases "snd (divmod m n) = (0::int)")
   1.292 +  case True
   1.293    then show ?thesis
   1.294 -    by (auto simp add: split_def Let_def adjust_div_def divides_aux_def modulo_int_def)
   1.295 +    by (simp add: mod_eq_0_iff_dvd divides_aux_def)
   1.296 +next
   1.297 +  case False
   1.298 +  then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
   1.299 +    by (simp only: snd_divmod modulo_int_def) auto
   1.300 +  then show ?thesis
   1.301 +    by (simp add: divides_aux_def adjust_div_def)
   1.302 +      (simp add: divides_aux_def modulo_int_def)
   1.303  qed
   1.304  
   1.305  lemma minus_one_div_numeral [simp]:
   1.306 @@ -1461,6 +1348,10 @@
   1.307  lemma even_int_iff [simp]: "even (int n) \<longleftrightarrow> even n"
   1.308    by (fact even_of_nat)
   1.309  
   1.310 +lemma is_unit_int:
   1.311 +  "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
   1.312 +  by auto
   1.313 +
   1.314  text \<open>Tool setup\<close>
   1.315  
   1.316  declare transfer_morphism_int_nat [transfer add return: even_int_iff]
     2.1 --- a/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:22 2017 +0200
     2.2 +++ b/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:22 2017 +0200
     2.3 @@ -704,7 +704,7 @@
     2.4  
     2.5  subsection \<open>Euclidean division on @{typ nat}\<close>
     2.6  
     2.7 -instantiation nat :: unique_euclidean_semiring
     2.8 +instantiation nat :: normalization_semidom
     2.9  begin
    2.10  
    2.11  definition normalize_nat :: "nat \<Rightarrow> nat"
    2.12 @@ -718,15 +718,23 @@
    2.13    "unit_factor (Suc n) = 1"
    2.14    by (simp_all add: unit_factor_nat_def)
    2.15  
    2.16 +definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    2.17 +  where "m div n = (if n = 0 then 0 else Max {k::nat. k * n \<le> m})"
    2.18 +
    2.19 +instance
    2.20 +  by standard (auto simp add: divide_nat_def ac_simps unit_factor_nat_def intro: Max_eqI)
    2.21 +
    2.22 +end
    2.23 +
    2.24 +instantiation nat :: unique_euclidean_semiring
    2.25 +begin
    2.26 +
    2.27  definition euclidean_size_nat :: "nat \<Rightarrow> nat"
    2.28    where [simp]: "euclidean_size_nat = id"
    2.29  
    2.30  definition uniqueness_constraint_nat :: "nat \<Rightarrow> nat \<Rightarrow> bool"
    2.31    where [simp]: "uniqueness_constraint_nat = \<top>"
    2.32  
    2.33 -definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    2.34 -  where "m div n = (if n = 0 then 0 else Max {k::nat. k * n \<le> m})"
    2.35 -
    2.36  definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    2.37    where "m mod n = m - (m div n * (n::nat))"
    2.38  
    2.39 @@ -757,15 +765,11 @@
    2.40      finally show ?thesis
    2.41        using False by (simp add: divide_nat_def ac_simps)
    2.42    qed
    2.43 -  show "n div 0 = 0"
    2.44 -    by (simp add: divide_nat_def)
    2.45    have less_eq: "m div n * n \<le> m"
    2.46      by (auto simp add: mult_div_unfold ac_simps intro: Max.boundedI)
    2.47    then show "m div n * n + m mod n = m"
    2.48      by (simp add: modulo_nat_def)
    2.49    assume "n \<noteq> 0" 
    2.50 -  show "m * n div n = m"
    2.51 -    using \<open>n \<noteq> 0\<close> by (auto simp add: divide_nat_def ac_simps intro: Max_eqI)
    2.52    show "euclidean_size (m mod n) < euclidean_size n"
    2.53    proof -
    2.54      have "m < Suc (m div n) * n"
    2.55 @@ -805,7 +809,7 @@
    2.56      with \<open>n \<noteq> 0\<close> ex fin show ?thesis
    2.57        by (auto simp add: divide_nat_def Max_eq_iff)
    2.58    qed
    2.59 -qed (simp_all add: unit_factor_nat_def)
    2.60 +qed simp_all
    2.61  
    2.62  end
    2.63  
    2.64 @@ -1329,6 +1333,186 @@
    2.65  qed
    2.66  
    2.67  
    2.68 +subsection \<open>Euclidean division on @{typ int}\<close>
    2.69 +
    2.70 +instantiation int :: normalization_semidom
    2.71 +begin
    2.72 +
    2.73 +definition normalize_int :: "int \<Rightarrow> int"
    2.74 +  where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
    2.75 +
    2.76 +definition unit_factor_int :: "int \<Rightarrow> int"
    2.77 +  where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
    2.78 +
    2.79 +definition divide_int :: "int \<Rightarrow> int \<Rightarrow> int"
    2.80 +  where "k div l = (if l = 0 then 0
    2.81 +    else if sgn k = sgn l
    2.82 +      then int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
    2.83 +      else - int (nat \<bar>k\<bar> div nat \<bar>l\<bar> + of_bool (\<not> l dvd k)))"
    2.84 +
    2.85 +lemma divide_int_unfold:
    2.86 +  "(sgn k * int m) div (sgn l * int n) =
    2.87 +   (if sgn l = 0 \<or> sgn k = 0 \<or> n = 0 then 0
    2.88 +    else if sgn k = sgn l
    2.89 +      then int (m div n)
    2.90 +      else - int (m div n + of_bool (\<not> n dvd m)))"
    2.91 +  by (auto simp add: divide_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
    2.92 +    nat_mult_distrib dvd_int_iff)
    2.93 +
    2.94 +instance proof
    2.95 +  fix k :: int show "k div 0 = 0"
    2.96 +  by (simp add: divide_int_def)
    2.97 +next
    2.98 +  fix k l :: int
    2.99 +  assume "l \<noteq> 0"
   2.100 +  obtain n m and s t where k: "k = sgn s * int n" and l: "l = sgn t * int m" 
   2.101 +    by (blast intro: int_sgnE elim: that)
   2.102 +  then have "k * l = sgn (s * t) * int (n * m)"
   2.103 +    by (simp add: ac_simps sgn_mult)
   2.104 +  with k l \<open>l \<noteq> 0\<close> show "k * l div l = k"
   2.105 +    by (simp only: divide_int_unfold)
   2.106 +      (auto simp add: algebra_simps sgn_mult sgn_1_pos sgn_0_0)
   2.107 +qed (auto simp add: sgn_mult mult_sgn_abs abs_eq_iff')
   2.108 +
   2.109 +end
   2.110 +
   2.111 +instantiation int :: unique_euclidean_ring
   2.112 +begin
   2.113 +
   2.114 +definition euclidean_size_int :: "int \<Rightarrow> nat"
   2.115 +  where [simp]: "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
   2.116 +
   2.117 +definition uniqueness_constraint_int :: "int \<Rightarrow> int \<Rightarrow> bool"
   2.118 +  where [simp]: "uniqueness_constraint_int k l \<longleftrightarrow> unit_factor k = unit_factor l"
   2.119 +
   2.120 +definition modulo_int :: "int \<Rightarrow> int \<Rightarrow> int"
   2.121 +  where "k mod l = (if l = 0 then k
   2.122 +    else if sgn k = sgn l
   2.123 +      then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
   2.124 +      else sgn l * (\<bar>l\<bar> * of_bool (\<not> l dvd k) - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
   2.125 +
   2.126 +lemma modulo_int_unfold:
   2.127 +  "(sgn k * int m) mod (sgn l * int n) =
   2.128 +   (if sgn l = 0 \<or> sgn k = 0 \<or> n = 0 then sgn k * int m
   2.129 +    else if sgn k = sgn l
   2.130 +      then sgn l * int (m mod n)
   2.131 +      else sgn l * (int (n * of_bool (\<not> n dvd m)) - int (m mod n)))"
   2.132 +  by (auto simp add: modulo_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
   2.133 +    nat_mult_distrib dvd_int_iff)
   2.134 +
   2.135 +lemma abs_mod_less:
   2.136 +  "\<bar>k mod l\<bar> < \<bar>l\<bar>" if "l \<noteq> 0" for k l :: int
   2.137 +proof -
   2.138 +  obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
   2.139 +    by (blast intro: int_sgnE elim: that)
   2.140 +  with that show ?thesis
   2.141 +    by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg
   2.142 +      abs_mult mod_greater_zero_iff_not_dvd)
   2.143 +qed
   2.144 +
   2.145 +lemma sgn_mod:
   2.146 +  "sgn (k mod l) = sgn l" if "l \<noteq> 0" "\<not> l dvd k" for k l :: int
   2.147 +proof -
   2.148 +  obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
   2.149 +    by (blast intro: int_sgnE elim: that)
   2.150 +  with that show ?thesis
   2.151 +    by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg
   2.152 +      sgn_mult mod_eq_0_iff_dvd int_dvd_iff)
   2.153 +qed
   2.154 +
   2.155 +instance proof
   2.156 +  fix k l :: int
   2.157 +  obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
   2.158 +    by (blast intro: int_sgnE elim: that)
   2.159 +  then show "k div l * l + k mod l = k"
   2.160 +    by (auto simp add: divide_int_unfold modulo_int_unfold algebra_simps dest!: sgn_not_eq_imp)
   2.161 +       (simp_all add: of_nat_mult [symmetric] of_nat_add [symmetric]
   2.162 +         distrib_left [symmetric] minus_mult_right
   2.163 +         del: of_nat_mult minus_mult_right [symmetric])
   2.164 +next
   2.165 +  fix l q r :: int
   2.166 +  obtain n m and s t
   2.167 +     where l: "l = sgn s * int n" and q: "q = sgn t * int m"
   2.168 +    by (blast intro: int_sgnE elim: that)
   2.169 +  assume \<open>l \<noteq> 0\<close>
   2.170 +  with l have "s \<noteq> 0" and "n > 0"
   2.171 +    by (simp_all add: sgn_0_0)
   2.172 +  assume "uniqueness_constraint r l"
   2.173 +  moreover have "r = sgn r * \<bar>r\<bar>"
   2.174 +    by (simp add: sgn_mult_abs)
   2.175 +  moreover define u where "u = nat \<bar>r\<bar>"
   2.176 +  ultimately have "r = sgn l * int u"
   2.177 +    by simp
   2.178 +  with l \<open>n > 0\<close> have r: "r = sgn s * int u"
   2.179 +    by (simp add: sgn_mult)
   2.180 +  assume "euclidean_size r < euclidean_size l"
   2.181 +  with l r \<open>s \<noteq> 0\<close> have "u < n"
   2.182 +    by (simp add: abs_mult)
   2.183 +  show "(q * l + r) div l = q"
   2.184 +  proof (cases "q = 0 \<or> r = 0")
   2.185 +    case True
   2.186 +    then show ?thesis
   2.187 +    proof
   2.188 +      assume "q = 0"
   2.189 +      then show ?thesis
   2.190 +        using l r \<open>u < n\<close> by (simp add: divide_int_unfold)
   2.191 +    next
   2.192 +      assume "r = 0"
   2.193 +      from \<open>r = 0\<close> have *: "q * l + r = sgn (t * s) * int (n * m)"
   2.194 +        using q l by (simp add: ac_simps sgn_mult)
   2.195 +      from \<open>s \<noteq> 0\<close> \<open>n > 0\<close> show ?thesis
   2.196 +        by (simp only: *, simp only: q l divide_int_unfold)
   2.197 +          (auto simp add: sgn_mult sgn_0_0 sgn_1_pos)
   2.198 +    qed
   2.199 +  next
   2.200 +    case False
   2.201 +    with q r have "t \<noteq> 0" and "m > 0" and "s \<noteq> 0" and "u > 0"
   2.202 +      by (simp_all add: sgn_0_0)
   2.203 +    moreover from \<open>0 < m\<close> \<open>u < n\<close> have "u \<le> m * n"
   2.204 +      using mult_le_less_imp_less [of 1 m u n] by simp
   2.205 +    ultimately have *: "q * l + r = sgn (s * t)
   2.206 +      * int (if t < 0 then m * n - u else m * n + u)"
   2.207 +      using l q r
   2.208 +      by (simp add: sgn_mult algebra_simps of_nat_diff)
   2.209 +    have "(m * n - u) div n = m - 1" if "u > 0"
   2.210 +      using \<open>0 < m\<close> \<open>u < n\<close> that
   2.211 +      by (auto intro: div_nat_eqI simp add: algebra_simps)
   2.212 +    moreover have "n dvd m * n - u \<longleftrightarrow> n dvd u"
   2.213 +      using \<open>u \<le> m * n\<close> dvd_diffD1 [of n "m * n" u]
   2.214 +      by auto
   2.215 +    ultimately show ?thesis
   2.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>
   2.217 +      by (simp only: *, simp only: l q divide_int_unfold)
   2.218 +        (auto simp add: sgn_mult sgn_0_0 sgn_1_pos algebra_simps dest: dvd_imp_le)
   2.219 +  qed
   2.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>)
   2.221 +
   2.222 +end
   2.223 +
   2.224 +lemma pos_mod_bound [simp]:
   2.225 +  "k mod l < l" if "l > 0" for k l :: int
   2.226 +proof -
   2.227 +  obtain m and s where "k = sgn s * int m"
   2.228 +    by (blast intro: int_sgnE elim: that)
   2.229 +  moreover from that obtain n where "l = sgn 1 * int n"
   2.230 +    by (cases l) auto
   2.231 +  ultimately show ?thesis
   2.232 +    using that by (simp only: modulo_int_unfold)
   2.233 +      (simp add: mod_greater_zero_iff_not_dvd)
   2.234 +qed
   2.235 +
   2.236 +lemma pos_mod_sign [simp]:
   2.237 +  "0 \<le> k mod l" if "l > 0" for k l :: int
   2.238 +proof -
   2.239 +  obtain m and s where "k = sgn s * int m"
   2.240 +    by (blast intro: int_sgnE elim: that)
   2.241 +  moreover from that obtain n where "l = sgn 1 * int n"
   2.242 +    by (cases l) auto
   2.243 +  ultimately show ?thesis
   2.244 +    using that by (simp only: modulo_int_unfold) simp
   2.245 +qed
   2.246 +
   2.247 +
   2.248  subsection \<open>Code generation\<close>
   2.249  
   2.250  code_identifier
     3.1 --- a/src/HOL/GCD.thy	Sun Oct 08 22:28:22 2017 +0200
     3.2 +++ b/src/HOL/GCD.thy	Sun Oct 08 22:28:22 2017 +0200
     3.3 @@ -2017,11 +2017,11 @@
     3.4  lemma gcd_non_0_int: "y > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
     3.5    for x y :: int
     3.6    apply (frule_tac b = y and a = x in pos_mod_sign)
     3.7 -  apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
     3.8 +  apply (simp del: Euclidean_Division.pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
     3.9    apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
    3.10    apply (frule_tac a = x in pos_mod_bound)
    3.11    apply (subst (1 2) gcd.commute)
    3.12 -  apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat nat_le_eq_zle)
    3.13 +  apply (simp del: Euclidean_Division.pos_mod_bound add: nat_diff_distrib gcd_diff2_nat nat_le_eq_zle)
    3.14    done
    3.15  
    3.16  lemma gcd_red_int: "gcd x y = gcd y (x mod y)"
     4.1 --- a/src/HOL/Int.thy	Sun Oct 08 22:28:22 2017 +0200
     4.2 +++ b/src/HOL/Int.thy	Sun Oct 08 22:28:22 2017 +0200
     4.3 @@ -255,6 +255,10 @@
     4.4  lemma of_int_power [simp]: "of_int (z ^ n) = of_int z ^ n"
     4.5    by (induct n) simp_all
     4.6  
     4.7 +lemma of_int_of_bool [simp]:
     4.8 +  "of_int (of_bool P) = of_bool P"
     4.9 +  by auto
    4.10 +
    4.11  end
    4.12  
    4.13  context ring_char_0
    4.14 @@ -548,6 +552,10 @@
    4.15  lemma diff_nat_numeral [simp]: "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
    4.16    by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
    4.17  
    4.18 +lemma nat_of_bool [simp]:
    4.19 +  "nat (of_bool P) = of_bool P"
    4.20 +  by auto
    4.21 +
    4.22  
    4.23  text \<open>For termination proofs:\<close>
    4.24  lemma measure_function_int[measure_function]: "is_measure (nat \<circ> abs)" ..
    4.25 @@ -668,6 +676,31 @@
    4.26    \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
    4.27    by (fact Let_neg_numeral) \<comment> \<open>FIXME drop\<close>
    4.28  
    4.29 +lemma sgn_mult_dvd_iff [simp]:
    4.30 +  "sgn r * l dvd k \<longleftrightarrow> l dvd k \<and> (r = 0 \<longrightarrow> k = 0)" for k l r :: int
    4.31 +  by (cases r rule: int_cases3) auto
    4.32 +
    4.33 +lemma mult_sgn_dvd_iff [simp]:
    4.34 +  "l * sgn r dvd k \<longleftrightarrow> l dvd k \<and> (r = 0 \<longrightarrow> k = 0)" for k l r :: int
    4.35 +  using sgn_mult_dvd_iff [of r l k] by (simp add: ac_simps)
    4.36 +
    4.37 +lemma dvd_sgn_mult_iff [simp]:
    4.38 +  "l dvd sgn r * k \<longleftrightarrow> l dvd k \<or> r = 0" for k l r :: int
    4.39 +  by (cases r rule: int_cases3) simp_all
    4.40 +
    4.41 +lemma dvd_mult_sgn_iff [simp]:
    4.42 +  "l dvd k * sgn r \<longleftrightarrow> l dvd k \<or> r = 0" for k l r :: int
    4.43 +  using dvd_sgn_mult_iff [of l r k] by (simp add: ac_simps)
    4.44 +
    4.45 +lemma int_sgnE:
    4.46 +  fixes k :: int
    4.47 +  obtains n and l where "k = sgn l * int n"
    4.48 +proof -
    4.49 +  have "k = sgn k * int (nat \<bar>k\<bar>)"
    4.50 +    by (simp add: sgn_mult_abs)
    4.51 +  then show ?thesis ..
    4.52 +qed
    4.53 +
    4.54  text \<open>Unfold \<open>min\<close> and \<open>max\<close> on numerals.\<close>
    4.55  
    4.56  lemmas max_number_of [simp] =
    4.57 @@ -1629,19 +1662,10 @@
    4.58    shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
    4.59      (is "?lhs \<longleftrightarrow> ?rhs")
    4.60  proof -
    4.61 -  from assms obtain k where "d = a * k" by (rule dvdE)
    4.62 -  show ?thesis
    4.63 -  proof
    4.64 -    assume ?lhs
    4.65 -    then obtain l where "x + t = a * l" by (rule dvdE)
    4.66 -    then have "x = a * l - t" by simp
    4.67 -    with \<open>d = a * k\<close> show ?rhs by simp
    4.68 -  next
    4.69 -    assume ?rhs
    4.70 -    then obtain l where "x + c * d + t = a * l" by (rule dvdE)
    4.71 -    then have "x = a * l - c * d - t" by simp
    4.72 -    with \<open>d = a * k\<close> show ?lhs by simp
    4.73 -  qed
    4.74 +  from assms have "a dvd (x + t) \<longleftrightarrow> a dvd ((x + t) + c * d)"
    4.75 +    by (simp add: dvd_add_left_iff)
    4.76 +  then show ?thesis
    4.77 +    by (simp add: ac_simps)
    4.78  qed
    4.79  
    4.80  
     5.1 --- a/src/HOL/Nat.thy	Sun Oct 08 22:28:22 2017 +0200
     5.2 +++ b/src/HOL/Nat.thy	Sun Oct 08 22:28:22 2017 +0200
     5.3 @@ -1676,6 +1676,10 @@
     5.4      by (simp add: add.commute)
     5.5  qed
     5.6  
     5.7 +lemma of_nat_of_bool [simp]:
     5.8 +  "of_nat (of_bool P) = of_bool P"
     5.9 +  by auto
    5.10 +
    5.11  end
    5.12  
    5.13  declare of_nat_code [code]
    5.14 @@ -1764,6 +1768,10 @@
    5.15  lemma abs_of_nat [simp]: "\<bar>of_nat n\<bar> = of_nat n"
    5.16    unfolding abs_if by auto
    5.17  
    5.18 +lemma sgn_of_nat [simp]:
    5.19 +  "sgn (of_nat n) = of_bool (n > 0)"
    5.20 +  by simp
    5.21 +
    5.22  end
    5.23  
    5.24  lemma of_nat_id [simp]: "of_nat n = n"
     6.1 --- a/src/HOL/Parity.thy	Sun Oct 08 22:28:22 2017 +0200
     6.2 +++ b/src/HOL/Parity.thy	Sun Oct 08 22:28:22 2017 +0200
     6.3 @@ -483,4 +483,40 @@
     6.4  
     6.5  end
     6.6  
     6.7 +
     6.8 +subsection \<open>Instance for @{typ int}\<close>
     6.9 +
    6.10 +instance int :: ring_parity
    6.11 +proof
    6.12 +  fix k l :: int
    6.13 +  show "k mod 2 = 1" if "\<not> 2 dvd k"
    6.14 +  proof (rule order_antisym)
    6.15 +    have "0 \<le> k mod 2" and "k mod 2 < 2"
    6.16 +      by auto
    6.17 +    moreover have "k mod 2 \<noteq> 0"
    6.18 +      using that by (simp add: dvd_eq_mod_eq_0)
    6.19 +    ultimately have "0 < k mod 2"
    6.20 +      by (simp only: less_le) simp
    6.21 +    then show "1 \<le> k mod 2"
    6.22 +      by simp
    6.23 +    from \<open>k mod 2 < 2\<close> show "k mod 2 \<le> 1"
    6.24 +      by (simp only: less_le) simp
    6.25 +  qed
    6.26 +qed (simp_all add: dvd_eq_mod_eq_0 divide_int_def)
    6.27 +
    6.28 +lemma even_diff_iff [simp]:
    6.29 +  "even (k - l) \<longleftrightarrow> even (k + l)" for k l :: int
    6.30 +  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
    6.31 +
    6.32 +lemma even_abs_add_iff [simp]:
    6.33 +  "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)" for k l :: int
    6.34 +  by (cases "k \<ge> 0") (simp_all add: ac_simps)
    6.35 +
    6.36 +lemma even_add_abs_iff [simp]:
    6.37 +  "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)" for k l :: int
    6.38 +  using even_abs_add_iff [of l k] by (simp add: ac_simps)
    6.39 +
    6.40 +lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
    6.41 +  by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric])
    6.42 +
    6.43  end
     7.1 --- a/src/HOL/Rings.thy	Sun Oct 08 22:28:22 2017 +0200
     7.2 +++ b/src/HOL/Rings.thy	Sun Oct 08 22:28:22 2017 +0200
     7.3 @@ -118,6 +118,13 @@
     7.4  end
     7.5  
     7.6  class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
     7.7 +begin
     7.8 +
     7.9 +lemma (in semiring_1) of_bool_conj:
    7.10 +  "of_bool (P \<and> Q) = of_bool P * of_bool Q"
    7.11 +  by auto
    7.12 +
    7.13 +end
    7.14  
    7.15  text \<open>Abstract divisibility\<close>
    7.16  
    7.17 @@ -2319,6 +2326,10 @@
    7.18      by (auto simp add: abs_mult)
    7.19  qed
    7.20  
    7.21 +lemma sgn_not_eq_imp:
    7.22 +  "sgn a = - sgn b" if "sgn b \<noteq> sgn a" and "sgn a \<noteq> 0" and "sgn b \<noteq> 0"
    7.23 +  using that by (cases "a < 0") (auto simp add: sgn_0_0 sgn_1_pos sgn_1_neg)
    7.24 +
    7.25  lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
    7.26    by (simp add: abs_if)
    7.27