author  hoelzl 
Tue, 05 Nov 2013 21:23:42 +0100  
changeset 54281  b01057e72233 
parent 54263  c4159fe6fa46 
child 56166  9a241bc276cd 
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 

51773  7 
header {* Conditionallycomplete Lattices *} 
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 
54263
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54262
diff
changeset

10 
imports Main 
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 

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

13 
lemma (in linorder) Sup_fin_eq_Max: "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

14 
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

15 

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

16 
lemma (in linorder) Inf_fin_eq_Min: "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

17 
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

18 

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

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

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

21 

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

22 
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

23 
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

24 

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

25 
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

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

27 

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

28 
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

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

30 

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

31 
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

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

33 

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

34 
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

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

36 

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

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

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

39 

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

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

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

42 

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

43 
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

44 
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

45 

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

46 
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

47 
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

48 

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

49 
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

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

51 

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

52 
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

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

54 

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

55 
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

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

57 

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

58 
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

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

60 

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

61 
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

62 
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

63 

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

64 
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

65 
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

66 

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

67 
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

68 
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

69 

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

70 
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

71 
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

72 

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

73 
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

74 
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

75 

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

76 
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

77 
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

78 

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

79 
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

80 
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

81 

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

82 
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

83 
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

84 

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

85 
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

86 
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

87 

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

88 
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

89 
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

90 

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

91 
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

92 
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

93 

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

94 
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

95 
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

96 

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

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

98 

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

101 

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

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

104 

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

105 
lemma bdd_above_uminus[simp]: 
326fd7103cb4
generalize bdd_above/below_uminus to ordered_ab_group_add
hoelzl
parents:
54261
diff
changeset

106 
fixes X :: "'a::ordered_ab_group_add set" 
326fd7103cb4
generalize bdd_above/below_uminus to ordered_ab_group_add
hoelzl
parents:
54261
diff
changeset

107 
shows "bdd_above (uminus ` X) \<longleftrightarrow> bdd_below X" 
326fd7103cb4
generalize bdd_above/below_uminus to ordered_ab_group_add
hoelzl
parents:
54261
diff
changeset

108 
by (auto simp: bdd_above_def bdd_below_def intro: le_imp_neg_le) (metis le_imp_neg_le minus_minus) 
326fd7103cb4
generalize bdd_above/below_uminus to ordered_ab_group_add
hoelzl
parents:
54261
diff
changeset

109 

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

110 
lemma bdd_below_uminus[simp]: 
326fd7103cb4
generalize bdd_above/below_uminus to ordered_ab_group_add
hoelzl
parents:
54261
diff
changeset

111 
fixes X :: "'a::ordered_ab_group_add set" 
326fd7103cb4
generalize bdd_above/below_uminus to ordered_ab_group_add
hoelzl
parents:
54261
diff
changeset

112 
shows"bdd_below (uminus ` X) \<longleftrightarrow> bdd_above X" 
326fd7103cb4
generalize bdd_above/below_uminus to ordered_ab_group_add
hoelzl
parents:
54261
diff
changeset

113 
by (auto simp: bdd_above_def bdd_below_def intro: le_imp_neg_le) (metis le_imp_neg_le minus_minus) 
326fd7103cb4
generalize bdd_above/below_uminus to ordered_ab_group_add
hoelzl
parents:
54261
diff
changeset

114 

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

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

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

117 

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

118 
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

119 
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

120 

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

121 
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

122 
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

123 

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

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

125 
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

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

127 

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

128 
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

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

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

131 
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

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

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

134 
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

135 
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

136 
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

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

138 

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

139 
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

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

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

142 
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

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

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

145 
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

146 
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

147 
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

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

149 

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

150 
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

151 
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

152 

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

153 
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

154 
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

155 

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

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

157 

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

158 

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

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

160 

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

161 
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

162 
@{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

163 

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

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

165 

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

167 
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

168 
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

169 
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

170 
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

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

172 

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

173 
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

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

175 

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

176 
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

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

178 

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

179 
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

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

181 

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

182 
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

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

184 

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

185 
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

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

187 

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

188 
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

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

190 

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

191 
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

192 
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

193 

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

194 
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

195 
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

196 

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

197 
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

198 
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

199 

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

200 
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

201 
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

202 

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

203 
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

204 
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

205 
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

206 
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

207 
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

208 
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

209 

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

210 
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

211 
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

212 
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

213 
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

214 
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

215 
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

216 

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

217 
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

218 
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

219 

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

220 
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

221 
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

222 

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

223 
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

224 
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

225 

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

226 
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

227 
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

228 

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

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

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

231 

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

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

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

234 

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

235 
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

236 
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

237 

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

238 
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

239 
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

240 

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

241 
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

242 
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

243 
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

244 
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

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

246 

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

247 
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

248 
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

249 
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

250 
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

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

252 

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

253 
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

254 
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

255 

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

256 
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

257 
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

258 

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

259 
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

260 
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

261 

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

262 
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

263 
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

264 

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

265 
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

266 
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

267 

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

268 
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

269 
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

270 

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

271 
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

272 
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

273 

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

274 
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

275 
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

276 

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

277 
lemma cINF_lower: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> INFI A f \<le> f x" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

278 
unfolding INF_def by (rule cInf_lower) auto 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

279 

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

280 
lemma cINF_greatest: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> m \<le> f x) \<Longrightarrow> m \<le> INFI A f" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

281 
unfolding INF_def by (rule cInf_greatest) auto 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

282 

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

283 
lemma cSUP_upper: "x \<in> A \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> f x \<le> SUPR A f" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

284 
unfolding SUP_def by (rule cSup_upper) auto 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

285 

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

286 
lemma cSUP_least: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> M) \<Longrightarrow> SUPR A f \<le> M" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

287 
unfolding SUP_def by (rule cSup_least) auto 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

288 

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

289 
lemma cINF_lower2: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<le> u \<Longrightarrow> INFI A f \<le> u" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

290 
by (auto intro: cINF_lower assms order_trans) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

291 

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

292 
lemma cSUP_upper2: "bdd_above (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> u \<le> f x \<Longrightarrow> u \<le> SUPR A f" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

293 
by (auto intro: cSUP_upper assms order_trans) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

294 

54261  295 
lemma cSUP_const: "A \<noteq> {} \<Longrightarrow> (SUP x:A. c) = c" 
296 
by (intro antisym cSUP_least) (auto intro: cSUP_upper) 

297 

298 
lemma cINF_const: "A \<noteq> {} \<Longrightarrow> (INF x:A. c) = c" 

299 
by (intro antisym cINF_greatest) (auto intro: cINF_lower) 

300 

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

301 
lemma le_cINF_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> u \<le> INFI A f \<longleftrightarrow> (\<forall>x\<in>A. u \<le> f x)" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

302 
by (metis cINF_greatest cINF_lower assms order_trans) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

303 

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

304 
lemma cSUP_le_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPR A f \<le> u \<longleftrightarrow> (\<forall>x\<in>A. f x \<le> u)" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

305 
by (metis cSUP_least cSUP_upper assms order_trans) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

306 

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

307 
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

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

309 

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

310 
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

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

312 

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

313 
lemma cINF_insert: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> INFI (insert a A) f = inf (f a) (INFI A f)" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

314 
by (metis INF_def cInf_insert assms empty_is_image image_insert) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

315 

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

316 
lemma cSUP_insert: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPR (insert a A) f = sup (f a) (SUPR A f)" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

317 
by (metis SUP_def cSup_insert assms empty_is_image image_insert) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

318 

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

319 
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> INFI A f \<le> INFI B g" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

320 
unfolding INF_def by (auto intro: cInf_mono) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

321 

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

322 
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> SUPR A f \<le> SUPR B g" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

323 
unfolding SUP_def by (auto intro: cSup_mono) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

324 

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

325 
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> INFI B g \<le> INFI A f" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

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

327 

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

328 
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> SUPR A f \<le> SUPR B g" 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

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

330 

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

331 
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

332 
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

333 

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

334 
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

335 
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

336 

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

337 
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

338 
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

339 

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

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

341 
unfolding INF_def using assms by (auto simp add: image_Un intro: cInf_union_distrib) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

342 

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

343 
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

344 
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

345 

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

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

347 
unfolding SUP_def by (auto simp add: image_Un intro: cSup_union_distrib) 
71c701dc5bf9
add SUP and INF for conditionally complete lattices
hoelzl
parents:
54258
diff
changeset

348 

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

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

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

351 
(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

352 

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

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

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

355 
(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

356 

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

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

358 

51773  359 
instance complete_lattice \<subseteq> conditionally_complete_lattice 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

360 
by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

361 

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

362 
lemma cSup_eq: 
51773  363 
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

364 
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

365 
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

366 
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

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

368 
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

369 
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

370 

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

371 
lemma cInf_eq: 
51773  372 
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

373 
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

374 
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

375 
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

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

377 
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

378 
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

379 

51773  380 
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

381 
begin 
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 less_cSup_iff : (*REAL_SUP_LE in HOL4*) 
54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

384 
"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

385 
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

386 

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

387 
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

388 
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

389 

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

390 
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)" 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54262
diff
changeset

391 
unfolding INF_def using cInf_less_iff[of "f`A"] by auto 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54262
diff
changeset

392 

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

393 
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)" 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54262
diff
changeset

394 
unfolding SUP_def using less_cSup_iff[of "f`A"] by auto 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54262
diff
changeset

395 

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

396 
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

397 
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

398 
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

399 

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

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

401 
"X \<noteq> {} \<Longrightarrow> z < Sup X \<Longrightarrow> \<exists>x\<in>X. z < x" 
54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

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

403 

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

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

405 
"X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x\<in>X. x < z" 
54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54257
diff
changeset

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

407 

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

408 
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

409 
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

410 
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

411 
(\<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

412 
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

413 
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

414 
by (rule cSup_upper, auto simp: bdd_above_def) 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

415 
(metis `a < b` `\<not> P b` linear less_le) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

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

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

418 
apply (rule cSup_least) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

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

420 
apply (metis 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

421 
apply (metis `a<b` `~ P b` linear less_le) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

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

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

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

425 
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

426 
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

427 
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

428 
apply (metis 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

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

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

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

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

433 
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

434 
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

435 
by (rule_tac cSup_upper, auto simp: bdd_above_def) 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

436 
(metis `a<b` `~ P b` linear less_le) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

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

438 

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

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

440 

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

441 
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

442 
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

443 

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

444 
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

445 
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

446 

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

447 
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

448 
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

449 

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

450 
lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<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

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

452 

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

453 
lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<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

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

455 

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

456 
lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditionally_complete_linorder, no_top, 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

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

458 

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

459 
lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditionally_complete_linorder, no_top, dense_linorder}} = y" 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

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

461 

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

462 
lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, no_top, dense_linorder}} = y" 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

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

464 

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

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

466 
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

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

468 

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

469 
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

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

471 

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

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

473 

54281  474 
instantiation nat :: conditionally_complete_linorder 
475 
begin 

476 

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

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

479 

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

481 
proof 

482 
assume "bdd_above X" 

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

484 
by (auto simp: bdd_above_def) 

485 
then show "finite X" 

486 
by (rule finite_subset) simp 

487 
qed simp 

488 

489 
instance 

490 
proof 

491 
fix x :: nat and X :: "nat set" 

492 
{ assume "x \<in> X" "bdd_below X" then show "Inf X \<le> x" 

493 
by (simp add: Inf_nat_def Least_le) } 

494 
{ assume "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> x \<le> y" then show "x \<le> Inf X" 

495 
unfolding Inf_nat_def ex_in_conv[symmetric] by (rule LeastI2_ex) } 

496 
{ assume "x \<in> X" "bdd_above X" then show "x \<le> Sup X" 

497 
by (simp add: Sup_nat_def bdd_above_nat) } 

498 
{ assume "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> y \<le> x" 

499 
moreover then have "bdd_above X" 

500 
by (auto simp: bdd_above_def) 

501 
ultimately show "Sup X \<le> x" 

502 
by (simp add: Sup_nat_def bdd_above_nat) } 

503 
qed 

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

504 
end 
54281  505 

506 
instantiation int :: conditionally_complete_linorder 

507 
begin 

508 

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

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

511 

512 
instance 

513 
proof 

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

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

516 
by (auto simp: bdd_above_def) 

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

518 
by (auto simp: subset_eq) 

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

520 
proof 

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

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

523 
proof cases 

524 
assume "x \<le> z" with `z \<in> X` `X \<subseteq> {..y}` *(1) show ?thesis 

525 
by (auto intro!: Max_ge) 

526 
next 

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

528 
then have "z < x" by simp 

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

530 
using `x \<in> X` *(1) `x \<le> y` by (intro Max_ge) auto 

531 
finally show ?thesis by simp 

532 
qed } 

533 
note le = this 

534 
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 

535 

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

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

538 
by auto 

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

540 
using * ex by auto 

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

542 
by auto 

543 
qed 

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

545 
unfolding Sup_int_def by (rule theI') } 

546 
note Sup_int = this 

547 

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

549 
using Sup_int[of X] by auto } 

550 
note le_Sup = this 

551 
{ 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" 

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

553 
note Sup_le = this 

554 

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

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

557 
{ 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" 

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

559 
qed 

560 
end 

561 

562 
end 