# HG changeset patch
# User wenzelm
# Date 1434750046 -7200
# Node ID eb431a5651fe8f2427b5fa5e0548ef3c2a6bcac8
# Parent  fad653acf58f8ca3e037317ee49ee6d07e8f5613
tuned proofs;

diff -r fad653acf58f -r eb431a5651fe src/HOL/Number_Theory/Eratosthenes.thy
--- a/src/HOL/Number_Theory/Eratosthenes.thy	Fri Jun 19 21:41:33 2015 +0200
+++ b/src/HOL/Number_Theory/Eratosthenes.thy	Fri Jun 19 23:40:46 2015 +0200
@@ -20,6 +20,7 @@
 
 end
 
+
 subsection \<open>Main corpus\<close>
 
 text \<open>The sieve is modelled as a list of booleans, where @{const False} means \emph{marked out}.\<close>
@@ -59,21 +60,19 @@
 
 
 text \<open>Marking out multiples in a sieve\<close>
- 
+
 definition mark_out :: "nat \<Rightarrow> marks \<Rightarrow> marks"
 where
   "mark_out n bs = map (\<lambda>(q, b). b \<and> \<not> Suc n dvd Suc (Suc q)) (enumerate n bs)"
 
-lemma mark_out_Nil [simp]:
-  "mark_out n [] = []"
+lemma mark_out_Nil [simp]: "mark_out n [] = []"
   by (simp add: mark_out_def)
-  
-lemma length_mark_out [simp]:
-  "length (mark_out n bs) = length bs"
+
+lemma length_mark_out [simp]: "length (mark_out n bs) = length bs"
   by (simp add: mark_out_def)
 
 lemma numbers_of_marks_mark_out:
-  "numbers_of_marks n (mark_out m bs) = {q \<in> numbers_of_marks n bs. \<not> Suc m dvd Suc q - n}"
+    "numbers_of_marks n (mark_out m bs) = {q \<in> numbers_of_marks n bs. \<not> Suc m dvd Suc q - n}"
   by (auto simp add: numbers_of_marks_def mark_out_def in_set_enumerate_eq image_iff
     nth_enumerate_eq less_eq_dvd_minus)
 
@@ -85,36 +84,36 @@
   "mark_out_aux n m bs =
     map (\<lambda>(q, b). b \<and> (q < m + n \<or> \<not> Suc n dvd Suc (Suc q) + (n - m mod Suc n))) (enumerate n bs)"
 
-lemma mark_out_code [code]:
-  "mark_out n bs = mark_out_aux n n bs"
+lemma mark_out_code [code]: "mark_out n bs = mark_out_aux n n bs"
 proof -
-  { fix a
-    assume A: "Suc n dvd Suc (Suc a)"
-      and B: "a < n + n"
-      and C: "n \<le> a"
-    have False
-    proof (cases "n = 0")
-      case True with A B C show False by simp
-    next
-      def m \<equiv> "Suc n" then have "m > 0" by simp
-      case False then have "n > 0" by simp
-      from A obtain q where q: "Suc (Suc a) = Suc n * q" by (rule dvdE)
-      have "q > 0"
-      proof (rule ccontr)
-        assume "\<not> q > 0"
-        with q show False by simp
-      qed
-      with \<open>n > 0\<close> have "Suc n * q \<ge> 2" by (auto simp add: gr0_conv_Suc)
-      with q have a: "a = Suc n * q - 2" by simp
-      with B have "q + n * q < n + n + 2"
-        by auto
-      then have "m * q < m * 2" by (simp add: m_def)
-      with \<open>m > 0\<close> have "q < 2" by simp
-      with \<open>q > 0\<close> have "q = 1" by simp
-      with a have "a = n - 1" by simp
-      with \<open>n > 0\<close> C show False by simp
+  have aux: False
+    if A: "Suc n dvd Suc (Suc a)"
+    and B: "a < n + n"
+    and C: "n \<le> a"
+    for a
+  proof (cases "n = 0")
+    case True
+    with A B C show ?thesis by simp
+  next
+    case False
+    def m \<equiv> "Suc n"
+    then have "m > 0" by simp
+    from False have "n > 0" by simp
+    from A obtain q where q: "Suc (Suc a) = Suc n * q" by (rule dvdE)
+    have "q > 0"
+    proof (rule ccontr)
+      assume "\<not> q > 0"
+      with q show False by simp
     qed
-  } note aux = this 
+    with \<open>n > 0\<close> have "Suc n * q \<ge> 2" by (auto simp add: gr0_conv_Suc)
+    with q have a: "a = Suc n * q - 2" by simp
+    with B have "q + n * q < n + n + 2" by auto
+    then have "m * q < m * 2" by (simp add: m_def)
+    with \<open>m > 0\<close> have "q < 2" by simp
+    with \<open>q > 0\<close> have "q = 1" by simp
+    with a have "a = n - 1" by simp
+    with \<open>n > 0\<close> C show False by simp
+  qed
   show ?thesis
     by (auto simp add: mark_out_def mark_out_aux_def in_set_enumerate_eq intro: aux)
 qed
@@ -185,51 +184,55 @@
   "numbers_of_marks (Suc n) (sieve n bs) =
     {q \<in> numbers_of_marks (Suc n) bs. \<forall>m \<in> numbers_of_marks (Suc n) bs. \<not> m dvd_strict q}"
 proof (induct n bs rule: sieve.induct)
-  case 1 show ?case by simp
+  case 1
+  show ?case by simp
 next
-  case 2 then show ?case by simp
+  case 2
+  then show ?case by simp
 next
   case (3 n bs)
-  have aux: "\<And>M n. n \<in> Suc ` M \<longleftrightarrow> n > 0 \<and> n - 1 \<in> M"
+  have aux: "n \<in> Suc ` M \<longleftrightarrow> n > 0 \<and> n - 1 \<in> M" (is "?lhs \<longleftrightarrow> ?rhs") for M n
   proof
-    fix M and n
-    assume "n \<in> Suc ` M" then show "n > 0 \<and> n - 1 \<in> M" by auto
-  next
-    fix M and n :: nat
-    assume "n > 0 \<and> n - 1 \<in> M"
-    then have "n > 0" and "n - 1 \<in> M" by auto
-    then have "Suc (n - 1) \<in> Suc ` M" by blast
-    with \<open>n > 0\<close> show "n \<in> Suc ` M" by simp
+    show ?rhs if ?lhs using that by auto
+    show ?lhs if ?rhs
+    proof -
+      from that have "n > 0" and "n - 1 \<in> M" by auto
+      then have "Suc (n - 1) \<in> Suc ` M" by blast
+      with \<open>n > 0\<close> show "n \<in> Suc ` M" by simp
+    qed
   qed
-  { fix m :: nat
-    assume "Suc (Suc n) \<le> m" and "m dvd Suc n"
+  have aux1: False if "Suc (Suc n) \<le> m" and "m dvd Suc n" for m :: nat
+  proof -
     from \<open>m dvd Suc n\<close> obtain q where "Suc n = m * q" ..
     with \<open>Suc (Suc n) \<le> m\<close> have "Suc (m * q) \<le> m" by simp
     then have "m * q < m" by arith
     then have "q = 0" by simp
-    with \<open>Suc n = m * q\<close> have False by simp
-  } note aux1 = this
-  { fix m q :: nat
-    assume "\<forall>q>0. 1 < q \<longrightarrow> Suc n < q \<longrightarrow> q \<le> Suc (n + length bs)
-      \<longrightarrow> bs ! (q - Suc (Suc n)) \<longrightarrow> \<not> Suc n dvd q \<longrightarrow> q dvd m \<longrightarrow> m dvd q"
-    then have *: "\<And>q. Suc n < q \<Longrightarrow> q \<le> Suc (n + length bs)
-      \<Longrightarrow> bs ! (q - Suc (Suc n)) \<Longrightarrow> \<not> Suc n dvd q \<Longrightarrow> q dvd m \<Longrightarrow> m dvd q"
+    with \<open>Suc n = m * q\<close> show ?thesis by simp
+  qed
+  have aux2: "m dvd q"
+    if 1: "\<forall>q>0. 1 < q \<longrightarrow> Suc n < q \<longrightarrow> q \<le> Suc (n + length bs) \<longrightarrow>
+      bs ! (q - Suc (Suc n)) \<longrightarrow> \<not> Suc n dvd q \<longrightarrow> q dvd m \<longrightarrow> m dvd q"
+    and 2: "\<not> Suc n dvd m" "q dvd m"
+    and 3: "Suc n < q" "q \<le> Suc (n + length bs)" "bs ! (q - Suc (Suc n))"
+    for m q :: nat
+  proof -
+    from 1 have *: "\<And>q. Suc n < q \<Longrightarrow> q \<le> Suc (n + length bs) \<Longrightarrow>
+      bs ! (q - Suc (Suc n)) \<Longrightarrow> \<not> Suc n dvd q \<Longrightarrow> q dvd m \<Longrightarrow> m dvd q"
       by auto
-    assume "\<not> Suc n dvd m" and "q dvd m"
-    then have "\<not> Suc n dvd q" by (auto elim: dvdE)
-    moreover assume "Suc n < q" and "q \<le> Suc (n + length bs)"
-      and "bs ! (q - Suc (Suc n))"
+    from 2 have "\<not> Suc n dvd q" by (auto elim: dvdE)
+    moreover note 3
     moreover note \<open>q dvd m\<close>
-    ultimately have "m dvd q" by (auto intro: *)
-  } note aux2 = this
+    ultimately show ?thesis by (auto intro: *)
+  qed
   from 3 show ?case
-    apply (simp_all add: numbers_of_marks_mark_out numbers_of_marks_Suc Compr_image_eq inj_image_eq_iff
-      in_numbers_of_marks_eq Ball_def imp_conjL aux)
+    apply (simp_all add: numbers_of_marks_mark_out numbers_of_marks_Suc Compr_image_eq
+      inj_image_eq_iff in_numbers_of_marks_eq Ball_def imp_conjL aux)
     apply safe
     apply (simp_all add: less_diff_conv2 le_diff_conv2 dvd_minus_self not_less)
     apply (clarsimp dest!: aux1)
     apply (simp add: Suc_le_eq less_Suc_eq_le)
-    apply (rule aux2) apply (clarsimp dest!: aux1)+
+    apply (rule aux2)
+    apply (clarsimp dest!: aux1)+
     done
 qed
 
@@ -240,51 +243,56 @@
 where
   "primes_upto n = sorted_list_of_set {m. m \<le> n \<and> prime m}"
 
-lemma set_primes_upto:
-  "set (primes_upto n) = {m. m \<le> n \<and> prime m}"
+lemma set_primes_upto: "set (primes_upto n) = {m. m \<le> n \<and> prime m}"
   by (simp add: primes_upto_def)
 
-lemma sorted_primes_upto [iff]:
-  "sorted (primes_upto n)"
+lemma sorted_primes_upto [iff]: "sorted (primes_upto n)"
   by (simp add: primes_upto_def)
 
-lemma distinct_primes_upto [iff]:
-  "distinct (primes_upto n)"
+lemma distinct_primes_upto [iff]: "distinct (primes_upto n)"
   by (simp add: primes_upto_def)
 
 lemma set_primes_upto_sieve:
   "set (primes_upto n) = numbers_of_marks 2 (sieve 1 (replicate (n - 1) True))"
-proof (cases "n > 1")
-  case False then have "n = 0 \<or> n = 1" by arith
+proof -
+  consider "n = 0 \<or> n = 1" | "n > 1" by arith
   then show ?thesis
-    by (auto simp add: numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto dest: prime_gt_Suc_0_nat)
-next
-  { fix m q
-    assume "Suc (Suc 0) \<le> q"
-      and "q < Suc n"
-      and "m dvd q"
-    then have "m < Suc n" by (auto dest: dvd_imp_le)
-    assume *: "\<forall>m\<in>{Suc (Suc 0)..<Suc n}. m dvd q \<longrightarrow> q dvd m"
-      and "m dvd q" and "m \<noteq> 1"
-    have "m = q" proof (cases "m = 0")
-      case True with \<open>m dvd q\<close> show ?thesis by simp
-    next
-      case False with \<open>m \<noteq> 1\<close> have "Suc (Suc 0) \<le> m" by arith
-      with \<open>m < Suc n\<close> * \<open>m dvd q\<close> have "q dvd m" by simp
-      with \<open>m dvd q\<close> show ?thesis by (simp add: dvd.eq_iff)
-    qed
-  }
-  then have aux: "\<And>m q. Suc (Suc 0) \<le> q \<Longrightarrow>
-    q < Suc n \<Longrightarrow>
-    m dvd q \<Longrightarrow>
-    \<forall>m\<in>{Suc (Suc 0)..<Suc n}. m dvd q \<longrightarrow> q dvd m \<Longrightarrow>
-    m dvd q \<Longrightarrow> m \<noteq> q \<Longrightarrow> m = 1" by auto
-  case True then show ?thesis
-    apply (auto simp add: One_nat_def numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto
+  proof cases
+    case 1
+    then show ?thesis
+      by (auto simp add: numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto
         dest: prime_gt_Suc_0_nat)
-    apply (metis One_nat_def Suc_le_eq less_not_refl prime_nat_def)
-    apply (metis One_nat_def Suc_le_eq aux prime_nat_def)
-    done
+  next
+    case 2
+    {
+      fix m q
+      assume "Suc (Suc 0) \<le> q"
+        and "q < Suc n"
+        and "m dvd q"
+      then have "m < Suc n" by (auto dest: dvd_imp_le)
+      assume *: "\<forall>m\<in>{Suc (Suc 0)..<Suc n}. m dvd q \<longrightarrow> q dvd m"
+        and "m dvd q" and "m \<noteq> 1"
+      have "m = q"
+      proof (cases "m = 0")
+        case True with \<open>m dvd q\<close> show ?thesis by simp
+      next
+        case False with \<open>m \<noteq> 1\<close> have "Suc (Suc 0) \<le> m" by arith
+        with \<open>m < Suc n\<close> * \<open>m dvd q\<close> have "q dvd m" by simp
+        with \<open>m dvd q\<close> show ?thesis by (simp add: dvd.eq_iff)
+      qed
+    }
+    then have aux: "\<And>m q. Suc (Suc 0) \<le> q \<Longrightarrow>
+      q < Suc n \<Longrightarrow>
+      m dvd q \<Longrightarrow>
+      \<forall>m\<in>{Suc (Suc 0)..<Suc n}. m dvd q \<longrightarrow> q dvd m \<Longrightarrow>
+      m dvd q \<Longrightarrow> m \<noteq> q \<Longrightarrow> m = 1" by auto
+    from 2 show ?thesis
+      apply (auto simp add: numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto
+        dest: prime_gt_Suc_0_nat)
+      apply (metis One_nat_def Suc_le_eq less_not_refl prime_nat_def)
+      apply (metis One_nat_def Suc_le_eq aux prime_nat_def)
+      done
+  qed
 qed
 
 lemma primes_upto_sieve [code]:
@@ -295,11 +303,11 @@
     apply (simp_all only: set_primes_upto_sieve numbers_of_marks_def)
     apply auto
     done
-  then show ?thesis by (simp add: sorted_list_of_set_numbers_of_marks)
+  then show ?thesis
+    by (simp add: sorted_list_of_set_numbers_of_marks)
 qed
 
-lemma prime_in_primes_upto:
-  "prime n \<longleftrightarrow> n \<in> set (primes_upto n)"
+lemma prime_in_primes_upto: "prime n \<longleftrightarrow> n \<in> set (primes_upto n)"
   by (simp add: set_primes_upto)
 
 
@@ -309,19 +317,19 @@
 where
   "smallest_prime_beyond n = (LEAST p. prime p \<and> p \<ge> n)"
 
-lemma
-  prime_smallest_prime_beyond [iff]: "prime (smallest_prime_beyond n)" (is ?P)
+lemma prime_smallest_prime_beyond [iff]: "prime (smallest_prime_beyond n)" (is ?P)
   and smallest_prime_beyond_le [iff]: "smallest_prime_beyond n \<ge> n" (is ?Q)
 proof -
   let ?least = "LEAST p. prime p \<and> p \<ge> n"
   from primes_infinite obtain q where "prime q \<and> q \<ge> n"
     by (metis finite_nat_set_iff_bounded_le mem_Collect_eq nat_le_linear)
-  then have "prime ?least \<and> ?least \<ge> n" by (rule LeastI)
-  then show ?P and ?Q by (simp_all add: smallest_prime_beyond_def)
+  then have "prime ?least \<and> ?least \<ge> n"
+    by (rule LeastI)
+  then show ?P and ?Q
+    by (simp_all add: smallest_prime_beyond_def)
 qed
 
-lemma smallest_prime_beyond_smallest:
-  "prime p \<Longrightarrow> p \<ge> n \<Longrightarrow> smallest_prime_beyond n \<le> p"
+lemma smallest_prime_beyond_smallest: "prime p \<Longrightarrow> p \<ge> n \<Longrightarrow> smallest_prime_beyond n \<le> p"
   by (simp only: smallest_prime_beyond_def) (auto intro: Least_le)
 
 lemma smallest_prime_beyond_eq:
@@ -341,22 +349,28 @@
   "smallest_prime_between m n = Some p \<longleftrightarrow> smallest_prime_beyond m = p \<and> p \<le> n"
   by (auto simp add: smallest_prime_between_def dest: smallest_prime_beyond_smallest [of _ m])
 
-lemma [code]:
-  "smallest_prime_between m n = List.find (\<lambda>p. p \<ge> m) (primes_upto n)"
+lemma [code]: "smallest_prime_between m n = List.find (\<lambda>p. p \<ge> m) (primes_upto n)"
 proof -
-  { fix p
+  have "List.find (\<lambda>p. p \<ge> m) (primes_upto n) = Some (smallest_prime_beyond m)"
+    if assms: "m \<le> p" "prime p" "p \<le> n" for p
+  proof -
     def A \<equiv> "{p. p \<le> n \<and> prime p \<and> m \<le> p}"
-    assume assms: "m \<le> p" "prime p" "p \<le> n"
-    then have "smallest_prime_beyond m \<le> p" by (auto intro: smallest_prime_beyond_smallest)
-    from this \<open>p \<le> n\<close> have *: "smallest_prime_beyond m \<le> n" by (rule order_trans)
-    from assms have ex: "\<exists>p\<le>n. prime p \<and> m \<le> p" by auto
-    then have "finite A" by (auto simp add: A_def)
+    from assms have "smallest_prime_beyond m \<le> p"
+      by (auto intro: smallest_prime_beyond_smallest)
+    from this \<open>p \<le> n\<close> have *: "smallest_prime_beyond m \<le> n"
+      by (rule order_trans)
+    from assms have ex: "\<exists>p\<le>n. prime p \<and> m \<le> p"
+      by auto
+    then have "finite A"
+      by (auto simp add: A_def)
     with * have "Min A = smallest_prime_beyond m"
       by (auto simp add: A_def intro: Min_eqI smallest_prime_beyond_smallest)
-    with ex sorted_primes_upto have "List.find (\<lambda>p. p \<ge> m) (primes_upto n) = Some (smallest_prime_beyond m)"
+    with ex sorted_primes_upto show ?thesis
       by (auto simp add: set_primes_upto sorted_find_Min A_def)
-  } then show ?thesis  
-  by (auto simp add: smallest_prime_between_def find_None_iff set_primes_upto intro!: sym [of _ None])
+  qed
+  then show ?thesis
+    by (auto simp add: smallest_prime_between_def find_None_iff set_primes_upto
+      intro!: sym [of _ None])
 qed
 
 definition smallest_prime_beyond_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat"
@@ -365,14 +379,12 @@
 
 lemma [code]:
   "smallest_prime_beyond_aux k n =
-    (case smallest_prime_between n (k * n)
-     of Some p \<Rightarrow> p
-      | None \<Rightarrow> smallest_prime_beyond_aux (Suc k) n)"
+    (case smallest_prime_between n (k * n) of
+      Some p \<Rightarrow> p
+    | None \<Rightarrow> smallest_prime_beyond_aux (Suc k) n)"
   by (simp add: smallest_prime_beyond_aux_def smallest_prime_betwen_Some split: option.split)
 
-lemma [code]:
-  "smallest_prime_beyond n = smallest_prime_beyond_aux 2 n"
+lemma [code]: "smallest_prime_beyond n = smallest_prime_beyond_aux 2 n"
   by (simp add: smallest_prime_beyond_aux_def)
 
 end
-
diff -r fad653acf58f -r eb431a5651fe src/HOL/Number_Theory/Fib.thy
--- a/src/HOL/Number_Theory/Fib.thy	Fri Jun 19 21:41:33 2015 +0200
+++ b/src/HOL/Number_Theory/Fib.thy	Fri Jun 19 23:40:46 2015 +0200
@@ -1,17 +1,12 @@
 (*  Title:      HOL/Number_Theory/Fib.thy
     Author:     Lawrence C. Paulson
     Author:     Jeremy Avigad
-
-Defines the fibonacci function.
-
-The original "Fib" is due to Lawrence C. Paulson, and was adapted by
-Jeremy Avigad.
 *)
 
-section \<open>Fib\<close>
+section \<open>The fibonacci function\<close>
 
 theory Fib
-imports Main "../GCD" "../Binomial"
+imports Main GCD Binomial
 begin
 
 
@@ -19,9 +14,10 @@
 
 fun fib :: "nat \<Rightarrow> nat"
 where
-    fib0: "fib 0 = 0"
-  | fib1: "fib (Suc 0) = 1"
-  | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
+  fib0: "fib 0 = 0"
+| fib1: "fib (Suc 0) = 1"
+| fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
+
 
 subsection \<open>Basic Properties\<close>
 
@@ -41,6 +37,7 @@
 lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0"
   by (induct n rule: fib.induct) (auto simp add: )
 
+
 subsection \<open>A Few Elementary Results\<close>
 
 text \<open>
@@ -49,12 +46,12 @@
 \<close>
 
 lemma fib_Cassini_int: "int (fib (Suc (Suc n)) * fib n) - int((fib (Suc n))\<^sup>2) = - ((-1)^n)"
-  by (induction n rule: fib.induct)  (auto simp add: field_simps power2_eq_square power_add)
+  by (induct n rule: fib.induct)  (auto simp add: field_simps power2_eq_square power_add)
 
 lemma fib_Cassini_nat:
-    "fib (Suc (Suc n)) * fib n =
-       (if even n then (fib (Suc n))\<^sup>2 - 1 else (fib (Suc n))\<^sup>2 + 1)"
-using fib_Cassini_int [of n] by auto
+  "fib (Suc (Suc n)) * fib n =
+     (if even n then (fib (Suc n))\<^sup>2 - 1 else (fib (Suc n))\<^sup>2 + 1)"
+  using fib_Cassini_int [of n] by auto
 
 
 subsection \<open>Law 6.111 of Concrete Mathematics\<close>
@@ -69,28 +66,26 @@
   apply (simp add: gcd_commute_nat [of "fib m"])
   apply (cases m)
   apply (auto simp add: fib_add)
-  apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute)
+  apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat
+    gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute)
   done
 
-lemma gcd_fib_diff: "m \<le> n \<Longrightarrow>
-    gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
+lemma gcd_fib_diff: "m \<le> n \<Longrightarrow> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
   by (simp add: gcd_fib_add [symmetric, of _ "n-m"])
 
-lemma gcd_fib_mod: "0 < m \<Longrightarrow>
-    gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
+lemma gcd_fib_mod: "0 < m \<Longrightarrow> gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
 proof (induct n rule: less_induct)
   case (less n)
-  from less.prems have pos_m: "0 < m" .
   show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
   proof (cases "m < n")
     case True
     then have "m \<le> n" by auto
-    with pos_m have pos_n: "0 < n" by auto
-    with pos_m \<open>m < n\<close> have diff: "n - m < n" by auto
+    with \<open>0 < m\<close> have pos_n: "0 < n" by auto
+    with \<open>0 < m\<close> \<open>m < n\<close> have diff: "n - m < n" by auto
     have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
       by (simp add: mod_if [of n]) (insert \<open>m < n\<close>, auto)
     also have "\<dots> = gcd (fib m)  (fib (n - m))"
-      by (simp add: less.hyps diff pos_m)
+      by (simp add: less.hyps diff \<open>0 < m\<close>)
     also have "\<dots> = gcd (fib m) (fib n)"
       by (simp add: gcd_fib_diff \<open>m \<le> n\<close>)
     finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
@@ -105,10 +100,10 @@
     -- \<open>Law 6.111\<close>
   by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod)
 
-theorem fib_mult_eq_setsum_nat:
-    "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
+theorem fib_mult_eq_setsum_nat: "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
   by (induct n rule: nat.induct) (auto simp add:  field_simps)
 
+
 subsection \<open>Fibonacci and Binomial Coefficients\<close>
 
 lemma setsum_drop_zero: "(\<Sum>k = 0..Suc n. if 0<k then (f (k - 1)) else 0) = (\<Sum>j = 0..n. f j)"
@@ -118,21 +113,22 @@
     "(\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k) choose (k - 1)) = (\<Sum>j = 0..n. (n-j) choose j)"
   by (rule trans [OF setsum.cong setsum_drop_zero]) auto
 
-lemma ne_diagonal_fib:
-   "(\<Sum>k = 0..n. (n-k) choose k) = fib (Suc n)"
+lemma ne_diagonal_fib: "(\<Sum>k = 0..n. (n-k) choose k) = fib (Suc n)"
 proof (induct n rule: fib.induct)
-  case 1 show ?case by simp
+  case 1
+  show ?case by simp
 next
-  case 2 show ?case by simp
+  case 2
+  show ?case by simp
 next
   case (3 n)
   have "(\<Sum>k = 0..Suc n. Suc (Suc n) - k choose k) =
         (\<Sum>k = 0..Suc n. (Suc n - k choose k) + (if k=0 then 0 else (Suc n - k choose (k - 1))))"
     by (rule setsum.cong) (simp_all add: choose_reduce_nat)
-  also have "... = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
+  also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
                    (\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k choose (k - 1)))"
     by (simp add: setsum.distrib)
-  also have "... = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
+  also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
                    (\<Sum>j = 0..n. n - j choose j)"
     by (metis setsum_choose_drop_zero)
   finally show ?case using 3
diff -r fad653acf58f -r eb431a5651fe src/HOL/Number_Theory/MiscAlgebra.thy
--- a/src/HOL/Number_Theory/MiscAlgebra.thy	Fri Jun 19 21:41:33 2015 +0200
+++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Fri Jun 19 23:40:46 2015 +0200
@@ -1,8 +1,8 @@
 (*  Title:      HOL/Number_Theory/MiscAlgebra.thy
     Author:     Jeremy Avigad
+*)
 
-These are things that can be added to the Algebra library.
-*)
+section \<open>Things that can be added to the Algebra library\<close>
 
 theory MiscAlgebra
 imports
@@ -10,26 +10,25 @@
   "~~/src/HOL/Algebra/FiniteProduct"
 begin
 
-(* finiteness stuff *)
+subsection \<open>Finiteness stuff\<close>
 
 lemma bounded_set1_int [intro]: "finite {(x::int). a < x & x < b & P x}"
   apply (subgoal_tac "{x. a < x & x < b & P x} <= {a<..<b}")
   apply (erule finite_subset)
   apply auto
-done
+  done
 
 
-(* The rest is for the algebra libraries *)
+subsection \<open>The rest is for the algebra libraries\<close>
 
-(* These go in Group.thy. *)
+subsubsection \<open>These go in Group.thy\<close>
 
-(*
+text \<open>
   Show that the units in any monoid give rise to a group.
 
   The file Residues.thy provides some infrastructure to use
   facts about the unit group within the ring locale.
-*)
-
+\<close>
 
 definition units_of :: "('a, 'b) monoid_scheme => 'a monoid" where
   "units_of G == (| carrier = Units G,
@@ -83,8 +82,7 @@
 lemma units_of_one: "one(units_of G) = one G"
   unfolding units_of_def by auto
 
-lemma (in monoid) units_of_inv: "x : Units G ==>
-    m_inv (units_of G) x = m_inv G x"
+lemma (in monoid) units_of_inv: "x : Units G ==> m_inv (units_of G) x = m_inv G x"
   apply (rule sym)
   apply (subst m_inv_def)
   apply (rule the1_equality)
@@ -103,14 +101,12 @@
   apply (subst units_of_mult [symmetric])
   apply (subst units_of_one [symmetric])
   apply (erule group.l_inv, assumption)
-done
+  done
 
-lemma (in group) inj_on_const_mult: "a: (carrier G) ==>
-    inj_on (%x. a \<otimes> x) (carrier G)"
+lemma (in group) inj_on_const_mult: "a: (carrier G) ==> inj_on (%x. a \<otimes> x) (carrier G)"
   unfolding inj_on_def by auto
 
-lemma (in group) surj_const_mult: "a : (carrier G) ==>
-    (%x. a \<otimes> x) ` (carrier G) = (carrier G)"
+lemma (in group) surj_const_mult: "a : (carrier G) ==> (%x. a \<otimes> x) ` (carrier G) = (carrier G)"
   apply (auto simp add: image_def)
   apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
   apply auto
@@ -120,8 +116,8 @@
   apply auto
   done
 
-lemma (in group) l_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
-    (x \<otimes> a = x) = (a = one G)"
+lemma (in group) l_cancel_one [simp]:
+    "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow> (x \<otimes> a = x) = (a = one G)"
   apply auto
   apply (subst l_cancel [symmetric])
   prefer 4
@@ -139,7 +135,6 @@
   done
 
 (* Is there a better way to do this? *)
-
 lemma (in group) l_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
     (x = x \<otimes> a) = (a = one G)"
   apply (subst eq_commute)
@@ -173,10 +168,9 @@
 qed
 
 
-(* Miscellaneous *)
+subsubsection \<open>Miscellaneous\<close>
 
-lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> ~= \<one>\<^bsub>R\<^esub> \<Longrightarrow> ALL x : carrier R - {\<zero>\<^bsub>R\<^esub>}.
-    x : Units R \<Longrightarrow> field R"
+lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> ~= \<one>\<^bsub>R\<^esub> \<Longrightarrow> \<forall>x \<in> carrier R - {\<zero>\<^bsub>R\<^esub>}. x \<in> Units R \<Longrightarrow> field R"
   apply (unfold_locales)
   apply (insert cring_axioms, auto)
   apply (rule trans)
@@ -239,10 +233,10 @@
   done
 
 lemma (in monoid) inv_eq_one_eq: "x : Units G \<Longrightarrow> (inv x = \<one>) = (x = \<one>)"
-by (metis Units_inv_inv inv_one)
+  by (metis Units_inv_inv inv_one)
 
 
-(* This goes in FiniteProduct *)
+subsubsection \<open>This goes in FiniteProduct\<close>
 
 lemma (in comm_monoid) finprod_UN_disjoint:
   "finite I \<Longrightarrow> (ALL i:I. finite (A i)) \<longrightarrow> (ALL i:I. ALL j:I. i ~= j \<longrightarrow>
@@ -276,17 +270,13 @@
 (* need better simplification rules for rings *)
 (* the next one holds more generally for abelian groups *)
 
-lemma (in cring) sum_zero_eq_neg:
-    "x : carrier R \<Longrightarrow> y : carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
-by (metis minus_equality)
+lemma (in cring) sum_zero_eq_neg: "x : carrier R \<Longrightarrow> y : carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
+  by (metis minus_equality)
 
-(* there's a name conflict -- maybe "domain" should be
-   "integral_domain" *)
-
-lemma (in Ring.domain) square_eq_one:
+lemma (in domain) square_eq_one:
   fixes x
-  assumes [simp]: "x : carrier R" and
-    "x \<otimes> x = \<one>"
+  assumes [simp]: "x : carrier R"
+    and "x \<otimes> x = \<one>"
   shows "x = \<one> | x = \<ominus>\<one>"
 proof -
   have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
@@ -308,23 +298,22 @@
     done
 qed
 
-lemma (in Ring.domain) inv_eq_self: "x : Units R \<Longrightarrow>
-    x = inv x \<Longrightarrow> x = \<one> | x = \<ominus> \<one>"
-by (metis Units_closed Units_l_inv square_eq_one)
+lemma (in Ring.domain) inv_eq_self: "x : Units R \<Longrightarrow> x = inv x \<Longrightarrow> x = \<one> \<or> x = \<ominus>\<one>"
+  by (metis Units_closed Units_l_inv square_eq_one)
 
 
-(*
+text \<open>
   The following translates theorems about groups to the facts about
   the units of a ring. (The list should be expanded as more things are
   needed.)
-*)
+\<close>
 
-lemma (in ring) finite_ring_finite_units [intro]:
-    "finite (carrier R) \<Longrightarrow> finite (Units R)"
+lemma (in ring) finite_ring_finite_units [intro]: "finite (carrier R) \<Longrightarrow> finite (Units R)"
   by (rule finite_subset) auto
 
 lemma (in monoid) units_of_pow:
-    "x : Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> (n::nat) = x (^)\<^bsub>G\<^esub> n"
+  fixes n :: nat
+  shows "x \<in> Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> n = x (^)\<^bsub>G\<^esub> n"
   apply (induct n)
   apply (auto simp add: units_group group.is_monoid
     monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)
diff -r fad653acf58f -r eb431a5651fe src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Fri Jun 19 21:41:33 2015 +0200
+++ b/src/HOL/Number_Theory/Residues.thy	Fri Jun 19 23:40:46 2015 +0200
@@ -11,26 +11,21 @@
 imports UniqueFactorization MiscAlgebra
 begin
 
-(*
-
-  A locale for residue rings
-
-*)
+subsection \<open>A locale for residue rings\<close>
 
-definition residue_ring :: "int => int ring" where
-  "residue_ring m == (|
-    carrier =       {0..m - 1},
-    mult =          (%x y. (x * y) mod m),
-    one =           1,
-    zero =          0,
-    add =           (%x y. (x + y) mod m) |)"
+definition residue_ring :: "int \<Rightarrow> int ring"
+  where
+  "residue_ring m =
+    \<lparr>carrier = {0..m - 1},
+     mult = \<lambda>x y. (x * y) mod m,
+     one = 1,
+     zero = 0,
+     add = \<lambda>x y. (x + y) mod m\<rparr>"
 
 locale residues =
   fixes m :: int and R (structure)
   assumes m_gt_one: "m > 1"
-  defines "R == residue_ring m"
-
-context residues
+  defines "R \<equiv> residue_ring m"
 begin
 
 lemma abelian_group: "abelian_group R"
@@ -76,8 +71,10 @@
 context residues
 begin
 
-(* These lemmas translate back and forth between internal and
-   external concepts *)
+text \<open>
+  These lemmas translate back and forth between internal and
+  external concepts.
+\<close>
 
 lemma res_carrier_eq: "carrier R = {0..m - 1}"
   unfolding R_def residue_ring_def by auto
@@ -94,11 +91,11 @@
 lemma res_one_eq: "\<one> = 1"
   unfolding R_def residue_ring_def units_of_def by auto
 
-lemma res_units_eq: "Units R = { x. 0 < x & x < m & coprime x m}"
+lemma res_units_eq: "Units R = {x. 0 < x \<and> x < m \<and> coprime x m}"
   apply (insert m_gt_one)
   apply (unfold Units_def R_def residue_ring_def)
   apply auto
-  apply (subgoal_tac "x ~= 0")
+  apply (subgoal_tac "x \<noteq> 0")
   apply auto
   apply (metis invertible_coprime_int)
   apply (subst (asm) coprime_iff_invertible'_int)
@@ -121,19 +118,20 @@
   done
 
 lemma finite [iff]: "finite (carrier R)"
-  by (subst res_carrier_eq, auto)
+  by (subst res_carrier_eq) auto
 
 lemma finite_Units [iff]: "finite (Units R)"
   by (subst res_units_eq) auto
 
-(* The function a -> a mod m maps the integers to the
-   residue classes. The following lemmas show that this mapping
-   respects addition and multiplication on the integers. *)
+text \<open>
+  The function @{text "a \<mapsto> a mod m"} maps the integers to the
+  residue classes. The following lemmas show that this mapping
+  respects addition and multiplication on the integers.
+\<close>
 
-lemma mod_in_carrier [iff]: "a mod m : carrier R"
-  apply (unfold res_carrier_eq)
-  apply (insert m_gt_one, auto)
-  done
+lemma mod_in_carrier [iff]: "a mod m \<in> carrier R"
+  unfolding res_carrier_eq
+  using insert m_gt_one by auto
 
 lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m"
   unfolding R_def residue_ring_def
@@ -151,7 +149,7 @@
 lemma one_cong: "\<one> = 1 mod m"
   using m_gt_one unfolding R_def residue_ring_def by auto
 
-(* revise algebra library to use 1? *)
+(* FIXME revise algebra library to use 1? *)
 lemma pow_cong: "(x mod m) (^) n = x^n mod m"
   apply (insert m_gt_one)
   apply (induct n)
@@ -162,19 +160,17 @@
 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:A. f i) mod m"
+lemma (in residues) prod_cong: "finite A \<Longrightarrow> (\<Otimes> i: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: A. f i) mod m"
+lemma (in residues) sum_cong: "finite A \<Longrightarrow> (\<Oplus> i: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 : Units R"
-  apply (subst res_units_eq, auto)
+lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow> a mod m \<in> Units R"
+  apply (subst res_units_eq)
+  apply auto
   apply (insert pos_mod_sign [of m a])
-  apply (subgoal_tac "a mod m ~= 0")
+  apply (subgoal_tac "a mod m \<noteq> 0")
   apply arith
   apply auto
   apply (metis gcd_int.commute gcd_red_int)
@@ -183,13 +179,13 @@
 lemma res_eq_to_cong: "((a mod m) = (b mod m)) = [a = b] (mod (m::int))"
   unfolding cong_int_def by auto
 
-(* Simplifying with these will translate a ring equation in R to a
-   congruence. *)
 
+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
 
-(* Other useful facts about the residue ring *)
+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)
@@ -200,12 +196,12 @@
 end
 
 
-(* prime residues *)
+subsection \<open>Prime residues\<close>
 
 locale residues_prime =
   fixes p and R (structure)
   assumes p_prime [intro]: "prime p"
-  defines "R == residue_ring p"
+  defines "R \<equiv> residue_ring p"
 
 sublocale residues_prime < residues p
   apply (unfold R_def residues_def)
@@ -243,40 +239,42 @@
   by (rule is_field)
 
 
-(*
-  Test cases: Euler's theorem and Wilson's theorem.
-*)
+section \<open>Test cases: Euler's theorem and Wilson's theorem\<close>
 
-
-subsection\<open>Euler's theorem\<close>
+subsection \<open>Euler's theorem\<close>
 
-(* the definition of the phi function *)
+text \<open>The definition of the phi function.\<close>
 
-definition phi :: "int => nat"
-  where "phi m = card({ x. 0 < x & x < m & gcd x m = 1})"
+definition phi :: "int \<Rightarrow> nat"
+  where "phi m = card {x. 0 < x \<and> x < m \<and> gcd x m = 1}"
 
-lemma phi_def_nat: "phi m = card({ x. 0 < x & x < nat m & gcd x (nat m) = 1})"
+lemma phi_def_nat: "phi m = card {x. 0 < x \<and> x < nat m \<and> gcd x (nat m) = 1}"
   apply (simp add: phi_def)
   apply (rule bij_betw_same_card [of nat])
   apply (auto simp add: inj_on_def bij_betw_def image_def)
   apply (metis dual_order.irrefl dual_order.strict_trans leI nat_1 transfer_nat_int_gcd(1))
-  apply (metis One_nat_def int_0 int_1 int_less_0_conv int_nat_eq nat_int transfer_int_nat_gcd(1) zless_int)
+  apply (metis One_nat_def int_0 int_1 int_less_0_conv int_nat_eq nat_int
+    transfer_int_nat_gcd(1) zless_int)
   done
 
 lemma prime_phi:
-  assumes  "2 \<le> p" "phi p = p - 1" shows "prime p"
+  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}"
     using assms unfolding phi_def_nat
     by (intro card_seteq) fastforce+
-  then have cop: "\<And>x. x \<in> {1::nat..p - 1} \<Longrightarrow> coprime x p"
+  then have cop: "\<And>x::nat. x \<in> {1..p - 1} \<Longrightarrow> coprime x p"
     by blast
-  { fix x::nat assume *: "1 < x" "x < p" and "x dvd p"
+  have False if *: "1 < x" "x < p" and "x dvd p" for x :: nat
+  proof -
     have "coprime x p"
       apply (rule cop)
       using * apply auto
       done
-    with \<open>x dvd p\<close> \<open>1 < x\<close> have "False" by auto }
+    with \<open>x dvd p\<close> \<open>1 < x\<close> show ?thesis
+      by auto
+  qed
   then show ?thesis
     using \<open>2 \<le> p\<close>
     by (simp add: prime_def)
@@ -285,9 +283,9 @@
 qed
 
 lemma phi_zero [simp]: "phi 0 = 0"
-  apply (subst phi_def)
+  unfolding phi_def
 (* Auto hangs here. Once again, where is the simplification rule
-   1 == Suc 0 coming from? *)
+   1 \<equiv> Suc 0 coming from? *)
   apply (auto simp add: card_eq_0_iff)
 (* Add card_eq_0_iff as a simp rule? delete card_empty_imp? *)
   done
@@ -295,19 +293,19 @@
 lemma phi_one [simp]: "phi 1 = 0"
   by (auto simp add: phi_def card_eq_0_iff)
 
-lemma (in residues) phi_eq: "phi m = card(Units R)"
+lemma (in residues) phi_eq: "phi m = card (Units R)"
   by (simp add: phi_def res_units_eq)
 
 lemma (in residues) euler_theorem1:
   assumes a: "gcd a m = 1"
   shows "[a^phi m = 1] (mod m)"
 proof -
-  from a m_gt_one have [simp]: "a mod m : Units R"
+  from a m_gt_one have [simp]: "a mod m \<in> Units R"
     by (intro mod_in_res_units)
   from phi_eq have "(a mod m) (^) (phi m) = (a mod m) (^) (card (Units R))"
     by simp
   also have "\<dots> = \<one>"
-    by (intro units_power_order_eq_one, auto)
+    by (intro units_power_order_eq_one) auto
   finally show ?thesis
     by (simp add: res_to_cong_simps)
 qed
@@ -329,55 +327,57 @@
 (* outside the locale, we can relax the restriction m > 1 *)
 
 lemma euler_theorem:
-  assumes "m >= 0" and "gcd a m = 1"
+  assumes "m \<ge> 0"
+    and "gcd a m = 1"
   shows "[a^phi m = 1] (mod m)"
-proof (cases)
-  assume "m = 0 | m = 1"
+proof (cases "m = 0 | m = 1")
+  case True
   then show ?thesis by auto
 next
-  assume "~(m = 0 | m = 1)"
+  case False
   with assms show ?thesis
     by (intro residues.euler_theorem1, unfold residues_def, auto)
 qed
 
-lemma (in residues_prime) phi_prime: "phi p = (nat p - 1)"
+lemma (in residues_prime) phi_prime: "phi p = nat p - 1"
   apply (subst phi_eq)
   apply (subst res_prime_units_eq)
   apply auto
   done
 
-lemma phi_prime: "prime p \<Longrightarrow> phi p = (nat p - 1)"
+lemma phi_prime: "prime p \<Longrightarrow> phi p = nat p - 1"
   apply (rule residues_prime.phi_prime)
   apply (erule residues_prime.intro)
   done
 
 lemma fermat_theorem:
-  fixes a::int
-  assumes "prime p" and "~ (p dvd a)"
+  fixes a :: int
+  assumes "prime p"
+    and "\<not> p dvd a"
   shows "[a^(p - 1) = 1] (mod p)"
 proof -
-  from assms have "[a^phi p = 1] (mod p)"
+  from assms have "[a ^ phi p = 1] (mod p)"
     apply (intro euler_theorem)
     apply (metis of_nat_0_le_iff)
     apply (metis gcd_int.commute prime_imp_coprime_int)
     done
   also have "phi p = nat p - 1"
-    by (rule phi_prime, rule assms)
+    by (rule phi_prime) (rule assms)
   finally show ?thesis
     by (metis nat_int)
 qed
 
 lemma fermat_theorem_nat:
-  assumes "prime p" and "~ (p dvd a)"
-  shows "[a^(p - 1) = 1] (mod p)"
-using fermat_theorem [of p a] assms
-by (metis int_1 of_nat_power transfer_int_nat_cong zdvd_int)
+  assumes "prime p" and "\<not> p dvd a"
+  shows "[a ^ (p - 1) = 1] (mod p)"
+  using fermat_theorem [of p a] assms
+  by (metis int_1 of_nat_power transfer_int_nat_cong zdvd_int)
 
 
 subsection \<open>Wilson's theorem\<close>
 
-lemma (in field) inv_pair_lemma: "x : Units R \<Longrightarrow> y : Units R \<Longrightarrow>
-    {x, inv x} ~= {y, inv y} \<Longrightarrow> {x, inv x} Int {y, inv y} = {}"
+lemma (in field) inv_pair_lemma: "x \<in> Units R \<Longrightarrow> y \<in> Units R \<Longrightarrow>
+    {x, inv x} \<noteq> {y, inv y} \<Longrightarrow> {x, inv x} \<inter> {y, inv y} = {}"
   apply auto
   apply (metis Units_inv_inv)+
   done
@@ -386,41 +386,43 @@
   assumes a: "p > 2"
   shows "[fact (p - 1) = (-1::int)] (mod p)"
 proof -
-  let ?InversePairs = "{ {x, inv x} | x. x : Units R - {\<one>, \<ominus> \<one>}}"
-  have UR: "Units R = {\<one>, \<ominus> \<one>} Un (Union ?InversePairs)"
+  let ?Inverse_Pairs = "{{x, inv x}| x. x \<in> Units R - {\<one>, \<ominus> \<one>}}"
+  have UR: "Units R = {\<one>, \<ominus> \<one>} \<union> \<Union>?Inverse_Pairs"
     by auto
-  have "(\<Otimes>i: Units R. i) =
-    (\<Otimes>i: {\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i: Union ?InversePairs. i)"
+  have "(\<Otimes>i\<in>Units R. i) = (\<Otimes>i\<in>{\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i\<in>\<Union>?Inverse_Pairs. i)"
     apply (subst UR)
     apply (subst finprod_Un_disjoint)
     apply (auto intro: funcsetI)
-    apply (metis Units_inv_inv inv_one inv_neg_one)+
+    using inv_one apply auto[1]
+    using inv_eq_neg_one_eq apply auto
     done
-  also have "(\<Otimes>i: {\<one>, \<ominus> \<one>}. i) = \<ominus> \<one>"
+  also have "(\<Otimes>i\<in>{\<one>, \<ominus> \<one>}. i) = \<ominus> \<one>"
     apply (subst finprod_insert)
     apply auto
     apply (frule one_eq_neg_one)
-    apply (insert a, force)
+    using a apply force
     done
-  also have "(\<Otimes>i:(Union ?InversePairs). i) =
-      (\<Otimes>A: ?InversePairs. (\<Otimes>y:A. y))"
-    apply (subst finprod_Union_disjoint, auto)
+  also have "(\<Otimes>i\<in>(\<Union>?Inverse_Pairs). i) = (\<Otimes>A\<in>?Inverse_Pairs. (\<Otimes>y\<in>A. y))"
+    apply (subst finprod_Union_disjoint)
+    apply auto
     apply (metis Units_inv_inv)+
     done
   also have "\<dots> = \<one>"
-    apply (rule finprod_one, auto)
-    apply (subst finprod_insert, auto)
+    apply (rule finprod_one)
+    apply auto
+    apply (subst finprod_insert)
+    apply auto
     apply (metis inv_eq_self)
     done
-  finally have "(\<Otimes>i: Units R. i) = \<ominus> \<one>"
+  finally have "(\<Otimes>i\<in>Units R. i) = \<ominus> \<one>"
     by simp
-  also have "(\<Otimes>i: Units R. i) = (\<Otimes>i: Units R. i mod p)"
+  also have "(\<Otimes>i\<in>Units R. i) = (\<Otimes>i\<in>Units R. i mod p)"
     apply (rule finprod_cong')
-    apply (auto)
+    apply auto
     apply (subst (asm) res_prime_units_eq)
     apply auto
     done
-  also have "\<dots> = (PROD i: Units R. i) mod p"
+  also have "\<dots> = (\<Prod>i\<in>Units R. i) mod p"
     apply (rule prod_cong)
     apply auto
     done
@@ -430,13 +432,14 @@
     apply (subst res_prime_units_eq)
     apply (simp add: int_setprod zmod_int setprod_int_eq)
     done
-  finally have "fact (p - 1) mod p = (\<ominus> \<one> :: int)".
-  then show ?thesis  
+  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)
 qed
 
 lemma wilson_theorem:
-  assumes "prime p" shows "[fact (p - 1) = - 1] (mod p)"
+  assumes "prime p"
+  shows "[fact (p - 1) = - 1] (mod p)"
 proof (cases "p = 2")
   case True
   then show ?thesis
diff -r fad653acf58f -r eb431a5651fe src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Fri Jun 19 21:41:33 2015 +0200
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Fri Jun 19 23:40:46 2015 +0200
@@ -1,14 +1,12 @@
 (*  Title:      HOL/Number_Theory/UniqueFactorization.thy
     Author:     Jeremy Avigad
 
-Unique factorization for the natural numbers and the integers.
-
 Note: there were previous Isabelle formalizations of unique
 factorization due to Thomas Marthedal Rasmussen, and, building on
-that, by Jeremy Avigad and David Gray.  
+that, by Jeremy Avigad and David Gray.
 *)
 
-section \<open>UniqueFactorization\<close>
+section \<open>Unique factorization for the natural numbers and the integers\<close>
 
 theory UniqueFactorization
 imports Cong "~~/src/HOL/Library/Multiset"
@@ -18,132 +16,135 @@
 
      prime p \<Longrightarrow> p > 0
 
-   wreaks havoc here. When the premise includes ALL x :# M. prime x, it 
+   wreaks havoc here. When the premise includes \<forall>x \<in># M. prime x, it
    leads to the backchaining
 
-     x > 0  
-     prime x 
-     x :# M   which is, unfortunately,
+     x > 0
+     prime x
+     x \<in># M   which is, unfortunately,
      count M x > 0
 *)
 
 (* Here is a version of set product for multisets. Is it worth moving
-   to multiset.thy? If so, one should similarly define msetsum for abelian 
-   semirings, using of_nat. Also, is it worth developing bounded quantifiers 
-   "ALL i :# M. P i"? 
+   to multiset.thy? If so, one should similarly define msetsum for abelian
+   semirings, using of_nat. Also, is it worth developing bounded quantifiers
+   "\<forall>i \<in># M. P i"?
 *)
 
 
-subsection \<open>unique factorization: multiset version\<close>
+subsection \<open>Unique factorization: multiset version\<close>
 
-lemma multiset_prime_factorization_exists [rule_format]: "n > 0 --> 
-    (EX M. (ALL (p::nat) : set_mset M. prime p) & n = (PROD i :# M. i))"
-proof (rule nat_less_induct, clarify)
+lemma multiset_prime_factorization_exists:
+  "n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))"
+proof (induct n rule: nat_less_induct)
   fix n :: nat
-  assume ih: "ALL m < n. 0 < m --> (EX M. (ALL p : set_mset M. prime p) & m = 
-      (PROD i :# M. i))"
-  assume "(n::nat) > 0"
-  then have "n = 1 | (n > 1 & prime n) | (n > 1 & ~ prime n)"
+  assume ih: "\<forall>m < n. 0 < m \<longrightarrow> (\<exists>M. (\<forall>p\<in>set_mset M. prime p) \<and> m = (\<Prod>i \<in># M. i))"
+  assume "n > 0"
+  then consider "n = 1" | "n > 1" "prime n" | "n > 1" "\<not> prime n"
     by arith
-  moreover {
-    assume "n = 1"
-    then have "(ALL p : set_mset {#}. prime p) & n = (PROD i :# {#}. i)" by auto
-  } moreover {
-    assume "n > 1" and "prime n"
-    then have "(ALL p : set_mset {# n #}. prime p) & n = (PROD i :# {# n #}. i)"
+  then show "\<exists>M. (\<forall>p \<in> set_mset M. prime p) \<and> n = (\<Prod>i::nat\<in>#M. i)"
+  proof cases
+    case 1
+    then have "(\<forall>p\<in>set_mset {#}. prime p) \<and> n = (\<Prod>i \<in># {#}. i)"
       by auto
-  } moreover {
-    assume "n > 1" and "~ prime n"
+    then show ?thesis ..
+  next
+    case 2
+    then have "(\<forall>p\<in>set_mset {#n#}. prime p) \<and> n = (\<Prod>i \<in># {#n#}. i)"
+      by auto
+    then show ?thesis ..
+  next
+    case 3
     with not_prime_eq_prod_nat
-    obtain m k where n: "n = m * k & 1 < m & m < n & 1 < k & k < n"
+    obtain m k where n: "n = m * k" "1 < m" "m < n" "1 < k" "k < n"
       by blast
-    with ih obtain Q R where "(ALL p : set_mset Q. prime p) & m = (PROD i:#Q. i)"
-        and "(ALL p: set_mset R. prime p) & k = (PROD i:#R. i)"
+    with ih obtain Q R where "(\<forall>p \<in> set_mset Q. prime p) \<and> m = (\<Prod>i\<in>#Q. i)"
+        and "(\<forall>p\<in>set_mset R. prime p) \<and> k = (\<Prod>i\<in>#R. i)"
       by blast
-    then have "(ALL p: set_mset (Q + R). prime p) & n = (PROD i :# Q + R. i)"
+    then have "(\<forall>p\<in>set_mset (Q + R). prime p) \<and> n = (\<Prod>i \<in># Q + R. i)"
       by (auto simp add: n msetprod_Un)
-    then have "EX M. (ALL p : set_mset M. prime p) & n = (PROD i :# M. i)"..
-  }
-  ultimately show "EX M. (ALL p : set_mset M. prime p) & n = (PROD i::nat:#M. i)"
-    by blast
+    then show ?thesis ..
+  qed
 qed
 
 lemma multiset_prime_factorization_unique_aux:
   fixes a :: nat
-  assumes "(ALL p : set_mset M. prime p)" and
-    "(ALL p : set_mset N. prime p)" and
-    "(PROD i :# M. i) dvd (PROD i:# N. i)"
-  shows
-    "count M a <= count N a"
-proof cases
-  assume M: "a : set_mset M"
-  with assms have a: "prime a" by auto
-  with M have "a ^ count M a dvd (PROD i :# M. i)"
+  assumes "\<forall>p\<in>set_mset M. prime p"
+    and "\<forall>p\<in>set_mset N. prime p"
+    and "(\<Prod>i \<in># M. i) dvd (\<Prod>i \<in># N. i)"
+  shows "count M a \<le> count N a"
+proof (cases "a \<in> set_mset M")
+  case True
+  with assms have a: "prime a"
+    by auto
+  with True have "a ^ count M a dvd (\<Prod>i \<in># M. i)"
     by (auto simp add: msetprod_multiplicity)
-  also have "... dvd (PROD i :# N. i)" by (rule assms)
-  also have "... = (PROD i : (set_mset N). i ^ (count N i))"
+  also have "\<dots> dvd (\<Prod>i \<in># N. i)"
+    by (rule assms)
+  also have "\<dots> = (\<Prod>i \<in> set_mset N. i ^ count N i)"
     by (simp add: msetprod_multiplicity)
-  also have "... = a^(count N a) * (PROD i : (set_mset N - {a}). i ^ (count N i))"
-  proof (cases)
-    assume "a : set_mset N"
-    then have b: "set_mset N = {a} Un (set_mset N - {a})"
+  also have "\<dots> = a ^ count N a * (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)"
+  proof (cases "a \<in> set_mset N")
+    case True
+    then have b: "set_mset N = {a} \<union> (set_mset N - {a})"
       by auto
     then show ?thesis
       by (subst (1) b, subst setprod.union_disjoint, auto)
   next
-    assume "a ~: set_mset N" 
-    then show ?thesis by auto
+    case False
+    then show ?thesis
+      by auto
   qed
-  finally have "a ^ count M a dvd 
-      a^(count N a) * (PROD i : (set_mset N - {a}). i ^ (count N i))".
+  finally have "a ^ count M a dvd a ^ count N a * (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)" .
   moreover
-  have "coprime (a ^ count M a) (PROD i : (set_mset N - {a}). i ^ (count N i))"
+  have "coprime (a ^ count M a) (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)"
     apply (subst gcd_commute_nat)
     apply (rule setprod_coprime_nat)
     apply (rule primes_imp_powers_coprime_nat)
-    using assms M
+    using assms True
     apply auto
     done
-  ultimately have "a ^ count M a dvd a^(count N a)"
+  ultimately have "a ^ count M a dvd a ^ count N a"
     by (elim coprime_dvd_mult_nat)
-  with a show ?thesis 
+  with a show ?thesis
     apply (intro power_dvd_imp_le)
     apply auto
     done
 next
-  assume "a ~: set_mset M"
-  then show ?thesis by auto
+  case False
+  then show ?thesis
+    by auto
 qed
 
 lemma multiset_prime_factorization_unique:
-  assumes "(ALL (p::nat) : set_mset M. prime p)" and
-    "(ALL p : set_mset N. prime p)" and
-    "(PROD i :# M. i) = (PROD i:# N. i)"
-  shows
-    "M = N"
+  assumes "\<forall>p::nat \<in> set_mset M. prime p"
+    and "\<forall>p \<in> set_mset N. prime p"
+    and "(\<Prod>i \<in># M. i) = (\<Prod>i \<in># N. i)"
+  shows "M = N"
 proof -
-  {
-    fix a
-    from assms have "count M a <= count N a"
-      by (intro multiset_prime_factorization_unique_aux, auto) 
-    moreover from assms have "count N a <= count M a"
-      by (intro multiset_prime_factorization_unique_aux, auto) 
-    ultimately have "count M a = count N a"
+  have "count M a = count N a" for a
+  proof -
+    from assms have "count M a \<le> count N a"
+      by (intro multiset_prime_factorization_unique_aux, auto)
+    moreover from assms have "count N a \<le> count M a"
+      by (intro multiset_prime_factorization_unique_aux, auto)
+    ultimately show ?thesis
       by auto
-  }
-  then show ?thesis by (simp add:multiset_eq_iff)
+  qed
+  then show ?thesis
+    by (simp add: multiset_eq_iff)
 qed
 
-definition multiset_prime_factorization :: "nat => nat multiset"
+definition multiset_prime_factorization :: "nat \<Rightarrow> nat multiset"
 where
-  "multiset_prime_factorization n ==
-     if n > 0 then (THE M. ((ALL p : set_mset M. prime p) & 
-       n = (PROD i :# M. i)))
-     else {#}"
+  "multiset_prime_factorization n =
+    (if n > 0
+     then THE M. (\<forall>p \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i)
+     else {#})"
 
-lemma multiset_prime_factorization: "n > 0 ==>
-    (ALL p : set_mset (multiset_prime_factorization n). prime p) &
-       n = (PROD i :# (multiset_prime_factorization n). i)"
+lemma multiset_prime_factorization: "n > 0 \<Longrightarrow>
+    (\<forall>p \<in> set_mset (multiset_prime_factorization n). prime p) \<and>
+       n = (\<Prod>i \<in># (multiset_prime_factorization n). i)"
   apply (unfold multiset_prime_factorization_def)
   apply clarsimp
   apply (frule multiset_prime_factorization_exists)
@@ -151,17 +152,16 @@
   apply (rule theI)
   apply (insert multiset_prime_factorization_unique)
   apply auto
-done
+  done
 
 
-subsection \<open>Prime factors and multiplicity for nats and ints\<close>
+subsection \<open>Prime factors and multiplicity for nat and int\<close>
 
 class unique_factorization =
   fixes multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat"
     and prime_factors :: "'a \<Rightarrow> 'a set"
 
-(* definitions for the natural numbers *)
-
+text \<open>Definitions for the natural numbers.\<close>
 instantiation nat :: unique_factorization
 begin
 
@@ -175,8 +175,7 @@
 
 end
 
-(* definitions for the integers *)
-
+text \<open>Definitions for the integers.\<close>
 instantiation int :: unique_factorization
 begin
 
@@ -200,96 +199,107 @@
   apply assumption
   done
 
-lemma transfer_nat_int_prime_factors_closure: "n >= 0 \<Longrightarrow> nat_set (prime_factors n)"
+lemma transfer_nat_int_prime_factors_closure: "n \<ge> 0 \<Longrightarrow> nat_set (prime_factors n)"
   by (auto simp add: nat_set_def prime_factors_int_def)
 
-lemma transfer_nat_int_multiplicity: "p >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
-    multiplicity (nat p) (nat n) = multiplicity p n"
+lemma transfer_nat_int_multiplicity:
+  "p \<ge> 0 \<Longrightarrow> n \<ge> 0 \<Longrightarrow> multiplicity (nat p) (nat n) = multiplicity p n"
   by (auto simp add: multiplicity_int_def)
 
-declare transfer_morphism_nat_int[transfer add return: 
+declare transfer_morphism_nat_int[transfer add return:
   transfer_nat_int_prime_factors transfer_nat_int_prime_factors_closure
   transfer_nat_int_multiplicity]
 
-
 lemma transfer_int_nat_prime_factors: "prime_factors (int n) = int ` prime_factors n"
   unfolding prime_factors_int_def by auto
 
-lemma transfer_int_nat_prime_factors_closure: "is_nat n \<Longrightarrow> 
-    nat_set (prime_factors n)"
+lemma transfer_int_nat_prime_factors_closure: "is_nat n \<Longrightarrow> nat_set (prime_factors n)"
   by (simp only: transfer_nat_int_prime_factors_closure is_nat_def)
 
-lemma transfer_int_nat_multiplicity: 
-    "multiplicity (int p) (int n) = multiplicity p n"
+lemma transfer_int_nat_multiplicity: "multiplicity (int p) (int n) = multiplicity p n"
   by (auto simp add: multiplicity_int_def)
 
-declare transfer_morphism_int_nat[transfer add return: 
+declare transfer_morphism_int_nat[transfer add return:
   transfer_int_nat_prime_factors transfer_int_nat_prime_factors_closure
   transfer_int_nat_multiplicity]
 
 
-subsection \<open>Properties of prime factors and multiplicity for nats and ints\<close>
+subsection \<open>Properties of prime factors and multiplicity for nat and int\<close>
 
-lemma prime_factors_ge_0_int [elim]: "p : prime_factors (n::int) \<Longrightarrow> p >= 0"
+lemma prime_factors_ge_0_int [elim]:
+  fixes n :: int
+  shows "p \<in> prime_factors n \<Longrightarrow> p \<ge> 0"
   unfolding prime_factors_int_def by auto
 
-lemma prime_factors_prime_nat [intro]: "p : prime_factors (n::nat) \<Longrightarrow> prime p"
+lemma prime_factors_prime_nat [intro]:
+  fixes n :: nat
+  shows "p \<in> prime_factors n \<Longrightarrow> prime p"
   apply (cases "n = 0")
   apply (simp add: prime_factors_nat_def multiset_prime_factorization_def)
   apply (auto simp add: prime_factors_nat_def multiset_prime_factorization)
   done
 
 lemma prime_factors_prime_int [intro]:
-  assumes "n >= 0" and "p : prime_factors (n::int)"
+  fixes n :: int
+  assumes "n \<ge> 0" and "p \<in> prime_factors n"
   shows "prime p"
   apply (rule prime_factors_prime_nat [transferred, of n p, simplified])
   using assms apply auto
   done
 
-lemma prime_factors_gt_0_nat [elim]: "p : prime_factors x \<Longrightarrow> p > (0::nat)"
-  apply (frule prime_factors_prime_nat)
-  apply auto
-  done
+lemma prime_factors_gt_0_nat [elim]:
+  fixes p :: nat
+  shows "p \<in> prime_factors x \<Longrightarrow> p > 0"
+  by (auto dest!: prime_factors_prime_nat)
 
-lemma prime_factors_gt_0_int [elim]: "x >= 0 \<Longrightarrow> p : prime_factors x \<Longrightarrow> 
-    int p > (0::int)"
-  apply auto
-  done
+lemma prime_factors_gt_0_int [elim]:
+  shows "x \<ge> 0 \<Longrightarrow> p \<in> prime_factors x \<Longrightarrow> int p > (0::int)"
+  by auto
 
-lemma prime_factors_finite_nat [iff]: "finite (prime_factors (n::nat))"
+lemma prime_factors_finite_nat [iff]:
+  fixes n :: nat
+  shows "finite (prime_factors n)"
   unfolding prime_factors_nat_def by auto
 
-lemma prime_factors_finite_int [iff]: "finite (prime_factors (n::int))"
+lemma prime_factors_finite_int [iff]:
+  fixes n :: int
+  shows "finite (prime_factors n)"
   unfolding prime_factors_int_def by auto
 
-lemma prime_factors_altdef_nat: "prime_factors (n::nat) = 
-    {p. multiplicity p n > 0}"
+lemma prime_factors_altdef_nat:
+  fixes n :: nat
+  shows "prime_factors n = {p. multiplicity p n > 0}"
   by (force simp add: prime_factors_nat_def multiplicity_nat_def)
 
-lemma prime_factors_altdef_int: "prime_factors (n::int) = 
-    {p. p >= 0 & multiplicity p n > 0}"
+lemma prime_factors_altdef_int:
+  fixes n :: int
+  shows "prime_factors n = {p. p \<ge> 0 \<and> multiplicity p n > 0}"
   apply (unfold prime_factors_int_def multiplicity_int_def)
   apply (subst prime_factors_altdef_nat)
   apply (auto simp add: image_def)
   done
 
-lemma prime_factorization_nat: "(n::nat) > 0 \<Longrightarrow> 
-    n = (PROD p : prime_factors n. p^(multiplicity p n))"
+lemma prime_factorization_nat:
+  fixes n :: nat
+  shows "n > 0 \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
   apply (frule multiset_prime_factorization)
   apply (simp add: prime_factors_nat_def multiplicity_nat_def msetprod_multiplicity)
   done
 
-lemma prime_factorization_int: 
-  assumes "(n::int) > 0"
-  shows "n = (PROD p : prime_factors n. p^(multiplicity p n))"
+lemma prime_factorization_int:
+  fixes n :: int
+  assumes "n > 0"
+  shows "n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
   apply (rule prime_factorization_nat [transferred, of n])
   using assms apply auto
   done
 
-lemma prime_factorization_unique_nat: 
+lemma prime_factorization_unique_nat:
   fixes f :: "nat \<Rightarrow> _"
-  assumes S_eq: "S = {p. 0 < f p}" and "finite S"
-    and "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)"
+  assumes S_eq: "S = {p. 0 < f p}"
+    and "finite S"
+    and "\<forall>p\<in>S. prime p"
+    and "n = (\<Prod>p\<in>S. p ^ f p)"
   shows "S = prime_factors n \<and> (\<forall>p. f p = multiplicity p n)"
 proof -
   from assms have "f \<in> multiset"
@@ -305,8 +315,7 @@
     apply force
     apply force
     apply force
-    using assms
-    apply (simp add: set_mset_def msetprod_multiplicity)
+    using assms apply (simp add: set_mset_def msetprod_multiplicity)
     done
   with \<open>f \<in> multiset\<close> have "count (multiset_prime_factorization n) = f"
     by simp
@@ -314,49 +323,40 @@
     by (simp add: set_mset_def multiset_def prime_factors_nat_def multiplicity_nat_def)
 qed
 
-lemma prime_factors_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow> 
-    finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
-      prime_factors n = S"
-  apply (rule prime_factorization_unique_nat [THEN conjunct1, symmetric])
-  apply assumption+
-  done
+lemma prime_factors_characterization_nat:
+  "S = {p. 0 < f (p::nat)} \<Longrightarrow>
+    finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
+  by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric])
 
-lemma prime_factors_characterization'_nat: 
+lemma prime_factors_characterization'_nat:
   "finite {p. 0 < f (p::nat)} \<Longrightarrow>
-    (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
-      prime_factors (PROD p | 0 < f p . p ^ f p) = {p. 0 < f p}"
-  apply (rule prime_factors_characterization_nat)
-  apply auto
-  done
+    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
+      prime_factors (\<Prod>p | 0 < f p. p ^ f p) = {p. 0 < f p}"
+  by (rule prime_factors_characterization_nat) auto
 
 (* A minor glitch:*)
-
-thm prime_factors_characterization'_nat 
-    [where f = "%x. f (int (x::nat))", 
-      transferred direction: nat "op <= (0::int)", rule_format]
+thm prime_factors_characterization'_nat
+    [where f = "\<lambda>x. f (int (x::nat))",
+      transferred direction: nat "op \<le> (0::int)", rule_format]
 
 (*
-  Transfer isn't smart enough to know that the "0 < f p" should 
-  remain a comparison between nats. But the transfer still works. 
+  Transfer isn't smart enough to know that the "0 < f p" should
+  remain a comparison between nats. But the transfer still works.
 *)
 
-lemma primes_characterization'_int [rule_format]: 
-    "finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow>
-      (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
-        prime_factors (PROD p | p >=0 & 0 < f p . p ^ f p) = 
-          {p. p >= 0 & 0 < f p}"
+lemma primes_characterization'_int [rule_format]:
+  "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow> \<forall>p. 0 < f p \<longrightarrow> prime p \<Longrightarrow>
+      prime_factors (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = {p. p \<ge> 0 \<and> 0 < f p}"
+  using prime_factors_characterization'_nat
+    [where f = "\<lambda>x. f (int (x::nat))",
+    transferred direction: nat "op \<le> (0::int)"]
+  by auto
 
-  apply (insert prime_factors_characterization'_nat 
-    [where f = "%x. f (int (x::nat))", 
-    transferred direction: nat "op <= (0::int)"])
-  apply auto
-  done
-
-lemma prime_factors_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> 
-    finite S \<Longrightarrow> (ALL p:S. prime (nat p)) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
-      prime_factors n = S"
+lemma prime_factors_characterization_int:
+  "S = {p. 0 < f (p::int)} \<Longrightarrow> finite S \<Longrightarrow>
+    \<forall>p\<in>S. prime (nat p) \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
   apply simp
-  apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}")
+  apply (subgoal_tac "{p. 0 < f p} = {p. 0 \<le> p \<and> 0 < f p}")
   apply (simp only:)
   apply (subst primes_characterization'_int)
   apply auto
@@ -364,36 +364,36 @@
   apply (metis le_cases nat_le_0 zero_not_prime_nat)
   done
 
-lemma multiplicity_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow> 
-    finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
-      multiplicity p n = f p"
+lemma multiplicity_characterization_nat:
+  "S = {p. 0 < f (p::nat)} \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow>
+    n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
   apply (frule prime_factorization_unique_nat [THEN conjunct2, rule_format, symmetric])
   apply auto
   done
 
 lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
-    (ALL p. 0 < f p \<longrightarrow> prime p) \<longrightarrow>
-      multiplicity p (PROD p | 0 < f p . p ^ f p) = f p"
+    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<longrightarrow>
+      multiplicity p (\<Prod>p | 0 < f p. p ^ f p) = f p"
   apply (intro impI)
   apply (rule multiplicity_characterization_nat)
   apply auto
   done
 
-lemma multiplicity_characterization'_int [rule_format]: 
-  "finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow>
-    (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> p >= 0 \<Longrightarrow>
-      multiplicity p (PROD p | p >= 0 & 0 < f p . p ^ f p) = f p"
-  apply (insert multiplicity_characterization'_nat 
-    [where f = "%x. f (int (x::nat))", 
-      transferred direction: nat "op <= (0::int)", rule_format])
+lemma multiplicity_characterization'_int [rule_format]:
+  "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow>
+    (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> p \<ge> 0 \<Longrightarrow>
+      multiplicity p (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = f p"
+  apply (insert multiplicity_characterization'_nat
+    [where f = "\<lambda>x. f (int (x::nat))",
+      transferred direction: nat "op \<le> (0::int)", rule_format])
   apply auto
   done
 
-lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> 
-    finite S \<Longrightarrow> (ALL p:S. prime (nat p)) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
-      p >= 0 \<Longrightarrow> multiplicity p n = f p"
+lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
+    finite S \<Longrightarrow> \<forall>p\<in>S. prime (nat p) \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow>
+      p \<ge> 0 \<Longrightarrow> multiplicity p n = f p"
   apply simp
-  apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}")
+  apply (subgoal_tac "{p. 0 < f p} = {p. 0 \<le> p \<and> 0 < f p}")
   apply (simp only:)
   apply (subst multiplicity_characterization'_int)
   apply auto
@@ -405,10 +405,10 @@
   by (simp add: multiplicity_nat_def multiset_prime_factorization_def)
 
 lemma multiplicity_zero_int [simp]: "multiplicity (p::int) 0 = 0"
-  by (simp add: multiplicity_int_def) 
+  by (simp add: multiplicity_int_def)
 
 lemma multiplicity_one_nat': "multiplicity p (1::nat) = 0"
-  by (subst multiplicity_characterization_nat [where f = "%x. 0"], auto)
+  by (subst multiplicity_characterization_nat [where f = "\<lambda>x. 0"], auto)
 
 lemma multiplicity_one_nat [simp]: "multiplicity p (Suc 0) = 0"
   by (metis One_nat_def multiplicity_one_nat')
@@ -417,99 +417,101 @@
   by (metis multiplicity_int_def multiplicity_one_nat' transfer_nat_int_numerals(2))
 
 lemma multiplicity_prime_nat [simp]: "prime p \<Longrightarrow> multiplicity p p = 1"
-  apply (subst multiplicity_characterization_nat [where f = "(%q. if q = p then 1 else 0)"])
+  apply (subst multiplicity_characterization_nat [where f = "\<lambda>q. if q = p then 1 else 0"])
   apply auto
-  by (metis (full_types) less_not_refl)
+  apply (metis (full_types) less_not_refl)
+  done
 
-lemma multiplicity_prime_power_nat [simp]: "prime p \<Longrightarrow> multiplicity p (p^n) = n"
+lemma multiplicity_prime_power_nat [simp]: "prime p \<Longrightarrow> multiplicity p (p ^ n) = n"
   apply (cases "n = 0")
   apply auto
-  apply (subst multiplicity_characterization_nat [where f = "(%q. if q = p then n else 0)"])
+  apply (subst multiplicity_characterization_nat [where f = "\<lambda>q. if q = p then n else 0"])
   apply auto
-  by (metis (full_types) less_not_refl)
+  apply (metis (full_types) less_not_refl)
+  done
 
-lemma multiplicity_prime_power_int [simp]: "prime p \<Longrightarrow> multiplicity p ( (int p)^n) = n"
+lemma multiplicity_prime_power_int [simp]: "prime p \<Longrightarrow> multiplicity p (int p ^ n) = n"
   by (metis multiplicity_prime_power_nat of_nat_power transfer_int_nat_multiplicity)
 
-lemma multiplicity_nonprime_nat [simp]: "~ prime (p::nat) \<Longrightarrow> multiplicity p n = 0"
+lemma multiplicity_nonprime_nat [simp]:
+  fixes p n :: nat
+  shows "\<not> prime p \<Longrightarrow> multiplicity p n = 0"
   apply (cases "n = 0")
   apply auto
   apply (frule multiset_prime_factorization)
   apply (auto simp add: set_mset_def multiplicity_nat_def)
   done
 
-lemma multiplicity_not_factor_nat [simp]: 
-    "p ~: prime_factors (n::nat) \<Longrightarrow> multiplicity p n = 0"
+lemma multiplicity_not_factor_nat [simp]:
+  fixes p n :: nat
+  shows "p \<notin> prime_factors n \<Longrightarrow> multiplicity p n = 0"
   apply (subst (asm) prime_factors_altdef_nat)
   apply auto
   done
 
-lemma multiplicity_not_factor_int [simp]: 
-    "p >= 0 \<Longrightarrow> p ~: prime_factors (n::int) \<Longrightarrow> multiplicity p n = 0"
+lemma multiplicity_not_factor_int [simp]:
+  fixes n :: int
+  shows "p \<ge> 0 \<Longrightarrow> p \<notin> prime_factors n \<Longrightarrow> multiplicity p n = 0"
   apply (subst (asm) prime_factors_altdef_int)
   apply auto
   done
 
 (*FIXME: messy*)
 lemma multiplicity_product_aux_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow>
-    (prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
-    (ALL p. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
+    (prime_factors k) \<union> (prime_factors l) = prime_factors (k * l) \<and>
+    (\<forall>p. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
   apply (rule prime_factorization_unique_nat)
   apply (simp only: prime_factors_altdef_nat)
   apply auto
   apply (subst power_add)
   apply (subst setprod.distrib)
   apply (rule arg_cong2 [where f = "\<lambda>x y. x*y"])
-  apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors k Un 
+  apply (subgoal_tac "prime_factors k \<union> prime_factors l = prime_factors k \<union>
       (prime_factors l - prime_factors k)")
   apply (erule ssubst)
   apply (subst setprod.union_disjoint)
   apply auto
   apply (metis One_nat_def nat_mult_1_right prime_factorization_nat setprod.neutral_const)
-  apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors l Un 
+  apply (subgoal_tac "prime_factors k \<union> prime_factors l = prime_factors l \<union>
       (prime_factors k - prime_factors l)")
   apply (erule ssubst)
   apply (subst setprod.union_disjoint)
   apply auto
-  apply (subgoal_tac "(\<Prod>p\<in>prime_factors k - prime_factors l. p ^ multiplicity p l) = 
+  apply (subgoal_tac "(\<Prod>p\<in>prime_factors k - prime_factors l. p ^ multiplicity p l) =
       (\<Prod>p\<in>prime_factors k - prime_factors l. 1)")
   apply auto
   apply (metis One_nat_def nat_mult_1_right prime_factorization_nat setprod.neutral_const)
   done
 
-(* transfer doesn't have the same problem here with the right 
+(* transfer doesn't have the same problem here with the right
    choice of rules. *)
 
-lemma multiplicity_product_aux_int: 
+lemma multiplicity_product_aux_int:
   assumes "(k::int) > 0" and "l > 0"
-  shows 
-    "(prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
-    (ALL p >= 0. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
+  shows "prime_factors k \<union> prime_factors l = prime_factors (k * l) \<and>
+    (\<forall>p \<ge> 0. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
   apply (rule multiplicity_product_aux_nat [transferred, of l k])
   using assms apply auto
   done
 
-lemma prime_factors_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) = 
-    prime_factors k Un prime_factors l"
+lemma prime_factors_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) =
+    prime_factors k \<union> prime_factors l"
   by (rule multiplicity_product_aux_nat [THEN conjunct1, symmetric])
 
-lemma prime_factors_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) = 
-    prime_factors k Un prime_factors l"
+lemma prime_factors_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) =
+    prime_factors k \<union> prime_factors l"
   by (rule multiplicity_product_aux_int [THEN conjunct1, symmetric])
 
-lemma multiplicity_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> multiplicity p (k * l) = 
+lemma multiplicity_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> multiplicity p (k * l) =
     multiplicity p k + multiplicity p l"
-  by (rule multiplicity_product_aux_nat [THEN conjunct2, rule_format, 
-      symmetric])
+  by (rule multiplicity_product_aux_nat [THEN conjunct2, rule_format, symmetric])
 
-lemma multiplicity_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> p >= 0 \<Longrightarrow> 
+lemma multiplicity_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> p \<ge> 0 \<Longrightarrow>
     multiplicity p (k * l) = multiplicity p k + multiplicity p l"
-  by (rule multiplicity_product_aux_int [THEN conjunct2, rule_format, 
-      symmetric])
+  by (rule multiplicity_product_aux_int [THEN conjunct2, rule_format, symmetric])
 
-lemma multiplicity_setprod_nat: "finite S \<Longrightarrow> (ALL x : S. f x > 0) \<Longrightarrow> 
-    multiplicity (p::nat) (PROD x : S. f x) = 
-      (SUM x : S. multiplicity p (f x))"
+lemma multiplicity_setprod_nat: "finite S \<Longrightarrow> \<forall>x\<in>S. f x > 0 \<Longrightarrow>
+    multiplicity (p::nat) (\<Prod>x \<in> S. f x) = (\<Sum>x \<in> S. multiplicity p (f x))"
   apply (induct set: finite)
   apply auto
   apply (subst multiplicity_product_nat)
@@ -517,33 +519,28 @@
   done
 
 (* Transfer is delicate here for two reasons: first, because there is
-   an implicit quantifier over functions (f), and, second, because the 
-   product over the multiplicity should not be translated to an integer 
+   an implicit quantifier over functions (f), and, second, because the
+   product over the multiplicity should not be translated to an integer
    product.
 
    The way to handle the first is to use quantifier rules for functions.
    The way to handle the second is to turn off the offending rule.
 *)
 
-lemma transfer_nat_int_sum_prod_closure3:
-  "(SUM x : A. int (f x)) >= 0"
-  "(PROD x : A. int (f x)) >= 0"
-  apply (rule setsum_nonneg, auto)
-  apply (rule setprod_nonneg, auto)
+lemma transfer_nat_int_sum_prod_closure3: "(\<Sum>x \<in> A. int (f x)) \<ge> 0" "(\<Prod>x \<in> A. int (f x)) \<ge> 0"
+  apply (rule setsum_nonneg; auto)
+  apply (rule setprod_nonneg; auto)
   done
 
-declare transfer_morphism_nat_int[transfer 
+declare transfer_morphism_nat_int[transfer
   add return: transfer_nat_int_sum_prod_closure3
   del: transfer_nat_int_sum_prod2 (1)]
 
-lemma multiplicity_setprod_int: "p >= 0 \<Longrightarrow> finite S \<Longrightarrow> 
-  (ALL x : S. f x > 0) \<Longrightarrow> 
-    multiplicity (p::int) (PROD x : S. f x) = 
-      (SUM x : S. multiplicity p (f x))"
-
+lemma multiplicity_setprod_int: "p \<ge> 0 \<Longrightarrow> finite S \<Longrightarrow> \<forall>x\<in>S. f x > 0 \<Longrightarrow>
+    multiplicity (p::int) (\<Prod>x \<in> S. f x) = (\<Sum>x \<in> S. multiplicity p (f x))"
   apply (frule multiplicity_setprod_nat
-    [where f = "%x. nat(int(nat(f x)))", 
-      transferred direction: nat "op <= (0::int)"])
+    [where f = "\<lambda>x. nat(int(nat(f x)))",
+      transferred direction: nat "op \<le> (0::int)"])
   apply auto
   apply (subst (asm) setprod.cong)
   apply (rule refl)
@@ -553,14 +550,13 @@
   apply auto
   done
 
-declare transfer_morphism_nat_int[transfer 
+declare transfer_morphism_nat_int[transfer
   add return: transfer_nat_int_sum_prod2 (1)]
 
 lemma multiplicity_prod_prime_powers_nat:
-    "finite S \<Longrightarrow> (ALL p : S. prime (p::nat)) \<Longrightarrow>
-       multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)"
-  apply (subgoal_tac "(PROD p : S. p ^ f p) = 
-      (PROD p : S. p ^ (%x. if x : S then f x else 0) p)")
+    "finite S \<Longrightarrow> \<forall>p\<in>S. prime (p::nat) \<Longrightarrow>
+       multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)"
+  apply (subgoal_tac "(\<Prod>p \<in> S. p ^ f p) = (\<Prod>p \<in> S. p ^ (\<lambda>x. if x \<in> S then f x else 0) p)")
   apply (erule ssubst)
   apply (subst multiplicity_characterization_nat)
   prefer 5 apply (rule refl)
@@ -572,43 +568,43 @@
   apply (rule setprod.cong)
   apply (rule refl)
   apply auto
-done
+  done
 
 (* Here the issue with transfer is the implicit quantifier over S *)
 
 lemma multiplicity_prod_prime_powers_int:
-    "(p::int) >= 0 \<Longrightarrow> finite S \<Longrightarrow> (ALL p:S. prime (nat p)) \<Longrightarrow>
-       multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)"
+    "(p::int) \<ge> 0 \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime (nat p) \<Longrightarrow>
+       multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)"
   apply (subgoal_tac "int ` nat ` S = S")
-  apply (frule multiplicity_prod_prime_powers_nat [where f = "%x. f(int x)" 
-    and S = "nat ` S", transferred])
+  apply (frule multiplicity_prod_prime_powers_nat
+    [where f = "\<lambda>x. f(int x)" and S = "nat ` S", transferred])
   apply auto
   apply (metis linear nat_0_iff zero_not_prime_nat)
   apply (metis (full_types) image_iff int_nat_eq less_le less_linear nat_0_iff zero_not_prime_nat)
   done
 
-lemma multiplicity_distinct_prime_power_nat: "prime p \<Longrightarrow> prime q \<Longrightarrow>
-    p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
-  apply (subgoal_tac "q^n = setprod (%x. x^n) {q}")
+lemma multiplicity_distinct_prime_power_nat:
+    "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0"
+  apply (subgoal_tac "q ^ n = setprod (\<lambda>x. x ^ n) {q}")
   apply (erule ssubst)
   apply (subst multiplicity_prod_prime_powers_nat)
   apply auto
   done
 
-lemma multiplicity_distinct_prime_power_int: "prime p \<Longrightarrow> prime q \<Longrightarrow>
-    p ~= q \<Longrightarrow> multiplicity p (int q ^ n) = 0"
+lemma multiplicity_distinct_prime_power_int:
+    "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (int q ^ n) = 0"
   by (metis multiplicity_distinct_prime_power_nat of_nat_power transfer_int_nat_multiplicity)
 
-
 lemma dvd_multiplicity_nat:
-    "(0::nat) < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x <= multiplicity p y"
+  fixes x y :: nat
+  shows "0 < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x \<le> multiplicity p y"
   apply (cases "x = 0")
   apply (auto simp add: dvd_def multiplicity_product_nat)
   done
 
-lemma dvd_multiplicity_int: 
-    "(0::int) < y \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> p >= 0 \<Longrightarrow> 
-      multiplicity p x <= multiplicity p y"
+lemma dvd_multiplicity_int:
+  fixes p x y :: int
+  shows "0 < y \<Longrightarrow> 0 \<le> x \<Longrightarrow> x dvd y \<Longrightarrow> p \<ge> 0 \<Longrightarrow> multiplicity p x \<le> multiplicity p y"
   apply (cases "x = 0")
   apply (auto simp add: dvd_def)
   apply (subgoal_tac "0 < k")
@@ -618,20 +614,23 @@
   done
 
 lemma dvd_prime_factors_nat [intro]:
-    "0 < (y::nat) \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
+  fixes x y :: nat
+  shows "0 < y \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x \<le> prime_factors y"
   apply (simp only: prime_factors_altdef_nat)
   apply auto
   apply (metis dvd_multiplicity_nat le_0_eq neq0_conv)
   done
 
 lemma dvd_prime_factors_int [intro]:
-    "0 < (y::int) \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
+  fixes x y :: int
+  shows "0 < y \<Longrightarrow> 0 \<le> x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x \<le> prime_factors y"
   apply (auto simp add: prime_factors_altdef_int)
   apply (metis dvd_multiplicity_int le_0_eq neq0_conv)
   done
 
-lemma multiplicity_dvd_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow> 
-    ALL p. multiplicity p x <= multiplicity p y \<Longrightarrow> x dvd y"
+lemma multiplicity_dvd_nat:
+  fixes x y :: nat
+  shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> \<forall>p. multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
   apply (subst prime_factorization_nat [of x], assumption)
   apply (subst prime_factorization_nat [of y], assumption)
   apply (rule setprod_dvd_setprod_subset2)
@@ -642,8 +641,9 @@
   apply (metis le_imp_power_dvd)
   done
 
-lemma multiplicity_dvd_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow> 
-    ALL p >= 0. multiplicity p x <= multiplicity p y \<Longrightarrow> x dvd y"
+lemma multiplicity_dvd_int:
+  fixes x y :: int
+  shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> \<forall>p\<ge>0. multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
   apply (subst prime_factorization_int [of x], assumption)
   apply (subst prime_factorization_int [of y], assumption)
   apply (rule setprod_dvd_setprod_subset2)
@@ -653,155 +653,171 @@
   apply (metis le_imp_power_dvd prime_factors_ge_0_int)
   done
 
-lemma multiplicity_dvd'_nat: "(0::nat) < x \<Longrightarrow> 
-    \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
+lemma multiplicity_dvd'_nat:
+  fixes x y :: nat
+  shows "0 < x \<Longrightarrow> \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
   by (metis gcd_lcm_complete_lattice_nat.top_greatest le_refl multiplicity_dvd_nat
       multiplicity_nonprime_nat neq0_conv)
 
-lemma multiplicity_dvd'_int: 
-  fixes x::int and y::int
-  shows "0 < x \<Longrightarrow> 0 <= y \<Longrightarrow>
+lemma multiplicity_dvd'_int:
+  fixes x y :: int
+  shows "0 < x \<Longrightarrow> 0 \<le> y \<Longrightarrow>
     \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
-by (metis GCD.dvd_int_iff abs_int_eq multiplicity_dvd'_nat multiplicity_int_def nat_int 
-          zero_le_imp_eq_int zero_less_imp_eq_int)
+  by (metis GCD.dvd_int_iff abs_int_eq multiplicity_dvd'_nat multiplicity_int_def nat_int
+    zero_le_imp_eq_int zero_less_imp_eq_int)
 
-lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
-    (x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
+lemma dvd_multiplicity_eq_nat:
+  fixes x y :: nat
+  shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> x dvd y \<longleftrightarrow> (\<forall>p. multiplicity p x \<le> multiplicity p y)"
   by (auto intro: dvd_multiplicity_nat multiplicity_dvd_nat)
 
 lemma dvd_multiplicity_eq_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow>
-    (x dvd y) = (ALL p >= 0. multiplicity p x <= multiplicity p y)"
+    (x dvd y) = (\<forall>p\<ge>0. multiplicity p x \<le> multiplicity p y)"
   by (auto intro: dvd_multiplicity_int multiplicity_dvd_int)
 
-lemma prime_factors_altdef2_nat: "(n::nat) > 0 \<Longrightarrow> 
-    (p : prime_factors n) = (prime p & p dvd n)"
+lemma prime_factors_altdef2_nat:
+  fixes n :: nat
+  shows "n > 0 \<Longrightarrow> p \<in> prime_factors n \<longleftrightarrow> prime p \<and> p dvd n"
   apply (cases "prime p")
   apply auto
   apply (subst prime_factorization_nat [where n = n], assumption)
-  apply (rule dvd_trans) 
+  apply (rule dvd_trans)
   apply (rule dvd_power [where x = p and n = "multiplicity p n"])
   apply (subst (asm) prime_factors_altdef_nat, force)
   apply rule
   apply auto
-  apply (metis One_nat_def Zero_not_Suc dvd_multiplicity_nat le0 le_antisym multiplicity_not_factor_nat multiplicity_prime_nat)  
+  apply (metis One_nat_def Zero_not_Suc dvd_multiplicity_nat le0
+    le_antisym multiplicity_not_factor_nat multiplicity_prime_nat)
   done
 
-lemma prime_factors_altdef2_int: 
-  assumes "(n::int) > 0" 
-  shows "(p : prime_factors n) = (prime p & p dvd n)"
-using assms by (simp add:  prime_factors_altdef2_nat [transferred])
+lemma prime_factors_altdef2_int:
+  fixes n :: int
+  assumes "n > 0"
+  shows "p \<in> prime_factors n \<longleftrightarrow> prime p \<and> p dvd n"
+  using assms by (simp add:  prime_factors_altdef2_nat [transferred])
 
 lemma multiplicity_eq_nat:
-  fixes x and y::nat 
-  assumes [arith]: "x > 0" "y > 0" and
-    mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
+  fixes x and y::nat
+  assumes [arith]: "x > 0" "y > 0"
+    and mult_eq [simp]: "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
   shows "x = y"
   apply (rule dvd_antisym)
-  apply (auto intro: multiplicity_dvd'_nat) 
+  apply (auto intro: multiplicity_dvd'_nat)
   done
 
 lemma multiplicity_eq_int:
-  fixes x and y::int 
-  assumes [arith]: "x > 0" "y > 0" and
-    mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
+  fixes x y :: int
+  assumes [arith]: "x > 0" "y > 0"
+    and mult_eq [simp]: "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
   shows "x = y"
   apply (rule dvd_antisym [transferred])
-  apply (auto intro: multiplicity_dvd'_int) 
+  apply (auto intro: multiplicity_dvd'_int)
   done
 
 
 subsection \<open>An application\<close>
 
-lemma gcd_eq_nat: 
+lemma gcd_eq_nat:
+  fixes x y :: nat
   assumes pos [arith]: "x > 0" "y > 0"
-  shows "gcd (x::nat) y = 
-    (PROD p: prime_factors x Un prime_factors y. 
-      p ^ (min (multiplicity p x) (multiplicity p y)))"
+  shows "gcd x y =
+    (\<Prod>p \<in> prime_factors x \<union> prime_factors y. p ^ min (multiplicity p x) (multiplicity p y))"
+  (is "_ = ?z")
 proof -
-  def z == "(PROD p: prime_factors (x::nat) Un prime_factors y. 
-      p ^ (min (multiplicity p x) (multiplicity p y)))"
-  have [arith]: "z > 0"
-    unfolding z_def by (rule setprod_pos_nat, auto)
-  have aux: "!!p. prime p \<Longrightarrow> multiplicity p z = 
-      min (multiplicity p x) (multiplicity p y)"
-    unfolding z_def
+  have [arith]: "?z > 0"
+    by (rule setprod_pos_nat) auto
+  have aux: "\<And>p. prime p \<Longrightarrow> multiplicity p ?z = min (multiplicity p x) (multiplicity p y)"
     apply (subst multiplicity_prod_prime_powers_nat)
     apply auto
     done
-  have "z dvd x" 
-    by (intro multiplicity_dvd'_nat, auto simp add: aux)
-  moreover have "z dvd y" 
-    by (intro multiplicity_dvd'_nat, auto simp add: aux)
-  moreover have "ALL w. w dvd x & w dvd y \<longrightarrow> w dvd z"
-    apply auto
-    apply (case_tac "w = 0", auto)
-    apply (erule multiplicity_dvd'_nat)
-    apply (auto intro: dvd_multiplicity_nat simp add: aux)
-    done
-  ultimately have "z = gcd x y"
+  have "?z dvd x"
+    by (intro multiplicity_dvd'_nat) (auto simp add: aux)
+  moreover have "?z dvd y"
+    by (intro multiplicity_dvd'_nat) (auto simp add: aux)
+  moreover have "w dvd x \<and> w dvd y \<longrightarrow> w dvd ?z" for w
+  proof (cases "w = 0")
+    case True
+    then show ?thesis by simp
+  next
+    case False
+    then show ?thesis
+      apply auto
+      apply (erule multiplicity_dvd'_nat)
+      apply (auto intro: dvd_multiplicity_nat simp add: aux)
+      done
+  qed
+  ultimately have "?z = gcd x y"
     by (subst gcd_unique_nat [symmetric], blast)
   then show ?thesis
-    unfolding z_def by auto
+    by auto
 qed
 
-lemma lcm_eq_nat: 
+lemma lcm_eq_nat:
   assumes pos [arith]: "x > 0" "y > 0"
-  shows "lcm (x::nat) y = 
-    (PROD p: prime_factors x Un prime_factors y. 
-      p ^ (max (multiplicity p x) (multiplicity p y)))"
+  shows "lcm (x::nat) y =
+    (\<Prod>p \<in> prime_factors x \<union> prime_factors y. p ^ max (multiplicity p x) (multiplicity p y))"
+  (is "_ = ?z")
 proof -
-  def z == "(PROD p: prime_factors (x::nat) Un prime_factors y. 
-      p ^ (max (multiplicity p x) (multiplicity p y)))"
-  have [arith]: "z > 0"
-    unfolding z_def by (rule setprod_pos_nat, auto)
-  have aux: "!!p. prime p \<Longrightarrow> multiplicity p z = 
-      max (multiplicity p x) (multiplicity p y)"
-    unfolding z_def
+  have [arith]: "?z > 0"
+    by (rule setprod_pos_nat, auto)
+  have aux: "\<And>p. prime p \<Longrightarrow> multiplicity p ?z = max (multiplicity p x) (multiplicity p y)"
     apply (subst multiplicity_prod_prime_powers_nat)
     apply auto
     done
-  have "x dvd z" 
-    by (intro multiplicity_dvd'_nat, auto simp add: aux)
-  moreover have "y dvd z" 
-    by (intro multiplicity_dvd'_nat, auto simp add: aux)
-  moreover have "ALL w. x dvd w & y dvd w \<longrightarrow> z dvd w"
-    apply auto
-    apply (case_tac "w = 0", auto)
-    apply (rule multiplicity_dvd'_nat)
-    apply (auto intro: dvd_multiplicity_nat simp add: aux)
-    done
-  ultimately have "z = lcm x y"
+  have "x dvd ?z"
+    by (intro multiplicity_dvd'_nat) (auto simp add: aux)
+  moreover have "y dvd ?z"
+    by (intro multiplicity_dvd'_nat) (auto simp add: aux)
+  moreover have "x dvd w \<and> y dvd w \<longrightarrow> ?z dvd w" for w
+  proof (cases "w = 0")
+    case True
+    then show ?thesis by auto
+  next
+    case False
+    then show ?thesis
+      apply auto
+      apply (rule multiplicity_dvd'_nat)
+      apply (auto intro: dvd_multiplicity_nat simp add: aux)
+      done
+  qed
+  ultimately have "?z = lcm x y"
     by (subst lcm_unique_nat [symmetric], blast)
   then show ?thesis
-    unfolding z_def by auto
+    by auto
 qed
 
-lemma multiplicity_gcd_nat: 
+lemma multiplicity_gcd_nat:
+  fixes p x y :: nat
   assumes [arith]: "x > 0" "y > 0"
-  shows "multiplicity (p::nat) (gcd x y) = min (multiplicity p x) (multiplicity p y)"
+  shows "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)"
   apply (subst gcd_eq_nat)
   apply auto
   apply (subst multiplicity_prod_prime_powers_nat)
   apply auto
   done
 
-lemma multiplicity_lcm_nat: 
+lemma multiplicity_lcm_nat:
+  fixes p x y :: nat
   assumes [arith]: "x > 0" "y > 0"
-  shows "multiplicity (p::nat) (lcm x y) = max (multiplicity p x) (multiplicity p y)"
+  shows "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)"
   apply (subst lcm_eq_nat)
   apply auto
   apply (subst multiplicity_prod_prime_powers_nat)
   apply auto
   done
 
-lemma gcd_lcm_distrib_nat: "gcd (x::nat) (lcm y z) = lcm (gcd x y) (gcd x z)"
-  apply (cases "x = 0 | y = 0 | z = 0") 
+lemma gcd_lcm_distrib_nat:
+  fixes x y z :: nat
+  shows "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)"
+  apply (cases "x = 0 | y = 0 | z = 0")
   apply auto
   apply (rule multiplicity_eq_nat)
   apply (auto simp add: multiplicity_gcd_nat multiplicity_lcm_nat lcm_pos_nat)
   done
 
-lemma gcd_lcm_distrib_int: "gcd (x::int) (lcm y z) = lcm (gcd x y) (gcd x z)"
+lemma gcd_lcm_distrib_int:
+  fixes x y z :: int
+  shows "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)"
   apply (subst (1 2 3) gcd_abs_int)
   apply (subst lcm_abs_int)
   apply (subst (2) abs_of_nonneg)
@@ -811,4 +827,3 @@
   done
 
 end
-