author paulson Fri, 05 Mar 2004 11:43:55 +0100 changeset 14434 5f14c1207499 parent 14433 f25291a96e17 child 14435 9e22eeccf129
patch to NumberTheory problems caused by Parity
```--- 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)```
```--- 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";
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";