src/HOL/NumberTheory/Int2.thy
changeset 16663 13e9c402308b
parent 16417 9bc16273c2d4
child 18369 694ea14ab4f2
     1.1 --- a/src/HOL/NumberTheory/Int2.thy	Fri Jul 01 14:55:05 2005 +0200
     1.2 +++ b/src/HOL/NumberTheory/Int2.thy	Fri Jul 01 17:41:10 2005 +0200
     1.3 @@ -37,13 +37,13 @@
     1.4  lemma aux4: " -(m * n) = (-m) * (n::int)";
     1.5    by auto
     1.6  
     1.7 -lemma zprime_zdvd_zmult_better: "[| p \<in> zprime;  p dvd (m * n) |] ==> 
     1.8 +lemma zprime_zdvd_zmult_better: "[| zprime p;  p dvd (m * n) |] ==> 
     1.9      (p dvd m) | (p dvd n)";
    1.10    apply (case_tac "0 \<le> m")
    1.11    apply (simp add: zprime_zdvd_zmult)
    1.12    by (insert zprime_zdvd_zmult [of "-m" p n], auto)
    1.13  
    1.14 -lemma zpower_zdvd_prop2 [rule_format]: "p \<in> zprime --> p dvd ((y::int) ^ n) 
    1.15 +lemma zpower_zdvd_prop2 [rule_format]: "zprime p --> p dvd ((y::int) ^ n) 
    1.16      --> 0 < n --> p dvd y";
    1.17    apply (induct_tac n, auto)
    1.18    apply (frule zprime_zdvd_zmult_better, auto)
    1.19 @@ -124,7 +124,7 @@
    1.20      ([c = d * a](mod m) = [c = d * b] (mod m))";
    1.21    by (auto simp add: zmult_ac zcong_zmult_prop1)
    1.22  
    1.23 -lemma zcong_zmult_prop3: "[|p \<in> zprime; ~[x = 0] (mod p); 
    1.24 +lemma zcong_zmult_prop3: "[| zprime p; ~[x = 0] (mod p); 
    1.25      ~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)";
    1.26    apply (auto simp add: zcong_def)
    1.27    apply (drule zprime_zdvd_zmult_better, auto)
    1.28 @@ -160,11 +160,11 @@
    1.29  lemma zcong_zero_equiv_div: "[a = 0] (mod m) = (m dvd a)";
    1.30    by (auto simp add: zcong_def)
    1.31  
    1.32 -lemma zcong_zprime_prod_zero: "[| p \<in> zprime; 0 < a |] ==> 
    1.33 +lemma zcong_zprime_prod_zero: "[| zprime p; 0 < a |] ==> 
    1.34    [a * b = 0] (mod p) ==> [a = 0] (mod p) | [b = 0] (mod p)"; 
    1.35    by (auto simp add: zcong_zero_equiv_div zprime_zdvd_zmult)
    1.36  
    1.37 -lemma zcong_zprime_prod_zero_contra: "[| p \<in> zprime; 0 < a |] ==>
    1.38 +lemma zcong_zprime_prod_zero_contra: "[| zprime p; 0 < a |] ==>
    1.39    ~[a = 0](mod p) & ~[b = 0](mod p) ==> ~[a * b = 0] (mod p)";
    1.40    apply auto 
    1.41    apply (frule_tac a = a and b = b and p = p in zcong_zprime_prod_zero)
    1.42 @@ -191,10 +191,10 @@
    1.43      [(MultInv p x) = (MultInv p y)] (mod p)";
    1.44    by (auto simp add: MultInv_def zcong_zpower)
    1.45  
    1.46 -lemma MultInv_prop2: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==> 
    1.47 +lemma MultInv_prop2: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> 
    1.48    [(x * (MultInv p x)) = 1] (mod p)";
    1.49  proof (simp add: MultInv_def zcong_eq_zdvd_prop);
    1.50 -  assume "2 < p" and "p \<in> zprime" and "~ p dvd x";
    1.51 +  assume "2 < p" and "zprime p" and "~ p dvd x";
    1.52    have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)";
    1.53      by auto
    1.54    also from prems have "nat (p - 2) + 1 = nat (p - 2 + 1)";
    1.55 @@ -207,7 +207,7 @@
    1.56    finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)";.;
    1.57  qed;
    1.58  
    1.59 -lemma MultInv_prop2a: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==> 
    1.60 +lemma MultInv_prop2a: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> 
    1.61      [(MultInv p x) * x = 1] (mod p)";
    1.62    by (auto simp add: MultInv_prop2 zmult_ac)
    1.63  
    1.64 @@ -217,14 +217,14 @@
    1.65  lemma aux_2: "2 < p ==> 0 < nat (p - 2)";
    1.66    by auto
    1.67  
    1.68 -lemma MultInv_prop3: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==> 
    1.69 +lemma MultInv_prop3: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> 
    1.70      ~([MultInv p x = 0](mod p))";
    1.71    apply (auto simp add: MultInv_def zcong_eq_zdvd_prop aux_1)
    1.72    apply (drule aux_2)
    1.73    apply (drule zpower_zdvd_prop2, auto)
    1.74  done
    1.75  
    1.76 -lemma aux__1: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p))|] ==> 
    1.77 +lemma aux__1: "[| 2 < p; zprime p; ~([x = 0](mod p))|] ==> 
    1.78      [(MultInv p (MultInv p x)) = (x * (MultInv p x) * 
    1.79        (MultInv p (MultInv p x)))] (mod p)";
    1.80    apply (drule MultInv_prop2, auto)
    1.81 @@ -232,7 +232,7 @@
    1.82    apply (auto simp add: zcong_sym)
    1.83  done
    1.84  
    1.85 -lemma aux__2: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p))|] ==>
    1.86 +lemma aux__2: "[| 2 < p; zprime p; ~([x = 0](mod p))|] ==>
    1.87      [(x * (MultInv p x) * (MultInv p (MultInv p x))) = x] (mod p)";
    1.88    apply (frule MultInv_prop3, auto)
    1.89    apply (insert MultInv_prop2 [of p "MultInv p x"], auto)
    1.90 @@ -241,14 +241,14 @@
    1.91    apply (auto simp add: zmult_ac)
    1.92  done
    1.93  
    1.94 -lemma MultInv_prop4: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==> 
    1.95 +lemma MultInv_prop4: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> 
    1.96      [(MultInv p (MultInv p x)) = x] (mod p)";
    1.97    apply (frule aux__1, auto)
    1.98    apply (drule aux__2, auto)
    1.99    apply (drule zcong_trans, auto)
   1.100  done
   1.101  
   1.102 -lemma MultInv_prop5: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)); 
   1.103 +lemma MultInv_prop5: "[| 2 < p; zprime p; ~([x = 0](mod p)); 
   1.104      ~([y = 0](mod p)); [(MultInv p x) = (MultInv p y)] (mod p) |] ==> 
   1.105      [x = y] (mod p)";
   1.106    apply (drule_tac a = "MultInv p x" and b = "MultInv p y" and 
   1.107 @@ -271,7 +271,7 @@
   1.108      [j * k = a * MultInv p k * k] (mod p)";
   1.109    by (auto simp add: zcong_scalar)
   1.110  
   1.111 -lemma aux___2: "[|2 < p; p \<in> zprime; ~([k = 0](mod p)); 
   1.112 +lemma aux___2: "[|2 < p; zprime p; ~([k = 0](mod p)); 
   1.113      [j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)";
   1.114    apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2 
   1.115      [of "MultInv p k * k" 1 p "j * k" a])
   1.116 @@ -282,7 +282,7 @@
   1.117       (MultInv p j) * a] (mod p)";
   1.118    by (auto simp add: zmult_assoc zcong_scalar2)
   1.119  
   1.120 -lemma aux___4: "[|2 < p; p \<in> zprime; ~([j = 0](mod p)); 
   1.121 +lemma aux___4: "[|2 < p; zprime p; ~([j = 0](mod p)); 
   1.122      [(MultInv p j) * j * k = (MultInv p j) * a] (mod p) |]
   1.123         ==> [k = a * (MultInv p j)] (mod p)";
   1.124    apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1 
   1.125 @@ -290,14 +290,14 @@
   1.126    apply (auto simp add: zmult_ac zcong_sym)
   1.127  done
   1.128  
   1.129 -lemma MultInv_zcong_prop2: "[| 2 < p; p \<in> zprime; ~([k = 0](mod p)); 
   1.130 +lemma MultInv_zcong_prop2: "[| 2 < p; zprime p; ~([k = 0](mod p)); 
   1.131      ~([j = 0](mod p)); [j = a * MultInv p k] (mod p) |] ==> 
   1.132      [k = a * MultInv p j] (mod p)";
   1.133    apply (drule aux___1)
   1.134    apply (frule aux___2, auto)
   1.135    by (drule aux___3, drule aux___4, auto)
   1.136  
   1.137 -lemma MultInv_zcong_prop3: "[| 2 < p; p \<in> zprime; ~([a = 0](mod p)); 
   1.138 +lemma MultInv_zcong_prop3: "[| 2 < p; zprime p; ~([a = 0](mod p)); 
   1.139      ~([k = 0](mod p)); ~([j = 0](mod p));
   1.140      [a * MultInv p j = a * MultInv p k] (mod p) |] ==> 
   1.141        [j = k] (mod p)";