src/HOL/Divides.thy
author wenzelm
Tue Oct 10 19:23:03 2017 +0200 (23 months ago)
changeset 66831 29ea2b900a05
parent 66817 0b12755ccbb2
child 66837 6ba663ff2b1c
permissions -rw-r--r--
tuned: each session has at most one defining entry;
     1 (*  Title:      HOL/Divides.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1999  University of Cambridge
     4 *)
     5 
     6 section \<open>More on quotient and remainder\<close>
     7 
     8 theory Divides
     9 imports Parity
    10 begin
    11 
    12 subsection \<open>Numeral division with a pragmatic type class\<close>
    13 
    14 text \<open>
    15   The following type class contains everything necessary to formulate
    16   a division algorithm in ring structures with numerals, restricted
    17   to its positive segments.  This is its primary motivation, and it
    18   could surely be formulated using a more fine-grained, more algebraic
    19   and less technical class hierarchy.
    20 \<close>
    21 
    22 class unique_euclidean_semiring_numeral = semiring_parity + linordered_semidom +
    23   assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
    24     and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
    25     and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
    26     and mod_less_eq_dividend: "0 \<le> a \<Longrightarrow> a mod b \<le> a"
    27     and pos_mod_bound: "0 < b \<Longrightarrow> a mod b < b"
    28     and pos_mod_sign: "0 < b \<Longrightarrow> 0 \<le> a mod b"
    29     and mod_mult2_eq: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
    30     and div_mult2_eq: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c"
    31   assumes discrete: "a < b \<longleftrightarrow> a + 1 \<le> b"
    32   fixes divmod :: "num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a"
    33     and divmod_step :: "num \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a"
    34   assumes divmod_def: "divmod m n = (numeral m div numeral n, numeral m mod numeral n)"
    35     and divmod_step_def: "divmod_step l qr = (let (q, r) = qr
    36     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
    37     else (2 * q, r))"
    38     \<comment> \<open>These are conceptually definitions but force generated code
    39     to be monomorphic wrt. particular instances of this class which
    40     yields a significant speedup.\<close>
    41 begin
    42 
    43 lemma divmod_digit_1:
    44   assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)"
    45   shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")
    46     and "a mod (2 * b) - b = a mod b" (is "?Q")
    47 proof -
    48   from assms mod_less_eq_dividend [of a "2 * b"] have "b \<le> a"
    49     by (auto intro: trans)
    50   with \<open>0 < b\<close> have "0 < a div b" by (auto intro: div_positive)
    51   then have [simp]: "1 \<le> a div b" by (simp add: discrete)
    52   with \<open>0 < b\<close> have mod_less: "a mod b < b" by (simp add: pos_mod_bound)
    53   define w where "w = a div b mod 2"
    54   then have w_exhaust: "w = 0 \<or> w = 1" by auto
    55   have mod_w: "a mod (2 * b) = a mod b + b * w"
    56     by (simp add: w_def mod_mult2_eq ac_simps)
    57   from assms w_exhaust have "w = 1"
    58     by (auto simp add: mod_w) (insert mod_less, auto)
    59   with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp
    60   have "2 * (a div (2 * b)) = a div b - w"
    61     by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
    62   with \<open>w = 1\<close> have div: "2 * (a div (2 * b)) = a div b - 1" by simp
    63   then show ?P and ?Q
    64     by (simp_all add: div mod add_implies_diff [symmetric])
    65 qed
    66 
    67 lemma divmod_digit_0:
    68   assumes "0 < b" and "a mod (2 * b) < b"
    69   shows "2 * (a div (2 * b)) = a div b" (is "?P")
    70     and "a mod (2 * b) = a mod b" (is "?Q")
    71 proof -
    72   define w where "w = a div b mod 2"
    73   then have w_exhaust: "w = 0 \<or> w = 1" by auto
    74   have mod_w: "a mod (2 * b) = a mod b + b * w"
    75     by (simp add: w_def mod_mult2_eq ac_simps)
    76   moreover have "b \<le> a mod b + b"
    77   proof -
    78     from \<open>0 < b\<close> pos_mod_sign have "0 \<le> a mod b" by blast
    79     then have "0 + b \<le> a mod b + b" by (rule add_right_mono)
    80     then show ?thesis by simp
    81   qed
    82   moreover note assms w_exhaust
    83   ultimately have "w = 0" by auto
    84   with mod_w have mod: "a mod (2 * b) = a mod b" by simp
    85   have "2 * (a div (2 * b)) = a div b - w"
    86     by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
    87   with \<open>w = 0\<close> have div: "2 * (a div (2 * b)) = a div b" by simp
    88   then show ?P and ?Q
    89     by (simp_all add: div mod)
    90 qed
    91 
    92 lemma fst_divmod:
    93   "fst (divmod m n) = numeral m div numeral n"
    94   by (simp add: divmod_def)
    95 
    96 lemma snd_divmod:
    97   "snd (divmod m n) = numeral m mod numeral n"
    98   by (simp add: divmod_def)
    99 
   100 text \<open>
   101   This is a formulation of one step (referring to one digit position)
   102   in school-method division: compare the dividend at the current
   103   digit position with the remainder from previous division steps
   104   and evaluate accordingly.
   105 \<close>
   106 
   107 lemma divmod_step_eq [simp]:
   108   "divmod_step l (q, r) = (if numeral l \<le> r
   109     then (2 * q + 1, r - numeral l) else (2 * q, r))"
   110   by (simp add: divmod_step_def)
   111 
   112 text \<open>
   113   This is a formulation of school-method division.
   114   If the divisor is smaller than the dividend, terminate.
   115   If not, shift the dividend to the right until termination
   116   occurs and then reiterate single division steps in the
   117   opposite direction.
   118 \<close>
   119 
   120 lemma divmod_divmod_step:
   121   "divmod m n = (if m < n then (0, numeral m)
   122     else divmod_step n (divmod m (Num.Bit0 n)))"
   123 proof (cases "m < n")
   124   case True then have "numeral m < numeral n" by simp
   125   then show ?thesis
   126     by (simp add: prod_eq_iff div_less mod_less fst_divmod snd_divmod)
   127 next
   128   case False
   129   have "divmod m n =
   130     divmod_step n (numeral m div (2 * numeral n),
   131       numeral m mod (2 * numeral n))"
   132   proof (cases "numeral n \<le> numeral m mod (2 * numeral n)")
   133     case True
   134     with divmod_step_eq
   135       have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
   136         (2 * (numeral m div (2 * numeral n)) + 1, numeral m mod (2 * numeral n) - numeral n)"
   137         by simp
   138     moreover from True divmod_digit_1 [of "numeral m" "numeral n"]
   139       have "2 * (numeral m div (2 * numeral n)) + 1 = numeral m div numeral n"
   140       and "numeral m mod (2 * numeral n) - numeral n = numeral m mod numeral n"
   141       by simp_all
   142     ultimately show ?thesis by (simp only: divmod_def)
   143   next
   144     case False then have *: "numeral m mod (2 * numeral n) < numeral n"
   145       by (simp add: not_le)
   146     with divmod_step_eq
   147       have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
   148         (2 * (numeral m div (2 * numeral n)), numeral m mod (2 * numeral n))"
   149         by auto
   150     moreover from * divmod_digit_0 [of "numeral n" "numeral m"]
   151       have "2 * (numeral m div (2 * numeral n)) = numeral m div numeral n"
   152       and "numeral m mod (2 * numeral n) = numeral m mod numeral n"
   153       by (simp_all only: zero_less_numeral)
   154     ultimately show ?thesis by (simp only: divmod_def)
   155   qed
   156   then have "divmod m n =
   157     divmod_step n (numeral m div numeral (Num.Bit0 n),
   158       numeral m mod numeral (Num.Bit0 n))"
   159     by (simp only: numeral.simps distrib mult_1)
   160   then have "divmod m n = divmod_step n (divmod m (Num.Bit0 n))"
   161     by (simp add: divmod_def)
   162   with False show ?thesis by simp
   163 qed
   164 
   165 text \<open>The division rewrite proper -- first, trivial results involving \<open>1\<close>\<close>
   166 
   167 lemma divmod_trivial [simp]:
   168   "divmod Num.One Num.One = (numeral Num.One, 0)"
   169   "divmod (Num.Bit0 m) Num.One = (numeral (Num.Bit0 m), 0)"
   170   "divmod (Num.Bit1 m) Num.One = (numeral (Num.Bit1 m), 0)"
   171   "divmod num.One (num.Bit0 n) = (0, Numeral1)"
   172   "divmod num.One (num.Bit1 n) = (0, Numeral1)"
   173   using divmod_divmod_step [of "Num.One"] by (simp_all add: divmod_def)
   174 
   175 text \<open>Division by an even number is a right-shift\<close>
   176 
   177 lemma divmod_cancel [simp]:
   178   "divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))" (is ?P)
   179   "divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))" (is ?Q)
   180 proof -
   181   have *: "\<And>q. numeral (Num.Bit0 q) = 2 * numeral q"
   182     "\<And>q. numeral (Num.Bit1 q) = 2 * numeral q + 1"
   183     by (simp_all only: numeral_mult numeral.simps distrib) simp_all
   184   have "1 div 2 = 0" "1 mod 2 = 1" by (auto intro: div_less mod_less)
   185   then show ?P and ?Q
   186     by (simp_all add: fst_divmod snd_divmod prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1
   187       div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2]
   188       add.commute del: numeral_times_numeral)
   189 qed
   190 
   191 text \<open>The really hard work\<close>
   192 
   193 lemma divmod_steps [simp]:
   194   "divmod (num.Bit0 m) (num.Bit1 n) =
   195       (if m \<le> n then (0, numeral (num.Bit0 m))
   196        else divmod_step (num.Bit1 n)
   197              (divmod (num.Bit0 m)
   198                (num.Bit0 (num.Bit1 n))))"
   199   "divmod (num.Bit1 m) (num.Bit1 n) =
   200       (if m < n then (0, numeral (num.Bit1 m))
   201        else divmod_step (num.Bit1 n)
   202              (divmod (num.Bit1 m)
   203                (num.Bit0 (num.Bit1 n))))"
   204   by (simp_all add: divmod_divmod_step)
   205 
   206 lemmas divmod_algorithm_code = divmod_step_eq divmod_trivial divmod_cancel divmod_steps  
   207 
   208 text \<open>Special case: divisibility\<close>
   209 
   210 definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool"
   211 where
   212   "divides_aux qr \<longleftrightarrow> snd qr = 0"
   213 
   214 lemma divides_aux_eq [simp]:
   215   "divides_aux (q, r) \<longleftrightarrow> r = 0"
   216   by (simp add: divides_aux_def)
   217 
   218 lemma dvd_numeral_simp [simp]:
   219   "numeral m dvd numeral n \<longleftrightarrow> divides_aux (divmod n m)"
   220   by (simp add: divmod_def mod_eq_0_iff_dvd)
   221 
   222 text \<open>Generic computation of quotient and remainder\<close>  
   223 
   224 lemma numeral_div_numeral [simp]: 
   225   "numeral k div numeral l = fst (divmod k l)"
   226   by (simp add: fst_divmod)
   227 
   228 lemma numeral_mod_numeral [simp]: 
   229   "numeral k mod numeral l = snd (divmod k l)"
   230   by (simp add: snd_divmod)
   231 
   232 lemma one_div_numeral [simp]:
   233   "1 div numeral n = fst (divmod num.One n)"
   234   by (simp add: fst_divmod)
   235 
   236 lemma one_mod_numeral [simp]:
   237   "1 mod numeral n = snd (divmod num.One n)"
   238   by (simp add: snd_divmod)
   239 
   240 text \<open>Computing congruences modulo \<open>2 ^ q\<close>\<close>
   241 
   242 lemma cong_exp_iff_simps:
   243   "numeral n mod numeral Num.One = 0
   244     \<longleftrightarrow> True"
   245   "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = 0
   246     \<longleftrightarrow> numeral n mod numeral q = 0"
   247   "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = 0
   248     \<longleftrightarrow> False"
   249   "numeral m mod numeral Num.One = (numeral n mod numeral Num.One)
   250     \<longleftrightarrow> True"
   251   "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
   252     \<longleftrightarrow> True"
   253   "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
   254     \<longleftrightarrow> False"
   255   "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
   256     \<longleftrightarrow> (numeral n mod numeral q) = 0"
   257   "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
   258     \<longleftrightarrow> False"
   259   "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
   260     \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
   261   "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
   262     \<longleftrightarrow> False"
   263   "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
   264     \<longleftrightarrow> (numeral m mod numeral q) = 0"
   265   "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
   266     \<longleftrightarrow> False"
   267   "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
   268     \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
   269   by (auto simp add: case_prod_beta dest: arg_cong [of _ _ even])
   270 
   271 end
   272 
   273 hide_fact (open) div_less mod_less mod_less_eq_dividend mod_mult2_eq div_mult2_eq
   274 
   275 
   276 subsection \<open>More on division\<close>
   277 
   278 instantiation nat :: unique_euclidean_semiring_numeral
   279 begin
   280 
   281 definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat"
   282 where
   283   divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)"
   284 
   285 definition divmod_step_nat :: "num \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
   286 where
   287   "divmod_step_nat l qr = (let (q, r) = qr
   288     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
   289     else (2 * q, r))"
   290 
   291 instance by standard
   292   (auto simp add: divmod'_nat_def divmod_step_nat_def div_greater_zero_iff div_mult2_eq mod_mult2_eq)
   293 
   294 end
   295 
   296 declare divmod_algorithm_code [where ?'a = nat, code]
   297 
   298 lemma Suc_0_div_numeral [simp]:
   299   fixes k l :: num
   300   shows "Suc 0 div numeral k = fst (divmod Num.One k)"
   301   by (simp_all add: fst_divmod)
   302 
   303 lemma Suc_0_mod_numeral [simp]:
   304   fixes k l :: num
   305   shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
   306   by (simp_all add: snd_divmod)
   307 
   308 definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
   309   where "divmod_nat m n = (m div n, m mod n)"
   310 
   311 lemma fst_divmod_nat [simp]:
   312   "fst (divmod_nat m n) = m div n"
   313   by (simp add: divmod_nat_def)
   314 
   315 lemma snd_divmod_nat [simp]:
   316   "snd (divmod_nat m n) = m mod n"
   317   by (simp add: divmod_nat_def)
   318 
   319 lemma divmod_nat_if [code]:
   320   "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
   321     let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
   322   by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
   323 
   324 lemma [code]:
   325   "m div n = fst (divmod_nat m n)"
   326   "m mod n = snd (divmod_nat m n)"
   327   by simp_all
   328 
   329 inductive eucl_rel_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool"
   330   where eucl_rel_int_by0: "eucl_rel_int k 0 (0, k)"
   331   | eucl_rel_int_dividesI: "l \<noteq> 0 \<Longrightarrow> k = q * l \<Longrightarrow> eucl_rel_int k l (q, 0)"
   332   | eucl_rel_int_remainderI: "sgn r = sgn l \<Longrightarrow> \<bar>r\<bar> < \<bar>l\<bar>
   333       \<Longrightarrow> k = q * l + r \<Longrightarrow> eucl_rel_int k l (q, r)"
   334 
   335 lemma eucl_rel_int_iff:    
   336   "eucl_rel_int k l (q, r) \<longleftrightarrow> 
   337     k = l * q + r \<and>
   338      (if 0 < l then 0 \<le> r \<and> r < l else if l < 0 then l < r \<and> r \<le> 0 else q = 0)"
   339   by (cases "r = 0")
   340     (auto elim!: eucl_rel_int.cases intro: eucl_rel_int_by0 eucl_rel_int_dividesI eucl_rel_int_remainderI
   341     simp add: ac_simps sgn_1_pos sgn_1_neg)
   342 
   343 lemma unique_quotient_lemma:
   344   "b * q' + r' \<le> b * q + r \<Longrightarrow> 0 \<le> r' \<Longrightarrow> r' < b \<Longrightarrow> r < b \<Longrightarrow> q' \<le> (q::int)"
   345 apply (subgoal_tac "r' + b * (q'-q) \<le> r")
   346  prefer 2 apply (simp add: right_diff_distrib)
   347 apply (subgoal_tac "0 < b * (1 + q - q') ")
   348 apply (erule_tac [2] order_le_less_trans)
   349  prefer 2 apply (simp add: right_diff_distrib distrib_left)
   350 apply (subgoal_tac "b * q' < b * (1 + q) ")
   351  prefer 2 apply (simp add: right_diff_distrib distrib_left)
   352 apply (simp add: mult_less_cancel_left)
   353 done
   354 
   355 lemma unique_quotient_lemma_neg:
   356   "b * q' + r' \<le> b*q + r \<Longrightarrow> r \<le> 0 \<Longrightarrow> b < r \<Longrightarrow> b < r' \<Longrightarrow> q \<le> (q'::int)"
   357   by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma) auto
   358 
   359 lemma unique_quotient:
   360   "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> q = q'"
   361   apply (simp add: eucl_rel_int_iff linorder_neq_iff split: if_split_asm)
   362   apply (blast intro: order_antisym
   363     dest: order_eq_refl [THEN unique_quotient_lemma]
   364     order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
   365   done
   366 
   367 lemma unique_remainder:
   368   "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> r = r'"
   369 apply (subgoal_tac "q = q'")
   370  apply (simp add: eucl_rel_int_iff)
   371 apply (blast intro: unique_quotient)
   372 done
   373 
   374 lemma eucl_rel_int:
   375   "eucl_rel_int k l (k div l, k mod l)"
   376 proof (cases k rule: int_cases3)
   377   case zero
   378   then show ?thesis
   379     by (simp add: eucl_rel_int_iff divide_int_def modulo_int_def)
   380 next
   381   case (pos n)
   382   then show ?thesis
   383     using div_mult_mod_eq [of n]
   384     by (cases l rule: int_cases3)
   385       (auto simp del: of_nat_mult of_nat_add
   386         simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
   387         eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
   388 next
   389   case (neg n)
   390   then show ?thesis
   391     using div_mult_mod_eq [of n]
   392     by (cases l rule: int_cases3)
   393       (auto simp del: of_nat_mult of_nat_add
   394         simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
   395         eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
   396 qed
   397 
   398 lemma divmod_int_unique:
   399   assumes "eucl_rel_int k l (q, r)"
   400   shows div_int_unique: "k div l = q" and mod_int_unique: "k mod l = r"
   401   using assms eucl_rel_int [of k l]
   402   using unique_quotient [of k l] unique_remainder [of k l]
   403   by auto
   404 
   405 lemma div_abs_eq_div_nat:
   406   "\<bar>k\<bar> div \<bar>l\<bar> = int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)"
   407   by (simp add: divide_int_def)
   408 
   409 lemma mod_abs_eq_div_nat:
   410   "\<bar>k\<bar> mod \<bar>l\<bar> = int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)"
   411   by (simp add: modulo_int_def)
   412 
   413 lemma zdiv_int:
   414   "int (a div b) = int a div int b"
   415   by (simp add: divide_int_def sgn_1_pos)
   416 
   417 lemma zmod_int:
   418   "int (a mod b) = int a mod int b"
   419   by (simp add: modulo_int_def sgn_1_pos)
   420 
   421 lemma div_sgn_abs_cancel:
   422   fixes k l v :: int
   423   assumes "v \<noteq> 0"
   424   shows "(sgn v * \<bar>k\<bar>) div (sgn v * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
   425 proof -
   426   from assms have "sgn v = - 1 \<or> sgn v = 1"
   427     by (cases "v \<ge> 0") auto
   428   then show ?thesis
   429     using assms unfolding divide_int_def [of "sgn v * \<bar>k\<bar>" "sgn v * \<bar>l\<bar>"]
   430     by (fastforce simp add: not_less div_abs_eq_div_nat)
   431 qed
   432 
   433 lemma div_eq_sgn_abs:
   434   fixes k l v :: int
   435   assumes "sgn k = sgn l"
   436   shows "k div l = \<bar>k\<bar> div \<bar>l\<bar>"
   437 proof (cases "l = 0")
   438   case True
   439   then show ?thesis
   440     by simp
   441 next
   442   case False
   443   with assms have "(sgn k * \<bar>k\<bar>) div (sgn l * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
   444     using div_sgn_abs_cancel [of l k l] by simp
   445   then show ?thesis
   446     by (simp add: sgn_mult_abs)
   447 qed
   448 
   449 lemma div_dvd_sgn_abs:
   450   fixes k l :: int
   451   assumes "l dvd k"
   452   shows "k div l = (sgn k * sgn l) * (\<bar>k\<bar> div \<bar>l\<bar>)"
   453 proof (cases "k = 0 \<or> l = 0")
   454   case True
   455   then show ?thesis
   456     by auto
   457 next
   458   case False
   459   then have "k \<noteq> 0" and "l \<noteq> 0"
   460     by auto
   461   show ?thesis
   462   proof (cases "sgn l = sgn k")
   463     case True
   464     then show ?thesis
   465       by (simp add: div_eq_sgn_abs)
   466   next
   467     case False
   468     with \<open>k \<noteq> 0\<close> \<open>l \<noteq> 0\<close>
   469     have "sgn l * sgn k = - 1"
   470       by (simp add: sgn_if split: if_splits)
   471     with assms show ?thesis
   472       unfolding divide_int_def [of k l]
   473       by (auto simp add: zdiv_int ac_simps)
   474   qed
   475 qed
   476 
   477 lemma div_noneq_sgn_abs:
   478   fixes k l :: int
   479   assumes "l \<noteq> 0"
   480   assumes "sgn k \<noteq> sgn l"
   481   shows "k div l = - (\<bar>k\<bar> div \<bar>l\<bar>) - of_bool (\<not> l dvd k)"
   482   using assms
   483   by (simp only: divide_int_def [of k l], auto simp add: not_less zdiv_int)
   484   
   485 text\<open>Basic laws about division and remainder\<close>
   486 
   487 lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
   488   using eucl_rel_int [of a b]
   489   by (auto simp add: eucl_rel_int_iff prod_eq_iff)
   490 
   491 lemmas pos_mod_sign = pos_mod_conj [THEN conjunct1]
   492    and pos_mod_bound = pos_mod_conj [THEN conjunct2]
   493 
   494 lemma neg_mod_conj: "b < (0::int) \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b"
   495   using eucl_rel_int [of a b]
   496   by (auto simp add: eucl_rel_int_iff prod_eq_iff)
   497 
   498 lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
   499    and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
   500 
   501 
   502 subsubsection \<open>General Properties of div and mod\<close>
   503 
   504 lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
   505 apply (rule div_int_unique)
   506 apply (auto simp add: eucl_rel_int_iff)
   507 done
   508 
   509 lemma div_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a div b = 0"
   510 apply (rule div_int_unique)
   511 apply (auto simp add: eucl_rel_int_iff)
   512 done
   513 
   514 lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a div b = -1"
   515 apply (rule div_int_unique)
   516 apply (auto simp add: eucl_rel_int_iff)
   517 done
   518 
   519 lemma div_positive_int:
   520   "k div l > 0" if "k \<ge> l" and "l > 0" for k l :: int
   521   using that by (simp add: divide_int_def div_positive)
   522 
   523 (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
   524 
   525 lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"
   526 apply (rule_tac q = 0 in mod_int_unique)
   527 apply (auto simp add: eucl_rel_int_iff)
   528 done
   529 
   530 lemma mod_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a mod b = a"
   531 apply (rule_tac q = 0 in mod_int_unique)
   532 apply (auto simp add: eucl_rel_int_iff)
   533 done
   534 
   535 lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"
   536 apply (rule_tac q = "-1" in mod_int_unique)
   537 apply (auto simp add: eucl_rel_int_iff)
   538 done
   539 
   540 text\<open>There is no \<open>mod_neg_pos_trivial\<close>.\<close>
   541 
   542 
   543 subsubsection \<open>Laws for div and mod with Unary Minus\<close>
   544 
   545 lemma zminus1_lemma:
   546      "eucl_rel_int a b (q, r) ==> b \<noteq> 0
   547       ==> eucl_rel_int (-a) b (if r=0 then -q else -q - 1,
   548                           if r=0 then 0 else b-r)"
   549 by (force simp add: eucl_rel_int_iff right_diff_distrib)
   550 
   551 
   552 lemma zdiv_zminus1_eq_if:
   553      "b \<noteq> (0::int)
   554       ==> (-a) div b =
   555           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
   556 by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN div_int_unique])
   557 
   558 lemma zmod_zminus1_eq_if:
   559      "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
   560 apply (case_tac "b = 0", simp)
   561 apply (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN mod_int_unique])
   562 done
   563 
   564 lemma zmod_zminus1_not_zero:
   565   fixes k l :: int
   566   shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
   567   by (simp add: mod_eq_0_iff_dvd)
   568 
   569 lemma zmod_zminus2_not_zero:
   570   fixes k l :: int
   571   shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
   572   by (simp add: mod_eq_0_iff_dvd)
   573 
   574 lemma zdiv_zminus2_eq_if:
   575   "b \<noteq> (0::int)
   576       ==> a div (-b) =
   577           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
   578   by (auto simp add: zdiv_zminus1_eq_if div_minus_right)
   579 
   580 lemma zmod_zminus2_eq_if:
   581   "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
   582   by (auto simp add: zmod_zminus1_eq_if mod_minus_right)
   583 
   584 
   585 subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
   586 
   587 lemma zdiv_mono1: "[| a \<le> a';  0 < (b::int) |] ==> a div b \<le> a' div b"
   588 using mult_div_mod_eq [symmetric, of a b]
   589 using mult_div_mod_eq [symmetric, of a' b]
   590 apply -
   591 apply (rule unique_quotient_lemma)
   592 apply (erule subst)
   593 apply (erule subst, simp_all)
   594 done
   595 
   596 lemma zdiv_mono1_neg: "[| a \<le> a';  (b::int) < 0 |] ==> a' div b \<le> a div b"
   597 using mult_div_mod_eq [symmetric, of a b]
   598 using mult_div_mod_eq [symmetric, of a' b]
   599 apply -
   600 apply (rule unique_quotient_lemma_neg)
   601 apply (erule subst)
   602 apply (erule subst, simp_all)
   603 done
   604 
   605 
   606 subsubsection \<open>Monotonicity in the Second Argument (Divisor)\<close>
   607 
   608 lemma q_pos_lemma:
   609      "[| 0 \<le> b'*q' + r'; r' < b';  0 < b' |] ==> 0 \<le> (q'::int)"
   610 apply (subgoal_tac "0 < b'* (q' + 1) ")
   611  apply (simp add: zero_less_mult_iff)
   612 apply (simp add: distrib_left)
   613 done
   614 
   615 lemma zdiv_mono2_lemma:
   616      "[| b*q + r = b'*q' + r';  0 \<le> b'*q' + r';
   617          r' < b';  0 \<le> r;  0 < b';  b' \<le> b |]
   618       ==> q \<le> (q'::int)"
   619 apply (frule q_pos_lemma, assumption+)
   620 apply (subgoal_tac "b*q < b* (q' + 1) ")
   621  apply (simp add: mult_less_cancel_left)
   622 apply (subgoal_tac "b*q = r' - r + b'*q'")
   623  prefer 2 apply simp
   624 apply (simp (no_asm_simp) add: distrib_left)
   625 apply (subst add.commute, rule add_less_le_mono, arith)
   626 apply (rule mult_right_mono, auto)
   627 done
   628 
   629 lemma zdiv_mono2:
   630      "[| (0::int) \<le> a;  0 < b';  b' \<le> b |] ==> a div b \<le> a div b'"
   631 apply (subgoal_tac "b \<noteq> 0")
   632   prefer 2 apply arith
   633 using mult_div_mod_eq [symmetric, of a b]
   634 using mult_div_mod_eq [symmetric, of a b']
   635 apply -
   636 apply (rule zdiv_mono2_lemma)
   637 apply (erule subst)
   638 apply (erule subst, simp_all)
   639 done
   640 
   641 lemma q_neg_lemma:
   642      "[| b'*q' + r' < 0;  0 \<le> r';  0 < b' |] ==> q' \<le> (0::int)"
   643 apply (subgoal_tac "b'*q' < 0")
   644  apply (simp add: mult_less_0_iff, arith)
   645 done
   646 
   647 lemma zdiv_mono2_neg_lemma:
   648      "[| b*q + r = b'*q' + r';  b'*q' + r' < 0;
   649          r < b;  0 \<le> r';  0 < b';  b' \<le> b |]
   650       ==> q' \<le> (q::int)"
   651 apply (frule q_neg_lemma, assumption+)
   652 apply (subgoal_tac "b*q' < b* (q + 1) ")
   653  apply (simp add: mult_less_cancel_left)
   654 apply (simp add: distrib_left)
   655 apply (subgoal_tac "b*q' \<le> b'*q'")
   656  prefer 2 apply (simp add: mult_right_mono_neg, arith)
   657 done
   658 
   659 lemma zdiv_mono2_neg:
   660      "[| a < (0::int);  0 < b';  b' \<le> b |] ==> a div b' \<le> a div b"
   661 using mult_div_mod_eq [symmetric, of a b]
   662 using mult_div_mod_eq [symmetric, of a b']
   663 apply -
   664 apply (rule zdiv_mono2_neg_lemma)
   665 apply (erule subst)
   666 apply (erule subst, simp_all)
   667 done
   668 
   669 
   670 subsubsection \<open>More Algebraic Laws for div and mod\<close>
   671 
   672 lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
   673   by (fact div_mult1_eq)
   674 
   675 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
   676 lemma zdiv_zadd1_eq:
   677      "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
   678   by (fact div_add1_eq)
   679 
   680 lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
   681 by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
   682 
   683 (* REVISIT: should this be generalized to all semiring_div types? *)
   684 lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
   685 
   686 
   687 subsubsection \<open>Proving  @{term "a div (b * c) = (a div b) div c"}\<close>
   688 
   689 (*The condition c>0 seems necessary.  Consider that 7 div ~6 = ~2 but
   690   7 div 2 div ~3 = 3 div ~3 = ~1.  The subcase (a div b) mod c = 0 seems
   691   to cause particular problems.*)
   692 
   693 text\<open>first, four lemmas to bound the remainder for the cases b<0 and b>0\<close>
   694 
   695 lemma zmult2_lemma_aux1: "[| (0::int) < c;  b < r;  r \<le> 0 |] ==> b * c < b * (q mod c) + r"
   696 apply (subgoal_tac "b * (c - q mod c) < r * 1")
   697  apply (simp add: algebra_simps)
   698 apply (rule order_le_less_trans)
   699  apply (erule_tac [2] mult_strict_right_mono)
   700  apply (rule mult_left_mono_neg)
   701   using add1_zle_eq[of "q mod c"]apply(simp add: algebra_simps)
   702  apply (simp)
   703 apply (simp)
   704 done
   705 
   706 lemma zmult2_lemma_aux2:
   707      "[| (0::int) < c;   b < r;  r \<le> 0 |] ==> b * (q mod c) + r \<le> 0"
   708 apply (subgoal_tac "b * (q mod c) \<le> 0")
   709  apply arith
   710 apply (simp add: mult_le_0_iff)
   711 done
   712 
   713 lemma zmult2_lemma_aux3: "[| (0::int) < c;  0 \<le> r;  r < b |] ==> 0 \<le> b * (q mod c) + r"
   714 apply (subgoal_tac "0 \<le> b * (q mod c) ")
   715 apply arith
   716 apply (simp add: zero_le_mult_iff)
   717 done
   718 
   719 lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 \<le> r; r < b |] ==> b * (q mod c) + r < b * c"
   720 apply (subgoal_tac "r * 1 < b * (c - q mod c) ")
   721  apply (simp add: right_diff_distrib)
   722 apply (rule order_less_le_trans)
   723  apply (erule mult_strict_right_mono)
   724  apply (rule_tac [2] mult_left_mono)
   725   apply simp
   726  using add1_zle_eq[of "q mod c"] apply (simp add: algebra_simps)
   727 apply simp
   728 done
   729 
   730 lemma zmult2_lemma: "[| eucl_rel_int a b (q, r); 0 < c |]
   731       ==> eucl_rel_int a (b * c) (q div c, b*(q mod c) + r)"
   732 by (auto simp add: mult.assoc eucl_rel_int_iff linorder_neq_iff
   733                    zero_less_mult_iff distrib_left [symmetric]
   734                    zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: if_split_asm)
   735 
   736 lemma zdiv_zmult2_eq:
   737   fixes a b c :: int
   738   shows "0 \<le> c \<Longrightarrow> a div (b * c) = (a div b) div c"
   739 apply (case_tac "b = 0", simp)
   740 apply (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN div_int_unique])
   741 done
   742 
   743 lemma zmod_zmult2_eq:
   744   fixes a b c :: int
   745   shows "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
   746 apply (case_tac "b = 0", simp)
   747 apply (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN mod_int_unique])
   748 done
   749 
   750 lemma div_pos_geq:
   751   fixes k l :: int
   752   assumes "0 < l" and "l \<le> k"
   753   shows "k div l = (k - l) div l + 1"
   754 proof -
   755   have "k = (k - l) + l" by simp
   756   then obtain j where k: "k = j + l" ..
   757   with assms show ?thesis by (simp add: div_add_self2)
   758 qed
   759 
   760 lemma mod_pos_geq:
   761   fixes k l :: int
   762   assumes "0 < l" and "l \<le> k"
   763   shows "k mod l = (k - l) mod l"
   764 proof -
   765   have "k = (k - l) + l" by simp
   766   then obtain j where k: "k = j + l" ..
   767   with assms show ?thesis by simp
   768 qed
   769 
   770 
   771 subsubsection \<open>Splitting Rules for div and mod\<close>
   772 
   773 text\<open>The proofs of the two lemmas below are essentially identical\<close>
   774 
   775 lemma split_pos_lemma:
   776  "0<k ==>
   777     P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
   778 apply (rule iffI, clarify)
   779  apply (erule_tac P="P x y" for x y in rev_mp)
   780  apply (subst mod_add_eq [symmetric])
   781  apply (subst zdiv_zadd1_eq)
   782  apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)
   783 txt\<open>converse direction\<close>
   784 apply (drule_tac x = "n div k" in spec)
   785 apply (drule_tac x = "n mod k" in spec, simp)
   786 done
   787 
   788 lemma split_neg_lemma:
   789  "k<0 ==>
   790     P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
   791 apply (rule iffI, clarify)
   792  apply (erule_tac P="P x y" for x y in rev_mp)
   793  apply (subst mod_add_eq [symmetric])
   794  apply (subst zdiv_zadd1_eq)
   795  apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)
   796 txt\<open>converse direction\<close>
   797 apply (drule_tac x = "n div k" in spec)
   798 apply (drule_tac x = "n mod k" in spec, simp)
   799 done
   800 
   801 lemma split_zdiv:
   802  "P(n div k :: int) =
   803   ((k = 0 --> P 0) &
   804    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) &
   805    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i)))"
   806 apply (case_tac "k=0", simp)
   807 apply (simp only: linorder_neq_iff)
   808 apply (erule disjE)
   809  apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"]
   810                       split_neg_lemma [of concl: "%x y. P x"])
   811 done
   812 
   813 lemma split_zmod:
   814  "P(n mod k :: int) =
   815   ((k = 0 --> P n) &
   816    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P j)) &
   817    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P j)))"
   818 apply (case_tac "k=0", simp)
   819 apply (simp only: linorder_neq_iff)
   820 apply (erule disjE)
   821  apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"]
   822                       split_neg_lemma [of concl: "%x y. P y"])
   823 done
   824 
   825 text \<open>Enable (lin)arith to deal with @{const divide} and @{const modulo}
   826   when these are applied to some constant that is of the form
   827   @{term "numeral k"}:\<close>
   828 declare split_zdiv [of _ _ "numeral k", arith_split] for k
   829 declare split_zmod [of _ _ "numeral k", arith_split] for k
   830 
   831 
   832 subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
   833 
   834 lemma pos_eucl_rel_int_mult_2:
   835   assumes "0 \<le> b"
   836   assumes "eucl_rel_int a b (q, r)"
   837   shows "eucl_rel_int (1 + 2*a) (2*b) (q, 1 + 2*r)"
   838   using assms unfolding eucl_rel_int_iff by auto
   839 
   840 lemma neg_eucl_rel_int_mult_2:
   841   assumes "b \<le> 0"
   842   assumes "eucl_rel_int (a + 1) b (q, r)"
   843   shows "eucl_rel_int (1 + 2*a) (2*b) (q, 2*r - 1)"
   844   using assms unfolding eucl_rel_int_iff by auto
   845 
   846 text\<open>computing div by shifting\<close>
   847 
   848 lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
   849   using pos_eucl_rel_int_mult_2 [OF _ eucl_rel_int]
   850   by (rule div_int_unique)
   851 
   852 lemma neg_zdiv_mult_2:
   853   assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
   854   using neg_eucl_rel_int_mult_2 [OF A eucl_rel_int]
   855   by (rule div_int_unique)
   856 
   857 (* FIXME: add rules for negative numerals *)
   858 lemma zdiv_numeral_Bit0 [simp]:
   859   "numeral (Num.Bit0 v) div numeral (Num.Bit0 w) =
   860     numeral v div (numeral w :: int)"
   861   unfolding numeral.simps unfolding mult_2 [symmetric]
   862   by (rule div_mult_mult1, simp)
   863 
   864 lemma zdiv_numeral_Bit1 [simp]:
   865   "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) =
   866     (numeral v div (numeral w :: int))"
   867   unfolding numeral.simps
   868   unfolding mult_2 [symmetric] add.commute [of _ 1]
   869   by (rule pos_zdiv_mult_2, simp)
   870 
   871 lemma pos_zmod_mult_2:
   872   fixes a b :: int
   873   assumes "0 \<le> a"
   874   shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"
   875   using pos_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
   876   by (rule mod_int_unique)
   877 
   878 lemma neg_zmod_mult_2:
   879   fixes a b :: int
   880   assumes "a \<le> 0"
   881   shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"
   882   using neg_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
   883   by (rule mod_int_unique)
   884 
   885 (* FIXME: add rules for negative numerals *)
   886 lemma zmod_numeral_Bit0 [simp]:
   887   "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =
   888     (2::int) * (numeral v mod numeral w)"
   889   unfolding numeral_Bit0 [of v] numeral_Bit0 [of w]
   890   unfolding mult_2 [symmetric] by (rule mod_mult_mult1)
   891 
   892 lemma zmod_numeral_Bit1 [simp]:
   893   "numeral (Num.Bit1 v) mod numeral (Num.Bit0 w) =
   894     2 * (numeral v mod numeral w) + (1::int)"
   895   unfolding numeral_Bit1 [of v] numeral_Bit0 [of w]
   896   unfolding mult_2 [symmetric] add.commute [of _ 1]
   897   by (rule pos_zmod_mult_2, simp)
   898 
   899 lemma zdiv_eq_0_iff:
   900  "(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")
   901 proof
   902   assume ?L
   903   have "?L \<longrightarrow> ?R" by (rule split_zdiv[THEN iffD2]) simp
   904   with \<open>?L\<close> show ?R by blast
   905 next
   906   assume ?R thus ?L
   907     by(auto simp: div_pos_pos_trivial div_neg_neg_trivial)
   908 qed
   909 
   910 lemma zmod_trival_iff:
   911   fixes i k :: int
   912   shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
   913 proof -
   914   have "i mod k = i \<longleftrightarrow> i div k = 0"
   915     by safe (insert div_mult_mod_eq [of i k], auto)
   916   with zdiv_eq_0_iff
   917   show ?thesis
   918     by simp
   919 qed
   920 
   921   
   922 subsubsection \<open>Quotients of Signs\<close>
   923 
   924 lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
   925 by (simp add: divide_int_def)
   926 
   927 lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
   928 by (simp add: modulo_int_def)
   929 
   930 lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"
   931 apply (subgoal_tac "a div b \<le> -1", force)
   932 apply (rule order_trans)
   933 apply (rule_tac a' = "-1" in zdiv_mono1)
   934 apply (auto simp add: div_eq_minus1)
   935 done
   936 
   937 lemma div_nonneg_neg_le0: "[| (0::int) \<le> a; b < 0 |] ==> a div b \<le> 0"
   938 by (drule zdiv_mono1_neg, auto)
   939 
   940 lemma div_nonpos_pos_le0: "[| (a::int) \<le> 0; b > 0 |] ==> a div b \<le> 0"
   941 by (drule zdiv_mono1, auto)
   942 
   943 text\<open>Now for some equivalences of the form \<open>a div b >=< 0 \<longleftrightarrow> \<dots>\<close>
   944 conditional upon the sign of \<open>a\<close> or \<open>b\<close>. There are many more.
   945 They should all be simp rules unless that causes too much search.\<close>
   946 
   947 lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"
   948 apply auto
   949 apply (drule_tac [2] zdiv_mono1)
   950 apply (auto simp add: linorder_neq_iff)
   951 apply (simp (no_asm_use) add: linorder_not_less [symmetric])
   952 apply (blast intro: div_neg_pos_less0)
   953 done
   954 
   955 lemma pos_imp_zdiv_pos_iff:
   956   "0<k \<Longrightarrow> 0 < (i::int) div k \<longleftrightarrow> k \<le> i"
   957 using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k]
   958 by arith
   959 
   960 lemma neg_imp_zdiv_nonneg_iff:
   961   "b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))"
   962 apply (subst div_minus_minus [symmetric])
   963 apply (subst pos_imp_zdiv_nonneg_iff, auto)
   964 done
   965 
   966 (*But not (a div b \<le> 0 iff a\<le>0); consider a=1, b=2 when a div b = 0.*)
   967 lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)"
   968 by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff)
   969 
   970 (*Again the law fails for \<le>: consider a = -1, b = -2 when a div b = 0*)
   971 lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"
   972 by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)
   973 
   974 lemma nonneg1_imp_zdiv_pos_iff:
   975   "(0::int) <= a \<Longrightarrow> (a div b > 0) = (a >= b & b>0)"
   976 apply rule
   977  apply rule
   978   using div_pos_pos_trivial[of a b]apply arith
   979  apply(cases "b=0")apply simp
   980  using div_nonneg_neg_le0[of a b]apply arith
   981 using int_one_le_iff_zero_less[of "a div b"] zdiv_mono1[of b a b]apply simp
   982 done
   983 
   984 lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 ==> m mod k \<le> m"
   985 apply (rule split_zmod[THEN iffD2])
   986 apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le)
   987 done
   988 
   989 
   990 subsubsection \<open>Computation of Division and Remainder\<close>
   991 
   992 instantiation int :: unique_euclidean_semiring_numeral
   993 begin
   994 
   995 definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int"
   996 where
   997   "divmod_int m n = (numeral m div numeral n, numeral m mod numeral n)"
   998 
   999 definition divmod_step_int :: "num \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int"
  1000 where
  1001   "divmod_step_int l qr = (let (q, r) = qr
  1002     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
  1003     else (2 * q, r))"
  1004 
  1005 instance
  1006   by standard (auto intro: zmod_le_nonneg_dividend simp add: divmod_int_def divmod_step_int_def
  1007     pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial zmod_zmult2_eq zdiv_zmult2_eq)
  1008 
  1009 end
  1010 
  1011 declare divmod_algorithm_code [where ?'a = int, code]
  1012 
  1013 context
  1014 begin
  1015   
  1016 qualified definition adjust_div :: "int \<times> int \<Rightarrow> int"
  1017 where
  1018   "adjust_div qr = (let (q, r) = qr in q + of_bool (r \<noteq> 0))"
  1019 
  1020 qualified lemma adjust_div_eq [simp, code]:
  1021   "adjust_div (q, r) = q + of_bool (r \<noteq> 0)"
  1022   by (simp add: adjust_div_def)
  1023 
  1024 qualified definition adjust_mod :: "int \<Rightarrow> int \<Rightarrow> int"
  1025 where
  1026   [simp]: "adjust_mod l r = (if r = 0 then 0 else l - r)"
  1027 
  1028 lemma minus_numeral_div_numeral [simp]:
  1029   "- numeral m div numeral n = - (adjust_div (divmod m n) :: int)"
  1030 proof -
  1031   have "int (fst (divmod m n)) = fst (divmod m n)"
  1032     by (simp only: fst_divmod divide_int_def) auto
  1033   then show ?thesis
  1034     by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
  1035 qed
  1036 
  1037 lemma minus_numeral_mod_numeral [simp]:
  1038   "- numeral m mod numeral n = adjust_mod (numeral n) (snd (divmod m n) :: int)"
  1039 proof (cases "snd (divmod m n) = (0::int)")
  1040   case True
  1041   then show ?thesis
  1042     by (simp add: mod_eq_0_iff_dvd divides_aux_def)
  1043 next
  1044   case False
  1045   then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
  1046     by (simp only: snd_divmod modulo_int_def) auto
  1047   then show ?thesis
  1048     by (simp add: divides_aux_def adjust_div_def)
  1049       (simp add: divides_aux_def modulo_int_def)
  1050 qed
  1051 
  1052 lemma numeral_div_minus_numeral [simp]:
  1053   "numeral m div - numeral n = - (adjust_div (divmod m n) :: int)"
  1054 proof -
  1055   have "int (fst (divmod m n)) = fst (divmod m n)"
  1056     by (simp only: fst_divmod divide_int_def) auto
  1057   then show ?thesis
  1058     by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
  1059 qed
  1060   
  1061 lemma numeral_mod_minus_numeral [simp]:
  1062   "numeral m mod - numeral n = - adjust_mod (numeral n) (snd (divmod m n) :: int)"
  1063 proof (cases "snd (divmod m n) = (0::int)")
  1064   case True
  1065   then show ?thesis
  1066     by (simp add: mod_eq_0_iff_dvd divides_aux_def)
  1067 next
  1068   case False
  1069   then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
  1070     by (simp only: snd_divmod modulo_int_def) auto
  1071   then show ?thesis
  1072     by (simp add: divides_aux_def adjust_div_def)
  1073       (simp add: divides_aux_def modulo_int_def)
  1074 qed
  1075 
  1076 lemma minus_one_div_numeral [simp]:
  1077   "- 1 div numeral n = - (adjust_div (divmod Num.One n) :: int)"
  1078   using minus_numeral_div_numeral [of Num.One n] by simp  
  1079 
  1080 lemma minus_one_mod_numeral [simp]:
  1081   "- 1 mod numeral n = adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
  1082   using minus_numeral_mod_numeral [of Num.One n] by simp
  1083 
  1084 lemma one_div_minus_numeral [simp]:
  1085   "1 div - numeral n = - (adjust_div (divmod Num.One n) :: int)"
  1086   using numeral_div_minus_numeral [of Num.One n] by simp
  1087   
  1088 lemma one_mod_minus_numeral [simp]:
  1089   "1 mod - numeral n = - adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
  1090   using numeral_mod_minus_numeral [of Num.One n] by simp
  1091 
  1092 end
  1093 
  1094 
  1095 subsubsection \<open>Further properties\<close>
  1096 
  1097 lemma div_int_pos_iff:
  1098   "k div l \<ge> 0 \<longleftrightarrow> k = 0 \<or> l = 0 \<or> k \<ge> 0 \<and> l \<ge> 0
  1099     \<or> k < 0 \<and> l < 0"
  1100   for k l :: int
  1101   apply (cases "k = 0 \<or> l = 0")
  1102    apply (auto simp add: pos_imp_zdiv_nonneg_iff neg_imp_zdiv_nonneg_iff)
  1103   apply (rule ccontr)
  1104   apply (simp add: neg_imp_zdiv_nonneg_iff)
  1105   done
  1106 
  1107 lemma mod_int_pos_iff:
  1108   "k mod l \<ge> 0 \<longleftrightarrow> l dvd k \<or> l = 0 \<and> k \<ge> 0 \<or> l > 0"
  1109   for k l :: int
  1110   apply (cases "l > 0")
  1111    apply (simp_all add: dvd_eq_mod_eq_0)
  1112   apply (use neg_mod_conj [of l k] in \<open>auto simp add: le_less not_less\<close>)
  1113   done
  1114 
  1115 text \<open>Simplify expresions in which div and mod combine numerical constants\<close>
  1116 
  1117 lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
  1118   by (rule div_int_unique [of a b q r]) (simp add: eucl_rel_int_iff)
  1119 
  1120 lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
  1121   by (rule div_int_unique [of a b q r],
  1122     simp add: eucl_rel_int_iff)
  1123 
  1124 lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
  1125   by (rule mod_int_unique [of a b q r],
  1126     simp add: eucl_rel_int_iff)
  1127 
  1128 lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
  1129   by (rule mod_int_unique [of a b q r],
  1130     simp add: eucl_rel_int_iff)
  1131 
  1132 lemma abs_div: "(y::int) dvd x \<Longrightarrow> \<bar>x div y\<bar> = \<bar>x\<bar> div \<bar>y\<bar>"
  1133 by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
  1134 
  1135 text\<open>Suggested by Matthias Daum\<close>
  1136 lemma int_power_div_base:
  1137      "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
  1138 apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)")
  1139  apply (erule ssubst)
  1140  apply (simp only: power_add)
  1141  apply simp_all
  1142 done
  1143 
  1144 text \<open>Distributive laws for function \<open>nat\<close>.\<close>
  1145 
  1146 lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"
  1147 apply (rule linorder_cases [of y 0])
  1148 apply (simp add: div_nonneg_neg_le0)
  1149 apply simp
  1150 apply (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int)
  1151 done
  1152 
  1153 (*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*)
  1154 lemma nat_mod_distrib:
  1155   "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x mod y) = nat x mod nat y"
  1156 apply (case_tac "y = 0", simp)
  1157 apply (simp add: nat_eq_iff zmod_int)
  1158 done
  1159 
  1160 text\<open>Suggested by Matthias Daum\<close>
  1161 lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
  1162 apply (subgoal_tac "nat x div nat k < nat x")
  1163  apply (simp add: nat_div_distrib [symmetric])
  1164 apply (rule div_less_dividend, simp_all)
  1165 done
  1166 
  1167 lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
  1168   shows "\<exists>q. x = y + n * q"
  1169 proof-
  1170   from xy have th: "int x - int y = int (x - y)" by simp
  1171   from xyn have "int x mod int n = int y mod int n"
  1172     by (simp add: zmod_int [symmetric])
  1173   hence "int n dvd int x - int y" by (simp only: mod_eq_dvd_iff [symmetric])
  1174   hence "n dvd x - y" by (simp add: th zdvd_int)
  1175   then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
  1176 qed
  1177 
  1178 lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)"
  1179   (is "?lhs = ?rhs")
  1180 proof
  1181   assume H: "x mod n = y mod n"
  1182   {assume xy: "x \<le> y"
  1183     from H have th: "y mod n = x mod n" by simp
  1184     from nat_mod_eq_lemma[OF th xy] have ?rhs
  1185       apply clarify  apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}
  1186   moreover
  1187   {assume xy: "y \<le> x"
  1188     from nat_mod_eq_lemma[OF H xy] have ?rhs
  1189       apply clarify  apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}
  1190   ultimately  show ?rhs using linear[of x y] by blast
  1191 next
  1192   assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast
  1193   hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp
  1194   thus  ?lhs by simp
  1195 qed
  1196 
  1197 
  1198 subsubsection \<open>Dedicated simproc for calculation\<close>
  1199 
  1200 text \<open>
  1201   There is space for improvement here: the calculation itself
  1202   could be carried out outside the logic, and a generic simproc
  1203   (simplifier setup) for generic calculation would be helpful. 
  1204 \<close>
  1205 
  1206 simproc_setup numeral_divmod
  1207   ("0 div 0 :: 'a :: unique_euclidean_semiring_numeral" | "0 mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
  1208    "0 div 1 :: 'a :: unique_euclidean_semiring_numeral" | "0 mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
  1209    "0 div - 1 :: int" | "0 mod - 1 :: int" |
  1210    "0 div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "0 mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
  1211    "0 div - numeral b :: int" | "0 mod - numeral b :: int" |
  1212    "1 div 0 :: 'a :: unique_euclidean_semiring_numeral" | "1 mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
  1213    "1 div 1 :: 'a :: unique_euclidean_semiring_numeral" | "1 mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
  1214    "1 div - 1 :: int" | "1 mod - 1 :: int" |
  1215    "1 div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "1 mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
  1216    "1 div - numeral b :: int" |"1 mod - numeral b :: int" |
  1217    "- 1 div 0 :: int" | "- 1 mod 0 :: int" | "- 1 div 1 :: int" | "- 1 mod 1 :: int" |
  1218    "- 1 div - 1 :: int" | "- 1 mod - 1 :: int" | "- 1 div numeral b :: int" | "- 1 mod numeral b :: int" |
  1219    "- 1 div - numeral b :: int" | "- 1 mod - numeral b :: int" |
  1220    "numeral a div 0 :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
  1221    "numeral a div 1 :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
  1222    "numeral a div - 1 :: int" | "numeral a mod - 1 :: int" |
  1223    "numeral a div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
  1224    "numeral a div - numeral b :: int" | "numeral a mod - numeral b :: int" |
  1225    "- numeral a div 0 :: int" | "- numeral a mod 0 :: int" |
  1226    "- numeral a div 1 :: int" | "- numeral a mod 1 :: int" |
  1227    "- numeral a div - 1 :: int" | "- numeral a mod - 1 :: int" |
  1228    "- numeral a div numeral b :: int" | "- numeral a mod numeral b :: int" |
  1229    "- numeral a div - numeral b :: int" | "- numeral a mod - numeral b :: int") =
  1230 \<open> let
  1231     val if_cong = the (Code.get_case_cong @{theory} @{const_name If});
  1232     fun successful_rewrite ctxt ct =
  1233       let
  1234         val thm = Simplifier.rewrite ctxt ct
  1235       in if Thm.is_reflexive thm then NONE else SOME thm end;
  1236   in fn phi =>
  1237     let
  1238       val simps = Morphism.fact phi (@{thms div_0 mod_0 div_by_0 mod_by_0 div_by_1 mod_by_1
  1239         one_div_numeral one_mod_numeral minus_one_div_numeral minus_one_mod_numeral
  1240         one_div_minus_numeral one_mod_minus_numeral
  1241         numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
  1242         numeral_div_minus_numeral numeral_mod_minus_numeral
  1243         div_minus_minus mod_minus_minus Divides.adjust_div_eq of_bool_eq one_neq_zero
  1244         numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial
  1245         divmod_cancel divmod_steps divmod_step_eq fst_conv snd_conv numeral_One
  1246         case_prod_beta rel_simps Divides.adjust_mod_def div_minus1_right mod_minus1_right
  1247         minus_minus numeral_times_numeral mult_zero_right mult_1_right}
  1248         @ [@{lemma "0 = 0 \<longleftrightarrow> True" by simp}]);
  1249       fun prepare_simpset ctxt = HOL_ss |> Simplifier.simpset_map ctxt
  1250         (Simplifier.add_cong if_cong #> fold Simplifier.add_simp simps)
  1251     in fn ctxt => successful_rewrite (Simplifier.put_simpset (prepare_simpset ctxt) ctxt) end
  1252   end;
  1253 \<close>
  1254 
  1255 
  1256 subsubsection \<open>Code generation\<close>
  1257 
  1258 lemma [code]:
  1259   fixes k :: int
  1260   shows 
  1261     "k div 0 = 0"
  1262     "k mod 0 = k"
  1263     "0 div k = 0"
  1264     "0 mod k = 0"
  1265     "k div Int.Pos Num.One = k"
  1266     "k mod Int.Pos Num.One = 0"
  1267     "k div Int.Neg Num.One = - k"
  1268     "k mod Int.Neg Num.One = 0"
  1269     "Int.Pos m div Int.Pos n = (fst (divmod m n) :: int)"
  1270     "Int.Pos m mod Int.Pos n = (snd (divmod m n) :: int)"
  1271     "Int.Neg m div Int.Pos n = - (Divides.adjust_div (divmod m n) :: int)"
  1272     "Int.Neg m mod Int.Pos n = Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
  1273     "Int.Pos m div Int.Neg n = - (Divides.adjust_div (divmod m n) :: int)"
  1274     "Int.Pos m mod Int.Neg n = - Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
  1275     "Int.Neg m div Int.Neg n = (fst (divmod m n) :: int)"
  1276     "Int.Neg m mod Int.Neg n = - (snd (divmod m n) :: int)"
  1277   by simp_all
  1278 
  1279 code_identifier
  1280   code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  1281 
  1282 lemma dvd_eq_mod_eq_0_numeral:
  1283   "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semidom_modulo)"
  1284   by (fact dvd_eq_mod_eq_0)
  1285 
  1286 declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
  1287 
  1288 
  1289 subsubsection \<open>Lemmas of doubtful value\<close>
  1290 
  1291 lemma mod_mult_self3':
  1292   "Suc (k * n + m) mod n = Suc m mod n"
  1293   by (fact Suc_mod_mult_self3)
  1294 
  1295 lemma mod_Suc_eq_Suc_mod:
  1296   "Suc m mod n = Suc (m mod n) mod n"
  1297   by (simp add: mod_simps)
  1298 
  1299 lemma div_geq:
  1300   "m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat
  1301   by (rule le_div_geq) (use that in \<open>simp_all add: not_less\<close>)
  1302 
  1303 lemma mod_geq:
  1304   "m mod n = (m - n) mod n" if "\<not> m < n" for m n :: nat
  1305   by (rule le_mod_geq) (use that in \<open>simp add: not_less\<close>)
  1306 
  1307 lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
  1308   by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
  1309 
  1310 lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
  1311 
  1312 (*Loses information, namely we also have r<d provided d is nonzero*)
  1313 lemma mod_eqD:
  1314   fixes m d r q :: nat
  1315   assumes "m mod d = r"
  1316   shows "\<exists>q. m = r + q * d"
  1317 proof -
  1318   from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast
  1319   with assms have "m = r + q * d" by simp
  1320   then show ?thesis ..
  1321 qed
  1322 
  1323 lemmas even_times_iff = even_mult_iff -- \<open>FIXME duplicate\<close>
  1324 
  1325 lemma mod_2_not_eq_zero_eq_one_nat:
  1326   fixes n :: nat
  1327   shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
  1328   by (fact not_mod_2_eq_0_eq_1)
  1329 
  1330 lemma even_int_iff [simp]: "even (int n) \<longleftrightarrow> even n"
  1331   by (fact even_of_nat)
  1332 
  1333 lemma is_unit_int:
  1334   "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
  1335   by auto
  1336 
  1337 end