1.1 --- a/src/HOL/Library/Extended_Real.thy Wed Jul 20 22:14:39 2011 +0200
1.2 +++ b/src/HOL/Library/Extended_Real.thy Thu Jul 21 18:40:31 2011 +0200
1.3 @@ -8,7 +8,7 @@
1.4 header {* Extended real number line *}
1.5
1.6 theory Extended_Real
1.7 - imports Complex_Main Extended_Nat
1.8 +imports Complex_Main Extended_Nat
1.9 begin
1.10
1.11 text {*
1.12 @@ -1244,8 +1244,11 @@
1.13 with Sup_le[of "uminus`A" "-x"] show "x \<le> Inf A"
1.14 unfolding ereal_Sup_uminus_image_eq by force }
1.15 qed
1.16 +
1.17 end
1.18
1.19 +instance ereal :: complete_linorder ..
1.20 +
1.21 lemma ereal_SUPR_uminus:
1.22 fixes f :: "'a => ereal"
1.23 shows "(SUP i : R. -(f i)) = -(INF i : R. f i)"
1.24 @@ -1335,12 +1338,11 @@
1.25 by (cases e) auto
1.26 qed
1.27
1.28 -lemma Sup_eq_top_iff:
1.29 - fixes A :: "'a::{complete_lattice, linorder} set"
1.30 - shows "Sup A = top \<longleftrightarrow> (\<forall>x<top. \<exists>i\<in>A. x < i)"
1.31 +lemma (in complete_linorder) Sup_eq_top_iff: -- "FIXME move"
1.32 + "Sup A = top \<longleftrightarrow> (\<forall>x<top. \<exists>i\<in>A. x < i)"
1.33 proof
1.34 assume *: "Sup A = top"
1.35 - show "(\<forall>x<top. \<exists>i\<in>A. x < i)" unfolding *[symmetric]
1.36 + show "(\<forall>x<top. \<exists>i\<in>A. x < i)" unfolding * [symmetric]
1.37 proof (intro allI impI)
1.38 fix x assume "x < Sup A" then show "\<exists>i\<in>A. x < i"
1.39 unfolding less_Sup_iff by auto
1.40 @@ -1350,7 +1352,7 @@
1.41 show "Sup A = top"
1.42 proof (rule ccontr)
1.43 assume "Sup A \<noteq> top"
1.44 - with top_greatest[of "Sup A"]
1.45 + with top_greatest [of "Sup A"]
1.46 have "Sup A < top" unfolding le_less by auto
1.47 then have "Sup A < Sup A"
1.48 using * unfolding less_Sup_iff by auto
1.49 @@ -1358,8 +1360,8 @@
1.50 qed
1.51 qed
1.52
1.53 -lemma SUP_eq_top_iff:
1.54 - fixes f :: "'a \<Rightarrow> 'b::{complete_lattice, linorder}"
1.55 +lemma (in complete_linorder) SUP_eq_top_iff: -- "FIXME move"
1.56 + fixes f :: "'b \<Rightarrow> 'a"
1.57 shows "(SUP i:A. f i) = top \<longleftrightarrow> (\<forall>x<top. \<exists>i\<in>A. x < f i)"
1.58 unfolding SUPR_def Sup_eq_top_iff by auto
1.59
1.60 @@ -2182,12 +2184,12 @@
1.61 "Limsup net f = (LEAST l. \<forall>y>l. eventually (\<lambda>x. f x < y) net)"
1.62
1.63 lemma Liminf_Sup:
1.64 - fixes f :: "'a => 'b::{complete_lattice, linorder}"
1.65 + fixes f :: "'a => 'b::complete_linorder"
1.66 shows "Liminf net f = Sup {l. \<forall>y<l. eventually (\<lambda>x. y < f x) net}"
1.67 by (auto intro!: Greatest_equality complete_lattice_class.Sup_upper simp: less_Sup_iff Liminf_def)
1.68
1.69 lemma Limsup_Inf:
1.70 - fixes f :: "'a => 'b::{complete_lattice, linorder}"
1.71 + fixes f :: "'a => 'b::complete_linorder"
1.72 shows "Limsup net f = Inf {l. \<forall>y>l. eventually (\<lambda>x. f x < y) net}"
1.73 by (auto intro!: Least_equality complete_lattice_class.Inf_lower simp: Inf_less_iff Limsup_def)
1.74
1.75 @@ -2208,7 +2210,7 @@
1.76 using assms by (auto intro!: Greatest_equality)
1.77
1.78 lemma Limsup_const:
1.79 - fixes c :: "'a::{complete_lattice, linorder}"
1.80 + fixes c :: "'a::complete_linorder"
1.81 assumes ntriv: "\<not> trivial_limit net"
1.82 shows "Limsup net (\<lambda>x. c) = c"
1.83 unfolding Limsup_Inf
1.84 @@ -2222,7 +2224,7 @@
1.85 qed auto
1.86
1.87 lemma Liminf_const:
1.88 - fixes c :: "'a::{complete_lattice, linorder}"
1.89 + fixes c :: "'a::complete_linorder"
1.90 assumes ntriv: "\<not> trivial_limit net"
1.91 shows "Liminf net (\<lambda>x. c) = c"
1.92 unfolding Liminf_Sup
1.93 @@ -2235,18 +2237,17 @@
1.94 qed
1.95 qed auto
1.96
1.97 -lemma mono_set:
1.98 - fixes S :: "('a::order) set"
1.99 - shows "mono S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
1.100 +lemma (in order) mono_set:
1.101 + "mono S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
1.102 by (auto simp: mono_def mem_def)
1.103
1.104 -lemma mono_greaterThan[intro, simp]: "mono {B<..}" unfolding mono_set by auto
1.105 -lemma mono_atLeast[intro, simp]: "mono {B..}" unfolding mono_set by auto
1.106 -lemma mono_UNIV[intro, simp]: "mono UNIV" unfolding mono_set by auto
1.107 -lemma mono_empty[intro, simp]: "mono {}" unfolding mono_set by auto
1.108 +lemma (in order) mono_greaterThan [intro, simp]: "mono {B<..}" unfolding mono_set by auto
1.109 +lemma (in order) mono_atLeast [intro, simp]: "mono {B..}" unfolding mono_set by auto
1.110 +lemma (in order) mono_UNIV [intro, simp]: "mono UNIV" unfolding mono_set by auto
1.111 +lemma (in order) mono_empty [intro, simp]: "mono {}" unfolding mono_set by auto
1.112
1.113 -lemma mono_set_iff:
1.114 - fixes S :: "'a::{linorder,complete_lattice} set"
1.115 +lemma (in complete_linorder) mono_set_iff:
1.116 + fixes S :: "'a set"
1.117 defines "a \<equiv> Inf S"
1.118 shows "mono S \<longleftrightarrow> (S = {a <..} \<or> S = {a..})" (is "_ = ?c")
1.119 proof
1.120 @@ -2257,13 +2258,13 @@
1.121 assume "a \<in> S"
1.122 show ?c
1.123 using mono[OF _ `a \<in> S`]
1.124 - by (auto intro: complete_lattice_class.Inf_lower simp: a_def)
1.125 + by (auto intro: Inf_lower simp: a_def)
1.126 next
1.127 assume "a \<notin> S"
1.128 have "S = {a <..}"
1.129 proof safe
1.130 fix x assume "x \<in> S"
1.131 - then have "a \<le> x" unfolding a_def by (rule complete_lattice_class.Inf_lower)
1.132 + then have "a \<le> x" unfolding a_def by (rule Inf_lower)
1.133 then show "a < x" using `x \<in> S` `a \<notin> S` by (cases "a = x") auto
1.134 next
1.135 fix x assume "a < x"
2.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy Wed Jul 20 22:14:39 2011 +0200
2.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy Thu Jul 21 18:40:31 2011 +0200
2.3 @@ -6,7 +6,7 @@
2.4 header {*Lebesgue Integration*}
2.5
2.6 theory Lebesgue_Integration
2.7 -imports Measure Borel_Space
2.8 + imports Measure Borel_Space
2.9 begin
2.10
2.11 lemma real_ereal_1[simp]: "real (1::ereal) = 1"