avoid using implicit prems in assumption
authorhuffman
Wed Jun 20 19:49:14 2007 +0200 (2007-06-20)
changeset 23441ee218296d635
parent 23440 37860871f241
child 23442 028e39e5e8f3
avoid using implicit prems in assumption
src/HOL/Hyperreal/Deriv.thy
src/HOL/Hyperreal/Filter.thy
src/HOL/Hyperreal/Lim.thy
src/HOL/Hyperreal/Ln.thy
src/HOL/Hyperreal/NthRoot.thy
src/HOL/Hyperreal/Series.thy
src/HOL/Hyperreal/Transcendental.thy
     1.1 --- a/src/HOL/Hyperreal/Deriv.thy	Wed Jun 20 17:34:44 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/Deriv.thy	Wed Jun 20 19:49:14 2007 +0200
     1.3 @@ -511,7 +511,7 @@
     1.4        and le:   "a \<le> b"
     1.5    shows "~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))"
     1.6  proof (induct n)
     1.7 -  case 0 thus ?case by simp
     1.8 +  case 0 show ?case using notP by simp
     1.9   next
    1.10    case (Suc n)
    1.11    thus ?case
    1.12 @@ -755,7 +755,7 @@
    1.13      by auto
    1.14    thus ?thesis
    1.15    proof (intro exI conjI strip)
    1.16 -    show "0<s" .
    1.17 +    show "0<s" using s .
    1.18      fix h::real
    1.19      assume "0 < h" "h < s"
    1.20      with all [of h] show "f x < f (x+h)"
    1.21 @@ -785,7 +785,7 @@
    1.22      by auto
    1.23    thus ?thesis
    1.24    proof (intro exI conjI strip)
    1.25 -    show "0<s" .
    1.26 +    show "0<s" using s .
    1.27      fix h::real
    1.28      assume "0 < h" "h < s"
    1.29      with all [of "-h"] show "f x < f (x-h)"
    1.30 @@ -807,7 +807,7 @@
    1.31        and le:  "\<forall>y. \<bar>x-y\<bar> < d --> f(y) \<le> f(x)"
    1.32    shows "l = 0"
    1.33  proof (cases rule: linorder_cases [of l 0])
    1.34 -  case equal show ?thesis .
    1.35 +  case equal thus ?thesis .
    1.36  next
    1.37    case less
    1.38    from DERIV_left_dec [OF der less]
    1.39 @@ -995,8 +995,8 @@
    1.40      by (rule DERIV_add [OF der])
    1.41    show ?thesis
    1.42    proof (intro exI conjI)
    1.43 -    show "a < z" .
    1.44 -    show "z < b" .
    1.45 +    show "a < z" using az .
    1.46 +    show "z < b" using zb .
    1.47      show "f b - f a = (b - a) * ((f b - f a)/(b-a))" by (simp)
    1.48      show "DERIV f z :> ((f b - f a)/(b-a))"  using derF by simp
    1.49    qed
    1.50 @@ -1186,7 +1186,7 @@
    1.51    obtain e where e: "0 < e" "e < f x - L" "e < M - f x" by auto
    1.52    thus ?thesis
    1.53    proof (intro exI conjI)
    1.54 -    show "0<e" .
    1.55 +    show "0<e" using e(1) .
    1.56      show "\<forall>y. \<bar>y - f x\<bar> \<le> e \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y)"
    1.57      proof (intro strip)
    1.58        fix y::real
    1.59 @@ -1226,7 +1226,7 @@
    1.60            by blast
    1.61      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"
    1.62      proof (intro exI conjI)
    1.63 -      show "0<e'" .
    1.64 +      show "0<e'" using e' .
    1.65        show "\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < e' \<longrightarrow> \<bar>g (f x + z) - g (f x)\<bar> < r"
    1.66        proof (intro strip)
    1.67          fix z::real
    1.68 @@ -1337,16 +1337,16 @@
    1.69    from cdef have "DERIV ?h c :> l" by auto
    1.70    moreover
    1.71    {
    1.72 -    from g'cdef have "DERIV (\<lambda>x. (f b - f a) * g x) c :> g'c * (f b - f a)"
    1.73 +    have "DERIV (\<lambda>x. (f b - f a) * g x) c :> g'c * (f b - f a)"
    1.74        apply (insert DERIV_const [where k="f b - f a"])
    1.75        apply (drule meta_spec [of _ c])
    1.76 -      apply (drule DERIV_mult [where f="(\<lambda>x. f b - f a)" and g=g])
    1.77 -      by simp_all
    1.78 -    moreover from f'cdef have "DERIV (\<lambda>x. (g b - g a) * f x) c :> f'c * (g b - g a)"
    1.79 +      apply (drule DERIV_mult [OF _ g'cdef])
    1.80 +      by simp
    1.81 +    moreover have "DERIV (\<lambda>x. (g b - g a) * f x) c :> f'c * (g b - g a)"
    1.82        apply (insert DERIV_const [where k="g b - g a"])
    1.83        apply (drule meta_spec [of _ c])
    1.84 -      apply (drule DERIV_mult [where f="(\<lambda>x. g b - g a)" and g=f])
    1.85 -      by simp_all
    1.86 +      apply (drule DERIV_mult [OF _ f'cdef])
    1.87 +      by simp
    1.88      ultimately have "DERIV ?h c :>  g'c * (f b - f a) - f'c * (g b - g a)"
    1.89        by (simp add: DERIV_diff)
    1.90    }
     2.1 --- a/src/HOL/Hyperreal/Filter.thy	Wed Jun 20 17:34:44 2007 +0200
     2.2 +++ b/src/HOL/Hyperreal/Filter.thy	Wed Jun 20 19:49:14 2007 +0200
     2.3 @@ -183,7 +183,7 @@
     2.4  lemma (in ultrafilter) max_filter:
     2.5  assumes G: "filter G" and sub: "F \<subseteq> G" shows "F = G"
     2.6  proof
     2.7 -  show "F \<subseteq> G" .
     2.8 +  show "F \<subseteq> G" using sub .
     2.9    show "G \<subseteq> F"
    2.10    proof
    2.11      fix A assume A: "A \<in> G"
    2.12 @@ -225,7 +225,7 @@
    2.13  proof (rule filter.intro)
    2.14    show "UNIV \<in> ?F" by simp
    2.15  next
    2.16 -  show "{} \<notin> ?F" by simp
    2.17 +  show "{} \<notin> ?F" using inf by simp
    2.18  next
    2.19    fix u v assume "u \<in> ?F" and "v \<in> ?F"
    2.20    thus "u \<inter> v \<in> ?F" by simp
    2.21 @@ -313,18 +313,18 @@
    2.22  qed
    2.23  
    2.24  lemma (in UFT) Union_chain_filter:
    2.25 -assumes "c \<in> chain superfrechet" and "c \<noteq> {}"
    2.26 +assumes chain: "c \<in> chain superfrechet" and nonempty: "c \<noteq> {}"
    2.27  shows "filter (\<Union>c)"
    2.28  proof (rule filter.intro)
    2.29 -  show "UNIV \<in> \<Union>c" by (rule Union_chain_UNIV)
    2.30 +  show "UNIV \<in> \<Union>c" using chain nonempty by (rule Union_chain_UNIV)
    2.31  next
    2.32 -  show "{} \<notin> \<Union>c" by (rule Union_chain_empty)
    2.33 +  show "{} \<notin> \<Union>c" using chain by (rule Union_chain_empty)
    2.34  next
    2.35    fix u v assume "u \<in> \<Union>c" and "v \<in> \<Union>c"
    2.36 -  show "u \<inter> v \<in> \<Union>c" by (rule Union_chain_Int)
    2.37 +  with chain show "u \<inter> v \<in> \<Union>c" by (rule Union_chain_Int)
    2.38  next
    2.39    fix u v assume "u \<in> \<Union>c" and "u \<subseteq> v"
    2.40 -  show "v \<in> \<Union>c" by (rule Union_chain_subset)
    2.41 +  with chain show "v \<in> \<Union>c" by (rule Union_chain_subset)
    2.42  qed
    2.43  
    2.44  lemma (in UFT) lemma_mem_chain_frechet_subset:
     3.1 --- a/src/HOL/Hyperreal/Lim.thy	Wed Jun 20 17:34:44 2007 +0200
     3.2 +++ b/src/HOL/Hyperreal/Lim.thy	Wed Jun 20 19:49:14 2007 +0200
     3.3 @@ -619,7 +619,7 @@
     3.4        fix e::real
     3.5        assume "0 < e"
     3.6          (* choose no such that inverse (real (Suc n)) < e *)
     3.7 -      have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean)
     3.8 +      then have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean)
     3.9        then obtain m where nodef: "inverse (real (Suc m)) < e" by auto
    3.10        show "\<exists>no. \<forall>n. no \<le> n --> \<bar>?F n - a\<bar> < e"
    3.11        proof (intro exI allI impI)
    3.12 @@ -628,7 +628,7 @@
    3.13          have "\<bar>?F n - a\<bar> < inverse (real (Suc n))"
    3.14            by (rule F2)
    3.15          also have "inverse (real (Suc n)) \<le> inverse (real (Suc m))"
    3.16 -          by auto
    3.17 +          using mlen by auto
    3.18          also from nodef have
    3.19            "inverse (real (Suc m)) < e" .
    3.20          finally show "\<bar>?F n - a\<bar> < e" .
    3.21 @@ -664,10 +664,10 @@
    3.22     (X -- a --> L)"
    3.23  proof
    3.24    assume "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
    3.25 -  show "X -- a --> L" by (rule LIMSEQ_SEQ_conv2)
    3.26 +  thus "X -- a --> L" by (rule LIMSEQ_SEQ_conv2)
    3.27  next
    3.28    assume "(X -- a --> L)"
    3.29 -  show "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" by (rule LIMSEQ_SEQ_conv1)
    3.30 +  thus "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" by (rule LIMSEQ_SEQ_conv1)
    3.31  qed
    3.32  
    3.33  end
     4.1 --- a/src/HOL/Hyperreal/Ln.thy	Wed Jun 20 17:34:44 2007 +0200
     4.2 +++ b/src/HOL/Hyperreal/Ln.thy	Wed Jun 20 19:49:14 2007 +0200
     4.3 @@ -92,7 +92,7 @@
     4.4        apply (subst inverse_nonnegative_iff_nonnegative)
     4.5        apply (rule real_of_nat_fact_ge_zero)
     4.6        apply (rule zero_le_power)
     4.7 -      apply assumption
     4.8 +      apply (rule a)
     4.9        done
    4.10      also have "... = 1 / 2 * (inverse (real (fact (n + 2))) * x ^ (n + 2))"
    4.11        by simp
    4.12 @@ -321,9 +321,9 @@
    4.13  lemma abs_ln_one_plus_x_minus_x_bound_nonneg:
    4.14      "0 <= x ==> x <= 1 ==> abs(ln (1 + x) - x) <= x^2"
    4.15  proof -
    4.16 -  assume "0 <= x"
    4.17 +  assume x: "0 <= x"
    4.18    assume "x <= 1"
    4.19 -  have "ln (1 + x) <= x"
    4.20 +  from x have "ln (1 + x) <= x"
    4.21      by (rule ln_add_one_self_le_self)
    4.22    then have "ln (1 + x) - x <= 0" 
    4.23      by simp
     5.1 --- a/src/HOL/Hyperreal/NthRoot.thy	Wed Jun 20 17:34:44 2007 +0200
     5.2 +++ b/src/HOL/Hyperreal/NthRoot.thy	Wed Jun 20 19:49:14 2007 +0200
     5.3 @@ -355,7 +355,7 @@
     5.4    show "real n * root n x ^ (n - Suc 0) \<noteq> 0"
     5.5      using n x by simp
     5.6    show "isCont (root n) x"
     5.7 -    by (rule isCont_real_root)
     5.8 +    using n by (rule isCont_real_root)
     5.9  qed
    5.10  
    5.11  lemma DERIV_odd_real_root:
     6.1 --- a/src/HOL/Hyperreal/Series.thy	Wed Jun 20 17:34:44 2007 +0200
     6.2 +++ b/src/HOL/Hyperreal/Series.thy	Wed Jun 20 19:49:14 2007 +0200
     6.3 @@ -648,6 +648,7 @@
     6.4    assumes a: "summable (\<lambda>k. norm (a k))"
     6.5    assumes b: "summable (\<lambda>k. norm (b k))"
     6.6    shows "(\<Sum>k. a k) * (\<Sum>k. b k) = (\<Sum>k. \<Sum>i=0..k. a i * b (k - i))"
     6.7 +using a b
     6.8  by (rule Cauchy_product_sums [THEN sums_unique])
     6.9  
    6.10  end
     7.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Wed Jun 20 17:34:44 2007 +0200
     7.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Wed Jun 20 19:49:14 2007 +0200
     7.3 @@ -823,7 +823,7 @@
     7.4    fixes x y :: real
     7.5    assumes xy: "x < y" shows "exp x < exp y"
     7.6  proof -
     7.7 -  have "1 < exp (y + - x)"
     7.8 +  from xy have "1 < exp (y + - x)"
     7.9      by (rule real_less_sum_gt_zero [THEN exp_gt_one])
    7.10    hence "exp x * inverse (exp x) < exp y * inverse (exp x)"
    7.11      by (auto simp add: exp_add exp_minus)