src/HOL/Number_Theory/Residues.thy
 changeset 66305 7454317f883c parent 66304 cde6ceffcbc7 child 66453 cc19f7ca2ed6
```     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Tue Aug 01 17:33:04 2017 +0200
1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Tue Aug 01 22:19:37 2017 +0200
1.3 @@ -17,24 +17,26 @@
1.4    Totient
1.5  begin
1.6
1.7 -definition QuadRes :: "int \<Rightarrow> int \<Rightarrow> bool" where
1.8 -  "QuadRes p a = (\<exists>y. ([y^2 = a] (mod p)))"
1.9 +definition QuadRes :: "int \<Rightarrow> int \<Rightarrow> bool"
1.10 +  where "QuadRes p a = (\<exists>y. ([y^2 = a] (mod p)))"
1.11
1.12 -definition Legendre :: "int \<Rightarrow> int \<Rightarrow> int" where
1.13 -  "Legendre a p = (if ([a = 0] (mod p)) then 0
1.14 -    else if QuadRes p a then 1
1.15 -    else -1)"
1.16 +definition Legendre :: "int \<Rightarrow> int \<Rightarrow> int"
1.17 +  where "Legendre a p =
1.18 +    (if ([a = 0] (mod p)) then 0
1.19 +     else if QuadRes p a then 1
1.20 +     else -1)"
1.21 +
1.22
1.23  subsection \<open>A locale for residue rings\<close>
1.24
1.25  definition residue_ring :: "int \<Rightarrow> int ring"
1.26 -where
1.27 -  "residue_ring m =
1.28 -    \<lparr>carrier = {0..m - 1},
1.29 -     monoid.mult = \<lambda>x y. (x * y) mod m,
1.30 -     one = 1,
1.31 -     zero = 0,
1.32 -     add = \<lambda>x y. (x + y) mod m\<rparr>"
1.33 +  where
1.34 +    "residue_ring m =
1.35 +      \<lparr>carrier = {0..m - 1},
1.36 +       monoid.mult = \<lambda>x y. (x * y) mod m,
1.37 +       one = 1,
1.38 +       zero = 0,
1.39 +       add = \<lambda>x y. (x + y) mod m\<rparr>"
1.40
1.41  locale residues =
1.42    fixes m :: int and R (structure)
1.43 @@ -88,37 +90,37 @@
1.44  \<close>
1.45
1.46  lemma res_carrier_eq: "carrier R = {0..m - 1}"
1.47 -  unfolding R_def residue_ring_def by auto
1.48 +  by (auto simp: R_def residue_ring_def)
1.49
1.50  lemma res_add_eq: "x \<oplus> y = (x + y) mod m"
1.51 -  unfolding R_def residue_ring_def by auto
1.52 +  by (auto simp: R_def residue_ring_def)
1.53
1.54  lemma res_mult_eq: "x \<otimes> y = (x * y) mod m"
1.55 -  unfolding R_def residue_ring_def by auto
1.56 +  by (auto simp: R_def residue_ring_def)
1.57
1.58  lemma res_zero_eq: "\<zero> = 0"
1.59 -  unfolding R_def residue_ring_def by auto
1.60 +  by (auto simp: R_def residue_ring_def)
1.61
1.62  lemma res_one_eq: "\<one> = 1"
1.63 -  unfolding R_def residue_ring_def units_of_def by auto
1.64 +  by (auto simp: R_def residue_ring_def units_of_def)
1.65
1.66  lemma res_units_eq: "Units R = {x. 0 < x \<and> x < m \<and> coprime x m}"
1.67    using m_gt_one
1.68    unfolding Units_def R_def residue_ring_def
1.69    apply auto
1.70 -  apply (subgoal_tac "x \<noteq> 0")
1.71 -  apply auto
1.72 -  apply (metis invertible_coprime_int)
1.73 +    apply (subgoal_tac "x \<noteq> 0")
1.74 +     apply auto
1.75 +   apply (metis invertible_coprime_int)
1.76    apply (subst (asm) coprime_iff_invertible'_int)
1.77 -  apply (auto simp add: cong_int_def mult.commute)
1.78 +   apply (auto simp add: cong_int_def mult.commute)
1.79    done
1.80
1.81  lemma res_neg_eq: "\<ominus> x = (- x) mod m"
1.82    using m_gt_one unfolding R_def a_inv_def m_inv_def residue_ring_def
1.83    apply simp
1.84    apply (rule the_equality)
1.90    done
1.91
1.92 @@ -139,18 +141,16 @@
1.93    using insert m_gt_one by auto
1.94
1.95  lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m"
1.96 -  unfolding R_def residue_ring_def
1.97 -  by (auto simp add: mod_simps)
1.98 +  by (auto simp: R_def residue_ring_def mod_simps)
1.99
1.100  lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m"
1.101 -  unfolding R_def residue_ring_def
1.102 -  by (auto simp add: mod_simps)
1.103 +  by (auto simp: R_def residue_ring_def mod_simps)
1.104
1.105  lemma zero_cong: "\<zero> = 0"
1.106 -  unfolding R_def residue_ring_def by auto
1.107 +  by (auto simp: R_def residue_ring_def)
1.108
1.109  lemma one_cong: "\<one> = 1 mod m"
1.110 -  using m_gt_one unfolding R_def residue_ring_def by auto
1.111 +  using m_gt_one by (auto simp: R_def residue_ring_def)
1.112
1.113  (* FIXME revise algebra library to use 1? *)
1.114  lemma pow_cong: "(x mod m) (^) n = x^n mod m"
1.115 @@ -173,24 +173,26 @@
1.116    assumes "1 < m" and "coprime a m"
1.117    shows "a mod m \<in> Units R"
1.118  proof (cases "a mod m = 0")
1.119 -  case True with assms show ?thesis
1.120 +  case True
1.121 +  with assms show ?thesis
1.122      by (auto simp add: res_units_eq gcd_red_int [symmetric])
1.123  next
1.124    case False
1.125    from assms have "0 < m" by simp
1.126 -  with pos_mod_sign [of m a] have "0 \<le> a mod m" .
1.127 +  then have "0 \<le> a mod m" by (rule pos_mod_sign [of m a])
1.128    with False have "0 < a mod m" by simp
1.129    with assms show ?thesis
1.130      by (auto simp add: res_units_eq gcd_red_int [symmetric] ac_simps)
1.131  qed
1.132
1.133  lemma res_eq_to_cong: "(a mod m) = (b mod m) \<longleftrightarrow> [a = b] (mod m)"
1.134 -  unfolding cong_int_def by auto
1.135 +  by (auto simp: cong_int_def)
1.136
1.137
1.138  text \<open>Simplifying with these will translate a ring equation in R to a congruence.\<close>
1.139 -lemmas res_to_cong_simps = add_cong mult_cong pow_cong one_cong
1.140 -    prod_cong sum_cong neg_cong res_eq_to_cong
1.141 +lemmas res_to_cong_simps =
1.142 +  add_cong mult_cong pow_cong one_cong
1.143 +  prod_cong sum_cong neg_cong res_eq_to_cong
1.144
1.145  text \<open>Other useful facts about the residue ring.\<close>
1.146  lemma one_eq_neg_one: "\<one> = \<ominus> \<one> \<Longrightarrow> m = 2"
1.147 @@ -220,11 +222,11 @@
1.148
1.149  lemma is_field: "field R"
1.150  proof -
1.151 -  have "\<And>x. \<lbrakk>gcd x (int p) \<noteq> 1; 0 \<le> x; x < int p\<rbrakk> \<Longrightarrow> x = 0"
1.152 +  have "gcd x (int p) \<noteq> 1 \<Longrightarrow> 0 \<le> x \<Longrightarrow> x < int p \<Longrightarrow> x = 0" for x
1.153      by (metis dual_order.order_iff_strict gcd.commute less_le_not_le p_prime prime_imp_coprime prime_nat_int_transfer zdvd_imp_le)
1.154    then show ?thesis
1.155 -  apply (intro cring.field_intro2 cring)
1.156 -  apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq)
1.157 +    apply (intro cring.field_intro2 cring)
1.158 +     apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq)
1.159      done
1.160  qed
1.161
1.162 @@ -245,23 +247,26 @@
1.163
1.164  subsection \<open>Euler's theorem\<close>
1.165
1.166 -lemma (in residues) totient_eq:
1.167 -  "totient (nat m) = card (Units R)"
1.168 +lemma (in residues) totient_eq: "totient (nat m) = card (Units R)"
1.169  proof -
1.170    have *: "inj_on nat (Units R)"
1.171      by (rule inj_onI) (auto simp add: res_units_eq)
1.172    define m' where "m' = nat m"
1.173 -  from m_gt_one have m: "m = int m'" "m' > 1" by (simp_all add: m'_def)
1.174 -  from m have "x \<in> Units R \<longleftrightarrow> x \<in> int ` totatives m'" for x
1.175 +  from m_gt_one have "m = int m'" "m' > 1"
1.176 +    by (simp_all add: m'_def)
1.177 +  then have "x \<in> Units R \<longleftrightarrow> x \<in> int ` totatives m'" for x
1.178      unfolding res_units_eq
1.179      by (cases x; cases "x = m") (auto simp: totatives_def transfer_int_nat_gcd)
1.180 -  hence "Units R = int ` totatives m'" by blast
1.181 -  hence "totatives m' = nat ` Units R" by (simp add: image_image)
1.182 +  then have "Units R = int ` totatives m'"
1.183 +    by blast
1.184 +  then have "totatives m' = nat ` Units R"
1.185 +    by (simp add: image_image)
1.186    then have "card (totatives (nat m)) = card (nat ` Units R)"
1.188    also have "\<dots> = card (Units R)"
1.189      using * card_image [of nat "Units R"] by auto
1.190 -  finally show ?thesis by (simp add: totient_def)
1.191 +  finally show ?thesis
1.192 +    by (simp add: totient_def)
1.193  qed
1.194
1.195  lemma (in residues_prime) totient_eq: "totient p = p - 1"
1.196 @@ -324,26 +329,26 @@
1.197    have "(\<Otimes>i\<in>Units R. i) = (\<Otimes>i\<in>{\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i\<in>\<Union>?Inverse_Pairs. i)"
1.198      apply (subst UR)
1.199      apply (subst finprod_Un_disjoint)
1.200 -    apply (auto intro: funcsetI)
1.201 +         apply (auto intro: funcsetI)
1.202      using inv_one apply auto[1]
1.203      using inv_eq_neg_one_eq apply auto
1.204      done
1.205    also have "(\<Otimes>i\<in>{\<one>, \<ominus> \<one>}. i) = \<ominus> \<one>"
1.206      apply (subst finprod_insert)
1.207 -    apply auto
1.208 +        apply auto
1.209      apply (frule one_eq_neg_one)
1.210      using a apply force
1.211      done
1.212    also have "(\<Otimes>i\<in>(\<Union>?Inverse_Pairs). i) = (\<Otimes>A\<in>?Inverse_Pairs. (\<Otimes>y\<in>A. y))"
1.213      apply (subst finprod_Union_disjoint)
1.214 -    apply auto
1.215 -    apply (metis Units_inv_inv)+
1.216 +       apply auto
1.217 +     apply (metis Units_inv_inv)+
1.218      done
1.219    also have "\<dots> = \<one>"
1.220      apply (rule finprod_one)
1.221 -    apply auto
1.222 +     apply auto
1.223      apply (subst finprod_insert)
1.224 -    apply auto
1.225 +        apply auto
1.226      apply (metis inv_eq_self)
1.227      done
1.228    finally have "(\<Otimes>i\<in>Units R. i) = \<ominus> \<one>"
1.229 @@ -361,7 +366,7 @@
1.230    finally have "fact (p - 1) mod p = \<ominus> \<one>" .
1.231    then show ?thesis
1.232      by (metis of_nat_fact Divides.transfer_int_nat_functions(2)
1.233 -      cong_int_def res_neg_eq res_one_eq)
1.234 +        cong_int_def res_neg_eq res_one_eq)
1.235  qed
1.236
1.237  lemma wilson_theorem:
1.238 @@ -380,13 +385,11 @@
1.239
1.240  text \<open>
1.241    This result can be transferred to the multiplicative group of
1.242 -  \$\mathbb{Z}/p\mathbb{Z}\$ for \$p\$ prime.\<close>
1.243 +  \<open>\<int>/p\<int>\<close> for \<open>p\<close> prime.\<close>
1.244
1.245  lemma mod_nat_int_pow_eq:
1.246    fixes n :: nat and p a :: int
1.247 -  assumes "a \<ge> 0" "p \<ge> 0"
1.248 -  shows "(nat a ^ n) mod (nat p) = nat ((a ^ n) mod p)"
1.249 -  using assms
1.250 +  shows "a \<ge> 0 \<Longrightarrow> p \<ge> 0 \<Longrightarrow> (nat a ^ n) mod (nat p) = nat ((a ^ n) mod p)"
1.251    by (simp add: int_one_le_iff_zero_less nat_mod_distrib order_less_imp_le nat_power_eq[symmetric])
1.252
1.253  theorem residue_prime_mult_group_has_gen :
1.254 @@ -394,43 +397,55 @@
1.255   assumes prime_p : "prime p"
1.256   shows "\<exists>a \<in> {1 .. p - 1}. {1 .. p - 1} = {a^i mod p|i . i \<in> UNIV}"
1.257  proof -
1.258 -  have "p\<ge>2" using prime_gt_1_nat[OF prime_p] by simp
1.259 -  interpret R:residues_prime "p" "residue_ring p" unfolding residues_prime_def
1.260 -    by (simp add: prime_p)
1.261 -  have car: "carrier (residue_ring (int p)) - {\<zero>\<^bsub>residue_ring (int p)\<^esub>} =  {1 .. int p - 1}"
1.262 +  have "p \<ge> 2"
1.263 +    using prime_gt_1_nat[OF prime_p] by simp
1.264 +  interpret R: residues_prime p "residue_ring p"
1.265 +    by (simp add: residues_prime_def prime_p)
1.266 +  have car: "carrier (residue_ring (int p)) - {\<zero>\<^bsub>residue_ring (int p)\<^esub>} = {1 .. int p - 1}"
1.267      by (auto simp add: R.zero_cong R.res_carrier_eq)
1.268 -  obtain a where a:"a \<in> {1 .. int p - 1}"
1.269 -         and a_gen:"{1 .. int p - 1} = {a(^)\<^bsub>residue_ring (int p)\<^esub>i|i::nat . i \<in> UNIV}"
1.270 -    apply atomize_elim using field.finite_field_mult_group_has_gen[OF R.is_field]
1.271 +
1.272 +  have "x (^)\<^bsub>residue_ring (int p)\<^esub> i = x ^ i mod (int p)"
1.273 +    if "x \<in> {1 .. int p - 1}" for x and i :: nat
1.274 +    using that R.pow_cong[of x i] by auto
1.275 +  moreover
1.276 +  obtain a where a: "a \<in> {1 .. int p - 1}"
1.277 +    and a_gen: "{1 .. int p - 1} = {a(^)\<^bsub>residue_ring (int p)\<^esub>i|i::nat . i \<in> UNIV}"
1.278 +    using field.finite_field_mult_group_has_gen[OF R.is_field]
1.279      by (auto simp add: car[symmetric] carrier_mult_of)
1.280 -  { fix x fix i :: nat assume x: "x \<in> {1 .. int p - 1}"
1.281 -    hence "x (^)\<^bsub>residue_ring (int p)\<^esub> i = x ^ i mod (int p)" using R.pow_cong[of x i] by auto}
1.282 -  note * = this
1.283 -  have **:"nat ` {1 .. int p - 1} = {1 .. p - 1}" (is "?L = ?R")
1.284 +  moreover
1.285 +  have "nat ` {1 .. int p - 1} = {1 .. p - 1}" (is "?L = ?R")
1.286    proof
1.287 -    { fix n assume n: "n \<in> ?L"
1.288 -      then have "n \<in> ?R" using \<open>p\<ge>2\<close> by force
1.289 -    } thus "?L \<subseteq> ?R" by blast
1.290 -    { fix n assume n: "n \<in> ?R"
1.291 -      then have "n \<in> ?L" using \<open>p\<ge>2\<close> Set_Interval.transfer_nat_int_set_functions(2) by fastforce
1.292 -    } thus "?R \<subseteq> ?L" by blast
1.293 +    have "n \<in> ?R" if "n \<in> ?L" for n
1.294 +      using that \<open>p\<ge>2\<close> by force
1.295 +    then show "?L \<subseteq> ?R" by blast
1.296 +    have "n \<in> ?L" if "n \<in> ?R" for n
1.297 +      using that \<open>p\<ge>2\<close> Set_Interval.transfer_nat_int_set_functions(2) by fastforce
1.298 +    then show "?R \<subseteq> ?L" by blast
1.299    qed
1.300 +  moreover
1.301    have "nat ` {a^i mod (int p) | i::nat. i \<in> UNIV} = {nat a^i mod p | i . i \<in> UNIV}" (is "?L = ?R")
1.302    proof
1.303 -    { fix x assume x: "x \<in> ?L"
1.304 -      then obtain i where i:"x = nat (a^i mod (int p))" by blast
1.305 -      hence "x = nat a ^ i mod p" using mod_nat_int_pow_eq[of a "int p" i] a \<open>p\<ge>2\<close> by auto
1.306 -      hence "x \<in> ?R" using i by blast
1.307 -    } thus "?L \<subseteq> ?R" by blast
1.308 -    { fix x assume x: "x \<in> ?R"
1.309 -      then obtain i where i:"x = nat a^i mod p" by blast
1.310 -      hence "x \<in> ?L" using mod_nat_int_pow_eq[of a "int p" i] a \<open>p\<ge>2\<close> by auto
1.311 -    } thus "?R \<subseteq> ?L" by blast
1.312 +    have "x \<in> ?R" if "x \<in> ?L" for x
1.313 +    proof -
1.314 +      from that obtain i where i: "x = nat (a^i mod (int p))"
1.315 +        by blast
1.316 +      then have "x = nat a ^ i mod p"
1.317 +        using mod_nat_int_pow_eq[of a "int p" i] a \<open>p\<ge>2\<close> by auto
1.318 +      with i show ?thesis by blast
1.319 +    qed
1.320 +    then show "?L \<subseteq> ?R" by blast
1.321 +    have "x \<in> ?L" if "x \<in> ?R" for x
1.322 +    proof -
1.323 +      from that obtain i where i: "x = nat a^i mod p"
1.324 +        by blast
1.325 +      with mod_nat_int_pow_eq[of a "int p" i] a \<open>p\<ge>2\<close> show ?thesis
1.326 +        by auto
1.327 +    qed
1.328 +    then show "?R \<subseteq> ?L" by blast
1.329    qed
1.330 -  hence "{1 .. p - 1} = {nat a^i mod p | i. i \<in> UNIV}"
1.331 -    using * a a_gen ** by presburger
1.332 -  moreover
1.333 -  have "nat a \<in> {1 .. p - 1}" using a by force
1.334 +  ultimately have "{1 .. p - 1} = {nat a^i mod p | i. i \<in> UNIV}"
1.335 +    by presburger
1.336 +  moreover from a have "nat a \<in> {1 .. p - 1}" by force
1.337    ultimately show ?thesis ..
1.338  qed
1.339
```