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