author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46757  ad878aff9c15 
child 51475  ebf9d4fd00ba 
permissions  rwrr 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

1 
(* Author: Amine Chaieb and L C Paulson, University of Cambridge *) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

2 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

3 
header {*Sup and Inf Operators on Sets of Reals.*} 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

4 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

5 
theory SupInf 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

6 
imports RComplete 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

7 
begin 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

8 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

9 
instantiation real :: Sup 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

10 
begin 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

11 
definition 
37765  12 
Sup_real_def: "Sup X == (LEAST z::real. \<forall>x\<in>X. x\<le>z)" 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

13 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

14 
instance .. 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

15 
end 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

16 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

17 
instantiation real :: Inf 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

18 
begin 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

19 
definition 
37765  20 
Inf_real_def: "Inf (X::real set) ==  (Sup (uminus ` X))" 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

21 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

22 
instance .. 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

23 
end 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

24 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

25 
subsection{*Supremum of a set of reals*} 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

26 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

27 
lemma Sup_upper [intro]: (*REAL_SUP_UBOUND in HOL4*) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

28 
fixes x :: real 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

29 
assumes x: "x \<in> X" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

30 
and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

31 
shows "x \<le> Sup X" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

32 
proof (auto simp add: Sup_real_def) 
44669
8e6cdb9c00a7
remove redundant lemma reals_complete2 in favor of complete_real
huffman
parents:
37887
diff
changeset

33 
from complete_real 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

34 
obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) > s \<le> z))" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

35 
by (blast intro: x z) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

36 
hence "x \<le> s" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

37 
by (blast intro: x z) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

38 
also with s have "... = (LEAST z. \<forall>x\<in>X. x \<le> z)" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

39 
by (fast intro: Least_equality [symmetric]) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

40 
finally show "x \<le> (LEAST z. \<forall>x\<in>X. x \<le> z)" . 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

41 
qed 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

42 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

43 
lemma Sup_least [intro]: (*REAL_IMP_SUP_LE in HOL4*) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

44 
fixes z :: real 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

45 
assumes x: "X \<noteq> {}" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

46 
and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

47 
shows "Sup X \<le> z" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

48 
proof (auto simp add: Sup_real_def) 
44669
8e6cdb9c00a7
remove redundant lemma reals_complete2 in favor of complete_real
huffman
parents:
37887
diff
changeset

49 
from complete_real x 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

50 
obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) > s \<le> z))" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

51 
by (blast intro: z) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

52 
hence "(LEAST z. \<forall>x\<in>X. x \<le> z) = s" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

53 
by (best intro: Least_equality) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

54 
also with s z have "... \<le> z" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

55 
by blast 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

56 
finally show "(LEAST z. \<forall>x\<in>X. x \<le> z) \<le> z" . 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

57 
qed 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

58 

33609  59 
lemma less_SupE: 
60 
fixes y :: real 

61 
assumes "y < Sup X" "X \<noteq> {}" 

62 
obtains x where "x\<in>X" "y < x" 

63 
by (metis SupInf.Sup_least assms linorder_not_less that) 

64 

33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

65 
lemma Sup_singleton [simp]: "Sup {x::real} = x" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

66 
by (force intro: Least_equality simp add: Sup_real_def) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

67 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

68 
lemma Sup_eq_maximum: (*REAL_SUP_MAX in HOL4*) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

69 
fixes z :: real 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

70 
assumes X: "z \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

71 
shows "Sup X = z" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

72 
by (force intro: Least_equality X z simp add: Sup_real_def) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

73 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

74 
lemma Sup_upper2: (*REAL_IMP_LE_SUP in HOL4*) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

75 
fixes x :: real 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

76 
shows "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X" 
36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36007
diff
changeset

77 
by (metis Sup_upper order_trans) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

78 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

79 
lemma Sup_real_iff : (*REAL_SUP_LE in HOL4*) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

80 
fixes z :: real 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

81 
shows "X ~= {} ==> (!!x. x \<in> X ==> x \<le> z) ==> (\<exists>x\<in>X. y<x) <> y < Sup X" 
44670
d1cb7bc44370
speed up extremely slow metis proof of Sup_real_iff
huffman
parents:
44669
diff
changeset

82 
by (rule iffI, metis less_le_trans Sup_upper, metis Sup_least not_less) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

83 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

84 
lemma Sup_eq: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

85 
fixes a :: real 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

86 
shows "(!!x. x \<in> X \<Longrightarrow> x \<le> a) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

87 
\<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y) \<Longrightarrow> Sup X = a" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

88 
by (metis Sup_least Sup_upper add_le_cancel_left diff_add_cancel insert_absorb 
36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36007
diff
changeset

89 
insert_not_empty order_antisym) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

90 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

91 
lemma Sup_le: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

92 
fixes S :: "real set" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

93 
shows "S \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

94 
by (metis SupInf.Sup_least setle_def) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

95 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

96 
lemma Sup_upper_EX: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

97 
fixes x :: real 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

98 
shows "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> x \<le> z \<Longrightarrow> x \<le> Sup X" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

99 
by blast 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

100 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

101 
lemma Sup_insert_nonempty: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

102 
fixes x :: real 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

103 
assumes x: "x \<in> X" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

104 
and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

105 
shows "Sup (insert a X) = max a (Sup X)" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

106 
proof (cases "Sup X \<le> a") 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

107 
case True 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

108 
thus ?thesis 
36007  109 
apply (simp add: max_def) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

110 
apply (rule Sup_eq_maximum) 
36007  111 
apply (rule insertI1) 
36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36007
diff
changeset

112 
apply (metis Sup_upper [OF _ z] insertE linear order_trans) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

113 
done 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

114 
next 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

115 
case False 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

116 
hence 1:"a < Sup X" by simp 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

117 
have "Sup X \<le> Sup (insert a X)" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

118 
apply (rule Sup_least) 
36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36007
diff
changeset

119 
apply (metis ex_in_conv x) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

120 
apply (rule Sup_upper_EX) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

121 
apply blast 
44669
8e6cdb9c00a7
remove redundant lemma reals_complete2 in favor of complete_real
huffman
parents:
37887
diff
changeset

122 
apply (metis insert_iff linear order_trans z) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

123 
done 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

124 
moreover 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

125 
have "Sup (insert a X) \<le> Sup X" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

126 
apply (rule Sup_least) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

127 
apply blast 
36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36007
diff
changeset

128 
apply (metis False Sup_upper insertE linear z) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

129 
done 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

130 
ultimately have "Sup (insert a X) = Sup X" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

131 
by (blast intro: antisym ) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

132 
thus ?thesis 
36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36007
diff
changeset

133 
by (metis 1 min_max.le_iff_sup less_le) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

134 
qed 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

135 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

136 
lemma Sup_insert_if: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

137 
fixes X :: "real set" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

138 
assumes z: "!!x. x \<in> X \<Longrightarrow> x \<le> z" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

139 
shows "Sup (insert a X) = (if X={} then a else max a (Sup X))" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

140 
by auto (metis Sup_insert_nonempty z) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

141 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

142 
lemma Sup: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

143 
fixes S :: "real set" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

144 
shows "S \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

145 
by (auto simp add: isLub_def setle_def leastP_def isUb_def intro!: setgeI) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

146 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

147 
lemma Sup_finite_Max: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

148 
fixes S :: "real set" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

149 
assumes fS: "finite S" and Se: "S \<noteq> {}" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

150 
shows "Sup S = Max S" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

151 
using fS Se 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

152 
proof 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

153 
let ?m = "Max S" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

154 
from Max_ge[OF fS] have Sm: "\<forall> x\<in> S. x \<le> ?m" by metis 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

155 
with Sup[OF Se] have lub: "isLub UNIV S (Sup S)" by (metis setle_def) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

156 
from Max_in[OF fS Se] lub have mrS: "?m \<le> Sup S" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

157 
by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

158 
moreover 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

159 
have "Sup S \<le> ?m" using Sm lub 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

160 
by (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

161 
ultimately show ?thesis by arith 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

162 
qed 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

163 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

164 
lemma Sup_finite_in: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

165 
fixes S :: "real set" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

166 
assumes fS: "finite S" and Se: "S \<noteq> {}" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

167 
shows "Sup S \<in> S" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

168 
using Sup_finite_Max[OF fS Se] Max_in[OF fS Se] by metis 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

169 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

170 
lemma Sup_finite_ge_iff: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

171 
fixes S :: "real set" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

172 
assumes fS: "finite S" and Se: "S \<noteq> {}" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

173 
shows "a \<le> Sup S \<longleftrightarrow> (\<exists> x \<in> S. a \<le> x)" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

174 
by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS linorder_not_le less_le_trans) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

175 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

176 
lemma Sup_finite_le_iff: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

177 
fixes S :: "real set" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

178 
assumes fS: "finite S" and Se: "S \<noteq> {}" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

179 
shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)" 
36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36007
diff
changeset

180 
by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS order_trans) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

181 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

182 
lemma Sup_finite_gt_iff: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

183 
fixes S :: "real set" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

184 
assumes fS: "finite S" and Se: "S \<noteq> {}" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

185 
shows "a < Sup S \<longleftrightarrow> (\<exists> x \<in> S. a < x)" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

186 
by (metis Se Sup_finite_le_iff fS linorder_not_less) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

187 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

188 
lemma Sup_finite_lt_iff: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

189 
fixes S :: "real set" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

190 
assumes fS: "finite S" and Se: "S \<noteq> {}" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

191 
shows "a > Sup S \<longleftrightarrow> (\<forall> x \<in> S. a > x)" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

192 
by (metis Se Sup_finite_ge_iff fS linorder_not_less) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

193 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

194 
lemma Sup_unique: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

195 
fixes S :: "real set" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

196 
shows "S *<= b \<Longrightarrow> (\<forall>b' < b. \<exists>x \<in> S. b' < x) \<Longrightarrow> Sup S = b" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

197 
unfolding setle_def 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

198 
apply (rule Sup_eq, auto) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

199 
apply (metis linorder_not_less) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

200 
done 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

201 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

202 
lemma Sup_abs_le: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

203 
fixes S :: "real set" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

204 
shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

205 
by (auto simp add: abs_le_interval_iff) (metis Sup_upper2) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

206 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

207 
lemma Sup_bounds: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

208 
fixes S :: "real set" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

209 
assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

210 
shows "a \<le> Sup S \<and> Sup S \<le> b" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

211 
proof 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

212 
from Sup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

213 
hence b: "Sup S \<le> b" using u 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

214 
by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

215 
from Se obtain y where y: "y \<in> S" by blast 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

216 
from lub l have "a \<le> Sup S" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

217 
by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

218 
(metis le_iff_sup le_sup_iff y) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

219 
with b show ?thesis by blast 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

220 
qed 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

221 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

222 
lemma Sup_asclose: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

223 
fixes S :: "real set" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

224 
assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x  l\<bar> \<le> e" shows "\<bar>Sup S  l\<bar> \<le> e" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

225 
proof 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

226 
have th: "\<And>(x::real) l e. \<bar>x  l\<bar> \<le> e \<longleftrightarrow> l  e \<le> x \<and> x \<le> l + e" by arith 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

227 
thus ?thesis using S b Sup_bounds[of S "l  e" "l+e"] unfolding th 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

228 
by (auto simp add: setge_def setle_def) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

229 
qed 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

230 

35581  231 
lemma Sup_lessThan[simp]: "Sup {..<x} = (x::real)" 
232 
by (auto intro!: Sup_eq intro: dense_le) 

233 

234 
lemma Sup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x} = (x::real)" 

235 
by (auto intro!: Sup_eq intro: dense_le_bounded) 

236 

237 
lemma Sup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x} = (x::real)" 

238 
by (auto intro!: Sup_eq intro: dense_le_bounded) 

239 

240 
lemma Sup_atMost[simp]: "Sup {..x} = (x::real)" 

241 
by (auto intro!: Sup_eq_maximum) 

242 

243 
lemma Sup_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Sup {y<..x} = (x::real)" 

244 
by (auto intro!: Sup_eq_maximum) 

245 

246 
lemma Sup_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Sup {y..x} = (x::real)" 

247 
by (auto intro!: Sup_eq_maximum) 

248 

33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

249 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

250 
subsection{*Infimum of a set of reals*} 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

251 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

252 
lemma Inf_lower [intro]: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

253 
fixes z :: real 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

254 
assumes x: "x \<in> X" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

255 
and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

256 
shows "Inf X \<le> x" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

257 
proof  
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

258 
have "x \<le> Sup (uminus ` X)" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

259 
by (rule Sup_upper [where z = "z"]) (auto simp add: image_iff x z) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

260 
thus ?thesis 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

261 
by (auto simp add: Inf_real_def) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

262 
qed 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

263 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

264 
lemma Inf_greatest [intro]: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

265 
fixes z :: real 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

266 
assumes x: "X \<noteq> {}" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

267 
and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

268 
shows "z \<le> Inf X" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

269 
proof  
35216  270 
have "Sup (uminus ` X) \<le> z" using x z by force 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

271 
hence "z \<le>  Sup (uminus ` X)" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

272 
by simp 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

273 
thus ?thesis 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

274 
by (auto simp add: Inf_real_def) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

275 
qed 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

276 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

277 
lemma Inf_singleton [simp]: "Inf {x::real} = x" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

278 
by (simp add: Inf_real_def) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

279 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

280 
lemma Inf_eq_minimum: (*REAL_INF_MIN in HOL4*) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

281 
fixes z :: real 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

282 
assumes x: "z \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

283 
shows "Inf X = z" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

284 
proof  
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

285 
have "Sup (uminus ` X) = z" using x z 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

286 
by (force intro: Sup_eq_maximum x z) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

287 
thus ?thesis 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

288 
by (simp add: Inf_real_def) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

289 
qed 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

290 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

291 
lemma Inf_lower2: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

292 
fixes x :: real 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

293 
shows "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y" 
36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36007
diff
changeset

294 
by (metis Inf_lower order_trans) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

295 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

296 
lemma Inf_real_iff: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

297 
fixes z :: real 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

298 
shows "X \<noteq> {} \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> (\<exists>x\<in>X. x<y) \<longleftrightarrow> Inf X < y" 
36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36007
diff
changeset

299 
by (metis Inf_greatest Inf_lower less_le_not_le linear 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

300 
order_less_le_trans) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

301 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

302 
lemma Inf_eq: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

303 
fixes a :: real 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

304 
shows "(!!x. x \<in> X \<Longrightarrow> a \<le> x) \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a) \<Longrightarrow> Inf X = a" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

305 
by (metis Inf_greatest Inf_lower add_le_cancel_left diff_add_cancel 
36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36007
diff
changeset

306 
insert_absorb insert_not_empty order_antisym) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

307 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

308 
lemma Inf_ge: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

309 
fixes S :: "real set" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

310 
shows "S \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

311 
by (metis SupInf.Inf_greatest setge_def) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

312 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

313 
lemma Inf_lower_EX: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

314 
fixes x :: real 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

315 
shows "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> z \<le> x \<Longrightarrow> Inf X \<le> x" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

316 
by blast 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

317 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

318 
lemma Inf_insert_nonempty: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

319 
fixes x :: real 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

320 
assumes x: "x \<in> X" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

321 
and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

322 
shows "Inf (insert a X) = min a (Inf X)" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

323 
proof (cases "a \<le> Inf X") 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

324 
case True 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

325 
thus ?thesis 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

326 
by (simp add: min_def) 
36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36007
diff
changeset

327 
(blast intro: Inf_eq_minimum order_trans z) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

328 
next 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

329 
case False 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

330 
hence 1:"Inf X < a" by simp 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

331 
have "Inf (insert a X) \<le> Inf X" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

332 
apply (rule Inf_greatest) 
36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36007
diff
changeset

333 
apply (metis ex_in_conv x) 
36007  334 
apply (rule Inf_lower_EX) 
335 
apply (erule insertI2) 

44669
8e6cdb9c00a7
remove redundant lemma reals_complete2 in favor of complete_real
huffman
parents:
37887
diff
changeset

336 
apply (metis insert_iff linear order_trans z) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

337 
done 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

338 
moreover 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

339 
have "Inf X \<le> Inf (insert a X)" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

340 
apply (rule Inf_greatest) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

341 
apply blast 
36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36007
diff
changeset

342 
apply (metis False Inf_lower insertE linear z) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

343 
done 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

344 
ultimately have "Inf (insert a X) = Inf X" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

345 
by (blast intro: antisym ) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

346 
thus ?thesis 
36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36007
diff
changeset

347 
by (metis False min_max.inf_absorb2 linear) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

348 
qed 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

349 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

350 
lemma Inf_insert_if: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

351 
fixes X :: "real set" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

352 
assumes z: "!!x. x \<in> X \<Longrightarrow> z \<le> x" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

353 
shows "Inf (insert a X) = (if X={} then a else min a (Inf X))" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

354 
by auto (metis Inf_insert_nonempty z) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

355 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

356 
lemma Inf_greater: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

357 
fixes z :: real 
35823
bd26885af9f4
dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35581
diff
changeset

358 
shows "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z" 
45966  359 
by (metis Inf_real_iff not_leE) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

360 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

361 
lemma Inf_close: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

362 
fixes e :: real 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

363 
shows "X \<noteq> {} \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>x \<in> X. x < Inf X + e" 
35823
bd26885af9f4
dropped odd interpretation of comm_monoid_mult into comm_monoid_add
haftmann
parents:
35581
diff
changeset

364 
by (metis add_strict_increasing add_commute Inf_greater linorder_not_le pos_add_strict) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

365 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

366 
lemma Inf_finite_Min: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

367 
fixes S :: "real set" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

368 
shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> Inf S = Min S" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

369 
by (simp add: Inf_real_def Sup_finite_Max image_image) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

370 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

371 
lemma Inf_finite_in: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

372 
fixes S :: "real set" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

373 
assumes fS: "finite S" and Se: "S \<noteq> {}" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

374 
shows "Inf S \<in> S" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

375 
using Inf_finite_Min[OF fS Se] Min_in[OF fS Se] by metis 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

376 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

377 
lemma Inf_finite_ge_iff: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

378 
fixes S :: "real set" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

379 
shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)" 
36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36007
diff
changeset

380 
by (metis Inf_finite_Min Inf_finite_in Min_le order_trans) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

381 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

382 
lemma Inf_finite_le_iff: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

383 
fixes S :: "real set" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

384 
shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

385 
by (metis Inf_finite_Min Inf_finite_ge_iff Inf_finite_in Min_le 
36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36007
diff
changeset

386 
order_antisym linear) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

387 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

388 
lemma Inf_finite_gt_iff: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

389 
fixes S :: "real set" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

390 
shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a < Inf S \<longleftrightarrow> (\<forall> x \<in> S. a < x)" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

391 
by (metis Inf_finite_le_iff linorder_not_less) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

392 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

393 
lemma Inf_finite_lt_iff: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

394 
fixes S :: "real set" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

395 
shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a > Inf S \<longleftrightarrow> (\<exists> x \<in> S. a > x)" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

396 
by (metis Inf_finite_ge_iff linorder_not_less) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

397 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

398 
lemma Inf_unique: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

399 
fixes S :: "real set" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

400 
shows "b <=* S \<Longrightarrow> (\<forall>b' > b. \<exists>x \<in> S. b' > x) \<Longrightarrow> Inf S = b" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

401 
unfolding setge_def 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

402 
apply (rule Inf_eq, auto) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

403 
apply (metis less_le_not_le linorder_not_less) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

404 
done 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

405 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

406 
lemma Inf_abs_ge: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

407 
fixes S :: "real set" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

408 
shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

409 
by (simp add: Inf_real_def) (rule Sup_abs_le, auto) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

410 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

411 
lemma Inf_asclose: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

412 
fixes S :: "real set" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

413 
assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x  l\<bar> \<le> e" shows "\<bar>Inf S  l\<bar> \<le> e" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

414 
proof  
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

415 
have "\<bar> Sup (uminus ` S)  l\<bar> = \<bar>Sup (uminus ` S)  (l)\<bar>" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

416 
by auto 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

417 
also have "... \<le> e" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

418 
apply (rule Sup_asclose) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

419 
apply (auto simp add: S) 
37887  420 
apply (metis abs_minus_add_cancel b add_commute diff_minus) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

421 
done 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

422 
finally have "\<bar> Sup (uminus ` S)  l\<bar> \<le> e" . 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

423 
thus ?thesis 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

424 
by (simp add: Inf_real_def) 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

425 
qed 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

426 

35581  427 
lemma Inf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x} = (y::real)" 
428 
by (simp add: Inf_real_def) 

429 

430 
lemma Inf_atLeastLessThan[simp]: "y < x \<Longrightarrow> Inf {y..<x} = (y::real)" 

431 
by (simp add: Inf_real_def) 

432 

433 
lemma Inf_atLeast[simp]: "Inf {x..} = (x::real)" 

434 
by (simp add: Inf_real_def) 

435 

436 
lemma Inf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x} = (y::real)" 

437 
by (simp add: Inf_real_def) 

438 

439 
lemma Inf_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Inf {y..x} = (y::real)" 

440 
by (simp add: Inf_real_def) 

441 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33269
diff
changeset

442 
subsection{*Relate max and min to Sup and Inf.*} 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

443 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

444 
lemma real_max_Sup: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

445 
fixes x :: real 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

446 
shows "max x y = Sup {x,y}" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

447 
proof 
46757  448 
have "Sup {x,y} \<le> max x y" by (simp add: Sup_finite_le_iff) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

449 
moreover 
46757  450 
have "max x y \<le> Sup {x,y}" by (simp add: linorder_linear Sup_finite_ge_iff) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

451 
ultimately show ?thesis by arith 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

452 
qed 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

453 

3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

454 
lemma real_min_Inf: 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

455 
fixes x :: real 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

456 
shows "min x y = Inf {x,y}" 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

457 
proof 
46757  458 
have "Inf {x,y} \<le> min x y" by (simp add: linorder_linear Inf_finite_le_iff) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

459 
moreover 
46757  460 
have "min x y \<le> Inf {x,y}" by (simp add: Inf_finite_ge_iff) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

461 
ultimately show ?thesis by arith 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

462 
qed 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

463 

33609  464 
lemma reals_complete_interval: 
465 
fixes a::real and b::real 

466 
assumes "a < b" and "P a" and "~P b" 

467 
shows "\<exists>c. a \<le> c & c \<le> b & (\<forall>x. a \<le> x & x < c > P x) & 

468 
(\<forall>d. (\<forall>x. a \<le> x & x < d > P x) > d \<le> c)" 

469 
proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d > P x}"], auto) 

470 
show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}" 

471 
by (rule SupInf.Sup_upper [where z=b], auto) 

36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36007
diff
changeset

472 
(metis `a < b` `\<not> P b` linear less_le) 
33609  473 
next 
474 
show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b" 

475 
apply (rule SupInf.Sup_least) 

476 
apply (auto simp add: ) 

477 
apply (metis less_le_not_le) 

36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36007
diff
changeset

478 
apply (metis `a<b` `~ P b` linear less_le) 
33609  479 
done 
480 
next 

481 
fix x 

482 
assume x: "a \<le> x" and lt: "x < Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}" 

483 
show "P x" 

484 
apply (rule less_SupE [OF lt], auto) 

485 
apply (metis less_le_not_le) 

486 
apply (metis x) 

487 
done 

488 
next 

489 
fix d 

490 
assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x" 

491 
thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}" 

492 
by (rule_tac z="b" in SupInf.Sup_upper, auto) 

36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36007
diff
changeset

493 
(metis `a<b` `~ P b` linear less_le) 
33609  494 
qed 
495 

33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

496 
end 