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