src/HOL/NumberTheory/Int2.thy
author paulson
Fri Mar 05 11:43:55 2004 +0100 (2004-03-05)
changeset 14434 5f14c1207499
parent 14387 e96d5c42c4b0
child 14981 e73f8140af78
permissions -rw-r--r--
patch to NumberTheory problems caused by Parity
paulson@13871
     1
(*  Title:      HOL/Quadratic_Reciprocity/Gauss.thy
paulson@13871
     2
    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
paulson@13871
     3
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
paulson@13871
     4
*)
paulson@13871
     5
paulson@13871
     6
header {*Integers: Divisibility and Congruences*}
paulson@13871
     7
paulson@13871
     8
theory Int2 = Finite2 + WilsonRuss:;
paulson@13871
     9
paulson@13871
    10
text{*Note.  This theory is being revised.  See the web page
paulson@13871
    11
\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
paulson@13871
    12
paulson@13871
    13
constdefs
paulson@13871
    14
  MultInv :: "int => int => int" 
paulson@13871
    15
  "MultInv p x == x ^ nat (p - 2)";
paulson@13871
    16
paulson@13871
    17
(*****************************************************************)
paulson@13871
    18
(*                                                               *)
paulson@13871
    19
(* Useful lemmas about dvd and powers                            *)
paulson@13871
    20
(*                                                               *)
paulson@13871
    21
(*****************************************************************)
paulson@13871
    22
paulson@13871
    23
lemma zpower_zdvd_prop1 [rule_format]: "((0 < n) & (p dvd y)) --> 
paulson@13871
    24
    p dvd ((y::int) ^ n)";
paulson@13871
    25
  by (induct_tac n, auto simp add: zdvd_zmult zdvd_zmult2 [of p y])
paulson@13871
    26
paulson@13871
    27
lemma zdvd_bounds: "n dvd m ==> (m \<le> (0::int) | n \<le> m)";
paulson@13871
    28
proof -;
paulson@13871
    29
  assume "n dvd m";
paulson@13871
    30
  then have "~(0 < m & m < n)";
paulson@13871
    31
    apply (insert zdvd_not_zless [of m n])
paulson@13871
    32
    by (rule contrapos_pn, auto)
paulson@13871
    33
  then have "(~0 < m | ~m < n)"  by auto
paulson@13871
    34
  then show ?thesis by auto
paulson@13871
    35
qed;
paulson@13871
    36
paulson@13871
    37
lemma aux4: " -(m * n) = (-m) * (n::int)";
paulson@13871
    38
  by auto
paulson@13871
    39
paulson@13871
    40
lemma zprime_zdvd_zmult_better: "[| p \<in> zprime;  p dvd (m * n) |] ==> 
paulson@13871
    41
    (p dvd m) | (p dvd n)";
paulson@13871
    42
  apply (case_tac "0 \<le> m")
paulson@13871
    43
  apply (simp add: zprime_zdvd_zmult)
paulson@13871
    44
  by (insert zprime_zdvd_zmult [of "-m" p n], auto)
paulson@13871
    45
paulson@13871
    46
lemma zpower_zdvd_prop2 [rule_format]: "p \<in> zprime --> p dvd ((y::int) ^ n) 
paulson@13871
    47
    --> 0 < n --> p dvd y";
paulson@13871
    48
  apply (induct_tac n, auto)
paulson@13871
    49
  apply (frule zprime_zdvd_zmult_better, auto)
paulson@13871
    50
done
paulson@13871
    51
paulson@13871
    52
lemma stupid: "(0 :: int) \<le> y ==> x \<le> x + y";
paulson@13871
    53
  by arith
paulson@13871
    54
paulson@13871
    55
lemma div_prop1: "[| 0 < z; (x::int) < y * z |] ==> x div z < y";
paulson@13871
    56
proof -;
paulson@13871
    57
  assume "0 < z";
paulson@13871
    58
  then have "(x div z) * z \<le> (x div z) * z + x mod z";
paulson@13871
    59
  apply (rule_tac x = "x div z * z" in stupid)
paulson@13871
    60
  by (simp add: pos_mod_sign)
paulson@13871
    61
  also have "... = x";
paulson@13871
    62
    by (auto simp add: zmod_zdiv_equality [THEN sym] zmult_ac)
paulson@13871
    63
  also assume  "x < y * z";
paulson@13871
    64
  finally show ?thesis;
paulson@14387
    65
    by (auto simp add: prems mult_less_cancel_right, insert prems, arith)
paulson@13871
    66
qed;
paulson@13871
    67
paulson@13871
    68
lemma div_prop2: "[| 0 < z; (x::int) < (y * z) + z |] ==> x div z \<le> y";
paulson@13871
    69
proof -;
paulson@13871
    70
  assume "0 < z" and "x < (y * z) + z";
paulson@13871
    71
  then have "x < (y + 1) * z" by (auto simp add: int_distrib)
paulson@13871
    72
  then have "x div z < y + 1";
paulson@13871
    73
    by (rule_tac y = "y + 1" in div_prop1, auto simp add: prems)
paulson@13871
    74
  then show ?thesis by auto
paulson@13871
    75
qed;
paulson@13871
    76
paulson@13871
    77
lemma zdiv_leq_prop: "[| 0 < y |] ==> y * (x div y) \<le> (x::int)";
paulson@13871
    78
proof-;
paulson@13871
    79
  assume "0 < y";
paulson@13871
    80
  from zmod_zdiv_equality have "x = y * (x div y) + x mod y" by auto
paulson@13871
    81
  moreover have "0 \<le> x mod y";
paulson@13871
    82
    by (auto simp add: prems pos_mod_sign)
paulson@13871
    83
  ultimately show ?thesis;
paulson@13871
    84
    by arith
paulson@13871
    85
qed;
paulson@13871
    86
paulson@13871
    87
(*****************************************************************)
paulson@13871
    88
(*                                                               *)
paulson@13871
    89
(* Useful properties of congruences                              *)
paulson@13871
    90
(*                                                               *)
paulson@13871
    91
(*****************************************************************)
paulson@13871
    92
paulson@13871
    93
lemma zcong_eq_zdvd_prop: "[x = 0](mod p) = (p dvd x)";
paulson@13871
    94
  by (auto simp add: zcong_def)
paulson@13871
    95
paulson@13871
    96
lemma zcong_id: "[m = 0] (mod m)";
paulson@13871
    97
  by (auto simp add: zcong_def zdvd_0_right)
paulson@13871
    98
paulson@13871
    99
lemma zcong_shift: "[a = b] (mod m) ==> [a + c = b + c] (mod m)";
paulson@13871
   100
  by (auto simp add: zcong_refl zcong_zadd)
paulson@13871
   101
paulson@13871
   102
lemma zcong_zpower: "[x = y](mod m) ==> [x^z = y^z](mod m)";
paulson@13871
   103
  by (induct_tac z, auto simp add: zcong_zmult)
paulson@13871
   104
paulson@13871
   105
lemma zcong_eq_trans: "[| [a = b](mod m); b = c; [c = d](mod m) |] ==> 
paulson@13871
   106
    [a = d](mod m)";
paulson@13871
   107
  by (auto, rule_tac b = c in zcong_trans)
paulson@13871
   108
paulson@13871
   109
lemma aux1: "a - b = (c::int) ==> a = c + b";
paulson@13871
   110
  by auto
paulson@13871
   111
paulson@13871
   112
lemma zcong_zmult_prop1: "[a = b](mod m) ==> ([c = a * d](mod m) = 
paulson@13871
   113
    [c = b * d] (mod m))";
paulson@13871
   114
  apply (auto simp add: zcong_def dvd_def)
paulson@13871
   115
  apply (rule_tac x = "ka + k * d" in exI)
paulson@13871
   116
  apply (drule aux1)+;
paulson@13871
   117
  apply (auto simp add: int_distrib)
paulson@13871
   118
  apply (rule_tac x = "ka - k * d" in exI)
paulson@13871
   119
  apply (drule aux1)+;
paulson@13871
   120
  apply (auto simp add: int_distrib)
paulson@13871
   121
done
paulson@13871
   122
paulson@13871
   123
lemma zcong_zmult_prop2: "[a = b](mod m) ==> 
paulson@13871
   124
    ([c = d * a](mod m) = [c = d * b] (mod m))";
paulson@13871
   125
  by (auto simp add: zmult_ac zcong_zmult_prop1)
paulson@13871
   126
paulson@13871
   127
lemma zcong_zmult_prop3: "[|p \<in> zprime; ~[x = 0] (mod p); 
paulson@13871
   128
    ~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)";
paulson@13871
   129
  apply (auto simp add: zcong_def)
paulson@13871
   130
  apply (drule zprime_zdvd_zmult_better, auto)
paulson@13871
   131
done
paulson@13871
   132
paulson@13871
   133
lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m); 
paulson@13871
   134
    x < m; y < m |] ==> x = y";
paulson@13871
   135
  apply (simp add: zcong_zmod_eq)
paulson@13871
   136
  apply (subgoal_tac "(x mod m) = x");
paulson@13871
   137
  apply (subgoal_tac "(y mod m) = y");
paulson@13871
   138
  apply simp
paulson@13871
   139
  apply (rule_tac [1-2] mod_pos_pos_trivial)
paulson@13871
   140
by auto
paulson@13871
   141
paulson@13871
   142
lemma zcong_neg_1_impl_ne_1: "[| 2 < p; [x = -1] (mod p) |] ==> 
paulson@13871
   143
    ~([x = 1] (mod p))";
paulson@13871
   144
proof;
paulson@13871
   145
  assume "2 < p" and "[x = 1] (mod p)" and "[x = -1] (mod p)"
paulson@13871
   146
  then have "[1 = -1] (mod p)";
paulson@13871
   147
    apply (auto simp add: zcong_sym)
paulson@13871
   148
    apply (drule zcong_trans, auto)
paulson@13871
   149
  done
paulson@13871
   150
  then have "[1 + 1 = -1 + 1] (mod p)";
paulson@13871
   151
    by (simp only: zcong_shift)
paulson@13871
   152
  then have "[2 = 0] (mod p)";
paulson@13871
   153
    by auto
paulson@13871
   154
  then have "p dvd 2";
paulson@13871
   155
    by (auto simp add: dvd_def zcong_def)
paulson@13871
   156
  with prems show False;
paulson@13871
   157
    by (auto simp add: zdvd_not_zless)
paulson@13871
   158
qed;
paulson@13871
   159
paulson@13871
   160
lemma zcong_zero_equiv_div: "[a = 0] (mod m) = (m dvd a)";
paulson@13871
   161
  by (auto simp add: zcong_def)
paulson@13871
   162
paulson@13871
   163
lemma zcong_zprime_prod_zero: "[| p \<in> zprime; 0 < a |] ==> 
paulson@13871
   164
  [a * b = 0] (mod p) ==> [a = 0] (mod p) | [b = 0] (mod p)"; 
paulson@13871
   165
  by (auto simp add: zcong_zero_equiv_div zprime_zdvd_zmult)
paulson@13871
   166
paulson@13871
   167
lemma zcong_zprime_prod_zero_contra: "[| p \<in> zprime; 0 < a |] ==>
paulson@13871
   168
  ~[a = 0](mod p) & ~[b = 0](mod p) ==> ~[a * b = 0] (mod p)";
paulson@13871
   169
  apply auto 
paulson@13871
   170
  apply (frule_tac a = a and b = b and p = p in zcong_zprime_prod_zero)
paulson@13871
   171
by auto
paulson@13871
   172
paulson@13871
   173
lemma zcong_not_zero: "[| 0 < x; x < m |] ==> ~[x = 0] (mod m)"; 
paulson@13871
   174
  by (auto simp add: zcong_zero_equiv_div zdvd_not_zless)
paulson@13871
   175
paulson@13871
   176
lemma zcong_zero: "[| 0 \<le> x; x < m; [x = 0](mod m) |] ==> x = 0";
paulson@13871
   177
  apply (drule order_le_imp_less_or_eq, auto)
paulson@13871
   178
by (frule_tac m = m in zcong_not_zero, auto)
paulson@13871
   179
paulson@13871
   180
lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. (zgcd(x,y) = 1) |]
paulson@13871
   181
    ==> zgcd (gsetprod id A,y) = 1";
paulson@13871
   182
  by (induct set: Finites, auto simp add: zgcd_zgcd_zmult)
paulson@13871
   183
paulson@13871
   184
(*****************************************************************)
paulson@13871
   185
(*                                                               *)
paulson@13871
   186
(* Some properties of MultInv                                    *)
paulson@13871
   187
(*                                                               *)
paulson@13871
   188
(*****************************************************************)
paulson@13871
   189
paulson@13871
   190
lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==> 
paulson@13871
   191
    [(MultInv p x) = (MultInv p y)] (mod p)";
paulson@13871
   192
  by (auto simp add: MultInv_def zcong_zpower)
paulson@13871
   193
paulson@13871
   194
lemma MultInv_prop2: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==> 
paulson@13871
   195
  [(x * (MultInv p x)) = 1] (mod p)";
paulson@13871
   196
proof (simp add: MultInv_def zcong_eq_zdvd_prop);
paulson@13871
   197
  assume "2 < p" and "p \<in> zprime" and "~ p dvd x";
paulson@13871
   198
  have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)";
paulson@13871
   199
    by auto
paulson@13871
   200
  also from prems have "nat (p - 2) + 1 = nat (p - 2 + 1)";
paulson@13871
   201
    by (simp only: nat_add_distrib, auto)
paulson@13871
   202
  also have "p - 2 + 1 = p - 1" by arith
paulson@13871
   203
  finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)";
paulson@13871
   204
    by (rule ssubst, auto)
paulson@13871
   205
  also from prems have "[x ^ nat (p - 1) = 1] (mod p)";
paulson@13871
   206
    by (auto simp add: Little_Fermat) 
paulson@13871
   207
  finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)";.;
paulson@13871
   208
qed;
paulson@13871
   209
paulson@13871
   210
lemma MultInv_prop2a: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==> 
paulson@13871
   211
    [(MultInv p x) * x = 1] (mod p)";
paulson@13871
   212
  by (auto simp add: MultInv_prop2 zmult_ac)
paulson@13871
   213
paulson@13871
   214
lemma aux_1: "2 < p ==> ((nat p) - 2) = (nat (p - 2))";
paulson@13871
   215
  by (simp add: nat_diff_distrib)
paulson@13871
   216
paulson@13871
   217
lemma aux_2: "2 < p ==> 0 < nat (p - 2)";
paulson@13871
   218
  by auto
paulson@13871
   219
paulson@13871
   220
lemma MultInv_prop3: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==> 
paulson@13871
   221
    ~([MultInv p x = 0](mod p))";
paulson@13871
   222
  apply (auto simp add: MultInv_def zcong_eq_zdvd_prop aux_1)
paulson@13871
   223
  apply (drule aux_2)
paulson@13871
   224
  apply (drule zpower_zdvd_prop2, auto)
paulson@13871
   225
done
paulson@13871
   226
paulson@13871
   227
lemma aux__1: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p))|] ==> 
paulson@13871
   228
    [(MultInv p (MultInv p x)) = (x * (MultInv p x) * 
paulson@13871
   229
      (MultInv p (MultInv p x)))] (mod p)";
paulson@13871
   230
  apply (drule MultInv_prop2, auto)
paulson@13871
   231
  apply (drule_tac k = "MultInv p (MultInv p x)" in zcong_scalar, auto);
paulson@13871
   232
  apply (auto simp add: zcong_sym)
paulson@13871
   233
done
paulson@13871
   234
paulson@13871
   235
lemma aux__2: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p))|] ==>
paulson@13871
   236
    [(x * (MultInv p x) * (MultInv p (MultInv p x))) = x] (mod p)";
paulson@13871
   237
  apply (frule MultInv_prop3, auto)
paulson@13871
   238
  apply (insert MultInv_prop2 [of p "MultInv p x"], auto)
paulson@13871
   239
  apply (drule MultInv_prop2, auto)
paulson@13871
   240
  apply (drule_tac k = x in zcong_scalar2, auto)
paulson@13871
   241
  apply (auto simp add: zmult_ac)
paulson@13871
   242
done
paulson@13871
   243
paulson@13871
   244
lemma MultInv_prop4: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)) |] ==> 
paulson@13871
   245
    [(MultInv p (MultInv p x)) = x] (mod p)";
paulson@13871
   246
  apply (frule aux__1, auto)
paulson@13871
   247
  apply (drule aux__2, auto)
paulson@13871
   248
  apply (drule zcong_trans, auto)
paulson@13871
   249
done
paulson@13871
   250
paulson@13871
   251
lemma MultInv_prop5: "[| 2 < p; p \<in> zprime; ~([x = 0](mod p)); 
paulson@13871
   252
    ~([y = 0](mod p)); [(MultInv p x) = (MultInv p y)] (mod p) |] ==> 
paulson@13871
   253
    [x = y] (mod p)";
paulson@13871
   254
  apply (drule_tac a = "MultInv p x" and b = "MultInv p y" and 
paulson@13871
   255
    m = p and k = x in zcong_scalar)
paulson@13871
   256
  apply (insert MultInv_prop2 [of p x], simp)
paulson@13871
   257
  apply (auto simp only: zcong_sym [of "MultInv p x * x"])
paulson@13871
   258
  apply (auto simp add:  zmult_ac)
paulson@13871
   259
  apply (drule zcong_trans, auto)
paulson@13871
   260
  apply (drule_tac a = "x * MultInv p y" and k = y in zcong_scalar, auto)
paulson@13871
   261
  apply (insert MultInv_prop2a [of p y], auto simp add: zmult_ac)
paulson@13871
   262
  apply (insert zcong_zmult_prop2 [of "y * MultInv p y" 1 p y x])
paulson@13871
   263
  apply (auto simp add: zcong_sym)
paulson@13871
   264
done
paulson@13871
   265
paulson@13871
   266
lemma MultInv_zcong_prop1: "[| 2 < p; [j = k] (mod p) |] ==> 
paulson@13871
   267
    [a * MultInv p j = a * MultInv p k] (mod p)";
paulson@13871
   268
  by (drule MultInv_prop1, auto simp add: zcong_scalar2)
paulson@13871
   269
paulson@13871
   270
lemma aux___1: "[j = a * MultInv p k] (mod p) ==> 
paulson@13871
   271
    [j * k = a * MultInv p k * k] (mod p)";
paulson@13871
   272
  by (auto simp add: zcong_scalar)
paulson@13871
   273
paulson@13871
   274
lemma aux___2: "[|2 < p; p \<in> zprime; ~([k = 0](mod p)); 
paulson@13871
   275
    [j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)";
paulson@13871
   276
  apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2 
paulson@13871
   277
    [of "MultInv p k * k" 1 p "j * k" a])
paulson@13871
   278
  apply (auto simp add: zmult_ac)
paulson@13871
   279
done
paulson@13871
   280
paulson@13871
   281
lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k = 
paulson@13871
   282
     (MultInv p j) * a] (mod p)";
paulson@13871
   283
  by (auto simp add: zmult_assoc zcong_scalar2)
paulson@13871
   284
paulson@13871
   285
lemma aux___4: "[|2 < p; p \<in> zprime; ~([j = 0](mod p)); 
paulson@13871
   286
    [(MultInv p j) * j * k = (MultInv p j) * a] (mod p) |]
paulson@13871
   287
       ==> [k = a * (MultInv p j)] (mod p)";
paulson@13871
   288
  apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1 
paulson@13871
   289
    [of "MultInv p j * j" 1 p "MultInv p j * a" k])
paulson@13871
   290
  apply (auto simp add: zmult_ac zcong_sym)
paulson@13871
   291
done
paulson@13871
   292
paulson@13871
   293
lemma MultInv_zcong_prop2: "[| 2 < p; p \<in> zprime; ~([k = 0](mod p)); 
paulson@13871
   294
    ~([j = 0](mod p)); [j = a * MultInv p k] (mod p) |] ==> 
paulson@13871
   295
    [k = a * MultInv p j] (mod p)";
paulson@13871
   296
  apply (drule aux___1)
paulson@13871
   297
  apply (frule aux___2, auto)
paulson@13871
   298
  by (drule aux___3, drule aux___4, auto)
paulson@13871
   299
paulson@13871
   300
lemma MultInv_zcong_prop3: "[| 2 < p; p \<in> zprime; ~([a = 0](mod p)); 
paulson@13871
   301
    ~([k = 0](mod p)); ~([j = 0](mod p));
paulson@13871
   302
    [a * MultInv p j = a * MultInv p k] (mod p) |] ==> 
paulson@13871
   303
      [j = k] (mod p)";
paulson@13871
   304
  apply (auto simp add: zcong_eq_zdvd_prop [of a p])
paulson@13871
   305
  apply (frule zprime_imp_zrelprime, auto)
paulson@13871
   306
  apply (insert zcong_cancel2 [of p a "MultInv p j" "MultInv p k"], auto)
paulson@13871
   307
  apply (drule MultInv_prop5, auto)
paulson@13871
   308
done
paulson@13871
   309
paulson@13871
   310
end