author wenzelm Fri Jun 19 23:51:30 2015 +0200 (2015-06-19) changeset 60528 190b4a7d8b87 parent 60527 eb431a5651fe child 60529 24c2ef12318b
tuned;
```     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.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:
```