isabelle: src/HOL/Divides.thy@b9853c187a1e

     1 (*  Title:      HOL/Divides.thy

     2     ID:         $Id$

     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     4     Copyright   1999  University of Cambridge

     5 *)

     7 header {* The division operators div, mod and the divides relation "dvd" *}

     9 theory Divides

    10 imports Datatype Power

    11 uses "~~/src/Provers/Arith/cancel_div_mod.ML"

    12 begin

    14 (*We use the same class for div and mod;

    15   moreover, dvd is defined whenever multiplication is*)

    16 class div = type +

    17   fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"

    18   fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"

    19 begin

    21 notation

    22   div (infixl "\<^loc>div" 70)

    24 notation

    25   mod (infixl "\<^loc>mod" 70)

    27 end

    29 notation

    30   div (infixl "div" 70)

    32 notation

    33   mod (infixl "mod" 70)

    35 instance nat :: Divides.div

    36   div_def: "m div n == wfrec (pred_nat^+)

    37                           (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"

    38   mod_def: "m mod n == wfrec (pred_nat^+)

    39                           (%f j. if j<n | n=0 then j else f (j-n)) m" ..

    41 definition

    42   (*The definition of dvd is polymorphic!*)

    43   dvd  :: "'a::times \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) where

    44   dvd_def: "m dvd n \<longleftrightarrow> (\<exists>k. n = m*k)"

    46 definition

    47   quorem :: "(nat*nat) * (nat*nat) => bool" where

    48   (*This definition helps prove the harder properties of div and mod.

    49     It is copied from IntDiv.thy; should it be overloaded?*)

    50   "quorem = (%((a,b), (q,r)).

    51                     a = b*q + r &

    52                     (if 0<b then 0\<le>r & r<b else b<r & r \<le>0))"

    56 subsection{*Initial Lemmas*}

    58 lemmas wf_less_trans =

    59        def_wfrec [THEN trans, OF eq_reflection wf_pred_nat [THEN wf_trancl],

    60                   standard]

    62 lemma mod_eq: "(%m. m mod n) =

    63               wfrec (pred_nat^+) (%f j. if j<n | n=0 then j else f (j-n))"

    64 by (simp add: mod_def)

    66 lemma div_eq: "(%m. m div n) = wfrec (pred_nat^+)

    67                (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))"

    68 by (simp add: div_def)

    71 (** Aribtrary definitions for division by zero.  Useful to simplify

    72     certain equations **)

    74 lemma DIVISION_BY_ZERO_DIV [simp]: "a div 0 = (0::nat)"

    75   by (rule div_eq [THEN wf_less_trans], simp)

    77 lemma DIVISION_BY_ZERO_MOD [simp]: "a mod 0 = (a::nat)"

    78   by (rule mod_eq [THEN wf_less_trans], simp)

    81 subsection{*Remainder*}

    83 lemma mod_less [simp]: "m<n ==> m mod n = (m::nat)"

    84   by (rule mod_eq [THEN wf_less_trans]) simp

    86 lemma mod_geq: "~ m < (n::nat) ==> m mod n = (m-n) mod n"

    87   apply (cases "n=0")

    88    apply simp

    89   apply (rule mod_eq [THEN wf_less_trans])

    90   apply (simp add: cut_apply less_eq)

    91   done

    93 (*Avoids the ugly ~m<n above*)

    94 lemma le_mod_geq: "(n::nat) \<le> m ==> m mod n = (m-n) mod n"

    95   by (simp add: mod_geq linorder_not_less)

    97 lemma mod_if: "m mod (n::nat) = (if m<n then m else (m-n) mod n)"

    98   by (simp add: mod_geq)

   100 lemma mod_1 [simp]: "m mod Suc 0 = 0"

   101   by (induct m) (simp_all add: mod_geq)

   103 lemma mod_self [simp]: "n mod n = (0::nat)"

   104   by (cases "n = 0") (simp_all add: mod_geq)

   106 lemma mod_add_self2 [simp]: "(m+n) mod n = m mod (n::nat)"

   107   apply (subgoal_tac "(n + m) mod n = (n+m-n) mod n")

   108    apply (simp add: add_commute)

   109   apply (subst mod_geq [symmetric], simp_all)

   110   done

   112 lemma mod_add_self1 [simp]: "(n+m) mod n = m mod (n::nat)"

   113   by (simp add: add_commute mod_add_self2)

   115 lemma mod_mult_self1 [simp]: "(m + k*n) mod n = m mod (n::nat)"

   116   by (induct k) (simp_all add: add_left_commute [of _ n])

   118 lemma mod_mult_self2 [simp]: "(m + n*k) mod n = m mod (n::nat)"

   119   by (simp add: mult_commute mod_mult_self1)

   121 lemma mod_mult_distrib: "(m mod n) * (k::nat) = (m*k) mod (n*k)"

   122   apply (cases "n = 0", simp)

   123   apply (cases "k = 0", simp)

   124   apply (induct m rule: nat_less_induct)

   125   apply (subst mod_if, simp)

   126   apply (simp add: mod_geq diff_mult_distrib)

   127   done

   129 lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)"

   130   by (simp add: mult_commute [of k] mod_mult_distrib)

   132 lemma mod_mult_self_is_0 [simp]: "(m*n) mod n = (0::nat)"

   133   apply (cases "n = 0", simp)

   134   apply (induct m, simp)

   135   apply (rename_tac k)

   136   apply (cut_tac m = "k * n" and n = n in mod_add_self2)

   137   apply (simp add: add_commute)

   138   done

   140 lemma mod_mult_self1_is_0 [simp]: "(n*m) mod n = (0::nat)"

   141   by (simp add: mult_commute mod_mult_self_is_0)

   144 subsection{*Quotient*}

   146 lemma div_less [simp]: "m<n ==> m div n = (0::nat)"

   147   by (rule div_eq [THEN wf_less_trans], simp)

   149 lemma div_geq: "[| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)"

   150   apply (rule div_eq [THEN wf_less_trans])

   151   apply (simp add: cut_apply less_eq)

   152   done

   154 (*Avoids the ugly ~m<n above*)

   155 lemma le_div_geq: "[| 0<n;  n\<le>m |] ==> m div n = Suc((m-n) div n)"

   156   by (simp add: div_geq linorder_not_less)

   158 lemma div_if: "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))"

   159   by (simp add: div_geq)

   162 (*Main Result about quotient and remainder.*)

   163 lemma mod_div_equality: "(m div n)*n + m mod n = (m::nat)"

   164   apply (cases "n = 0", simp)

   165   apply (induct m rule: nat_less_induct)

   166   apply (subst mod_if)

   167   apply (simp_all add: add_assoc div_geq add_diff_inverse)

   168   done

   170 lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)"

   171   apply (cut_tac m = m and n = n in mod_div_equality)

   172   apply (simp add: mult_commute)

   173   done

   175 subsection{*Simproc for Cancelling Div and Mod*}

   177 lemma div_mod_equality: "((m div n)*n + m mod n) + k = (m::nat) + k"

   178   by (simp add: mod_div_equality)

   180 lemma div_mod_equality2: "(n*(m div n) + m mod n) + k = (m::nat) + k"

   181   by (simp add: mod_div_equality2)

   183 ML

   184 {*

   185 structure CancelDivModData =

   186 struct

   188 val div_name = @{const_name Divides.div};

   189 val mod_name = @{const_name Divides.mod};

   190 val mk_binop = HOLogic.mk_binop;

   191 val mk_sum = NatArithUtils.mk_sum;

   192 val dest_sum = NatArithUtils.dest_sum;

   194 (*logic*)

   196 val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}]

   198 val trans = trans

   200 val prove_eq_sums =

   201   let val simps = @{thm add_0} :: @{thm add_0_right} :: @{thms add_ac}

   202   in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;

   204 end;

   206 structure CancelDivMod = CancelDivModFun(CancelDivModData);

   208 val cancel_div_mod_proc = NatArithUtils.prep_simproc

   209       ("cancel_div_mod", ["(m::nat) + n"], K CancelDivMod.proc);

   211 Addsimprocs[cancel_div_mod_proc];

   212 *}

   215 (* a simple rearrangement of mod_div_equality: *)

   216 lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"

   217   by (cut_tac m = m and n = n in mod_div_equality2, arith)

   219 lemma mod_less_divisor [simp]: "0<n ==> m mod n < (n::nat)"

   220   apply (induct m rule: nat_less_induct)

   221   apply (rename_tac m)

   222   apply (case_tac "m<n", simp)

   223   txt{*case @{term "n \<le> m"}*}

   224   apply (simp add: mod_geq)

   225   done

   227 lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"

   228   apply (drule mod_less_divisor [where m = m])

   229   apply simp

   230   done

   232 lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"

   233   by (cut_tac m = "m*n" and n = n in mod_div_equality, auto)

   235 lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"

   236   by (simp add: mult_commute div_mult_self_is_m)

   238 (*mod_mult_distrib2 above is the counterpart for remainder*)

   241 subsection{*Proving facts about Quotient and Remainder*}

   243 lemma unique_quotient_lemma:

   244      "[| b*q' + r'  \<le> b*q + r;  x < b;  r < b |]

   245       ==> q' \<le> (q::nat)"

   246   apply (rule leI)

   247   apply (subst less_iff_Suc_add)

   248   apply (auto simp add: add_mult_distrib2)

   249   done

   251 lemma unique_quotient:

   252      "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |]

   253       ==> q = q'"

   254   apply (simp add: split_ifs quorem_def)

   255   apply (blast intro: order_antisym

   256     dest: order_eq_refl [THEN unique_quotient_lemma] sym)

   257   done

   259 lemma unique_remainder:

   260      "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |]

   261       ==> r = r'"

   262   apply (subgoal_tac "q = q'")

   263    prefer 2 apply (blast intro: unique_quotient)

   264   apply (simp add: quorem_def)

   265   done

   267 lemma quorem_div_mod: "0 < b ==> quorem ((a, b), (a div b, a mod b))"

   268   unfolding quorem_def by simp

   270 lemma quorem_div: "[| quorem((a,b),(q,r));  0 < b |] ==> a div b = q"

   271   by (simp add: quorem_div_mod [THEN unique_quotient])

   273 lemma quorem_mod: "[| quorem((a,b),(q,r));  0 < b |] ==> a mod b = r"

   274   by (simp add: quorem_div_mod [THEN unique_remainder])

   276 (** A dividend of zero **)

   278 lemma div_0 [simp]: "0 div m = (0::nat)"

   279   by (cases "m = 0") simp_all

   281 lemma mod_0 [simp]: "0 mod m = (0::nat)"

   282   by (cases "m = 0") simp_all

   284 (** proving (a*b) div c = a * (b div c) + a * (b mod c) **)

   286 lemma quorem_mult1_eq:

   287      "[| quorem((b,c),(q,r));  0 < c |]

   288       ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"

   289   by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)

   291 lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"

   292   apply (cases "c = 0", simp)

   293   apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_div])

   294   done

   296 lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)"

   297   apply (cases "c = 0", simp)

   298   apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_mod])

   299   done

   301 lemma mod_mult1_eq': "(a*b) mod (c::nat) = ((a mod c) * b) mod c"

   302   apply (rule trans)

   303    apply (rule_tac s = "b*a mod c" in trans)

   304     apply (rule_tac [2] mod_mult1_eq)

   305    apply (simp_all add: mult_commute)

   306   done

   308 lemma mod_mult_distrib_mod: "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"

   309   apply (rule mod_mult1_eq' [THEN trans])

   310   apply (rule mod_mult1_eq)

   311   done

   313 (** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)

   315 lemma quorem_add1_eq:

   316      "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  0 < c |]

   317       ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"

   318   by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)

   320 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)

   321 lemma div_add1_eq:

   322      "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"

   323   apply (cases "c = 0", simp)

   324   apply (blast intro: quorem_add1_eq [THEN quorem_div] quorem_div_mod quorem_div_mod)

   325   done

   327 lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"

   328   apply (cases "c = 0", simp)

   329   apply (blast intro: quorem_div_mod quorem_div_mod quorem_add1_eq [THEN quorem_mod])

   330   done

   333 subsection{*Proving @{term "a div (b*c) = (a div b) div c"}*}

   335 (** first, a lemma to bound the remainder **)

   337 lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"

   338   apply (cut_tac m = q and n = c in mod_less_divisor)

   339   apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)

   340   apply (erule_tac P = "%x. ?lhs < ?rhs x" in ssubst)

   341   apply (simp add: add_mult_distrib2)

   342   done

   344 lemma quorem_mult2_eq: "[| quorem ((a,b), (q,r));  0 < b;  0 < c |]

   345       ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"

   346   by (auto simp add: mult_ac quorem_def add_mult_distrib2 [symmetric] mod_lemma)

   348 lemma div_mult2_eq: "a div (b*c) = (a div b) div (c::nat)"

   349   apply (cases "b = 0", simp)

   350   apply (cases "c = 0", simp)

   351   apply (force simp add: quorem_div_mod [THEN quorem_mult2_eq, THEN quorem_div])

   352   done

   354 lemma mod_mult2_eq: "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)"

   355   apply (cases "b = 0", simp)

   356   apply (cases "c = 0", simp)

   357   apply (auto simp add: mult_commute quorem_div_mod [THEN quorem_mult2_eq, THEN quorem_mod])

   358   done

   361 subsection{*Cancellation of Common Factors in Division*}

   363 lemma div_mult_mult_lemma:

   364     "[| (0::nat) < b;  0 < c |] ==> (c*a) div (c*b) = a div b"

   365   by (auto simp add: div_mult2_eq)

   367 lemma div_mult_mult1 [simp]: "(0::nat) < c ==> (c*a) div (c*b) = a div b"

   368   apply (cases "b = 0")

   369   apply (auto simp add: linorder_neq_iff [of b] div_mult_mult_lemma)

   370   done

   372 lemma div_mult_mult2 [simp]: "(0::nat) < c ==> (a*c) div (b*c) = a div b"

   373   apply (drule div_mult_mult1)

   374   apply (auto simp add: mult_commute)

   375   done

   378 subsection{*Further Facts about Quotient and Remainder*}

   380 lemma div_1 [simp]: "m div Suc 0 = m"

   381   by (induct m) (simp_all add: div_geq)

   383 lemma div_self [simp]: "0<n ==> n div n = (1::nat)"

   384   by (simp add: div_geq)

   386 lemma div_add_self2: "0<n ==> (m+n) div n = Suc (m div n)"

   387   apply (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n) ")

   388    apply (simp add: add_commute)

   389   apply (subst div_geq [symmetric], simp_all)

   390   done

   392 lemma div_add_self1: "0<n ==> (n+m) div n = Suc (m div n)"

   393   by (simp add: add_commute div_add_self2)

   395 lemma div_mult_self1 [simp]: "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n"

   396   apply (subst div_add1_eq)

   397   apply (subst div_mult1_eq, simp)

   398   done

   400 lemma div_mult_self2 [simp]: "0<n ==> (m + n*k) div n = k + m div (n::nat)"

   401   by (simp add: mult_commute div_mult_self1)

   404 (* Monotonicity of div in first argument *)

   405 lemma div_le_mono [rule_format (no_asm)]:

   406     "\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"

   407 apply (case_tac "k=0", simp)

   408 apply (induct "n" rule: nat_less_induct, clarify)

   409 apply (case_tac "n<k")

   410 (* 1  case n<k *)

   411 apply simp

   412 (* 2  case n >= k *)

   413 apply (case_tac "m<k")

   414 (* 2.1  case m<k *)

   415 apply simp

   416 (* 2.2  case m>=k *)

   417 apply (simp add: div_geq diff_le_mono)

   418 done

   420 (* Antimonotonicity of div in second argument *)

   421 lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"

   422 apply (subgoal_tac "0<n")

   423  prefer 2 apply simp

   424 apply (induct_tac k rule: nat_less_induct)

   425 apply (rename_tac "k")

   426 apply (case_tac "k<n", simp)

   427 apply (subgoal_tac "~ (k<m) ")

   428  prefer 2 apply simp

   429 apply (simp add: div_geq)

   430 apply (subgoal_tac "(k-n) div n \<le> (k-m) div n")

   431  prefer 2

   432  apply (blast intro: div_le_mono diff_le_mono2)

   433 apply (rule le_trans, simp)

   434 apply (simp)

   435 done

   437 lemma div_le_dividend [simp]: "m div n \<le> (m::nat)"

   438 apply (case_tac "n=0", simp)

   439 apply (subgoal_tac "m div n \<le> m div 1", simp)

   440 apply (rule div_le_mono2)

   441 apply (simp_all (no_asm_simp))

   442 done

   444 (* Similar for "less than" *)

   445 lemma div_less_dividend [rule_format]:

   446      "!!n::nat. 1<n ==> 0 < m --> m div n < m"

   447 apply (induct_tac m rule: nat_less_induct)

   448 apply (rename_tac "m")

   449 apply (case_tac "m<n", simp)

   450 apply (subgoal_tac "0<n")

   451  prefer 2 apply simp

   452 apply (simp add: div_geq)

   453 apply (case_tac "n<m")

   454  apply (subgoal_tac "(m-n) div n < (m-n) ")

   455   apply (rule impI less_trans_Suc)+

   456 apply assumption

   457   apply (simp_all)

   458 done

   460 declare div_less_dividend [simp]

   462 text{*A fact for the mutilated chess board*}

   463 lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"

   464 apply (case_tac "n=0", simp)

   465 apply (induct "m" rule: nat_less_induct)

   466 apply (case_tac "Suc (na) <n")

   467 (* case Suc(na) < n *)

   468 apply (frule lessI [THEN less_trans], simp add: less_not_refl3)

   469 (* case n \<le> Suc(na) *)

   470 apply (simp add: linorder_not_less le_Suc_eq mod_geq)

   471 apply (auto simp add: Suc_diff_le le_mod_geq)

   472 done

   474 lemma nat_mod_div_trivial [simp]: "m mod n div n = (0 :: nat)"

   475   by (cases "n = 0") auto

   477 lemma nat_mod_mod_trivial [simp]: "m mod n mod n = (m mod n :: nat)"

   478   by (cases "n = 0") auto

   481 subsection{*The Divides Relation*}

   483 lemma dvdI [intro?]: "n = m * k ==> m dvd n"

   484   unfolding dvd_def by blast

   486 lemma dvdE [elim?]: "!!P. [|m dvd n;  !!k. n = m*k ==> P|] ==> P"

   487   unfolding dvd_def by blast

   489 lemma dvd_0_right [iff]: "m dvd (0::nat)"

   490   unfolding dvd_def by (blast intro: mult_0_right [symmetric])

   492 lemma dvd_0_left: "0 dvd m ==> m = (0::nat)"

   493   by (force simp add: dvd_def)

   495 lemma dvd_0_left_iff [iff]: "(0 dvd (m::nat)) = (m = 0)"

   496   by (blast intro: dvd_0_left)

   498 lemma dvd_1_left [iff]: "Suc 0 dvd k"

   499   unfolding dvd_def by simp

   501 lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)"

   502   by (simp add: dvd_def)

   504 lemma dvd_refl [simp]: "m dvd (m::nat)"

   505   unfolding dvd_def by (blast intro: mult_1_right [symmetric])

   507 lemma dvd_trans [trans]: "[| m dvd n; n dvd p |] ==> m dvd (p::nat)"

   508   unfolding dvd_def by (blast intro: mult_assoc)

   510 lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"

   511   unfolding dvd_def

   512   by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)

   514 lemma dvd_add: "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)"

   515   unfolding dvd_def

   516   by (blast intro: add_mult_distrib2 [symmetric])

   518 lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"

   519   unfolding dvd_def

   520   by (blast intro: diff_mult_distrib2 [symmetric])

   522 lemma dvd_diffD: "[| k dvd m-n; k dvd n; n\<le>m |] ==> k dvd (m::nat)"

   523   apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])

   524   apply (blast intro: dvd_add)

   525   done

   527 lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\<le>m |] ==> k dvd (n::nat)"

   528   by (drule_tac m = m in dvd_diff, auto)

   530 lemma dvd_mult: "k dvd n ==> k dvd (m*n :: nat)"

   531   unfolding dvd_def by (blast intro: mult_left_commute)

   533 lemma dvd_mult2: "k dvd m ==> k dvd (m*n :: nat)"

   534   apply (subst mult_commute)

   535   apply (erule dvd_mult)

   536   done

   538 lemma dvd_triv_right [iff]: "k dvd (m*k :: nat)"

   539   by (rule dvd_refl [THEN dvd_mult])

   541 lemma dvd_triv_left [iff]: "k dvd (k*m :: nat)"

   542   by (rule dvd_refl [THEN dvd_mult2])

   544 lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"

   545   apply (rule iffI)

   546    apply (erule_tac [2] dvd_add)

   547    apply (rule_tac [2] dvd_refl)

   548   apply (subgoal_tac "n = (n+k) -k")

   549    prefer 2 apply simp

   550   apply (erule ssubst)

   551   apply (erule dvd_diff)

   552   apply (rule dvd_refl)

   553   done

   555 lemma dvd_mod: "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n"

   556   unfolding dvd_def

   557   apply (case_tac "n = 0", auto)

   558   apply (blast intro: mod_mult_distrib2 [symmetric])

   559   done

   561 lemma dvd_mod_imp_dvd: "[| (k::nat) dvd m mod n;  k dvd n |] ==> k dvd m"

   562   apply (subgoal_tac "k dvd (m div n) *n + m mod n")

   563    apply (simp add: mod_div_equality)

   564   apply (simp only: dvd_add dvd_mult)

   565   done

   567 lemma dvd_mod_iff: "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)"

   568   by (blast intro: dvd_mod_imp_dvd dvd_mod)

   570 lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"

   571   unfolding dvd_def

   572   apply (erule exE)

   573   apply (simp add: mult_ac)

   574   done

   576 lemma dvd_mult_cancel1: "0<m ==> (m*n dvd m) = (n = (1::nat))"

   577   apply auto

   578    apply (subgoal_tac "m*n dvd m*1")

   579    apply (drule dvd_mult_cancel, auto)

   580   done

   582 lemma dvd_mult_cancel2: "0<m ==> (n*m dvd m) = (n = (1::nat))"

   583   apply (subst mult_commute)

   584   apply (erule dvd_mult_cancel1)

   585   done

   587 lemma mult_dvd_mono: "[| i dvd m; j dvd n|] ==> i*j dvd (m*n :: nat)"

   588   apply (unfold dvd_def, clarify)

   589   apply (rule_tac x = "k*ka" in exI)

   590   apply (simp add: mult_ac)

   591   done

   593 lemma dvd_mult_left: "(i*j :: nat) dvd k ==> i dvd k"

   594   by (simp add: dvd_def mult_assoc, blast)

   596 lemma dvd_mult_right: "(i*j :: nat) dvd k ==> j dvd k"

   597   apply (unfold dvd_def, clarify)

   598   apply (rule_tac x = "i*k" in exI)

   599   apply (simp add: mult_ac)

   600   done

   602 lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \<le> (n::nat)"

   603   apply (unfold dvd_def, clarify)

   604   apply (simp_all (no_asm_use) add: zero_less_mult_iff)

   605   apply (erule conjE)

   606   apply (rule le_trans)

   607    apply (rule_tac [2] le_refl [THEN mult_le_mono])

   608    apply (erule_tac [2] Suc_leI, simp)

   609   done

   611 lemma dvd_eq_mod_eq_0: "!!k::nat. (k dvd n) = (n mod k = 0)"

   612   apply (unfold dvd_def)

   613   apply (case_tac "k=0", simp, safe)

   614    apply (simp add: mult_commute)

   615   apply (rule_tac t = n and n1 = k in mod_div_equality [THEN subst])

   616   apply (subst mult_commute, simp)

   617   done

   619 lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"

   620   apply (subgoal_tac "m mod n = 0")

   621    apply (simp add: mult_div_cancel)

   622   apply (simp only: dvd_eq_mod_eq_0)

   623   done

   625 lemma le_imp_power_dvd: "!!i::nat. m \<le> n ==> i^m dvd i^n"

   626   apply (unfold dvd_def)

   627   apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])

   628   apply (simp add: power_add)

   629   done

   631 lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"

   632   by (induct n) auto

   634 lemma power_le_dvd [rule_format]: "k^j dvd n --> i\<le>j --> k^i dvd (n::nat)"

   635   apply (induct j)

   636    apply (simp_all add: le_Suc_eq)

   637   apply (blast dest!: dvd_mult_right)

   638   done

   640 lemma power_dvd_imp_le: "[|i^m dvd i^n;  (1::nat) < i|] ==> m \<le> n"

   641   apply (rule power_le_imp_le_exp, assumption)

   642   apply (erule dvd_imp_le, simp)

   643   done

   645 lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"

   646   by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)

   648 lemmas mod_eq_0D [dest!] = mod_eq_0_iff [THEN iffD1]

   650 (*Loses information, namely we also have r<d provided d is nonzero*)

   651 lemma mod_eqD: "(m mod d = r) ==> \<exists>q::nat. m = r + q*d"

   652   apply (cut_tac m = m in mod_div_equality)

   653   apply (simp only: add_ac)

   654   apply (blast intro: sym)

   655   done

   658 lemma split_div:

   659  "P(n div k :: nat) =

   660  ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"

   661  (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")

   662 proof

   663   assume P: ?P

   664   show ?Q

   665   proof (cases)

   666     assume "k = 0"

   667     with P show ?Q by(simp add:DIVISION_BY_ZERO_DIV)

   668   next

   669     assume not0: "k \<noteq> 0"

   670     thus ?Q

   671     proof (simp, intro allI impI)

   672       fix i j

   673       assume n: "n = k*i + j" and j: "j < k"

   674       show "P i"

   675       proof (cases)

   676         assume "i = 0"

   677         with n j P show "P i" by simp

   678       next

   679         assume "i \<noteq> 0"

   680         with not0 n j P show "P i" by(simp add:add_ac)

   681       qed

   682     qed

   683   qed

   684 next

   685   assume Q: ?Q

   686   show ?P

   687   proof (cases)

   688     assume "k = 0"

   689     with Q show ?P by(simp add:DIVISION_BY_ZERO_DIV)

   690   next

   691     assume not0: "k \<noteq> 0"

   692     with Q have R: ?R by simp

   693     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]

   694     show ?P by simp

   695   qed

   696 qed

   698 lemma split_div_lemma:

   699   "0 < n \<Longrightarrow> (n * q \<le> m \<and> m < n * (Suc q)) = (q = ((m::nat) div n))"

   700   apply (rule iffI)

   701   apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)

   702 prefer 3; apply assumption

   703   apply (simp_all add: quorem_def) apply arith

   704   apply (rule conjI)

   705   apply (rule_tac P="%x. n * (m div n) \<le> x" in

   706     subst [OF mod_div_equality [of _ n]])

   707   apply (simp only: add: mult_ac)

   708   apply (rule_tac P="%x. x < n + n * (m div n)" in

   709     subst [OF mod_div_equality [of _ n]])

   710   apply (simp only: add: mult_ac add_ac)

   711   apply (rule add_less_mono1, simp)

   712   done

   714 theorem split_div':

   715   "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>

   716    (\<exists>q. (n * q \<le> m \<and> m < n * (Suc q)) \<and> P q))"

   717   apply (case_tac "0 < n")

   718   apply (simp only: add: split_div_lemma)

   719   apply (simp_all add: DIVISION_BY_ZERO_DIV)

   720   done

   722 lemma split_mod:

   723  "P(n mod k :: nat) =

   724  ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"

   725  (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")

   726 proof

   727   assume P: ?P

   728   show ?Q

   729   proof (cases)

   730     assume "k = 0"

   731     with P show ?Q by(simp add:DIVISION_BY_ZERO_MOD)

   732   next

   733     assume not0: "k \<noteq> 0"

   734     thus ?Q

   735     proof (simp, intro allI impI)

   736       fix i j

   737       assume "n = k*i + j" "j < k"

   738       thus "P j" using not0 P by(simp add:add_ac mult_ac)

   739     qed

   740   qed

   741 next

   742   assume Q: ?Q

   743   show ?P

   744   proof (cases)

   745     assume "k = 0"

   746     with Q show ?P by(simp add:DIVISION_BY_ZERO_MOD)

   747   next

   748     assume not0: "k \<noteq> 0"

   749     with Q have R: ?R by simp

   750     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]

   751     show ?P by simp

   752   qed

   753 qed

   755 theorem mod_div_equality': "(m::nat) mod n = m - (m div n) * n"

   756   apply (rule_tac P="%x. m mod n = x - (m div n) * n" in

   757     subst [OF mod_div_equality [of _ n]])

   758   apply arith

   759   done

   761 lemma div_mod_equality':

   762   fixes m n :: nat

   763   shows "m div n * n = m - m mod n"

   764 proof -

   765   have "m mod n \<le> m mod n" ..

   766   from div_mod_equality have

   767     "m div n * n + m mod n - m mod n = m - m mod n" by simp

   768   with diff_add_assoc [OF `m mod n \<le> m mod n`, of "m div n * n"] have

   769     "m div n * n + (m mod n - m mod n) = m - m mod n"

   770     by simp

   771   then show ?thesis by simp

   772 qed

   775 subsection {*An ``induction'' law for modulus arithmetic.*}

   777 lemma mod_induct_0:

   778   assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"

   779   and base: "P i" and i: "i<p"

   780   shows "P 0"

   781 proof (rule ccontr)

   782   assume contra: "\<not>(P 0)"

   783   from i have p: "0<p" by simp

   784   have "\<forall>k. 0<k \<longrightarrow> \<not> P (p-k)" (is "\<forall>k. ?A k")

   785   proof

   786     fix k

   787     show "?A k"

   788     proof (induct k)

   789       show "?A 0" by simp  -- "by contradiction"

   790     next

   791       fix n

   792       assume ih: "?A n"

   793       show "?A (Suc n)"

   794       proof (clarsimp)

   795         assume y: "P (p - Suc n)"

   796         have n: "Suc n < p"

   797         proof (rule ccontr)

   798           assume "\<not>(Suc n < p)"

   799           hence "p - Suc n = 0"

   800             by simp

   801           with y contra show "False"

   802             by simp

   803         qed

   804         hence n2: "Suc (p - Suc n) = p-n" by arith

   805         from p have "p - Suc n < p" by arith

   806         with y step have z: "P ((Suc (p - Suc n)) mod p)"

   807           by blast

   808         show "False"

   809         proof (cases "n=0")

   810           case True

   811           with z n2 contra show ?thesis by simp

   812         next

   813           case False

   814           with p have "p-n < p" by arith

   815           with z n2 False ih show ?thesis by simp

   816         qed

   817       qed

   818     qed

   819   qed

   820   moreover

   821   from i obtain k where "0<k \<and> i+k=p"

   822     by (blast dest: less_imp_add_positive)

   823   hence "0<k \<and> i=p-k" by auto

   824   moreover

   825   note base

   826   ultimately

   827   show "False" by blast

   828 qed

   830 lemma mod_induct:

   831   assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"

   832   and base: "P i" and i: "i<p" and j: "j<p"

   833   shows "P j"

   834 proof -

   835   have "\<forall>j<p. P j"

   836   proof

   837     fix j

   838     show "j<p \<longrightarrow> P j" (is "?A j")

   839     proof (induct j)

   840       from step base i show "?A 0"

   841         by (auto elim: mod_induct_0)

   842     next

   843       fix k

   844       assume ih: "?A k"

   845       show "?A (Suc k)"

   846       proof

   847         assume suc: "Suc k < p"

   848         hence k: "k<p" by simp

   849         with ih have "P k" ..

   850         with step k have "P (Suc k mod p)"

   851           by blast

   852         moreover

   853         from suc have "Suc k mod p = Suc k"

   854           by simp

   855         ultimately

   856         show "P (Suc k)" by simp

   857       qed

   858     qed

   859   qed

   860   with j show ?thesis by blast

   861 qed

   864 lemma mod_add_left_eq: "((a::nat) + b) mod c = (a mod c + b) mod c"

   865   apply (rule trans [symmetric])

   866    apply (rule mod_add1_eq, simp)

   867   apply (rule mod_add1_eq [symmetric])

   868   done

   870 lemma mod_add_right_eq: "(a+b) mod (c::nat) = (a + (b mod c)) mod c"

   871   apply (rule trans [symmetric])

   872    apply (rule mod_add1_eq, simp)

   873   apply (rule mod_add1_eq [symmetric])

   874   done

   876 lemma mod_div_decomp:

   877   fixes n k :: nat

   878   obtains m q where "m = n div k" and "q = n mod k"

   879     and "n = m * k + q"

   880 proof -

   881   from mod_div_equality have "n = n div k * k + n mod k" by auto

   882   moreover have "n div k = n div k" ..

   883   moreover have "n mod k = n mod k" ..

   884   note that ultimately show thesis by blast

   885 qed

   888 subsection {* Code generation for div, mod and dvd on nat *}

   890 definition [code func del]:

   891   "divmod (m\<Colon>nat) n = (m div n, m mod n)"

   893 lemma divmod_zero [code]: "divmod m 0 = (0, m)"

   894   unfolding divmod_def by simp

   896 lemma divmod_succ [code]:

   897   "divmod m (Suc k) = (if m < Suc k then (0, m) else

   898     let

   899       (p, q) = divmod (m - Suc k) (Suc k)

   900     in (Suc p, q))"

   901   unfolding divmod_def Let_def split_def

   902   by (auto intro: div_geq mod_geq)

   904 lemma div_divmod [code]: "m div n = fst (divmod m n)"

   905   unfolding divmod_def by simp

   907 lemma mod_divmod [code]: "m mod n = snd (divmod m n)"

   908   unfolding divmod_def by simp

   910 definition

   911   dvd_nat :: "nat \<Rightarrow> nat \<Rightarrow> bool"

   912 where

   913   "dvd_nat m n \<longleftrightarrow> n mod m = (0 \<Colon> nat)"

   915 lemma [code inline]:

   916   "op dvd = dvd_nat"

   917   by (auto simp add: dvd_nat_def dvd_eq_mod_eq_0 expand_fun_eq)

   919 code_modulename SML

   920   Divides Nat

   922 code_modulename OCaml

   923   Divides Nat

   925 code_modulename Haskell

   926   Divides Nat

   928 hide (open) const divmod dvd_nat

   930 subsection {* Legacy bindings *}

   932 ML

   933 {*

   934 val div_def = thm "div_def"

   935 val mod_def = thm "mod_def"

   936 val dvd_def = thm "dvd_def"

   937 val quorem_def = thm "quorem_def"

   939 val wf_less_trans = thm "wf_less_trans";

   940 val mod_eq = thm "mod_eq";

   941 val div_eq = thm "div_eq";

   942 val DIVISION_BY_ZERO_DIV = thm "DIVISION_BY_ZERO_DIV";

   943 val DIVISION_BY_ZERO_MOD = thm "DIVISION_BY_ZERO_MOD";

   944 val mod_less = thm "mod_less";

   945 val mod_geq = thm "mod_geq";

   946 val le_mod_geq = thm "le_mod_geq";

   947 val mod_if = thm "mod_if";

   948 val mod_1 = thm "mod_1";

   949 val mod_self = thm "mod_self";

   950 val mod_add_self2 = thm "mod_add_self2";

   951 val mod_add_self1 = thm "mod_add_self1";

   952 val mod_mult_self1 = thm "mod_mult_self1";

   953 val mod_mult_self2 = thm "mod_mult_self2";

   954 val mod_mult_distrib = thm "mod_mult_distrib";

   955 val mod_mult_distrib2 = thm "mod_mult_distrib2";

   956 val mod_mult_self_is_0 = thm "mod_mult_self_is_0";

   957 val mod_mult_self1_is_0 = thm "mod_mult_self1_is_0";

   958 val div_less = thm "div_less";

   959 val div_geq = thm "div_geq";

   960 val le_div_geq = thm "le_div_geq";

   961 val div_if = thm "div_if";

   962 val mod_div_equality = thm "mod_div_equality";

   963 val mod_div_equality2 = thm "mod_div_equality2";

   964 val div_mod_equality = thm "div_mod_equality";

   965 val div_mod_equality2 = thm "div_mod_equality2";

   966 val mult_div_cancel = thm "mult_div_cancel";

   967 val mod_less_divisor = thm "mod_less_divisor";

   968 val div_mult_self_is_m = thm "div_mult_self_is_m";

   969 val div_mult_self1_is_m = thm "div_mult_self1_is_m";

   970 val unique_quotient_lemma = thm "unique_quotient_lemma";

   971 val unique_quotient = thm "unique_quotient";

   972 val unique_remainder = thm "unique_remainder";

   973 val div_0 = thm "div_0";

   974 val mod_0 = thm "mod_0";

   975 val div_mult1_eq = thm "div_mult1_eq";

   976 val mod_mult1_eq = thm "mod_mult1_eq";

   977 val mod_mult1_eq' = thm "mod_mult1_eq'";

   978 val mod_mult_distrib_mod = thm "mod_mult_distrib_mod";

   979 val div_add1_eq = thm "div_add1_eq";

   980 val mod_add1_eq = thm "mod_add1_eq";

   981 val mod_add_left_eq = thm "mod_add_left_eq";

   982  val mod_add_right_eq = thm "mod_add_right_eq";

   983 val mod_lemma = thm "mod_lemma";

   984 val div_mult2_eq = thm "div_mult2_eq";

   985 val mod_mult2_eq = thm "mod_mult2_eq";

   986 val div_mult_mult_lemma = thm "div_mult_mult_lemma";

   987 val div_mult_mult1 = thm "div_mult_mult1";

   988 val div_mult_mult2 = thm "div_mult_mult2";

   989 val div_1 = thm "div_1";

   990 val div_self = thm "div_self";

   991 val div_add_self2 = thm "div_add_self2";

   992 val div_add_self1 = thm "div_add_self1";

   993 val div_mult_self1 = thm "div_mult_self1";

   994 val div_mult_self2 = thm "div_mult_self2";

   995 val div_le_mono = thm "div_le_mono";

   996 val div_le_mono2 = thm "div_le_mono2";

   997 val div_le_dividend = thm "div_le_dividend";

   998 val div_less_dividend = thm "div_less_dividend";

   999 val mod_Suc = thm "mod_Suc";

  1000 val dvdI = thm "dvdI";

  1001 val dvdE = thm "dvdE";

  1002 val dvd_0_right = thm "dvd_0_right";

  1003 val dvd_0_left = thm "dvd_0_left";

  1004 val dvd_0_left_iff = thm "dvd_0_left_iff";

  1005 val dvd_1_left = thm "dvd_1_left";

  1006 val dvd_1_iff_1 = thm "dvd_1_iff_1";

  1007 val dvd_refl = thm "dvd_refl";

  1008 val dvd_trans = thm "dvd_trans";

  1009 val dvd_anti_sym = thm "dvd_anti_sym";

  1010 val dvd_add = thm "dvd_add";

  1011 val dvd_diff = thm "dvd_diff";

  1012 val dvd_diffD = thm "dvd_diffD";

  1013 val dvd_diffD1 = thm "dvd_diffD1";

  1014 val dvd_mult = thm "dvd_mult";

  1015 val dvd_mult2 = thm "dvd_mult2";

  1016 val dvd_reduce = thm "dvd_reduce";

  1017 val dvd_mod = thm "dvd_mod";

  1018 val dvd_mod_imp_dvd = thm "dvd_mod_imp_dvd";

  1019 val dvd_mod_iff = thm "dvd_mod_iff";

  1020 val dvd_mult_cancel = thm "dvd_mult_cancel";

  1021 val dvd_mult_cancel1 = thm "dvd_mult_cancel1";

  1022 val dvd_mult_cancel2 = thm "dvd_mult_cancel2";

  1023 val mult_dvd_mono = thm "mult_dvd_mono";

  1024 val dvd_mult_left = thm "dvd_mult_left";

  1025 val dvd_mult_right = thm "dvd_mult_right";

  1026 val dvd_imp_le = thm "dvd_imp_le";

  1027 val dvd_eq_mod_eq_0 = thm "dvd_eq_mod_eq_0";

  1028 val dvd_mult_div_cancel = thm "dvd_mult_div_cancel";

  1029 val mod_eq_0_iff = thm "mod_eq_0_iff";

  1030 val mod_eqD = thm "mod_eqD";

  1031 *}

  1033 (*

  1034 lemma split_div:

  1035 assumes m: "m \<noteq> 0"

  1036 shows "P(n div m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P i)"

  1037        (is "?P = ?Q")

  1038 proof

  1039   assume P: ?P

  1040   show ?Q

  1041   proof (intro allI impI)

  1042     fix i j

  1043     assume n: "n = m*i + j" and j: "j < m"

  1044     show "P i"

  1045     proof (cases)

  1046       assume "i = 0"

  1047       with n j P show "P i" by simp

  1048     next

  1049       assume "i \<noteq> 0"

  1050       with n j P show "P i" by (simp add:add_ac div_mult_self1)

  1051     qed

  1052   qed

  1053 next

  1054   assume Q: ?Q

  1055   from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]

  1056   show ?P by simp

  1057 qed

  1059 lemma split_mod:

  1060 assumes m: "m \<noteq> 0"

  1061 shows "P(n mod m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P j)"

  1062        (is "?P = ?Q")

  1063 proof

  1064   assume P: ?P

  1065   show ?Q

  1066   proof (intro allI impI)

  1067     fix i j

  1068     assume "n = m*i + j" "j < m"

  1069     thus "P j" using m P by(simp add:add_ac mult_ac)

  1070   qed

  1071 next

  1072   assume Q: ?Q

  1073   from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]

  1074   show ?P by simp

  1075 qed

  1076 *)

  1077 end

author	wenzelm
	Thu May 31 18:16:50 2007 +0200 (2007-05-31)
changeset 23162	b9853c187a1e
parent 23017	00c0e4c42396
child 23684	8c508c4dc53b
permissions	-rw-r--r--