src/HOL/Divides.thy
author haftmann
Sun Oct 08 22:28:21 2017 +0200 (21 months ago)
changeset 66806 a4e82b58d833
parent 66801 f3fda9777f9a
child 66808 1907167b6038
permissions -rw-r--r--
abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
     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>Parity\<close>
    13 
    14 class unique_euclidean_semiring_parity = unique_euclidean_semiring +
    15   assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
    16   assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
    17   assumes zero_not_eq_two: "0 \<noteq> 2"
    18 begin
    19 
    20 lemma parity_cases [case_names even odd]:
    21   assumes "a mod 2 = 0 \<Longrightarrow> P"
    22   assumes "a mod 2 = 1 \<Longrightarrow> P"
    23   shows P
    24   using assms parity by blast
    25 
    26 lemma one_div_two_eq_zero [simp]:
    27   "1 div 2 = 0"
    28 proof (cases "2 = 0")
    29   case True then show ?thesis by simp
    30 next
    31   case False
    32   from div_mult_mod_eq have "1 div 2 * 2 + 1 mod 2 = 1" .
    33   with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
    34   then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)
    35   then have "1 div 2 = 0 \<or> 2 = 0" by simp
    36   with False show ?thesis by auto
    37 qed
    38 
    39 lemma not_mod_2_eq_0_eq_1 [simp]:
    40   "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
    41   by (cases a rule: parity_cases) simp_all
    42 
    43 lemma not_mod_2_eq_1_eq_0 [simp]:
    44   "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
    45   by (cases a rule: parity_cases) simp_all
    46 
    47 subclass semiring_parity
    48 proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
    49   show "1 mod 2 = 1"
    50     by (fact one_mod_two_eq_one)
    51 next
    52   fix a b
    53   assume "a mod 2 = 1"
    54   moreover assume "b mod 2 = 1"
    55   ultimately show "(a + b) mod 2 = 0"
    56     using mod_add_eq [of a 2 b] by simp
    57 next
    58   fix a b
    59   assume "(a * b) mod 2 = 0"
    60   then have "(a mod 2) * (b mod 2) mod 2 = 0"
    61     by (simp add: mod_mult_eq)
    62   then have "(a mod 2) * (b mod 2) = 0"
    63     by (cases "a mod 2 = 0") simp_all
    64   then show "a mod 2 = 0 \<or> b mod 2 = 0"
    65     by (rule divisors_zero)
    66 next
    67   fix a
    68   assume "a mod 2 = 1"
    69   then have "a = a div 2 * 2 + 1"
    70     using div_mult_mod_eq [of a 2] by simp
    71   then show "\<exists>b. a = b + 1" ..
    72 qed
    73 
    74 lemma even_iff_mod_2_eq_zero:
    75   "even a \<longleftrightarrow> a mod 2 = 0"
    76   by (fact dvd_eq_mod_eq_0)
    77 
    78 lemma odd_iff_mod_2_eq_one:
    79   "odd a \<longleftrightarrow> a mod 2 = 1"
    80   by (simp add: even_iff_mod_2_eq_zero)
    81 
    82 lemma even_succ_div_two [simp]:
    83   "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
    84   by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
    85 
    86 lemma odd_succ_div_two [simp]:
    87   "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
    88   by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc)
    89 
    90 lemma even_two_times_div_two:
    91   "even a \<Longrightarrow> 2 * (a div 2) = a"
    92   by (fact dvd_mult_div_cancel)
    93 
    94 lemma odd_two_times_div_two_succ [simp]:
    95   "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
    96   using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
    97  
    98 end
    99 
   100 
   101 subsection \<open>Numeral division with a pragmatic type class\<close>
   102 
   103 text \<open>
   104   The following type class contains everything necessary to formulate
   105   a division algorithm in ring structures with numerals, restricted
   106   to its positive segments.  This is its primary motivation, and it
   107   could surely be formulated using a more fine-grained, more algebraic
   108   and less technical class hierarchy.
   109 \<close>
   110 
   111 class unique_euclidean_semiring_numeral = unique_euclidean_semiring + linordered_semidom +
   112   assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
   113     and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
   114     and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
   115     and mod_less_eq_dividend: "0 \<le> a \<Longrightarrow> a mod b \<le> a"
   116     and pos_mod_bound: "0 < b \<Longrightarrow> a mod b < b"
   117     and pos_mod_sign: "0 < b \<Longrightarrow> 0 \<le> a mod b"
   118     and mod_mult2_eq: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
   119     and div_mult2_eq: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c"
   120   assumes discrete: "a < b \<longleftrightarrow> a + 1 \<le> b"
   121   fixes divmod :: "num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a"
   122     and divmod_step :: "num \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a"
   123   assumes divmod_def: "divmod m n = (numeral m div numeral n, numeral m mod numeral n)"
   124     and divmod_step_def: "divmod_step l qr = (let (q, r) = qr
   125     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
   126     else (2 * q, r))"
   127     \<comment> \<open>These are conceptually definitions but force generated code
   128     to be monomorphic wrt. particular instances of this class which
   129     yields a significant speedup.\<close>
   130 begin
   131 
   132 subclass unique_euclidean_semiring_parity
   133 proof
   134   fix a
   135   show "a mod 2 = 0 \<or> a mod 2 = 1"
   136   proof (rule ccontr)
   137     assume "\<not> (a mod 2 = 0 \<or> a mod 2 = 1)"
   138     then have "a mod 2 \<noteq> 0" and "a mod 2 \<noteq> 1" by simp_all
   139     have "0 < 2" by simp
   140     with pos_mod_bound pos_mod_sign have "0 \<le> a mod 2" "a mod 2 < 2" by simp_all
   141     with \<open>a mod 2 \<noteq> 0\<close> have "0 < a mod 2" by simp
   142     with discrete have "1 \<le> a mod 2" by simp
   143     with \<open>a mod 2 \<noteq> 1\<close> have "1 < a mod 2" by simp
   144     with discrete have "2 \<le> a mod 2" by simp
   145     with \<open>a mod 2 < 2\<close> show False by simp
   146   qed
   147 next
   148   show "1 mod 2 = 1"
   149     by (rule mod_less) simp_all
   150 next
   151   show "0 \<noteq> 2"
   152     by simp
   153 qed
   154 
   155 lemma divmod_digit_1:
   156   assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)"
   157   shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")
   158     and "a mod (2 * b) - b = a mod b" (is "?Q")
   159 proof -
   160   from assms mod_less_eq_dividend [of a "2 * b"] have "b \<le> a"
   161     by (auto intro: trans)
   162   with \<open>0 < b\<close> have "0 < a div b" by (auto intro: div_positive)
   163   then have [simp]: "1 \<le> a div b" by (simp add: discrete)
   164   with \<open>0 < b\<close> have mod_less: "a mod b < b" by (simp add: pos_mod_bound)
   165   define w where "w = a div b mod 2"
   166   with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
   167   have mod_w: "a mod (2 * b) = a mod b + b * w"
   168     by (simp add: w_def mod_mult2_eq ac_simps)
   169   from assms w_exhaust have "w = 1"
   170     by (auto simp add: mod_w) (insert mod_less, auto)
   171   with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp
   172   have "2 * (a div (2 * b)) = a div b - w"
   173     by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
   174   with \<open>w = 1\<close> have div: "2 * (a div (2 * b)) = a div b - 1" by simp
   175   then show ?P and ?Q
   176     by (simp_all add: div mod add_implies_diff [symmetric])
   177 qed
   178 
   179 lemma divmod_digit_0:
   180   assumes "0 < b" and "a mod (2 * b) < b"
   181   shows "2 * (a div (2 * b)) = a div b" (is "?P")
   182     and "a mod (2 * b) = a mod b" (is "?Q")
   183 proof -
   184   define w where "w = a div b mod 2"
   185   with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
   186   have mod_w: "a mod (2 * b) = a mod b + b * w"
   187     by (simp add: w_def mod_mult2_eq ac_simps)
   188   moreover have "b \<le> a mod b + b"
   189   proof -
   190     from \<open>0 < b\<close> pos_mod_sign have "0 \<le> a mod b" by blast
   191     then have "0 + b \<le> a mod b + b" by (rule add_right_mono)
   192     then show ?thesis by simp
   193   qed
   194   moreover note assms w_exhaust
   195   ultimately have "w = 0" by auto
   196   with mod_w have mod: "a mod (2 * b) = a mod b" by simp
   197   have "2 * (a div (2 * b)) = a div b - w"
   198     by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
   199   with \<open>w = 0\<close> have div: "2 * (a div (2 * b)) = a div b" by simp
   200   then show ?P and ?Q
   201     by (simp_all add: div mod)
   202 qed
   203 
   204 lemma fst_divmod:
   205   "fst (divmod m n) = numeral m div numeral n"
   206   by (simp add: divmod_def)
   207 
   208 lemma snd_divmod:
   209   "snd (divmod m n) = numeral m mod numeral n"
   210   by (simp add: divmod_def)
   211 
   212 text \<open>
   213   This is a formulation of one step (referring to one digit position)
   214   in school-method division: compare the dividend at the current
   215   digit position with the remainder from previous division steps
   216   and evaluate accordingly.
   217 \<close>
   218 
   219 lemma divmod_step_eq [simp]:
   220   "divmod_step l (q, r) = (if numeral l \<le> r
   221     then (2 * q + 1, r - numeral l) else (2 * q, r))"
   222   by (simp add: divmod_step_def)
   223 
   224 text \<open>
   225   This is a formulation of school-method division.
   226   If the divisor is smaller than the dividend, terminate.
   227   If not, shift the dividend to the right until termination
   228   occurs and then reiterate single division steps in the
   229   opposite direction.
   230 \<close>
   231 
   232 lemma divmod_divmod_step:
   233   "divmod m n = (if m < n then (0, numeral m)
   234     else divmod_step n (divmod m (Num.Bit0 n)))"
   235 proof (cases "m < n")
   236   case True then have "numeral m < numeral n" by simp
   237   then show ?thesis
   238     by (simp add: prod_eq_iff div_less mod_less fst_divmod snd_divmod)
   239 next
   240   case False
   241   have "divmod m n =
   242     divmod_step n (numeral m div (2 * numeral n),
   243       numeral m mod (2 * numeral n))"
   244   proof (cases "numeral n \<le> numeral m mod (2 * numeral n)")
   245     case True
   246     with divmod_step_eq
   247       have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
   248         (2 * (numeral m div (2 * numeral n)) + 1, numeral m mod (2 * numeral n) - numeral n)"
   249         by simp
   250     moreover from True divmod_digit_1 [of "numeral m" "numeral n"]
   251       have "2 * (numeral m div (2 * numeral n)) + 1 = numeral m div numeral n"
   252       and "numeral m mod (2 * numeral n) - numeral n = numeral m mod numeral n"
   253       by simp_all
   254     ultimately show ?thesis by (simp only: divmod_def)
   255   next
   256     case False then have *: "numeral m mod (2 * numeral n) < numeral n"
   257       by (simp add: not_le)
   258     with divmod_step_eq
   259       have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
   260         (2 * (numeral m div (2 * numeral n)), numeral m mod (2 * numeral n))"
   261         by auto
   262     moreover from * divmod_digit_0 [of "numeral n" "numeral m"]
   263       have "2 * (numeral m div (2 * numeral n)) = numeral m div numeral n"
   264       and "numeral m mod (2 * numeral n) = numeral m mod numeral n"
   265       by (simp_all only: zero_less_numeral)
   266     ultimately show ?thesis by (simp only: divmod_def)
   267   qed
   268   then have "divmod m n =
   269     divmod_step n (numeral m div numeral (Num.Bit0 n),
   270       numeral m mod numeral (Num.Bit0 n))"
   271     by (simp only: numeral.simps distrib mult_1)
   272   then have "divmod m n = divmod_step n (divmod m (Num.Bit0 n))"
   273     by (simp add: divmod_def)
   274   with False show ?thesis by simp
   275 qed
   276 
   277 text \<open>The division rewrite proper -- first, trivial results involving \<open>1\<close>\<close>
   278 
   279 lemma divmod_trivial [simp]:
   280   "divmod Num.One Num.One = (numeral Num.One, 0)"
   281   "divmod (Num.Bit0 m) Num.One = (numeral (Num.Bit0 m), 0)"
   282   "divmod (Num.Bit1 m) Num.One = (numeral (Num.Bit1 m), 0)"
   283   "divmod num.One (num.Bit0 n) = (0, Numeral1)"
   284   "divmod num.One (num.Bit1 n) = (0, Numeral1)"
   285   using divmod_divmod_step [of "Num.One"] by (simp_all add: divmod_def)
   286 
   287 text \<open>Division by an even number is a right-shift\<close>
   288 
   289 lemma divmod_cancel [simp]:
   290   "divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))" (is ?P)
   291   "divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))" (is ?Q)
   292 proof -
   293   have *: "\<And>q. numeral (Num.Bit0 q) = 2 * numeral q"
   294     "\<And>q. numeral (Num.Bit1 q) = 2 * numeral q + 1"
   295     by (simp_all only: numeral_mult numeral.simps distrib) simp_all
   296   have "1 div 2 = 0" "1 mod 2 = 1" by (auto intro: div_less mod_less)
   297   then show ?P and ?Q
   298     by (simp_all add: fst_divmod snd_divmod prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1
   299       div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2]
   300       add.commute del: numeral_times_numeral)
   301 qed
   302 
   303 text \<open>The really hard work\<close>
   304 
   305 lemma divmod_steps [simp]:
   306   "divmod (num.Bit0 m) (num.Bit1 n) =
   307       (if m \<le> n then (0, numeral (num.Bit0 m))
   308        else divmod_step (num.Bit1 n)
   309              (divmod (num.Bit0 m)
   310                (num.Bit0 (num.Bit1 n))))"
   311   "divmod (num.Bit1 m) (num.Bit1 n) =
   312       (if m < n then (0, numeral (num.Bit1 m))
   313        else divmod_step (num.Bit1 n)
   314              (divmod (num.Bit1 m)
   315                (num.Bit0 (num.Bit1 n))))"
   316   by (simp_all add: divmod_divmod_step)
   317 
   318 lemmas divmod_algorithm_code = divmod_step_eq divmod_trivial divmod_cancel divmod_steps  
   319 
   320 text \<open>Special case: divisibility\<close>
   321 
   322 definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool"
   323 where
   324   "divides_aux qr \<longleftrightarrow> snd qr = 0"
   325 
   326 lemma divides_aux_eq [simp]:
   327   "divides_aux (q, r) \<longleftrightarrow> r = 0"
   328   by (simp add: divides_aux_def)
   329 
   330 lemma dvd_numeral_simp [simp]:
   331   "numeral m dvd numeral n \<longleftrightarrow> divides_aux (divmod n m)"
   332   by (simp add: divmod_def mod_eq_0_iff_dvd)
   333 
   334 text \<open>Generic computation of quotient and remainder\<close>  
   335 
   336 lemma numeral_div_numeral [simp]: 
   337   "numeral k div numeral l = fst (divmod k l)"
   338   by (simp add: fst_divmod)
   339 
   340 lemma numeral_mod_numeral [simp]: 
   341   "numeral k mod numeral l = snd (divmod k l)"
   342   by (simp add: snd_divmod)
   343 
   344 lemma one_div_numeral [simp]:
   345   "1 div numeral n = fst (divmod num.One n)"
   346   by (simp add: fst_divmod)
   347 
   348 lemma one_mod_numeral [simp]:
   349   "1 mod numeral n = snd (divmod num.One n)"
   350   by (simp add: snd_divmod)
   351 
   352 text \<open>Computing congruences modulo \<open>2 ^ q\<close>\<close>
   353 
   354 lemma cong_exp_iff_simps:
   355   "numeral n mod numeral Num.One = 0
   356     \<longleftrightarrow> True"
   357   "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = 0
   358     \<longleftrightarrow> numeral n mod numeral q = 0"
   359   "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = 0
   360     \<longleftrightarrow> False"
   361   "numeral m mod numeral Num.One = (numeral n mod numeral Num.One)
   362     \<longleftrightarrow> True"
   363   "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
   364     \<longleftrightarrow> True"
   365   "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
   366     \<longleftrightarrow> False"
   367   "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
   368     \<longleftrightarrow> (numeral n mod numeral q) = 0"
   369   "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
   370     \<longleftrightarrow> False"
   371   "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
   372     \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
   373   "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
   374     \<longleftrightarrow> False"
   375   "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
   376     \<longleftrightarrow> (numeral m mod numeral q) = 0"
   377   "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
   378     \<longleftrightarrow> False"
   379   "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
   380     \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
   381   by (auto simp add: case_prod_beta dest: arg_cong [of _ _ even])
   382 
   383 end
   384 
   385 
   386 subsection \<open>Division on @{typ nat}\<close>
   387 
   388 context
   389 begin
   390 
   391 text \<open>
   392   We define @{const divide} and @{const modulo} on @{typ nat} by means
   393   of a characteristic relation with two input arguments
   394   @{term "m::nat"}, @{term "n::nat"} and two output arguments
   395   @{term "q::nat"}(uotient) and @{term "r::nat"}(emainder).
   396 \<close>
   397 
   398 inductive eucl_rel_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool"
   399   where eucl_rel_nat_by0: "eucl_rel_nat m 0 (0, m)"
   400   | eucl_rel_natI: "r < n \<Longrightarrow> m = q * n + r \<Longrightarrow> eucl_rel_nat m n (q, r)"
   401 
   402 text \<open>@{const eucl_rel_nat} is total:\<close>
   403 
   404 qualified lemma eucl_rel_nat_ex:
   405   obtains q r where "eucl_rel_nat m n (q, r)"
   406 proof (cases "n = 0")
   407   case True
   408   with that eucl_rel_nat_by0 show thesis
   409     by blast
   410 next
   411   case False
   412   have "\<exists>q r. m = q * n + r \<and> r < n"
   413   proof (induct m)
   414     case 0 with \<open>n \<noteq> 0\<close>
   415     have "(0::nat) = 0 * n + 0 \<and> 0 < n" by simp
   416     then show ?case by blast
   417   next
   418     case (Suc m) then obtain q' r'
   419       where m: "m = q' * n + r'" and n: "r' < n" by auto
   420     then show ?case proof (cases "Suc r' < n")
   421       case True
   422       from m n have "Suc m = q' * n + Suc r'" by simp
   423       with True show ?thesis by blast
   424     next
   425       case False then have "n \<le> Suc r'"
   426         by (simp add: not_less)
   427       moreover from n have "Suc r' \<le> n"
   428         by (simp add: Suc_le_eq)
   429       ultimately have "n = Suc r'" by auto
   430       with m have "Suc m = Suc q' * n + 0" by simp
   431       with \<open>n \<noteq> 0\<close> show ?thesis by blast
   432     qed
   433   qed
   434   with that \<open>n \<noteq> 0\<close> eucl_rel_natI show thesis
   435     by blast
   436 qed
   437 
   438 text \<open>@{const eucl_rel_nat} is injective:\<close>
   439 
   440 qualified lemma eucl_rel_nat_unique_div:
   441   assumes "eucl_rel_nat m n (q, r)"
   442     and "eucl_rel_nat m n (q', r')"
   443   shows "q = q'"
   444 proof (cases "n = 0")
   445   case True with assms show ?thesis
   446     by (auto elim: eucl_rel_nat.cases)
   447 next
   448   case False
   449   have *: "q' \<le> q" if "q' * n + r' = q * n + r" "r < n" for q r q' r' :: nat
   450   proof (rule ccontr)
   451     assume "\<not> q' \<le> q"
   452     then have "q < q'"
   453       by (simp add: not_le)
   454     with that show False
   455       by (auto simp add: less_iff_Suc_add algebra_simps)
   456   qed
   457   from \<open>n \<noteq> 0\<close> assms show ?thesis
   458     by (auto intro: order_antisym elim: eucl_rel_nat.cases dest: * sym split: if_splits)
   459 qed
   460 
   461 qualified lemma eucl_rel_nat_unique_mod:
   462   assumes "eucl_rel_nat m n (q, r)"
   463     and "eucl_rel_nat m n (q', r')"
   464   shows "r = r'"
   465 proof -
   466   from assms have "q' = q"
   467     by (auto intro: eucl_rel_nat_unique_div)
   468   with assms show ?thesis
   469     by (auto elim!: eucl_rel_nat.cases)
   470 qed
   471 
   472 text \<open>
   473   We instantiate divisibility on the natural numbers by
   474   means of @{const eucl_rel_nat}:
   475 \<close>
   476 
   477 qualified definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
   478   "divmod_nat m n = (THE qr. eucl_rel_nat m n qr)"
   479 
   480 qualified lemma eucl_rel_nat_divmod_nat:
   481   "eucl_rel_nat m n (divmod_nat m n)"
   482 proof -
   483   from eucl_rel_nat_ex
   484     obtain q r where rel: "eucl_rel_nat m n (q, r)" .
   485   then show ?thesis
   486     by (auto simp add: divmod_nat_def intro: theI
   487       elim: eucl_rel_nat_unique_div eucl_rel_nat_unique_mod)
   488 qed
   489 
   490 qualified lemma divmod_nat_unique:
   491   "divmod_nat m n = (q, r)" if "eucl_rel_nat m n (q, r)"
   492   using that
   493   by (auto simp add: divmod_nat_def intro: eucl_rel_nat_divmod_nat elim: eucl_rel_nat_unique_div eucl_rel_nat_unique_mod)
   494 
   495 qualified lemma divmod_nat_zero:
   496   "divmod_nat m 0 = (0, m)"
   497   by (rule divmod_nat_unique) (fact eucl_rel_nat_by0)
   498 
   499 qualified lemma divmod_nat_zero_left:
   500   "divmod_nat 0 n = (0, 0)"
   501   by (rule divmod_nat_unique) 
   502     (cases n, auto intro: eucl_rel_nat_by0 eucl_rel_natI)
   503 
   504 qualified lemma divmod_nat_base:
   505   "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
   506   by (rule divmod_nat_unique) 
   507     (cases n, auto intro: eucl_rel_nat_by0 eucl_rel_natI)
   508 
   509 qualified lemma divmod_nat_step:
   510   assumes "0 < n" and "n \<le> m"
   511   shows "divmod_nat m n =
   512     (Suc (fst (divmod_nat (m - n) n)), snd (divmod_nat (m - n) n))"
   513 proof (rule divmod_nat_unique)
   514   have "eucl_rel_nat (m - n) n (divmod_nat (m - n) n)"
   515     by (fact eucl_rel_nat_divmod_nat)
   516   then show "eucl_rel_nat m n (Suc
   517     (fst (divmod_nat (m - n) n)), snd (divmod_nat (m - n) n))"
   518     using assms
   519       by (auto split: if_splits intro: eucl_rel_natI elim!: eucl_rel_nat.cases simp add: algebra_simps)
   520 qed
   521 
   522 end
   523 
   524 instantiation nat :: "{semidom_modulo, normalization_semidom}"
   525 begin
   526 
   527 definition normalize_nat :: "nat \<Rightarrow> nat"
   528   where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
   529 
   530 definition unit_factor_nat :: "nat \<Rightarrow> nat"
   531   where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
   532 
   533 lemma unit_factor_simps [simp]:
   534   "unit_factor 0 = (0::nat)"
   535   "unit_factor (Suc n) = 1"
   536   by (simp_all add: unit_factor_nat_def)
   537 
   538 definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   539   where div_nat_def: "m div n = fst (Divides.divmod_nat m n)"
   540 
   541 definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   542   where mod_nat_def: "m mod n = snd (Divides.divmod_nat m n)"
   543 
   544 lemma fst_divmod_nat [simp]:
   545   "fst (Divides.divmod_nat m n) = m div n"
   546   by (simp add: div_nat_def)
   547 
   548 lemma snd_divmod_nat [simp]:
   549   "snd (Divides.divmod_nat m n) = m mod n"
   550   by (simp add: mod_nat_def)
   551 
   552 lemma divmod_nat_div_mod:
   553   "Divides.divmod_nat m n = (m div n, m mod n)"
   554   by (simp add: prod_eq_iff)
   555 
   556 lemma div_nat_unique:
   557   assumes "eucl_rel_nat m n (q, r)"
   558   shows "m div n = q"
   559   using assms
   560   by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
   561 
   562 lemma mod_nat_unique:
   563   assumes "eucl_rel_nat m n (q, r)"
   564   shows "m mod n = r"
   565   using assms
   566   by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
   567 
   568 lemma eucl_rel_nat: "eucl_rel_nat m n (m div n, m mod n)"
   569   using Divides.eucl_rel_nat_divmod_nat
   570   by (simp add: divmod_nat_div_mod)
   571 
   572 text \<open>The ''recursion'' equations for @{const divide} and @{const modulo}\<close>
   573 
   574 lemma div_less [simp]:
   575   fixes m n :: nat
   576   assumes "m < n"
   577   shows "m div n = 0"
   578   using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
   579 
   580 lemma le_div_geq:
   581   fixes m n :: nat
   582   assumes "0 < n" and "n \<le> m"
   583   shows "m div n = Suc ((m - n) div n)"
   584   using assms Divides.divmod_nat_step by (simp add: prod_eq_iff)
   585 
   586 lemma mod_less [simp]:
   587   fixes m n :: nat
   588   assumes "m < n"
   589   shows "m mod n = m"
   590   using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
   591 
   592 lemma le_mod_geq:
   593   fixes m n :: nat
   594   assumes "n \<le> m"
   595   shows "m mod n = (m - n) mod n"
   596   using assms Divides.divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
   597 
   598 lemma mod_less_divisor [simp]:
   599   fixes m n :: nat
   600   assumes "n > 0"
   601   shows "m mod n < n"
   602   using assms eucl_rel_nat [of m n]
   603     by (auto elim: eucl_rel_nat.cases)
   604 
   605 lemma mod_le_divisor [simp]:
   606   fixes m n :: nat
   607   assumes "n > 0"
   608   shows "m mod n \<le> n"
   609   using assms eucl_rel_nat [of m n]
   610     by (auto elim: eucl_rel_nat.cases)
   611 
   612 instance proof
   613   fix m n :: nat
   614   show "m div n * n + m mod n = m"
   615     using eucl_rel_nat [of m n]
   616     by (auto elim: eucl_rel_nat.cases)
   617 next
   618   fix n :: nat show "n div 0 = 0"
   619     by (simp add: div_nat_def Divides.divmod_nat_zero)
   620 next
   621   fix m n :: nat
   622   assume "n \<noteq> 0"
   623   then show "m * n div n = m"
   624     by (auto intro!: eucl_rel_natI div_nat_unique [of _ _ _ 0])
   625 qed (simp_all add: unit_factor_nat_def)
   626 
   627 end
   628 
   629 text \<open>Simproc for cancelling @{const divide} and @{const modulo}\<close>
   630 
   631 lemma (in semiring_modulo) cancel_div_mod_rules:
   632   "((a div b) * b + a mod b) + c = a + c"
   633   "(b * (a div b) + a mod b) + c = a + c"
   634   by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
   635 
   636 ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
   637 
   638 ML \<open>
   639 structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
   640 (
   641   val div_name = @{const_name divide};
   642   val mod_name = @{const_name modulo};
   643   val mk_binop = HOLogic.mk_binop;
   644   val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
   645   val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
   646   fun mk_sum [] = HOLogic.zero
   647     | mk_sum [t] = t
   648     | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   649   fun dest_sum tm =
   650     if HOLogic.is_zero tm then []
   651     else
   652       (case try HOLogic.dest_Suc tm of
   653         SOME t => HOLogic.Suc_zero :: dest_sum t
   654       | NONE =>
   655           (case try dest_plus tm of
   656             SOME (t, u) => dest_sum t @ dest_sum u
   657           | NONE => [tm]));
   658 
   659   val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
   660 
   661   val prove_eq_sums = Arith_Data.prove_conv2 all_tac
   662     (Arith_Data.simp_all_tac @{thms add_0_left add_0_right ac_simps})
   663 )
   664 \<close>
   665 
   666 simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
   667   \<open>K Cancel_Div_Mod_Nat.proc\<close>
   668 
   669 lemma div_by_Suc_0 [simp]:
   670   "m div Suc 0 = m"
   671   using div_by_1 [of m] by simp
   672 
   673 lemma mod_by_Suc_0 [simp]:
   674   "m mod Suc 0 = 0"
   675   using mod_by_1 [of m] by simp
   676 
   677 lemma mod_greater_zero_iff_not_dvd:
   678   fixes m n :: nat
   679   shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
   680   by (simp add: dvd_eq_mod_eq_0)
   681 
   682 instantiation nat :: unique_euclidean_semiring
   683 begin
   684 
   685 definition [simp]:
   686   "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
   687 
   688 definition [simp]:
   689   "uniqueness_constraint_nat = (top :: nat \<Rightarrow> nat \<Rightarrow> bool)"
   690 
   691 instance proof
   692   fix n q r :: nat
   693   assume "euclidean_size r < euclidean_size n"
   694   then have "n > r"
   695     by simp_all
   696   then have "eucl_rel_nat (q * n + r) n (q, r)"
   697     by (rule eucl_rel_natI) rule
   698   then show "(q * n + r) div n = q"
   699     by (rule div_nat_unique)
   700 qed (use mult_le_mono2 [of 1] in \<open>simp_all\<close>)
   701 
   702 end
   703   
   704 lemma divmod_nat_if [code]:
   705   "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
   706     let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
   707   by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
   708 
   709 lemma mod_Suc_eq [mod_simps]:
   710   "Suc (m mod n) mod n = Suc m mod n"
   711 proof -
   712   have "(m mod n + 1) mod n = (m + 1) mod n"
   713     by (simp only: mod_simps)
   714   then show ?thesis
   715     by simp
   716 qed
   717 
   718 lemma mod_Suc_Suc_eq [mod_simps]:
   719   "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n"
   720 proof -
   721   have "(m mod n + 2) mod n = (m + 2) mod n"
   722     by (simp only: mod_simps)
   723   then show ?thesis
   724     by simp
   725 qed
   726 
   727 
   728 subsubsection \<open>Quotient\<close>
   729 
   730 lemma div_geq: "0 < n \<Longrightarrow>  \<not> m < n \<Longrightarrow> m div n = Suc ((m - n) div n)"
   731 by (simp add: le_div_geq linorder_not_less)
   732 
   733 lemma div_if: "0 < n \<Longrightarrow> m div n = (if m < n then 0 else Suc ((m - n) div n))"
   734 by (simp add: div_geq)
   735 
   736 lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
   737 by simp
   738 
   739 lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
   740 by simp
   741 
   742 lemma div_positive:
   743   fixes m n :: nat
   744   assumes "n > 0"
   745   assumes "m \<ge> n"
   746   shows "m div n > 0"
   747 proof -
   748   from \<open>m \<ge> n\<close> obtain q where "m = n + q"
   749     by (auto simp add: le_iff_add)
   750   with \<open>n > 0\<close> show ?thesis by (simp add: div_add_self1)
   751 qed
   752 
   753 lemma div_eq_0_iff: "(a div b::nat) = 0 \<longleftrightarrow> a < b \<or> b = 0"
   754   by auto (metis div_positive less_numeral_extra(3) not_less)
   755 
   756 
   757 subsubsection \<open>Remainder\<close>
   758 
   759 lemma mod_Suc_le_divisor [simp]:
   760   "m mod Suc n \<le> n"
   761   using mod_less_divisor [of "Suc n" m] by arith
   762 
   763 lemma mod_less_eq_dividend [simp]:
   764   fixes m n :: nat
   765   shows "m mod n \<le> m"
   766 proof (rule add_leD2)
   767   from div_mult_mod_eq have "m div n * n + m mod n = m" .
   768   then show "m div n * n + m mod n \<le> m" by auto
   769 qed
   770 
   771 lemma mod_geq: "\<not> m < (n::nat) \<Longrightarrow> m mod n = (m - n) mod n"
   772 by (simp add: le_mod_geq linorder_not_less)
   773 
   774 lemma mod_if: "m mod (n::nat) = (if m < n then m else (m - n) mod n)"
   775 by (simp add: le_mod_geq)
   776 
   777 
   778 subsubsection \<open>Quotient and Remainder\<close>
   779 
   780 lemma div_mult1_eq:
   781   "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"
   782   by (cases "c = 0")
   783      (auto simp add: algebra_simps distrib_left [symmetric]
   784      intro!: div_nat_unique [of _ _ _ "(a * (b mod c)) mod c"] eucl_rel_natI)
   785 
   786 lemma eucl_rel_nat_add1_eq:
   787   "eucl_rel_nat a c (aq, ar) \<Longrightarrow> eucl_rel_nat b c (bq, br)
   788    \<Longrightarrow> eucl_rel_nat (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
   789   by (auto simp add: split_ifs algebra_simps elim!: eucl_rel_nat.cases intro: eucl_rel_nat_by0 eucl_rel_natI)
   790 
   791 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
   792 lemma div_add1_eq:
   793   "(a + b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
   794 by (blast intro: eucl_rel_nat_add1_eq [THEN div_nat_unique] eucl_rel_nat)
   795 
   796 lemma eucl_rel_nat_mult2_eq:
   797   assumes "eucl_rel_nat a b (q, r)"
   798   shows "eucl_rel_nat a (b * c) (q div c, b *(q mod c) + r)"
   799 proof (cases "c = 0")
   800   case True
   801   with assms show ?thesis
   802     by (auto intro: eucl_rel_nat_by0 elim!: eucl_rel_nat.cases simp add: ac_simps)
   803 next
   804   case False
   805   { assume "r < b"
   806     with False have "b * (q mod c) + r < b * c"
   807       apply (cut_tac m = q and n = c in mod_less_divisor)
   808       apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
   809       apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
   810       apply (simp add: add_mult_distrib2)
   811       done
   812     then have "r + b * (q mod c) < b * c"
   813       by (simp add: ac_simps)
   814   } with assms False show ?thesis
   815     by (auto simp add: algebra_simps add_mult_distrib2 [symmetric] elim!: eucl_rel_nat.cases intro: eucl_rel_nat.intros)
   816 qed
   817 
   818 lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
   819 by (force simp add: eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN div_nat_unique])
   820 
   821 lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
   822 by (auto simp add: mult.commute eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN mod_nat_unique])
   823 
   824 instantiation nat :: unique_euclidean_semiring_numeral
   825 begin
   826 
   827 definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat"
   828 where
   829   divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)"
   830 
   831 definition divmod_step_nat :: "num \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
   832 where
   833   "divmod_step_nat l qr = (let (q, r) = qr
   834     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
   835     else (2 * q, r))"
   836 
   837 instance
   838   by standard (auto intro: div_positive simp add: divmod'_nat_def divmod_step_nat_def mod_mult2_eq div_mult2_eq)
   839 
   840 end
   841 
   842 declare divmod_algorithm_code [where ?'a = nat, code]
   843   
   844 
   845 subsubsection \<open>Further Facts about Quotient and Remainder\<close>
   846 
   847 lemma div_le_mono:
   848   fixes m n k :: nat
   849   assumes "m \<le> n"
   850   shows "m div k \<le> n div k"
   851 proof -
   852   from assms obtain q where "n = m + q"
   853     by (auto simp add: le_iff_add)
   854   then show ?thesis
   855     by (simp add: div_add1_eq [of m q k])
   856 qed
   857 
   858 (* Antimonotonicity of div in second argument *)
   859 lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
   860 apply (subgoal_tac "0<n")
   861  prefer 2 apply simp
   862 apply (induct_tac k rule: nat_less_induct)
   863 apply (rename_tac "k")
   864 apply (case_tac "k<n", simp)
   865 apply (subgoal_tac "~ (k<m) ")
   866  prefer 2 apply simp
   867 apply (simp add: div_geq)
   868 apply (subgoal_tac "(k-n) div n \<le> (k-m) div n")
   869  prefer 2
   870  apply (blast intro: div_le_mono diff_le_mono2)
   871 apply (rule le_trans, simp)
   872 apply (simp)
   873 done
   874 
   875 lemma div_le_dividend [simp]: "m div n \<le> (m::nat)"
   876 apply (case_tac "n=0", simp)
   877 apply (subgoal_tac "m div n \<le> m div 1", simp)
   878 apply (rule div_le_mono2)
   879 apply (simp_all (no_asm_simp))
   880 done
   881 
   882 (* Similar for "less than" *)
   883 lemma div_less_dividend [simp]:
   884   "\<lbrakk>(1::nat) < n; 0 < m\<rbrakk> \<Longrightarrow> m div n < m"
   885 apply (induct m rule: nat_less_induct)
   886 apply (rename_tac "m")
   887 apply (case_tac "m<n", simp)
   888 apply (subgoal_tac "0<n")
   889  prefer 2 apply simp
   890 apply (simp add: div_geq)
   891 apply (case_tac "n<m")
   892  apply (subgoal_tac "(m-n) div n < (m-n) ")
   893   apply (rule impI less_trans_Suc)+
   894 apply assumption
   895   apply (simp_all)
   896 done
   897 
   898 text\<open>A fact for the mutilated chess board\<close>
   899 lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
   900 apply (case_tac "n=0", simp)
   901 apply (induct "m" rule: nat_less_induct)
   902 apply (case_tac "Suc (na) <n")
   903 (* case Suc(na) < n *)
   904 apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
   905 (* case n \<le> Suc(na) *)
   906 apply (simp add: linorder_not_less le_Suc_eq mod_geq)
   907 apply (auto simp add: Suc_diff_le le_mod_geq)
   908 done
   909 
   910 lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
   911 by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
   912 
   913 lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]
   914 
   915 (*Loses information, namely we also have r<d provided d is nonzero*)
   916 lemma mod_eqD:
   917   fixes m d r q :: nat
   918   assumes "m mod d = r"
   919   shows "\<exists>q. m = r + q * d"
   920 proof -
   921   from div_mult_mod_eq obtain q where "q * d + m mod d = m" by blast
   922   with assms have "m = r + q * d" by simp
   923   then show ?thesis ..
   924 qed
   925 
   926 lemma split_div:
   927  "P(n div k :: nat) =
   928  ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"
   929  (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
   930 proof
   931   assume P: ?P
   932   show ?Q
   933   proof (cases)
   934     assume "k = 0"
   935     with P show ?Q by simp
   936   next
   937     assume not0: "k \<noteq> 0"
   938     thus ?Q
   939     proof (simp, intro allI impI)
   940       fix i j
   941       assume n: "n = k*i + j" and j: "j < k"
   942       show "P i"
   943       proof (cases)
   944         assume "i = 0"
   945         with n j P show "P i" by simp
   946       next
   947         assume "i \<noteq> 0"
   948         with not0 n j P show "P i" by(simp add:ac_simps)
   949       qed
   950     qed
   951   qed
   952 next
   953   assume Q: ?Q
   954   show ?P
   955   proof (cases)
   956     assume "k = 0"
   957     with Q show ?P by simp
   958   next
   959     assume not0: "k \<noteq> 0"
   960     with Q have R: ?R by simp
   961     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
   962     show ?P by simp
   963   qed
   964 qed
   965 
   966 lemma split_div_lemma:
   967   assumes "0 < n"
   968   shows "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> q = ((m::nat) div n)" (is "?lhs \<longleftrightarrow> ?rhs")
   969 proof
   970   assume ?rhs
   971   with minus_mod_eq_mult_div [symmetric] have nq: "n * q = m - (m mod n)" by simp
   972   then have A: "n * q \<le> m" by simp
   973   have "n - (m mod n) > 0" using mod_less_divisor assms by auto
   974   then have "m < m + (n - (m mod n))" by simp
   975   then have "m < n + (m - (m mod n))" by simp
   976   with nq have "m < n + n * q" by simp
   977   then have B: "m < n * Suc q" by simp
   978   from A B show ?lhs ..
   979 next
   980   assume P: ?lhs
   981   then have "eucl_rel_nat m n (q, m - n * q)"
   982     by (auto intro: eucl_rel_natI simp add: ac_simps)
   983   then have "m div n = q"
   984     by (rule div_nat_unique)
   985   then show ?rhs by simp
   986 qed
   987 
   988 theorem split_div':
   989   "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
   990    (\<exists>q. (n * q \<le> m \<and> m < n * (Suc q)) \<and> P q))"
   991   apply (cases "0 < n")
   992   apply (simp only: add: split_div_lemma)
   993   apply simp_all
   994   done
   995 
   996 lemma split_mod:
   997  "P(n mod k :: nat) =
   998  ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"
   999  (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
  1000 proof
  1001   assume P: ?P
  1002   show ?Q
  1003   proof (cases)
  1004     assume "k = 0"
  1005     with P show ?Q by simp
  1006   next
  1007     assume not0: "k \<noteq> 0"
  1008     thus ?Q
  1009     proof (simp, intro allI impI)
  1010       fix i j
  1011       assume "n = k*i + j" "j < k"
  1012       thus "P j" using not0 P by (simp add: ac_simps)
  1013     qed
  1014   qed
  1015 next
  1016   assume Q: ?Q
  1017   show ?P
  1018   proof (cases)
  1019     assume "k = 0"
  1020     with Q show ?P by simp
  1021   next
  1022     assume not0: "k \<noteq> 0"
  1023     with Q have R: ?R by simp
  1024     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
  1025     show ?P by simp
  1026   qed
  1027 qed
  1028 
  1029 lemma div_eq_dividend_iff: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
  1030   apply rule
  1031   apply (cases "b = 0")
  1032   apply simp_all
  1033   apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3)
  1034   done
  1035 
  1036 lemma (in field_char_0) of_nat_div:
  1037   "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)"
  1038 proof -
  1039   have "of_nat (m div n) = ((of_nat (m div n * n + m mod n) - of_nat (m mod n)) / of_nat n :: 'a)"
  1040     unfolding of_nat_add by (cases "n = 0") simp_all
  1041   then show ?thesis
  1042     by simp
  1043 qed
  1044 
  1045 
  1046 subsubsection \<open>An ``induction'' law for modulus arithmetic.\<close>
  1047 
  1048 lemma mod_induct_0:
  1049   assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
  1050   and base: "P i" and i: "i<p"
  1051   shows "P 0"
  1052 proof (rule ccontr)
  1053   assume contra: "\<not>(P 0)"
  1054   from i have p: "0<p" by simp
  1055   have "\<forall>k. 0<k \<longrightarrow> \<not> P (p-k)" (is "\<forall>k. ?A k")
  1056   proof
  1057     fix k
  1058     show "?A k"
  1059     proof (induct k)
  1060       show "?A 0" by simp  \<comment> "by contradiction"
  1061     next
  1062       fix n
  1063       assume ih: "?A n"
  1064       show "?A (Suc n)"
  1065       proof (clarsimp)
  1066         assume y: "P (p - Suc n)"
  1067         have n: "Suc n < p"
  1068         proof (rule ccontr)
  1069           assume "\<not>(Suc n < p)"
  1070           hence "p - Suc n = 0"
  1071             by simp
  1072           with y contra show "False"
  1073             by simp
  1074         qed
  1075         hence n2: "Suc (p - Suc n) = p-n" by arith
  1076         from p have "p - Suc n < p" by arith
  1077         with y step have z: "P ((Suc (p - Suc n)) mod p)"
  1078           by blast
  1079         show "False"
  1080         proof (cases "n=0")
  1081           case True
  1082           with z n2 contra show ?thesis by simp
  1083         next
  1084           case False
  1085           with p have "p-n < p" by arith
  1086           with z n2 False ih show ?thesis by simp
  1087         qed
  1088       qed
  1089     qed
  1090   qed
  1091   moreover
  1092   from i obtain k where "0<k \<and> i+k=p"
  1093     by (blast dest: less_imp_add_positive)
  1094   hence "0<k \<and> i=p-k" by auto
  1095   moreover
  1096   note base
  1097   ultimately
  1098   show "False" by blast
  1099 qed
  1100 
  1101 lemma mod_induct:
  1102   assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
  1103   and base: "P i" and i: "i<p" and j: "j<p"
  1104   shows "P j"
  1105 proof -
  1106   have "\<forall>j<p. P j"
  1107   proof
  1108     fix j
  1109     show "j<p \<longrightarrow> P j" (is "?A j")
  1110     proof (induct j)
  1111       from step base i show "?A 0"
  1112         by (auto elim: mod_induct_0)
  1113     next
  1114       fix k
  1115       assume ih: "?A k"
  1116       show "?A (Suc k)"
  1117       proof
  1118         assume suc: "Suc k < p"
  1119         hence k: "k<p" by simp
  1120         with ih have "P k" ..
  1121         with step k have "P (Suc k mod p)"
  1122           by blast
  1123         moreover
  1124         from suc have "Suc k mod p = Suc k"
  1125           by simp
  1126         ultimately
  1127         show "P (Suc k)" by simp
  1128       qed
  1129     qed
  1130   qed
  1131   with j show ?thesis by blast
  1132 qed
  1133 
  1134 lemma div2_Suc_Suc [simp]: "Suc (Suc m) div 2 = Suc (m div 2)"
  1135   by (simp add: numeral_2_eq_2 le_div_geq)
  1136 
  1137 lemma mod2_Suc_Suc [simp]: "Suc (Suc m) mod 2 = m mod 2"
  1138   by (simp add: numeral_2_eq_2 le_mod_geq)
  1139 
  1140 lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
  1141 by (simp add: mult_2 [symmetric])
  1142 
  1143 lemma mod2_gr_0 [simp]: "0 < (m::nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
  1144 proof -
  1145   { fix n :: nat have  "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (cases n) simp_all }
  1146   moreover have "m mod 2 < 2" by simp
  1147   ultimately have "m mod 2 = 0 \<or> m mod 2 = 1" .
  1148   then show ?thesis by auto
  1149 qed
  1150 
  1151 text\<open>These lemmas collapse some needless occurrences of Suc:
  1152     at least three Sucs, since two and fewer are rewritten back to Suc again!
  1153     We already have some rules to simplify operands smaller than 3.\<close>
  1154 
  1155 lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
  1156 by (simp add: Suc3_eq_add_3)
  1157 
  1158 lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
  1159 by (simp add: Suc3_eq_add_3)
  1160 
  1161 lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
  1162 by (simp add: Suc3_eq_add_3)
  1163 
  1164 lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
  1165 by (simp add: Suc3_eq_add_3)
  1166 
  1167 lemmas Suc_div_eq_add3_div_numeral [simp] = Suc_div_eq_add3_div [of _ "numeral v"] for v
  1168 lemmas Suc_mod_eq_add3_mod_numeral [simp] = Suc_mod_eq_add3_mod [of _ "numeral v"] for v
  1169 
  1170 lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1"
  1171 apply (induct "m")
  1172 apply (simp_all add: mod_Suc)
  1173 done
  1174 
  1175 declare Suc_times_mod_eq [of "numeral w", simp] for w
  1176 
  1177 lemma Suc_div_le_mono [simp]: "n div k \<le> (Suc n) div k"
  1178 by (simp add: div_le_mono)
  1179 
  1180 lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2"
  1181 by (cases n) simp_all
  1182 
  1183 lemma div_2_gt_zero [simp]: assumes A: "(1::nat) < n" shows "0 < n div 2"
  1184 proof -
  1185   from A have B: "0 < n - 1" and C: "n - 1 + 1 = n" by simp_all
  1186   from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp
  1187 qed
  1188 
  1189 lemma mod_mult_self3' [simp]: "Suc (k * n + m) mod n = Suc m mod n"
  1190   using mod_mult_self3 [of k n "Suc m"] by simp
  1191 
  1192 lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
  1193 apply (subst mod_Suc [of m])
  1194 apply (subst mod_Suc [of "m mod n"], simp)
  1195 done
  1196 
  1197 lemma mod_2_not_eq_zero_eq_one_nat:
  1198   fixes n :: nat
  1199   shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
  1200   by (fact not_mod_2_eq_0_eq_1)
  1201 
  1202 lemma even_Suc_div_two [simp]:
  1203   "even n \<Longrightarrow> Suc n div 2 = n div 2"
  1204   using even_succ_div_two [of n] by simp
  1205 
  1206 lemma odd_Suc_div_two [simp]:
  1207   "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
  1208   using odd_succ_div_two [of n] by simp
  1209 
  1210 lemma odd_two_times_div_two_nat [simp]:
  1211   assumes "odd n"
  1212   shows "2 * (n div 2) = n - (1 :: nat)"
  1213 proof -
  1214   from assms have "2 * (n div 2) + 1 = n"
  1215     by (rule odd_two_times_div_two_succ)
  1216   then have "Suc (2 * (n div 2)) - 1 = n - 1"
  1217     by simp
  1218   then show ?thesis
  1219     by simp
  1220 qed
  1221 
  1222 lemma parity_induct [case_names zero even odd]:
  1223   assumes zero: "P 0"
  1224   assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
  1225   assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
  1226   shows "P n"
  1227 proof (induct n rule: less_induct)
  1228   case (less n)
  1229   show "P n"
  1230   proof (cases "n = 0")
  1231     case True with zero show ?thesis by simp
  1232   next
  1233     case False
  1234     with less have hyp: "P (n div 2)" by simp
  1235     show ?thesis
  1236     proof (cases "even n")
  1237       case True
  1238       with hyp even [of "n div 2"] show ?thesis
  1239         by simp
  1240     next
  1241       case False
  1242       with hyp odd [of "n div 2"] show ?thesis
  1243         by simp
  1244     qed
  1245   qed
  1246 qed
  1247 
  1248 lemma Suc_0_div_numeral [simp]:
  1249   fixes k l :: num
  1250   shows "Suc 0 div numeral k = fst (divmod Num.One k)"
  1251   by (simp_all add: fst_divmod)
  1252 
  1253 lemma Suc_0_mod_numeral [simp]:
  1254   fixes k l :: num
  1255   shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
  1256   by (simp_all add: snd_divmod)
  1257 
  1258 
  1259 subsection \<open>Division on @{typ int}\<close>
  1260 
  1261 context
  1262 begin
  1263 
  1264 inductive eucl_rel_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool"
  1265   where eucl_rel_int_by0: "eucl_rel_int k 0 (0, k)"
  1266   | eucl_rel_int_dividesI: "l \<noteq> 0 \<Longrightarrow> k = q * l \<Longrightarrow> eucl_rel_int k l (q, 0)"
  1267   | eucl_rel_int_remainderI: "sgn r = sgn l \<Longrightarrow> \<bar>r\<bar> < \<bar>l\<bar>
  1268       \<Longrightarrow> k = q * l + r \<Longrightarrow> eucl_rel_int k l (q, r)"
  1269 
  1270 lemma eucl_rel_int_iff:    
  1271   "eucl_rel_int k l (q, r) \<longleftrightarrow> 
  1272     k = l * q + r \<and>
  1273      (if 0 < l then 0 \<le> r \<and> r < l else if l < 0 then l < r \<and> r \<le> 0 else q = 0)"
  1274   by (cases "r = 0")
  1275     (auto elim!: eucl_rel_int.cases intro: eucl_rel_int_by0 eucl_rel_int_dividesI eucl_rel_int_remainderI
  1276     simp add: ac_simps sgn_1_pos sgn_1_neg)
  1277 
  1278 lemma unique_quotient_lemma:
  1279   "b * q' + r' \<le> b * q + r \<Longrightarrow> 0 \<le> r' \<Longrightarrow> r' < b \<Longrightarrow> r < b \<Longrightarrow> q' \<le> (q::int)"
  1280 apply (subgoal_tac "r' + b * (q'-q) \<le> r")
  1281  prefer 2 apply (simp add: right_diff_distrib)
  1282 apply (subgoal_tac "0 < b * (1 + q - q') ")
  1283 apply (erule_tac [2] order_le_less_trans)
  1284  prefer 2 apply (simp add: right_diff_distrib distrib_left)
  1285 apply (subgoal_tac "b * q' < b * (1 + q) ")
  1286  prefer 2 apply (simp add: right_diff_distrib distrib_left)
  1287 apply (simp add: mult_less_cancel_left)
  1288 done
  1289 
  1290 lemma unique_quotient_lemma_neg:
  1291   "b * q' + r' \<le> b*q + r \<Longrightarrow> r \<le> 0 \<Longrightarrow> b < r \<Longrightarrow> b < r' \<Longrightarrow> q \<le> (q'::int)"
  1292   by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma) auto
  1293 
  1294 lemma unique_quotient:
  1295   "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> q = q'"
  1296   apply (simp add: eucl_rel_int_iff linorder_neq_iff split: if_split_asm)
  1297   apply (blast intro: order_antisym
  1298     dest: order_eq_refl [THEN unique_quotient_lemma]
  1299     order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
  1300   done
  1301 
  1302 lemma unique_remainder:
  1303   "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> r = r'"
  1304 apply (subgoal_tac "q = q'")
  1305  apply (simp add: eucl_rel_int_iff)
  1306 apply (blast intro: unique_quotient)
  1307 done
  1308 
  1309 end
  1310 
  1311 instantiation int :: "{idom_modulo, normalization_semidom}"
  1312 begin
  1313 
  1314 definition normalize_int :: "int \<Rightarrow> int"
  1315   where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
  1316 
  1317 definition unit_factor_int :: "int \<Rightarrow> int"
  1318   where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
  1319 
  1320 definition divide_int :: "int \<Rightarrow> int \<Rightarrow> int"
  1321   where "k div l = (if l = 0 \<or> k = 0 then 0
  1322     else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
  1323       then int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
  1324       else
  1325         if l dvd k then - int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
  1326         else - int (Suc (nat \<bar>k\<bar> div nat \<bar>l\<bar>)))"
  1327 
  1328 definition modulo_int :: "int \<Rightarrow> int \<Rightarrow> int"
  1329   where "k mod l = (if l = 0 then k else if l dvd k then 0
  1330     else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
  1331       then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
  1332       else sgn l * (\<bar>l\<bar> - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
  1333 
  1334 lemma eucl_rel_int:
  1335   "eucl_rel_int k l (k div l, k mod l)"
  1336 proof (cases k rule: int_cases3)
  1337   case zero
  1338   then show ?thesis
  1339     by (simp add: eucl_rel_int_iff divide_int_def modulo_int_def)
  1340 next
  1341   case (pos n)
  1342   then show ?thesis
  1343     using div_mult_mod_eq [of n]
  1344     by (cases l rule: int_cases3)
  1345       (auto simp del: of_nat_mult of_nat_add
  1346         simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
  1347         eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
  1348 next
  1349   case (neg n)
  1350   then show ?thesis
  1351     using div_mult_mod_eq [of n]
  1352     by (cases l rule: int_cases3)
  1353       (auto simp del: of_nat_mult of_nat_add
  1354         simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
  1355         eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
  1356 qed
  1357 
  1358 lemma divmod_int_unique:
  1359   assumes "eucl_rel_int k l (q, r)"
  1360   shows div_int_unique: "k div l = q" and mod_int_unique: "k mod l = r"
  1361   using assms eucl_rel_int [of k l]
  1362   using unique_quotient [of k l] unique_remainder [of k l]
  1363   by auto
  1364 
  1365 instance proof
  1366   fix k l :: int
  1367   show "k div l * l + k mod l = k"
  1368     using eucl_rel_int [of k l]
  1369     unfolding eucl_rel_int_iff by (simp add: ac_simps)
  1370 next
  1371   fix k :: int show "k div 0 = 0"
  1372     by (rule div_int_unique, simp add: eucl_rel_int_iff)
  1373 next
  1374   fix k l :: int
  1375   assume "l \<noteq> 0"
  1376   then show "k * l div l = k"
  1377     by (auto simp add: eucl_rel_int_iff ac_simps intro: div_int_unique [of _ _ _ 0])
  1378 qed (auto simp add: sgn_mult mult_sgn_abs abs_eq_iff')
  1379 
  1380 end
  1381 
  1382 ML \<open>
  1383 structure Cancel_Div_Mod_Int = Cancel_Div_Mod
  1384 (
  1385   val div_name = @{const_name divide};
  1386   val mod_name = @{const_name modulo};
  1387   val mk_binop = HOLogic.mk_binop;
  1388   val mk_sum = Arith_Data.mk_sum HOLogic.intT;
  1389   val dest_sum = Arith_Data.dest_sum;
  1390 
  1391   val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
  1392 
  1393   val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
  1394     @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
  1395 )
  1396 \<close>
  1397 
  1398 simproc_setup cancel_div_mod_int ("(k::int) + l") =
  1399   \<open>K Cancel_Div_Mod_Int.proc\<close>
  1400 
  1401 lemma is_unit_int:
  1402   "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
  1403   by auto
  1404 
  1405 lemma zdiv_int:
  1406   "int (a div b) = int a div int b"
  1407   by (simp add: divide_int_def)
  1408 
  1409 lemma zmod_int:
  1410   "int (a mod b) = int a mod int b"
  1411   by (simp add: modulo_int_def int_dvd_iff)
  1412 
  1413 lemma div_abs_eq_div_nat:
  1414   "\<bar>k\<bar> div \<bar>l\<bar> = int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)"
  1415   by (simp add: divide_int_def)
  1416 
  1417 lemma mod_abs_eq_div_nat:
  1418   "\<bar>k\<bar> mod \<bar>l\<bar> = int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)"
  1419   by (simp add: modulo_int_def dvd_int_unfold_dvd_nat)
  1420 
  1421 lemma div_sgn_abs_cancel:
  1422   fixes k l v :: int
  1423   assumes "v \<noteq> 0"
  1424   shows "(sgn v * \<bar>k\<bar>) div (sgn v * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
  1425 proof -
  1426   from assms have "sgn v = - 1 \<or> sgn v = 1"
  1427     by (cases "v \<ge> 0") auto
  1428   then show ?thesis
  1429     using assms unfolding divide_int_def [of "sgn v * \<bar>k\<bar>" "sgn v * \<bar>l\<bar>"]
  1430     by (fastforce simp add: not_less div_abs_eq_div_nat)
  1431 qed
  1432 
  1433 lemma div_eq_sgn_abs:
  1434   fixes k l v :: int
  1435   assumes "sgn k = sgn l"
  1436   shows "k div l = \<bar>k\<bar> div \<bar>l\<bar>"
  1437 proof (cases "l = 0")
  1438   case True
  1439   then show ?thesis
  1440     by simp
  1441 next
  1442   case False
  1443   with assms have "(sgn k * \<bar>k\<bar>) div (sgn l * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
  1444     by (simp add: div_sgn_abs_cancel)
  1445   then show ?thesis
  1446     by (simp add: sgn_mult_abs)
  1447 qed
  1448 
  1449 lemma div_dvd_sgn_abs:
  1450   fixes k l :: int
  1451   assumes "l dvd k"
  1452   shows "k div l = (sgn k * sgn l) * (\<bar>k\<bar> div \<bar>l\<bar>)"
  1453 proof (cases "k = 0")
  1454   case True
  1455   then show ?thesis
  1456     by simp
  1457 next
  1458   case False
  1459   show ?thesis
  1460   proof (cases "sgn l = sgn k")
  1461     case True
  1462     then show ?thesis
  1463       by (simp add: div_eq_sgn_abs)
  1464   next
  1465     case False
  1466     with \<open>k \<noteq> 0\<close> assms show ?thesis
  1467       unfolding divide_int_def [of k l]
  1468         by (auto simp add: zdiv_int)
  1469   qed
  1470 qed
  1471 
  1472 lemma div_noneq_sgn_abs:
  1473   fixes k l :: int
  1474   assumes "l \<noteq> 0"
  1475   assumes "sgn k \<noteq> sgn l"
  1476   shows "k div l = - (\<bar>k\<bar> div \<bar>l\<bar>) - of_bool (\<not> l dvd k)"
  1477   using assms
  1478   by (simp only: divide_int_def [of k l], auto simp add: not_less zdiv_int)
  1479   
  1480 lemma sgn_mod:
  1481   fixes k l :: int
  1482   assumes "l \<noteq> 0" "\<not> l dvd k"
  1483   shows "sgn (k mod l) = sgn l"
  1484 proof -
  1485   from \<open>\<not> l dvd k\<close>
  1486   have "k mod l \<noteq> 0"
  1487     by (simp add: dvd_eq_mod_eq_0)
  1488   show ?thesis
  1489     using \<open>l \<noteq> 0\<close> \<open>\<not> l dvd k\<close>
  1490     unfolding modulo_int_def [of k l]
  1491     by (auto simp add: sgn_1_pos sgn_1_neg mod_greater_zero_iff_not_dvd nat_dvd_iff not_less
  1492       zless_nat_eq_int_zless [symmetric] elim: nonpos_int_cases)
  1493 qed
  1494 
  1495 lemma abs_mod_less:
  1496   fixes k l :: int
  1497   assumes "l \<noteq> 0"
  1498   shows "\<bar>k mod l\<bar> < \<bar>l\<bar>"
  1499   using assms unfolding modulo_int_def [of k l]
  1500   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)
  1501 
  1502 instantiation int :: unique_euclidean_ring
  1503 begin
  1504 
  1505 definition [simp]:
  1506   "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
  1507 
  1508 definition [simp]:
  1509   "uniqueness_constraint_int (k :: int) l \<longleftrightarrow> unit_factor k = unit_factor l"
  1510   
  1511 instance proof
  1512   fix l q r:: int
  1513   assume "uniqueness_constraint r l"
  1514     and "euclidean_size r < euclidean_size l"
  1515   then have "sgn r = sgn l" and "\<bar>r\<bar> < \<bar>l\<bar>"
  1516     by simp_all
  1517   then have "eucl_rel_int (q * l + r) l (q, r)"
  1518     by (rule eucl_rel_int_remainderI) simp
  1519   then show "(q * l + r) div l = q"
  1520     by (rule div_int_unique)
  1521 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>)
  1522 
  1523 end
  1524 
  1525 text\<open>Basic laws about division and remainder\<close>
  1526 
  1527 lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
  1528   using eucl_rel_int [of a b]
  1529   by (auto simp add: eucl_rel_int_iff prod_eq_iff)
  1530 
  1531 lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
  1532    and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]
  1533 
  1534 lemma neg_mod_conj: "b < (0::int) \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b"
  1535   using eucl_rel_int [of a b]
  1536   by (auto simp add: eucl_rel_int_iff prod_eq_iff)
  1537 
  1538 lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
  1539    and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
  1540 
  1541 
  1542 subsubsection \<open>General Properties of div and mod\<close>
  1543 
  1544 lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
  1545 apply (rule div_int_unique)
  1546 apply (auto simp add: eucl_rel_int_iff)
  1547 done
  1548 
  1549 lemma div_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a div b = 0"
  1550 apply (rule div_int_unique)
  1551 apply (auto simp add: eucl_rel_int_iff)
  1552 done
  1553 
  1554 lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a div b = -1"
  1555 apply (rule div_int_unique)
  1556 apply (auto simp add: eucl_rel_int_iff)
  1557 done
  1558 
  1559 lemma div_positive_int:
  1560   "k div l > 0" if "k \<ge> l" and "l > 0" for k l :: int
  1561   using that by (simp add: divide_int_def div_positive)
  1562 
  1563 (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
  1564 
  1565 lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"
  1566 apply (rule_tac q = 0 in mod_int_unique)
  1567 apply (auto simp add: eucl_rel_int_iff)
  1568 done
  1569 
  1570 lemma mod_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a mod b = a"
  1571 apply (rule_tac q = 0 in mod_int_unique)
  1572 apply (auto simp add: eucl_rel_int_iff)
  1573 done
  1574 
  1575 lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"
  1576 apply (rule_tac q = "-1" in mod_int_unique)
  1577 apply (auto simp add: eucl_rel_int_iff)
  1578 done
  1579 
  1580 text\<open>There is no \<open>mod_neg_pos_trivial\<close>.\<close>
  1581 
  1582 
  1583 subsubsection \<open>Laws for div and mod with Unary Minus\<close>
  1584 
  1585 lemma zminus1_lemma:
  1586      "eucl_rel_int a b (q, r) ==> b \<noteq> 0
  1587       ==> eucl_rel_int (-a) b (if r=0 then -q else -q - 1,
  1588                           if r=0 then 0 else b-r)"
  1589 by (force simp add: eucl_rel_int_iff right_diff_distrib)
  1590 
  1591 
  1592 lemma zdiv_zminus1_eq_if:
  1593      "b \<noteq> (0::int)
  1594       ==> (-a) div b =
  1595           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
  1596 by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN div_int_unique])
  1597 
  1598 lemma zmod_zminus1_eq_if:
  1599      "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
  1600 apply (case_tac "b = 0", simp)
  1601 apply (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN mod_int_unique])
  1602 done
  1603 
  1604 lemma zmod_zminus1_not_zero:
  1605   fixes k l :: int
  1606   shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
  1607   by (simp add: mod_eq_0_iff_dvd)
  1608 
  1609 lemma zmod_zminus2_not_zero:
  1610   fixes k l :: int
  1611   shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
  1612   by (simp add: mod_eq_0_iff_dvd)
  1613 
  1614 lemma zdiv_zminus2_eq_if:
  1615      "b \<noteq> (0::int)
  1616       ==> a div (-b) =
  1617           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
  1618 by (simp add: zdiv_zminus1_eq_if div_minus_right)
  1619 
  1620 lemma zmod_zminus2_eq_if:
  1621      "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
  1622 by (simp add: zmod_zminus1_eq_if mod_minus_right)
  1623 
  1624 
  1625 subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
  1626 
  1627 lemma zdiv_mono1: "[| a \<le> a';  0 < (b::int) |] ==> a div b \<le> a' div b"
  1628 using mult_div_mod_eq [symmetric, of a b]
  1629 using mult_div_mod_eq [symmetric, of a' b]
  1630 apply -
  1631 apply (rule unique_quotient_lemma)
  1632 apply (erule subst)
  1633 apply (erule subst, simp_all)
  1634 done
  1635 
  1636 lemma zdiv_mono1_neg: "[| a \<le> a';  (b::int) < 0 |] ==> a' div b \<le> a div b"
  1637 using mult_div_mod_eq [symmetric, of a b]
  1638 using mult_div_mod_eq [symmetric, of a' b]
  1639 apply -
  1640 apply (rule unique_quotient_lemma_neg)
  1641 apply (erule subst)
  1642 apply (erule subst, simp_all)
  1643 done
  1644 
  1645 
  1646 subsubsection \<open>Monotonicity in the Second Argument (Divisor)\<close>
  1647 
  1648 lemma q_pos_lemma:
  1649      "[| 0 \<le> b'*q' + r'; r' < b';  0 < b' |] ==> 0 \<le> (q'::int)"
  1650 apply (subgoal_tac "0 < b'* (q' + 1) ")
  1651  apply (simp add: zero_less_mult_iff)
  1652 apply (simp add: distrib_left)
  1653 done
  1654 
  1655 lemma zdiv_mono2_lemma:
  1656      "[| b*q + r = b'*q' + r';  0 \<le> b'*q' + r';
  1657          r' < b';  0 \<le> r;  0 < b';  b' \<le> b |]
  1658       ==> q \<le> (q'::int)"
  1659 apply (frule q_pos_lemma, assumption+)
  1660 apply (subgoal_tac "b*q < b* (q' + 1) ")
  1661  apply (simp add: mult_less_cancel_left)
  1662 apply (subgoal_tac "b*q = r' - r + b'*q'")
  1663  prefer 2 apply simp
  1664 apply (simp (no_asm_simp) add: distrib_left)
  1665 apply (subst add.commute, rule add_less_le_mono, arith)
  1666 apply (rule mult_right_mono, auto)
  1667 done
  1668 
  1669 lemma zdiv_mono2:
  1670      "[| (0::int) \<le> a;  0 < b';  b' \<le> b |] ==> a div b \<le> a div b'"
  1671 apply (subgoal_tac "b \<noteq> 0")
  1672   prefer 2 apply arith
  1673 using mult_div_mod_eq [symmetric, of a b]
  1674 using mult_div_mod_eq [symmetric, of a b']
  1675 apply -
  1676 apply (rule zdiv_mono2_lemma)
  1677 apply (erule subst)
  1678 apply (erule subst, simp_all)
  1679 done
  1680 
  1681 lemma q_neg_lemma:
  1682      "[| b'*q' + r' < 0;  0 \<le> r';  0 < b' |] ==> q' \<le> (0::int)"
  1683 apply (subgoal_tac "b'*q' < 0")
  1684  apply (simp add: mult_less_0_iff, arith)
  1685 done
  1686 
  1687 lemma zdiv_mono2_neg_lemma:
  1688      "[| b*q + r = b'*q' + r';  b'*q' + r' < 0;
  1689          r < b;  0 \<le> r';  0 < b';  b' \<le> b |]
  1690       ==> q' \<le> (q::int)"
  1691 apply (frule q_neg_lemma, assumption+)
  1692 apply (subgoal_tac "b*q' < b* (q + 1) ")
  1693  apply (simp add: mult_less_cancel_left)
  1694 apply (simp add: distrib_left)
  1695 apply (subgoal_tac "b*q' \<le> b'*q'")
  1696  prefer 2 apply (simp add: mult_right_mono_neg, arith)
  1697 done
  1698 
  1699 lemma zdiv_mono2_neg:
  1700      "[| a < (0::int);  0 < b';  b' \<le> b |] ==> a div b' \<le> a div b"
  1701 using mult_div_mod_eq [symmetric, of a b]
  1702 using mult_div_mod_eq [symmetric, of a b']
  1703 apply -
  1704 apply (rule zdiv_mono2_neg_lemma)
  1705 apply (erule subst)
  1706 apply (erule subst, simp_all)
  1707 done
  1708 
  1709 
  1710 subsubsection \<open>More Algebraic Laws for div and mod\<close>
  1711 
  1712 text\<open>proving (a*b) div c = a * (b div c) + a * (b mod c)\<close>
  1713 
  1714 lemma zmult1_lemma:
  1715      "[| eucl_rel_int b c (q, r) |]
  1716       ==> eucl_rel_int (a * b) c (a*q + a*r div c, a*r mod c)"
  1717 by (auto simp add: split_ifs eucl_rel_int_iff linorder_neq_iff distrib_left ac_simps)
  1718 
  1719 lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
  1720 apply (case_tac "c = 0", simp)
  1721 apply (blast intro: eucl_rel_int [THEN zmult1_lemma, THEN div_int_unique])
  1722 done
  1723 
  1724 text\<open>proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c)\<close>
  1725 
  1726 lemma zadd1_lemma:
  1727      "[| eucl_rel_int a c (aq, ar);  eucl_rel_int b c (bq, br) |]
  1728       ==> eucl_rel_int (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
  1729 by (force simp add: split_ifs eucl_rel_int_iff linorder_neq_iff distrib_left)
  1730 
  1731 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
  1732 lemma zdiv_zadd1_eq:
  1733      "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
  1734 apply (case_tac "c = 0", simp)
  1735 apply (blast intro: zadd1_lemma [OF eucl_rel_int eucl_rel_int] div_int_unique)
  1736 done
  1737 
  1738 lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
  1739 by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
  1740 
  1741 (* REVISIT: should this be generalized to all semiring_div types? *)
  1742 lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
  1743 
  1744 
  1745 subsubsection \<open>Proving  @{term "a div (b * c) = (a div b) div c"}\<close>
  1746 
  1747 (*The condition c>0 seems necessary.  Consider that 7 div ~6 = ~2 but
  1748   7 div 2 div ~3 = 3 div ~3 = ~1.  The subcase (a div b) mod c = 0 seems
  1749   to cause particular problems.*)
  1750 
  1751 text\<open>first, four lemmas to bound the remainder for the cases b<0 and b>0\<close>
  1752 
  1753 lemma zmult2_lemma_aux1: "[| (0::int) < c;  b < r;  r \<le> 0 |] ==> b * c < b * (q mod c) + r"
  1754 apply (subgoal_tac "b * (c - q mod c) < r * 1")
  1755  apply (simp add: algebra_simps)
  1756 apply (rule order_le_less_trans)
  1757  apply (erule_tac [2] mult_strict_right_mono)
  1758  apply (rule mult_left_mono_neg)
  1759   using add1_zle_eq[of "q mod c"]apply(simp add: algebra_simps)
  1760  apply (simp)
  1761 apply (simp)
  1762 done
  1763 
  1764 lemma zmult2_lemma_aux2:
  1765      "[| (0::int) < c;   b < r;  r \<le> 0 |] ==> b * (q mod c) + r \<le> 0"
  1766 apply (subgoal_tac "b * (q mod c) \<le> 0")
  1767  apply arith
  1768 apply (simp add: mult_le_0_iff)
  1769 done
  1770 
  1771 lemma zmult2_lemma_aux3: "[| (0::int) < c;  0 \<le> r;  r < b |] ==> 0 \<le> b * (q mod c) + r"
  1772 apply (subgoal_tac "0 \<le> b * (q mod c) ")
  1773 apply arith
  1774 apply (simp add: zero_le_mult_iff)
  1775 done
  1776 
  1777 lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 \<le> r; r < b |] ==> b * (q mod c) + r < b * c"
  1778 apply (subgoal_tac "r * 1 < b * (c - q mod c) ")
  1779  apply (simp add: right_diff_distrib)
  1780 apply (rule order_less_le_trans)
  1781  apply (erule mult_strict_right_mono)
  1782  apply (rule_tac [2] mult_left_mono)
  1783   apply simp
  1784  using add1_zle_eq[of "q mod c"] apply (simp add: algebra_simps)
  1785 apply simp
  1786 done
  1787 
  1788 lemma zmult2_lemma: "[| eucl_rel_int a b (q, r); 0 < c |]
  1789       ==> eucl_rel_int a (b * c) (q div c, b*(q mod c) + r)"
  1790 by (auto simp add: mult.assoc eucl_rel_int_iff linorder_neq_iff
  1791                    zero_less_mult_iff distrib_left [symmetric]
  1792                    zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: if_split_asm)
  1793 
  1794 lemma zdiv_zmult2_eq:
  1795   fixes a b c :: int
  1796   shows "0 \<le> c \<Longrightarrow> a div (b * c) = (a div b) div c"
  1797 apply (case_tac "b = 0", simp)
  1798 apply (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN div_int_unique])
  1799 done
  1800 
  1801 lemma zmod_zmult2_eq:
  1802   fixes a b c :: int
  1803   shows "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
  1804 apply (case_tac "b = 0", simp)
  1805 apply (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN mod_int_unique])
  1806 done
  1807 
  1808 lemma div_pos_geq:
  1809   fixes k l :: int
  1810   assumes "0 < l" and "l \<le> k"
  1811   shows "k div l = (k - l) div l + 1"
  1812 proof -
  1813   have "k = (k - l) + l" by simp
  1814   then obtain j where k: "k = j + l" ..
  1815   with assms show ?thesis by (simp add: div_add_self2)
  1816 qed
  1817 
  1818 lemma mod_pos_geq:
  1819   fixes k l :: int
  1820   assumes "0 < l" and "l \<le> k"
  1821   shows "k mod l = (k - l) mod l"
  1822 proof -
  1823   have "k = (k - l) + l" by simp
  1824   then obtain j where k: "k = j + l" ..
  1825   with assms show ?thesis by simp
  1826 qed
  1827 
  1828 
  1829 subsubsection \<open>Splitting Rules for div and mod\<close>
  1830 
  1831 text\<open>The proofs of the two lemmas below are essentially identical\<close>
  1832 
  1833 lemma split_pos_lemma:
  1834  "0<k ==>
  1835     P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
  1836 apply (rule iffI, clarify)
  1837  apply (erule_tac P="P x y" for x y in rev_mp)
  1838  apply (subst mod_add_eq [symmetric])
  1839  apply (subst zdiv_zadd1_eq)
  1840  apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)
  1841 txt\<open>converse direction\<close>
  1842 apply (drule_tac x = "n div k" in spec)
  1843 apply (drule_tac x = "n mod k" in spec, simp)
  1844 done
  1845 
  1846 lemma split_neg_lemma:
  1847  "k<0 ==>
  1848     P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
  1849 apply (rule iffI, clarify)
  1850  apply (erule_tac P="P x y" for x y in rev_mp)
  1851  apply (subst mod_add_eq [symmetric])
  1852  apply (subst zdiv_zadd1_eq)
  1853  apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)
  1854 txt\<open>converse direction\<close>
  1855 apply (drule_tac x = "n div k" in spec)
  1856 apply (drule_tac x = "n mod k" in spec, simp)
  1857 done
  1858 
  1859 lemma split_zdiv:
  1860  "P(n div k :: int) =
  1861   ((k = 0 --> P 0) &
  1862    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) &
  1863    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i)))"
  1864 apply (case_tac "k=0", simp)
  1865 apply (simp only: linorder_neq_iff)
  1866 apply (erule disjE)
  1867  apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"]
  1868                       split_neg_lemma [of concl: "%x y. P x"])
  1869 done
  1870 
  1871 lemma split_zmod:
  1872  "P(n mod k :: int) =
  1873   ((k = 0 --> P n) &
  1874    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P j)) &
  1875    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P j)))"
  1876 apply (case_tac "k=0", simp)
  1877 apply (simp only: linorder_neq_iff)
  1878 apply (erule disjE)
  1879  apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"]
  1880                       split_neg_lemma [of concl: "%x y. P y"])
  1881 done
  1882 
  1883 text \<open>Enable (lin)arith to deal with @{const divide} and @{const modulo}
  1884   when these are applied to some constant that is of the form
  1885   @{term "numeral k"}:\<close>
  1886 declare split_zdiv [of _ _ "numeral k", arith_split] for k
  1887 declare split_zmod [of _ _ "numeral k", arith_split] for k
  1888 
  1889 
  1890 subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
  1891 
  1892 lemma pos_eucl_rel_int_mult_2:
  1893   assumes "0 \<le> b"
  1894   assumes "eucl_rel_int a b (q, r)"
  1895   shows "eucl_rel_int (1 + 2*a) (2*b) (q, 1 + 2*r)"
  1896   using assms unfolding eucl_rel_int_iff by auto
  1897 
  1898 lemma neg_eucl_rel_int_mult_2:
  1899   assumes "b \<le> 0"
  1900   assumes "eucl_rel_int (a + 1) b (q, r)"
  1901   shows "eucl_rel_int (1 + 2*a) (2*b) (q, 2*r - 1)"
  1902   using assms unfolding eucl_rel_int_iff by auto
  1903 
  1904 text\<open>computing div by shifting\<close>
  1905 
  1906 lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
  1907   using pos_eucl_rel_int_mult_2 [OF _ eucl_rel_int]
  1908   by (rule div_int_unique)
  1909 
  1910 lemma neg_zdiv_mult_2:
  1911   assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
  1912   using neg_eucl_rel_int_mult_2 [OF A eucl_rel_int]
  1913   by (rule div_int_unique)
  1914 
  1915 (* FIXME: add rules for negative numerals *)
  1916 lemma zdiv_numeral_Bit0 [simp]:
  1917   "numeral (Num.Bit0 v) div numeral (Num.Bit0 w) =
  1918     numeral v div (numeral w :: int)"
  1919   unfolding numeral.simps unfolding mult_2 [symmetric]
  1920   by (rule div_mult_mult1, simp)
  1921 
  1922 lemma zdiv_numeral_Bit1 [simp]:
  1923   "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) =
  1924     (numeral v div (numeral w :: int))"
  1925   unfolding numeral.simps
  1926   unfolding mult_2 [symmetric] add.commute [of _ 1]
  1927   by (rule pos_zdiv_mult_2, simp)
  1928 
  1929 lemma pos_zmod_mult_2:
  1930   fixes a b :: int
  1931   assumes "0 \<le> a"
  1932   shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"
  1933   using pos_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
  1934   by (rule mod_int_unique)
  1935 
  1936 lemma neg_zmod_mult_2:
  1937   fixes a b :: int
  1938   assumes "a \<le> 0"
  1939   shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"
  1940   using neg_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
  1941   by (rule mod_int_unique)
  1942 
  1943 (* FIXME: add rules for negative numerals *)
  1944 lemma zmod_numeral_Bit0 [simp]:
  1945   "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =
  1946     (2::int) * (numeral v mod numeral w)"
  1947   unfolding numeral_Bit0 [of v] numeral_Bit0 [of w]
  1948   unfolding mult_2 [symmetric] by (rule mod_mult_mult1)
  1949 
  1950 lemma zmod_numeral_Bit1 [simp]:
  1951   "numeral (Num.Bit1 v) mod numeral (Num.Bit0 w) =
  1952     2 * (numeral v mod numeral w) + (1::int)"
  1953   unfolding numeral_Bit1 [of v] numeral_Bit0 [of w]
  1954   unfolding mult_2 [symmetric] add.commute [of _ 1]
  1955   by (rule pos_zmod_mult_2, simp)
  1956 
  1957 lemma zdiv_eq_0_iff:
  1958  "(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")
  1959 proof
  1960   assume ?L
  1961   have "?L \<longrightarrow> ?R" by (rule split_zdiv[THEN iffD2]) simp
  1962   with \<open>?L\<close> show ?R by blast
  1963 next
  1964   assume ?R thus ?L
  1965     by(auto simp: div_pos_pos_trivial div_neg_neg_trivial)
  1966 qed
  1967 
  1968 lemma zmod_trival_iff:
  1969   fixes i k :: int
  1970   shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
  1971 proof -
  1972   have "i mod k = i \<longleftrightarrow> i div k = 0"
  1973     by safe (insert div_mult_mod_eq [of i k], auto)
  1974   with zdiv_eq_0_iff
  1975   show ?thesis
  1976     by simp
  1977 qed
  1978 
  1979   
  1980 subsubsection \<open>Quotients of Signs\<close>
  1981 
  1982 lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
  1983 by (simp add: divide_int_def)
  1984 
  1985 lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
  1986 by (simp add: modulo_int_def)
  1987 
  1988 lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"
  1989 apply (subgoal_tac "a div b \<le> -1", force)
  1990 apply (rule order_trans)
  1991 apply (rule_tac a' = "-1" in zdiv_mono1)
  1992 apply (auto simp add: div_eq_minus1)
  1993 done
  1994 
  1995 lemma div_nonneg_neg_le0: "[| (0::int) \<le> a; b < 0 |] ==> a div b \<le> 0"
  1996 by (drule zdiv_mono1_neg, auto)
  1997 
  1998 lemma div_nonpos_pos_le0: "[| (a::int) \<le> 0; b > 0 |] ==> a div b \<le> 0"
  1999 by (drule zdiv_mono1, auto)
  2000 
  2001 text\<open>Now for some equivalences of the form \<open>a div b >=< 0 \<longleftrightarrow> \<dots>\<close>
  2002 conditional upon the sign of \<open>a\<close> or \<open>b\<close>. There are many more.
  2003 They should all be simp rules unless that causes too much search.\<close>
  2004 
  2005 lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"
  2006 apply auto
  2007 apply (drule_tac [2] zdiv_mono1)
  2008 apply (auto simp add: linorder_neq_iff)
  2009 apply (simp (no_asm_use) add: linorder_not_less [symmetric])
  2010 apply (blast intro: div_neg_pos_less0)
  2011 done
  2012 
  2013 lemma pos_imp_zdiv_pos_iff:
  2014   "0<k \<Longrightarrow> 0 < (i::int) div k \<longleftrightarrow> k \<le> i"
  2015 using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k]
  2016 by arith
  2017 
  2018 lemma neg_imp_zdiv_nonneg_iff:
  2019   "b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))"
  2020 apply (subst div_minus_minus [symmetric])
  2021 apply (subst pos_imp_zdiv_nonneg_iff, auto)
  2022 done
  2023 
  2024 (*But not (a div b \<le> 0 iff a\<le>0); consider a=1, b=2 when a div b = 0.*)
  2025 lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)"
  2026 by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff)
  2027 
  2028 (*Again the law fails for \<le>: consider a = -1, b = -2 when a div b = 0*)
  2029 lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"
  2030 by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)
  2031 
  2032 lemma nonneg1_imp_zdiv_pos_iff:
  2033   "(0::int) <= a \<Longrightarrow> (a div b > 0) = (a >= b & b>0)"
  2034 apply rule
  2035  apply rule
  2036   using div_pos_pos_trivial[of a b]apply arith
  2037  apply(cases "b=0")apply simp
  2038  using div_nonneg_neg_le0[of a b]apply arith
  2039 using int_one_le_iff_zero_less[of "a div b"] zdiv_mono1[of b a b]apply simp
  2040 done
  2041 
  2042 lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 ==> m mod k \<le> m"
  2043 apply (rule split_zmod[THEN iffD2])
  2044 apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le)
  2045 done
  2046 
  2047 
  2048 subsubsection \<open>Computation of Division and Remainder\<close>
  2049 
  2050 instantiation int :: unique_euclidean_semiring_numeral
  2051 begin
  2052 
  2053 definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int"
  2054 where
  2055   "divmod_int m n = (numeral m div numeral n, numeral m mod numeral n)"
  2056 
  2057 definition divmod_step_int :: "num \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int"
  2058 where
  2059   "divmod_step_int l qr = (let (q, r) = qr
  2060     in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
  2061     else (2 * q, r))"
  2062 
  2063 instance
  2064   by standard (auto intro: zmod_le_nonneg_dividend simp add: divmod_int_def divmod_step_int_def
  2065     pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial zmod_zmult2_eq zdiv_zmult2_eq)
  2066 
  2067 end
  2068 
  2069 declare divmod_algorithm_code [where ?'a = int, code]
  2070 
  2071 context
  2072 begin
  2073   
  2074 qualified definition adjust_div :: "int \<times> int \<Rightarrow> int"
  2075 where
  2076   "adjust_div qr = (let (q, r) = qr in q + of_bool (r \<noteq> 0))"
  2077 
  2078 qualified lemma adjust_div_eq [simp, code]:
  2079   "adjust_div (q, r) = q + of_bool (r \<noteq> 0)"
  2080   by (simp add: adjust_div_def)
  2081 
  2082 qualified definition adjust_mod :: "int \<Rightarrow> int \<Rightarrow> int"
  2083 where
  2084   [simp]: "adjust_mod l r = (if r = 0 then 0 else l - r)"
  2085 
  2086 lemma minus_numeral_div_numeral [simp]:
  2087   "- numeral m div numeral n = - (adjust_div (divmod m n) :: int)"
  2088 proof -
  2089   have "int (fst (divmod m n)) = fst (divmod m n)"
  2090     by (simp only: fst_divmod divide_int_def) auto
  2091   then show ?thesis
  2092     by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
  2093 qed
  2094 
  2095 lemma minus_numeral_mod_numeral [simp]:
  2096   "- numeral m mod numeral n = adjust_mod (numeral n) (snd (divmod m n) :: int)"
  2097 proof -
  2098   have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
  2099     using that by (simp only: snd_divmod modulo_int_def) auto
  2100   then show ?thesis
  2101     by (auto simp add: split_def Let_def adjust_div_def divides_aux_def modulo_int_def)
  2102 qed
  2103 
  2104 lemma numeral_div_minus_numeral [simp]:
  2105   "numeral m div - numeral n = - (adjust_div (divmod m n) :: int)"
  2106 proof -
  2107   have "int (fst (divmod m n)) = fst (divmod m n)"
  2108     by (simp only: fst_divmod divide_int_def) auto
  2109   then show ?thesis
  2110     by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def)
  2111 qed
  2112   
  2113 lemma numeral_mod_minus_numeral [simp]:
  2114   "numeral m mod - numeral n = - adjust_mod (numeral n) (snd (divmod m n) :: int)"
  2115 proof -
  2116   have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
  2117     using that by (simp only: snd_divmod modulo_int_def) auto
  2118   then show ?thesis
  2119     by (auto simp add: split_def Let_def adjust_div_def divides_aux_def modulo_int_def)
  2120 qed
  2121 
  2122 lemma minus_one_div_numeral [simp]:
  2123   "- 1 div numeral n = - (adjust_div (divmod Num.One n) :: int)"
  2124   using minus_numeral_div_numeral [of Num.One n] by simp  
  2125 
  2126 lemma minus_one_mod_numeral [simp]:
  2127   "- 1 mod numeral n = adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
  2128   using minus_numeral_mod_numeral [of Num.One n] by simp
  2129 
  2130 lemma one_div_minus_numeral [simp]:
  2131   "1 div - numeral n = - (adjust_div (divmod Num.One n) :: int)"
  2132   using numeral_div_minus_numeral [of Num.One n] by simp
  2133   
  2134 lemma one_mod_minus_numeral [simp]:
  2135   "1 mod - numeral n = - adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
  2136   using numeral_mod_minus_numeral [of Num.One n] by simp
  2137 
  2138 end
  2139 
  2140 
  2141 subsubsection \<open>Further properties\<close>
  2142 
  2143 text \<open>Simplify expresions in which div and mod combine numerical constants\<close>
  2144 
  2145 lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
  2146   by (rule div_int_unique [of a b q r]) (simp add: eucl_rel_int_iff)
  2147 
  2148 lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
  2149   by (rule div_int_unique [of a b q r],
  2150     simp add: eucl_rel_int_iff)
  2151 
  2152 lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
  2153   by (rule mod_int_unique [of a b q r],
  2154     simp add: eucl_rel_int_iff)
  2155 
  2156 lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
  2157   by (rule mod_int_unique [of a b q r],
  2158     simp add: eucl_rel_int_iff)
  2159 
  2160 lemma abs_div: "(y::int) dvd x \<Longrightarrow> \<bar>x div y\<bar> = \<bar>x\<bar> div \<bar>y\<bar>"
  2161 by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
  2162 
  2163 text\<open>Suggested by Matthias Daum\<close>
  2164 lemma int_power_div_base:
  2165      "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
  2166 apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)")
  2167  apply (erule ssubst)
  2168  apply (simp only: power_add)
  2169  apply simp_all
  2170 done
  2171 
  2172 text \<open>Distributive laws for function \<open>nat\<close>.\<close>
  2173 
  2174 lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"
  2175 apply (rule linorder_cases [of y 0])
  2176 apply (simp add: div_nonneg_neg_le0)
  2177 apply simp
  2178 apply (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int)
  2179 done
  2180 
  2181 (*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*)
  2182 lemma nat_mod_distrib:
  2183   "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x mod y) = nat x mod nat y"
  2184 apply (case_tac "y = 0", simp)
  2185 apply (simp add: nat_eq_iff zmod_int)
  2186 done
  2187 
  2188 text  \<open>transfer setup\<close>
  2189 
  2190 lemma transfer_nat_int_functions:
  2191     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
  2192     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
  2193   by (auto simp add: nat_div_distrib nat_mod_distrib)
  2194 
  2195 lemma transfer_nat_int_function_closures:
  2196     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
  2197     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
  2198   apply (cases "y = 0")
  2199   apply (auto simp add: pos_imp_zdiv_nonneg_iff)
  2200   apply (cases "y = 0")
  2201   apply auto
  2202 done
  2203 
  2204 declare transfer_morphism_nat_int [transfer add return:
  2205   transfer_nat_int_functions
  2206   transfer_nat_int_function_closures
  2207 ]
  2208 
  2209 lemma transfer_int_nat_functions:
  2210     "(int x) div (int y) = int (x div y)"
  2211     "(int x) mod (int y) = int (x mod y)"
  2212   by (auto simp add: zdiv_int zmod_int)
  2213 
  2214 lemma transfer_int_nat_function_closures:
  2215     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
  2216     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
  2217   by (simp_all only: is_nat_def transfer_nat_int_function_closures)
  2218 
  2219 declare transfer_morphism_int_nat [transfer add return:
  2220   transfer_int_nat_functions
  2221   transfer_int_nat_function_closures
  2222 ]
  2223 
  2224 text\<open>Suggested by Matthias Daum\<close>
  2225 lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
  2226 apply (subgoal_tac "nat x div nat k < nat x")
  2227  apply (simp add: nat_div_distrib [symmetric])
  2228 apply (rule Divides.div_less_dividend, simp_all)
  2229 done
  2230 
  2231 lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
  2232   shows "\<exists>q. x = y + n * q"
  2233 proof-
  2234   from xy have th: "int x - int y = int (x - y)" by simp
  2235   from xyn have "int x mod int n = int y mod int n"
  2236     by (simp add: zmod_int [symmetric])
  2237   hence "int n dvd int x - int y" by (simp only: mod_eq_dvd_iff [symmetric])
  2238   hence "n dvd x - y" by (simp add: th zdvd_int)
  2239   then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
  2240 qed
  2241 
  2242 lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)"
  2243   (is "?lhs = ?rhs")
  2244 proof
  2245   assume H: "x mod n = y mod n"
  2246   {assume xy: "x \<le> y"
  2247     from H have th: "y mod n = x mod n" by simp
  2248     from nat_mod_eq_lemma[OF th xy] have ?rhs
  2249       apply clarify  apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}
  2250   moreover
  2251   {assume xy: "y \<le> x"
  2252     from nat_mod_eq_lemma[OF H xy] have ?rhs
  2253       apply clarify  apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}
  2254   ultimately  show ?rhs using linear[of x y] by blast
  2255 next
  2256   assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast
  2257   hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp
  2258   thus  ?lhs by simp
  2259 qed
  2260 
  2261 subsubsection \<open>Dedicated simproc for calculation\<close>
  2262 
  2263 text \<open>
  2264   There is space for improvement here: the calculation itself
  2265   could be carried outside the logic, and a generic simproc
  2266   (simplifier setup) for generic calculation would be helpful. 
  2267 \<close>
  2268 
  2269 simproc_setup numeral_divmod
  2270   ("0 div 0 :: 'a :: unique_euclidean_semiring_numeral" | "0 mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
  2271    "0 div 1 :: 'a :: unique_euclidean_semiring_numeral" | "0 mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
  2272    "0 div - 1 :: int" | "0 mod - 1 :: int" |
  2273    "0 div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "0 mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
  2274    "0 div - numeral b :: int" | "0 mod - numeral b :: int" |
  2275    "1 div 0 :: 'a :: unique_euclidean_semiring_numeral" | "1 mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
  2276    "1 div 1 :: 'a :: unique_euclidean_semiring_numeral" | "1 mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
  2277    "1 div - 1 :: int" | "1 mod - 1 :: int" |
  2278    "1 div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "1 mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
  2279    "1 div - numeral b :: int" |"1 mod - numeral b :: int" |
  2280    "- 1 div 0 :: int" | "- 1 mod 0 :: int" | "- 1 div 1 :: int" | "- 1 mod 1 :: int" |
  2281    "- 1 div - 1 :: int" | "- 1 mod - 1 :: int" | "- 1 div numeral b :: int" | "- 1 mod numeral b :: int" |
  2282    "- 1 div - numeral b :: int" | "- 1 mod - numeral b :: int" |
  2283    "numeral a div 0 :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
  2284    "numeral a div 1 :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
  2285    "numeral a div - 1 :: int" | "numeral a mod - 1 :: int" |
  2286    "numeral a div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
  2287    "numeral a div - numeral b :: int" | "numeral a mod - numeral b :: int" |
  2288    "- numeral a div 0 :: int" | "- numeral a mod 0 :: int" |
  2289    "- numeral a div 1 :: int" | "- numeral a mod 1 :: int" |
  2290    "- numeral a div - 1 :: int" | "- numeral a mod - 1 :: int" |
  2291    "- numeral a div numeral b :: int" | "- numeral a mod numeral b :: int" |
  2292    "- numeral a div - numeral b :: int" | "- numeral a mod - numeral b :: int") =
  2293 \<open> let
  2294     val if_cong = the (Code.get_case_cong @{theory} @{const_name If});
  2295     fun successful_rewrite ctxt ct =
  2296       let
  2297         val thm = Simplifier.rewrite ctxt ct
  2298       in if Thm.is_reflexive thm then NONE else SOME thm end;
  2299   in fn phi =>
  2300     let
  2301       val simps = Morphism.fact phi (@{thms div_0 mod_0 div_by_0 mod_by_0 div_by_1 mod_by_1
  2302         one_div_numeral one_mod_numeral minus_one_div_numeral minus_one_mod_numeral
  2303         one_div_minus_numeral one_mod_minus_numeral
  2304         numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
  2305         numeral_div_minus_numeral numeral_mod_minus_numeral
  2306         div_minus_minus mod_minus_minus Divides.adjust_div_eq of_bool_eq one_neq_zero
  2307         numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial
  2308         divmod_cancel divmod_steps divmod_step_eq fst_conv snd_conv numeral_One
  2309         case_prod_beta rel_simps Divides.adjust_mod_def div_minus1_right mod_minus1_right
  2310         minus_minus numeral_times_numeral mult_zero_right mult_1_right}
  2311         @ [@{lemma "0 = 0 \<longleftrightarrow> True" by simp}]);
  2312       fun prepare_simpset ctxt = HOL_ss |> Simplifier.simpset_map ctxt
  2313         (Simplifier.add_cong if_cong #> fold Simplifier.add_simp simps)
  2314     in fn ctxt => successful_rewrite (Simplifier.put_simpset (prepare_simpset ctxt) ctxt) end
  2315   end;
  2316 \<close>
  2317 
  2318 
  2319 subsubsection \<open>Code generation\<close>
  2320 
  2321 lemma [code]:
  2322   fixes k :: int
  2323   shows 
  2324     "k div 0 = 0"
  2325     "k mod 0 = k"
  2326     "0 div k = 0"
  2327     "0 mod k = 0"
  2328     "k div Int.Pos Num.One = k"
  2329     "k mod Int.Pos Num.One = 0"
  2330     "k div Int.Neg Num.One = - k"
  2331     "k mod Int.Neg Num.One = 0"
  2332     "Int.Pos m div Int.Pos n = (fst (divmod m n) :: int)"
  2333     "Int.Pos m mod Int.Pos n = (snd (divmod m n) :: int)"
  2334     "Int.Neg m div Int.Pos n = - (Divides.adjust_div (divmod m n) :: int)"
  2335     "Int.Neg m mod Int.Pos n = Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
  2336     "Int.Pos m div Int.Neg n = - (Divides.adjust_div (divmod m n) :: int)"
  2337     "Int.Pos m mod Int.Neg n = - Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
  2338     "Int.Neg m div Int.Neg n = (fst (divmod m n) :: int)"
  2339     "Int.Neg m mod Int.Neg n = - (snd (divmod m n) :: int)"
  2340   by simp_all
  2341 
  2342 code_identifier
  2343   code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  2344 
  2345 lemma dvd_eq_mod_eq_0_numeral:
  2346   "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semidom_modulo)"
  2347   by (fact dvd_eq_mod_eq_0)
  2348 
  2349 declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
  2350 
  2351 end