--- a/src/HOL/Divides.thy Mon Feb 20 12:37:17 2012 +0100
+++ b/src/HOL/Divides.thy Mon Feb 20 14:23:46 2012 +0100
@@ -523,9 +523,6 @@
means of @{const divmod_nat_rel}:
*}
-instantiation nat :: semiring_div
-begin
-
definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
"divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
@@ -543,28 +540,39 @@
shows "divmod_nat m n = qr"
using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
+instantiation nat :: semiring_div
+begin
+
definition div_nat where
"m div n = fst (divmod_nat m n)"
+lemma fst_divmod_nat [simp]:
+ "fst (divmod_nat m n) = m div n"
+ by (simp add: div_nat_def)
+
definition mod_nat where
"m mod n = snd (divmod_nat m n)"
+lemma snd_divmod_nat [simp]:
+ "snd (divmod_nat m n) = m mod n"
+ by (simp add: mod_nat_def)
+
lemma divmod_nat_div_mod:
"divmod_nat m n = (m div n, m mod n)"
- unfolding div_nat_def mod_nat_def by simp
+ by (simp add: prod_eq_iff)
lemma div_eq:
assumes "divmod_nat_rel m n (q, r)"
shows "m div n = q"
- using assms by (auto dest: divmod_nat_eq simp add: divmod_nat_div_mod)
+ using assms by (auto dest!: divmod_nat_eq simp add: prod_eq_iff)
lemma mod_eq:
assumes "divmod_nat_rel m n (q, r)"
shows "m mod n = r"
- using assms by (auto dest: divmod_nat_eq simp add: divmod_nat_div_mod)
+ using assms by (auto dest!: divmod_nat_eq simp add: prod_eq_iff)
lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
- by (simp add: div_nat_def mod_nat_def divmod_nat_rel_divmod_nat)
+ using divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod)
lemma divmod_nat_zero:
"divmod_nat m 0 = (0, m)"
@@ -613,25 +621,25 @@
fixes m n :: nat
assumes "m < n"
shows "m div n = 0"
- using assms divmod_nat_base divmod_nat_div_mod by simp
+ using assms divmod_nat_base by (simp add: prod_eq_iff)
lemma le_div_geq:
fixes m n :: nat
assumes "0 < n" and "n \<le> m"
shows "m div n = Suc ((m - n) div n)"
- using assms divmod_nat_step divmod_nat_div_mod by simp
+ using assms divmod_nat_step by (simp add: prod_eq_iff)
lemma mod_less [simp]:
fixes m n :: nat
assumes "m < n"
shows "m mod n = m"
- using assms divmod_nat_base divmod_nat_div_mod by simp
+ using assms divmod_nat_base by (simp add: prod_eq_iff)
lemma le_mod_geq:
fixes m n :: nat
assumes "n \<le> m"
shows "m mod n = (m - n) mod n"
- using assms divmod_nat_step divmod_nat_div_mod by (cases "n = 0") simp_all
+ using assms divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
instance proof -
have [simp]: "\<And>n::nat. n div 0 = 0"
@@ -673,8 +681,7 @@
lemma divmod_nat_if [code]: "divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
let (q, r) = divmod_nat (m - n) n in (Suc q, r))"
-by (simp add: divmod_nat_zero divmod_nat_base divmod_nat_step)
- (simp add: divmod_nat_div_mod)
+ by (simp add: prod_eq_iff prod_case_beta not_less le_div_geq le_mod_geq)
text {* Simproc for cancelling @{const div} and @{const mod} *}
@@ -807,12 +814,11 @@
done
-subsubsection{*Further Facts about Quotient and Remainder*}
+subsubsection {* Further Facts about Quotient and Remainder *}
lemma div_1 [simp]: "m div Suc 0 = m"
by (induct m) (simp_all add: div_geq)
-
(* Monotonicity of div in first argument *)
lemma div_le_mono [rule_format (no_asm)]:
"\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
@@ -1018,7 +1024,7 @@
qed
-subsubsection {*An ``induction'' law for modulus arithmetic.*}
+subsubsection {* An ``induction'' law for modulus arithmetic. *}
lemma mod_induct_0:
assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
@@ -1228,19 +1234,27 @@
instantiation int :: Divides.div
begin
-definition
+definition div_int where
"a div b = fst (divmod_int a b)"
-definition
+lemma fst_divmod_int [simp]:
+ "fst (divmod_int a b) = a div b"
+ by (simp add: div_int_def)
+
+definition mod_int where
"a mod b = snd (divmod_int a b)"
+lemma snd_divmod_int [simp]:
+ "snd (divmod_int a b) = a mod b"
+ by (simp add: mod_int_def)
+
instance ..
end
lemma divmod_int_mod_div:
"divmod_int p q = (p div q, p mod q)"
- by (auto simp add: div_int_def mod_int_def)
+ by (simp add: prod_eq_iff)
text{*
Here is the division algorithm in ML:
@@ -1271,8 +1285,7 @@
*}
-
-subsubsection{*Uniqueness and Monotonicity of Quotients and Remainders*}
+subsubsection {* Uniqueness and Monotonicity of Quotients and Remainders *}
lemma unique_quotient_lemma:
"[| b*q' + r' \<le> b*q + r; 0 \<le> r'; r' < b; r < b |]
@@ -1312,7 +1325,7 @@
done
-subsubsection{*Correctness of @{term posDivAlg}, the Algorithm for Non-Negative Dividends*}
+subsubsection {* Correctness of @{term posDivAlg}, the Algorithm for Non-Negative Dividends *}
text{*And positive divisors*}
@@ -1347,7 +1360,7 @@
done
-subsubsection{*Correctness of @{term negDivAlg}, the Algorithm for Negative Dividends*}
+subsubsection {* Correctness of @{term negDivAlg}, the Algorithm for Negative Dividends *}
text{*And positive divisors*}
@@ -1377,7 +1390,7 @@
done
-subsubsection{*Existence Shown by Proving the Division Algorithm to be Correct*}
+subsubsection {* Existence Shown by Proving the Division Algorithm to be Correct *}
(*the case a=0*)
lemma divmod_int_rel_0: "b \<noteq> 0 ==> divmod_int_rel 0 b (0, 0)"
@@ -1411,7 +1424,7 @@
lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
apply (case_tac "b = 0", simp)
apply (cut_tac a = a and b = b in divmod_int_correct)
-apply (auto simp add: divmod_int_rel_def div_int_def mod_int_def)
+apply (auto simp add: divmod_int_rel_def prod_eq_iff)
done
lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k"
@@ -1442,7 +1455,7 @@
lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b"
apply (cut_tac a = a and b = b in divmod_int_correct)
-apply (auto simp add: divmod_int_rel_def mod_int_def)
+apply (auto simp add: divmod_int_rel_def prod_eq_iff)
done
lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
@@ -1450,14 +1463,14 @@
lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b"
apply (cut_tac a = a and b = b in divmod_int_correct)
-apply (auto simp add: divmod_int_rel_def div_int_def mod_int_def)
+apply (auto simp add: divmod_int_rel_def prod_eq_iff)
done
lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
-subsubsection{*General Properties of div and mod*}
+subsubsection {* General Properties of div and mod *}
lemma divmod_int_rel_div_mod: "b \<noteq> 0 ==> divmod_int_rel a b (a div b, a mod b)"
apply (cut_tac a = a and b = b in zmod_zdiv_equality)
@@ -1521,7 +1534,7 @@
done
-subsubsection{*Laws for div and mod with Unary Minus*}
+subsubsection {* Laws for div and mod with Unary Minus *}
lemma zminus1_lemma:
"divmod_int_rel a b (q, r)
@@ -1569,7 +1582,7 @@
unfolding zmod_zminus2_eq_if by auto
-subsubsection{*Division of a Number by Itself*}
+subsubsection {* Division of a Number by Itself *}
lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 \<le> q"
apply (subgoal_tac "0 < a*q")
@@ -1605,7 +1618,7 @@
done
-subsubsection{*Computation of Division and Remainder*}
+subsubsection {* Computation of Division and Remainder *}
lemma zdiv_zero [simp]: "(0::int) div b = 0"
by (simp add: div_int_def divmod_int_def)
@@ -1748,7 +1761,7 @@
lemmas negDivAlg_eqn_1_number_of [simp] = negDivAlg_eqn [of concl: 1 "number_of w"] for w
-subsubsection{*Monotonicity in the First Argument (Dividend)*}
+subsubsection {* Monotonicity in the First Argument (Dividend) *}
lemma zdiv_mono1: "[| a \<le> a'; 0 < (b::int) |] ==> a div b \<le> a' div b"
apply (cut_tac a = a and b = b in zmod_zdiv_equality)
@@ -1767,7 +1780,7 @@
done
-subsubsection{*Monotonicity in the Second Argument (Divisor)*}
+subsubsection {* Monotonicity in the Second Argument (Divisor) *}
lemma q_pos_lemma:
"[| 0 \<le> b'*q' + r'; r' < b'; 0 < b' |] ==> 0 \<le> (q'::int)"
@@ -1829,7 +1842,7 @@
done
-subsubsection{*More Algebraic Laws for div and mod*}
+subsubsection {* More Algebraic Laws for div and mod *}
text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *}
@@ -1929,7 +1942,7 @@
lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
-subsubsection{*Proving @{term "a div (b*c) = (a div b) div c"} *}
+subsubsection {* Proving @{term "a div (b*c) = (a div b) div c"} *}
(*The condition c>0 seems necessary. Consider that 7 div ~6 = ~2 but
7 div 2 div ~3 = 3 div ~3 = ~1. The subcase (a div b) mod c = 0 seems
@@ -1990,7 +2003,7 @@
done
-subsubsection {*Splitting Rules for div and mod*}
+subsubsection {* Splitting Rules for div and mod *}
text{*The proofs of the two lemmas below are essentially identical*}
@@ -2051,7 +2064,7 @@
declare split_zmod [of _ _ "number_of k", arith_split] for k
-subsubsection{*Speeding up the Division Algorithm with Shifting*}
+subsubsection {* Speeding up the Division Algorithm with Shifting *}
text{*computing div by shifting *}
@@ -2105,7 +2118,7 @@
done
-subsubsection{*Computing mod by Shifting (proofs resemble those for div)*}
+subsubsection {* Computing mod by Shifting (proofs resemble those for div) *}
lemma pos_zmod_mult_2:
fixes a b :: int
@@ -2169,7 +2182,7 @@
qed
-subsubsection{*Quotients of Signs*}
+subsubsection {* Quotients of Signs *}
lemma div_neg_pos_less0: "[| a < (0::int); 0 < b |] ==> a div b < 0"
apply (subgoal_tac "a div b \<le> -1", force)
@@ -2225,7 +2238,6 @@
using int_one_le_iff_zero_less[of "a div b"] zdiv_mono1[of b a b]apply simp
done
-
lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 ==> m mod k \<le> m"
apply (rule split_zmod[THEN iffD2])
apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le)
@@ -2384,7 +2396,7 @@
proof-
from xy have th: "int x - int y = int (x - y)" by simp
from xyn have "int x mod int n = int y mod int n"
- by (simp add: zmod_int[symmetric])
+ by (simp add: zmod_int [symmetric])
hence "int n dvd int x - int y" by (simp only: zmod_eq_dvd_iff[symmetric])
hence "n dvd x - y" by (simp add: th zdvd_int)
then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith