--- a/src/HOL/Groebner_Basis.thy Fri Oct 24 15:07:51 2014 +0200
+++ b/src/HOL/Groebner_Basis.thy Thu Oct 23 19:40:39 2014 +0200
@@ -5,7 +5,7 @@
header {* Groebner bases *}
theory Groebner_Basis
-imports Semiring_Normalization
+imports Semiring_Normalization Parity
keywords "try0" :: diag
begin
@@ -77,4 +77,22 @@
declare zmod_eq_dvd_iff[algebra]
declare nat_mod_eq_iff[algebra]
+context semiring_parity
+begin
+
+declare even_times_iff [algebra]
+declare even_power [algebra]
+
end
+
+context ring_parity
+begin
+
+declare even_minus [algebra]
+
+end
+
+declare even_Suc [algebra]
+declare even_diff_nat [algebra]
+
+end
--- a/src/HOL/Main.thy Fri Oct 24 15:07:51 2014 +0200
+++ b/src/HOL/Main.thy Thu Oct 23 19:40:39 2014 +0200
@@ -2,7 +2,7 @@
theory Main
imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick
- BNF_Greatest_Fixpoint Parity
+ BNF_Greatest_Fixpoint
begin
text {*
--- a/src/HOL/Parity.thy Fri Oct 24 15:07:51 2014 +0200
+++ b/src/HOL/Parity.thy Thu Oct 23 19:40:39 2014 +0200
@@ -6,7 +6,7 @@
header {* Even and Odd for int and nat *}
theory Parity
-imports Presburger
+imports Divides
begin
subsection {* Preliminaries about divisibility on @{typ nat} and @{typ int} *}
@@ -36,7 +36,7 @@
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: ac_simps)
+ 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
@@ -546,77 +546,5 @@
even_int_iff
]
-context semiring_parity
-begin
-
-declare even_times_iff [presburger, algebra]
-
-declare even_power [presburger, algebra]
-
-lemma [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
-
-declare even_diff_nat [presburger, algebra]
-
-lemma [presburger]:
- fixes k :: int
- shows "(k + 1) div 2 = k div 2 \<longleftrightarrow> even k"
- by presburger
-
-lemma [presburger]:
- fixes k :: int
- shows "(k + 1) div 2 = k div 2 + 1 \<longleftrightarrow> odd k"
- by presburger
-
-lemma [presburger]:
- "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/Presburger.thy Fri Oct 24 15:07:51 2014 +0200
+++ b/src/HOL/Presburger.thy Thu Oct 23 19:40:39 2014 +0200
@@ -434,6 +434,78 @@
lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
+context semiring_parity
+begin
+
+declare even_times_iff [presburger]
+
+declare even_power [presburger]
+
+lemma [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]
+
+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]
+
+lemma [presburger]:
+ "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n"
+ by presburger
+
+declare even_diff_nat [presburger]
+
+lemma [presburger]:
+ fixes k :: int
+ shows "(k + 1) div 2 = k div 2 \<longleftrightarrow> even k"
+ by presburger
+
+lemma [presburger]:
+ fixes k :: int
+ shows "(k + 1) div 2 = k div 2 + 1 \<longleftrightarrow> odd k"
+ by presburger
+
+lemma [presburger]:
+ "even n \<longleftrightarrow> even (int n)"
+ using even_int_iff [of n] by simp
+
+
+subsection {* 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
+
subsection {* Try0 *}