# HG changeset patch
# User wenzelm
# Date 1332431059 -3600
# Node ID 737d7bc8e50fe9b17d9cd2ef77049489ecaba306
# Parent  5e70b457b704ee296cbbdf85ccfd111a744dad61
tuned proofs;

diff -r 5e70b457b704 -r 737d7bc8e50f src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Thu Mar 22 15:41:49 2012 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Thu Mar 22 16:44:19 2012 +0100
@@ -14,7 +14,7 @@
 text {*
 
 For more lemmas about the extended real numbers go to
-  @{text "src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"}
+  @{file "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"}
 
 *}
 
@@ -127,7 +127,7 @@
 instantiation ereal :: number
 begin
 definition [simp]: "number_of x = ereal (number_of x)"
-instance proof qed
+instance ..
 end
 
 instantiation ereal :: abs
@@ -184,11 +184,12 @@
 
 instance
 proof
-  fix a :: ereal show "0 + a = a"
+  fix a b c :: ereal
+  show "0 + a = a"
     by (cases a) (simp_all add: zero_ereal_def)
-  fix b :: ereal show "a + b = b + a"
+  show "a + b = b + a"
     by (cases rule: ereal2_cases[of a b]) simp_all
-  fix c :: ereal show "a + b + c = a + (b + c)"
+  show "a + b + c = a + (b + c)"
     by (cases rule: ereal3_cases[of a b c]) simp_all
 qed
 end
@@ -232,7 +233,8 @@
 
 lemma real_of_ereal_add:
   fixes a b :: ereal
-  shows "real (a + b) = (if (\<bar>a\<bar> = \<infinity>) \<and> (\<bar>b\<bar> = \<infinity>) \<or> (\<bar>a\<bar> \<noteq> \<infinity>) \<and> (\<bar>b\<bar> \<noteq> \<infinity>) then real a + real b else 0)"
+  shows "real (a + b) =
+    (if (\<bar>a\<bar> = \<infinity>) \<and> (\<bar>b\<bar> = \<infinity>) \<or> (\<bar>a\<bar> \<noteq> \<infinity>) \<and> (\<bar>b\<bar> \<noteq> \<infinity>) then real a + real b else 0)"
   by (cases rule: ereal2_cases[of a b]) auto
 
 subsubsection "Linear order on @{typ ereal}"
@@ -240,13 +242,14 @@
 instantiation ereal :: linorder
 begin
 
-function less_ereal where
-"   ereal x < ereal y     \<longleftrightarrow> x < y" |
-"(\<infinity>::ereal) < a           \<longleftrightarrow> False" |
-"         a < -(\<infinity>::ereal) \<longleftrightarrow> False" |
-"ereal x    < \<infinity>           \<longleftrightarrow> True" |
-"        -\<infinity> < ereal r     \<longleftrightarrow> True" |
-"        -\<infinity> < (\<infinity>::ereal) \<longleftrightarrow> True"
+function less_ereal
+where
+  "   ereal x < ereal y     \<longleftrightarrow> x < y"
+| "(\<infinity>::ereal) < a           \<longleftrightarrow> False"
+| "         a < -(\<infinity>::ereal) \<longleftrightarrow> False"
+| "ereal x    < \<infinity>           \<longleftrightarrow> True"
+| "        -\<infinity> < ereal r     \<longleftrightarrow> True"
+| "        -\<infinity> < (\<infinity>::ereal) \<longleftrightarrow> True"
 proof -
   case (goal1 P x)
   moreover then obtain a b where "x = (a,b)" by (cases x) auto
@@ -290,17 +293,19 @@
 
 instance
 proof
-  fix x :: ereal show "x \<le> x"
+  fix x y z :: ereal
+  show "x \<le> x"
     by (cases x) simp_all
-  fix y :: ereal show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
+  show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
     by (cases rule: ereal2_cases[of x y]) auto
   show "x \<le> y \<or> y \<le> x "
     by (cases rule: ereal2_cases[of x y]) auto
   { assume "x \<le> y" "y \<le> x" then show "x = y"
     by (cases rule: ereal2_cases[of x y]) auto }
-  { fix z assume "x \<le> y" "y \<le> z" then show "x \<le> z"
+  { assume "x \<le> y" "y \<le> z" then show "x \<le> z"
     by (cases rule: ereal3_cases[of x y z]) auto }
 qed
+
 end
 
 instance ereal :: ordered_ab_semigroup_add
@@ -430,16 +435,20 @@
   fixes x :: ereal assumes "\<And>B. x \<le> ereal B" shows "x = - \<infinity>"
 proof (cases x)
   case (real r) with assms[of "r - 1"] show ?thesis by auto
-next case PInf with assms[of 0] show ?thesis by auto
-next case MInf then show ?thesis by simp
+next
+  case PInf with assms[of 0] show ?thesis by auto
+next
+  case MInf then show ?thesis by simp
 qed
 
 lemma ereal_top:
   fixes x :: ereal assumes "\<And>B. x \<ge> ereal B" shows "x = \<infinity>"
 proof (cases x)
   case (real r) with assms[of "r + 1"] show ?thesis by auto
-next case MInf with assms[of 0] show ?thesis by auto
-next case PInf then show ?thesis by simp
+next
+  case MInf with assms[of 0] show ?thesis by auto
+next
+  case PInf then show ?thesis by simp
 qed
 
 lemma
@@ -516,11 +525,11 @@
 
 instance
 proof
-  fix a :: ereal show "1 * a = a"
+  fix a b c :: ereal show "1 * a = a"
     by (cases a) (simp_all add: one_ereal_def)
-  fix b :: ereal show "a * b = b * a"
+  show "a * b = b * a"
     by (cases rule: ereal2_cases[of a b]) simp_all
-  fix c :: ereal show "a * b * c = a * (b * c)"
+  show "a * b * c = a * (b * c)"
     by (cases rule: ereal3_cases[of a b c])
        (simp_all add: zero_ereal_def zero_less_mult_iff)
 qed
@@ -668,11 +677,11 @@
   shows "x <= y"
 proof-
 { assume a: "EX r. y = ereal r"
-  from this obtain r where r_def: "y = ereal r" by auto
+  then obtain r where r_def: "y = ereal r" by auto
   { assume "x=(-\<infinity>)" hence ?thesis by auto }
   moreover
   { assume "~(x=(-\<infinity>))"
-    from this obtain p where p_def: "x = ereal p"
+    then obtain p where p_def: "x = ereal p"
     using a assms[rule_format, of 1] by (cases x) auto
     { fix e have "0 < e --> p <= r + e"
       using assms[rule_format, of "ereal e"] p_def r_def by auto }
@@ -696,10 +705,10 @@
   { assume "e=\<infinity>" hence "x<=y+e" by auto }
   moreover
   { assume "e~=\<infinity>"
-    from this obtain r where "e = ereal r" using `e>0` apply (cases e) by auto
+    then obtain r where "e = ereal r" using `e>0` apply (cases e) by auto
     hence "x<=y+e" using assms[rule_format, of r] `e>0` by auto
   } ultimately have "x<=y+e" by blast
-} from this show ?thesis using ereal_le_epsilon by auto
+} then show ?thesis using ereal_le_epsilon by auto
 qed
 
 lemma ereal_le_real:
@@ -790,11 +799,14 @@
 
 lemma ereal_uminus_lessThan[simp]:
   fixes a :: ereal shows "uminus ` {..<a} = {-a<..}"
-proof (safe intro!: image_eqI)
-  fix x assume "-a < x"
-  then have "- x < - (- a)" by (simp del: ereal_uminus_uminus)
-  then show "- x < a" by simp
-qed auto
+proof -
+  {
+    fix x assume "-a < x"
+    then have "- x < - (- a)" by (simp del: ereal_uminus_uminus)
+    then have "- x < a" by simp
+  }
+  then show ?thesis by (auto intro!: image_eqI)
+qed
 
 lemma ereal_uminus_greaterThan[simp]:
   "uminus ` {(a::ereal)<..} = {..<-a}"
@@ -923,7 +935,8 @@
   assumes "\<bar>x\<bar> \<noteq> \<infinity>" "0 < e"
   shows "x - e < x" "x < x + e"
 using assms apply (cases x, cases e) apply auto
-using assms by (cases x, cases e) auto
+using assms apply (cases x, cases e) apply auto
+done
 
 subsubsection {* Division *}
 
@@ -939,7 +952,7 @@
 
 definition "x / y = x * inverse (y :: ereal)"
 
-instance proof qed
+instance ..
 end
 
 lemma real_of_ereal_inverse[simp]:
@@ -1092,7 +1105,7 @@
 begin
 definition [simp]: "sup x y = (max x y :: ereal)"
 definition [simp]: "inf x y = (min x y :: ereal)"
-instance proof qed simp_all
+instance by default simp_all
 end
 
 instantiation ereal :: complete_lattice
@@ -1161,7 +1174,7 @@
 proof-
 def S1 == "uminus ` S"
 hence "S1 ~= {}" using assms by auto
-from this obtain x where x_def: "(ALL y:S1. y <= x) & (ALL z. (ALL y:S1. y <= z) --> x <= z)"
+then obtain x where x_def: "(ALL y:S1. y <= x) & (ALL z. (ALL y:S1. y <= z) --> x <= z)"
    using ereal_complete_Sup[of S1] by auto
 { fix z assume "ALL y:S. z <= y"
   hence "ALL y:S1. y <= -z" unfolding S1_def by auto
@@ -1372,8 +1385,8 @@
 proof-
 { assume "?rhs"
   { assume "~(x <= (SUP i:A. f i))" hence "(SUP i:A. f i)<x" by (simp add: not_le)
-    from this obtain y where y_def: "(SUP i:A. f i)<y & y<x" using ereal_dense by auto
-    from this obtain i where "i : A & y <= f i" using `?rhs` by auto
+    then obtain y where y_def: "(SUP i:A. f i)<y & y<x" using ereal_dense by auto
+    then obtain i where "i : A & y <= f i" using `?rhs` by auto
     hence "y <= (SUP i:A. f i)" using SUP_upper[of i A f] by auto
     hence False using y_def by auto
   } hence "?lhs" by auto
@@ -1391,8 +1404,8 @@
 proof-
 { assume "?rhs"
   { assume "~((INF i:A. f i) <= x)" hence "x < (INF i:A. f i)" by (simp add: not_le)
-    from this obtain y where y_def: "x<y & y<(INF i:A. f i)" using ereal_dense by auto
-    from this obtain i where "i : A & f i <= y" using `?rhs` by auto
+    then obtain y where y_def: "x<y & y<(INF i:A. f i)" using ereal_dense by auto
+    then obtain i where "i : A & f i <= y" using `?rhs` by auto
     hence "(INF i:A. f i) <= y" using INF_lower[of i A f] by auto
     hence False using y_def by auto
   } hence "?lhs" by auto
@@ -2023,7 +2036,7 @@
   shows "Y ----> L"
 proof-
 { fix S assume "open S" and "L:S"
-  from this obtain N1 where "ALL n>=N1. X n : S"
+  then obtain N1 where "ALL n>=N1. X n : S"
      using assms unfolding tendsto_def eventually_sequentially by auto
   hence "ALL n>=max N N1. Y n : S" using assms by auto
   hence "EX N. ALL n>=N. Y n : S" apply(rule_tac x="max N N1" in exI) by auto
@@ -2058,14 +2071,14 @@
     hence ?thesis by auto }
   moreover
   { assume "EX B. C = ereal B"
-    from this obtain B where B_def: "C=ereal B" by auto
+    then obtain B where B_def: "C=ereal B" by auto
     hence "~(l=\<infinity>)" using Lim_bounded_PInfty2 assms by auto
-    from this obtain m where m_def: "ereal m=l" using `~(l=(-\<infinity>))` by (cases l) auto
-    from this obtain N where N_def: "ALL n>=N. f n : {ereal(m - 1) <..< ereal(m+1)}"
+    then obtain m where m_def: "ereal m=l" using `~(l=(-\<infinity>))` by (cases l) auto
+    then obtain N where N_def: "ALL n>=N. f n : {ereal(m - 1) <..< ereal(m+1)}"
        apply (subst tendsto_obtains_N[of f l "{ereal(m - 1) <..< ereal(m+1)}"]) using assms by auto
     { fix n assume "n>=N"
       hence "EX r. ereal r = f n" using N_def by (cases "f n") auto
-    } from this obtain g where g_def: "ALL n>=N. ereal (g n) = f n" by metis
+    } then obtain g where g_def: "ALL n>=N. ereal (g n) = f n" by metis
     hence "(%n. ereal (g n)) ----> l" using tail_same_limit[of f l N] assms by auto
     hence *: "(%n. g n) ----> m" using m_def by auto
     { fix n assume "n>=max N M"
@@ -2175,7 +2188,7 @@
     fix N assume "n <= N"
     from upper[OF this] lower[OF this] assms `0 < r`
     have "u N ~: {\<infinity>,(-\<infinity>)}" by auto
-    from this obtain ra where ra_def: "(u N) = ereal ra" by (cases "u N") auto
+    then obtain ra where ra_def: "(u N) = ereal ra" by (cases "u N") auto
     hence "rx < ra + r" and "ra < rx + r"
        using rx_def assms `0 < r` lower[OF `n <= N`] upper[OF `n <= N`] by auto
     hence "dist (real (u N)) rx < r"
@@ -2194,7 +2207,7 @@
 proof
   assume lim: "u ----> x"
   { fix r assume "(r::ereal)>0"
-    from this obtain N where N_def: "ALL n>=N. u n : {x - r <..< x + r}"
+    then obtain N where N_def: "ALL n>=N. u n : {x - r <..< x + r}"
        apply (subst tendsto_obtains_N[of u x "{x - r <..< x + r}"])
        using lim ereal_between[of x r] assms `r>0` by auto
     hence "EX N. ALL n>=N. u n < x + r & x < u n + r"
@@ -2537,8 +2550,8 @@
 
 lemma real_ereal_id: "real o ereal = id"
 proof-
-{ fix x have "(real o ereal) x = id x" by auto }
-from this show ?thesis using ext by blast
+  { fix x have "(real o ereal) x = id x" by auto }
+  then show ?thesis using ext by blast
 qed
 
 lemma open_image_ereal: "open(UNIV-{ \<infinity> , (-\<infinity> :: ereal)})"