src/HOL/Library/Extended_Real.thy
changeset 47108 2a1953f0d20d
parent 47082 737d7bc8e50f
child 50104 de19856feb54
     1.1 --- a/src/HOL/Library/Extended_Real.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -124,11 +124,6 @@
     1.4    fix x :: ereal show "x \<in> range uminus" by (intro image_eqI[of _ _ "-x"]) auto
     1.5  qed auto
     1.6  
     1.7 -instantiation ereal :: number
     1.8 -begin
     1.9 -definition [simp]: "number_of x = ereal (number_of x)"
    1.10 -instance ..
    1.11 -end
    1.12  
    1.13  instantiation ereal :: abs
    1.14  begin
    1.15 @@ -671,6 +666,14 @@
    1.16    using assms
    1.17    by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
    1.18  
    1.19 +instance ereal :: numeral ..
    1.20 +
    1.21 +lemma numeral_eq_ereal [simp]: "numeral w = ereal (numeral w)"
    1.22 +  apply (induct w rule: num_induct)
    1.23 +  apply (simp only: numeral_One one_ereal_def)
    1.24 +  apply (simp only: numeral_inc ereal_plus_1)
    1.25 +  done
    1.26 +
    1.27  lemma ereal_le_epsilon:
    1.28    fixes x y :: ereal
    1.29    assumes "ALL e. 0 < e --> x <= y + e"
    1.30 @@ -781,8 +784,8 @@
    1.31    shows "(- x) ^ n = (if even n then x ^ n else - (x^n))"
    1.32    by (induct n) (auto simp: one_ereal_def)
    1.33  
    1.34 -lemma ereal_power_number_of[simp]:
    1.35 -  "(number_of num :: ereal) ^ n = ereal (number_of num ^ n)"
    1.36 +lemma ereal_power_numeral[simp]:
    1.37 +  "(numeral num :: ereal) ^ n = ereal (numeral num ^ n)"
    1.38    by (induct n) (auto simp: one_ereal_def)
    1.39  
    1.40  lemma zero_le_power_ereal[simp]:
    1.41 @@ -1730,8 +1733,8 @@
    1.42    "ereal_of_enat m \<le> ereal_of_enat n \<longleftrightarrow> m \<le> n"
    1.43  by (cases m n rule: enat2_cases) auto
    1.44  
    1.45 -lemma number_of_le_ereal_of_enat_iff[simp]:
    1.46 -  shows "number_of m \<le> ereal_of_enat n \<longleftrightarrow> number_of m \<le> n"
    1.47 +lemma numeral_le_ereal_of_enat_iff[simp]:
    1.48 +  shows "numeral m \<le> ereal_of_enat n \<longleftrightarrow> numeral m \<le> n"
    1.49  by (cases n) (auto dest: natceiling_le intro: natceiling_le_eq[THEN iffD1])
    1.50  
    1.51  lemma ereal_of_enat_ge_zero_cancel_iff[simp]: