tuned;
authorwenzelm
Fri Nov 10 10:42:28 2006 +0100 (2006-11-10)
changeset 212882c7d3d120418
parent 21287 a713ae348e8a
child 21289 920b7b893d9c
tuned;
src/HOL/NumberTheory/Gauss.thy
src/HOL/NumberTheory/Quadratic_Reciprocity.thy
     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.6  
     1.7 -end
     1.8  
     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.12    apply (simp add: zEven_def)
    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.17  
    1.18 -context GAUSS
    1.19 -begin
    1.20  
    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.6  
     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.17  
    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.27  
    2.28 -end
    2.29  
    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.37  
    2.38 -context QRTEMP
    2.39 -begin
    2.40  
    2.41  lemma QR_short: "(Legendre p q) * (Legendre q p) =
    2.42      (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))"