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.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"
```