
diff -r fbfdc5ac86be -r a98ef45122f3 src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Sat Sep 10 22:11:55 2011 +0200
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Sat Sep 10 23:27:32 2011 +0200
@@ -42,7 +42,7 @@
   apply auto
   apply (subst setsum_Un_disjoint)
   apply auto
-done
+  done
 
 lemma setprod_Un2: "finite (A Un B) \<Longrightarrow> 
     setprod f (A Un B) = setprod f (A - B) * setprod f (B - A) * 
@@ -53,7 +53,7 @@
   apply auto
   apply (subst setprod_Un_disjoint)
   apply auto
-done
+  done
  
 (* 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 
@@ -71,12 +71,10 @@
 translations
   "PROD i :# A. b" == "CONST msetprod (%i. b) A"
 
-lemma msetprod_empty:
-  "msetprod f {#} = 1"
+lemma msetprod_empty: "msetprod f {#} = 1"
   by (simp add: msetprod_def)
 
-lemma msetprod_singleton:
-  "msetprod f {#x#} = f x"
+lemma msetprod_singleton: "msetprod f {#x#} = f x"
   by (simp add: msetprod_def)
 
 lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B" 
@@ -105,7 +103,7 @@
   apply (auto intro: setprod_cong)
   apply (subst setprod_Un_disjoint [symmetric])
   apply (auto intro: setprod_cong)
-done
+  done
 
 
 subsection {* unique factorization: multiset version *}
@@ -119,27 +117,23 @@
   assume "(n::nat) > 0"
   then have "n = 1 | (n > 1 & prime n) | (n > 1 & ~ prime n)"
     by arith
-  moreover 
-  {
+  moreover {
     assume "n = 1"
     then have "(ALL p : set_of {#}. prime p) & n = (PROD i :# {#}. i)"
         by (auto simp add: msetprod_def)
-  } 
-  moreover 
-  {
+  } moreover {
     assume "n > 1" and "prime n"
     then have "(ALL p : set_of {# n #}. prime p) & n = (PROD i :# {# n #}. i)"
       by (auto simp add: msetprod_def)
-  } 
-  moreover 
-  {
+  } moreover {
     assume "n > 1" and "~ prime n"
-    with not_prime_eq_prod_nat obtain m k where n: "n = m * k & 1 < m & m < n & 1 < k & k < n"
-        by blast
+    with not_prime_eq_prod_nat
+    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_of Q. prime p) & m = (PROD i:#Q. i)"
         and "(ALL p: set_of R. prime p) & k = (PROD i:#R. i)"
       by blast
-    hence "(ALL p: set_of (Q + R). prime p) & n = (PROD i :# Q + R. i)"
+    then have "(ALL p: set_of (Q + R). prime p) & n = (PROD i :# Q + R. i)"
       by (auto simp add: n msetprod_Un)
     then have "EX M. (ALL p : set_of M. prime p) & n = (PROD i :# M. i)"..
   }
@@ -162,23 +156,21 @@
   also have "... dvd (PROD i :# N. i)" by (rule assms)
   also have "... = (PROD i : (set_of N). i ^ (count N i))"
     by (simp add: msetprod_def)
-  also have "... = 
-      a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))"
-    proof (cases)
-      assume "a : set_of N"
-      hence b: "set_of N = {a} Un (set_of N - {a})"
-        by auto
-      thus ?thesis
-        by (subst (1) b, subst setprod_Un_disjoint, auto)
-    next
-      assume "a ~: set_of N" 
-      thus ?thesis
-        by auto
-    qed
+  also have "... = a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))"
+  proof (cases)
+    assume "a : set_of N"
+    then have b: "set_of N = {a} Un (set_of N - {a})"
+      by auto
+    then show ?thesis
+      by (subst (1) b, subst setprod_Un_disjoint, auto)
+  next
+    assume "a ~: set_of N" 
+    then show ?thesis by auto
+  qed
   finally have "a ^ count M a dvd 
       a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))".
-  moreover have "coprime (a ^ count M a)
-      (PROD i : (set_of N - {a}). i ^ (count N i))"
+  moreover
+  have "coprime (a ^ count M a) (PROD i : (set_of N - {a}). i ^ (count N i))"
     apply (subst gcd_commute_nat)
     apply (rule setprod_coprime_nat)
     apply (rule primes_imp_powers_coprime_nat)
@@ -188,10 +180,12 @@
   ultimately have "a ^ count M a dvd a^(count N a)"
     by (elim coprime_dvd_mult_nat)
   with a show ?thesis 
-    by (intro power_dvd_imp_le, auto)
+    apply (intro power_dvd_imp_le)
+    apply auto
+    done
 next
   assume "a ~: set_of M"
-  thus ?thesis by auto
+  then show ?thesis by auto
 qed
 
 lemma multiset_prime_factorization_unique:
@@ -210,10 +204,11 @@
     ultimately have "count M a = count N a"
       by auto
   }
-  thus ?thesis by (simp add:multiset_eq_iff)
+  then show ?thesis by (simp add:multiset_eq_iff)
 qed
 
-definition multiset_prime_factorization :: "nat => nat multiset" where
+definition multiset_prime_factorization :: "nat => nat multiset"
+where
   "multiset_prime_factorization n ==
      if n > 0 then (THE M. ((ALL p : set_of M. prime p) & 
        n = (PROD i :# M. i)))
@@ -234,27 +229,21 @@
 subsection {* Prime factors and multiplicity for nats and ints *}
 
 class unique_factorization =
-
-fixes
-  multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat" and
-  prime_factors :: "'a \<Rightarrow> 'a set"
+  fixes multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat"
+    and prime_factors :: "'a \<Rightarrow> 'a set"
 
 (* definitions for the natural numbers *)
 
 instantiation nat :: unique_factorization
 begin
 
-definition
-  multiplicity_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-where
-  "multiplicity_nat p n = count (multiset_prime_factorization n) p"
+definition multiplicity_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+  where "multiplicity_nat p n = count (multiset_prime_factorization n) p"
 
-definition
-  prime_factors_nat :: "nat \<Rightarrow> nat set"
-where
-  "prime_factors_nat n = set_of (multiset_prime_factorization n)"
+definition prime_factors_nat :: "nat \<Rightarrow> nat set"
+  where "prime_factors_nat n = set_of (multiset_prime_factorization n)"
 
-instance proof qed
+instance ..
 
 end
 
@@ -263,34 +252,31 @@
 instantiation int :: unique_factorization
 begin
 
-definition
-  multiplicity_int :: "int \<Rightarrow> int \<Rightarrow> nat"
-where
-  "multiplicity_int p n = multiplicity (nat p) (nat n)"
+definition multiplicity_int :: "int \<Rightarrow> int \<Rightarrow> nat"
+  where "multiplicity_int p n = multiplicity (nat p) (nat n)"
 
-definition
-  prime_factors_int :: "int \<Rightarrow> int set"
-where
-  "prime_factors_int n = int ` (prime_factors (nat n))"
+definition prime_factors_int :: "int \<Rightarrow> int set"
+  where "prime_factors_int n = int ` (prime_factors (nat n))"
 
-instance proof qed
+instance ..
 
 end
 
 
 subsection {* Set up transfer *}
 
-lemma transfer_nat_int_prime_factors: 
-  "prime_factors (nat n) = nat ` prime_factors n"
-  unfolding prime_factors_int_def apply auto
-  by (subst transfer_int_nat_set_return_embed, assumption)
+lemma transfer_nat_int_prime_factors: "prime_factors (nat n) = nat ` prime_factors n"
+  unfolding prime_factors_int_def
+  apply auto
+  apply (subst transfer_int_nat_set_return_embed)
+  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 >= 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"
+    multiplicity (nat p) (nat n) = multiplicity p n"
   by (auto simp add: multiplicity_int_def)
 
 declare transfer_morphism_nat_int[transfer add return: 
@@ -298,8 +284,7 @@
   transfer_nat_int_multiplicity]
 
 
-lemma transfer_int_nat_prime_factors:
-    "prime_factors (int n) = int ` prime_factors n"
+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> 
@@ -318,10 +303,10 @@
 subsection {* Properties of prime factors and multiplicity for nats and ints *}
 
 lemma prime_factors_ge_0_int [elim]: "p : prime_factors (n::int) \<Longrightarrow> p >= 0"
-  by (unfold prime_factors_int_def, auto)
+  unfolding prime_factors_int_def by auto
 
 lemma prime_factors_prime_nat [intro]: "p : prime_factors (n::nat) \<Longrightarrow> prime p"
-  apply (case_tac "n = 0")
+  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
@@ -334,17 +319,21 @@
   done
 
 lemma prime_factors_gt_0_nat [elim]: "p : prime_factors x \<Longrightarrow> p > (0::nat)"
-  by (frule prime_factors_prime_nat, auto)
+  apply (frule prime_factors_prime_nat)
+  apply auto
+  done
 
 lemma prime_factors_gt_0_int [elim]: "x >= 0 \<Longrightarrow> p : prime_factors x \<Longrightarrow> 
     p > (0::int)"
-  by (frule (1) prime_factors_prime_int, auto)
+  apply (frule (1) prime_factors_prime_int)
+  apply auto
+  done
 
 lemma prime_factors_finite_nat [iff]: "finite (prime_factors (n::nat))"
-  by (unfold prime_factors_nat_def, auto)
+  unfolding prime_factors_nat_def by auto
 
 lemma prime_factors_finite_int [iff]: "finite (prime_factors (n::int))"
-  by (unfold prime_factors_int_def, auto)
+  unfolding prime_factors_int_def by auto
 
 lemma prime_factors_altdef_nat: "prime_factors (n::nat) = 
     {p. multiplicity p n > 0}"
@@ -359,8 +348,9 @@
 
 lemma prime_factorization_nat: "(n::nat) > 0 \<Longrightarrow> 
     n = (PROD p : prime_factors n. p^(multiplicity p n))"
-  by (frule multiset_prime_factorization, 
-    simp add: prime_factors_nat_def multiplicity_nat_def msetprod_def)
+  apply (frule multiset_prime_factorization)
+  apply (simp add: prime_factors_nat_def multiplicity_nat_def msetprod_def)
+  done
 
 lemma prime_factorization_int: 
   assumes "(n::int) > 0"
@@ -376,8 +366,7 @@
     "S = { (p::nat) . f p > 0} \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
       n = (PROD p : S. p^(f p)) \<Longrightarrow>
         S = prime_factors n & (ALL p. f p = multiplicity p n)"
-  apply (subgoal_tac "multiset_prime_factorization n = Abs_multiset
-      f")
+  apply (subgoal_tac "multiset_prime_factorization n = Abs_multiset f")
   apply (unfold prime_factors_nat_def multiplicity_nat_def)
   apply (simp add: set_of_def Abs_multiset_inverse multiset_def)
   apply (unfold multiset_prime_factorization_def)
@@ -396,13 +385,14 @@
   apply (subgoal_tac "f : multiset")
   apply (auto simp only: Abs_multiset_inverse)
   unfolding multiset_def apply force 
-done
+  done
 
 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"
-  by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric],
-    assumption+)
+  apply (rule prime_factorization_unique_nat [THEN conjunct1, symmetric])
+  apply assumption+
+  done
 
 lemma prime_factors_characterization'_nat: 
   "finite {p. 0 < f (p::nat)} \<Longrightarrow>
@@ -410,7 +400,7 @@
       prime_factors (PROD p | 0 < f p . p ^ f p) = {p. 0 < f p}"
   apply (rule prime_factors_characterization_nat)
   apply auto
-done
+  done
 
 (* A minor glitch:*)
 
@@ -433,7 +423,7 @@
     [where f = "%x. f (int (x::nat))", 
     transferred direction: nat "op <= (0::int)"])
   apply auto
-done
+  done
 
 lemma prime_factors_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> 
     finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
@@ -444,32 +434,32 @@
   apply (subst primes_characterization'_int)
   apply auto
   apply (auto simp add: prime_ge_0_int)
-done
+  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"
-  by (frule prime_factorization_unique_nat [THEN conjunct2, rule_format, 
-    symmetric], auto)
+  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"
-  apply (rule impI)+
+  apply (intro impI)
   apply (rule multiplicity_characterization_nat)
   apply auto
-done
+  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])
   apply auto
-done
+  done
 
 lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> 
     finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
@@ -480,7 +470,7 @@
   apply (subst multiplicity_characterization'_int)
   apply auto
   apply (auto simp add: prime_ge_0_int)
-done
+  done
 
 lemma multiplicity_zero_nat [simp]: "multiplicity (p::nat) 0 = 0"
   by (simp add: multiplicity_nat_def multiset_prime_factorization_def)
@@ -495,51 +485,50 @@
   by (simp add: multiplicity_int_def)
 
 lemma multiplicity_prime_nat [simp]: "prime (p::nat) \<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 = "(%q. if q = p then 1 else 0)"])
   apply auto
   apply (case_tac "x = p")
   apply auto
-done
+  done
 
 lemma multiplicity_prime_int [simp]: "prime (p::int) \<Longrightarrow> multiplicity p p = 1"
   unfolding prime_int_def multiplicity_int_def by auto
 
-lemma multiplicity_prime_power_nat [simp]: "prime (p::nat) \<Longrightarrow> 
-    multiplicity p (p^n) = n"
-  apply (case_tac "n = 0")
+lemma multiplicity_prime_power_nat [simp]: "prime (p::nat) \<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 = "(%q. if q = p then n else 0)"])
   apply auto
   apply (case_tac "x = p")
   apply auto
-done
+  done
 
-lemma multiplicity_prime_power_int [simp]: "prime (p::int) \<Longrightarrow> 
-    multiplicity p (p^n) = n"
+lemma multiplicity_prime_power_int [simp]: "prime (p::int) \<Longrightarrow> multiplicity p (p^n) = n"
   apply (frule prime_ge_0_int)
   apply (auto simp add: prime_int_def multiplicity_int_def nat_power_eq)
-done
+  done
 
-lemma multiplicity_nonprime_nat [simp]: "~ prime (p::nat) \<Longrightarrow> 
-    multiplicity p n = 0"
-  apply (case_tac "n = 0")
+lemma multiplicity_nonprime_nat [simp]: "~ prime (p::nat) \<Longrightarrow> multiplicity p n = 0"
+  apply (cases "n = 0")
   apply auto
   apply (frule multiset_prime_factorization)
   apply (auto simp add: set_of_def multiplicity_nat_def)
-done
+  done
 
 lemma multiplicity_nonprime_int [simp]: "~ prime (p::int) \<Longrightarrow> multiplicity p n = 0"
-  by (unfold multiplicity_int_def prime_int_def, auto)
+  unfolding multiplicity_int_def prime_int_def by auto
 
 lemma multiplicity_not_factor_nat [simp]: 
     "p ~: prime_factors (n::nat) \<Longrightarrow> multiplicity p n = 0"
-  by (subst (asm) prime_factors_altdef_nat, auto)
+  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"
-  by (subst (asm) prime_factors_altdef_int, auto)
+  apply (subst (asm) prime_factors_altdef_int)
+  apply auto
+  done
 
 lemma multiplicity_product_aux_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow>
     (prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
@@ -572,7 +561,7 @@
   apply (simp add: setprod_1)
   apply (erule prime_factorization_nat)
   apply (rule setprod_cong, auto)
-done
+  done
 
 (* transfer doesn't have the same problem here with the right 
    choice of rules. *)
@@ -611,7 +600,7 @@
   apply auto
   apply (subst multiplicity_product_nat)
   apply auto
-done
+  done
 
 (* Transfer is delicate here for two reasons: first, because there is
    an implicit quantifier over functions (f), and, second, because the 
@@ -627,7 +616,7 @@
   "(PROD x : A. int (f x)) >= 0"
   apply (rule setsum_nonneg, auto)
   apply (rule setprod_nonneg, auto)
-done
+  done
 
 declare transfer_morphism_nat_int[transfer 
   add return: transfer_nat_int_sum_prod_closure3
@@ -648,7 +637,7 @@
   apply auto
   apply (rule setsum_cong)
   apply auto
-done
+  done
 
 declare transfer_morphism_nat_int[transfer 
   add return: transfer_nat_int_sum_prod2 (1)]
@@ -676,7 +665,6 @@
 lemma multiplicity_prod_prime_powers_int:
     "(p::int) >= 0 \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
        multiplicity p (PROD p : S. p ^ f p) = (if p : 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])
@@ -684,7 +672,7 @@
   apply (metis prime_int_def)
   apply (metis prime_ge_0_int)
   apply (metis nat_set_def prime_ge_0_int transfer_nat_int_set_return_embed)
-done
+  done
 
 lemma multiplicity_distinct_prime_power_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow>
     p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
@@ -692,7 +680,7 @@
   apply (erule ssubst)
   apply (subst multiplicity_prod_prime_powers_nat)
   apply auto
-done
+  done
 
 lemma multiplicity_distinct_prime_power_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow>
     p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
@@ -701,41 +689,40 @@
   prefer 4
   apply assumption
   apply auto
-done
+  done
 
-lemma dvd_multiplicity_nat: 
+lemma dvd_multiplicity_nat:
     "(0::nat) < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x <= multiplicity p y"
-  apply (case_tac "x = 0")
+  apply (cases "x = 0")
   apply (auto simp add: dvd_def multiplicity_product_nat)
-done
+  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"
-  apply (case_tac "x = 0")
+  apply (cases "x = 0")
   apply (auto simp add: dvd_def)
   apply (subgoal_tac "0 < k")
   apply (auto simp add: multiplicity_product_int)
   apply (erule zero_less_mult_pos)
   apply arith
-done
+  done
 
 lemma dvd_prime_factors_nat [intro]:
     "0 < (y::nat) \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
   apply (simp only: prime_factors_altdef_nat)
   apply auto
   apply (metis dvd_multiplicity_nat le_0_eq neq_zero_eq_gt_zero_nat)
-done
+  done
 
 lemma dvd_prime_factors_int [intro]:
     "0 < (y::int) \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
   apply (auto simp add: prime_factors_altdef_int)
   apply (metis dvd_multiplicity_int le_0_eq neq_zero_eq_gt_zero_nat)
-done
+  done
 
 lemma multiplicity_dvd_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow> 
-    ALL p. multiplicity p x <= multiplicity p y \<Longrightarrow>
-      x dvd y"
+    ALL p. multiplicity p x <= 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)
@@ -744,11 +731,10 @@
   apply auto
   apply (metis gr0I le_0_eq less_not_refl)
   apply (metis le_imp_power_dvd)
-done
+  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"
+    ALL p >= 0. multiplicity p x <= 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)
@@ -756,17 +742,18 @@
   apply (subst prime_factors_altdef_int)+
   apply auto
   apply (metis le_imp_power_dvd prime_factors_ge_0_int)
-done
+  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"
-by (metis gcd_lcm_complete_lattice_nat.top_greatest le_refl multiplicity_dvd_nat
-          multiplicity_nonprime_nat neq0_conv)
+  by (metis gcd_lcm_complete_lattice_nat.top_greatest le_refl multiplicity_dvd_nat
+      multiplicity_nonprime_nat neq0_conv)
 
 lemma multiplicity_dvd'_int: "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
     \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
-by (metis eq_imp_le gcd_lcm_complete_lattice_nat.top_greatest int_eq_0_conv multiplicity_dvd_int
-          multiplicity_nonprime_int nat_int transfer_nat_int_relations(4) less_le)
+  by (metis eq_imp_le gcd_lcm_complete_lattice_nat.top_greatest int_eq_0_conv
+      multiplicity_dvd_int multiplicity_nonprime_int nat_int transfer_nat_int_relations(4)
+      less_le)
 
 lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
     (x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
@@ -778,7 +765,7 @@
 
 lemma prime_factors_altdef2_nat: "(n::nat) > 0 \<Longrightarrow> 
     (p : prime_factors n) = (prime p & p dvd n)"
-  apply (case_tac "prime p")
+  apply (cases "prime p")
   apply auto
   apply (subst prime_factorization_nat [where n = n], assumption)
   apply (rule dvd_trans) 
@@ -787,13 +774,12 @@
   apply (rule dvd_setprod)
   apply auto
   apply (metis One_nat_def Zero_not_Suc dvd_multiplicity_nat le0 le_antisym multiplicity_not_factor_nat multiplicity_prime_nat)  
-done
+  done
 
 lemma prime_factors_altdef2_int: 
   assumes "(n::int) > 0" 
   shows "(p : prime_factors n) = (prime p & p dvd n)"
-
-  apply (case_tac "p >= 0")
+  apply (cases "p >= 0")
   apply (rule prime_factors_altdef2_nat [transferred])
   using assms apply auto
   apply (auto simp add: prime_ge_0_int prime_factors_ge_0_int)
@@ -804,20 +790,18 @@
   assumes [arith]: "x > 0" "y > 0" and
     mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
   shows "x = y"
-
   apply (rule dvd_antisym)
   apply (auto intro: multiplicity_dvd'_nat) 
-done
+  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"
   shows "x = y"
-
   apply (rule dvd_antisym [transferred])
   apply (auto intro: multiplicity_dvd'_int) 
-done
+  done
 
 
 subsection {* An application *}
@@ -850,7 +834,7 @@
     done
   ultimately have "z = gcd x y"
     by (subst gcd_unique_nat [symmetric], blast)
-  thus ?thesis
+  then show ?thesis
     unfolding z_def by auto
 qed
 
@@ -882,39 +866,34 @@
     done
   ultimately have "z = lcm x y"
     by (subst lcm_unique_nat [symmetric], blast)
-  thus ?thesis
+  then show ?thesis
     unfolding z_def by auto
 qed
 
 lemma multiplicity_gcd_nat: 
   assumes [arith]: "x > 0" "y > 0"
-  shows "multiplicity (p::nat) (gcd x y) = 
-    min (multiplicity p x) (multiplicity p y)"
-
+  shows "multiplicity (p::nat) (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
+  done
 
 lemma multiplicity_lcm_nat: 
   assumes [arith]: "x > 0" "y > 0"
-  shows "multiplicity (p::nat) (lcm x y) = 
-    max (multiplicity p x) (multiplicity p y)"
-
+  shows "multiplicity (p::nat) (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
+  done
 
 lemma gcd_lcm_distrib_nat: "gcd (x::nat) (lcm y z) = lcm (gcd x y) (gcd x z)"
-  apply (case_tac "x = 0 | y = 0 | z = 0") 
+  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
+  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)"
   apply (subst (1 2 3) gcd_abs_int)
@@ -923,6 +902,6 @@
   apply force
   apply (rule gcd_lcm_distrib_nat [transferred])
   apply auto
-done
+  done
 
 end




