author wenzelm Sat, 16 Nov 2013 18:31:30 +0100 changeset 54452 f3090621446e parent 54451 459cf6ee254e child 54453 b9d6e7acad38
tuned proofs;
```--- a/src/HOL/Library/Formal_Power_Series.thy	Sat Nov 16 18:08:57 2013 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Sat Nov 16 18:31:30 2013 +0100
@@ -415,7 +415,7 @@
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
-  thus ?case by (simp add: X_def fps_eq_iff)
+  then show ?case by (simp add: X_def fps_eq_iff)
next
case (Suc k)
{
@@ -578,13 +578,13 @@

-lemma fps_sum_rep_nth: "(setsum (%i. fps_const(a\$i)*X^i) {0..m})\$n =
+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))"
apply (auto simp add: fps_setsum_nth cond_value_iff cong del: if_weak_cong)
done

-lemma fps_notation: "(%n. setsum (%i. fps_const(a\$i) * X^i) {0..n}) ----> a"
+lemma fps_notation: "(\<lambda>n. setsum (\<lambda>i. fps_const(a\$i) * X^i) {0..n}) ----> a"
(is "?s ----> a")
proof -
{
@@ -596,7 +596,7 @@
{
fix n::nat
assume nn0: "n \<ge> n0"
-      then have thnn0: "(1/2)^n <= (1/2 :: real)^n0"
+      then have thnn0: "(1/2)^n \<le> (1/2 :: real)^n0"
by (auto intro: power_decreasing)
{
assume "?s n = a"
@@ -615,7 +615,7 @@
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> <= (1/2)^n0" using nn0
+        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" .
@@ -1080,7 +1080,7 @@
{
assume a0: "a\$0 = 0"
then have eq: "inverse a = 0" by (simp add: fps_inverse_def)
-    { assume "n = 0" hence ?thesis by simp }
+    { assume "n = 0" then have ?thesis by simp }
moreover
{
assume n: "n > 0"
@@ -1120,8 +1120,10 @@
proof-
from inverse_mult_eq_1[OF a0]
have "fps_deriv (inverse a * a) = 0" by simp
-  hence "inverse a * fps_deriv a + fps_deriv (inverse a) * a = 0" by simp
-  hence "inverse a * (inverse a * fps_deriv a + fps_deriv (inverse a) * a) = 0"  by simp
+  then have "inverse a * fps_deriv a + fps_deriv (inverse a) * a = 0"
+    by simp
+  then have "inverse a * (inverse a * fps_deriv a + fps_deriv (inverse a) * a) = 0"
+    by simp
with inverse_mult_eq_1[OF a0]
have "(inverse a)\<^sup>2 * fps_deriv a + fps_deriv (inverse a) = 0"
unfolding power2_eq_square
@@ -1140,13 +1142,15 @@
shows "inverse (a * b) = inverse a * inverse b"
proof -
{
-    assume a0: "a\$0 = 0" hence ab0: "(a*b)\$0 = 0" by (simp add: fps_mult_nth)
+    assume a0: "a\$0 = 0"
+    then have ab0: "(a*b)\$0 = 0" by (simp add: fps_mult_nth)
from a0 ab0 have th: "inverse a = 0" "inverse (a*b) = 0" by simp_all
have ?thesis unfolding th by simp
}
moreover
{
-    assume b0: "b\$0 = 0" hence ab0: "(a*b)\$0 = 0" by (simp add: fps_mult_nth)
+    assume b0: "b\$0 = 0"
+    then have ab0: "(a*b)\$0 = 0" by (simp add: fps_mult_nth)
from b0 ab0 have th: "inverse b = 0" "inverse (a*b) = 0" by simp_all
have ?thesis unfolding th by simp
}
@@ -1264,7 +1268,7 @@
also have "\<dots> = ?rhs \$ n"
proof (induct k)
case 0
-      thus ?case by (simp add: fps_setsum_nth)
+      then show ?case by (simp add: fps_setsum_nth)
next
case (Suc k)
note th = Suc.hyps[symmetric]
@@ -1335,7 +1339,7 @@
fix n:: nat
{
assume "n=0"
-      hence "a\$n = ((1 - ?X) * ?sa) \$ n"
+      then have "a\$n = ((1 - ?X) * ?sa) \$ n"
}
moreover
@@ -1391,16 +1395,19 @@
done

lemma append_natpermute_less_eq:
-  assumes h: "xs@ys \<in> natpermute n k"
+  assumes "xs @ ys \<in> natpermute n k"
shows "listsum xs \<le> n" and "listsum ys \<le> n"
proof -
-  from h have "listsum (xs @ ys) = n" by (simp add: natpermute_def)
-  hence "listsum xs + listsum ys = n" by simp
-  then show "listsum xs \<le> n" and "listsum ys \<le> n" by simp_all
+  from assms have "listsum (xs @ ys) = n"
+  then have "listsum xs + listsum ys = n"
+    by simp
+  then show "listsum xs \<le> n" and "listsum ys \<le> n"
+    by simp_all
qed

lemma natpermute_split:
-  assumes mn: "h \<le> k"
+  assumes "h \<le> k"
shows "natpermute n k =
(\<Union>m \<in>{0..n}. {l1 @ l2 |l1 l2. l1 \<in> natpermute m h \<and> l2 \<in> natpermute (n - m) (k - h)})"
(is "?L = ?R" is "?L = (\<Union>m \<in>{0..n}. ?S m)")
@@ -1419,7 +1426,7 @@
have "l \<in> ?L" using leq xs ys h
unfolding xs' ys'
-      using mn xs ys
+      using assms xs ys
unfolding natpermute_def
apply simp
done
@@ -1433,12 +1440,12 @@
let ?m = "listsum ?xs"
from l have ls: "listsum (?xs @ ?ys) = n"
-    have xs: "?xs \<in> natpermute ?m h" using l mn
+    have xs: "?xs \<in> natpermute ?m h" using l assms
have l_take_drop: "listsum l = listsum (take h l @ drop h l)"
by simp
then have ys: "?ys \<in> natpermute (n - ?m) (k - h)"
-      using l mn ls by (auto simp add: natpermute_def simp del: append_take_drop_id)
+      using l assms ls by (auto simp add: natpermute_def simp del: append_take_drop_id)
from ls have m: "?m \<in> {0..n}"
by (simp add: l_take_drop del: append_take_drop_id)
from xs ys ls have "l \<in> ?R"
@@ -1544,7 +1551,7 @@
ultimately show ?thesis by auto
qed

-    (* The general form *)
+text {* The general form *}
lemma fps_setprod_nth:
fixes m :: nat
and a :: "nat \<Rightarrow> ('a::comm_ring_1) fps"
@@ -1565,9 +1572,7 @@
case (Suc k)
then have km: "k < m" by arith
have u0: "{0 .. k} \<union> {m} = {0..m}"
-      using Suc apply (simp add: set_eq_iff)
-      apply presburger
-      done
+      using Suc by (simp add: set_eq_iff) presburger
have f0: "finite {0 .. k}" "finite {m}" by auto
have d0: "{0 .. k} \<inter> {m} = {}" using Suc by auto
have "(setprod a {0 .. m}) \$ n = (setprod a {0 .. k} * a m) \$ n"
@@ -1606,18 +1611,21 @@
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}" by (simp add: setprod_constant)
+  have th0: "a^Suc m = setprod (\<lambda>i. a) {0..m}"
show ?thesis unfolding th0 fps_setprod_nth ..
qed

lemma fps_power_nth:
-  fixes m :: nat and a :: "('a::comm_ring_1) fps"
+  fixes m :: nat
+    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"
+  fixes m :: nat
+    and a :: "('a::{comm_ring_1}) fps"
shows "(a ^m)\$0 = (a\$0) ^ m"
proof (cases m)
case 0
@@ -1650,7 +1658,7 @@
{
assume n0: "n=0"
from h have "(b oo a)\$n = (c oo a)\$n" by simp
-        hence "b\$n = c\$n" using n0 by (simp add: fps_compose_nth)
+        then have "b\$n = c\$n" using n0 by (simp add: fps_compose_nth)
}
moreover
{
@@ -1767,7 +1775,7 @@
qed

lemma natpermute_max_card:
-  assumes n0: "n\<noteq>0"
+  assumes n0: "n \<noteq> 0"
shows "card {xs \<in> natpermute n (k+1). n \<in> set xs} = k + 1"
unfolding natpermute_contain_maximal
proof -
@@ -1793,7 +1801,8 @@
then show "{replicate (k + 1) 0[i := n]} \<inter> {replicate (k + 1) 0[j := n]} = {}"
by auto
qed
-  from card_UN_disjoint[OF fK fAK d] show "card (\<Union>i\<in>{0..k}. {replicate (k + 1) 0[i := n]}) = k+1"
+  from card_UN_disjoint[OF fK fAK d]
+  show "card (\<Union>i\<in>{0..k}. {replicate (k + 1) 0[i := n]}) = k + 1"
by simp
qed

@@ -1801,7 +1810,7 @@
fixes a:: "'a::field_char_0 fps"
assumes a0: "a\$0 \<noteq> 0"
shows "(r (Suc k) (a\$0)) ^ Suc k = a\$0 \<longleftrightarrow> (fps_radical r (Suc k) a) ^ (Suc k) = a"
-proof-
+proof -
let ?r = "fps_radical r (Suc k) a"
{
assume r0: "(r (Suc k) (a\$0)) ^ Suc k = a\$0"
@@ -1814,7 +1823,7 @@
assume H: "\<forall>m<n. ?r ^ Suc k \$ m = a\$m"
{
assume "n = 0"
-          hence "?r ^ Suc k \$ n = a \$n"
+          then have "?r ^ Suc k \$ n = a \$n"
using fps_radical_power_nth[of r "Suc k" a, OF r0] by simp
}
moreover
@@ -1865,7 +1874,7 @@
moreover
{
assume h: "(fps_radical r (Suc k) a) ^ (Suc k) = a"
-    hence "((fps_radical r (Suc k) a) ^ (Suc k))\$0 = a\$0" by simp
+    then have "((fps_radical r (Suc k) a) ^ (Suc k))\$0 = a\$0" by simp
then have "(r (Suc k) (a\$0)) ^ Suc k = a\$0"
unfolding fps_power_nth_Suc
by (simp add: setprod_constant del: replicate.simps)
@@ -1884,7 +1893,7 @@
{fix z have "?r ^ Suc k \$ z = a\$z"
proof(induct z rule: nat_less_induct)
fix n assume H: "\<forall>m<n. ?r ^ Suc k \$ m = a\$m"
-      {assume "n = 0" hence "?r ^ Suc k \$ n = a \$n"
+      {assume "n = 0" then have "?r ^ Suc k \$ n = a \$n"
using fps_radical_power_nth[of r "Suc k" a, OF r0] by simp}
moreover
{fix n1 assume n1: "n = Suc n1"
@@ -1928,13 +1937,13 @@

*)
lemma eq_divide_imp':
-  assumes c0: "(c::'a::field) ~= 0"
+  assumes c0: "(c::'a::field) \<noteq> 0"
and eq: "a * c = b"
shows "a = b / c"
proof -
from eq have "a * c * inverse c = b * inverse c"
by simp
-  hence "a * (inverse c * c) = b/c"
+  then have "a * (inverse c * c) = b/c"
by (simp only: field_simps divide_inverse)
then show "a = b/c"
unfolding  field_inverse[OF c0] by simp
@@ -1966,7 +1975,7 @@
assume h: "\<forall>m<n. a\$m = ?r \$m"
{
assume "n = 0"
-          hence "a\$n = ?r \$n" using a0 by simp
+          then have "a\$n = ?r \$n" using a0 by simp
}
moreover
{
@@ -1994,7 +2003,8 @@
by (auto simp del: replicate.simps)
have "(\<Prod>j\<in>{0..k}. a \$ v ! j) = (\<Prod>j\<in>{0..k}. if j = i then a \$ n else r (Suc k) (b\$0))"
apply (rule setprod_cong, simp)
-            using i a0 apply (simp del: replicate.simps)
+            using i a0
+            apply (simp del: replicate.simps)
done
also have "\<dots> = a \$ n * (?r \$ 0)^k"
using i by (simp add: setprod_gen_delta)
@@ -2100,11 +2110,11 @@
from iffD1[OF power_radical[of a r], OF a0 r0]
have "fps_deriv (?r ^ Suc k) = fps_deriv a"
by simp
-  hence "fps_deriv ?r * ?w = fps_deriv a"
+  then have "fps_deriv ?r * ?w = fps_deriv a"
by (simp add: fps_deriv_power mult_ac del: power_Suc)
-  hence "?iw * fps_deriv ?r * ?w = ?iw * fps_deriv a"
+  then have "?iw * fps_deriv ?r * ?w = ?iw * fps_deriv a"
by simp
-  hence "fps_deriv ?r * (?iw * ?w) = fps_deriv a / ?w"
+  then have "fps_deriv ?r * (?iw * ?w) = fps_deriv a / ?w"
then show ?thesis unfolding th0 by simp
qed
@@ -2125,7 +2135,7 @@
by (simp add: fps_mult_nth ra0 rb0 power_mult_distrib)
{
assume "k = 0"
-      hence ?thesis using r0' by simp
+      then have ?thesis using r0' by simp
}
moreover
{
@@ -2145,7 +2155,7 @@
moreover
{
+    then have "(fps_radical r k (a*b))\$0 = (fps_radical r k a * fps_radical r k b)\$0"
by simp
then have "r k ((a * b) \$ 0) = r k (a \$ 0) * r k (b \$ 0)"
using k by (simp add: fps_mult_nth)
@@ -2166,7 +2176,7 @@
proof-
from r0' have r0: "(r (k) ((a*b)\$0)) ^ k = (a*b)\$0"
by (simp add: fps_mult_nth ra0 rb0 power_mult_distrib)
-  {assume "k=0" hence ?thesis by simp}
+  {assume "k=0" then have ?thesis by simp}
moreover
{fix h assume k: "k = Suc h"
let ?ra = "fps_radical r (Suc h) a"
@@ -2447,7 +2457,8 @@
qed

lemma convolution_eq:
-  "setsum (%i. a (i :: nat) * b (n - i)) {0 .. n} = setsum (%(i,j). a i * b j) {(i,j). i <= n \<and> j \<le> n \<and> i + j = n}"
+  "setsum (\<lambda>i. a (i :: nat) * b (n - i)) {0 .. n} =
+    setsum (\<lambda>(i,j). a i * b j) {(i,j). i \<le> n \<and> j \<le> n \<and> i + j = n}"
apply (rule setsum_reindex_cong[where f=fst])
apply (auto simp add: set_eq_iff image_iff)
@@ -2461,7 +2472,7 @@
assumes c0: "c\$0 = (0::'a::idom)"
and d0: "d\$0 = 0"
shows "((a oo c) * (b oo d))\$n =
-    setsum (%(k,m). a\$k * b\$m * (c^k * d^m) \$ n) {(k,m). k + m \<le> n}" (is "?l = ?r")
+    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}"
have s: "?S \<subseteq> {0..n} <*> {0..n}" by (auto simp add: subset_eq)
@@ -2469,7 +2480,7 @@
apply (rule finite_subset[OF s])
apply auto
done
-  have "?r =  setsum (%i. setsum (%(k,m). a\$k * (c^k)\$i * b\$m * (d^m) \$ (n - i)) {(k,m). k + m \<le> n}) {0..n}"
+  have "?r =  setsum (\<lambda>i. setsum (\<lambda>(k,m). a\$k * (c^k)\$i * b\$m * (d^m) \$ (n - i)) {(k,m). k + m \<le> n}) {0..n}"
apply (subst setsum_commute)
apply (rule setsum_cong2)
@@ -2480,7 +2491,8 @@
apply (rule setsum_cong2)
apply (rule setsum_mono_zero_right[OF f])
-    apply (simp add: subset_eq) apply presburger
+    apply presburger
apply clarsimp
apply (rule ccontr)
@@ -2499,7 +2511,7 @@
assumes c0: "c\$0 = (0::'a::idom)"
and d0: "d\$0 = 0"
shows "((a oo c) * (b oo d))\$n =
-    setsum (%k. setsum (%m. a\$k * b\$m * (c^k * d^m) \$ n) {0..n}) {0..n}" (is "?l = ?r")
+    setsum (\<lambda>k. setsum (\<lambda>m. a\$k * b\$m * (c^k * d^m) \$ n) {0..n}) {0..n}"  (is "?l = ?r")
unfolding product_composition_lemma[OF c0 d0]
unfolding setsum_cartesian_product
apply (rule setsum_mono_zero_left)
@@ -2523,12 +2535,12 @@

lemma setsum_pair_less_iff:
-  "setsum (%((k::nat),m). a k * b m * c (k + m)) {(k,m). k + m \<le> n} =
-    setsum (%s. setsum (%i. a i * b (s - i) * c s) {0..s}) {0..n}"
+  "setsum (\<lambda>((k::nat),m). a k * b m * c (k + m)) {(k,m). k + m \<le> n} =
+    setsum (\<lambda>s. setsum (\<lambda>i. a i * b (s - i) * c s) {0..s}) {0..n}"
(is "?l = ?r")
proof -
let ?KM = "{(k,m). k + m \<le> n}"
-  let ?f = "%s. UNION {(0::nat)..s} (%i. {(i,s - i)})"
+  let ?f = "\<lambda>s. UNION {(0::nat)..s} (\<lambda>i. {(i,s - i)})"
have th0: "?KM = UNION {0..n} ?f"
apply presburger (* FIXME: slow! *)
@@ -2545,10 +2557,10 @@
lemma fps_compose_mult_distrib_lemma:
assumes c0: "c\$0 = (0::'a::idom)"
shows "((a oo c) * (b oo c))\$n =
-    setsum (%s. setsum (%i. a\$i * b\$(s - i) * (c^s) \$ n) {0..s}) {0..n}"
+    setsum (\<lambda>s. setsum (\<lambda>i. a\$i * b\$(s - i) * (c^s) \$ n) {0..s}) {0..n}"
(is "?l = ?r")
-  unfolding setsum_pair_less_iff[where a = "%k. a\$k" and b="%m. b\$m" and c="%s. (c ^ s)\$n" and n = n] ..
+  unfolding setsum_pair_less_iff[where a = "\<lambda>k. a\$k" and b="\<lambda>m. b\$m" and c="\<lambda>s. (c ^ s)\$n" and n = n] ..

lemma fps_compose_mult_distrib:
@@ -2560,7 +2572,7 @@

lemma fps_compose_setprod_distrib:
assumes c0: "c\$0 = (0::'a::idom)"
-  shows "(setprod a S) oo c = setprod (%k. a k oo c) S" (is "?l = ?r")
+  shows "setprod a S oo c = setprod (\<lambda>k. a k oo c) S"
apply (cases "finite S")
apply simp_all
apply (induct S rule: finite_induct)
@@ -2577,7 +2589,7 @@
then show ?thesis by simp
next
case (Suc m)
-  have th0: "a^n = setprod (%k. a) {0..m}" "(a oo c) ^ n = setprod (%k. a oo c) {0..m}"
+  have th0: "a^n = setprod (\<lambda>k. a) {0..m}" "(a oo c) ^ n = setprod (\<lambda>k. a oo c) {0..m}"
then show ?thesis
@@ -2607,7 +2619,7 @@
unfolding fps_compose_mult_distrib[OF b0, symmetric]
unfolding inverse_mult_eq_1[OF a0]
fps_compose_1 ..
-
+
then have "(?ia oo b) *  (a oo b) * ?iab  = 1 * ?iab" by simp
then have "(?ia oo b) *  (?iab * (a oo b))  = ?iab" by simp
then show ?thesis unfolding inverse_mult_eq_1[OF ab0] by simp
@@ -2629,8 +2641,8 @@
have th0: "(1 - X) \$ 0 \<noteq> (0::'a)" by simp
from fps_inverse_gp[where ?'a = 'a]
have "inverse ?one = 1 - X" by (simp add: fps_eq_iff)
-  hence "inverse (inverse ?one) = inverse (1 - X)" by simp
-  hence th: "?one = 1/(1 - X)" unfolding fps_inverse_idempotent[OF o0]
+  then have "inverse (inverse ?one) = inverse (1 - X)" by simp
+  then have th: "?one = 1/(1 - X)" unfolding fps_inverse_idempotent[OF o0]
show ?thesis
unfolding th
@@ -2706,13 +2718,13 @@
fix n
{
assume kn: "k>n"
-      hence "?l \$ n = ?r \$n" using a0 startsby_zero_power_prefix[OF a0] Suc
+      then have "?l \$ n = ?r \$n" using a0 startsby_zero_power_prefix[OF a0] Suc
by (simp add: fps_compose_nth del: power_Suc)
}
moreover
{
assume kn: "k \<le> n"
-      hence "?l\$n = ?r\$n"
+      then have "?l\$n = ?r\$n"
by (simp add: fps_compose_nth mult_delta_left setsum_delta)
}
moreover have "k >n \<or> k\<le> n"  by arith
@@ -2751,7 +2763,7 @@
have th0: "?d\$0 \<noteq> 0" using a1 by (simp add: fps_compose_nth)
from fps_inv_right[OF a0 a1] have "?d * ?dia = 1"
by (simp add: fps_compose_deriv[OF ia0, of a, symmetric] )
-  hence "inverse ?d * ?d * ?dia = inverse ?d * 1" by simp
+  then have "inverse ?d * ?d * ?dia = inverse ?d * 1" by simp
with inverse_mult_eq_1 [OF th0]
show "?dia = inverse ?d" by simp
qed
@@ -2988,7 +3000,7 @@
subsubsection{* Logarithmic series *}

lemma Abs_fps_if_0:
-  "Abs_fps(%n. if n=0 then (v::'a::ring_1) else f n) = fps_const v + X * Abs_fps (%n. f (Suc n))"
+  "Abs_fps(\<lambda>n. if n=0 then (v::'a::ring_1) else f n) = fps_const v + X * Abs_fps (\<lambda>n. f (Suc n))"

definition L :: "'a::field_char_0 \<Rightarrow> 'a fps"
@@ -3004,8 +3016,9 @@
lemma L_0[simp]: "L c \$ 0 = 0" by (simp add: L_def)

lemma L_E_inv:
-  assumes a: "a\<noteq> (0::'a::{field_char_0})"
-  shows "L a = fps_inv (E a - 1)" (is "?l = ?r")
+  fixes a :: "'a::field_char_0"
+  assumes a: "a \<noteq> 0"
+  shows "L a = fps_inv (E a - 1)"  (is "?l = ?r")
proof -
let ?b = "E a - 1"
have b0: "?b \$ 0 = 0" by simp
@@ -3022,7 +3035,7 @@
have "fps_deriv (fps_inv ?b) = fps_const (inverse a) / (X + 1)"
using a
by (simp add: fps_const_inverse eq fps_divide_def fps_inverse_mult)
-  hence "fps_deriv ?l = fps_deriv ?r"
+  then have "fps_deriv ?l = fps_deriv ?r"
then show ?thesis unfolding fps_deriv_eq_iff
@@ -3085,10 +3098,10 @@
have "a\$n = (c gchoose n) * a\$0"
proof (induct n)
case 0
-        thus ?case by simp
+        then show ?case by simp
next
case (Suc m)
-        thus ?case unfolding th0
+        then show ?case unfolding th0
apply (simp add: field_simps del: of_nat_Suc)
unfolding mult_assoc[symmetric] gbinomial_mult_1
@@ -3142,7 +3155,7 @@
have "?P = fps_const (?P\$0) * ?b (c + d)"
unfolding fps_binomial_ODE_unique[symmetric]
using th0 by simp
-  hence "?P = 0" by (simp add: fps_mult_nth)
+  then have "?P = 0" by (simp add: fps_mult_nth)
then show ?thesis by simp
qed

@@ -3189,14 +3202,14 @@
lemma Vandermonde_pochhammer_lemma:
fixes a :: "'a::field_char_0"
assumes b: "\<forall> j\<in>{0 ..<n}. b \<noteq> of_nat j"
-  shows "setsum (%k. (pochhammer (- a) k * pochhammer (- (of_nat n)) k) /
+  shows "setsum (\<lambda>k. (pochhammer (- a) k * pochhammer (- (of_nat n)) k) /
(of_nat (fact k) * pochhammer (b - of_nat n + 1) k)) {0..n} =
-    pochhammer (- (a+ b)) n / pochhammer (- b) n"
+    pochhammer (- (a + b)) n / pochhammer (- b) n"
(is "?l = ?r")
proof -
-  let ?m1 = "%m. (- 1 :: 'a) ^ m"
-  let ?f = "%m. of_nat (fact m)"
-  let ?p = "%(x::'a). pochhammer (- x)"
+  let ?m1 = "\<lambda>m. (- 1 :: 'a) ^ m"
+  let ?f = "\<lambda>m. of_nat (fact m)"
+  let ?p = "\<lambda>(x::'a). pochhammer (- x)"
from b have bn0: "?p b n \<noteq> 0" unfolding pochhammer_eq_0_iff by simp
{
fix k
@@ -3241,7 +3254,7 @@
moreover
{
assume nk: "k \<noteq> n"
-        have m1nk: "?m1 n = setprod (%i. - 1) {0..m}" "?m1 k = setprod (%i. - 1) {0..h}"
+        have m1nk: "?m1 n = setprod (\<lambda>i. - 1) {0..m}" "?m1 k = setprod (\<lambda>i. - 1) {0..h}"
by (simp_all add: setprod_constant m h)
from kn nk have kn': "k < n" by simp
have bnz0: "pochhammer (b - of_nat n + 1) k \<noteq> 0"
@@ -3251,9 +3264,9 @@
apply (erule_tac x= "n - ka - 1" in allE)
apply (auto simp add: algebra_simps of_nat_diff)
done
-        have eq1: "setprod (%k. (1::'a) + of_nat m - of_nat k) {0 .. h} =
+        have eq1: "setprod (\<lambda>k. (1::'a) + of_nat m - of_nat k) {0 .. h} =
setprod of_nat {Suc (m - h) .. Suc m}"
-          apply (rule strong_setprod_reindex_cong[where f="%k. Suc m - k "])
+          apply (rule strong_setprod_reindex_cong[where f="\<lambda>k. Suc m - k "])
using kn' h m
apply (auto simp add: inj_on_def image_def)
apply (rule_tac x="Suc m - x" in bexI)
@@ -3274,17 +3287,17 @@
apply (rule setprod_cong)
apply auto
done
-        have th20: "?m1 n * ?p b n = setprod (%i. b - of_nat i) {0..m}"
+        have th20: "?m1 n * ?p b n = setprod (\<lambda>i. b - of_nat i) {0..m}"
unfolding m1nk
unfolding m h pochhammer_Suc_setprod
unfolding setprod_timesf[symmetric]
apply (rule setprod_cong)
apply auto
done
-        have th21:"pochhammer (b - of_nat n + 1) k = setprod (%i. b - of_nat i) {n - k .. n - 1}"
+        have th21:"pochhammer (b - of_nat n + 1) k = setprod (\<lambda>i. b - of_nat i) {n - k .. n - 1}"
unfolding h m
unfolding pochhammer_Suc_setprod
-          apply (rule strong_setprod_reindex_cong[where f="%k. n - 1 - k"])
+          apply (rule strong_setprod_reindex_cong[where f="\<lambda>k. n - 1 - k"])
using kn
apply (auto simp add: inj_on_def m h image_def)
apply (rule_tac x= "m - x" in bexI)
@@ -3292,7 +3305,7 @@
done

have "?m1 n * ?p b n =
-          pochhammer (b - of_nat n + 1) k * setprod (%i. b - of_nat i) {0.. n - k - 1}"
+          pochhammer (b - of_nat n + 1) k * setprod (\<lambda>i. b - of_nat i) {0.. n - k - 1}"
unfolding th20 th21
unfolding h m
apply (subst setprod_Un_disjoint[symmetric])
@@ -3302,7 +3315,7 @@
apply auto
done
then have th2: "(?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k =
-          setprod (%i. b - of_nat i) {0.. n - k - 1}"
+          setprod (\<lambda>i. b - of_nat i) {0.. n - k - 1}"
using nz' by (simp add: field_simps)
have "(?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k) =
((?m1 k * ?p (of_nat n) k) / ?f n) * ((?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k)"
@@ -3349,8 +3362,8 @@

lemma Vandermonde_pochhammer:
fixes a :: "'a::field_char_0"
-  assumes c: "ALL i : {0..< n}. c \<noteq> - of_nat i"
-  shows "setsum (%k. (pochhammer a k * pochhammer (- (of_nat n)) k) /
+  assumes c: "\<forall>i \<in> {0..< n}. c \<noteq> - of_nat i"
+  shows "setsum (\<lambda>k. (pochhammer a k * pochhammer (- (of_nat n)) k) /
(of_nat (fact k) * pochhammer c k)) {0..n} = pochhammer (c - a) n / pochhammer c n"
proof -
let ?a = "- a"
@@ -3637,8 +3650,8 @@
subsection {* Hypergeometric series *}

definition "F as bs (c::'a::{field_char_0, field_inverse_zero}) =
-  Abs_fps (%n. (foldl (%r a. r* pochhammer a n) 1 as * c^n) /
-    (foldl (%r b. r * pochhammer b n) 1 bs * of_nat (fact n)))"
+  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)))"

lemma F_nth[simp]: "F as bs c \$ n =
(foldl (\<lambda>r a. r* pochhammer a n) 1 as * c^n) /
@@ -3646,11 +3659,13 @@

lemma foldl_mult_start:
-  "foldl (%r x. r * f x) (v::'a::comm_ring_1) as * x = foldl (%r x. r * f x) (v * x) as "
+  fixes v :: "'a::comm_ring_1"
+  shows "foldl (\<lambda>r x. r * f x) v as * x = foldl (\<lambda>r x. r * f x) (v * x) as "
by (induct as arbitrary: x v) (auto simp add: algebra_simps)

lemma foldr_mult_foldl:
-  "foldr (%x r. r * f x) as v = foldl (%r x. r * f x) (v :: 'a::comm_ring_1) as"
+  fixes v :: "'a::comm_ring_1"
+  shows "foldr (\<lambda>x r. r * f x) as v = foldl (\<lambda>r x. r * f x) v as"
by (induct as arbitrary: v) (auto simp add: foldl_mult_start)

lemma F_nth_alt:
@@ -3675,28 +3690,28 @@

lemma F_0[simp]: "F as bs c \$0 = 1"
apply simp
-  apply (subgoal_tac "ALL as. foldl (%(r::'a) (a::'a). r) 1 as = 1")
+  apply (subgoal_tac "\<forall>as. foldl (\<lambda>(r::'a) (a::'a). r) 1 as = 1")
apply auto
apply (induct_tac as)
apply auto
done

lemma foldl_prod_prod:
-  "foldl (%(r::'b::comm_ring_1) (x::'a::comm_ring_1). r * f x) v as * foldl (%r x. r * g x) w as =
-    foldl (%r x. r * f x * g x) (v*w) as"
+  "foldl (\<lambda>(r::'b::comm_ring_1) (x::'a::comm_ring_1). r * f x) v as * foldl (\<lambda>r x. r * g x) w as =
+    foldl (\<lambda>r x. r * f x * g x) (v * w) as"
by (induct as arbitrary: v w) (auto simp add: algebra_simps)

lemma F_rec:
-  "F as bs c \$ Suc n = ((foldl (%r a. r* (a + of_nat n)) c as) /
-    (foldl (%r b. r * (b + of_nat n)) (of_nat (Suc n)) bs )) * F as bs c \$ n"
+  "F as bs c \$ Suc n = ((foldl (\<lambda>r a. r* (a + of_nat n)) c as) /
+    (foldl (\<lambda>r b. r * (b + of_nat n)) (of_nat (Suc n)) bs )) * F as bs c \$ n"
apply (simp del: of_nat_Suc of_nat_add fact_Suc)
apply (simp add: foldl_mult_start del: fact_Suc of_nat_Suc)
unfolding foldl_prod_prod[unfolded foldl_mult_start] pochhammer_Suc
done

-lemma XD_nth[simp]: "XD a \$ n = (if n=0 then 0 else of_nat n * a\$n)"
+lemma XD_nth[simp]: "XD a \$ n = (if n = 0 then 0 else of_nat n * a\$n)"

lemma XD_0th[simp]: "XD a \$ 0 = 0" by simp
@@ -3718,11 +3733,11 @@

lemma F_minus_nat:
"F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0, field_inverse_zero}) \$ k =
-    (if k <= n then
+    (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 =
-    (if k <= m then
+    (if k \<le> m then
pochhammer (- of_nat m) k * c ^ k / (pochhammer (- of_nat (m + n)) k * of_nat (fact k))
else 0)"
@@ -3736,14 +3751,14 @@
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 (%c r. XDp c o r) cs (%c. XDp c a) c0 \$ n =
-  foldr (%c r. (c + of_nat n) * r) cs (c0 + of_nat n) * a\$n"
+lemma XDp_foldr_nth [simp]: "foldr (\<lambda>c r. XDp c o 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: "ALL n c a. f c a \$ n = (of_nat n + k c) * a\$n"
-  shows "foldr (%c r. f c o r) cs (%c. g c a) c0 \$ n =
-    foldr (%c r. (k c + of_nat n) * r) cs (g c0 a \$ n)"
+  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 =
+    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)

lemma dist_less_imp_nth_equal:
@@ -3765,7 +3780,7 @@
shows "dist f g < inverse (2 ^ i)"
proof (cases "f = g")
case False
-  hence "\<exists>n. f \$ n \<noteq> g \$ n" by (simp add: fps_eq_iff)
+  then have "\<exists>n. f \$ n \<noteq> g \$ n" by (simp add: fps_eq_iff)
with assms have "dist f g = inverse (2 ^ (LEAST n. f \$ n \<noteq> g \$ n))"
moreover
@@ -3788,7 +3803,7 @@
have "\<exists>M. \<forall>m \<ge> M. \<forall>j\<le>i. X M \$ j = X m \$ j" by blast
}
then obtain M where M: "\<forall>i. \<forall>m \<ge> M i. \<forall>j \<le> i. X (M i) \$ j = X m \$ j" by metis
-  hence "\<forall>i. \<forall>m \<ge> M i. \<forall>j \<le> i. X (M i) \$ j = X m \$ j" by metis
+  then have "\<forall>i. \<forall>m \<ge> M i. \<forall>j \<le> i. X (M i) \$ j = X m \$ j" by metis
show "convergent X"
proof (rule convergentI)
show "X ----> Abs_fps (\<lambda>i. X (M i) \$ i)"
@@ -3803,7 +3818,7 @@
done
then obtain i where "inverse (2 ^ i) < e" by (auto simp: eventually_sequentially)
have "eventually (\<lambda>x. M i \<le> x) sequentially" by (auto simp: eventually_sequentially)
-      thus "eventually (\<lambda>x. dist (X x) (Abs_fps (\<lambda>i. X (M i) \$ i)) < e) sequentially"
+      then show "eventually (\<lambda>x. dist (X x) (Abs_fps (\<lambda>i. X (M i) \$ i)) < e) sequentially"
proof eventually_elim
fix x
assume "M i \<le> x"```