# HG changeset patch
# User paulson
# Date 1078483435 -3600
# Node ID 5f14c12074991c61e9eb926ac5dc7e0954093565
# Parent  f25291a96e17c48418490f560a82496b6a8ed130
patch to NumberTheory problems caused by Parity

diff -r f25291a96e17 -r 5f14c1207499 src/HOL/NumberTheory/EvenOdd.thy
--- a/src/HOL/NumberTheory/EvenOdd.thy	Fri Mar 05 07:46:07 2004 +0100
+++ b/src/HOL/NumberTheory/EvenOdd.thy	Fri Mar 05 11:43:55 2004 +0100
@@ -43,17 +43,7 @@
   qed;
 
 lemma even_odd_disj: "(x \<in> zOdd | x \<in> zEven)";
-  apply (auto simp add: zOdd_def zEven_def)
-  proof -;
-    assume "\<forall>k. x \<noteq> 2 * k";
-    have "0 \<le> (x mod 2) & (x mod 2) < 2";
-      by (auto intro: pos_mod_sign pos_mod_bound)
-    then have "x mod 2 = 0 | x mod 2 = 1" by arith
-    moreover from prems have "x mod 2 \<noteq> 0" by auto
-    ultimately have "x mod 2 = 1" by auto
-    thus "\<exists>k. x = 2 * k + 1";
-      by (insert zmod_zdiv_equality [of "x" "2"], auto)
-  qed;
+  by (simp add: zOdd_def zEven_def, presburger)
 
 lemma not_odd_impl_even: "~(x \<in> zOdd) ==> x \<in> zEven";
   by (insert even_odd_disj, auto)
diff -r f25291a96e17 -r 5f14c1207499 src/HOL/NumberTheory/Quadratic_Reciprocity.thy
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Fri Mar 05 07:46:07 2004 +0100
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Fri Mar 05 11:43:55 2004 +0100
@@ -105,7 +105,7 @@
   with a have "p * (setsum (%x. ((x * a) div p)) A - int(card E)): zEven";
     by simp
   hence "p \<in> zEven | (setsum (%x. ((x * a) div p)) A - int(card E)): zEven";
-    by (rule even_product)
+    by (rule EvenOdd.even_product)
   with p_odd have "(setsum (%x. ((x * a) div p)) A - int(card E)): zEven";
     by (auto simp add: odd_iff_not_even)
   thus ?thesis;
@@ -271,7 +271,7 @@
 
 lemma (in QRTEMP) S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))";
   apply (insert P_set_card Q_set_card P_set_finite Q_set_finite)
-  apply (auto simp add: S_def zmult_int)
+  apply (auto simp add: S_def zmult_int setsum_constant_nat) 
 done
 
 lemma (in QRTEMP) S1_Int_S2_prop: "S1 \<inter> S2 = {}";
@@ -378,7 +378,7 @@
   then have even2: "(2 * p):zEven & ((q - 1) * p):zEven";
     by (auto simp add: zEven_def)
   then have even3: "(((q - 1) * p) + (2 * p)):zEven";
-    by (auto simp: even_plus_even)
+    by (auto simp: EvenOdd.even_plus_even)
   (* using these prove it *)
   from prems have "q * (p - 1) < ((q - 1) * p) + (2 * p)";
     by (auto simp add: int_distrib)