moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
tuned presburger

--- a/NEWS	Thu Oct 31 11:44:20 2013 +0100
+++ b/NEWS	Thu Oct 31 11:44:20 2013 +0100
@@ -4,6 +4,11 @@
 New in this Isabelle version
 ----------------------------
 
+*** HOL ***
+
+* Fact name generalization and consolidation:
+  neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1
+
 
 
 New in Isabelle2013-1 (November 2013)

--- a/src/HOL/Divides.thy	Thu Oct 31 11:44:20 2013 +0100
+++ b/src/HOL/Divides.thy	Thu Oct 31 11:44:20 2013 +0100
@@ -2620,11 +2620,6 @@
   "Suc 0 mod numeral v' = nat (1 mod numeral v')"
   by (subst nat_mod_distrib) simp_all
 
-lemma mod_2_not_eq_zero_eq_one_int:
-  fixes k :: int
-  shows "k mod 2 \<noteq> 0 \<longleftrightarrow> k mod 2 = 1"
-  by auto
-
 instance int :: semiring_numeral_div
   by intro_classes (auto intro: zmod_le_nonneg_dividend
     simp add: zmult_div_cancel

--- a/src/HOL/Library/Code_Target_Int.thy	Thu Oct 31 11:44:20 2013 +0100
+++ b/src/HOL/Library/Code_Target_Int.thy	Thu Oct 31 11:44:20 2013 +0100
@@ -99,7 +99,7 @@
 proof -
   from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
   show ?thesis
-    by (simp add: Let_def divmod_int_mod_div mod_2_not_eq_zero_eq_one_int
+    by (simp add: Let_def divmod_int_mod_div not_mod_2_eq_0_eq_1
       of_int_add [symmetric]) (simp add: * mult_commute)
 qed
 

--- a/src/HOL/Parity.thy	Thu Oct 31 11:44:20 2013 +0100
+++ b/src/HOL/Parity.thy	Thu Oct 31 11:44:20 2013 +0100
@@ -11,11 +11,14 @@
 
 class even_odd = 
   fixes even :: "'a \<Rightarrow> bool"
+begin
 
-abbreviation
-  odd :: "'a\<Colon>even_odd \<Rightarrow> bool" where
+abbreviation odd :: "'a \<Rightarrow> bool"
+where
   "odd x \<equiv> \<not> even x"
 
+end
+
 instantiation nat and int  :: even_odd
 begin
 
@@ -52,7 +55,7 @@
   unfolding even_def by simp
 
 (* TODO: proper simp rules for Num.Bit0, Num.Bit1 *)
-declare even_def[of "neg_numeral v", simp] for v
+declare even_def [of "neg_numeral v", simp] for v
 
 lemma even_numeral_nat [simp]: "even (numeral (Num.Bit0 k) :: nat)"
   unfolding even_nat_def by simp
@@ -62,13 +65,6 @@
 
 subsection {* Even and odd are mutually exclusive *}
 
-lemma int_pos_lt_two_imp_zero_or_one:
-    "0 <= x ==> (x::int) < 2 ==> x = 0 | x = 1"
-  by presburger
-
-lemma neq_one_mod_two [simp, presburger]: 
-  "((x::int) mod 2 ~= 0) = (x mod 2 = 1)" by presburger
-
 
 subsection {* Behavior under integer arithmetic operations *}
 declare dvd_def[algebra]
@@ -158,10 +154,6 @@
 
 subsection {* Equivalent definitions *}
 
-lemma nat_lt_two_imp_zero_or_one:
-  "(x::nat) < Suc (Suc 0) ==> x = 0 | x = Suc 0"
-by presburger
-
 lemma even_nat_mod_two_eq_zero: "even (x::nat) ==> x mod (Suc (Suc 0)) = 0"
 by presburger
 
@@ -244,7 +236,7 @@
 apply (metis field_power_not_zero divisors_zero order_antisym_conv zero_le_square)
 done
 
-lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) =
+lemma zero_le_power_eq [presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) =
     (even n | (odd n & 0 <= x))"
   apply auto
   apply (subst zero_le_odd_power [symmetric])
@@ -277,9 +269,6 @@
   apply (simp add: zero_le_even_power)
   done
 
-lemma zero_less_power_nat_eq[presburger]: "(0 < (x::nat) ^ n) = (n = 0 | 0 < x)"
-  by (induct n) auto
-
 lemma power_minus_even [simp]: "even n ==>
     (- x)^n = (x^n::'a::{comm_ring_1})"
   apply (subst power_minus)
@@ -336,13 +325,6 @@
 
 lemma odd_add [simp]: "odd(m + n::nat) = (odd m \<noteq> odd n)" by presburger
 
-lemma div_Suc: "Suc a div c = a div c + Suc 0 div c +
-    (a mod c + Suc 0 mod c) div c" 
-  apply (subgoal_tac "Suc a = a + Suc 0")
-  apply (erule ssubst)
-  apply (rule div_add1_eq, simp)
-  done
-
 lemma lemma_even_div2 [simp]: "even (n::nat) ==> (n + 1) div 2 = n div 2" by presburger
 
 lemma lemma_not_even_div2 [simp]: "~even n ==> (n + 1) div 2 = Suc (n div 2)"
@@ -359,31 +341,29 @@
 text {* Simplify, when the exponent is a numeral *}
 
 lemmas zero_le_power_eq_numeral [simp] =
-    zero_le_power_eq [of _ "numeral w"] for w
+  zero_le_power_eq [of _ "numeral w"] for w
 
 lemmas zero_less_power_eq_numeral [simp] =
-    zero_less_power_eq [of _ "numeral w"] for w
+  zero_less_power_eq [of _ "numeral w"] for w
 
 lemmas power_le_zero_eq_numeral [simp] =
-    power_le_zero_eq [of _ "numeral w"] for w
+  power_le_zero_eq [of _ "numeral w"] for w
 
 lemmas power_less_zero_eq_numeral [simp] =
-    power_less_zero_eq [of _ "numeral w"] for w
+  power_less_zero_eq [of _ "numeral w"] for w
 
 lemmas zero_less_power_nat_eq_numeral [simp] =
-    zero_less_power_nat_eq [of _ "numeral w"] for w
+  nat_zero_less_power_iff [of _ "numeral w"] for w
 
-lemmas power_eq_0_iff_numeral [simp] = power_eq_0_iff [of _ "numeral w"] for w
+lemmas power_eq_0_iff_numeral [simp] =
+  power_eq_0_iff [of _ "numeral w"] for w
 
-lemmas power_even_abs_numeral [simp] = power_even_abs [of "numeral w" _] for w
+lemmas power_even_abs_numeral [simp] =
+  power_even_abs [of "numeral w" _] for w
 
 
 subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *}
 
-lemma even_power_le_0_imp_0:
-    "a ^ (2*k) \<le> (0::'a::{linordered_idom}) ==> a=0"
-  by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff)
-
 lemma zero_le_power_iff[presburger]:
   "(0 \<le> a^n) = (0 \<le> (a::'a::{linordered_idom}) | even n)"
 proof cases
@@ -395,9 +375,10 @@
   assume odd: "odd n"
   then obtain k where "n = Suc(2*k)"
     by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2)
-  thus ?thesis
-    by (auto simp add: zero_le_mult_iff zero_le_even_power
-             dest!: even_power_le_0_imp_0)
+  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
 
 
@@ -409,7 +390,6 @@
 lemma odd_plus_one_div_two: "odd (x::int) ==> (x + 1) div 2 = x div 2 + 1" by presburger
 
 lemma [presburger]: "(Suc x) div Suc (Suc 0) = x div Suc (Suc 0) \<longleftrightarrow> even x" by presburger
-lemma [presburger]: "(Suc x) div Suc (Suc 0) = x div Suc (Suc 0) \<longleftrightarrow> even x" by presburger
 lemma even_nat_plus_one_div_two: "even (x::nat) ==>
     (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)" by presburger
 
@@ -417,3 +397,4 @@
     (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))" by presburger
 
 end
+

--- a/src/HOL/Presburger.thy	Thu Oct 31 11:44:20 2013 +0100
+++ b/src/HOL/Presburger.thy	Thu Oct 31 11:44:20 2013 +0100
@@ -360,11 +360,15 @@
   apply simp
   done
 
-lemma zdvd_mono: assumes not0: "(k::int) \<noteq> 0"
-shows "((m::int) dvd t) \<equiv> (k*m dvd k*t)" 
-  using not0 by (simp add: dvd_def)
+lemma zdvd_mono:
+  fixes k m t :: int
+  assumes "k \<noteq> 0"
+  shows "m dvd t \<equiv> k * m dvd k * t" 
+  using assms by simp
 
-lemma uminus_dvd_conv: "(d dvd (t::int)) \<equiv> (-d dvd t)" "(d dvd (t::int)) \<equiv> (d dvd -t)"
+lemma uminus_dvd_conv:
+  fixes d t :: int
+  shows "d dvd t \<equiv> - d dvd t" and "d dvd t \<equiv> d dvd - t"
   by simp_all
 
 text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
@@ -406,24 +410,23 @@
   end
 *} "Cooper's algorithm for Presburger arithmetic"
 
-declare dvd_eq_mod_eq_0[symmetric, presburger]
-declare mod_1[presburger] 
-declare mod_0[presburger]
-declare mod_by_1[presburger]
-declare mod_self[presburger]
-declare mod_by_0[presburger]
-declare mod_div_trivial[presburger]
-declare div_mod_equality2[presburger]
-declare div_mod_equality[presburger]
-declare mod_div_equality2[presburger]
-declare mod_div_equality[presburger]
-declare mod_mult_self1[presburger]
-declare mod_mult_self2[presburger]
-declare div_mod_equality[presburger]
-declare div_mod_equality2[presburger]
+declare dvd_eq_mod_eq_0 [symmetric, presburger]
+declare mod_1 [presburger] 
+declare mod_0 [presburger]
+declare mod_by_1 [presburger]
+declare mod_self [presburger]
+declare div_by_0 [presburger]
+declare mod_by_0 [presburger]
+declare mod_div_trivial [presburger]
+declare div_mod_equality2 [presburger]
+declare div_mod_equality [presburger]
+declare mod_div_equality2 [presburger]
+declare mod_div_equality [presburger]
+declare mod_mult_self1 [presburger]
+declare mod_mult_self2 [presburger]
 declare mod2_Suc_Suc[presburger]
-lemma [presburger]: "(a::int) div 0 = 0" and [presburger]: "a mod 0 = a"
-by simp_all
+declare not_mod_2_eq_0_eq_1 [presburger] 
+declare nat_zero_less_power_iff [presburger]
 
 lemma [presburger, algebra]: "m mod 2 = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
 lemma [presburger, algebra]: "m mod 2 = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
@@ -432,3 +435,4 @@
 lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
 
 end
+

--- a/src/HOL/Tools/Qelim/qelim.ML	Thu Oct 31 11:44:20 2013 +0100
+++ b/src/HOL/Tools/Qelim/qelim.ML	Thu Oct 31 11:44:20 2013 +0100
@@ -37,7 +37,7 @@
      val th = Thm.abstract_rule s x ((conv env' then_conv ncv env') p')
                    |> Drule.arg_cong_rule e
      val th' = simpex_conv (Thm.rhs_of th)
-     val (l,r) = Thm.dest_equals (cprop_of th')
+     val (_, r) = Thm.dest_equals (cprop_of th')
     in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th))
        else Thm.transitive (Thm.transitive th th') (conv env r) end
   | Const(@{const_name Ex},_)$ _ => (Thm.eta_long_conversion then_conv conv env) p