--- a/src/HOL/Divides.thy Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Divides.thy Sun Oct 08 22:28:22 2017 +0200
@@ -326,12 +326,6 @@
"m mod n = snd (divmod_nat m n)"
by simp_all
-
-subsection \<open>Division on @{typ int}\<close>
-
-context
-begin
-
inductive eucl_rel_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool"
where eucl_rel_int_by0: "eucl_rel_int k 0 (0, k)"
| eucl_rel_int_dividesI: "l \<noteq> 0 \<Longrightarrow> k = q * l \<Longrightarrow> eucl_rel_int k l (q, 0)"
@@ -377,31 +371,6 @@
apply (blast intro: unique_quotient)
done
-end
-
-instantiation int :: "{idom_modulo, normalization_semidom}"
-begin
-
-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>)
- else
- 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 :: "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>)))"
-
lemma eucl_rel_int:
"eucl_rel_int k l (k div l, k mod l)"
proof (cases k rule: int_cases3)
@@ -433,42 +402,21 @@
using unique_quotient [of k l] unique_remainder [of k l]
by auto
-instance proof
- fix k l :: int
- show "k div l * l + k mod l = k"
- using eucl_rel_int [of k l]
- unfolding eucl_rel_int_iff by (simp add: ac_simps)
-next
- fix k :: int show "k div 0 = 0"
- by (rule div_int_unique, simp add: eucl_rel_int_iff)
-next
- fix k l :: int
- assume "l \<noteq> 0"
- then show "k * l div l = k"
- by (auto simp add: eucl_rel_int_iff ac_simps intro: div_int_unique [of _ _ _ 0])
-qed (auto simp add: sgn_mult mult_sgn_abs abs_eq_iff')
-
-end
-
-lemma is_unit_int:
- "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
- by auto
-
-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 div_abs_eq_div_nat:
"\<bar>k\<bar> div \<bar>l\<bar> = int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)"
by (simp add: divide_int_def)
lemma mod_abs_eq_div_nat:
"\<bar>k\<bar> mod \<bar>l\<bar> = int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)"
- by (simp add: modulo_int_def dvd_int_unfold_dvd_nat)
+ by (simp add: modulo_int_def)
+
+lemma zdiv_int:
+ "int (a div b) = int a div int b"
+ by (simp add: divide_int_def sgn_1_pos)
+
+lemma zmod_int:
+ "int (a mod b) = int a mod int b"
+ by (simp add: modulo_int_def sgn_1_pos)
lemma div_sgn_abs_cancel:
fixes k l v :: int
@@ -493,7 +441,7 @@
next
case False
with assms have "(sgn k * \<bar>k\<bar>) div (sgn l * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
- by (simp add: div_sgn_abs_cancel)
+ using div_sgn_abs_cancel [of l k l] by simp
then show ?thesis
by (simp add: sgn_mult_abs)
qed
@@ -502,12 +450,14 @@
fixes k l :: int
assumes "l dvd k"
shows "k div l = (sgn k * sgn l) * (\<bar>k\<bar> div \<bar>l\<bar>)"
-proof (cases "k = 0")
+proof (cases "k = 0 \<or> l = 0")
case True
then show ?thesis
- by simp
+ by auto
next
case False
+ then have "k \<noteq> 0" and "l \<noteq> 0"
+ by auto
show ?thesis
proof (cases "sgn l = sgn k")
case True
@@ -515,9 +465,12 @@
by (simp add: div_eq_sgn_abs)
next
case False
- with \<open>k \<noteq> 0\<close> assms show ?thesis
+ with \<open>k \<noteq> 0\<close> \<open>l \<noteq> 0\<close>
+ have "sgn l * sgn k = - 1"
+ by (simp add: sgn_if split: if_splits)
+ with assms show ?thesis
unfolding divide_int_def [of k l]
- by (auto simp add: zdiv_int)
+ by (auto simp add: zdiv_int ac_simps)
qed
qed
@@ -529,59 +482,14 @@
using assms
by (simp only: divide_int_def [of k l], auto simp add: not_less zdiv_int)
-lemma sgn_mod:
- fixes k l :: int
- assumes "l \<noteq> 0" "\<not> l dvd k"
- shows "sgn (k mod l) = sgn l"
-proof -
- from \<open>\<not> l dvd k\<close>
- have "k mod l \<noteq> 0"
- by (simp add: dvd_eq_mod_eq_0)
- show ?thesis
- using \<open>l \<noteq> 0\<close> \<open>\<not> l dvd k\<close>
- unfolding modulo_int_def [of k l]
- by (auto simp add: sgn_1_pos sgn_1_neg mod_greater_zero_iff_not_dvd nat_dvd_iff not_less
- zless_nat_eq_int_zless [symmetric] elim: nonpos_int_cases)
-qed
-
-lemma abs_mod_less:
- fixes k l :: int
- assumes "l \<noteq> 0"
- shows "\<bar>k mod l\<bar> < \<bar>l\<bar>"
- using assms unfolding modulo_int_def [of k l]
- by (auto simp add: not_less int_dvd_iff mod_greater_zero_iff_not_dvd elim: pos_int_cases neg_int_cases nonneg_int_cases nonpos_int_cases)
-
-instantiation int :: unique_euclidean_ring
-begin
-
-definition [simp]:
- "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
-
-definition [simp]:
- "uniqueness_constraint_int (k :: int) l \<longleftrightarrow> unit_factor k = unit_factor l"
-
-instance proof
- fix l q r:: int
- assume "uniqueness_constraint r l"
- and "euclidean_size r < euclidean_size l"
- then have "sgn r = sgn l" and "\<bar>r\<bar> < \<bar>l\<bar>"
- by simp_all
- then have "eucl_rel_int (q * l + r) l (q, r)"
- by (rule eucl_rel_int_remainderI) simp
- then show "(q * l + r) div l = q"
- by (rule div_int_unique)
-qed (use mult_le_mono2 [of 1] in \<open>auto simp add: abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>)
-
-end
-
text\<open>Basic laws about division and remainder\<close>
lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
using eucl_rel_int [of a b]
by (auto simp add: eucl_rel_int_iff prod_eq_iff)
-lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
- and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]
+lemmas pos_mod_sign = pos_mod_conj [THEN conjunct1]
+ and pos_mod_bound = pos_mod_conj [THEN conjunct2]
lemma neg_mod_conj: "b < (0::int) \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b"
using eucl_rel_int [of a b]
@@ -631,39 +539,6 @@
text\<open>There is no \<open>mod_neg_pos_trivial\<close>.\<close>
-instance int :: ring_parity
-proof
- fix k l :: int
- show "k mod 2 = 1" if "\<not> 2 dvd k"
- proof (rule order_antisym)
- have "0 \<le> k mod 2" and "k mod 2 < 2"
- by auto
- moreover have "k mod 2 \<noteq> 0"
- using that by (simp add: dvd_eq_mod_eq_0)
- ultimately have "0 < k mod 2"
- by (simp only: less_le) simp
- then show "1 \<le> k mod 2"
- by simp
- from \<open>k mod 2 < 2\<close> show "k mod 2 \<le> 1"
- by (simp only: less_le) simp
- qed
-qed (simp_all add: dvd_eq_mod_eq_0 divide_int_def)
-
-lemma even_diff_iff [simp]:
- "even (k - l) \<longleftrightarrow> even (k + l)" for k l :: int
- using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
-
-lemma even_abs_add_iff [simp]:
- "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)" for k l :: int
- by (cases "k \<ge> 0") (simp_all add: ac_simps)
-
-lemma even_add_abs_iff [simp]:
- "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)" for k l :: int
- using even_abs_add_iff [of l k] by (simp add: ac_simps)
-
-lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
- by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric])
-
subsubsection \<open>Laws for div and mod with Unary Minus\<close>
@@ -697,14 +572,14 @@
by (simp add: mod_eq_0_iff_dvd)
lemma zdiv_zminus2_eq_if:
- "b \<noteq> (0::int)
+ "b \<noteq> (0::int)
==> a div (-b) =
(if a mod b = 0 then - (a div b) else - (a div b) - 1)"
-by (simp add: zdiv_zminus1_eq_if div_minus_right)
+ by (auto simp add: zdiv_zminus1_eq_if div_minus_right)
lemma zmod_zminus2_eq_if:
- "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)
+ "a mod (-b::int) = (if a mod b = 0 then 0 else (a mod b) - b)"
+ by (auto simp add: zmod_zminus1_eq_if mod_minus_right)
subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
@@ -1161,11 +1036,17 @@
lemma minus_numeral_mod_numeral [simp]:
"- numeral m mod numeral n = adjust_mod (numeral n) (snd (divmod m n) :: int)"
-proof -
- have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
- using that by (simp only: snd_divmod modulo_int_def) auto
+proof (cases "snd (divmod m n) = (0::int)")
+ case True
then show ?thesis
- by (auto simp add: split_def Let_def adjust_div_def divides_aux_def modulo_int_def)
+ by (simp add: mod_eq_0_iff_dvd divides_aux_def)
+next
+ case False
+ then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
+ by (simp only: snd_divmod modulo_int_def) auto
+ then show ?thesis
+ by (simp add: divides_aux_def adjust_div_def)
+ (simp add: divides_aux_def modulo_int_def)
qed
lemma numeral_div_minus_numeral [simp]:
@@ -1179,11 +1060,17 @@
lemma numeral_mod_minus_numeral [simp]:
"numeral m mod - numeral n = - adjust_mod (numeral n) (snd (divmod m n) :: int)"
-proof -
- have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
- using that by (simp only: snd_divmod modulo_int_def) auto
+proof (cases "snd (divmod m n) = (0::int)")
+ case True
then show ?thesis
- by (auto simp add: split_def Let_def adjust_div_def divides_aux_def modulo_int_def)
+ by (simp add: mod_eq_0_iff_dvd divides_aux_def)
+next
+ case False
+ then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)"
+ by (simp only: snd_divmod modulo_int_def) auto
+ then show ?thesis
+ by (simp add: divides_aux_def adjust_div_def)
+ (simp add: divides_aux_def modulo_int_def)
qed
lemma minus_one_div_numeral [simp]:
@@ -1461,6 +1348,10 @@
lemma even_int_iff [simp]: "even (int n) \<longleftrightarrow> even n"
by (fact even_of_nat)
+lemma is_unit_int:
+ "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
+ by auto
+
text \<open>Tool setup\<close>
declare transfer_morphism_int_nat [transfer add return: even_int_iff]
--- a/src/HOL/Euclidean_Division.thy Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Euclidean_Division.thy Sun Oct 08 22:28:22 2017 +0200
@@ -704,7 +704,7 @@
subsection \<open>Euclidean division on @{typ nat}\<close>
-instantiation nat :: unique_euclidean_semiring
+instantiation nat :: normalization_semidom
begin
definition normalize_nat :: "nat \<Rightarrow> nat"
@@ -718,15 +718,23 @@
"unit_factor (Suc n) = 1"
by (simp_all add: unit_factor_nat_def)
+definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+ where "m div n = (if n = 0 then 0 else Max {k::nat. k * n \<le> m})"
+
+instance
+ by standard (auto simp add: divide_nat_def ac_simps unit_factor_nat_def intro: Max_eqI)
+
+end
+
+instantiation nat :: unique_euclidean_semiring
+begin
+
definition euclidean_size_nat :: "nat \<Rightarrow> nat"
where [simp]: "euclidean_size_nat = id"
definition uniqueness_constraint_nat :: "nat \<Rightarrow> nat \<Rightarrow> bool"
where [simp]: "uniqueness_constraint_nat = \<top>"
-definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
- where "m div n = (if n = 0 then 0 else Max {k::nat. k * n \<le> m})"
-
definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
where "m mod n = m - (m div n * (n::nat))"
@@ -757,15 +765,11 @@
finally show ?thesis
using False by (simp add: divide_nat_def ac_simps)
qed
- show "n div 0 = 0"
- by (simp add: divide_nat_def)
have less_eq: "m div n * n \<le> m"
by (auto simp add: mult_div_unfold ac_simps intro: Max.boundedI)
then show "m div n * n + m mod n = m"
by (simp add: modulo_nat_def)
assume "n \<noteq> 0"
- show "m * n div n = m"
- using \<open>n \<noteq> 0\<close> by (auto simp add: divide_nat_def ac_simps intro: Max_eqI)
show "euclidean_size (m mod n) < euclidean_size n"
proof -
have "m < Suc (m div n) * n"
@@ -805,7 +809,7 @@
with \<open>n \<noteq> 0\<close> ex fin show ?thesis
by (auto simp add: divide_nat_def Max_eq_iff)
qed
-qed (simp_all add: unit_factor_nat_def)
+qed simp_all
end
@@ -1329,6 +1333,186 @@
qed
+subsection \<open>Euclidean division on @{typ int}\<close>
+
+instantiation int :: normalization_semidom
+begin
+
+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 then 0
+ else if sgn k = sgn l
+ then int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
+ else - int (nat \<bar>k\<bar> div nat \<bar>l\<bar> + of_bool (\<not> l dvd k)))"
+
+lemma divide_int_unfold:
+ "(sgn k * int m) div (sgn l * int n) =
+ (if sgn l = 0 \<or> sgn k = 0 \<or> n = 0 then 0
+ else if sgn k = sgn l
+ then int (m div n)
+ else - int (m div n + of_bool (\<not> n dvd m)))"
+ by (auto simp add: divide_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
+ nat_mult_distrib dvd_int_iff)
+
+instance proof
+ fix k :: int show "k div 0 = 0"
+ by (simp add: divide_int_def)
+next
+ fix k l :: int
+ assume "l \<noteq> 0"
+ obtain n m and s t where k: "k = sgn s * int n" and l: "l = sgn t * int m"
+ by (blast intro: int_sgnE elim: that)
+ then have "k * l = sgn (s * t) * int (n * m)"
+ by (simp add: ac_simps sgn_mult)
+ with k l \<open>l \<noteq> 0\<close> show "k * l div l = k"
+ by (simp only: divide_int_unfold)
+ (auto simp add: algebra_simps sgn_mult sgn_1_pos sgn_0_0)
+qed (auto simp add: sgn_mult mult_sgn_abs abs_eq_iff')
+
+end
+
+instantiation int :: unique_euclidean_ring
+begin
+
+definition euclidean_size_int :: "int \<Rightarrow> nat"
+ where [simp]: "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
+
+definition uniqueness_constraint_int :: "int \<Rightarrow> int \<Rightarrow> bool"
+ where [simp]: "uniqueness_constraint_int k l \<longleftrightarrow> unit_factor k = unit_factor l"
+
+definition modulo_int :: "int \<Rightarrow> int \<Rightarrow> int"
+ where "k mod l = (if l = 0 then k
+ else if sgn k = sgn l
+ then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
+ else sgn l * (\<bar>l\<bar> * of_bool (\<not> l dvd k) - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
+
+lemma modulo_int_unfold:
+ "(sgn k * int m) mod (sgn l * int n) =
+ (if sgn l = 0 \<or> sgn k = 0 \<or> n = 0 then sgn k * int m
+ else if sgn k = sgn l
+ then sgn l * int (m mod n)
+ else sgn l * (int (n * of_bool (\<not> n dvd m)) - int (m mod n)))"
+ by (auto simp add: modulo_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
+ nat_mult_distrib dvd_int_iff)
+
+lemma abs_mod_less:
+ "\<bar>k mod l\<bar> < \<bar>l\<bar>" if "l \<noteq> 0" for k l :: int
+proof -
+ obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m"
+ by (blast intro: int_sgnE elim: that)
+ with that show ?thesis
+ by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg
+ abs_mult mod_greater_zero_iff_not_dvd)
+qed
+
+lemma sgn_mod:
+ "sgn (k mod l) = sgn l" if "l \<noteq> 0" "\<not> l dvd k" for k l :: int
+proof -
+ obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m"
+ by (blast intro: int_sgnE elim: that)
+ with that show ?thesis
+ by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg
+ sgn_mult mod_eq_0_iff_dvd int_dvd_iff)
+qed
+
+instance proof
+ fix k l :: int
+ obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m"
+ by (blast intro: int_sgnE elim: that)
+ then show "k div l * l + k mod l = k"
+ by (auto simp add: divide_int_unfold modulo_int_unfold algebra_simps dest!: sgn_not_eq_imp)
+ (simp_all add: of_nat_mult [symmetric] of_nat_add [symmetric]
+ distrib_left [symmetric] minus_mult_right
+ del: of_nat_mult minus_mult_right [symmetric])
+next
+ fix l q r :: int
+ obtain n m and s t
+ where l: "l = sgn s * int n" and q: "q = sgn t * int m"
+ by (blast intro: int_sgnE elim: that)
+ assume \<open>l \<noteq> 0\<close>
+ with l have "s \<noteq> 0" and "n > 0"
+ by (simp_all add: sgn_0_0)
+ assume "uniqueness_constraint r l"
+ moreover have "r = sgn r * \<bar>r\<bar>"
+ by (simp add: sgn_mult_abs)
+ moreover define u where "u = nat \<bar>r\<bar>"
+ ultimately have "r = sgn l * int u"
+ by simp
+ with l \<open>n > 0\<close> have r: "r = sgn s * int u"
+ by (simp add: sgn_mult)
+ assume "euclidean_size r < euclidean_size l"
+ with l r \<open>s \<noteq> 0\<close> have "u < n"
+ by (simp add: abs_mult)
+ show "(q * l + r) div l = q"
+ proof (cases "q = 0 \<or> r = 0")
+ case True
+ then show ?thesis
+ proof
+ assume "q = 0"
+ then show ?thesis
+ using l r \<open>u < n\<close> by (simp add: divide_int_unfold)
+ next
+ assume "r = 0"
+ from \<open>r = 0\<close> have *: "q * l + r = sgn (t * s) * int (n * m)"
+ using q l by (simp add: ac_simps sgn_mult)
+ from \<open>s \<noteq> 0\<close> \<open>n > 0\<close> show ?thesis
+ by (simp only: *, simp only: q l divide_int_unfold)
+ (auto simp add: sgn_mult sgn_0_0 sgn_1_pos)
+ qed
+ next
+ case False
+ with q r have "t \<noteq> 0" and "m > 0" and "s \<noteq> 0" and "u > 0"
+ by (simp_all add: sgn_0_0)
+ moreover from \<open>0 < m\<close> \<open>u < n\<close> have "u \<le> m * n"
+ using mult_le_less_imp_less [of 1 m u n] by simp
+ ultimately have *: "q * l + r = sgn (s * t)
+ * int (if t < 0 then m * n - u else m * n + u)"
+ using l q r
+ by (simp add: sgn_mult algebra_simps of_nat_diff)
+ have "(m * n - u) div n = m - 1" if "u > 0"
+ using \<open>0 < m\<close> \<open>u < n\<close> that
+ by (auto intro: div_nat_eqI simp add: algebra_simps)
+ moreover have "n dvd m * n - u \<longleftrightarrow> n dvd u"
+ using \<open>u \<le> m * n\<close> dvd_diffD1 [of n "m * n" u]
+ by auto
+ ultimately show ?thesis
+ using \<open>s \<noteq> 0\<close> \<open>m > 0\<close> \<open>u > 0\<close> \<open>u < n\<close> \<open>u \<le> m * n\<close>
+ by (simp only: *, simp only: l q divide_int_unfold)
+ (auto simp add: sgn_mult sgn_0_0 sgn_1_pos algebra_simps dest: dvd_imp_le)
+ qed
+qed (use mult_le_mono2 [of 1] in \<open>auto simp add: abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>)
+
+end
+
+lemma pos_mod_bound [simp]:
+ "k mod l < l" if "l > 0" for k l :: int
+proof -
+ obtain m and s where "k = sgn s * int m"
+ by (blast intro: int_sgnE elim: that)
+ moreover from that obtain n where "l = sgn 1 * int n"
+ by (cases l) auto
+ ultimately show ?thesis
+ using that by (simp only: modulo_int_unfold)
+ (simp add: mod_greater_zero_iff_not_dvd)
+qed
+
+lemma pos_mod_sign [simp]:
+ "0 \<le> k mod l" if "l > 0" for k l :: int
+proof -
+ obtain m and s where "k = sgn s * int m"
+ by (blast intro: int_sgnE elim: that)
+ moreover from that obtain n where "l = sgn 1 * int n"
+ by (cases l) auto
+ ultimately show ?thesis
+ using that by (simp only: modulo_int_unfold) simp
+qed
+
+
subsection \<open>Code generation\<close>
code_identifier
--- a/src/HOL/GCD.thy Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/GCD.thy Sun Oct 08 22:28:22 2017 +0200
@@ -2017,11 +2017,11 @@
lemma gcd_non_0_int: "y > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
for x y :: int
apply (frule_tac b = y and a = x in pos_mod_sign)
- apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
+ apply (simp del: Euclidean_Division.pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
apply (frule_tac a = x in pos_mod_bound)
apply (subst (1 2) gcd.commute)
- apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat nat_le_eq_zle)
+ apply (simp del: Euclidean_Division.pos_mod_bound add: nat_diff_distrib gcd_diff2_nat nat_le_eq_zle)
done
lemma gcd_red_int: "gcd x y = gcd y (x mod y)"
--- a/src/HOL/Int.thy Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Int.thy Sun Oct 08 22:28:22 2017 +0200
@@ -255,6 +255,10 @@
lemma of_int_power [simp]: "of_int (z ^ n) = of_int z ^ n"
by (induct n) simp_all
+lemma of_int_of_bool [simp]:
+ "of_int (of_bool P) = of_bool P"
+ by auto
+
end
context ring_char_0
@@ -548,6 +552,10 @@
lemma diff_nat_numeral [simp]: "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
+lemma nat_of_bool [simp]:
+ "nat (of_bool P) = of_bool P"
+ by auto
+
text \<open>For termination proofs:\<close>
lemma measure_function_int[measure_function]: "is_measure (nat \<circ> abs)" ..
@@ -668,6 +676,31 @@
\<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
by (fact Let_neg_numeral) \<comment> \<open>FIXME drop\<close>
+lemma sgn_mult_dvd_iff [simp]:
+ "sgn r * l dvd k \<longleftrightarrow> l dvd k \<and> (r = 0 \<longrightarrow> k = 0)" for k l r :: int
+ by (cases r rule: int_cases3) auto
+
+lemma mult_sgn_dvd_iff [simp]:
+ "l * sgn r dvd k \<longleftrightarrow> l dvd k \<and> (r = 0 \<longrightarrow> k = 0)" for k l r :: int
+ using sgn_mult_dvd_iff [of r l k] by (simp add: ac_simps)
+
+lemma dvd_sgn_mult_iff [simp]:
+ "l dvd sgn r * k \<longleftrightarrow> l dvd k \<or> r = 0" for k l r :: int
+ by (cases r rule: int_cases3) simp_all
+
+lemma dvd_mult_sgn_iff [simp]:
+ "l dvd k * sgn r \<longleftrightarrow> l dvd k \<or> r = 0" for k l r :: int
+ using dvd_sgn_mult_iff [of l r k] by (simp add: ac_simps)
+
+lemma int_sgnE:
+ fixes k :: int
+ obtains n and l where "k = sgn l * int n"
+proof -
+ have "k = sgn k * int (nat \<bar>k\<bar>)"
+ by (simp add: sgn_mult_abs)
+ then show ?thesis ..
+qed
+
text \<open>Unfold \<open>min\<close> and \<open>max\<close> on numerals.\<close>
lemmas max_number_of [simp] =
@@ -1629,19 +1662,10 @@
shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
(is "?lhs \<longleftrightarrow> ?rhs")
proof -
- from assms obtain k where "d = a * k" by (rule dvdE)
- show ?thesis
- proof
- assume ?lhs
- then obtain l where "x + t = a * l" by (rule dvdE)
- then have "x = a * l - t" by simp
- with \<open>d = a * k\<close> show ?rhs by simp
- next
- assume ?rhs
- then obtain l where "x + c * d + t = a * l" by (rule dvdE)
- then have "x = a * l - c * d - t" by simp
- with \<open>d = a * k\<close> show ?lhs by simp
- qed
+ from assms have "a dvd (x + t) \<longleftrightarrow> a dvd ((x + t) + c * d)"
+ by (simp add: dvd_add_left_iff)
+ then show ?thesis
+ by (simp add: ac_simps)
qed
--- a/src/HOL/Nat.thy Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Nat.thy Sun Oct 08 22:28:22 2017 +0200
@@ -1676,6 +1676,10 @@
by (simp add: add.commute)
qed
+lemma of_nat_of_bool [simp]:
+ "of_nat (of_bool P) = of_bool P"
+ by auto
+
end
declare of_nat_code [code]
@@ -1764,6 +1768,10 @@
lemma abs_of_nat [simp]: "\<bar>of_nat n\<bar> = of_nat n"
unfolding abs_if by auto
+lemma sgn_of_nat [simp]:
+ "sgn (of_nat n) = of_bool (n > 0)"
+ by simp
+
end
lemma of_nat_id [simp]: "of_nat n = n"
--- a/src/HOL/Parity.thy Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Parity.thy Sun Oct 08 22:28:22 2017 +0200
@@ -483,4 +483,40 @@
end
+
+subsection \<open>Instance for @{typ int}\<close>
+
+instance int :: ring_parity
+proof
+ fix k l :: int
+ show "k mod 2 = 1" if "\<not> 2 dvd k"
+ proof (rule order_antisym)
+ have "0 \<le> k mod 2" and "k mod 2 < 2"
+ by auto
+ moreover have "k mod 2 \<noteq> 0"
+ using that by (simp add: dvd_eq_mod_eq_0)
+ ultimately have "0 < k mod 2"
+ by (simp only: less_le) simp
+ then show "1 \<le> k mod 2"
+ by simp
+ from \<open>k mod 2 < 2\<close> show "k mod 2 \<le> 1"
+ by (simp only: less_le) simp
+ qed
+qed (simp_all add: dvd_eq_mod_eq_0 divide_int_def)
+
+lemma even_diff_iff [simp]:
+ "even (k - l) \<longleftrightarrow> even (k + l)" for k l :: int
+ using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
+
+lemma even_abs_add_iff [simp]:
+ "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)" for k l :: int
+ by (cases "k \<ge> 0") (simp_all add: ac_simps)
+
+lemma even_add_abs_iff [simp]:
+ "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)" for k l :: int
+ using even_abs_add_iff [of l k] by (simp add: ac_simps)
+
+lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
+ by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric])
+
end
--- a/src/HOL/Rings.thy Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Rings.thy Sun Oct 08 22:28:22 2017 +0200
@@ -118,6 +118,13 @@
end
class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
+begin
+
+lemma (in semiring_1) of_bool_conj:
+ "of_bool (P \<and> Q) = of_bool P * of_bool Q"
+ by auto
+
+end
text \<open>Abstract divisibility\<close>
@@ -2319,6 +2326,10 @@
by (auto simp add: abs_mult)
qed
+lemma sgn_not_eq_imp:
+ "sgn a = - sgn b" if "sgn b \<noteq> sgn a" and "sgn a \<noteq> 0" and "sgn b \<noteq> 0"
+ using that by (cases "a < 0") (auto simp add: sgn_0_0 sgn_1_pos sgn_1_neg)
+
lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
by (simp add: abs_if)