--- a/src/HOL/Code_Numeral.thy Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Code_Numeral.thy Sat Dec 17 15:22:14 2016 +0100
@@ -168,21 +168,9 @@
"integer_of_num (Num.Bit0 Num.One) = 2"
by (transfer, simp)+
-instantiation integer :: "{ring_div, equal, linordered_idom}"
+instantiation integer :: "{linordered_idom, equal}"
begin
-lift_definition divide_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
- is "divide :: int \<Rightarrow> int \<Rightarrow> int"
- .
-
-declare divide_integer.rep_eq [simp]
-
-lift_definition modulo_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
- is "modulo :: int \<Rightarrow> int \<Rightarrow> int"
- .
-
-declare modulo_integer.rep_eq [simp]
-
lift_definition abs_integer :: "integer \<Rightarrow> integer"
is "abs :: int \<Rightarrow> int"
.
@@ -199,6 +187,7 @@
is "less_eq :: int \<Rightarrow> int \<Rightarrow> bool"
.
+
lift_definition less_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
is "less :: int \<Rightarrow> int \<Rightarrow> bool"
.
@@ -207,8 +196,8 @@
is "HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool"
.
-instance proof
-qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] mult_strict_right_mono linear)+
+instance
+ by standard (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] mult_strict_right_mono linear)+
end
@@ -236,6 +225,38 @@
"of_nat (nat_of_integer k) = max 0 k"
by transfer auto
+instantiation integer :: "{ring_div, normalization_semidom}"
+begin
+
+lift_definition normalize_integer :: "integer \<Rightarrow> integer"
+ is "normalize :: int \<Rightarrow> int"
+ .
+
+declare normalize_integer.rep_eq [simp]
+
+lift_definition unit_factor_integer :: "integer \<Rightarrow> integer"
+ is "unit_factor :: int \<Rightarrow> int"
+ .
+
+declare unit_factor_integer.rep_eq [simp]
+
+lift_definition divide_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+ is "divide :: int \<Rightarrow> int \<Rightarrow> int"
+ .
+
+declare divide_integer.rep_eq [simp]
+
+lift_definition modulo_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+ is "modulo :: int \<Rightarrow> int \<Rightarrow> int"
+ .
+
+declare modulo_integer.rep_eq [simp]
+
+instance
+ by standard (transfer, simp add: mult_sgn_abs sgn_mult)+
+
+end
+
instantiation integer :: semiring_numeral_div
begin
@@ -389,6 +410,14 @@
"Neg m * Neg n = Pos (m * n)"
by simp_all
+lemma normalize_integer_code [code]:
+ "normalize = (abs :: integer \<Rightarrow> integer)"
+ by transfer simp
+
+lemma unit_factor_integer_code [code]:
+ "unit_factor = (sgn :: integer \<Rightarrow> integer)"
+ by transfer simp
+
definition divmod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer \<times> integer"
where
"divmod_integer k l = (k div l, k mod l)"
@@ -760,21 +789,9 @@
"nat_of_natural (numeral k) = numeral k"
by transfer rule
-instantiation natural :: "{semiring_div, equal, linordered_semiring}"
+instantiation natural :: "{linordered_semiring, equal}"
begin
-lift_definition divide_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
- is "divide :: nat \<Rightarrow> nat \<Rightarrow> nat"
- .
-
-declare divide_natural.rep_eq [simp]
-
-lift_definition modulo_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
- is "modulo :: nat \<Rightarrow> nat \<Rightarrow> nat"
- .
-
-declare modulo_natural.rep_eq [simp]
-
lift_definition less_eq_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
is "less_eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
.
@@ -812,6 +829,38 @@
"nat_of_natural (max k l) = max (nat_of_natural k) (nat_of_natural l)"
by transfer rule
+instantiation natural :: "{semiring_div, normalization_semidom}"
+begin
+
+lift_definition normalize_natural :: "natural \<Rightarrow> natural"
+ is "normalize :: nat \<Rightarrow> nat"
+ .
+
+declare normalize_natural.rep_eq [simp]
+
+lift_definition unit_factor_natural :: "natural \<Rightarrow> natural"
+ is "unit_factor :: nat \<Rightarrow> nat"
+ .
+
+declare unit_factor_natural.rep_eq [simp]
+
+lift_definition divide_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+ is "divide :: nat \<Rightarrow> nat \<Rightarrow> nat"
+ .
+
+declare divide_natural.rep_eq [simp]
+
+lift_definition modulo_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+ is "modulo :: nat \<Rightarrow> nat \<Rightarrow> nat"
+ .
+
+declare modulo_natural.rep_eq [simp]
+
+instance
+ by standard (transfer, auto simp add: algebra_simps unit_factor_nat_def gr0_conv_Suc)+
+
+end
+
lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
is "nat :: int \<Rightarrow> nat"
.
@@ -945,7 +994,32 @@
lemma [code abstract]:
"integer_of_natural (m * n) = integer_of_natural m * integer_of_natural n"
- by transfer (simp add: of_nat_mult)
+ by transfer simp
+
+lemma [code]:
+ "normalize n = n" for n :: natural
+ by transfer simp
+
+lemma [code]:
+ "unit_factor n = of_bool (n \<noteq> 0)" for n :: natural
+proof (cases "n = 0")
+ case True
+ then show ?thesis
+ by simp
+next
+ case False
+ then have "unit_factor n = 1"
+ proof transfer
+ fix n :: nat
+ assume "n \<noteq> 0"
+ then obtain m where "n = Suc m"
+ by (cases n) auto
+ then show "unit_factor n = 1"
+ by simp
+ qed
+ with False show ?thesis
+ by simp
+qed
lemma [code abstract]:
"integer_of_natural (m div n) = integer_of_natural m div integer_of_natural n"
--- a/src/HOL/Divides.thy Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Divides.thy Sat Dec 17 15:22:14 2016 +0100
@@ -3,37 +3,95 @@
Copyright 1999 University of Cambridge
*)
-section \<open>The division operators div and mod\<close>
+section \<open>Quotient and remainder\<close>
theory Divides
imports Parity
begin
-subsection \<open>Abstract division in commutative semirings.\<close>
-
-class semiring_div = semidom + semiring_modulo +
- assumes div_by_0: "a div 0 = 0"
- and div_0: "0 div a = 0"
- and div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
+subsection \<open>Quotient and remainder in integral domains\<close>
+
+class semidom_modulo = algebraic_semidom + semiring_modulo
+begin
+
+lemma mod_0 [simp]: "0 mod a = 0"
+ using div_mult_mod_eq [of 0 a] by simp
+
+lemma mod_by_0 [simp]: "a mod 0 = a"
+ using div_mult_mod_eq [of a 0] by simp
+
+lemma mod_by_1 [simp]:
+ "a mod 1 = 0"
+proof -
+ from div_mult_mod_eq [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 div_mult_mod_eq [of a a] by simp
+
+lemma dvd_imp_mod_0 [simp]:
+ assumes "a dvd b"
+ shows "b mod a = 0"
+ using assms minus_div_mult_eq_mod [of b a] by simp
+
+lemma mod_0_imp_dvd:
+ assumes "a mod b = 0"
+ shows "b dvd a"
+proof -
+ have "b dvd ((a div b) * b)" by simp
+ also have "(a div b) * b = a"
+ using div_mult_mod_eq [of a b] by (simp add: assms)
+ finally show ?thesis .
+qed
+
+lemma mod_eq_0_iff_dvd:
+ "a mod b = 0 \<longleftrightarrow> b dvd a"
+ by (auto intro: mod_0_imp_dvd)
+
+lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
+ "a dvd b \<longleftrightarrow> b mod a = 0"
+ by (simp add: mod_eq_0_iff_dvd)
+
+lemma dvd_mod_iff:
+ assumes "c dvd b"
+ shows "c dvd a mod b \<longleftrightarrow> c dvd a"
+proof -
+ from assms have "(c dvd a mod b) \<longleftrightarrow> (c dvd ((a div b) * b + a mod b))"
+ by (simp add: dvd_add_right_iff)
+ also have "(a div b) * b + a mod b = a"
+ using div_mult_mod_eq [of a b] by simp
+ finally show ?thesis .
+qed
+
+lemma dvd_mod_imp_dvd:
+ assumes "c dvd a mod b" and "c dvd b"
+ shows "c dvd a"
+ using assms dvd_mod_iff [of c b a] by simp
+
+end
+
+class idom_modulo = idom + semidom_modulo
+begin
+
+subclass idom_divide ..
+
+lemma div_diff [simp]:
+ "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> (a - b) div c = a div c - b div c"
+ using div_add [of _ _ "- b"] by (simp add: dvd_neg_div)
+
+end
+
+
+subsection \<open>Quotient and remainder in integral domains with additional properties\<close>
+
+class semiring_div = semidom_modulo +
+ assumes 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
-subclass algebraic_semidom
-proof
- fix b a
- assume "b \<noteq> 0"
- then show "a * b div b = a"
- using div_mult_self1 [of b 0 a] by (simp add: ac_simps div_0)
-qed (simp add: div_by_0)
-
-text \<open>@{const divide} and @{const modulo}\<close>
-
-lemma mod_by_0 [simp]: "a mod 0 = a"
- using div_mult_mod_eq [of a zero] by simp
-
-lemma mod_0 [simp]: "0 mod a = 0"
- using div_mult_mod_eq [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"
@@ -86,18 +144,6 @@
"a * b mod b = 0"
using mod_mult_self1 [of 0 a b] by simp
-lemma mod_by_1 [simp]:
- "a mod 1 = 0"
-proof -
- from div_mult_mod_eq [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_add_self1:
assumes "b \<noteq> 0"
shows "(b + a) div b = a div b + 1"
@@ -116,31 +162,6 @@
"(a + b) mod b = a mod b"
using mod_mult_self1 [of a 1 b] by simp
-lemma dvd_imp_mod_0 [simp]:
- assumes "a dvd b"
- shows "b mod a = 0"
-proof -
- from assms obtain c where "b = a * c" ..
- then have "b mod a = a * c mod a" by simp
- then show "b mod a = 0" by simp
-qed
-
-lemma mod_eq_0_iff_dvd:
- "a mod b = 0 \<longleftrightarrow> b dvd a"
-proof
- assume "b dvd a"
- then show "a mod b = 0" by simp
-next
- assume "a mod b = 0"
- with div_mult_mod_eq [of a b] have "a div b * b = a" by simp
- then have "a = b * (a div b)" by (simp add: ac_simps)
- then show "b dvd a" ..
-qed
-
-lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
- "a dvd b \<longleftrightarrow> b mod a = 0"
- by (simp add: mod_eq_0_iff_dvd)
-
lemma mod_div_trivial [simp]:
"a mod b div b = 0"
proof (cases "b = 0")
@@ -168,15 +189,6 @@
finally show ?thesis .
qed
-lemma dvd_mod_imp_dvd:
- assumes "k dvd m mod n" and "k dvd n"
- shows "k dvd m"
-proof -
- from assms have "k dvd (m div n) * n + m mod n"
- by (simp only: dvd_add dvd_mult)
- then show ?thesis by (simp add: div_mult_mod_eq)
-qed
-
text \<open>Addition respects modular equivalence.\<close>
lemma mod_add_left_eq: \<comment> \<open>FIXME reorient\<close>
@@ -319,31 +331,6 @@
lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
unfolding dvd_def by (auto simp add: mod_mult_mult1)
-lemma dvd_mod_iff: "k dvd n \<Longrightarrow> k dvd (m mod n) \<longleftrightarrow> k dvd m"
-by (blast intro: dvd_mod_imp_dvd dvd_mod)
-
-lemma div_div_eq_right:
- assumes "c dvd b" "b dvd a"
- shows "a div (b div c) = a div b * c"
-proof -
- from assms have "a div b * c = (a * c) div b"
- by (subst dvd_div_mult) simp_all
- also from assms have "\<dots> = (a * c) div ((b div c) * c)" by simp
- also have "a * c div (b div c * c) = a div (b div c)"
- by (cases "c = 0") simp_all
- finally show ?thesis ..
-qed
-
-lemma div_div_div_same:
- assumes "d dvd a" "d dvd b" "b dvd a"
- shows "(a div d) div (b div d) = a div b"
- using assms by (subst dvd_div_mult2_eq [symmetric]) simp_all
-
-lemma cancel_div_mod_rules:
- "((a div b) * b + a mod b) + c = a + c"
- "(b * (a div b) + a mod b) + c = a + c"
- by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
-
end
class ring_div = comm_ring_1 + semiring_div
@@ -394,28 +381,6 @@
shows "(a - b) mod c = (a' - b') mod c"
using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"] by simp
-lemma dvd_neg_div: "y dvd x \<Longrightarrow> -x div y = - (x div y)"
-apply (case_tac "y = 0") apply simp
-apply (auto simp add: dvd_def)
-apply (subgoal_tac "-(y * k) = y * - k")
- apply (simp only:)
- apply (erule nonzero_mult_div_cancel_left)
-apply simp
-done
-
-lemma dvd_div_neg: "y dvd x \<Longrightarrow> x div -y = - (x div y)"
-apply (case_tac "y = 0") apply simp
-apply (auto simp add: dvd_def)
-apply (subgoal_tac "y * k = -y * -k")
- apply (erule ssubst, rule nonzero_mult_div_cancel_left)
- apply simp
-apply simp
-done
-
-lemma div_diff [simp]:
- "z dvd x \<Longrightarrow> z dvd y \<Longrightarrow> (x - y) div z = x div z - y div z"
- using div_add [of _ _ "- y"] by (simp add: dvd_neg_div)
-
lemma div_minus_minus [simp]: "(-a) div (-b) = a div b"
using div_mult_mult1 [of "- 1" a b]
unfolding neg_equal_0_iff_equal by simp
@@ -446,7 +411,7 @@
end
-subsubsection \<open>Parity and division\<close>
+subsection \<open>Parity\<close>
class semiring_div_parity = semiring_div + comm_semiring_1_cancel + numeral +
assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
@@ -532,7 +497,7 @@
end
-subsection \<open>Generic numeral division with a pragmatic type class\<close>
+subsection \<open>Numeral division with a pragmatic type class\<close>
text \<open>
The following type class contains everything necessary to formulate
@@ -826,8 +791,10 @@
from m n have "Suc m = q' * n + Suc r'" by simp
with True show ?thesis by blast
next
- case False then have "n \<le> Suc r'" by auto
- moreover from n have "Suc r' \<le> n" by auto
+ case False then have "n \<le> Suc r'"
+ by (simp add: not_less)
+ moreover from n have "Suc r' \<le> n"
+ by (simp add: Suc_le_eq)
ultimately have "n = Suc r'" by auto
with m have "Suc m = Suc q' * n + 0" by simp
with \<open>n \<noteq> 0\<close> show ?thesis by blast
@@ -855,7 +822,7 @@
apply (auto simp add: add_mult_distrib)
done
from \<open>n \<noteq> 0\<close> assms have *: "fst qr = fst qr'"
- by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym)
+ by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym split: if_splits)
with assms have "snd qr = snd qr'"
by (simp add: divmod_nat_rel_def)
with * show ?thesis by (cases qr, cases qr') simp
@@ -884,10 +851,10 @@
using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
qualified lemma divmod_nat_zero: "divmod_nat m 0 = (0, m)"
- by (simp add: Divides.divmod_nat_unique divmod_nat_rel_def)
+ by (simp add: divmod_nat_unique divmod_nat_rel_def)
qualified lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)"
- by (simp add: Divides.divmod_nat_unique divmod_nat_rel_def)
+ by (simp add: divmod_nat_unique divmod_nat_rel_def)
qualified lemma divmod_nat_base: "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
by (simp add: divmod_nat_unique divmod_nat_rel_def)
@@ -899,19 +866,31 @@
have "divmod_nat_rel (m - n) n (divmod_nat (m - n) n)"
by (fact divmod_nat_rel_divmod_nat)
then show "divmod_nat_rel m n (apfst Suc (divmod_nat (m - n) n))"
- unfolding divmod_nat_rel_def using assms by auto
+ unfolding divmod_nat_rel_def using assms
+ by (auto split: if_splits simp add: algebra_simps)
qed
end
-
-instantiation nat :: semiring_div
+
+instantiation nat :: "{semidom_modulo, normalization_semidom}"
begin
-definition divide_nat where
- div_nat_def: "m div n = fst (Divides.divmod_nat m n)"
-
-definition modulo_nat where
- mod_nat_def: "m mod n = snd (Divides.divmod_nat m n)"
+definition normalize_nat :: "nat \<Rightarrow> nat"
+ where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
+
+definition unit_factor_nat :: "nat \<Rightarrow> nat"
+ where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
+
+lemma unit_factor_simps [simp]:
+ "unit_factor 0 = (0::nat)"
+ "unit_factor (Suc n) = 1"
+ by (simp_all add: unit_factor_nat_def)
+
+definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+ where div_nat_def: "m div n = fst (Divides.divmod_nat m n)"
+
+definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+ where mod_nat_def: "m mod n = snd (Divides.divmod_nat m n)"
lemma fst_divmod_nat [simp]:
"fst (Divides.divmod_nat m n) = m div n"
@@ -928,15 +907,18 @@
lemma div_nat_unique:
assumes "divmod_nat_rel m n (q, r)"
shows "m div n = q"
- using assms by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
+ using assms
+ by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
lemma mod_nat_unique:
assumes "divmod_nat_rel m n (q, r)"
shows "m mod n = r"
- using assms by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
+ using assms
+ by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
- using Divides.divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod)
+ using Divides.divmod_nat_rel_divmod_nat
+ by (simp add: divmod_nat_div_mod)
text \<open>The ''recursion'' equations for @{const divide} and @{const modulo}\<close>
@@ -964,11 +946,40 @@
shows "m mod n = (m - n) mod n"
using assms Divides.divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
+lemma mod_less_divisor [simp]:
+ fixes m n :: nat
+ assumes "n > 0"
+ shows "m mod n < n"
+ using assms divmod_nat_rel [of m n] unfolding divmod_nat_rel_def
+ by (auto split: if_splits)
+
+lemma mod_le_divisor [simp]:
+ fixes m n :: nat
+ assumes "n > 0"
+ shows "m mod n \<le> n"
+proof (rule less_imp_le)
+ from assms show "m mod n < n"
+ by simp
+qed
+
instance proof
fix m n :: nat
show "m div n * n + m mod n = m"
using divmod_nat_rel [of m n] by (simp add: divmod_nat_rel_def)
next
+ fix n :: nat show "n div 0 = 0"
+ by (simp add: div_nat_def Divides.divmod_nat_zero)
+next
+ fix m n :: nat
+ assume "n \<noteq> 0"
+ then show "m * n div n = m"
+ by (auto simp add: divmod_nat_rel_def intro: div_nat_unique [of _ _ _ 0])
+qed (simp_all add: unit_factor_nat_def)
+
+end
+
+instance nat :: semiring_div
+proof
fix m n q :: nat
assume "n \<noteq> 0"
then show "(q + m * n) div n = m + q div n"
@@ -976,48 +987,33 @@
next
fix m n q :: nat
assume "m \<noteq> 0"
- hence "\<And>a b. divmod_nat_rel n q (a, b) \<Longrightarrow> divmod_nat_rel (m * n) (m * q) (a, m * b)"
- unfolding divmod_nat_rel_def
- by (auto split: if_split_asm, simp_all add: algebra_simps)
- moreover from divmod_nat_rel have "divmod_nat_rel n q (n div q, n mod q)" .
- ultimately have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))" .
- thus "(m * n) div (m * q) = n div q" by (rule div_nat_unique)
-next
- fix n :: nat show "n div 0 = 0"
- by (simp add: div_nat_def Divides.divmod_nat_zero)
-next
- fix n :: nat show "0 div n = 0"
- by (simp add: div_nat_def Divides.divmod_nat_zero_left)
+ then have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))"
+ using div_mult_mod_eq [of n q]
+ by (auto simp add: divmod_nat_rel_def algebra_simps distrib_left [symmetric] simp del: distrib_left)
+ then show "(m * n) div (m * q) = n div q"
+ by (rule div_nat_unique)
qed
-end
-
-instantiation nat :: normalization_semidom
-begin
-
-definition normalize_nat
- where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
-
-definition unit_factor_nat
- where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
-
-lemma unit_factor_simps [simp]:
- "unit_factor 0 = (0::nat)"
- "unit_factor (Suc n) = 1"
- by (simp_all add: unit_factor_nat_def)
-
-instance
- by standard (simp_all add: unit_factor_nat_def)
-
-end
-
-lemma divmod_nat_if [code]:
- "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
- let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
- by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
+lemma div_by_Suc_0 [simp]:
+ "m div Suc 0 = m"
+ using div_by_1 [of m] by simp
+
+lemma mod_by_Suc_0 [simp]:
+ "m mod Suc 0 = 0"
+ using mod_by_1 [of m] by simp
+
+lemma mod_greater_zero_iff_not_dvd:
+ fixes m n :: nat
+ shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
+ by (simp add: dvd_eq_mod_eq_0)
text \<open>Simproc for cancelling @{const divide} and @{const modulo}\<close>
+lemma (in semiring_modulo) cancel_div_mod_rules:
+ "((a div b) * b + a mod b) + c = a + c"
+ "(b * (a div b) + a mod b) + c = a + c"
+ by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
+
ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
ML \<open>
@@ -1048,7 +1044,13 @@
)
\<close>
-simproc_setup cancel_div_mod_nat ("(m::nat) + n") = \<open>K Cancel_Div_Mod_Nat.proc\<close>
+simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
+ \<open>K Cancel_Div_Mod_Nat.proc\<close>
+
+lemma divmod_nat_if [code]:
+ "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
+ let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
+ by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
subsubsection \<open>Quotient\<close>
@@ -1077,16 +1079,11 @@
qed
lemma div_eq_0_iff: "(a div b::nat) = 0 \<longleftrightarrow> a < b \<or> b = 0"
- by (metis div_less div_positive div_by_0 gr0I less_numeral_extra(3) not_less)
+ by auto (metis div_positive less_numeral_extra(3) not_less)
+
subsubsection \<open>Remainder\<close>
-lemma mod_less_divisor [simp]:
- fixes m n :: nat
- assumes "n > 0"
- shows "m mod n < (n::nat)"
- using assms divmod_nat_rel [of m n] unfolding divmod_nat_rel_def by auto
-
lemma mod_Suc_le_divisor [simp]:
"m mod Suc n \<le> n"
using mod_less_divisor [of "Suc n" m] by arith
@@ -1105,13 +1102,6 @@
lemma mod_if: "m mod (n::nat) = (if m < n then m else (m - n) mod n)"
by (simp add: le_mod_geq)
-lemma mod_by_Suc_0 [simp]: "m mod Suc 0 = 0"
-by (induct m) (simp_all add: mod_geq)
-
-lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
- apply (drule mod_less_divisor [where m = m])
- apply simp
- done
subsubsection \<open>Quotient and Remainder\<close>
@@ -1180,25 +1170,16 @@
subsubsection \<open>Further Facts about Quotient and Remainder\<close>
-lemma div_by_Suc_0 [simp]:
- "m div Suc 0 = m"
- using div_by_1 [of m] by simp
-
-(* 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)"
-apply (case_tac "k=0", simp)
-apply (induct "n" rule: nat_less_induct, clarify)
-apply (case_tac "n<k")
-(* 1 case n<k *)
-apply simp
-(* 2 case n >= k *)
-apply (case_tac "m<k")
-(* 2.1 case m<k *)
-apply simp
-(* 2.2 case m>=k *)
-apply (simp add: div_geq diff_le_mono)
-done
+lemma div_le_mono:
+ fixes m n k :: nat
+ assumes "m \<le> n"
+ shows "m div k \<le> n div k"
+proof -
+ from assms obtain q where "n = m + q"
+ by (auto simp add: le_iff_add)
+ then show ?thesis
+ by (simp add: div_add1_eq [of m q k])
+qed
(* Antimonotonicity of div in second argument *)
lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
@@ -1519,11 +1500,6 @@
declare Suc_times_mod_eq [of "numeral w", simp] for w
-lemma mod_greater_zero_iff_not_dvd:
- fixes m n :: nat
- shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
- by (simp add: dvd_eq_mod_eq_0)
-
lemma Suc_div_le_mono [simp]: "n div k \<le> (Suc n) div k"
by (simp add: div_le_mono)
@@ -1643,6 +1619,9 @@
subsection \<open>Division on @{typ int}\<close>
+context
+begin
+
definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" \<comment> \<open>definition of quotient and remainder\<close>
where "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
(if 0 < b then 0 \<le> r \<and> r < b else if b < 0 then b < r \<and> r \<le> 0 else q = 0))"
@@ -1678,10 +1657,18 @@
apply (blast intro: unique_quotient)
done
-instantiation int :: modulo
+end
+
+instantiation int :: "{idom_modulo, normalization_semidom}"
begin
-definition divide_int
+definition normalize_int :: "int \<Rightarrow> int"
+ where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
+
+definition unit_factor_int :: "int \<Rightarrow> int"
+ where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
+
+definition divide_int :: "int \<Rightarrow> int \<Rightarrow> int"
where "k div l = (if l = 0 \<or> k = 0 then 0
else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
then int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
@@ -1689,32 +1676,35 @@
if l dvd k then - int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
else - int (Suc (nat \<bar>k\<bar> div nat \<bar>l\<bar>)))"
-definition modulo_int
+definition modulo_int :: "int \<Rightarrow> int \<Rightarrow> int"
where "k mod l = (if l = 0 then k else if l dvd k then 0
else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
else sgn l * (\<bar>l\<bar> - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
-instance ..
-
-end
-
lemma divmod_int_rel:
"divmod_int_rel k l (k div l, k mod l)"
- unfolding divmod_int_rel_def divide_int_def modulo_int_def
- apply (cases k rule: int_cases3)
- apply (simp add: mod_greater_zero_iff_not_dvd not_le algebra_simps)
- apply (cases l rule: int_cases3)
- apply (simp add: mod_greater_zero_iff_not_dvd not_le algebra_simps)
- apply (simp_all del: of_nat_add of_nat_mult add: mod_greater_zero_iff_not_dvd not_le algebra_simps int_dvd_iff of_nat_add [symmetric] of_nat_mult [symmetric])
- apply (cases l rule: int_cases3)
- apply (simp_all del: of_nat_add of_nat_mult add: not_le algebra_simps int_dvd_iff of_nat_add [symmetric] of_nat_mult [symmetric])
- done
-
-instantiation int :: ring_div
-begin
-
-subsubsection \<open>Uniqueness and Monotonicity of Quotients and Remainders\<close>
+proof (cases k rule: int_cases3)
+ case zero
+ then show ?thesis
+ by (simp add: divmod_int_rel_def divide_int_def modulo_int_def)
+next
+ case (pos n)
+ then show ?thesis
+ using div_mult_mod_eq [of n]
+ by (cases l rule: int_cases3)
+ (auto simp del: of_nat_mult of_nat_add
+ simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
+ divmod_int_rel_def divide_int_def modulo_int_def int_dvd_iff)
+next
+ case (neg n)
+ then show ?thesis
+ using div_mult_mod_eq [of n]
+ by (cases l rule: int_cases3)
+ (auto simp del: of_nat_mult of_nat_add
+ simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
+ divmod_int_rel_def divide_int_def modulo_int_def int_dvd_iff)
+qed
lemma divmod_int_unique:
assumes "divmod_int_rel k l (q, r)"
@@ -1722,42 +1712,21 @@
using assms divmod_int_rel [of k l]
using unique_quotient [of k l] unique_remainder [of k l]
by auto
-
-instance
-proof
- fix a b :: int
- show "a div b * b + a mod b = a"
- using divmod_int_rel [of a b]
- unfolding divmod_int_rel_def by (simp add: mult.commute)
-next
- fix a b c :: int
- assume "b \<noteq> 0"
- hence "divmod_int_rel (a + c * b) b (c + a div b, a mod b)"
- using divmod_int_rel [of a b]
- unfolding divmod_int_rel_def by (auto simp: algebra_simps)
- thus "(a + c * b) div b = c + a div b"
- by (rule div_int_unique)
+
+instance proof
+ fix k l :: int
+ show "k div l * l + k mod l = k"
+ using divmod_int_rel [of k l]
+ unfolding divmod_int_rel_def by (simp add: ac_simps)
next
- fix a b c :: int
- assume c: "c \<noteq> 0"
- have "\<And>q r. divmod_int_rel a b (q, r)
- \<Longrightarrow> divmod_int_rel (c * a) (c * b) (q, c * r)"
- unfolding divmod_int_rel_def
- by (rule linorder_cases [of 0 b])
- (use c in \<open>auto simp: algebra_simps
- mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
- mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff\<close>)
- hence "divmod_int_rel (c * a) (c * b) (a div b, c * (a mod b))"
- using divmod_int_rel [of a b] .
- thus "(c * a) div (c * b) = a div b"
- by (rule div_int_unique)
-next
- fix a :: int show "a div 0 = 0"
+ fix k :: int show "k div 0 = 0"
by (rule div_int_unique, simp add: divmod_int_rel_def)
next
- fix a :: int show "0 div a = 0"
- by (rule div_int_unique, auto simp add: divmod_int_rel_def)
-qed
+ fix k l :: int
+ assume "l \<noteq> 0"
+ then show "k * l div l = k"
+ by (auto simp add: divmod_int_rel_def ac_simps intro: div_int_unique [of _ _ _ 0])
+qed (simp_all add: sgn_mult mult_sgn_abs abs_sgn_eq)
end
@@ -1765,36 +1734,30 @@
"is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
by auto
-instantiation int :: normalization_semidom
-begin
-
-definition normalize_int
- where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
-
-definition unit_factor_int
- where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
-
-instance
+instance int :: ring_div
proof
- fix k :: int
- assume "k \<noteq> 0"
- then have "\<bar>sgn k\<bar> = 1"
- by (cases "0::int" k rule: linorder_cases) simp_all
- then show "is_unit (unit_factor k)"
- by simp
-qed (simp_all add: sgn_mult mult_sgn_abs)
-
-end
-
-text\<open>Basic laws about division and remainder\<close>
-
-lemma zdiv_int: "int (a div b) = int a div int b"
- by (simp add: divide_int_def)
-
-lemma zmod_int: "int (a mod b) = int a mod int b"
- by (simp add: modulo_int_def int_dvd_iff)
-
-text \<open>Tool setup\<close>
+ fix k l s :: int
+ assume "l \<noteq> 0"
+ then have "divmod_int_rel (k + s * l) l (s + k div l, k mod l)"
+ using divmod_int_rel [of k l]
+ unfolding divmod_int_rel_def by (auto simp: algebra_simps)
+ then show "(k + s * l) div l = s + k div l"
+ by (rule div_int_unique)
+next
+ fix k l s :: int
+ assume "s \<noteq> 0"
+ have "\<And>q r. divmod_int_rel k l (q, r)
+ \<Longrightarrow> divmod_int_rel (s * k) (s * l) (q, s * r)"
+ unfolding divmod_int_rel_def
+ by (rule linorder_cases [of 0 l])
+ (use \<open>s \<noteq> 0\<close> in \<open>auto simp: algebra_simps
+ mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
+ mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff\<close>)
+ then have "divmod_int_rel (s * k) (s * l) (k div l, s * (k mod l))"
+ using divmod_int_rel [of k l] .
+ then show "(s * k) div (s * l) = k div l"
+ by (rule div_int_unique)
+qed
ML \<open>
structure Cancel_Div_Mod_Int = Cancel_Div_Mod
@@ -1807,12 +1770,22 @@
val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
- val prove_eq_sums = Arith_Data.prove_conv2 all_tac
- (Arith_Data.simp_all_tac @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
+ val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
+ @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
)
\<close>
-simproc_setup cancel_div_mod_int ("(k::int) + l") = \<open>K Cancel_Div_Mod_Int.proc\<close>
+simproc_setup cancel_div_mod_int ("(k::int) + l") =
+ \<open>K Cancel_Div_Mod_Int.proc\<close>
+
+
+text\<open>Basic laws about division and remainder\<close>
+
+lemma zdiv_int: "int (a div b) = int a div int b"
+ by (simp add: divide_int_def)
+
+lemma zmod_int: "int (a mod b) = int a mod int b"
+ by (simp add: modulo_int_def int_dvd_iff)
lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
using divmod_int_rel [of a b]
@@ -1887,10 +1860,15 @@
apply (blast intro: divmod_int_rel [THEN zminus1_lemma, THEN mod_int_unique])
done
-lemma zmod_zminus1_not_zero:
+lemma zmod_zminus1_not_zero: -- \<open>FIXME generalize\<close>
fixes k l :: int
shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
- unfolding zmod_zminus1_eq_if by auto
+ by (simp add: mod_eq_0_iff_dvd)
+
+lemma zmod_zminus2_not_zero: -- \<open>FIXME generalize\<close>
+ fixes k l :: int
+ shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
+ by (simp add: mod_eq_0_iff_dvd)
lemma zdiv_zminus2_eq_if:
"b \<noteq> (0::int)
@@ -1902,11 +1880,6 @@
"a mod (-b::int) = (if a mod b = 0 then 0 else (a mod b) - b)"
by (simp add: zmod_zminus1_eq_if mod_minus_right)
-lemma zmod_zminus2_not_zero:
- fixes k l :: int
- shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
- unfolding zmod_zminus2_eq_if by auto
-
subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
@@ -2666,6 +2639,4 @@
declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
-hide_fact (open) div_0 div_by_0
-
end
--- a/src/HOL/Enum.thy Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Enum.thy Sat Dec 17 15:22:14 2016 +0100
@@ -683,7 +683,7 @@
instance finite_2 :: complete_linorder ..
-instantiation finite_2 :: "{field, ring_div, idom_abs_sgn}" begin
+instantiation finite_2 :: "{field, idom_abs_sgn}" begin
definition [simp]: "0 = a\<^sub>1"
definition [simp]: "1 = a\<^sub>2"
definition "x + y = (case (x, y) of (a\<^sub>1, a\<^sub>1) \<Rightarrow> a\<^sub>1 | (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)"
@@ -693,19 +693,33 @@
definition "inverse = (\<lambda>x :: finite_2. x)"
definition "divide = (op * :: finite_2 \<Rightarrow> _)"
definition "abs = (\<lambda>x :: finite_2. x)"
-definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
definition "sgn = (\<lambda>x :: finite_2. x)"
instance
-by intro_classes
- (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def times_finite_2_def
- inverse_finite_2_def divide_finite_2_def abs_finite_2_def modulo_finite_2_def sgn_finite_2_def
- split: finite_2.splits)
+ by standard
+ (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def times_finite_2_def
+ inverse_finite_2_def divide_finite_2_def abs_finite_2_def sgn_finite_2_def
+ split: finite_2.splits)
end
lemma two_finite_2 [simp]:
"2 = a\<^sub>1"
by (simp add: numeral.simps plus_finite_2_def)
-
+
+lemma dvd_finite_2_unfold:
+ "x dvd y \<longleftrightarrow> x = a\<^sub>2 \<or> y = a\<^sub>1"
+ by (auto simp add: dvd_def times_finite_2_def split: finite_2.splits)
+
+instantiation finite_2 :: "{ring_div, normalization_semidom}" begin
+definition [simp]: "normalize = (id :: finite_2 \<Rightarrow> _)"
+definition [simp]: "unit_factor = (id :: finite_2 \<Rightarrow> _)"
+definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
+instance
+ by standard
+ (simp_all add: dvd_finite_2_unfold times_finite_2_def
+ divide_finite_2_def modulo_finite_2_def split: finite_2.splits)
+end
+
+
hide_const (open) a\<^sub>1 a\<^sub>2
datatype (plugins only: code "quickcheck" extraction) finite_3 =
@@ -736,6 +750,12 @@
end
+lemma finite_3_not_eq_unfold:
+ "x \<noteq> a\<^sub>1 \<longleftrightarrow> x \<in> {a\<^sub>2, a\<^sub>3}"
+ "x \<noteq> a\<^sub>2 \<longleftrightarrow> x \<in> {a\<^sub>1, a\<^sub>3}"
+ "x \<noteq> a\<^sub>3 \<longleftrightarrow> x \<in> {a\<^sub>1, a\<^sub>2}"
+ by (cases x; simp)+
+
instantiation finite_3 :: linorder
begin
@@ -806,7 +826,7 @@
instance finite_3 :: complete_linorder ..
-instantiation finite_3 :: "{field, ring_div, idom_abs_sgn}" begin
+instantiation finite_3 :: "{field, idom_abs_sgn}" begin
definition [simp]: "0 = a\<^sub>1"
definition [simp]: "1 = a\<^sub>2"
definition
@@ -820,14 +840,33 @@
definition "inverse = (\<lambda>x :: finite_3. x)"
definition "x div y = x * inverse (y :: finite_3)"
definition "abs = (\<lambda>x. case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
-definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>1) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
definition "sgn = (\<lambda>x :: finite_3. x)"
instance
-by intro_classes
- (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def times_finite_3_def
- inverse_finite_3_def divide_finite_3_def abs_finite_3_def modulo_finite_3_def sgn_finite_3_def
- less_finite_3_def
- split: finite_3.splits)
+ by standard
+ (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def times_finite_3_def
+ inverse_finite_3_def divide_finite_3_def abs_finite_3_def sgn_finite_3_def
+ less_finite_3_def
+ split: finite_3.splits)
+end
+
+lemma two_finite_3 [simp]:
+ "2 = a\<^sub>3"
+ by (simp add: numeral.simps plus_finite_3_def)
+
+lemma dvd_finite_3_unfold:
+ "x dvd y \<longleftrightarrow> x = a\<^sub>2 \<or> x = a\<^sub>3 \<or> y = a\<^sub>1"
+ by (cases x) (auto simp add: dvd_def times_finite_3_def split: finite_3.splits)
+
+instantiation finite_3 :: "{ring_div, normalization_semidom}" begin
+definition "normalize x = (case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
+definition [simp]: "unit_factor = (id :: finite_3 \<Rightarrow> _)"
+definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>1) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
+instance
+ by standard
+ (auto simp add: finite_3_not_eq_unfold plus_finite_3_def
+ dvd_finite_3_unfold times_finite_3_def inverse_finite_3_def
+ normalize_finite_3_def divide_finite_3_def modulo_finite_3_def
+ split: finite_3.splits)
end
--- a/src/HOL/Library/Formal_Power_Series.thy Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy Sat Dec 17 15:22:14 2016 +0100
@@ -1157,7 +1157,40 @@
lemma fps_unit_dvd [simp]: "(f $ 0 :: 'a :: field) \<noteq> 0 \<Longrightarrow> f dvd g"
by (rule dvd_trans, subst fps_is_unit_iff) simp_all
-
+instantiation fps :: (field) normalization_semidom
+begin
+
+definition fps_unit_factor_def [simp]:
+ "unit_factor f = fps_shift (subdegree f) f"
+
+definition fps_normalize_def [simp]:
+ "normalize f = (if f = 0 then 0 else X ^ subdegree f)"
+
+instance proof
+ fix f :: "'a fps"
+ show "unit_factor f * normalize f = f"
+ by (simp add: fps_shift_times_X_power)
+next
+ fix f g :: "'a fps"
+ show "unit_factor (f * g) = unit_factor f * unit_factor g"
+ proof (cases "f = 0 \<or> g = 0")
+ assume "\<not>(f = 0 \<or> g = 0)"
+ thus "unit_factor (f * g) = unit_factor f * unit_factor g"
+ unfolding fps_unit_factor_def
+ by (auto simp: fps_shift_fps_shift fps_shift_mult fps_shift_mult_right)
+ qed auto
+next
+ fix f g :: "'a fps"
+ assume "g \<noteq> 0"
+ then have "f * (fps_shift (subdegree g) g * inverse (fps_shift (subdegree g) g)) = f"
+ by (metis add_cancel_right_left fps_shift_nth inverse_mult_eq_1 mult.commute mult_cancel_left2 nth_subdegree_nonzero)
+ then have "fps_shift (subdegree g) (g * (f * inverse (fps_shift (subdegree g) g))) = f"
+ by (simp add: fps_shift_mult_right mult.commute)
+ with \<open>g \<noteq> 0\<close> show "f * g / g = f"
+ by (simp add: fps_divide_def Let_def ac_simps)
+qed (auto simp add: fps_divide_def Let_def)
+
+end
instantiation fps :: (field) ring_div
begin
@@ -1291,7 +1324,7 @@
also have "fps_shift n (f * inverse h') = f div h"
by (simp add: fps_divide_def Let_def dfs)
finally show "(f + g * h) div h = g + f div h" by simp
-qed (auto simp: fps_divide_def fps_mod_def Let_def)
+qed
end
end
@@ -1365,36 +1398,6 @@
fps_numeral_divide_divide fps_numeral_mult_divide inverse_fps_numeral neg_numeral_fps_const
-
-instantiation fps :: (field) normalization_semidom
-begin
-
-definition fps_unit_factor_def [simp]:
- "unit_factor f = fps_shift (subdegree f) f"
-
-definition fps_normalize_def [simp]:
- "normalize f = (if f = 0 then 0 else X ^ subdegree f)"
-
-instance proof
- fix f :: "'a fps"
- show "unit_factor f * normalize f = f"
- by (simp add: fps_shift_times_X_power)
-next
- fix f g :: "'a fps"
- show "unit_factor (f * g) = unit_factor f * unit_factor g"
- proof (cases "f = 0 \<or> g = 0")
- assume "\<not>(f = 0 \<or> g = 0)"
- thus "unit_factor (f * g) = unit_factor f * unit_factor g"
- unfolding fps_unit_factor_def
- by (auto simp: fps_shift_fps_shift fps_shift_mult fps_shift_mult_right)
- qed auto
-qed auto
-
-end
-
-instance fps :: (field) algebraic_semidom ..
-
-
subsection \<open>Formal power series form a Euclidean ring\<close>
instantiation fps :: (field) euclidean_ring
--- a/src/HOL/Library/Normalized_Fraction.thy Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Library/Normalized_Fraction.thy Sat Dec 17 15:22:14 2016 +0100
@@ -184,7 +184,7 @@
lemma quot_of_fract_uminus:
"quot_of_fract (-x) = (let (a,b) = quot_of_fract x in (-a, b))"
- by transfer (auto simp: case_prod_unfold Let_def normalize_quot_def dvd_neg_div' mult_unit_dvd_iff)
+ by transfer (auto simp: case_prod_unfold Let_def normalize_quot_def dvd_neg_div mult_unit_dvd_iff)
lemma quot_of_fract_diff:
"quot_of_fract (x - y) =
--- a/src/HOL/Library/Polynomial.thy Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Library/Polynomial.thy Sat Dec 17 15:22:14 2016 +0100
@@ -2274,12 +2274,6 @@
from pdivmod_rel[of x y,unfolded pdivmod_rel_def]
show "x div y * y + x mod y = x" by auto
next
- fix x :: "'a poly"
- show "x div 0 = 0" by simp
-next
- fix y :: "'a poly"
- show "0 div y = 0" by simp
-next
fix x y z :: "'a poly"
assume "y \<noteq> 0"
hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)"
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Sat Dec 17 15:22:14 2016 +0100
@@ -17,7 +17,7 @@
The existence of these functions makes it possible to derive gcd and lcm functions
for any Euclidean semiring.
\<close>
-class euclidean_semiring = semiring_modulo + normalization_semidom +
+class euclidean_semiring = semidom_modulo + normalization_semidom +
fixes euclidean_size :: "'a \<Rightarrow> nat"
assumes size_0 [simp]: "euclidean_size 0 = 0"
assumes mod_size_less:
@@ -26,30 +26,6 @@
"b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
begin
-lemma mod_0 [simp]: "0 mod a = 0"
- using div_mult_mod_eq [of 0 a] by simp
-
-lemma dvd_mod_iff:
- assumes "k dvd n"
- shows "(k dvd m mod n) = (k dvd m)"
-proof -
- from assms have "(k dvd m mod n) \<longleftrightarrow> (k dvd ((m div n) * n + m mod n))"
- by (simp add: dvd_add_right_iff)
- also have "(m div n) * n + m mod n = m"
- using div_mult_mod_eq [of m n] by simp
- finally show ?thesis .
-qed
-
-lemma mod_0_imp_dvd:
- assumes "a mod b = 0"
- shows "b dvd a"
-proof -
- have "b dvd ((a div b) * b)" by simp
- also have "(a div b) * b = a"
- using div_mult_mod_eq [of a b] by (simp add: assms)
- finally show ?thesis .
-qed
-
lemma euclidean_size_normalize [simp]:
"euclidean_size (normalize a) = euclidean_size a"
proof (cases "a = 0")
--- a/src/HOL/Rings.thy Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Rings.thy Sat Dec 17 15:22:14 2016 +0100
@@ -731,7 +731,7 @@
class idom_divide = idom + semidom_divide
begin
-lemma dvd_neg_div':
+lemma dvd_neg_div:
assumes "b dvd a"
shows "- a div b = - (a div b)"
proof (cases "b = 0")
@@ -740,10 +740,30 @@
next
case False
from assms obtain c where "a = b * c" ..
- moreover from False have "b * - c div b = - (b * c div b)"
- using nonzero_mult_div_cancel_left [of b "- c"]
+ then have "- a div b = (b * - c) div b"
+ by simp
+ from False also have "\<dots> = - c"
+ by (rule nonzero_mult_div_cancel_left)
+ with False \<open>a = b * c\<close> show ?thesis
by simp
- ultimately show ?thesis
+qed
+
+lemma dvd_div_neg:
+ assumes "b dvd a"
+ shows "a div - b = - (a div b)"
+proof (cases "b = 0")
+ case True
+ then show ?thesis by simp
+next
+ case False
+ then have "- b \<noteq> 0"
+ by simp
+ from assms obtain c where "a = b * c" ..
+ then have "a div - b = (- b * - c) div - b"
+ by simp
+ from \<open>- b \<noteq> 0\<close> also have "\<dots> = - c"
+ by (rule nonzero_mult_div_cancel_left)
+ with False \<open>a = b * c\<close> show ?thesis
by simp
qed
@@ -916,6 +936,39 @@
by (simp add: mult.commute [of a] mult.assoc)
qed
+lemma div_div_eq_right:
+ assumes "c dvd b" "b dvd a"
+ shows "a div (b div c) = a div b * c"
+proof (cases "c = 0 \<or> b = 0")
+ case True
+ then show ?thesis
+ by auto
+next
+ case False
+ from assms obtain r s where "b = c * r" and "a = c * r * s"
+ by (blast elim: dvdE)
+ moreover with False have "r \<noteq> 0"
+ by auto
+ ultimately show ?thesis using False
+ by simp (simp add: mult.commute [of _ r] mult.assoc mult.commute [of c])
+qed
+
+lemma div_div_div_same:
+ assumes "d dvd b" "b dvd a"
+ shows "(a div d) div (b div d) = a div b"
+proof (cases "b = 0 \<or> d = 0")
+ case True
+ with assms show ?thesis
+ by auto
+next
+ case False
+ from assms obtain r s
+ where "a = d * r * s" and "b = d * r"
+ by (blast elim: dvdE)
+ with False show ?thesis
+ by simp (simp add: ac_simps)
+qed
+
text \<open>Units: invertible elements in a ring\<close>