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 *}