--- a/NEWS Thu Oct 23 14:04:05 2014 +0200
+++ b/NEWS Thu Oct 23 14:04:05 2014 +0200
@@ -55,7 +55,8 @@
dvd_plus_eq_left ~> dvd_add_left_iff
Minor INCOMPATIBILITY.
-* "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _".
+* "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _"
+and part of HOL-Main.
even_def ~> even_iff_mod_2_eq_zero
INCOMPATIBILITY.
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy Thu Oct 23 14:04:05 2014 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Thu Oct 23 14:04:05 2014 +0200
@@ -6,7 +6,7 @@
header {* Proving equalities in commutative rings *}
theory Commutative_Ring
-imports Parity
+imports Main
begin
text {* Syntax of multivariate polynomials (pol) and polynomial expressions. *}
--- a/src/HOL/GCD.thy Thu Oct 23 14:04:05 2014 +0200
+++ b/src/HOL/GCD.thy Thu Oct 23 14:04:05 2014 +0200
@@ -28,7 +28,7 @@
header {* Greatest common divisor and least common multiple *}
theory GCD
-imports Fact Parity
+imports Fact
begin
declare One_nat_def [simp del]
--- a/src/HOL/IMPP/EvenOdd.thy Thu Oct 23 14:04:05 2014 +0200
+++ b/src/HOL/IMPP/EvenOdd.thy Thu Oct 23 14:04:05 2014 +0200
@@ -5,7 +5,7 @@
header {* Example of mutually recursive procedures verified with Hoare logic *}
theory EvenOdd
-imports Misc "~~/src/HOL/Parity"
+imports Main Misc
begin
axiomatization
--- a/src/HOL/Import/Import_Setup.thy Thu Oct 23 14:04:05 2014 +0200
+++ b/src/HOL/Import/Import_Setup.thy Thu Oct 23 14:04:05 2014 +0200
@@ -6,7 +6,7 @@
header {* Importer machinery and required theorems *}
theory Import_Setup
-imports "~~/src/HOL/Parity" "~~/src/HOL/Fact"
+imports Main "~~/src/HOL/Fact"
keywords "import_type_map" "import_const_map" "import_file" :: thy_decl
begin
--- a/src/HOL/Library/Nat_Bijection.thy Thu Oct 23 14:04:05 2014 +0200
+++ b/src/HOL/Library/Nat_Bijection.thy Thu Oct 23 14:04:05 2014 +0200
@@ -9,7 +9,7 @@
header {* Bijections between natural numbers and other types *}
theory Nat_Bijection
-imports Main Parity
+imports Main
begin
subsection {* Type @{typ "nat \<times> nat"} *}
--- a/src/HOL/Library/Permutations.thy Thu Oct 23 14:04:05 2014 +0200
+++ b/src/HOL/Library/Permutations.thy Thu Oct 23 14:04:05 2014 +0200
@@ -5,7 +5,7 @@
header {* Permutations, both general and specifically on finite sets.*}
theory Permutations
-imports Parity Fact
+imports Fact
begin
subsection {* Transpositions *}
--- a/src/HOL/Main.thy Thu Oct 23 14:04:05 2014 +0200
+++ b/src/HOL/Main.thy Thu Oct 23 14:04:05 2014 +0200
@@ -2,7 +2,7 @@
theory Main
imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick
- BNF_Greatest_Fixpoint
+ BNF_Greatest_Fixpoint Parity
begin
text {*
--- a/src/HOL/NthRoot.thy Thu Oct 23 14:04:05 2014 +0200
+++ b/src/HOL/NthRoot.thy Thu Oct 23 14:04:05 2014 +0200
@@ -7,7 +7,7 @@
header {* Nth Roots of Real Numbers *}
theory NthRoot
-imports Parity Deriv
+imports Deriv
begin
lemma abs_sgn_eq: "abs (sgn x :: real) = (if x = 0 then 0 else 1)"
--- a/src/HOL/Parity.thy Thu Oct 23 14:04:05 2014 +0200
+++ b/src/HOL/Parity.thy Thu Oct 23 14:04:05 2014 +0200
@@ -6,7 +6,7 @@
header {* Even and Odd for int and nat *}
theory Parity
-imports Main
+imports Presburger
begin
subsection {* Preliminaries about divisibility on @{typ nat} and @{typ int} *}
@@ -24,7 +24,7 @@
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
+ 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
@@ -103,7 +103,7 @@
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
+ 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
@@ -207,7 +207,7 @@
obtains b where "a = 2 * b + 1"
using assms by (rule not_two_dvdE)
-lemma even_times_iff [simp, presburger, algebra]:
+lemma even_times_iff [simp]:
"even (a * b) \<longleftrightarrow> even a \<or> even b"
by (auto simp add: dest: two_is_prime)
@@ -254,7 +254,7 @@
"odd (a + b) \<longleftrightarrow> (\<not> (odd a \<longleftrightarrow> odd b))"
by simp
-lemma even_power [simp, presburger]:
+lemma even_power [simp]:
"even (a ^ n) \<longleftrightarrow> even a \<and> n \<noteq> 0"
by (induct n) auto
@@ -263,7 +263,7 @@
context ring_parity
begin
-lemma even_minus [simp, presburger, algebra]:
+lemma even_minus [simp]:
"even (- a) \<longleftrightarrow> even a"
by (fact dvd_minus_iff)
@@ -317,7 +317,7 @@
subsubsection {* Particularities for @{typ nat} and @{typ int} *}
-lemma even_Suc [simp, presburger, algebra]:
+lemma even_Suc [simp]:
"even (Suc n) = odd n"
by (fact two_dvd_Suc_iff)
@@ -380,20 +380,6 @@
qed
qed
-text {* Nice facts about division by @{term 4} *}
-
-lemma even_even_mod_4_iff:
- "even (n::nat) \<longleftrightarrow> even (n mod 4)"
- by presburger
-
-lemma odd_mod_4_div_2:
- "n mod 4 = (3::nat) \<Longrightarrow> odd ((n - 1) div 2)"
- by presburger
-
-lemma even_mod_4_div_2:
- "n mod 4 = (1::nat) \<Longrightarrow> even ((n - 1) div 2)"
- by presburger
-
text {* Parity and powers *}
context comm_ring_1
@@ -451,7 +437,7 @@
"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 [presburger]: -- \<open>FIXME cf. @{text zero_le_power_eq}\<close>
+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
@@ -466,11 +452,11 @@
by (auto simp add: zero_le_mult_iff zero_le_even_power)
qed
-lemma zero_le_power_eq [presburger]:
+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
-lemma zero_less_power_eq [presburger]:
+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"
@@ -479,11 +465,11 @@
unfolding less_le zero_le_power_eq by auto
qed
-lemma power_less_zero_eq [presburger]:
+lemma power_less_zero_eq:
"a ^ n < 0 \<longleftrightarrow> odd n \<and> a < 0"
unfolding not_le [symmetric] zero_le_power_eq by auto
-lemma power_le_zero_eq [presburger]:
+lemma power_le_zero_eq:
"a ^ n \<le> 0 \<longleftrightarrow> n > 0 \<and> (odd n \<and> a \<le> 0 \<or> even n \<and> a = 0)"
unfolding not_less [symmetric] zero_less_power_eq by auto
@@ -560,14 +546,47 @@
even_int_iff
]
+context semiring_parity
+begin
+
+declare even_times_iff [presburger, algebra]
+
+declare even_power [presburger]
+
lemma [presburger]:
- "even n \<longleftrightarrow> even (int n)"
- using even_int_iff [of n] by simp
-
-lemma (in semiring_parity) [presburger]:
"even (a + b) \<longleftrightarrow> even a \<and> even b \<or> odd a \<and> odd b"
by auto
+end
+
+context ring_parity
+begin
+
+declare even_minus [presburger, algebra]
+
+end
+
+context linordered_idom
+begin
+
+declare zero_le_power_iff [presburger]
+
+declare zero_le_power_eq [presburger]
+
+declare zero_less_power_eq [presburger]
+
+declare power_less_zero_eq [presburger]
+
+declare power_le_zero_eq [presburger]
+
+end
+
+declare even_Suc [presburger, algebra]
+
+lemma [presburger]:
+ "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n"
+ by presburger
+
lemma [presburger, algebra]:
fixes m n :: nat
shows "even (m - n) \<longleftrightarrow> m < n \<or> even m \<and> even n \<or> odd m \<and> odd n"
@@ -587,10 +606,25 @@
fixes k :: int
shows "(k + 1) div 2 = k div 2 + 1 \<longleftrightarrow> odd k"
by presburger
-
+
lemma [presburger]:
- "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n"
+ "even n \<longleftrightarrow> even (int n)"
+ using even_int_iff [of n] by simp
+
+
+subsubsection {* Nice facts about division by @{term 4} *}
+
+lemma even_even_mod_4_iff:
+ "even (n::nat) \<longleftrightarrow> even (n mod 4)"
by presburger
+lemma odd_mod_4_div_2:
+ "n mod 4 = (3::nat) \<Longrightarrow> odd ((n - 1) div 2)"
+ by presburger
+
+lemma even_mod_4_div_2:
+ "n mod 4 = (1::nat) \<Longrightarrow> even ((n - 1) div 2)"
+ by presburger
+
end
--- a/src/HOL/Word/Misc_Numeric.thy Thu Oct 23 14:04:05 2014 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy Thu Oct 23 14:04:05 2014 +0200
@@ -5,7 +5,7 @@
header {* Useful Numerical Lemmas *}
theory Misc_Numeric
-imports Main Parity
+imports Main
begin
lemma mod_2_neq_1_eq_eq_0:
--- a/src/HOL/Word/Word_Miscellaneous.thy Thu Oct 23 14:04:05 2014 +0200
+++ b/src/HOL/Word/Word_Miscellaneous.thy Thu Oct 23 14:04:05 2014 +0200
@@ -5,7 +5,7 @@
header {* Miscellaneous lemmas, of at least doubtful value *}
theory Word_Miscellaneous
-imports Main Parity "~~/src/HOL/Library/Bit" Misc_Numeric
+imports Main "~~/src/HOL/Library/Bit" Misc_Numeric
begin
lemma power_minus_simp:
--- a/src/HOL/ex/Fundefs.thy Thu Oct 23 14:04:05 2014 +0200
+++ b/src/HOL/ex/Fundefs.thy Thu Oct 23 14:04:05 2014 +0200
@@ -5,7 +5,7 @@
header {* Examples of function definitions *}
theory Fundefs
-imports Parity "~~/src/HOL/Library/Monad_Syntax"
+imports Main "~~/src/HOL/Library/Monad_Syntax"
begin
subsection {* Very basic *}
--- a/src/HOL/ex/NatSum.thy Thu Oct 23 14:04:05 2014 +0200
+++ b/src/HOL/ex/NatSum.thy Thu Oct 23 14:04:05 2014 +0200
@@ -4,7 +4,7 @@
header {* Summing natural numbers *}
-theory NatSum imports Main Parity begin
+theory NatSum imports Main begin
text {*
Summing natural numbers, squares, cubes, etc.