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.85 -  apply (simp add: mod_add_right_eq)
    1.86 -  apply (simp add: add.commute mod_add_right_eq)
    1.87 +   apply (simp add: mod_add_right_eq)
    1.88 +   apply (simp add: add.commute mod_add_right_eq)
    1.89    apply (metis add.right_neutral minus_add_cancel mod_add_right_eq mod_pos_pos_trivial)
    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.187      by (simp add: m'_def)
   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