author wenzelm Fri Nov 10 10:42:28 2006 +0100 (2006-11-10) changeset 21288 2c7d3d120418 parent 21287 a713ae348e8a child 21289 920b7b893d9c
tuned;
1.1 --- a/src/HOL/NumberTheory/Gauss.thy	Fri Nov 10 10:42:25 2006 +0100
1.2 +++ b/src/HOL/NumberTheory/Gauss.thy	Fri Nov 10 10:42:28 2006 +0100
1.3 @@ -59,9 +59,8 @@
1.4  lemma p_eq: "p = (2 * (p - 1) div 2) + 1"
1.5    using zdiv_zmult_self2 [of 2 "p - 1"] by auto
1.7 -end
1.9 -lemma zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)"
1.10 +lemma (in -) zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)"
1.11    apply (frule odd_minus_one_even)
1.13    apply (subgoal_tac "2 \<noteq> 0")
1.14 @@ -69,8 +68,6 @@
1.15    apply (auto simp add: even_div_2_prop2)
1.16    done
1.18 -context GAUSS
1.19 -begin
1.21  lemma p_eq2: "p = (2 * ((p - 1) div 2)) + 1"
1.22    apply (insert p_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 [of p], auto)
2.1 --- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Fri Nov 10 10:42:25 2006 +0100
2.2 +++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Fri Nov 10 10:42:28 2006 +0100
2.3 @@ -371,9 +371,7 @@
2.4    ultimately show ?thesis ..
2.5  qed
2.7 -end
2.8 -
2.9 -lemma aux2: "[| zprime p; zprime q; 2 < p; 2 < q |] ==>
2.10 +lemma (in -) aux2: "[| zprime p; zprime q; 2 < p; 2 < q |] ==>
2.11               (q * ((p - 1) div 2)) div p \<le> (q - 1) div 2"
2.12  proof-
2.13    assume "zprime p" and "zprime q" and "2 < p" and "2 < q"
2.14 @@ -402,9 +400,6 @@
2.15      using prems by auto
2.16  qed
2.18 -context QRTEMP
2.19 -begin
2.20 -
2.21  lemma aux3a: "\<forall>j \<in> P_set. int (card (f1 j)) = (q * j) div p"
2.22  proof
2.23    fix j
2.24 @@ -582,17 +577,14 @@
2.25    finally show ?thesis .
2.26  qed
2.28 -end
2.30 -lemma pq_prime_neq: "[| zprime p; zprime q; p \<noteq> q |] ==> (~[p = 0] (mod q))"
2.31 +lemma (in -) pq_prime_neq: "[| zprime p; zprime q; p \<noteq> q |] ==> (~[p = 0] (mod q))"
2.32    apply (auto simp add: zcong_eq_zdvd_prop zprime_def)
2.33    apply (drule_tac x = q in allE)
2.34    apply (drule_tac x = p in allE)
2.35    apply auto
2.36    done
2.38 -context QRTEMP
2.39 -begin
2.41  lemma QR_short: "(Legendre p q) * (Legendre q p) =
2.42      (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))"