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