# HG changeset patch
# User haftmann
# Date 1414086039 -7200
# Node ID 6ba2f1fa243b46e188f71e80649c6b8b45eac518
# Parent  95e58e04e534ea4c2b05dffe38e827432a6c3dc4
further downshift of theory Parity in the hierarchy

diff -r 95e58e04e534 -r 6ba2f1fa243b src/HOL/Groebner_Basis.thy
--- 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
diff -r 95e58e04e534 -r 6ba2f1fa243b src/HOL/Main.thy
--- 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 {*
diff -r 95e58e04e534 -r 6ba2f1fa243b src/HOL/Parity.thy
--- 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
-
diff -r 95e58e04e534 -r 6ba2f1fa243b src/HOL/Presburger.thy
--- 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 *}