# HG changeset patch
# User huffman
# Date 1182361754 -7200
# Node ID ee218296d6351a3b408fb0d9a3248d92962568f5
# Parent  37860871f241a0d8848964b48b89d0c64bc08e0a
avoid using implicit prems in assumption

diff -r 37860871f241 -r ee218296d635 src/HOL/Hyperreal/Deriv.thy
--- 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)
   }
diff -r 37860871f241 -r ee218296d635 src/HOL/Hyperreal/Filter.thy
--- 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:
diff -r 37860871f241 -r ee218296d635 src/HOL/Hyperreal/Lim.thy
--- 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
diff -r 37860871f241 -r ee218296d635 src/HOL/Hyperreal/Ln.thy
--- 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
diff -r 37860871f241 -r ee218296d635 src/HOL/Hyperreal/NthRoot.thy
--- 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:
diff -r 37860871f241 -r ee218296d635 src/HOL/Hyperreal/Series.thy
--- 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
diff -r 37860871f241 -r ee218296d635 src/HOL/Hyperreal/Transcendental.thy
--- 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)