src/HOL/Library/Extended_Real.thy
changeset 56212 3253aaf73a01
parent 56166 9a241bc276cd
child 56218 1c3f1f2431f9
     1.1 --- a/src/HOL/Library/Extended_Real.thy	Tue Mar 18 21:02:33 2014 +0100
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Tue Mar 18 22:11:46 2014 +0100
     1.3 @@ -1421,16 +1421,16 @@
     1.4    using INF_lower2[of _ A f u] INF_greatest[of A l f]
     1.5    by (cases "INFI A f") auto
     1.6  
     1.7 -lemma ereal_SUPR_uminus:
     1.8 +lemma ereal_SUP_uminus:
     1.9    fixes f :: "'a \<Rightarrow> ereal"
    1.10    shows "(SUP i : R. -(f i)) = -(INF i : R. f i)"
    1.11    using ereal_Sup_uminus_image_eq[of "f`R"]
    1.12    by (simp add: image_image)
    1.13  
    1.14 -lemma ereal_INFI_uminus:
    1.15 +lemma ereal_INF_uminus:
    1.16    fixes f :: "'a \<Rightarrow> ereal"
    1.17    shows "(INF i : R. - f i) = - (SUP i : R. f i)"
    1.18 -  using ereal_SUPR_uminus[of _ "\<lambda>x. - f x"] by simp
    1.19 +  using ereal_SUP_uminus [of _ "\<lambda>x. - f x"] by simp
    1.20  
    1.21  lemma ereal_image_uminus_shift:
    1.22    fixes X Y :: "ereal set"
    1.23 @@ -1539,7 +1539,7 @@
    1.24      using real by (simp add: ereal_le_minus_iff)
    1.25  qed (insert assms, auto)
    1.26  
    1.27 -lemma SUPR_ereal_add:
    1.28 +lemma SUP_ereal_add:
    1.29    fixes f g :: "nat \<Rightarrow> ereal"
    1.30    assumes "incseq f"
    1.31      and "incseq g"
    1.32 @@ -1575,18 +1575,18 @@
    1.33      by (simp add: ac_simps)
    1.34  qed (auto intro!: add_mono SUP_upper)
    1.35  
    1.36 -lemma SUPR_ereal_add_pos:
    1.37 +lemma SUP_ereal_add_pos:
    1.38    fixes f g :: "nat \<Rightarrow> ereal"
    1.39    assumes inc: "incseq f" "incseq g"
    1.40      and pos: "\<And>i. 0 \<le> f i" "\<And>i. 0 \<le> g i"
    1.41    shows "(SUP i. f i + g i) = SUPR UNIV f + SUPR UNIV g"
    1.42 -proof (intro SUPR_ereal_add inc)
    1.43 +proof (intro SUP_ereal_add inc)
    1.44    fix i
    1.45    show "f i \<noteq> -\<infinity>" "g i \<noteq> -\<infinity>"
    1.46      using pos[of i] by auto
    1.47  qed
    1.48  
    1.49 -lemma SUPR_ereal_setsum:
    1.50 +lemma SUP_ereal_setsum:
    1.51    fixes f g :: "'a \<Rightarrow> nat \<Rightarrow> ereal"
    1.52    assumes "\<And>n. n \<in> A \<Longrightarrow> incseq (f n)"
    1.53      and pos: "\<And>n i. n \<in> A \<Longrightarrow> 0 \<le> f n i"
    1.54 @@ -1594,13 +1594,13 @@
    1.55  proof (cases "finite A")
    1.56    case True
    1.57    then show ?thesis using assms
    1.58 -    by induct (auto simp: incseq_setsumI2 setsum_nonneg SUPR_ereal_add_pos)
    1.59 +    by induct (auto simp: incseq_setsumI2 setsum_nonneg SUP_ereal_add_pos)
    1.60  next
    1.61    case False
    1.62    then show ?thesis by simp
    1.63  qed
    1.64  
    1.65 -lemma SUPR_ereal_cmult:
    1.66 +lemma SUP_ereal_cmult:
    1.67    fixes f :: "nat \<Rightarrow> ereal"
    1.68    assumes "\<And>i. 0 \<le> f i"
    1.69      and "0 \<le> c"
    1.70 @@ -1675,7 +1675,7 @@
    1.71    qed
    1.72  qed
    1.73  
    1.74 -lemma Sup_countable_SUPR:
    1.75 +lemma Sup_countable_SUP:
    1.76    assumes "A \<noteq> {}"
    1.77    shows "\<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> A \<and> Sup A = SUPR UNIV f"
    1.78  proof (cases "Sup A")
    1.79 @@ -1770,9 +1770,9 @@
    1.80      using MInf by (auto intro!: exI[of _ "\<lambda>x. -\<infinity>"])
    1.81  qed
    1.82  
    1.83 -lemma SUPR_countable_SUPR:
    1.84 +lemma SUP_countable_SUP:
    1.85    "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> SUPR A g = SUPR UNIV f"
    1.86 -  using Sup_countable_SUPR[of "g`A"]
    1.87 +  using Sup_countable_SUP [of "g`A"]
    1.88    by auto
    1.89  
    1.90  lemma Sup_ereal_cadd:
    1.91 @@ -1807,7 +1807,7 @@
    1.92    using Sup_ereal_cadd [of "uminus ` A" a] assms
    1.93    unfolding image_image minus_ereal_def by (simp add: ereal_SUP_uminus_eq)
    1.94  
    1.95 -lemma SUPR_ereal_cminus:
    1.96 +lemma SUP_ereal_cminus:
    1.97    fixes f :: "'i \<Rightarrow> ereal"
    1.98    fixes A
    1.99    assumes "A \<noteq> {}"
   1.100 @@ -1834,7 +1834,7 @@
   1.101      by (auto simp add: ereal_INF_uminus_eq ereal_SUP_uminus_eq)
   1.102  qed
   1.103  
   1.104 -lemma INFI_ereal_cminus:
   1.105 +lemma INF_ereal_cminus:
   1.106    fixes a :: ereal
   1.107    assumes "A \<noteq> {}"
   1.108      and "\<bar>a\<bar> \<noteq> \<infinity>"
   1.109 @@ -1848,7 +1848,7 @@
   1.110    shows "a \<noteq> \<infinity> \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> - (- a + - b) = a + b"
   1.111    by (cases rule: ereal2_cases[of a b]) auto
   1.112  
   1.113 -lemma INFI_ereal_add:
   1.114 +lemma INF_ereal_add:
   1.115    fixes f :: "nat \<Rightarrow> ereal"
   1.116    assumes "decseq f" "decseq g"
   1.117      and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
   1.118 @@ -1864,10 +1864,10 @@
   1.119    then have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
   1.120      by simp
   1.121    also have "\<dots> = INFI UNIV f + INFI UNIV g"
   1.122 -    unfolding ereal_INFI_uminus
   1.123 +    unfolding ereal_INF_uminus
   1.124      using assms INF_less
   1.125 -    by (subst SUPR_ereal_add)
   1.126 -       (auto simp: ereal_SUPR_uminus intro!: uminus_ereal_add_uminus_uminus)
   1.127 +    by (subst SUP_ereal_add)
   1.128 +       (auto simp: ereal_SUP_uminus intro!: uminus_ereal_add_uminus_uminus)
   1.129    finally show ?thesis .
   1.130  qed
   1.131  
   1.132 @@ -2430,7 +2430,7 @@
   1.133  lemma ereal_Limsup_uminus:
   1.134    fixes f :: "'a \<Rightarrow> ereal"
   1.135    shows "Limsup net (\<lambda>x. - (f x)) = - Liminf net f"
   1.136 -  unfolding Limsup_def Liminf_def ereal_SUPR_uminus ereal_INFI_uminus ..
   1.137 +  unfolding Limsup_def Liminf_def ereal_SUP_uminus ereal_INF_uminus ..
   1.138  
   1.139  lemma liminf_bounded_iff:
   1.140    fixes x :: "nat \<Rightarrow> ereal"