src/HOL/Probability/Positive_Extended_Real.thy
author hoelzl
Fri Jan 14 14:21:48 2011 +0100 (2011-01-14)
changeset 41544 c3b977fee8a3
parent 41413 64cd30d6b0b8
permissions -rw-r--r--
introduced integral syntax
     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 minus_omega[simp]: "x - \<omega> = 0" by (cases x) auto
  1607 
  1608 lemma open_pextreal_alt: "open A \<longleftrightarrow>
  1609   (\<forall>x\<in>A. \<exists>e>0. {x-e <..< x+e} \<subseteq> A) \<and> (\<omega> \<in> A \<longrightarrow> (\<exists>x\<ge>0. {Real x <..} \<subseteq> A))"
  1610 proof -
  1611   have *: "(\<exists>T. open T \<and> (Real ` (T\<inter>{0..}) = A - {\<omega>})) \<longleftrightarrow>
  1612     open (real ` (A - {\<omega>}) \<union> {..<0})"
  1613   proof safe
  1614     fix T assume "open T" and A: "Real ` (T \<inter> {0..}) = A - {\<omega>}"
  1615     have *: "(\<lambda>x. real (Real x)) ` (T \<inter> {0..}) = T \<inter> {0..}"
  1616       by auto
  1617     have **: "T \<inter> {0..} \<union> {..<0} = T \<union> {..<0}" by auto
  1618     show "open (real ` (A - {\<omega>}) \<union> {..<0})"
  1619       unfolding A[symmetric] image_image * ** using `open T` by auto
  1620   next
  1621     assume "open (real ` (A - {\<omega>}) \<union> {..<0})"
  1622     moreover have "Real ` ((real ` (A - {\<omega>}) \<union> {..<0}) \<inter> {0..}) = A - {\<omega>}"
  1623       apply auto
  1624       apply (case_tac xb)
  1625       apply auto
  1626       apply (case_tac x)
  1627       apply (auto simp: image_iff)
  1628       apply (erule_tac x="Real r" in ballE)
  1629       apply auto
  1630       done
  1631     ultimately show "\<exists>T. open T \<and> Real ` (T \<inter> {0..}) = A - {\<omega>}" by auto
  1632   qed
  1633   also have "\<dots> \<longleftrightarrow> (\<forall>x\<in>A. \<exists>e>0. {x-e <..< x+e} \<subseteq> A)"
  1634   proof (intro iffI ballI open_subopen[THEN iffD2])
  1635     fix x assume *: "\<forall>x\<in>A. \<exists>e>0. {x - e<..<x + e} \<subseteq> A" and x: "x \<in> real ` (A - {\<omega>}) \<union> {..<0}"
  1636     show "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> real ` (A - {\<omega>}) \<union> {..<0}"
  1637     proof (cases rule: linorder_cases)
  1638       assume "x < 0" then show ?thesis by (intro exI[of _ "{..<0}"]) auto
  1639     next
  1640       assume "x = 0" with x
  1641       have "0 \<in> A"
  1642         apply auto by (case_tac x) auto
  1643       with * obtain e where "e > 0" "{0 - e<..<0 + e} \<subseteq> A" by auto
  1644       then have "{..<e} \<subseteq> A" using `0 \<in> A`
  1645         apply auto
  1646         apply (case_tac "x = 0")
  1647         by (auto dest!: pextreal_zero_lessI)
  1648       then have *: "{..<e} \<subseteq> A - {\<omega>}" by auto
  1649       def e' \<equiv> "if e = \<omega> then 1 else real e"
  1650       then have "0 < e'" using `e > 0` by (cases e) auto
  1651       have "{0..<e'} \<subseteq> real ` (A - {\<omega>})"
  1652       proof (cases e)
  1653         case infinite
  1654         then have "{..<e} = UNIV - {\<omega>}" by auto
  1655         then have A: "A - {\<omega>} = UNIV - {\<omega>}" using * by auto
  1656         show ?thesis unfolding e'_def infinite A
  1657           apply safe
  1658           apply (rule_tac x="Real x" in image_eqI)
  1659           apply auto
  1660           done
  1661       next
  1662         case (preal r)
  1663         then show ?thesis unfolding e'_def using *
  1664           apply safe
  1665           apply (rule_tac x="Real x" in image_eqI)
  1666           by (auto simp: subset_eq)
  1667       qed
  1668       then have "{0..<e'} \<union> {..<0} \<subseteq> real ` (A - {\<omega>}) \<union> {..<0}" by auto
  1669       moreover have "{0..<e'} \<union> {..<0} = {..<e'}" using `0 < e'` by auto
  1670       ultimately have "{..<e'} \<subseteq> real ` (A - {\<omega>}) \<union> {..<0}" by simp
  1671       then show ?thesis using `0 < e'` `x = 0` by auto
  1672     next
  1673       assume "0 < x"
  1674       with x have "Real x \<in> A" apply auto by (case_tac x) auto
  1675       with * obtain e where "0 < e" and e: "{Real x - e<..<Real x + e} \<subseteq> A" by auto
  1676       show ?thesis
  1677       proof cases
  1678         assume "e < Real x"
  1679         with `0 < e` obtain r where r: "e = Real r" "0 < r" by (cases e) auto
  1680         then have "r < x" using `e < Real x` `0 < e` by (auto split: split_if_asm)
  1681         then have "{x - r <..< x + r} \<subseteq> real ` (A - {\<omega>}) \<union> {..<0}"
  1682           using e unfolding r
  1683           apply (auto simp: subset_eq)
  1684           apply (rule_tac x="Real xa" in image_eqI)
  1685           by auto
  1686         then show ?thesis using `0 < r` by (intro exI[of _ "{x - r <..< x + r}"]) auto
  1687       next
  1688         assume "\<not> e < Real x"
  1689         moreover then have "Real x - e = 0" by (cases e) auto
  1690         moreover have "\<And>z. 0 < z \<Longrightarrow>  z * 2 < 3 * x \<Longrightarrow> Real z < Real x + e"
  1691           using `\<not> e < Real x` by (cases e) auto
  1692         ultimately have "{0 <..< x + x / 2} \<subseteq> real ` (A - {\<omega>}) \<union> {..<0}"
  1693           using e
  1694           apply (auto simp: subset_eq)
  1695           apply (erule_tac x="Real xa" in ballE)
  1696           apply (auto simp: not_less)
  1697           apply (rule_tac x="Real xa" in image_eqI)
  1698           apply auto
  1699           done
  1700         moreover have "x \<in> {0 <..< x + x / 2}" using `0 < x` by auto
  1701         ultimately show ?thesis by (intro exI[of _ "{0 <..< x + x / 2}"]) auto
  1702       qed
  1703     qed
  1704   next
  1705     fix x assume x: "x \<in> A" "open (real ` (A - {\<omega>}) \<union> {..<0})"
  1706     then show "\<exists>e>0. {x - e<..<x + e} \<subseteq> A"
  1707     proof (cases x)
  1708       case infinite then show ?thesis by (intro exI[of _ 2]) auto
  1709     next
  1710       case (preal r)
  1711       with `x \<in> A` have r: "r \<in> real ` (A - {\<omega>}) \<union> {..<0}" by force
  1712       from x(2)[unfolded open_real, THEN bspec, OF r]
  1713       obtain e where e: "0 < e" "\<And>x'. \<bar>x' - r\<bar> < e \<Longrightarrow> x' \<in> real ` (A - {\<omega>}) \<union> {..<0}"
  1714         by auto
  1715       show ?thesis using `0 < e` preal
  1716       proof (auto intro!: exI[of _ "Real e"] simp: greaterThanLessThan_iff not_less 
  1717                   split: split_if_asm)
  1718         fix z assume *: "Real (r - e) < z" "z < Real (r + e)"
  1719         then obtain q where [simp]: "z = Real q" "0 \<le> q" by (cases z) auto
  1720         with * have "r - e < q" "q < r + e" by (auto split: split_if_asm)
  1721         with e(2)[of q] have "q \<in> real ` (A - {\<omega>}) \<union> {..<0}" by auto
  1722         then show "z \<in> A" using `0 \<le> q` apply auto apply (case_tac x) apply auto done
  1723       next
  1724         fix z assume *: "0 < z" "z < Real (r + e)" "r \<le> e"
  1725         then obtain q where [simp]: "z = Real q" and "0 < q" by (cases z) auto
  1726         with * have "q < r + e" by (auto split: split_if_asm)
  1727         moreover have "r - e < q" using `r \<le> e` `0 < q` by auto
  1728         ultimately have "q \<in> real ` (A - {\<omega>}) \<union> {..<0}" using e(2)[of q] by auto
  1729         then show "z \<in> A" using `0 < q` apply auto apply (case_tac x) apply auto done
  1730       qed
  1731     qed
  1732   qed
  1733   finally show ?thesis unfolding open_pextreal_def by simp
  1734 qed
  1735 
  1736 lemma open_pextreal_lessThan[simp]:
  1737   "open {..< a :: pextreal}"
  1738 proof (cases a)
  1739   case (preal x) thus ?thesis unfolding open_pextreal_def
  1740   proof (safe intro!: exI[of _ "{..< x}"])
  1741     fix y assume "y < Real x"
  1742     moreover assume "y \<notin> Real ` ({..<x} \<inter> {0..})"
  1743     ultimately have "y \<noteq> Real (real y)" using preal by (cases y) auto
  1744     thus "y = \<omega>" by (auto simp: Real_real split: split_if_asm)
  1745   qed auto
  1746 next
  1747   case infinite thus ?thesis
  1748     unfolding open_pextreal_def by (auto intro!: exI[of _ UNIV])
  1749 qed
  1750 
  1751 lemma open_pextreal_greaterThan[simp]:
  1752   "open {a :: pextreal <..}"
  1753 proof (cases a)
  1754   case (preal x) thus ?thesis unfolding open_pextreal_def
  1755   proof (safe intro!: exI[of _ "{x <..}"])
  1756     fix y assume "Real x < y"
  1757     moreover assume "y \<notin> Real ` ({x<..} \<inter> {0..})"
  1758     ultimately have "y \<noteq> Real (real y)" using preal by (cases y) auto
  1759     thus "y = \<omega>" by (auto simp: Real_real split: split_if_asm)
  1760   qed auto
  1761 next
  1762   case infinite thus ?thesis
  1763     unfolding open_pextreal_def by (auto intro!: exI[of _ "{}"])
  1764 qed
  1765 
  1766 lemma pextreal_open_greaterThanLessThan[simp]: "open {a::pextreal <..< b}"
  1767   unfolding greaterThanLessThan_def by auto
  1768 
  1769 lemma closed_pextreal_atLeast[simp, intro]: "closed {a :: pextreal ..}"
  1770 proof -
  1771   have "- {a ..} = {..< a}" by auto
  1772   then show "closed {a ..}"
  1773     unfolding closed_def using open_pextreal_lessThan by auto
  1774 qed
  1775 
  1776 lemma closed_pextreal_atMost[simp, intro]: "closed {.. b :: pextreal}"
  1777 proof -
  1778   have "- {.. b} = {b <..}" by auto
  1779   then show "closed {.. b}" 
  1780     unfolding closed_def using open_pextreal_greaterThan by auto
  1781 qed
  1782 
  1783 lemma closed_pextreal_atLeastAtMost[simp, intro]:
  1784   shows "closed {a :: pextreal .. b}"
  1785   unfolding atLeastAtMost_def by auto
  1786 
  1787 lemma pextreal_dense:
  1788   fixes x y :: pextreal assumes "x < y"
  1789   shows "\<exists>z. x < z \<and> z < y"
  1790 proof -
  1791   from `x < y` obtain p where p: "x = Real p" "0 \<le> p" by (cases x) auto
  1792   show ?thesis
  1793   proof (cases y)
  1794     case (preal r) with p `x < y` have "p < r" by auto
  1795     with dense obtain z where "p < z" "z < r" by auto
  1796     thus ?thesis using preal p by (auto intro!: exI[of _ "Real z"])
  1797   next
  1798     case infinite thus ?thesis using `x < y` p
  1799       by (auto intro!: exI[of _ "Real p + 1"])
  1800   qed
  1801 qed
  1802 
  1803 instance pextreal :: t2_space
  1804 proof
  1805   fix x y :: pextreal assume "x \<noteq> y"
  1806   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 = {}"
  1807 
  1808   { fix x y :: pextreal assume "x < y"
  1809     from pextreal_dense[OF this] obtain z where z: "x < z" "z < y" by auto
  1810     have "?P x y"
  1811       apply (rule exI[of _ "{..<z}"])
  1812       apply (rule exI[of _ "{z<..}"])
  1813       using z by auto }
  1814   note * = this
  1815 
  1816   from `x \<noteq> y`
  1817   show "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
  1818   proof (cases rule: linorder_cases)
  1819     assume "x = y" with `x \<noteq> y` show ?thesis by simp
  1820   next assume "x < y" from *[OF this] show ?thesis by auto
  1821   next assume "y < x" from *[OF this] show ?thesis by auto
  1822   qed
  1823 qed
  1824 
  1825 definition (in complete_lattice) isoton :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<up>" 50) where
  1826   "A \<up> X \<longleftrightarrow> (\<forall>i. A i \<le> A (Suc i)) \<and> (SUP i. A i) = X"
  1827 
  1828 definition (in complete_lattice) antiton (infix "\<down>" 50) where
  1829   "A \<down> X \<longleftrightarrow> (\<forall>i. A i \<ge> A (Suc i)) \<and> (INF i. A i) = X"
  1830 
  1831 lemma isotoneI[intro?]: "\<lbrakk> \<And>i. f i \<le> f (Suc i) ; (SUP i. f i) = F \<rbrakk> \<Longrightarrow> f \<up> F"
  1832   unfolding isoton_def by auto
  1833 
  1834 lemma (in complete_lattice) isotonD[dest]:
  1835   assumes "A \<up> X" shows "A i \<le> A (Suc i)" "(SUP i. A i) = X"
  1836   using assms unfolding isoton_def by auto
  1837 
  1838 lemma isotonD'[dest]:
  1839   assumes "(A::_=>_) \<up> X" shows "A i x \<le> A (Suc i) x" "(SUP i. A i) = X"
  1840   using assms unfolding isoton_def le_fun_def by auto
  1841 
  1842 lemma isoton_mono_le:
  1843   assumes "f \<up> x" "i \<le> j"
  1844   shows "f i \<le> f j"
  1845   using `f \<up> x`[THEN isotonD(1)] lift_Suc_mono_le[of f, OF _ `i \<le> j`] by auto
  1846 
  1847 lemma isoton_const:
  1848   shows "(\<lambda> i. c) \<up> c"
  1849 unfolding isoton_def by auto
  1850 
  1851 lemma isoton_cmult_right:
  1852   assumes "f \<up> (x::pextreal)"
  1853   shows "(\<lambda>i. c * f i) \<up> (c * x)"
  1854   using assms unfolding isoton_def pextreal_SUP_cmult
  1855   by (auto intro: pextreal_mult_cancel)
  1856 
  1857 lemma isoton_cmult_left:
  1858   "f \<up> (x::pextreal) \<Longrightarrow> (\<lambda>i. f i * c) \<up> (x * c)"
  1859   by (subst (1 2) mult_commute) (rule isoton_cmult_right)
  1860 
  1861 lemma isoton_add:
  1862   assumes "f \<up> (x::pextreal)" and "g \<up> y"
  1863   shows "(\<lambda>i. f i + g i) \<up> (x + y)"
  1864   using assms unfolding isoton_def
  1865   by (auto intro: pextreal_mult_cancel add_mono simp: SUPR_pextreal_add)
  1866 
  1867 lemma isoton_fun_expand:
  1868   "f \<up> x \<longleftrightarrow> (\<forall>i. (\<lambda>j. f j i) \<up> (x i))"
  1869 proof -
  1870   have "\<And>i. {y. \<exists>f'\<in>range f. y = f' i} = range (\<lambda>j. f j i)"
  1871     by auto
  1872   with assms show ?thesis
  1873     by (auto simp add: isoton_def le_fun_def Sup_fun_def SUPR_def)
  1874 qed
  1875 
  1876 lemma isoton_indicator:
  1877   assumes "f \<up> g"
  1878   shows "(\<lambda>i x. f i x * indicator A x) \<up> (\<lambda>x. g x * indicator A x :: pextreal)"
  1879   using assms unfolding isoton_fun_expand by (auto intro!: isoton_cmult_left)
  1880 
  1881 lemma isoton_setsum:
  1882   fixes f :: "'a \<Rightarrow> nat \<Rightarrow> pextreal"
  1883   assumes "finite A" "A \<noteq> {}"
  1884   assumes "\<And> x. x \<in> A \<Longrightarrow> f x \<up> y x"
  1885   shows "(\<lambda> i. (\<Sum> x \<in> A. f x i)) \<up> (\<Sum> x \<in> A. y x)"
  1886 using assms
  1887 proof (induct A rule:finite_ne_induct)
  1888   case singleton thus ?case by auto
  1889 next
  1890   case (insert a A) note asms = this
  1891   hence *: "(\<lambda> i. \<Sum> x \<in> A. f x i) \<up> (\<Sum> x \<in> A. y x)" by auto
  1892   have **: "(\<lambda> i. f a i) \<up> y a" using asms by simp
  1893   have "(\<lambda> i. f a i + (\<Sum> x \<in> A. f x i)) \<up> (y a + (\<Sum> x \<in> A. y x))"
  1894     using * ** isoton_add by auto
  1895   thus "(\<lambda> i. \<Sum> x \<in> insert a A. f x i) \<up> (\<Sum> x \<in> insert a A. y x)"
  1896     using asms by fastsimp
  1897 qed
  1898 
  1899 lemma isoton_Sup:
  1900   assumes "f \<up> u"
  1901   shows "f i \<le> u"
  1902   using le_SUPI[of i UNIV f] assms
  1903   unfolding isoton_def by auto
  1904 
  1905 lemma isoton_mono:
  1906   assumes iso: "x \<up> a" "y \<up> b" and *: "\<And>n. x n \<le> y (N n)"
  1907   shows "a \<le> b"
  1908 proof -
  1909   from iso have "a = (SUP n. x n)" "b = (SUP n. y n)"
  1910     unfolding isoton_def by auto
  1911   with * show ?thesis by (auto intro!: SUP_mono)
  1912 qed
  1913 
  1914 lemma pextreal_le_mult_one_interval:
  1915   fixes x y :: pextreal
  1916   assumes "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
  1917   shows "x \<le> y"
  1918 proof (cases x, cases y)
  1919   assume "x = \<omega>"
  1920   with assms[of "1 / 2"]
  1921   show "x \<le> y" by simp
  1922 next
  1923   fix r p assume *: "y = Real p" "x = Real r" and **: "0 \<le> r" "0 \<le> p"
  1924   have "r \<le> p"
  1925   proof (rule field_le_mult_one_interval)
  1926     fix z :: real assume "0 < z" and "z < 1"
  1927     with assms[of "Real z"]
  1928     show "z * r \<le> p" using ** * by (auto simp: zero_le_mult_iff)
  1929   qed
  1930   thus "x \<le> y" using ** * by simp
  1931 qed simp
  1932 
  1933 lemma pextreal_greater_0[intro]:
  1934   fixes a :: pextreal
  1935   assumes "a \<noteq> 0"
  1936   shows "a > 0"
  1937 using assms apply (cases a) by auto
  1938 
  1939 lemma pextreal_mult_strict_right_mono:
  1940   assumes "a < b" and "0 < c" "c < \<omega>"
  1941   shows "a * c < b * c"
  1942   using assms
  1943   by (cases a, cases b, cases c)
  1944      (auto simp: zero_le_mult_iff pextreal_less_\<omega>)
  1945 
  1946 lemma minus_pextreal_eq2:
  1947   fixes x y z :: pextreal
  1948   assumes "y \<le> x" and "y \<noteq> \<omega>" shows "z = x - y \<longleftrightarrow> z + y = x"
  1949   using assms
  1950   apply (subst eq_commute)
  1951   apply (subst minus_pextreal_eq)
  1952   by (cases x, cases z, auto simp add: ac_simps not_less)
  1953 
  1954 lemma pextreal_diff_eq_diff_imp_eq:
  1955   assumes "a \<noteq> \<omega>" "b \<le> a" "c \<le> a"
  1956   assumes "a - b = a - c"
  1957   shows "b = c"
  1958   using assms
  1959   by (cases a, cases b, cases c) (auto split: split_if_asm)
  1960 
  1961 lemma pextreal_inverse_eq_0: "inverse x = 0 \<longleftrightarrow> x = \<omega>"
  1962   by (cases x) auto
  1963 
  1964 lemma pextreal_mult_inverse:
  1965   "\<lbrakk> x \<noteq> \<omega> ; x \<noteq> 0 \<rbrakk> \<Longrightarrow> x * inverse x = 1"
  1966   by (cases x) auto
  1967 
  1968 lemma pextreal_zero_less_diff_iff:
  1969   fixes a b :: pextreal shows "0 < a - b \<longleftrightarrow> b < a"
  1970   apply (cases a, cases b)
  1971   apply (auto simp: pextreal_noteq_omega_Ex pextreal_less_\<omega>)
  1972   apply (cases b)
  1973   by auto
  1974 
  1975 lemma pextreal_less_Real_Ex:
  1976   fixes a b :: pextreal shows "x < Real r \<longleftrightarrow> (\<exists>p\<ge>0. p < r \<and> x = Real p)"
  1977   by (cases x) auto
  1978 
  1979 lemma open_Real: assumes "open S" shows "open (Real ` ({0..} \<inter> S))"
  1980   unfolding open_pextreal_def apply(rule,rule,rule,rule assms) by auto
  1981 
  1982 lemma pextreal_zero_le_diff:
  1983   fixes a b :: pextreal shows "a - b = 0 \<longleftrightarrow> a \<le> b"
  1984   by (cases a, cases b, simp_all, cases b, auto)
  1985 
  1986 lemma lim_Real[simp]: assumes "\<forall>n. f n \<ge> 0" "m\<ge>0"
  1987   shows "(\<lambda>n. Real (f n)) ----> Real m \<longleftrightarrow> (\<lambda>n. f n) ----> m" (is "?l = ?r")
  1988 proof assume ?l show ?r unfolding Lim_sequentially
  1989   proof safe fix e::real assume e:"e>0"
  1990     note open_ball[of m e] note open_Real[OF this]
  1991     note * = `?l`[unfolded tendsto_def,rule_format,OF this]
  1992     have "eventually (\<lambda>x. Real (f x) \<in> Real ` ({0..} \<inter> ball m e)) sequentially"
  1993       apply(rule *) unfolding image_iff using assms(2) e by auto
  1994     thus "\<exists>N. \<forall>n\<ge>N. dist (f n) m < e" unfolding eventually_sequentially 
  1995       apply safe apply(rule_tac x=N in exI,safe) apply(erule_tac x=n in allE,safe)
  1996     proof- fix n x assume "Real (f n) = Real x" "0 \<le> x"
  1997       hence *:"f n = x" using assms(1) by auto
  1998       assume "x \<in> ball m e" thus "dist (f n) m < e" unfolding *
  1999         by (auto simp add:dist_commute)
  2000     qed qed
  2001 next assume ?r show ?l unfolding tendsto_def eventually_sequentially 
  2002   proof safe fix S assume S:"open S" "Real m \<in> S"
  2003     guess T y using S(1) apply-apply(erule pextreal_openE) . note T=this
  2004     have "m\<in>real ` (S - {\<omega>})" unfolding image_iff 
  2005       apply(rule_tac x="Real m" in bexI) using assms(2) S(2) by auto
  2006     hence "m \<in> T" unfolding T(2)[THEN sym] by auto 
  2007     from `?r`[unfolded tendsto_def eventually_sequentially,rule_format,OF T(1) this]
  2008     guess N .. note N=this[rule_format]
  2009     show "\<exists>N. \<forall>n\<ge>N. Real (f n) \<in> S" apply(rule_tac x=N in exI) 
  2010     proof safe fix n assume n:"N\<le>n"
  2011       have "f n \<in> real ` (S - {\<omega>})" using N[OF n] assms unfolding T(2)[THEN sym] 
  2012         unfolding image_iff apply-apply(rule_tac x="Real (f n)" in bexI)
  2013         unfolding real_Real by auto
  2014       then guess x unfolding image_iff .. note x=this
  2015       show "Real (f n) \<in> S" unfolding x apply(subst Real_real) using x by auto
  2016     qed
  2017   qed
  2018 qed
  2019 
  2020 lemma pextreal_INFI:
  2021   fixes x :: pextreal
  2022   assumes "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i"
  2023   assumes "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> f i) \<Longrightarrow> y \<le> x"
  2024   shows "(INF i:A. f i) = x"
  2025   unfolding INFI_def Inf_pextreal_def
  2026   using assms by (auto intro!: Greatest_equality)
  2027 
  2028 lemma real_of_pextreal_less:"x < y \<Longrightarrow> y\<noteq>\<omega> \<Longrightarrow> real x < real y"
  2029 proof- case goal1
  2030   have *:"y = Real (real y)" "x = Real (real x)" using goal1 Real_real by auto
  2031   show ?case using goal1 apply- apply(subst(asm) *(1))apply(subst(asm) *(2))
  2032     unfolding pextreal_less by auto
  2033 qed
  2034 
  2035 lemma not_less_omega[simp]:"\<not> x < \<omega> \<longleftrightarrow> x = \<omega>"
  2036   by (metis antisym_conv3 pextreal_less(3)) 
  2037 
  2038 lemma Real_real': assumes "x\<noteq>\<omega>" shows "Real (real x) = x"
  2039 proof- have *:"(THE r. 0 \<le> r \<and> x = Real r) = real x"
  2040     apply(rule the_equality) using assms unfolding Real_real by auto
  2041   have "Real (THE r. 0 \<le> r \<and> x = Real r) = x" unfolding *
  2042     using assms unfolding Real_real by auto
  2043   thus ?thesis unfolding real_of_pextreal_def of_pextreal_def
  2044     unfolding pextreal_case_def using assms by auto
  2045 qed 
  2046 
  2047 lemma Real_less_plus_one:"Real x < Real (max (x + 1) 1)" 
  2048   unfolding pextreal_less by auto
  2049 
  2050 lemma Lim_omega: "f ----> \<omega> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. f n \<ge> Real B)" (is "?l = ?r")
  2051 proof assume ?r show ?l apply(rule topological_tendstoI)
  2052     unfolding eventually_sequentially
  2053   proof- fix S assume "open S" "\<omega> \<in> S"
  2054     from open_omega[OF this] guess B .. note B=this
  2055     from `?r`[rule_format,of "(max B 0)+1"] guess N .. note N=this
  2056     show "\<exists>N. \<forall>n\<ge>N. f n \<in> S" apply(rule_tac x=N in exI)
  2057     proof safe case goal1 
  2058       have "Real B < Real ((max B 0) + 1)" by auto
  2059       also have "... \<le> f n" using goal1 N by auto
  2060       finally show ?case using B by fastsimp
  2061     qed
  2062   qed
  2063 next assume ?l show ?r
  2064   proof fix B::real have "open {Real B<..}" "\<omega> \<in> {Real B<..}" by auto
  2065     from topological_tendstoD[OF `?l` this,unfolded eventually_sequentially]
  2066     guess N .. note N=this
  2067     show "\<exists>N. \<forall>n\<ge>N. Real B \<le> f n" apply(rule_tac x=N in exI) using N by auto
  2068   qed
  2069 qed
  2070 
  2071 lemma Lim_bounded_omgea: assumes lim:"f ----> l" and "\<And>n. f n \<le> Real B" shows "l \<noteq> \<omega>"
  2072 proof(rule ccontr,unfold not_not) let ?B = "max (B + 1) 1" assume as:"l=\<omega>"
  2073   from lim[unfolded this Lim_omega,rule_format,of "?B"]
  2074   guess N .. note N=this[rule_format,OF le_refl]
  2075   hence "Real ?B \<le> Real B" using assms(2)[of N] by(rule order_trans) 
  2076   hence "Real ?B < Real ?B" using Real_less_plus_one[of B] by(rule le_less_trans)
  2077   thus False by auto
  2078 qed
  2079 
  2080 lemma incseq_le_pextreal: assumes inc: "\<And>n m. n\<ge>m \<Longrightarrow> X n \<ge> X m"
  2081   and lim: "X ----> (L::pextreal)" shows "X n \<le> L"
  2082 proof(cases "L = \<omega>")
  2083   case False have "\<forall>n. X n \<noteq> \<omega>"
  2084   proof(rule ccontr,unfold not_all not_not,safe)
  2085     case goal1 hence "\<forall>n\<ge>x. X n = \<omega>" using inc[of x] by auto
  2086     hence "X ----> \<omega>" unfolding tendsto_def eventually_sequentially
  2087       apply safe apply(rule_tac x=x in exI) by auto
  2088     note Lim_unique[OF trivial_limit_sequentially this lim]
  2089     with False show False by auto
  2090   qed note * =this[rule_format]
  2091 
  2092   have **:"\<forall>m n. m \<le> n \<longrightarrow> Real (real (X m)) \<le> Real (real (X n))"
  2093     unfolding Real_real using * inc by auto
  2094   have "real (X n) \<le> real L" apply-apply(rule incseq_le) defer
  2095     apply(subst lim_Real[THEN sym]) apply(rule,rule,rule)
  2096     unfolding Real_real'[OF *] Real_real'[OF False] 
  2097     unfolding incseq_def using ** lim by auto
  2098   hence "Real (real (X n)) \<le> Real (real L)" by auto
  2099   thus ?thesis unfolding Real_real using * False by auto
  2100 qed auto
  2101 
  2102 lemma SUP_Lim_pextreal: assumes "\<And>n m. n\<ge>m \<Longrightarrow> f n \<ge> f m" "f ----> l"
  2103   shows "(SUP n. f n) = (l::pextreal)" unfolding SUPR_def Sup_pextreal_def
  2104 proof (safe intro!: Least_equality)
  2105   fix n::nat show "f n \<le> l" apply(rule incseq_le_pextreal)
  2106     using assms by auto
  2107 next fix y assume y:"\<forall>x\<in>range f. x \<le> y" show "l \<le> y"
  2108   proof(rule ccontr,cases "y=\<omega>",unfold not_le)
  2109     case False assume as:"y < l"
  2110     have l:"l \<noteq> \<omega>" apply(rule Lim_bounded_omgea[OF assms(2), of "real y"])
  2111       using False y unfolding Real_real by auto
  2112 
  2113     have yl:"real y < real l" using as apply-
  2114       apply(subst(asm) Real_real'[THEN sym,OF `y\<noteq>\<omega>`])
  2115       apply(subst(asm) Real_real'[THEN sym,OF `l\<noteq>\<omega>`]) 
  2116       unfolding pextreal_less apply(subst(asm) if_P) by auto
  2117     hence "y + (y - l) * Real (1 / 2) < l" apply-
  2118       apply(subst Real_real'[THEN sym,OF `y\<noteq>\<omega>`]) apply(subst(2) Real_real'[THEN sym,OF `y\<noteq>\<omega>`])
  2119       apply(subst Real_real'[THEN sym,OF `l\<noteq>\<omega>`]) apply(subst(2) Real_real'[THEN sym,OF `l\<noteq>\<omega>`]) by auto
  2120     hence *:"l \<in> {y + (y - l) / 2<..}" by auto
  2121     have "open {y + (y-l)/2 <..}" by auto
  2122     note topological_tendstoD[OF assms(2) this *]
  2123     from this[unfolded eventually_sequentially] guess N .. note this[rule_format, of N]
  2124     hence "y + (y - l) * Real (1 / 2) < y" using y[rule_format,of "f N"] by auto
  2125     hence "Real (real y) + (Real (real y) - Real (real l)) * Real (1 / 2) < Real (real y)"
  2126       unfolding Real_real using `y\<noteq>\<omega>` `l\<noteq>\<omega>` by auto
  2127     thus False using yl by auto
  2128   qed auto
  2129 qed
  2130 
  2131 lemma Real_max':"Real x = Real (max x 0)" 
  2132 proof(cases "x < 0") case True
  2133   hence *:"max x 0 = 0" by auto
  2134   show ?thesis unfolding * using True by auto
  2135 qed auto
  2136 
  2137 lemma lim_pextreal_increasing: assumes "\<forall>n m. n\<ge>m \<longrightarrow> f n \<ge> f m"
  2138   obtains l where "f ----> (l::pextreal)"
  2139 proof(cases "\<exists>B. \<forall>n. f n < Real B")
  2140   case False thus thesis apply- apply(rule that[of \<omega>]) unfolding Lim_omega not_ex not_all
  2141     apply safe apply(erule_tac x=B in allE,safe) apply(rule_tac x=x in exI,safe)
  2142     apply(rule order_trans[OF _ assms[rule_format]]) by auto
  2143 next case True then guess B .. note B = this[rule_format]
  2144   hence *:"\<And>n. f n < \<omega>" apply-apply(rule less_le_trans,assumption) by auto
  2145   have *:"\<And>n. f n \<noteq> \<omega>" proof- case goal1 show ?case using *[of n] by auto qed
  2146   have B':"\<And>n. real (f n) \<le> max 0 B" proof- case goal1 thus ?case
  2147       using B[of n] apply-apply(subst(asm) Real_real'[THEN sym]) defer
  2148       apply(subst(asm)(2) Real_max') unfolding pextreal_less apply(subst(asm) if_P) using *[of n] by auto
  2149   qed
  2150   have "\<exists>l. (\<lambda>n. real (f n)) ----> l" apply(rule Topology_Euclidean_Space.bounded_increasing_convergent)
  2151   proof safe show "bounded {real (f n) |n. True}"
  2152       unfolding bounded_def apply(rule_tac x=0 in exI,rule_tac x="max 0 B" in exI)
  2153       using B' unfolding dist_norm by auto
  2154     fix n::nat have "Real (real (f n)) \<le> Real (real (f (Suc n)))"
  2155       using assms[rule_format,of n "Suc n"] apply(subst Real_real)+
  2156       using *[of n] *[of "Suc n"] by fastsimp
  2157     thus "real (f n) \<le> real (f (Suc n))" by auto
  2158   qed then guess l .. note l=this
  2159   have "0 \<le> l" apply(rule LIMSEQ_le_const[OF l])
  2160     by(rule_tac x=0 in exI,auto)
  2161 
  2162   thus ?thesis apply-apply(rule that[of "Real l"])
  2163     using l apply-apply(subst(asm) lim_Real[THEN sym]) prefer 3
  2164     unfolding Real_real using * by auto
  2165 qed
  2166 
  2167 lemma setsum_neq_omega: assumes "finite s" "\<And>x. x \<in> s \<Longrightarrow> f x \<noteq> \<omega>"
  2168   shows "setsum f s \<noteq> \<omega>" using assms
  2169 proof induct case (insert x s)
  2170   show ?case unfolding setsum.insert[OF insert(1-2)] 
  2171     using insert by auto
  2172 qed auto
  2173 
  2174 
  2175 lemma real_Real': "0 \<le> x \<Longrightarrow> real (Real x) = x"
  2176   unfolding real_Real by auto
  2177 
  2178 lemma real_pextreal_pos[intro]:
  2179   assumes "x \<noteq> 0" "x \<noteq> \<omega>"
  2180   shows "real x > 0"
  2181   apply(subst real_Real'[THEN sym,of 0]) defer
  2182   apply(rule real_of_pextreal_less) using assms by auto
  2183 
  2184 lemma Lim_omega_gt: "f ----> \<omega> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. f n > Real B)" (is "?l = ?r")
  2185 proof assume ?l thus ?r unfolding Lim_omega apply safe
  2186     apply(erule_tac x="max B 0 +1" in allE,safe)
  2187     apply(rule_tac x=N in exI,safe) apply(erule_tac x=n in allE,safe)
  2188     apply(rule_tac y="Real (max B 0 + 1)" in less_le_trans) by auto
  2189 next assume ?r thus ?l unfolding Lim_omega apply safe
  2190     apply(erule_tac x=B in allE,safe) apply(rule_tac x=N in exI,safe) by auto
  2191 qed
  2192 
  2193 lemma pextreal_minus_le_cancel:
  2194   fixes a b c :: pextreal
  2195   assumes "b \<le> a"
  2196   shows "c - a \<le> c - b"
  2197   using assms by (cases a, cases b, cases c, simp, simp, simp, cases b, cases c, simp_all)
  2198 
  2199 lemma pextreal_minus_\<omega>[simp]: "x - \<omega> = 0" by (cases x) simp_all
  2200 
  2201 lemma pextreal_minus_mono[intro]: "a - x \<le> (a::pextreal)"
  2202 proof- have "a - x \<le> a - 0"
  2203     apply(rule pextreal_minus_le_cancel) by auto
  2204   thus ?thesis by auto
  2205 qed
  2206 
  2207 lemma pextreal_minus_eq_\<omega>[simp]: "x - y = \<omega> \<longleftrightarrow> (x = \<omega> \<and> y \<noteq> \<omega>)"
  2208   by (cases x, cases y) (auto, cases y, auto)
  2209 
  2210 lemma pextreal_less_minus_iff:
  2211   fixes a b c :: pextreal
  2212   shows "a < b - c \<longleftrightarrow> c + a < b"
  2213   by (cases c, cases a, cases b, auto)
  2214 
  2215 lemma pextreal_minus_less_iff:
  2216   fixes a b c :: pextreal shows "a - c < b \<longleftrightarrow> (0 < b \<and> (c \<noteq> \<omega> \<longrightarrow> a < b + c))"
  2217   by (cases c, cases a, cases b, auto)
  2218 
  2219 lemma pextreal_le_minus_iff:
  2220   fixes a b c :: pextreal
  2221   shows "a \<le> c - b \<longleftrightarrow> ((c \<le> b \<longrightarrow> a = 0) \<and> (b < c \<longrightarrow> a + b \<le> c))"
  2222   by (cases a, cases c, cases b, auto simp: pextreal_noteq_omega_Ex)
  2223 
  2224 lemma pextreal_minus_le_iff:
  2225   fixes a b c :: pextreal
  2226   shows "a - c \<le> b \<longleftrightarrow> (c \<le> a \<longrightarrow> a \<le> b + c)"
  2227   by (cases a, cases c, cases b, auto simp: pextreal_noteq_omega_Ex)
  2228 
  2229 lemmas pextreal_minus_order = pextreal_minus_le_iff pextreal_minus_less_iff pextreal_le_minus_iff pextreal_less_minus_iff
  2230 
  2231 lemma pextreal_minus_strict_mono:
  2232   assumes "a > 0" "x > 0" "a\<noteq>\<omega>"
  2233   shows "a - x < (a::pextreal)"
  2234   using assms by(cases x, cases a, auto)
  2235 
  2236 lemma pextreal_minus':
  2237   "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)"
  2238   by (auto simp: minus_pextreal_eq not_less)
  2239 
  2240 lemma pextreal_minus_plus:
  2241   "x \<le> (a::pextreal) \<Longrightarrow> a - x + x = a"
  2242   by (cases a, cases x) auto
  2243 
  2244 lemma pextreal_cancel_plus_minus: "b \<noteq> \<omega> \<Longrightarrow> a + b - b = a"
  2245   by (cases a, cases b) auto
  2246 
  2247 lemma pextreal_minus_le_cancel_right:
  2248   fixes a b c :: pextreal
  2249   assumes "a \<le> b" "c \<le> a"
  2250   shows "a - c \<le> b - c"
  2251   using assms by (cases a, cases b, cases c, auto, cases c, auto)
  2252 
  2253 lemma real_of_pextreal_setsum':
  2254   assumes "\<forall>x \<in> S. f x \<noteq> \<omega>"
  2255   shows "(\<Sum>x\<in>S. real (f x)) = real (setsum f S)"
  2256 proof cases
  2257   assume "finite S"
  2258   from this assms show ?thesis
  2259     by induct (simp_all add: real_of_pextreal_add setsum_\<omega>)
  2260 qed simp
  2261 
  2262 lemma Lim_omega_pos: "f ----> \<omega> \<longleftrightarrow> (\<forall>B>0. \<exists>N. \<forall>n\<ge>N. f n \<ge> Real B)" (is "?l = ?r")
  2263   unfolding Lim_omega apply safe defer
  2264   apply(erule_tac x="max 1 B" in allE) apply safe defer
  2265   apply(rule_tac x=N in exI,safe) apply(erule_tac x=n in allE,safe)
  2266   apply(rule_tac y="Real (max 1 B)" in order_trans) by auto
  2267 
  2268 lemma pextreal_LimI_finite:
  2269   assumes "x \<noteq> \<omega>" "\<And>r. 0 < r \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. u n < x + r \<and> x < u n + r"
  2270   shows "u ----> x"
  2271 proof (rule topological_tendstoI, unfold eventually_sequentially)
  2272   fix S assume "open S" "x \<in> S"
  2273   then obtain A where "open A" and A_eq: "Real ` (A \<inter> {0..}) = S - {\<omega>}" by (auto elim!: pextreal_openE)
  2274   then have "x \<in> Real ` (A \<inter> {0..})" using `x \<in> S` `x \<noteq> \<omega>` by auto
  2275   then have "real x \<in> A" by auto
  2276   then obtain r where "0 < r" and dist: "\<And>y. dist y (real x) < r \<Longrightarrow> y \<in> A"
  2277     using `open A` unfolding open_real_def by auto
  2278   then obtain n where
  2279     upper: "\<And>N. n \<le> N \<Longrightarrow> u N < x + Real r" and
  2280     lower: "\<And>N. n \<le> N \<Longrightarrow> x < u N + Real r" using assms(2)[of "Real r"] by auto
  2281   show "\<exists>N. \<forall>n\<ge>N. u n \<in> S"
  2282   proof (safe intro!: exI[of _ n])
  2283     fix N assume "n \<le> N"
  2284     from upper[OF this] `x \<noteq> \<omega>` `0 < r`
  2285     have "u N \<noteq> \<omega>" by (force simp: pextreal_noteq_omega_Ex)
  2286     with `x \<noteq> \<omega>` `0 < r` lower[OF `n \<le> N`] upper[OF `n \<le> N`]
  2287     have "dist (real (u N)) (real x) < r" "u N \<noteq> \<omega>"
  2288       by (auto simp: pextreal_noteq_omega_Ex dist_real_def abs_diff_less_iff field_simps)
  2289     from dist[OF this(1)]
  2290     have "u N \<in> Real ` (A \<inter> {0..})" using `u N \<noteq> \<omega>`
  2291       by (auto intro!: image_eqI[of _ _ "real (u N)"] simp: pextreal_noteq_omega_Ex Real_real)
  2292     thus "u N \<in> S" using A_eq by simp
  2293   qed
  2294 qed
  2295 
  2296 lemma real_Real_max:"real (Real x) = max x 0"
  2297   unfolding real_Real by auto
  2298 
  2299 lemma Sup_lim:
  2300   assumes "\<forall>n. b n \<in> s" "b ----> (a::pextreal)"
  2301   shows "a \<le> Sup s"
  2302 proof(rule ccontr,unfold not_le)
  2303   assume as:"Sup s < a" hence om:"Sup s \<noteq> \<omega>" by auto
  2304   have s:"s \<noteq> {}" using assms by auto
  2305   { presume *:"\<forall>n. b n < a \<Longrightarrow> False"
  2306     show False apply(cases,rule *,assumption,unfold not_all not_less)
  2307     proof- case goal1 then guess n .. note n=this
  2308       thus False using complete_lattice_class.Sup_upper[OF assms(1)[rule_format,of n]]
  2309         using as by auto
  2310     qed
  2311   } assume b:"\<forall>n. b n < a"
  2312   show False
  2313   proof(cases "a = \<omega>")
  2314     case False have *:"a - Sup s > 0" 
  2315       using False as by(auto simp: pextreal_zero_le_diff)
  2316     have "(a - Sup s) / 2 \<le> a / 2" unfolding divide_pextreal_def
  2317       apply(rule mult_right_mono) by auto
  2318     also have "... = Real (real (a / 2))" apply(rule Real_real'[THEN sym])
  2319       using False by auto
  2320     also have "... < Real (real a)" unfolding pextreal_less using as False
  2321       by(auto simp add: real_of_pextreal_mult[THEN sym])
  2322     also have "... = a" apply(rule Real_real') using False by auto
  2323     finally have asup:"a > (a - Sup s) / 2" .
  2324     have "\<exists>n. a - b n < (a - Sup s) / 2"
  2325     proof(rule ccontr,unfold not_ex not_less)
  2326       case goal1
  2327       have "(a - Sup s) * Real (1 / 2)  > 0" 
  2328         using * by auto
  2329       hence "a - (a - Sup s) * Real (1 / 2) < a"
  2330         apply-apply(rule pextreal_minus_strict_mono)
  2331         using False * by auto
  2332       hence *:"a \<in> {a - (a - Sup s) / 2<..}"using asup by auto 
  2333       note topological_tendstoD[OF assms(2) open_pextreal_greaterThan,OF *]
  2334       from this[unfolded eventually_sequentially] guess n .. 
  2335       note n = this[rule_format,of n] 
  2336       have "b n + (a - Sup s) / 2 \<le> a" 
  2337         using add_right_mono[OF goal1[rule_format,of n],of "b n"]
  2338         unfolding pextreal_minus_plus[OF less_imp_le[OF b[rule_format]]]
  2339         by(auto simp: add_commute)
  2340       hence "b n \<le> a - (a - Sup s) / 2" unfolding pextreal_le_minus_iff
  2341         using asup by auto
  2342       hence "b n \<notin> {a - (a - Sup s) / 2<..}" by auto
  2343       thus False using n by auto
  2344     qed
  2345     then guess n .. note n = this
  2346     have "Sup s < a - (a - Sup s) / 2"
  2347       using False as om by (cases a) (auto simp: pextreal_noteq_omega_Ex field_simps)
  2348     also have "... \<le> b n"
  2349     proof- note add_right_mono[OF less_imp_le[OF n],of "b n"]
  2350       note this[unfolded pextreal_minus_plus[OF less_imp_le[OF b[rule_format]]]]
  2351       hence "a - (a - Sup s) / 2 \<le> (a - Sup s) / 2 + b n - (a - Sup s) / 2"
  2352         apply(rule pextreal_minus_le_cancel_right) using asup by auto
  2353       also have "... = b n + (a - Sup s) / 2 - (a - Sup s) / 2" 
  2354         by(auto simp add: add_commute)
  2355       also have "... = b n" apply(subst pextreal_cancel_plus_minus)
  2356       proof(rule ccontr,unfold not_not) case goal1
  2357         show ?case using asup unfolding goal1 by auto 
  2358       qed auto
  2359       finally show ?thesis .
  2360     qed     
  2361     finally show False
  2362       using complete_lattice_class.Sup_upper[OF assms(1)[rule_format,of n]] by auto  
  2363   next case True
  2364     from assms(2)[unfolded True Lim_omega_gt,rule_format,of "real (Sup s)"]
  2365     guess N .. note N = this[rule_format,of N]
  2366     thus False using complete_lattice_class.Sup_upper[OF assms(1)[rule_format,of N]] 
  2367       unfolding Real_real using om by auto
  2368   qed qed
  2369 
  2370 lemma Sup_mono_lim:
  2371   assumes "\<forall>a\<in>A. \<exists>b. \<forall>n. b n \<in> B \<and> b ----> (a::pextreal)"
  2372   shows "Sup A \<le> Sup B"
  2373   unfolding Sup_le_iff apply(rule) apply(drule assms[rule_format]) apply safe
  2374   apply(rule_tac b=b in Sup_lim) by auto
  2375 
  2376 lemma pextreal_less_add:
  2377   assumes "x \<noteq> \<omega>" "a < b"
  2378   shows "x + a < x + b"
  2379   using assms by (cases a, cases b, cases x) auto
  2380 
  2381 lemma SUPR_lim:
  2382   assumes "\<forall>n. b n \<in> B" "(\<lambda>n. f (b n)) ----> (f a::pextreal)"
  2383   shows "f a \<le> SUPR B f"
  2384   unfolding SUPR_def apply(rule Sup_lim[of "\<lambda>n. f (b n)"])
  2385   using assms by auto
  2386 
  2387 lemma SUP_\<omega>_imp:
  2388   assumes "(SUP i. f i) = \<omega>"
  2389   shows "\<exists>i. Real x < f i"
  2390 proof (rule ccontr)
  2391   assume "\<not> ?thesis" hence "\<And>i. f i \<le> Real x" by (simp add: not_less)
  2392   hence "(SUP i. f i) \<le> Real x" unfolding SUP_le_iff by auto
  2393   with assms show False by auto
  2394 qed
  2395 
  2396 lemma SUPR_mono_lim:
  2397   assumes "\<forall>a\<in>A. \<exists>b. \<forall>n. b n \<in> B \<and> (\<lambda>n. f (b n)) ----> (f a::pextreal)"
  2398   shows "SUPR A f \<le> SUPR B f"
  2399   unfolding SUPR_def apply(rule Sup_mono_lim)
  2400   apply safe apply(drule assms[rule_format],safe)
  2401   apply(rule_tac x="\<lambda>n. f (b n)" in exI) by auto
  2402 
  2403 lemma real_0_imp_eq_0:
  2404   assumes "x \<noteq> \<omega>" "real x = 0"
  2405   shows "x = 0"
  2406 using assms by (cases x) auto
  2407 
  2408 lemma SUPR_mono:
  2409   assumes "\<forall>a\<in>A. \<exists>b\<in>B. f b \<ge> f a"
  2410   shows "SUPR A f \<le> SUPR B f"
  2411   unfolding SUPR_def apply(rule Sup_mono)
  2412   using assms by auto
  2413 
  2414 lemma less_add_Real:
  2415   fixes x :: real
  2416   fixes a b :: pextreal
  2417   assumes "x \<ge> 0" "a < b"
  2418   shows "a + Real x < b + Real x"
  2419 using assms by (cases a, cases b) auto
  2420 
  2421 lemma le_add_Real:
  2422   fixes x :: real
  2423   fixes a b :: pextreal
  2424   assumes "x \<ge> 0" "a \<le> b"
  2425   shows "a + Real x \<le> b + Real x"
  2426 using assms by (cases a, cases b) auto
  2427 
  2428 lemma le_imp_less_pextreal:
  2429   fixes x :: pextreal
  2430   assumes "x > 0" "a + x \<le> b" "a \<noteq> \<omega>"
  2431   shows "a < b"
  2432 using assms by (cases x, cases a, cases b) auto
  2433 
  2434 lemma pextreal_INF_minus:
  2435   fixes f :: "nat \<Rightarrow> pextreal"
  2436   assumes "c \<noteq> \<omega>"
  2437   shows "(INF i. c - f i) = c - (SUP i. f i)"
  2438 proof (cases "SUP i. f i")
  2439   case infinite
  2440   from `c \<noteq> \<omega>` obtain x where [simp]: "c = Real x" by (cases c) auto
  2441   from SUP_\<omega>_imp[OF infinite] obtain i where "Real x < f i" by auto
  2442   have "(INF i. c - f i) \<le> c - f i"
  2443     by (auto intro!: complete_lattice_class.INF_leI)
  2444   also have "\<dots> = 0" using `Real x < f i` by (auto simp: minus_pextreal_eq)
  2445   finally show ?thesis using infinite by auto
  2446 next
  2447   case (preal r)
  2448   from `c \<noteq> \<omega>` obtain x where c: "c = Real x" by (cases c) auto
  2449 
  2450   show ?thesis unfolding c
  2451   proof (rule pextreal_INFI)
  2452     fix i have "f i \<le> (SUP i. f i)" by (rule le_SUPI) simp
  2453     thus "Real x - (SUP i. f i) \<le> Real x - f i" by (rule pextreal_minus_le_cancel)
  2454   next
  2455     fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> y \<le> Real x - f i"
  2456     from this[of 0] obtain p where p: "y = Real p" "0 \<le> p"
  2457       by (cases "f 0", cases y, auto split: split_if_asm)
  2458     hence "\<And>i. Real p \<le> Real x - f i" using * by auto
  2459     hence *: "\<And>i. Real x \<le> f i \<Longrightarrow> Real p = 0"
  2460       "\<And>i. f i < Real x \<Longrightarrow> Real p + f i \<le> Real x"
  2461       unfolding pextreal_le_minus_iff by auto
  2462     show "y \<le> Real x - (SUP i. f i)" unfolding p pextreal_le_minus_iff
  2463     proof safe
  2464       assume x_less: "Real x \<le> (SUP i. f i)"
  2465       show "Real p = 0"
  2466       proof (rule ccontr)
  2467         assume "Real p \<noteq> 0"
  2468         hence "0 < Real p" by auto
  2469         from Sup_close[OF this, of "range f"]
  2470         obtain i where e: "(SUP i. f i) < f i + Real p"
  2471           using preal unfolding SUPR_def by auto
  2472         hence "Real x \<le> f i + Real p" using x_less by auto
  2473         show False
  2474         proof cases
  2475           assume "\<forall>i. f i < Real x"
  2476           hence "Real p + f i \<le> Real x" using * by auto
  2477           hence "f i + Real p \<le> (SUP i. f i)" using x_less by (auto simp: field_simps)
  2478           thus False using e by auto
  2479         next
  2480           assume "\<not> (\<forall>i. f i < Real x)"
  2481           then obtain i where "Real x \<le> f i" by (auto simp: not_less)
  2482           from *(1)[OF this] show False using `Real p \<noteq> 0` by auto
  2483         qed
  2484       qed
  2485     next
  2486       have "\<And>i. f i \<le> (SUP i. f i)" by (rule complete_lattice_class.le_SUPI) auto
  2487       also assume "(SUP i. f i) < Real x"
  2488       finally have "\<And>i. f i < Real x" by auto
  2489       hence *: "\<And>i. Real p + f i \<le> Real x" using * by auto
  2490       have "Real p \<le> Real x" using *[of 0] by (cases "f 0") (auto split: split_if_asm)
  2491 
  2492       have SUP_eq: "(SUP i. f i) \<le> Real x - Real p"
  2493       proof (rule SUP_leI)
  2494         fix i show "f i \<le> Real x - Real p" unfolding pextreal_le_minus_iff
  2495         proof safe
  2496           assume "Real x \<le> Real p"
  2497           with *[of i] show "f i = 0"
  2498             by (cases "f i") (auto split: split_if_asm)
  2499         next
  2500           assume "Real p < Real x"
  2501           show "f i + Real p \<le> Real x" using * by (auto simp: field_simps)
  2502         qed
  2503       qed
  2504 
  2505       show "Real p + (SUP i. f i) \<le> Real x"
  2506       proof cases
  2507         assume "Real x \<le> Real p"
  2508         with `Real p \<le> Real x` have [simp]: "Real p = Real x" by (rule antisym)
  2509         { fix i have "f i = 0" using *[of i] by (cases "f i") (auto split: split_if_asm) }
  2510         hence "(SUP i. f i) \<le> 0" by (auto intro!: SUP_leI)
  2511         thus ?thesis by simp
  2512       next
  2513         assume "\<not> Real x \<le> Real p" hence "Real p < Real x" unfolding not_le .
  2514         with SUP_eq show ?thesis unfolding pextreal_le_minus_iff by (auto simp: field_simps)
  2515       qed
  2516     qed
  2517   qed
  2518 qed
  2519 
  2520 lemma pextreal_SUP_minus:
  2521   fixes f :: "nat \<Rightarrow> pextreal"
  2522   shows "(SUP i. c - f i) = c - (INF i. f i)"
  2523 proof (rule pextreal_SUPI)
  2524   fix i have "(INF i. f i) \<le> f i" by (rule INF_leI) simp
  2525   thus "c - f i \<le> c - (INF i. f i)" by (rule pextreal_minus_le_cancel)
  2526 next
  2527   fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> c - f i \<le> y"
  2528   show "c - (INF i. f i) \<le> y"
  2529   proof (cases y)
  2530     case (preal p)
  2531 
  2532     show ?thesis unfolding pextreal_minus_le_iff preal
  2533     proof safe
  2534       assume INF_le_x: "(INF i. f i) \<le> c"
  2535       from * have *: "\<And>i. f i \<le> c \<Longrightarrow> c \<le> Real p + f i"
  2536         unfolding pextreal_minus_le_iff preal by auto
  2537 
  2538       have INF_eq: "c - Real p \<le> (INF i. f i)"
  2539       proof (rule le_INFI)
  2540         fix i show "c - Real p \<le> f i" unfolding pextreal_minus_le_iff
  2541         proof safe
  2542           assume "Real p \<le> c"
  2543           show "c \<le> f i + Real p"
  2544           proof cases
  2545             assume "f i \<le> c" from *[OF this]
  2546             show ?thesis by (simp add: field_simps)
  2547           next
  2548             assume "\<not> f i \<le> c"
  2549             hence "c \<le> f i" by auto
  2550             also have "\<dots> \<le> f i + Real p" by auto
  2551             finally show ?thesis .
  2552           qed
  2553         qed
  2554       qed
  2555 
  2556       show "c \<le> Real p + (INF i. f i)"
  2557       proof cases
  2558         assume "Real p \<le> c"
  2559         with INF_eq show ?thesis unfolding pextreal_minus_le_iff by (auto simp: field_simps)
  2560       next
  2561         assume "\<not> Real p \<le> c"
  2562         hence "c \<le> Real p" by auto
  2563         also have "Real p \<le> Real p + (INF i. f i)" by auto
  2564         finally show ?thesis .
  2565       qed
  2566     qed
  2567   qed simp
  2568 qed
  2569 
  2570 lemma pextreal_le_minus_imp_0:
  2571   fixes a b :: pextreal
  2572   shows "a \<le> a - b \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> a \<noteq> \<omega> \<Longrightarrow> b = 0"
  2573   by (cases a, cases b, auto split: split_if_asm)
  2574 
  2575 lemma lim_INF_eq_lim_SUP:
  2576   fixes X :: "nat \<Rightarrow> real"
  2577   assumes "\<And>i. 0 \<le> X i" and "0 \<le> x"
  2578   and lim_INF: "(SUP n. INF m. Real (X (n + m))) = Real x" (is "(SUP n. ?INF n) = _")
  2579   and lim_SUP: "(INF n. SUP m. Real (X (n + m))) = Real x" (is "(INF n. ?SUP n) = _")
  2580   shows "X ----> x"
  2581 proof (rule LIMSEQ_I)
  2582   fix r :: real assume "0 < r"
  2583   hence "0 \<le> r" by auto
  2584   from Sup_close[of "Real r" "range ?INF"]
  2585   obtain n where inf: "Real x < ?INF n + Real r"
  2586     unfolding SUPR_def lim_INF[unfolded SUPR_def] using `0 < r` by auto
  2587 
  2588   from Inf_close[of "range ?SUP" "Real r"]
  2589   obtain n' where sup: "?SUP n' < Real x + Real r"
  2590     unfolding INFI_def lim_SUP[unfolded INFI_def] using `0 < r` by auto
  2591 
  2592   show "\<exists>N. \<forall>n\<ge>N. norm (X n - x) < r"
  2593   proof (safe intro!: exI[of _ "max n n'"])
  2594     fix m assume "max n n' \<le> m" hence "n \<le> m" "n' \<le> m" by auto
  2595 
  2596     note inf
  2597     also have "?INF n + Real r \<le> Real (X (n + (m - n))) + Real r"
  2598       by (rule le_add_Real, auto simp: `0 \<le> r` intro: INF_leI)
  2599     finally have up: "x < X m + r"
  2600       using `0 \<le> X m` `0 \<le> x` `0 \<le> r` `n \<le> m` by auto
  2601 
  2602     have "Real (X (n' + (m - n'))) \<le> ?SUP n'"
  2603       by (auto simp: `0 \<le> r` intro: le_SUPI)
  2604     also note sup
  2605     finally have down: "X m < x + r"
  2606       using `0 \<le> X m` `0 \<le> x` `0 \<le> r` `n' \<le> m` by auto
  2607 
  2608     show "norm (X m - x) < r" using up down by auto
  2609   qed
  2610 qed
  2611 
  2612 lemma Sup_countable_SUPR:
  2613   assumes "Sup A \<noteq> \<omega>" "A \<noteq> {}"
  2614   shows "\<exists> f::nat \<Rightarrow> pextreal. range f \<subseteq> A \<and> Sup A = SUPR UNIV f"
  2615 proof -
  2616   have "\<And>n. 0 < 1 / (of_nat n :: pextreal)" by auto
  2617   from Sup_close[OF this assms]
  2618   have "\<forall>n. \<exists>x. x \<in> A \<and> Sup A < x + 1 / of_nat n" by blast
  2619   from choice[OF this] obtain f where "range f \<subseteq> A" and
  2620     epsilon: "\<And>n. Sup A < f n + 1 / of_nat n" by blast
  2621   have "SUPR UNIV f = Sup A"
  2622   proof (rule pextreal_SUPI)
  2623     fix i show "f i \<le> Sup A" using `range f \<subseteq> A`
  2624       by (auto intro!: complete_lattice_class.Sup_upper)
  2625   next
  2626     fix y assume bound: "\<And>i. i \<in> UNIV \<Longrightarrow> f i \<le> y"
  2627     show "Sup A \<le> y"
  2628     proof (rule pextreal_le_epsilon)
  2629       fix e :: pextreal assume "0 < e"
  2630       show "Sup A \<le> y + e"
  2631       proof (cases e)
  2632         case (preal r)
  2633         hence "0 < r" using `0 < e` by auto
  2634         then obtain n where *: "inverse (of_nat n) < r" "0 < n"
  2635           using ex_inverse_of_nat_less by auto
  2636         have "Sup A \<le> f n + 1 / of_nat n" using epsilon[of n] by auto
  2637         also have "1 / of_nat n \<le> e" using preal * by (auto simp: real_eq_of_nat)
  2638         with bound have "f n + 1 / of_nat n \<le> y + e" by (rule add_mono) simp
  2639         finally show "Sup A \<le> y + e" .
  2640       qed simp
  2641     qed
  2642   qed
  2643   with `range f \<subseteq> A` show ?thesis by (auto intro!: exI[of _ f])
  2644 qed
  2645 
  2646 lemma SUPR_countable_SUPR:
  2647   assumes "SUPR A g \<noteq> \<omega>" "A \<noteq> {}"
  2648   shows "\<exists> f::nat \<Rightarrow> pextreal. range f \<subseteq> g`A \<and> SUPR A g = SUPR UNIV f"
  2649 proof -
  2650   have "Sup (g`A) \<noteq> \<omega>" "g`A \<noteq> {}" using assms unfolding SUPR_def by auto
  2651   from Sup_countable_SUPR[OF this]
  2652   show ?thesis unfolding SUPR_def .
  2653 qed
  2654 
  2655 lemma pextreal_setsum_subtractf:
  2656   assumes "\<And>i. i\<in>A \<Longrightarrow> g i \<le> f i" and "\<And>i. i\<in>A \<Longrightarrow> f i \<noteq> \<omega>"
  2657   shows "(\<Sum>i\<in>A. f i - g i) = (\<Sum>i\<in>A. f i) - (\<Sum>i\<in>A. g i)"
  2658 proof cases
  2659   assume "finite A" from this assms show ?thesis
  2660   proof induct
  2661     case (insert x A)
  2662     hence hyp: "(\<Sum>i\<in>A. f i - g i) = (\<Sum>i\<in>A. f i) - (\<Sum>i\<in>A. g i)"
  2663       by auto
  2664     { fix i assume *: "i \<in> insert x A"
  2665       hence "g i \<le> f i" using insert by simp
  2666       also have "f i < \<omega>" using * insert by (simp add: pextreal_less_\<omega>)
  2667       finally have "g i \<noteq> \<omega>" by (simp add: pextreal_less_\<omega>) }
  2668     hence "setsum g A \<noteq> \<omega>" "g x \<noteq> \<omega>" by (auto simp: setsum_\<omega>)
  2669     moreover have "setsum f A \<noteq> \<omega>" "f x \<noteq> \<omega>" using insert by (auto simp: setsum_\<omega>)
  2670     moreover have "g x \<le> f x" using insert by auto
  2671     moreover have "(\<Sum>i\<in>A. g i) \<le> (\<Sum>i\<in>A. f i)" using insert by (auto intro!: setsum_mono)
  2672     ultimately show ?case using `finite A` `x \<notin> A` hyp
  2673       by (auto simp: pextreal_noteq_omega_Ex)
  2674   qed simp
  2675 qed simp
  2676 
  2677 lemma real_of_pextreal_diff:
  2678   "y \<le> x \<Longrightarrow> x \<noteq> \<omega> \<Longrightarrow> real x - real y = real (x - y)"
  2679   by (cases x, cases y) auto
  2680 
  2681 lemma psuminf_minus:
  2682   assumes ord: "\<And>i. g i \<le> f i" and fin: "psuminf g \<noteq> \<omega>" "psuminf f \<noteq> \<omega>"
  2683   shows "(\<Sum>\<^isub>\<infinity> i. f i - g i) = psuminf f - psuminf g"
  2684 proof -
  2685   have [simp]: "\<And>i. f i \<noteq> \<omega>" using fin by (auto intro: psuminf_\<omega>)
  2686   from fin have "(\<lambda>x. real (f x)) sums real (\<Sum>\<^isub>\<infinity>x. f x)"
  2687     and "(\<lambda>x. real (g x)) sums real (\<Sum>\<^isub>\<infinity>x. g x)"
  2688     by (auto intro: psuminf_imp_suminf)
  2689   from sums_diff[OF this]
  2690   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
  2691     by (subst (asm) (1 2) real_of_pextreal_diff) (auto simp: psuminf_\<omega> psuminf_le)
  2692   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)))"
  2693     by (rule suminf_imp_psuminf) simp
  2694   thus ?thesis using fin by (simp add: Real_real psuminf_\<omega>)
  2695 qed
  2696 
  2697 lemma INF_eq_LIMSEQ:
  2698   assumes "mono (\<lambda>i. - f i)" and "\<And>n. 0 \<le> f n" and "0 \<le> x"
  2699   shows "(INF n. Real (f n)) = Real x \<longleftrightarrow> f ----> x"
  2700 proof
  2701   assume x: "(INF n. Real (f n)) = Real x"
  2702   { fix n
  2703     have "Real x \<le> Real (f n)" using x[symmetric] by (auto intro: INF_leI)
  2704     hence "x \<le> f n" using assms by simp
  2705     hence "\<bar>f n - x\<bar> = f n - x" by auto }
  2706   note abs_eq = this
  2707   show "f ----> x"
  2708   proof (rule LIMSEQ_I)
  2709     fix r :: real assume "0 < r"
  2710     show "\<exists>no. \<forall>n\<ge>no. norm (f n - x) < r"
  2711     proof (rule ccontr)
  2712       assume *: "\<not> ?thesis"
  2713       { fix N
  2714         from * obtain n where *: "N \<le> n" "r \<le> f n - x"
  2715           using abs_eq by (auto simp: not_less)
  2716         hence "x + r \<le> f n" by auto
  2717         also have "f n \<le> f N" using `mono (\<lambda>i. - f i)` * by (auto dest: monoD)
  2718         finally have "Real (x + r) \<le> Real (f N)" using `0 \<le> f N` by auto }
  2719       hence "Real x < Real (x + r)"
  2720         and "Real (x + r) \<le> (INF n. Real (f n))" using `0 < r` `0 \<le> x` by (auto intro: le_INFI)
  2721       hence "Real x < (INF n. Real (f n))" by (rule less_le_trans)
  2722       thus False using x by auto
  2723     qed
  2724   qed
  2725 next
  2726   assume "f ----> x"
  2727   show "(INF n. Real (f n)) = Real x"
  2728   proof (rule pextreal_INFI)
  2729     fix n
  2730     from decseq_le[OF _ `f ----> x`] assms
  2731     show "Real x \<le> Real (f n)" unfolding decseq_eq_incseq incseq_mono by auto
  2732   next
  2733     fix y assume *: "\<And>n. n\<in>UNIV \<Longrightarrow> y \<le> Real (f n)"
  2734     thus "y \<le> Real x"
  2735     proof (cases y)
  2736       case (preal r)
  2737       with * have "\<exists>N. \<forall>n\<ge>N. r \<le> f n" using assms by fastsimp
  2738       from LIMSEQ_le_const[OF `f ----> x` this]
  2739       show "y \<le> Real x" using `0 \<le> x` preal by auto
  2740     qed simp
  2741   qed
  2742 qed
  2743 
  2744 lemma INFI_bound:
  2745   assumes "\<forall>N. x \<le> f N"
  2746   shows "x \<le> (INF n. f n)"
  2747   using assms by (simp add: INFI_def le_Inf_iff)
  2748 
  2749 lemma LIMSEQ_imp_lim_INF:
  2750   assumes pos: "\<And>i. 0 \<le> X i" and lim: "X ----> x"
  2751   shows "(SUP n. INF m. Real (X (n + m))) = Real x"
  2752 proof -
  2753   have "0 \<le> x" using assms by (auto intro!: LIMSEQ_le_const)
  2754 
  2755   have "\<And>n. (INF m. Real (X (n + m))) \<le> Real (X (n + 0))" by (rule INF_leI) simp
  2756   also have "\<And>n. Real (X (n + 0)) < \<omega>" by simp
  2757   finally have "\<forall>n. \<exists>r\<ge>0. (INF m. Real (X (n + m))) = Real r"
  2758     by (auto simp: pextreal_less_\<omega> pextreal_noteq_omega_Ex)
  2759   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"
  2760     by auto
  2761 
  2762   show ?thesis unfolding r
  2763   proof (subst SUP_eq_LIMSEQ)
  2764     show "mono r" unfolding mono_def
  2765     proof safe
  2766       fix x y :: nat assume "x \<le> y"
  2767       have "Real (r x) \<le> Real (r y)" unfolding r(1)[symmetric] using pos
  2768       proof (safe intro!: INF_mono bexI)
  2769         fix m have "x + (m + y - x) = y + m"
  2770           using `x \<le> y` by auto
  2771         thus "Real (X (x + (m + y - x))) \<le> Real (X (y + m))" by simp
  2772       qed simp
  2773       thus "r x \<le> r y" using r by auto
  2774     qed
  2775     show "\<And>n. 0 \<le> r n" by fact
  2776     show "0 \<le> x" by fact
  2777     show "r ----> x"
  2778     proof (rule LIMSEQ_I)
  2779       fix e :: real assume "0 < e"
  2780       hence "0 < e/2" by auto
  2781       from LIMSEQ_D[OF lim this] obtain N where *: "\<And>n. N \<le> n \<Longrightarrow> \<bar>X n - x\<bar> < e/2"
  2782         by auto
  2783       show "\<exists>N. \<forall>n\<ge>N. norm (r n - x) < e"
  2784       proof (safe intro!: exI[of _ N])
  2785         fix n assume "N \<le> n"
  2786         show "norm (r n - x) < e"
  2787         proof cases
  2788           assume "r n < x"
  2789           have "x - r n \<le> e/2"
  2790           proof cases
  2791             assume e: "e/2 \<le> x"
  2792             have "Real (x - e/2) \<le> Real (r n)" unfolding r(1)[symmetric]
  2793             proof (rule le_INFI)
  2794               fix m show "Real (x - e / 2) \<le> Real (X (n + m))"
  2795                 using *[of "n + m"] `N \<le> n`
  2796                 using pos by (auto simp: field_simps abs_real_def split: split_if_asm)
  2797             qed
  2798             with e show ?thesis using pos `0 \<le> x` r(2) by auto
  2799           next
  2800             assume "\<not> e/2 \<le> x" hence "x - e/2 < 0" by auto
  2801             with `0 \<le> r n` show ?thesis by auto
  2802           qed
  2803           with `r n < x` show ?thesis by simp
  2804         next
  2805           assume e: "\<not> r n < x"
  2806           have "Real (r n) \<le> Real (X (n + 0))" unfolding r(1)[symmetric]
  2807             by (rule INF_leI) simp
  2808           hence "r n - x \<le> X n - x" using r pos by auto
  2809           also have "\<dots> < e/2" using *[OF `N \<le> n`] by (auto simp: field_simps abs_real_def split: split_if_asm)
  2810           finally have "r n - x < e" using `0 < e` by auto
  2811           with e show ?thesis by auto
  2812         qed
  2813       qed
  2814     qed
  2815   qed
  2816 qed
  2817 
  2818 lemma real_of_pextreal_strict_mono_iff:
  2819   "real a < real b \<longleftrightarrow> (b \<noteq> \<omega> \<and> ((a = \<omega> \<and> 0 < b) \<or> (a < b)))"
  2820 proof (cases a)
  2821   case infinite thus ?thesis by (cases b) auto
  2822 next
  2823   case preal thus ?thesis by (cases b) auto
  2824 qed
  2825 
  2826 lemma real_of_pextreal_mono_iff:
  2827   "real a \<le> real b \<longleftrightarrow> (a = \<omega> \<or> (b \<noteq> \<omega> \<and> a \<le> b) \<or> (b = \<omega> \<and> a = 0))"
  2828 proof (cases a)
  2829   case infinite thus ?thesis by (cases b) auto
  2830 next
  2831   case preal thus ?thesis by (cases b)  auto
  2832 qed
  2833 
  2834 lemma ex_pextreal_inverse_of_nat_Suc_less:
  2835   fixes e :: pextreal assumes "0 < e" shows "\<exists>n. inverse (of_nat (Suc n)) < e"
  2836 proof (cases e)
  2837   case (preal r)
  2838   with `0 < e` ex_inverse_of_nat_Suc_less[of r]
  2839   obtain n where "inverse (of_nat (Suc n)) < r" by auto
  2840   with preal show ?thesis
  2841     by (auto simp: real_eq_of_nat[symmetric])
  2842 qed auto
  2843 
  2844 lemma Lim_eq_Sup_mono:
  2845   fixes u :: "nat \<Rightarrow> pextreal" assumes "mono u"
  2846   shows "u ----> (SUP i. u i)"
  2847 proof -
  2848   from lim_pextreal_increasing[of u] `mono u`
  2849   obtain l where l: "u ----> l" unfolding mono_def by auto
  2850   from SUP_Lim_pextreal[OF _ this] `mono u`
  2851   have "(SUP i. u i) = l" unfolding mono_def by auto
  2852   with l show ?thesis by simp
  2853 qed
  2854 
  2855 lemma isotone_Lim:
  2856   fixes x :: pextreal assumes "u \<up> x"
  2857   shows "u ----> x" (is ?lim) and "mono u" (is ?mono)
  2858 proof -
  2859   show ?mono using assms unfolding mono_iff_le_Suc isoton_def by auto
  2860   from Lim_eq_Sup_mono[OF this] `u \<up> x`
  2861   show ?lim unfolding isoton_def by simp
  2862 qed
  2863 
  2864 lemma isoton_iff_Lim_mono:
  2865   fixes u :: "nat \<Rightarrow> pextreal"
  2866   shows "u \<up> x \<longleftrightarrow> (mono u \<and> u ----> x)"
  2867 proof safe
  2868   assume "mono u" and x: "u ----> x"
  2869   with SUP_Lim_pextreal[OF _ x]
  2870   show "u \<up> x" unfolding isoton_def
  2871     using `mono u`[unfolded mono_def]
  2872     using `mono u`[unfolded mono_iff_le_Suc]
  2873     by auto
  2874 qed (auto dest: isotone_Lim)
  2875 
  2876 lemma pextreal_inverse_inverse[simp]:
  2877   fixes x :: pextreal
  2878   shows "inverse (inverse x) = x"
  2879   by (cases x) auto
  2880 
  2881 lemma atLeastAtMost_omega_eq_atLeast:
  2882   shows "{a .. \<omega>} = {a ..}"
  2883 by auto
  2884 
  2885 lemma atLeast0AtMost_eq_atMost: "{0 :: pextreal .. a} = {.. a}" by auto
  2886 
  2887 lemma greaterThan_omega_Empty: "{\<omega> <..} = {}" by auto
  2888 
  2889 lemma lessThan_0_Empty: "{..< 0 :: pextreal} = {}" by auto
  2890 
  2891 lemma real_of_pextreal_inverse[simp]:
  2892   fixes X :: pextreal
  2893   shows "real (inverse X) = 1 / real X"
  2894   by (cases X) (auto simp: inverse_eq_divide)
  2895 
  2896 lemma real_of_pextreal_le_0[simp]: "real (X :: pextreal) \<le> 0 \<longleftrightarrow> (X = 0 \<or> X = \<omega>)"
  2897   by (cases X) auto
  2898 
  2899 lemma real_of_pextreal_less_0[simp]: "\<not> (real (X :: pextreal) < 0)"
  2900   by (cases X) auto
  2901 
  2902 lemma abs_real_of_pextreal[simp]: "\<bar>real (X :: pextreal)\<bar> = real X"
  2903   by simp
  2904 
  2905 lemma zero_less_real_of_pextreal: "0 < real (X :: pextreal) \<longleftrightarrow> X \<noteq> 0 \<and> X \<noteq> \<omega>"
  2906   by (cases X) auto
  2907 
  2908 end