src/HOL/Probability/Positive_Extended_Real.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 41096 843c40bbc379
child 41544 c3b977fee8a3
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
     1 (* Author: Johannes Hoelzl, TU Muenchen *)
     2 
     3 header {* A type for positive real numbers with infinity *}
     4 
     5 theory Positive_Extended_Real
     6   imports Complex_Main "~~/src/HOL/Library/Nat_Bijection" Multivariate_Analysis
     7 begin
     8 
     9 lemma (in complete_lattice) Sup_start:
    10   assumes *: "\<And>x. f x \<le> f 0"
    11   shows "(SUP n. f n) = f 0"
    12 proof (rule antisym)
    13   show "f 0 \<le> (SUP n. f n)" by (rule le_SUPI) auto
    14   show "(SUP n. f n) \<le> f 0" by (rule SUP_leI[OF *])
    15 qed
    16 
    17 lemma (in complete_lattice) Inf_start:
    18   assumes *: "\<And>x. f 0 \<le> f x"
    19   shows "(INF n. f n) = f 0"
    20 proof (rule antisym)
    21   show "(INF n. f n) \<le> f 0" by (rule INF_leI) simp
    22   show "f 0 \<le> (INF n. f n)" by (rule le_INFI[OF *])
    23 qed
    24 
    25 lemma (in complete_lattice) Sup_mono_offset:
    26   fixes f :: "'b :: {ordered_ab_semigroup_add,monoid_add} \<Rightarrow> 'a"
    27   assumes *: "\<And>x y. x \<le> y \<Longrightarrow> f x \<le> f y" and "0 \<le> k"
    28   shows "(SUP n . f (k + n)) = (SUP n. f n)"
    29 proof (rule antisym)
    30   show "(SUP n. f (k + n)) \<le> (SUP n. f n)"
    31     by (auto intro!: Sup_mono simp: SUPR_def)
    32   { fix n :: 'b
    33     have "0 + n \<le> k + n" using `0 \<le> k` by (rule add_right_mono)
    34     with * have "f n \<le> f (k + n)" by simp }
    35   thus "(SUP n. f n) \<le> (SUP n. f (k + n))"
    36     by (auto intro!: Sup_mono exI simp: SUPR_def)
    37 qed
    38 
    39 lemma (in complete_lattice) Sup_mono_offset_Suc:
    40   assumes *: "\<And>x. f x \<le> f (Suc x)"
    41   shows "(SUP n . f (Suc n)) = (SUP n. f n)"
    42   unfolding Suc_eq_plus1
    43   apply (subst add_commute)
    44   apply (rule Sup_mono_offset)
    45   by (auto intro!: order.lift_Suc_mono_le[of "op \<le>" "op <" f, OF _ *]) default
    46 
    47 lemma (in complete_lattice) Inf_mono_offset:
    48   fixes f :: "'b :: {ordered_ab_semigroup_add,monoid_add} \<Rightarrow> 'a"
    49   assumes *: "\<And>x y. x \<le> y \<Longrightarrow> f y \<le> f x" and "0 \<le> k"
    50   shows "(INF n . f (k + n)) = (INF n. f n)"
    51 proof (rule antisym)
    52   show "(INF n. f n) \<le> (INF n. f (k + n))"
    53     by (auto intro!: Inf_mono simp: INFI_def)
    54   { fix n :: 'b
    55     have "0 + n \<le> k + n" using `0 \<le> k` by (rule add_right_mono)
    56     with * have "f (k + n) \<le> f n" by simp }
    57   thus "(INF n. f (k + n)) \<le> (INF n. f n)"
    58     by (auto intro!: Inf_mono exI simp: INFI_def)
    59 qed
    60 
    61 lemma (in complete_lattice) isotone_converge:
    62   fixes f :: "nat \<Rightarrow> 'a" assumes "\<And>x y. x \<le> y \<Longrightarrow> f x \<le> f y "
    63   shows "(INF n. SUP m. f (n + m)) = (SUP n. INF m. f (n + m))"
    64 proof -
    65   have "\<And>n. (SUP m. f (n + m)) = (SUP n. f n)"
    66     apply (rule Sup_mono_offset)
    67     apply (rule assms)
    68     by simp_all
    69   moreover
    70   { fix n have "(INF m. f (n + m)) = f n"
    71       using Inf_start[of "\<lambda>m. f (n + m)"] assms by simp }
    72   ultimately show ?thesis by simp
    73 qed
    74 
    75 lemma (in complete_lattice) antitone_converges:
    76   fixes f :: "nat \<Rightarrow> 'a" assumes "\<And>x y. x \<le> y \<Longrightarrow> f y \<le> f x"
    77   shows "(INF n. SUP m. f (n + m)) = (SUP n. INF m. f (n + m))"
    78 proof -
    79   have "\<And>n. (INF m. f (n + m)) = (INF n. f n)"
    80     apply (rule Inf_mono_offset)
    81     apply (rule assms)
    82     by simp_all
    83   moreover
    84   { fix n have "(SUP m. f (n + m)) = f n"
    85       using Sup_start[of "\<lambda>m. f (n + m)"] assms by simp }
    86   ultimately show ?thesis by simp
    87 qed
    88 
    89 lemma (in complete_lattice) lim_INF_le_lim_SUP:
    90   fixes f :: "nat \<Rightarrow> 'a"
    91   shows "(SUP n. INF m. f (n + m)) \<le> (INF n. SUP m. f (n + m))"
    92 proof (rule SUP_leI, rule le_INFI)
    93   fix i j show "(INF m. f (i + m)) \<le> (SUP m. f (j + m))"
    94   proof (cases rule: le_cases)
    95     assume "i \<le> j"
    96     have "(INF m. f (i + m)) \<le> f (i + (j - i))" by (rule INF_leI) simp
    97     also have "\<dots> = f (j + 0)" using `i \<le> j` by auto
    98     also have "\<dots> \<le> (SUP m. f (j + m))" by (rule le_SUPI) simp
    99     finally show ?thesis .
   100   next
   101     assume "j \<le> i"
   102     have "(INF m. f (i + m)) \<le> f (i + 0)" by (rule INF_leI) simp
   103     also have "\<dots> = f (j + (i - j))" using `j \<le> i` by auto
   104     also have "\<dots> \<le> (SUP m. f (j + m))" by (rule le_SUPI) simp
   105     finally show ?thesis .
   106   qed
   107 qed
   108 
   109 text {*
   110 
   111 We introduce the the positive real numbers as needed for measure theory.
   112 
   113 *}
   114 
   115 typedef pextreal = "(Some ` {0::real..}) \<union> {None}"
   116   by (rule exI[of _ None]) simp
   117 
   118 subsection "Introduce @{typ pextreal} similar to a datatype"
   119 
   120 definition "Real x = Abs_pextreal (Some (sup 0 x))"
   121 definition "\<omega> = Abs_pextreal None"
   122 
   123 definition "pextreal_case f i x = (if x = \<omega> then i else f (THE r. 0 \<le> r \<and> x = Real r))"
   124 
   125 definition "of_pextreal = pextreal_case (\<lambda>x. x) 0"
   126 
   127 defs (overloaded)
   128   real_of_pextreal_def [code_unfold]: "real == of_pextreal"
   129 
   130 lemma pextreal_Some[simp]: "0 \<le> x \<Longrightarrow> Some x \<in> pextreal"
   131   unfolding pextreal_def by simp
   132 
   133 lemma pextreal_Some_sup[simp]: "Some (sup 0 x) \<in> pextreal"
   134   by (simp add: sup_ge1)
   135 
   136 lemma pextreal_None[simp]: "None \<in> pextreal"
   137   unfolding pextreal_def by simp
   138 
   139 lemma Real_inj[simp]:
   140   assumes  "0 \<le> x" and "0 \<le> y"
   141   shows "Real x = Real y \<longleftrightarrow> x = y"
   142   unfolding Real_def assms[THEN sup_absorb2]
   143   using assms by (simp add: Abs_pextreal_inject)
   144 
   145 lemma Real_neq_\<omega>[simp]:
   146   "Real x = \<omega> \<longleftrightarrow> False"
   147   "\<omega> = Real x \<longleftrightarrow> False"
   148   by (simp_all add: Abs_pextreal_inject \<omega>_def Real_def)
   149 
   150 lemma Real_neg: "x < 0 \<Longrightarrow> Real x = Real 0"
   151   unfolding Real_def by (auto simp add: Abs_pextreal_inject intro!: sup_absorb1)
   152 
   153 lemma pextreal_cases[case_names preal infinite, cases type: pextreal]:
   154   assumes preal: "\<And>r. x = Real r \<Longrightarrow> 0 \<le> r \<Longrightarrow> P" and inf: "x = \<omega> \<Longrightarrow> P"
   155   shows P
   156 proof (cases x rule: pextreal.Abs_pextreal_cases)
   157   case (Abs_pextreal y)
   158   hence "y = None \<or> (\<exists>x \<ge> 0. y = Some x)"
   159     unfolding pextreal_def by auto
   160   thus P
   161   proof (rule disjE)
   162     assume "\<exists>x\<ge>0. y = Some x" then guess x ..
   163     thus P by (simp add: preal[of x] Real_def Abs_pextreal(1) sup_absorb2)
   164   qed (simp add: \<omega>_def Abs_pextreal(1) inf)
   165 qed
   166 
   167 lemma pextreal_case_\<omega>[simp]: "pextreal_case f i \<omega> = i"
   168   unfolding pextreal_case_def by simp
   169 
   170 lemma pextreal_case_Real[simp]: "pextreal_case f i (Real x) = (if 0 \<le> x then f x else f 0)"
   171 proof (cases "0 \<le> x")
   172   case True thus ?thesis unfolding pextreal_case_def by (auto intro: theI2)
   173 next
   174   case False
   175   moreover have "(THE r. 0 \<le> r \<and> Real 0 = Real r) = 0"
   176     by (auto intro!: the_equality)
   177   ultimately show ?thesis unfolding pextreal_case_def by (simp add: Real_neg)
   178 qed
   179 
   180 lemma pextreal_case_cancel[simp]: "pextreal_case (\<lambda>c. i) i x = i"
   181   by (cases x) simp_all
   182 
   183 lemma pextreal_case_split:
   184   "P (pextreal_case f i x) = ((x = \<omega> \<longrightarrow> P i) \<and> (\<forall>r\<ge>0. x = Real r \<longrightarrow> P (f r)))"
   185   by (cases x) simp_all
   186 
   187 lemma pextreal_case_split_asm:
   188   "P (pextreal_case f i x) = (\<not> (x = \<omega> \<and> \<not> P i \<or> (\<exists>r. r \<ge> 0 \<and> x = Real r \<and> \<not> P (f r))))"
   189   by (cases x) auto
   190 
   191 lemma pextreal_case_cong[cong]:
   192   assumes eq: "x = x'" "i = i'" and cong: "\<And>r. 0 \<le> r \<Longrightarrow> f r = f' r"
   193   shows "pextreal_case f i x = pextreal_case f' i' x'"
   194   unfolding eq using cong by (cases x') simp_all
   195 
   196 lemma real_Real[simp]: "real (Real x) = (if 0 \<le> x then x else 0)"
   197   unfolding real_of_pextreal_def of_pextreal_def by simp
   198 
   199 lemma Real_real_image:
   200   assumes "\<omega> \<notin> A" shows "Real ` real ` A = A"
   201 proof safe
   202   fix x assume "x \<in> A"
   203   hence *: "x = Real (real x)"
   204     using `\<omega> \<notin> A` by (cases x) auto
   205   show "x \<in> Real ` real ` A"
   206     using `x \<in> A` by (subst *) (auto intro!: imageI)
   207 next
   208   fix x assume "x \<in> A"
   209   thus "Real (real x) \<in> A"
   210     using `\<omega> \<notin> A` by (cases x) auto
   211 qed
   212 
   213 lemma real_pextreal_nonneg[simp, intro]: "0 \<le> real (x :: pextreal)"
   214   unfolding real_of_pextreal_def of_pextreal_def
   215   by (cases x) auto
   216 
   217 lemma real_\<omega>[simp]: "real \<omega> = 0"
   218   unfolding real_of_pextreal_def of_pextreal_def by simp
   219 
   220 lemma pextreal_noteq_omega_Ex: "X \<noteq> \<omega> \<longleftrightarrow> (\<exists>r\<ge>0. X = Real r)" by (cases X) auto
   221 
   222 subsection "@{typ pextreal} is a monoid for addition"
   223 
   224 instantiation pextreal :: comm_monoid_add
   225 begin
   226 
   227 definition "0 = Real 0"
   228 definition "x + y = pextreal_case (\<lambda>r. pextreal_case (\<lambda>p. Real (r + p)) \<omega> y) \<omega> x"
   229 
   230 lemma pextreal_plus[simp]:
   231   "Real r + Real p = (if 0 \<le> r then if 0 \<le> p then Real (r + p) else Real r else Real p)"
   232   "x + 0 = x"
   233   "0 + x = x"
   234   "x + \<omega> = \<omega>"
   235   "\<omega> + x = \<omega>"
   236   by (simp_all add: plus_pextreal_def Real_neg zero_pextreal_def split: pextreal_case_split)
   237 
   238 lemma \<omega>_neq_0[simp]:
   239   "\<omega> = 0 \<longleftrightarrow> False"
   240   "0 = \<omega> \<longleftrightarrow> False"
   241   by (simp_all add: zero_pextreal_def)
   242 
   243 lemma Real_eq_0[simp]:
   244   "Real r = 0 \<longleftrightarrow> r \<le> 0"
   245   "0 = Real r \<longleftrightarrow> r \<le> 0"
   246   by (auto simp add: Abs_pextreal_inject zero_pextreal_def Real_def sup_real_def)
   247 
   248 lemma Real_0[simp]: "Real 0 = 0" by (simp add: zero_pextreal_def)
   249 
   250 instance
   251 proof
   252   fix a :: pextreal
   253   show "0 + a = a" by (cases a) simp_all
   254 
   255   fix b show "a + b = b + a"
   256     by (cases a, cases b) simp_all
   257 
   258   fix c show "a + b + c = a + (b + c)"
   259     by (cases a, cases b, cases c) simp_all
   260 qed
   261 end
   262 
   263 lemma Real_minus_abs[simp]: "Real (- \<bar>x\<bar>) = 0"
   264   by simp
   265 
   266 lemma pextreal_plus_eq_\<omega>[simp]: "(a :: pextreal) + b = \<omega> \<longleftrightarrow> a = \<omega> \<or> b = \<omega>"
   267   by (cases a, cases b) auto
   268 
   269 lemma pextreal_add_cancel_left:
   270   "a + b = a + c \<longleftrightarrow> (a = \<omega> \<or> b = c)"
   271   by (cases a, cases b, cases c, simp_all, cases c, simp_all)
   272 
   273 lemma pextreal_add_cancel_right:
   274   "b + a = c + a \<longleftrightarrow> (a = \<omega> \<or> b = c)"
   275   by (cases a, cases b, cases c, simp_all, cases c, simp_all)
   276 
   277 lemma Real_eq_Real:
   278   "Real a = Real b \<longleftrightarrow> (a = b \<or> (a \<le> 0 \<and> b \<le> 0))"
   279 proof (cases "a \<le> 0 \<or> b \<le> 0")
   280   case False with Real_inj[of a b] show ?thesis by auto
   281 next
   282   case True
   283   thus ?thesis
   284   proof
   285     assume "a \<le> 0"
   286     hence *: "Real a = 0" by simp
   287     show ?thesis using `a \<le> 0` unfolding * by auto
   288   next
   289     assume "b \<le> 0"
   290     hence *: "Real b = 0" by simp
   291     show ?thesis using `b \<le> 0` unfolding * by auto
   292   qed
   293 qed
   294 
   295 lemma real_pextreal_0[simp]: "real (0 :: pextreal) = 0"
   296   unfolding zero_pextreal_def real_Real by simp
   297 
   298 lemma real_of_pextreal_eq_0: "real X = 0 \<longleftrightarrow> (X = 0 \<or> X = \<omega>)"
   299   by (cases X) auto
   300 
   301 lemma real_of_pextreal_eq: "real X = real Y \<longleftrightarrow>
   302     (X = Y \<or> (X = 0 \<and> Y = \<omega>) \<or> (Y = 0 \<and> X = \<omega>))"
   303   by (cases X, cases Y) (auto simp add: real_of_pextreal_eq_0)
   304 
   305 lemma real_of_pextreal_add: "real X + real Y =
   306     (if X = \<omega> then real Y else if Y = \<omega> then real X else real (X + Y))"
   307   by (auto simp: pextreal_noteq_omega_Ex)
   308 
   309 subsection "@{typ pextreal} is a monoid for multiplication"
   310 
   311 instantiation pextreal :: comm_monoid_mult
   312 begin
   313 
   314 definition "1 = Real 1"
   315 definition "x * y = (if x = 0 \<or> y = 0 then 0 else
   316   pextreal_case (\<lambda>r. pextreal_case (\<lambda>p. Real (r * p)) \<omega> y) \<omega> x)"
   317 
   318 lemma pextreal_times[simp]:
   319   "Real r * Real p = (if 0 \<le> r \<and> 0 \<le> p then Real (r * p) else 0)"
   320   "\<omega> * x = (if x = 0 then 0 else \<omega>)"
   321   "x * \<omega> = (if x = 0 then 0 else \<omega>)"
   322   "0 * x = 0"
   323   "x * 0 = 0"
   324   "1 = \<omega> \<longleftrightarrow> False"
   325   "\<omega> = 1 \<longleftrightarrow> False"
   326   by (auto simp add: times_pextreal_def one_pextreal_def)
   327 
   328 lemma pextreal_one_mult[simp]:
   329   "Real x + 1 = (if 0 \<le> x then Real (x + 1) else 1)"
   330   "1 + Real x = (if 0 \<le> x then Real (1 + x) else 1)"
   331   unfolding one_pextreal_def by simp_all
   332 
   333 instance
   334 proof
   335   fix a :: pextreal show "1 * a = a"
   336     by (cases a) (simp_all add: one_pextreal_def)
   337 
   338   fix b show "a * b = b * a"
   339     by (cases a, cases b) (simp_all add: mult_nonneg_nonneg)
   340 
   341   fix c show "a * b * c = a * (b * c)"
   342     apply (cases a, cases b, cases c)
   343     apply (simp_all add: mult_nonneg_nonneg not_le mult_pos_pos)
   344     apply (cases b, cases c)
   345     apply (simp_all add: mult_nonneg_nonneg not_le mult_pos_pos)
   346     done
   347 qed
   348 end
   349 
   350 lemma pextreal_mult_cancel_left:
   351   "a * b = a * c \<longleftrightarrow> (a = 0 \<or> b = c \<or> (a = \<omega> \<and> b \<noteq> 0 \<and> c \<noteq> 0))"
   352   by (cases a, cases b, cases c, auto simp: Real_eq_Real mult_le_0_iff, cases c, auto)
   353 
   354 lemma pextreal_mult_cancel_right:
   355   "b * a = c * a \<longleftrightarrow> (a = 0 \<or> b = c \<or> (a = \<omega> \<and> b \<noteq> 0 \<and> c \<noteq> 0))"
   356   by (cases a, cases b, cases c, auto simp: Real_eq_Real mult_le_0_iff, cases c, auto)
   357 
   358 lemma Real_1[simp]: "Real 1 = 1" by (simp add: one_pextreal_def)
   359 
   360 lemma real_pextreal_1[simp]: "real (1 :: pextreal) = 1"
   361   unfolding one_pextreal_def real_Real by simp
   362 
   363 lemma real_of_pextreal_mult: "real X * real Y = real (X * Y :: pextreal)"
   364   by (cases X, cases Y) (auto simp: zero_le_mult_iff)
   365 
   366 lemma Real_mult_nonneg: assumes "x \<ge> 0" "y \<ge> 0"
   367   shows "Real (x * y) = Real x * Real y" using assms by auto
   368 
   369 lemma Real_setprod: assumes "\<forall>x\<in>A. f x \<ge> 0" shows "Real (setprod f A) = setprod (\<lambda>x. Real (f x)) A"
   370 proof(cases "finite A")
   371   case True thus ?thesis using assms
   372   proof(induct A) case (insert x A)
   373     have "0 \<le> setprod f A" apply(rule setprod_nonneg) using insert by auto
   374     thus ?case unfolding setprod_insert[OF insert(1-2)] apply-
   375       apply(subst Real_mult_nonneg) prefer 3 apply(subst insert(3)[THEN sym])
   376       using insert by auto
   377   qed auto
   378 qed auto
   379 
   380 subsection "@{typ pextreal} is a linear order"
   381 
   382 instantiation pextreal :: linorder
   383 begin
   384 
   385 definition "x < y \<longleftrightarrow> pextreal_case (\<lambda>i. pextreal_case (\<lambda>j. i < j) True y) False x"
   386 definition "x \<le> y \<longleftrightarrow> pextreal_case (\<lambda>j. pextreal_case (\<lambda>i. i \<le> j) False x) True y"
   387 
   388 lemma pextreal_less[simp]:
   389   "Real r < \<omega>"
   390   "Real r < Real p \<longleftrightarrow> (if 0 \<le> r \<and> 0 \<le> p then r < p else 0 < p)"
   391   "\<omega> < x \<longleftrightarrow> False"
   392   "0 < \<omega>"
   393   "0 < Real r \<longleftrightarrow> 0 < r"
   394   "x < 0 \<longleftrightarrow> False"
   395   "0 < (1::pextreal)"
   396   by (simp_all add: less_pextreal_def zero_pextreal_def one_pextreal_def del: Real_0 Real_1)
   397 
   398 lemma pextreal_less_eq[simp]:
   399   "x \<le> \<omega>"
   400   "Real r \<le> Real p \<longleftrightarrow> (if 0 \<le> r \<and> 0 \<le> p then r \<le> p else r \<le> 0)"
   401   "0 \<le> x"
   402   by (simp_all add: less_eq_pextreal_def zero_pextreal_def del: Real_0)
   403 
   404 lemma pextreal_\<omega>_less_eq[simp]:
   405   "\<omega> \<le> x \<longleftrightarrow> x = \<omega>"
   406   by (cases x) (simp_all add: not_le less_eq_pextreal_def)
   407 
   408 lemma pextreal_less_eq_zero[simp]:
   409   "(x::pextreal) \<le> 0 \<longleftrightarrow> x = 0"
   410   by (cases x) (simp_all add: zero_pextreal_def del: Real_0)
   411 
   412 instance
   413 proof
   414   fix x :: pextreal
   415   show "x \<le> x" by (cases x) simp_all
   416   fix y
   417   show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)"
   418     by (cases x, cases y) auto
   419   show "x \<le> y \<or> y \<le> x "
   420     by (cases x, cases y) auto
   421   { assume "x \<le> y" "y \<le> x" thus "x = y"
   422       by (cases x, cases y) auto }
   423   { fix z assume "x \<le> y" "y \<le> z"
   424     thus "x \<le> z" by (cases x, cases y, cases z) auto }
   425 qed
   426 end
   427 
   428 lemma pextreal_zero_lessI[intro]:
   429   "(a :: pextreal) \<noteq> 0 \<Longrightarrow> 0 < a"
   430   by (cases a) auto
   431 
   432 lemma pextreal_less_omegaI[intro, simp]:
   433   "a \<noteq> \<omega> \<Longrightarrow> a < \<omega>"
   434   by (cases a) auto
   435 
   436 lemma pextreal_plus_eq_0[simp]: "(a :: pextreal) + b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
   437   by (cases a, cases b) auto
   438 
   439 lemma pextreal_le_add1[simp, intro]: "n \<le> n + (m::pextreal)"
   440   by (cases n, cases m) simp_all
   441 
   442 lemma pextreal_le_add2: "(n::pextreal) + m \<le> k \<Longrightarrow> m \<le> k"
   443   by (cases n, cases m, cases k) simp_all
   444 
   445 lemma pextreal_le_add3: "(n::pextreal) + m \<le> k \<Longrightarrow> n \<le> k"
   446   by (cases n, cases m, cases k) simp_all
   447 
   448 lemma pextreal_less_\<omega>: "x < \<omega> \<longleftrightarrow> x \<noteq> \<omega>"
   449   by (cases x) auto
   450 
   451 lemma pextreal_0_less_mult_iff[simp]:
   452   fixes x y :: pextreal shows "0 < x * y \<longleftrightarrow> 0 < x \<and> 0 < y"
   453   by (cases x, cases y) (auto simp: zero_less_mult_iff)
   454 
   455 lemma pextreal_ord_one[simp]:
   456   "Real p < 1 \<longleftrightarrow> p < 1"
   457   "Real p \<le> 1 \<longleftrightarrow> p \<le> 1"
   458   "1 < Real p \<longleftrightarrow> 1 < p"
   459   "1 \<le> Real p \<longleftrightarrow> 1 \<le> p"
   460   by (simp_all add: one_pextreal_def del: Real_1)
   461 
   462 subsection {* @{text "x - y"} on @{typ pextreal} *}
   463 
   464 instantiation pextreal :: minus
   465 begin
   466 definition "x - y = (if y < x then THE d. x = y + d else 0 :: pextreal)"
   467 
   468 lemma minus_pextreal_eq:
   469   "(x - y = (z :: pextreal)) \<longleftrightarrow> (if y < x then x = y + z else z = 0)"
   470   (is "?diff \<longleftrightarrow> ?if")
   471 proof
   472   assume ?diff
   473   thus ?if
   474   proof (cases "y < x")
   475     case True
   476     then obtain p where p: "y = Real p" "0 \<le> p" by (cases y) auto
   477 
   478     show ?thesis unfolding `?diff`[symmetric] if_P[OF True] minus_pextreal_def
   479     proof (rule theI2[where Q="\<lambda>d. x = y + d"])
   480       show "x = y + pextreal_case (\<lambda>r. Real (r - real y)) \<omega> x" (is "x = y + ?d")
   481         using `y < x` p by (cases x) simp_all
   482 
   483       fix d assume "x = y + d"
   484       thus "d = ?d" using `y < x` p by (cases d, cases x) simp_all
   485     qed simp
   486   qed (simp add: minus_pextreal_def)
   487 next
   488   assume ?if
   489   thus ?diff
   490   proof (cases "y < x")
   491     case True
   492     then obtain p where p: "y = Real p" "0 \<le> p" by (cases y) auto
   493 
   494     from True `?if` have "x = y + z" by simp
   495 
   496     show ?thesis unfolding minus_pextreal_def if_P[OF True] unfolding `x = y + z`
   497     proof (rule the_equality)
   498       fix d :: pextreal assume "y + z = y + d"
   499       thus "d = z" using `y < x` p
   500         by (cases d, cases z) simp_all
   501     qed simp
   502   qed (simp add: minus_pextreal_def)
   503 qed
   504 
   505 instance ..
   506 end
   507 
   508 lemma pextreal_minus[simp]:
   509   "Real r - Real p = (if 0 \<le> r \<and> p < r then if 0 \<le> p then Real (r - p) else Real r else 0)"
   510   "(A::pextreal) - A = 0"
   511   "\<omega> - Real r = \<omega>"
   512   "Real r - \<omega> = 0"
   513   "A - 0 = A"
   514   "0 - A = 0"
   515   by (auto simp: minus_pextreal_eq not_less)
   516 
   517 lemma pextreal_le_epsilon:
   518   fixes x y :: pextreal
   519   assumes "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e"
   520   shows "x \<le> y"
   521 proof (cases y)
   522   case (preal r)
   523   then obtain p where x: "x = Real p" "0 \<le> p"
   524     using assms[of 1] by (cases x) auto
   525   { fix e have "0 < e \<Longrightarrow> p \<le> r + e"
   526       using assms[of "Real e"] preal x by auto }
   527   hence "p \<le> r" by (rule field_le_epsilon)
   528   thus ?thesis using preal x by auto
   529 qed simp
   530 
   531 instance pextreal :: "{ordered_comm_semiring, comm_semiring_1}"
   532 proof
   533   show "0 \<noteq> (1::pextreal)" unfolding zero_pextreal_def one_pextreal_def
   534     by (simp del: Real_1 Real_0)
   535 
   536   fix a :: pextreal
   537   show "0 * a = 0" "a * 0 = 0" by simp_all
   538 
   539   fix b c :: pextreal
   540   show "(a + b) * c = a * c + b * c"
   541     by (cases c, cases a, cases b)
   542        (auto intro!: arg_cong[where f=Real] simp: field_simps not_le mult_le_0_iff mult_less_0_iff)
   543 
   544   { assume "a \<le> b" thus "c + a \<le> c + b"
   545      by (cases c, cases a, cases b) auto }
   546 
   547   assume "a \<le> b" "0 \<le> c"
   548   thus "c * a \<le> c * b"
   549     apply (cases c, cases a, cases b)
   550     by (auto simp: mult_left_mono mult_le_0_iff mult_less_0_iff not_le)
   551 qed
   552 
   553 lemma mult_\<omega>[simp]: "x * y = \<omega> \<longleftrightarrow> (x = \<omega> \<or> y = \<omega>) \<and> x \<noteq> 0 \<and> y \<noteq> 0"
   554   by (cases x, cases y) auto
   555 
   556 lemma \<omega>_mult[simp]: "(\<omega> = x * y) = ((x = \<omega> \<or> y = \<omega>) \<and> x \<noteq> 0 \<and> y \<noteq> 0)"
   557   by (cases x, cases y) auto
   558 
   559 lemma pextreal_mult_0[simp]: "x * y = 0 \<longleftrightarrow> x = 0 \<or> (y::pextreal) = 0"
   560   by (cases x, cases y) (auto simp: mult_le_0_iff)
   561 
   562 lemma pextreal_mult_cancel:
   563   fixes x y z :: pextreal
   564   assumes "y \<le> z"
   565   shows "x * y \<le> x * z"
   566   using assms
   567   by (cases x, cases y, cases z)
   568      (auto simp: mult_le_cancel_left mult_le_0_iff mult_less_0_iff not_le)
   569 
   570 lemma Real_power[simp]:
   571   "Real x ^ n = (if x \<le> 0 then (if n = 0 then 1 else 0) else Real (x ^ n))"
   572   by (induct n) auto
   573 
   574 lemma Real_power_\<omega>[simp]:
   575   "\<omega> ^ n = (if n = 0 then 1 else \<omega>)"
   576   by (induct n) auto
   577 
   578 lemma pextreal_of_nat[simp]: "of_nat m = Real (real m)"
   579   by (induct m) (auto simp: real_of_nat_Suc one_pextreal_def simp del: Real_1)
   580 
   581 lemma less_\<omega>_Ex_of_nat: "x < \<omega> \<longleftrightarrow> (\<exists>n. x < of_nat n)"
   582 proof safe
   583   assume "x < \<omega>"
   584   then obtain r where "0 \<le> r" "x = Real r" by (cases x) auto
   585   moreover obtain n where "r < of_nat n" using ex_less_of_nat by auto
   586   ultimately show "\<exists>n. x < of_nat n" by (auto simp: real_eq_of_nat)
   587 qed auto
   588 
   589 lemma real_of_pextreal_mono:
   590   fixes a b :: pextreal
   591   assumes "b \<noteq> \<omega>" "a \<le> b"
   592   shows "real a \<le> real b"
   593 using assms by (cases b, cases a) auto
   594 
   595 lemma setprod_pextreal_0:
   596   "(\<Prod>i\<in>I. f i) = (0::pextreal) \<longleftrightarrow> finite I \<and> (\<exists>i\<in>I. f i = 0)"
   597 proof cases
   598   assume "finite I" then show ?thesis
   599   proof (induct I)
   600     case (insert i I)
   601     then show ?case by simp
   602   qed simp
   603 qed simp
   604 
   605 lemma setprod_\<omega>:
   606   "(\<Prod>i\<in>I. f i) = \<omega> \<longleftrightarrow> finite I \<and> (\<exists>i\<in>I. f i = \<omega>) \<and> (\<forall>i\<in>I. f i \<noteq> 0)"
   607 proof cases
   608   assume "finite I" then show ?thesis
   609   proof (induct I)
   610     case (insert i I) then show ?case
   611       by (auto simp: setprod_pextreal_0)
   612   qed simp
   613 qed simp
   614 
   615 instance pextreal :: "semiring_char_0"
   616 proof
   617   fix m n
   618   show "inj (of_nat::nat\<Rightarrow>pextreal)" by (auto intro!: inj_onI)
   619 qed
   620 
   621 subsection "@{typ pextreal} is a complete lattice"
   622 
   623 instantiation pextreal :: lattice
   624 begin
   625 definition [simp]: "sup x y = (max x y :: pextreal)"
   626 definition [simp]: "inf x y = (min x y :: pextreal)"
   627 instance proof qed simp_all
   628 end
   629 
   630 instantiation pextreal :: complete_lattice
   631 begin
   632 
   633 definition "bot = Real 0"
   634 definition "top = \<omega>"
   635 
   636 definition "Sup S = (LEAST z. \<forall>x\<in>S. x \<le> z :: pextreal)"
   637 definition "Inf S = (GREATEST z. \<forall>x\<in>S. z \<le> x :: pextreal)"
   638 
   639 lemma pextreal_complete_Sup:
   640   fixes S :: "pextreal set" assumes "S \<noteq> {}"
   641   shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) \<and> (\<forall>z. (\<forall>y\<in>S. y \<le> z) \<longrightarrow> x \<le> z)"
   642 proof (cases "\<exists>x\<ge>0. \<forall>a\<in>S. a \<le> Real x")
   643   case False
   644   hence *: "\<And>x. x\<ge>0 \<Longrightarrow> \<exists>a\<in>S. \<not>a \<le> Real x" by simp
   645   show ?thesis
   646   proof (safe intro!: exI[of _ \<omega>])
   647     fix y assume **: "\<forall>z\<in>S. z \<le> y"
   648     show "\<omega> \<le> y" unfolding pextreal_\<omega>_less_eq
   649     proof (rule ccontr)
   650       assume "y \<noteq> \<omega>"
   651       then obtain x where [simp]: "y = Real x" and "0 \<le> x" by (cases y) auto
   652       from *[OF `0 \<le> x`] show False using ** by auto
   653     qed
   654   qed simp
   655 next
   656   case True then obtain y where y: "\<And>a. a\<in>S \<Longrightarrow> a \<le> Real y" and "0 \<le> y" by auto
   657   from y[of \<omega>] have "\<omega> \<notin> S" by auto
   658 
   659   with `S \<noteq> {}` obtain x where "x \<in> S" and "x \<noteq> \<omega>" by auto
   660 
   661   have bound: "\<forall>x\<in>real ` S. x \<le> y"
   662   proof
   663     fix z assume "z \<in> real ` S" then guess a ..
   664     with y[of a] `\<omega> \<notin> S` `0 \<le> y` show "z \<le> y" by (cases a) auto
   665   qed
   666   with reals_complete2[of "real ` S"] `x \<in> S`
   667   obtain s where s: "\<forall>y\<in>S. real y \<le> s" "\<forall>z. ((\<forall>y\<in>S. real y \<le> z) \<longrightarrow> s \<le> z)"
   668     by auto
   669 
   670   show ?thesis
   671   proof (safe intro!: exI[of _ "Real s"])
   672     fix z assume "z \<in> S" thus "z \<le> Real s"
   673       using s `\<omega> \<notin> S` by (cases z) auto
   674   next
   675     fix z assume *: "\<forall>y\<in>S. y \<le> z"
   676     show "Real s \<le> z"
   677     proof (cases z)
   678       case (preal u)
   679       { fix v assume "v \<in> S"
   680         hence "v \<le> Real u" using * preal by auto
   681         hence "real v \<le> u" using `\<omega> \<notin> S` `0 \<le> u` by (cases v) auto }
   682       hence "s \<le> u" using s(2) by auto
   683       thus "Real s \<le> z" using preal by simp
   684     qed simp
   685   qed
   686 qed
   687 
   688 lemma pextreal_complete_Inf:
   689   fixes S :: "pextreal set" assumes "S \<noteq> {}"
   690   shows "\<exists>x. (\<forall>y\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>y\<in>S. z \<le> y) \<longrightarrow> z \<le> x)"
   691 proof (cases "S = {\<omega>}")
   692   case True thus ?thesis by (auto intro!: exI[of _ \<omega>])
   693 next
   694   case False with `S \<noteq> {}` have "S - {\<omega>} \<noteq> {}" by auto
   695   hence not_empty: "\<exists>x. x \<in> uminus ` real ` (S - {\<omega>})" by auto
   696   have bounds: "\<exists>x. \<forall>y\<in>uminus ` real ` (S - {\<omega>}). y \<le> x" by (auto intro!: exI[of _ 0])
   697   from reals_complete2[OF not_empty bounds]
   698   obtain s where s: "\<And>y. y\<in>S - {\<omega>} \<Longrightarrow> - real y \<le> s" "\<forall>z. ((\<forall>y\<in>S - {\<omega>}. - real y \<le> z) \<longrightarrow> s \<le> z)"
   699     by auto
   700 
   701   show ?thesis
   702   proof (safe intro!: exI[of _ "Real (-s)"])
   703     fix z assume "z \<in> S"
   704     show "Real (-s) \<le> z"
   705     proof (cases z)
   706       case (preal r)
   707       with s `z \<in> S` have "z \<in> S - {\<omega>}" by simp
   708       hence "- r \<le> s" using preal s(1)[of z] by auto
   709       hence "- s \<le> r" by (subst neg_le_iff_le[symmetric]) simp
   710       thus ?thesis using preal by simp
   711     qed simp
   712   next
   713     fix z assume *: "\<forall>y\<in>S. z \<le> y"
   714     show "z \<le> Real (-s)"
   715     proof (cases z)
   716       case (preal u)
   717       { fix v assume "v \<in> S-{\<omega>}"
   718         hence "Real u \<le> v" using * preal by auto
   719         hence "- real v \<le> - u" using `0 \<le> u` `v \<in> S - {\<omega>}` by (cases v) auto }
   720       hence "u \<le> - s" using s(2) by (subst neg_le_iff_le[symmetric]) auto
   721       thus "z \<le> Real (-s)" using preal by simp
   722     next
   723       case infinite
   724       with * have "S = {\<omega>}" using `S \<noteq> {}` by auto
   725       with `S - {\<omega>} \<noteq> {}` show ?thesis by simp
   726     qed
   727   qed
   728 qed
   729 
   730 instance
   731 proof
   732   fix x :: pextreal and A
   733 
   734   show "bot \<le> x" by (cases x) (simp_all add: bot_pextreal_def)
   735   show "x \<le> top" by (simp add: top_pextreal_def)
   736 
   737   { assume "x \<in> A"
   738     with pextreal_complete_Sup[of A]
   739     obtain s where s: "\<forall>y\<in>A. y \<le> s" "\<forall>z. (\<forall>y\<in>A. y \<le> z) \<longrightarrow> s \<le> z" by auto
   740     hence "x \<le> s" using `x \<in> A` by auto
   741     also have "... = Sup A" using s unfolding Sup_pextreal_def
   742       by (auto intro!: Least_equality[symmetric])
   743     finally show "x \<le> Sup A" . }
   744 
   745   { assume "x \<in> A"
   746     with pextreal_complete_Inf[of A]
   747     obtain i where i: "\<forall>y\<in>A. i \<le> y" "\<forall>z. (\<forall>y\<in>A. z \<le> y) \<longrightarrow> z \<le> i" by auto
   748     hence "Inf A = i" unfolding Inf_pextreal_def
   749       by (auto intro!: Greatest_equality)
   750     also have "i \<le> x" using i `x \<in> A` by auto
   751     finally show "Inf A \<le> x" . }
   752 
   753   { assume *: "\<And>z. z \<in> A \<Longrightarrow> z \<le> x"
   754     show "Sup A \<le> x"
   755     proof (cases "A = {}")
   756       case True
   757       hence "Sup A = 0" unfolding Sup_pextreal_def
   758         by (auto intro!: Least_equality)
   759       thus "Sup A \<le> x" by simp
   760     next
   761       case False
   762       with pextreal_complete_Sup[of A]
   763       obtain s where s: "\<forall>y\<in>A. y \<le> s" "\<forall>z. (\<forall>y\<in>A. y \<le> z) \<longrightarrow> s \<le> z" by auto
   764       hence "Sup A = s"
   765         unfolding Sup_pextreal_def by (auto intro!: Least_equality)
   766       also have "s \<le> x" using * s by auto
   767       finally show "Sup A \<le> x" .
   768     qed }
   769 
   770   { assume *: "\<And>z. z \<in> A \<Longrightarrow> x \<le> z"
   771     show "x \<le> Inf A"
   772     proof (cases "A = {}")
   773       case True
   774       hence "Inf A = \<omega>" unfolding Inf_pextreal_def
   775         by (auto intro!: Greatest_equality)
   776       thus "x \<le> Inf A" by simp
   777     next
   778       case False
   779       with pextreal_complete_Inf[of A]
   780       obtain i where i: "\<forall>y\<in>A. i \<le> y" "\<forall>z. (\<forall>y\<in>A. z \<le> y) \<longrightarrow> z \<le> i" by auto
   781       have "x \<le> i" using * i by auto
   782       also have "i = Inf A" using i
   783         unfolding Inf_pextreal_def by (auto intro!: Greatest_equality[symmetric])
   784       finally show "x \<le> Inf A" .
   785     qed }
   786 qed
   787 end
   788 
   789 lemma Inf_pextreal_iff:
   790   fixes z :: pextreal
   791   shows "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> (\<exists>x\<in>X. x<y) \<longleftrightarrow> Inf X < y"
   792   by (metis complete_lattice_class.Inf_greatest complete_lattice_class.Inf_lower less_le_not_le linear
   793             order_less_le_trans)
   794 
   795 lemma Inf_greater:
   796   fixes z :: pextreal assumes "Inf X < z"
   797   shows "\<exists>x \<in> X. x < z"
   798 proof -
   799   have "X \<noteq> {}" using assms by (auto simp: Inf_empty top_pextreal_def)
   800   with assms show ?thesis
   801     by (metis Inf_pextreal_iff mem_def not_leE)
   802 qed
   803 
   804 lemma Inf_close:
   805   fixes e :: pextreal assumes "Inf X \<noteq> \<omega>" "0 < e"
   806   shows "\<exists>x \<in> X. x < Inf X + e"
   807 proof (rule Inf_greater)
   808   show "Inf X < Inf X + e" using assms
   809     by (cases "Inf X", cases e) auto
   810 qed
   811 
   812 lemma pextreal_SUPI:
   813   fixes x :: pextreal
   814   assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x"
   815   assumes "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> x \<le> y"
   816   shows "(SUP i:A. f i) = x"
   817   unfolding SUPR_def Sup_pextreal_def
   818   using assms by (auto intro!: Least_equality)
   819 
   820 lemma Sup_pextreal_iff:
   821   fixes z :: pextreal
   822   shows "(\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> (\<exists>x\<in>X. y<x) \<longleftrightarrow> y < Sup X"
   823   by (metis complete_lattice_class.Sup_least complete_lattice_class.Sup_upper less_le_not_le linear
   824             order_less_le_trans)
   825 
   826 lemma Sup_lesser:
   827   fixes z :: pextreal assumes "z < Sup X"
   828   shows "\<exists>x \<in> X. z < x"
   829 proof -
   830   have "X \<noteq> {}" using assms by (auto simp: Sup_empty bot_pextreal_def)
   831   with assms show ?thesis
   832     by (metis Sup_pextreal_iff mem_def not_leE)
   833 qed
   834 
   835 lemma Sup_eq_\<omega>: "\<omega> \<in> S \<Longrightarrow> Sup S = \<omega>"
   836   unfolding Sup_pextreal_def
   837   by (auto intro!: Least_equality)
   838 
   839 lemma Sup_close:
   840   assumes "0 < e" and S: "Sup S \<noteq> \<omega>" "S \<noteq> {}"
   841   shows "\<exists>X\<in>S. Sup S < X + e"
   842 proof cases
   843   assume "Sup S = 0"
   844   moreover obtain X where "X \<in> S" using `S \<noteq> {}` by auto
   845   ultimately show ?thesis using `0 < e` by (auto intro!: bexI[OF _ `X\<in>S`])
   846 next
   847   assume "Sup S \<noteq> 0"
   848   have "\<exists>X\<in>S. Sup S - e < X"
   849   proof (rule Sup_lesser)
   850     show "Sup S - e < Sup S" using `0 < e` `Sup S \<noteq> 0` `Sup S \<noteq> \<omega>`
   851       by (cases e) (auto simp: pextreal_noteq_omega_Ex)
   852   qed
   853   then guess X .. note X = this
   854   with `Sup S \<noteq> \<omega>` Sup_eq_\<omega> have "X \<noteq> \<omega>" by auto
   855   thus ?thesis using `Sup S \<noteq> \<omega>` X unfolding pextreal_noteq_omega_Ex
   856     by (cases e) (auto intro!: bexI[OF _ `X\<in>S`] simp: split: split_if_asm)
   857 qed
   858 
   859 lemma Sup_\<omega>: "(SUP i::nat. Real (real i)) = \<omega>"
   860 proof (rule pextreal_SUPI)
   861   fix y assume *: "\<And>i::nat. i \<in> UNIV \<Longrightarrow> Real (real i) \<le> y"
   862   thus "\<omega> \<le> y"
   863   proof (cases y)
   864     case (preal r)
   865     then obtain k :: nat where "r < real k"
   866       using ex_less_of_nat by (auto simp: real_eq_of_nat)
   867     with *[of k] preal show ?thesis by auto
   868   qed simp
   869 qed simp
   870 
   871 lemma SUP_\<omega>: "(SUP i:A. f i) = \<omega> \<longleftrightarrow> (\<forall>x<\<omega>. \<exists>i\<in>A. x < f i)"
   872 proof
   873   assume *: "(SUP i:A. f i) = \<omega>"
   874   show "(\<forall>x<\<omega>. \<exists>i\<in>A. x < f i)" unfolding *[symmetric]
   875   proof (intro allI impI)
   876     fix x assume "x < SUPR A f" then show "\<exists>i\<in>A. x < f i"
   877       unfolding less_SUP_iff by auto
   878   qed
   879 next
   880   assume *: "\<forall>x<\<omega>. \<exists>i\<in>A. x < f i"
   881   show "(SUP i:A. f i) = \<omega>"
   882   proof (rule pextreal_SUPI)
   883     fix y assume **: "\<And>i. i \<in> A \<Longrightarrow> f i \<le> y"
   884     show "\<omega> \<le> y"
   885     proof cases
   886       assume "y < \<omega>"
   887       from *[THEN spec, THEN mp, OF this]
   888       obtain i where "i \<in> A" "\<not> (f i \<le> y)" by auto
   889       with ** show ?thesis by auto
   890     qed auto
   891   qed auto
   892 qed
   893 
   894 subsubsection {* Equivalence between @{text "f ----> x"} and @{text SUP} on @{typ pextreal} *}
   895 
   896 lemma monoseq_monoI: "mono f \<Longrightarrow> monoseq f"
   897   unfolding mono_def monoseq_def by auto
   898 
   899 lemma incseq_mono: "mono f \<longleftrightarrow> incseq f"
   900   unfolding mono_def incseq_def by auto
   901 
   902 lemma SUP_eq_LIMSEQ:
   903   assumes "mono f" and "\<And>n. 0 \<le> f n" and "0 \<le> x"
   904   shows "(SUP n. Real (f n)) = Real x \<longleftrightarrow> f ----> x"
   905 proof
   906   assume x: "(SUP n. Real (f n)) = Real x"
   907   { fix n
   908     have "Real (f n) \<le> Real x" using x[symmetric] by (auto intro: le_SUPI)
   909     hence "f n \<le> x" using assms by simp }
   910   show "f ----> x"
   911   proof (rule LIMSEQ_I)
   912     fix r :: real assume "0 < r"
   913     show "\<exists>no. \<forall>n\<ge>no. norm (f n - x) < r"
   914     proof (rule ccontr)
   915       assume *: "\<not> ?thesis"
   916       { fix N
   917         from * obtain n where "N \<le> n" "r \<le> x - f n"
   918           using `\<And>n. f n \<le> x` by (auto simp: not_less)
   919         hence "f N \<le> f n" using `mono f` by (auto dest: monoD)
   920         hence "f N \<le> x - r" using `r \<le> x - f n` by auto
   921         hence "Real (f N) \<le> Real (x - r)" and "r \<le> x" using `0 \<le> f N` by auto }
   922       hence "(SUP n. Real (f n)) \<le> Real (x - r)"
   923         and "Real (x - r) < Real x" using `0 < r` by (auto intro: SUP_leI)
   924       hence "(SUP n. Real (f n)) < Real x" by (rule le_less_trans)
   925       thus False using x by auto
   926     qed
   927   qed
   928 next
   929   assume "f ----> x"
   930   show "(SUP n. Real (f n)) = Real x"
   931   proof (rule pextreal_SUPI)
   932     fix n
   933     from incseq_le[of f x] `mono f` `f ----> x`
   934     show "Real (f n) \<le> Real x" using assms incseq_mono by auto
   935   next
   936     fix y assume *: "\<And>n. n\<in>UNIV \<Longrightarrow> Real (f n) \<le> y"
   937     show "Real x \<le> y"
   938     proof (cases y)
   939       case (preal r)
   940       with * have "\<exists>N. \<forall>n\<ge>N. f n \<le> r" using assms by fastsimp
   941       from LIMSEQ_le_const2[OF `f ----> x` this]
   942       show "Real x \<le> y" using `0 \<le> x` preal by auto
   943     qed simp
   944   qed
   945 qed
   946 
   947 lemma SUPR_bound:
   948   assumes "\<forall>N. f N \<le> x"
   949   shows "(SUP n. f n) \<le> x"
   950   using assms by (simp add: SUPR_def Sup_le_iff)
   951 
   952 lemma pextreal_less_eq_diff_eq_sum:
   953   fixes x y z :: pextreal
   954   assumes "y \<le> x" and "x \<noteq> \<omega>"
   955   shows "z \<le> x - y \<longleftrightarrow> z + y \<le> x"
   956   using assms
   957   apply (cases z, cases y, cases x)
   958   by (simp_all add: field_simps minus_pextreal_eq)
   959 
   960 lemma Real_diff_less_omega: "Real r - x < \<omega>" by (cases x) auto
   961 
   962 subsubsection {* Numbers on @{typ pextreal} *}
   963 
   964 instantiation pextreal :: number
   965 begin
   966 definition [simp]: "number_of x = Real (number_of x)"
   967 instance proof qed
   968 end
   969 
   970 subsubsection {* Division on @{typ pextreal} *}
   971 
   972 instantiation pextreal :: inverse
   973 begin
   974 
   975 definition "inverse x = pextreal_case (\<lambda>x. if x = 0 then \<omega> else Real (inverse x)) 0 x"
   976 definition [simp]: "x / y = x * inverse (y :: pextreal)"
   977 
   978 instance proof qed
   979 end
   980 
   981 lemma pextreal_inverse[simp]:
   982   "inverse 0 = \<omega>"
   983   "inverse (Real x) = (if x \<le> 0 then \<omega> else Real (inverse x))"
   984   "inverse \<omega> = 0"
   985   "inverse (1::pextreal) = 1"
   986   "inverse (inverse x) = x"
   987   by (simp_all add: inverse_pextreal_def one_pextreal_def split: pextreal_case_split del: Real_1)
   988 
   989 lemma pextreal_inverse_le_eq:
   990   assumes "x \<noteq> 0" "x \<noteq> \<omega>"
   991   shows "y \<le> z / x \<longleftrightarrow> x * y \<le> (z :: pextreal)"
   992 proof -
   993   from assms obtain r where r: "x = Real r" "0 < r" by (cases x) auto
   994   { fix p q :: real assume "0 \<le> p" "0 \<le> q"
   995     have "p \<le> q * inverse r \<longleftrightarrow> p \<le> q / r" by (simp add: divide_inverse)
   996     also have "... \<longleftrightarrow> p * r \<le> q" using `0 < r` by (auto simp: field_simps)
   997     finally have "p \<le> q * inverse r \<longleftrightarrow> p * r \<le> q" . }
   998   with r show ?thesis
   999     by (cases y, cases z, auto simp: zero_le_mult_iff field_simps)
  1000 qed
  1001 
  1002 lemma inverse_antimono_strict:
  1003   fixes x y :: pextreal
  1004   assumes "x < y" shows "inverse y < inverse x"
  1005   using assms by (cases x, cases y) auto
  1006 
  1007 lemma inverse_antimono:
  1008   fixes x y :: pextreal
  1009   assumes "x \<le> y" shows "inverse y \<le> inverse x"
  1010   using assms by (cases x, cases y) auto
  1011 
  1012 lemma pextreal_inverse_\<omega>_iff[simp]: "inverse x = \<omega> \<longleftrightarrow> x = 0"
  1013   by (cases x) auto
  1014 
  1015 subsection "Infinite sum over @{typ pextreal}"
  1016 
  1017 text {*
  1018 
  1019 The infinite sum over @{typ pextreal} has the nice property that it is always
  1020 defined.
  1021 
  1022 *}
  1023 
  1024 definition psuminf :: "(nat \<Rightarrow> pextreal) \<Rightarrow> pextreal" (binder "\<Sum>\<^isub>\<infinity>" 10) where
  1025   "(\<Sum>\<^isub>\<infinity> x. f x) = (SUP n. \<Sum>i<n. f i)"
  1026 
  1027 subsubsection {* Equivalence between @{text "\<Sum> n. f n"} and @{text "\<Sum>\<^isub>\<infinity> n. f n"} *}
  1028 
  1029 lemma setsum_Real:
  1030   assumes "\<forall>x\<in>A. 0 \<le> f x"
  1031   shows "(\<Sum>x\<in>A. Real (f x)) = Real (\<Sum>x\<in>A. f x)"
  1032 proof (cases "finite A")
  1033   case True
  1034   thus ?thesis using assms
  1035   proof induct case (insert x s)
  1036     hence "0 \<le> setsum f s" apply-apply(rule setsum_nonneg) by auto
  1037     thus ?case using insert by auto
  1038   qed auto
  1039 qed simp
  1040 
  1041 lemma setsum_Real':
  1042   assumes "\<forall>x. 0 \<le> f x"
  1043   shows "(\<Sum>x\<in>A. Real (f x)) = Real (\<Sum>x\<in>A. f x)"
  1044   apply(rule setsum_Real) using assms by auto
  1045 
  1046 lemma setsum_\<omega>:
  1047   "(\<Sum>x\<in>P. f x) = \<omega> \<longleftrightarrow> (finite P \<and> (\<exists>i\<in>P. f i = \<omega>))"
  1048 proof safe
  1049   assume *: "setsum f P = \<omega>"
  1050   show "finite P"
  1051   proof (rule ccontr) assume "infinite P" with * show False by auto qed
  1052   show "\<exists>i\<in>P. f i = \<omega>"
  1053   proof (rule ccontr)
  1054     assume "\<not> ?thesis" hence "\<And>i. i\<in>P \<Longrightarrow> f i \<noteq> \<omega>" by auto
  1055     from `finite P` this have "setsum f P \<noteq> \<omega>"
  1056       by induct auto
  1057     with * show False by auto
  1058   qed
  1059 next
  1060   fix i assume "finite P" "i \<in> P" "f i = \<omega>"
  1061   thus "setsum f P = \<omega>"
  1062   proof induct
  1063     case (insert x A)
  1064     show ?case using insert by (cases "x = i") auto
  1065   qed simp
  1066 qed
  1067 
  1068 lemma real_of_pextreal_setsum:
  1069   assumes "\<And>x. x \<in> S \<Longrightarrow> f x \<noteq> \<omega>"
  1070   shows "(\<Sum>x\<in>S. real (f x)) = real (setsum f S)"
  1071 proof cases
  1072   assume "finite S"
  1073   from this assms show ?thesis
  1074     by induct (simp_all add: real_of_pextreal_add setsum_\<omega>)
  1075 qed simp
  1076 
  1077 lemma setsum_0:
  1078   fixes f :: "'a \<Rightarrow> pextreal" assumes "finite A"
  1079   shows "(\<Sum>x\<in>A. f x) = 0 \<longleftrightarrow> (\<forall>i\<in>A. f i = 0)"
  1080   using assms by induct auto
  1081 
  1082 lemma suminf_imp_psuminf:
  1083   assumes "f sums x" and "\<forall>n. 0 \<le> f n"
  1084   shows "(\<Sum>\<^isub>\<infinity> x. Real (f x)) = Real x"
  1085   unfolding psuminf_def setsum_Real'[OF assms(2)]
  1086 proof (rule SUP_eq_LIMSEQ[THEN iffD2])
  1087   show "mono (\<lambda>n. setsum f {..<n})" (is "mono ?S")
  1088     unfolding mono_iff_le_Suc using assms by simp
  1089 
  1090   { fix n show "0 \<le> ?S n"
  1091       using setsum_nonneg[of "{..<n}" f] assms by auto }
  1092 
  1093   thus "0 \<le> x" "?S ----> x"
  1094     using `f sums x` LIMSEQ_le_const
  1095     by (auto simp: atLeast0LessThan sums_def)
  1096 qed
  1097 
  1098 lemma psuminf_equality:
  1099   assumes "\<And>n. setsum f {..<n} \<le> x"
  1100   and "\<And>y. y \<noteq> \<omega> \<Longrightarrow> (\<And>n. setsum f {..<n} \<le> y) \<Longrightarrow> x \<le> y"
  1101   shows "psuminf f = x"
  1102   unfolding psuminf_def
  1103 proof (safe intro!: pextreal_SUPI)
  1104   fix n show "setsum f {..<n} \<le> x" using assms(1) .
  1105 next
  1106   fix y assume *: "\<forall>n. n \<in> UNIV \<longrightarrow> setsum f {..<n} \<le> y"
  1107   show "x \<le> y"
  1108   proof (cases "y = \<omega>")
  1109     assume "y \<noteq> \<omega>" from assms(2)[OF this] *
  1110     show "x \<le> y" by auto
  1111   qed simp
  1112 qed
  1113 
  1114 lemma psuminf_\<omega>:
  1115   assumes "f i = \<omega>"
  1116   shows "(\<Sum>\<^isub>\<infinity> x. f x) = \<omega>"
  1117 proof (rule psuminf_equality)
  1118   fix y assume *: "\<And>n. setsum f {..<n} \<le> y"
  1119   have "setsum f {..<Suc i} = \<omega>" 
  1120     using assms by (simp add: setsum_\<omega>)
  1121   thus "\<omega> \<le> y" using *[of "Suc i"] by auto
  1122 qed simp
  1123 
  1124 lemma psuminf_imp_suminf:
  1125   assumes "(\<Sum>\<^isub>\<infinity> x. f x) \<noteq> \<omega>"
  1126   shows "(\<lambda>x. real (f x)) sums real (\<Sum>\<^isub>\<infinity> x. f x)"
  1127 proof -
  1128   have "\<forall>i. \<exists>r. f i = Real r \<and> 0 \<le> r"
  1129   proof
  1130     fix i show "\<exists>r. f i = Real r \<and> 0 \<le> r" using psuminf_\<omega> assms by (cases "f i") auto
  1131   qed
  1132   from choice[OF this] obtain r where f: "f = (\<lambda>i. Real (r i))"
  1133     and pos: "\<forall>i. 0 \<le> r i"
  1134     by (auto simp: fun_eq_iff)
  1135   hence [simp]: "\<And>i. real (f i) = r i" by auto
  1136 
  1137   have "mono (\<lambda>n. setsum r {..<n})" (is "mono ?S")
  1138     unfolding mono_iff_le_Suc using pos by simp
  1139 
  1140   { fix n have "0 \<le> ?S n"
  1141       using setsum_nonneg[of "{..<n}" r] pos by auto }
  1142 
  1143   from assms obtain p where *: "(\<Sum>\<^isub>\<infinity> x. f x) = Real p" and "0 \<le> p"
  1144     by (cases "(\<Sum>\<^isub>\<infinity> x. f x)") auto
  1145   show ?thesis unfolding * using * pos `0 \<le> p` SUP_eq_LIMSEQ[OF `mono ?S` `\<And>n. 0 \<le> ?S n` `0 \<le> p`]
  1146     by (simp add: f atLeast0LessThan sums_def psuminf_def setsum_Real'[OF pos] f)
  1147 qed
  1148 
  1149 lemma psuminf_bound:
  1150   assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x"
  1151   shows "(\<Sum>\<^isub>\<infinity> n. f n) \<le> x"
  1152   using assms by (simp add: psuminf_def SUPR_def Sup_le_iff)
  1153 
  1154 lemma psuminf_bound_add:
  1155   assumes "\<forall>N. (\<Sum>n<N. f n) + y \<le> x"
  1156   shows "(\<Sum>\<^isub>\<infinity> n. f n) + y \<le> x"
  1157 proof (cases "x = \<omega>")
  1158   have "y \<le> x" using assms by (auto intro: pextreal_le_add2)
  1159   assume "x \<noteq> \<omega>"
  1160   note move_y = pextreal_less_eq_diff_eq_sum[OF `y \<le> x` this]
  1161 
  1162   have "\<forall>N. (\<Sum>n<N. f n) \<le> x - y" using assms by (simp add: move_y)
  1163   hence "(\<Sum>\<^isub>\<infinity> n. f n) \<le> x - y" by (rule psuminf_bound)
  1164   thus ?thesis by (simp add: move_y)
  1165 qed simp
  1166 
  1167 lemma psuminf_finite:
  1168   assumes "\<forall>N\<ge>n. f N = 0"
  1169   shows "(\<Sum>\<^isub>\<infinity> n. f n) = (\<Sum>N<n. f N)"
  1170 proof (rule psuminf_equality)
  1171   fix N
  1172   show "setsum f {..<N} \<le> setsum f {..<n}"
  1173   proof (cases rule: linorder_cases)
  1174     assume "N < n" thus ?thesis by (auto intro!: setsum_mono3)
  1175   next
  1176     assume "n < N"
  1177     hence *: "{..<N} = {..<n} \<union> {n..<N}" by auto
  1178     moreover have "setsum f {n..<N} = 0"
  1179       using assms by (auto intro!: setsum_0')
  1180     ultimately show ?thesis unfolding *
  1181       by (subst setsum_Un_disjoint) auto
  1182   qed simp
  1183 qed simp
  1184 
  1185 lemma psuminf_upper:
  1186   shows "(\<Sum>n<N. f n) \<le> (\<Sum>\<^isub>\<infinity> n. f n)"
  1187   unfolding psuminf_def SUPR_def
  1188   by (auto intro: complete_lattice_class.Sup_upper image_eqI)
  1189 
  1190 lemma psuminf_le:
  1191   assumes "\<And>N. f N \<le> g N"
  1192   shows "psuminf f \<le> psuminf g"
  1193 proof (safe intro!: psuminf_bound)
  1194   fix n
  1195   have "setsum f {..<n} \<le> setsum g {..<n}" using assms by (auto intro: setsum_mono)
  1196   also have "... \<le> psuminf g" by (rule psuminf_upper)
  1197   finally show "setsum f {..<n} \<le> psuminf g" .
  1198 qed
  1199 
  1200 lemma psuminf_const[simp]: "psuminf (\<lambda>n. c) = (if c = 0 then 0 else \<omega>)" (is "_ = ?if")
  1201 proof (rule psuminf_equality)
  1202   fix y assume *: "\<And>n :: nat. (\<Sum>n<n. c) \<le> y" and "y \<noteq> \<omega>"
  1203   then obtain r p where
  1204     y: "y = Real r" "0 \<le> r" and
  1205     c: "c = Real p" "0 \<le> p"
  1206       using *[of 1] by (cases c, cases y) auto
  1207   show "(if c = 0 then 0 else \<omega>) \<le> y"
  1208   proof (cases "p = 0")
  1209     assume "p = 0" with c show ?thesis by simp
  1210   next
  1211     assume "p \<noteq> 0"
  1212     with * c y have **: "\<And>n :: nat. real n \<le> r / p"
  1213       by (auto simp: zero_le_mult_iff field_simps)
  1214     from ex_less_of_nat[of "r / p"] guess n ..
  1215     with **[of n] show ?thesis by (simp add: real_eq_of_nat)
  1216   qed
  1217 qed (cases "c = 0", simp_all)
  1218 
  1219 lemma psuminf_add[simp]: "psuminf (\<lambda>n. f n + g n) = psuminf f + psuminf g"
  1220 proof (rule psuminf_equality)
  1221   fix n
  1222   from psuminf_upper[of f n] psuminf_upper[of g n]
  1223   show "(\<Sum>n<n. f n + g n) \<le> psuminf f + psuminf g"
  1224     by (auto simp add: setsum_addf intro!: add_mono)
  1225 next
  1226   fix y assume *: "\<And>n. (\<Sum>n<n. f n + g n) \<le> y" and "y \<noteq> \<omega>"
  1227   { fix n m
  1228     have **: "(\<Sum>n<n. f n) + (\<Sum>n<m. g n) \<le> y"
  1229     proof (cases rule: linorder_le_cases)
  1230       assume "n \<le> m"
  1231       hence "(\<Sum>n<n. f n) + (\<Sum>n<m. g n) \<le> (\<Sum>n<m. f n) + (\<Sum>n<m. g n)"
  1232         by (auto intro!: add_right_mono setsum_mono3)
  1233       also have "... \<le> y"
  1234         using * by (simp add: setsum_addf)
  1235       finally show ?thesis .
  1236     next
  1237       assume "m \<le> n"
  1238       hence "(\<Sum>n<n. f n) + (\<Sum>n<m. g n) \<le> (\<Sum>n<n. f n) + (\<Sum>n<n. g n)"
  1239         by (auto intro!: add_left_mono setsum_mono3)
  1240       also have "... \<le> y"
  1241         using * by (simp add: setsum_addf)
  1242       finally show ?thesis .
  1243     qed }
  1244   hence "\<And>m. \<forall>n. (\<Sum>n<n. f n) + (\<Sum>n<m. g n) \<le> y" by simp
  1245   from psuminf_bound_add[OF this]
  1246   have "\<forall>m. (\<Sum>n<m. g n) + psuminf f \<le> y" by (simp add: ac_simps)
  1247   from psuminf_bound_add[OF this]
  1248   show "psuminf f + psuminf g \<le> y" by (simp add: ac_simps)
  1249 qed
  1250 
  1251 lemma psuminf_0: "psuminf f = 0 \<longleftrightarrow> (\<forall>i. f i = 0)"
  1252 proof safe
  1253   assume "\<forall>i. f i = 0"
  1254   hence "f = (\<lambda>i. 0)" by (simp add: fun_eq_iff)
  1255   thus "psuminf f = 0" using psuminf_const by simp
  1256 next
  1257   fix i assume "psuminf f = 0"
  1258   hence "(\<Sum>n<Suc i. f n) = 0" using psuminf_upper[of f "Suc i"] by simp
  1259   thus "f i = 0" by simp
  1260 qed
  1261 
  1262 lemma psuminf_cmult_right[simp]: "psuminf (\<lambda>n. c * f n) = c * psuminf f"
  1263 proof (rule psuminf_equality)
  1264   fix n show "(\<Sum>n<n. c * f n) \<le> c * psuminf f"
  1265    by (auto simp: setsum_right_distrib[symmetric] intro: mult_left_mono psuminf_upper)
  1266 next
  1267   fix y
  1268   assume "\<And>n. (\<Sum>n<n. c * f n) \<le> y"
  1269   hence *: "\<And>n. c * (\<Sum>n<n. f n) \<le> y" by (auto simp add: setsum_right_distrib)
  1270   thus "c * psuminf f \<le> y"
  1271   proof (cases "c = \<omega> \<or> c = 0")
  1272     assume "c = \<omega> \<or> c = 0"
  1273     thus ?thesis
  1274       using * by (fastsimp simp add: psuminf_0 setsum_0 split: split_if_asm)
  1275   next
  1276     assume "\<not> (c = \<omega> \<or> c = 0)"
  1277     hence "c \<noteq> 0" "c \<noteq> \<omega>" by auto
  1278     note rewrite_div = pextreal_inverse_le_eq[OF this, of _ y]
  1279     hence "\<forall>n. (\<Sum>n<n. f n) \<le> y / c" using * by simp
  1280     hence "psuminf f \<le> y / c" by (rule psuminf_bound)
  1281     thus ?thesis using rewrite_div by simp
  1282   qed
  1283 qed
  1284 
  1285 lemma psuminf_cmult_left[simp]: "psuminf (\<lambda>n. f n * c) = psuminf f * c"
  1286   using psuminf_cmult_right[of c f] by (simp add: ac_simps)
  1287 
  1288 lemma psuminf_half_series: "psuminf (\<lambda>n. (1/2)^Suc n) = 1"
  1289   using suminf_imp_psuminf[OF power_half_series] by auto
  1290 
  1291 lemma setsum_pinfsum: "(\<Sum>\<^isub>\<infinity> n. \<Sum>m\<in>A. f n m) = (\<Sum>m\<in>A. (\<Sum>\<^isub>\<infinity> n. f n m))"
  1292 proof (cases "finite A")
  1293   assume "finite A"
  1294   thus ?thesis by induct simp_all
  1295 qed simp
  1296 
  1297 lemma psuminf_reindex:
  1298   fixes f:: "nat \<Rightarrow> nat" assumes "bij f"
  1299   shows "psuminf (g \<circ> f) = psuminf g"
  1300 proof -
  1301   have [intro, simp]: "\<And>A. inj_on f A" using `bij f` unfolding bij_def by (auto intro: subset_inj_on)
  1302   have f[intro, simp]: "\<And>x. f (inv f x) = x"
  1303     using `bij f` unfolding bij_def by (auto intro: surj_f_inv_f)
  1304   show ?thesis
  1305   proof (rule psuminf_equality)
  1306     fix n
  1307     have "setsum (g \<circ> f) {..<n} = setsum g (f ` {..<n})"
  1308       by (simp add: setsum_reindex)
  1309     also have "\<dots> \<le> setsum g {..Max (f ` {..<n})}"
  1310       by (rule setsum_mono3) auto
  1311     also have "\<dots> \<le> psuminf g" unfolding lessThan_Suc_atMost[symmetric] by (rule psuminf_upper)
  1312     finally show "setsum (g \<circ> f) {..<n} \<le> psuminf g" .
  1313   next
  1314     fix y assume *: "\<And>n. setsum (g \<circ> f) {..<n} \<le> y"
  1315     show "psuminf g \<le> y"
  1316     proof (safe intro!: psuminf_bound)
  1317       fix N
  1318       have "setsum g {..<N} \<le> setsum g (f ` {..Max (inv f ` {..<N})})"
  1319         by (rule setsum_mono3) (auto intro!: image_eqI[where f="f", OF f[symmetric]])
  1320       also have "\<dots> = setsum (g \<circ> f) {..Max (inv f ` {..<N})}"
  1321         by (simp add: setsum_reindex)
  1322       also have "\<dots> \<le> y" unfolding lessThan_Suc_atMost[symmetric] by (rule *)
  1323       finally show "setsum g {..<N} \<le> y" .
  1324     qed
  1325   qed
  1326 qed
  1327 
  1328 lemma pextreal_mult_less_right:
  1329   assumes "b * a < c * a" "0 < a" "a < \<omega>"
  1330   shows "b < c"
  1331   using assms
  1332   by (cases a, cases b, cases c) (auto split: split_if_asm simp: zero_less_mult_iff zero_le_mult_iff)
  1333 
  1334 lemma pextreal_\<omega>_eq_plus[simp]: "\<omega> = a + b \<longleftrightarrow> (a = \<omega> \<or> b = \<omega>)"
  1335   by (cases a, cases b) auto
  1336 
  1337 lemma pextreal_of_nat_le_iff:
  1338   "(of_nat k :: pextreal) \<le> of_nat m \<longleftrightarrow> k \<le> m" by auto
  1339 
  1340 lemma pextreal_of_nat_less_iff:
  1341   "(of_nat k :: pextreal) < of_nat m \<longleftrightarrow> k < m" by auto
  1342 
  1343 lemma pextreal_bound_add:
  1344   assumes "\<forall>N. f N + y \<le> (x::pextreal)"
  1345   shows "(SUP n. f n) + y \<le> x"
  1346 proof (cases "x = \<omega>")
  1347   have "y \<le> x" using assms by (auto intro: pextreal_le_add2)
  1348   assume "x \<noteq> \<omega>"
  1349   note move_y = pextreal_less_eq_diff_eq_sum[OF `y \<le> x` this]
  1350 
  1351   have "\<forall>N. f N \<le> x - y" using assms by (simp add: move_y)
  1352   hence "(SUP n. f n) \<le> x - y" by (rule SUPR_bound)
  1353   thus ?thesis by (simp add: move_y)
  1354 qed simp
  1355 
  1356 lemma SUPR_pextreal_add:
  1357   fixes f g :: "nat \<Rightarrow> pextreal"
  1358   assumes f: "\<forall>n. f n \<le> f (Suc n)" and g: "\<forall>n. g n \<le> g (Suc n)"
  1359   shows "(SUP n. f n + g n) = (SUP n. f n) + (SUP n. g n)"
  1360 proof (rule pextreal_SUPI)
  1361   fix n :: nat from le_SUPI[of n UNIV f] le_SUPI[of n UNIV g]
  1362   show "f n + g n \<le> (SUP n. f n) + (SUP n. g n)"
  1363     by (auto intro!: add_mono)
  1364 next
  1365   fix y assume *: "\<And>n. n \<in> UNIV \<Longrightarrow> f n + g n \<le> y"
  1366   { fix n m
  1367     have "f n + g m \<le> y"
  1368     proof (cases rule: linorder_le_cases)
  1369       assume "n \<le> m"
  1370       hence "f n + g m \<le> f m + g m"
  1371         using f lift_Suc_mono_le by (auto intro!: add_right_mono)
  1372       also have "\<dots> \<le> y" using * by simp
  1373       finally show ?thesis .
  1374     next
  1375       assume "m \<le> n"
  1376       hence "f n + g m \<le> f n + g n"
  1377         using g lift_Suc_mono_le by (auto intro!: add_left_mono)
  1378       also have "\<dots> \<le> y" using * by simp
  1379       finally show ?thesis .
  1380     qed }
  1381   hence "\<And>m. \<forall>n. f n + g m \<le> y" by simp
  1382   from pextreal_bound_add[OF this]
  1383   have "\<forall>m. (g m) + (SUP n. f n) \<le> y" by (simp add: ac_simps)
  1384   from pextreal_bound_add[OF this]
  1385   show "SUPR UNIV f + SUPR UNIV g \<le> y" by (simp add: ac_simps)
  1386 qed
  1387 
  1388 lemma SUPR_pextreal_setsum:
  1389   fixes f :: "'x \<Rightarrow> nat \<Rightarrow> pextreal"
  1390   assumes "\<And>i. i \<in> P \<Longrightarrow> \<forall>n. f i n \<le> f i (Suc n)"
  1391   shows "(SUP n. \<Sum>i\<in>P. f i n) = (\<Sum>i\<in>P. SUP n. f i n)"
  1392 proof cases
  1393   assume "finite P" from this assms show ?thesis
  1394   proof induct
  1395     case (insert i P)
  1396     thus ?case
  1397       apply simp
  1398       apply (subst SUPR_pextreal_add)
  1399       by (auto intro!: setsum_mono)
  1400   qed simp
  1401 qed simp
  1402 
  1403 lemma psuminf_SUP_eq:
  1404   assumes "\<And>n i. f n i \<le> f (Suc n) i"
  1405   shows "(\<Sum>\<^isub>\<infinity> i. SUP n::nat. f n i) = (SUP n::nat. \<Sum>\<^isub>\<infinity> i. f n i)"
  1406 proof -
  1407   { fix n :: nat
  1408     have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)"
  1409       using assms by (auto intro!: SUPR_pextreal_setsum[symmetric]) }
  1410   note * = this
  1411   show ?thesis
  1412     unfolding psuminf_def
  1413     unfolding *
  1414     apply (subst SUP_commute) ..
  1415 qed
  1416 
  1417 lemma psuminf_commute:
  1418   shows "(\<Sum>\<^isub>\<infinity> i j. f i j) = (\<Sum>\<^isub>\<infinity> j i. f i j)"
  1419 proof -
  1420   have "(SUP n. \<Sum> i < n. SUP m. \<Sum> j < m. f i j) = (SUP n. SUP m. \<Sum> i < n. \<Sum> j < m. f i j)"
  1421     apply (subst SUPR_pextreal_setsum)
  1422     by auto
  1423   also have "\<dots> = (SUP m n. \<Sum> j < m. \<Sum> i < n. f i j)"
  1424     apply (subst SUP_commute)
  1425     apply (subst setsum_commute)
  1426     by auto
  1427   also have "\<dots> = (SUP m. \<Sum> j < m. SUP n. \<Sum> i < n. f i j)"
  1428     apply (subst SUPR_pextreal_setsum)
  1429     by auto
  1430   finally show ?thesis
  1431     unfolding psuminf_def by auto
  1432 qed
  1433 
  1434 lemma psuminf_2dimen:
  1435   fixes f:: "nat * nat \<Rightarrow> pextreal"
  1436   assumes fsums: "\<And>m. g m = (\<Sum>\<^isub>\<infinity> n. f (m,n))"
  1437   shows "psuminf (f \<circ> prod_decode) = psuminf g"
  1438 proof (rule psuminf_equality)
  1439   fix n :: nat
  1440   let ?P = "prod_decode ` {..<n}"
  1441   have "setsum (f \<circ> prod_decode) {..<n} = setsum f ?P"
  1442     by (auto simp: setsum_reindex inj_prod_decode)
  1443   also have "\<dots> \<le> setsum f ({..Max (fst ` ?P)} \<times> {..Max (snd ` ?P)})"
  1444   proof (safe intro!: setsum_mono3 Max_ge image_eqI)
  1445     fix a b x assume "(a, b) = prod_decode x"
  1446     from this[symmetric] show "a = fst (prod_decode x)" "b = snd (prod_decode x)"
  1447       by simp_all
  1448   qed simp_all
  1449   also have "\<dots> = (\<Sum>m\<le>Max (fst ` ?P). (\<Sum>n\<le>Max (snd ` ?P). f (m,n)))"
  1450     unfolding setsum_cartesian_product by simp
  1451   also have "\<dots> \<le> (\<Sum>m\<le>Max (fst ` ?P). g m)"
  1452     by (auto intro!: setsum_mono psuminf_upper simp del: setsum_lessThan_Suc
  1453         simp: fsums lessThan_Suc_atMost[symmetric])
  1454   also have "\<dots> \<le> psuminf g"
  1455     by (auto intro!: psuminf_upper simp del: setsum_lessThan_Suc
  1456         simp: lessThan_Suc_atMost[symmetric])
  1457   finally show "setsum (f \<circ> prod_decode) {..<n} \<le> psuminf g" .
  1458 next
  1459   fix y assume *: "\<And>n. setsum (f \<circ> prod_decode) {..<n} \<le> y"
  1460   have g: "g = (\<lambda>m. \<Sum>\<^isub>\<infinity> n. f (m,n))" unfolding fsums[symmetric] ..
  1461   show "psuminf g \<le> y" unfolding g
  1462   proof (rule psuminf_bound, unfold setsum_pinfsum[symmetric], safe intro!: psuminf_bound)
  1463     fix N M :: nat
  1464     let ?P = "{..<N} \<times> {..<M}"
  1465     let ?M = "Max (prod_encode ` ?P)"
  1466     have "(\<Sum>n<M. \<Sum>m<N. f (m, n)) \<le> (\<Sum>(m, n)\<in>?P. f (m, n))"
  1467       unfolding setsum_commute[of _ _ "{..<M}"] unfolding setsum_cartesian_product ..
  1468     also have "\<dots> \<le> (\<Sum>(m,n)\<in>(prod_decode ` {..?M}). f (m, n))"
  1469       by (auto intro!: setsum_mono3 image_eqI[where f=prod_decode, OF prod_encode_inverse[symmetric]])
  1470     also have "\<dots> \<le> y" using *[of "Suc ?M"]
  1471       by (simp add: lessThan_Suc_atMost[symmetric] setsum_reindex
  1472                inj_prod_decode del: setsum_lessThan_Suc)
  1473     finally show "(\<Sum>n<M. \<Sum>m<N. f (m, n)) \<le> y" .
  1474   qed
  1475 qed
  1476 
  1477 lemma Real_max:
  1478   assumes "x \<ge> 0" "y \<ge> 0"
  1479   shows "Real (max x y) = max (Real x) (Real y)"
  1480   using assms unfolding max_def by (auto simp add:not_le)
  1481 
  1482 lemma Real_real: "Real (real x) = (if x = \<omega> then 0 else x)"
  1483   using assms by (cases x) auto
  1484 
  1485 lemma inj_on_real: "inj_on real (UNIV - {\<omega>})"
  1486 proof (rule inj_onI)
  1487   fix x y assume mem: "x \<in> UNIV - {\<omega>}" "y \<in> UNIV - {\<omega>}" and "real x = real y"
  1488   thus "x = y" by (cases x, cases y) auto
  1489 qed
  1490 
  1491 lemma inj_on_Real: "inj_on Real {0..}"
  1492   by (auto intro!: inj_onI)
  1493 
  1494 lemma range_Real[simp]: "range Real = UNIV - {\<omega>}"
  1495 proof safe
  1496   fix x assume "x \<notin> range Real"
  1497   thus "x = \<omega>" by (cases x) auto
  1498 qed auto
  1499 
  1500 lemma image_Real[simp]: "Real ` {0..} = UNIV - {\<omega>}"
  1501 proof safe
  1502   fix x assume "x \<notin> Real ` {0..}"
  1503   thus "x = \<omega>" by (cases x) auto
  1504 qed auto
  1505 
  1506 lemma pextreal_SUP_cmult:
  1507   fixes f :: "'a \<Rightarrow> pextreal"
  1508   shows "(SUP i : R. z * f i) = z * (SUP i : R. f i)"
  1509 proof (rule pextreal_SUPI)
  1510   fix i assume "i \<in> R"
  1511   from le_SUPI[OF this]
  1512   show "z * f i \<le> z * (SUP i:R. f i)" by (rule pextreal_mult_cancel)
  1513 next
  1514   fix y assume "\<And>i. i\<in>R \<Longrightarrow> z * f i \<le> y"
  1515   hence *: "\<And>i. i\<in>R \<Longrightarrow> z * f i \<le> y" by auto
  1516   show "z * (SUP i:R. f i) \<le> y"
  1517   proof (cases "\<forall>i\<in>R. f i = 0")
  1518     case True
  1519     show ?thesis
  1520     proof cases
  1521       assume "R \<noteq> {}" hence "f ` R = {0}" using True by auto
  1522       thus ?thesis by (simp add: SUPR_def)
  1523     qed (simp add: SUPR_def Sup_empty bot_pextreal_def)
  1524   next
  1525     case False then obtain i where i: "i \<in> R" and f0: "f i \<noteq> 0" by auto
  1526     show ?thesis
  1527     proof (cases "z = 0 \<or> z = \<omega>")
  1528       case True with f0 *[OF i] show ?thesis by auto
  1529     next
  1530       case False hence z: "z \<noteq> 0" "z \<noteq> \<omega>" by auto
  1531       note div = pextreal_inverse_le_eq[OF this, symmetric]
  1532       hence "\<And>i. i\<in>R \<Longrightarrow> f i \<le> y / z" using * by auto
  1533       thus ?thesis unfolding div SUP_le_iff by simp
  1534     qed
  1535   qed
  1536 qed
  1537 
  1538 instantiation pextreal :: topological_space
  1539 begin
  1540 
  1541 definition "open A \<longleftrightarrow>
  1542   (\<exists>T. open T \<and> (Real ` (T\<inter>{0..}) = A - {\<omega>})) \<and> (\<omega> \<in> A \<longrightarrow> (\<exists>x\<ge>0. {Real x <..} \<subseteq> A))"
  1543 
  1544 lemma open_omega: "open A \<Longrightarrow> \<omega> \<in> A \<Longrightarrow> (\<exists>x\<ge>0. {Real x<..} \<subseteq> A)"
  1545   unfolding open_pextreal_def by auto
  1546 
  1547 lemma open_omegaD: assumes "open A" "\<omega> \<in> A" obtains x where "x\<ge>0" "{Real x<..} \<subseteq> A"
  1548   using open_omega[OF assms] by auto
  1549 
  1550 lemma pextreal_openE: assumes "open A" obtains A' x where
  1551   "open A'" "Real ` (A' \<inter> {0..}) = A - {\<omega>}"
  1552   "x \<ge> 0" "\<omega> \<in> A \<Longrightarrow> {Real x<..} \<subseteq> A"
  1553   using assms open_pextreal_def by auto
  1554 
  1555 instance
  1556 proof
  1557   let ?U = "UNIV::pextreal set"
  1558   show "open ?U" unfolding open_pextreal_def
  1559     by (auto intro!: exI[of _ "UNIV"] exI[of _ 0])
  1560 next
  1561   fix S T::"pextreal set" assume "open S" and "open T"
  1562   from `open S`[THEN pextreal_openE] guess S' xS . note S' = this
  1563   from `open T`[THEN pextreal_openE] guess T' xT . note T' = this
  1564 
  1565   from S'(1-3) T'(1-3)
  1566   show "open (S \<inter> T)" unfolding open_pextreal_def
  1567   proof (safe intro!: exI[of _ "S' \<inter> T'"] exI[of _ "max xS xT"])
  1568     fix x assume *: "Real (max xS xT) < x" and "\<omega> \<in> S" "\<omega> \<in> T"
  1569     from `\<omega> \<in> S`[THEN S'(4)] * show "x \<in> S"
  1570       by (cases x, auto simp: max_def split: split_if_asm)
  1571     from `\<omega> \<in> T`[THEN T'(4)] * show "x \<in> T"
  1572       by (cases x, auto simp: max_def split: split_if_asm)
  1573   next
  1574     fix x assume x: "x \<notin> Real ` (S' \<inter> T' \<inter> {0..})"
  1575     have *: "S' \<inter> T' \<inter> {0..} = (S' \<inter> {0..}) \<inter> (T' \<inter> {0..})" by auto
  1576     assume "x \<in> T" "x \<in> S"
  1577     with S'(2) T'(2) show "x = \<omega>"
  1578       using x[unfolded *] inj_on_image_Int[OF inj_on_Real] by auto
  1579   qed auto
  1580 next
  1581   fix K assume openK: "\<forall>S \<in> K. open (S:: pextreal set)"
  1582   hence "\<forall>S\<in>K. \<exists>T. open T \<and> Real ` (T \<inter> {0..}) = S - {\<omega>}" by (auto simp: open_pextreal_def)
  1583   from bchoice[OF this] guess T .. note T = this[rule_format]
  1584 
  1585   show "open (\<Union>K)" unfolding open_pextreal_def
  1586   proof (safe intro!: exI[of _ "\<Union>(T ` K)"])
  1587     fix x S assume "0 \<le> x" "x \<in> T S" "S \<in> K"
  1588     with T[OF `S \<in> K`] show "Real x \<in> \<Union>K" by auto
  1589   next
  1590     fix x S assume x: "x \<notin> Real ` (\<Union>T ` K \<inter> {0..})" "S \<in> K" "x \<in> S"
  1591     hence "x \<notin> Real ` (T S \<inter> {0..})"
  1592       by (auto simp: image_UN UN_simps[symmetric] simp del: UN_simps)
  1593     thus "x = \<omega>" using T[OF `S \<in> K`] `x \<in> S` by auto
  1594   next
  1595     fix S assume "\<omega> \<in> S" "S \<in> K"
  1596     from openK[rule_format, OF `S \<in> K`, THEN pextreal_openE] guess S' x .
  1597     from this(3, 4) `\<omega> \<in> S`
  1598     show "\<exists>x\<ge>0. {Real x<..} \<subseteq> \<Union>K"
  1599       by (auto intro!: exI[of _ x] bexI[OF _ `S \<in> K`])
  1600   next
  1601     from T[THEN conjunct1] show "open (\<Union>T`K)" by auto
  1602   qed auto
  1603 qed
  1604 end
  1605 
  1606 lemma open_pextreal_lessThan[simp]:
  1607   "open {..< a :: pextreal}"
  1608 proof (cases a)
  1609   case (preal x) thus ?thesis unfolding open_pextreal_def
  1610   proof (safe intro!: exI[of _ "{..< x}"])
  1611     fix y assume "y < Real x"
  1612     moreover assume "y \<notin> Real ` ({..<x} \<inter> {0..})"
  1613     ultimately have "y \<noteq> Real (real y)" using preal by (cases y) auto
  1614     thus "y = \<omega>" by (auto simp: Real_real split: split_if_asm)
  1615   qed auto
  1616 next
  1617   case infinite thus ?thesis
  1618     unfolding open_pextreal_def by (auto intro!: exI[of _ UNIV])
  1619 qed
  1620 
  1621 lemma open_pextreal_greaterThan[simp]:
  1622   "open {a :: pextreal <..}"
  1623 proof (cases a)
  1624   case (preal x) thus ?thesis unfolding open_pextreal_def
  1625   proof (safe intro!: exI[of _ "{x <..}"])
  1626     fix y assume "Real x < y"
  1627     moreover assume "y \<notin> Real ` ({x<..} \<inter> {0..})"
  1628     ultimately have "y \<noteq> Real (real y)" using preal by (cases y) auto
  1629     thus "y = \<omega>" by (auto simp: Real_real split: split_if_asm)
  1630   qed auto
  1631 next
  1632   case infinite thus ?thesis
  1633     unfolding open_pextreal_def by (auto intro!: exI[of _ "{}"])
  1634 qed
  1635 
  1636 lemma pextreal_open_greaterThanLessThan[simp]: "open {a::pextreal <..< b}"
  1637   unfolding greaterThanLessThan_def by auto
  1638 
  1639 lemma closed_pextreal_atLeast[simp, intro]: "closed {a :: pextreal ..}"
  1640 proof -
  1641   have "- {a ..} = {..< a}" by auto
  1642   then show "closed {a ..}"
  1643     unfolding closed_def using open_pextreal_lessThan by auto
  1644 qed
  1645 
  1646 lemma closed_pextreal_atMost[simp, intro]: "closed {.. b :: pextreal}"
  1647 proof -
  1648   have "- {.. b} = {b <..}" by auto
  1649   then show "closed {.. b}" 
  1650     unfolding closed_def using open_pextreal_greaterThan by auto
  1651 qed
  1652 
  1653 lemma closed_pextreal_atLeastAtMost[simp, intro]:
  1654   shows "closed {a :: pextreal .. b}"
  1655   unfolding atLeastAtMost_def by auto
  1656 
  1657 lemma pextreal_dense:
  1658   fixes x y :: pextreal assumes "x < y"
  1659   shows "\<exists>z. x < z \<and> z < y"
  1660 proof -
  1661   from `x < y` obtain p where p: "x = Real p" "0 \<le> p" by (cases x) auto
  1662   show ?thesis
  1663   proof (cases y)
  1664     case (preal r) with p `x < y` have "p < r" by auto
  1665     with dense obtain z where "p < z" "z < r" by auto
  1666     thus ?thesis using preal p by (auto intro!: exI[of _ "Real z"])
  1667   next
  1668     case infinite thus ?thesis using `x < y` p
  1669       by (auto intro!: exI[of _ "Real p + 1"])
  1670   qed
  1671 qed
  1672 
  1673 instance pextreal :: t2_space
  1674 proof
  1675   fix x y :: pextreal assume "x \<noteq> y"
  1676   let "?P x (y::pextreal)" = "\<exists> U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
  1677 
  1678   { fix x y :: pextreal assume "x < y"
  1679     from pextreal_dense[OF this] obtain z where z: "x < z" "z < y" by auto
  1680     have "?P x y"
  1681       apply (rule exI[of _ "{..<z}"])
  1682       apply (rule exI[of _ "{z<..}"])
  1683       using z by auto }
  1684   note * = this
  1685 
  1686   from `x \<noteq> y`
  1687   show "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
  1688   proof (cases rule: linorder_cases)
  1689     assume "x = y" with `x \<noteq> y` show ?thesis by simp
  1690   next assume "x < y" from *[OF this] show ?thesis by auto
  1691   next assume "y < x" from *[OF this] show ?thesis by auto
  1692   qed
  1693 qed
  1694 
  1695 definition (in complete_lattice) isoton :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<up>" 50) where
  1696   "A \<up> X \<longleftrightarrow> (\<forall>i. A i \<le> A (Suc i)) \<and> (SUP i. A i) = X"
  1697 
  1698 definition (in complete_lattice) antiton (infix "\<down>" 50) where
  1699   "A \<down> X \<longleftrightarrow> (\<forall>i. A i \<ge> A (Suc i)) \<and> (INF i. A i) = X"
  1700 
  1701 lemma isotoneI[intro?]: "\<lbrakk> \<And>i. f i \<le> f (Suc i) ; (SUP i. f i) = F \<rbrakk> \<Longrightarrow> f \<up> F"
  1702   unfolding isoton_def by auto
  1703 
  1704 lemma (in complete_lattice) isotonD[dest]:
  1705   assumes "A \<up> X" shows "A i \<le> A (Suc i)" "(SUP i. A i) = X"
  1706   using assms unfolding isoton_def by auto
  1707 
  1708 lemma isotonD'[dest]:
  1709   assumes "(A::_=>_) \<up> X" shows "A i x \<le> A (Suc i) x" "(SUP i. A i) = X"
  1710   using assms unfolding isoton_def le_fun_def by auto
  1711 
  1712 lemma isoton_mono_le:
  1713   assumes "f \<up> x" "i \<le> j"
  1714   shows "f i \<le> f j"
  1715   using `f \<up> x`[THEN isotonD(1)] lift_Suc_mono_le[of f, OF _ `i \<le> j`] by auto
  1716 
  1717 lemma isoton_const:
  1718   shows "(\<lambda> i. c) \<up> c"
  1719 unfolding isoton_def by auto
  1720 
  1721 lemma isoton_cmult_right:
  1722   assumes "f \<up> (x::pextreal)"
  1723   shows "(\<lambda>i. c * f i) \<up> (c * x)"
  1724   using assms unfolding isoton_def pextreal_SUP_cmult
  1725   by (auto intro: pextreal_mult_cancel)
  1726 
  1727 lemma isoton_cmult_left:
  1728   "f \<up> (x::pextreal) \<Longrightarrow> (\<lambda>i. f i * c) \<up> (x * c)"
  1729   by (subst (1 2) mult_commute) (rule isoton_cmult_right)
  1730 
  1731 lemma isoton_add:
  1732   assumes "f \<up> (x::pextreal)" and "g \<up> y"
  1733   shows "(\<lambda>i. f i + g i) \<up> (x + y)"
  1734   using assms unfolding isoton_def
  1735   by (auto intro: pextreal_mult_cancel add_mono simp: SUPR_pextreal_add)
  1736 
  1737 lemma isoton_fun_expand:
  1738   "f \<up> x \<longleftrightarrow> (\<forall>i. (\<lambda>j. f j i) \<up> (x i))"
  1739 proof -
  1740   have "\<And>i. {y. \<exists>f'\<in>range f. y = f' i} = range (\<lambda>j. f j i)"
  1741     by auto
  1742   with assms show ?thesis
  1743     by (auto simp add: isoton_def le_fun_def Sup_fun_def SUPR_def)
  1744 qed
  1745 
  1746 lemma isoton_indicator:
  1747   assumes "f \<up> g"
  1748   shows "(\<lambda>i x. f i x * indicator A x) \<up> (\<lambda>x. g x * indicator A x :: pextreal)"
  1749   using assms unfolding isoton_fun_expand by (auto intro!: isoton_cmult_left)
  1750 
  1751 lemma isoton_setsum:
  1752   fixes f :: "'a \<Rightarrow> nat \<Rightarrow> pextreal"
  1753   assumes "finite A" "A \<noteq> {}"
  1754   assumes "\<And> x. x \<in> A \<Longrightarrow> f x \<up> y x"
  1755   shows "(\<lambda> i. (\<Sum> x \<in> A. f x i)) \<up> (\<Sum> x \<in> A. y x)"
  1756 using assms
  1757 proof (induct A rule:finite_ne_induct)
  1758   case singleton thus ?case by auto
  1759 next
  1760   case (insert a A) note asms = this
  1761   hence *: "(\<lambda> i. \<Sum> x \<in> A. f x i) \<up> (\<Sum> x \<in> A. y x)" by auto
  1762   have **: "(\<lambda> i. f a i) \<up> y a" using asms by simp
  1763   have "(\<lambda> i. f a i + (\<Sum> x \<in> A. f x i)) \<up> (y a + (\<Sum> x \<in> A. y x))"
  1764     using * ** isoton_add by auto
  1765   thus "(\<lambda> i. \<Sum> x \<in> insert a A. f x i) \<up> (\<Sum> x \<in> insert a A. y x)"
  1766     using asms by fastsimp
  1767 qed
  1768 
  1769 lemma isoton_Sup:
  1770   assumes "f \<up> u"
  1771   shows "f i \<le> u"
  1772   using le_SUPI[of i UNIV f] assms
  1773   unfolding isoton_def by auto
  1774 
  1775 lemma isoton_mono:
  1776   assumes iso: "x \<up> a" "y \<up> b" and *: "\<And>n. x n \<le> y (N n)"
  1777   shows "a \<le> b"
  1778 proof -
  1779   from iso have "a = (SUP n. x n)" "b = (SUP n. y n)"
  1780     unfolding isoton_def by auto
  1781   with * show ?thesis by (auto intro!: SUP_mono)
  1782 qed
  1783 
  1784 lemma pextreal_le_mult_one_interval:
  1785   fixes x y :: pextreal
  1786   assumes "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
  1787   shows "x \<le> y"
  1788 proof (cases x, cases y)
  1789   assume "x = \<omega>"
  1790   with assms[of "1 / 2"]
  1791   show "x \<le> y" by simp
  1792 next
  1793   fix r p assume *: "y = Real p" "x = Real r" and **: "0 \<le> r" "0 \<le> p"
  1794   have "r \<le> p"
  1795   proof (rule field_le_mult_one_interval)
  1796     fix z :: real assume "0 < z" and "z < 1"
  1797     with assms[of "Real z"]
  1798     show "z * r \<le> p" using ** * by (auto simp: zero_le_mult_iff)
  1799   qed
  1800   thus "x \<le> y" using ** * by simp
  1801 qed simp
  1802 
  1803 lemma pextreal_greater_0[intro]:
  1804   fixes a :: pextreal
  1805   assumes "a \<noteq> 0"
  1806   shows "a > 0"
  1807 using assms apply (cases a) by auto
  1808 
  1809 lemma pextreal_mult_strict_right_mono:
  1810   assumes "a < b" and "0 < c" "c < \<omega>"
  1811   shows "a * c < b * c"
  1812   using assms
  1813   by (cases a, cases b, cases c)
  1814      (auto simp: zero_le_mult_iff pextreal_less_\<omega>)
  1815 
  1816 lemma minus_pextreal_eq2:
  1817   fixes x y z :: pextreal
  1818   assumes "y \<le> x" and "y \<noteq> \<omega>" shows "z = x - y \<longleftrightarrow> z + y = x"
  1819   using assms
  1820   apply (subst eq_commute)
  1821   apply (subst minus_pextreal_eq)
  1822   by (cases x, cases z, auto simp add: ac_simps not_less)
  1823 
  1824 lemma pextreal_diff_eq_diff_imp_eq:
  1825   assumes "a \<noteq> \<omega>" "b \<le> a" "c \<le> a"
  1826   assumes "a - b = a - c"
  1827   shows "b = c"
  1828   using assms
  1829   by (cases a, cases b, cases c) (auto split: split_if_asm)
  1830 
  1831 lemma pextreal_inverse_eq_0: "inverse x = 0 \<longleftrightarrow> x = \<omega>"
  1832   by (cases x) auto
  1833 
  1834 lemma pextreal_mult_inverse:
  1835   "\<lbrakk> x \<noteq> \<omega> ; x \<noteq> 0 \<rbrakk> \<Longrightarrow> x * inverse x = 1"
  1836   by (cases x) auto
  1837 
  1838 lemma pextreal_zero_less_diff_iff:
  1839   fixes a b :: pextreal shows "0 < a - b \<longleftrightarrow> b < a"
  1840   apply (cases a, cases b)
  1841   apply (auto simp: pextreal_noteq_omega_Ex pextreal_less_\<omega>)
  1842   apply (cases b)
  1843   by auto
  1844 
  1845 lemma pextreal_less_Real_Ex:
  1846   fixes a b :: pextreal shows "x < Real r \<longleftrightarrow> (\<exists>p\<ge>0. p < r \<and> x = Real p)"
  1847   by (cases x) auto
  1848 
  1849 lemma open_Real: assumes "open S" shows "open (Real ` ({0..} \<inter> S))"
  1850   unfolding open_pextreal_def apply(rule,rule,rule,rule assms) by auto
  1851 
  1852 lemma pextreal_zero_le_diff:
  1853   fixes a b :: pextreal shows "a - b = 0 \<longleftrightarrow> a \<le> b"
  1854   by (cases a, cases b, simp_all, cases b, auto)
  1855 
  1856 lemma lim_Real[simp]: assumes "\<forall>n. f n \<ge> 0" "m\<ge>0"
  1857   shows "(\<lambda>n. Real (f n)) ----> Real m \<longleftrightarrow> (\<lambda>n. f n) ----> m" (is "?l = ?r")
  1858 proof assume ?l show ?r unfolding Lim_sequentially
  1859   proof safe fix e::real assume e:"e>0"
  1860     note open_ball[of m e] note open_Real[OF this]
  1861     note * = `?l`[unfolded tendsto_def,rule_format,OF this]
  1862     have "eventually (\<lambda>x. Real (f x) \<in> Real ` ({0..} \<inter> ball m e)) sequentially"
  1863       apply(rule *) unfolding image_iff using assms(2) e by auto
  1864     thus "\<exists>N. \<forall>n\<ge>N. dist (f n) m < e" unfolding eventually_sequentially 
  1865       apply safe apply(rule_tac x=N in exI,safe) apply(erule_tac x=n in allE,safe)
  1866     proof- fix n x assume "Real (f n) = Real x" "0 \<le> x"
  1867       hence *:"f n = x" using assms(1) by auto
  1868       assume "x \<in> ball m e" thus "dist (f n) m < e" unfolding *
  1869         by (auto simp add:dist_commute)
  1870     qed qed
  1871 next assume ?r show ?l unfolding tendsto_def eventually_sequentially 
  1872   proof safe fix S assume S:"open S" "Real m \<in> S"
  1873     guess T y using S(1) apply-apply(erule pextreal_openE) . note T=this
  1874     have "m\<in>real ` (S - {\<omega>})" unfolding image_iff 
  1875       apply(rule_tac x="Real m" in bexI) using assms(2) S(2) by auto
  1876     hence "m \<in> T" unfolding T(2)[THEN sym] by auto 
  1877     from `?r`[unfolded tendsto_def eventually_sequentially,rule_format,OF T(1) this]
  1878     guess N .. note N=this[rule_format]
  1879     show "\<exists>N. \<forall>n\<ge>N. Real (f n) \<in> S" apply(rule_tac x=N in exI) 
  1880     proof safe fix n assume n:"N\<le>n"
  1881       have "f n \<in> real ` (S - {\<omega>})" using N[OF n] assms unfolding T(2)[THEN sym] 
  1882         unfolding image_iff apply-apply(rule_tac x="Real (f n)" in bexI)
  1883         unfolding real_Real by auto
  1884       then guess x unfolding image_iff .. note x=this
  1885       show "Real (f n) \<in> S" unfolding x apply(subst Real_real) using x by auto
  1886     qed
  1887   qed
  1888 qed
  1889 
  1890 lemma pextreal_INFI:
  1891   fixes x :: pextreal
  1892   assumes "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i"
  1893   assumes "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> f i) \<Longrightarrow> y \<le> x"
  1894   shows "(INF i:A. f i) = x"
  1895   unfolding INFI_def Inf_pextreal_def
  1896   using assms by (auto intro!: Greatest_equality)
  1897 
  1898 lemma real_of_pextreal_less:"x < y \<Longrightarrow> y\<noteq>\<omega> \<Longrightarrow> real x < real y"
  1899 proof- case goal1
  1900   have *:"y = Real (real y)" "x = Real (real x)" using goal1 Real_real by auto
  1901   show ?case using goal1 apply- apply(subst(asm) *(1))apply(subst(asm) *(2))
  1902     unfolding pextreal_less by auto
  1903 qed
  1904 
  1905 lemma not_less_omega[simp]:"\<not> x < \<omega> \<longleftrightarrow> x = \<omega>"
  1906   by (metis antisym_conv3 pextreal_less(3)) 
  1907 
  1908 lemma Real_real': assumes "x\<noteq>\<omega>" shows "Real (real x) = x"
  1909 proof- have *:"(THE r. 0 \<le> r \<and> x = Real r) = real x"
  1910     apply(rule the_equality) using assms unfolding Real_real by auto
  1911   have "Real (THE r. 0 \<le> r \<and> x = Real r) = x" unfolding *
  1912     using assms unfolding Real_real by auto
  1913   thus ?thesis unfolding real_of_pextreal_def of_pextreal_def
  1914     unfolding pextreal_case_def using assms by auto
  1915 qed 
  1916 
  1917 lemma Real_less_plus_one:"Real x < Real (max (x + 1) 1)" 
  1918   unfolding pextreal_less by auto
  1919 
  1920 lemma Lim_omega: "f ----> \<omega> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. f n \<ge> Real B)" (is "?l = ?r")
  1921 proof assume ?r show ?l apply(rule topological_tendstoI)
  1922     unfolding eventually_sequentially
  1923   proof- fix S assume "open S" "\<omega> \<in> S"
  1924     from open_omega[OF this] guess B .. note B=this
  1925     from `?r`[rule_format,of "(max B 0)+1"] guess N .. note N=this
  1926     show "\<exists>N. \<forall>n\<ge>N. f n \<in> S" apply(rule_tac x=N in exI)
  1927     proof safe case goal1 
  1928       have "Real B < Real ((max B 0) + 1)" by auto
  1929       also have "... \<le> f n" using goal1 N by auto
  1930       finally show ?case using B by fastsimp
  1931     qed
  1932   qed
  1933 next assume ?l show ?r
  1934   proof fix B::real have "open {Real B<..}" "\<omega> \<in> {Real B<..}" by auto
  1935     from topological_tendstoD[OF `?l` this,unfolded eventually_sequentially]
  1936     guess N .. note N=this
  1937     show "\<exists>N. \<forall>n\<ge>N. Real B \<le> f n" apply(rule_tac x=N in exI) using N by auto
  1938   qed
  1939 qed
  1940 
  1941 lemma Lim_bounded_omgea: assumes lim:"f ----> l" and "\<And>n. f n \<le> Real B" shows "l \<noteq> \<omega>"
  1942 proof(rule ccontr,unfold not_not) let ?B = "max (B + 1) 1" assume as:"l=\<omega>"
  1943   from lim[unfolded this Lim_omega,rule_format,of "?B"]
  1944   guess N .. note N=this[rule_format,OF le_refl]
  1945   hence "Real ?B \<le> Real B" using assms(2)[of N] by(rule order_trans) 
  1946   hence "Real ?B < Real ?B" using Real_less_plus_one[of B] by(rule le_less_trans)
  1947   thus False by auto
  1948 qed
  1949 
  1950 lemma incseq_le_pextreal: assumes inc: "\<And>n m. n\<ge>m \<Longrightarrow> X n \<ge> X m"
  1951   and lim: "X ----> (L::pextreal)" shows "X n \<le> L"
  1952 proof(cases "L = \<omega>")
  1953   case False have "\<forall>n. X n \<noteq> \<omega>"
  1954   proof(rule ccontr,unfold not_all not_not,safe)
  1955     case goal1 hence "\<forall>n\<ge>x. X n = \<omega>" using inc[of x] by auto
  1956     hence "X ----> \<omega>" unfolding tendsto_def eventually_sequentially
  1957       apply safe apply(rule_tac x=x in exI) by auto
  1958     note Lim_unique[OF trivial_limit_sequentially this lim]
  1959     with False show False by auto
  1960   qed note * =this[rule_format]
  1961 
  1962   have **:"\<forall>m n. m \<le> n \<longrightarrow> Real (real (X m)) \<le> Real (real (X n))"
  1963     unfolding Real_real using * inc by auto
  1964   have "real (X n) \<le> real L" apply-apply(rule incseq_le) defer
  1965     apply(subst lim_Real[THEN sym]) apply(rule,rule,rule)
  1966     unfolding Real_real'[OF *] Real_real'[OF False] 
  1967     unfolding incseq_def using ** lim by auto
  1968   hence "Real (real (X n)) \<le> Real (real L)" by auto
  1969   thus ?thesis unfolding Real_real using * False by auto
  1970 qed auto
  1971 
  1972 lemma SUP_Lim_pextreal: assumes "\<And>n m. n\<ge>m \<Longrightarrow> f n \<ge> f m" "f ----> l"
  1973   shows "(SUP n. f n) = (l::pextreal)" unfolding SUPR_def Sup_pextreal_def
  1974 proof (safe intro!: Least_equality)
  1975   fix n::nat show "f n \<le> l" apply(rule incseq_le_pextreal)
  1976     using assms by auto
  1977 next fix y assume y:"\<forall>x\<in>range f. x \<le> y" show "l \<le> y"
  1978   proof(rule ccontr,cases "y=\<omega>",unfold not_le)
  1979     case False assume as:"y < l"
  1980     have l:"l \<noteq> \<omega>" apply(rule Lim_bounded_omgea[OF assms(2), of "real y"])
  1981       using False y unfolding Real_real by auto
  1982 
  1983     have yl:"real y < real l" using as apply-
  1984       apply(subst(asm) Real_real'[THEN sym,OF `y\<noteq>\<omega>`])
  1985       apply(subst(asm) Real_real'[THEN sym,OF `l\<noteq>\<omega>`]) 
  1986       unfolding pextreal_less apply(subst(asm) if_P) by auto
  1987     hence "y + (y - l) * Real (1 / 2) < l" apply-
  1988       apply(subst Real_real'[THEN sym,OF `y\<noteq>\<omega>`]) apply(subst(2) Real_real'[THEN sym,OF `y\<noteq>\<omega>`])
  1989       apply(subst Real_real'[THEN sym,OF `l\<noteq>\<omega>`]) apply(subst(2) Real_real'[THEN sym,OF `l\<noteq>\<omega>`]) by auto
  1990     hence *:"l \<in> {y + (y - l) / 2<..}" by auto
  1991     have "open {y + (y-l)/2 <..}" by auto
  1992     note topological_tendstoD[OF assms(2) this *]
  1993     from this[unfolded eventually_sequentially] guess N .. note this[rule_format, of N]
  1994     hence "y + (y - l) * Real (1 / 2) < y" using y[rule_format,of "f N"] by auto
  1995     hence "Real (real y) + (Real (real y) - Real (real l)) * Real (1 / 2) < Real (real y)"
  1996       unfolding Real_real using `y\<noteq>\<omega>` `l\<noteq>\<omega>` by auto
  1997     thus False using yl by auto
  1998   qed auto
  1999 qed
  2000 
  2001 lemma Real_max':"Real x = Real (max x 0)" 
  2002 proof(cases "x < 0") case True
  2003   hence *:"max x 0 = 0" by auto
  2004   show ?thesis unfolding * using True by auto
  2005 qed auto
  2006 
  2007 lemma lim_pextreal_increasing: assumes "\<forall>n m. n\<ge>m \<longrightarrow> f n \<ge> f m"
  2008   obtains l where "f ----> (l::pextreal)"
  2009 proof(cases "\<exists>B. \<forall>n. f n < Real B")
  2010   case False thus thesis apply- apply(rule that[of \<omega>]) unfolding Lim_omega not_ex not_all
  2011     apply safe apply(erule_tac x=B in allE,safe) apply(rule_tac x=x in exI,safe)
  2012     apply(rule order_trans[OF _ assms[rule_format]]) by auto
  2013 next case True then guess B .. note B = this[rule_format]
  2014   hence *:"\<And>n. f n < \<omega>" apply-apply(rule less_le_trans,assumption) by auto
  2015   have *:"\<And>n. f n \<noteq> \<omega>" proof- case goal1 show ?case using *[of n] by auto qed
  2016   have B':"\<And>n. real (f n) \<le> max 0 B" proof- case goal1 thus ?case
  2017       using B[of n] apply-apply(subst(asm) Real_real'[THEN sym]) defer
  2018       apply(subst(asm)(2) Real_max') unfolding pextreal_less apply(subst(asm) if_P) using *[of n] by auto
  2019   qed
  2020   have "\<exists>l. (\<lambda>n. real (f n)) ----> l" apply(rule Topology_Euclidean_Space.bounded_increasing_convergent)
  2021   proof safe show "bounded {real (f n) |n. True}"
  2022       unfolding bounded_def apply(rule_tac x=0 in exI,rule_tac x="max 0 B" in exI)
  2023       using B' unfolding dist_norm by auto
  2024     fix n::nat have "Real (real (f n)) \<le> Real (real (f (Suc n)))"
  2025       using assms[rule_format,of n "Suc n"] apply(subst Real_real)+
  2026       using *[of n] *[of "Suc n"] by fastsimp
  2027     thus "real (f n) \<le> real (f (Suc n))" by auto
  2028   qed then guess l .. note l=this
  2029   have "0 \<le> l" apply(rule LIMSEQ_le_const[OF l])
  2030     by(rule_tac x=0 in exI,auto)
  2031 
  2032   thus ?thesis apply-apply(rule that[of "Real l"])
  2033     using l apply-apply(subst(asm) lim_Real[THEN sym]) prefer 3
  2034     unfolding Real_real using * by auto
  2035 qed
  2036 
  2037 lemma setsum_neq_omega: assumes "finite s" "\<And>x. x \<in> s \<Longrightarrow> f x \<noteq> \<omega>"
  2038   shows "setsum f s \<noteq> \<omega>" using assms
  2039 proof induct case (insert x s)
  2040   show ?case unfolding setsum.insert[OF insert(1-2)] 
  2041     using insert by auto
  2042 qed auto
  2043 
  2044 
  2045 lemma real_Real': "0 \<le> x \<Longrightarrow> real (Real x) = x"
  2046   unfolding real_Real by auto
  2047 
  2048 lemma real_pextreal_pos[intro]:
  2049   assumes "x \<noteq> 0" "x \<noteq> \<omega>"
  2050   shows "real x > 0"
  2051   apply(subst real_Real'[THEN sym,of 0]) defer
  2052   apply(rule real_of_pextreal_less) using assms by auto
  2053 
  2054 lemma Lim_omega_gt: "f ----> \<omega> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. f n > Real B)" (is "?l = ?r")
  2055 proof assume ?l thus ?r unfolding Lim_omega apply safe
  2056     apply(erule_tac x="max B 0 +1" in allE,safe)
  2057     apply(rule_tac x=N in exI,safe) apply(erule_tac x=n in allE,safe)
  2058     apply(rule_tac y="Real (max B 0 + 1)" in less_le_trans) by auto
  2059 next assume ?r thus ?l unfolding Lim_omega apply safe
  2060     apply(erule_tac x=B in allE,safe) apply(rule_tac x=N in exI,safe) by auto
  2061 qed
  2062 
  2063 lemma pextreal_minus_le_cancel:
  2064   fixes a b c :: pextreal
  2065   assumes "b \<le> a"
  2066   shows "c - a \<le> c - b"
  2067   using assms by (cases a, cases b, cases c, simp, simp, simp, cases b, cases c, simp_all)
  2068 
  2069 lemma pextreal_minus_\<omega>[simp]: "x - \<omega> = 0" by (cases x) simp_all
  2070 
  2071 lemma pextreal_minus_mono[intro]: "a - x \<le> (a::pextreal)"
  2072 proof- have "a - x \<le> a - 0"
  2073     apply(rule pextreal_minus_le_cancel) by auto
  2074   thus ?thesis by auto
  2075 qed
  2076 
  2077 lemma pextreal_minus_eq_\<omega>[simp]: "x - y = \<omega> \<longleftrightarrow> (x = \<omega> \<and> y \<noteq> \<omega>)"
  2078   by (cases x, cases y) (auto, cases y, auto)
  2079 
  2080 lemma pextreal_less_minus_iff:
  2081   fixes a b c :: pextreal
  2082   shows "a < b - c \<longleftrightarrow> c + a < b"
  2083   by (cases c, cases a, cases b, auto)
  2084 
  2085 lemma pextreal_minus_less_iff:
  2086   fixes a b c :: pextreal shows "a - c < b \<longleftrightarrow> (0 < b \<and> (c \<noteq> \<omega> \<longrightarrow> a < b + c))"
  2087   by (cases c, cases a, cases b, auto)
  2088 
  2089 lemma pextreal_le_minus_iff:
  2090   fixes a b c :: pextreal
  2091   shows "a \<le> c - b \<longleftrightarrow> ((c \<le> b \<longrightarrow> a = 0) \<and> (b < c \<longrightarrow> a + b \<le> c))"
  2092   by (cases a, cases c, cases b, auto simp: pextreal_noteq_omega_Ex)
  2093 
  2094 lemma pextreal_minus_le_iff:
  2095   fixes a b c :: pextreal
  2096   shows "a - c \<le> b \<longleftrightarrow> (c \<le> a \<longrightarrow> a \<le> b + c)"
  2097   by (cases a, cases c, cases b, auto simp: pextreal_noteq_omega_Ex)
  2098 
  2099 lemmas pextreal_minus_order = pextreal_minus_le_iff pextreal_minus_less_iff pextreal_le_minus_iff pextreal_less_minus_iff
  2100 
  2101 lemma pextreal_minus_strict_mono:
  2102   assumes "a > 0" "x > 0" "a\<noteq>\<omega>"
  2103   shows "a - x < (a::pextreal)"
  2104   using assms by(cases x, cases a, auto)
  2105 
  2106 lemma pextreal_minus':
  2107   "Real r - Real p = (if 0 \<le> r \<and> p \<le> r then if 0 \<le> p then Real (r - p) else Real r else 0)"
  2108   by (auto simp: minus_pextreal_eq not_less)
  2109 
  2110 lemma pextreal_minus_plus:
  2111   "x \<le> (a::pextreal) \<Longrightarrow> a - x + x = a"
  2112   by (cases a, cases x) auto
  2113 
  2114 lemma pextreal_cancel_plus_minus: "b \<noteq> \<omega> \<Longrightarrow> a + b - b = a"
  2115   by (cases a, cases b) auto
  2116 
  2117 lemma pextreal_minus_le_cancel_right:
  2118   fixes a b c :: pextreal
  2119   assumes "a \<le> b" "c \<le> a"
  2120   shows "a - c \<le> b - c"
  2121   using assms by (cases a, cases b, cases c, auto, cases c, auto)
  2122 
  2123 lemma real_of_pextreal_setsum':
  2124   assumes "\<forall>x \<in> S. f x \<noteq> \<omega>"
  2125   shows "(\<Sum>x\<in>S. real (f x)) = real (setsum f S)"
  2126 proof cases
  2127   assume "finite S"
  2128   from this assms show ?thesis
  2129     by induct (simp_all add: real_of_pextreal_add setsum_\<omega>)
  2130 qed simp
  2131 
  2132 lemma Lim_omega_pos: "f ----> \<omega> \<longleftrightarrow> (\<forall>B>0. \<exists>N. \<forall>n\<ge>N. f n \<ge> Real B)" (is "?l = ?r")
  2133   unfolding Lim_omega apply safe defer
  2134   apply(erule_tac x="max 1 B" in allE) apply safe defer
  2135   apply(rule_tac x=N in exI,safe) apply(erule_tac x=n in allE,safe)
  2136   apply(rule_tac y="Real (max 1 B)" in order_trans) by auto
  2137 
  2138 lemma pextreal_LimI_finite:
  2139   assumes "x \<noteq> \<omega>" "\<And>r. 0 < r \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. u n < x + r \<and> x < u n + r"
  2140   shows "u ----> x"
  2141 proof (rule topological_tendstoI, unfold eventually_sequentially)
  2142   fix S assume "open S" "x \<in> S"
  2143   then obtain A where "open A" and A_eq: "Real ` (A \<inter> {0..}) = S - {\<omega>}" by (auto elim!: pextreal_openE)
  2144   then have "x \<in> Real ` (A \<inter> {0..})" using `x \<in> S` `x \<noteq> \<omega>` by auto
  2145   then have "real x \<in> A" by auto
  2146   then obtain r where "0 < r" and dist: "\<And>y. dist y (real x) < r \<Longrightarrow> y \<in> A"
  2147     using `open A` unfolding open_real_def by auto
  2148   then obtain n where
  2149     upper: "\<And>N. n \<le> N \<Longrightarrow> u N < x + Real r" and
  2150     lower: "\<And>N. n \<le> N \<Longrightarrow> x < u N + Real r" using assms(2)[of "Real r"] by auto
  2151   show "\<exists>N. \<forall>n\<ge>N. u n \<in> S"
  2152   proof (safe intro!: exI[of _ n])
  2153     fix N assume "n \<le> N"
  2154     from upper[OF this] `x \<noteq> \<omega>` `0 < r`
  2155     have "u N \<noteq> \<omega>" by (force simp: pextreal_noteq_omega_Ex)
  2156     with `x \<noteq> \<omega>` `0 < r` lower[OF `n \<le> N`] upper[OF `n \<le> N`]
  2157     have "dist (real (u N)) (real x) < r" "u N \<noteq> \<omega>"
  2158       by (auto simp: pextreal_noteq_omega_Ex dist_real_def abs_diff_less_iff field_simps)
  2159     from dist[OF this(1)]
  2160     have "u N \<in> Real ` (A \<inter> {0..})" using `u N \<noteq> \<omega>`
  2161       by (auto intro!: image_eqI[of _ _ "real (u N)"] simp: pextreal_noteq_omega_Ex Real_real)
  2162     thus "u N \<in> S" using A_eq by simp
  2163   qed
  2164 qed
  2165 
  2166 lemma real_Real_max:"real (Real x) = max x 0"
  2167   unfolding real_Real by auto
  2168 
  2169 lemma Sup_lim:
  2170   assumes "\<forall>n. b n \<in> s" "b ----> (a::pextreal)"
  2171   shows "a \<le> Sup s"
  2172 proof(rule ccontr,unfold not_le)
  2173   assume as:"Sup s < a" hence om:"Sup s \<noteq> \<omega>" by auto
  2174   have s:"s \<noteq> {}" using assms by auto
  2175   { presume *:"\<forall>n. b n < a \<Longrightarrow> False"
  2176     show False apply(cases,rule *,assumption,unfold not_all not_less)
  2177     proof- case goal1 then guess n .. note n=this
  2178       thus False using complete_lattice_class.Sup_upper[OF assms(1)[rule_format,of n]]
  2179         using as by auto
  2180     qed
  2181   } assume b:"\<forall>n. b n < a"
  2182   show False
  2183   proof(cases "a = \<omega>")
  2184     case False have *:"a - Sup s > 0" 
  2185       using False as by(auto simp: pextreal_zero_le_diff)
  2186     have "(a - Sup s) / 2 \<le> a / 2" unfolding divide_pextreal_def
  2187       apply(rule mult_right_mono) by auto
  2188     also have "... = Real (real (a / 2))" apply(rule Real_real'[THEN sym])
  2189       using False by auto
  2190     also have "... < Real (real a)" unfolding pextreal_less using as False
  2191       by(auto simp add: real_of_pextreal_mult[THEN sym])
  2192     also have "... = a" apply(rule Real_real') using False by auto
  2193     finally have asup:"a > (a - Sup s) / 2" .
  2194     have "\<exists>n. a - b n < (a - Sup s) / 2"
  2195     proof(rule ccontr,unfold not_ex not_less)
  2196       case goal1
  2197       have "(a - Sup s) * Real (1 / 2)  > 0" 
  2198         using * by auto
  2199       hence "a - (a - Sup s) * Real (1 / 2) < a"
  2200         apply-apply(rule pextreal_minus_strict_mono)
  2201         using False * by auto
  2202       hence *:"a \<in> {a - (a - Sup s) / 2<..}"using asup by auto 
  2203       note topological_tendstoD[OF assms(2) open_pextreal_greaterThan,OF *]
  2204       from this[unfolded eventually_sequentially] guess n .. 
  2205       note n = this[rule_format,of n] 
  2206       have "b n + (a - Sup s) / 2 \<le> a" 
  2207         using add_right_mono[OF goal1[rule_format,of n],of "b n"]
  2208         unfolding pextreal_minus_plus[OF less_imp_le[OF b[rule_format]]]
  2209         by(auto simp: add_commute)
  2210       hence "b n \<le> a - (a - Sup s) / 2" unfolding pextreal_le_minus_iff
  2211         using asup by auto
  2212       hence "b n \<notin> {a - (a - Sup s) / 2<..}" by auto
  2213       thus False using n by auto
  2214     qed
  2215     then guess n .. note n = this
  2216     have "Sup s < a - (a - Sup s) / 2"
  2217       using False as om by (cases a) (auto simp: pextreal_noteq_omega_Ex field_simps)
  2218     also have "... \<le> b n"
  2219     proof- note add_right_mono[OF less_imp_le[OF n],of "b n"]
  2220       note this[unfolded pextreal_minus_plus[OF less_imp_le[OF b[rule_format]]]]
  2221       hence "a - (a - Sup s) / 2 \<le> (a - Sup s) / 2 + b n - (a - Sup s) / 2"
  2222         apply(rule pextreal_minus_le_cancel_right) using asup by auto
  2223       also have "... = b n + (a - Sup s) / 2 - (a - Sup s) / 2" 
  2224         by(auto simp add: add_commute)
  2225       also have "... = b n" apply(subst pextreal_cancel_plus_minus)
  2226       proof(rule ccontr,unfold not_not) case goal1
  2227         show ?case using asup unfolding goal1 by auto 
  2228       qed auto
  2229       finally show ?thesis .
  2230     qed     
  2231     finally show False
  2232       using complete_lattice_class.Sup_upper[OF assms(1)[rule_format,of n]] by auto  
  2233   next case True
  2234     from assms(2)[unfolded True Lim_omega_gt,rule_format,of "real (Sup s)"]
  2235     guess N .. note N = this[rule_format,of N]
  2236     thus False using complete_lattice_class.Sup_upper[OF assms(1)[rule_format,of N]] 
  2237       unfolding Real_real using om by auto
  2238   qed qed
  2239 
  2240 lemma Sup_mono_lim:
  2241   assumes "\<forall>a\<in>A. \<exists>b. \<forall>n. b n \<in> B \<and> b ----> (a::pextreal)"
  2242   shows "Sup A \<le> Sup B"
  2243   unfolding Sup_le_iff apply(rule) apply(drule assms[rule_format]) apply safe
  2244   apply(rule_tac b=b in Sup_lim) by auto
  2245 
  2246 lemma pextreal_less_add:
  2247   assumes "x \<noteq> \<omega>" "a < b"
  2248   shows "x + a < x + b"
  2249   using assms by (cases a, cases b, cases x) auto
  2250 
  2251 lemma SUPR_lim:
  2252   assumes "\<forall>n. b n \<in> B" "(\<lambda>n. f (b n)) ----> (f a::pextreal)"
  2253   shows "f a \<le> SUPR B f"
  2254   unfolding SUPR_def apply(rule Sup_lim[of "\<lambda>n. f (b n)"])
  2255   using assms by auto
  2256 
  2257 lemma SUP_\<omega>_imp:
  2258   assumes "(SUP i. f i) = \<omega>"
  2259   shows "\<exists>i. Real x < f i"
  2260 proof (rule ccontr)
  2261   assume "\<not> ?thesis" hence "\<And>i. f i \<le> Real x" by (simp add: not_less)
  2262   hence "(SUP i. f i) \<le> Real x" unfolding SUP_le_iff by auto
  2263   with assms show False by auto
  2264 qed
  2265 
  2266 lemma SUPR_mono_lim:
  2267   assumes "\<forall>a\<in>A. \<exists>b. \<forall>n. b n \<in> B \<and> (\<lambda>n. f (b n)) ----> (f a::pextreal)"
  2268   shows "SUPR A f \<le> SUPR B f"
  2269   unfolding SUPR_def apply(rule Sup_mono_lim)
  2270   apply safe apply(drule assms[rule_format],safe)
  2271   apply(rule_tac x="\<lambda>n. f (b n)" in exI) by auto
  2272 
  2273 lemma real_0_imp_eq_0:
  2274   assumes "x \<noteq> \<omega>" "real x = 0"
  2275   shows "x = 0"
  2276 using assms by (cases x) auto
  2277 
  2278 lemma SUPR_mono:
  2279   assumes "\<forall>a\<in>A. \<exists>b\<in>B. f b \<ge> f a"
  2280   shows "SUPR A f \<le> SUPR B f"
  2281   unfolding SUPR_def apply(rule Sup_mono)
  2282   using assms by auto
  2283 
  2284 lemma less_add_Real:
  2285   fixes x :: real
  2286   fixes a b :: pextreal
  2287   assumes "x \<ge> 0" "a < b"
  2288   shows "a + Real x < b + Real x"
  2289 using assms by (cases a, cases b) auto
  2290 
  2291 lemma le_add_Real:
  2292   fixes x :: real
  2293   fixes a b :: pextreal
  2294   assumes "x \<ge> 0" "a \<le> b"
  2295   shows "a + Real x \<le> b + Real x"
  2296 using assms by (cases a, cases b) auto
  2297 
  2298 lemma le_imp_less_pextreal:
  2299   fixes x :: pextreal
  2300   assumes "x > 0" "a + x \<le> b" "a \<noteq> \<omega>"
  2301   shows "a < b"
  2302 using assms by (cases x, cases a, cases b) auto
  2303 
  2304 lemma pextreal_INF_minus:
  2305   fixes f :: "nat \<Rightarrow> pextreal"
  2306   assumes "c \<noteq> \<omega>"
  2307   shows "(INF i. c - f i) = c - (SUP i. f i)"
  2308 proof (cases "SUP i. f i")
  2309   case infinite
  2310   from `c \<noteq> \<omega>` obtain x where [simp]: "c = Real x" by (cases c) auto
  2311   from SUP_\<omega>_imp[OF infinite] obtain i where "Real x < f i" by auto
  2312   have "(INF i. c - f i) \<le> c - f i"
  2313     by (auto intro!: complete_lattice_class.INF_leI)
  2314   also have "\<dots> = 0" using `Real x < f i` by (auto simp: minus_pextreal_eq)
  2315   finally show ?thesis using infinite by auto
  2316 next
  2317   case (preal r)
  2318   from `c \<noteq> \<omega>` obtain x where c: "c = Real x" by (cases c) auto
  2319 
  2320   show ?thesis unfolding c
  2321   proof (rule pextreal_INFI)
  2322     fix i have "f i \<le> (SUP i. f i)" by (rule le_SUPI) simp
  2323     thus "Real x - (SUP i. f i) \<le> Real x - f i" by (rule pextreal_minus_le_cancel)
  2324   next
  2325     fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> y \<le> Real x - f i"
  2326     from this[of 0] obtain p where p: "y = Real p" "0 \<le> p"
  2327       by (cases "f 0", cases y, auto split: split_if_asm)
  2328     hence "\<And>i. Real p \<le> Real x - f i" using * by auto
  2329     hence *: "\<And>i. Real x \<le> f i \<Longrightarrow> Real p = 0"
  2330       "\<And>i. f i < Real x \<Longrightarrow> Real p + f i \<le> Real x"
  2331       unfolding pextreal_le_minus_iff by auto
  2332     show "y \<le> Real x - (SUP i. f i)" unfolding p pextreal_le_minus_iff
  2333     proof safe
  2334       assume x_less: "Real x \<le> (SUP i. f i)"
  2335       show "Real p = 0"
  2336       proof (rule ccontr)
  2337         assume "Real p \<noteq> 0"
  2338         hence "0 < Real p" by auto
  2339         from Sup_close[OF this, of "range f"]
  2340         obtain i where e: "(SUP i. f i) < f i + Real p"
  2341           using preal unfolding SUPR_def by auto
  2342         hence "Real x \<le> f i + Real p" using x_less by auto
  2343         show False
  2344         proof cases
  2345           assume "\<forall>i. f i < Real x"
  2346           hence "Real p + f i \<le> Real x" using * by auto
  2347           hence "f i + Real p \<le> (SUP i. f i)" using x_less by (auto simp: field_simps)
  2348           thus False using e by auto
  2349         next
  2350           assume "\<not> (\<forall>i. f i < Real x)"
  2351           then obtain i where "Real x \<le> f i" by (auto simp: not_less)
  2352           from *(1)[OF this] show False using `Real p \<noteq> 0` by auto
  2353         qed
  2354       qed
  2355     next
  2356       have "\<And>i. f i \<le> (SUP i. f i)" by (rule complete_lattice_class.le_SUPI) auto
  2357       also assume "(SUP i. f i) < Real x"
  2358       finally have "\<And>i. f i < Real x" by auto
  2359       hence *: "\<And>i. Real p + f i \<le> Real x" using * by auto
  2360       have "Real p \<le> Real x" using *[of 0] by (cases "f 0") (auto split: split_if_asm)
  2361 
  2362       have SUP_eq: "(SUP i. f i) \<le> Real x - Real p"
  2363       proof (rule SUP_leI)
  2364         fix i show "f i \<le> Real x - Real p" unfolding pextreal_le_minus_iff
  2365         proof safe
  2366           assume "Real x \<le> Real p"
  2367           with *[of i] show "f i = 0"
  2368             by (cases "f i") (auto split: split_if_asm)
  2369         next
  2370           assume "Real p < Real x"
  2371           show "f i + Real p \<le> Real x" using * by (auto simp: field_simps)
  2372         qed
  2373       qed
  2374 
  2375       show "Real p + (SUP i. f i) \<le> Real x"
  2376       proof cases
  2377         assume "Real x \<le> Real p"
  2378         with `Real p \<le> Real x` have [simp]: "Real p = Real x" by (rule antisym)
  2379         { fix i have "f i = 0" using *[of i] by (cases "f i") (auto split: split_if_asm) }
  2380         hence "(SUP i. f i) \<le> 0" by (auto intro!: SUP_leI)
  2381         thus ?thesis by simp
  2382       next
  2383         assume "\<not> Real x \<le> Real p" hence "Real p < Real x" unfolding not_le .
  2384         with SUP_eq show ?thesis unfolding pextreal_le_minus_iff by (auto simp: field_simps)
  2385       qed
  2386     qed
  2387   qed
  2388 qed
  2389 
  2390 lemma pextreal_SUP_minus:
  2391   fixes f :: "nat \<Rightarrow> pextreal"
  2392   shows "(SUP i. c - f i) = c - (INF i. f i)"
  2393 proof (rule pextreal_SUPI)
  2394   fix i have "(INF i. f i) \<le> f i" by (rule INF_leI) simp
  2395   thus "c - f i \<le> c - (INF i. f i)" by (rule pextreal_minus_le_cancel)
  2396 next
  2397   fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> c - f i \<le> y"
  2398   show "c - (INF i. f i) \<le> y"
  2399   proof (cases y)
  2400     case (preal p)
  2401 
  2402     show ?thesis unfolding pextreal_minus_le_iff preal
  2403     proof safe
  2404       assume INF_le_x: "(INF i. f i) \<le> c"
  2405       from * have *: "\<And>i. f i \<le> c \<Longrightarrow> c \<le> Real p + f i"
  2406         unfolding pextreal_minus_le_iff preal by auto
  2407 
  2408       have INF_eq: "c - Real p \<le> (INF i. f i)"
  2409       proof (rule le_INFI)
  2410         fix i show "c - Real p \<le> f i" unfolding pextreal_minus_le_iff
  2411         proof safe
  2412           assume "Real p \<le> c"
  2413           show "c \<le> f i + Real p"
  2414           proof cases
  2415             assume "f i \<le> c" from *[OF this]
  2416             show ?thesis by (simp add: field_simps)
  2417           next
  2418             assume "\<not> f i \<le> c"
  2419             hence "c \<le> f i" by auto
  2420             also have "\<dots> \<le> f i + Real p" by auto
  2421             finally show ?thesis .
  2422           qed
  2423         qed
  2424       qed
  2425 
  2426       show "c \<le> Real p + (INF i. f i)"
  2427       proof cases
  2428         assume "Real p \<le> c"
  2429         with INF_eq show ?thesis unfolding pextreal_minus_le_iff by (auto simp: field_simps)
  2430       next
  2431         assume "\<not> Real p \<le> c"
  2432         hence "c \<le> Real p" by auto
  2433         also have "Real p \<le> Real p + (INF i. f i)" by auto
  2434         finally show ?thesis .
  2435       qed
  2436     qed
  2437   qed simp
  2438 qed
  2439 
  2440 lemma pextreal_le_minus_imp_0:
  2441   fixes a b :: pextreal
  2442   shows "a \<le> a - b \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> a \<noteq> \<omega> \<Longrightarrow> b = 0"
  2443   by (cases a, cases b, auto split: split_if_asm)
  2444 
  2445 lemma lim_INF_eq_lim_SUP:
  2446   fixes X :: "nat \<Rightarrow> real"
  2447   assumes "\<And>i. 0 \<le> X i" and "0 \<le> x"
  2448   and lim_INF: "(SUP n. INF m. Real (X (n + m))) = Real x" (is "(SUP n. ?INF n) = _")
  2449   and lim_SUP: "(INF n. SUP m. Real (X (n + m))) = Real x" (is "(INF n. ?SUP n) = _")
  2450   shows "X ----> x"
  2451 proof (rule LIMSEQ_I)
  2452   fix r :: real assume "0 < r"
  2453   hence "0 \<le> r" by auto
  2454   from Sup_close[of "Real r" "range ?INF"]
  2455   obtain n where inf: "Real x < ?INF n + Real r"
  2456     unfolding SUPR_def lim_INF[unfolded SUPR_def] using `0 < r` by auto
  2457 
  2458   from Inf_close[of "range ?SUP" "Real r"]
  2459   obtain n' where sup: "?SUP n' < Real x + Real r"
  2460     unfolding INFI_def lim_SUP[unfolded INFI_def] using `0 < r` by auto
  2461 
  2462   show "\<exists>N. \<forall>n\<ge>N. norm (X n - x) < r"
  2463   proof (safe intro!: exI[of _ "max n n'"])
  2464     fix m assume "max n n' \<le> m" hence "n \<le> m" "n' \<le> m" by auto
  2465 
  2466     note inf
  2467     also have "?INF n + Real r \<le> Real (X (n + (m - n))) + Real r"
  2468       by (rule le_add_Real, auto simp: `0 \<le> r` intro: INF_leI)
  2469     finally have up: "x < X m + r"
  2470       using `0 \<le> X m` `0 \<le> x` `0 \<le> r` `n \<le> m` by auto
  2471 
  2472     have "Real (X (n' + (m - n'))) \<le> ?SUP n'"
  2473       by (auto simp: `0 \<le> r` intro: le_SUPI)
  2474     also note sup
  2475     finally have down: "X m < x + r"
  2476       using `0 \<le> X m` `0 \<le> x` `0 \<le> r` `n' \<le> m` by auto
  2477 
  2478     show "norm (X m - x) < r" using up down by auto
  2479   qed
  2480 qed
  2481 
  2482 lemma Sup_countable_SUPR:
  2483   assumes "Sup A \<noteq> \<omega>" "A \<noteq> {}"
  2484   shows "\<exists> f::nat \<Rightarrow> pextreal. range f \<subseteq> A \<and> Sup A = SUPR UNIV f"
  2485 proof -
  2486   have "\<And>n. 0 < 1 / (of_nat n :: pextreal)" by auto
  2487   from Sup_close[OF this assms]
  2488   have "\<forall>n. \<exists>x. x \<in> A \<and> Sup A < x + 1 / of_nat n" by blast
  2489   from choice[OF this] obtain f where "range f \<subseteq> A" and
  2490     epsilon: "\<And>n. Sup A < f n + 1 / of_nat n" by blast
  2491   have "SUPR UNIV f = Sup A"
  2492   proof (rule pextreal_SUPI)
  2493     fix i show "f i \<le> Sup A" using `range f \<subseteq> A`
  2494       by (auto intro!: complete_lattice_class.Sup_upper)
  2495   next
  2496     fix y assume bound: "\<And>i. i \<in> UNIV \<Longrightarrow> f i \<le> y"
  2497     show "Sup A \<le> y"
  2498     proof (rule pextreal_le_epsilon)
  2499       fix e :: pextreal assume "0 < e"
  2500       show "Sup A \<le> y + e"
  2501       proof (cases e)
  2502         case (preal r)
  2503         hence "0 < r" using `0 < e` by auto
  2504         then obtain n where *: "inverse (of_nat n) < r" "0 < n"
  2505           using ex_inverse_of_nat_less by auto
  2506         have "Sup A \<le> f n + 1 / of_nat n" using epsilon[of n] by auto
  2507         also have "1 / of_nat n \<le> e" using preal * by (auto simp: real_eq_of_nat)
  2508         with bound have "f n + 1 / of_nat n \<le> y + e" by (rule add_mono) simp
  2509         finally show "Sup A \<le> y + e" .
  2510       qed simp
  2511     qed
  2512   qed
  2513   with `range f \<subseteq> A` show ?thesis by (auto intro!: exI[of _ f])
  2514 qed
  2515 
  2516 lemma SUPR_countable_SUPR:
  2517   assumes "SUPR A g \<noteq> \<omega>" "A \<noteq> {}"
  2518   shows "\<exists> f::nat \<Rightarrow> pextreal. range f \<subseteq> g`A \<and> SUPR A g = SUPR UNIV f"
  2519 proof -
  2520   have "Sup (g`A) \<noteq> \<omega>" "g`A \<noteq> {}" using assms unfolding SUPR_def by auto
  2521   from Sup_countable_SUPR[OF this]
  2522   show ?thesis unfolding SUPR_def .
  2523 qed
  2524 
  2525 lemma pextreal_setsum_subtractf:
  2526   assumes "\<And>i. i\<in>A \<Longrightarrow> g i \<le> f i" and "\<And>i. i\<in>A \<Longrightarrow> f i \<noteq> \<omega>"
  2527   shows "(\<Sum>i\<in>A. f i - g i) = (\<Sum>i\<in>A. f i) - (\<Sum>i\<in>A. g i)"
  2528 proof cases
  2529   assume "finite A" from this assms show ?thesis
  2530   proof induct
  2531     case (insert x A)
  2532     hence hyp: "(\<Sum>i\<in>A. f i - g i) = (\<Sum>i\<in>A. f i) - (\<Sum>i\<in>A. g i)"
  2533       by auto
  2534     { fix i assume *: "i \<in> insert x A"
  2535       hence "g i \<le> f i" using insert by simp
  2536       also have "f i < \<omega>" using * insert by (simp add: pextreal_less_\<omega>)
  2537       finally have "g i \<noteq> \<omega>" by (simp add: pextreal_less_\<omega>) }
  2538     hence "setsum g A \<noteq> \<omega>" "g x \<noteq> \<omega>" by (auto simp: setsum_\<omega>)
  2539     moreover have "setsum f A \<noteq> \<omega>" "f x \<noteq> \<omega>" using insert by (auto simp: setsum_\<omega>)
  2540     moreover have "g x \<le> f x" using insert by auto
  2541     moreover have "(\<Sum>i\<in>A. g i) \<le> (\<Sum>i\<in>A. f i)" using insert by (auto intro!: setsum_mono)
  2542     ultimately show ?case using `finite A` `x \<notin> A` hyp
  2543       by (auto simp: pextreal_noteq_omega_Ex)
  2544   qed simp
  2545 qed simp
  2546 
  2547 lemma real_of_pextreal_diff:
  2548   "y \<le> x \<Longrightarrow> x \<noteq> \<omega> \<Longrightarrow> real x - real y = real (x - y)"
  2549   by (cases x, cases y) auto
  2550 
  2551 lemma psuminf_minus:
  2552   assumes ord: "\<And>i. g i \<le> f i" and fin: "psuminf g \<noteq> \<omega>" "psuminf f \<noteq> \<omega>"
  2553   shows "(\<Sum>\<^isub>\<infinity> i. f i - g i) = psuminf f - psuminf g"
  2554 proof -
  2555   have [simp]: "\<And>i. f i \<noteq> \<omega>" using fin by (auto intro: psuminf_\<omega>)
  2556   from fin have "(\<lambda>x. real (f x)) sums real (\<Sum>\<^isub>\<infinity>x. f x)"
  2557     and "(\<lambda>x. real (g x)) sums real (\<Sum>\<^isub>\<infinity>x. g x)"
  2558     by (auto intro: psuminf_imp_suminf)
  2559   from sums_diff[OF this]
  2560   have "(\<lambda>n. real (f n - g n)) sums (real ((\<Sum>\<^isub>\<infinity>x. f x) - (\<Sum>\<^isub>\<infinity>x. g x)))" using fin ord
  2561     by (subst (asm) (1 2) real_of_pextreal_diff) (auto simp: psuminf_\<omega> psuminf_le)
  2562   hence "(\<Sum>\<^isub>\<infinity> i. Real (real (f i - g i))) = Real (real ((\<Sum>\<^isub>\<infinity>x. f x) - (\<Sum>\<^isub>\<infinity>x. g x)))"
  2563     by (rule suminf_imp_psuminf) simp
  2564   thus ?thesis using fin by (simp add: Real_real psuminf_\<omega>)
  2565 qed
  2566 
  2567 lemma INF_eq_LIMSEQ:
  2568   assumes "mono (\<lambda>i. - f i)" and "\<And>n. 0 \<le> f n" and "0 \<le> x"
  2569   shows "(INF n. Real (f n)) = Real x \<longleftrightarrow> f ----> x"
  2570 proof
  2571   assume x: "(INF n. Real (f n)) = Real x"
  2572   { fix n
  2573     have "Real x \<le> Real (f n)" using x[symmetric] by (auto intro: INF_leI)
  2574     hence "x \<le> f n" using assms by simp
  2575     hence "\<bar>f n - x\<bar> = f n - x" by auto }
  2576   note abs_eq = this
  2577   show "f ----> x"
  2578   proof (rule LIMSEQ_I)
  2579     fix r :: real assume "0 < r"
  2580     show "\<exists>no. \<forall>n\<ge>no. norm (f n - x) < r"
  2581     proof (rule ccontr)
  2582       assume *: "\<not> ?thesis"
  2583       { fix N
  2584         from * obtain n where *: "N \<le> n" "r \<le> f n - x"
  2585           using abs_eq by (auto simp: not_less)
  2586         hence "x + r \<le> f n" by auto
  2587         also have "f n \<le> f N" using `mono (\<lambda>i. - f i)` * by (auto dest: monoD)
  2588         finally have "Real (x + r) \<le> Real (f N)" using `0 \<le> f N` by auto }
  2589       hence "Real x < Real (x + r)"
  2590         and "Real (x + r) \<le> (INF n. Real (f n))" using `0 < r` `0 \<le> x` by (auto intro: le_INFI)
  2591       hence "Real x < (INF n. Real (f n))" by (rule less_le_trans)
  2592       thus False using x by auto
  2593     qed
  2594   qed
  2595 next
  2596   assume "f ----> x"
  2597   show "(INF n. Real (f n)) = Real x"
  2598   proof (rule pextreal_INFI)
  2599     fix n
  2600     from decseq_le[OF _ `f ----> x`] assms
  2601     show "Real x \<le> Real (f n)" unfolding decseq_eq_incseq incseq_mono by auto
  2602   next
  2603     fix y assume *: "\<And>n. n\<in>UNIV \<Longrightarrow> y \<le> Real (f n)"
  2604     thus "y \<le> Real x"
  2605     proof (cases y)
  2606       case (preal r)
  2607       with * have "\<exists>N. \<forall>n\<ge>N. r \<le> f n" using assms by fastsimp
  2608       from LIMSEQ_le_const[OF `f ----> x` this]
  2609       show "y \<le> Real x" using `0 \<le> x` preal by auto
  2610     qed simp
  2611   qed
  2612 qed
  2613 
  2614 lemma INFI_bound:
  2615   assumes "\<forall>N. x \<le> f N"
  2616   shows "x \<le> (INF n. f n)"
  2617   using assms by (simp add: INFI_def le_Inf_iff)
  2618 
  2619 lemma LIMSEQ_imp_lim_INF:
  2620   assumes pos: "\<And>i. 0 \<le> X i" and lim: "X ----> x"
  2621   shows "(SUP n. INF m. Real (X (n + m))) = Real x"
  2622 proof -
  2623   have "0 \<le> x" using assms by (auto intro!: LIMSEQ_le_const)
  2624 
  2625   have "\<And>n. (INF m. Real (X (n + m))) \<le> Real (X (n + 0))" by (rule INF_leI) simp
  2626   also have "\<And>n. Real (X (n + 0)) < \<omega>" by simp
  2627   finally have "\<forall>n. \<exists>r\<ge>0. (INF m. Real (X (n + m))) = Real r"
  2628     by (auto simp: pextreal_less_\<omega> pextreal_noteq_omega_Ex)
  2629   from choice[OF this] obtain r where r: "\<And>n. (INF m. Real (X (n + m))) = Real (r n)" "\<And>n. 0 \<le> r n"
  2630     by auto
  2631 
  2632   show ?thesis unfolding r
  2633   proof (subst SUP_eq_LIMSEQ)
  2634     show "mono r" unfolding mono_def
  2635     proof safe
  2636       fix x y :: nat assume "x \<le> y"
  2637       have "Real (r x) \<le> Real (r y)" unfolding r(1)[symmetric] using pos
  2638       proof (safe intro!: INF_mono bexI)
  2639         fix m have "x + (m + y - x) = y + m"
  2640           using `x \<le> y` by auto
  2641         thus "Real (X (x + (m + y - x))) \<le> Real (X (y + m))" by simp
  2642       qed simp
  2643       thus "r x \<le> r y" using r by auto
  2644     qed
  2645     show "\<And>n. 0 \<le> r n" by fact
  2646     show "0 \<le> x" by fact
  2647     show "r ----> x"
  2648     proof (rule LIMSEQ_I)
  2649       fix e :: real assume "0 < e"
  2650       hence "0 < e/2" by auto
  2651       from LIMSEQ_D[OF lim this] obtain N where *: "\<And>n. N \<le> n \<Longrightarrow> \<bar>X n - x\<bar> < e/2"
  2652         by auto
  2653       show "\<exists>N. \<forall>n\<ge>N. norm (r n - x) < e"
  2654       proof (safe intro!: exI[of _ N])
  2655         fix n assume "N \<le> n"
  2656         show "norm (r n - x) < e"
  2657         proof cases
  2658           assume "r n < x"
  2659           have "x - r n \<le> e/2"
  2660           proof cases
  2661             assume e: "e/2 \<le> x"
  2662             have "Real (x - e/2) \<le> Real (r n)" unfolding r(1)[symmetric]
  2663             proof (rule le_INFI)
  2664               fix m show "Real (x - e / 2) \<le> Real (X (n + m))"
  2665                 using *[of "n + m"] `N \<le> n`
  2666                 using pos by (auto simp: field_simps abs_real_def split: split_if_asm)
  2667             qed
  2668             with e show ?thesis using pos `0 \<le> x` r(2) by auto
  2669           next
  2670             assume "\<not> e/2 \<le> x" hence "x - e/2 < 0" by auto
  2671             with `0 \<le> r n` show ?thesis by auto
  2672           qed
  2673           with `r n < x` show ?thesis by simp
  2674         next
  2675           assume e: "\<not> r n < x"
  2676           have "Real (r n) \<le> Real (X (n + 0))" unfolding r(1)[symmetric]
  2677             by (rule INF_leI) simp
  2678           hence "r n - x \<le> X n - x" using r pos by auto
  2679           also have "\<dots> < e/2" using *[OF `N \<le> n`] by (auto simp: field_simps abs_real_def split: split_if_asm)
  2680           finally have "r n - x < e" using `0 < e` by auto
  2681           with e show ?thesis by auto
  2682         qed
  2683       qed
  2684     qed
  2685   qed
  2686 qed
  2687 
  2688 lemma real_of_pextreal_strict_mono_iff:
  2689   "real a < real b \<longleftrightarrow> (b \<noteq> \<omega> \<and> ((a = \<omega> \<and> 0 < b) \<or> (a < b)))"
  2690 proof (cases a)
  2691   case infinite thus ?thesis by (cases b) auto
  2692 next
  2693   case preal thus ?thesis by (cases b) auto
  2694 qed
  2695 
  2696 lemma real_of_pextreal_mono_iff:
  2697   "real a \<le> real b \<longleftrightarrow> (a = \<omega> \<or> (b \<noteq> \<omega> \<and> a \<le> b) \<or> (b = \<omega> \<and> a = 0))"
  2698 proof (cases a)
  2699   case infinite thus ?thesis by (cases b) auto
  2700 next
  2701   case preal thus ?thesis by (cases b)  auto
  2702 qed
  2703 
  2704 lemma ex_pextreal_inverse_of_nat_Suc_less:
  2705   fixes e :: pextreal assumes "0 < e" shows "\<exists>n. inverse (of_nat (Suc n)) < e"
  2706 proof (cases e)
  2707   case (preal r)
  2708   with `0 < e` ex_inverse_of_nat_Suc_less[of r]
  2709   obtain n where "inverse (of_nat (Suc n)) < r" by auto
  2710   with preal show ?thesis
  2711     by (auto simp: real_eq_of_nat[symmetric])
  2712 qed auto
  2713 
  2714 lemma Lim_eq_Sup_mono:
  2715   fixes u :: "nat \<Rightarrow> pextreal" assumes "mono u"
  2716   shows "u ----> (SUP i. u i)"
  2717 proof -
  2718   from lim_pextreal_increasing[of u] `mono u`
  2719   obtain l where l: "u ----> l" unfolding mono_def by auto
  2720   from SUP_Lim_pextreal[OF _ this] `mono u`
  2721   have "(SUP i. u i) = l" unfolding mono_def by auto
  2722   with l show ?thesis by simp
  2723 qed
  2724 
  2725 lemma isotone_Lim:
  2726   fixes x :: pextreal assumes "u \<up> x"
  2727   shows "u ----> x" (is ?lim) and "mono u" (is ?mono)
  2728 proof -
  2729   show ?mono using assms unfolding mono_iff_le_Suc isoton_def by auto
  2730   from Lim_eq_Sup_mono[OF this] `u \<up> x`
  2731   show ?lim unfolding isoton_def by simp
  2732 qed
  2733 
  2734 lemma isoton_iff_Lim_mono:
  2735   fixes u :: "nat \<Rightarrow> pextreal"
  2736   shows "u \<up> x \<longleftrightarrow> (mono u \<and> u ----> x)"
  2737 proof safe
  2738   assume "mono u" and x: "u ----> x"
  2739   with SUP_Lim_pextreal[OF _ x]
  2740   show "u \<up> x" unfolding isoton_def
  2741     using `mono u`[unfolded mono_def]
  2742     using `mono u`[unfolded mono_iff_le_Suc]
  2743     by auto
  2744 qed (auto dest: isotone_Lim)
  2745 
  2746 lemma pextreal_inverse_inverse[simp]:
  2747   fixes x :: pextreal
  2748   shows "inverse (inverse x) = x"
  2749   by (cases x) auto
  2750 
  2751 lemma atLeastAtMost_omega_eq_atLeast:
  2752   shows "{a .. \<omega>} = {a ..}"
  2753 by auto
  2754 
  2755 lemma atLeast0AtMost_eq_atMost: "{0 :: pextreal .. a} = {.. a}" by auto
  2756 
  2757 lemma greaterThan_omega_Empty: "{\<omega> <..} = {}" by auto
  2758 
  2759 lemma lessThan_0_Empty: "{..< 0 :: pextreal} = {}" by auto
  2760 
  2761 lemma real_of_pextreal_inverse[simp]:
  2762   fixes X :: pextreal
  2763   shows "real (inverse X) = 1 / real X"
  2764   by (cases X) (auto simp: inverse_eq_divide)
  2765 
  2766 lemma real_of_pextreal_le_0[simp]: "real (X :: pextreal) \<le> 0 \<longleftrightarrow> (X = 0 \<or> X = \<omega>)"
  2767   by (cases X) auto
  2768 
  2769 lemma real_of_pextreal_less_0[simp]: "\<not> (real (X :: pextreal) < 0)"
  2770   by (cases X) auto
  2771 
  2772 lemma abs_real_of_pextreal[simp]: "\<bar>real (X :: pextreal)\<bar> = real X"
  2773   by simp
  2774 
  2775 lemma zero_less_real_of_pextreal: "0 < real (X :: pextreal) \<longleftrightarrow> X \<noteq> 0 \<and> X \<noteq> \<omega>"
  2776   by (cases X) auto
  2777 
  2778 end