author  haftmann 
Wed, 12 Apr 2017 09:27:47 +0200  
changeset 65466  b0f89998c2a1 
parent 63540  f8652d0534fa 
child 67091  1393c2340eec 
permissions  rwrr 
52265  1 
(* Title: HOL/Conditionally_Complete_Lattices.thy 
51518
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

2 
Author: Amine Chaieb and L C Paulson, University of Cambridge 
51643  3 
Author: Johannes Hölzl, TU München 
54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

4 
Author: Luke S. Serafin, Carnegie Mellon University 
51518
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

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

6 

60758  7 
section \<open>Conditionallycomplete Lattices\<close> 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

8 

51773  9 
theory Conditionally_Complete_Lattices 
63331  10 
imports Finite_Set Lattices_Big Set_Interval 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

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

12 

65466  13 
context linorder 
14 
begin 

15 

16 
lemma Sup_fin_eq_Max: 

17 
"finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X" 

51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

18 
by (induct X rule: finite_ne_induct) (simp_all add: sup_max) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

19 

65466  20 
lemma Inf_fin_eq_Min: 
21 
"finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf_fin X = Min X" 

51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

22 
by (induct X rule: finite_ne_induct) (simp_all add: inf_min) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

23 

65466  24 
end 
25 

54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

26 
context preorder 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

27 
begin 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

28 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

29 
definition "bdd_above A \<longleftrightarrow> (\<exists>M. \<forall>x \<in> A. x \<le> M)" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

30 
definition "bdd_below A \<longleftrightarrow> (\<exists>m. \<forall>x \<in> A. m \<le> x)" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

31 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

32 
lemma bdd_aboveI[intro]: "(\<And>x. x \<in> A \<Longrightarrow> x \<le> M) \<Longrightarrow> bdd_above A" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

33 
by (auto simp: bdd_above_def) 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

34 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

35 
lemma bdd_belowI[intro]: "(\<And>x. x \<in> A \<Longrightarrow> m \<le> x) \<Longrightarrow> bdd_below A" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

36 
by (auto simp: bdd_below_def) 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

37 

54263
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54262
diff
changeset

38 
lemma bdd_aboveI2: "(\<And>x. x \<in> A \<Longrightarrow> f x \<le> M) \<Longrightarrow> bdd_above (f`A)" 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54262
diff
changeset

39 
by force 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54262
diff
changeset

40 

c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54262
diff
changeset

41 
lemma bdd_belowI2: "(\<And>x. x \<in> A \<Longrightarrow> m \<le> f x) \<Longrightarrow> bdd_below (f`A)" 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54262
diff
changeset

42 
by force 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54262
diff
changeset

43 

54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

44 
lemma bdd_above_empty [simp, intro]: "bdd_above {}" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

45 
unfolding bdd_above_def by auto 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

46 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

47 
lemma bdd_below_empty [simp, intro]: "bdd_below {}" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

48 
unfolding bdd_below_def by auto 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

49 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

50 
lemma bdd_above_mono: "bdd_above B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> bdd_above A" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

51 
by (metis (full_types) bdd_above_def order_class.le_neq_trans psubsetD) 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

52 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

53 
lemma bdd_below_mono: "bdd_below B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> bdd_below A" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

54 
by (metis bdd_below_def order_class.le_neq_trans psubsetD) 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

55 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

56 
lemma bdd_above_Int1 [simp]: "bdd_above A \<Longrightarrow> bdd_above (A \<inter> B)" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

57 
using bdd_above_mono by auto 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

58 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

59 
lemma bdd_above_Int2 [simp]: "bdd_above B \<Longrightarrow> bdd_above (A \<inter> B)" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

60 
using bdd_above_mono by auto 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

61 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

62 
lemma bdd_below_Int1 [simp]: "bdd_below A \<Longrightarrow> bdd_below (A \<inter> B)" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

63 
using bdd_below_mono by auto 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

64 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

65 
lemma bdd_below_Int2 [simp]: "bdd_below B \<Longrightarrow> bdd_below (A \<inter> B)" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

66 
using bdd_below_mono by auto 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

67 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

68 
lemma bdd_above_Ioo [simp, intro]: "bdd_above {a <..< b}" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

69 
by (auto simp add: bdd_above_def intro!: exI[of _ b] less_imp_le) 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

70 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

71 
lemma bdd_above_Ico [simp, intro]: "bdd_above {a ..< b}" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

72 
by (auto simp add: bdd_above_def intro!: exI[of _ b] less_imp_le) 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

73 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

74 
lemma bdd_above_Iio [simp, intro]: "bdd_above {..< b}" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

75 
by (auto simp add: bdd_above_def intro: exI[of _ b] less_imp_le) 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

76 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

77 
lemma bdd_above_Ioc [simp, intro]: "bdd_above {a <.. b}" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

78 
by (auto simp add: bdd_above_def intro: exI[of _ b] less_imp_le) 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

79 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

80 
lemma bdd_above_Icc [simp, intro]: "bdd_above {a .. b}" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

81 
by (auto simp add: bdd_above_def intro: exI[of _ b] less_imp_le) 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

82 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

83 
lemma bdd_above_Iic [simp, intro]: "bdd_above {.. b}" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

84 
by (auto simp add: bdd_above_def intro: exI[of _ b] less_imp_le) 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

85 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

86 
lemma bdd_below_Ioo [simp, intro]: "bdd_below {a <..< b}" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

87 
by (auto simp add: bdd_below_def intro!: exI[of _ a] less_imp_le) 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

88 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

89 
lemma bdd_below_Ioc [simp, intro]: "bdd_below {a <.. b}" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

90 
by (auto simp add: bdd_below_def intro!: exI[of _ a] less_imp_le) 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

91 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

92 
lemma bdd_below_Ioi [simp, intro]: "bdd_below {a <..}" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

93 
by (auto simp add: bdd_below_def intro: exI[of _ a] less_imp_le) 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

94 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

95 
lemma bdd_below_Ico [simp, intro]: "bdd_below {a ..< b}" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

96 
by (auto simp add: bdd_below_def intro: exI[of _ a] less_imp_le) 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

97 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

98 
lemma bdd_below_Icc [simp, intro]: "bdd_below {a .. b}" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

99 
by (auto simp add: bdd_below_def intro: exI[of _ a] less_imp_le) 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

100 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

101 
lemma bdd_below_Ici [simp, intro]: "bdd_below {a ..}" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

102 
by (auto simp add: bdd_below_def intro: exI[of _ a] less_imp_le) 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

103 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

104 
end 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

105 

54261  106 
lemma (in order_top) bdd_above_top[simp, intro!]: "bdd_above A" 
107 
by (rule bdd_aboveI[of _ top]) simp 

108 

109 
lemma (in order_bot) bdd_above_bot[simp, intro!]: "bdd_below A" 

110 
by (rule bdd_belowI[of _ bot]) simp 

111 

59452
2538b2c51769
ereal: tuned proofs concerning continuity and suprema
hoelzl
parents:
58889
diff
changeset

112 
lemma bdd_above_image_mono: "mono f \<Longrightarrow> bdd_above A \<Longrightarrow> bdd_above (f`A)" 
2538b2c51769
ereal: tuned proofs concerning continuity and suprema
hoelzl
parents:
58889
diff
changeset

113 
by (auto simp: bdd_above_def mono_def) 
2538b2c51769
ereal: tuned proofs concerning continuity and suprema
hoelzl
parents:
58889
diff
changeset

114 

2538b2c51769
ereal: tuned proofs concerning continuity and suprema
hoelzl
parents:
58889
diff
changeset

115 
lemma bdd_below_image_mono: "mono f \<Longrightarrow> bdd_below A \<Longrightarrow> bdd_below (f`A)" 
2538b2c51769
ereal: tuned proofs concerning continuity and suprema
hoelzl
parents:
58889
diff
changeset

116 
by (auto simp: bdd_below_def mono_def) 
63331  117 

59452
2538b2c51769
ereal: tuned proofs concerning continuity and suprema
hoelzl
parents:
58889
diff
changeset

118 
lemma bdd_above_image_antimono: "antimono f \<Longrightarrow> bdd_below A \<Longrightarrow> bdd_above (f`A)" 
2538b2c51769
ereal: tuned proofs concerning continuity and suprema
hoelzl
parents:
58889
diff
changeset

119 
by (auto simp: bdd_above_def bdd_below_def antimono_def) 
54262
326fd7103cb4
generalize bdd_above/below_uminus to ordered_ab_group_add
hoelzl
parents:
54261
diff
changeset

120 

59452
2538b2c51769
ereal: tuned proofs concerning continuity and suprema
hoelzl
parents:
58889
diff
changeset

121 
lemma bdd_below_image_antimono: "antimono f \<Longrightarrow> bdd_above A \<Longrightarrow> bdd_below (f`A)" 
2538b2c51769
ereal: tuned proofs concerning continuity and suprema
hoelzl
parents:
58889
diff
changeset

122 
by (auto simp: bdd_above_def bdd_below_def antimono_def) 
2538b2c51769
ereal: tuned proofs concerning continuity and suprema
hoelzl
parents:
58889
diff
changeset

123 

2538b2c51769
ereal: tuned proofs concerning continuity and suprema
hoelzl
parents:
58889
diff
changeset

124 
lemma 
54262
326fd7103cb4
generalize bdd_above/below_uminus to ordered_ab_group_add
hoelzl
parents:
54261
diff
changeset

125 
fixes X :: "'a::ordered_ab_group_add set" 
59452
2538b2c51769
ereal: tuned proofs concerning continuity and suprema
hoelzl
parents:
58889
diff
changeset

126 
shows bdd_above_uminus[simp]: "bdd_above (uminus ` X) \<longleftrightarrow> bdd_below X" 
2538b2c51769
ereal: tuned proofs concerning continuity and suprema
hoelzl
parents:
58889
diff
changeset

127 
and bdd_below_uminus[simp]: "bdd_below (uminus ` X) \<longleftrightarrow> bdd_above X" 
2538b2c51769
ereal: tuned proofs concerning continuity and suprema
hoelzl
parents:
58889
diff
changeset

128 
using bdd_above_image_antimono[of uminus X] bdd_below_image_antimono[of uminus "uminus`X"] 
2538b2c51769
ereal: tuned proofs concerning continuity and suprema
hoelzl
parents:
58889
diff
changeset

129 
using bdd_below_image_antimono[of uminus X] bdd_above_image_antimono[of uminus "uminus`X"] 
2538b2c51769
ereal: tuned proofs concerning continuity and suprema
hoelzl
parents:
58889
diff
changeset

130 
by (auto simp: antimono_def image_image) 
54262
326fd7103cb4
generalize bdd_above/below_uminus to ordered_ab_group_add
hoelzl
parents:
54261
diff
changeset

131 

54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

132 
context lattice 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

133 
begin 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

134 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

135 
lemma bdd_above_insert [simp]: "bdd_above (insert a A) = bdd_above A" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

136 
by (auto simp: bdd_above_def intro: le_supI2 sup_ge1) 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

137 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

138 
lemma bdd_below_insert [simp]: "bdd_below (insert a A) = bdd_below A" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

139 
by (auto simp: bdd_below_def intro: le_infI2 inf_le1) 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

140 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

141 
lemma bdd_finite [simp]: 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

142 
assumes "finite A" shows bdd_above_finite: "bdd_above A" and bdd_below_finite: "bdd_below A" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

143 
using assms by (induct rule: finite_induct, auto) 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

144 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

145 
lemma bdd_above_Un [simp]: "bdd_above (A \<union> B) = (bdd_above A \<and> bdd_above B)" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

146 
proof 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

147 
assume "bdd_above (A \<union> B)" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

148 
thus "bdd_above A \<and> bdd_above B" unfolding bdd_above_def by auto 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

149 
next 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

150 
assume "bdd_above A \<and> bdd_above B" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

151 
then obtain a b where "\<forall>x\<in>A. x \<le> a" "\<forall>x\<in>B. x \<le> b" unfolding bdd_above_def by auto 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

152 
hence "\<forall>x \<in> A \<union> B. x \<le> sup a b" by (auto intro: Un_iff le_supI1 le_supI2) 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

153 
thus "bdd_above (A \<union> B)" unfolding bdd_above_def .. 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

154 
qed 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

155 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

156 
lemma bdd_below_Un [simp]: "bdd_below (A \<union> B) = (bdd_below A \<and> bdd_below B)" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

157 
proof 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

158 
assume "bdd_below (A \<union> B)" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

159 
thus "bdd_below A \<and> bdd_below B" unfolding bdd_below_def by auto 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

160 
next 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

161 
assume "bdd_below A \<and> bdd_below B" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

162 
then obtain a b where "\<forall>x\<in>A. a \<le> x" "\<forall>x\<in>B. b \<le> x" unfolding bdd_below_def by auto 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

163 
hence "\<forall>x \<in> A \<union> B. inf a b \<le> x" by (auto intro: Un_iff le_infI1 le_infI2) 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

164 
thus "bdd_below (A \<union> B)" unfolding bdd_below_def .. 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

165 
qed 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

166 

54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

167 
lemma bdd_above_sup[simp]: "bdd_above ((\<lambda>x. sup (f x) (g x)) ` A) \<longleftrightarrow> bdd_above (f`A) \<and> bdd_above (g`A)" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

168 
by (auto simp: bdd_above_def intro: le_supI1 le_supI2) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

169 

71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

170 
lemma bdd_below_inf[simp]: "bdd_below ((\<lambda>x. inf (f x) (g x)) ` A) \<longleftrightarrow> bdd_below (f`A) \<and> bdd_below (g`A)" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

171 
by (auto simp: bdd_below_def intro: le_infI1 le_infI2) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

172 

54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

173 
end 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

174 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

175 

60758  176 
text \<open> 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

177 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

178 
To avoid name classes with the @{class complete_lattice}class we prefix @{const Sup} and 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

179 
@{const Inf} in theorem names with c. 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

180 

60758  181 
\<close> 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

182 

51773  183 
class conditionally_complete_lattice = lattice + Sup + Inf + 
54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

184 
assumes cInf_lower: "x \<in> X \<Longrightarrow> bdd_below X \<Longrightarrow> Inf X \<le> x" 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

185 
and cInf_greatest: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X" 
54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

186 
assumes cSup_upper: "x \<in> X \<Longrightarrow> bdd_above X \<Longrightarrow> x \<le> Sup X" 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

187 
and cSup_least: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z" 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

188 
begin 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

189 

54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

190 
lemma cSup_upper2: "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> bdd_above X \<Longrightarrow> y \<le> Sup X" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

191 
by (metis cSup_upper order_trans) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

192 

71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

193 
lemma cInf_lower2: "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> bdd_below X \<Longrightarrow> Inf X \<le> y" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

194 
by (metis cInf_lower order_trans) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

195 

71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

196 
lemma cSup_mono: "B \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> (\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. b \<le> a) \<Longrightarrow> Sup B \<le> Sup A" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

197 
by (metis cSup_least cSup_upper2) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

198 

71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

199 
lemma cInf_mono: "B \<noteq> {} \<Longrightarrow> bdd_below A \<Longrightarrow> (\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b) \<Longrightarrow> Inf A \<le> Inf B" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

200 
by (metis cInf_greatest cInf_lower2) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

201 

71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

202 
lemma cSup_subset_mono: "A \<noteq> {} \<Longrightarrow> bdd_above B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> Sup A \<le> Sup B" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

203 
by (metis cSup_least cSup_upper subsetD) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

204 

71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

205 
lemma cInf_superset_mono: "A \<noteq> {} \<Longrightarrow> bdd_below B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> Inf B \<le> Inf A" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

206 
by (metis cInf_greatest cInf_lower subsetD) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

207 

54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

208 
lemma cSup_eq_maximum: "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X = z" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

209 
by (intro antisym cSup_upper[of z X] cSup_least[of X z]) auto 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

210 

54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

211 
lemma cInf_eq_minimum: "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X = z" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

212 
by (intro antisym cInf_lower[of z X] cInf_greatest[of X z]) auto 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

213 

54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

214 
lemma cSup_le_iff: "S \<noteq> {} \<Longrightarrow> bdd_above S \<Longrightarrow> Sup S \<le> a \<longleftrightarrow> (\<forall>x\<in>S. x \<le> a)" 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

215 
by (metis order_trans cSup_upper cSup_least) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

216 

54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

217 
lemma le_cInf_iff: "S \<noteq> {} \<Longrightarrow> bdd_below S \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall>x\<in>S. a \<le> x)" 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

218 
by (metis order_trans cInf_lower cInf_greatest) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

219 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

220 
lemma cSup_eq_non_empty: 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

221 
assumes 1: "X \<noteq> {}" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

222 
assumes 2: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

223 
assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

224 
shows "Sup X = a" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

225 
by (intro 3 1 antisym cSup_least) (auto intro: 2 1 cSup_upper) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

226 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

227 
lemma cInf_eq_non_empty: 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

228 
assumes 1: "X \<noteq> {}" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

229 
assumes 2: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

230 
assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

231 
shows "Inf X = a" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

232 
by (intro 3 1 antisym cInf_greatest) (auto intro: 2 1 cInf_lower) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

233 

54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

234 
lemma cInf_cSup: "S \<noteq> {} \<Longrightarrow> bdd_below S \<Longrightarrow> Inf S = Sup {x. \<forall>s\<in>S. x \<le> s}" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

235 
by (rule cInf_eq_non_empty) (auto intro!: cSup_upper cSup_least simp: bdd_below_def) 
51518
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

236 

54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

237 
lemma cSup_cInf: "S \<noteq> {} \<Longrightarrow> bdd_above S \<Longrightarrow> Sup S = Inf {x. \<forall>s\<in>S. s \<le> x}" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

238 
by (rule cSup_eq_non_empty) (auto intro!: cInf_lower cInf_greatest simp: bdd_above_def) 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

239 

adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

240 
lemma cSup_insert: "X \<noteq> {} \<Longrightarrow> bdd_above X \<Longrightarrow> Sup (insert a X) = sup a (Sup X)" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

241 
by (intro cSup_eq_non_empty) (auto intro: le_supI2 cSup_upper cSup_least) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

242 

54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

243 
lemma cInf_insert: "X \<noteq> {} \<Longrightarrow> bdd_below X \<Longrightarrow> Inf (insert a X) = inf a (Inf X)" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

244 
by (intro cInf_eq_non_empty) (auto intro: le_infI2 cInf_lower cInf_greatest) 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

245 

54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

246 
lemma cSup_singleton [simp]: "Sup {x} = x" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

247 
by (intro cSup_eq_maximum) auto 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

248 

71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

249 
lemma cInf_singleton [simp]: "Inf {x} = x" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

250 
by (intro cInf_eq_minimum) auto 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

251 

54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

252 
lemma cSup_insert_If: "bdd_above X \<Longrightarrow> Sup (insert a X) = (if X = {} then a else sup a (Sup X))" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

253 
using cSup_insert[of X] by simp 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

254 

54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

255 
lemma cInf_insert_If: "bdd_below X \<Longrightarrow> Inf (insert a X) = (if X = {} then a else inf a (Inf X))" 
54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

256 
using cInf_insert[of X] by simp 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

257 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

258 
lemma le_cSup_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> x \<le> Sup X" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

259 
proof (induct X arbitrary: x rule: finite_induct) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

260 
case (insert x X y) then show ?case 
54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

261 
by (cases "X = {}") (auto simp: cSup_insert intro: le_supI2) 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

262 
qed simp 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

263 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

264 
lemma cInf_le_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> Inf X \<le> x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

265 
proof (induct X arbitrary: x rule: finite_induct) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

266 
case (insert x X y) then show ?case 
54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

267 
by (cases "X = {}") (auto simp: cInf_insert intro: le_infI2) 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

268 
qed simp 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

269 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

270 
lemma cSup_eq_Sup_fin: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Sup_fin X" 
54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

271 
by (induct X rule: finite_ne_induct) (simp_all add: cSup_insert) 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

272 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

273 
lemma cInf_eq_Inf_fin: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Inf_fin X" 
54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

274 
by (induct X rule: finite_ne_induct) (simp_all add: cInf_insert) 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

275 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

276 
lemma cSup_atMost[simp]: "Sup {..x} = x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

277 
by (auto intro!: cSup_eq_maximum) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

278 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

279 
lemma cSup_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Sup {y<..x} = x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

280 
by (auto intro!: cSup_eq_maximum) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

281 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

282 
lemma cSup_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Sup {y..x} = x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

283 
by (auto intro!: cSup_eq_maximum) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

284 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

285 
lemma cInf_atLeast[simp]: "Inf {x..} = x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

286 
by (auto intro!: cInf_eq_minimum) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

287 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

288 
lemma cInf_atLeastLessThan[simp]: "y < x \<Longrightarrow> Inf {y..<x} = y" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

289 
by (auto intro!: cInf_eq_minimum) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

290 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

291 
lemma cInf_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Inf {y..x} = y" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

292 
by (auto intro!: cInf_eq_minimum) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

293 

56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56166
diff
changeset

294 
lemma cINF_lower: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> INFIMUM A f \<le> f x" 
56166  295 
using cInf_lower [of _ "f ` A"] by simp 
54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

296 

56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56166
diff
changeset

297 
lemma cINF_greatest: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> m \<le> f x) \<Longrightarrow> m \<le> INFIMUM A f" 
56166  298 
using cInf_greatest [of "f ` A"] by auto 
54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

299 

56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56166
diff
changeset

300 
lemma cSUP_upper: "x \<in> A \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> f x \<le> SUPREMUM A f" 
56166  301 
using cSup_upper [of _ "f ` A"] by simp 
54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

302 

56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56166
diff
changeset

303 
lemma cSUP_least: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> M) \<Longrightarrow> SUPREMUM A f \<le> M" 
56166  304 
using cSup_least [of "f ` A"] by auto 
54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

305 

56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56166
diff
changeset

306 
lemma cINF_lower2: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<le> u \<Longrightarrow> INFIMUM A f \<le> u" 
63092  307 
by (auto intro: cINF_lower order_trans) 
54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

308 

56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56166
diff
changeset

309 
lemma cSUP_upper2: "bdd_above (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> u \<le> f x \<Longrightarrow> u \<le> SUPREMUM A f" 
63092  310 
by (auto intro: cSUP_upper order_trans) 
54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

311 

60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60172
diff
changeset

312 
lemma cSUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (SUP x:A. c) = c" 
54261  313 
by (intro antisym cSUP_least) (auto intro: cSUP_upper) 
314 

60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60172
diff
changeset

315 
lemma cINF_const [simp]: "A \<noteq> {} \<Longrightarrow> (INF x:A. c) = c" 
54261  316 
by (intro antisym cINF_greatest) (auto intro: cINF_lower) 
317 

56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56166
diff
changeset

318 
lemma le_cINF_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> u \<le> INFIMUM A f \<longleftrightarrow> (\<forall>x\<in>A. u \<le> f x)" 
63092  319 
by (metis cINF_greatest cINF_lower order_trans) 
54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

320 

56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56166
diff
changeset

321 
lemma cSUP_le_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPREMUM A f \<le> u \<longleftrightarrow> (\<forall>x\<in>A. f x \<le> u)" 
63092  322 
by (metis cSUP_least cSUP_upper order_trans) 
54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

323 

54263
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54262
diff
changeset

324 
lemma less_cINF_D: "bdd_below (f`A) \<Longrightarrow> y < (INF i:A. f i) \<Longrightarrow> i \<in> A \<Longrightarrow> y < f i" 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54262
diff
changeset

325 
by (metis cINF_lower less_le_trans) 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54262
diff
changeset

326 

c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54262
diff
changeset

327 
lemma cSUP_lessD: "bdd_above (f`A) \<Longrightarrow> (SUP i:A. f i) < y \<Longrightarrow> i \<in> A \<Longrightarrow> f i < y" 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54262
diff
changeset

328 
by (metis cSUP_upper le_less_trans) 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54262
diff
changeset

329 

56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56166
diff
changeset

330 
lemma cINF_insert: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> INFIMUM (insert a A) f = inf (f a) (INFIMUM A f)" 
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61824
diff
changeset

331 
by (metis cInf_insert image_insert image_is_empty) 
54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

332 

56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56166
diff
changeset

333 
lemma cSUP_insert: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPREMUM (insert a A) f = sup (f a) (SUPREMUM A f)" 
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
61824
diff
changeset

334 
by (metis cSup_insert image_insert image_is_empty) 
54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

335 

56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56166
diff
changeset

336 
lemma cINF_mono: "B \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> (\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> INFIMUM A f \<le> INFIMUM B g" 
56166  337 
using cInf_mono [of "g ` B" "f ` A"] by auto 
54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

338 

56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56166
diff
changeset

339 
lemma cSUP_mono: "A \<noteq> {} \<Longrightarrow> bdd_above (g ` B) \<Longrightarrow> (\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> SUPREMUM A f \<le> SUPREMUM B g" 
56166  340 
using cSup_mono [of "f ` A" "g ` B"] by auto 
54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

341 

56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56166
diff
changeset

342 
lemma cINF_superset_mono: "A \<noteq> {} \<Longrightarrow> bdd_below (g ` B) \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> g x \<le> f x) \<Longrightarrow> INFIMUM B g \<le> INFIMUM A f" 
54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

343 
by (rule cINF_mono) auto 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

344 

56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56166
diff
changeset

345 
lemma cSUP_subset_mono: "A \<noteq> {} \<Longrightarrow> bdd_above (g ` B) \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> SUPREMUM A f \<le> SUPREMUM B g" 
54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

346 
by (rule cSUP_mono) auto 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

347 

71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

348 
lemma less_eq_cInf_inter: "bdd_below A \<Longrightarrow> bdd_below B \<Longrightarrow> A \<inter> B \<noteq> {} \<Longrightarrow> inf (Inf A) (Inf B) \<le> Inf (A \<inter> B)" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

349 
by (metis cInf_superset_mono lattice_class.inf_sup_ord(1) le_infI1) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

350 

71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

351 
lemma cSup_inter_less_eq: "bdd_above A \<Longrightarrow> bdd_above B \<Longrightarrow> A \<inter> B \<noteq> {} \<Longrightarrow> Sup (A \<inter> B) \<le> sup (Sup A) (Sup B) " 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

352 
by (metis cSup_subset_mono lattice_class.inf_sup_ord(1) le_supI1) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

353 

71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

354 
lemma cInf_union_distrib: "A \<noteq> {} \<Longrightarrow> bdd_below A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_below B \<Longrightarrow> Inf (A \<union> B) = inf (Inf A) (Inf B)" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

355 
by (intro antisym le_infI cInf_greatest cInf_lower) (auto intro: le_infI1 le_infI2 cInf_lower) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

356 

56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56166
diff
changeset

357 
lemma cINF_union: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_below (f`B) \<Longrightarrow> INFIMUM (A \<union> B) f = inf (INFIMUM A f) (INFIMUM B f)" 
56166  358 
using cInf_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un [symmetric]) 
54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

359 

71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

360 
lemma cSup_union_distrib: "A \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_above B \<Longrightarrow> Sup (A \<union> B) = sup (Sup A) (Sup B)" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

361 
by (intro antisym le_supI cSup_least cSup_upper) (auto intro: le_supI1 le_supI2 cSup_upper) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

362 

56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56166
diff
changeset

363 
lemma cSUP_union: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_above (f`B) \<Longrightarrow> SUPREMUM (A \<union> B) f = sup (SUPREMUM A f) (SUPREMUM B f)" 
56166  364 
using cSup_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un [symmetric]) 
54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

365 

56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56166
diff
changeset

366 
lemma cINF_inf_distrib: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> bdd_below (g`A) \<Longrightarrow> inf (INFIMUM A f) (INFIMUM A g) = (INF a:A. inf (f a) (g a))" 
54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

367 
by (intro antisym le_infI cINF_greatest cINF_lower2) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

368 
(auto intro: le_infI1 le_infI2 cINF_greatest cINF_lower le_infI) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

369 

56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56166
diff
changeset

370 
lemma SUP_sup_distrib: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> bdd_above (g`A) \<Longrightarrow> sup (SUPREMUM A f) (SUPREMUM A g) = (SUP a:A. sup (f a) (g a))" 
54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

371 
by (intro antisym le_supI cSUP_least cSUP_upper2) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

372 
(auto intro: le_supI1 le_supI2 cSUP_least cSUP_upper le_supI) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

373 

57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset

374 
lemma cInf_le_cSup: 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset

375 
"A \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> bdd_below A \<Longrightarrow> Inf A \<le> Sup A" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset

376 
by (auto intro!: cSup_upper2[of "SOME a. a \<in> A"] intro: someI cInf_lower) 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset

377 

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

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

379 

51773  380 
instance complete_lattice \<subseteq> conditionally_complete_lattice 
61169  381 
by standard (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest) 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

382 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

383 
lemma cSup_eq: 
51773  384 
fixes a :: "'a :: {conditionally_complete_lattice, no_bot}" 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

385 
assumes upper: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

386 
assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

387 
shows "Sup X = a" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

388 
proof cases 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

389 
assume "X = {}" with lt_ex[of a] least show ?thesis by (auto simp: less_le_not_le) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

390 
qed (intro cSup_eq_non_empty assms) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

391 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

392 
lemma cInf_eq: 
51773  393 
fixes a :: "'a :: {conditionally_complete_lattice, no_top}" 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

394 
assumes upper: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

395 
assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

396 
shows "Inf X = a" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

397 
proof cases 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

398 
assume "X = {}" with gt_ex[of a] least show ?thesis by (auto simp: less_le_not_le) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

399 
qed (intro cInf_eq_non_empty assms) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

400 

51773  401 
class conditionally_complete_linorder = conditionally_complete_lattice + linorder 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

402 
begin 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

403 

63331  404 
lemma less_cSup_iff: 
54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

405 
"X \<noteq> {} \<Longrightarrow> bdd_above X \<Longrightarrow> y < Sup X \<longleftrightarrow> (\<exists>x\<in>X. y < x)" 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

406 
by (rule iffI) (metis cSup_least not_less, metis cSup_upper less_le_trans) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

407 

54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

408 
lemma cInf_less_iff: "X \<noteq> {} \<Longrightarrow> bdd_below X \<Longrightarrow> Inf X < y \<longleftrightarrow> (\<exists>x\<in>X. x < y)" 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

409 
by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

410 

54263
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54262
diff
changeset

411 
lemma cINF_less_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> (INF i:A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)" 
56166  412 
using cInf_less_iff[of "f`A"] by auto 
54263
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54262
diff
changeset

413 

c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54262
diff
changeset

414 
lemma less_cSUP_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> a < (SUP i:A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)" 
56166  415 
using less_cSup_iff[of "f`A"] by auto 
54263
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54262
diff
changeset

416 

51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

417 
lemma less_cSupE: 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

418 
assumes "y < Sup X" "X \<noteq> {}" obtains x where "x \<in> X" "y < x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

419 
by (metis cSup_least assms not_le that) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

420 

51518
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

421 
lemma less_cSupD: 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

422 
"X \<noteq> {} \<Longrightarrow> z < Sup X \<Longrightarrow> \<exists>x\<in>X. z < x" 
61824
dcbe9f756ae0
not_leE > not_le_imp_less and other tidying
paulson <lp15@cam.ac.uk>
parents:
61169
diff
changeset

423 
by (metis less_cSup_iff not_le_imp_less bdd_above_def) 
51518
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

424 

6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

425 
lemma cInf_lessD: 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

426 
"X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x\<in>X. x < z" 
61824
dcbe9f756ae0
not_leE > not_le_imp_less and other tidying
paulson <lp15@cam.ac.uk>
parents:
61169
diff
changeset

427 
by (metis cInf_less_iff not_le_imp_less bdd_below_def) 
51518
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

428 

51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

429 
lemma complete_interval: 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

430 
assumes "a < b" and "P a" and "\<not> P b" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

431 
shows "\<exists>c. a \<le> c \<and> c \<le> b \<and> (\<forall>x. a \<le> x \<and> x < c \<longrightarrow> P x) \<and> 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

432 
(\<forall>d. (\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x) \<longrightarrow> d \<le> c)" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

433 
proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d > P x}"], auto) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

434 
show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}" 
54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

435 
by (rule cSup_upper, auto simp: bdd_above_def) 
60758  436 
(metis \<open>a < b\<close> \<open>\<not> P b\<close> linear less_le) 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

437 
next 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

438 
show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b" 
63331  439 
apply (rule cSup_least) 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

440 
apply auto 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

441 
apply (metis less_le_not_le) 
60758  442 
apply (metis \<open>a<b\<close> \<open>~ P b\<close> linear less_le) 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

443 
done 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

444 
next 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

445 
fix x 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

446 
assume x: "a \<le> x" and lt: "x < Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

447 
show "P x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

448 
apply (rule less_cSupE [OF lt], auto) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

449 
apply (metis less_le_not_le) 
63331  450 
apply (metis x) 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

451 
done 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

452 
next 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

453 
fix d 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

454 
assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

455 
thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}" 
54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

456 
by (rule_tac cSup_upper, auto simp: bdd_above_def) 
60758  457 
(metis \<open>a<b\<close> \<open>~ P b\<close> linear less_le) 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

458 
qed 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

459 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

460 
end 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

461 

60172
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
59452
diff
changeset

462 
instance complete_linorder < conditionally_complete_linorder 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
59452
diff
changeset

463 
.. 
423273355b55
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents:
59452
diff
changeset

464 

54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

465 
lemma cSup_eq_Max: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Max X" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

466 
using cSup_eq_Sup_fin[of X] Sup_fin_eq_Max[of X] by simp 
51775
408d937c9486
revert #916271d52466; add nontopological linear_continuum type class; show linear_continuum_topology is a perfect_space
hoelzl
parents:
51773
diff
changeset

467 

54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

468 
lemma cInf_eq_Min: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

469 
using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp 
51775
408d937c9486
revert #916271d52466; add nontopological linear_continuum type class; show linear_continuum_topology is a perfect_space
hoelzl
parents:
51773
diff
changeset

470 

54257
5c7a3b6b05a9
generalize SUP and INF to the syntactic type classes Sup and Inf
hoelzl
parents:
53216
diff
changeset

471 
lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x" 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

472 
by (auto intro!: cSup_eq_non_empty intro: dense_le) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

473 

57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset

474 
lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditionally_complete_linorder, dense_linorder}} = x" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset

475 
by (auto intro!: cSup_eq_non_empty intro: dense_le_bounded) 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

476 

57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset

477 
lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditionally_complete_linorder, dense_linorder}} = x" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset

478 
by (auto intro!: cSup_eq_non_empty intro: dense_le_bounded) 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

479 

54257
5c7a3b6b05a9
generalize SUP and INF to the syntactic type classes Sup and Inf
hoelzl
parents:
53216
diff
changeset

480 
lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditionally_complete_linorder, no_top, dense_linorder} <..} = x" 
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset

481 
by (auto intro!: cInf_eq_non_empty intro: dense_ge) 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

482 

57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset

483 
lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditionally_complete_linorder, dense_linorder}} = y" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset

484 
by (auto intro!: cInf_eq_non_empty intro: dense_ge_bounded) 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

485 

57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset

486 
lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, dense_linorder}} = y" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset

487 
by (auto intro!: cInf_eq_non_empty intro: dense_ge_bounded) 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

488 

54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

489 
class linear_continuum = conditionally_complete_linorder + dense_linorder + 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

490 
assumes UNIV_not_singleton: "\<exists>a b::'a. a \<noteq> b" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

491 
begin 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

492 

71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

493 
lemma ex_gt_or_lt: "\<exists>b. a < b \<or> b < a" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

494 
by (metis UNIV_not_singleton neq_iff) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

495 

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

496 
end 
54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

497 

54281  498 
instantiation nat :: conditionally_complete_linorder 
499 
begin 

500 

501 
definition "Sup (X::nat set) = Max X" 

502 
definition "Inf (X::nat set) = (LEAST n. n \<in> X)" 

503 

504 
lemma bdd_above_nat: "bdd_above X \<longleftrightarrow> finite (X::nat set)" 

505 
proof 

506 
assume "bdd_above X" 

507 
then obtain z where "X \<subseteq> {.. z}" 

508 
by (auto simp: bdd_above_def) 

509 
then show "finite X" 

510 
by (rule finite_subset) simp 

511 
qed simp 

512 

513 
instance 

514 
proof 

63540  515 
fix x :: nat 
516 
fix X :: "nat set" 

517 
show "Inf X \<le> x" if "x \<in> X" "bdd_below X" 

518 
using that by (simp add: Inf_nat_def Least_le) 

519 
show "x \<le> Inf X" if "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> x \<le> y" 

520 
using that unfolding Inf_nat_def ex_in_conv[symmetric] by (rule LeastI2_ex) 

521 
show "x \<le> Sup X" if "x \<in> X" "bdd_above X" 

522 
using that by (simp add: Sup_nat_def bdd_above_nat) 

523 
show "Sup X \<le> x" if "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> y \<le> x" 

524 
proof  

525 
from that have "bdd_above X" 

54281  526 
by (auto simp: bdd_above_def) 
63540  527 
with that show ?thesis 
528 
by (simp add: Sup_nat_def bdd_above_nat) 

529 
qed 

54281  530 
qed 
63540  531 

54259
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

532 
end 
54281  533 

534 
instantiation int :: conditionally_complete_linorder 

535 
begin 

536 

537 
definition "Sup (X::int set) = (THE x. x \<in> X \<and> (\<forall>y\<in>X. y \<le> x))" 

538 
definition "Inf (X::int set) =  (Sup (uminus ` X))" 

539 

540 
instance 

541 
proof 

542 
{ fix x :: int and X :: "int set" assume "X \<noteq> {}" "bdd_above X" 

543 
then obtain x y where "X \<subseteq> {..y}" "x \<in> X" 

544 
by (auto simp: bdd_above_def) 

545 
then have *: "finite (X \<inter> {x..y})" "X \<inter> {x..y} \<noteq> {}" and "x \<le> y" 

546 
by (auto simp: subset_eq) 

547 
have "\<exists>!x\<in>X. (\<forall>y\<in>X. y \<le> x)" 

548 
proof 

549 
{ fix z assume "z \<in> X" 

550 
have "z \<le> Max (X \<inter> {x..y})" 

551 
proof cases 

60758  552 
assume "x \<le> z" with \<open>z \<in> X\<close> \<open>X \<subseteq> {..y}\<close> *(1) show ?thesis 
54281  553 
by (auto intro!: Max_ge) 
554 
next 

555 
assume "\<not> x \<le> z" 

556 
then have "z < x" by simp 

557 
also have "x \<le> Max (X \<inter> {x..y})" 

60758  558 
using \<open>x \<in> X\<close> *(1) \<open>x \<le> y\<close> by (intro Max_ge) auto 
54281  559 
finally show ?thesis by simp 
560 
qed } 

561 
note le = this 

562 
with Max_in[OF *] show ex: "Max (X \<inter> {x..y}) \<in> X \<and> (\<forall>z\<in>X. z \<le> Max (X \<inter> {x..y}))" by auto 

563 

564 
fix z assume *: "z \<in> X \<and> (\<forall>y\<in>X. y \<le> z)" 

565 
with le have "z \<le> Max (X \<inter> {x..y})" 

566 
by auto 

567 
moreover have "Max (X \<inter> {x..y}) \<le> z" 

568 
using * ex by auto 

569 
ultimately show "z = Max (X \<inter> {x..y})" 

570 
by auto 

571 
qed 

572 
then have "Sup X \<in> X \<and> (\<forall>y\<in>X. y \<le> Sup X)" 

573 
unfolding Sup_int_def by (rule theI') } 

574 
note Sup_int = this 

575 

576 
{ fix x :: int and X :: "int set" assume "x \<in> X" "bdd_above X" then show "x \<le> Sup X" 

577 
using Sup_int[of X] by auto } 

578 
note le_Sup = this 

579 
{ fix x :: int and X :: "int set" assume "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> y \<le> x" then show "Sup X \<le> x" 

580 
using Sup_int[of X] by (auto simp: bdd_above_def) } 

581 
note Sup_le = this 

582 

583 
{ fix x :: int and X :: "int set" assume "x \<in> X" "bdd_below X" then show "Inf X \<le> x" 

584 
using le_Sup[of "x" "uminus ` X"] by (auto simp: Inf_int_def) } 

585 
{ fix x :: int and X :: "int set" assume "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> x \<le> y" then show "x \<le> Inf X" 

586 
using Sup_le[of "uminus ` X" "x"] by (force simp: Inf_int_def) } 

587 
qed 

588 
end 

589 

57275
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

590 
lemma interval_cases: 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

591 
fixes S :: "'a :: conditionally_complete_linorder set" 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

592 
assumes ivl: "\<And>a b x. a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> x \<in> S" 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

593 
shows "\<exists>a b. S = {} \<or> 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

594 
S = UNIV \<or> 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

595 
S = {..<b} \<or> 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

596 
S = {..b} \<or> 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

597 
S = {a<..} \<or> 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

598 
S = {a..} \<or> 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

599 
S = {a<..<b} \<or> 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

600 
S = {a<..b} \<or> 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

601 
S = {a..<b} \<or> 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

602 
S = {a..b}" 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

603 
proof  
63040  604 
define lower upper where "lower = {x. \<exists>s\<in>S. s \<le> x}" and "upper = {x. \<exists>s\<in>S. x \<le> s}" 
57275
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

605 
with ivl have "S = lower \<inter> upper" 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

606 
by auto 
63331  607 
moreover 
57275
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

608 
have "\<exists>a. upper = UNIV \<or> upper = {} \<or> upper = {.. a} \<or> upper = {..< a}" 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

609 
proof cases 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

610 
assume *: "bdd_above S \<and> S \<noteq> {}" 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

611 
from * have "upper \<subseteq> {.. Sup S}" 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

612 
by (auto simp: upper_def intro: cSup_upper2) 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

613 
moreover from * have "{..< Sup S} \<subseteq> upper" 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

614 
by (force simp add: less_cSup_iff upper_def subset_eq Ball_def) 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

615 
ultimately have "upper = {.. Sup S} \<or> upper = {..< Sup S}" 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

616 
unfolding ivl_disj_un(2)[symmetric] by auto 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

617 
then show ?thesis by auto 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

618 
next 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

619 
assume "\<not> (bdd_above S \<and> S \<noteq> {})" 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

620 
then have "upper = UNIV \<or> upper = {}" 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

621 
by (auto simp: upper_def bdd_above_def not_le dest: less_imp_le) 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

622 
then show ?thesis 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

623 
by auto 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

624 
qed 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

625 
moreover 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

626 
have "\<exists>b. lower = UNIV \<or> lower = {} \<or> lower = {b ..} \<or> lower = {b <..}" 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

627 
proof cases 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

628 
assume *: "bdd_below S \<and> S \<noteq> {}" 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

629 
from * have "lower \<subseteq> {Inf S ..}" 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

630 
by (auto simp: lower_def intro: cInf_lower2) 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

631 
moreover from * have "{Inf S <..} \<subseteq> lower" 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

632 
by (force simp add: cInf_less_iff lower_def subset_eq Ball_def) 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

633 
ultimately have "lower = {Inf S ..} \<or> lower = {Inf S <..}" 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

634 
unfolding ivl_disj_un(1)[symmetric] by auto 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

635 
then show ?thesis by auto 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

636 
next 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

637 
assume "\<not> (bdd_below S \<and> S \<noteq> {})" 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

638 
then have "lower = UNIV \<or> lower = {}" 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

639 
by (auto simp: lower_def bdd_below_def not_le dest: less_imp_le) 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

640 
then show ?thesis 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

641 
by auto 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

642 
qed 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

643 
ultimately show ?thesis 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

644 
unfolding greaterThanAtMost_def greaterThanLessThan_def atLeastAtMost_def atLeastLessThan_def 
63171  645 
by (metis inf_bot_left inf_bot_right inf_top.left_neutral inf_top.right_neutral) 
57275
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

646 
qed 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56218
diff
changeset

647 

60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60172
diff
changeset

648 
lemma cSUP_eq_cINF_D: 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60172
diff
changeset

649 
fixes f :: "_ \<Rightarrow> 'b::conditionally_complete_lattice" 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60172
diff
changeset

650 
assumes eq: "(SUP x:A. f x) = (INF x:A. f x)" 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60172
diff
changeset

651 
and bdd: "bdd_above (f ` A)" "bdd_below (f ` A)" 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60172
diff
changeset

652 
and a: "a \<in> A" 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60172
diff
changeset

653 
shows "f a = (INF x:A. f x)" 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60172
diff
changeset

654 
apply (rule antisym) 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60172
diff
changeset

655 
using a bdd 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60172
diff
changeset

656 
apply (auto simp: cINF_lower) 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60172
diff
changeset

657 
apply (metis eq cSUP_upper) 
63331  658 
done 
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60172
diff
changeset

659 

62379
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

660 
lemma cSUP_UNION: 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

661 
fixes f :: "_ \<Rightarrow> 'b::conditionally_complete_lattice" 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

662 
assumes ne: "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> B(x) \<noteq> {}" 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

663 
and bdd_UN: "bdd_above (\<Union>x\<in>A. f ` B x)" 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

664 
shows "(SUP z : \<Union>x\<in>A. B x. f z) = (SUP x:A. SUP z:B x. f z)" 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

665 
proof  
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

666 
have bdd: "\<And>x. x \<in> A \<Longrightarrow> bdd_above (f ` B x)" 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

667 
using bdd_UN by (meson UN_upper bdd_above_mono) 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

668 
obtain M where "\<And>x y. x \<in> A \<Longrightarrow> y \<in> B(x) \<Longrightarrow> f y \<le> M" 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

669 
using bdd_UN by (auto simp: bdd_above_def) 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

670 
then have bdd2: "bdd_above ((\<lambda>x. SUP z:B x. f z) ` A)" 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

671 
unfolding bdd_above_def by (force simp: bdd cSUP_le_iff ne(2)) 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

672 
have "(SUP z:\<Union>x\<in>A. B x. f z) \<le> (SUP x:A. SUP z:B x. f z)" 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

673 
using assms by (fastforce simp add: intro!: cSUP_least intro: cSUP_upper2 simp: bdd2 bdd) 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

674 
moreover have "(SUP x:A. SUP z:B x. f z) \<le> (SUP z:\<Union>x\<in>A. B x. f z)" 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

675 
using assms by (fastforce simp add: intro!: cSUP_least intro: cSUP_upper simp: image_UN bdd_UN) 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

676 
ultimately show ?thesis 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

677 
by (rule order_antisym) 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

678 
qed 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

679 

340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

680 
lemma cINF_UNION: 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

681 
fixes f :: "_ \<Rightarrow> 'b::conditionally_complete_lattice" 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

682 
assumes ne: "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> B(x) \<noteq> {}" 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

683 
and bdd_UN: "bdd_below (\<Union>x\<in>A. f ` B x)" 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

684 
shows "(INF z : \<Union>x\<in>A. B x. f z) = (INF x:A. INF z:B x. f z)" 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

685 
proof  
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

686 
have bdd: "\<And>x. x \<in> A \<Longrightarrow> bdd_below (f ` B x)" 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

687 
using bdd_UN by (meson UN_upper bdd_below_mono) 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

688 
obtain M where "\<And>x y. x \<in> A \<Longrightarrow> y \<in> B(x) \<Longrightarrow> f y \<ge> M" 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

689 
using bdd_UN by (auto simp: bdd_below_def) 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

690 
then have bdd2: "bdd_below ((\<lambda>x. INF z:B x. f z) ` A)" 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

691 
unfolding bdd_below_def by (force simp: bdd le_cINF_iff ne(2)) 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

692 
have "(INF z:\<Union>x\<in>A. B x. f z) \<le> (INF x:A. INF z:B x. f z)" 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

693 
using assms by (fastforce simp add: intro!: cINF_greatest intro: cINF_lower simp: bdd2 bdd) 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

694 
moreover have "(INF x:A. INF z:B x. f z) \<le> (INF z:\<Union>x\<in>A. B x. f z)" 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

695 
using assms by (fastforce simp add: intro!: cINF_greatest intro: cINF_lower2 simp: bdd bdd_UN bdd2) 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

696 
ultimately show ?thesis 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

697 
by (rule order_antisym) 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

698 
qed 
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62343
diff
changeset

699 

63331  700 
lemma cSup_abs_le: 
62626
de25474ce728
Contractible sets. Also removal of obsolete theorems and refactoring
paulson <lp15@cam.ac.uk>
parents:
62379
diff
changeset

701 
fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set" 
de25474ce728
Contractible sets. Also removal of obsolete theorems and refactoring
paulson <lp15@cam.ac.uk>
parents:
62379
diff
changeset

702 
shows "S \<noteq> {} \<Longrightarrow> (\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a" 
de25474ce728
Contractible sets. Also removal of obsolete theorems and refactoring
paulson <lp15@cam.ac.uk>
parents:
62379
diff
changeset

703 
apply (auto simp add: abs_le_iff intro: cSup_least) 
de25474ce728
Contractible sets. Also removal of obsolete theorems and refactoring
paulson <lp15@cam.ac.uk>
parents:
62379
diff
changeset

704 
by (metis bdd_aboveI cSup_upper neg_le_iff_le order_trans) 
de25474ce728
Contractible sets. Also removal of obsolete theorems and refactoring
paulson <lp15@cam.ac.uk>
parents:
62379
diff
changeset

705 

54281  706 
end 