--- a/src/HOL/Parity.thy Sat Oct 25 19:20:28 2014 +0200
+++ b/src/HOL/Parity.thy Sun Oct 26 19:11:16 2014 +0100
@@ -3,148 +3,19 @@
Author: Jacques D. Fleuriot
*)
-header {* Even and Odd for int and nat *}
+header {* Parity in rings and semirings *}
theory Parity
imports Nat_Transfer
begin
-subsection {* Preliminaries about divisibility on @{typ nat} and @{typ int} *}
-
-lemma two_dvd_Suc_Suc_iff [simp]:
- "2 dvd Suc (Suc n) \<longleftrightarrow> 2 dvd n"
- using dvd_add_triv_right_iff [of 2 n] by simp
-
-lemma two_dvd_Suc_iff:
- "2 dvd Suc n \<longleftrightarrow> \<not> 2 dvd n"
- by (induct n) auto
-
-lemma two_dvd_diff_nat_iff:
- fixes m n :: nat
- shows "2 dvd m - n \<longleftrightarrow> m < n \<or> 2 dvd m + n"
-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:)
- then show ?thesis by auto
-next
- case False
- then show ?thesis by simp
-qed
-
-lemma two_dvd_diff_iff:
- fixes k l :: int
- shows "2 dvd k - l \<longleftrightarrow> 2 dvd k + l"
- using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
-
-lemma two_dvd_abs_add_iff:
- fixes k l :: int
- shows "2 dvd \<bar>k\<bar> + l \<longleftrightarrow> 2 dvd k + l"
- by (cases "k \<ge> 0") (simp_all add: two_dvd_diff_iff ac_simps)
-
-lemma two_dvd_add_abs_iff:
- fixes k l :: int
- shows "2 dvd k + \<bar>l\<bar> \<longleftrightarrow> 2 dvd k + l"
- using two_dvd_abs_add_iff [of l k] by (simp add: ac_simps)
-
-
-subsection {* Ring structures with parity *}
+subsection {* Ring structures with parity and @{text even}/@{text odd} predicates *}
class semiring_parity = semiring_dvd + semiring_numeral +
- assumes two_not_dvd_one [simp]: "\<not> 2 dvd 1"
- assumes not_dvd_not_dvd_dvd_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b"
- assumes two_is_prime: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b"
- assumes not_dvd_ex_decrement: "\<not> 2 dvd a \<Longrightarrow> \<exists>b. a = b + 1"
-begin
-
-lemma two_dvd_plus_one_iff [simp]:
- "2 dvd a + 1 \<longleftrightarrow> \<not> 2 dvd a"
- by (auto simp add: dvd_add_right_iff intro: not_dvd_not_dvd_dvd_add)
-
-lemma not_two_dvdE [elim?]:
- assumes "\<not> 2 dvd a"
- obtains b where "a = 2 * b + 1"
-proof -
- from assms obtain b where *: "a = b + 1"
- by (blast dest: not_dvd_ex_decrement)
- with assms have "2 dvd b + 2" by simp
- then have "2 dvd b" by simp
- then obtain c where "b = 2 * c" ..
- with * have "a = 2 * c + 1" by simp
- with that show thesis .
-qed
-
-end
-
-instance nat :: semiring_parity
-proof
- show "\<not> (2 :: nat) dvd 1"
- 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 add: two_dvd_Suc_iff)
- 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 add: two_dvd_Suc_iff)
- 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
-
-class ring_parity = comm_ring_1 + semiring_parity
-
-instance int :: ring_parity
-proof
- show "\<not> (2 :: int) dvd 1" by (simp add: dvd_int_unfold_dvd_nat)
- 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: not_dvd_not_dvd_dvd_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"
- by (simp add: two_dvd_abs_add_iff two_dvd_add_abs_iff)
-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 two_is_prime nat_abs_mult_distrib)
-next
- fix k :: int
- have "k = (k - 1) + 1" by simp
- then show "\<exists>l. k = l + 1" ..
-qed
-
-
-subsection {* Dedicated @{text even}/@{text odd} predicate *}
-
-subsubsection {* Properties *}
-
-context semiring_parity
+ 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"
begin
abbreviation even :: "'a \<Rightarrow> bool"
@@ -155,6 +26,14 @@
where
"odd a \<equiv> \<not> 2 dvd a"
+lemma even_zero [simp]:
+ "even 0"
+ by (fact dvd_0_right)
+
+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 evenE [elim?]:
assumes "even a"
obtains b where "a = 2 * b"
@@ -163,19 +42,19 @@
lemma oddE [elim?]:
assumes "odd a"
obtains b where "a = 2 * b + 1"
- using assms by (rule not_two_dvdE)
-
+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 .
+qed
+
lemma even_times_iff [simp]:
"even (a * b) \<longleftrightarrow> even a \<or> even b"
- by (auto simp add: dest: two_is_prime)
-
-lemma even_zero [simp]:
- "even 0"
- by simp
-
-lemma odd_one [simp]:
- "odd 1"
- by simp
+ by (auto dest: even_multD)
lemma even_numeral [simp]:
"even (numeral (Num.Bit0 n))"
@@ -206,7 +85,7 @@
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 not_dvd_not_dvd_dvd_add)
+ 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))"
@@ -218,7 +97,7 @@
end
-context ring_parity
+class ring_parity = comm_ring_1 + semiring_parity
begin
lemma even_minus [simp]:
@@ -232,22 +111,110 @@
end
-subsubsection {* Particularities for @{typ nat} and @{typ int} *}
+subsection {* Instances for @{typ nat} and @{typ int} *}
+
+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]:
- "even (Suc n) = odd n"
- by (fact two_dvd_Suc_iff)
+ "even (Suc n) \<longleftrightarrow> odd n"
+ by (induct n) auto
+
+lemma even_diff_nat [simp]:
+ fixes m n :: nat
+ shows "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)"
+proof (cases "n \<le> m")
+ case True
+ then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
+ 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
+
+lemma even_diff_iff [simp]:
+ fixes k l :: int
+ shows "even (k - l) \<longleftrightarrow> even (k + l)"
+ using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
+
+lemma even_abs_add_iff [simp]:
+ fixes k l :: int
+ shows "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)"
+ by (cases "k \<ge> 0") (simp_all add: ac_simps)
+
+lemma even_add_abs_iff [simp]:
+ fixes k l :: int
+ shows "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)"
+ using even_abs_add_iff [of l k] by (simp add: ac_simps)
+
+instance nat :: semiring_parity
+proof
+ show "odd (1 :: nat)"
+ by (rule notI, erule dvdE) simp
+next
+ fix m n :: nat
+ assume "odd m"
+ moreover assume "odd n"
+ ultimately have *: "even (Suc m) \<and> even (Suc n)"
+ by simp
+ then have "even (Suc m + Suc n)"
+ by (blast intro: dvd_add)
+ also have "Suc m + Suc n = m + n + 2"
+ by simp
+ finally show "even (m + n)"
+ using dvd_add_triv_right_iff [of 2 "m + n"] by simp
+next
+ fix m n :: nat
+ assume *: "even (m * n)"
+ show "even m \<or> even n"
+ proof (rule disjCI)
+ assume "odd n"
+ then have "even (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 "even m" ..
+ qed
+next
+ fix n :: nat
+ assume "odd n"
+ then show "\<exists>m. n = m + 1"
+ by (cases n) simp_all
+qed
lemma odd_pos:
"odd (n :: nat) \<Longrightarrow> 0 < n"
by (auto elim: oddE)
-lemma even_diff_nat [simp]:
- fixes m n :: nat
- shows "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)"
- by (fact two_dvd_diff_nat_iff)
+instance int :: ring_parity
+proof
+ show "odd (1 :: int)" by (simp add: dvd_int_unfold_dvd_nat)
+ fix k l :: int
+ assume "odd k"
+ moreover assume "odd l"
+ ultimately have "even (nat \<bar>k\<bar> + nat \<bar>l\<bar>)"
+ by (auto simp add: dvd_int_unfold_dvd_nat intro: odd_even_add)
+ then have "even (\<bar>k\<bar> + \<bar>l\<bar>)"
+ by (simp add: dvd_int_unfold_dvd_nat nat_add_distrib)
+ then show "even (k + l)"
+ by simp
+next
+ fix k l :: int
+ assume "even (k * l)"
+ then show "even k \<or> even 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" ..
+qed
-lemma even_int_iff:
+lemma even_int_iff [simp]:
"even (int n) \<longleftrightarrow> even n"
by (simp add: dvd_int_iff)
@@ -255,11 +222,8 @@
"0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
by (simp add: even_int_iff [symmetric])
-lemma even_num_iff:
- "0 < n \<Longrightarrow> even n = odd (n - 1 :: nat)"
- by simp
-text {* Parity and powers *}
+subsection {* Parity and powers *}
context comm_ring_1
begin
@@ -272,10 +236,6 @@
"odd n \<Longrightarrow> (- a) ^ n = - (a ^ n)"
by (auto elim: oddE)
-lemma neg_power_if:
- "(- a) ^ n = (if even n then a ^ n else - (a ^ n))"
- by simp
-
lemma neg_one_even_power [simp]:
"even n \<Longrightarrow> (- 1) ^ n = 1"
by simp
@@ -286,28 +246,9 @@
end
-lemma zero_less_power_nat_eq_numeral [simp]: -- \<open>FIXME move\<close>
- "0 < (n :: nat) ^ numeral w \<longleftrightarrow> 0 < n \<or> numeral w = (0 :: nat)"
- by (fact nat_zero_less_power_iff)
-
context linordered_idom
begin
-lemma power_eq_0_iff' [simp]: -- \<open>FIXME move\<close>
- "a ^ n = 0 \<longleftrightarrow> a = 0 \<and> n > 0"
- by (induct n) auto
-
-lemma power2_less_eq_zero_iff [simp]: -- \<open>FIXME move\<close>
- "a\<^sup>2 \<le> 0 \<longleftrightarrow> a = 0"
-proof (cases "a = 0")
- case True then show ?thesis by simp
-next
- case False then have "a < 0 \<or> a > 0" by auto
- then have "a\<^sup>2 > 0" by auto
- then have "\<not> a\<^sup>2 \<le> 0" by (simp add: not_le)
- with False show ?thesis by simp
-qed
-
lemma zero_le_even_power:
"even n \<Longrightarrow> 0 \<le> a ^ n"
by (auto elim: evenE)
@@ -316,35 +257,20 @@
"odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a"
by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE)
-lemma zero_le_power_iff: -- \<open>FIXME cf. @{text zero_le_power_eq}\<close>
- "0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a \<or> even n"
-proof (cases "even n")
- case True
- then obtain k where "n = 2 * k" ..
- then show ?thesis by simp
-next
- case False
- then obtain k where "n = 2 * k + 1" ..
- moreover have "a ^ (2 * k) \<le> 0 \<Longrightarrow> a = 0"
- by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff)
- ultimately show ?thesis
- by (auto simp add: zero_le_mult_iff zero_le_even_power)
-qed
-
lemma zero_le_power_eq:
"0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a"
- using zero_le_power_iff [of a n] by auto
-
+ by (auto simp add: zero_le_even_power zero_le_odd_power)
+
lemma zero_less_power_eq:
"0 < a ^ n \<longleftrightarrow> n = 0 \<or> even n \<and> a \<noteq> 0 \<or> odd n \<and> 0 < a"
proof -
have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> n > 0"
- unfolding power_eq_0_iff' [of a n, symmetric] by blast
+ unfolding power_eq_0_iff [of a n, symmetric] by blast
show ?thesis
unfolding less_le zero_le_power_eq by auto
qed
-lemma power_less_zero_eq:
+lemma power_less_zero_eq [simp]:
"a ^ n < 0 \<longleftrightarrow> odd n \<and> a < 0"
unfolding not_le [symmetric] zero_le_power_eq by auto
@@ -408,10 +334,6 @@
"a ^ numeral w < 0 \<longleftrightarrow> odd (numeral w :: nat) \<and> a < 0"
by (fact power_less_zero_eq)
-lemma power_eq_0_iff_numeral [simp]:
- "a ^ numeral w = (0 :: nat) \<longleftrightarrow> a = 0 \<and> numeral w \<noteq> (0 :: nat)"
- by (fact power_eq_0_iff)
-
lemma power_even_abs_numeral [simp]:
"even (numeral w :: nat) \<Longrightarrow> \<bar>a\<bar> ^ numeral w = a ^ numeral w"
by (fact power_even_abs)