--- a/src/HOL/Divides.thy Fri Jul 18 17:09:48 2008 +0200
+++ b/src/HOL/Divides.thy Fri Jul 18 18:25:53 2008 +0200
@@ -4,7 +4,7 @@
Copyright 1999 University of Cambridge
*)
-header {* The division operators div, mod and the divides relation dvd *}
+header {* The division operators div and mod *}
theory Divides
imports Nat Power Product_Type
@@ -13,71 +13,22 @@
subsection {* Syntactic division operations *}
-class dvd = times
-begin
-
-definition
- dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50)
-where
- [code func del]: "m dvd n \<longleftrightarrow> (\<exists>k. n = m * k)"
-
-end
-
-class div = times +
+class div = dvd +
fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
- fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
+ and mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
-subsection {* Abstract divisibility in commutative semirings. *}
+subsection {* Abstract division in commutative semirings. *}
-class semiring_div = comm_semiring_1_cancel + dvd + div +
+class semiring_div = comm_semiring_1_cancel + div +
assumes mod_div_equality: "a div b * b + a mod b = a"
- and div_by_0: "a div 0 = 0"
- and mult_div: "b \<noteq> 0 \<Longrightarrow> a * b div 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"
begin
text {* @{const div} and @{const mod} *}
-lemma div_by_1: "a div 1 = a"
- using mult_div [of 1 a] zero_neq_one by simp
-
-lemma mod_by_1: "a mod 1 = 0"
-proof -
- from mod_div_equality [of a one] div_by_1 have "a + a mod 1 = a" by simp
- then have "a + a mod 1 = a + 0" by simp
- then show ?thesis by (rule add_left_imp_eq)
-qed
-
-lemma mod_by_0: "a mod 0 = a"
- using mod_div_equality [of a zero] by simp
-
-lemma mult_mod: "a * b mod b = 0"
-proof (cases "b = 0")
- case True then show ?thesis by (simp add: mod_by_0)
-next
- case False with mult_div have abb: "a * b div b = a" .
- from mod_div_equality have "a * b div b * b + a * b mod b = a * b" .
- with abb have "a * b + a * b mod b = a * b + 0" by simp
- then show ?thesis by (rule add_left_imp_eq)
-qed
-
-lemma mod_self: "a mod a = 0"
- using mult_mod [of one] by simp
-
-lemma div_self: "a \<noteq> 0 \<Longrightarrow> a div a = 1"
- using mult_div [of _ one] by simp
-
-lemma div_0: "0 div a = 0"
-proof (cases "a = 0")
- case True then show ?thesis by (simp add: div_by_0)
-next
- case False with mult_div have "0 * a div a = 0" .
- then show ?thesis by simp
-qed
-
-lemma mod_0: "0 mod a = 0"
- using mod_div_equality [of zero a] div_0 by simp
-
lemma mod_div_equality2: "b * (a div b) + a mod b = a"
unfolding mult_commute [of b]
by (rule mod_div_equality)
@@ -88,15 +39,95 @@
lemma div_mod_equality2: "(b * (a div b) + a mod b) + c = a + c"
by (simp add: mod_div_equality2)
-text {* The @{const dvd} relation *}
+lemma mod_by_0 [simp]: "a mod 0 = a"
+ 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
+
+lemma div_mult_self2 [simp]:
+ assumes "b \<noteq> 0"
+ shows "(a + b * c) div b = c + a div b"
+ using assms div_mult_self1 [of b a c] by (simp add: mult_commute)
-lemma dvdI [intro?]: "a = b * c \<Longrightarrow> b dvd a"
- unfolding dvd_def ..
+lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
+proof (cases "b = 0")
+ case True then show ?thesis by simp
+next
+ case False
+ have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
+ by (simp add: mod_div_equality)
+ also from False div_mult_self1 [of b a c] have
+ "\<dots> = (c + a div b) * b + (a + c * b) mod b"
+ by (simp add: left_distrib add_ac)
+ finally have "a = a div b * b + (a + c * b) mod b"
+ by (simp add: add_commute [of a] add_assoc left_distrib)
+ then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
+ by (simp add: mod_div_equality)
+ then show ?thesis by simp
+qed
+
+lemma mod_mult_self2 [simp]: "(a + b * c) mod b = a mod 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
+
+lemma div_mult_self2_is_id [simp]: "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
+ using div_mult_self1 [of b 0 a] by simp
+
+lemma mod_mult_self1_is_0 [simp]: "b * a mod b = 0"
+ using mod_mult_self2 [of 0 b a] by simp
+
+lemma mod_mult_self2_is_0 [simp]: "a * b mod b = 0"
+ using mod_mult_self1 [of 0 a b] by simp
-lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>c. a = b * c \<Longrightarrow> P) \<Longrightarrow> P"
- unfolding dvd_def by blast
+lemma div_by_1 [simp]: "a div 1 = a"
+ using div_mult_self2_is_id [of 1 a] zero_neq_one by simp
+
+lemma mod_by_1 [simp]: "a mod 1 = 0"
+proof -
+ from mod_div_equality [of a one] div_by_1 have "a + a mod 1 = a" by simp
+ then have "a + a mod 1 = a + 0" by simp
+ then show ?thesis by (rule add_left_imp_eq)
+qed
+
+lemma mod_self [simp]: "a mod a = 0"
+ using mod_mult_self2_is_0 [of 1] by simp
+
+lemma div_self [simp]: "a \<noteq> 0 \<Longrightarrow> a div a = 1"
+ using div_mult_self2_is_id [of _ 1] by simp
+
+lemma div_add_self1:
+ assumes "b \<noteq> 0"
+ shows "(b + a) div b = a div b + 1"
+ using assms div_mult_self1 [of b a 1] by (simp add: add_commute)
-lemma dvd_def_mod [code func]: "a dvd b \<longleftrightarrow> b mod a = 0"
+lemma div_add_self2:
+ assumes "b \<noteq> 0"
+ shows "(a + b) div b = a div b + 1"
+ using assms div_add_self1 [of b a] by (simp add: add_commute)
+
+lemma mod_add_self1:
+ "(b + a) mod b = a mod b"
+ using mod_mult_self1 [of a 1 b] by (simp add: add_commute)
+
+lemma mod_add_self2:
+ "(a + b) mod b = a mod b"
+ using mod_mult_self1 [of a 1 b] by simp
+
+lemma mod_div_decomp:
+ fixes a b
+ obtains q r where "q = a div b" and "r = a mod b"
+ and "a = q * b + r"
+proof -
+ from mod_div_equality have "a = a div b * b + a mod b" by simp
+ moreover have "a div b = a div b" ..
+ moreover have "a mod b = a mod b" ..
+ note that ultimately show thesis by blast
+qed
+
+lemma dvd_eq_mod_eq_0 [code func]: "a dvd b \<longleftrightarrow> b mod a = 0"
proof
assume "b mod a = 0"
with mod_div_equality [of b a] have "b div a * a = b" by simp
@@ -109,59 +140,9 @@
then obtain c where "b = a * c" ..
then have "b mod a = a * c mod a" by simp
then have "b mod a = c * a mod a" by (simp add: mult_commute)
- then show "b mod a = 0" by (simp add: mult_mod)
-qed
-
-lemma dvd_refl: "a dvd a"
- unfolding dvd_def_mod mod_self ..
-
-lemma dvd_trans:
- assumes "a dvd b" and "b dvd c"
- shows "a dvd c"
-proof -
- from assms obtain v where "b = a * v" unfolding dvd_def by auto
- moreover from assms obtain w where "c = b * w" unfolding dvd_def by auto
- ultimately have "c = a * (v * w)" by (simp add: mult_assoc)
- then show ?thesis unfolding dvd_def ..
-qed
-
-lemma zero_dvd_iff [noatp]: "0 dvd a \<longleftrightarrow> a = 0"
- unfolding dvd_def by simp
-
-lemma dvd_0: "a dvd 0"
-unfolding dvd_def proof
- show "0 = a * 0" by simp
+ then show "b mod a = 0" by simp
qed
-lemma one_dvd: "1 dvd a"
- unfolding dvd_def by simp
-
-lemma dvd_mult: "a dvd c \<Longrightarrow> a dvd (b * c)"
- unfolding dvd_def by (blast intro: mult_left_commute)
-
-lemma dvd_mult2: "a dvd b \<Longrightarrow> a dvd (b * c)"
- apply (subst mult_commute)
- apply (erule dvd_mult)
- done
-
-lemma dvd_triv_right: "a dvd b * a"
- by (rule dvd_mult) (rule dvd_refl)
-
-lemma dvd_triv_left: "a dvd a * b"
- by (rule dvd_mult2) (rule dvd_refl)
-
-lemma mult_dvd_mono: "a dvd c \<Longrightarrow> b dvd d \<Longrightarrow> a * b dvd c * d"
- apply (unfold dvd_def, clarify)
- apply (rule_tac x = "k * ka" in exI)
- apply (simp add: mult_ac)
- done
-
-lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c"
- by (simp add: dvd_def mult_assoc, blast)
-
-lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c"
- unfolding mult_ac [of a] by (rule dvd_mult_left)
-
end
@@ -352,7 +333,10 @@
fix n :: nat show "n div 0 = 0"
using divmod_zero divmod_div_mod [of n 0] by simp
next
- fix m n :: nat assume "n \<noteq> 0" then show "m * n div n = m"
+ 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)
qed
@@ -360,10 +344,8 @@
text {* Simproc for cancelling @{const div} and @{const mod} *}
-lemmas mod_div_equality = semiring_div_class.times_div_mod_plus_zero_one.mod_div_equality [of "m\<Colon>nat" n, standard]
-lemmas mod_div_equality2 = mod_div_equality2 [of "n\<Colon>nat" m, standard]
-lemmas div_mod_equality = div_mod_equality [of "m\<Colon>nat" n k, standard]
-lemmas div_mod_equality2 = div_mod_equality2 [of "m\<Colon>nat" n k, standard]
+(*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 {*
structure CancelDivModData =
@@ -414,9 +396,6 @@
subsubsection {* Quotient *}
-lemmas DIVISION_BY_ZERO_DIV [simp] = div_by_0 [of "a\<Colon>nat", standard]
-lemmas div_0 [simp] = semiring_div_class.div_0 [of "n\<Colon>nat", standard]
-
lemma div_geq: "0 < n \<Longrightarrow> \<not> m < n \<Longrightarrow> m div n = Suc ((m - n) div n)"
by (simp add: le_div_geq linorder_not_less)
@@ -424,17 +403,14 @@
by (simp add: div_geq)
lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
- by (rule mult_div) simp
+ by simp
lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
- by (simp add: mult_commute)
+ by simp
subsubsection {* Remainder *}
-lemmas DIVISION_BY_ZERO_MOD [simp] = mod_by_0 [of "a\<Colon>nat", standard]
-lemmas mod_0 [simp] = semiring_div_class.mod_0 [of "n\<Colon>nat", standard]
-
lemma mod_less_divisor [simp]:
fixes m n :: nat
assumes "n > 0"
@@ -458,23 +434,6 @@
lemma mod_1 [simp]: "m mod Suc 0 = 0"
by (induct m) (simp_all add: mod_geq)
-lemmas mod_self [simp] = semiring_div_class.mod_self [of "n\<Colon>nat", standard]
-
-lemma mod_add_self2 [simp]: "(m+n) mod n = m mod (n::nat)"
- apply (subgoal_tac "(n + m) mod n = (n+m-n) mod n")
- apply (simp add: add_commute)
- apply (subst le_mod_geq [symmetric], simp_all)
- done
-
-lemma mod_add_self1 [simp]: "(n+m) mod n = m mod (n::nat)"
- by (simp add: add_commute mod_add_self2)
-
-lemma mod_mult_self1 [simp]: "(m + k*n) mod n = m mod (n::nat)"
- by (induct k) (simp_all add: add_left_commute [of _ n])
-
-lemma mod_mult_self2 [simp]: "(m + n*k) mod n = m mod (n::nat)"
- by (simp add: mult_commute mod_mult_self1)
-
lemma mod_mult_distrib: "(m mod n) * (k\<Colon>nat) = (m * k) mod (n * k)"
apply (cases "n = 0", simp)
apply (cases "k = 0", simp)
@@ -486,20 +445,9 @@
lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)"
by (simp add: mult_commute [of k] mod_mult_distrib)
-lemma mod_mult_self_is_0 [simp]: "(m*n) mod n = (0::nat)"
- apply (cases "n = 0", simp)
- apply (induct m, simp)
- apply (rename_tac k)
- apply (cut_tac m = "k * n" and n = n in mod_add_self2)
- apply (simp add: add_commute)
- done
-
-lemma mod_mult_self1_is_0 [simp]: "(n*m) mod n = (0::nat)"
- by (simp add: mult_commute mod_mult_self_is_0)
-
(* a simple rearrangement of mod_div_equality: *)
lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
- by (cut_tac m = m and n = n in mod_div_equality2, arith)
+ by (cut_tac a = m and b = n in mod_div_equality2, arith)
lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
apply (drule mod_less_divisor [where m = m])
@@ -508,17 +456,6 @@
subsubsection {* Quotient and Remainder *}
-lemma mod_div_decomp:
- fixes n k :: nat
- obtains m q where "m = n div k" and "q = n mod k"
- and "n = m * k + q"
-proof -
- from mod_div_equality have "n = n div k * k + n mod k" by auto
- moreover have "n div k = n div k" ..
- moreover have "n mod k = n mod k" ..
- note that ultimately show thesis by blast
-qed
-
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)"
@@ -610,25 +547,6 @@
lemma div_1 [simp]: "m div Suc 0 = m"
by (induct m) (simp_all add: div_geq)
-lemmas div_self [simp] = semiring_div_class.div_self [of "n\<Colon>nat", standard]
-
-lemma div_add_self2: "0<n ==> (m+n) div n = Suc (m div n)"
- apply (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n) ")
- apply (simp add: add_commute)
- apply (subst div_geq [symmetric], simp_all)
- done
-
-lemma div_add_self1: "0<n ==> (n+m) div n = Suc (m div n)"
- by (simp add: add_commute div_add_self2)
-
-lemma div_mult_self1 [simp]: "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n"
- apply (subst div_add1_eq)
- apply (subst div_mult1_eq, simp)
- done
-
-lemma div_mult_self2 [simp]: "0<n ==> (m + n*k) div n = k + m div (n::nat)"
- by (simp add: mult_commute div_mult_self1)
-
(* Monotonicity of div in first argument *)
lemma div_le_mono [rule_format (no_asm)]:
@@ -707,24 +625,7 @@
by (cases "n = 0") auto
-subsubsection{*The Divides Relation*}
-
-lemma dvdI [intro?]: "n = m * k ==> m dvd n"
- unfolding dvd_def by blast
-
-lemma dvdE [elim?]: "!!P. [|m dvd n; !!k. n = m*k ==> P|] ==> P"
- unfolding dvd_def by blast
-
-lemma dvd_0_right [iff]: "m dvd (0::nat)"
- unfolding dvd_def by (blast intro: mult_0_right [symmetric])
-
-lemma dvd_0_left: "0 dvd m ==> m = (0::nat)"
- by (force simp add: dvd_def)
-
-lemma dvd_0_left_iff [iff]: "(0 dvd (m::nat)) = (m = 0)"
- by (blast intro: dvd_0_left)
-
-declare dvd_0_left_iff [noatp]
+subsubsection {* The Divides Relation *}
lemma dvd_1_left [iff]: "Suc 0 dvd k"
unfolding dvd_def by simp
@@ -732,9 +633,6 @@
lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)"
by (simp add: dvd_def)
-lemmas dvd_refl [simp] = semiring_div_class.dvd_refl [of "m\<Colon>nat", standard]
-lemmas dvd_trans [trans] = semiring_div_class.dvd_trans [of "m\<Colon>nat" n p, standard]
-
lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
unfolding dvd_def
by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
@@ -742,11 +640,7 @@
text {* @{term "op dvd"} is a partial order *}
interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> n \<noteq> m"]
- by unfold_locales (auto intro: dvd_trans dvd_anti_sym)
-
-lemma dvd_add: "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)"
- unfolding dvd_def
- by (blast intro: add_mult_distrib2 [symmetric])
+ by unfold_locales (auto intro: dvd_refl dvd_trans dvd_anti_sym)
lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
unfolding dvd_def
@@ -760,20 +654,6 @@
lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\<le>m |] ==> k dvd (n::nat)"
by (drule_tac m = m in dvd_diff, auto)
-lemma dvd_mult: "k dvd n ==> k dvd (m*n :: nat)"
- unfolding dvd_def by (blast intro: mult_left_commute)
-
-lemma dvd_mult2: "k dvd m ==> k dvd (m*n :: nat)"
- apply (subst mult_commute)
- apply (erule dvd_mult)
- done
-
-lemma dvd_triv_right [iff]: "k dvd (m*k :: nat)"
- by (rule dvd_refl [THEN dvd_mult])
-
-lemma dvd_triv_left [iff]: "k dvd (k*m :: nat)"
- by (rule dvd_refl [THEN dvd_mult2])
-
lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"
apply (rule iffI)
apply (erule_tac [2] dvd_add)
@@ -817,21 +697,6 @@
apply (erule dvd_mult_cancel1)
done
-lemma mult_dvd_mono: "[| i dvd m; j dvd n|] ==> i*j dvd (m*n :: nat)"
- apply (unfold dvd_def, clarify)
- apply (rule_tac x = "k*ka" in exI)
- apply (simp add: mult_ac)
- done
-
-lemma dvd_mult_left: "(i*j :: nat) dvd k ==> i dvd k"
- by (simp add: dvd_def mult_assoc, blast)
-
-lemma dvd_mult_right: "(i*j :: nat) dvd k ==> j dvd k"
- apply (unfold dvd_def, clarify)
- apply (rule_tac x = "i*k" in exI)
- apply (simp add: mult_ac)
- done
-
lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \<le> (n::nat)"
apply (unfold dvd_def, clarify)
apply (simp_all (no_asm_use) add: zero_less_mult_iff)
@@ -841,8 +706,6 @@
apply (erule_tac [2] Suc_leI, simp)
done
-lemmas dvd_eq_mod_eq_0 = dvd_def_mod [of "k\<Colon>nat" n, standard]
-
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)
@@ -888,7 +751,7 @@
(*Loses information, namely we also have r<d provided d is nonzero*)
lemma mod_eqD: "(m mod d = r) ==> \<exists>q::nat. m = r + q*d"
- apply (cut_tac m = m in mod_div_equality)
+ apply (cut_tac a = m in mod_div_equality)
apply (simp only: add_ac)
apply (blast intro: sym)
done
@@ -902,7 +765,7 @@
show ?Q
proof (cases)
assume "k = 0"
- with P show ?Q by(simp add:DIVISION_BY_ZERO_DIV)
+ with P show ?Q by simp
next
assume not0: "k \<noteq> 0"
thus ?Q
@@ -924,7 +787,7 @@
show ?P
proof (cases)
assume "k = 0"
- with Q show ?P by(simp add:DIVISION_BY_ZERO_DIV)
+ with Q show ?P by simp
next
assume not0: "k \<noteq> 0"
with Q have R: ?R by simp
@@ -958,7 +821,7 @@
(\<exists>q. (n * q \<le> m \<and> m < n * (Suc q)) \<and> P q))"
apply (case_tac "0 < n")
apply (simp only: add: split_div_lemma)
- apply (simp_all add: DIVISION_BY_ZERO_DIV)
+ apply simp_all
done
lemma split_mod:
@@ -970,7 +833,7 @@
show ?Q
proof (cases)
assume "k = 0"
- with P show ?Q by(simp add:DIVISION_BY_ZERO_MOD)
+ with P show ?Q by simp
next
assume not0: "k \<noteq> 0"
thus ?Q
@@ -985,7 +848,7 @@
show ?P
proof (cases)
assume "k = 0"
- with Q show ?P by(simp add:DIVISION_BY_ZERO_MOD)
+ with Q show ?P by simp
next
assume not0: "k \<noteq> 0"
with Q have R: ?R by simp