--- 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";
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)