src/HOL/Library/Extended_Real.thy
changeset 45934 9321cd2572fe
parent 45769 2d5b1af2426a
child 47082 737d7bc8e50f
     1.1 --- a/src/HOL/Library/Extended_Real.thy	Mon Dec 19 14:41:08 2011 +0100
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Tue Dec 20 11:40:56 2011 +0100
     1.3 @@ -55,11 +55,7 @@
     1.4    instance ..
     1.5  end
     1.6  
     1.7 -definition "ereal_of_enat n = (case n of enat n \<Rightarrow> ereal (real n) | \<infinity> \<Rightarrow> \<infinity>)"
     1.8 -
     1.9  declare [[coercion "ereal :: real \<Rightarrow> ereal"]]
    1.10 -declare [[coercion "ereal_of_enat :: enat \<Rightarrow> ereal"]]
    1.11 -declare [[coercion "(\<lambda>n. ereal (real n)) :: nat \<Rightarrow> ereal"]]
    1.12  
    1.13  lemma ereal_uminus_uminus[simp]:
    1.14    fixes a :: ereal shows "- (- a) = a"
    1.15 @@ -1068,6 +1064,28 @@
    1.16    qed (insert y, simp_all)
    1.17  qed simp
    1.18  
    1.19 +lemma ereal_divide_right_mono[simp]:
    1.20 +  fixes x y z :: ereal
    1.21 +  assumes "x \<le> y" "0 < z" shows "x / z \<le> y / z"
    1.22 +using assms by (cases x y z rule: ereal3_cases) (auto intro: divide_right_mono)
    1.23 +
    1.24 +lemma ereal_divide_left_mono[simp]:
    1.25 +  fixes x y z :: ereal
    1.26 +  assumes "y \<le> x" "0 < z" "0 < x * y"
    1.27 +  shows "z / x \<le> z / y"
    1.28 +using assms by (cases x y z rule: ereal3_cases)
    1.29 +  (auto intro: divide_left_mono simp: field_simps sign_simps split: split_if_asm)
    1.30 +
    1.31 +lemma ereal_divide_zero_left[simp]:
    1.32 +  fixes a :: ereal
    1.33 +  shows "0 / a = 0"
    1.34 +  by (cases a) (auto simp: zero_ereal_def)
    1.35 +
    1.36 +lemma ereal_times_divide_eq_left[simp]:
    1.37 +  fixes a b c :: ereal
    1.38 +  shows "b / c * a = b * a / c"
    1.39 +  by (cases a b c rule: ereal3_cases) (auto simp: field_simps sign_simps)
    1.40 +
    1.41  subsection "Complete lattice"
    1.42  
    1.43  instantiation ereal :: lattice
    1.44 @@ -1683,6 +1701,54 @@
    1.45    finally show ?thesis .
    1.46  qed
    1.47  
    1.48 +subsection "Relation to @{typ enat}"
    1.49 +
    1.50 +definition "ereal_of_enat n = (case n of enat n \<Rightarrow> ereal (real n) | \<infinity> \<Rightarrow> \<infinity>)"
    1.51 +
    1.52 +declare [[coercion "ereal_of_enat :: enat \<Rightarrow> ereal"]]
    1.53 +declare [[coercion "(\<lambda>n. ereal (real n)) :: nat \<Rightarrow> ereal"]]
    1.54 +
    1.55 +lemma ereal_of_enat_simps[simp]:
    1.56 +  "ereal_of_enat (enat n) = ereal n"
    1.57 +  "ereal_of_enat \<infinity> = \<infinity>"
    1.58 +  by (simp_all add: ereal_of_enat_def)
    1.59 +
    1.60 +lemma ereal_of_enat_le_iff[simp]:
    1.61 +  "ereal_of_enat m \<le> ereal_of_enat n \<longleftrightarrow> m \<le> n"
    1.62 +by (cases m n rule: enat2_cases) auto
    1.63 +
    1.64 +lemma number_of_le_ereal_of_enat_iff[simp]:
    1.65 +  shows "number_of m \<le> ereal_of_enat n \<longleftrightarrow> number_of m \<le> n"
    1.66 +by (cases n) (auto dest: natceiling_le intro: natceiling_le_eq[THEN iffD1])
    1.67 +
    1.68 +lemma ereal_of_enat_ge_zero_cancel_iff[simp]:
    1.69 +  "0 \<le> ereal_of_enat n \<longleftrightarrow> 0 \<le> n"
    1.70 +by (cases n) (auto simp: enat_0[symmetric])
    1.71 +
    1.72 +lemma ereal_of_enat_gt_zero_cancel_iff[simp]:
    1.73 +  "0 < ereal_of_enat n \<longleftrightarrow> 0 < n"
    1.74 +by (cases n) (auto simp: enat_0[symmetric])
    1.75 +
    1.76 +lemma ereal_of_enat_zero[simp]:
    1.77 +  "ereal_of_enat 0 = 0"
    1.78 +by (auto simp: enat_0[symmetric])
    1.79 +
    1.80 +lemma ereal_of_enat_add:
    1.81 +  "ereal_of_enat (m + n) = ereal_of_enat m + ereal_of_enat n"
    1.82 +by (cases m n rule: enat2_cases) auto
    1.83 +
    1.84 +lemma ereal_of_enat_sub:
    1.85 +  assumes "n \<le> m" shows "ereal_of_enat (m - n) = ereal_of_enat m - ereal_of_enat n "
    1.86 +using assms by (cases m n rule: enat2_cases) auto
    1.87 +
    1.88 +lemma ereal_of_enat_mult:
    1.89 +  "ereal_of_enat (m * n) = ereal_of_enat m * ereal_of_enat n"
    1.90 +by (cases m n rule: enat2_cases) auto
    1.91 +
    1.92 +lemmas ereal_of_enat_pushin = ereal_of_enat_add ereal_of_enat_sub ereal_of_enat_mult
    1.93 +lemmas ereal_of_enat_pushout = ereal_of_enat_pushin[symmetric]
    1.94 +
    1.95 +
    1.96  subsection "Limits on @{typ ereal}"
    1.97  
    1.98  subsubsection "Topological space"