src/HOL/Old_Number_Theory/EulerFermat.thy
author huffman
Sun, 13 Nov 2011 19:26:53 +0100
changeset 45480 a39bb6d42ace
parent 44766 d4d33a4d7548
child 45605 a89b4bc311a5
permissions -rw-r--r--
remove unnecessary number-representation-specific rules from metis calls; speed up another proof
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38159
e9b4835a54ee modernized specifications;
wenzelm
parents: 35440
diff changeset
     1
(*  Title:      HOL/Old_Number_Theory/EulerFermat.thy
e9b4835a54ee modernized specifications;
wenzelm
parents: 35440
diff changeset
     2
    Author:     Thomas M. Rasmussen
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
     3
    Copyright   2000  University of Cambridge
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     4
*)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
     5
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
     6
header {* Fermat's Little Theorem extended to Euler's Totient function *}
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
     7
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 26793
diff changeset
     8
theory EulerFermat
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 26793
diff changeset
     9
imports BijectionRel IntFact
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 26793
diff changeset
    10
begin
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    11
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    12
text {*
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    13
  Fermat's Little Theorem extended to Euler's Totient function. More
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    14
  abstract approach than Boyer-Moore (which seems necessary to achieve
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    15
  the extended version).
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    16
*}
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    17
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    18
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    19
subsection {* Definitions and lemmas *}
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    20
38159
e9b4835a54ee modernized specifications;
wenzelm
parents: 35440
diff changeset
    21
inductive_set RsetR :: "int => int set set" for m :: int
e9b4835a54ee modernized specifications;
wenzelm
parents: 35440
diff changeset
    22
where
e9b4835a54ee modernized specifications;
wenzelm
parents: 35440
diff changeset
    23
  empty [simp]: "{} \<in> RsetR m"
e9b4835a54ee modernized specifications;
wenzelm
parents: 35440
diff changeset
    24
| insert: "A \<in> RsetR m ==> zgcd a m = 1 ==>
e9b4835a54ee modernized specifications;
wenzelm
parents: 35440
diff changeset
    25
    \<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    26
38159
e9b4835a54ee modernized specifications;
wenzelm
parents: 35440
diff changeset
    27
fun BnorRset :: "int \<Rightarrow> int => int set" where
35440
bdf8ad377877 killed more recdefs
krauss
parents: 32960
diff changeset
    28
  "BnorRset a m =
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
    29
   (if 0 < a then
35440
bdf8ad377877 killed more recdefs
krauss
parents: 32960
diff changeset
    30
    let na = BnorRset (a - 1) m
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 26793
diff changeset
    31
    in (if zgcd a m = 1 then insert a na else na)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    32
    else {})"
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
    33
38159
e9b4835a54ee modernized specifications;
wenzelm
parents: 35440
diff changeset
    34
definition norRRset :: "int => int set"
e9b4835a54ee modernized specifications;
wenzelm
parents: 35440
diff changeset
    35
  where "norRRset m = BnorRset (m - 1) m"
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    36
38159
e9b4835a54ee modernized specifications;
wenzelm
parents: 35440
diff changeset
    37
definition noXRRset :: "int => int => int set"
e9b4835a54ee modernized specifications;
wenzelm
parents: 35440
diff changeset
    38
  where "noXRRset m x = (\<lambda>a. a * x) ` norRRset m"
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    39
38159
e9b4835a54ee modernized specifications;
wenzelm
parents: 35440
diff changeset
    40
definition phi :: "int => nat"
e9b4835a54ee modernized specifications;
wenzelm
parents: 35440
diff changeset
    41
  where "phi m = card (norRRset m)"
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    42
38159
e9b4835a54ee modernized specifications;
wenzelm
parents: 35440
diff changeset
    43
definition is_RRset :: "int set => int => bool"
e9b4835a54ee modernized specifications;
wenzelm
parents: 35440
diff changeset
    44
  where "is_RRset A m = (A \<in> RsetR m \<and> card A = phi m)"
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    45
38159
e9b4835a54ee modernized specifications;
wenzelm
parents: 35440
diff changeset
    46
definition RRset2norRR :: "int set => int => int => int"
e9b4835a54ee modernized specifications;
wenzelm
parents: 35440
diff changeset
    47
  where
e9b4835a54ee modernized specifications;
wenzelm
parents: 35440
diff changeset
    48
    "RRset2norRR A m a =
e9b4835a54ee modernized specifications;
wenzelm
parents: 35440
diff changeset
    49
       (if 1 < m \<and> is_RRset A m \<and> a \<in> A then
e9b4835a54ee modernized specifications;
wenzelm
parents: 35440
diff changeset
    50
          SOME b. zcong a b m \<and> b \<in> norRRset m
e9b4835a54ee modernized specifications;
wenzelm
parents: 35440
diff changeset
    51
        else 0)"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    52
38159
e9b4835a54ee modernized specifications;
wenzelm
parents: 35440
diff changeset
    53
definition zcongm :: "int => int => int => bool"
e9b4835a54ee modernized specifications;
wenzelm
parents: 35440
diff changeset
    54
  where "zcongm m = (\<lambda>a b. zcong a b m)"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    55
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
    56
lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    57
  -- {* LCP: not sure why this lemma is needed now *}
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16733
diff changeset
    58
  by (auto simp add: abs_if)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    59
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    60
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    61
text {* \medskip @{text norRRset} *}
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    62
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    63
declare BnorRset.simps [simp del]
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    64
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    65
lemma BnorRset_induct:
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16733
diff changeset
    66
  assumes "!!a m. P {} a m"
35440
bdf8ad377877 killed more recdefs
krauss
parents: 32960
diff changeset
    67
    and "!!a m :: int. 0 < a ==> P (BnorRset (a - 1) m) (a - 1) m
bdf8ad377877 killed more recdefs
krauss
parents: 32960
diff changeset
    68
      ==> P (BnorRset a m) a m"
bdf8ad377877 killed more recdefs
krauss
parents: 32960
diff changeset
    69
  shows "P (BnorRset u v) u v"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16733
diff changeset
    70
  apply (rule BnorRset.induct)
35440
bdf8ad377877 killed more recdefs
krauss
parents: 32960
diff changeset
    71
   apply (case_tac "0 < a")
bdf8ad377877 killed more recdefs
krauss
parents: 32960
diff changeset
    72
    apply (rule_tac assms)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16733
diff changeset
    73
     apply simp_all
35440
bdf8ad377877 killed more recdefs
krauss
parents: 32960
diff changeset
    74
   apply (simp_all add: BnorRset.simps assms)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    75
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    76
35440
bdf8ad377877 killed more recdefs
krauss
parents: 32960
diff changeset
    77
lemma Bnor_mem_zle [rule_format]: "b \<in> BnorRset a m \<longrightarrow> b \<le> a"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    78
  apply (induct a m rule: BnorRset_induct)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16733
diff changeset
    79
   apply simp
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16733
diff changeset
    80
  apply (subst BnorRset.simps)
13833
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
    81
   apply (unfold Let_def, auto)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    82
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    83
35440
bdf8ad377877 killed more recdefs
krauss
parents: 32960
diff changeset
    84
lemma Bnor_mem_zle_swap: "a < b ==> b \<notin> BnorRset a m"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16733
diff changeset
    85
  by (auto dest: Bnor_mem_zle)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    86
35440
bdf8ad377877 killed more recdefs
krauss
parents: 32960
diff changeset
    87
lemma Bnor_mem_zg [rule_format]: "b \<in> BnorRset a m --> 0 < b"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    88
  apply (induct a m rule: BnorRset_induct)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    89
   prefer 2
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    90
   apply (subst BnorRset.simps)
13833
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
    91
   apply (unfold Let_def, auto)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    92
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    93
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    94
lemma Bnor_mem_if [rule_format]:
35440
bdf8ad377877 killed more recdefs
krauss
parents: 32960
diff changeset
    95
    "zgcd b m = 1 --> 0 < b --> b \<le> a --> b \<in> BnorRset a m"
13833
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
    96
  apply (induct a m rule: BnorRset.induct, auto)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    97
   apply (subst BnorRset.simps)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    98
   defer
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
    99
   apply (subst BnorRset.simps)
13833
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
   100
   apply (unfold Let_def, auto)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   101
  done
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   102
35440
bdf8ad377877 killed more recdefs
krauss
parents: 32960
diff changeset
   103
lemma Bnor_in_RsetR [rule_format]: "a < m --> BnorRset a m \<in> RsetR m"
13833
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
   104
  apply (induct a m rule: BnorRset_induct, simp)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   105
  apply (subst BnorRset.simps)
13833
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
   106
  apply (unfold Let_def, auto)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   107
  apply (rule RsetR.insert)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   108
    apply (rule_tac [3] allI)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   109
    apply (rule_tac [3] impI)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   110
    apply (rule_tac [3] zcong_not)
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   111
       apply (subgoal_tac [6] "a' \<le> a - 1")
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   112
        apply (rule_tac [7] Bnor_mem_zle)
13833
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
   113
        apply (rule_tac [5] Bnor_mem_zg, auto)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   114
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   115
35440
bdf8ad377877 killed more recdefs
krauss
parents: 32960
diff changeset
   116
lemma Bnor_fin: "finite (BnorRset a m)"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   117
  apply (induct a m rule: BnorRset_induct)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   118
   prefer 2
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   119
   apply (subst BnorRset.simps)
13833
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
   120
   apply (unfold Let_def, auto)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   121
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   122
13524
604d0f3622d6 *** empty log message ***
wenzelm
parents: 13187
diff changeset
   123
lemma norR_mem_unique_aux: "a \<le> b - 1 ==> a < (b::int)"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   124
  apply auto
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   125
  done
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   126
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   127
lemma norR_mem_unique:
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   128
  "1 < m ==>
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 26793
diff changeset
   129
    zgcd a m = 1 ==> \<exists>!b. [a = b] (mod m) \<and> b \<in> norRRset m"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   130
  apply (unfold norRRset_def)
13833
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
   131
  apply (cut_tac a = a and m = m in zcong_zless_unique, auto)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   132
   apply (rule_tac [2] m = m in zcong_zless_imp_eq)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   133
       apply (auto intro: Bnor_mem_zle Bnor_mem_zg zcong_trans
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32479
diff changeset
   134
         order_less_imp_le norR_mem_unique_aux simp add: zcong_sym)
14174
f3cafd2929d5 Methods rule_tac etc support static (Isar) contexts.
ballarin
parents: 13833
diff changeset
   135
  apply (rule_tac x = b in exI, safe)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   136
  apply (rule Bnor_mem_if)
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   137
    apply (case_tac [2] "b = 0")
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   138
     apply (auto intro: order_less_le [THEN iffD2])
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   139
   prefer 2
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   140
   apply (simp only: zcong_def)
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 26793
diff changeset
   141
   apply (subgoal_tac "zgcd a m = m")
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   142
    prefer 2
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   143
    apply (subst zdvd_iff_zgcd [symmetric])
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   144
     apply (rule_tac [4] zgcd_zcong_zgcd)
45480
a39bb6d42ace remove unnecessary number-representation-specific rules from metis calls;
huffman
parents: 44766
diff changeset
   145
       apply (simp_all (no_asm_use) add: zcong_sym)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   146
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   147
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   148
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   149
text {* \medskip @{term noXRRset} *}
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   150
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   151
lemma RRset_gcd [rule_format]:
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 26793
diff changeset
   152
    "is_RRset A m ==> a \<in> A --> zgcd a m = 1"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   153
  apply (unfold is_RRset_def)
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 26793
diff changeset
   154
  apply (rule RsetR.induct [where P="%A. a \<in> A --> zgcd a m = 1"], auto)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   155
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   156
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   157
lemma RsetR_zmult_mono:
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   158
  "A \<in> RsetR m ==>
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 26793
diff changeset
   159
    0 < m ==> zgcd x m = 1 ==> (\<lambda>a. a * x) ` A \<in> RsetR m"
13833
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
   160
  apply (erule RsetR.induct, simp_all)
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
   161
  apply (rule RsetR.insert, auto)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   162
   apply (blast intro: zgcd_zgcd_zmult)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   163
  apply (simp add: zcong_cancel)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   164
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   165
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   166
lemma card_nor_eq_noX:
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   167
  "0 < m ==>
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 26793
diff changeset
   168
    zgcd x m = 1 ==> card (noXRRset m x) = card (norRRset m)"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   169
  apply (unfold norRRset_def noXRRset_def)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   170
  apply (rule card_image)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   171
   apply (auto simp add: inj_on_def Bnor_fin)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   172
  apply (simp add: BnorRset.simps)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   173
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   174
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   175
lemma noX_is_RRset:
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 26793
diff changeset
   176
    "0 < m ==> zgcd x m = 1 ==> is_RRset (noXRRset m x) m"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   177
  apply (unfold is_RRset_def phi_def)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   178
  apply (auto simp add: card_nor_eq_noX)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   179
  apply (unfold noXRRset_def norRRset_def)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   180
  apply (rule RsetR_zmult_mono)
13833
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
   181
    apply (rule Bnor_in_RsetR, simp_all)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   182
  done
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   183
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   184
lemma aux_some:
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   185
  "1 < m ==> is_RRset A m ==> a \<in> A
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   186
    ==> zcong a (SOME b. [a = b] (mod m) \<and> b \<in> norRRset m) m \<and>
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   187
      (SOME b. [a = b] (mod m) \<and> b \<in> norRRset m) \<in> norRRset m"
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   188
  apply (rule norR_mem_unique [THEN ex1_implies_ex, THEN someI_ex])
13833
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
   189
   apply (rule_tac [2] RRset_gcd, simp_all)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   190
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   191
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   192
lemma RRset2norRR_correct:
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   193
  "1 < m ==> is_RRset A m ==> a \<in> A ==>
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   194
    [a = RRset2norRR A m a] (mod m) \<and> RRset2norRR A m a \<in> norRRset m"
13833
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
   195
  apply (unfold RRset2norRR_def, simp)
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
   196
  apply (rule aux_some, simp_all)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   197
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   198
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   199
lemmas RRset2norRR_correct1 =
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   200
  RRset2norRR_correct [THEN conjunct1, standard]
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   201
lemmas RRset2norRR_correct2 =
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   202
  RRset2norRR_correct [THEN conjunct2, standard]
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   203
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   204
lemma RsetR_fin: "A \<in> RsetR m ==> finite A"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16733
diff changeset
   205
  by (induct set: RsetR) auto
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   206
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   207
lemma RRset_zcong_eq [rule_format]:
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   208
  "1 < m ==>
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   209
    is_RRset A m ==> [a = b] (mod m) ==> a \<in> A --> b \<in> A --> a = b"
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   210
  apply (unfold is_RRset_def)
26793
e36a92ff543e Instantiated some rules to avoid problems with HO unification.
berghofe
parents: 23755
diff changeset
   211
  apply (rule RsetR.induct [where P="%A. a \<in> A --> b \<in> A --> a = b"])
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   212
    apply (auto simp add: zcong_sym)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   213
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   214
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   215
lemma aux:
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   216
  "P (SOME a. P a) ==> Q (SOME a. Q a) ==>
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   217
    (SOME a. P a) = (SOME a. Q a) ==> \<exists>a. P a \<and> Q a"
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   218
  apply auto
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   219
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   220
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   221
lemma RRset2norRR_inj:
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   222
    "1 < m ==> is_RRset A m ==> inj_on (RRset2norRR A m) A"
13833
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
   223
  apply (unfold RRset2norRR_def inj_on_def, auto)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   224
  apply (subgoal_tac "\<exists>b. ([x = b] (mod m) \<and> b \<in> norRRset m) \<and>
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   225
      ([y = b] (mod m) \<and> b \<in> norRRset m)")
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   226
   apply (rule_tac [2] aux)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   227
     apply (rule_tac [3] aux_some)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   228
       apply (rule_tac [2] aux_some)
13833
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
   229
         apply (rule RRset_zcong_eq, auto)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   230
  apply (rule_tac b = b in zcong_trans)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   231
   apply (simp_all add: zcong_sym)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   232
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   233
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   234
lemma RRset2norRR_eq_norR:
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   235
    "1 < m ==> is_RRset A m ==> RRset2norRR A m ` A = norRRset m"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   236
  apply (rule card_seteq)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   237
    prefer 3
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   238
    apply (subst card_image)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   239
      apply (rule_tac RRset2norRR_inj, auto)
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   240
     apply (rule_tac [3] RRset2norRR_correct2, auto)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   241
    apply (unfold is_RRset_def phi_def norRRset_def)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   242
    apply (auto simp add: Bnor_fin)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   243
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   244
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   245
13524
604d0f3622d6 *** empty log message ***
wenzelm
parents: 13187
diff changeset
   246
lemma Bnor_prod_power_aux: "a \<notin> A ==> inj f ==> f a \<notin> f ` A"
13833
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
   247
by (unfold inj_on_def, auto)
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   248
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   249
lemma Bnor_prod_power [rule_format]:
35440
bdf8ad377877 killed more recdefs
krauss
parents: 32960
diff changeset
   250
  "x \<noteq> 0 ==> a < m --> \<Prod>((\<lambda>a. a * x) ` BnorRset a m) =
bdf8ad377877 killed more recdefs
krauss
parents: 32960
diff changeset
   251
      \<Prod>(BnorRset a m) * x^card (BnorRset a m)"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   252
  apply (induct a m rule: BnorRset_induct)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   253
   prefer 2
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 15402
diff changeset
   254
   apply (simplesubst BnorRset.simps)  --{*multiple redexes*}
13833
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
   255
   apply (unfold Let_def, auto)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   256
  apply (simp add: Bnor_fin Bnor_mem_zle_swap)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   257
  apply (subst setprod_insert)
13524
604d0f3622d6 *** empty log message ***
wenzelm
parents: 13187
diff changeset
   258
    apply (rule_tac [2] Bnor_prod_power_aux)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   259
     apply (unfold inj_on_def)
44766
d4d33a4d7548 avoid using legacy theorem names
huffman
parents: 40786
diff changeset
   260
     apply (simp_all add: mult_ac Bnor_fin Bnor_mem_zle_swap)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   261
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   262
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   263
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   264
subsection {* Fermat *}
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   265
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   266
lemma bijzcong_zcong_prod:
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15197
diff changeset
   267
    "(A, B) \<in> bijR (zcongm m) ==> [\<Prod>A = \<Prod>B] (mod m)"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   268
  apply (unfold zcongm_def)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   269
  apply (erule bijR.induct)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   270
   apply (subgoal_tac [2] "a \<notin> A \<and> b \<notin> B \<and> finite A \<and> finite B")
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   271
    apply (auto intro: fin_bijRl fin_bijRr zcong_zmult)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   272
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   273
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   274
lemma Bnor_prod_zgcd [rule_format]:
35440
bdf8ad377877 killed more recdefs
krauss
parents: 32960
diff changeset
   275
    "a < m --> zgcd (\<Prod>(BnorRset a m)) m = 1"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   276
  apply (induct a m rule: BnorRset_induct)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   277
   prefer 2
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   278
   apply (subst BnorRset.simps)
13833
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
   279
   apply (unfold Let_def, auto)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   280
  apply (simp add: Bnor_fin Bnor_mem_zle_swap)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   281
  apply (blast intro: zgcd_zgcd_zmult)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   282
  done
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   283
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   284
theorem Euler_Fermat:
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 26793
diff changeset
   285
    "0 < m ==> zgcd x m = 1 ==> [x^(phi m) = 1] (mod m)"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   286
  apply (unfold norRRset_def phi_def)
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   287
  apply (case_tac "x = 0")
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   288
   apply (case_tac [2] "m = 1")
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   289
    apply (rule_tac [3] iffD1)
35440
bdf8ad377877 killed more recdefs
krauss
parents: 32960
diff changeset
   290
     apply (rule_tac [3] k = "\<Prod>(BnorRset (m - 1) m)"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   291
       in zcong_cancel2)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   292
      prefer 5
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   293
      apply (subst Bnor_prod_power [symmetric])
13833
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
   294
        apply (rule_tac [7] Bnor_prod_zgcd, simp_all)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   295
  apply (rule bijzcong_zcong_prod)
35440
bdf8ad377877 killed more recdefs
krauss
parents: 32960
diff changeset
   296
  apply (fold norRRset_def, fold noXRRset_def)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   297
  apply (subst RRset2norRR_eq_norR [symmetric])
13833
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
   298
    apply (rule_tac [3] inj_func_bijR, auto)
13187
e5434b822a96 Modifications due to enhanced linear arithmetic.
nipkow
parents: 11868
diff changeset
   299
     apply (unfold zcongm_def)
e5434b822a96 Modifications due to enhanced linear arithmetic.
nipkow
parents: 11868
diff changeset
   300
     apply (rule_tac [2] RRset2norRR_correct1)
e5434b822a96 Modifications due to enhanced linear arithmetic.
nipkow
parents: 11868
diff changeset
   301
       apply (rule_tac [5] RRset2norRR_inj)
e5434b822a96 Modifications due to enhanced linear arithmetic.
nipkow
parents: 11868
diff changeset
   302
        apply (auto intro: order_less_le [THEN iffD2]
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32479
diff changeset
   303
           simp add: noX_is_RRset)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   304
  apply (unfold noXRRset_def norRRset_def)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   305
  apply (rule finite_imageI)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   306
  apply (rule Bnor_fin)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   307
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   308
16733
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16663
diff changeset
   309
lemma Bnor_prime:
35440
bdf8ad377877 killed more recdefs
krauss
parents: 32960
diff changeset
   310
  "\<lbrakk> zprime p; a < p \<rbrakk> \<Longrightarrow> card (BnorRset a p) = nat a"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   311
  apply (induct a p rule: BnorRset.induct)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   312
  apply (subst BnorRset.simps)
16733
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16663
diff changeset
   313
  apply (unfold Let_def, auto simp add:zless_zprime_imp_zrelprime)
35440
bdf8ad377877 killed more recdefs
krauss
parents: 32960
diff changeset
   314
  apply (subgoal_tac "finite (BnorRset (a - 1) m)")
bdf8ad377877 killed more recdefs
krauss
parents: 32960
diff changeset
   315
   apply (subgoal_tac "a ~: BnorRset (a - 1) m")
13833
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
   316
    apply (auto simp add: card_insert_disjoint Suc_nat_eq_nat_zadd1)
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
   317
   apply (frule Bnor_mem_zle, arith)
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
   318
  apply (frule Bnor_fin)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   319
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   320
16663
13e9c402308b prime is a predicate now.
nipkow
parents: 16417
diff changeset
   321
lemma phi_prime: "zprime p ==> phi p = nat (p - 1)"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   322
  apply (unfold phi_def norRRset_def)
13833
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
   323
  apply (rule Bnor_prime, auto)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   324
  done
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   325
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   326
theorem Little_Fermat:
16663
13e9c402308b prime is a predicate now.
nipkow
parents: 16417
diff changeset
   327
    "zprime p ==> \<not> p dvd x ==> [x^(nat (p - 1)) = 1] (mod p)"
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   328
  apply (subst phi_prime [symmetric])
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   329
   apply (rule_tac [2] Euler_Fermat)
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   330
    apply (erule_tac [3] zprime_imp_zrelprime)
13833
f8dcb1d9ea68 zprime_def fixes by Jeremy Avigad
paulson
parents: 13524
diff changeset
   331
    apply (unfold zprime_def, auto)
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 10834
diff changeset
   332
  done
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   333
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   334
end