src/HOL/Divides.thy
changeset 47108 2a1953f0d20d
parent 46560 8e252a608765
child 47134 28c1db43d4d0
     1.1 --- a/src/HOL/Divides.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Divides.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -1138,8 +1138,8 @@
     1.4  lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
     1.5  by (simp add: Suc3_eq_add_3)
     1.6  
     1.7 -lemmas Suc_div_eq_add3_div_number_of [simp] = Suc_div_eq_add3_div [of _ "number_of v"] for v
     1.8 -lemmas Suc_mod_eq_add3_mod_number_of [simp] = Suc_mod_eq_add3_mod [of _ "number_of v"] for v
     1.9 +lemmas Suc_div_eq_add3_div_numeral [simp] = Suc_div_eq_add3_div [of _ "numeral v"] for v
    1.10 +lemmas Suc_mod_eq_add3_mod_numeral [simp] = Suc_mod_eq_add3_mod [of _ "numeral v"] for v
    1.11  
    1.12  
    1.13  lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1" 
    1.14 @@ -1147,7 +1147,7 @@
    1.15  apply (simp_all add: mod_Suc)
    1.16  done
    1.17  
    1.18 -declare Suc_times_mod_eq [of "number_of w", simp] for w
    1.19 +declare Suc_times_mod_eq [of "numeral w", simp] for w
    1.20  
    1.21  lemma [simp]: "n div k \<le> (Suc n) div k"
    1.22  by (simp add: div_le_mono) 
    1.23 @@ -1177,17 +1177,22 @@
    1.24  apply (subst mod_Suc [of "m mod n"], simp) 
    1.25  done
    1.26  
    1.27 +lemma mod_2_not_eq_zero_eq_one_nat:
    1.28 +  fixes n :: nat
    1.29 +  shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
    1.30 +  by simp
    1.31 +
    1.32  
    1.33  subsection {* Division on @{typ int} *}
    1.34  
    1.35  definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where
    1.36      --{*definition of quotient and remainder*}
    1.37 -    [code]: "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
    1.38 +    "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
    1.39                 (if 0 < b then 0 \<le> r \<and> r < b else b < r \<and> r \<le> 0))"
    1.40  
    1.41  definition adjust :: "int \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int" where
    1.42      --{*for the division algorithm*}
    1.43 -    [code]: "adjust b = (\<lambda>(q, r). if 0 \<le> r - b then (2 * q + 1, r - b)
    1.44 +    "adjust b = (\<lambda>(q, r). if 0 \<le> r - b then (2 * q + 1, r - b)
    1.45                           else (2 * q, r))"
    1.46  
    1.47  text{*algorithm for the case @{text "a\<ge>0, b>0"}*}
    1.48 @@ -1318,11 +1323,11 @@
    1.49  text{*And positive divisors*}
    1.50  
    1.51  lemma adjust_eq [simp]:
    1.52 -     "adjust b (q,r) = 
    1.53 -      (let diff = r-b in  
    1.54 -        if 0 \<le> diff then (2*q + 1, diff)   
    1.55 +     "adjust b (q, r) = 
    1.56 +      (let diff = r - b in  
    1.57 +        if 0 \<le> diff then (2 * q + 1, diff)   
    1.58                       else (2*q, r))"
    1.59 -by (simp add: Let_def adjust_def)
    1.60 +  by (simp add: Let_def adjust_def)
    1.61  
    1.62  declare posDivAlg.simps [simp del]
    1.63  
    1.64 @@ -1420,6 +1425,9 @@
    1.65  
    1.66  text {* Tool setup *}
    1.67  
    1.68 +(* FIXME: Theorem list add_0s doesn't exist, because Numeral0 has gone. *)
    1.69 +lemmas add_0s = add_0_left add_0_right
    1.70 +
    1.71  ML {*
    1.72  structure Cancel_Div_Mod_Int = Cancel_Div_Mod
    1.73  (
    1.74 @@ -1674,16 +1682,6 @@
    1.75    by (rule divmod_int_rel_mod [of a b q r],
    1.76      simp add: divmod_int_rel_def)
    1.77  
    1.78 -lemmas arithmetic_simps =
    1.79 -  arith_simps
    1.80 -  add_special
    1.81 -  add_0_left
    1.82 -  add_0_right
    1.83 -  mult_zero_left
    1.84 -  mult_zero_right
    1.85 -  mult_1_left
    1.86 -  mult_1_right
    1.87 -
    1.88  (* simprocs adapted from HOL/ex/Binary.thy *)
    1.89  ML {*
    1.90  local
    1.91 @@ -1694,7 +1692,7 @@
    1.92    val less = @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"}
    1.93    val le = @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"}
    1.94    val simps = @{thms arith_simps} @ @{thms rel_simps} @
    1.95 -    map (fn th => th RS sym) [@{thm numeral_0_eq_0}, @{thm numeral_1_eq_1}]
    1.96 +    map (fn th => th RS sym) [@{thm numeral_1_eq_1}]
    1.97    fun prove ctxt goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)
    1.98      (K (ALLGOALS (full_simp_tac (HOL_basic_ss addsimps simps))));
    1.99    fun binary_proc proc ss ct =
   1.100 @@ -1717,14 +1715,25 @@
   1.101  end
   1.102  *}
   1.103  
   1.104 -simproc_setup binary_int_div ("number_of m div number_of n :: int") =
   1.105 +simproc_setup binary_int_div
   1.106 +  ("numeral m div numeral n :: int" |
   1.107 +   "numeral m div neg_numeral n :: int" |
   1.108 +   "neg_numeral m div numeral n :: int" |
   1.109 +   "neg_numeral m div neg_numeral n :: int") =
   1.110    {* K (divmod_proc @{thm int_div_pos_eq} @{thm int_div_neg_eq}) *}
   1.111  
   1.112 -simproc_setup binary_int_mod ("number_of m mod number_of n :: int") =
   1.113 +simproc_setup binary_int_mod
   1.114 +  ("numeral m mod numeral n :: int" |
   1.115 +   "numeral m mod neg_numeral n :: int" |
   1.116 +   "neg_numeral m mod numeral n :: int" |
   1.117 +   "neg_numeral m mod neg_numeral n :: int") =
   1.118    {* K (divmod_proc @{thm int_mod_pos_eq} @{thm int_mod_neg_eq}) *}
   1.119  
   1.120 -lemmas posDivAlg_eqn_number_of [simp] = posDivAlg_eqn [of "number_of v" "number_of w"] for v w
   1.121 -lemmas negDivAlg_eqn_number_of [simp] = negDivAlg_eqn [of "number_of v" "number_of w"] for v w
   1.122 +lemmas posDivAlg_eqn_numeral [simp] =
   1.123 +    posDivAlg_eqn [of "numeral v" "numeral w", OF zero_less_numeral] for v w
   1.124 +
   1.125 +lemmas negDivAlg_eqn_numeral [simp] =
   1.126 +    negDivAlg_eqn [of "numeral v" "neg_numeral w", OF zero_less_numeral] for v w
   1.127  
   1.128  
   1.129  text{*Special-case simplification *}
   1.130 @@ -1741,12 +1750,25 @@
   1.131  (** The last remaining special cases for constant arithmetic:
   1.132      1 div z and 1 mod z **)
   1.133  
   1.134 -lemmas div_pos_pos_1_number_of [simp] = div_pos_pos [OF zero_less_one, of "number_of w"] for w
   1.135 -lemmas div_pos_neg_1_number_of [simp] = div_pos_neg [OF zero_less_one, of "number_of w"] for w
   1.136 -lemmas mod_pos_pos_1_number_of [simp] = mod_pos_pos [OF zero_less_one, of "number_of w"] for w
   1.137 -lemmas mod_pos_neg_1_number_of [simp] = mod_pos_neg [OF zero_less_one, of "number_of w"] for w
   1.138 -lemmas posDivAlg_eqn_1_number_of [simp] = posDivAlg_eqn [of concl: 1 "number_of w"] for w
   1.139 -lemmas negDivAlg_eqn_1_number_of [simp] = negDivAlg_eqn [of concl: 1 "number_of w"] for w
   1.140 +lemmas div_pos_pos_1_numeral [simp] =
   1.141 +  div_pos_pos [OF zero_less_one, of "numeral w", OF zero_le_numeral] for w
   1.142 +
   1.143 +lemmas div_pos_neg_1_numeral [simp] =
   1.144 +  div_pos_neg [OF zero_less_one, of "neg_numeral w",
   1.145 +  OF neg_numeral_less_zero] for w
   1.146 +
   1.147 +lemmas mod_pos_pos_1_numeral [simp] =
   1.148 +  mod_pos_pos [OF zero_less_one, of "numeral w", OF zero_le_numeral] for w
   1.149 +
   1.150 +lemmas mod_pos_neg_1_numeral [simp] =
   1.151 +  mod_pos_neg [OF zero_less_one, of "neg_numeral w",
   1.152 +  OF neg_numeral_less_zero] for w
   1.153 +
   1.154 +lemmas posDivAlg_eqn_1_numeral [simp] =
   1.155 +    posDivAlg_eqn [of concl: 1 "numeral w", OF zero_less_numeral] for w
   1.156 +
   1.157 +lemmas negDivAlg_eqn_1_numeral [simp] =
   1.158 +    negDivAlg_eqn [of concl: 1 "numeral w", OF zero_less_numeral] for w
   1.159  
   1.160  
   1.161  subsubsection {* Monotonicity in the First Argument (Dividend) *}
   1.162 @@ -1928,6 +1950,11 @@
   1.163  (* REVISIT: should this be generalized to all semiring_div types? *)
   1.164  lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
   1.165  
   1.166 +lemma zmod_zdiv_equality':
   1.167 +  "(m\<Colon>int) mod n = m - (m div n) * n"
   1.168 +  by (rule_tac P="%x. m mod n = x - (m div n) * n" in subst [OF mod_div_equality [of _ n]])
   1.169 +    arith
   1.170 +
   1.171  
   1.172  subsubsection {* Proving  @{term "a div (b*c) = (a div b) div c"} *}
   1.173  
   1.174 @@ -1989,6 +2016,26 @@
   1.175  apply (force simp add: divmod_int_rel_div_mod [THEN zmult2_lemma, THEN divmod_int_rel_mod])
   1.176  done
   1.177  
   1.178 +lemma div_pos_geq:
   1.179 +  fixes k l :: int
   1.180 +  assumes "0 < l" and "l \<le> k"
   1.181 +  shows "k div l = (k - l) div l + 1"
   1.182 +proof -
   1.183 +  have "k = (k - l) + l" by simp
   1.184 +  then obtain j where k: "k = j + l" ..
   1.185 +  with assms show ?thesis by simp
   1.186 +qed
   1.187 +
   1.188 +lemma mod_pos_geq:
   1.189 +  fixes k l :: int
   1.190 +  assumes "0 < l" and "l \<le> k"
   1.191 +  shows "k mod l = (k - l) mod l"
   1.192 +proof -
   1.193 +  have "k = (k - l) + l" by simp
   1.194 +  then obtain j where k: "k = j + l" ..
   1.195 +  with assms show ?thesis by simp
   1.196 +qed
   1.197 +
   1.198  
   1.199  subsubsection {* Splitting Rules for div and mod *}
   1.200  
   1.201 @@ -2046,9 +2093,9 @@
   1.202  
   1.203  text {* Enable (lin)arith to deal with @{const div} and @{const mod}
   1.204    when these are applied to some constant that is of the form
   1.205 -  @{term "number_of k"}: *}
   1.206 -declare split_zdiv [of _ _ "number_of k", arith_split] for k
   1.207 -declare split_zmod [of _ _ "number_of k", arith_split] for k
   1.208 +  @{term "numeral k"}: *}
   1.209 +declare split_zdiv [of _ _ "numeral k", arith_split] for k
   1.210 +declare split_zmod [of _ _ "numeral k", arith_split] for k
   1.211  
   1.212  
   1.213  subsubsection {* Speeding up the Division Algorithm with Shifting *}
   1.214 @@ -2090,19 +2137,19 @@
   1.215        minus_add_distrib [symmetric] mult_minus_right)
   1.216  qed
   1.217  
   1.218 -lemma zdiv_number_of_Bit0 [simp]:
   1.219 -     "number_of (Int.Bit0 v) div number_of (Int.Bit0 w) =  
   1.220 -          number_of v div (number_of w :: int)"
   1.221 -by (simp only: number_of_eq numeral_simps) (simp add: mult_2 [symmetric])
   1.222 -
   1.223 -lemma zdiv_number_of_Bit1 [simp]:
   1.224 -     "number_of (Int.Bit1 v) div number_of (Int.Bit0 w) =  
   1.225 -          (if (0::int) \<le> number_of w                    
   1.226 -           then number_of v div (number_of w)     
   1.227 -           else (number_of v + (1::int)) div (number_of w))"
   1.228 -apply (simp only: number_of_eq numeral_simps UNIV_I split: split_if) 
   1.229 -apply (simp add: pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac mult_2 [symmetric])
   1.230 -done
   1.231 +(* FIXME: add rules for negative numerals *)
   1.232 +lemma zdiv_numeral_Bit0 [simp]:
   1.233 +  "numeral (Num.Bit0 v) div numeral (Num.Bit0 w) =
   1.234 +    numeral v div (numeral w :: int)"
   1.235 +  unfolding numeral.simps unfolding mult_2 [symmetric]
   1.236 +  by (rule div_mult_mult1, simp)
   1.237 +
   1.238 +lemma zdiv_numeral_Bit1 [simp]:
   1.239 +  "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) =  
   1.240 +    (numeral v div (numeral w :: int))"
   1.241 +  unfolding numeral.simps
   1.242 +  unfolding mult_2 [symmetric] add_commute [of _ 1]
   1.243 +  by (rule pos_zdiv_mult_2, simp)
   1.244  
   1.245  
   1.246  subsubsection {* Computing mod by Shifting (proofs resemble those for div) *}
   1.247 @@ -2138,24 +2185,19 @@
   1.248       (simp add: diff_minus add_ac)
   1.249  qed
   1.250  
   1.251 -lemma zmod_number_of_Bit0 [simp]:
   1.252 -     "number_of (Int.Bit0 v) mod number_of (Int.Bit0 w) =  
   1.253 -      (2::int) * (number_of v mod number_of w)"
   1.254 -apply (simp only: number_of_eq numeral_simps) 
   1.255 -apply (simp add: mod_mult_mult1 pos_zmod_mult_2 
   1.256 -                 neg_zmod_mult_2 add_ac mult_2 [symmetric])
   1.257 -done
   1.258 -
   1.259 -lemma zmod_number_of_Bit1 [simp]:
   1.260 -     "number_of (Int.Bit1 v) mod number_of (Int.Bit0 w) =  
   1.261 -      (if (0::int) \<le> number_of w  
   1.262 -                then 2 * (number_of v mod number_of w) + 1     
   1.263 -                else 2 * ((number_of v + (1::int)) mod number_of w) - 1)"
   1.264 -apply (simp only: number_of_eq numeral_simps) 
   1.265 -apply (simp add: mod_mult_mult1 pos_zmod_mult_2 
   1.266 -                 neg_zmod_mult_2 add_ac mult_2 [symmetric])
   1.267 -done
   1.268 -
   1.269 +(* FIXME: add rules for negative numerals *)
   1.270 +lemma zmod_numeral_Bit0 [simp]:
   1.271 +  "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =  
   1.272 +    (2::int) * (numeral v mod numeral w)"
   1.273 +  unfolding numeral_Bit0 [of v] numeral_Bit0 [of w]
   1.274 +  unfolding mult_2 [symmetric] by (rule mod_mult_mult1)
   1.275 +
   1.276 +lemma zmod_numeral_Bit1 [simp]:
   1.277 +  "numeral (Num.Bit1 v) mod numeral (Num.Bit0 w) =
   1.278 +    2 * (numeral v mod numeral w) + (1::int)"
   1.279 +  unfolding numeral_Bit1 [of v] numeral_Bit0 [of w]
   1.280 +  unfolding mult_2 [symmetric] add_commute [of _ 1]
   1.281 +  by (rule pos_zmod_mult_2, simp)
   1.282  
   1.283  lemma zdiv_eq_0_iff:
   1.284   "(i::int) div k = 0 \<longleftrightarrow> k=0 \<or> 0\<le>i \<and> i<k \<or> i\<le>0 \<and> k<i" (is "?L = ?R")
   1.285 @@ -2233,8 +2275,11 @@
   1.286  
   1.287  subsubsection {* The Divides Relation *}
   1.288  
   1.289 -lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
   1.290 -  dvd_eq_mod_eq_0 [of "number_of x" "number_of y"] for x y :: int
   1.291 +lemmas zdvd_iff_zmod_eq_0_numeral [simp] =
   1.292 +  dvd_eq_mod_eq_0 [of "numeral x::int" "numeral y::int"]
   1.293 +  dvd_eq_mod_eq_0 [of "numeral x::int" "neg_numeral y::int"]
   1.294 +  dvd_eq_mod_eq_0 [of "neg_numeral x::int" "numeral y::int"]
   1.295 +  dvd_eq_mod_eq_0 [of "neg_numeral x::int" "neg_numeral y::int"] for x y
   1.296  
   1.297  lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
   1.298    by (rule dvd_mod) (* TODO: remove *)
   1.299 @@ -2242,6 +2287,12 @@
   1.300  lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
   1.301    by (rule dvd_mod_imp_dvd) (* TODO: remove *)
   1.302  
   1.303 +lemmas dvd_eq_mod_eq_0_numeral [simp] =
   1.304 +  dvd_eq_mod_eq_0 [of "numeral x" "numeral y"] for x y
   1.305 +
   1.306 +
   1.307 +subsubsection {* Further properties *}
   1.308 +
   1.309  lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
   1.310    using zmod_zdiv_equality[where a="m" and b="n"]
   1.311    by (simp add: algebra_simps)
   1.312 @@ -2408,42 +2459,31 @@
   1.313    thus  ?lhs by simp
   1.314  qed
   1.315  
   1.316 -lemma div_nat_number_of [simp]:
   1.317 -     "(number_of v :: nat)  div  number_of v' =  
   1.318 -          (if neg (number_of v :: int) then 0  
   1.319 -           else nat (number_of v div number_of v'))"
   1.320 -  unfolding nat_number_of_def number_of_is_id neg_def
   1.321 +lemma div_nat_numeral [simp]:
   1.322 +  "(numeral v :: nat) div numeral v' = nat (numeral v div numeral v')"
   1.323    by (simp add: nat_div_distrib)
   1.324  
   1.325 -lemma one_div_nat_number_of [simp]:
   1.326 -     "Suc 0 div number_of v' = nat (1 div number_of v')" 
   1.327 -  by (simp del: semiring_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric] semiring_numeral_1_eq_1 [symmetric]) 
   1.328 -
   1.329 -lemma mod_nat_number_of [simp]:
   1.330 -     "(number_of v :: nat)  mod  number_of v' =  
   1.331 -        (if neg (number_of v :: int) then 0  
   1.332 -         else if neg (number_of v' :: int) then number_of v  
   1.333 -         else nat (number_of v mod number_of v'))"
   1.334 -  unfolding nat_number_of_def number_of_is_id neg_def
   1.335 +lemma one_div_nat_numeral [simp]:
   1.336 +  "Suc 0 div numeral v' = nat (1 div numeral v')"
   1.337 +  by (subst nat_div_distrib, simp_all)
   1.338 +
   1.339 +lemma mod_nat_numeral [simp]:
   1.340 +  "(numeral v :: nat) mod numeral v' = nat (numeral v mod numeral v')"
   1.341    by (simp add: nat_mod_distrib)
   1.342  
   1.343 -lemma one_mod_nat_number_of [simp]:
   1.344 -     "Suc 0 mod number_of v' =  
   1.345 -        (if neg (number_of v' :: int) then Suc 0
   1.346 -         else nat (1 mod number_of v'))"
   1.347 -by (simp del: semiring_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric] semiring_numeral_1_eq_1 [symmetric]) 
   1.348 -
   1.349 -lemmas dvd_eq_mod_eq_0_number_of [simp] =
   1.350 -  dvd_eq_mod_eq_0 [of "number_of x" "number_of y"] for x y
   1.351 -
   1.352 -
   1.353 -subsubsection {* Nitpick *}
   1.354 -
   1.355 -lemma zmod_zdiv_equality':
   1.356 -"(m\<Colon>int) mod n = m - (m div n) * n"
   1.357 -by (rule_tac P="%x. m mod n = x - (m div n) * n"
   1.358 -    in subst [OF mod_div_equality [of _ n]])
   1.359 -   arith
   1.360 +lemma one_mod_nat_numeral [simp]:
   1.361 +  "Suc 0 mod numeral v' = nat (1 mod numeral v')"
   1.362 +  by (subst nat_mod_distrib) simp_all
   1.363 +
   1.364 +lemma mod_2_not_eq_zero_eq_one_int:
   1.365 +  fixes k :: int
   1.366 +  shows "k mod 2 \<noteq> 0 \<longleftrightarrow> k mod 2 = 1"
   1.367 +  by auto
   1.368 +
   1.369 +
   1.370 +subsubsection {* Tools setup *}
   1.371 +
   1.372 +text {* Nitpick *}
   1.373  
   1.374  lemmas [nitpick_unfold] = dvd_eq_mod_eq_0 mod_div_equality' zmod_zdiv_equality'
   1.375  
   1.376 @@ -2461,7 +2501,7 @@
   1.377    apsnd ((op *) (sgn l)) (if 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0
   1.378      then pdivmod k l
   1.379      else (let (r, s) = pdivmod k l in
   1.380 -      if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
   1.381 +       if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
   1.382  proof -
   1.383    have aux: "\<And>q::int. - k = l * q \<longleftrightarrow> k = l * - q" by auto
   1.384    show ?thesis
   1.385 @@ -2481,45 +2521,6 @@
   1.386    then show ?thesis by (simp add: divmod_int_pdivmod)
   1.387  qed
   1.388  
   1.389 -context ring_1
   1.390 -begin
   1.391 -
   1.392 -lemma of_int_num [code]:
   1.393 -  "of_int k = (if k = 0 then 0 else if k < 0 then
   1.394 -     - of_int (- k) else let
   1.395 -       (l, m) = divmod_int k 2;
   1.396 -       l' = of_int l
   1.397 -     in if m = 0 then l' + l' else l' + l' + 1)"
   1.398 -proof -
   1.399 -  have aux1: "k mod (2\<Colon>int) \<noteq> (0\<Colon>int) \<Longrightarrow> 
   1.400 -    of_int k = of_int (k div 2 * 2 + 1)"
   1.401 -  proof -
   1.402 -    have "k mod 2 < 2" by (auto intro: pos_mod_bound)
   1.403 -    moreover have "0 \<le> k mod 2" by (auto intro: pos_mod_sign)
   1.404 -    moreover assume "k mod 2 \<noteq> 0"
   1.405 -    ultimately have "k mod 2 = 1" by arith
   1.406 -    moreover have "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
   1.407 -    ultimately show ?thesis by auto
   1.408 -  qed
   1.409 -  have aux2: "\<And>x. of_int 2 * x = x + x"
   1.410 -  proof -
   1.411 -    fix x
   1.412 -    have int2: "(2::int) = 1 + 1" by arith
   1.413 -    show "of_int 2 * x = x + x"
   1.414 -    unfolding int2 of_int_add left_distrib by simp
   1.415 -  qed
   1.416 -  have aux3: "\<And>x. x * of_int 2 = x + x"
   1.417 -  proof -
   1.418 -    fix x
   1.419 -    have int2: "(2::int) = 1 + 1" by arith
   1.420 -    show "x * of_int 2 = x + x" 
   1.421 -    unfolding int2 of_int_add right_distrib by simp
   1.422 -  qed
   1.423 -  from aux1 show ?thesis by (auto simp add: divmod_int_mod_div Let_def aux2 aux3)
   1.424 -qed
   1.425 -
   1.426 -end
   1.427 -
   1.428  code_modulename SML
   1.429    Divides Arith
   1.430