src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
changeset 41541 1fa4725c4656
parent 38159 e9b4835a54ee
child 44766 d4d33a4d7548
     1.1 --- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Thu Jan 13 21:50:13 2011 +0100
     1.2 +++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Thu Jan 13 23:50:16 2011 +0100
     1.3 @@ -201,10 +201,11 @@
     1.4    then show ?thesis by auto
     1.5  qed
     1.6  
     1.7 -lemma pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==>
     1.8 -    (p * b \<noteq> q * a)"
     1.9 +lemma pb_neq_qa:
    1.10 +  assumes "1 \<le> b" and "b \<le> (q - 1) div 2"
    1.11 +  shows "p * b \<noteq> q * a"
    1.12  proof
    1.13 -  assume "p * b = q * a" and "1 \<le> b" and "b \<le> (q - 1) div 2"
    1.14 +  assume "p * b = q * a"
    1.15    then have "q dvd (p * b)" by (auto simp add: dvd_def)
    1.16    with q_prime p_g_2 have "q dvd p | q dvd b"
    1.17      by (auto simp add: zprime_zdvd_zmult)
    1.18 @@ -216,7 +217,7 @@
    1.19        apply (drule_tac x = q and R = False in allE)
    1.20        apply (simp add: QRTEMP_def)
    1.21        apply (subgoal_tac "0 \<le> q", simp add: QRTEMP_def)
    1.22 -      apply (insert prems)
    1.23 +      apply (insert assms)
    1.24        apply (auto simp add: QRTEMP_def)
    1.25        done
    1.26      with q_g_2 p_neq_q show False by auto
    1.27 @@ -225,18 +226,18 @@
    1.28    then have "q \<le> b"
    1.29    proof -
    1.30      assume "q dvd b"
    1.31 -    moreover from prems have "0 < b" by auto
    1.32 +    moreover from assms have "0 < b" by auto
    1.33      ultimately show ?thesis using zdvd_bounds [of q b] by auto
    1.34    qed
    1.35 -  with prems have "q \<le> (q - 1) div 2" by auto
    1.36 +  with assms have "q \<le> (q - 1) div 2" by auto
    1.37    then have "2 * q \<le> 2 * ((q - 1) div 2)" by arith
    1.38    then have "2 * q \<le> q - 1"
    1.39    proof -
    1.40 -    assume "2 * q \<le> 2 * ((q - 1) div 2)"
    1.41 -    with prems have "q \<in> zOdd" by (auto simp add: QRTEMP_def zprime_zOdd_eq_grt_2)
    1.42 +    assume a: "2 * q \<le> 2 * ((q - 1) div 2)"
    1.43 +    with assms have "q \<in> zOdd" by (auto simp add: QRTEMP_def zprime_zOdd_eq_grt_2)
    1.44      with odd_minus_one_even have "(q - 1):zEven" by auto
    1.45      with even_div_2_prop2 have "(q - 1) = 2 * ((q - 1) div 2)" by auto
    1.46 -    with prems show ?thesis by auto
    1.47 +    with a show ?thesis by auto
    1.48    qed
    1.49    then have p1: "q \<le> -1" by arith
    1.50    with q_g_2 show False by auto
    1.51 @@ -273,7 +274,7 @@
    1.52  
    1.53  lemma S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
    1.54    using P_set_card Q_set_card P_set_finite Q_set_finite
    1.55 -  by (auto simp add: S_def zmult_int setsum_constant)
    1.56 +  by (auto simp add: S_def zmult_int)
    1.57  
    1.58  lemma S1_Int_S2_prop: "S1 \<inter> S2 = {}"
    1.59    by (auto simp add: S1_def S2_def)
    1.60 @@ -301,11 +302,11 @@
    1.61    finally show ?thesis .
    1.62  qed
    1.63  
    1.64 -lemma aux1a: "[| 0 < a; a \<le> (p - 1) div 2;
    1.65 -                             0 < b; b \<le> (q - 1) div 2 |] ==>
    1.66 -                          (p * b < q * a) = (b \<le> q * a div p)"
    1.67 +lemma aux1a:
    1.68 +  assumes "0 < a" and "a \<le> (p - 1) div 2"
    1.69 +    and "0 < b" and "b \<le> (q - 1) div 2"
    1.70 +  shows "(p * b < q * a) = (b \<le> q * a div p)"
    1.71  proof -
    1.72 -  assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2"
    1.73    have "p * b < q * a ==> b \<le> q * a div p"
    1.74    proof -
    1.75      assume "p * b < q * a"
    1.76 @@ -329,17 +330,17 @@
    1.77      then have "p * b < q * a | p * b = q * a"
    1.78        by (simp only: order_le_imp_less_or_eq)
    1.79      moreover have "p * b \<noteq> q * a"
    1.80 -      by (rule  pb_neq_qa) (insert prems, auto)
    1.81 +      by (rule pb_neq_qa) (insert assms, auto)
    1.82      ultimately show ?thesis by auto
    1.83    qed
    1.84    ultimately show ?thesis ..
    1.85  qed
    1.86  
    1.87 -lemma aux1b: "[| 0 < a; a \<le> (p - 1) div 2;
    1.88 -                             0 < b; b \<le> (q - 1) div 2 |] ==>
    1.89 -                          (q * a < p * b) = (a \<le> p * b div q)"
    1.90 +lemma aux1b:
    1.91 +  assumes "0 < a" and "a \<le> (p - 1) div 2"
    1.92 +    and "0 < b" and "b \<le> (q - 1) div 2"
    1.93 +  shows "(q * a < p * b) = (a \<le> p * b div q)"
    1.94  proof -
    1.95 -  assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2"
    1.96    have "q * a < p * b ==> a \<le> p * b div q"
    1.97    proof -
    1.98      assume "q * a < p * b"
    1.99 @@ -363,18 +364,18 @@
   1.100      then have "q * a < p * b | q * a = p * b"
   1.101        by (simp only: order_le_imp_less_or_eq)
   1.102      moreover have "p * b \<noteq> q * a"
   1.103 -      by (rule  pb_neq_qa) (insert prems, auto)
   1.104 +      by (rule  pb_neq_qa) (insert assms, auto)
   1.105      ultimately show ?thesis by auto
   1.106    qed
   1.107    ultimately show ?thesis ..
   1.108  qed
   1.109  
   1.110 -lemma (in -) aux2: "[| zprime p; zprime q; 2 < p; 2 < q |] ==>
   1.111 -             (q * ((p - 1) div 2)) div p \<le> (q - 1) div 2"
   1.112 +lemma (in -) aux2:
   1.113 +  assumes "zprime p" and "zprime q" and "2 < p" and "2 < q"
   1.114 +  shows "(q * ((p - 1) div 2)) div p \<le> (q - 1) div 2"
   1.115  proof-
   1.116 -  assume "zprime p" and "zprime q" and "2 < p" and "2 < q"
   1.117    (* Set up what's even and odd *)
   1.118 -  then have "p \<in> zOdd & q \<in> zOdd"
   1.119 +  from assms have "p \<in> zOdd & q \<in> zOdd"
   1.120      by (auto simp add:  zprime_zOdd_eq_grt_2)
   1.121    then have even1: "(p - 1):zEven & (q - 1):zEven"
   1.122      by (auto simp add: odd_minus_one_even)
   1.123 @@ -383,7 +384,7 @@
   1.124    then have even3: "(((q - 1) * p) + (2 * p)):zEven"
   1.125      by (auto simp: EvenOdd.even_plus_even)
   1.126    (* using these prove it *)
   1.127 -  from prems have "q * (p - 1) < ((q - 1) * p) + (2 * p)"
   1.128 +  from assms have "q * (p - 1) < ((q - 1) * p) + (2 * p)"
   1.129      by (auto simp add: int_distrib)
   1.130    then have "((p - 1) * q) div 2 < (((q - 1) * p) + (2 * p)) div 2"
   1.131      apply (rule_tac x = "((p - 1) * q)" in even_div_2_l)
   1.132 @@ -395,7 +396,7 @@
   1.133    finally show ?thesis
   1.134      apply (rule_tac x = " q * ((p - 1) div 2)" and
   1.135                      y = "(q - 1) div 2" in div_prop2)
   1.136 -    using prems by auto
   1.137 +    using assms by auto
   1.138  qed
   1.139  
   1.140  lemma aux3a: "\<forall>j \<in> P_set. int (card (f1 j)) = (q * j) div p"
   1.141 @@ -414,7 +415,7 @@
   1.142      ultimately have "card ((%(x,y). y) ` (f1 j)) = card  (f1 j)"
   1.143        by (auto simp add: f1_def card_image)
   1.144      moreover have "((%(x,y). y) ` (f1 j)) = {y. y \<in> Q_set & y \<le> (q * j) div p}"
   1.145 -      using prems by (auto simp add: f1_def S_def Q_set_def P_set_def image_def)
   1.146 +      using j_fact by (auto simp add: f1_def S_def Q_set_def P_set_def image_def)
   1.147      ultimately show ?thesis by (auto simp add: f1_def)
   1.148    qed
   1.149    also have "... = int (card {y. 0 < y & y \<le> (q * j) div p})"
   1.150 @@ -424,18 +425,18 @@
   1.151        apply (auto simp add: Q_set_def)
   1.152      proof -
   1.153        fix x
   1.154 -      assume "0 < x" and "x \<le> q * j div p"
   1.155 +      assume x: "0 < x" "x \<le> q * j div p"
   1.156        with j_fact P_set_def  have "j \<le> (p - 1) div 2" by auto
   1.157        with q_g_2 have "q * j \<le> q * ((p - 1) div 2)"
   1.158          by (auto simp add: mult_le_cancel_left)
   1.159        with p_g_2 have "q * j div p \<le> q * ((p - 1) div 2) div p"
   1.160          by (auto simp add: zdiv_mono1)
   1.161 -      also from prems P_set_def have "... \<le> (q - 1) div 2"
   1.162 +      also from QRTEMP_axioms j_fact P_set_def have "... \<le> (q - 1) div 2"
   1.163          apply simp
   1.164          apply (insert aux2)
   1.165          apply (simp add: QRTEMP_def)
   1.166          done
   1.167 -      finally show "x \<le> (q - 1) div 2" using prems by auto
   1.168 +      finally show "x \<le> (q - 1) div 2" using x by auto
   1.169      qed
   1.170      then show ?thesis by auto
   1.171    qed
   1.172 @@ -470,7 +471,7 @@
   1.173      ultimately have "card ((%(x,y). x) ` (f2 j)) = card  (f2 j)"
   1.174        by (auto simp add: f2_def card_image)
   1.175      moreover have "((%(x,y). x) ` (f2 j)) = {y. y \<in> P_set & y \<le> (p * j) div q}"
   1.176 -      using prems by (auto simp add: f2_def S_def Q_set_def P_set_def image_def)
   1.177 +      using j_fact by (auto simp add: f2_def S_def Q_set_def P_set_def image_def)
   1.178      ultimately show ?thesis by (auto simp add: f2_def)
   1.179    qed
   1.180    also have "... = int (card {y. 0 < y & y \<le> (p * j) div q})"
   1.181 @@ -480,15 +481,15 @@
   1.182        apply (auto simp add: P_set_def)
   1.183      proof -
   1.184        fix x
   1.185 -      assume "0 < x" and "x \<le> p * j div q"
   1.186 +      assume x: "0 < x" "x \<le> p * j div q"
   1.187        with j_fact Q_set_def  have "j \<le> (q - 1) div 2" by auto
   1.188        with p_g_2 have "p * j \<le> p * ((q - 1) div 2)"
   1.189          by (auto simp add: mult_le_cancel_left)
   1.190        with q_g_2 have "p * j div q \<le> p * ((q - 1) div 2) div q"
   1.191          by (auto simp add: zdiv_mono1)
   1.192 -      also from prems have "... \<le> (p - 1) div 2"
   1.193 +      also from QRTEMP_axioms j_fact have "... \<le> (p - 1) div 2"
   1.194          by (auto simp add: aux2 QRTEMP_def)
   1.195 -      finally show "x \<le> (p - 1) div 2" using prems by auto
   1.196 +      finally show "x \<le> (p - 1) div 2" using x by auto
   1.197        qed
   1.198      then show ?thesis by auto
   1.199    qed
   1.200 @@ -587,18 +588,18 @@
   1.201  lemma QR_short: "(Legendre p q) * (Legendre q p) =
   1.202      (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))"
   1.203  proof -
   1.204 -  from prems have "~([p = 0] (mod q))"
   1.205 +  from QRTEMP_axioms have "~([p = 0] (mod q))"
   1.206      by (auto simp add: pq_prime_neq QRTEMP_def)
   1.207 -  with prems Q_set_def have a1: "(Legendre p q) = (-1::int) ^
   1.208 +  with QRTEMP_axioms Q_set_def have a1: "(Legendre p q) = (-1::int) ^
   1.209        nat(setsum (%x. ((x * p) div q)) Q_set)"
   1.210      apply (rule_tac p = q in  MainQRLemma)
   1.211      apply (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
   1.212      done
   1.213 -  from prems have "~([q = 0] (mod p))"
   1.214 +  from QRTEMP_axioms have "~([q = 0] (mod p))"
   1.215      apply (rule_tac p = q and q = p in pq_prime_neq)
   1.216      apply (simp add: QRTEMP_def)+
   1.217      done
   1.218 -  with prems P_set_def have a2: "(Legendre q p) =
   1.219 +  with QRTEMP_axioms P_set_def have a2: "(Legendre q p) =
   1.220        (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)"
   1.221      apply (rule_tac p = p in  MainQRLemma)
   1.222      apply (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)