tidied some messy proofs
authorpaulson <lp15@cam.ac.uk>
Tue Feb 28 15:17:57 2017 +0000 (2017-02-28)
changeset 65066c64d778a593a
parent 65065 3d7ec12f7af7
child 65068 a2522ea43216
tidied some messy proofs
src/HOL/Number_Theory/Residues.thy
     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.10 -  apply (auto simp add: mod_add_right_eq ac_simps)
    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.53 -  apply (subst mod_add_eq)
    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.59 +  apply (auto simp add: comm_semiring_class.distrib mod_add_eq mod_mult_left_eq)
    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.85 -  apply (subst mod_add_right_eq)
    1.86 -  apply auto
    1.87 -  apply (subst mod_add_left_eq)
    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.92 +  apply (simp add: mod_add_right_eq)
    1.93 +  apply (simp add: add.commute mod_add_right_eq)
    1.94 +  apply (metis add.right_neutral minus_add_cancel mod_add_right_eq mod_pos_pos_trivial)
    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"
   1.260      apply (simp add: fact_prod)
   1.261 -    apply (insert assms)
   1.262 +    using assms
   1.263      apply (subst res_prime_units_eq)
   1.264      apply (simp add: int_prod zmod_int prod_int_eq)
   1.265      done