src/HOL/Old_Number_Theory/EulerFermat.thy
 author wenzelm Thu May 26 17:51:22 2016 +0200 (2016-05-26) changeset 63167 0909deb8059b parent 61945 1135b8de26c3 child 64272 f76b6dda2e56 permissions -rw-r--r--
isabelle update_cartouches -c -t;
```     1 (*  Title:      HOL/Old_Number_Theory/EulerFermat.thy
```
```     2     Author:     Thomas M. Rasmussen
```
```     3     Copyright   2000  University of Cambridge
```
```     4 *)
```
```     5
```
```     6 section \<open>Fermat's Little Theorem extended to Euler's Totient function\<close>
```
```     7
```
```     8 theory EulerFermat
```
```     9 imports BijectionRel IntFact
```
```    10 begin
```
```    11
```
```    12 text \<open>
```
```    13   Fermat's Little Theorem extended to Euler's Totient function. More
```
```    14   abstract approach than Boyer-Moore (which seems necessary to achieve
```
```    15   the extended version).
```
```    16 \<close>
```
```    17
```
```    18
```
```    19 subsection \<open>Definitions and lemmas\<close>
```
```    20
```
```    21 inductive_set RsetR :: "int => int set set" for m :: int
```
```    22 where
```
```    23   empty [simp]: "{} \<in> RsetR m"
```
```    24 | insert: "A \<in> RsetR m ==> zgcd a m = 1 ==>
```
```    25     \<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
```
```    26
```
```    27 fun BnorRset :: "int \<Rightarrow> int => int set" where
```
```    28   "BnorRset a m =
```
```    29    (if 0 < a then
```
```    30     let na = BnorRset (a - 1) m
```
```    31     in (if zgcd a m = 1 then insert a na else na)
```
```    32     else {})"
```
```    33
```
```    34 definition norRRset :: "int => int set"
```
```    35   where "norRRset m = BnorRset (m - 1) m"
```
```    36
```
```    37 definition noXRRset :: "int => int => int set"
```
```    38   where "noXRRset m x = (\<lambda>a. a * x) ` norRRset m"
```
```    39
```
```    40 definition phi :: "int => nat"
```
```    41   where "phi m = card (norRRset m)"
```
```    42
```
```    43 definition is_RRset :: "int set => int => bool"
```
```    44   where "is_RRset A m = (A \<in> RsetR m \<and> card A = phi m)"
```
```    45
```
```    46 definition RRset2norRR :: "int set => int => int => int"
```
```    47   where
```
```    48     "RRset2norRR A m a =
```
```    49        (if 1 < m \<and> is_RRset A m \<and> a \<in> A then
```
```    50           SOME b. zcong a b m \<and> b \<in> norRRset m
```
```    51         else 0)"
```
```    52
```
```    53 definition zcongm :: "int => int => int => bool"
```
```    54   where "zcongm m = (\<lambda>a b. zcong a b m)"
```
```    55
```
```    56 lemma abs_eq_1_iff [iff]: "(\<bar>z\<bar> = (1::int)) = (z = 1 \<or> z = -1)"
```
```    57   \<comment> \<open>LCP: not sure why this lemma is needed now\<close>
```
```    58   by (auto simp add: abs_if)
```
```    59
```
```    60
```
```    61 text \<open>\medskip \<open>norRRset\<close>\<close>
```
```    62
```
```    63 declare BnorRset.simps [simp del]
```
```    64
```
```    65 lemma BnorRset_induct:
```
```    66   assumes "!!a m. P {} a m"
```
```    67     and "!!a m :: int. 0 < a ==> P (BnorRset (a - 1) m) (a - 1) m
```
```    68       ==> P (BnorRset a m) a m"
```
```    69   shows "P (BnorRset u v) u v"
```
```    70   apply (rule BnorRset.induct)
```
```    71    apply (case_tac "0 < a")
```
```    72     apply (rule_tac assms)
```
```    73      apply simp_all
```
```    74    apply (simp_all add: BnorRset.simps assms)
```
```    75   done
```
```    76
```
```    77 lemma Bnor_mem_zle [rule_format]: "b \<in> BnorRset a m \<longrightarrow> b \<le> a"
```
```    78   apply (induct a m rule: BnorRset_induct)
```
```    79    apply simp
```
```    80   apply (subst BnorRset.simps)
```
```    81    apply (unfold Let_def, auto)
```
```    82   done
```
```    83
```
```    84 lemma Bnor_mem_zle_swap: "a < b ==> b \<notin> BnorRset a m"
```
```    85   by (auto dest: Bnor_mem_zle)
```
```    86
```
```    87 lemma Bnor_mem_zg [rule_format]: "b \<in> BnorRset a m --> 0 < b"
```
```    88   apply (induct a m rule: BnorRset_induct)
```
```    89    prefer 2
```
```    90    apply (subst BnorRset.simps)
```
```    91    apply (unfold Let_def, auto)
```
```    92   done
```
```    93
```
```    94 lemma Bnor_mem_if [rule_format]:
```
```    95     "zgcd b m = 1 --> 0 < b --> b \<le> a --> b \<in> BnorRset a m"
```
```    96   apply (induct a m rule: BnorRset.induct, auto)
```
```    97    apply (subst BnorRset.simps)
```
```    98    defer
```
```    99    apply (subst BnorRset.simps)
```
```   100    apply (unfold Let_def, auto)
```
```   101   done
```
```   102
```
```   103 lemma Bnor_in_RsetR [rule_format]: "a < m --> BnorRset a m \<in> RsetR m"
```
```   104   apply (induct a m rule: BnorRset_induct, simp)
```
```   105   apply (subst BnorRset.simps)
```
```   106   apply (unfold Let_def, auto)
```
```   107   apply (rule RsetR.insert)
```
```   108     apply (rule_tac [3] allI)
```
```   109     apply (rule_tac [3] impI)
```
```   110     apply (rule_tac [3] zcong_not)
```
```   111        apply (subgoal_tac [6] "a' \<le> a - 1")
```
```   112         apply (rule_tac [7] Bnor_mem_zle)
```
```   113         apply (rule_tac [5] Bnor_mem_zg, auto)
```
```   114   done
```
```   115
```
```   116 lemma Bnor_fin: "finite (BnorRset a m)"
```
```   117   apply (induct a m rule: BnorRset_induct)
```
```   118    prefer 2
```
```   119    apply (subst BnorRset.simps)
```
```   120    apply (unfold Let_def, auto)
```
```   121   done
```
```   122
```
```   123 lemma norR_mem_unique_aux: "a \<le> b - 1 ==> a < (b::int)"
```
```   124   apply auto
```
```   125   done
```
```   126
```
```   127 lemma norR_mem_unique:
```
```   128   "1 < m ==>
```
```   129     zgcd a m = 1 ==> \<exists>!b. [a = b] (mod m) \<and> b \<in> norRRset m"
```
```   130   apply (unfold norRRset_def)
```
```   131   apply (cut_tac a = a and m = m in zcong_zless_unique, auto)
```
```   132    apply (rule_tac [2] m = m in zcong_zless_imp_eq)
```
```   133        apply (auto intro: Bnor_mem_zle Bnor_mem_zg zcong_trans
```
```   134          order_less_imp_le norR_mem_unique_aux simp add: zcong_sym)
```
```   135   apply (rule_tac x = b in exI, safe)
```
```   136   apply (rule Bnor_mem_if)
```
```   137     apply (case_tac [2] "b = 0")
```
```   138      apply (auto intro: order_less_le [THEN iffD2])
```
```   139    prefer 2
```
```   140    apply (simp only: zcong_def)
```
```   141    apply (subgoal_tac "zgcd a m = m")
```
```   142     prefer 2
```
```   143     apply (subst zdvd_iff_zgcd [symmetric])
```
```   144      apply (rule_tac [4] zgcd_zcong_zgcd)
```
```   145        apply (simp_all (no_asm_use) add: zcong_sym)
```
```   146   done
```
```   147
```
```   148
```
```   149 text \<open>\medskip @{term noXRRset}\<close>
```
```   150
```
```   151 lemma RRset_gcd [rule_format]:
```
```   152     "is_RRset A m ==> a \<in> A --> zgcd a m = 1"
```
```   153   apply (unfold is_RRset_def)
```
```   154   apply (rule RsetR.induct, auto)
```
```   155   done
```
```   156
```
```   157 lemma RsetR_zmult_mono:
```
```   158   "A \<in> RsetR m ==>
```
```   159     0 < m ==> zgcd x m = 1 ==> (\<lambda>a. a * x) ` A \<in> RsetR m"
```
```   160   apply (erule RsetR.induct, simp_all)
```
```   161   apply (rule RsetR.insert, auto)
```
```   162    apply (blast intro: zgcd_zgcd_zmult)
```
```   163   apply (simp add: zcong_cancel)
```
```   164   done
```
```   165
```
```   166 lemma card_nor_eq_noX:
```
```   167   "0 < m ==>
```
```   168     zgcd x m = 1 ==> card (noXRRset m x) = card (norRRset m)"
```
```   169   apply (unfold norRRset_def noXRRset_def)
```
```   170   apply (rule card_image)
```
```   171    apply (auto simp add: inj_on_def Bnor_fin)
```
```   172   apply (simp add: BnorRset.simps)
```
```   173   done
```
```   174
```
```   175 lemma noX_is_RRset:
```
```   176     "0 < m ==> zgcd x m = 1 ==> is_RRset (noXRRset m x) m"
```
```   177   apply (unfold is_RRset_def phi_def)
```
```   178   apply (auto simp add: card_nor_eq_noX)
```
```   179   apply (unfold noXRRset_def norRRset_def)
```
```   180   apply (rule RsetR_zmult_mono)
```
```   181     apply (rule Bnor_in_RsetR, simp_all)
```
```   182   done
```
```   183
```
```   184 lemma aux_some:
```
```   185   "1 < m ==> is_RRset A m ==> a \<in> A
```
```   186     ==> zcong a (SOME b. [a = b] (mod m) \<and> b \<in> norRRset m) m \<and>
```
```   187       (SOME b. [a = b] (mod m) \<and> b \<in> norRRset m) \<in> norRRset m"
```
```   188   apply (rule norR_mem_unique [THEN ex1_implies_ex, THEN someI_ex])
```
```   189    apply (rule_tac [2] RRset_gcd, simp_all)
```
```   190   done
```
```   191
```
```   192 lemma RRset2norRR_correct:
```
```   193   "1 < m ==> is_RRset A m ==> a \<in> A ==>
```
```   194     [a = RRset2norRR A m a] (mod m) \<and> RRset2norRR A m a \<in> norRRset m"
```
```   195   apply (unfold RRset2norRR_def, simp)
```
```   196   apply (rule aux_some, simp_all)
```
```   197   done
```
```   198
```
```   199 lemmas RRset2norRR_correct1 = RRset2norRR_correct [THEN conjunct1]
```
```   200 lemmas RRset2norRR_correct2 = RRset2norRR_correct [THEN conjunct2]
```
```   201
```
```   202 lemma RsetR_fin: "A \<in> RsetR m ==> finite A"
```
```   203   by (induct set: RsetR) auto
```
```   204
```
```   205 lemma RRset_zcong_eq [rule_format]:
```
```   206   "1 < m ==>
```
```   207     is_RRset A m ==> [a = b] (mod m) ==> a \<in> A --> b \<in> A --> a = b"
```
```   208   apply (unfold is_RRset_def)
```
```   209   apply (rule RsetR.induct)
```
```   210     apply (auto simp add: zcong_sym)
```
```   211   done
```
```   212
```
```   213 lemma aux:
```
```   214   "P (SOME a. P a) ==> Q (SOME a. Q a) ==>
```
```   215     (SOME a. P a) = (SOME a. Q a) ==> \<exists>a. P a \<and> Q a"
```
```   216   apply auto
```
```   217   done
```
```   218
```
```   219 lemma RRset2norRR_inj:
```
```   220     "1 < m ==> is_RRset A m ==> inj_on (RRset2norRR A m) A"
```
```   221   apply (unfold RRset2norRR_def inj_on_def, auto)
```
```   222   apply (subgoal_tac "\<exists>b. ([x = b] (mod m) \<and> b \<in> norRRset m) \<and>
```
```   223       ([y = b] (mod m) \<and> b \<in> norRRset m)")
```
```   224    apply (rule_tac [2] aux)
```
```   225      apply (rule_tac [3] aux_some)
```
```   226        apply (rule_tac [2] aux_some)
```
```   227          apply (rule RRset_zcong_eq, auto)
```
```   228   apply (rule_tac b = b in zcong_trans)
```
```   229    apply (simp_all add: zcong_sym)
```
```   230   done
```
```   231
```
```   232 lemma RRset2norRR_eq_norR:
```
```   233     "1 < m ==> is_RRset A m ==> RRset2norRR A m ` A = norRRset m"
```
```   234   apply (rule card_seteq)
```
```   235     prefer 3
```
```   236     apply (subst card_image)
```
```   237       apply (rule_tac RRset2norRR_inj, auto)
```
```   238      apply (rule_tac [3] RRset2norRR_correct2, auto)
```
```   239     apply (unfold is_RRset_def phi_def norRRset_def)
```
```   240     apply (auto simp add: Bnor_fin)
```
```   241   done
```
```   242
```
```   243
```
```   244 lemma Bnor_prod_power_aux: "a \<notin> A ==> inj f ==> f a \<notin> f ` A"
```
```   245 by (unfold inj_on_def, auto)
```
```   246
```
```   247 lemma Bnor_prod_power [rule_format]:
```
```   248   "x \<noteq> 0 ==> a < m --> \<Prod>((\<lambda>a. a * x) ` BnorRset a m) =
```
```   249       \<Prod>(BnorRset a m) * x^card (BnorRset a m)"
```
```   250   apply (induct a m rule: BnorRset_induct)
```
```   251    prefer 2
```
```   252    apply (simplesubst BnorRset.simps)  \<comment>\<open>multiple redexes\<close>
```
```   253    apply (unfold Let_def, auto)
```
```   254   apply (simp add: Bnor_fin Bnor_mem_zle_swap)
```
```   255   apply (subst setprod.insert)
```
```   256     apply (rule_tac [2] Bnor_prod_power_aux)
```
```   257      apply (unfold inj_on_def)
```
```   258      apply (simp_all add: ac_simps Bnor_fin Bnor_mem_zle_swap)
```
```   259   done
```
```   260
```
```   261
```
```   262 subsection \<open>Fermat\<close>
```
```   263
```
```   264 lemma bijzcong_zcong_prod:
```
```   265     "(A, B) \<in> bijR (zcongm m) ==> [\<Prod>A = \<Prod>B] (mod m)"
```
```   266   apply (unfold zcongm_def)
```
```   267   apply (erule bijR.induct)
```
```   268    apply (subgoal_tac [2] "a \<notin> A \<and> b \<notin> B \<and> finite A \<and> finite B")
```
```   269     apply (auto intro: fin_bijRl fin_bijRr zcong_zmult)
```
```   270   done
```
```   271
```
```   272 lemma Bnor_prod_zgcd [rule_format]:
```
```   273     "a < m --> zgcd (\<Prod>(BnorRset a m)) m = 1"
```
```   274   apply (induct a m rule: BnorRset_induct)
```
```   275    prefer 2
```
```   276    apply (subst BnorRset.simps)
```
```   277    apply (unfold Let_def, auto)
```
```   278   apply (simp add: Bnor_fin Bnor_mem_zle_swap)
```
```   279   apply (blast intro: zgcd_zgcd_zmult)
```
```   280   done
```
```   281
```
```   282 theorem Euler_Fermat:
```
```   283     "0 < m ==> zgcd x m = 1 ==> [x^(phi m) = 1] (mod m)"
```
```   284   apply (unfold norRRset_def phi_def)
```
```   285   apply (case_tac "x = 0")
```
```   286    apply (case_tac [2] "m = 1")
```
```   287     apply (rule_tac [3] iffD1)
```
```   288      apply (rule_tac [3] k = "\<Prod>(BnorRset (m - 1) m)"
```
```   289        in zcong_cancel2)
```
```   290       prefer 5
```
```   291       apply (subst Bnor_prod_power [symmetric])
```
```   292         apply (rule_tac [7] Bnor_prod_zgcd, simp_all)
```
```   293   apply (rule bijzcong_zcong_prod)
```
```   294   apply (fold norRRset_def, fold noXRRset_def)
```
```   295   apply (subst RRset2norRR_eq_norR [symmetric])
```
```   296     apply (rule_tac [3] inj_func_bijR, auto)
```
```   297      apply (unfold zcongm_def)
```
```   298      apply (rule_tac [2] RRset2norRR_correct1)
```
```   299        apply (rule_tac [5] RRset2norRR_inj)
```
```   300         apply (auto intro: order_less_le [THEN iffD2]
```
```   301            simp add: noX_is_RRset)
```
```   302   apply (unfold noXRRset_def norRRset_def)
```
```   303   apply (rule finite_imageI)
```
```   304   apply (rule Bnor_fin)
```
```   305   done
```
```   306
```
```   307 lemma Bnor_prime:
```
```   308   "\<lbrakk> zprime p; a < p \<rbrakk> \<Longrightarrow> card (BnorRset a p) = nat a"
```
```   309   apply (induct a p rule: BnorRset.induct)
```
```   310   apply (subst BnorRset.simps)
```
```   311   apply (unfold Let_def, auto simp add:zless_zprime_imp_zrelprime)
```
```   312   apply (subgoal_tac "finite (BnorRset (a - 1) m)")
```
```   313    apply (subgoal_tac "a ~: BnorRset (a - 1) m")
```
```   314     apply (auto simp add: card_insert_disjoint Suc_nat_eq_nat_zadd1)
```
```   315    apply (frule Bnor_mem_zle, arith)
```
```   316   apply (frule Bnor_fin)
```
```   317   done
```
```   318
```
```   319 lemma phi_prime: "zprime p ==> phi p = nat (p - 1)"
```
```   320   apply (unfold phi_def norRRset_def)
```
```   321   apply (rule Bnor_prime, auto)
```
```   322   done
```
```   323
```
```   324 theorem Little_Fermat:
```
```   325     "zprime p ==> \<not> p dvd x ==> [x^(nat (p - 1)) = 1] (mod p)"
```
```   326   apply (subst phi_prime [symmetric])
```
```   327    apply (rule_tac [2] Euler_Fermat)
```
```   328     apply (erule_tac [3] zprime_imp_zrelprime)
```
```   329     apply (unfold zprime_def, auto)
```
```   330   done
```
```   331
```
```   332 end
```