--- 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 @@
by (simp add: X_power_iff)
-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)
apply (simp add: setsum_delta')
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"
by (simp add: fps_mult_nth)
}
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"
+ by (simp add: natpermute_def)
+ 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
apply (clarsimp simp add: natpermute_def)
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"
by (simp add: natpermute_def)
- have xs: "?xs \<in> natpermute ?m h" using l mn
+ have xs: "?xs \<in> natpermute ?m h" using l assms
by (simp add: natpermute_def)
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}"
+ by (simp add: setprod_constant)
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"
by (simp add: fps_divide_def)
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
{
assume h: "fps_radical r k (a*b) = fps_radical r k a * fps_radical r k b"
- hence "(fps_radical r k (a*b))$0 = (fps_radical r k a * fps_radical r k b)$0"
+ 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 (clarsimp simp add: inj_on_def)
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 (simp add: fps_mult_nth setsum_right_distrib)
apply (subst setsum_commute)
apply (rule setsum_cong2)
@@ -2480,7 +2491,8 @@
apply (rule setsum_cong2)
apply (simp add: setsum_cartesian_product mult_assoc)
apply (rule setsum_mono_zero_right[OF f])
- apply (simp add: subset_eq) apply presburger
+ apply (simp add: subset_eq)
+ apply presburger
apply clarsimp
apply (rule ccontr)
apply (clarsimp simp add: not_le)
@@ -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 (simp add: set_eq_iff)
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 product_composition_lemma[OF c0 c0] power_add[symmetric]
- 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}"
by (simp_all add: setprod_constant Suc)
then show ?thesis
by (simp add: fps_compose_setprod_distrib[OF c0])
@@ -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]
by (simp add: fps_divide_def)
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))"
by (auto simp add: fps_eq_iff)
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"
by (simp add: fps_deriv_L add_commute fps_divide_def divide_inverse)
then show ?thesis unfolding fps_deriv_eq_iff
by (simp add: L_nth fps_inv_def)
@@ -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
apply (simp add: field_simps)
@@ -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 @@
by (simp add: F_def)
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
apply (simp add: algebra_simps of_nat_mult)
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)"
by (simp add: XD_def)
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)"
by (auto simp add: pochhammer_eq_0_iff)
@@ -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))"
by (simp add: split_if_asm dist_fps_def)
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"