--- a/src/HOL/Code_Numeral.thy Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Code_Numeral.thy Sun Oct 08 22:28:22 2017 +0200
@@ -282,6 +282,9 @@
"uniqueness_constraint (k :: integer) l \<longleftrightarrow> unit_factor k = unit_factor l"
by (simp add: integer_eq_iff)
+instance integer :: ring_parity
+ by (standard; transfer) (simp_all add: of_nat_div odd_iff_mod_2_eq_one)
+
instantiation integer :: unique_euclidean_semiring_numeral
begin
@@ -927,6 +930,9 @@
"uniqueness_constraint = (\<top> :: natural \<Rightarrow> natural \<Rightarrow> bool)"
by (simp add: fun_eq_iff)
+instance natural :: semiring_parity
+ by (standard; transfer) (simp_all add: of_nat_div odd_iff_mod_2_eq_one)
+
lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
is "nat :: int \<Rightarrow> nat"
.
--- 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
@@ -6,7 +6,7 @@
section \<open>More on quotient and remainder\<close>
theory Divides
-imports Parity
+imports Parity Nat_Transfer
begin
subsection \<open>Numeral division with a pragmatic type class\<close>
@@ -19,7 +19,7 @@
and less technical class hierarchy.
\<close>
-class unique_euclidean_semiring_numeral = unique_euclidean_semiring + linordered_semidom +
+class unique_euclidean_semiring_numeral = semiring_parity + linordered_semidom +
assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
@@ -40,29 +40,6 @@
yields a significant speedup.\<close>
begin
-subclass unique_euclidean_semiring_parity
-proof
- fix a
- show "a mod 2 = 0 \<or> a mod 2 = 1"
- proof (rule ccontr)
- assume "\<not> (a mod 2 = 0 \<or> a mod 2 = 1)"
- then have "a mod 2 \<noteq> 0" and "a mod 2 \<noteq> 1" by simp_all
- have "0 < 2" by simp
- with pos_mod_bound pos_mod_sign have "0 \<le> a mod 2" "a mod 2 < 2" by simp_all
- with \<open>a mod 2 \<noteq> 0\<close> have "0 < a mod 2" by simp
- with discrete have "1 \<le> a mod 2" by simp
- with \<open>a mod 2 \<noteq> 1\<close> have "1 < a mod 2" by simp
- with discrete have "2 \<le> a mod 2" by simp
- with \<open>a mod 2 < 2\<close> show False by simp
- qed
-next
- show "1 mod 2 = 1"
- by (rule mod_less) simp_all
-next
- show "0 \<noteq> 2"
- by simp
-qed
-
lemma divmod_digit_1:
assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)"
shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")
@@ -74,7 +51,7 @@
then have [simp]: "1 \<le> a div b" by (simp add: discrete)
with \<open>0 < b\<close> have mod_less: "a mod b < b" by (simp add: pos_mod_bound)
define w where "w = a div b mod 2"
- with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
+ then have w_exhaust: "w = 0 \<or> w = 1" by auto
have mod_w: "a mod (2 * b) = a mod b + b * w"
by (simp add: w_def mod_mult2_eq ac_simps)
from assms w_exhaust have "w = 1"
@@ -93,7 +70,7 @@
and "a mod (2 * b) = a mod b" (is "?Q")
proof -
define w where "w = a div b mod 2"
- with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
+ then have w_exhaust: "w = 0 \<or> w = 1" by auto
have mod_w: "a mod (2 * b) = a mod b + b * w"
by (simp add: w_def mod_mult2_eq ac_simps)
moreover have "b \<le> a mod b + b"
@@ -318,60 +295,6 @@
declare divmod_algorithm_code [where ?'a = nat, code]
-lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
- by (auto elim: oddE)
-
-lemma even_Suc_div_two [simp]:
- "even n \<Longrightarrow> Suc n div 2 = n div 2"
- using even_succ_div_two [of n] by simp
-
-lemma odd_Suc_div_two [simp]:
- "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
- using odd_succ_div_two [of n] by simp
-
-lemma odd_two_times_div_two_nat [simp]:
- assumes "odd n"
- shows "2 * (n div 2) = n - (1 :: nat)"
-proof -
- from assms have "2 * (n div 2) + 1 = n"
- by (rule odd_two_times_div_two_succ)
- then have "Suc (2 * (n div 2)) - 1 = n - 1"
- by simp
- then show ?thesis
- by simp
-qed
-
-lemma parity_induct [case_names zero even odd]:
- assumes zero: "P 0"
- assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
- assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
- shows "P n"
-proof (induct n rule: less_induct)
- case (less n)
- show "P n"
- proof (cases "n = 0")
- case True with zero show ?thesis by simp
- next
- case False
- with less have hyp: "P (n div 2)" by simp
- show ?thesis
- proof (cases "even n")
- case True
- with hyp even [of "n div 2"] show ?thesis
- by simp
- next
- case False
- with hyp odd [of "n div 2"] show ?thesis
- by simp
- qed
- qed
-qed
-
-lemma mod_2_not_eq_zero_eq_one_nat:
- fixes n :: nat
- shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
- by (fact not_mod_2_eq_0_eq_1)
-
lemma Suc_0_div_numeral [simp]:
fixes k l :: num
shows "Suc 0 div numeral k = fst (divmod Num.One k)"
@@ -708,6 +631,39 @@
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>
@@ -1495,4 +1451,18 @@
then show ?thesis ..
qed
+lemmas even_times_iff = even_mult_iff -- \<open>FIXME duplicate\<close>
+
+lemma mod_2_not_eq_zero_eq_one_nat:
+ fixes n :: nat
+ shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
+ by (fact not_mod_2_eq_0_eq_1)
+
+lemma even_int_iff [simp]: "even (int n) \<longleftrightarrow> even n"
+ by (fact even_of_nat)
+
+text \<open>Tool setup\<close>
+
+declare transfer_morphism_int_nat [transfer add return: even_int_iff]
+
end
--- a/src/HOL/Nonstandard_Analysis/StarDef.thy Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy Sun Oct 08 22:28:22 2017 +0200
@@ -834,6 +834,10 @@
end
+instance star :: (semidom_modulo) semidom_modulo
+ by standard (transfer; simp)
+
+
subsection \<open>Power\<close>
@@ -917,14 +921,6 @@
instance star :: (ring_char_0) ring_char_0 ..
-instance star :: (semiring_parity) semiring_parity
- apply intro_classes
- apply (transfer, rule odd_one)
- apply (transfer, erule (1) odd_even_add)
- apply (transfer, erule even_multD)
- apply (transfer, erule odd_ex_decrement)
- done
-
subsection \<open>Finite class\<close>
--- a/src/HOL/NthRoot.thy Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/NthRoot.thy Sun Oct 08 22:28:22 2017 +0200
@@ -218,7 +218,7 @@
lemma real_root_inverse: "root n (inverse x) = inverse (root n x)"
by (auto split: split_root elim!: sgn_power_injE
- simp: inverse_sgn power_inverse)
+ simp: power_inverse)
lemma real_root_divide: "root n (x / y) = root n x / root n y"
by (simp add: divide_inverse real_root_mult real_root_inverse)
@@ -715,7 +715,7 @@
have "x n \<le> sqrt (2 / real n)" if "2 < n" for n :: nat
proof -
have "1 + (real (n - 1) * n) / 2 * (x n)\<^sup>2 = 1 + of_nat (n choose 2) * (x n)\<^sup>2"
- by (auto simp add: choose_two of_nat_div mod_eq_0_iff_dvd)
+ by (auto simp add: choose_two field_char_0_class.of_nat_div mod_eq_0_iff_dvd)
also have "\<dots> \<le> (\<Sum>k\<in>{0, 2}. of_nat (n choose k) * x n^k)"
by (simp add: x_def)
also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
--- 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
@@ -6,19 +6,73 @@
section \<open>Parity in rings and semirings\<close>
theory Parity
- imports Nat_Transfer Euclidean_Division
+ imports Euclidean_Division
begin
subsection \<open>Ring structures with parity and \<open>even\<close>/\<open>odd\<close> predicates\<close>
-class semiring_parity = comm_semiring_1_cancel + numeral +
- assumes odd_one [simp]: "\<not> 2 dvd 1"
- assumes odd_even_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b"
- assumes even_multD: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b"
- assumes odd_ex_decrement: "\<not> 2 dvd a \<Longrightarrow> \<exists>b. a = b + 1"
+class semiring_parity = linordered_semidom + unique_euclidean_semiring +
+ assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n"
+ and odd_imp_mod_2_eq_1: "\<not> 2 dvd a \<Longrightarrow> a mod 2 = 1"
+
+context semiring_parity
begin
-subclass semiring_numeral ..
+lemma of_nat_dvd_iff:
+ "of_nat m dvd of_nat n \<longleftrightarrow> m dvd n" (is "?P \<longleftrightarrow> ?Q")
+proof (cases "m = 0")
+ case True
+ then show ?thesis
+ by simp
+next
+ case False
+ show ?thesis
+ proof
+ assume ?Q
+ then show ?P
+ by (auto elim: dvd_class.dvdE)
+ next
+ assume ?P
+ with False have "of_nat n = of_nat n div of_nat m * of_nat m"
+ by simp
+ then have "of_nat n = of_nat (n div m * m)"
+ by (simp add: of_nat_div)
+ then have "n = n div m * m"
+ by (simp only: of_nat_eq_iff)
+ then have "n = m * (n div m)"
+ by (simp add: ac_simps)
+ then show ?Q ..
+ qed
+qed
+
+lemma of_nat_mod:
+ "of_nat (m mod n) = of_nat m mod of_nat n"
+proof -
+ have "of_nat m div of_nat n * of_nat n + of_nat m mod of_nat n = of_nat m"
+ by (simp add: div_mult_mod_eq)
+ also have "of_nat m = of_nat (m div n * n + m mod n)"
+ by simp
+ finally show ?thesis
+ by (simp only: of_nat_div of_nat_mult of_nat_add) simp
+qed
+
+lemma one_div_two_eq_zero [simp]:
+ "1 div 2 = 0"
+proof -
+ from of_nat_div [symmetric] have "of_nat 1 div of_nat 2 = of_nat 0"
+ by (simp only:) simp
+ then show ?thesis
+ by simp
+qed
+
+lemma one_mod_two_eq_one [simp]:
+ "1 mod 2 = 1"
+proof -
+ from of_nat_mod [symmetric] have "of_nat 1 mod of_nat 2 = of_nat 1"
+ by (simp only:) simp
+ then show ?thesis
+ by simp
+qed
abbreviation even :: "'a \<Rightarrow> bool"
where "even a \<equiv> 2 dvd a"
@@ -26,11 +80,27 @@
abbreviation odd :: "'a \<Rightarrow> bool"
where "odd a \<equiv> \<not> 2 dvd a"
-lemma even_zero [simp]: "even 0"
- by (fact dvd_0_right)
+lemma even_iff_mod_2_eq_zero:
+ "even a \<longleftrightarrow> a mod 2 = 0"
+ by (fact dvd_eq_mod_eq_0)
+
+lemma odd_iff_mod_2_eq_one:
+ "odd a \<longleftrightarrow> a mod 2 = 1"
+ by (auto dest: odd_imp_mod_2_eq_1)
-lemma even_plus_one_iff [simp]: "even (a + 1) \<longleftrightarrow> odd a"
- by (auto simp add: dvd_add_right_iff intro: odd_even_add)
+lemma parity_cases [case_names even odd]:
+ assumes "even a \<Longrightarrow> a mod 2 = 0 \<Longrightarrow> P"
+ assumes "odd a \<Longrightarrow> a mod 2 = 1 \<Longrightarrow> P"
+ shows P
+ using assms by (cases "even a") (simp_all add: odd_iff_mod_2_eq_one)
+
+lemma not_mod_2_eq_1_eq_0 [simp]:
+ "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
+ by (cases a rule: parity_cases) simp_all
+
+lemma not_mod_2_eq_0_eq_1 [simp]:
+ "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
+ by (cases a rule: parity_cases) simp_all
lemma evenE [elim?]:
assumes "even a"
@@ -41,22 +111,107 @@
assumes "odd a"
obtains b where "a = 2 * b + 1"
proof -
- from assms obtain b where *: "a = b + 1"
- by (blast dest: odd_ex_decrement)
- with assms have "even (b + 2)" by simp
- then have "even b" by simp
- then obtain c where "b = 2 * c" ..
- with * have "a = 2 * c + 1" by simp
- with that show thesis .
+ have "a = 2 * (a div 2) + a mod 2"
+ by (simp add: mult_div_mod_eq)
+ with assms have "a = 2 * (a div 2) + 1"
+ by (simp add: odd_iff_mod_2_eq_one)
+ then show ?thesis ..
+qed
+
+lemma mod_2_eq_odd:
+ "a mod 2 = of_bool (odd a)"
+ by (auto elim: oddE)
+
+lemma one_mod_2_pow_eq [simp]:
+ "1 mod (2 ^ n) = of_bool (n > 0)"
+proof -
+ have "1 mod (2 ^ n) = (of_bool (n > 0) :: nat)"
+ by (induct n) (simp_all add: mod_mult2_eq)
+ then have "of_nat (1 mod (2 ^ n)) = of_bool (n > 0)"
+ by simp
+ then show ?thesis
+ by (simp add: of_nat_mod)
+qed
+
+lemma even_of_nat [simp]:
+ "even (of_nat a) \<longleftrightarrow> even a"
+proof -
+ have "even (of_nat a) \<longleftrightarrow> of_nat 2 dvd of_nat a"
+ by simp
+ also have "\<dots> \<longleftrightarrow> even a"
+ by (simp only: of_nat_dvd_iff)
+ finally show ?thesis .
+qed
+
+lemma even_zero [simp]:
+ "even 0"
+ by (fact dvd_0_right)
+
+lemma odd_one [simp]:
+ "odd 1"
+proof -
+ have "\<not> (2 :: nat) dvd 1"
+ by simp
+ then have "\<not> of_nat 2 dvd of_nat 1"
+ unfolding of_nat_dvd_iff by simp
+ then show ?thesis
+ by simp
qed
-lemma even_times_iff [simp]: "even (a * b) \<longleftrightarrow> even a \<or> even b"
- by (auto dest: even_multD)
+lemma odd_even_add:
+ "even (a + b)" if "odd a" and "odd b"
+proof -
+ from that obtain c d where "a = 2 * c + 1" and "b = 2 * d + 1"
+ by (blast elim: oddE)
+ then have "a + b = 2 * c + 2 * d + (1 + 1)"
+ by (simp only: ac_simps)
+ also have "\<dots> = 2 * (c + d + 1)"
+ by (simp add: algebra_simps)
+ finally show ?thesis ..
+qed
+
+lemma even_add [simp]:
+ "even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)"
+ by (auto simp add: dvd_add_right_iff dvd_add_left_iff odd_even_add)
+
+lemma odd_add [simp]:
+ "odd (a + b) \<longleftrightarrow> \<not> (odd a \<longleftrightarrow> odd b)"
+ by simp
+
+lemma even_plus_one_iff [simp]:
+ "even (a + 1) \<longleftrightarrow> odd a"
+ by (auto simp add: dvd_add_right_iff intro: odd_even_add)
+
+lemma even_mult_iff [simp]:
+ "even (a * b) \<longleftrightarrow> even a \<or> even b" (is "?P \<longleftrightarrow> ?Q")
+proof
+ assume ?Q
+ then show ?P
+ by auto
+next
+ assume ?P
+ show ?Q
+ proof (rule ccontr)
+ assume "\<not> (even a \<or> even b)"
+ then have "odd a" and "odd b"
+ by auto
+ then obtain r s where "a = 2 * r + 1" and "b = 2 * s + 1"
+ by (blast elim: oddE)
+ then have "a * b = (2 * r + 1) * (2 * s + 1)"
+ by simp
+ also have "\<dots> = 2 * (2 * r * s + r + s) + 1"
+ by (simp add: algebra_simps)
+ finally have "odd (a * b)"
+ by simp
+ with \<open>?P\<close> show False
+ by auto
+ qed
+qed
lemma even_numeral [simp]: "even (numeral (Num.Bit0 n))"
proof -
have "even (2 * numeral n)"
- unfolding even_times_iff by simp
+ unfolding even_mult_iff by simp
then have "even (numeral n + numeral n)"
unfolding mult_2 .
then show ?thesis
@@ -77,15 +232,26 @@
then show False by simp
qed
-lemma even_add [simp]: "even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)"
- by (auto simp add: dvd_add_right_iff dvd_add_left_iff odd_even_add)
-
-lemma odd_add [simp]: "odd (a + b) \<longleftrightarrow> (\<not> (odd a \<longleftrightarrow> odd b))"
- by simp
-
lemma even_power [simp]: "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0"
by (induct n) auto
+lemma even_succ_div_two [simp]:
+ "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
+ by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
+
+lemma odd_succ_div_two [simp]:
+ "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
+ by (auto elim!: oddE simp add: add.assoc)
+
+lemma even_two_times_div_two:
+ "even a \<Longrightarrow> 2 * (a div 2) = a"
+ by (fact dvd_mult_div_cancel)
+
+lemma odd_two_times_div_two_succ [simp]:
+ "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
+ using mult_div_mod_eq [of 2 a]
+ by (simp add: even_iff_mod_2_eq_zero)
+
end
class ring_parity = ring + semiring_parity
@@ -93,166 +259,48 @@
subclass comm_ring_1 ..
-lemma even_minus [simp]: "even (- a) \<longleftrightarrow> even a"
+lemma even_minus [simp]:
+ "even (- a) \<longleftrightarrow> even a"
by (fact dvd_minus_iff)
-lemma even_diff [simp]: "even (a - b) \<longleftrightarrow> even (a + b)"
+lemma even_diff [simp]:
+ "even (a - b) \<longleftrightarrow> even (a + b)"
using even_add [of a "- b"] by simp
end
-class unique_euclidean_semiring_parity = unique_euclidean_semiring +
- assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
- assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
- assumes zero_not_eq_two: "0 \<noteq> 2"
-begin
-lemma parity_cases [case_names even odd]:
- assumes "a mod 2 = 0 \<Longrightarrow> P"
- assumes "a mod 2 = 1 \<Longrightarrow> P"
- shows P
- using assms parity by blast
-
-lemma one_div_two_eq_zero [simp]:
- "1 div 2 = 0"
-proof (cases "2 = 0")
- case True then show ?thesis by simp
-next
- case False
- from div_mult_mod_eq have "1 div 2 * 2 + 1 mod 2 = 1" .
- with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
- then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)
- then have "1 div 2 = 0 \<or> 2 = 0" by simp
- with False show ?thesis by auto
-qed
-
-lemma not_mod_2_eq_0_eq_1 [simp]:
- "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
- by (cases a rule: parity_cases) simp_all
-
-lemma not_mod_2_eq_1_eq_0 [simp]:
- "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
- by (cases a rule: parity_cases) simp_all
+subsection \<open>Instance for @{typ nat}\<close>
-subclass semiring_parity
-proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
- show "1 mod 2 = 1"
- by (fact one_mod_two_eq_one)
-next
- fix a b
- assume "a mod 2 = 1"
- moreover assume "b mod 2 = 1"
- ultimately show "(a + b) mod 2 = 0"
- using mod_add_eq [of a 2 b] by simp
-next
- fix a b
- assume "(a * b) mod 2 = 0"
- then have "(a mod 2) * (b mod 2) mod 2 = 0"
- by (simp add: mod_mult_eq)
- then have "(a mod 2) * (b mod 2) = 0"
- by (cases "a mod 2 = 0") simp_all
- then show "a mod 2 = 0 \<or> b mod 2 = 0"
- by (rule divisors_zero)
-next
- fix a
- assume "a mod 2 = 1"
- then have "a = a div 2 * 2 + 1"
- using div_mult_mod_eq [of a 2] by simp
- then show "\<exists>b. a = b + 1" ..
-qed
+instance nat :: semiring_parity
+ by standard (simp_all add: dvd_eq_mod_eq_0)
-lemma even_iff_mod_2_eq_zero:
- "even a \<longleftrightarrow> a mod 2 = 0"
- by (fact dvd_eq_mod_eq_0)
-
-lemma odd_iff_mod_2_eq_one:
- "odd a \<longleftrightarrow> a mod 2 = 1"
- by (simp add: even_iff_mod_2_eq_zero)
-
-lemma even_succ_div_two [simp]:
- "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
- by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
-
-lemma odd_succ_div_two [simp]:
- "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
- by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc)
-
-lemma even_two_times_div_two:
- "even a \<Longrightarrow> 2 * (a div 2) = a"
- by (fact dvd_mult_div_cancel)
-
-lemma odd_two_times_div_two_succ [simp]:
- "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
- using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
-
-end
-
-
-subsection \<open>Instances for @{typ nat} and @{typ int}\<close>
-
-lemma even_Suc_Suc_iff [simp]: "2 dvd Suc (Suc n) \<longleftrightarrow> 2 dvd n"
+lemma even_Suc_Suc_iff [simp]:
+ "even (Suc (Suc n)) \<longleftrightarrow> even n"
using dvd_add_triv_right_iff [of 2 n] by simp
-lemma even_Suc [simp]: "2 dvd Suc n \<longleftrightarrow> \<not> 2 dvd n"
- by (induct n) auto
+lemma even_Suc [simp]: "even (Suc n) \<longleftrightarrow> odd n"
+ using even_plus_one_iff [of n] by simp
-lemma even_diff_nat [simp]: "2 dvd (m - n) \<longleftrightarrow> m < n \<or> 2 dvd (m + n)"
- for m n :: nat
+lemma even_diff_nat [simp]:
+ "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)" for m n :: nat
proof (cases "n \<le> m")
case True
then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
- moreover have "2 dvd (m - n) \<longleftrightarrow> 2 dvd (m - n + n * 2)" by simp
- ultimately have "2 dvd (m - n) \<longleftrightarrow> 2 dvd (m + n)" by (simp only:)
+ moreover have "even (m - n) \<longleftrightarrow> even (m - n + n * 2)" by simp
+ ultimately have "even (m - n) \<longleftrightarrow> even (m + n)" by (simp only:)
then show ?thesis by auto
next
case False
then show ?thesis by simp
qed
-instance nat :: semiring_parity
-proof
- show "\<not> 2 dvd (1 :: nat)"
- by (rule notI, erule dvdE) simp
-next
- fix m n :: nat
- assume "\<not> 2 dvd m"
- moreover assume "\<not> 2 dvd n"
- ultimately have *: "2 dvd Suc m \<and> 2 dvd Suc n"
- by simp
- then have "2 dvd (Suc m + Suc n)"
- by (blast intro: dvd_add)
- also have "Suc m + Suc n = m + n + 2"
- by simp
- finally show "2 dvd (m + n)"
- using dvd_add_triv_right_iff [of 2 "m + n"] by simp
-next
- fix m n :: nat
- assume *: "2 dvd (m * n)"
- show "2 dvd m \<or> 2 dvd n"
- proof (rule disjCI)
- assume "\<not> 2 dvd n"
- then have "2 dvd (Suc n)" by simp
- then obtain r where "Suc n = 2 * r" ..
- moreover from * obtain s where "m * n = 2 * s" ..
- then have "2 * s + m = m * Suc n" by simp
- ultimately have " 2 * s + m = 2 * (m * r)"
- by (simp add: algebra_simps)
- then have "m = 2 * (m * r - s)" by simp
- then show "2 dvd m" ..
- qed
-next
- fix n :: nat
- assume "\<not> 2 dvd n"
- then show "\<exists>m. n = m + 1"
- by (cases n) simp_all
-qed
-
-lemma odd_pos: "odd n \<Longrightarrow> 0 < n"
- for n :: nat
+lemma odd_pos:
+ "odd n \<Longrightarrow> 0 < n" for n :: nat
by (auto elim: oddE)
-lemma Suc_double_not_eq_double: "Suc (2 * m) \<noteq> 2 * n"
- for m n :: nat
+lemma Suc_double_not_eq_double:
+ "Suc (2 * m) \<noteq> 2 * n"
proof
assume "Suc (2 * m) = 2 * n"
moreover have "odd (Suc (2 * m))" and "even (2 * n)"
@@ -260,52 +308,58 @@
ultimately show False by simp
qed
-lemma double_not_eq_Suc_double: "2 * m \<noteq> Suc (2 * n)"
- for m n :: nat
+lemma double_not_eq_Suc_double:
+ "2 * m \<noteq> Suc (2 * n)"
using Suc_double_not_eq_double [of n m] by simp
-lemma even_diff_iff [simp]: "2 dvd (k - l) \<longleftrightarrow> 2 dvd (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 odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
+ by (auto elim: oddE)
-lemma even_abs_add_iff [simp]: "2 dvd (\<bar>k\<bar> + l) \<longleftrightarrow> 2 dvd (k + l)"
- for k l :: int
- by (cases "k \<ge> 0") (simp_all add: ac_simps)
+lemma even_Suc_div_two [simp]:
+ "even n \<Longrightarrow> Suc n div 2 = n div 2"
+ using even_succ_div_two [of n] by simp
-lemma even_add_abs_iff [simp]: "2 dvd (k + \<bar>l\<bar>) \<longleftrightarrow> 2 dvd (k + l)"
- for k l :: int
- using even_abs_add_iff [of l k] by (simp add: ac_simps)
+lemma odd_Suc_div_two [simp]:
+ "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
+ using odd_succ_div_two [of n] by simp
-instance int :: ring_parity
-proof
- show "\<not> 2 dvd (1 :: int)"
- by (simp add: dvd_int_unfold_dvd_nat)
-next
- fix k l :: int
- assume "\<not> 2 dvd k"
- moreover assume "\<not> 2 dvd l"
- ultimately have "2 dvd (nat \<bar>k\<bar> + nat \<bar>l\<bar>)"
- by (auto simp add: dvd_int_unfold_dvd_nat intro: odd_even_add)
- then have "2 dvd (\<bar>k\<bar> + \<bar>l\<bar>)"
- by (simp add: dvd_int_unfold_dvd_nat nat_add_distrib)
- then show "2 dvd (k + l)"
+lemma odd_two_times_div_two_nat [simp]:
+ assumes "odd n"
+ shows "2 * (n div 2) = n - (1 :: nat)"
+proof -
+ from assms have "2 * (n div 2) + 1 = n"
+ by (rule odd_two_times_div_two_succ)
+ then have "Suc (2 * (n div 2)) - 1 = n - 1"
by simp
-next
- fix k l :: int
- assume "2 dvd (k * l)"
- then show "2 dvd k \<or> 2 dvd l"
- by (simp add: dvd_int_unfold_dvd_nat even_multD nat_abs_mult_distrib)
-next
- fix k :: int
- have "k = (k - 1) + 1" by simp
- then show "\<exists>l. k = l + 1" ..
+ then show ?thesis
+ by simp
qed
-lemma even_int_iff [simp]: "even (int n) \<longleftrightarrow> even n"
- by (simp add: dvd_int_iff)
-
-lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
- by (simp add: even_int_iff [symmetric])
+lemma parity_induct [case_names zero even odd]:
+ assumes zero: "P 0"
+ assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
+ assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
+ shows "P n"
+proof (induct n rule: less_induct)
+ case (less n)
+ show "P n"
+ proof (cases "n = 0")
+ case True with zero show ?thesis by simp
+ next
+ case False
+ with less have hyp: "P (n div 2)" by simp
+ show ?thesis
+ proof (cases "even n")
+ case True
+ with hyp even [of "n div 2"] show ?thesis
+ by simp
+ next
+ case False
+ with hyp odd [of "n div 2"] show ?thesis
+ by simp
+ qed
+ qed
+qed
subsection \<open>Parity and powers\<close>
@@ -319,6 +373,10 @@
lemma power_minus_odd [simp]: "odd n \<Longrightarrow> (- a) ^ n = - (a ^ n)"
by (auto elim: oddE)
+lemma uminus_power_if:
+ "(- a) ^ n = (if even n then a ^ n else - (a ^ n))"
+ by auto
+
lemma neg_one_even_power [simp]: "even n \<Longrightarrow> (- 1) ^ n = 1"
by simp
@@ -396,9 +454,6 @@
qed
qed
-lemma (in comm_ring_1) uminus_power_if: "(- x) ^ n = (if even n then x^n else - (x ^ n))"
- by auto
-
text \<open>Simplify, when the exponent is a numeral\<close>
lemma zero_le_power_eq_numeral [simp]:
@@ -428,9 +483,4 @@
end
-
-subsubsection \<open>Tool setup\<close>
-
-declare transfer_morphism_int_nat [transfer add return: even_int_iff]
-
end
--- a/src/HOL/ex/Word_Type.thy Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/ex/Word_Type.thy Sun Oct 08 22:28:22 2017 +0200
@@ -11,7 +11,7 @@
subsection \<open>Truncating bit representations of numeric types\<close>
-class semiring_bits = unique_euclidean_semiring_parity +
+class semiring_bits = semiring_parity +
assumes semiring_bits: "(1 + 2 * a) mod of_nat (2 * n) = 1 + 2 * (a mod of_nat n)"
begin
@@ -27,28 +27,16 @@
by (simp add: bitrunc_eq_mod)
lemma bitrunc_Suc [simp]:
- "bitrunc (Suc n) a = bitrunc n (a div 2) * 2 + a mod 2"
+ "bitrunc (Suc n) a = bitrunc n (a div 2) * 2 + of_bool (odd a)"
proof -
- define b and c
- where "b = a div 2" and "c = a mod 2"
- then have a: "a = b * 2 + c"
- and "c = 0 \<or> c = 1"
- by (simp_all add: div_mult_mod_eq parity)
- from \<open>c = 0 \<or> c = 1\<close>
- have "bitrunc (Suc n) (b * 2 + c) = bitrunc n b * 2 + c"
- proof
- assume "c = 0"
- moreover have "(2 * b) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n)"
- by (simp add: mod_mult_mult1)
- ultimately show ?thesis
- by (simp add: bitrunc_eq_mod ac_simps)
- next
- assume "c = 1"
- with semiring_bits [of b "2 ^ n"] show ?thesis
- by (simp add: bitrunc_eq_mod ac_simps)
- qed
- with a show ?thesis
- by (simp add: b_def c_def)
+ have "1 + 2 * (a div 2) mod (2 * 2 ^ n) = (a div 2 * 2 + a mod 2) mod (2 * 2 ^ n)"
+ if "odd a"
+ using that semiring_bits [of "a div 2" "2 ^ n"]
+ by (simp add: algebra_simps odd_iff_mod_2_eq_one mult_mod_right)
+ also have "\<dots> = a mod (2 * 2 ^ n)"
+ by (simp only: div_mult_mod_eq)
+ finally show ?thesis
+ by (simp add: bitrunc_eq_mod algebra_simps mult_mod_right)
qed
lemma bitrunc_of_0 [simp]:
@@ -57,11 +45,11 @@
lemma bitrunc_plus:
"bitrunc n (bitrunc n a + bitrunc n b) = bitrunc n (a + b)"
- by (simp add: bitrunc_eq_mod mod_add_eq)
+ by (simp add: bitrunc_eq_mod mod_simps)
lemma bitrunc_of_1_eq_0_iff [simp]:
"bitrunc n 1 = 0 \<longleftrightarrow> n = 0"
- by (induct n) simp_all
+ by (simp add: bitrunc_eq_mod)
end
@@ -113,7 +101,7 @@
lemma signed_bitrunc_Suc [simp]:
"signed_bitrunc (Suc n) k = signed_bitrunc n (k div 2) * 2 + k mod 2"
- using zero_not_eq_two by (simp add: signed_bitrunc_eq_bitrunc algebra_simps)
+ by (simp add: odd_iff_mod_2_eq_one signed_bitrunc_eq_bitrunc algebra_simps)
lemma signed_bitrunc_of_0 [simp]:
"signed_bitrunc n 0 = 0"