src/HOL/NumberTheory/Int2.thy

 qed;
 
 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)
 done
 

 
 lemma zcong_zmult_prop2: "[a = b](mod m) ==> 
     ([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)
 done
 

 qed;
 
 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)
 by auto
 

 
 lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==> 
     [(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)";
     by (simp only: nat_add_distrib, auto)
   also have "p - 2 + 1 = p - 1" by arith

   also from prems have "[x ^ nat (p - 1) = 1] (mod p)";
     by (auto simp add: Little_Fermat) 
   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)
 
 lemma aux_1: "2 < p ==> ((nat p) - 2) = (nat (p - 2))";
   by (simp add: nat_diff_distrib)
 
 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)
   apply (drule_tac k = "MultInv p (MultInv p x)" in zcong_scalar, auto);
   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)
   apply (drule MultInv_prop2, auto)
   apply (drule_tac k = x in zcong_scalar2, auto)
   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 
     m = p and k = x in zcong_scalar)
   apply (insert MultInv_prop2 [of p x], simp)

 
 lemma aux___1: "[j = a * MultInv p k] (mod p) ==> 
     [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])
   apply (auto simp add: zmult_ac)
 done
 
 lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k = 
      (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 
     [of "MultInv p j * j" 1 p "MultInv p j * a" k])
   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)";
   apply (auto simp add: zcong_eq_zdvd_prop [of a p])
   apply (frule zprime_imp_zrelprime, auto)