src/HOL/Divides.thy
changeset 66816 212a3334e7da
parent 66815 93c6632ddf44
child 66817 0b12755ccbb2
     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]