# HG changeset patch
# User wenzelm
# Date 1434750690 -7200
# Node ID 190b4a7d8b87e76d0d0c24578c3a6878a090bc3b
# Parent  eb431a5651fe8f2427b5fa5e0548ef3c2a6bcac8
tuned;

diff -r eb431a5651fe -r 190b4a7d8b87 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Fri Jun 19 23:40:46 2015 +0200
+++ b/src/HOL/Number_Theory/Residues.thy	Fri Jun 19 23:51:30 2015 +0200
@@ -14,7 +14,7 @@
 subsection \<open>A locale for residue rings\<close>
 
 definition residue_ring :: "int \<Rightarrow> int ring"
-  where
+where
   "residue_ring m =
     \<lparr>carrier = {0..m - 1},
      mult = \<lambda>x y. (x * y) mod m,
@@ -160,10 +160,10 @@
 lemma neg_cong: "\<ominus> (x mod m) = (- x) mod m"
   by (metis mod_minus_eq res_neg_eq)
 
-lemma (in residues) prod_cong: "finite A \<Longrightarrow> (\<Otimes> i:A. (f i) mod m) = (\<Prod>i\<in>A. f i) mod m"
+lemma (in residues) prod_cong: "finite A \<Longrightarrow> (\<Otimes>i\<in>A. (f i) mod m) = (\<Prod>i\<in>A. f i) mod m"
   by (induct set: finite) (auto simp: one_cong mult_cong)
 
-lemma (in residues) sum_cong: "finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (\<Sum>i\<in>A. f i) mod m"
+lemma (in residues) sum_cong: "finite A \<Longrightarrow> (\<Oplus>i\<in>A. (f i) mod m) = (\<Sum>i\<in>A. f i) mod m"
   by (induct set: finite) (auto simp: zero_cong add_cong)
 
 lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow> a mod m \<in> Units R"
@@ -176,21 +176,19 @@
   apply (metis gcd_int.commute gcd_red_int)
   done
 
-lemma res_eq_to_cong: "((a mod m) = (b mod m)) = [a = b] (mod (m::int))"
+lemma res_eq_to_cong: "(a mod m) = (b mod m) \<longleftrightarrow> [a = b] (mod m)"
   unfolding cong_int_def by auto
 
 
-text \<open>Simplifying with these will translate a ring equation in R to a
-   congruence.\<close>
+text \<open>Simplifying with these will translate a ring equation in R to a congruence.\<close>
 lemmas res_to_cong_simps = add_cong mult_cong pow_cong one_cong
     prod_cong sum_cong neg_cong res_eq_to_cong
 
 text \<open>Other useful facts about the residue ring.\<close>
-
 lemma one_eq_neg_one: "\<one> = \<ominus> \<one> \<Longrightarrow> m = 2"
   apply (simp add: res_one_eq res_neg_eq)
   apply (metis add.commute add_diff_cancel mod_mod_trivial one_add_one uminus_add_conv_diff
-            zero_neq_one zmod_zminus1_eq_if)
+    zero_neq_one zmod_zminus1_eq_if)
   done
 
 end
@@ -261,16 +259,16 @@
   assumes "2 \<le> p" "phi p = p - 1"
   shows "prime p"
 proof -
-  have "{x. 0 < x \<and> x < p \<and> coprime x p} = {1..p - 1}"
+  have *: "{x. 0 < x \<and> x < p \<and> coprime x p} = {1..p - 1}"
     using assms unfolding phi_def_nat
     by (intro card_seteq) fastforce+
-  then have cop: "\<And>x::nat. x \<in> {1..p - 1} \<Longrightarrow> coprime x p"
-    by blast
-  have False if *: "1 < x" "x < p" and "x dvd p" for x :: nat
+  have False if **: "1 < x" "x < p" and "x dvd p" for x :: nat
   proof -
+    from * have cop: "x \<in> {1..p - 1} \<Longrightarrow> coprime x p"
+      by blast
     have "coprime x p"
       apply (rule cop)
-      using * apply auto
+      using ** apply auto
       done
     with \<open>x dvd p\<close> \<open>1 < x\<close> show ?thesis
       by auto
@@ -324,8 +322,7 @@
 
 *)
 
-(* outside the locale, we can relax the restriction m > 1 *)
-
+text \<open>Outside the locale, we can relax the restriction @{text "m > 1"}.\<close>
 lemma euler_theorem:
   assumes "m \<ge> 0"
     and "gcd a m = 1"
@@ -434,7 +431,8 @@
     done
   finally have "fact (p - 1) mod p = \<ominus> \<one>" .
   then show ?thesis
-    by (metis of_nat_fact Divides.transfer_int_nat_functions(2) cong_int_def res_neg_eq res_one_eq)
+    by (metis of_nat_fact Divides.transfer_int_nat_functions(2)
+      cong_int_def res_neg_eq res_one_eq)
 qed
 
 lemma wilson_theorem: