--- a/src/HOL/Hyperreal/Deriv.thy Wed Jun 20 17:34:44 2007 +0200
+++ b/src/HOL/Hyperreal/Deriv.thy Wed Jun 20 19:49:14 2007 +0200
@@ -511,7 +511,7 @@
and le: "a \<le> b"
shows "~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))"
proof (induct n)
- case 0 thus ?case by simp
+ case 0 show ?case using notP by simp
next
case (Suc n)
thus ?case
@@ -755,7 +755,7 @@
by auto
thus ?thesis
proof (intro exI conjI strip)
- show "0<s" .
+ show "0<s" using s .
fix h::real
assume "0 < h" "h < s"
with all [of h] show "f x < f (x+h)"
@@ -785,7 +785,7 @@
by auto
thus ?thesis
proof (intro exI conjI strip)
- show "0<s" .
+ show "0<s" using s .
fix h::real
assume "0 < h" "h < s"
with all [of "-h"] show "f x < f (x-h)"
@@ -807,7 +807,7 @@
and le: "\<forall>y. \<bar>x-y\<bar> < d --> f(y) \<le> f(x)"
shows "l = 0"
proof (cases rule: linorder_cases [of l 0])
- case equal show ?thesis .
+ case equal thus ?thesis .
next
case less
from DERIV_left_dec [OF der less]
@@ -995,8 +995,8 @@
by (rule DERIV_add [OF der])
show ?thesis
proof (intro exI conjI)
- show "a < z" .
- show "z < b" .
+ show "a < z" using az .
+ show "z < b" using zb .
show "f b - f a = (b - a) * ((f b - f a)/(b-a))" by (simp)
show "DERIV f z :> ((f b - f a)/(b-a))" using derF by simp
qed
@@ -1186,7 +1186,7 @@
obtain e where e: "0 < e" "e < f x - L" "e < M - f x" by auto
thus ?thesis
proof (intro exI conjI)
- show "0<e" .
+ show "0<e" using e(1) .
show "\<forall>y. \<bar>y - f x\<bar> \<le> e \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y)"
proof (intro strip)
fix y::real
@@ -1226,7 +1226,7 @@
by blast
show "\<exists>s>0. \<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r"
proof (intro exI conjI)
- show "0<e'" .
+ show "0<e'" using e' .
show "\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < e' \<longrightarrow> \<bar>g (f x + z) - g (f x)\<bar> < r"
proof (intro strip)
fix z::real
@@ -1337,16 +1337,16 @@
from cdef have "DERIV ?h c :> l" by auto
moreover
{
- from g'cdef have "DERIV (\<lambda>x. (f b - f a) * g x) c :> g'c * (f b - f a)"
+ have "DERIV (\<lambda>x. (f b - f a) * g x) c :> g'c * (f b - f a)"
apply (insert DERIV_const [where k="f b - f a"])
apply (drule meta_spec [of _ c])
- apply (drule DERIV_mult [where f="(\<lambda>x. f b - f a)" and g=g])
- by simp_all
- moreover from f'cdef have "DERIV (\<lambda>x. (g b - g a) * f x) c :> f'c * (g b - g a)"
+ apply (drule DERIV_mult [OF _ g'cdef])
+ by simp
+ moreover have "DERIV (\<lambda>x. (g b - g a) * f x) c :> f'c * (g b - g a)"
apply (insert DERIV_const [where k="g b - g a"])
apply (drule meta_spec [of _ c])
- apply (drule DERIV_mult [where f="(\<lambda>x. g b - g a)" and g=f])
- by simp_all
+ apply (drule DERIV_mult [OF _ f'cdef])
+ by simp
ultimately have "DERIV ?h c :> g'c * (f b - f a) - f'c * (g b - g a)"
by (simp add: DERIV_diff)
}
--- a/src/HOL/Hyperreal/Filter.thy Wed Jun 20 17:34:44 2007 +0200
+++ b/src/HOL/Hyperreal/Filter.thy Wed Jun 20 19:49:14 2007 +0200
@@ -183,7 +183,7 @@
lemma (in ultrafilter) max_filter:
assumes G: "filter G" and sub: "F \<subseteq> G" shows "F = G"
proof
- show "F \<subseteq> G" .
+ show "F \<subseteq> G" using sub .
show "G \<subseteq> F"
proof
fix A assume A: "A \<in> G"
@@ -225,7 +225,7 @@
proof (rule filter.intro)
show "UNIV \<in> ?F" by simp
next
- show "{} \<notin> ?F" by simp
+ show "{} \<notin> ?F" using inf by simp
next
fix u v assume "u \<in> ?F" and "v \<in> ?F"
thus "u \<inter> v \<in> ?F" by simp
@@ -313,18 +313,18 @@
qed
lemma (in UFT) Union_chain_filter:
-assumes "c \<in> chain superfrechet" and "c \<noteq> {}"
+assumes chain: "c \<in> chain superfrechet" and nonempty: "c \<noteq> {}"
shows "filter (\<Union>c)"
proof (rule filter.intro)
- show "UNIV \<in> \<Union>c" by (rule Union_chain_UNIV)
+ show "UNIV \<in> \<Union>c" using chain nonempty by (rule Union_chain_UNIV)
next
- show "{} \<notin> \<Union>c" by (rule Union_chain_empty)
+ show "{} \<notin> \<Union>c" using chain by (rule Union_chain_empty)
next
fix u v assume "u \<in> \<Union>c" and "v \<in> \<Union>c"
- show "u \<inter> v \<in> \<Union>c" by (rule Union_chain_Int)
+ with chain show "u \<inter> v \<in> \<Union>c" by (rule Union_chain_Int)
next
fix u v assume "u \<in> \<Union>c" and "u \<subseteq> v"
- show "v \<in> \<Union>c" by (rule Union_chain_subset)
+ with chain show "v \<in> \<Union>c" by (rule Union_chain_subset)
qed
lemma (in UFT) lemma_mem_chain_frechet_subset:
--- a/src/HOL/Hyperreal/Lim.thy Wed Jun 20 17:34:44 2007 +0200
+++ b/src/HOL/Hyperreal/Lim.thy Wed Jun 20 19:49:14 2007 +0200
@@ -619,7 +619,7 @@
fix e::real
assume "0 < e"
(* choose no such that inverse (real (Suc n)) < e *)
- have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean)
+ then have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean)
then obtain m where nodef: "inverse (real (Suc m)) < e" by auto
show "\<exists>no. \<forall>n. no \<le> n --> \<bar>?F n - a\<bar> < e"
proof (intro exI allI impI)
@@ -628,7 +628,7 @@
have "\<bar>?F n - a\<bar> < inverse (real (Suc n))"
by (rule F2)
also have "inverse (real (Suc n)) \<le> inverse (real (Suc m))"
- by auto
+ using mlen by auto
also from nodef have
"inverse (real (Suc m)) < e" .
finally show "\<bar>?F n - a\<bar> < e" .
@@ -664,10 +664,10 @@
(X -- a --> L)"
proof
assume "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
- show "X -- a --> L" by (rule LIMSEQ_SEQ_conv2)
+ thus "X -- a --> L" by (rule LIMSEQ_SEQ_conv2)
next
assume "(X -- a --> L)"
- show "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" by (rule LIMSEQ_SEQ_conv1)
+ thus "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" by (rule LIMSEQ_SEQ_conv1)
qed
end
--- a/src/HOL/Hyperreal/Ln.thy Wed Jun 20 17:34:44 2007 +0200
+++ b/src/HOL/Hyperreal/Ln.thy Wed Jun 20 19:49:14 2007 +0200
@@ -92,7 +92,7 @@
apply (subst inverse_nonnegative_iff_nonnegative)
apply (rule real_of_nat_fact_ge_zero)
apply (rule zero_le_power)
- apply assumption
+ apply (rule a)
done
also have "... = 1 / 2 * (inverse (real (fact (n + 2))) * x ^ (n + 2))"
by simp
@@ -321,9 +321,9 @@
lemma abs_ln_one_plus_x_minus_x_bound_nonneg:
"0 <= x ==> x <= 1 ==> abs(ln (1 + x) - x) <= x^2"
proof -
- assume "0 <= x"
+ assume x: "0 <= x"
assume "x <= 1"
- have "ln (1 + x) <= x"
+ from x have "ln (1 + x) <= x"
by (rule ln_add_one_self_le_self)
then have "ln (1 + x) - x <= 0"
by simp
--- a/src/HOL/Hyperreal/NthRoot.thy Wed Jun 20 17:34:44 2007 +0200
+++ b/src/HOL/Hyperreal/NthRoot.thy Wed Jun 20 19:49:14 2007 +0200
@@ -355,7 +355,7 @@
show "real n * root n x ^ (n - Suc 0) \<noteq> 0"
using n x by simp
show "isCont (root n) x"
- by (rule isCont_real_root)
+ using n by (rule isCont_real_root)
qed
lemma DERIV_odd_real_root:
--- a/src/HOL/Hyperreal/Series.thy Wed Jun 20 17:34:44 2007 +0200
+++ b/src/HOL/Hyperreal/Series.thy Wed Jun 20 19:49:14 2007 +0200
@@ -648,6 +648,7 @@
assumes a: "summable (\<lambda>k. norm (a k))"
assumes b: "summable (\<lambda>k. norm (b k))"
shows "(\<Sum>k. a k) * (\<Sum>k. b k) = (\<Sum>k. \<Sum>i=0..k. a i * b (k - i))"
+using a b
by (rule Cauchy_product_sums [THEN sums_unique])
end
--- a/src/HOL/Hyperreal/Transcendental.thy Wed Jun 20 17:34:44 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy Wed Jun 20 19:49:14 2007 +0200
@@ -823,7 +823,7 @@
fixes x y :: real
assumes xy: "x < y" shows "exp x < exp y"
proof -
- have "1 < exp (y + - x)"
+ from xy have "1 < exp (y + - x)"
by (rule real_less_sum_gt_zero [THEN exp_gt_one])
hence "exp x * inverse (exp x) < exp y * inverse (exp x)"
by (auto simp add: exp_add exp_minus)