src/HOL/NumberTheory/Int2.thy

--- a/src/HOL/NumberTheory/Int2.thy	Fri Jul 01 14:55:05 2005 +0200
+++ b/src/HOL/NumberTheory/Int2.thy	Fri Jul 01 17:41:10 2005 +0200
@@ -37,13 +37,13 @@
 lemma aux4: " -(m * n) = (-m) * (n::int)";
   by auto
 
-lemma zprime_zdvd_zmult_better: "[| p \<in> zprime;  p dvd (m * n) |] ==> 
+lemma zprime_zdvd_zmult_better: "[| zprime p;  p dvd (m * n) |] ==> 
     (p dvd m) | (p dvd n)";
   apply (case_tac "0 \<le> m")
   apply (simp add: zprime_zdvd_zmult)
   by (insert zprime_zdvd_zmult [of "-m" p n], auto)
 
-lemma zpower_zdvd_prop2 [rule_format]: "p \<in> zprime --> p dvd ((y::int) ^ n) 
+lemma zpower_zdvd_prop2 [rule_format]: "zprime p --> p dvd ((y::int) ^ n) 
     --> 0 < n --> p dvd y";
   apply (induct_tac n, auto)
   apply (frule zprime_zdvd_zmult_better, auto)
@@ -124,7 +124,7 @@
     ([c = d * a](mod m) = [c = d * b] (mod m))";
   by (auto simp add: zmult_ac zcong_zmult_prop1)
 
-lemma zcong_zmult_prop3: "[|p \<in> zprime; ~[x = 0] (mod p); 
+lemma zcong_zmult_prop3: "[| zprime p; ~[x = 0] (mod p); 
     ~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)";
   apply (auto simp add: zcong_def)
   apply (drule zprime_zdvd_zmult_better, auto)
@@ -160,11 +160,11 @@
 lemma zcong_zero_equiv_div: "[a = 0] (mod m) = (m dvd a)";
   by (auto simp add: zcong_def)
 
-lemma zcong_zprime_prod_zero: "[| p \<in> zprime; 0 < a |] ==> 
+lemma zcong_zprime_prod_zero: "[| zprime p; 0 < a |] ==> 
   [a * b = 0] (mod p) ==> [a = 0] (mod p) | [b = 0] (mod p)"; 
   by (auto simp add: zcong_zero_equiv_div zprime_zdvd_zmult)
 
-lemma zcong_zprime_prod_zero_contra: "[| p \<in> zprime; 0 < a |] ==>
+lemma zcong_zprime_prod_zero_contra: "[| zprime p; 0 < a |] ==>
   ~[a = 0](mod p) & ~[b = 0](mod p) ==> ~[a * b = 0] (mod p)";
   apply auto 
   apply (frule_tac a = a and b = b and p = p in zcong_zprime_prod_zero)
@@ -191,10 +191,10 @@
     [(MultInv p x) = (MultInv p y)] (mod p)";
   by (auto simp add: MultInv_def zcong_zpower)
 
-lemma MultInv_prop2: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==> 
+lemma MultInv_prop2: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> 
   [(x * (MultInv p x)) = 1] (mod p)";
 proof (simp add: MultInv_def zcong_eq_zdvd_prop);
-  assume "2 < p" and "p \<in> zprime" and "~ p dvd x";
+  assume "2 < p" and "zprime p" and "~ p dvd x";
   have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)";
     by auto
   also from prems have "nat (p - 2) + 1 = nat (p - 2 + 1)";
@@ -207,7 +207,7 @@
   finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)";.;
 qed;
 
-lemma MultInv_prop2a: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==> 
+lemma MultInv_prop2a: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> 
     [(MultInv p x) * x = 1] (mod p)";
   by (auto simp add: MultInv_prop2 zmult_ac)
 
@@ -217,14 +217,14 @@
 lemma aux_2: "2 < p ==> 0 < nat (p - 2)";
   by auto
 
-lemma MultInv_prop3: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==> 
+lemma MultInv_prop3: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> 
     ~([MultInv p x = 0](mod p))";
   apply (auto simp add: MultInv_def zcong_eq_zdvd_prop aux_1)
   apply (drule aux_2)
   apply (drule zpower_zdvd_prop2, auto)
 done
 
-lemma aux__1: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p))|] ==> 
+lemma aux__1: "[| 2 < p; zprime p; ~([x = 0](mod p))|] ==> 
     [(MultInv p (MultInv p x)) = (x * (MultInv p x) * 
       (MultInv p (MultInv p x)))] (mod p)";
   apply (drule MultInv_prop2, auto)
@@ -232,7 +232,7 @@
   apply (auto simp add: zcong_sym)
 done
 
-lemma aux__2: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p))|] ==>
+lemma aux__2: "[| 2 < p; zprime p; ~([x = 0](mod p))|] ==>
     [(x * (MultInv p x) * (MultInv p (MultInv p x))) = x] (mod p)";
   apply (frule MultInv_prop3, auto)
   apply (insert MultInv_prop2 [of p "MultInv p x"], auto)
@@ -241,14 +241,14 @@
   apply (auto simp add: zmult_ac)
 done
 
-lemma MultInv_prop4: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==> 
+lemma MultInv_prop4: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> 
     [(MultInv p (MultInv p x)) = x] (mod p)";
   apply (frule aux__1, auto)
   apply (drule aux__2, auto)
   apply (drule zcong_trans, auto)
 done
 
-lemma MultInv_prop5: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)); 
+lemma MultInv_prop5: "[| 2 < p; zprime p; ~([x = 0](mod p)); 
     ~([y = 0](mod p)); [(MultInv p x) = (MultInv p y)] (mod p) |] ==> 
     [x = y] (mod p)";
   apply (drule_tac a = "MultInv p x" and b = "MultInv p y" and 
@@ -271,7 +271,7 @@
     [j * k = a * MultInv p k * k] (mod p)";
   by (auto simp add: zcong_scalar)
 
-lemma aux___2: "[|2 < p; p \<in> zprime; ~([k = 0](mod p)); 
+lemma aux___2: "[|2 < p; zprime p; ~([k = 0](mod p)); 
     [j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)";
   apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2 
     [of "MultInv p k * k" 1 p "j * k" a])
@@ -282,7 +282,7 @@
      (MultInv p j) * a] (mod p)";
   by (auto simp add: zmult_assoc zcong_scalar2)
 
-lemma aux___4: "[|2 < p; p \<in> zprime; ~([j = 0](mod p)); 
+lemma aux___4: "[|2 < p; zprime p; ~([j = 0](mod p)); 
     [(MultInv p j) * j * k = (MultInv p j) * a] (mod p) |]
        ==> [k = a * (MultInv p j)] (mod p)";
   apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1 
@@ -290,14 +290,14 @@
   apply (auto simp add: zmult_ac zcong_sym)
 done
 
-lemma MultInv_zcong_prop2: "[| 2 < p; p \<in> zprime; ~([k = 0](mod p)); 
+lemma MultInv_zcong_prop2: "[| 2 < p; zprime p; ~([k = 0](mod p)); 
     ~([j = 0](mod p)); [j = a * MultInv p k] (mod p) |] ==> 
     [k = a * MultInv p j] (mod p)";
   apply (drule aux___1)
   apply (frule aux___2, auto)
   by (drule aux___3, drule aux___4, auto)
 
-lemma MultInv_zcong_prop3: "[| 2 < p; p \<in> zprime; ~([a = 0](mod p)); 
+lemma MultInv_zcong_prop3: "[| 2 < p; zprime p; ~([a = 0](mod p)); 
     ~([k = 0](mod p)); ~([j = 0](mod p));
     [a * MultInv p j = a * MultInv p k] (mod p) |] ==> 
       [j = k] (mod p)";