author paulson Tue Feb 28 15:17:57 2017 +0000 (2017-02-28) changeset 65066 c64d778a593a parent 65065 3d7ec12f7af7 child 65068 a2522ea43216
tidied some messy proofs
```     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Tue Feb 28 13:55:34 2017 +0000
1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Tue Feb 28 15:17:57 2017 +0000
1.3 @@ -37,37 +37,34 @@
1.4  begin
1.5
1.6  lemma abelian_group: "abelian_group R"
1.7 -  apply (insert m_gt_one)
1.8 -  apply (rule abelian_groupI)
1.9 -  apply (unfold R_def residue_ring_def)
1.11 -  apply (case_tac "x = 0")
1.12 -  apply force
1.13 -  apply (subgoal_tac "(x + (m - x)) mod m = 0")
1.14 -  apply (erule bexI)
1.15 -  apply auto
1.16 -  done
1.17 +proof -
1.18 +  have "\<exists>y\<in>{0..m - 1}. (x + y) mod m = 0" if "0 \<le> x" "x < m" for x
1.19 +  proof (cases "x = 0")
1.20 +    case True
1.21 +    with m_gt_one show ?thesis by simp
1.22 +  next
1.23 +    case False
1.24 +    then have "(x + (m - x)) mod m = 0"
1.25 +      by simp
1.26 +    with m_gt_one that show ?thesis
1.27 +      by (metis False atLeastAtMost_iff diff_ge_0_iff_ge diff_left_mono int_one_le_iff_zero_less less_le)
1.28 +  qed
1.29 +  with m_gt_one show ?thesis
1.30 +    by (fastforce simp add: R_def residue_ring_def mod_add_right_eq ac_simps  intro!: abelian_groupI)
1.31 +qed
1.32
1.33  lemma comm_monoid: "comm_monoid R"
1.34 -  apply (insert m_gt_one)
1.35 -  apply (unfold R_def residue_ring_def)
1.36 +  unfolding R_def residue_ring_def
1.37    apply (rule comm_monoidI)
1.38 -  apply auto
1.39 -  apply (subgoal_tac "x * y mod m * z mod m = z * (x * y mod m) mod m")
1.40 -  apply (erule ssubst)
1.41 -  apply (subst mod_mult_right_eq)+
1.42 -  apply (simp_all only: ac_simps)
1.43 +    using m_gt_one  apply auto
1.44 +  apply (metis mod_mult_right_eq mult.assoc mult.commute)
1.45 +  apply (metis mult.commute)
1.46    done
1.47
1.48  lemma cring: "cring R"
1.49 -  apply (rule cringI)
1.50 -  apply (rule abelian_group)
1.51 -  apply (rule comm_monoid)
1.52 -  apply (unfold R_def residue_ring_def, auto)
1.54 -  apply (subst mult.commute)
1.55 -  apply (subst mod_mult_right_eq)
1.56 -  apply (simp add: field_simps)
1.57 +  apply (intro cringI abelian_group comm_monoid)
1.58 +  unfolding R_def residue_ring_def
1.60    done
1.61
1.62  end
1.63 @@ -100,8 +97,8 @@
1.64    unfolding R_def residue_ring_def units_of_def by auto
1.65
1.66  lemma res_units_eq: "Units R = {x. 0 < x \<and> x < m \<and> coprime x m}"
1.67 -  apply (insert m_gt_one)
1.68 -  apply (unfold Units_def R_def residue_ring_def)
1.69 +  using m_gt_one
1.70 +  unfolding Units_def R_def residue_ring_def
1.71    apply auto
1.72    apply (subgoal_tac "x \<noteq> 0")
1.73    apply auto
1.74 @@ -111,18 +108,12 @@
1.75    done
1.76
1.77  lemma res_neg_eq: "\<ominus> x = (- x) mod m"
1.78 -  apply (insert m_gt_one)
1.79 -  apply (unfold R_def a_inv_def m_inv_def residue_ring_def)
1.80 -  apply auto
1.81 +  using m_gt_one unfolding R_def a_inv_def m_inv_def residue_ring_def
1.82 +  apply simp
1.83    apply (rule the_equality)
1.84 -  apply auto
1.86 -  apply auto
1.88 -  apply auto
1.89 -  apply (subgoal_tac "y mod m = - x mod m")
1.90 -  apply simp
1.91 -  apply (metis minus_add_cancel mod_mult_self1 mult.commute)
1.95    done
1.96
1.97  lemma finite [iff]: "finite (carrier R)"
1.98 @@ -157,7 +148,7 @@
1.99
1.100  (* FIXME revise algebra library to use 1? *)
1.101  lemma pow_cong: "(x mod m) (^) n = x^n mod m"
1.102 -  apply (insert m_gt_one)
1.103 +  using m_gt_one
1.104    apply (induct n)
1.105    apply (auto simp add: nat_pow_def one_cong)
1.106    apply (metis mult.commute mult_cong)
1.107 @@ -213,7 +204,7 @@
1.108    defines "R \<equiv> residue_ring (int p)"
1.109
1.110  sublocale residues_prime < residues p
1.111 -  apply (unfold R_def residues_def)
1.112 +  unfolding R_def residues_def
1.113    using p_prime apply auto
1.114    apply (metis (full_types) of_nat_1 of_nat_less_iff prime_gt_1_nat)
1.115    done
1.116 @@ -222,18 +213,14 @@
1.117  begin
1.118
1.119  lemma is_field: "field R"
1.120 -  apply (rule cring.field_intro2)
1.121 -  apply (rule cring)
1.122 +proof -
1.123 +  have "\<And>x. \<lbrakk>gcd x (int p) \<noteq> 1; 0 \<le> x; x < int p\<rbrakk> \<Longrightarrow> x = 0"
1.124 +    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.125 +  then show ?thesis
1.126 +  apply (intro cring.field_intro2 cring)
1.127    apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq)
1.128 -  apply (rule classical)
1.129 -  apply (erule notE)
1.130 -  apply (subst gcd.commute)
1.131 -  apply (rule prime_imp_coprime_int)
1.132 -  apply (simp add: p_prime)
1.133 -  apply (rule notI)
1.134 -  apply (frule zdvd_imp_le)
1.135 -  apply auto
1.136 -  done
1.137 +    done
1.138 +qed
1.139
1.140  lemma res_prime_units_eq: "Units R = {1..p - 1}"
1.141    apply (subst res_units_eq)
1.142 @@ -252,20 +239,22 @@
1.143
1.144  subsection \<open>Euler's theorem\<close>
1.145
1.146 -text \<open>The definition of the phi function.\<close>
1.147 +text \<open>The definition of the totient function.\<close>
1.148
1.149  definition phi :: "int \<Rightarrow> nat"
1.150 -  where "phi m = card {x. 0 < x \<and> x < m \<and> gcd x m = 1}"
1.151 +  where "phi m = card {x. 0 < x \<and> x < m \<and> coprime x m}"
1.152
1.153 -lemma phi_def_nat: "phi m = card {x. 0 < x \<and> x < nat m \<and> gcd x (nat m) = 1}"
1.154 -  apply (simp add: phi_def)
1.155 -  apply (rule bij_betw_same_card [of nat])
1.156 -  apply (auto simp add: inj_on_def bij_betw_def image_def)
1.157 -  apply (metis dual_order.irrefl dual_order.strict_trans leI nat_1 transfer_nat_int_gcd(1))
1.158 -  apply (metis One_nat_def of_nat_0 of_nat_1 of_nat_less_0_iff int_nat_eq nat_int
1.159 -    transfer_int_nat_gcd(1) of_nat_less_iff)
1.160 -  done
1.161 -
1.162 +lemma phi_def_nat: "phi m = card {x. 0 < x \<and> x < nat m \<and> coprime x (nat m)}"
1.163 +  unfolding phi_def
1.164 +proof (rule bij_betw_same_card [of nat])
1.165 +  show "bij_betw nat {x. 0 < x \<and> x < m \<and> coprime x m} {x. 0 < x \<and> x < nat m \<and> coprime x (nat m)}"
1.166 +    apply (auto simp add: inj_on_def bij_betw_def image_def)
1.167 +     apply (metis dual_order.irrefl dual_order.strict_trans leI nat_1 transfer_nat_int_gcd(1))
1.168 +    apply (metis One_nat_def of_nat_0 of_nat_1 of_nat_less_0_iff int_nat_eq nat_int
1.169 +        transfer_int_nat_gcd(1) of_nat_less_iff)
1.170 +    done
1.171 +qed
1.172 +
1.173  lemma prime_phi:
1.174    assumes "2 \<le> p" "phi p = p - 1"
1.175    shows "prime p"
1.176 @@ -292,12 +281,7 @@
1.177  qed
1.178
1.179  lemma phi_zero [simp]: "phi 0 = 0"
1.180 -  unfolding phi_def
1.181 -(* Auto hangs here. Once again, where is the simplification rule
1.182 -   1 \<equiv> Suc 0 coming from? *)
1.183 -  apply (auto simp add: card_eq_0_iff)
1.184 -(* Add card_eq_0_iff as a simp rule? delete card_empty_imp? *)
1.185 -  done
1.186 +  unfolding phi_def by (auto simp add: card_eq_0_iff)
1.187
1.188  lemma phi_one [simp]: "phi 1 = 0"
1.189    by (auto simp add: phi_def card_eq_0_iff)
1.190 @@ -309,30 +293,12 @@
1.191    assumes a: "gcd a m = 1"
1.192    shows "[a^phi m = 1] (mod m)"
1.193  proof -
1.194 -  from a m_gt_one have [simp]: "a mod m \<in> Units R"
1.195 -    by (intro mod_in_res_units)
1.196 -  from phi_eq have "(a mod m) (^) (phi m) = (a mod m) (^) (card (Units R))"
1.197 -    by simp
1.198 -  also have "\<dots> = \<one>"
1.199 -    by (intro units_power_order_eq_one) auto
1.200 -  finally show ?thesis
1.201 -    by (simp add: res_to_cong_simps)
1.202 +  have "a ^ phi m mod m = 1 mod m"
1.203 +    by (metis assms finite_Units m_gt_one mod_in_res_units one_cong phi_eq pow_cong units_power_order_eq_one)
1.204 +  then show ?thesis
1.205 +    using res_eq_to_cong by blast
1.206  qed
1.207
1.208 -(* In fact, there is a two line proof!
1.209 -
1.210 -lemma (in residues) euler_theorem1:
1.211 -  assumes a: "gcd a m = 1"
1.212 -  shows "[a^phi m = 1] (mod m)"
1.213 -proof -
1.214 -  have "(a mod m) (^) (phi m) = \<one>"
1.215 -    by (simp add: phi_eq units_power_order_eq_one a m_gt_one)
1.216 -  then show ?thesis
1.217 -    by (simp add: res_to_cong_simps)
1.218 -qed
1.219 -
1.220 -*)
1.221 -
1.222  text \<open>Outside the locale, we can relax the restriction \<open>m > 1\<close>.\<close>
1.223  lemma euler_theorem:
1.224    assumes "m \<ge> 0"
1.225 @@ -348,16 +314,10 @@
1.226  qed
1.227
1.228  lemma (in residues_prime) phi_prime: "phi p = nat p - 1"
1.229 -  apply (subst phi_eq)
1.230 -  apply (subst res_prime_units_eq)
1.231 -  apply auto
1.232 -  done
1.233 +  by (simp add: residues.phi_eq residues_axioms residues_prime.res_prime_units_eq residues_prime_axioms)
1.234
1.235  lemma phi_prime: "prime (int p) \<Longrightarrow> phi p = nat p - 1"
1.236 -  apply (rule residues_prime.phi_prime)
1.237 -  apply simp
1.238 -  apply (erule residues_prime.intro)
1.239 -  done
1.240 +  by (simp add: residues_prime.intro residues_prime.phi_prime)
1.241
1.242  lemma fermat_theorem:
1.243    fixes a :: int
1.244 @@ -424,18 +384,12 @@
1.245    finally have "(\<Otimes>i\<in>Units R. i) = \<ominus> \<one>"
1.246      by simp
1.247    also have "(\<Otimes>i\<in>Units R. i) = (\<Otimes>i\<in>Units R. i mod p)"
1.248 -    apply (rule finprod_cong')
1.249 -    apply auto
1.250 -    apply (subst (asm) res_prime_units_eq)
1.251 -    apply auto
1.252 -    done
1.253 +    by (rule finprod_cong') (auto simp: res_units_eq)
1.254    also have "\<dots> = (\<Prod>i\<in>Units R. i) mod p"
1.255 -    apply (rule prod_cong)
1.256 -    apply auto
1.257 -    done
1.258 +    by (rule prod_cong) auto
1.259    also have "\<dots> = fact (p - 1) mod p"