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
```