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.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)";
```