--- a/src/HOL/Divides.thy Mon Apr 20 12:27:23 2009 +0200
+++ b/src/HOL/Divides.thy Mon Apr 20 16:28:13 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Divides.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1999 University of Cambridge
*)
@@ -20,11 +19,12 @@
subsection {* Abstract division in commutative semirings. *}
-class semiring_div = comm_semiring_1_cancel + div +
+class semiring_div = comm_semiring_1_cancel + no_zero_divisors + div +
assumes mod_div_equality: "a div b * b + a mod b = a"
and div_by_0 [simp]: "a div 0 = 0"
and div_0 [simp]: "0 div a = 0"
and div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
+ and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
begin
text {* @{const div} and @{const mod} *}
@@ -38,16 +38,16 @@
by (simp only: add_ac)
lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
-by (simp add: mod_div_equality)
+ by (simp add: mod_div_equality)
lemma div_mod_equality2: "(b * (a div b) + a mod b) + c = a + c"
-by (simp add: mod_div_equality2)
+ by (simp add: mod_div_equality2)
lemma mod_by_0 [simp]: "a mod 0 = a"
-using mod_div_equality [of a zero] by simp
+ using mod_div_equality [of a zero] by simp
lemma mod_0 [simp]: "0 mod a = 0"
-using mod_div_equality [of zero a] div_0 by simp
+ using mod_div_equality [of zero a] div_0 by simp
lemma div_mult_self2 [simp]:
assumes "b \<noteq> 0"
@@ -72,7 +72,7 @@
qed
lemma mod_mult_self2 [simp]: "(a + b * c) mod b = a mod b"
-by (simp add: mult_commute [of b])
+ by (simp add: mult_commute [of b])
lemma div_mult_self1_is_id [simp]: "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
using div_mult_self2 [of b 0 a] by simp
@@ -238,9 +238,9 @@
by (simp only: mod_add_eq [symmetric])
qed
-lemma div_add[simp]: "z dvd x \<Longrightarrow> z dvd y
+lemma div_add [simp]: "z dvd x \<Longrightarrow> z dvd y
\<Longrightarrow> (x + y) div z = x div z + y div z"
-by(cases "z=0", simp, unfold dvd_def, auto simp add: algebra_simps)
+by (cases "z = 0", simp, unfold dvd_def, auto simp add: algebra_simps)
text {* Multiplication respects modular equivalence. *}
@@ -297,21 +297,41 @@
finally show ?thesis .
qed
-end
-
-lemma div_mult_div_if_dvd: "(y::'a::{semiring_div,no_zero_divisors}) dvd x \<Longrightarrow>
- z dvd w \<Longrightarrow> (x div y) * (w div z) = (x * w) div (y * z)"
-unfolding dvd_def
- apply clarify
- apply (case_tac "y = 0")
- apply simp
- apply (case_tac "z = 0")
- apply simp
- apply (simp add: algebra_simps)
+lemma div_mult_div_if_dvd:
+ "y dvd x \<Longrightarrow> z dvd w \<Longrightarrow> (x div y) * (w div z) = (x * w) div (y * z)"
+ apply (cases "y = 0", simp)
+ apply (cases "z = 0", simp)
+ apply (auto elim!: dvdE simp add: algebra_simps)
apply (subst mult_assoc [symmetric])
apply (simp add: no_zero_divisors)
-done
+ done
+
+lemma div_mult_mult2 [simp]:
+ "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
+ by (drule div_mult_mult1) (simp add: mult_commute)
+
+lemma div_mult_mult1_if [simp]:
+ "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
+ by simp_all
+lemma mod_mult_mult1:
+ "(c * a) mod (c * b) = c * (a mod b)"
+proof (cases "c = 0")
+ case True then show ?thesis by simp
+next
+ case False
+ from mod_div_equality
+ have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
+ with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
+ = c * a + c * (a mod b)" by (simp add: algebra_simps)
+ with mod_div_equality show ?thesis by simp
+qed
+
+lemma mod_mult_mult2:
+ "(a * c) mod (b * c) = (a mod b) * c"
+ using mod_mult_mult1 [of c a b] by (simp add: mult_commute)
+
+end
lemma div_power: "(y::'a::{semiring_div,no_zero_divisors,recpower}) dvd x \<Longrightarrow>
(x div y)^n = x^n div y^n"
@@ -398,15 +418,17 @@
@{term "q\<Colon>nat"}(uotient) and @{term "r\<Colon>nat"}(emainder).
*}
-definition divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
- "divmod_rel m n q r \<longleftrightarrow> m = q * n + r \<and> (if n > 0 then 0 \<le> r \<and> r < n else q = 0)"
+definition divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where
+ "divmod_rel m n qr \<longleftrightarrow>
+ m = fst qr * n + snd qr \<and>
+ (if n = 0 then fst qr = 0 else if n > 0 then 0 \<le> snd qr \<and> snd qr < n else n < snd qr \<and> snd qr \<le> 0)"
text {* @{const divmod_rel} is total: *}
lemma divmod_rel_ex:
- obtains q r where "divmod_rel m n q r"
+ obtains q r where "divmod_rel m n (q, r)"
proof (cases "n = 0")
- case True with that show thesis
+ case True with that show thesis
by (auto simp add: divmod_rel_def)
next
case False
@@ -436,13 +458,14 @@
text {* @{const divmod_rel} is injective: *}
-lemma divmod_rel_unique_div:
- assumes "divmod_rel m n q r"
- and "divmod_rel m n q' r'"
- shows "q = q'"
+lemma divmod_rel_unique:
+ assumes "divmod_rel m n qr"
+ and "divmod_rel m n qr'"
+ shows "qr = qr'"
proof (cases "n = 0")
case True with assms show ?thesis
- by (simp add: divmod_rel_def)
+ by (cases qr, cases qr')
+ (simp add: divmod_rel_def)
next
case False
have aux: "\<And>q r q' r'. q' * n + r' = q * n + r \<Longrightarrow> r < n \<Longrightarrow> q' \<le> (q\<Colon>nat)"
@@ -450,18 +473,11 @@
apply (subst less_iff_Suc_add)
apply (auto simp add: add_mult_distrib)
done
- from `n \<noteq> 0` assms show ?thesis
- by (auto simp add: divmod_rel_def
- intro: order_antisym dest: aux sym)
-qed
-
-lemma divmod_rel_unique_mod:
- assumes "divmod_rel m n q r"
- and "divmod_rel m n q' r'"
- shows "r = r'"
-proof -
- from assms have "q = q'" by (rule divmod_rel_unique_div)
- with assms show ?thesis by (simp add: divmod_rel_def)
+ from `n \<noteq> 0` assms have "fst qr = fst qr'"
+ by (auto simp add: divmod_rel_def intro: order_antisym dest: aux sym)
+ moreover from this assms have "snd qr = snd qr'"
+ by (simp add: divmod_rel_def)
+ ultimately show ?thesis by (cases qr, cases qr') simp
qed
text {*
@@ -473,7 +489,21 @@
begin
definition divmod :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
- [code del]: "divmod m n = (THE (q, r). divmod_rel m n q r)"
+ [code del]: "divmod m n = (THE qr. divmod_rel m n qr)"
+
+lemma divmod_rel_divmod:
+ "divmod_rel m n (divmod m n)"
+proof -
+ from divmod_rel_ex
+ obtain qr where rel: "divmod_rel m n qr" .
+ then show ?thesis
+ by (auto simp add: divmod_def intro: theI elim: divmod_rel_unique)
+qed
+
+lemma divmod_eq:
+ assumes "divmod_rel m n qr"
+ shows "divmod m n = qr"
+ using assms by (auto intro: divmod_rel_unique divmod_rel_divmod)
definition div_nat where
"m div n = fst (divmod m n)"
@@ -485,30 +515,18 @@
"divmod m n = (m div n, m mod n)"
unfolding div_nat_def mod_nat_def by simp
-lemma divmod_eq:
- assumes "divmod_rel m n q r"
- shows "divmod m n = (q, r)"
- using assms by (auto simp add: divmod_def
- dest: divmod_rel_unique_div divmod_rel_unique_mod)
-
lemma div_eq:
- assumes "divmod_rel m n q r"
+ assumes "divmod_rel m n (q, r)"
shows "m div n = q"
- using assms by (auto dest: divmod_eq simp add: div_nat_def)
+ using assms by (auto dest: divmod_eq simp add: divmod_div_mod)
lemma mod_eq:
- assumes "divmod_rel m n q r"
+ assumes "divmod_rel m n (q, r)"
shows "m mod n = r"
- using assms by (auto dest: divmod_eq simp add: mod_nat_def)
+ using assms by (auto dest: divmod_eq simp add: divmod_div_mod)
-lemma divmod_rel: "divmod_rel m n (m div n) (m mod n)"
-proof -
- from divmod_rel_ex
- obtain q r where rel: "divmod_rel m n q r" .
- moreover with div_eq mod_eq have "m div n = q" and "m mod n = r"
- by simp_all
- ultimately show ?thesis by simp
-qed
+lemma divmod_rel: "divmod_rel m n (m div n, m mod n)"
+ by (simp add: div_nat_def mod_nat_def divmod_rel_divmod)
lemma divmod_zero:
"divmod m 0 = (0, m)"
@@ -531,10 +549,10 @@
assumes "0 < n" and "n \<le> m"
shows "divmod m n = (Suc ((m - n) div n), (m - n) mod n)"
proof -
- from divmod_rel have divmod_m_n: "divmod_rel m n (m div n) (m mod n)" .
+ from divmod_rel have divmod_m_n: "divmod_rel m n (m div n, m mod n)" .
with assms have m_div_n: "m div n \<ge> 1"
by (cases "m div n") (auto simp add: divmod_rel_def)
- from assms divmod_m_n have "divmod_rel (m - n) n (m div n - Suc 0) (m mod n)"
+ from assms divmod_m_n have "divmod_rel (m - n) n (m div n - Suc 0, m mod n)"
by (cases "m div n") (auto simp add: divmod_rel_def)
with divmod_eq have "divmod (m - n) n = (m div n - Suc 0, m mod n)" by simp
moreover from divmod_div_mod have "divmod (m - n) n = ((m - n) div n, (m - n) mod n)" .
@@ -569,55 +587,74 @@
shows "m mod n = (m - n) mod n"
using assms divmod_step divmod_div_mod by (cases "n = 0") simp_all
-instance proof
- fix m n :: nat show "m div n * n + m mod n = m"
- using divmod_rel [of m n] by (simp add: divmod_rel_def)
-next
- fix n :: nat show "n div 0 = 0"
- using divmod_zero divmod_div_mod [of n 0] by simp
-next
- fix n :: nat show "0 div n = 0"
- using divmod_rel [of 0 n] by (cases n) (simp_all add: divmod_rel_def)
-next
- fix m n q :: nat assume "n \<noteq> 0" then show "(q + m * n) div n = m + q div n"
- by (induct m) (simp_all add: le_div_geq)
+instance proof -
+ have [simp]: "\<And>n::nat. n div 0 = 0"
+ by (simp add: div_nat_def divmod_zero)
+ have [simp]: "\<And>n::nat. 0 div n = 0"
+ proof -
+ fix n :: nat
+ show "0 div n = 0"
+ by (cases "n = 0") simp_all
+ qed
+ show "OFCLASS(nat, semiring_div_class)" proof
+ fix m n :: nat
+ show "m div n * n + m mod n = m"
+ using divmod_rel [of m n] by (simp add: divmod_rel_def)
+ next
+ fix m n q :: nat
+ assume "n \<noteq> 0"
+ then show "(q + m * n) div n = m + q div n"
+ by (induct m) (simp_all add: le_div_geq)
+ next
+ fix m n q :: nat
+ assume "m \<noteq> 0"
+ then show "(m * n) div (m * q) = n div q"
+ proof (cases "n \<noteq> 0 \<and> q \<noteq> 0")
+ case False then show ?thesis by auto
+ next
+ case True with `m \<noteq> 0`
+ have "m > 0" and "n > 0" and "q > 0" by auto
+ then have "\<And>a b. divmod_rel n q (a, b) \<Longrightarrow> divmod_rel (m * n) (m * q) (a, m * b)"
+ by (auto simp add: divmod_rel_def) (simp_all add: algebra_simps)
+ moreover from divmod_rel have "divmod_rel n q (n div q, n mod q)" .
+ ultimately have "divmod_rel (m * n) (m * q) (n div q, m * (n mod q))" .
+ then show ?thesis by (simp add: div_eq)
+ qed
+ qed simp_all
qed
end
text {* Simproc for cancelling @{const div} and @{const mod} *}
-(*lemmas mod_div_equality_nat = semiring_div_class.times_div_mod_plus_zero_one.mod_div_equality [of "m\<Colon>nat" n, standard]
-lemmas mod_div_equality2_nat = mod_div_equality2 [of "n\<Colon>nat" m, standard*)
+ML {*
+local
+
+structure CancelDivMod = CancelDivModFun(struct
-ML {*
-structure CancelDivModData =
-struct
-
-val div_name = @{const_name div};
-val mod_name = @{const_name mod};
-val mk_binop = HOLogic.mk_binop;
-val mk_sum = Nat_Arith.mk_sum;
-val dest_sum = Nat_Arith.dest_sum;
+ val div_name = @{const_name div};
+ val mod_name = @{const_name mod};
+ val mk_binop = HOLogic.mk_binop;
+ val mk_sum = Nat_Arith.mk_sum;
+ val dest_sum = Nat_Arith.dest_sum;
-(*logic*)
+ val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
-val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}]
-
-val trans = trans
+ val trans = trans;
-val prove_eq_sums =
- let val simps = @{thm add_0} :: @{thm add_0_right} :: @{thms add_ac}
- in Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac simps) end;
+ val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
+ (@{thm monoid_add_class.add_0_left} :: @{thm monoid_add_class.add_0_right} :: @{thms add_ac}))
-end;
+end)
-structure CancelDivMod = CancelDivModFun(CancelDivModData);
+in
-val cancel_div_mod_proc = Simplifier.simproc (the_context ())
+val cancel_div_mod_nat_proc = Simplifier.simproc (the_context ())
"cancel_div_mod" ["(m::nat) + n"] (K CancelDivMod.proc);
-Addsimprocs[cancel_div_mod_proc];
+val _ = Addsimprocs [cancel_div_mod_nat_proc];
+
+end
*}
text {* code generator setup *}
@@ -658,7 +695,7 @@
fixes m n :: nat
assumes "n > 0"
shows "m mod n < (n::nat)"
- using assms divmod_rel unfolding divmod_rel_def by auto
+ using assms divmod_rel [of m n] unfolding divmod_rel_def by auto
lemma mod_less_eq_dividend [simp]:
fixes m n :: nat
@@ -700,18 +737,19 @@
subsubsection {* Quotient and Remainder *}
lemma divmod_rel_mult1_eq:
- "[| divmod_rel b c q r; c > 0 |]
- ==> divmod_rel (a*b) c (a*q + a*r div c) (a*r mod c)"
+ "divmod_rel b c (q, r) \<Longrightarrow> c > 0
+ \<Longrightarrow> divmod_rel (a * b) c (a * q + a * r div c, a * r mod c)"
by (auto simp add: split_ifs divmod_rel_def algebra_simps)
-lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"
+lemma div_mult1_eq:
+ "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"
apply (cases "c = 0", simp)
apply (blast intro: divmod_rel [THEN divmod_rel_mult1_eq, THEN div_eq])
done
lemma divmod_rel_add1_eq:
- "[| divmod_rel a c aq ar; divmod_rel b c bq br; c > 0 |]
- ==> divmod_rel (a + b) c (aq + bq + (ar+br) div c) ((ar + br) mod c)"
+ "divmod_rel a c (aq, ar) \<Longrightarrow> divmod_rel b c (bq, br) \<Longrightarrow> c > 0
+ \<Longrightarrow> divmod_rel (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
by (auto simp add: split_ifs divmod_rel_def algebra_simps)
(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
@@ -728,8 +766,9 @@
apply (simp add: add_mult_distrib2)
done
-lemma divmod_rel_mult2_eq: "[| divmod_rel a b q r; 0 < b; 0 < c |]
- ==> divmod_rel a (b*c) (q div c) (b*(q mod c) + r)"
+lemma divmod_rel_mult2_eq:
+ "divmod_rel a b (q, r) \<Longrightarrow> 0 < b \<Longrightarrow> 0 < c
+ \<Longrightarrow> divmod_rel a (b * c) (q div c, b *(q mod c) + r)"
by (auto simp add: mult_ac divmod_rel_def add_mult_distrib2 [symmetric] mod_lemma)
lemma div_mult2_eq: "a div (b*c) = (a div b) div (c::nat)"
@@ -745,23 +784,6 @@
done
-subsubsection{*Cancellation of Common Factors in Division*}
-
-lemma div_mult_mult_lemma:
- "[| (0::nat) < b; 0 < c |] ==> (c*a) div (c*b) = a div b"
-by (auto simp add: div_mult2_eq)
-
-lemma div_mult_mult1 [simp]: "(0::nat) < c ==> (c*a) div (c*b) = a div b"
- apply (cases "b = 0")
- apply (auto simp add: linorder_neq_iff [of b] div_mult_mult_lemma)
- done
-
-lemma div_mult_mult2 [simp]: "(0::nat) < c ==> (a*c) div (b*c) = a div b"
- apply (drule div_mult_mult1)
- apply (auto simp add: mult_commute)
- done
-
-
subsubsection{*Further Facts about Quotient and Remainder*}
lemma div_1 [simp]: "m div Suc 0 = m"
@@ -769,7 +791,7 @@
(* Monotonicity of div in first argument *)
-lemma div_le_mono [rule_format]:
+lemma div_le_mono [rule_format (no_asm)]:
"\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
apply (case_tac "k=0", simp)
apply (induct "n" rule: nat_less_induct, clarify)
@@ -824,12 +846,6 @@
apply (simp_all)
done
-lemma nat_div_eq_0 [simp]: "(n::nat) > 0 ==> ((m div n) = 0) = (m < n)"
-by(auto, subst mod_div_equality [of m n, symmetric], auto)
-
-lemma nat_div_gt_0 [simp]: "(n::nat) > 0 ==> ((m div n) > 0) = (m >= n)"
-by (subst neq0_conv [symmetric], auto)
-
declare div_less_dividend [simp]
text{*A fact for the mutilated chess board*}
@@ -915,16 +931,10 @@
done
lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \<le> (n::nat)"
-by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
-
-lemma nat_dvd_not_less: "(0::nat) < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
-by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
+ by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
- apply (subgoal_tac "m mod n = 0")
- apply (simp add: mult_div_cancel)
- apply (simp only: dvd_eq_mod_eq_0)
- done
+ by (simp add: dvd_eq_mod_eq_0 mult_div_cancel)
lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
by (induct n) auto
@@ -1001,9 +1011,11 @@
from A B show ?lhs ..
next
assume P: ?lhs
- then have "divmod_rel m n q (m - n * q)"
+ then have "divmod_rel m n (q, m - n * q)"
unfolding divmod_rel_def by (auto simp add: mult_ac)
- then show ?rhs using divmod_rel by (rule divmod_rel_unique_div)
+ with divmod_rel_unique divmod_rel [of m n]
+ have "(q, m - n * q) = (m div n, m mod n)" by auto
+ then show ?rhs by simp
qed
theorem split_div':
@@ -1155,4 +1167,9 @@
with j show ?thesis by blast
qed
+lemma nat_dvd_not_less:
+ fixes m n :: nat
+ shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
+by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
+
end