src/HOL/Old_Number_Theory/WilsonRuss.thy
author wenzelm
Sat Oct 17 14:43:18 2009 +0200 (2009-10-17)
changeset 32960 69916a850301
parent 32479 521cc9bf2958
child 35048 82ab78fff970
permissions -rw-r--r--
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
haftmann@32479
     1
(*  Author:     Thomas M. Rasmussen
wenzelm@11049
     2
    Copyright   2000  University of Cambridge
paulson@9508
     3
*)
paulson@9508
     4
wenzelm@11049
     5
header {* Wilson's Theorem according to Russinoff *}
wenzelm@11049
     6
haftmann@16417
     7
theory WilsonRuss imports EulerFermat begin
wenzelm@11049
     8
wenzelm@11049
     9
text {*
wenzelm@11049
    10
  Wilson's Theorem following quite closely Russinoff's approach
wenzelm@11049
    11
  using Boyer-Moore (using finite sets instead of lists, though).
wenzelm@11049
    12
*}
wenzelm@11049
    13
wenzelm@11049
    14
subsection {* Definitions and lemmas *}
paulson@9508
    15
wenzelm@19670
    16
definition
wenzelm@21404
    17
  inv :: "int => int => int" where
wenzelm@19670
    18
  "inv p a = (a^(nat (p - 2))) mod p"
wenzelm@19670
    19
paulson@9508
    20
consts
wenzelm@11049
    21
  wset :: "int * int => int set"
paulson@9508
    22
wenzelm@11049
    23
recdef wset
wenzelm@11049
    24
  "measure ((\<lambda>(a, p). nat a) :: int * int => nat)"
wenzelm@11049
    25
  "wset (a, p) =
paulson@11868
    26
    (if 1 < a then
paulson@11868
    27
      let ws = wset (a - 1, p)
wenzelm@11049
    28
      in (if a \<in> ws then ws else insert a (insert (inv p a) ws)) else {})"
wenzelm@11049
    29
wenzelm@11049
    30
wenzelm@11049
    31
text {* \medskip @{term [source] inv} *}
wenzelm@11049
    32
wenzelm@13524
    33
lemma inv_is_inv_aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)"
paulson@13833
    34
by (subst int_int_eq [symmetric], auto)
wenzelm@11049
    35
wenzelm@11049
    36
lemma inv_is_inv:
nipkow@16663
    37
    "zprime p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> [a * inv p a = 1] (mod p)"
wenzelm@11049
    38
  apply (unfold inv_def)
wenzelm@11049
    39
  apply (subst zcong_zmod)
wenzelm@11049
    40
  apply (subst zmod_zmult1_eq [symmetric])
wenzelm@11049
    41
  apply (subst zcong_zmod [symmetric])
wenzelm@11049
    42
  apply (subst power_Suc [symmetric])
wenzelm@13524
    43
  apply (subst inv_is_inv_aux)
wenzelm@11049
    44
   apply (erule_tac [2] Little_Fermat)
wenzelm@11049
    45
   apply (erule_tac [2] zdvd_not_zless)
paulson@13833
    46
   apply (unfold zprime_def, auto)
wenzelm@11049
    47
  done
wenzelm@11049
    48
wenzelm@11049
    49
lemma inv_distinct:
nipkow@16663
    50
    "zprime p \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> a \<noteq> inv p a"
wenzelm@11049
    51
  apply safe
wenzelm@11049
    52
  apply (cut_tac a = a and p = p in zcong_square)
paulson@13833
    53
     apply (cut_tac [3] a = a and p = p in inv_is_inv, auto)
paulson@11868
    54
   apply (subgoal_tac "a = 1")
wenzelm@11049
    55
    apply (rule_tac [2] m = p in zcong_zless_imp_eq)
paulson@11868
    56
        apply (subgoal_tac [7] "a = p - 1")
paulson@13833
    57
         apply (rule_tac [8] m = p in zcong_zless_imp_eq, auto)
wenzelm@11049
    58
  done
wenzelm@11049
    59
wenzelm@11049
    60
lemma inv_not_0:
nipkow@16663
    61
    "zprime p \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a \<noteq> 0"
wenzelm@11049
    62
  apply safe
wenzelm@11049
    63
  apply (cut_tac a = a and p = p in inv_is_inv)
paulson@13833
    64
     apply (unfold zcong_def, auto)
paulson@11868
    65
  apply (subgoal_tac "\<not> p dvd 1")
wenzelm@11049
    66
   apply (rule_tac [2] zdvd_not_zless)
paulson@11868
    67
    apply (subgoal_tac "p dvd 1")
wenzelm@11049
    68
     prefer 2
nipkow@30042
    69
     apply (subst dvd_minus_iff [symmetric], auto)
wenzelm@11049
    70
  done
wenzelm@11049
    71
wenzelm@11049
    72
lemma inv_not_1:
nipkow@16663
    73
    "zprime p \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a \<noteq> 1"
wenzelm@11049
    74
  apply safe
wenzelm@11049
    75
  apply (cut_tac a = a and p = p in inv_is_inv)
wenzelm@11049
    76
     prefer 4
wenzelm@11049
    77
     apply simp
paulson@11868
    78
     apply (subgoal_tac "a = 1")
paulson@13833
    79
      apply (rule_tac [2] zcong_zless_imp_eq, auto)
wenzelm@11049
    80
  done
wenzelm@11049
    81
wenzelm@19670
    82
lemma inv_not_p_minus_1_aux:
wenzelm@19670
    83
    "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
wenzelm@11049
    84
  apply (unfold zcong_def)
obua@14738
    85
  apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
paulson@11868
    86
  apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
paulson@14271
    87
   apply (simp add: mult_commute)
nipkow@30042
    88
  apply (subst dvd_minus_iff)
wenzelm@11049
    89
  apply (subst zdvd_reduce)
paulson@11868
    90
  apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans)
paulson@13833
    91
   apply (subst zdvd_reduce, auto)
wenzelm@11049
    92
  done
wenzelm@11049
    93
wenzelm@11049
    94
lemma inv_not_p_minus_1:
nipkow@16663
    95
    "zprime p \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a \<noteq> p - 1"
wenzelm@11049
    96
  apply safe
paulson@13833
    97
  apply (cut_tac a = a and p = p in inv_is_inv, auto)
wenzelm@13524
    98
  apply (simp add: inv_not_p_minus_1_aux)
paulson@11868
    99
  apply (subgoal_tac "a = p - 1")
paulson@13833
   100
   apply (rule_tac [2] zcong_zless_imp_eq, auto)
wenzelm@11049
   101
  done
wenzelm@11049
   102
wenzelm@11049
   103
lemma inv_g_1:
nipkow@16663
   104
    "zprime p \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> 1 < inv p a"
paulson@11868
   105
  apply (case_tac "0\<le> inv p a")
paulson@11868
   106
   apply (subgoal_tac "inv p a \<noteq> 1")
paulson@11868
   107
    apply (subgoal_tac "inv p a \<noteq> 0")
wenzelm@11049
   108
     apply (subst order_less_le)
wenzelm@11049
   109
     apply (subst zle_add1_eq_le [symmetric])
wenzelm@11049
   110
     apply (subst order_less_le)
wenzelm@11049
   111
     apply (rule_tac [2] inv_not_0)
paulson@13833
   112
       apply (rule_tac [5] inv_not_1, auto)
paulson@13833
   113
  apply (unfold inv_def zprime_def, simp)
wenzelm@11049
   114
  done
wenzelm@11049
   115
wenzelm@11049
   116
lemma inv_less_p_minus_1:
nipkow@16663
   117
    "zprime p \<Longrightarrow> 1 < a \<Longrightarrow> a < p - 1 ==> inv p a < p - 1"
wenzelm@11049
   118
  apply (case_tac "inv p a < p")
wenzelm@11049
   119
   apply (subst order_less_le)
paulson@13833
   120
   apply (simp add: inv_not_p_minus_1, auto)
paulson@13833
   121
  apply (unfold inv_def zprime_def, simp)
wenzelm@11049
   122
  done
wenzelm@11049
   123
wenzelm@13524
   124
lemma inv_inv_aux: "5 \<le> p ==>
paulson@11868
   125
    nat (p - 2) * nat (p - 2) = Suc (nat (p - 1) * nat (p - 3))"
wenzelm@11049
   126
  apply (subst int_int_eq [symmetric])
wenzelm@11049
   127
  apply (simp add: zmult_int [symmetric])
wenzelm@11049
   128
  apply (simp add: zdiff_zmult_distrib zdiff_zmult_distrib2)
wenzelm@11049
   129
  done
wenzelm@11049
   130
wenzelm@11049
   131
lemma zcong_zpower_zmult:
paulson@11868
   132
    "[x^y = 1] (mod p) \<Longrightarrow> [x^(y * z) = 1] (mod p)"
wenzelm@11049
   133
  apply (induct z)
wenzelm@11049
   134
   apply (auto simp add: zpower_zadd_distrib)
nipkow@15236
   135
  apply (subgoal_tac "zcong (x^y * x^(y * z)) (1 * 1) p")
paulson@13833
   136
   apply (rule_tac [2] zcong_zmult, simp_all)
wenzelm@11049
   137
  done
wenzelm@11049
   138
nipkow@16663
   139
lemma inv_inv: "zprime p \<Longrightarrow>
paulson@11868
   140
    5 \<le> p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a"
wenzelm@11049
   141
  apply (unfold inv_def)
wenzelm@11049
   142
  apply (subst zpower_zmod)
wenzelm@11049
   143
  apply (subst zpower_zpower)
wenzelm@11049
   144
  apply (rule zcong_zless_imp_eq)
wenzelm@11049
   145
      prefer 5
wenzelm@11049
   146
      apply (subst zcong_zmod)
wenzelm@11049
   147
      apply (subst mod_mod_trivial)
wenzelm@11049
   148
      apply (subst zcong_zmod [symmetric])
wenzelm@13524
   149
      apply (subst inv_inv_aux)
wenzelm@11049
   150
       apply (subgoal_tac [2]
wenzelm@32960
   151
         "zcong (a * a^(nat (p - 1) * nat (p - 3))) (a * 1) p")
wenzelm@11049
   152
        apply (rule_tac [3] zcong_zmult)
wenzelm@11049
   153
         apply (rule_tac [4] zcong_zpower_zmult)
wenzelm@11049
   154
         apply (erule_tac [4] Little_Fermat)
paulson@13833
   155
         apply (rule_tac [4] zdvd_not_zless, simp_all)
wenzelm@11049
   156
  done
wenzelm@11049
   157
wenzelm@11049
   158
wenzelm@11049
   159
text {* \medskip @{term wset} *}
wenzelm@11049
   160
wenzelm@11049
   161
declare wset.simps [simp del]
paulson@9508
   162
wenzelm@11049
   163
lemma wset_induct:
wenzelm@18369
   164
  assumes "!!a p. P {} a p"
wenzelm@19670
   165
    and "!!a p. 1 < (a::int) \<Longrightarrow>
wenzelm@19670
   166
      P (wset (a - 1, p)) (a - 1) p ==> P (wset (a, p)) a p"
wenzelm@18369
   167
  shows "P (wset (u, v)) u v"
wenzelm@18369
   168
  apply (rule wset.induct, safe)
wenzelm@18369
   169
   prefer 2
wenzelm@18369
   170
   apply (case_tac "1 < a")
wenzelm@18369
   171
    apply (rule prems)
wenzelm@18369
   172
     apply simp_all
wenzelm@18369
   173
   apply (simp_all add: wset.simps prems)
wenzelm@18369
   174
  done
wenzelm@11049
   175
wenzelm@11049
   176
lemma wset_mem_imp_or [rule_format]:
paulson@11868
   177
  "1 < a \<Longrightarrow> b \<notin> wset (a - 1, p)
wenzelm@11049
   178
    ==> b \<in> wset (a, p) --> b = a \<or> b = inv p a"
wenzelm@11049
   179
  apply (subst wset.simps)
paulson@13833
   180
  apply (unfold Let_def, simp)
wenzelm@11049
   181
  done
wenzelm@11049
   182
paulson@11868
   183
lemma wset_mem_mem [simp]: "1 < a ==> a \<in> wset (a, p)"
wenzelm@11049
   184
  apply (subst wset.simps)
paulson@13833
   185
  apply (unfold Let_def, simp)
wenzelm@11049
   186
  done
wenzelm@11049
   187
paulson@11868
   188
lemma wset_subset: "1 < a \<Longrightarrow> b \<in> wset (a - 1, p) ==> b \<in> wset (a, p)"
wenzelm@11049
   189
  apply (subst wset.simps)
paulson@13833
   190
  apply (unfold Let_def, auto)
wenzelm@11049
   191
  done
wenzelm@11049
   192
wenzelm@11049
   193
lemma wset_g_1 [rule_format]:
nipkow@16663
   194
    "zprime p --> a < p - 1 --> b \<in> wset (a, p) --> 1 < b"
paulson@13833
   195
  apply (induct a p rule: wset_induct, auto)
wenzelm@11049
   196
  apply (case_tac "b = a")
wenzelm@11049
   197
   apply (case_tac [2] "b = inv p a")
wenzelm@11049
   198
    apply (subgoal_tac [3] "b = a \<or> b = inv p a")
wenzelm@11049
   199
     apply (rule_tac [4] wset_mem_imp_or)
wenzelm@11049
   200
       prefer 2
wenzelm@11049
   201
       apply simp
paulson@13833
   202
       apply (rule inv_g_1, auto)
wenzelm@11049
   203
  done
wenzelm@11049
   204
wenzelm@11049
   205
lemma wset_less [rule_format]:
nipkow@16663
   206
    "zprime p --> a < p - 1 --> b \<in> wset (a, p) --> b < p - 1"
paulson@13833
   207
  apply (induct a p rule: wset_induct, auto)
wenzelm@11049
   208
  apply (case_tac "b = a")
wenzelm@11049
   209
   apply (case_tac [2] "b = inv p a")
wenzelm@11049
   210
    apply (subgoal_tac [3] "b = a \<or> b = inv p a")
wenzelm@11049
   211
     apply (rule_tac [4] wset_mem_imp_or)
wenzelm@11049
   212
       prefer 2
wenzelm@11049
   213
       apply simp
paulson@13833
   214
       apply (rule inv_less_p_minus_1, auto)
wenzelm@11049
   215
  done
wenzelm@11049
   216
wenzelm@11049
   217
lemma wset_mem [rule_format]:
nipkow@16663
   218
  "zprime p -->
paulson@11868
   219
    a < p - 1 --> 1 < b --> b \<le> a --> b \<in> wset (a, p)"
paulson@13833
   220
  apply (induct a p rule: wset.induct, auto)
nipkow@15197
   221
  apply (rule_tac wset_subset)
nipkow@15197
   222
  apply (simp (no_asm_simp))
nipkow@15197
   223
  apply auto
wenzelm@11049
   224
  done
wenzelm@11049
   225
wenzelm@11049
   226
lemma wset_mem_inv_mem [rule_format]:
nipkow@16663
   227
  "zprime p --> 5 \<le> p --> a < p - 1 --> b \<in> wset (a, p)
wenzelm@11049
   228
    --> inv p b \<in> wset (a, p)"
paulson@13833
   229
  apply (induct a p rule: wset_induct, auto)
wenzelm@11049
   230
   apply (case_tac "b = a")
wenzelm@11049
   231
    apply (subst wset.simps)
wenzelm@11049
   232
    apply (unfold Let_def)
paulson@13833
   233
    apply (rule_tac [3] wset_subset, auto)
wenzelm@11049
   234
  apply (case_tac "b = inv p a")
wenzelm@11049
   235
   apply (simp (no_asm_simp))
wenzelm@11049
   236
   apply (subst inv_inv)
wenzelm@11049
   237
       apply (subgoal_tac [6] "b = a \<or> b = inv p a")
paulson@13833
   238
        apply (rule_tac [7] wset_mem_imp_or, auto)
wenzelm@11049
   239
  done
wenzelm@11049
   240
wenzelm@11049
   241
lemma wset_inv_mem_mem:
nipkow@16663
   242
  "zprime p \<Longrightarrow> 5 \<le> p \<Longrightarrow> a < p - 1 \<Longrightarrow> 1 < b \<Longrightarrow> b < p - 1
wenzelm@11049
   243
    \<Longrightarrow> inv p b \<in> wset (a, p) \<Longrightarrow> b \<in> wset (a, p)"
wenzelm@11049
   244
  apply (rule_tac s = "inv p (inv p b)" and t = b in subst)
wenzelm@11049
   245
   apply (rule_tac [2] wset_mem_inv_mem)
paulson@13833
   246
      apply (rule inv_inv, simp_all)
wenzelm@11049
   247
  done
wenzelm@11049
   248
wenzelm@11049
   249
lemma wset_fin: "finite (wset (a, p))"
wenzelm@11049
   250
  apply (induct a p rule: wset_induct)
wenzelm@11049
   251
   prefer 2
wenzelm@11049
   252
   apply (subst wset.simps)
paulson@13833
   253
   apply (unfold Let_def, auto)
wenzelm@11049
   254
  done
wenzelm@11049
   255
wenzelm@11049
   256
lemma wset_zcong_prod_1 [rule_format]:
nipkow@16663
   257
  "zprime p -->
nipkow@15392
   258
    5 \<le> p --> a < p - 1 --> [(\<Prod>x\<in>wset(a, p). x) = 1] (mod p)"
wenzelm@11049
   259
  apply (induct a p rule: wset_induct)
wenzelm@11049
   260
   prefer 2
wenzelm@11049
   261
   apply (subst wset.simps)
paulson@13833
   262
   apply (unfold Let_def, auto)
wenzelm@11049
   263
  apply (subst setprod_insert)
wenzelm@11049
   264
    apply (tactic {* stac (thm "setprod_insert") 3 *})
wenzelm@11049
   265
      apply (subgoal_tac [5]
wenzelm@32960
   266
        "zcong (a * inv p a * (\<Prod>x\<in> wset(a - 1, p). x)) (1 * 1) p")
wenzelm@11049
   267
       prefer 5
wenzelm@11049
   268
       apply (simp add: zmult_assoc)
wenzelm@11049
   269
      apply (rule_tac [5] zcong_zmult)
wenzelm@11049
   270
       apply (rule_tac [5] inv_is_inv)
wenzelm@23894
   271
         apply (tactic "clarify_tac @{claset} 4")
paulson@11868
   272
         apply (subgoal_tac [4] "a \<in> wset (a - 1, p)")
wenzelm@11049
   273
          apply (rule_tac [5] wset_inv_mem_mem)
wenzelm@11049
   274
               apply (simp_all add: wset_fin)
paulson@13833
   275
  apply (rule inv_distinct, auto)
wenzelm@11049
   276
  done
wenzelm@11049
   277
nipkow@16663
   278
lemma d22set_eq_wset: "zprime p ==> d22set (p - 2) = wset (p - 2, p)"
wenzelm@11049
   279
  apply safe
wenzelm@11049
   280
   apply (erule wset_mem)
wenzelm@11049
   281
     apply (rule_tac [2] d22set_g_1)
wenzelm@11049
   282
     apply (rule_tac [3] d22set_le)
wenzelm@11049
   283
     apply (rule_tac [4] d22set_mem)
wenzelm@11049
   284
      apply (erule_tac [4] wset_g_1)
wenzelm@11049
   285
       prefer 6
wenzelm@11049
   286
       apply (subst zle_add1_eq_le [symmetric])
paulson@11868
   287
       apply (subgoal_tac "p - 2 + 1 = p - 1")
wenzelm@11049
   288
        apply (simp (no_asm_simp))
paulson@13833
   289
        apply (erule wset_less, auto)
wenzelm@11049
   290
  done
wenzelm@11049
   291
wenzelm@11049
   292
wenzelm@11049
   293
subsection {* Wilson *}
wenzelm@11049
   294
nipkow@16663
   295
lemma prime_g_5: "zprime p \<Longrightarrow> p \<noteq> 2 \<Longrightarrow> p \<noteq> 3 ==> 5 \<le> p"
wenzelm@11049
   296
  apply (unfold zprime_def dvd_def)
paulson@13833
   297
  apply (case_tac "p = 4", auto)
wenzelm@11049
   298
   apply (rule notE)
wenzelm@11049
   299
    prefer 2
wenzelm@11049
   300
    apply assumption
wenzelm@11049
   301
   apply (simp (no_asm))
paulson@13833
   302
   apply (rule_tac x = 2 in exI)
paulson@13833
   303
   apply (safe, arith)
paulson@13833
   304
     apply (rule_tac x = 2 in exI, auto)
wenzelm@11049
   305
  done
wenzelm@11049
   306
wenzelm@11049
   307
theorem Wilson_Russ:
nipkow@16663
   308
    "zprime p ==> [zfact (p - 1) = -1] (mod p)"
paulson@11868
   309
  apply (subgoal_tac "[(p - 1) * zfact (p - 2) = -1 * 1] (mod p)")
wenzelm@11049
   310
   apply (rule_tac [2] zcong_zmult)
wenzelm@11049
   311
    apply (simp only: zprime_def)
wenzelm@11049
   312
    apply (subst zfact.simps)
paulson@13833
   313
    apply (rule_tac t = "p - 1 - 1" and s = "p - 2" in subst, auto)
wenzelm@11049
   314
   apply (simp only: zcong_def)
wenzelm@11049
   315
   apply (simp (no_asm_simp))
wenzelm@11704
   316
  apply (case_tac "p = 2")
wenzelm@11049
   317
   apply (simp add: zfact.simps)
wenzelm@11704
   318
  apply (case_tac "p = 3")
wenzelm@11049
   319
   apply (simp add: zfact.simps)
wenzelm@11704
   320
  apply (subgoal_tac "5 \<le> p")
wenzelm@11049
   321
   apply (erule_tac [2] prime_g_5)
wenzelm@11049
   322
    apply (subst d22set_prod_zfact [symmetric])
wenzelm@11049
   323
    apply (subst d22set_eq_wset)
paulson@13833
   324
     apply (rule_tac [2] wset_zcong_prod_1, auto)
wenzelm@11049
   325
  done
paulson@9508
   326
paulson@9508
   327
end