# HG changeset patch
# User wenzelm
# Date 1315690052 -7200
# Node ID a98ef45122f3eaecb2ecc2fefc15869b8ffc668c
# Parent  fbfdc5ac86be20a51052a296bdf5d68f49105d29
misc tuning;

diff -r fbfdc5ac86be -r a98ef45122f3 src/HOL/Number_Theory/Binomial.thy
--- a/src/HOL/Number_Theory/Binomial.thy	Sat Sep 10 22:11:55 2011 +0200
+++ b/src/HOL/Number_Theory/Binomial.thy	Sat Sep 10 23:27:32 2011 +0200
@@ -20,40 +20,35 @@
 subsection {* Main definitions *}
 
 class binomial =
-
-fixes 
-  binomial :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "choose" 65)
+  fixes binomial :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "choose" 65)
 
 (* definitions for the natural numbers *)
 
 instantiation nat :: binomial
-
 begin 
 
-fun
-  binomial_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+fun binomial_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
 where
   "binomial_nat n k =
    (if k = 0 then 1 else
     if n = 0 then 0 else
       (binomial (n - 1) k) + (binomial (n - 1) (k - 1)))"
 
-instance proof qed
+instance ..
 
 end
 
 (* definitions for the integers *)
 
 instantiation int :: binomial
-
 begin 
 
-definition
-  binomial_int :: "int => int \<Rightarrow> int"
-where
-  "binomial_int n k = (if n \<ge> 0 \<and> k \<ge> 0 then int (binomial (nat n) (nat k))
-      else 0)"
-instance proof qed
+definition binomial_int :: "int => int \<Rightarrow> int" where
+  "binomial_int n k =
+   (if n \<ge> 0 \<and> k \<ge> 0 then int (binomial (nat n) (nat k))
+    else 0)"
+
+instance ..
 
 end
 
@@ -97,10 +92,11 @@
   by (induct n rule: induct'_nat, auto)
 
 lemma zero_choose_int [rule_format,simp]: "(k::int) > n \<Longrightarrow> n choose k = 0"
-  unfolding binomial_int_def apply (case_tac "n < 0")
+  unfolding binomial_int_def
+  apply (cases "n < 0")
   apply force
   apply (simp del: binomial_nat.simps)
-done
+  done
 
 lemma choose_reduce_nat: "(n::nat) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
     (n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
@@ -108,10 +104,10 @@
 
 lemma choose_reduce_int: "(n::int) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
     (n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
-  unfolding binomial_int_def apply (subst choose_reduce_nat)
-    apply (auto simp del: binomial_nat.simps 
-      simp add: nat_diff_distrib)
-done
+  unfolding binomial_int_def
+  apply (subst choose_reduce_nat)
+    apply (auto simp del: binomial_nat.simps simp add: nat_diff_distrib)
+  done
 
 lemma choose_plus_one_nat: "((n::nat) + 1) choose (k + 1) = 
     (n choose (k + 1)) + (n choose k)"
@@ -128,13 +124,13 @@
 declare binomial_nat.simps [simp del]
 
 lemma choose_self_nat [simp]: "((n::nat) choose n) = 1"
-  by (induct n rule: induct'_nat, auto simp add: choose_plus_one_nat)
+  by (induct n rule: induct'_nat) (auto simp add: choose_plus_one_nat)
 
 lemma choose_self_int [simp]: "n \<ge> 0 \<Longrightarrow> ((n::int) choose n) = 1"
   by (auto simp add: binomial_int_def)
 
 lemma choose_one_nat [simp]: "(n::nat) choose 1 = n"
-  by (induct n rule: induct'_nat, auto simp add: choose_reduce_nat)
+  by (induct n rule: induct'_nat) (auto simp add: choose_reduce_nat)
 
 lemma choose_one_int [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 1 = n"
   by (auto simp add: binomial_int_def)
@@ -165,7 +161,7 @@
   apply force
   apply (subst choose_reduce_nat)
   apply auto
-done
+  done
 
 lemma choose_pos_int: "n \<ge> 0 \<Longrightarrow> k >= 0 \<Longrightarrow> k \<le> n \<Longrightarrow>
     ((n::int) choose k) > 0"
@@ -183,7 +179,7 @@
   apply (drule_tac x = n in spec) back back 
   apply (drule_tac x = "k - 1" in spec) back back back
   apply auto
-done
+  done
 
 lemma choose_altdef_aux_nat: "(k::nat) \<le> n \<Longrightarrow> 
     fact k * fact (n - k) * (n choose k) = fact n"
@@ -193,10 +189,9 @@
   fix k :: nat and n
   assume less: "k < n"
   assume ih1: "fact k * fact (n - k) * (n choose k) = fact n"
-  hence one: "fact (k + 1) * fact (n - k) * (n choose k) = (k + 1) * fact n"
+  then have one: "fact (k + 1) * fact (n - k) * (n choose k) = (k + 1) * fact n"
     by (subst fact_plus_one_nat, auto)
-  assume ih2: "fact (k + 1) * fact (n - (k + 1)) * (n choose (k + 1)) = 
-      fact n"
+  assume ih2: "fact (k + 1) * fact (n - (k + 1)) * (n choose (k + 1)) =  fact n"
   with less have "fact (k + 1) * fact ((n - (k + 1)) + 1) * 
       (n choose (k + 1)) = (n - k) * fact n"
     by (subst (2) fact_plus_one_nat, auto)
@@ -222,7 +217,7 @@
   apply (frule choose_altdef_aux_nat)
   apply (erule subst)
   apply (simp add: mult_ac)
-done
+  done
 
 
 lemma choose_altdef_int: 
@@ -238,7 +233,7 @@
   (* why don't blast and auto get this??? *)
   apply (rule exI)
   apply (erule sym)
-done
+  done
 
 lemma choose_dvd_int: 
   assumes "(0::int) <= k" and "k <= n"
@@ -293,7 +288,8 @@
   fixes S :: "'a set"
   shows "finite S \<Longrightarrow> card {T. T \<le> S \<and> card T = k} = card S choose k"
 proof (induct arbitrary: k set: finite)
-  case empty show ?case by (auto simp add: Collect_conv_if)
+  case empty
+  show ?case by (auto simp add: Collect_conv_if)
 next
   case (insert x F)
   note iassms = insert(1,2)
@@ -303,11 +299,11 @@
     case zero
     from iassms have "{T. T \<le> (insert x F) \<and> card T = 0} = {{}}"
       by (auto simp: finite_subset)
-    thus ?case by auto
+    then show ?case by auto
   next
     case (plus1 k)
     from iassms have fin: "finite (insert x F)" by auto
-    hence "{ T. T \<subseteq> insert x F \<and> card T = k + 1} =
+    then have "{ T. T \<subseteq> insert x F \<and> card T = k + 1} =
       {T. T \<le> F & card T = k + 1} Un 
       {T. T \<le> insert x F & x : T & card T = k + 1}"
       by auto
@@ -326,14 +322,14 @@
       let ?f = "%T. T Un {x}"
       from iassms have "inj_on ?f {T. T <= F & card T = k}"
         unfolding inj_on_def by auto
-      hence "card ({T. T <= F & card T = k}) = 
+      then have "card ({T. T <= F & card T = k}) = 
         card(?f ` {T. T <= F & card T = k})"
         by (rule card_image [symmetric])
       also have "?f ` {T. T <= F & card T = k} = 
         {T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}" (is "?L=?R")
       proof-
         { fix S assume "S \<subseteq> F"
-          hence "card(insert x S) = card S +1"
+          then have "card(insert x S) = card S +1"
             using iassms by (auto simp: finite_subset) }
         moreover
         { fix T assume 1: "T \<subseteq> insert x F" "x : T" "card T = k+1"
@@ -353,5 +349,4 @@
   qed
 qed
 
-
 end
diff -r fbfdc5ac86be -r a98ef45122f3 src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Sat Sep 10 22:11:55 2011 +0200
+++ b/src/HOL/Number_Theory/Cong.thy	Sat Sep 10 23:27:32 2011 +0200
@@ -14,7 +14,7 @@
 The original theory "IntPrimes" was by Thomas M. Rasmussen, and
 extended gcd, lcm, primes to the integers. Amine Chaieb provided
 another extension of the notions to the integers, and added a number
-of results to "Primes" and "GCD". 
+of results to "Primes" and "GCD".
 
 The original theory, "IntPrimes", by Thomas M. Rasmussen, defined and
 developed the congruence relations on the integers. The notion was
@@ -29,34 +29,33 @@
 imports Primes
 begin
 
-subsection {* Turn off One_nat_def *}
+subsection {* Turn off @{text One_nat_def} *}
 
-lemma induct'_nat [case_names zero plus1, induct type: nat]: 
-    "\<lbrakk> P (0::nat); !!n. P n \<Longrightarrow> P (n + 1)\<rbrakk> \<Longrightarrow> P n"
-by (erule nat_induct) (simp add:One_nat_def)
+lemma induct'_nat [case_names zero plus1, induct type: nat]:
+    "P (0::nat) \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (n + 1)) \<Longrightarrow> P n"
+  by (induct n) (simp_all add: One_nat_def)
 
-lemma cases_nat [case_names zero plus1, cases type: nat]: 
-    "P (0::nat) \<Longrightarrow> (!!n. P (n + 1)) \<Longrightarrow> P n"
-by(metis induct'_nat)
+lemma cases_nat [case_names zero plus1, cases type: nat]:
+    "P (0::nat) \<Longrightarrow> (\<And>n. P (n + 1)) \<Longrightarrow> P n"
+  by (rule induct'_nat)
 
 lemma power_plus_one [simp]: "(x::'a::power)^(n + 1) = x * x^n"
-by (simp add: One_nat_def)
+  by (simp add: One_nat_def)
 
-lemma power_eq_one_eq_nat [simp]: 
-  "((x::nat)^m = 1) = (m = 0 | x = 1)"
-by (induct m, auto)
+lemma power_eq_one_eq_nat [simp]: "((x::nat)^m = 1) = (m = 0 | x = 1)"
+  by (induct m) auto
 
 lemma card_insert_if' [simp]: "finite A \<Longrightarrow>
-  card (insert x A) = (if x \<in> A then (card A) else (card A) + 1)"
-by (auto simp add: insert_absorb)
+    card (insert x A) = (if x \<in> A then (card A) else (card A) + 1)"
+  by (auto simp add: insert_absorb)
 
 lemma nat_1' [simp]: "nat 1 = 1"
-by simp
+  by simp
 
 (* For those annoying moments where Suc reappears, use Suc_eq_plus1 *)
 
 declare nat_1 [simp del]
-declare add_2_eq_Suc [simp del] 
+declare add_2_eq_Suc [simp del]
 declare add_2_eq_Suc' [simp del]
 
 
@@ -66,31 +65,23 @@
 subsection {* Main definitions *}
 
 class cong =
-
-fixes 
-  cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(mod _'))")
-
+  fixes cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(mod _'))")
 begin
 
-abbreviation
-  notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ \<noteq> _] '(mod _'))")
-where
-  "notcong x y m == (~cong x y m)" 
+abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  ("(1[_ \<noteq> _] '(mod _'))")
+  where "notcong x y m \<equiv> \<not> cong x y m"
 
 end
 
 (* definitions for the natural numbers *)
 
 instantiation nat :: cong
-
-begin 
+begin
 
-definition 
-  cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
-where 
-  "cong_nat x y m = ((x mod m) = (y mod m))"
+definition cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+  where "cong_nat x y m = ((x mod m) = (y mod m))"
 
-instance proof qed
+instance ..
 
 end
 
@@ -98,15 +89,12 @@
 (* definitions for the integers *)
 
 instantiation int :: cong
-
-begin 
+begin
 
-definition 
-  cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
-where 
-  "cong_int x y m = ((x mod m) = (y mod m))"
+definition cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
+  where "cong_int x y m = ((x mod m) = (y mod m))"
 
-instance proof qed
+instance ..
 
 end
 
@@ -115,25 +103,25 @@
 
 
 lemma transfer_nat_int_cong:
-  "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> m >= 0 \<Longrightarrow> 
+  "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> m >= 0 \<Longrightarrow>
     ([(nat x) = (nat y)] (mod (nat m))) = ([x = y] (mod m))"
-  unfolding cong_int_def cong_nat_def 
+  unfolding cong_int_def cong_nat_def
   apply (auto simp add: nat_mod_distrib [symmetric])
   apply (subst (asm) eq_nat_nat_iff)
-  apply (case_tac "m = 0", force, rule pos_mod_sign, force)+
+  apply (cases "m = 0", force, rule pos_mod_sign, force)+
   apply assumption
-done
+  done
 
-declare transfer_morphism_nat_int[transfer add return: 
+declare transfer_morphism_nat_int[transfer add return:
     transfer_nat_int_cong]
 
 lemma transfer_int_nat_cong:
   "[(int x) = (int y)] (mod (int m)) = [x = y] (mod m)"
   apply (auto simp add: cong_int_def cong_nat_def)
   apply (auto simp add: zmod_int [symmetric])
-done
+  done
 
-declare transfer_morphism_int_nat[transfer add return: 
+declare transfer_morphism_int_nat[transfer add return:
     transfer_int_nat_cong]
 
 
@@ -141,52 +129,52 @@
 
 (* was zcong_0, etc. *)
 lemma cong_0_nat [simp, presburger]: "([(a::nat) = b] (mod 0)) = (a = b)"
-  by (unfold cong_nat_def, auto)
+  unfolding cong_nat_def by auto
 
 lemma cong_0_int [simp, presburger]: "([(a::int) = b] (mod 0)) = (a = b)"
-  by (unfold cong_int_def, auto)
+  unfolding cong_int_def by auto
 
 lemma cong_1_nat [simp, presburger]: "[(a::nat) = b] (mod 1)"
-  by (unfold cong_nat_def, auto)
+  unfolding cong_nat_def by auto
 
 lemma cong_Suc_0_nat [simp, presburger]: "[(a::nat) = b] (mod Suc 0)"
-  by (unfold cong_nat_def, auto simp add: One_nat_def)
+  unfolding cong_nat_def by (auto simp add: One_nat_def)
 
 lemma cong_1_int [simp, presburger]: "[(a::int) = b] (mod 1)"
-  by (unfold cong_int_def, auto)
+  unfolding cong_int_def by auto
 
 lemma cong_refl_nat [simp]: "[(k::nat) = k] (mod m)"
-  by (unfold cong_nat_def, auto)
+  unfolding cong_nat_def by auto
 
 lemma cong_refl_int [simp]: "[(k::int) = k] (mod m)"
-  by (unfold cong_int_def, auto)
+  unfolding cong_int_def by auto
 
 lemma cong_sym_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
-  by (unfold cong_nat_def, auto)
+  unfolding cong_nat_def by auto
 
 lemma cong_sym_int: "[(a::int) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
-  by (unfold cong_int_def, auto)
+  unfolding cong_int_def by auto
 
 lemma cong_sym_eq_nat: "[(a::nat) = b] (mod m) = [b = a] (mod m)"
-  by (unfold cong_nat_def, auto)
+  unfolding cong_nat_def by auto
 
 lemma cong_sym_eq_int: "[(a::int) = b] (mod m) = [b = a] (mod m)"
-  by (unfold cong_int_def, auto)
+  unfolding cong_int_def by auto
 
 lemma cong_trans_nat [trans]:
     "[(a::nat) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
-  by (unfold cong_nat_def, auto)
+  unfolding cong_nat_def by auto
 
 lemma cong_trans_int [trans]:
     "[(a::int) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
-  by (unfold cong_int_def, auto)
+  unfolding cong_int_def by auto
 
 lemma cong_add_nat:
     "[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
   apply (unfold cong_nat_def)
   apply (subst (1 2) mod_add_eq)
   apply simp
-done
+  done
 
 lemma cong_add_int:
     "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
@@ -194,21 +182,21 @@
   apply (subst (1 2) mod_add_left_eq)
   apply (subst (1 2) mod_add_right_eq)
   apply simp
-done
+  done
 
 lemma cong_diff_int:
     "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a - c = b - d] (mod m)"
   apply (unfold cong_int_def)
   apply (subst (1 2) mod_diff_eq)
   apply simp
-done
+  done
 
 lemma cong_diff_aux_int:
-  "(a::int) >= c \<Longrightarrow> b >= d \<Longrightarrow> [(a::int) = b] (mod m) \<Longrightarrow> 
+  "(a::int) >= c \<Longrightarrow> b >= d \<Longrightarrow> [(a::int) = b] (mod m) \<Longrightarrow>
       [c = d] (mod m) \<Longrightarrow> [tsub a c = tsub b d] (mod m)"
   apply (subst (1 2) tsub_eq)
   apply (auto intro: cong_diff_int)
-done;
+  done
 
 lemma cong_diff_nat:
   assumes "(a::nat) >= c" and "b >= d" and "[a = b] (mod m)" and
@@ -221,7 +209,7 @@
   apply (unfold cong_nat_def)
   apply (subst (1 2) mod_mult_eq)
   apply simp
-done
+  done
 
 lemma cong_mult_int:
     "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
@@ -230,73 +218,69 @@
   apply (subst (1 2) mult_commute)
   apply (subst (1 2) zmod_zmult1_eq)
   apply simp
-done
-
-lemma cong_exp_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
-  apply (induct k)
-  apply (auto simp add: cong_mult_nat)
-  done
-
-lemma cong_exp_int: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
-  apply (induct k)
-  apply (auto simp add: cong_mult_int)
   done
 
-lemma cong_setsum_nat [rule_format]: 
-    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow> 
+lemma cong_exp_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
+  by (induct k) (auto simp add: cong_mult_nat)
+
+lemma cong_exp_int: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
+  by (induct k) (auto simp add: cong_mult_int)
+
+lemma cong_setsum_nat [rule_format]:
+    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
       [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
-  apply (case_tac "finite A")
+  apply (cases "finite A")
   apply (induct set: finite)
   apply (auto intro: cong_add_nat)
-done
+  done
 
 lemma cong_setsum_int [rule_format]:
-    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow> 
+    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
       [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
-  apply (case_tac "finite A")
+  apply (cases "finite A")
   apply (induct set: finite)
   apply (auto intro: cong_add_int)
-done
+  done
 
-lemma cong_setprod_nat [rule_format]: 
-    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow> 
+lemma cong_setprod_nat [rule_format]:
+    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
       [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
-  apply (case_tac "finite A")
+  apply (cases "finite A")
   apply (induct set: finite)
   apply (auto intro: cong_mult_nat)
-done
+  done
 
-lemma cong_setprod_int [rule_format]: 
-    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow> 
+lemma cong_setprod_int [rule_format]:
+    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
       [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
-  apply (case_tac "finite A")
+  apply (cases "finite A")
   apply (induct set: finite)
   apply (auto intro: cong_mult_int)
-done
+  done
 
 lemma cong_scalar_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
-  by (rule cong_mult_nat, simp_all)
+  by (rule cong_mult_nat) simp_all
 
 lemma cong_scalar_int: "[(a::int)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
-  by (rule cong_mult_int, simp_all)
+  by (rule cong_mult_int) simp_all
 
 lemma cong_scalar2_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
-  by (rule cong_mult_nat, simp_all)
+  by (rule cong_mult_nat) simp_all
 
 lemma cong_scalar2_int: "[(a::int)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
-  by (rule cong_mult_int, simp_all)
+  by (rule cong_mult_int) simp_all
 
 lemma cong_mult_self_nat: "[(a::nat) * m = 0] (mod m)"
-  by (unfold cong_nat_def, auto)
+  unfolding cong_nat_def by auto
 
 lemma cong_mult_self_int: "[(a::int) * m = 0] (mod m)"
-  by (unfold cong_int_def, auto)
+  unfolding cong_int_def by auto
 
 lemma cong_eq_diff_cong_0_int: "[(a::int) = b] (mod m) = [a - b = 0] (mod m)"
   apply (rule iffI)
   apply (erule cong_diff_int [of a b m b b, simplified])
   apply (erule cong_add_int [of "a - b" 0 m b b, simplified])
-done
+  done
 
 lemma cong_eq_diff_cong_0_aux_int: "a >= b \<Longrightarrow>
     [(a::int) = b] (mod m) = [tsub a b = 0] (mod m)"
@@ -307,29 +291,29 @@
   shows "[a = b] (mod m) = [a - b = 0] (mod m)"
   using assms by (rule cong_eq_diff_cong_0_aux_int [transferred])
 
-lemma cong_diff_cong_0'_nat: 
-  "[(x::nat) = y] (mod n) \<longleftrightarrow> 
+lemma cong_diff_cong_0'_nat:
+  "[(x::nat) = y] (mod n) \<longleftrightarrow>
     (if x <= y then [y - x = 0] (mod n) else [x - y = 0] (mod n))"
-  apply (case_tac "y <= x")
+  apply (cases "y <= x")
   apply (frule cong_eq_diff_cong_0_nat [where m = n])
   apply auto [1]
   apply (subgoal_tac "x <= y")
   apply (frule cong_eq_diff_cong_0_nat [where m = n])
   apply (subst cong_sym_eq_nat)
   apply auto
-done
+  done
 
 lemma cong_altdef_nat: "(a::nat) >= b \<Longrightarrow> [a = b] (mod m) = (m dvd (a - b))"
   apply (subst cong_eq_diff_cong_0_nat, assumption)
   apply (unfold cong_nat_def)
   apply (simp add: dvd_eq_mod_eq_0 [symmetric])
-done
+  done
 
 lemma cong_altdef_int: "[(a::int) = b] (mod m) = (m dvd (a - b))"
   apply (subst cong_eq_diff_cong_0_int)
   apply (unfold cong_int_def)
   apply (simp add: dvd_eq_mod_eq_0 [symmetric])
-done
+  done
 
 lemma cong_abs_int: "[(x::int) = y] (mod abs m) = [x = y] (mod m)"
   by (simp add: cong_altdef_int)
@@ -342,29 +326,29 @@
   (* any way around this? *)
   apply (subgoal_tac "a * a - 1 = (a - 1) * (a - -1)")
   apply (auto simp add: field_simps)
-done
+  done
 
 lemma cong_mult_rcancel_int:
-  "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
+    "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
   apply (subst (1 2) cong_altdef_int)
   apply (subst left_diff_distrib [symmetric])
   apply (rule coprime_dvd_mult_iff_int)
   apply (subst gcd_commute_int, assumption)
-done
+  done
 
 lemma cong_mult_rcancel_nat:
   assumes  "coprime k (m::nat)"
   shows "[a * k = b * k] (mod m) = [a = b] (mod m)"
   apply (rule cong_mult_rcancel_int [transferred])
   using assms apply auto
-done
+  done
 
 lemma cong_mult_lcancel_nat:
-  "coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
+    "coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
   by (simp add: mult_commute cong_mult_rcancel_nat)
 
 lemma cong_mult_lcancel_int:
-  "coprime k (m::int) \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
+    "coprime k (m::int) \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
   by (simp add: mult_commute cong_mult_rcancel_int)
 
 (* was zcong_zgcd_zmult_zmod *)
@@ -395,7 +379,7 @@
   apply auto
   apply (rule_tac x = "a mod m" in exI)
   apply (unfold cong_nat_def, auto)
-done
+  done
 
 lemma cong_less_unique_int:
     "0 < (m::int) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
@@ -407,12 +391,12 @@
 lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
   apply (auto simp add: cong_altdef_int dvd_def field_simps)
   apply (rule_tac [!] x = "-k" in exI, auto)
-done
+  done
 
-lemma cong_iff_lin_nat: "([(a::nat) = b] (mod m)) = 
+lemma cong_iff_lin_nat: "([(a::nat) = b] (mod m)) =
     (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
   apply (rule iffI)
-  apply (case_tac "b <= a")
+  apply (cases "b <= a")
   apply (subst (asm) cong_altdef_nat, assumption)
   apply (unfold dvd_def, auto)
   apply (rule_tac x = k in exI)
@@ -430,42 +414,40 @@
   apply (erule ssubst)back
   apply (erule subst)
   apply auto
-done
+  done
 
 lemma cong_gcd_eq_int: "[(a::int) = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
   apply (subst (asm) cong_iff_lin_int, auto)
-  apply (subst add_commute) 
+  apply (subst add_commute)
   apply (subst (2) gcd_commute_int)
   apply (subst mult_commute)
   apply (subst gcd_add_mult_int)
   apply (rule gcd_commute_int)
   done
 
-lemma cong_gcd_eq_nat: 
+lemma cong_gcd_eq_nat:
   assumes "[(a::nat) = b] (mod m)"
   shows "gcd a m = gcd b m"
   apply (rule cong_gcd_eq_int [transferred])
   using assms apply auto
   done
 
-lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> 
-    coprime b m"
+lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
   by (auto simp add: cong_gcd_eq_nat)
 
-lemma cong_imp_coprime_int: "[(a::int) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> 
-    coprime b m"
+lemma cong_imp_coprime_int: "[(a::int) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
   by (auto simp add: cong_gcd_eq_int)
 
-lemma cong_cong_mod_nat: "[(a::nat) = b] (mod m) = 
-    [a mod m = b mod m] (mod m)"
+lemma cong_cong_mod_nat: "[(a::nat) = b] (mod m) = [a mod m = b mod m] (mod m)"
   by (auto simp add: cong_nat_def)
 
-lemma cong_cong_mod_int: "[(a::int) = b] (mod m) = 
-    [a mod m = b mod m] (mod m)"
+lemma cong_cong_mod_int: "[(a::int) = b] (mod m) = [a mod m = b mod m] (mod m)"
   by (auto simp add: cong_int_def)
 
 lemma cong_minus_int [iff]: "[(a::int) = b] (mod -m) = [a = b] (mod m)"
-  by (subst (1 2) cong_altdef_int, auto)
+  apply (subst (1 2) cong_altdef_int)
+  apply auto
+  done
 
 lemma cong_zero_nat: "[(a::nat) = b] (mod 0) = (a = b)"
   by auto
@@ -479,7 +461,7 @@
   apply (unfold dvd_def, auto)
   apply (rule mod_mod_cancel)
   apply auto
-done
+  done
 
 lemma mod_dvd_mod:
   assumes "0 < (m::nat)" and "m dvd b"
@@ -490,12 +472,12 @@
   done
 *)
 
-lemma cong_add_lcancel_nat: 
-    "[(a::nat) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" 
+lemma cong_add_lcancel_nat:
+    "[(a::nat) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
   by (simp add: cong_iff_lin_nat)
 
-lemma cong_add_lcancel_int: 
-    "[(a::int) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" 
+lemma cong_add_lcancel_int:
+    "[(a::int) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
   by (simp add: cong_iff_lin_int)
 
 lemma cong_add_rcancel_nat: "[(x::nat) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
@@ -504,43 +486,42 @@
 lemma cong_add_rcancel_int: "[(x::int) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
   by (simp add: cong_iff_lin_int)
 
-lemma cong_add_lcancel_0_nat: "[(a::nat) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
+lemma cong_add_lcancel_0_nat: "[(a::nat) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
   by (simp add: cong_iff_lin_nat)
 
-lemma cong_add_lcancel_0_int: "[(a::int) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
+lemma cong_add_lcancel_0_int: "[(a::int) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
   by (simp add: cong_iff_lin_int)
 
-lemma cong_add_rcancel_0_nat: "[x + (a::nat) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
+lemma cong_add_rcancel_0_nat: "[x + (a::nat) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
   by (simp add: cong_iff_lin_nat)
 
-lemma cong_add_rcancel_0_int: "[x + (a::int) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
+lemma cong_add_rcancel_0_int: "[x + (a::int) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
   by (simp add: cong_iff_lin_int)
 
-lemma cong_dvd_modulus_nat: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> 
+lemma cong_dvd_modulus_nat: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
     [x = y] (mod n)"
   apply (auto simp add: cong_iff_lin_nat dvd_def)
   apply (rule_tac x="k1 * k" in exI)
   apply (rule_tac x="k2 * k" in exI)
   apply (simp add: field_simps)
-done
+  done
 
-lemma cong_dvd_modulus_int: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> 
-    [x = y] (mod n)"
+lemma cong_dvd_modulus_int: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)"
   by (auto simp add: cong_altdef_int dvd_def)
 
 lemma cong_dvd_eq_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
-  by (unfold cong_nat_def, auto simp add: dvd_eq_mod_eq_0)
+  unfolding cong_nat_def by (auto simp add: dvd_eq_mod_eq_0)
 
 lemma cong_dvd_eq_int: "[(x::int) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
-  by (unfold cong_int_def, auto simp add: dvd_eq_mod_eq_0)
+  unfolding cong_int_def by (auto simp add: dvd_eq_mod_eq_0)
 
-lemma cong_mod_nat: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)" 
+lemma cong_mod_nat: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
   by (simp add: cong_nat_def)
 
-lemma cong_mod_int: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)" 
+lemma cong_mod_int: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
   by (simp add: cong_int_def)
 
-lemma mod_mult_cong_nat: "(a::nat) ~= 0 \<Longrightarrow> b ~= 0 
+lemma mod_mult_cong_nat: "(a::nat) ~= 0 \<Longrightarrow> b ~= 0
     \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
   by (simp add: cong_nat_def mod_mult2_eq  mod_add_left_eq)
 
@@ -548,43 +529,43 @@
   apply (simp add: cong_altdef_int)
   apply (subst dvd_minus_iff [symmetric])
   apply (simp add: field_simps)
-done
+  done
 
 lemma cong_modulus_neg_int: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
   by (auto simp add: cong_altdef_int)
 
-lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0 
+lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0
     \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
-  apply (case_tac "b > 0")
+  apply (cases "b > 0")
   apply (simp add: cong_int_def mod_mod_cancel mod_add_left_eq)
   apply (subst (1 2) cong_modulus_neg_int)
   apply (unfold cong_int_def)
   apply (subgoal_tac "a * b = (-a * -b)")
   apply (erule ssubst)
   apply (subst zmod_zmult2_eq)
-  apply (auto simp add: mod_add_left_eq) 
-done
+  apply (auto simp add: mod_add_left_eq)
+  done
 
 lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))"
-  apply (case_tac "a = 0")
+  apply (cases "a = 0")
   apply force
   apply (subst (asm) cong_altdef_nat)
   apply auto
-done
+  done
 
 lemma cong_0_1_nat: "[(0::nat) = 1] (mod n) = (n = 1)"
-  by (unfold cong_nat_def, auto)
+  unfolding cong_nat_def by auto
 
 lemma cong_0_1_int: "[(0::int) = 1] (mod n) = ((n = 1) | (n = -1))"
-  by (unfold cong_int_def, auto simp add: zmult_eq_1_iff)
+  unfolding cong_int_def by (auto simp add: zmult_eq_1_iff)
 
-lemma cong_to_1'_nat: "[(a::nat) = 1] (mod n) \<longleftrightarrow> 
+lemma cong_to_1'_nat: "[(a::nat) = 1] (mod n) \<longleftrightarrow>
     a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)"
-  apply (case_tac "n = 1")
+  apply (cases "n = 1")
   apply auto [1]
   apply (drule_tac x = "a - 1" in spec)
   apply force
-  apply (case_tac "a = 0")
+  apply (cases "a = 0")
   apply (auto simp add: cong_0_1_nat) [1]
   apply (rule iffI)
   apply (drule cong_to_1_nat)
@@ -594,7 +575,7 @@
   apply (auto simp add: field_simps) [1]
   apply (subst cong_altdef_nat)
   apply (auto simp add: dvd_def)
-done
+  done
 
 lemma cong_le_nat: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
   apply (subst cong_altdef_nat)
@@ -602,10 +583,10 @@
   apply (unfold dvd_def, auto simp add: field_simps)
   apply (rule_tac x = k in exI)
   apply auto
-done
+  done
 
 lemma cong_solve_nat: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
-  apply (case_tac "n = 0")
+  apply (cases "n = 0")
   apply force
   apply (frule bezout_nat [of a n], auto)
   apply (rule exI, erule ssubst)
@@ -617,11 +598,11 @@
   apply simp
   apply (rule cong_refl_nat)
   apply (rule cong_refl_nat)
-done
+  done
 
 lemma cong_solve_int: "(a::int) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
-  apply (case_tac "n = 0")
-  apply (case_tac "a \<ge> 0")
+  apply (cases "n = 0")
+  apply (cases "a \<ge> 0")
   apply auto
   apply (rule_tac x = "-1" in exI)
   apply auto
@@ -637,16 +618,15 @@
   apply simp
   apply (subst mult_commute)
   apply (rule cong_refl_int)
-done
-  
-lemma cong_solve_dvd_nat: 
+  done
+
+lemma cong_solve_dvd_nat:
   assumes a: "(a::nat) \<noteq> 0" and b: "gcd a n dvd d"
   shows "EX x. [a * x = d] (mod n)"
 proof -
-  from cong_solve_nat [OF a] obtain x where 
-      "[a * x = gcd a n](mod n)"
+  from cong_solve_nat [OF a] obtain x where "[a * x = gcd a n](mod n)"
     by auto
-  hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)" 
+  then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
     by (elim cong_scalar2_nat)
   also from b have "(d div gcd a n) * gcd a n = d"
     by (rule dvd_div_mult_self)
@@ -656,14 +636,13 @@
     by auto
 qed
 
-lemma cong_solve_dvd_int: 
+lemma cong_solve_dvd_int:
   assumes a: "(a::int) \<noteq> 0" and b: "gcd a n dvd d"
   shows "EX x. [a * x = d] (mod n)"
 proof -
-  from cong_solve_int [OF a] obtain x where 
-      "[a * x = gcd a n](mod n)"
+  from cong_solve_int [OF a] obtain x where "[a * x = gcd a n](mod n)"
     by auto
-  hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)" 
+  then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
     by (elim cong_scalar2_int)
   also from b have "(d div gcd a n) * gcd a n = d"
     by (rule dvd_div_mult_self)
@@ -673,56 +652,52 @@
     by auto
 qed
 
-lemma cong_solve_coprime_nat: "coprime (a::nat) n \<Longrightarrow> 
-    EX x. [a * x = 1] (mod n)"
-  apply (case_tac "a = 0")
+lemma cong_solve_coprime_nat: "coprime (a::nat) n \<Longrightarrow> EX x. [a * x = 1] (mod n)"
+  apply (cases "a = 0")
   apply force
   apply (frule cong_solve_nat [of a n])
   apply auto
-done
+  done
 
-lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> 
-    EX x. [a * x = 1] (mod n)"
-  apply (case_tac "a = 0")
+lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> EX x. [a * x = 1] (mod n)"
+  apply (cases "a = 0")
   apply auto
-  apply (case_tac "n \<ge> 0")
+  apply (cases "n \<ge> 0")
   apply auto
   apply (subst cong_int_def, auto)
   apply (frule cong_solve_int [of a n])
   apply auto
-done
+  done
 
-lemma coprime_iff_invertible_nat: "m > (1::nat) \<Longrightarrow> coprime a m = 
-    (EX x. [a * x = 1] (mod m))"
+lemma coprime_iff_invertible_nat: "m > (1::nat) \<Longrightarrow> coprime a m = (EX x. [a * x = 1] (mod m))"
   apply (auto intro: cong_solve_coprime_nat)
   apply (unfold cong_nat_def, auto intro: invertible_coprime_nat)
-done
+  done
 
-lemma coprime_iff_invertible_int: "m > (1::int) \<Longrightarrow> coprime a m = 
-    (EX x. [a * x = 1] (mod m))"
+lemma coprime_iff_invertible_int: "m > (1::int) \<Longrightarrow> coprime a m = (EX x. [a * x = 1] (mod m))"
   apply (auto intro: cong_solve_coprime_int)
   apply (unfold cong_int_def)
   apply (auto intro: invertible_coprime_int)
-done
+  done
 
-lemma coprime_iff_invertible'_int: "m > (1::int) \<Longrightarrow> coprime a m = 
+lemma coprime_iff_invertible'_int: "m > (1::int) \<Longrightarrow> coprime a m =
     (EX x. 0 <= x & x < m & [a * x = 1] (mod m))"
   apply (subst coprime_iff_invertible_int)
   apply auto
   apply (auto simp add: cong_int_def)
   apply (rule_tac x = "x mod m" in exI)
   apply (auto simp add: mod_mult_right_eq [symmetric])
-done
+  done
 
 
 lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow>
     [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
-  apply (case_tac "y \<le> x")
+  apply (cases "y \<le> x")
   apply (auto simp add: cong_altdef_nat lcm_least_nat) [1]
   apply (rule cong_sym_nat)
   apply (subst (asm) (1 2) cong_sym_eq_nat)
   apply (auto simp add: cong_altdef_nat lcm_least_nat)
-done
+  done
 
 lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow>
     [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
@@ -730,15 +705,17 @@
 
 lemma cong_cong_coprime_nat: "coprime a b \<Longrightarrow> [(x::nat) = y] (mod a) \<Longrightarrow>
     [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
-  apply (frule (1) cong_cong_lcm_nat)back
+  apply (frule (1) cong_cong_lcm_nat)
+  back
   apply (simp add: lcm_nat_def)
-done
+  done
 
 lemma cong_cong_coprime_int: "coprime a b \<Longrightarrow> [(x::int) = y] (mod a) \<Longrightarrow>
     [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
-  apply (frule (1) cong_cong_lcm_int)back
+  apply (frule (1) cong_cong_lcm_int)
+  back
   apply (simp add: lcm_altdef_int cong_abs_int abs_mult [symmetric])
-done
+  done
 
 lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
     (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
@@ -750,7 +727,7 @@
   apply (subst gcd_commute_nat)
   apply (rule setprod_coprime_nat)
   apply auto
-done
+  done
 
 lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow>
     (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
@@ -762,20 +739,18 @@
   apply (subst gcd_commute_int)
   apply (rule setprod_coprime_int)
   apply auto
-done
+  done
 
-lemma binary_chinese_remainder_aux_nat: 
+lemma binary_chinese_remainder_aux_nat:
   assumes a: "coprime (m1::nat) m2"
   shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
     [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
 proof -
-  from cong_solve_coprime_nat [OF a]
-      obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
+  from cong_solve_coprime_nat [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
     by auto
-  from a have b: "coprime m2 m1" 
+  from a have b: "coprime m2 m1"
     by (subst gcd_commute_nat)
-  from cong_solve_coprime_nat [OF b]
-      obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
+  from cong_solve_coprime_nat [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
     by auto
   have "[m1 * x1 = 0] (mod m1)"
     by (subst mult_commute, rule cong_mult_self_nat)
@@ -785,18 +760,16 @@
   ultimately show ?thesis by blast
 qed
 
-lemma binary_chinese_remainder_aux_int: 
+lemma binary_chinese_remainder_aux_int:
   assumes a: "coprime (m1::int) m2"
   shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
     [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
 proof -
-  from cong_solve_coprime_int [OF a]
-      obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
+  from cong_solve_coprime_int [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
     by auto
-  from a have b: "coprime m2 m1" 
+  from a have b: "coprime m2 m1"
     by (subst gcd_commute_int)
-  from cong_solve_coprime_int [OF b]
-      obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
+  from cong_solve_coprime_int [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
     by auto
   have "[m1 * x1 = 0] (mod m1)"
     by (subst mult_commute, rule cong_mult_self_int)
@@ -811,8 +784,8 @@
   shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
 proof -
   from binary_chinese_remainder_aux_nat [OF a] obtain b1 b2
-    where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
-          "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
+      where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
+            "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
     by blast
   let ?x = "u1 * b1 + u2 * b2"
   have "[?x = u1 * 1 + u2 * 0] (mod m1)"
@@ -822,7 +795,7 @@
     apply (rule cong_scalar2_nat)
     apply (rule `[b2 = 0] (mod m1)`)
     done
-  hence "[?x = u1] (mod m1)" by simp
+  then have "[?x = u1] (mod m1)" by simp
   have "[?x = u1 * 0 + u2 * 1] (mod m2)"
     apply (rule cong_add_nat)
     apply (rule cong_scalar2_nat)
@@ -830,7 +803,7 @@
     apply (rule cong_scalar2_nat)
     apply (rule `[b2 = 1] (mod m2)`)
     done
-  hence "[?x = u2] (mod m2)" by simp
+  then have "[?x = u2] (mod m2)" by simp
   with `[?x = u1] (mod m1)` show ?thesis by blast
 qed
 
@@ -850,7 +823,7 @@
     apply (rule cong_scalar2_int)
     apply (rule `[b2 = 0] (mod m1)`)
     done
-  hence "[?x = u1] (mod m1)" by simp
+  then have "[?x = u1] (mod m1)" by simp
   have "[?x = u1 * 0 + u2 * 1] (mod m2)"
     apply (rule cong_add_int)
     apply (rule cong_scalar2_int)
@@ -858,42 +831,42 @@
     apply (rule cong_scalar2_int)
     apply (rule `[b2 = 1] (mod m2)`)
     done
-  hence "[?x = u2] (mod m2)" by simp
+  then have "[?x = u2] (mod m2)" by simp
   with `[?x = u1] (mod m1)` show ?thesis by blast
 qed
 
-lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow> 
+lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow>
     [x = y] (mod m)"
-  apply (case_tac "y \<le> x")
+  apply (cases "y \<le> x")
   apply (simp add: cong_altdef_nat)
   apply (erule dvd_mult_left)
   apply (rule cong_sym_nat)
   apply (subst (asm) cong_sym_eq_nat)
-  apply (simp add: cong_altdef_nat) 
+  apply (simp add: cong_altdef_nat)
   apply (erule dvd_mult_left)
-done
+  done
 
-lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow> 
+lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow>
     [x = y] (mod m)"
-  apply (simp add: cong_altdef_int) 
+  apply (simp add: cong_altdef_int)
   apply (erule dvd_mult_left)
-done
+  done
 
-lemma cong_less_modulus_unique_nat: 
+lemma cong_less_modulus_unique_nat:
     "[(x::nat) = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y"
   by (simp add: cong_nat_def)
 
 lemma binary_chinese_remainder_unique_nat:
-  assumes a: "coprime (m1::nat) m2" and
-         nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
+  assumes a: "coprime (m1::nat) m2"
+    and nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
   shows "EX! x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
 proof -
-  from binary_chinese_remainder_nat [OF a] obtain y where 
+  from binary_chinese_remainder_nat [OF a] obtain y where
       "[y = u1] (mod m1)" and "[y = u2] (mod m2)"
     by blast
   let ?x = "y mod (m1 * m2)"
   from nz have less: "?x < m1 * m2"
-    by auto   
+    by auto
   have one: "[?x = u1] (mod m1)"
     apply (rule cong_trans_nat)
     prefer 2
@@ -911,9 +884,8 @@
     apply (rule cong_mod_nat)
     using nz apply auto
     done
-  have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow>
-      z = ?x"
-  proof (clarify)
+  have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow> z = ?x"
+  proof clarify
     fix z
     assume "z < m1 * m2"
     assume "[z = u1] (mod m1)" and  "[z = u2] (mod m2)"
@@ -935,46 +907,43 @@
       apply (intro cong_less_modulus_unique_nat)
       apply (auto, erule cong_sym_nat)
       done
-  qed  
-  with less one two show ?thesis
-    by auto
+  qed
+  with less one two show ?thesis by auto
  qed
 
 lemma chinese_remainder_aux_nat:
-  fixes A :: "'a set" and
-        m :: "'a \<Rightarrow> nat"
-  assumes fin: "finite A" and
-          cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
-  shows "EX b. (ALL i : A. 
-      [b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))"
+  fixes A :: "'a set"
+    and m :: "'a \<Rightarrow> nat"
+  assumes fin: "finite A"
+    and cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
+  shows "EX b. (ALL i : A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))"
 proof (rule finite_set_choice, rule fin, rule ballI)
   fix i
   assume "i : A"
   with cop have "coprime (PROD j : A - {i}. m j) (m i)"
     by (intro setprod_coprime_nat, auto)
-  hence "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
+  then have "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
     by (elim cong_solve_coprime_nat)
   then obtain x where "[(PROD j : A - {i}. m j) * x = 1] (mod m i)"
     by auto
-  moreover have "[(PROD j : A - {i}. m j) * x = 0] 
+  moreover have "[(PROD j : A - {i}. m j) * x = 0]
     (mod (PROD j : A - {i}. m j))"
     by (subst mult_commute, rule cong_mult_self_nat)
-  ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] 
+  ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0]
       (mod setprod m (A - {i}))"
     by blast
 qed
 
 lemma chinese_remainder_nat:
-  fixes A :: "'a set" and
-        m :: "'a \<Rightarrow> nat" and
-        u :: "'a \<Rightarrow> nat"
-  assumes 
-        fin: "finite A" and
-        cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
+  fixes A :: "'a set"
+    and m :: "'a \<Rightarrow> nat"
+    and u :: "'a \<Rightarrow> nat"
+  assumes fin: "finite A"
+    and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
   shows "EX x. (ALL i:A. [x = u i] (mod m i))"
 proof -
   from chinese_remainder_aux_nat [OF fin cop] obtain b where
-    bprop: "ALL i:A. [b i = 1] (mod m i) \<and> 
+    bprop: "ALL i:A. [b i = 1] (mod m i) \<and>
       [b i = 0] (mod (PROD j : A - {i}. m j))"
     by blast
   let ?x = "SUM i:A. (u i) * (b i)"
@@ -982,12 +951,12 @@
   proof (rule exI, clarify)
     fix i
     assume a: "i : A"
-    show "[?x = u i] (mod m i)" 
+    show "[?x = u i] (mod m i)"
     proof -
-      from fin a have "?x = (SUM j:{i}. u j * b j) + 
+      from fin a have "?x = (SUM j:{i}. u j * b j) +
           (SUM j:A-{i}. u j * b j)"
         by (subst setsum_Un_disjoint [symmetric], auto intro: setsum_cong)
-      hence "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)"
+      then have "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)"
         by auto
       also have "[u i * b i + (SUM j:A-{i}. u j * b j) =
                   u i * 1 + (SUM j:A-{i}. u j * 0)] (mod m i)"
@@ -1010,35 +979,34 @@
   qed
 qed
 
-lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow> 
+lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow>
     (ALL i: A. (ALL j: A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
       (ALL i: A. [(x::nat) = y] (mod m i)) \<longrightarrow>
-         [x = y] (mod (PROD i:A. m i))" 
+         [x = y] (mod (PROD i:A. m i))"
   apply (induct set: finite)
   apply auto
   apply (erule (1) coprime_cong_mult_nat)
   apply (subst gcd_commute_nat)
   apply (rule setprod_coprime_nat)
   apply auto
-done
+  done
 
 lemma chinese_remainder_unique_nat:
-  fixes A :: "'a set" and
-        m :: "'a \<Rightarrow> nat" and
-        u :: "'a \<Rightarrow> nat"
-  assumes 
-        fin: "finite A" and
-         nz: "ALL i:A. m i \<noteq> 0" and
-        cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
+  fixes A :: "'a set"
+    and m :: "'a \<Rightarrow> nat"
+    and u :: "'a \<Rightarrow> nat"
+  assumes fin: "finite A"
+    and nz: "ALL i:A. m i \<noteq> 0"
+    and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
   shows "EX! x. x < (PROD i:A. m i) \<and> (ALL i:A. [x = u i] (mod m i))"
 proof -
-  from chinese_remainder_nat [OF fin cop] obtain y where
-      one: "(ALL i:A. [y = u i] (mod m i))" 
+  from chinese_remainder_nat [OF fin cop]
+  obtain y where one: "(ALL i:A. [y = u i] (mod m i))"
     by blast
   let ?x = "y mod (PROD i:A. m i)"
   from fin nz have prodnz: "(PROD i:A. m i) \<noteq> 0"
     by auto
-  hence less: "?x < (PROD i:A. m i)"
+  then have less: "?x < (PROD i:A. m i)"
     by auto
   have cong: "ALL i:A. [?x = u i] (mod m i)"
     apply auto
@@ -1052,28 +1020,29 @@
     apply (rule fin)
     apply assumption
     done
-  have unique: "ALL z. z < (PROD i:A. m i) \<and> 
+  have unique: "ALL z. z < (PROD i:A. m i) \<and>
       (ALL i:A. [z = u i] (mod m i)) \<longrightarrow> z = ?x"
   proof (clarify)
     fix z
     assume zless: "z < (PROD i:A. m i)"
     assume zcong: "(ALL i:A. [z = u i] (mod m i))"
     have "ALL i:A. [?x = z] (mod m i)"
-      apply clarify     
+      apply clarify
       apply (rule cong_trans_nat)
       using cong apply (erule bspec)
       apply (rule cong_sym_nat)
       using zcong apply auto
       done
     with fin cop have "[?x = z] (mod (PROD i:A. m i))"
-      by (intro coprime_cong_prod_nat, auto)
+      apply (intro coprime_cong_prod_nat)
+      apply auto
+      done
     with zless less show "z = ?x"
       apply (intro cong_less_modulus_unique_nat)
       apply (auto, erule cong_sym_nat)
       done
-  qed 
-  from less cong unique show ?thesis
-    by blast  
+  qed
+  from less cong unique show ?thesis by blast
 qed
 
 end
diff -r fbfdc5ac86be -r a98ef45122f3 src/HOL/Number_Theory/Fib.thy
--- a/src/HOL/Number_Theory/Fib.thy	Sat Sep 10 22:11:55 2011 +0200
+++ b/src/HOL/Number_Theory/Fib.thy	Sat Sep 10 23:27:32 2011 +0200
@@ -18,48 +18,40 @@
 subsection {* Main definitions *}
 
 class fib =
-
-fixes 
-  fib :: "'a \<Rightarrow> 'a"
+  fixes fib :: "'a \<Rightarrow> 'a"
 
 
 (* definition for the natural numbers *)
 
 instantiation nat :: fib
-
-begin 
+begin
 
-fun 
-  fib_nat :: "nat \<Rightarrow> nat"
+fun fib_nat :: "nat \<Rightarrow> nat"
 where
   "fib_nat n =
    (if n = 0 then 0 else
    (if n = 1 then 1 else
      fib (n - 1) + fib (n - 2)))"
 
-instance proof qed
+instance ..
 
 end
 
 (* definition for the integers *)
 
 instantiation int :: fib
-
-begin 
+begin
 
-definition
-  fib_int :: "int \<Rightarrow> int"
-where  
-  "fib_int n = (if n >= 0 then int (fib (nat n)) else 0)"
+definition fib_int :: "int \<Rightarrow> int"
+  where "fib_int n = (if n >= 0 then int (fib (nat n)) else 0)"
 
-instance proof qed
+instance ..
 
 end
 
 
 subsection {* Set up Transfer *}
 
-
 lemma transfer_nat_int_fib:
   "(x::int) >= 0 \<Longrightarrow> fib (nat x) = nat (fib x)"
   unfolding fib_int_def by auto
@@ -68,18 +60,16 @@
   "n >= (0::int) \<Longrightarrow> fib n >= 0"
   by (auto simp add: fib_int_def)
 
-declare transfer_morphism_nat_int[transfer add return: 
+declare transfer_morphism_nat_int[transfer add return:
     transfer_nat_int_fib transfer_nat_int_fib_closure]
 
-lemma transfer_int_nat_fib:
-  "fib (int n) = int (fib n)"
+lemma transfer_int_nat_fib: "fib (int n) = int (fib n)"
   unfolding fib_int_def by auto
 
-lemma transfer_int_nat_fib_closure:
-  "is_nat n \<Longrightarrow> fib n >= 0"
+lemma transfer_int_nat_fib_closure: "is_nat n \<Longrightarrow> fib n >= 0"
   unfolding fib_int_def by auto
 
-declare transfer_morphism_int_nat[transfer add return: 
+declare transfer_morphism_int_nat[transfer add return:
     transfer_int_nat_fib transfer_int_nat_fib_closure]
 
 
@@ -123,7 +113,7 @@
 (* the need for One_nat_def is due to the natdiff_cancel_numerals
    procedure *)
 
-lemma fib_induct_nat: "P (0::nat) \<Longrightarrow> P (1::nat) \<Longrightarrow> 
+lemma fib_induct_nat: "P (0::nat) \<Longrightarrow> P (1::nat) \<Longrightarrow>
     (!!n. P n \<Longrightarrow> P (n + 1) \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n"
   apply (atomize, induct n rule: nat_less_induct)
   apply auto
@@ -137,7 +127,7 @@
   apply (auto simp add: One_nat_def) (* again, natdiff_cancel *)
 done
 
-lemma fib_add_nat: "fib ((n::nat) + k + 1) = fib (k + 1) * fib (n + 1) + 
+lemma fib_add_nat: "fib ((n::nat) + k + 1) = fib (k + 1) * fib (n + 1) +
     fib k * fib n"
   apply (induct n rule: fib_induct_nat)
   apply auto
@@ -148,26 +138,24 @@
 (* hmmm. Why doesn't "n + (1 + (1 + k))" simplify to "n + k + 2"? *)
   apply (subgoal_tac "n + (k + 2) = n + (1 + (1 + k))")
   apply (erule ssubst) back back
-  apply (erule ssubst) back 
+  apply (erule ssubst) back
   apply auto
 done
 
-lemma fib_add'_nat: "fib (n + Suc k) = fib (Suc k) * fib (Suc n) + 
-    fib k * fib n"
+lemma fib_add'_nat: "fib (n + Suc k) =
+    fib (Suc k) * fib (Suc n) + fib k * fib n"
   using fib_add_nat by (auto simp add: One_nat_def)
 
 
 (* transfer from nats to ints *)
-lemma fib_add_int [rule_format]: "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow>
-    fib (n + k + 1) = fib (k + 1) * fib (n + 1) + 
-    fib k * fib n "
-
+lemma fib_add_int: "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow>
+    fib (n + k + 1) = fib (k + 1) * fib (n + 1) +  fib k * fib n "
   by (rule fib_add_nat [transferred])
 
 lemma fib_neq_0_nat: "(n::nat) > 0 \<Longrightarrow> fib n ~= 0"
   apply (induct n rule: fib_induct_nat)
   apply (auto simp add: fib_plus_2_nat)
-done
+  done
 
 lemma fib_gr_0_nat: "(n::nat) > 0 \<Longrightarrow> fib n > 0"
   by (frule fib_neq_0_nat, simp)
@@ -180,21 +168,20 @@
   much easier using integers, not natural numbers!
 *}
 
-lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n) - 
+lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n) -
     (fib (int n + 1))^2 = (-1)^(n + 1)"
   apply (induct n)
-  apply (auto simp add: field_simps power2_eq_square fib_reduce_int
-      power_add)
-done
+  apply (auto simp add: field_simps power2_eq_square fib_reduce_int power_add)
+  done
 
-lemma fib_Cassini_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n - 
+lemma fib_Cassini_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n -
     (fib (n + 1))^2 = (-1)^(nat n + 1)"
   by (insert fib_Cassini_aux_int [of "nat n"], auto)
 
 (*
-lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n = 
+lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n =
     (fib (n + 1))^2 + (-1)^(nat n + 1)"
-  by (frule fib_Cassini_int, simp) 
+  by (frule fib_Cassini_int, simp)
 *)
 
 lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib ((n::int) + 2) * fib n =
@@ -204,12 +191,11 @@
   apply (subst tsub_eq)
   apply (insert fib_gr_0_int [of "n + 1"], force)
   apply auto
-done
+  done
 
 lemma fib_Cassini_nat: "fib ((n::nat) + 2) * fib n =
-  (if even n then (fib (n + 1))^2 - 1
-   else (fib (n + 1))^2 + 1)"
-
+    (if even n then (fib (n + 1))^2 - 1
+     else (fib (n + 1))^2 + 1)"
   by (rule fib_Cassini'_int [transferred, of n], auto)
 
 
@@ -222,13 +208,12 @@
   apply (auto simp add: Suc_eq_plus1) (* again, natdiff_cancel *)
   apply (subst add_commute, auto)
   apply (subst gcd_commute_nat, auto simp add: field_simps)
-done
+  done
 
 lemma coprime_fib_Suc_nat: "coprime (fib n) (fib (Suc n))"
   using coprime_fib_plus_1_nat by (simp add: One_nat_def)
 
-lemma coprime_fib_plus_1_int: 
-    "n >= 0 \<Longrightarrow> coprime (fib (n::int)) (fib (n + 1))"
+lemma coprime_fib_plus_1_int: "n >= 0 \<Longrightarrow> coprime (fib (n::int)) (fib (n + 1))"
   by (erule coprime_fib_plus_1_nat [transferred])
 
 lemma gcd_fib_add_nat: "gcd (fib (m::nat)) (fib (n + m)) = gcd (fib m) (fib n)"
@@ -243,51 +228,53 @@
   apply (subst gcd_commute_nat)
   apply (rule gcd_mult_cancel_nat)
   apply (rule coprime_fib_plus_1_nat)
-done
+  done
 
-lemma gcd_fib_add_int [rule_format]: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow> 
+lemma gcd_fib_add_int [rule_format]: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
     gcd (fib (m::int)) (fib (n + m)) = gcd (fib m) (fib n)"
   by (erule gcd_fib_add_nat [transferred])
 
-lemma gcd_fib_diff_nat: "(m::nat) \<le> n \<Longrightarrow> 
+lemma gcd_fib_diff_nat: "(m::nat) \<le> n \<Longrightarrow>
     gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
   by (simp add: gcd_fib_add_nat [symmetric, of _ "n-m"])
 
-lemma gcd_fib_diff_int: "0 <= (m::int) \<Longrightarrow> m \<le> n \<Longrightarrow> 
+lemma gcd_fib_diff_int: "0 <= (m::int) \<Longrightarrow> m \<le> n \<Longrightarrow>
     gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
   by (simp add: gcd_fib_add_int [symmetric, of _ "n-m"])
 
-lemma gcd_fib_mod_nat: "0 < (m::nat) \<Longrightarrow> 
+lemma gcd_fib_mod_nat: "0 < (m::nat) \<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 note m_n = True
-    then have m_n': "m \<le> n" by auto
+    case True
+    then have "m \<le> n" by auto
     with pos_m have pos_n: "0 < n" by auto
-    with pos_m m_n have diff: "n - m < n" by auto
+    with pos_m `m < n` 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 m_n, auto)
-    also have "\<dots> = gcd (fib m)  (fib (n - m))" 
+      by (simp add: mod_if [of n]) (insert `m < n`, auto)
+    also have "\<dots> = gcd (fib m)  (fib (n - m))"
       by (simp add: less.hyps diff pos_m)
-    also have "\<dots> = gcd (fib m) (fib n)" by (simp add: gcd_fib_diff_nat m_n')
+    also have "\<dots> = gcd (fib m) (fib n)"
+      by (simp add: gcd_fib_diff_nat `m \<le> n`)
     finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
   next
-    case False then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
-    by (cases "m = n") auto
+    case False
+    then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
+      by (cases "m = n") auto
   qed
 qed
 
-lemma gcd_fib_mod_int: 
+lemma gcd_fib_mod_int:
   assumes "0 < (m::int)" and "0 <= n"
   shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
   apply (rule gcd_fib_mod_nat [transferred])
   using assms apply auto
   done
 
-lemma fib_gcd_nat: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)"  
+lemma fib_gcd_nat: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)"
     -- {* Law 6.111 *}
   apply (induct m n rule: gcd_nat_induct)
   apply (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod_nat)
@@ -297,7 +284,7 @@
     fib (gcd (m::int) n) = gcd (fib m) (fib n)"
   by (erule fib_gcd_nat [transferred])
 
-lemma atMost_plus_one_nat: "{..(k::nat) + 1} = insert (k + 1) {..k}" 
+lemma atMost_plus_one_nat: "{..(k::nat) + 1} = insert (k + 1) {..k}"
   by auto
 
 theorem fib_mult_eq_setsum_nat:
diff -r fbfdc5ac86be -r a98ef45122f3 src/HOL/Number_Theory/MiscAlgebra.thy
--- a/src/HOL/Number_Theory/MiscAlgebra.thy	Sat Sep 10 22:11:55 2011 +0200
+++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Sat Sep 10 23:27:32 2011 +0200
@@ -12,7 +12,7 @@
 
 (* finiteness stuff *)
 
-lemma bounded_set1_int [intro]: "finite {(x::int). a < x & x < b & P x}" 
+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
@@ -64,7 +64,7 @@
   apply auto
   apply (rule_tac x = "inv x" in bexI)
   apply auto
-done
+  done
 
 lemma (in comm_monoid) units_comm_group: "comm_group(units_of G)"
   apply (rule group.group_comm_groupI)
@@ -75,15 +75,15 @@
   done
 
 lemma units_of_carrier: "carrier (units_of G) = Units G"
-  by (unfold units_of_def, auto)
+  unfolding units_of_def by auto
 
 lemma units_of_mult: "mult(units_of G) = mult G"
-  by (unfold units_of_def, auto)
+  unfolding units_of_def by auto
 
 lemma units_of_one: "one(units_of G) = one G"
-  by (unfold units_of_def, auto)
+  unfolding units_of_def by auto
 
-lemma (in monoid) units_of_inv: "x : Units G ==> 
+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)
@@ -105,12 +105,12 @@
   apply (erule group.l_inv, assumption)
 done
 
-lemma (in group) inj_on_const_mult: "a: (carrier G) ==> 
+lemma (in group) inj_on_const_mult: "a: (carrier G) ==>
     inj_on (%x. a \<otimes> x) (carrier G)"
-  by (unfold inj_on_def, auto)
+  unfolding inj_on_def by auto
 
 lemma (in group) surj_const_mult: "a : (carrier G) ==>
-    (%x. a \<otimes> x) ` (carrier G) = (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
@@ -118,7 +118,7 @@
    for mult_ac rewriting. *)
   apply (subst m_assoc [symmetric])
   apply auto
-done
+  done
 
 lemma (in group) l_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
     (x \<otimes> a = x) = (a = one G)"
@@ -127,7 +127,7 @@
   prefer 4
   apply (erule ssubst)
   apply auto
-done
+  done
 
 lemma (in group) r_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
     (a \<otimes> x = x) = (a = one G)"
@@ -136,28 +136,32 @@
   prefer 4
   apply (erule ssubst)
   apply auto
-done
+  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)"
-  by (subst eq_commute, simp)
+  apply (subst eq_commute)
+  apply simp
+  done
 
 lemma (in group) r_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
     (x = a \<otimes> x) = (a = one G)"
-  by (subst eq_commute, simp)
+  apply (subst eq_commute)
+  apply simp
+  done
 
 (* This should be generalized to arbitrary groups, not just commutative
    ones, using Lagrange's theorem. *)
 
 lemma (in comm_group) power_order_eq_one:
-    assumes fin [simp]: "finite (carrier G)"
-        and a [simp]: "a : carrier G" 
-      shows "a (^) card(carrier G) = one G" 
+  assumes fin [simp]: "finite (carrier G)"
+    and a [simp]: "a : carrier G"
+  shows "a (^) card(carrier G) = one G"
 proof -
   have "(\<Otimes>x:carrier G. x) = (\<Otimes>x:carrier G. a \<otimes> x)"
-    by (subst (2) finprod_reindex [symmetric], 
+    by (subst (2) finprod_reindex [symmetric],
       auto simp add: Pi_def inj_on_const_mult surj_const_mult)
   also have "\<dots> = (\<Otimes>x:carrier G. a) \<otimes> (\<Otimes>x:carrier G. x)"
     by (auto simp add: finprod_multf Pi_def)
@@ -178,7 +182,7 @@
   apply (rule trans)
   apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
   apply assumption
-  apply (subst m_assoc) 
+  apply (subst m_assoc)
   apply auto
   apply (unfold Units_def)
   apply auto
@@ -200,20 +204,20 @@
   x \<otimes> y = \<one> \<Longrightarrow> inv x = y"
   apply (rule inv_char)
   apply auto
-  apply (subst m_comm, auto) 
+  apply (subst m_comm, auto)
   done
 
-lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"  
+lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"
   apply (rule inv_char)
   apply (auto simp add: l_minus r_minus)
   done
 
-lemma (in monoid) inv_eq_imp_eq: "x : Units G \<Longrightarrow> y : Units G \<Longrightarrow> 
+lemma (in monoid) inv_eq_imp_eq: "x : Units G \<Longrightarrow> y : Units G \<Longrightarrow>
     inv x = inv y \<Longrightarrow> x = y"
   apply (subgoal_tac "inv(inv x) = inv(inv y)")
   apply (subst (asm) Units_inv_inv)+
   apply auto
-done
+  done
 
 lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> : Units R"
   apply (unfold Units_def)
@@ -221,24 +225,24 @@
   apply (rule_tac x = "\<ominus> \<one>" in bexI)
   apply auto
   apply (simp add: l_minus r_minus)
-done
+  done
 
 lemma (in monoid) inv_one [simp]: "inv \<one> = \<one>"
   apply (rule inv_char)
   apply auto
-done
+  done
 
 lemma (in ring) inv_eq_neg_one_eq: "x : Units R \<Longrightarrow> (inv x = \<ominus> \<one>) = (x = \<ominus> \<one>)"
   apply auto
   apply (subst Units_inv_inv [symmetric])
   apply auto
-done
+  done
 
 lemma (in monoid) inv_eq_one_eq: "x : Units G \<Longrightarrow> (inv x = \<one>) = (x = \<one>)"
   apply auto
   apply (subst Units_inv_inv [symmetric])
   apply auto
-done
+  done
 
 
 (* This goes in FiniteProduct *)
@@ -256,29 +260,28 @@
   apply (erule finite_UN_I)
   apply blast
   apply (fastsimp)
-  apply (auto intro!: funcsetI finprod_closed) 
-done
+  apply (auto intro!: funcsetI finprod_closed)
+  done
 
 lemma (in comm_monoid) finprod_Union_disjoint:
   "[| finite C; (ALL A:C. finite A & (ALL x:A. f x : carrier G));
-      (ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |] 
-   ==> finprod G f (Union C) = finprod G (finprod G f) C" 
+      (ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |]
+   ==> finprod G f (Union C) = finprod G (finprod G f) C"
   apply (frule finprod_UN_disjoint [of C id f])
   apply (auto simp add: SUP_def)
-done
+  done
 
-lemma (in comm_monoid) finprod_one [rule_format]: 
-  "finite A \<Longrightarrow> (ALL x:A. f x = \<one>) \<longrightarrow>
-     finprod G f A = \<one>"
-by (induct set: finite) auto
+lemma (in comm_monoid) finprod_one:
+    "finite A \<Longrightarrow> (\<And>x. x:A \<Longrightarrow> f x = \<one>) \<Longrightarrow> finprod G f A = \<one>"
+  by (induct set: finite) auto
 
 
 (* 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"
-  apply (subgoal_tac "\<ominus> y = \<zero> \<oplus> \<ominus> y") 
+    "x : carrier R \<Longrightarrow> y : carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
+  apply (subgoal_tac "\<ominus> y = \<zero> \<oplus> \<ominus> y")
   apply (erule ssubst)back
   apply (erule subst)
   apply (simp_all add: ring_simprules)
@@ -287,7 +290,7 @@
 (* there's a name conflict -- maybe "domain" should be
    "integral_domain" *)
 
-lemma (in Ring.domain) square_eq_one: 
+lemma (in Ring.domain) square_eq_one:
   fixes x
   assumes [simp]: "x : carrier R" and
     "x \<otimes> x = \<one>"
@@ -298,15 +301,15 @@
   also with `x \<otimes> x = \<one>` have "\<dots> = \<zero>"
     by (simp add: ring_simprules)
   finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
-  hence "(x \<oplus> \<one>) = \<zero> | (x \<oplus> \<ominus> \<one>) = \<zero>"
+  then have "(x \<oplus> \<one>) = \<zero> | (x \<oplus> \<ominus> \<one>) = \<zero>"
     by (intro integral, auto)
-  thus ?thesis
+  then show ?thesis
     apply auto
     apply (erule notE)
     apply (rule sum_zero_eq_neg)
     apply auto
     apply (subgoal_tac "x = \<ominus> (\<ominus> \<one>)")
-    apply (simp add: ring_simprules) 
+    apply (simp add: ring_simprules)
     apply (rule sum_zero_eq_neg)
     apply auto
     done
@@ -318,7 +321,7 @@
   apply auto
   apply (erule ssubst)back
   apply (erule Units_r_inv)
-done
+  done
 
 
 (*
@@ -327,15 +330,15 @@
   needed.)
 *)
 
-lemma (in ring) finite_ring_finite_units [intro]: "finite (carrier R) \<Longrightarrow> 
-    finite (Units R)"
-  by (rule finite_subset, auto)
+lemma (in ring) finite_ring_finite_units [intro]:
+    "finite (carrier R) \<Longrightarrow> finite (Units R)"
+  by (rule finite_subset) auto
 
 (* this belongs with MiscAlgebra.thy *)
-lemma (in monoid) units_of_pow: 
+lemma (in monoid) units_of_pow:
     "x : Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> (n::nat) = x (^)\<^bsub>G\<^esub> n"
   apply (induct n)
-  apply (auto simp add: units_group group.is_monoid  
+  apply (auto simp add: units_group group.is_monoid
     monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)
   done
 
diff -r fbfdc5ac86be -r a98ef45122f3 src/HOL/Number_Theory/Primes.thy
--- a/src/HOL/Number_Theory/Primes.thy	Sat Sep 10 22:11:55 2011 +0200
+++ b/src/HOL/Number_Theory/Primes.thy	Sat Sep 10 23:27:32 2011 +0200
@@ -31,54 +31,41 @@
 imports "~~/src/HOL/GCD"
 begin
 
-declare One_nat_def [simp del]
-
 class prime = one +
-
-fixes
-  prime :: "'a \<Rightarrow> bool"
+  fixes prime :: "'a \<Rightarrow> bool"
 
 instantiation nat :: prime
-
 begin
 
-definition
-  prime_nat :: "nat \<Rightarrow> bool"
-where
-  "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
+definition prime_nat :: "nat \<Rightarrow> bool"
+  where "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
 
-instance proof qed
+instance ..
 
 end
 
 instantiation int :: prime
-
 begin
 
-definition
-  prime_int :: "int \<Rightarrow> bool"
-where
-  "prime_int p = prime (nat p)"
+definition prime_int :: "int \<Rightarrow> bool"
+  where "prime_int p = prime (nat p)"
 
-instance proof qed
+instance ..
 
 end
 
 
 subsection {* Set up Transfer *}
 
-
 lemma transfer_nat_int_prime:
   "(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
-  unfolding gcd_int_def lcm_int_def prime_int_def
-  by auto
+  unfolding gcd_int_def lcm_int_def prime_int_def by auto
 
 declare transfer_morphism_nat_int[transfer add return:
     transfer_nat_int_prime]
 
-lemma transfer_int_nat_prime:
-  "prime (int x) = prime x"
-  by (unfold gcd_int_def lcm_int_def prime_int_def, auto)
+lemma transfer_int_nat_prime: "prime (int x) = prime x"
+  unfolding gcd_int_def lcm_int_def prime_int_def by auto
 
 declare transfer_morphism_int_nat[transfer add return:
     transfer_int_nat_prime]
@@ -94,52 +81,54 @@
   unfolding prime_int_def
   apply (frule prime_odd_nat)
   apply (auto simp add: even_nat_def)
-done
+  done
 
 (* FIXME Is there a better way to handle these, rather than making them elim rules? *)
 
 lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
-  by (unfold prime_nat_def, auto)
+  unfolding prime_nat_def by auto
 
 lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
-  by (unfold prime_nat_def, auto)
+  unfolding prime_nat_def by auto
 
 lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
-  by (unfold prime_nat_def, auto)
+  unfolding prime_nat_def by auto
 
 lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
-  by (unfold prime_nat_def, auto)
+  unfolding prime_nat_def by auto
 
 lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
-  by (unfold prime_nat_def, auto)
+  unfolding prime_nat_def by auto
 
 lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
-  by (unfold prime_nat_def, auto)
+  unfolding prime_nat_def by auto
 
 lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
-  by (unfold prime_nat_def, auto)
+  unfolding prime_nat_def by auto
 
 lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
-  by (unfold prime_int_def prime_nat_def) auto
+  unfolding prime_int_def prime_nat_def by auto
 
 lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
-  by (unfold prime_int_def prime_nat_def, auto)
+  unfolding prime_int_def prime_nat_def by auto
 
 lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
-  by (unfold prime_int_def prime_nat_def, auto)
+  unfolding prime_int_def prime_nat_def by auto
 
 lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1"
-  by (unfold prime_int_def prime_nat_def, auto)
+  unfolding prime_int_def prime_nat_def by auto
 
 lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
-  by (unfold prime_int_def prime_nat_def, auto)
+  unfolding prime_int_def prime_nat_def by auto
 
 
 lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
     m = 1 \<or> m = p))"
   using prime_nat_def [transferred]
-    apply (case_tac "p >= 0")
-    by (blast, auto simp add: prime_ge_0_int)
+  apply (cases "p >= 0")
+  apply blast
+  apply (auto simp add: prime_ge_0_int)
+  done
 
 lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
   apply (unfold prime_nat_def)
@@ -168,26 +157,29 @@
 lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
   unfolding prime_nat_def dvd_def apply auto
-  by(metis mult_commute linorder_neq_iff linorder_not_le mult_1 n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
+  by (metis mult_commute linorder_neq_iff linorder_not_le mult_1
+      n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
 
 lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
   unfolding prime_int_altdef dvd_def
   apply auto
-  by(metis div_mult_self1_is_id div_mult_self2_is_id int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos less_le)
+  by (metis div_mult_self1_is_id div_mult_self2_is_id
+      int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos less_le)
 
 lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
     n > 0 --> (p dvd x^n --> p dvd x)"
-  by (induct n rule: nat_induct, auto)
+  by (induct n rule: nat_induct) auto
 
 lemma prime_dvd_power_int [rule_format]: "prime (p::int) -->
     n > 0 --> (p dvd x^n --> p dvd x)"
-  apply (induct n rule: nat_induct, auto)
+  apply (induct n rule: nat_induct)
+  apply auto
   apply (frule prime_ge_0_int)
   apply auto
-done
+  done
 
-subsubsection{* Make prime naively executable *}
+subsubsection {* Make prime naively executable *}
 
 lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
   by (simp add: prime_nat_def)
@@ -205,89 +197,87 @@
   by (simp add: prime_int_def)
 
 lemma prime_nat_code [code]:
- "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
-apply (simp add: Ball_def)
-apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
-done
+    "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
+  apply (simp add: Ball_def)
+  apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
+  done
 
 lemma prime_nat_simp:
- "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
-by (auto simp add: prime_nat_code)
+    "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
+  by (auto simp add: prime_nat_code)
 
 lemmas prime_nat_simp_number_of [simp] = prime_nat_simp [of "number_of m", standard]
 
 lemma prime_int_code [code]:
   "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
 proof
-  assume "?L" thus "?R"
+  assume "?L"
+  then show "?R"
     by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef less_le)
 next
-    assume "?R" thus "?L" by (clarsimp simp:Ball_def) (metis dvdI not_prime_eq_prod_int)
+  assume "?R"
+  then show "?L" by (clarsimp simp: Ball_def) (metis dvdI not_prime_eq_prod_int)
 qed
 
-lemma prime_int_simp:
-  "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)"
-by (auto simp add: prime_int_code)
+lemma prime_int_simp: "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)"
+  by (auto simp add: prime_int_code)
 
 lemmas prime_int_simp_number_of [simp] = prime_int_simp [of "number_of m", standard]
 
 lemma two_is_prime_nat [simp]: "prime (2::nat)"
-by simp
+  by simp
 
 lemma two_is_prime_int [simp]: "prime (2::int)"
-by simp
+  by simp
 
 text{* A bit of regression testing: *}
 
-lemma "prime(97::nat)"
-by simp
-
-lemma "prime(97::int)"
-by simp
-
-lemma "prime(997::nat)"
-by eval
-
-lemma "prime(997::int)"
-by eval
+lemma "prime(97::nat)" by simp
+lemma "prime(97::int)" by simp
+lemma "prime(997::nat)" by eval
+lemma "prime(997::int)" by eval
 
 
 lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   apply (rule coprime_exp_nat)
   apply (subst gcd_commute_nat)
   apply (erule (1) prime_imp_coprime_nat)
-done
+  done
 
 lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   apply (rule coprime_exp_int)
   apply (subst gcd_commute_int)
   apply (erule (1) prime_imp_coprime_int)
-done
+  done
 
 lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   apply (rule prime_imp_coprime_nat, assumption)
-  apply (unfold prime_nat_def, auto)
-done
+  apply (unfold prime_nat_def)
+  apply auto
+  done
 
 lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   apply (rule prime_imp_coprime_int, assumption)
   apply (unfold prime_int_altdef)
   apply (metis int_one_le_iff_zero_less less_le)
-done
+  done
 
-lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
+lemma primes_imp_powers_coprime_nat:
+    "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
   by (rule coprime_exp2_nat, rule primes_coprime_nat)
 
-lemma primes_imp_powers_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
+lemma primes_imp_powers_coprime_int:
+    "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
   by (rule coprime_exp2_int, rule primes_coprime_int)
 
 lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
   apply (induct n rule: nat_less_induct)
   apply (case_tac "n = 0")
-  using two_is_prime_nat apply blast
-  apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat nat_dvd_not_less 
-               neq0_conv prime_nat_def)
-done
+  using two_is_prime_nat
+  apply blast
+  apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat
+    nat_dvd_not_less neq0_conv prime_nat_def)
+  done
 
 (* An Isar version:
 
@@ -301,7 +291,7 @@
   fix n :: nat
   assume "n ~= 1" and
     ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
-  thus "\<exists>p. prime p \<and> p dvd n"
+  then show "\<exists>p. prime p \<and> p dvd n"
   proof -
   {
     assume "n = 0"
@@ -312,7 +302,7 @@
   moreover
   {
     assume "prime n"
-    hence ?thesis by auto
+    then have ?thesis by auto
   }
   moreover
   {
@@ -335,13 +325,14 @@
   assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
   shows "p^n dvd a \<or> p^n dvd b"
 proof-
-  {assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
+  { assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
       apply (cases "n=0", simp_all)
-      apply (cases "a=1", simp_all) done}
+      apply (cases "a=1", simp_all)
+      done }
   moreover
-  {assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
-    then obtain m where m: "n = Suc m" by (cases n, auto)
-    from n have "p dvd p^n" by (intro dvd_power, auto)
+  { assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
+    then obtain m where m: "n = Suc m" by (cases n) auto
+    from n have "p dvd p^n" apply (intro dvd_power) apply auto done
     also note pab
     finally have pab': "p dvd a * b".
     from prime_dvd_mult_nat[OF p pab']
@@ -351,7 +342,7 @@
       from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
       with p have "coprime b p"
         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
-      hence pnb: "coprime (p^n) b"
+      then have pnb: "coprime (p^n) b"
         by (subst gcd_commute_nat, rule coprime_exp_nat)
       from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
     moreover
@@ -361,39 +352,39 @@
         by auto
       with p have "coprime a p"
         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
-      hence pna: "coprime (p^n) a"
+      then have pna: "coprime (p^n) a"
         by (subst gcd_commute_nat, rule coprime_exp_nat)
       from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
-    ultimately have ?thesis by blast}
+    ultimately have ?thesis by blast }
   ultimately show ?thesis by blast
 qed
 
+
 subsection {* Infinitely many primes *}
 
 lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
 proof-
   have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith 
   from prime_factor_nat [OF f1]
-      obtain p where "prime p" and "p dvd fact n + 1" by auto
-  hence "p \<le> fact n + 1" 
-    by (intro dvd_imp_le, auto)
-  {assume "p \<le> n"
+  obtain p where "prime p" and "p dvd fact n + 1" by auto
+  then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
+  { assume "p \<le> n"
     from `prime p` have "p \<ge> 1" 
       by (cases p, simp_all)
     with `p <= n` have "p dvd fact n" 
       by (intro dvd_fact_nat)
     with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
       by (rule dvd_diff_nat)
-    hence "p dvd 1" by simp
-    hence "p <= 1" by auto
+    then have "p dvd 1" by simp
+    then have "p <= 1" by auto
     moreover from `prime p` have "p > 1" by auto
     ultimately have False by auto}
-  hence "n < p" by arith
+  then have "n < p" by presburger
   with `prime p` and `p <= fact n + 1` show ?thesis by auto
 qed
 
 lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" 
-using next_prime_bound by auto
+  using next_prime_bound by auto
 
 lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
 proof
@@ -402,8 +393,8 @@
     by auto
   then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
     by auto
-  with bigger_prime [of b] show False by auto
+  with bigger_prime [of b] show False
+    by auto
 qed
 
-
 end
diff -r fbfdc5ac86be -r a98ef45122f3 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Sat Sep 10 22:11:55 2011 +0200
+++ b/src/HOL/Number_Theory/Residues.thy	Sat Sep 10 23:27:32 2011 +0200
@@ -16,14 +16,14 @@
 
 
 (*
- 
+
   A locale for residue rings
 
 *)
 
 definition residue_ring :: "int => int ring" where
-  "residue_ring m == (| 
-    carrier =       {0..m - 1}, 
+  "residue_ring m == (|
+    carrier =       {0..m - 1},
     mult =          (%x y. (x * y) mod m),
     one =           1,
     zero =          0,
@@ -34,7 +34,8 @@
   assumes m_gt_one: "m > 1"
   defines "R == residue_ring m"
 
-context residues begin
+context residues
+begin
 
 lemma abelian_group: "abelian_group R"
   apply (insert m_gt_one)
@@ -79,23 +80,23 @@
 context residues
 begin
 
-(* These lemmas translate back and forth between internal and 
+(* These lemmas translate back and forth between internal and
    external concepts *)
 
 lemma res_carrier_eq: "carrier R = {0..m - 1}"
-  by (unfold R_def residue_ring_def, auto)
+  unfolding R_def residue_ring_def by auto
 
 lemma res_add_eq: "x \<oplus> y = (x + y) mod m"
-  by (unfold R_def residue_ring_def, auto)
+  unfolding R_def residue_ring_def by auto
 
 lemma res_mult_eq: "x \<otimes> y = (x * y) mod m"
-  by (unfold R_def residue_ring_def, auto)
+  unfolding R_def residue_ring_def by auto
 
 lemma res_zero_eq: "\<zero> = 0"
-  by (unfold R_def residue_ring_def, auto)
+  unfolding R_def residue_ring_def by auto
 
 lemma res_one_eq: "\<one> = 1"
-  by (unfold R_def residue_ring_def units_of_def, auto)
+  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}"
   apply (insert m_gt_one)
@@ -127,14 +128,14 @@
   apply auto
   done
 
-lemma finite [iff]: "finite(carrier R)"
+lemma finite [iff]: "finite (carrier R)"
   by (subst res_carrier_eq, auto)
 
-lemma finite_Units [iff]: "finite(Units R)"
+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 
+(* 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. *)
 
 lemma mod_in_carrier [iff]: "a mod m : carrier R"
@@ -143,7 +144,10 @@
   done
 
 lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m"
-  by (unfold R_def residue_ring_def, auto, arith)
+  unfolding R_def residue_ring_def
+  apply auto
+  apply presburger
+  done
 
 lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m"
   apply (unfold R_def residue_ring_def, auto)
@@ -155,13 +159,10 @@
   done
 
 lemma zero_cong: "\<zero> = 0"
-  apply (unfold R_def residue_ring_def, auto)
-  done
+  unfolding R_def residue_ring_def by auto
 
 lemma one_cong: "\<one> = 1 mod m"
-  apply (insert m_gt_one)
-  apply (unfold R_def residue_ring_def, auto)
-  done
+  using m_gt_one unfolding R_def residue_ring_def by auto
 
 (* revise algebra library to use 1? *)
 lemma pow_cong: "(x mod m) (^) n = x^n mod m"
@@ -181,19 +182,19 @@
   apply auto
   done
 
-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:A. f i) mod m"
   apply (induct set: finite)
   apply (auto simp: one_cong mult_cong)
   done
 
 lemma (in residues) sum_cong:
-  "finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (SUM i: A. f i) mod m"
+    "finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (SUM i: A. f i) mod m"
   apply (induct set: finite)
   apply (auto simp: zero_cong add_cong)
   done
 
-lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow> 
+lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow>
     a mod m : Units R"
   apply (subst res_units_eq, auto)
   apply (insert pos_mod_sign [of m a])
@@ -204,10 +205,10 @@
   apply (subst gcd_commute_int, assumption)
   done
 
-lemma res_eq_to_cong: "((a mod m) = (b mod m)) = [a = b] (mod (m::int))" 
+lemma res_eq_to_cong: "((a mod m) = (b mod m)) = [a = b] (mod (m::int))"
   unfolding cong_int_def by auto
 
-(* Simplifying with these will translate a ring equation in R to a 
+(* Simplifying with these will translate a ring equation in R to a
    congruence. *)
 
 lemmas res_to_cong_simps = add_cong mult_cong pow_cong one_cong
@@ -243,13 +244,13 @@
   using p_prime apply auto
   done
 
-context residues_prime begin
+context residues_prime
+begin
 
 lemma is_field: "field R"
   apply (rule cring.field_intro2)
   apply (rule cring)
-  apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq
-    res_units_eq)
+  apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq)
   apply (rule classical)
   apply (erule notE)
   apply (subst gcd_commute_int)
@@ -285,25 +286,24 @@
 
 (* the definition of the phi function *)
 
-definition phi :: "int => nat" where
-  "phi m == card({ x. 0 < x & x < m & gcd x m = 1})" 
+definition phi :: "int => nat"
+  where "phi m = card({ x. 0 < x & x < m & gcd x m = 1})"
 
 lemma phi_zero [simp]: "phi 0 = 0"
   apply (subst phi_def)
-(* Auto hangs here. Once again, where is the simplification rule 
+(* Auto hangs here. Once again, where is the simplification rule
    1 == 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
 
 lemma phi_one [simp]: "phi 1 = 0"
-  apply (auto simp add: phi_def card_eq_0_iff)
-  done
+  by (auto simp add: phi_def card_eq_0_iff)
 
 lemma (in residues) phi_eq: "phi m = card(Units R)"
   by (simp add: phi_def res_units_eq)
 
-lemma (in residues) euler_theorem1: 
+lemma (in residues) euler_theorem1:
   assumes a: "gcd a m = 1"
   shows "[a^phi m = 1] (mod m)"
 proof -
@@ -311,7 +311,7 @@
     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>" 
+  also have "\<dots> = \<one>"
     by (intro units_power_order_eq_one, auto)
   finally show ?thesis
     by (simp add: res_to_cong_simps)
@@ -319,13 +319,13 @@
 
 (* In fact, there is a two line proof!
 
-lemma (in residues) euler_theorem1: 
+lemma (in residues) euler_theorem1:
   assumes a: "gcd a m = 1"
   shows "[a^phi m = 1] (mod m)"
 proof -
   have "(a mod m) (^) (phi m) = \<one>"
     by (simp add: phi_eq units_power_order_eq_one a m_gt_one)
-  thus ?thesis
+  then show ?thesis
     by (simp add: res_to_cong_simps)
 qed
 
@@ -338,7 +338,7 @@
   shows "[a^phi m = 1] (mod m)"
 proof (cases)
   assume "m = 0 | m = 1"
-  thus ?thesis by auto
+  then show ?thesis by auto
 next
   assume "~(m = 0 | m = 1)"
   with assms show ?thesis
@@ -375,8 +375,8 @@
 
 subsection {* Wilson's theorem *}
 
-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 : Units R \<Longrightarrow> y : Units R \<Longrightarrow>
+    {x, inv x} ~= {y, inv y} \<Longrightarrow> {x, inv x} Int {y, inv y} = {}"
   apply auto
   apply (erule notE)
   apply (erule inv_eq_imp_eq)
@@ -390,10 +390,10 @@
   assumes a: "p > 2"
   shows "[fact (p - 1) = - 1] (mod p)"
 proof -
-  let ?InversePairs = "{ {x, inv x} | x. x : Units R - {\<one>, \<ominus> \<one>}}" 
+  let ?InversePairs = "{ {x, inv x} | x. x : Units R - {\<one>, \<ominus> \<one>}}"
   have UR: "Units R = {\<one>, \<ominus> \<one>} Un (Union ?InversePairs)"
     by auto
-  have "(\<Otimes>i: Units R. i) = 
+  have "(\<Otimes>i: Units R. i) =
     (\<Otimes>i: {\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i: Union ?InversePairs. i)"
     apply (subst UR)
     apply (subst finprod_Un_disjoint)
@@ -409,7 +409,7 @@
     apply (frule one_eq_neg_one)
     apply (insert a, force)
     done
-  also have "(\<Otimes>i:(Union ?InversePairs). i) = 
+  also have "(\<Otimes>i:(Union ?InversePairs). i) =
       (\<Otimes>A: ?InversePairs. (\<Otimes>y:A. y))"
     apply (subst finprod_Union_disjoint)
     apply force
@@ -444,8 +444,7 @@
     apply (subst res_prime_units_eq, rule refl)
     done
   finally have "fact (p - 1) mod p = \<ominus> \<one>".
-  thus ?thesis
-    by (simp add: res_to_cong_simps)
+  then show ?thesis by (simp add: res_to_cong_simps)
 qed
 
 lemma wilson_theorem: "prime (p::int) \<Longrightarrow> [fact (p - 1) = - 1] (mod p)"
@@ -457,7 +456,6 @@
   apply (rule residues_prime.wilson_theorem1)
   apply (rule residues_prime.intro)
   apply auto
-done
-
+  done
 
 end
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