1.1 --- a/src/HOL/Library/Extended_Nat.thy	Tue Nov 12 19:28:55 2013 +0100
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Tue Nov 12 19:28:55 2013 +0100
     1.3 @@ -60,10 +60,10 @@
     1.4  lemmas enat2_cases = enat.exhaust[case_product enat.exhaust]
     1.5  lemmas enat3_cases = enat.exhaust[case_product enat.exhaust enat.exhaust]
     1.6  
     1.7 -lemma not_infinity_eq [iff]: "(x \<noteq> \<infinity>) = (EX i. x = enat i)"
     1.8 +lemma not_infinity_eq [iff]: "(x \<noteq> \<infinity>) = (\<exists>i. x = enat i)"
     1.9    by (cases x) auto
    1.10  
    1.11 -lemma not_enat_eq [iff]: "(ALL y. x ~= enat y) = (x = \<infinity>)"
    1.12 +lemma not_enat_eq [iff]: "(\<forall>y. x \<noteq> enat y) = (x = \<infinity>)"
    1.13    by (cases x) auto
    1.14  
    1.15  primrec the_enat :: "enat \<Rightarrow> nat"
    1.16 @@ -94,6 +94,12 @@
    1.17  lemma enat_1 [code_post]: "enat 1 = 1"
    1.18    by (simp add: one_enat_def)
    1.19  
    1.20 +lemma enat_0_iff: "enat x = 0 \<longleftrightarrow> x = 0" "0 = enat x \<longleftrightarrow> x = 0"
    1.21 +  by (auto simp add: zero_enat_def)
    1.22 +
    1.23 +lemma enat_1_iff: "enat x = 1 \<longleftrightarrow> x = 1" "1 = enat x \<longleftrightarrow> x = 1"
    1.24 +  by (auto simp add: one_enat_def)
    1.25 +
    1.26  lemma one_eSuc: "1 = eSuc 0"
    1.27    by (simp add: zero_enat_def one_enat_def eSuc_def)
    1.28  

     2.1 --- a/src/HOL/Library/Extended_Real.thy	Tue Nov 12 19:28:55 2013 +0100
     2.2 +++ b/src/HOL/Library/Extended_Real.thy	Tue Nov 12 19:28:55 2013 +0100
     2.3 @@ -188,6 +188,11 @@
     2.4    "0 = ereal r \<longleftrightarrow> r = 0"
     2.5    unfolding zero_ereal_def by simp_all
     2.6  
     2.7 +lemma ereal_eq_1[simp]:
     2.8 +  "ereal r = 1 \<longleftrightarrow> r = 1"
     2.9 +  "1 = ereal r \<longleftrightarrow> r = 1"
    2.10 +  unfolding one_ereal_def by simp_all
    2.11 +
    2.12  instance
    2.13  proof
    2.14    fix a b c :: ereal
    2.15 @@ -288,9 +293,11 @@
    2.16  lemma ereal_less[simp]:
    2.17    "ereal r < 0 \<longleftrightarrow> (r < 0)"
    2.18    "0 < ereal r \<longleftrightarrow> (0 < r)"
    2.19 +  "ereal r < 1 \<longleftrightarrow> (r < 1)"
    2.20 +  "1 < ereal r \<longleftrightarrow> (1 < r)"
    2.21    "0 < (\<infinity>::ereal)"
    2.22    "-(\<infinity>::ereal) < 0"
    2.23 -  by (simp_all add: zero_ereal_def)
    2.24 +  by (simp_all add: zero_ereal_def one_ereal_def)
    2.25  
    2.26  lemma ereal_less_eq[simp]:
    2.27    "x \<le> (\<infinity>::ereal)"
    2.28 @@ -298,7 +305,9 @@
    2.29    "ereal r \<le> ereal p \<longleftrightarrow> r \<le> p"
    2.30    "ereal r \<le> 0 \<longleftrightarrow> r \<le> 0"
    2.31    "0 \<le> ereal r \<longleftrightarrow> 0 \<le> r"
    2.32 -  by (auto simp add: less_eq_ereal_def zero_ereal_def)
    2.33 +  "ereal r \<le> 1 \<longleftrightarrow> r \<le> 1"
    2.34 +  "1 \<le> ereal r \<longleftrightarrow> 1 \<le> r"
    2.35 +  by (auto simp add: less_eq_ereal_def zero_ereal_def one_ereal_def)
    2.36  
    2.37  lemma ereal_infty_less_eq2:
    2.38    "a \<le> b \<Longrightarrow> a = \<infinity> \<Longrightarrow> b = (\<infinity>::ereal)"
    2.39 @@ -458,6 +467,11 @@
    2.40    shows "\<bar>a\<bar> \<noteq> \<infinity> \<Longrightarrow> c < b \<Longrightarrow> a + c < a + b"
    2.41    by (cases rule: ereal2_cases[of b c]) auto
    2.42  
    2.43 +lemma ereal_add_nonneg_eq_0_iff:
    2.44 +  fixes a b :: ereal
    2.45 +  shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a + b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
    2.46 +  by (cases a b rule: ereal2_cases) auto
    2.47 +
    2.48  lemma ereal_uminus_eq_reorder: "- a = b \<longleftrightarrow> a = (-b::ereal)"
    2.49    by auto
    2.50  
    2.51 @@ -516,8 +530,8 @@
    2.52  
    2.53  lemma
    2.54    fixes f :: "nat \<Rightarrow> ereal"
    2.55 -  shows incseq_uminus[simp]: "incseq (\<lambda>x. - f x) \<longleftrightarrow> decseq f"
    2.56 -  and decseq_uminus[simp]: "decseq (\<lambda>x. - f x) \<longleftrightarrow> incseq f"
    2.57 +  shows ereal_incseq_uminus[simp]: "incseq (\<lambda>x. - f x) \<longleftrightarrow> decseq f"
    2.58 +    and ereal_decseq_uminus[simp]: "decseq (\<lambda>x. - f x) \<longleftrightarrow> incseq f"
    2.59    unfolding decseq_def incseq_def by auto
    2.60  
    2.61  lemma incseq_ereal: "incseq f \<Longrightarrow> incseq (\<lambda>x. ereal (f x))"
    2.62 @@ -620,14 +634,6 @@
    2.63  lemma ereal_m1_less_0[simp]: "-(1::ereal) < 0"
    2.64    by (simp add: zero_ereal_def one_ereal_def)
    2.65  
    2.66 -lemma ereal_zero_m1[simp]: "1 \<noteq> (0::ereal)"
    2.67 -  by (simp add: zero_ereal_def one_ereal_def)
    2.68 -
    2.69 -lemma ereal_times_0[simp]:
    2.70 -  fixes x :: ereal
    2.71 -  shows "0 * x = 0"
    2.72 -  by (cases x) (auto simp: zero_ereal_def)
    2.73 -
    2.74  lemma ereal_times[simp]:
    2.75    "1 \<noteq> (\<infinity>::ereal)" "(\<infinity>::ereal) \<noteq> 1"
    2.76    "1 \<noteq> -(\<infinity>::ereal)" "-(\<infinity>::ereal) \<noteq> 1"
    2.77 @@ -655,12 +661,12 @@
    2.78      (a = \<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = \<infinity>) \<or> (a = -\<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = -\<infinity>)"
    2.79    by (cases rule: ereal2_cases[of a b]) auto
    2.80  
    2.81 +lemma ereal_abs_mult: "\<bar>x * y :: ereal\<bar> = \<bar>x\<bar> * \<bar>y\<bar>"
    2.82 +  by (cases x y rule: ereal2_cases) (auto simp: abs_mult)
    2.83 +
    2.84  lemma ereal_0_less_1[simp]: "0 < (1::ereal)"
    2.85    by (simp_all add: zero_ereal_def one_ereal_def)
    2.86  
    2.87 -lemma ereal_zero_one[simp]: "0 \<noteq> (1::ereal)"
    2.88 -  by (simp_all add: zero_ereal_def one_ereal_def)
    2.89 -
    2.90  lemma ereal_mult_minus_left[simp]:
    2.91    fixes a b :: ereal
    2.92    shows "-a * b = - (a * b)"
    2.93 @@ -952,7 +958,7 @@
    2.94        by simp
    2.95    }
    2.96    then show ?thesis
    2.97 -    by (auto intro!: image_eqI)
    2.98 +    by force
    2.99  qed
   2.100  
   2.101  lemma ereal_uminus_greaterThan[simp]: "uminus ` {(a::ereal)<..} = {..<-a}"
   2.102 @@ -1267,7 +1273,7 @@
   2.103    shows "z / x \<le> z / y"
   2.104    using assms
   2.105    by (cases x y z rule: ereal3_cases)
   2.106 -    (auto intro: divide_left_mono simp: field_simps sign_simps split: split_if_asm)
   2.107 +     (auto intro: divide_left_mono simp: field_simps zero_less_mult_iff mult_less_0_iff split: split_if_asm)
   2.108  
   2.109  lemma ereal_divide_zero_left[simp]:
   2.110    fixes a :: ereal
   2.111 @@ -1277,7 +1283,7 @@
   2.112  lemma ereal_times_divide_eq_left[simp]:
   2.113    fixes a b c :: ereal
   2.114    shows "b / c * a = b * a / c"
   2.115 -  by (cases a b c rule: ereal3_cases) (auto simp: field_simps sign_simps)
   2.116 +  by (cases a b c rule: ereal3_cases) (auto simp: field_simps zero_less_mult_iff mult_less_0_iff)
   2.117  
   2.118  
   2.119  subsection "Complete lattice"
   2.120 @@ -1380,7 +1386,7 @@
   2.121  instance ereal :: linear_continuum
   2.122  proof
   2.123    show "\<exists>a b::ereal. a \<noteq> b"
   2.124 -    using ereal_zero_one by blast
   2.125 +    using zero_neq_one by blast
   2.126  qed
   2.127  
   2.128  lemma ereal_Sup_uminus_image_eq: "Sup (uminus ` S::ereal set) = - Inf S"
   2.129 @@ -1394,6 +1400,18 @@
   2.130  lemma ereal_Inf_uminus_image_eq: "Inf (uminus ` S::ereal set) = - Sup S"
   2.131    using ereal_Sup_uminus_image_eq[of "uminus ` S"] by simp
   2.132  
   2.133 +lemma ereal_SUP_not_infty:
   2.134 +  fixes f :: "_ \<Rightarrow> ereal"
   2.135 +  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>"
   2.136 +  using SUP_upper2[of _ A l f] SUP_least[of A f u]
   2.137 +  by (cases "SUPR A f") auto
   2.138 +
   2.139 +lemma ereal_INF_not_infty:
   2.140 +  fixes f :: "_ \<Rightarrow> ereal"
   2.141 +  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>INFI A f\<bar> \<noteq> \<infinity>"
   2.142 +  using INF_lower2[of _ A f u] INF_greatest[of A l f]
   2.143 +  by (cases "INFI A f") auto
   2.144 +
   2.145  lemma ereal_SUPR_uminus:
   2.146    fixes f :: "'a \<Rightarrow> ereal"
   2.147    shows "(SUP i : R. -(f i)) = -(INF i : R. f i)"
   2.148 @@ -1712,8 +1730,7 @@
   2.149    next
   2.150      case False
   2.151      have "\<exists>x\<in>A. 0 \<le> x"
   2.152 -      by (metis Infty_neq_0 PInf complete_lattice_class.Sup_least
   2.153 -          ereal_infty_less_eq2 linorder_linear)
   2.154 +      by (metis Infty_neq_0(2) PInf complete_lattice_class.Sup_least ereal_infty_less_eq2(1) linorder_linear)
   2.155      then obtain x where "x \<in> A" and "0 \<le> x"
   2.156        by auto
   2.157      have "\<forall>n::nat. \<exists>f. f \<in> A \<and> x + ereal (real n) \<le> f"
   2.158 @@ -1845,7 +1862,6 @@
   2.159    finally show ?thesis .
   2.160  qed
   2.161  
   2.162 -
   2.163  subsection "Relation to @{typ enat}"
   2.164  
   2.165  definition "ereal_of_enat n = (case n of enat n \<Rightarrow> ereal (real n) | \<infinity> \<Rightarrow> \<infinity>)"
   2.166 @@ -2413,12 +2429,6 @@
   2.167    (is "?lhs \<longleftrightarrow> ?rhs")
   2.168    unfolding le_Liminf_iff eventually_sequentially ..
   2.169  
   2.170 -lemma
   2.171 -  fixes X :: "nat \<Rightarrow> ereal"
   2.172 -  shows ereal_incseq_uminus[simp]: "incseq (\<lambda>i. - X i) = decseq X"
   2.173 -    and ereal_decseq_uminus[simp]: "decseq (\<lambda>i. - X i) = incseq X"
   2.174 -  unfolding incseq_def decseq_def by auto
   2.175 -
   2.176  
   2.177  subsubsection {* Tests for code generator *}
   2.178