src/HOL/Library/Extended_Real.thy
changeset 56166 9a241bc276cd
parent 55913 c1409c103b77
child 56212 3253aaf73a01
     1.1 --- a/src/HOL/Library/Extended_Real.thy	Sat Mar 15 16:54:32 2014 +0100
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Sun Mar 16 18:09:04 2014 +0100
     1.3 @@ -1389,16 +1389,26 @@
     1.4  qed
     1.5  
     1.6  lemma ereal_Sup_uminus_image_eq: "Sup (uminus ` S::ereal set) = - Inf S"
     1.7 -  by (auto intro!: Sup_eqI
     1.8 +  by (auto intro!: SUP_eqI
     1.9             simp: Ball_def[symmetric] ereal_uminus_le_reorder le_Inf_iff
    1.10             intro!: complete_lattice_class.Inf_lower2)
    1.11  
    1.12 +lemma ereal_SUP_uminus_eq:
    1.13 +  fixes f :: "'a \<Rightarrow> ereal"
    1.14 +  shows "(SUP x:S. uminus (f x)) = - (INF x:S. f x)"
    1.15 +  using ereal_Sup_uminus_image_eq [of "f ` S"] by (simp add: comp_def)
    1.16 +
    1.17  lemma ereal_inj_on_uminus[intro, simp]: "inj_on uminus (A :: ereal set)"
    1.18    by (auto intro!: inj_onI)
    1.19  
    1.20  lemma ereal_Inf_uminus_image_eq: "Inf (uminus ` S::ereal set) = - Sup S"
    1.21    using ereal_Sup_uminus_image_eq[of "uminus ` S"] by simp
    1.22  
    1.23 +lemma ereal_INF_uminus_eq:
    1.24 +  fixes f :: "'a \<Rightarrow> ereal"
    1.25 +  shows "(INF x:S. uminus (f x)) = - (SUP x:S. f x)"
    1.26 +  using ereal_Inf_uminus_image_eq [of "f ` S"] by (simp add: comp_def)
    1.27 +
    1.28  lemma ereal_SUP_not_infty:
    1.29    fixes f :: "_ \<Rightarrow> ereal"
    1.30    shows "A \<noteq> {} \<Longrightarrow> l \<noteq> -\<infinity> \<Longrightarrow> u \<noteq> \<infinity> \<Longrightarrow> \<forall>a\<in>A. l \<le> f a \<and> f a \<le> u \<Longrightarrow> \<bar>SUPR A f\<bar> \<noteq> \<infinity>"
    1.31 @@ -1415,7 +1425,7 @@
    1.32    fixes f :: "'a \<Rightarrow> ereal"
    1.33    shows "(SUP i : R. -(f i)) = -(INF i : R. f i)"
    1.34    using ereal_Sup_uminus_image_eq[of "f`R"]
    1.35 -  by (simp add: SUP_def INF_def image_image)
    1.36 +  by (simp add: image_image)
    1.37  
    1.38  lemma ereal_INFI_uminus:
    1.39    fixes f :: "'a \<Rightarrow> ereal"
    1.40 @@ -1763,7 +1773,7 @@
    1.41  lemma SUPR_countable_SUPR:
    1.42    "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> SUPR A g = SUPR UNIV f"
    1.43    using Sup_countable_SUPR[of "g`A"]
    1.44 -  by (auto simp: SUP_def)
    1.45 +  by auto
    1.46  
    1.47  lemma Sup_ereal_cadd:
    1.48    fixes A :: "ereal set"
    1.49 @@ -1772,7 +1782,7 @@
    1.50    shows "Sup ((\<lambda>x. a + x) ` A) = a + Sup A"
    1.51  proof (rule antisym)
    1.52    have *: "\<And>a::ereal. \<And>A. Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A"
    1.53 -    by (auto intro!: add_mono complete_lattice_class.Sup_least complete_lattice_class.Sup_upper)
    1.54 +    by (auto intro!: add_mono complete_lattice_class.SUP_least complete_lattice_class.Sup_upper)
    1.55    then show "Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A" .
    1.56    show "a + Sup A \<le> Sup ((\<lambda>x. a + x) ` A)"
    1.57    proof (cases a)
    1.58 @@ -1794,8 +1804,8 @@
    1.59    assumes "A \<noteq> {}"
    1.60      and "a \<noteq> -\<infinity>"
    1.61    shows "Sup ((\<lambda>x. a - x) ` A) = a - Inf A"
    1.62 -  using Sup_ereal_cadd[of "uminus ` A" a] assms
    1.63 -  by (simp add: comp_def image_image minus_ereal_def ereal_Sup_uminus_image_eq)
    1.64 +  using Sup_ereal_cadd [of "uminus ` A" a] assms
    1.65 +  unfolding image_image minus_ereal_def by (simp add: ereal_SUP_uminus_eq)
    1.66  
    1.67  lemma SUPR_ereal_cminus:
    1.68    fixes f :: "'i \<Rightarrow> ereal"
    1.69 @@ -1820,8 +1830,8 @@
    1.70    then have "(\<lambda>x. -a - x)`uminus`A = uminus ` (\<lambda>x. a - x) ` A"
    1.71      by (auto simp: image_image)
    1.72    with * show ?thesis
    1.73 -    using Sup_ereal_cminus[of "uminus ` A" "-a"] assms
    1.74 -    by (auto simp add: ereal_Sup_uminus_image_eq ereal_Inf_uminus_image_eq)
    1.75 +    using Sup_ereal_cminus [of "uminus ` A" "- a"] assms
    1.76 +    by (auto simp add: ereal_INF_uminus_eq ereal_SUP_uminus_eq)
    1.77  qed
    1.78  
    1.79  lemma INFI_ereal_cminus: