src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
changeset 44170 510ac30f44c0
parent 44167 e81d676d598e
child 44571 bd91b77c4cd6
     1.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Fri Aug 12 07:18:28 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Fri Aug 12 09:17:24 2011 -0700
     1.3 @@ -102,7 +102,7 @@
     1.4      then show False using MInf by auto
     1.5    next
     1.6      case PInf then have "S={\<infinity>}" by (metis Inf_eq_PInfty assms(2))
     1.7 -    then show False by (metis `Inf S ~: S` insert_code mem_def PInf)
     1.8 +    then show False using `Inf S ~: S` by simp
     1.9    next
    1.10      case (real r) then have fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>" by simp
    1.11      from ereal_open_cont_interval[OF a this] guess e . note e = this
    1.12 @@ -284,22 +284,22 @@
    1.13  lemma ereal_open_mono_set:
    1.14    fixes S :: "ereal set"
    1.15    defines "a \<equiv> Inf S"
    1.16 -  shows "(open S \<and> mono S) \<longleftrightarrow> (S = UNIV \<or> S = {a <..})"
    1.17 +  shows "(open S \<and> mono_set S) \<longleftrightarrow> (S = UNIV \<or> S = {a <..})"
    1.18    by (metis Inf_UNIV a_def atLeast_eq_UNIV_iff ereal_open_atLeast
    1.19              ereal_open_closed mono_set_iff open_ereal_greaterThan)
    1.20  
    1.21  lemma ereal_closed_mono_set:
    1.22    fixes S :: "ereal set"
    1.23 -  shows "(closed S \<and> mono S) \<longleftrightarrow> (S = {} \<or> S = {Inf S ..})"
    1.24 +  shows "(closed S \<and> mono_set S) \<longleftrightarrow> (S = {} \<or> S = {Inf S ..})"
    1.25    by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast
    1.26              ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan)
    1.27  
    1.28  lemma ereal_Liminf_Sup_monoset:
    1.29    fixes f :: "'a => ereal"
    1.30 -  shows "Liminf net f = Sup {l. \<forall>S. open S \<longrightarrow> mono S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
    1.31 +  shows "Liminf net f = Sup {l. \<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
    1.32    unfolding Liminf_Sup
    1.33  proof (intro arg_cong[where f="\<lambda>P. Sup (Collect P)"] ext iffI allI impI)
    1.34 -  fix l S assume ev: "\<forall>y<l. eventually (\<lambda>x. y < f x) net" and "open S" "mono S" "l \<in> S"
    1.35 +  fix l S assume ev: "\<forall>y<l. eventually (\<lambda>x. y < f x) net" and "open S" "mono_set S" "l \<in> S"
    1.36    then have "S = UNIV \<or> S = {Inf S <..}"
    1.37      using ereal_open_mono_set[of S] by auto
    1.38    then show "eventually (\<lambda>x. f x \<in> S) net"
    1.39 @@ -310,7 +310,7 @@
    1.40      then show "eventually (\<lambda>x. f x \<in> S) net"  by (subst S) auto
    1.41    qed auto
    1.42  next
    1.43 -  fix l y assume S: "\<forall>S. open S \<longrightarrow> mono S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net" "y < l"
    1.44 +  fix l y assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net" "y < l"
    1.45    have "eventually  (\<lambda>x. f x \<in> {y <..}) net"
    1.46      using `y < l` by (intro S[rule_format]) auto
    1.47    then show "eventually (\<lambda>x. y < f x) net" by auto
    1.48 @@ -318,11 +318,11 @@
    1.49  
    1.50  lemma ereal_Limsup_Inf_monoset:
    1.51    fixes f :: "'a => ereal"
    1.52 -  shows "Limsup net f = Inf {l. \<forall>S. open S \<longrightarrow> mono (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
    1.53 +  shows "Limsup net f = Inf {l. \<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
    1.54    unfolding Limsup_Inf
    1.55  proof (intro arg_cong[where f="\<lambda>P. Inf (Collect P)"] ext iffI allI impI)
    1.56 -  fix l S assume ev: "\<forall>y>l. eventually (\<lambda>x. f x < y) net" and "open S" "mono (uminus`S)" "l \<in> S"
    1.57 -  then have "open (uminus`S) \<and> mono (uminus`S)" by (simp add: ereal_open_uminus)
    1.58 +  fix l S assume ev: "\<forall>y>l. eventually (\<lambda>x. f x < y) net" and "open S" "mono_set (uminus`S)" "l \<in> S"
    1.59 +  then have "open (uminus`S) \<and> mono_set (uminus`S)" by (simp add: ereal_open_uminus)
    1.60    then have "S = UNIV \<or> S = {..< Sup S}"
    1.61      unfolding ereal_open_mono_set ereal_Inf_uminus_image_eq ereal_image_uminus_shift by simp
    1.62    then show "eventually (\<lambda>x. f x \<in> S) net"
    1.63 @@ -333,7 +333,7 @@
    1.64      then show "eventually (\<lambda>x. f x \<in> S) net"  by (subst S) auto
    1.65    qed auto
    1.66  next
    1.67 -  fix l y assume S: "\<forall>S. open S \<longrightarrow> mono (uminus`S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net" "l < y"
    1.68 +  fix l y assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus`S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net" "l < y"
    1.69    have "eventually  (\<lambda>x. f x \<in> {..< y}) net"
    1.70      using `l < y` by (intro S[rule_format]) auto
    1.71    then show "eventually (\<lambda>x. f x < y) net" by auto
    1.72 @@ -469,7 +469,7 @@
    1.73  
    1.74  lemma liminf_bounded_open:
    1.75    fixes x :: "nat \<Rightarrow> ereal"
    1.76 -  shows "x0 \<le> liminf x \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> mono S \<longrightarrow> x0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. x n \<in> S))" 
    1.77 +  shows "x0 \<le> liminf x \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> x0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. x n \<in> S))" 
    1.78    (is "_ \<longleftrightarrow> ?P x0")
    1.79  proof
    1.80    assume "?P x0" then show "x0 \<le> liminf x"
    1.81 @@ -477,7 +477,7 @@
    1.82      by (intro complete_lattice_class.Sup_upper) auto
    1.83  next
    1.84    assume "x0 \<le> liminf x"
    1.85 -  { fix S :: "ereal set" assume om: "open S & mono S & x0:S"
    1.86 +  { fix S :: "ereal set" assume om: "open S & mono_set S & x0:S"
    1.87      { assume "S = UNIV" hence "EX N. (ALL n>=N. x n : S)" by auto }
    1.88      moreover
    1.89      { assume "~(S=UNIV)"
    1.90 @@ -641,7 +641,7 @@
    1.91    shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"
    1.92  proof-
    1.93  let ?l="(SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"
    1.94 -{ fix T assume T_def: "open T & mono T & ?l:T"
    1.95 +{ fix T assume T_def: "open T & mono_set T & ?l:T"
    1.96    have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T"
    1.97    proof-
    1.98    { assume "T=UNIV" hence ?thesis by (simp add: gt_ex) }
    1.99 @@ -660,7 +660,7 @@
   1.100  }
   1.101  moreover
   1.102  { fix z
   1.103 -  assume a: "ALL T. open T --> mono T --> z : T -->
   1.104 +  assume a: "ALL T. open T --> mono_set T --> z : T -->
   1.105       (EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)"
   1.106    { fix B assume "B<z"
   1.107      then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> B < f y)"
   1.108 @@ -683,7 +683,7 @@
   1.109    shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)"
   1.110  proof-
   1.111  let ?l="(INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)"
   1.112 -{ fix T assume T_def: "open T & mono (uminus ` T) & ?l:T"
   1.113 +{ fix T assume T_def: "open T & mono_set (uminus ` T) & ?l:T"
   1.114    have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T"
   1.115    proof-
   1.116    { assume "T=UNIV" hence ?thesis by (simp add: gt_ex) }
   1.117 @@ -707,7 +707,7 @@
   1.118  }
   1.119  moreover
   1.120  { fix z
   1.121 -  assume a: "ALL T. open T --> mono (uminus ` T) --> z : T -->
   1.122 +  assume a: "ALL T. open T --> mono_set (uminus ` T) --> z : T -->
   1.123       (EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)"
   1.124    { fix B assume "z<B"
   1.125      then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> f y<B)"