# HG changeset patch
# User wenzelm
# Date 1386347625 -3600
# Node ID 8a8e6db7f391fcd4080dd032b34a3edae040324a
# Parent  93f6d33a754e101c0335dd1c02dcb0343d2d06b9
tuned proofs;

diff -r 93f6d33a754e -r 8a8e6db7f391 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Fri Dec 06 09:42:13 2013 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Dec 06 17:33:45 2013 +0100
@@ -53,7 +53,7 @@
 lemma fps_one_nth [simp]: "1 $ n = (if n = 0 then 1 else 0)"
   unfolding fps_one_def by simp
 
-instantiation fps :: (plus)  plus
+instantiation fps :: (plus) plus
 begin
 
 definition fps_plus_def:
@@ -89,7 +89,7 @@
 lemma fps_neg_nth [simp]: "(- f) $ n = - (f $ n)"
   unfolding fps_uminus_def by simp
 
-instantiation fps :: ("{comm_monoid_add, times}")  times
+instantiation fps :: ("{comm_monoid_add, times}") times
 begin
 
 definition fps_times_def:
@@ -312,28 +312,28 @@
 lemma fps_const_neg [simp]: "- (fps_const (c::'a::ring)) = fps_const (- c)"
   by (simp add: fps_ext)
 
-lemma fps_const_add [simp]: "fps_const (c::'a\<Colon>monoid_add) + fps_const d = fps_const (c + d)"
+lemma fps_const_add [simp]: "fps_const (c::'a::monoid_add) + fps_const d = fps_const (c + d)"
   by (simp add: fps_ext)
 
-lemma fps_const_sub [simp]: "fps_const (c::'a\<Colon>group_add) - fps_const d = fps_const (c - d)"
+lemma fps_const_sub [simp]: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)"
   by (simp add: fps_ext)
 
-lemma fps_const_mult[simp]: "fps_const (c::'a\<Colon>ring) * fps_const d = fps_const (c * d)"
+lemma fps_const_mult[simp]: "fps_const (c::'a::ring) * fps_const d = fps_const (c * d)"
   by (simp add: fps_eq_iff fps_mult_nth setsum_0')
 
-lemma fps_const_add_left: "fps_const (c::'a\<Colon>monoid_add) + f =
+lemma fps_const_add_left: "fps_const (c::'a::monoid_add) + f =
     Abs_fps (\<lambda>n. if n = 0 then c + f$0 else f$n)"
   by (simp add: fps_ext)
 
-lemma fps_const_add_right: "f + fps_const (c::'a\<Colon>monoid_add) =
+lemma fps_const_add_right: "f + fps_const (c::'a::monoid_add) =
     Abs_fps (\<lambda>n. if n = 0 then f$0 + c else f$n)"
   by (simp add: fps_ext)
 
-lemma fps_const_mult_left: "fps_const (c::'a\<Colon>semiring_0) * f = Abs_fps (\<lambda>n. c * f$n)"
+lemma fps_const_mult_left: "fps_const (c::'a::semiring_0) * f = Abs_fps (\<lambda>n. c * f$n)"
   unfolding fps_eq_iff fps_mult_nth
   by (simp add: fps_const_def mult_delta_left setsum_delta)
 
-lemma fps_const_mult_right: "f * fps_const (c::'a\<Colon>semiring_0) = Abs_fps (\<lambda>n. f$n * c)"
+lemma fps_const_mult_right: "f * fps_const (c::'a::semiring_0) = Abs_fps (\<lambda>n. f$n * c)"
   unfolding fps_eq_iff fps_mult_nth
   by (simp add: fps_const_def mult_delta_right setsum_delta')
 
@@ -357,8 +357,8 @@
 proof
   fix a b :: "'a fps"
   assume a0: "a \<noteq> 0" and b0: "b \<noteq> 0"
-  then obtain i j where i: "a$i\<noteq>0" "\<forall>k<i. a$k=0"
-    and j: "b$j \<noteq>0" "\<forall>k<j. b$k =0" unfolding fps_nonzero_nth_minimal
+  then obtain i j where i: "a$i\<noteq>0" "\<forall>k<i. a$k=0" and j: "b$j \<noteq>0" "\<forall>k<j. b$k =0"
+    unfolding fps_nonzero_nth_minimal
     by blast+
   have "(a * b) $ (i+j) = (\<Sum>k=0..i+j. a$k * b$(i+j-k))"
     by (rule fps_mult_nth)
@@ -389,13 +389,13 @@
 
 subsection{* The eXtractor series X*}
 
-lemma minus_one_power_iff: "(- (1::'a :: {comm_ring_1})) ^ n = (if even n then 1 else - 1)"
+lemma minus_one_power_iff: "(- (1::'a::comm_ring_1)) ^ n = (if even n then 1 else - 1)"
   by (induct n) auto
 
 definition "X = Abs_fps (\<lambda>n. if n = 1 then 1 else 0)"
 
 lemma X_mult_nth [simp]:
-  "(X * (f :: ('a::semiring_1) fps)) $n = (if n = 0 then 0 else f $ (n - 1))"
+  "(X * (f :: 'a::semiring_1 fps)) $n = (if n = 0 then 0 else f $ (n - 1))"
 proof (cases "n = 0")
   case False
   have "(X * f) $n = (\<Sum>i = 0..n. X $ i * f $ (n - i))"
@@ -409,10 +409,10 @@
 qed
 
 lemma X_mult_right_nth[simp]:
-    "((f :: ('a::comm_semiring_1) fps) * X) $n = (if n = 0 then 0 else f $ (n - 1))"
+    "((f :: 'a::comm_semiring_1 fps) * X) $n = (if n = 0 then 0 else f $ (n - 1))"
   by (metis X_mult_nth mult_commute)
 
-lemma X_power_iff: "X^k = Abs_fps (\<lambda>n. if n = k then (1::'a::comm_ring_1) else 0)"
+lemma X_power_iff: "X^k = Abs_fps (\<lambda>n. if n = k then 1::'a::comm_ring_1 else 0)"
 proof (induct k)
   case 0
   then show ?case by (simp add: X_def fps_eq_iff)
@@ -420,16 +420,16 @@
   case (Suc k)
   {
     fix m
-    have "(X^Suc k) $ m = (if m = 0 then (0::'a) else (X^k) $ (m - 1))"
+    have "(X^Suc k) $ m = (if m = 0 then 0::'a else (X^k) $ (m - 1))"
       by (simp del: One_nat_def)
-    then have "(X^Suc k) $ m = (if m = Suc k then (1::'a) else 0)"
+    then have "(X^Suc k) $ m = (if m = Suc k then 1::'a else 0)"
       using Suc.hyps by (auto cong del: if_weak_cong)
   }
   then show ?case by (simp add: fps_eq_iff)
 qed
 
 lemma X_power_mult_nth:
-    "(X^k * (f :: ('a::comm_ring_1) fps)) $n = (if n < k then 0 else f $ (n - k))"
+    "(X^k * (f :: 'a::comm_ring_1 fps)) $n = (if n < k then 0 else f $ (n - k))"
   apply (induct k arbitrary: n)
   apply simp
   unfolding power_Suc mult_assoc
@@ -438,7 +438,7 @@
   done
 
 lemma X_power_mult_right_nth:
-    "((f :: ('a::comm_ring_1) fps) * X^k) $n = (if n < k then 0 else f $ (n - k))"
+    "((f :: 'a::comm_ring_1 fps) * X^k) $n = (if n < k then 0 else f $ (n - k))"
   by (metis X_power_mult_nth mult_commute)
 
 
@@ -450,15 +450,15 @@
 begin
 
 definition
-  dist_fps_def: "dist (a::'a fps) b =
+  dist_fps_def: "dist (a :: 'a fps) b =
     (if (\<exists>n. a$n \<noteq> b$n) then inverse (2 ^ (LEAST n. a$n \<noteq> b$n)) else 0)"
 
-lemma dist_fps_ge0: "dist (a::'a fps) b \<ge> 0"
+lemma dist_fps_ge0: "dist (a :: 'a fps) b \<ge> 0"
   by (simp add: dist_fps_def)
 
-lemma dist_fps_sym: "dist (a::'a fps) b = dist b a"
+lemma dist_fps_sym: "dist (a :: 'a fps) b = dist b a"
   apply (auto simp add: dist_fps_def)
-  apply (rule cong[OF refl, where x="(\<lambda>n\<Colon>nat. a $ n \<noteq> b $ n)"])
+  apply (rule cong[OF refl, where x="(\<lambda>n. a $ n \<noteq> b $ n)"])
   apply (rule ext)
   apply auto
   done
@@ -550,18 +550,26 @@
 text{* The infinite sums and justification of the notation in textbooks*}
 
 lemma reals_power_lt_ex:
-  assumes xp: "x > 0" and y1: "(y::real) > 1"
+  fixes x y :: real
+  assumes xp: "x > 0"
+    and y1: "y > 1"
   shows "\<exists>k>0. (1/y)^k < x"
 proof -
-  have yp: "y > 0" using y1 by simp
+  have yp: "y > 0"
+    using y1 by simp
   from reals_Archimedean2[of "max 0 (- log y x) + 1"]
-  obtain k::nat where k: "real k > max 0 (- log y x) + 1" by blast
-  from k have kp: "k > 0" by simp
-  from k have "real k > - log y x" by simp
-  then have "ln y * real k > - ln x" unfolding log_def
+  obtain k :: nat where k: "real k > max 0 (- log y x) + 1"
+    by blast
+  from k have kp: "k > 0"
+    by simp
+  from k have "real k > - log y x"
+    by simp
+  then have "ln y * real k > - ln x"
+    unfolding log_def
     using ln_gt_zero_iff[OF yp] y1
-    by (simp add: minus_divide_left field_simps del:minus_divide_left[symmetric])
-  then have "ln y * real k + ln x > 0" by simp
+    by (simp add: minus_divide_left field_simps del: minus_divide_left[symmetric])
+  then have "ln y * real k + ln x > 0"
+    by simp
   then have "exp (real k * ln y + ln x) > exp 0"
     by (simp add: mult_ac)
   then have "y ^ k * x > 1"
@@ -569,17 +577,18 @@
     by simp
   then have "x > (1 / y)^k" using yp
     by (simp add: field_simps nonzero_power_divide)
-  then show ?thesis using kp by blast
+  then show ?thesis
+    using kp by blast
 qed
 
-lemma X_nth[simp]: "X$n = (if n = 1 then 1 else 0)" by (simp add: X_def)
-
-lemma X_power_nth[simp]: "(X^k) $n = (if n = k then 1 else (0::'a::comm_ring_1))"
+lemma X_nth[simp]: "X$n = (if n = 1 then 1 else 0)"
+  by (simp add: X_def)
+
+lemma X_power_nth[simp]: "(X^k) $n = (if n = k then 1 else 0::'a::comm_ring_1)"
   by (simp add: X_power_iff)
 
-
 lemma fps_sum_rep_nth: "(setsum (\<lambda>i. fps_const(a$i)*X^i) {0..m})$n =
-    (if n \<le> m then a$n else (0::'a::comm_ring_1))"
+    (if n \<le> m then a$n else 0::'a::comm_ring_1)"
   apply (auto simp add: fps_setsum_nth cond_value_iff cong del: if_weak_cong)
   apply (simp add: setsum_delta')
   done
@@ -588,13 +597,13 @@
   (is "?s ----> a")
 proof -
   {
-    fix r:: real
+    fix r :: real
     assume rp: "r > 0"
     have th0: "(2::real) > 1" by simp
     from reals_power_lt_ex[OF rp th0]
     obtain n0 where n0: "(1/2)^n0 < r" "n0 > 0" by blast
     {
-      fix n::nat
+      fix n :: nat
       assume nn0: "n \<ge> n0"
       then have thnn0: "(1/2)^n \<le> (1/2 :: real)^n0"
         by (auto intro: power_decreasing)
@@ -612,21 +621,27 @@
           by (auto simp add: dist_fps_def inverse_eq_divide power_divide k_def fps_eq_iff)
 
         from neq have kn: "k > n"
-          by (auto simp: fps_sum_rep_nth not_le k_def fps_eq_iff split: split_if_asm intro: LeastI2_ex)
-        then have "dist (?s n) a < (1/2)^n" unfolding dth
-          by (auto intro: power_strict_decreasing)
-        also have "\<dots> \<le> (1/2)^n0" using nn0
-          by (auto intro: power_decreasing)
-        also have "\<dots> < r" using n0 by simp
+          by (auto simp: fps_sum_rep_nth not_le k_def fps_eq_iff
+              split: split_if_asm intro: LeastI2_ex)
+        then have "dist (?s n) a < (1/2)^n"
+          unfolding dth by (auto intro: power_strict_decreasing)
+        also have "\<dots> \<le> (1/2)^n0"
+          using nn0 by (auto intro: power_decreasing)
+        also have "\<dots> < r"
+          using n0 by simp
         finally have "dist (?s n) a < r" .
       }
-      ultimately have "dist (?s n) a < r" by blast
+      ultimately have "dist (?s n) a < r"
+        by blast
     }
-    then have "\<exists>n0. \<forall> n \<ge> n0. dist (?s n) a < r " by blast
+    then have "\<exists>n0. \<forall> n \<ge> n0. dist (?s n) a < r"
+      by blast
   }
-  then show ?thesis unfolding LIMSEQ_def by blast
+  then show ?thesis
+    unfolding LIMSEQ_def by blast
 qed
 
+
 subsection{* Inverses of formal power series *}
 
 declare setsum_cong[fundef_cong]
@@ -650,7 +665,7 @@
 end
 
 lemma fps_inverse_zero [simp]:
-  "inverse (0 :: 'a::{comm_monoid_add,inverse, times, uminus} fps) = 0"
+  "inverse (0 :: 'a::{comm_monoid_add,inverse,times,uminus} fps) = 0"
   by (simp add: fps_ext fps_inverse_def)
 
 lemma fps_inverse_one [simp]: "inverse (1 :: 'a::{division_ring,zero_neq_one} fps) = 1"
@@ -663,7 +678,8 @@
   assumes f0: "f$0 \<noteq> (0::'a::field)"
   shows "inverse f * f = 1"
 proof -
-  have c: "inverse f * f = f * inverse f" by (simp add: mult_commute)
+  have c: "inverse f * f = f * inverse f"
+    by (simp add: mult_commute)
   from f0 have ifn: "\<And>n. inverse f $ n = natfun_inverse f n"
     by (simp add: fps_inverse_def)
   from f0 have th0: "(inverse f * f) $ 0 = 1"
@@ -671,8 +687,10 @@
   {
     fix n :: nat
     assume np: "n > 0"
-    from np have eq: "{0..n} = {0} \<union> {1 .. n}" by auto
-    have d: "{0} \<inter> {1 .. n} = {}" by auto
+    from np have eq: "{0..n} = {0} \<union> {1 .. n}"
+      by auto
+    have d: "{0} \<inter> {1 .. n} = {}"
+      by auto
     from f0 np have th0: "- (inverse f $ n) =
       (setsum (\<lambda>i. f$i * natfun_inverse f (n - i)) {1..n}) / (f$0)"
       by (cases n) (simp_all add: divide_inverse fps_inverse_def)
@@ -683,10 +701,13 @@
       unfolding fps_mult_nth ifn ..
     also have "\<dots> = f$0 * natfun_inverse f n + (\<Sum>i = 1..n. f$i * natfun_inverse f (n-i))"
       by (simp add: eq)
-    also have "\<dots> = 0" unfolding th1 ifn by simp
-    finally have "(inverse f * f)$n = 0" unfolding c .
+    also have "\<dots> = 0"
+      unfolding th1 ifn by simp
+    finally have "(inverse f * f)$n = 0"
+      unfolding c .
   }
-  with th0 show ?thesis by (simp add: fps_eq_iff)
+  with th0 show ?thesis
+    by (simp add: fps_eq_iff)
 qed
 
 lemma fps_inverse_0_iff[simp]: "(inverse f)$0 = (0::'a::division_ring) \<longleftrightarrow> f$0 = 0"
@@ -695,13 +716,16 @@
 lemma fps_inverse_eq_0_iff[simp]: "inverse f = (0:: ('a::field) fps) \<longleftrightarrow> f $0 = 0"
 proof -
   {
-    assume "f$0 = 0"
-    then have "inverse f = 0" by (simp add: fps_inverse_def)
+    assume "f $ 0 = 0"
+    then have "inverse f = 0"
+      by (simp add: fps_inverse_def)
   }
   moreover
   {
-    assume h: "inverse f = 0" and c: "f $0 \<noteq> 0"
-    from inverse_mult_eq_1[OF c] h have False by simp
+    assume h: "inverse f = 0"
+    assume c: "f $0 \<noteq> 0"
+    from inverse_mult_eq_1[OF c] h have False
+      by simp
   }
   ultimately show ?thesis by blast
 qed
@@ -714,7 +738,8 @@
   from inverse_mult_eq_1[OF f0] inverse_mult_eq_1[OF if0]
   have "inverse f * f = inverse f * inverse (inverse f)"
     by (simp add: mult_ac)
-  then show ?thesis using f0 unfolding mult_cancel_left by simp
+  then show ?thesis
+    using f0 unfolding mult_cancel_left by simp
 qed
 
 lemma fps_inverse_unique:
@@ -723,8 +748,11 @@
   shows "inverse f = g"
 proof -
   from inverse_mult_eq_1[OF f0] fg
-  have th0: "inverse f * f = g * f" by (simp add: mult_ac)
-  then show ?thesis using f0  unfolding mult_cancel_right
+  have th0: "inverse f * f = g * f"
+    by (simp add: mult_ac)
+  then show ?thesis
+    using f0
+    unfolding mult_cancel_right
     by (auto simp add: expand_fps_eq)
 qed
 
@@ -733,19 +761,26 @@
   apply (rule fps_inverse_unique)
   apply simp
   apply (simp add: fps_eq_iff fps_mult_nth)
-proof clarsimp
+  apply clarsimp
+proof -
   fix n :: nat
   assume n: "n > 0"
-  let ?f = "\<lambda>i. if n = i then (1\<Colon>'a) else if n - i = 1 then - 1 else 0"
+  let ?f = "\<lambda>i. if n = i then (1::'a) else if n - i = 1 then - 1 else 0"
   let ?g = "\<lambda>i. if i = n then 1 else if i=n - 1 then - 1 else 0"
   let ?h = "\<lambda>i. if i=n - 1 then - 1 else 0"
   have th1: "setsum ?f {0..n} = setsum ?g {0..n}"
     by (rule setsum_cong2) auto
   have th2: "setsum ?g {0..n - 1} = setsum ?h {0..n - 1}"
-    using n apply - by (rule setsum_cong2) auto
-  have eq: "{0 .. n} = {0.. n - 1} \<union> {n}" by auto
-  from n have d: "{0.. n - 1} \<inter> {n} = {}" by auto
-  have f: "finite {0.. n - 1}" "finite {n}" by auto
+    apply (insert n)
+    apply (rule setsum_cong2)
+    apply auto
+    done
+  have eq: "{0 .. n} = {0.. n - 1} \<union> {n}"
+    by auto
+  from n have d: "{0.. n - 1} \<inter> {n} = {}"
+    by auto
+  have f: "finite {0.. n - 1}" "finite {n}"
+    by auto
   show "setsum ?f {0..n} = 0"
     unfolding th1
     apply (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] del: One_nat_def)
@@ -754,11 +789,12 @@
     done
 qed
 
-subsection{* Formal Derivatives, and the MacLaurin theorem around 0*}
+
+subsection {* Formal Derivatives, and the MacLaurin theorem around 0 *}
 
 definition "fps_deriv f = Abs_fps (\<lambda>n. of_nat (n + 1) * f $ (n + 1))"
 
-lemma fps_deriv_nth[simp]: "fps_deriv f $ n = of_nat (n +1) * f $ (n+1)"
+lemma fps_deriv_nth[simp]: "fps_deriv f $ n = of_nat (n +1) * f $ (n + 1)"
   by (simp add: fps_deriv_def)
 
 lemma fps_deriv_linear[simp]:
@@ -767,16 +803,19 @@
   unfolding fps_eq_iff fps_add_nth  fps_const_mult_left fps_deriv_nth by (simp add: field_simps)
 
 lemma fps_deriv_mult[simp]:
-  fixes f :: "('a :: comm_ring_1) fps"
+  fixes f :: "'a::comm_ring_1 fps"
   shows "fps_deriv (f * g) = f * fps_deriv g + fps_deriv f * g"
 proof -
   let ?D = "fps_deriv"
-  { fix n::nat
+  {
+    fix n :: nat
     let ?Zn = "{0 ..n}"
     let ?Zn1 = "{0 .. n + 1}"
     let ?f = "\<lambda>i. i + 1"
-    have fi: "inj_on ?f {0..n}" by (simp add: inj_on_def)
-    have eq: "{1.. n+1} = ?f ` {0..n}" by auto
+    have fi: "inj_on ?f {0..n}"
+      by (simp add: inj_on_def)
+    have eq: "{1.. n+1} = ?f ` {0..n}"
+      by auto
     let ?g = "\<lambda>i. of_nat (i+1) * g $ (i+1) * f $ (n - i) +
         of_nat (i+1)* f $ (i+1) * g $ (n - i)"
     let ?h = "\<lambda>i. of_nat i * g $ i * f $ ((n+1) - i) +
@@ -784,7 +823,8 @@
     {
       fix k
       assume k: "k \<in> {0..n}"
-      have "?h (k + 1) = ?g k" using k by auto
+      have "?h (k + 1) = ?g k"
+        using k by auto
     }
     note th0 = this
     have eq': "{0..n +1}- {1 .. n+1} = {0}" by auto
@@ -834,20 +874,23 @@
 lemma fps_deriv_X[simp]: "fps_deriv X = 1"
   by (simp add: fps_deriv_def X_def fps_eq_iff)
 
-lemma fps_deriv_neg[simp]: "fps_deriv (- (f:: ('a:: comm_ring_1) fps)) = - (fps_deriv f)"
+lemma fps_deriv_neg[simp]:
+  "fps_deriv (- (f:: 'a::comm_ring_1 fps)) = - (fps_deriv f)"
   by (simp add: fps_eq_iff fps_deriv_def)
 
-lemma fps_deriv_add[simp]: "fps_deriv ((f:: ('a::comm_ring_1) fps) + g) = fps_deriv f + fps_deriv g"
+lemma fps_deriv_add[simp]:
+  "fps_deriv ((f:: 'a::comm_ring_1 fps) + g) = fps_deriv f + fps_deriv g"
   using fps_deriv_linear[of 1 f 1 g] by simp
 
-lemma fps_deriv_sub[simp]: "fps_deriv ((f:: ('a::comm_ring_1) fps) - g) = fps_deriv f - fps_deriv g"
+lemma fps_deriv_sub[simp]:
+  "fps_deriv ((f:: 'a::comm_ring_1 fps) - g) = fps_deriv f - fps_deriv g"
   using fps_deriv_add [of f "- g"] by simp
 
 lemma fps_deriv_const[simp]: "fps_deriv (fps_const c) = 0"
   by (simp add: fps_ext fps_deriv_def fps_const_def)
 
 lemma fps_deriv_mult_const_left[simp]:
-    "fps_deriv (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_deriv f"
+  "fps_deriv (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_deriv f"
   by simp
 
 lemma fps_deriv_0[simp]: "fps_deriv 0 = 0"
@@ -857,11 +900,11 @@
   by (simp add: fps_deriv_def fps_eq_iff )
 
 lemma fps_deriv_mult_const_right[simp]:
-    "fps_deriv (f * fps_const (c::'a::comm_ring_1)) = fps_deriv f * fps_const c"
+  "fps_deriv (f * fps_const (c::'a::comm_ring_1)) = fps_deriv f * fps_const c"
   by simp
 
 lemma fps_deriv_setsum:
-  "fps_deriv (setsum f S) = setsum (\<lambda>i. fps_deriv (f i :: ('a::comm_ring_1) fps)) S"
+  "fps_deriv (setsum f S) = setsum (\<lambda>i. fps_deriv (f i :: 'a::comm_ring_1 fps)) S"
 proof (cases "finite S")
   case False
   then show ?thesis by simp
@@ -871,7 +914,7 @@
 qed
 
 lemma fps_deriv_eq_0_iff [simp]:
-  "fps_deriv f = 0 \<longleftrightarrow> (f = fps_const (f$0 :: 'a::{idom,semiring_char_0}))"
+  "fps_deriv f = 0 \<longleftrightarrow> f = fps_const (f$0 :: 'a::{idom,semiring_char_0})"
 proof -
   {
     assume "f = fps_const (f$0)"
@@ -893,22 +936,22 @@
 qed
 
 lemma fps_deriv_eq_iff:
-  fixes f:: "('a::{idom,semiring_char_0}) fps"
+  fixes f :: "'a::{idom,semiring_char_0} fps"
   shows "fps_deriv f = fps_deriv g \<longleftrightarrow> (f = fps_const(f$0 - g$0) + g)"
 proof -
   have "fps_deriv f = fps_deriv g \<longleftrightarrow> fps_deriv (f - g) = 0"
     by simp
-  also have "\<dots> \<longleftrightarrow> f - g = fps_const ((f-g)$0)"
+  also have "\<dots> \<longleftrightarrow> f - g = fps_const ((f - g) $ 0)"
     unfolding fps_deriv_eq_0_iff ..
   finally show ?thesis by (simp add: field_simps)
 qed
 
 lemma fps_deriv_eq_iff_ex:
-  "(fps_deriv f = fps_deriv g) \<longleftrightarrow> (\<exists>(c::'a::{idom,semiring_char_0}). f = fps_const c + g)"
+  "(fps_deriv f = fps_deriv g) \<longleftrightarrow> (\<exists>c::'a::{idom,semiring_char_0}. f = fps_const c + g)"
   by (auto simp: fps_deriv_eq_iff)
 
 
-fun fps_nth_deriv :: "nat \<Rightarrow> ('a::semiring_1) fps \<Rightarrow> 'a fps"
+fun fps_nth_deriv :: "nat \<Rightarrow> 'a::semiring_1 fps \<Rightarrow> 'a fps"
 where
   "fps_nth_deriv 0 f = f"
 | "fps_nth_deriv (Suc n) f = fps_nth_deriv n (fps_deriv f)"
@@ -922,15 +965,15 @@
   by (induct n arbitrary: f g) (auto simp add: fps_nth_deriv_commute)
 
 lemma fps_nth_deriv_neg[simp]:
-  "fps_nth_deriv n (- (f:: ('a:: comm_ring_1) fps)) = - (fps_nth_deriv n f)"
+  "fps_nth_deriv n (- (f :: 'a::comm_ring_1 fps)) = - (fps_nth_deriv n f)"
   by (induct n arbitrary: f) simp_all
 
 lemma fps_nth_deriv_add[simp]:
-  "fps_nth_deriv n ((f:: ('a::comm_ring_1) fps) + g) = fps_nth_deriv n f + fps_nth_deriv n g"
+  "fps_nth_deriv n ((f :: 'a::comm_ring_1 fps) + g) = fps_nth_deriv n f + fps_nth_deriv n g"
   using fps_nth_deriv_linear[of n 1 f 1 g] by simp
 
 lemma fps_nth_deriv_sub[simp]:
-  "fps_nth_deriv n ((f:: ('a::comm_ring_1) fps) - g) = fps_nth_deriv n f - fps_nth_deriv n g"
+  "fps_nth_deriv n ((f :: 'a::comm_ring_1 fps) - g) = fps_nth_deriv n f - fps_nth_deriv n g"
   using fps_nth_deriv_add [of n f "- g"] by simp
 
 lemma fps_nth_deriv_0[simp]: "fps_nth_deriv n 0 = 0"
@@ -952,7 +995,7 @@
   using fps_nth_deriv_linear[of n "c" f 0 0] by (simp add: mult_commute)
 
 lemma fps_nth_deriv_setsum:
-  "fps_nth_deriv n (setsum f S) = setsum (\<lambda>i. fps_nth_deriv n (f i :: ('a::comm_ring_1) fps)) S"
+  "fps_nth_deriv n (setsum f S) = setsum (\<lambda>i. fps_nth_deriv n (f i :: 'a::comm_ring_1 fps)) S"
 proof (cases "finite S")
   case True
   show ?thesis by (induct rule: finite_induct [OF True]) simp_all
@@ -962,15 +1005,16 @@
 qed
 
 lemma fps_deriv_maclauren_0:
-  "(fps_nth_deriv k (f:: ('a::comm_semiring_1) fps)) $ 0 = of_nat (fact k) * f$(k)"
+  "(fps_nth_deriv k (f :: 'a::comm_semiring_1 fps)) $ 0 = of_nat (fact k) * f $ k"
   by (induct k arbitrary: f) (auto simp add: field_simps of_nat_mult)
 
-subsection {* Powers*}
+
+subsection {* Powers *}
 
 lemma fps_power_zeroth_eq_one: "a$0 =1 \<Longrightarrow> a^n $ 0 = (1::'a::semiring_1)"
   by (induct n) (auto simp add: expand_fps_eq fps_mult_nth)
 
-lemma fps_power_first_eq: "(a:: 'a::comm_ring_1 fps)$0 =1 \<Longrightarrow> a^n $ 1 = of_nat n * a$1"
+lemma fps_power_first_eq: "(a :: 'a::comm_ring_1 fps) $ 0 =1 \<Longrightarrow> a^n $ 1 = of_nat n * a$1"
 proof (induct n)
   case 0
   then show ?case by simp
@@ -988,10 +1032,10 @@
 lemma startsby_zero_power:"a $0 = (0::'a::comm_ring_1) \<Longrightarrow> n > 0 \<Longrightarrow> a^n $0 = 0"
   by (induct n) (auto simp add: fps_mult_nth)
 
-lemma startsby_power:"a $0 = (v::'a::{comm_ring_1}) \<Longrightarrow> a^n $0 = v^n"
+lemma startsby_power:"a $0 = (v::'a::comm_ring_1) \<Longrightarrow> a^n $0 = v^n"
   by (induct n) (auto simp add: fps_mult_nth)
 
-lemma startsby_zero_power_iff[simp]: "a^n $0 = (0::'a::{idom}) \<longleftrightarrow> (n \<noteq> 0 \<and> a$0 = 0)"
+lemma startsby_zero_power_iff[simp]: "a^n $0 = (0::'a::idom) \<longleftrightarrow> n \<noteq> 0 \<and> a$0 = 0"
   apply (rule iffI)
   apply (induct n)
   apply (auto simp add: fps_mult_nth)
@@ -1002,11 +1046,14 @@
   assumes a0: "a $0 = (0::'a::idom)"
   shows "\<forall>n < k. a ^ k $ n = 0"
   using a0
-proof(induct k rule: nat_less_induct)
+proof (induct k rule: nat_less_induct)
   fix k
-  assume H: "\<forall>m<k. a $0 =  0 \<longrightarrow> (\<forall>n<m. a ^ m $ n = 0)" and a0: "a $0 = (0\<Colon>'a)"
+  assume H: "\<forall>m<k. a $0 =  0 \<longrightarrow> (\<forall>n<m. a ^ m $ n = 0)" and a0: "a $ 0 = 0"
   let ?ths = "\<forall>m<k. a ^ k $ m = 0"
-  { assume "k = 0" then have ?ths by simp }
+  {
+    assume "k = 0"
+    then have ?ths by simp
+  }
   moreover
   {
     fix l
@@ -1022,8 +1069,10 @@
       moreover
       {
         assume m0: "m \<noteq> 0"
-        have "a ^k $ m = (a^l * a) $m" by (simp add: k mult_commute)
-        also have "\<dots> = (\<Sum>i = 0..m. a ^ l $ i * a $ (m - i))" by (simp add: fps_mult_nth)
+        have "a ^k $ m = (a^l * a) $m"
+          by (simp add: k mult_commute)
+        also have "\<dots> = (\<Sum>i = 0..m. a ^ l $ i * a $ (m - i))"
+          by (simp add: fps_mult_nth)
         also have "\<dots> = 0"
           apply (rule setsum_0')
           apply auto
@@ -1034,31 +1083,36 @@
           done
         finally have "a^k $ m = 0" .
       }
-      ultimately have "a^k $ m = 0" by blast
+      ultimately have "a^k $ m = 0"
+        by blast
     }
     then have ?ths by blast
   }
-  ultimately show ?ths by (cases k) auto
+  ultimately show ?ths
+    by (cases k) auto
 qed
 
 lemma startsby_zero_setsum_depends:
-  assumes a0: "a $0 = (0::'a::idom)" and kn: "n \<ge> k"
+  assumes a0: "a $0 = (0::'a::idom)"
+    and kn: "n \<ge> k"
   shows "setsum (\<lambda>i. (a ^ i)$k) {0 .. n} = setsum (\<lambda>i. (a ^ i)$k) {0 .. k}"
   apply (rule setsum_mono_zero_right)
-  using kn apply auto
+  using kn
+  apply auto
   apply (rule startsby_zero_power_prefix[rule_format, OF a0])
   apply arith
   done
 
 lemma startsby_zero_power_nth_same:
-  assumes a0: "a$0 = (0::'a::{idom})"
+  assumes a0: "a$0 = (0::'a::idom)"
   shows "a^n $ n = (a$1) ^ n"
 proof (induct n)
   case 0
   then show ?case by simp
 next
   case (Suc n)
-  have "a ^ Suc n $ (Suc n) = (a^n * a)$(Suc n)" by (simp add: field_simps)
+  have "a ^ Suc n $ (Suc n) = (a^n * a)$(Suc n)"
+    by (simp add: field_simps)
   also have "\<dots> = setsum (\<lambda>i. a^n$i * a $ (Suc n - i)) {0.. Suc n}"
     by (simp add: fps_mult_nth)
   also have "\<dots> = setsum (\<lambda>i. a^n$i * a $ (Suc n - i)) {n .. Suc n}"
@@ -1069,18 +1123,24 @@
     apply (rule startsby_zero_power_prefix[rule_format, OF a0])
     apply arith
     done
-  also have "\<dots> = a^n $ n * a$1" using a0 by simp
-  finally show ?case using Suc.hyps by simp
+  also have "\<dots> = a^n $ n * a$1"
+    using a0 by simp
+  finally show ?case
+    using Suc.hyps by simp
 qed
 
 lemma fps_inverse_power:
-  fixes a :: "('a::{field}) fps"
+  fixes a :: "'a::field fps"
   shows "inverse (a^n) = inverse a ^ n"
 proof -
   {
     assume a0: "a$0 = 0"
-    then have eq: "inverse a = 0" by (simp add: fps_inverse_def)
-    { assume "n = 0" then have ?thesis by simp }
+    then have eq: "inverse a = 0"
+      by (simp add: fps_inverse_def)
+    {
+      assume "n = 0"
+      then have ?thesis by simp
+    }
     moreover
     {
       assume n: "n > 0"
@@ -1106,7 +1166,7 @@
 qed
 
 lemma fps_deriv_power:
-    "fps_deriv (a ^ n) = fps_const (of_nat n :: 'a:: comm_ring_1) * fps_deriv a * a ^ (n - 1)"
+  "fps_deriv (a ^ n) = fps_const (of_nat n :: 'a::comm_ring_1) * fps_deriv a * a ^ (n - 1)"
   apply (induct n)
   apply (auto simp add: field_simps fps_const_add[symmetric] simp del: fps_const_add)
   apply (case_tac n)
@@ -1114,10 +1174,10 @@
   done
 
 lemma fps_inverse_deriv:
-  fixes a:: "('a :: field) fps"
+  fixes a :: "'a::field fps"
   assumes a0: "a$0 \<noteq> 0"
   shows "fps_deriv (inverse a) = - fps_deriv a * (inverse a)\<^sup>2"
-proof-
+proof -
   from inverse_mult_eq_1[OF a0]
   have "fps_deriv (inverse a * a) = 0" by simp
   then have "inverse a * fps_deriv a + fps_deriv (inverse a) * a = 0"
@@ -1138,7 +1198,7 @@
 qed
 
 lemma fps_inverse_mult:
-  fixes a::"('a :: field) fps"
+  fixes a :: "'a::field fps"
   shows "inverse (a * b) = inverse a * inverse b"
 proof -
   {
@@ -1168,7 +1228,7 @@
 qed
 
 lemma fps_inverse_deriv':
-  fixes a:: "('a :: field) fps"
+  fixes a :: "'a::field fps"
   assumes a0: "a$0 \<noteq> 0"
   shows "fps_deriv (inverse a) = - fps_deriv a / a\<^sup>2"
   using fps_inverse_deriv[OF a0]
@@ -1181,7 +1241,7 @@
   by (metis mult_commute inverse_mult_eq_1 f0)
 
 lemma fps_divide_deriv:
-  fixes a:: "('a :: field) fps"
+  fixes a :: "'a::field fps"
   assumes a0: "b$0 \<noteq> 0"
   shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b\<^sup>2"
   using fps_inverse_deriv[OF a0]
@@ -1189,7 +1249,7 @@
     power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0])
 
 
-lemma fps_inverse_gp': "inverse (Abs_fps(\<lambda>n. (1::'a::field))) = 1 - X"
+lemma fps_inverse_gp': "inverse (Abs_fps (\<lambda>n. 1::'a::field)) = 1 - X"
   by (simp add: fps_inverse_gp fps_eq_iff X_def)
 
 lemma fps_nth_deriv_X[simp]: "fps_nth_deriv n X = (if n = 0 then X else if n=1 then 1 else 0)"
@@ -1197,12 +1257,13 @@
 
 
 lemma fps_inverse_X_plus1:
-  "inverse (1 + X) = Abs_fps (\<lambda>n. (- (1::'a::{field})) ^ n)" (is "_ = ?r")
-proof-
+  "inverse (1 + X) = Abs_fps (\<lambda>n. (- (1::'a::field)) ^ n)" (is "_ = ?r")
+proof -
   have eq: "(1 + X) * ?r = 1"
     unfolding minus_one_power_iff
     by (auto simp add: field_simps fps_eq_iff)
-  show ?thesis by (auto simp add: eq intro: fps_inverse_unique)
+  show ?thesis
+    by (auto simp add: eq intro: fps_inverse_unique)
 qed
 
 
@@ -1220,8 +1281,10 @@
     fps_const a * fps_integral f a0 + fps_const b * fps_integral g b0"
   (is "?l = ?r")
 proof -
-  have "fps_deriv ?l = fps_deriv ?r" by (simp add: fps_deriv_fps_integral)
-  moreover have "?l$0 = ?r$0" by (simp add: fps_integral_def)
+  have "fps_deriv ?l = fps_deriv ?r"
+    by (simp add: fps_deriv_fps_integral)
+  moreover have "?l$0 = ?r$0"
+    by (simp add: fps_integral_def)
   ultimately show ?thesis
     unfolding fps_deriv_eq_iff by auto
 qed
@@ -1229,26 +1292,26 @@
 
 subsection {* Composition of FPSs *}
 
-definition fps_compose :: "('a::semiring_1) fps \<Rightarrow> 'a fps \<Rightarrow> 'a fps" (infixl "oo" 55) where
-  fps_compose_def: "a oo b = Abs_fps (\<lambda>n. setsum (\<lambda>i. a$i * (b^i$n)) {0..n})"
+definition fps_compose :: "'a::semiring_1 fps \<Rightarrow> 'a fps \<Rightarrow> 'a fps" (infixl "oo" 55)
+  where "a oo b = Abs_fps (\<lambda>n. setsum (\<lambda>i. a$i * (b^i$n)) {0..n})"
 
 lemma fps_compose_nth: "(a oo b)$n = setsum (\<lambda>i. a$i * (b^i$n)) {0..n}"
   by (simp add: fps_compose_def)
 
-lemma fps_compose_X[simp]: "a oo X = (a :: ('a :: comm_ring_1) fps)"
+lemma fps_compose_X[simp]: "a oo X = (a :: 'a::comm_ring_1 fps)"
   by (simp add: fps_ext fps_compose_def mult_delta_right setsum_delta')
 
 lemma fps_const_compose[simp]:
-  "fps_const (a::'a::{comm_ring_1}) oo b = fps_const (a)"
+  "fps_const (a::'a::comm_ring_1) oo b = fps_const a"
   by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta)
 
-lemma numeral_compose[simp]: "(numeral k::('a::{comm_ring_1}) fps) oo b = numeral k"
+lemma numeral_compose[simp]: "(numeral k :: 'a::comm_ring_1 fps) oo b = numeral k"
   unfolding numeral_fps_const by simp
 
-lemma neg_numeral_compose[simp]: "(- numeral k::('a::{comm_ring_1}) fps) oo b = - numeral k"
+lemma neg_numeral_compose[simp]: "(- numeral k :: 'a::comm_ring_1 fps) oo b = - numeral k"
   unfolding neg_numeral_fps_const by simp
 
-lemma X_fps_compose_startby0[simp]: "a$0 = 0 \<Longrightarrow> X oo a = (a :: ('a :: comm_ring_1) fps)"
+lemma X_fps_compose_startby0[simp]: "a$0 = 0 \<Longrightarrow> X oo a = (a :: 'a::comm_ring_1 fps)"
   by (simp add: fps_eq_iff fps_compose_def mult_delta_left setsum_delta not_le)
 
 
@@ -1259,10 +1322,10 @@
 
 lemma fps_power_mult_eq_shift:
   "X^Suc k * Abs_fps (\<lambda>n. a (n + Suc k)) =
-    Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a:: comm_ring_1) * X^i) {0 .. k}"
+    Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a::comm_ring_1) * X^i) {0 .. k}"
   (is "?lhs = ?rhs")
 proof -
-  { fix n:: nat
+  { fix n :: nat
     have "?lhs $ n = (if n < Suc k then 0 else a n)"
       unfolding X_power_mult_nth by auto
     also have "\<dots> = ?rhs $ n"
@@ -1298,21 +1361,21 @@
   (* If f reprents {a_n} and P is a polynomial, then
         P(xD) f represents {P(n) a_n}*)
 
-definition "XD = op * X o fps_deriv"
-
-lemma XD_add[simp]:"XD (a + b) = XD a + XD (b :: ('a::comm_ring_1) fps)"
+definition "XD = op * X \<circ> fps_deriv"
+
+lemma XD_add[simp]:"XD (a + b) = XD a + XD (b :: 'a::comm_ring_1 fps)"
   by (simp add: XD_def field_simps)
 
 lemma XD_mult_const[simp]:"XD (fps_const (c::'a::comm_ring_1) * a) = fps_const c * XD a"
   by (simp add: XD_def field_simps)
 
 lemma XD_linear[simp]: "XD (fps_const c * a + fps_const d * b) =
-    fps_const c * XD a + fps_const d * XD (b :: ('a::comm_ring_1) fps)"
+    fps_const c * XD a + fps_const d * XD (b :: 'a::comm_ring_1 fps)"
   by simp
 
 lemma XDN_linear:
   "(XD ^^ n) (fps_const c * a + fps_const d * b) =
-    fps_const c * (XD ^^ n) a + fps_const d * (XD ^^ n) (b :: ('a::comm_ring_1) fps)"
+    fps_const c * (XD ^^ n) a + fps_const d * (XD ^^ n) (b :: 'a::comm_ring_1 fps)"
   by (induct n) simp_all
 
 lemma fps_mult_X_deriv_shift: "X* fps_deriv a = Abs_fps (\<lambda>n. of_nat n* a$n)"
@@ -1320,39 +1383,38 @@
 
 
 lemma fps_mult_XD_shift:
-  "(XD ^^ k) (a:: ('a::{comm_ring_1}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
+  "(XD ^^ k) (a :: 'a::comm_ring_1 fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
   by (induct k arbitrary: a) (simp_all add: XD_def fps_eq_iff field_simps del: One_nat_def)
 
 
-subsubsection{* Rule 3 is trivial and is given by @{text fps_times_def}*}
-
-subsubsection{* Rule 5 --- summation and "division" by (1 - X)*}
+subsubsection {* Rule 3 is trivial and is given by @{text fps_times_def} *}
+
+subsubsection {* Rule 5 --- summation and "division" by (1 - X) *}
 
 lemma fps_divide_X_minus1_setsum_lemma:
-  "a = ((1::('a::comm_ring_1) fps) - X) * Abs_fps (\<lambda>n. setsum (\<lambda>i. a $ i) {0..n})"
+  "a = ((1::'a::comm_ring_1 fps) - X) * Abs_fps (\<lambda>n. setsum (\<lambda>i. a $ i) {0..n})"
 proof -
-  let ?X = "X::('a::comm_ring_1) fps"
   let ?sa = "Abs_fps (\<lambda>n. setsum (\<lambda>i. a $ i) {0..n})"
   have th0: "\<And>i. (1 - (X::'a fps)) $ i = (if i = 0 then 1 else if i = 1 then - 1 else 0)"
     by simp
   {
-    fix n:: nat
+    fix n :: nat
     {
-      assume "n=0"
-      then have "a$n = ((1 - ?X) * ?sa) $ n"
+      assume "n = 0"
+      then have "a $ n = ((1 - X) * ?sa) $ n"
         by (simp add: fps_mult_nth)
     }
     moreover
     {
       assume n0: "n \<noteq> 0"
-      then have u: "{0} \<union> ({1} \<union> {2..n}) = {0..n}" "{1}\<union>{2..n} = {1..n}"
-        "{0..n - 1}\<union>{n} = {0..n}"
+      then have u: "{0} \<union> ({1} \<union> {2..n}) = {0..n}" "{1} \<union> {2..n} = {1..n}"
+        "{0..n - 1} \<union> {n} = {0..n}"
         by (auto simp: set_eq_iff)
-      have d: "{0} \<inter> ({1} \<union> {2..n}) = {}" "{1} \<inter> {2..n} = {}"
-        "{0..n - 1}\<inter>{n} ={}" using n0 by simp_all
+      have d: "{0} \<inter> ({1} \<union> {2..n}) = {}" "{1} \<inter> {2..n} = {}" "{0..n - 1} \<inter> {n} = {}"
+        using n0 by simp_all
       have f: "finite {0}" "finite {1}" "finite {2 .. n}"
         "finite {0 .. n - 1}" "finite {n}" by simp_all
-      have "((1 - ?X) * ?sa) $ n = setsum (\<lambda>i. (1 - ?X)$ i * ?sa $ (n - i)) {0 .. n}"
+      have "((1 - X) * ?sa) $ n = setsum (\<lambda>i. (1 - X)$ i * ?sa $ (n - i)) {0 .. n}"
         by (simp add: fps_mult_nth)
       also have "\<dots> = a$n"
         unfolding th0
@@ -1362,24 +1424,29 @@
         unfolding setsum_Un_disjoint[OF f(4,5) d(3), unfolded u(3)]
         apply simp
         done
-      finally have "a$n = ((1 - ?X) * ?sa) $ n" by simp
+      finally have "a$n = ((1 - X) * ?sa) $ n"
+        by simp
     }
-    ultimately have "a$n = ((1 - ?X) * ?sa) $ n" by blast
+    ultimately have "a$n = ((1 - X) * ?sa) $ n"
+      by blast
   }
-  then show ?thesis unfolding fps_eq_iff by blast
+  then show ?thesis
+    unfolding fps_eq_iff by blast
 qed
 
 lemma fps_divide_X_minus1_setsum:
-  "a /((1::('a::field) fps) - X) = Abs_fps (\<lambda>n. setsum (\<lambda>i. a $ i) {0..n})"
+  "a /((1::'a::field fps) - X) = Abs_fps (\<lambda>n. setsum (\<lambda>i. a $ i) {0..n})"
 proof -
-  let ?X = "1 - (X::('a::field) fps)"
-  have th0: "?X $ 0 \<noteq> 0" by simp
-  have "a /?X = ?X *  Abs_fps (\<lambda>n\<Colon>nat. setsum (op $ a) {0..n}) * inverse ?X"
+  let ?X = "1 - (X::'a fps)"
+  have th0: "?X $ 0 \<noteq> 0"
+    by simp
+  have "a /?X = ?X *  Abs_fps (\<lambda>n::nat. setsum (op $ a) {0..n}) * inverse ?X"
     using fps_divide_X_minus1_setsum_lemma[of a, symmetric] th0
     by (simp add: fps_divide_def mult_assoc)
-  also have "\<dots> = (inverse ?X * ?X) * Abs_fps (\<lambda>n\<Colon>nat. setsum (op $ a) {0..n}) "
+  also have "\<dots> = (inverse ?X * ?X) * Abs_fps (\<lambda>n::nat. setsum (op $ a) {0..n}) "
     by (simp add: mult_ac)
-  finally show ?thesis by (simp add: inverse_mult_eq_1[OF th0])
+  finally show ?thesis
+    by (simp add: inverse_mult_eq_1[OF th0])
 qed
 
 
@@ -1396,7 +1463,8 @@
 
 lemma append_natpermute_less_eq:
   assumes "xs @ ys \<in> natpermute n k"
-  shows "listsum xs \<le> n" and "listsum ys \<le> n"
+  shows "listsum xs \<le> n"
+    and "listsum ys \<le> n"
 proof -
   from assms have "listsum (xs @ ys) = n"
     by (simp add: natpermute_def)
@@ -1554,8 +1622,8 @@
 text {* The general form *}
 lemma fps_setprod_nth:
   fixes m :: nat
-    and a :: "nat \<Rightarrow> ('a::comm_ring_1) fps"
-  shows "(setprod a {0 .. m})$n =
+    and a :: "nat \<Rightarrow> 'a::comm_ring_1 fps"
+  shows "(setprod a {0 .. m}) $ n =
     setsum (\<lambda>v. setprod (\<lambda>j. (a j) $ (v!j)) {0..m}) (natpermute n (m+1))"
   (is "?P m n")
 proof (induct m arbitrary: n rule: nat_less_induct)
@@ -1608,7 +1676,7 @@
 text{* The special form for powers *}
 lemma fps_power_nth_Suc:
   fixes m :: nat
-    and a :: "('a::comm_ring_1) fps"
+    and a :: "'a::comm_ring_1 fps"
   shows "(a ^ Suc m)$n = setsum (\<lambda>v. setprod (\<lambda>j. a $ (v!j)) {0..m}) (natpermute n (m+1))"
 proof -
   have th0: "a^Suc m = setprod (\<lambda>i. a) {0..m}"
@@ -1618,14 +1686,14 @@
 
 lemma fps_power_nth:
   fixes m :: nat
-    and a :: "('a::comm_ring_1) fps"
+    and a :: "'a::comm_ring_1 fps"
   shows "(a ^m)$n =
     (if m=0 then 1$n else setsum (\<lambda>v. setprod (\<lambda>j. a $ (v!j)) {0..m - 1}) (natpermute n m))"
   by (cases m) (simp_all add: fps_power_nth_Suc del: power_Suc)
 
 lemma fps_nth_power_0:
   fixes m :: nat
-    and a :: "('a::{comm_ring_1}) fps"
+    and a :: "'a::comm_ring_1 fps"
   shows "(a ^m)$0 = (a$0) ^ m"
 proof (cases m)
   case 0
@@ -1641,9 +1709,10 @@
 qed
 
 lemma fps_compose_inj_right:
-  assumes a0: "a$0 = (0::'a::{idom})"
+  assumes a0: "a$0 = (0::'a::idom)"
     and a1: "a$1 \<noteq> 0"
-  shows "(b oo a = c oo a) \<longleftrightarrow> b = c" (is "?lhs \<longleftrightarrow>?rhs")
+  shows "(b oo a = c oo a) \<longleftrightarrow> b = c"
+  (is "?lhs \<longleftrightarrow>?rhs")
 proof
   assume ?rhs
   then show "?lhs" by simp
@@ -1692,7 +1761,7 @@
 
 declare setprod_cong [fundef_cong]
 
-function radical :: "(nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> ('a::{field}) fps \<Rightarrow> nat \<Rightarrow> 'a"
+function radical :: "(nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a::field fps \<Rightarrow> nat \<Rightarrow> 'a"
 where
   "radical r 0 a 0 = 1"
 | "radical r 0 a (Suc n) = 0"
@@ -1767,7 +1836,7 @@
     apply (rule setprod_cong)
     apply simp
     using Suc
-    apply (subgoal_tac "replicate k (0::nat) ! x = 0")
+    apply (subgoal_tac "replicate k 0 ! x = 0")
     apply (auto intro: nth_replicate simp del: replicate.simps)
     done
   also have "\<dots> = a$0" using r Suc by (simp add: setprod_constant)
@@ -2040,7 +2109,7 @@
           then have thn: "xs!i < n" by presburger
           from h[rule_format, OF thn] show "a$(xs !i) = ?r$(xs!i)" .
         qed
-        have th00: "\<And>(x::'a). of_nat (Suc k) * (x * inverse (of_nat (Suc k))) = x"
+        have th00: "\<And>x::'a. of_nat (Suc k) * (x * inverse (of_nat (Suc k))) = x"
           by (simp add: field_simps del: of_nat_Suc)
         from H have "b$n = a^Suc k $ n"
           by (simp add: fps_eq_iff)
@@ -2076,7 +2145,7 @@
 
 lemma radical_power:
   assumes r0: "r (Suc k) ((a$0) ^ Suc k) = a$0"
-    and a0: "(a$0 ::'a::field_char_0) \<noteq> 0"
+    and a0: "(a$0 :: 'a::field_char_0) \<noteq> 0"
   shows "(fps_radical r (Suc k) (a ^ Suc k)) = a"
 proof -
   let ?ak = "a^ Suc k"
@@ -2093,7 +2162,7 @@
 qed
 
 lemma fps_deriv_radical:
-  fixes a:: "'a::field_char_0 fps"
+  fixes a :: "'a::field_char_0 fps"
   assumes r0: "(r (Suc k) (a$0)) ^ Suc k = a$0"
     and a0: "a$0 \<noteq> 0"
   shows "fps_deriv (fps_radical r (Suc k) a) =
@@ -2120,7 +2189,7 @@
 qed
 
 lemma radical_mult_distrib:
-  fixes a:: "'a::field_char_0 fps"
+  fixes a :: "'a::field_char_0 fps"
   assumes k: "k > 0"
     and ra0: "r k (a $ 0) ^ k = a $ 0"
     and rb0: "r k (b $ 0) ^ k = b $ 0"
@@ -2191,7 +2260,7 @@
 qed
 *)
 
-lemma fps_divide_1[simp]: "(a:: ('a::field) fps) / 1 = a"
+lemma fps_divide_1[simp]: "(a :: 'a::field fps) / 1 = a"
   by (simp add: fps_divide_def)
 
 lemma radical_divide:
@@ -2252,9 +2321,9 @@
 subsection{* Derivative of composition *}
 
 lemma fps_compose_deriv:
-  fixes a:: "('a::idom) fps"
+  fixes a :: "'a::idom fps"
   assumes b0: "b$0 = 0"
-  shows "fps_deriv (a oo b) = ((fps_deriv a) oo b) * (fps_deriv b)"
+  shows "fps_deriv (a oo b) = ((fps_deriv a) oo b) * fps_deriv b"
 proof -
   {
     fix n
@@ -2305,7 +2374,8 @@
   "((1+X)*a) $n = (if n = 0 then (a$n :: 'a::comm_ring_1) else a$n + a$(n - 1))"
 proof (cases n)
   case 0
-  then show ?thesis by (simp add: fps_mult_nth )
+  then show ?thesis
+    by (simp add: fps_mult_nth )
 next
   case (Suc m)
   have "((1+X)*a) $n = setsum (\<lambda>i. (1+X)$i * a$(n-i)) {0..n}"
@@ -2317,7 +2387,8 @@
   finally show ?thesis .
 qed
 
-subsection{* Finite FPS (i.e. polynomials) and X *}
+
+subsection {* Finite FPS (i.e. polynomials) and X *}
 
 lemma fps_poly_sum_X:
   assumes z: "\<forall>i > n. a$i = (0::'a::comm_ring_1)"
@@ -2335,7 +2406,7 @@
 
 subsection{* Compositional inverses *}
 
-fun compinv :: "'a fps \<Rightarrow> nat \<Rightarrow> 'a::{field}"
+fun compinv :: "'a fps \<Rightarrow> nat \<Rightarrow> 'a::field"
 where
   "compinv a 0 = X$0"
 | "compinv a (Suc n) =
@@ -2376,7 +2447,7 @@
 qed
 
 
-fun gcompinv :: "'a fps \<Rightarrow> 'a fps \<Rightarrow> nat \<Rightarrow> 'a::{field}"
+fun gcompinv :: "'a fps \<Rightarrow> 'a fps \<Rightarrow> nat \<Rightarrow> 'a::field"
 where
   "gcompinv b a 0 = b$0"
 | "gcompinv b a (Suc n) =
@@ -2474,9 +2545,9 @@
   shows "((a oo c) * (b oo d))$n =
     setsum (\<lambda>(k,m). a$k * b$m * (c^k * d^m) $ n) {(k,m). k + m \<le> n}"  (is "?l = ?r")
 proof -
-  let ?S = "{(k\<Colon>nat, m\<Colon>nat). k + m \<le> n}"
+  let ?S = "{(k::nat, m::nat). k + m \<le> n}"
   have s: "?S \<subseteq> {0..n} <*> {0..n}" by (auto simp add: subset_eq)
-  have f: "finite {(k\<Colon>nat, m\<Colon>nat). k + m \<le> n}"
+  have f: "finite {(k::nat, m::nat). k + m \<le> n}"
     apply (rule finite_subset[OF s])
     apply auto
     done
@@ -2708,7 +2779,8 @@
 
 lemma fps_X_power_compose:
   assumes a0: "a$0=0"
-  shows "X^k oo a = (a::('a::idom fps))^k" (is "?l = ?r")
+  shows "X^k oo a = (a::'a::idom fps)^k"
+  (is "?l = ?r")
 proof (cases k)
   case 0
   then show ?thesis by simp
@@ -2752,7 +2824,7 @@
 qed
 
 lemma fps_inv_deriv:
-  assumes a0:"a$0 = (0::'a::{field})"
+  assumes a0:"a$0 = (0::'a::field)"
     and a1: "a$1 \<noteq> 0"
   shows "fps_deriv (fps_inv a) = inverse (fps_deriv a oo fps_inv a)"
 proof -
@@ -2815,7 +2887,7 @@
 qed
 
 lemma fps_ginv_deriv:
-  assumes a0:"a$0 = (0::'a::{field})"
+  assumes a0:"a$0 = (0::'a::field)"
     and a1: "a$1 \<noteq> 0"
   shows "fps_deriv (fps_ginv b a) = (fps_deriv b / fps_deriv a) oo fps_ginv X a"
 proof -
@@ -2858,7 +2930,7 @@
 qed
 
 lemma E_unique_ODE:
-  "fps_deriv a = fps_const c * a \<longleftrightarrow> a = fps_const (a$0) * E (c :: 'a::field_char_0)"
+  "fps_deriv a = fps_const c * a \<longleftrightarrow> a = fps_const (a$0) * E (c::'a::field_char_0)"
   (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume d: ?lhs
@@ -2900,7 +2972,7 @@
 lemma E_nth[simp]: "E a $ n = a^n / of_nat (fact n)"
   by (simp add: E_def)
 
-lemma E0[simp]: "E (0::'a::{field}) = 1"
+lemma E0[simp]: "E (0::'a::field) = 1"
   by (simp add: fps_eq_iff power_0_left)
 
 lemma E_neg: "E (- a) = inverse (E (a::'a::field_char_0))"
@@ -2914,7 +2986,7 @@
 lemma E_nth_deriv[simp]: "fps_nth_deriv n (E (a::'a::field_char_0)) = (fps_const a)^n * (E a)"
   by (induct n) auto
 
-lemma X_compose_E[simp]: "X oo E (a::'a::{field}) = E a - 1"
+lemma X_compose_E[simp]: "X oo E (a::'a::field) = E a - 1"
   by (simp add: fps_eq_iff X_fps_compose)
 
 lemma LE_compose:
@@ -2937,7 +3009,7 @@
   done
 
 lemma inverse_one_plus_X:
-  "inverse (1 + X) = Abs_fps (\<lambda>n. (- 1 ::'a::{field})^n)"
+  "inverse (1 + X) = Abs_fps (\<lambda>n. (- 1 ::'a::field)^n)"
   (is "inverse ?l = ?r")
 proof -
   have th: "?l * ?r = 1"
@@ -2951,7 +3023,7 @@
 
 lemma radical_E:
   assumes r: "r (Suc k) 1 = 1"
-  shows "fps_radical r (Suc k) (E (c::'a::{field_char_0})) = E (c / of_nat (Suc k))"
+  shows "fps_radical r (Suc k) (E (c::'a::field_char_0)) = E (c / of_nat (Suc k))"
 proof -
   let ?ck = "(c / of_nat (Suc k))"
   let ?r = "fps_radical r (Suc k)"
@@ -2964,7 +3036,7 @@
   show ?thesis by auto
 qed
 
-lemma Ec_E1_eq: "E (1::'a::{field_char_0}) oo (fps_const c * X) = E c"
+lemma Ec_E1_eq: "E (1::'a::field_char_0) oo (fps_const c * X) = E c"
   apply (auto simp add: fps_eq_iff E_def fps_compose_def power_mult_distrib)
   apply (simp add: cond_value_iff cond_application_beta setsum_delta' cong del: if_weak_cong)
   done
@@ -2972,13 +3044,13 @@
 text{* The generalized binomial theorem as a  consequence of @{thm E_add_mult} *}
 
 lemma gbinomial_theorem:
-  "((a::'a::{field_char_0, field_inverse_zero})+b) ^ n =
+  "((a::'a::{field_char_0,field_inverse_zero})+b) ^ n =
     (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
 proof -
   from E_add_mult[of a b]
   have "(E (a + b)) $ n = (E a * E b)$n" by simp
   then have "(a + b) ^ n =
-    (\<Sum>i\<Colon>nat = 0\<Colon>nat..n. a ^ i * b ^ (n - i)  * (of_nat (fact n) / of_nat (fact i * fact (n - i))))"
+    (\<Sum>i::nat = 0::nat..n. a ^ i * b ^ (n - i)  * (of_nat (fact n) / of_nat (fact i * fact (n - i))))"
     by (simp add: field_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib)
   then show ?thesis
     apply simp
@@ -3614,7 +3686,7 @@
 lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)"
   by (simp add: fps_eq_iff fps_const_def)
 
-lemma fps_numeral_fps_const: "numeral i = fps_const (numeral i :: 'a:: {comm_ring_1})"
+lemma fps_numeral_fps_const: "numeral i = fps_const (numeral i :: 'a::comm_ring_1)"
   by (fact numeral_fps_const) (* FIXME: duplicate *)
 
 lemma fps_cos_Eii: "fps_cos c = (E (ii * c) + E (- ii * c)) / fps_const 2"
@@ -3649,7 +3721,7 @@
 
 subsection {* Hypergeometric series *}
 
-definition "F as bs (c::'a::{field_char_0, field_inverse_zero}) =
+definition "F as bs (c::'a::{field_char_0,field_inverse_zero}) =
   Abs_fps (\<lambda>n. (foldl (\<lambda>r a. r* pochhammer a n) 1 as * c^n) /
     (foldl (\<lambda>r b. r * pochhammer b n) 1 bs * of_nat (fact n)))"
 
@@ -3722,7 +3794,7 @@
 lemma XDp_nth[simp]: "XDp c a $ n = (c + of_nat n) * a$n"
   by (simp add: XDp_def algebra_simps)
 
-lemma XDp_commute: "XDp b o XDp (c::'a::comm_ring_1) = XDp c o XDp b"
+lemma XDp_commute: "XDp b \<circ> XDp (c::'a::comm_ring_1) = XDp c \<circ> XDp b"
   by (auto simp add: XDp_def fun_eq_iff fps_eq_iff algebra_simps)
 
 lemma XDp0 [simp]: "XDp 0 = XD"
@@ -3732,11 +3804,11 @@
   by (simp add: fps_eq_iff fps_integral_def)
 
 lemma F_minus_nat:
-  "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0, field_inverse_zero}) $ k =
+  "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0,field_inverse_zero}) $ k =
     (if k \<le> n then
       pochhammer (- of_nat n) k * c ^ k / (pochhammer (- of_nat (n + m)) k * of_nat (fact k))
      else 0)"
-  "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0, field_inverse_zero}) $ k =
+  "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0,field_inverse_zero}) $ k =
     (if k \<le> m then
       pochhammer (- of_nat m) k * c ^ k / (pochhammer (- of_nat (m + n)) k * of_nat (fact k))
      else 0)"
@@ -3751,13 +3823,13 @@
 lemma pochhammer_rec_if: "pochhammer a n = (if n = 0 then 1 else a * pochhammer (a + 1) (n - 1))"
   by (cases n) (simp_all add: pochhammer_rec)
 
-lemma XDp_foldr_nth [simp]: "foldr (\<lambda>c r. XDp c o r) cs (\<lambda>c. XDp c a) c0 $ n =
+lemma XDp_foldr_nth [simp]: "foldr (\<lambda>c r. XDp c \<circ> r) cs (\<lambda>c. XDp c a) c0 $ n =
     foldr (\<lambda>c r. (c + of_nat n) * r) cs (c0 + of_nat n) * a$n"
   by (induct cs arbitrary: c0) (auto simp add: algebra_simps)
 
 lemma genric_XDp_foldr_nth:
   assumes f: "\<forall>n c a. f c a $ n = (of_nat n + k c) * a$n"
-  shows "foldr (\<lambda>c r. f c o r) cs (\<lambda>c. g c a) c0 $ n =
+  shows "foldr (\<lambda>c r. f c \<circ> r) cs (\<lambda>c. g c a) c0 $ n =
     foldr (\<lambda>c r. (k c + of_nat n) * r) cs (g c0 a $ n)"
   by (induct cs arbitrary: c0) (auto simp add: algebra_simps f)
 
@@ -3794,7 +3866,7 @@
 
 instance fps :: (comm_ring_1) complete_space
 proof
-  fix X::"nat \<Rightarrow> 'a fps"
+  fix X :: "nat \<Rightarrow> 'a fps"
   assume "Cauchy X"
   {
     fix i
diff -r 93f6d33a754e -r 8a8e6db7f391 src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Fri Dec 06 09:42:13 2013 +0100
+++ b/src/HOL/Library/Permutations.thy	Fri Dec 06 17:33:45 2013 +0100
@@ -8,371 +8,465 @@
 imports Parity Fact
 begin
 
-definition permutes (infixr "permutes" 41) where
-  "(p permutes S) \<longleftrightarrow> (\<forall>x. x \<notin> S \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)"
-
-(* ------------------------------------------------------------------------- *)
-(* Transpositions.                                                           *)
-(* ------------------------------------------------------------------------- *)
+subsection {* Transpositions *}
 
 lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id"
   by (auto simp add: fun_eq_iff swap_def fun_upd_def)
-lemma swap_id_refl: "Fun.swap a a id = id" by simp
+
+lemma swap_id_refl: "Fun.swap a a id = id"
+  by simp
+
 lemma swap_id_sym: "Fun.swap a b id = Fun.swap b a id"
   by (rule ext, simp add: swap_def)
-lemma swap_id_idempotent[simp]: "Fun.swap a b id o Fun.swap a b id = id"
+
+lemma swap_id_idempotent[simp]: "Fun.swap a b id \<circ> Fun.swap a b id = id"
   by (rule ext, auto simp add: swap_def)
 
-lemma inv_unique_comp: assumes fg: "f o g = id" and gf: "g o f = id"
+lemma inv_unique_comp:
+  assumes fg: "f \<circ> g = id"
+    and gf: "g \<circ> f = id"
   shows "inv f = g"
   using fg gf inv_equality[of g f] by (auto simp add: fun_eq_iff)
 
 lemma inverse_swap_id: "inv (Fun.swap a b id) = Fun.swap a b id"
-  by (rule inv_unique_comp, simp_all)
+  by (rule inv_unique_comp) simp_all
 
 lemma swap_id_eq: "Fun.swap a b id x = (if x = a then b else if x = b then a else x)"
   by (simp add: swap_def)
 
-(* ------------------------------------------------------------------------- *)
-(* Basic consequences of the definition.                                     *)
-(* ------------------------------------------------------------------------- *)
+
+subsection {* Basic consequences of the definition *}
+
+definition permutes  (infixr "permutes" 41)
+  where "(p permutes S) \<longleftrightarrow> (\<forall>x. x \<notin> S \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)"
 
 lemma permutes_in_image: "p permutes S \<Longrightarrow> p x \<in> S \<longleftrightarrow> x \<in> S"
   unfolding permutes_def by metis
 
-lemma permutes_image: assumes pS: "p permutes S" shows "p ` S = S"
-  using pS
+lemma permutes_image: "p permutes S \<Longrightarrow> p ` S = S"
   unfolding permutes_def
-  apply -
   apply (rule set_eqI)
   apply (simp add: image_iff)
   apply metis
   done
 
-lemma permutes_inj: "p permutes S ==> inj p "
+lemma permutes_inj: "p permutes S \<Longrightarrow> inj p"
   unfolding permutes_def inj_on_def by blast
 
-lemma permutes_surj: "p permutes s ==> surj p"
+lemma permutes_surj: "p permutes s \<Longrightarrow> surj p"
   unfolding permutes_def surj_def by metis
 
-lemma permutes_inv_o: assumes pS: "p permutes S"
-  shows " p o inv p = id"
-  and "inv p o p = id"
+lemma permutes_inv_o:
+  assumes pS: "p permutes S"
+  shows "p \<circ> inv p = id"
+    and "inv p \<circ> p = id"
   using permutes_inj[OF pS] permutes_surj[OF pS]
   unfolding inj_iff[symmetric] surj_iff[symmetric] by blast+
 
-
 lemma permutes_inverses:
   fixes p :: "'a \<Rightarrow> 'a"
   assumes pS: "p permutes S"
   shows "p (inv p x) = x"
-  and "inv p (p x) = x"
+    and "inv p (p x) = x"
   using permutes_inv_o[OF pS, unfolded fun_eq_iff o_def] by auto
 
-lemma permutes_subset: "p permutes S \<Longrightarrow> S \<subseteq> T ==> p permutes T"
+lemma permutes_subset: "p permutes S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> p permutes T"
   unfolding permutes_def by blast
 
 lemma permutes_empty[simp]: "p permutes {} \<longleftrightarrow> p = id"
-  unfolding fun_eq_iff permutes_def apply simp by metis
+  unfolding fun_eq_iff permutes_def by simp metis
 
 lemma permutes_sing[simp]: "p permutes {a} \<longleftrightarrow> p = id"
-  unfolding fun_eq_iff permutes_def apply simp by metis
+  unfolding fun_eq_iff permutes_def by simp metis
 
 lemma permutes_univ: "p permutes UNIV \<longleftrightarrow> (\<forall>y. \<exists>!x. p x = y)"
   unfolding permutes_def by simp
 
-lemma permutes_inv_eq: "p permutes S ==> inv p y = x \<longleftrightarrow> p x = y"
-  unfolding permutes_def inv_def apply auto
+lemma permutes_inv_eq: "p permutes S \<Longrightarrow> inv p y = x \<longleftrightarrow> p x = y"
+  unfolding permutes_def inv_def
+  apply auto
   apply (erule allE[where x=y])
   apply (erule allE[where x=y])
-  apply (rule someI_ex) apply blast
+  apply (rule someI_ex)
+  apply blast
   apply (rule some1_equality)
   apply blast
   apply blast
   done
 
-lemma permutes_swap_id: "a \<in> S \<Longrightarrow> b \<in> S ==> Fun.swap a b id permutes S"
-  unfolding permutes_def swap_def fun_upd_def  by auto metis
+lemma permutes_swap_id: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> Fun.swap a b id permutes S"
+  unfolding permutes_def swap_def fun_upd_def by auto metis
 
-lemma permutes_superset:
-  "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
-by (simp add: Ball_def permutes_def) metis
+lemma permutes_superset: "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
+  by (simp add: Ball_def permutes_def) metis
+
 
-(* ------------------------------------------------------------------------- *)
-(* Group properties.                                                         *)
-(* ------------------------------------------------------------------------- *)
+subsection {* Group properties *}
 
-lemma permutes_id: "id permutes S" unfolding permutes_def by simp
+lemma permutes_id: "id permutes S"
+  unfolding permutes_def by simp
 
-lemma permutes_compose: "p permutes S \<Longrightarrow> q permutes S ==> q o p permutes S"
+lemma permutes_compose: "p permutes S \<Longrightarrow> q permutes S \<Longrightarrow> q \<circ> p permutes S"
   unfolding permutes_def o_def by metis
 
-lemma permutes_inv: assumes pS: "p permutes S" shows "inv p permutes S"
+lemma permutes_inv:
+  assumes pS: "p permutes S"
+  shows "inv p permutes S"
   using pS unfolding permutes_def permutes_inv_eq[OF pS] by metis
 
-lemma permutes_inv_inv: assumes pS: "p permutes S" shows "inv (inv p) = p"
+lemma permutes_inv_inv:
+  assumes pS: "p permutes S"
+  shows "inv (inv p) = p"
   unfolding fun_eq_iff permutes_inv_eq[OF pS] permutes_inv_eq[OF permutes_inv[OF pS]]
   by blast
 
-(* ------------------------------------------------------------------------- *)
-(* The number of permutations on a finite set.                               *)
-(* ------------------------------------------------------------------------- *)
+
+subsection {* The number of permutations on a finite set *}
 
 lemma permutes_insert_lemma:
   assumes pS: "p permutes (insert a S)"
-  shows "Fun.swap a (p a) id o p permutes S"
+  shows "Fun.swap a (p a) id \<circ> p permutes S"
   apply (rule permutes_superset[where S = "insert a S"])
   apply (rule permutes_compose[OF pS])
   apply (rule permutes_swap_id, simp)
-  using permutes_in_image[OF pS, of a] apply simp
+  using permutes_in_image[OF pS, of a]
+  apply simp
   apply (auto simp add: Ball_def swap_def)
   done
 
 lemma permutes_insert: "{p. p permutes (insert a S)} =
-        (\<lambda>(b,p). Fun.swap a b id o p) ` {(b,p). b \<in> insert a S \<and> p \<in> {p. p permutes S}}"
-proof-
-
-  {fix p
-    {assume pS: "p permutes insert a S"
+  (\<lambda>(b,p). Fun.swap a b id \<circ> p) ` {(b,p). b \<in> insert a S \<and> p \<in> {p. p permutes S}}"
+proof -
+  {
+    fix p
+    {
+      assume pS: "p permutes insert a S"
       let ?b = "p a"
-      let ?q = "Fun.swap a (p a) id o p"
-      have th0: "p = Fun.swap a ?b id o ?q" unfolding fun_eq_iff o_assoc by simp
-      have th1: "?b \<in> insert a S " unfolding permutes_in_image[OF pS] by simp
+      let ?q = "Fun.swap a (p a) id \<circ> p"
+      have th0: "p = Fun.swap a ?b id \<circ> ?q"
+        unfolding fun_eq_iff o_assoc by simp
+      have th1: "?b \<in> insert a S"
+        unfolding permutes_in_image[OF pS] by simp
       from permutes_insert_lemma[OF pS] th0 th1
-      have "\<exists> b q. p = Fun.swap a b id o q \<and> b \<in> insert a S \<and> q permutes S" by blast}
+      have "\<exists>b q. p = Fun.swap a b id \<circ> q \<and> b \<in> insert a S \<and> q permutes S" by blast
+    }
     moreover
-    {fix b q assume bq: "p = Fun.swap a b id o q" "b \<in> insert a S" "q permutes S"
+    {
+      fix b q
+      assume bq: "p = Fun.swap a b id \<circ> q" "b \<in> insert a S" "q permutes S"
       from permutes_subset[OF bq(3), of "insert a S"]
-      have qS: "q permutes insert a S" by auto
-      have aS: "a \<in> insert a S" by simp
+      have qS: "q permutes insert a S"
+        by auto
+      have aS: "a \<in> insert a S"
+        by simp
       from bq(1) permutes_compose[OF qS permutes_swap_id[OF aS bq(2)]]
-      have "p permutes insert a S"  by simp }
-    ultimately have "p permutes insert a S \<longleftrightarrow> (\<exists> b q. p = Fun.swap a b id o q \<and> b \<in> insert a S \<and> q permutes S)" by blast}
-  thus ?thesis by auto
+      have "p permutes insert a S"
+        by simp
+    }
+    ultimately have "p permutes insert a S \<longleftrightarrow>
+        (\<exists>b q. p = Fun.swap a b id \<circ> q \<and> b \<in> insert a S \<and> q permutes S)"
+      by blast
+  }
+  then show ?thesis
+    by auto
 qed
 
-lemma card_permutations: assumes Sn: "card S = n" and fS: "finite S"
+lemma card_permutations:
+  assumes Sn: "card S = n"
+    and fS: "finite S"
   shows "card {p. p permutes S} = fact n"
-using fS Sn proof (induct arbitrary: n)
-  case empty thus ?case by simp
+  using fS Sn
+proof (induct arbitrary: n)
+  case empty
+  then show ?case by simp
 next
   case (insert x F)
-  { fix n assume H0: "card (insert x F) = n"
+  {
+    fix n
+    assume H0: "card (insert x F) = n"
     let ?xF = "{p. p permutes insert x F}"
     let ?pF = "{p. p permutes F}"
     let ?pF' = "{(b, p). b \<in> insert x F \<and> p \<in> ?pF}"
     let ?g = "(\<lambda>(b, p). Fun.swap x b id \<circ> p)"
     from permutes_insert[of x F]
     have xfgpF': "?xF = ?g ` ?pF'" .
-    have Fs: "card F = n - 1" using `x \<notin> F` H0 `finite F` by auto
-    from insert.hyps Fs have pFs: "card ?pF = fact (n - 1)" using `finite F` by auto
-    then have "finite ?pF" using fact_gt_zero_nat by (auto intro: card_ge_0_finite)
-    then have pF'f: "finite ?pF'" using H0 `finite F`
+    have Fs: "card F = n - 1"
+      using `x \<notin> F` H0 `finite F` by auto
+    from insert.hyps Fs have pFs: "card ?pF = fact (n - 1)"
+      using `finite F` by auto
+    then have "finite ?pF"
+      using fact_gt_zero_nat by (auto intro: card_ge_0_finite)
+    then have pF'f: "finite ?pF'"
+      using H0 `finite F`
       apply (simp only: Collect_split Collect_mem_eq)
       apply (rule finite_cartesian_product)
       apply simp_all
       done
 
     have ginj: "inj_on ?g ?pF'"
-    proof-
+    proof -
       {
-        fix b p c q assume bp: "(b,p) \<in> ?pF'" and cq: "(c,q) \<in> ?pF'"
-          and eq: "?g (b,p) = ?g (c,q)"
-        from bp cq have ths: "b \<in> insert x F" "c \<in> insert x F" "x \<in> insert x F" "p permutes F" "q permutes F" by auto
-        from ths(4) `x \<notin> F` eq have "b = ?g (b,p) x" unfolding permutes_def
+        fix b p c q
+        assume bp: "(b,p) \<in> ?pF'"
+        assume cq: "(c,q) \<in> ?pF'"
+        assume eq: "?g (b,p) = ?g (c,q)"
+        from bp cq have ths: "b \<in> insert x F" "c \<in> insert x F" "x \<in> insert x F"
+          "p permutes F" "q permutes F"
+          by auto
+        from ths(4) `x \<notin> F` eq have "b = ?g (b,p) x"
+          unfolding permutes_def
           by (auto simp add: swap_def fun_upd_def fun_eq_iff)
-        also have "\<dots> = ?g (c,q) x" using ths(5) `x \<notin> F` eq
+        also have "\<dots> = ?g (c,q) x"
+          using ths(5) `x \<notin> F` eq
           by (auto simp add: swap_def fun_upd_def fun_eq_iff)
-        also have "\<dots> = c"using ths(5) `x \<notin> F` unfolding permutes_def
+        also have "\<dots> = c"
+          using ths(5) `x \<notin> F`
+          unfolding permutes_def
           by (auto simp add: swap_def fun_upd_def fun_eq_iff)
         finally have bc: "b = c" .
-        hence "Fun.swap x b id = Fun.swap x c id" by simp
-        with eq have "Fun.swap x b id o p = Fun.swap x b id o q" by simp
-        hence "Fun.swap x b id o (Fun.swap x b id o p) = Fun.swap x b id o (Fun.swap x b id o q)" by simp
-        hence "p = q" by (simp add: o_assoc)
-        with bc have "(b,p) = (c,q)" by simp
+        then have "Fun.swap x b id = Fun.swap x c id"
+          by simp
+        with eq have "Fun.swap x b id \<circ> p = Fun.swap x b id \<circ> q"
+          by simp
+        then have "Fun.swap x b id \<circ> (Fun.swap x b id \<circ> p) =
+          Fun.swap x b id \<circ> (Fun.swap x b id \<circ> q)"
+          by simp
+        then have "p = q"
+          by (simp add: o_assoc)
+        with bc have "(b, p) = (c, q)"
+          by simp
       }
-      thus ?thesis  unfolding inj_on_def by blast
+      then show ?thesis
+        unfolding inj_on_def by blast
     qed
-    from `x \<notin> F` H0 have n0: "n \<noteq> 0 " using `finite F` by auto
-    hence "\<exists>m. n = Suc m" by presburger
-    then obtain m where n[simp]: "n = Suc m" by blast
+    from `x \<notin> F` H0 have n0: "n \<noteq> 0"
+      using `finite F` by auto
+    then have "\<exists>m. n = Suc m"
+      by presburger
+    then obtain m where n[simp]: "n = Suc m"
+      by blast
     from pFs H0 have xFc: "card ?xF = fact n"
-      unfolding xfgpF' card_image[OF ginj] using `finite F` `finite ?pF`
+      unfolding xfgpF' card_image[OF ginj]
+      using `finite F` `finite ?pF`
       apply (simp only: Collect_split Collect_mem_eq card_cartesian_product)
-      by simp
-    from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF" unfolding xfgpF' by simp
+      apply simp
+      done
+    from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF"
+      unfolding xfgpF' by simp
     have "card ?xF = fact n"
       using xFf xFc unfolding xFf by blast
   }
-  thus ?case using insert by simp
+  then show ?case
+    using insert by simp
 qed
 
-lemma finite_permutations: assumes fS: "finite S" shows "finite {p. p permutes S}"
+lemma finite_permutations:
+  assumes fS: "finite S"
+  shows "finite {p. p permutes S}"
   using card_permutations[OF refl fS] fact_gt_zero_nat
   by (auto intro: card_ge_0_finite)
 
-(* ------------------------------------------------------------------------- *)
-(* Permutations of index set for iterated operations.                        *)
-(* ------------------------------------------------------------------------- *)
+
+subsection {* Permutations of index set for iterated operations *}
 
 lemma (in comm_monoid_set) permute:
   assumes "p permutes S"
-  shows "F g S = F (g o p) S"
+  shows "F g S = F (g \<circ> p) S"
 proof -
-  from `p permutes S` have "inj p" by (rule permutes_inj)
-  then have "inj_on p S" by (auto intro: subset_inj_on)
-  then have "F g (p ` S) = F (g o p) S" by (rule reindex)
-  moreover from `p permutes S` have "p ` S = S" by (rule permutes_image)
-  ultimately show ?thesis by simp
+  from `p permutes S` have "inj p"
+    by (rule permutes_inj)
+  then have "inj_on p S"
+    by (auto intro: subset_inj_on)
+  then have "F g (p ` S) = F (g \<circ> p) S"
+    by (rule reindex)
+  moreover from `p permutes S` have "p ` S = S"
+    by (rule permutes_image)
+  ultimately show ?thesis
+    by simp
 qed
 
 lemma setsum_permute:
   assumes "p permutes S"
-  shows "setsum f S = setsum (f o p) S"
+  shows "setsum f S = setsum (f \<circ> p) S"
   using assms by (fact setsum.permute)
 
 lemma setsum_permute_natseg:
   assumes pS: "p permutes {m .. n}"
-  shows "setsum f {m .. n} = setsum (f o p) {m .. n}"
+  shows "setsum f {m .. n} = setsum (f \<circ> p) {m .. n}"
   using setsum_permute [OF pS, of f ] pS by blast
 
 lemma setprod_permute:
   assumes "p permutes S"
-  shows "setprod f S = setprod (f o p) S"
+  shows "setprod f S = setprod (f \<circ> p) S"
   using assms by (fact setprod.permute)
 
 lemma setprod_permute_natseg:
   assumes pS: "p permutes {m .. n}"
-  shows "setprod f {m .. n} = setprod (f o p) {m .. n}"
+  shows "setprod f {m .. n} = setprod (f \<circ> p) {m .. n}"
   using setprod_permute [OF pS, of f ] pS by blast
 
-(* ------------------------------------------------------------------------- *)
-(* Various combinations of transpositions with 2, 1 and 0 common elements.   *)
-(* ------------------------------------------------------------------------- *)
+
+subsection {* Various combinations of transpositions with 2, 1 and 0 common elements *}
+
+lemma swap_id_common:" a \<noteq> c \<Longrightarrow> b \<noteq> c \<Longrightarrow>
+  Fun.swap a b id \<circ> Fun.swap a c id = Fun.swap b c id \<circ> Fun.swap a b id"
+  by (simp add: fun_eq_iff swap_def)
 
-lemma swap_id_common:" a \<noteq> c \<Longrightarrow> b \<noteq> c \<Longrightarrow>  Fun.swap a b id o Fun.swap a c id = Fun.swap b c id o Fun.swap a b id" by (simp add: fun_eq_iff swap_def)
+lemma swap_id_common': "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow>
+  Fun.swap a c id \<circ> Fun.swap b c id = Fun.swap b c id \<circ> Fun.swap a b id"
+  by (simp add: fun_eq_iff swap_def)
 
-lemma swap_id_common': "~(a = b) \<Longrightarrow> ~(a = c) \<Longrightarrow> Fun.swap a c id o Fun.swap b c id = Fun.swap b c id o Fun.swap a b id" by (simp add: fun_eq_iff swap_def)
-
-lemma swap_id_independent: "~(a = c) \<Longrightarrow> ~(a = d) \<Longrightarrow> ~(b = c) \<Longrightarrow> ~(b = d) ==> Fun.swap a b id o Fun.swap c d id = Fun.swap c d id o Fun.swap a b id"
+lemma swap_id_independent: "a \<noteq> c \<Longrightarrow> a \<noteq> d \<Longrightarrow> b \<noteq> c \<Longrightarrow> b \<noteq> d \<Longrightarrow>
+  Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap c d id \<circ> Fun.swap a b id"
   by (simp add: swap_def fun_eq_iff)
 
-(* ------------------------------------------------------------------------- *)
-(* Permutations as transposition sequences.                                  *)
-(* ------------------------------------------------------------------------- *)
+
+subsection {* Permutations as transposition sequences *}
+
+inductive swapidseq :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool"
+where
+  id[simp]: "swapidseq 0 id"
+| comp_Suc: "swapidseq n p \<Longrightarrow> a \<noteq> b \<Longrightarrow> swapidseq (Suc n) (Fun.swap a b id \<circ> p)"
+
+declare id[unfolded id_def, simp]
+
+definition "permutation p \<longleftrightarrow> (\<exists>n. swapidseq n p)"
 
 
-inductive swapidseq :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" where
-  id[simp]: "swapidseq 0 id"
-| comp_Suc: "swapidseq n p \<Longrightarrow> a \<noteq> b \<Longrightarrow> swapidseq (Suc n) (Fun.swap a b id o p)"
-
-declare id[unfolded id_def, simp]
-definition "permutation p \<longleftrightarrow> (\<exists>n. swapidseq n p)"
+subsection {* Some closure properties of the set of permutations, with lengths *}
 
-(* ------------------------------------------------------------------------- *)
-(* Some closure properties of the set of permutations, with lengths.         *)
-(* ------------------------------------------------------------------------- *)
+lemma permutation_id[simp]: "permutation id"
+  unfolding permutation_def by (rule exI[where x=0]) simp
 
-lemma permutation_id[simp]: "permutation id"unfolding permutation_def
-  by (rule exI[where x=0], simp)
 declare permutation_id[unfolded id_def, simp]
 
 lemma swapidseq_swap: "swapidseq (if a = b then 0 else 1) (Fun.swap a b id)"
   apply clarsimp
-  using comp_Suc[of 0 id a b] by simp
+  using comp_Suc[of 0 id a b]
+  apply simp
+  done
 
 lemma permutation_swap_id: "permutation (Fun.swap a b id)"
-  apply (cases "a=b", simp_all)
-  unfolding permutation_def using swapidseq_swap[of a b] by blast
+  apply (cases "a = b")
+  apply simp_all
+  unfolding permutation_def
+  using swapidseq_swap[of a b]
+  apply blast
+  done
 
-lemma swapidseq_comp_add: "swapidseq n p \<Longrightarrow> swapidseq m q ==> swapidseq (n + m) (p o q)"
-  proof (induct n p arbitrary: m q rule: swapidseq.induct)
-    case (id m q) thus ?case by simp
-  next
-    case (comp_Suc n p a b m q)
-    have th: "Suc n + m = Suc (n + m)" by arith
-    show ?case unfolding th comp_assoc
-      apply (rule swapidseq.comp_Suc) using comp_Suc.hyps(2)[OF comp_Suc.prems]  comp_Suc.hyps(3) by blast+
+lemma swapidseq_comp_add: "swapidseq n p \<Longrightarrow> swapidseq m q \<Longrightarrow> swapidseq (n + m) (p \<circ> q)"
+proof (induct n p arbitrary: m q rule: swapidseq.induct)
+  case (id m q)
+  then show ?case by simp
+next
+  case (comp_Suc n p a b m q)
+  have th: "Suc n + m = Suc (n + m)"
+    by arith
+  show ?case
+    unfolding th comp_assoc
+    apply (rule swapidseq.comp_Suc)
+    using comp_Suc.hyps(2)[OF comp_Suc.prems] comp_Suc.hyps(3)
+    apply blast+
+    done
 qed
 
-lemma permutation_compose: "permutation p \<Longrightarrow> permutation q ==> permutation(p o q)"
+lemma permutation_compose: "permutation p \<Longrightarrow> permutation q \<Longrightarrow> permutation (p \<circ> q)"
   unfolding permutation_def using swapidseq_comp_add[of _ p _ q] by metis
 
-lemma swapidseq_endswap: "swapidseq n p \<Longrightarrow> a \<noteq> b ==> swapidseq (Suc n) (p o Fun.swap a b id)"
+lemma swapidseq_endswap: "swapidseq n p \<Longrightarrow> a \<noteq> b \<Longrightarrow> swapidseq (Suc n) (p \<circ> Fun.swap a b id)"
   apply (induct n p rule: swapidseq.induct)
   using swapidseq_swap[of a b]
-  by (auto simp add: comp_assoc intro: swapidseq.comp_Suc)
+  apply (auto simp add: comp_assoc intro: swapidseq.comp_Suc)
+  done
 
-lemma swapidseq_inverse_exists: "swapidseq n p ==> \<exists>q. swapidseq n q \<and> p o q = id \<and> q o p = id"
-proof(induct n p rule: swapidseq.induct)
-  case id  thus ?case by (rule exI[where x=id], simp)
+lemma swapidseq_inverse_exists: "swapidseq n p \<Longrightarrow> \<exists>q. swapidseq n q \<and> p \<circ> q = id \<and> q \<circ> p = id"
+proof (induct n p rule: swapidseq.induct)
+  case id
+  then show ?case
+    by (rule exI[where x=id]) simp
 next
   case (comp_Suc n p a b)
-  from comp_Suc.hyps obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" by blast
-  let ?q = "q o Fun.swap a b id"
+  from comp_Suc.hyps obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id"
+    by blast
+  let ?q = "q \<circ> Fun.swap a b id"
   note H = comp_Suc.hyps
-  from swapidseq_swap[of a b] H(3)  have th0: "swapidseq 1 (Fun.swap a b id)" by simp
-  from swapidseq_comp_add[OF q(1) th0] have th1:"swapidseq (Suc n) ?q" by simp
-  have "Fun.swap a b id o p o ?q = Fun.swap a b id o (p o q) o Fun.swap a b id" by (simp add: o_assoc)
-  also have "\<dots> = id" by (simp add: q(2))
-  finally have th2: "Fun.swap a b id o p o ?q = id" .
-  have "?q \<circ> (Fun.swap a b id \<circ> p) = q \<circ> (Fun.swap a b id o Fun.swap a b id) \<circ> p" by (simp only: o_assoc)
-  hence "?q \<circ> (Fun.swap a b id \<circ> p) = id" by (simp add: q(3))
-  with th1 th2 show ?case by blast
+  from swapidseq_swap[of a b] H(3) have th0: "swapidseq 1 (Fun.swap a b id)"
+    by simp
+  from swapidseq_comp_add[OF q(1) th0] have th1: "swapidseq (Suc n) ?q"
+    by simp
+  have "Fun.swap a b id \<circ> p \<circ> ?q = Fun.swap a b id \<circ> (p \<circ> q) \<circ> Fun.swap a b id"
+    by (simp add: o_assoc)
+  also have "\<dots> = id"
+    by (simp add: q(2))
+  finally have th2: "Fun.swap a b id \<circ> p \<circ> ?q = id" .
+  have "?q \<circ> (Fun.swap a b id \<circ> p) = q \<circ> (Fun.swap a b id \<circ> Fun.swap a b id) \<circ> p"
+    by (simp only: o_assoc)
+  then have "?q \<circ> (Fun.swap a b id \<circ> p) = id"
+    by (simp add: q(3))
+  with th1 th2 show ?case
+    by blast
 qed
 
+lemma swapidseq_inverse:
+  assumes H: "swapidseq n p"
+  shows "swapidseq n (inv p)"
+  using swapidseq_inverse_exists[OF H] inv_unique_comp[of p] by auto
+
+lemma permutation_inverse: "permutation p \<Longrightarrow> permutation (inv p)"
+  using permutation_def swapidseq_inverse by blast
+
 
-lemma swapidseq_inverse: assumes H: "swapidseq n p" shows "swapidseq n (inv p)"
-  using swapidseq_inverse_exists[OF H] inv_unique_comp[of p] by auto
-
-lemma permutation_inverse: "permutation p ==> permutation (inv p)"
-  using permutation_def swapidseq_inverse by blast
+subsection {* The identity map only has even transposition sequences *}
 
-(* ------------------------------------------------------------------------- *)
-(* The identity map only has even transposition sequences.                   *)
-(* ------------------------------------------------------------------------- *)
-
-lemma symmetry_lemma:"(\<And>a b c d. P a b c d ==> P a b d c) \<Longrightarrow>
-   (\<And>a b c d. a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow> (a = c \<and> b = d \<or>  a = c \<and> b \<noteq> d \<or> a \<noteq> c \<and> b = d \<or> a \<noteq> c \<and> a \<noteq> d \<and> b \<noteq> c \<and> b \<noteq> d) ==> P a b c d)
-   ==> (\<And>a b c d. a \<noteq> b --> c \<noteq> d \<longrightarrow>  P a b c d)" by metis
+lemma symmetry_lemma:
+  assumes "\<And>a b c d. P a b c d \<Longrightarrow> P a b d c"
+    and "\<And>a b c d. a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow>
+      a = c \<and> b = d \<or> a = c \<and> b \<noteq> d \<or> a \<noteq> c \<and> b = d \<or> a \<noteq> c \<and> a \<noteq> d \<and> b \<noteq> c \<and> b \<noteq> d \<Longrightarrow>
+      P a b c d"
+  shows "\<And>a b c d. a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow>  P a b c d"
+  using assms by metis
 
-lemma swap_general: "a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow> Fun.swap a b id o Fun.swap c d id = id \<or>
-  (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and> Fun.swap a b id o Fun.swap c d id = Fun.swap x y id o Fun.swap a z id)"
-proof-
-  assume H: "a\<noteq>b" "c\<noteq>d"
-have "a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow>
-(  Fun.swap a b id o Fun.swap c d id = id \<or>
-  (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and> Fun.swap a b id o Fun.swap c d id = Fun.swap x y id o Fun.swap a z id))"
-  apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d])
-  apply (simp_all only: swapid_sym)
-  apply (case_tac "a = c \<and> b = d", clarsimp simp only: swapid_sym swap_id_idempotent)
-  apply (case_tac "a = c \<and> b \<noteq> d")
-  apply (rule disjI2)
-  apply (rule_tac x="b" in exI)
-  apply (rule_tac x="d" in exI)
-  apply (rule_tac x="b" in exI)
-  apply (clarsimp simp add: fun_eq_iff swap_def)
-  apply (case_tac "a \<noteq> c \<and> b = d")
-  apply (rule disjI2)
-  apply (rule_tac x="c" in exI)
-  apply (rule_tac x="d" in exI)
-  apply (rule_tac x="c" in exI)
-  apply (clarsimp simp add: fun_eq_iff swap_def)
-  apply (rule disjI2)
-  apply (rule_tac x="c" in exI)
-  apply (rule_tac x="d" in exI)
-  apply (rule_tac x="b" in exI)
-  apply (clarsimp simp add: fun_eq_iff swap_def)
-  done
-with H show ?thesis by metis
+lemma swap_general: "a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow>
+  Fun.swap a b id \<circ> Fun.swap c d id = id \<or>
+  (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and>
+    Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap x y id \<circ> Fun.swap a z id)"
+proof -
+  assume H: "a \<noteq> b" "c \<noteq> d"
+  have "a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow>
+    (Fun.swap a b id \<circ> Fun.swap c d id = id \<or>
+      (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and>
+        Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap x y id \<circ> Fun.swap a z id))"
+    apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d])
+    apply (simp_all only: swapid_sym)
+    apply (case_tac "a = c \<and> b = d")
+    apply (clarsimp simp only: swapid_sym swap_id_idempotent)
+    apply (case_tac "a = c \<and> b \<noteq> d")
+    apply (rule disjI2)
+    apply (rule_tac x="b" in exI)
+    apply (rule_tac x="d" in exI)
+    apply (rule_tac x="b" in exI)
+    apply (clarsimp simp add: fun_eq_iff swap_def)
+    apply (case_tac "a \<noteq> c \<and> b = d")
+    apply (rule disjI2)
+    apply (rule_tac x="c" in exI)
+    apply (rule_tac x="d" in exI)
+    apply (rule_tac x="c" in exI)
+    apply (clarsimp simp add: fun_eq_iff swap_def)
+    apply (rule disjI2)
+    apply (rule_tac x="c" in exI)
+    apply (rule_tac x="d" in exI)
+    apply (rule_tac x="b" in exI)
+    apply (clarsimp simp add: fun_eq_iff swap_def)
+    done
+  with H show ?thesis by metis
 qed
 
 lemma swapidseq_id_iff[simp]: "swapidseq 0 p \<longleftrightarrow> p = id"
   using swapidseq.cases[of 0 p "p = id"]
   by auto
 
-lemma swapidseq_cases: "swapidseq n p \<longleftrightarrow> (n=0 \<and> p = id \<or> (\<exists>a b q m. n = Suc m \<and> p = Fun.swap a b id o q \<and> swapidseq m q \<and> a\<noteq> b))"
+lemma swapidseq_cases: "swapidseq n p \<longleftrightarrow>
+  n = 0 \<and> p = id \<or> (\<exists>a b q m. n = Suc m \<and> p = Fun.swap a b id \<circ> q \<and> swapidseq m q \<and> a \<noteq> b)"
   apply (rule iffI)
   apply (erule swapidseq.cases[of n p])
   apply simp
@@ -385,124 +479,161 @@
   apply auto
   apply (rule comp_Suc, simp_all)
   done
+
 lemma fixing_swapidseq_decrease:
-  assumes spn: "swapidseq n p" and ab: "a\<noteq>b" and pa: "(Fun.swap a b id o p) a = a"
-  shows "n \<noteq> 0 \<and> swapidseq (n - 1) (Fun.swap a b id o p)"
+  assumes spn: "swapidseq n p"
+    and ab: "a \<noteq> b"
+    and pa: "(Fun.swap a b id \<circ> p) a = a"
+  shows "n \<noteq> 0 \<and> swapidseq (n - 1) (Fun.swap a b id \<circ> p)"
   using spn ab pa
-proof(induct n arbitrary: p a b)
-  case 0 thus ?case by (auto simp add: swap_def fun_upd_def)
+proof (induct n arbitrary: p a b)
+  case 0
+  then show ?case
+    by (auto simp add: swap_def fun_upd_def)
 next
   case (Suc n p a b)
-  from Suc.prems(1) swapidseq_cases[of "Suc n" p] obtain
-    c d q m where cdqm: "Suc n = Suc m" "p = Fun.swap c d id o q" "swapidseq m q" "c \<noteq> d" "n = m"
+  from Suc.prems(1) swapidseq_cases[of "Suc n" p]
+  obtain c d q m where
+    cdqm: "Suc n = Suc m" "p = Fun.swap c d id \<circ> q" "swapidseq m q" "c \<noteq> d" "n = m"
     by auto
-  {assume H: "Fun.swap a b id o Fun.swap c d id = id"
-
-    have ?case apply (simp only: cdqm o_assoc H)
-      by (simp add: cdqm)}
+  {
+    assume H: "Fun.swap a b id \<circ> Fun.swap c d id = id"
+    have ?case by (simp only: cdqm o_assoc H) (simp add: cdqm)
+  }
   moreover
-  { fix x y z
-    assume H: "x\<noteq>a" "y\<noteq>a" "z \<noteq>a" "x \<noteq>y"
-      "Fun.swap a b id o Fun.swap c d id = Fun.swap x y id o Fun.swap a z id"
-    from H have az: "a \<noteq> z" by simp
+  {
+    fix x y z
+    assume H: "x \<noteq> a" "y \<noteq> a" "z \<noteq> a" "x \<noteq> y"
+      "Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap x y id \<circ> Fun.swap a z id"
+    from H have az: "a \<noteq> z"
+      by simp
 
-    {fix h have "(Fun.swap x y id o h) a = a \<longleftrightarrow> h a = a"
-      using H by (simp add: swap_def)}
+    {
+      fix h
+      have "(Fun.swap x y id \<circ> h) a = a \<longleftrightarrow> h a = a"
+        using H by (simp add: swap_def)
+    }
     note th3 = this
-    from cdqm(2) have "Fun.swap a b id o p = Fun.swap a b id o (Fun.swap c d id o q)" by simp
-    hence "Fun.swap a b id o p = Fun.swap x y id o (Fun.swap a z id o q)" by (simp add: o_assoc H)
-    hence "(Fun.swap a b id o p) a = (Fun.swap x y id o (Fun.swap a z id o q)) a" by simp
-    hence "(Fun.swap x y id o (Fun.swap a z id o q)) a  = a" unfolding Suc by metis
-    hence th1: "(Fun.swap a z id o q) a = a" unfolding th3 .
+    from cdqm(2) have "Fun.swap a b id \<circ> p = Fun.swap a b id \<circ> (Fun.swap c d id \<circ> q)"
+      by simp
+    then have "Fun.swap a b id \<circ> p = Fun.swap x y id \<circ> (Fun.swap a z id \<circ> q)"
+      by (simp add: o_assoc H)
+    then have "(Fun.swap a b id \<circ> p) a = (Fun.swap x y id \<circ> (Fun.swap a z id \<circ> q)) a"
+      by simp
+    then have "(Fun.swap x y id \<circ> (Fun.swap a z id \<circ> q)) a = a"
+      unfolding Suc by metis
+    then have th1: "(Fun.swap a z id \<circ> q) a = a"
+      unfolding th3 .
     from Suc.hyps[OF cdqm(3)[ unfolded cdqm(5)[symmetric]] az th1]
-    have th2: "swapidseq (n - 1) (Fun.swap a z id o q)" "n \<noteq> 0" by blast+
-    have th: "Suc n - 1 = Suc (n - 1)" using th2(2) by auto
-    have ?case unfolding cdqm(2) H o_assoc th
+    have th2: "swapidseq (n - 1) (Fun.swap a z id \<circ> q)" "n \<noteq> 0"
+      by blast+
+    have th: "Suc n - 1 = Suc (n - 1)"
+      using th2(2) by auto
+    have ?case
+      unfolding cdqm(2) H o_assoc th
       apply (simp only: Suc_not_Zero simp_thms comp_assoc)
       apply (rule comp_Suc)
-      using th2 H apply blast+
-      done}
-  ultimately show ?case using swap_general[OF Suc.prems(2) cdqm(4)] by metis
+      using th2 H
+      apply blast+
+      done
+  }
+  ultimately show ?case
+    using swap_general[OF Suc.prems(2) cdqm(4)] by metis
 qed
 
 lemma swapidseq_identity_even:
-  assumes "swapidseq n (id :: 'a \<Rightarrow> 'a)" shows "even n"
+  assumes "swapidseq n (id :: 'a \<Rightarrow> 'a)"
+  shows "even n"
   using `swapidseq n id`
-proof(induct n rule: nat_less_induct)
+proof (induct n rule: nat_less_induct)
   fix n
   assume H: "\<forall>m<n. swapidseq m (id::'a \<Rightarrow> 'a) \<longrightarrow> even m" "swapidseq n (id :: 'a \<Rightarrow> 'a)"
-  {assume "n = 0" hence "even n" by arith}
+  {
+    assume "n = 0"
+    then have "even n" by presburger
+  }
   moreover
-  {fix a b :: 'a and q m
+  {
+    fix a b :: 'a and q m
     assume h: "n = Suc m" "(id :: 'a \<Rightarrow> 'a) = Fun.swap a b id \<circ> q" "swapidseq m q" "a \<noteq> b"
     from fixing_swapidseq_decrease[OF h(3,4), unfolded h(2)[symmetric]]
-    have m: "m \<noteq> 0" "swapidseq (m - 1) (id :: 'a \<Rightarrow> 'a)" by auto
-    from h m have mn: "m - 1 < n" by arith
-    from H(1)[rule_format, OF mn m(2)] h(1) m(1) have "even n" apply arith done}
-  ultimately show "even n" using H(2)[unfolded swapidseq_cases[of n id]] by auto
+    have m: "m \<noteq> 0" "swapidseq (m - 1) (id :: 'a \<Rightarrow> 'a)"
+      by auto
+    from h m have mn: "m - 1 < n"
+      by arith
+    from H(1)[rule_format, OF mn m(2)] h(1) m(1) have "even n"
+      by presburger
+  }
+  ultimately show "even n"
+    using H(2)[unfolded swapidseq_cases[of n id]] by auto
 qed
 
-(* ------------------------------------------------------------------------- *)
-(* Therefore we have a welldefined notion of parity.                         *)
-(* ------------------------------------------------------------------------- *)
+
+subsection {* Therefore we have a welldefined notion of parity *}
 
 definition "evenperm p = even (SOME n. swapidseq n p)"
 
-lemma swapidseq_even_even: assumes
-  m: "swapidseq m p" and n: "swapidseq n p"
+lemma swapidseq_even_even:
+  assumes m: "swapidseq m p"
+    and n: "swapidseq n p"
   shows "even m \<longleftrightarrow> even n"
-proof-
+proof -
   from swapidseq_inverse_exists[OF n]
-  obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" by blast
-
+  obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id"
+    by blast
   from swapidseq_identity_even[OF swapidseq_comp_add[OF m q(1), unfolded q]]
-  show ?thesis by arith
+  show ?thesis
+    by arith
 qed
 
-lemma evenperm_unique: assumes p: "swapidseq n p" and n:"even n = b"
+lemma evenperm_unique:
+  assumes p: "swapidseq n p"
+    and n:"even n = b"
   shows "evenperm p = b"
   unfolding n[symmetric] evenperm_def
   apply (rule swapidseq_even_even[where p = p])
   apply (rule someI[where x = n])
-  using p by blast+
+  using p
+  apply blast+
+  done
 
-(* ------------------------------------------------------------------------- *)
-(* And it has the expected composition properties.                           *)
-(* ------------------------------------------------------------------------- *)
+
+subsection {* And it has the expected composition properties *}
 
 lemma evenperm_id[simp]: "evenperm id = True"
-  apply (rule evenperm_unique[where n = 0]) by simp_all
+  by (rule evenperm_unique[where n = 0]) simp_all
 
 lemma evenperm_swap: "evenperm (Fun.swap a b id) = (a = b)"
-apply (rule evenperm_unique[where n="if a = b then 0 else 1"])
-by (simp_all add: swapidseq_swap)
+  by (rule evenperm_unique[where n="if a = b then 0 else 1"]) (simp_all add: swapidseq_swap)
 
 lemma evenperm_comp:
-  assumes p: "permutation p" and q:"permutation q"
-  shows "evenperm (p o q) = (evenperm p = evenperm q)"
-proof-
-  from p q obtain
-    n m where n: "swapidseq n p" and m: "swapidseq m q"
+  assumes p: "permutation p"
+    and q:"permutation q"
+  shows "evenperm (p \<circ> q) = (evenperm p = evenperm q)"
+proof -
+  from p q obtain n m where n: "swapidseq n p" and m: "swapidseq m q"
     unfolding permutation_def by blast
   note nm =  swapidseq_comp_add[OF n m]
-  have th: "even (n + m) = (even n \<longleftrightarrow> even m)" by arith
+  have th: "even (n + m) = (even n \<longleftrightarrow> even m)"
+    by arith
   from evenperm_unique[OF n refl] evenperm_unique[OF m refl]
     evenperm_unique[OF nm th]
-  show ?thesis by blast
+  show ?thesis
+    by blast
 qed
 
-lemma evenperm_inv: assumes p: "permutation p"
+lemma evenperm_inv:
+  assumes p: "permutation p"
   shows "evenperm (inv p) = evenperm p"
-proof-
-  from p obtain n where n: "swapidseq n p" unfolding permutation_def by blast
+proof -
+  from p obtain n where n: "swapidseq n p"
+    unfolding permutation_def by blast
   from evenperm_unique[OF swapidseq_inverse[OF n] evenperm_unique[OF n refl, symmetric]]
   show ?thesis .
 qed
 
-(* ------------------------------------------------------------------------- *)
-(* A more abstract characterization of permutations.                         *)
-(* ------------------------------------------------------------------------- *)
 
+subsection {* A more abstract characterization of permutations *}
 
 lemma bij_iff: "bij f \<longleftrightarrow> (\<forall>x. \<exists>!y. f y = x)"
   unfolding bij_def inj_on_def surj_def
@@ -514,40 +645,50 @@
 lemma permutation_bijective:
   assumes p: "permutation p"
   shows "bij p"
-proof-
-  from p obtain n where n: "swapidseq n p" unfolding permutation_def by blast
-  from swapidseq_inverse_exists[OF n] obtain q where
-    q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" by blast
-  thus ?thesis unfolding bij_iff  apply (auto simp add: fun_eq_iff) apply metis done
+proof -
+  from p obtain n where n: "swapidseq n p"
+    unfolding permutation_def by blast
+  from swapidseq_inverse_exists[OF n]
+  obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id"
+    by blast
+  then show ?thesis unfolding bij_iff
+    apply (auto simp add: fun_eq_iff)
+    apply metis
+    done
 qed
 
-lemma permutation_finite_support: assumes p: "permutation p"
+lemma permutation_finite_support:
+  assumes p: "permutation p"
   shows "finite {x. p x \<noteq> x}"
-proof-
-  from p obtain n where n: "swapidseq n p" unfolding permutation_def by blast
+proof -
+  from p obtain n where n: "swapidseq n p"
+    unfolding permutation_def by blast
   from n show ?thesis
-  proof(induct n p rule: swapidseq.induct)
-    case id thus ?case by simp
+  proof (induct n p rule: swapidseq.induct)
+    case id
+    then show ?case by simp
   next
     case (comp_Suc n p a b)
     let ?S = "insert a (insert b {x. p x \<noteq> x})"
-    from comp_Suc.hyps(2) have fS: "finite ?S" by simp
-    from `a \<noteq> b` have th: "{x. (Fun.swap a b id o p) x \<noteq> x} \<subseteq> ?S"
+    from comp_Suc.hyps(2) have fS: "finite ?S"
+      by simp
+    from `a \<noteq> b` have th: "{x. (Fun.swap a b id \<circ> p) x \<noteq> x} \<subseteq> ?S"
       by (auto simp add: swap_def)
     from finite_subset[OF th fS] show ?case  .
-qed
+  qed
 qed
 
-lemma bij_inv_eq_iff: "bij p ==> x = inv p y \<longleftrightarrow> p x = y"
-  using surj_f_inv_f[of p] inv_f_f[of f] by (auto simp add: bij_def)
+lemma bij_inv_eq_iff: "bij p \<Longrightarrow> x = inv p y \<longleftrightarrow> p x = y"
+  using surj_f_inv_f[of p] by (auto simp add: bij_def)
 
 lemma bij_swap_comp:
-  assumes bp: "bij p" shows "Fun.swap a b id o p = Fun.swap (inv p a) (inv p b) p"
+  assumes bp: "bij p"
+  shows "Fun.swap a b id \<circ> p = Fun.swap (inv p a) (inv p b) p"
   using surj_f_inv_f[OF bij_is_surj[OF bp]]
   by (simp add: fun_eq_iff swap_def bij_inv_eq_iff[OF bp])
 
-lemma bij_swap_ompose_bij: "bij p \<Longrightarrow> bij (Fun.swap a b id o p)"
-proof-
+lemma bij_swap_ompose_bij: "bij p \<Longrightarrow> bij (Fun.swap a b id \<circ> p)"
+proof -
   assume H: "bij p"
   show ?thesis
     unfolding bij_swap_comp[OF H] bij_swap_iff
@@ -555,16 +696,20 @@
 qed
 
 lemma permutation_lemma:
-  assumes fS: "finite S" and p: "bij p" and pS: "\<forall>x. x\<notin> S \<longrightarrow> p x = x"
+  assumes fS: "finite S"
+    and p: "bij p"
+    and pS: "\<forall>x. x\<notin> S \<longrightarrow> p x = x"
   shows "permutation p"
-using fS p pS
-proof(induct S arbitrary: p rule: finite_induct)
-  case (empty p) thus ?case by simp
+  using fS p pS
+proof (induct S arbitrary: p rule: finite_induct)
+  case (empty p)
+  then show ?case by simp
 next
   case (insert a F p)
-  let ?r = "Fun.swap a (p a) id o p"
-  let ?q = "Fun.swap a (p a) id o ?r "
-  have raa: "?r a = a" by (simp add: swap_def)
+  let ?r = "Fun.swap a (p a) id \<circ> p"
+  let ?q = "Fun.swap a (p a) id \<circ> ?r"
+  have raa: "?r a = a"
+    by (simp add: swap_def)
   from bij_swap_ompose_bij[OF insert(4)]
   have br: "bij ?r"  .
 
@@ -572,136 +717,193 @@
     apply (clarsimp simp add: swap_def)
     apply (erule_tac x="x" in allE)
     apply auto
-    unfolding bij_iff apply metis
+    unfolding bij_iff
+    apply metis
     done
   from insert(3)[OF br th]
   have rp: "permutation ?r" .
-  have "permutation ?q" by (simp add: permutation_compose permutation_swap_id rp)
-  thus ?case by (simp add: o_assoc)
+  have "permutation ?q"
+    by (simp add: permutation_compose permutation_swap_id rp)
+  then show ?case
+    by (simp add: o_assoc)
 qed
 
 lemma permutation: "permutation p \<longleftrightarrow> bij p \<and> finite {x. p x \<noteq> x}"
   (is "?lhs \<longleftrightarrow> ?b \<and> ?f")
 proof
   assume p: ?lhs
-  from p permutation_bijective permutation_finite_support show "?b \<and> ?f" by auto
+  from p permutation_bijective permutation_finite_support show "?b \<and> ?f"
+    by auto
 next
-  assume bf: "?b \<and> ?f"
-  hence bf: "?f" "?b" by blast+
-  from permutation_lemma[OF bf] show ?lhs by blast
+  assume "?b \<and> ?f"
+  then have "?f" "?b" by blast+
+  from permutation_lemma[OF this] show ?lhs
+    by blast
 qed
 
-lemma permutation_inverse_works: assumes p: "permutation p"
-  shows "inv p o p = id" "p o inv p = id"
+lemma permutation_inverse_works:
+  assumes p: "permutation p"
+  shows "inv p \<circ> p = id"
+    and "p \<circ> inv p = id"
   using permutation_bijective [OF p]
   unfolding bij_def inj_iff surj_iff by auto
 
 lemma permutation_inverse_compose:
-  assumes p: "permutation p" and q: "permutation q"
-  shows "inv (p o q) = inv q o inv p"
-proof-
+  assumes p: "permutation p"
+    and q: "permutation q"
+  shows "inv (p \<circ> q) = inv q \<circ> inv p"
+proof -
   note ps = permutation_inverse_works[OF p]
   note qs = permutation_inverse_works[OF q]
-  have "p o q o (inv q o inv p) = p o (q o inv q) o inv p" by (simp add: o_assoc)
-  also have "\<dots> = id" by (simp add: ps qs)
-  finally have th0: "p o q o (inv q o inv p) = id" .
-  have "inv q o inv p o (p o q) = inv q o (inv p o p) o q" by (simp add: o_assoc)
-  also have "\<dots> = id" by (simp add: ps qs)
-  finally have th1: "inv q o inv p o (p o q) = id" .
+  have "p \<circ> q \<circ> (inv q \<circ> inv p) = p \<circ> (q \<circ> inv q) \<circ> inv p"
+    by (simp add: o_assoc)
+  also have "\<dots> = id"
+    by (simp add: ps qs)
+  finally have th0: "p \<circ> q \<circ> (inv q \<circ> inv p) = id" .
+  have "inv q \<circ> inv p \<circ> (p \<circ> q) = inv q \<circ> (inv p \<circ> p) \<circ> q"
+    by (simp add: o_assoc)
+  also have "\<dots> = id"
+    by (simp add: ps qs)
+  finally have th1: "inv q \<circ> inv p \<circ> (p \<circ> q) = id" .
   from inv_unique_comp[OF th0 th1] show ?thesis .
 qed
 
-(* ------------------------------------------------------------------------- *)
-(* Relation to "permutes".                                                   *)
-(* ------------------------------------------------------------------------- *)
+
+subsection {* Relation to "permutes" *}
 
 lemma permutation_permutes: "permutation p \<longleftrightarrow> (\<exists>S. finite S \<and> p permutes S)"
-unfolding permutation permutes_def bij_iff[symmetric]
-apply (rule iffI, clarify)
-apply (rule exI[where x="{x. p x \<noteq> x}"])
-apply simp
-apply clarsimp
-apply (rule_tac B="S" in finite_subset)
-apply auto
-done
+  unfolding permutation permutes_def bij_iff[symmetric]
+  apply (rule iffI, clarify)
+  apply (rule exI[where x="{x. p x \<noteq> x}"])
+  apply simp
+  apply clarsimp
+  apply (rule_tac B="S" in finite_subset)
+  apply auto
+  done
 
-(* ------------------------------------------------------------------------- *)
-(* Hence a sort of induction principle composing by swaps.                   *)
-(* ------------------------------------------------------------------------- *)
+
+subsection {* Hence a sort of induction principle composing by swaps *}
 
-lemma permutes_induct: "finite S \<Longrightarrow>  P id  \<Longrightarrow> (\<And> a b p. a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> P p \<Longrightarrow> P p \<Longrightarrow> permutation p ==> P (Fun.swap a b id o p))
-         ==> (\<And>p. p permutes S ==> P p)"
-proof(induct S rule: finite_induct)
-  case empty thus ?case by auto
+lemma permutes_induct: "finite S \<Longrightarrow> P id \<Longrightarrow>
+  (\<And> a b p. a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> P p \<Longrightarrow> P p \<Longrightarrow> permutation p \<Longrightarrow> P (Fun.swap a b id \<circ> p)) \<Longrightarrow>
+  (\<And>p. p permutes S \<Longrightarrow> P p)"
+proof (induct S rule: finite_induct)
+  case empty
+  then show ?case by auto
 next
   case (insert x F p)
-  let ?r = "Fun.swap x (p x) id o p"
-  let ?q = "Fun.swap x (p x) id o ?r"
-  have qp: "?q = p" by (simp add: o_assoc)
-  from permutes_insert_lemma[OF insert.prems(3)] insert have Pr: "P ?r" by blast
+  let ?r = "Fun.swap x (p x) id \<circ> p"
+  let ?q = "Fun.swap x (p x) id \<circ> ?r"
+  have qp: "?q = p"
+    by (simp add: o_assoc)
+  from permutes_insert_lemma[OF insert.prems(3)] insert have Pr: "P ?r"
+    by blast
   from permutes_in_image[OF insert.prems(3), of x]
-  have pxF: "p x \<in> insert x F" by simp
-  have xF: "x \<in> insert x F" by simp
+  have pxF: "p x \<in> insert x F"
+    by simp
+  have xF: "x \<in> insert x F"
+    by simp
   have rp: "permutation ?r"
     unfolding permutation_permutes using insert.hyps(1)
-      permutes_insert_lemma[OF insert.prems(3)] by blast
+      permutes_insert_lemma[OF insert.prems(3)]
+    by blast
   from insert.prems(2)[OF xF pxF Pr Pr rp]
-  show ?case  unfolding qp .
+  show ?case
+    unfolding qp .
 qed
 
-(* ------------------------------------------------------------------------- *)
-(* Sign of a permutation as a real number.                                   *)
-(* ------------------------------------------------------------------------- *)
+
+subsection {* Sign of a permutation as a real number *}
 
 definition "sign p = (if evenperm p then (1::int) else -1)"
 
-lemma sign_nz: "sign p \<noteq> 0" by (simp add: sign_def)
-lemma sign_id: "sign id = 1" by (simp add: sign_def)
-lemma sign_inverse: "permutation p ==> sign (inv p) = sign p"
+lemma sign_nz: "sign p \<noteq> 0"
+  by (simp add: sign_def)
+
+lemma sign_id: "sign id = 1"
+  by (simp add: sign_def)
+
+lemma sign_inverse: "permutation p \<Longrightarrow> sign (inv p) = sign p"
   by (simp add: sign_def evenperm_inv)
-lemma sign_compose: "permutation p \<Longrightarrow> permutation q ==> sign (p o q) = sign(p) * sign(q)" by (simp add: sign_def evenperm_comp)
+
+lemma sign_compose: "permutation p \<Longrightarrow> permutation q \<Longrightarrow> sign (p \<circ> q) = sign p * sign q"
+  by (simp add: sign_def evenperm_comp)
+
 lemma sign_swap_id: "sign (Fun.swap a b id) = (if a = b then 1 else -1)"
   by (simp add: sign_def evenperm_swap)
-lemma sign_idempotent: "sign p * sign p = 1" by (simp add: sign_def)
 
-(* ------------------------------------------------------------------------- *)
-(* More lemmas about permutations.                                           *)
-(* ------------------------------------------------------------------------- *)
+lemma sign_idempotent: "sign p * sign p = 1"
+  by (simp add: sign_def)
+
+
+subsection {* More lemmas about permutations *}
 
 lemma permutes_natset_le:
-  assumes p: "p permutes (S::'a::wellorder set)" and le: "\<forall>i \<in> S.  p i <= i" shows "p = id"
-proof-
-  {fix n
+  fixes S :: "'a::wellorder set"
+  assumes p: "p permutes S"
+    and le: "\<forall>i \<in> S. p i \<le> i"
+  shows "p = id"
+proof -
+  {
+    fix n
     have "p n = n"
       using p le
-    proof(induct n arbitrary: S rule: less_induct)
-      fix n S assume H: "\<And>m S. \<lbrakk>m < n; p permutes S; \<forall>i\<in>S. p i \<le> i\<rbrakk> \<Longrightarrow> p m = m"
+    proof (induct n arbitrary: S rule: less_induct)
+      fix n S
+      assume H:
+        "\<And>m S. m < n \<Longrightarrow> p permutes S \<Longrightarrow> \<forall>i\<in>S. p i \<le> i \<Longrightarrow> p m = m"
         "p permutes S" "\<forall>i \<in>S. p i \<le> i"
-      {assume "n \<notin> S"
-        with H(2) have "p n = n" unfolding permutes_def by metis}
+      {
+        assume "n \<notin> S"
+        with H(2) have "p n = n"
+          unfolding permutes_def by metis
+      }
       moreover
-      {assume ns: "n \<in> S"
-        from H(3)  ns have "p n < n \<or> p n = n" by auto
-        moreover{assume h: "p n < n"
-          from H h have "p (p n) = p n" by metis
-          with permutes_inj[OF H(2)] have "p n = n" unfolding inj_on_def by blast
-          with h have False by simp}
-        ultimately have "p n = n" by blast }
-      ultimately show "p n = n"  by blast
-    qed}
-  thus ?thesis by (auto simp add: fun_eq_iff)
+      {
+        assume ns: "n \<in> S"
+        from H(3)  ns have "p n < n \<or> p n = n"
+          by auto
+        moreover {
+          assume h: "p n < n"
+          from H h have "p (p n) = p n"
+            by metis
+          with permutes_inj[OF H(2)] have "p n = n"
+            unfolding inj_on_def by blast
+          with h have False
+            by simp
+        }
+        ultimately have "p n = n"
+          by blast
+      }
+      ultimately show "p n = n"
+        by blast
+    qed
+  }
+  then show ?thesis
+    by (auto simp add: fun_eq_iff)
 qed
 
 lemma permutes_natset_ge:
-  assumes p: "p permutes (S::'a::wellorder set)" and le: "\<forall>i \<in> S.  p i \<ge> i" shows "p = id"
-proof-
-  {fix i assume i: "i \<in> S"
-    from i permutes_in_image[OF permutes_inv[OF p]] have "inv p i \<in> S" by simp
-    with le have "p (inv p i) \<ge> inv p i" by blast
-    with permutes_inverses[OF p] have "i \<ge> inv p i" by simp}
-  then have th: "\<forall>i\<in>S. inv p i \<le> i"  by blast
+  fixes S :: "'a::wellorder set"
+  assumes p: "p permutes S"
+    and le: "\<forall>i \<in> S. p i \<ge> i"
+  shows "p = id"
+proof -
+  {
+    fix i
+    assume i: "i \<in> S"
+    from i permutes_in_image[OF permutes_inv[OF p]] have "inv p i \<in> S"
+      by simp
+    with le have "p (inv p i) \<ge> inv p i"
+      by blast
+    with permutes_inverses[OF p] have "i \<ge> inv p i"
+      by simp
+  }
+  then have th: "\<forall>i\<in>S. inv p i \<le> i"
+    by blast
   from permutes_natset_le[OF permutes_inv[OF p] th]
-  have "inv p = inv id" by simp
+  have "inv p = inv id"
+    by simp
   then show ?thesis
     apply (subst permutes_inv_inv[OF p, symmetric])
     apply (rule inv_unique_comp)
@@ -710,134 +912,160 @@
 qed
 
 lemma image_inverse_permutations: "{inv p |p. p permutes S} = {p. p permutes S}"
-apply (rule set_eqI)
-apply auto
-  using permutes_inv_inv permutes_inv apply auto
+  apply (rule set_eqI)
+  apply auto
+  using permutes_inv_inv permutes_inv
+  apply auto
   apply (rule_tac x="inv x" in exI)
   apply auto
   done
 
 lemma image_compose_permutations_left:
-  assumes q: "q permutes S" shows "{q o p | p. p permutes S} = {p . p permutes S}"
-apply (rule set_eqI)
-apply auto
-apply (rule permutes_compose)
-using q apply auto
-apply (rule_tac x = "inv q o x" in exI)
-by (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o)
+  assumes q: "q permutes S"
+  shows "{q \<circ> p | p. p permutes S} = {p . p permutes S}"
+  apply (rule set_eqI)
+  apply auto
+  apply (rule permutes_compose)
+  using q
+  apply auto
+  apply (rule_tac x = "inv q \<circ> x" in exI)
+  apply (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o)
+  done
 
 lemma image_compose_permutations_right:
   assumes q: "q permutes S"
-  shows "{p o q | p. p permutes S} = {p . p permutes S}"
-apply (rule set_eqI)
-apply auto
-apply (rule permutes_compose)
-using q apply auto
-apply (rule_tac x = "x o inv q" in exI)
-by (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o comp_assoc)
+  shows "{p \<circ> q | p. p permutes S} = {p . p permutes S}"
+  apply (rule set_eqI)
+  apply auto
+  apply (rule permutes_compose)
+  using q
+  apply auto
+  apply (rule_tac x = "x \<circ> inv q" in exI)
+  apply (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o comp_assoc)
+  done
 
-lemma permutes_in_seg: "p permutes {1 ..n} \<Longrightarrow> i \<in> {1..n} ==> 1 <= p i \<and> p i <= n"
-
-apply (simp add: permutes_def)
-apply metis
-done
+lemma permutes_in_seg: "p permutes {1 ..n} \<Longrightarrow> i \<in> {1..n} \<Longrightarrow> 1 \<le> p i \<and> p i \<le> n"
+  by (simp add: permutes_def) metis
 
-lemma setsum_permutations_inverse: "setsum f {p. p permutes S} = setsum (\<lambda>p. f(inv p)) {p. p permutes S}" (is "?lhs = ?rhs")
-proof-
+lemma setsum_permutations_inverse:
+  "setsum f {p. p permutes S} = setsum (\<lambda>p. f(inv p)) {p. p permutes S}"
+  (is "?lhs = ?rhs")
+proof -
   let ?S = "{p . p permutes S}"
-have th0: "inj_on inv ?S"
-proof(auto simp add: inj_on_def)
-  fix q r
-  assume q: "q permutes S" and r: "r permutes S" and qr: "inv q = inv r"
-  hence "inv (inv q) = inv (inv r)" by simp
-  with permutes_inv_inv[OF q] permutes_inv_inv[OF r]
-  show "q = r" by metis
-qed
-  have th1: "inv ` ?S = ?S" using image_inverse_permutations by blast
-  have th2: "?rhs = setsum (f o inv) ?S" by (simp add: o_def)
-  from setsum_reindex[OF th0, of f]  show ?thesis unfolding th1 th2 .
+  have th0: "inj_on inv ?S"
+  proof (auto simp add: inj_on_def)
+    fix q r
+    assume q: "q permutes S"
+      and r: "r permutes S"
+      and qr: "inv q = inv r"
+    then have "inv (inv q) = inv (inv r)"
+      by simp
+    with permutes_inv_inv[OF q] permutes_inv_inv[OF r] show "q = r"
+      by metis
+  qed
+  have th1: "inv ` ?S = ?S"
+    using image_inverse_permutations by blast
+  have th2: "?rhs = setsum (f \<circ> inv) ?S"
+    by (simp add: o_def)
+  from setsum_reindex[OF th0, of f] show ?thesis unfolding th1 th2 .
 qed
 
 lemma setum_permutations_compose_left:
   assumes q: "q permutes S"
-  shows "setsum f {p. p permutes S} =
-            setsum (\<lambda>p. f(q o p)) {p. p permutes S}" (is "?lhs = ?rhs")
-proof-
+  shows "setsum f {p. p permutes S} = setsum (\<lambda>p. f(q \<circ> p)) {p. p permutes S}"
+  (is "?lhs = ?rhs")
+proof -
   let ?S = "{p. p permutes S}"
-  have th0: "?rhs = setsum (f o (op o q)) ?S" by (simp add: o_def)
-  have th1: "inj_on (op o q) ?S"
-    apply (auto simp add: inj_on_def)
-  proof-
+  have th0: "?rhs = setsum (f \<circ> (op \<circ> q)) ?S"
+    by (simp add: o_def)
+  have th1: "inj_on (op \<circ> q) ?S"
+  proof (auto simp add: inj_on_def)
     fix p r
-    assume "p permutes S" and r:"r permutes S" and rp: "q \<circ> p = q \<circ> r"
-    hence "inv q o q o p = inv q o q o r" by (simp add: comp_assoc)
-    with permutes_inj[OF q, unfolded inj_iff]
-
-    show "p = r" by simp
+    assume "p permutes S"
+      and r: "r permutes S"
+      and rp: "q \<circ> p = q \<circ> r"
+    then have "inv q \<circ> q \<circ> p = inv q \<circ> q \<circ> r"
+      by (simp add: comp_assoc)
+    with permutes_inj[OF q, unfolded inj_iff] show "p = r"
+      by simp
   qed
-  have th3: "(op o q) ` ?S = ?S" using image_compose_permutations_left[OF q] by auto
-  from setsum_reindex[OF th1, of f]
-  show ?thesis unfolding th0 th1 th3 .
+  have th3: "(op \<circ> q) ` ?S = ?S"
+    using image_compose_permutations_left[OF q] by auto
+  from setsum_reindex[OF th1, of f] show ?thesis unfolding th0 th1 th3 .
 qed
 
 lemma sum_permutations_compose_right:
   assumes q: "q permutes S"
-  shows "setsum f {p. p permutes S} =
-            setsum (\<lambda>p. f(p o q)) {p. p permutes S}" (is "?lhs = ?rhs")
-proof-
+  shows "setsum f {p. p permutes S} = setsum (\<lambda>p. f(p \<circ> q)) {p. p permutes S}"
+  (is "?lhs = ?rhs")
+proof -
   let ?S = "{p. p permutes S}"
-  have th0: "?rhs = setsum (f o (\<lambda>p. p o q)) ?S" by (simp add: o_def)
-  have th1: "inj_on (\<lambda>p. p o q) ?S"
-    apply (auto simp add: inj_on_def)
-  proof-
+  have th0: "?rhs = setsum (f \<circ> (\<lambda>p. p \<circ> q)) ?S"
+    by (simp add: o_def)
+  have th1: "inj_on (\<lambda>p. p \<circ> q) ?S"
+  proof (auto simp add: inj_on_def)
     fix p r
-    assume "p permutes S" and r:"r permutes S" and rp: "p o q = r o q"
-    hence "p o (q o inv q)  = r o (q o inv q)" by (simp add: o_assoc)
-    with permutes_surj[OF q, unfolded surj_iff]
-
-    show "p = r" by simp
+    assume "p permutes S"
+      and r: "r permutes S"
+      and rp: "p \<circ> q = r \<circ> q"
+    then have "p \<circ> (q \<circ> inv q) = r \<circ> (q \<circ> inv q)"
+      by (simp add: o_assoc)
+    with permutes_surj[OF q, unfolded surj_iff] show "p = r"
+      by simp
   qed
-  have th3: "(\<lambda>p. p o q) ` ?S = ?S" using image_compose_permutations_right[OF q] by auto
+  have th3: "(\<lambda>p. p \<circ> q) ` ?S = ?S"
+    using image_compose_permutations_right[OF q] by auto
   from setsum_reindex[OF th1, of f]
   show ?thesis unfolding th0 th1 th3 .
 qed
 
-(* ------------------------------------------------------------------------- *)
-(* Sum over a set of permutations (could generalize to iteration).           *)
-(* ------------------------------------------------------------------------- *)
+
+subsection {* Sum over a set of permutations (could generalize to iteration) *}
 
 lemma setsum_over_permutations_insert:
-  assumes fS: "finite S" and aS: "a \<notin> S"
-  shows "setsum f {p. p permutes (insert a S)} = setsum (\<lambda>b. setsum (\<lambda>q. f (Fun.swap a b id o q)) {p. p permutes S}) (insert a S)"
-proof-
-  have th0: "\<And>f a b. (\<lambda>(b,p). f (Fun.swap a b id o p)) = f o (\<lambda>(b,p). Fun.swap a b id o p)"
+  assumes fS: "finite S"
+    and aS: "a \<notin> S"
+  shows "setsum f {p. p permutes (insert a S)} =
+    setsum (\<lambda>b. setsum (\<lambda>q. f (Fun.swap a b id \<circ> q)) {p. p permutes S}) (insert a S)"
+proof -
+  have th0: "\<And>f a b. (\<lambda>(b,p). f (Fun.swap a b id \<circ> p)) = f \<circ> (\<lambda>(b,p). Fun.swap a b id \<circ> p)"
     by (simp add: fun_eq_iff)
-  have th1: "\<And>P Q. P \<times> Q = {(a,b). a \<in> P \<and> b \<in> Q}" by blast
-  have th2: "\<And>P Q. P \<Longrightarrow> (P \<Longrightarrow> Q) \<Longrightarrow> P \<and> Q" by blast
+  have th1: "\<And>P Q. P \<times> Q = {(a,b). a \<in> P \<and> b \<in> Q}"
+    by blast
+  have th2: "\<And>P Q. P \<Longrightarrow> (P \<Longrightarrow> Q) \<Longrightarrow> P \<and> Q"
+    by blast
   show ?thesis
     unfolding permutes_insert
     unfolding setsum_cartesian_product
     unfolding  th1[symmetric]
     unfolding th0
-  proof(rule setsum_reindex)
+  proof (rule setsum_reindex)
     let ?f = "(\<lambda>(b, y). Fun.swap a b id \<circ> y)"
     let ?P = "{p. p permutes S}"
-    {fix b c p q assume b: "b \<in> insert a S" and c: "c \<in> insert a S"
-      and p: "p permutes S" and q: "q permutes S"
-      and eq: "Fun.swap a b id o p = Fun.swap a c id o q"
+    {
+      fix b c p q
+      assume b: "b \<in> insert a S"
+      assume c: "c \<in> insert a S"
+      assume p: "p permutes S"
+      assume q: "q permutes S"
+      assume eq: "Fun.swap a b id \<circ> p = Fun.swap a c id \<circ> q"
       from p q aS have pa: "p a = a" and qa: "q a = a"
         unfolding permutes_def by metis+
-      from eq have "(Fun.swap a b id o p) a  = (Fun.swap a c id o q) a" by simp
-      hence bc: "b = c"
-        by (simp add: permutes_def pa qa o_def fun_upd_def swap_def id_def cong del: if_weak_cong split: split_if_asm)
-      from eq[unfolded bc] have "(\<lambda>p. Fun.swap a c id o p) (Fun.swap a c id o p) = (\<lambda>p. Fun.swap a c id o p) (Fun.swap a c id o q)" by simp
-      hence "p = q" unfolding o_assoc swap_id_idempotent
+      from eq have "(Fun.swap a b id \<circ> p) a  = (Fun.swap a c id \<circ> q) a"
+        by simp
+      then have bc: "b = c"
+        by (simp add: permutes_def pa qa o_def fun_upd_def swap_def id_def
+            cong del: if_weak_cong split: split_if_asm)
+      from eq[unfolded bc] have "(\<lambda>p. Fun.swap a c id \<circ> p) (Fun.swap a c id \<circ> p) =
+        (\<lambda>p. Fun.swap a c id \<circ> p) (Fun.swap a c id \<circ> q)" by simp
+      then have "p = q"
+        unfolding o_assoc swap_id_idempotent
         by (simp add: o_def)
-      with bc have "b = c \<and> p = q" by blast
+      with bc have "b = c \<and> p = q"
+        by blast
     }
     then show "inj_on ?f (insert a S \<times> ?P)"
-      unfolding inj_on_def
-      apply clarify by metis
+      unfolding inj_on_def by clarify metis
   qed
 qed