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.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.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)