tuned;
authorwenzelm
Fri Jun 19 23:51:30 2015 +0200 (2015-06-19)
changeset 60528190b4a7d8b87
parent 60527 eb431a5651fe
child 60529 24c2ef12318b
tuned;
src/HOL/Number_Theory/Residues.thy
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Fri Jun 19 23:40:46 2015 +0200
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Fri Jun 19 23:51:30 2015 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  subsection \<open>A locale for residue rings\<close>
     1.5  
     1.6  definition residue_ring :: "int \<Rightarrow> int ring"
     1.7 -  where
     1.8 +where
     1.9    "residue_ring m =
    1.10      \<lparr>carrier = {0..m - 1},
    1.11       mult = \<lambda>x y. (x * y) mod m,
    1.12 @@ -160,10 +160,10 @@
    1.13  lemma neg_cong: "\<ominus> (x mod m) = (- x) mod m"
    1.14    by (metis mod_minus_eq res_neg_eq)
    1.15  
    1.16 -lemma (in residues) prod_cong: "finite A \<Longrightarrow> (\<Otimes> i:A. (f i) mod m) = (\<Prod>i\<in>A. f i) mod m"
    1.17 +lemma (in residues) prod_cong: "finite A \<Longrightarrow> (\<Otimes>i\<in>A. (f i) mod m) = (\<Prod>i\<in>A. f i) mod m"
    1.18    by (induct set: finite) (auto simp: one_cong mult_cong)
    1.19  
    1.20 -lemma (in residues) sum_cong: "finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (\<Sum>i\<in>A. f i) mod m"
    1.21 +lemma (in residues) sum_cong: "finite A \<Longrightarrow> (\<Oplus>i\<in>A. (f i) mod m) = (\<Sum>i\<in>A. f i) mod m"
    1.22    by (induct set: finite) (auto simp: zero_cong add_cong)
    1.23  
    1.24  lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow> a mod m \<in> Units R"
    1.25 @@ -176,21 +176,19 @@
    1.26    apply (metis gcd_int.commute gcd_red_int)
    1.27    done
    1.28  
    1.29 -lemma res_eq_to_cong: "((a mod m) = (b mod m)) = [a = b] (mod (m::int))"
    1.30 +lemma res_eq_to_cong: "(a mod m) = (b mod m) \<longleftrightarrow> [a = b] (mod m)"
    1.31    unfolding cong_int_def by auto
    1.32  
    1.33  
    1.34 -text \<open>Simplifying with these will translate a ring equation in R to a
    1.35 -   congruence.\<close>
    1.36 +text \<open>Simplifying with these will translate a ring equation in R to a congruence.\<close>
    1.37  lemmas res_to_cong_simps = add_cong mult_cong pow_cong one_cong
    1.38      prod_cong sum_cong neg_cong res_eq_to_cong
    1.39  
    1.40  text \<open>Other useful facts about the residue ring.\<close>
    1.41 -
    1.42  lemma one_eq_neg_one: "\<one> = \<ominus> \<one> \<Longrightarrow> m = 2"
    1.43    apply (simp add: res_one_eq res_neg_eq)
    1.44    apply (metis add.commute add_diff_cancel mod_mod_trivial one_add_one uminus_add_conv_diff
    1.45 -            zero_neq_one zmod_zminus1_eq_if)
    1.46 +    zero_neq_one zmod_zminus1_eq_if)
    1.47    done
    1.48  
    1.49  end
    1.50 @@ -261,16 +259,16 @@
    1.51    assumes "2 \<le> p" "phi p = p - 1"
    1.52    shows "prime p"
    1.53  proof -
    1.54 -  have "{x. 0 < x \<and> x < p \<and> coprime x p} = {1..p - 1}"
    1.55 +  have *: "{x. 0 < x \<and> x < p \<and> coprime x p} = {1..p - 1}"
    1.56      using assms unfolding phi_def_nat
    1.57      by (intro card_seteq) fastforce+
    1.58 -  then have cop: "\<And>x::nat. x \<in> {1..p - 1} \<Longrightarrow> coprime x p"
    1.59 -    by blast
    1.60 -  have False if *: "1 < x" "x < p" and "x dvd p" for x :: nat
    1.61 +  have False if **: "1 < x" "x < p" and "x dvd p" for x :: nat
    1.62    proof -
    1.63 +    from * have cop: "x \<in> {1..p - 1} \<Longrightarrow> coprime x p"
    1.64 +      by blast
    1.65      have "coprime x p"
    1.66        apply (rule cop)
    1.67 -      using * apply auto
    1.68 +      using ** apply auto
    1.69        done
    1.70      with \<open>x dvd p\<close> \<open>1 < x\<close> show ?thesis
    1.71        by auto
    1.72 @@ -324,8 +322,7 @@
    1.73  
    1.74  *)
    1.75  
    1.76 -(* outside the locale, we can relax the restriction m > 1 *)
    1.77 -
    1.78 +text \<open>Outside the locale, we can relax the restriction @{text "m > 1"}.\<close>
    1.79  lemma euler_theorem:
    1.80    assumes "m \<ge> 0"
    1.81      and "gcd a m = 1"
    1.82 @@ -434,7 +431,8 @@
    1.83      done
    1.84    finally have "fact (p - 1) mod p = \<ominus> \<one>" .
    1.85    then show ?thesis
    1.86 -    by (metis of_nat_fact Divides.transfer_int_nat_functions(2) cong_int_def res_neg_eq res_one_eq)
    1.87 +    by (metis of_nat_fact Divides.transfer_int_nat_functions(2)
    1.88 +      cong_int_def res_neg_eq res_one_eq)
    1.89  qed
    1.90  
    1.91  lemma wilson_theorem: