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