author  wenzelm 
Wed, 13 Jun 2007 00:01:41 +0200  
changeset 23350  50c5b0912a0c 
parent 22265  3c5c6bdf61de 
child 23463  9953ff53cc64 
permissions  rwrr 
14551  1 
(* 
14706  2 
Title: HOL/Algebra/Lattice.thy 
14551  3 
Id: $Id$ 
4 
Author: Clemens Ballarin, started 7 November 2003 

5 
Copyright: Clemens Ballarin 

6 
*) 

7 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset

8 
theory Lattice imports Main begin 
14551  9 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset

10 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset

11 
section {* Orders and Lattices *} 
14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

12 

0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

13 
text {* Object with a carrier set. *} 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

14 

0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

15 
record 'a partial_object = 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

16 
carrier :: "'a set" 
14551  17 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset

18 

14551  19 
subsection {* Partial Orders *} 
20 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

21 
record 'a order = "'a partial_object" + 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

22 
le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50) 
21041
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

23 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

24 
locale partial_order = 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

25 
fixes L (structure) 
14551  26 
assumes refl [intro, simp]: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

27 
"x \<in> carrier L ==> x \<sqsubseteq> x" 
14551  28 
and anti_sym [intro]: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

29 
"[ x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L ] ==> x = y" 
14551  30 
and trans [trans]: 
31 
"[ x \<sqsubseteq> y; y \<sqsubseteq> z; 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

32 
x \<in> carrier L; y \<in> carrier L; z \<in> carrier L ] ==> x \<sqsubseteq> z" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

33 

717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

34 
constdefs (structure L) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

35 
lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

36 
"x \<sqsubset> y == x \<sqsubseteq> y & x ~= y" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

37 

717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

38 
 {* Upper and lower bounds of a set. *} 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

39 
Upper :: "[_, 'a set] => 'a set" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

40 
"Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L > x \<sqsubseteq> u)} \<inter> 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

41 
carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

42 

717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

43 
Lower :: "[_, 'a set] => 'a set" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

44 
"Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L > l \<sqsubseteq> x)} \<inter> 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

45 
carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

46 

717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

47 
 {* Least and greatest, as predicate. *} 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

48 
least :: "[_, 'a, 'a set] => bool" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

49 
"least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

50 

717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

51 
greatest :: "[_, 'a, 'a set] => bool" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

52 
"greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

53 

717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

54 
 {* Supremum and infimum *} 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

55 
sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

56 
"\<Squnion>A == THE x. least L x (Upper L A)" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

57 

717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

58 
inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

59 
"\<Sqinter>A == THE x. greatest L x (Lower L A)" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

60 

717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

61 
join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

62 
"x \<squnion> y == sup L {x, y}" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

63 

717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

64 
meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

65 
"x \<sqinter> y == inf L {x, y}" 
14551  66 

14651  67 

68 
subsubsection {* Upper *} 

14551  69 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

70 
lemma Upper_closed [intro, simp]: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

71 
"Upper L A \<subseteq> carrier L" 
14551  72 
by (unfold Upper_def) clarify 
73 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

74 
lemma UpperD [dest]: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

75 
fixes L (structure) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

76 
shows "[ u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L ] ==> x \<sqsubseteq> u" 
14693  77 
by (unfold Upper_def) blast 
14551  78 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

79 
lemma Upper_memI: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

80 
fixes L (structure) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

81 
shows "[ !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L ] ==> x \<in> Upper L A" 
14693  82 
by (unfold Upper_def) blast 
14551  83 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

84 
lemma Upper_antimono: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

85 
"A \<subseteq> B ==> Upper L B \<subseteq> Upper L A" 
14551  86 
by (unfold Upper_def) blast 
87 

14651  88 

89 
subsubsection {* Lower *} 

14551  90 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

91 
lemma Lower_closed [intro, simp]: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

92 
"Lower L A \<subseteq> carrier L" 
14551  93 
by (unfold Lower_def) clarify 
94 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

95 
lemma LowerD [dest]: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

96 
fixes L (structure) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

97 
shows "[ l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L ] ==> l \<sqsubseteq> x" 
14693  98 
by (unfold Lower_def) blast 
14551  99 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

100 
lemma Lower_memI: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

101 
fixes L (structure) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

102 
shows "[ !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L ] ==> x \<in> Lower L A" 
14693  103 
by (unfold Lower_def) blast 
14551  104 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

105 
lemma Lower_antimono: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

106 
"A \<subseteq> B ==> Lower L B \<subseteq> Lower L A" 
14551  107 
by (unfold Lower_def) blast 
108 

14651  109 

110 
subsubsection {* least *} 

14551  111 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

112 
lemma least_carrier [intro, simp]: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

113 
shows "least L l A ==> l \<in> carrier L" 
14551  114 
by (unfold least_def) fast 
115 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

116 
lemma least_mem: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

117 
"least L l A ==> l \<in> A" 
14551  118 
by (unfold least_def) fast 
119 

120 
lemma (in partial_order) least_unique: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

121 
"[ least L x A; least L y A ] ==> x = y" 
14551  122 
by (unfold least_def) blast 
123 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

124 
lemma least_le: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

125 
fixes L (structure) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

126 
shows "[ least L x A; a \<in> A ] ==> x \<sqsubseteq> a" 
14551  127 
by (unfold least_def) fast 
128 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

129 
lemma least_UpperI: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

130 
fixes L (structure) 
14551  131 
assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s" 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

132 
and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

133 
and L: "A \<subseteq> carrier L" "s \<in> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

134 
shows "least L s (Upper L A)" 
14693  135 
proof  
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

136 
have "Upper L A \<subseteq> carrier L" by simp 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

137 
moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

138 
moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast 
14693  139 
ultimately show ?thesis by (simp add: least_def) 
14551  140 
qed 
141 

14651  142 

143 
subsubsection {* greatest *} 

14551  144 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

145 
lemma greatest_carrier [intro, simp]: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

146 
shows "greatest L l A ==> l \<in> carrier L" 
14551  147 
by (unfold greatest_def) fast 
148 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

149 
lemma greatest_mem: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

150 
"greatest L l A ==> l \<in> A" 
14551  151 
by (unfold greatest_def) fast 
152 

153 
lemma (in partial_order) greatest_unique: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

154 
"[ greatest L x A; greatest L y A ] ==> x = y" 
14551  155 
by (unfold greatest_def) blast 
156 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

157 
lemma greatest_le: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

158 
fixes L (structure) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

159 
shows "[ greatest L x A; a \<in> A ] ==> a \<sqsubseteq> x" 
14551  160 
by (unfold greatest_def) fast 
161 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

162 
lemma greatest_LowerI: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

163 
fixes L (structure) 
14551  164 
assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x" 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

165 
and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

166 
and L: "A \<subseteq> carrier L" "i \<in> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

167 
shows "greatest L i (Lower L A)" 
14693  168 
proof  
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

169 
have "Lower L A \<subseteq> carrier L" by simp 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

170 
moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

171 
moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast 
14693  172 
ultimately show ?thesis by (simp add: greatest_def) 
14551  173 
qed 
174 

14693  175 

14551  176 
subsection {* Lattices *} 
177 

178 
locale lattice = partial_order + 

179 
assumes sup_of_two_exists: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

180 
"[ x \<in> carrier L; y \<in> carrier L ] ==> EX s. least L s (Upper L {x, y})" 
14551  181 
and inf_of_two_exists: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

182 
"[ x \<in> carrier L; y \<in> carrier L ] ==> EX s. greatest L s (Lower L {x, y})" 
14551  183 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

184 
lemma least_Upper_above: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

185 
fixes L (structure) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

186 
shows "[ least L s (Upper L A); x \<in> A; A \<subseteq> carrier L ] ==> x \<sqsubseteq> s" 
14551  187 
by (unfold least_def) blast 
188 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

189 
lemma greatest_Lower_above: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

190 
fixes L (structure) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

191 
shows "[ greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L ] ==> i \<sqsubseteq> x" 
14551  192 
by (unfold greatest_def) blast 
193 

14666  194 

14551  195 
subsubsection {* Supremum *} 
196 

197 
lemma (in lattice) joinI: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

198 
"[ !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L ] 
14551  199 
==> P (x \<squnion> y)" 
200 
proof (unfold join_def sup_def) 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

201 
assume L: "x \<in> carrier L" "y \<in> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

202 
and P: "!!l. least L l (Upper L {x, y}) ==> P l" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

203 
with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

204 
with L show "P (THE l. least L l (Upper L {x, y}))" 
14693  205 
by (fast intro: theI2 least_unique P) 
14551  206 
qed 
207 

208 
lemma (in lattice) join_closed [simp]: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

209 
"[ x \<in> carrier L; y \<in> carrier L ] ==> x \<squnion> y \<in> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

210 
by (rule joinI) (rule least_carrier) 
14551  211 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

212 
lemma (in partial_order) sup_of_singletonI: (* only reflexivity needed ? *) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

213 
"x \<in> carrier L ==> least L x (Upper L {x})" 
14551  214 
by (rule least_UpperI) fast+ 
215 

216 
lemma (in partial_order) sup_of_singleton [simp]: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

217 
"x \<in> carrier L ==> \<Squnion>{x} = x" 
14551  218 
by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI) 
219 

14666  220 

221 
text {* Condition on @{text A}: supremum exists. *} 

14551  222 

223 
lemma (in lattice) sup_insertI: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

224 
"[ !!s. least L s (Upper L (insert x A)) ==> P s; 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

225 
least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L ] 
14693  226 
==> P (\<Squnion>(insert x A))" 
14551  227 
proof (unfold sup_def) 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

228 
assume L: "x \<in> carrier L" "A \<subseteq> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

229 
and P: "!!l. least L l (Upper L (insert x A)) ==> P l" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

230 
and least_a: "least L a (Upper L A)" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

231 
from L least_a have La: "a \<in> carrier L" by simp 
14551  232 
from L sup_of_two_exists least_a 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

233 
obtain s where least_s: "least L s (Upper L {a, x})" by blast 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

234 
show "P (THE l. least L l (Upper L (insert x A)))" 
14693  235 
proof (rule theI2) 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

236 
show "least L s (Upper L (insert x A))" 
14551  237 
proof (rule least_UpperI) 
238 
fix z 

14693  239 
assume "z \<in> insert x A" 
240 
then show "z \<sqsubseteq> s" 

241 
proof 

242 
assume "z = x" then show ?thesis 

243 
by (simp add: least_Upper_above [OF least_s] L La) 

244 
next 

245 
assume "z \<in> A" 

246 
with L least_s least_a show ?thesis 

247 
by (rule_tac trans [where y = a]) (auto dest: least_Upper_above) 

248 
qed 

249 
next 

250 
fix y 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

251 
assume y: "y \<in> Upper L (insert x A)" 
14693  252 
show "s \<sqsubseteq> y" 
253 
proof (rule least_le [OF least_s], rule Upper_memI) 

254 
fix z 

255 
assume z: "z \<in> {a, x}" 

256 
then show "z \<sqsubseteq> y" 

257 
proof 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

258 
have y': "y \<in> Upper L A" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

259 
apply (rule subsetD [where A = "Upper L (insert x A)"]) 
14693  260 
apply (rule Upper_antimono) apply clarify apply assumption 
261 
done 

262 
assume "z = a" 

263 
with y' least_a show ?thesis by (fast dest: least_le) 

264 
next 

265 
assume "z \<in> {x}" (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *) 

266 
with y L show ?thesis by blast 

267 
qed 

23350  268 
qed (rule Upper_closed [THEN subsetD, OF y]) 
14693  269 
next 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

270 
from L show "insert x A \<subseteq> carrier L" by simp 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

271 
from least_s show "s \<in> carrier L" by simp 
14551  272 
qed 
273 
next 

274 
fix l 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

275 
assume least_l: "least L l (Upper L (insert x A))" 
14551  276 
show "l = s" 
277 
proof (rule least_unique) 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

278 
show "least L s (Upper L (insert x A))" 
14551  279 
proof (rule least_UpperI) 
14693  280 
fix z 
281 
assume "z \<in> insert x A" 

282 
then show "z \<sqsubseteq> s" 

283 
proof 

284 
assume "z = x" then show ?thesis 

285 
by (simp add: least_Upper_above [OF least_s] L La) 

286 
next 

287 
assume "z \<in> A" 

288 
with L least_s least_a show ?thesis 

289 
by (rule_tac trans [where y = a]) (auto dest: least_Upper_above) 

14551  290 
qed 
291 
next 

14693  292 
fix y 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

293 
assume y: "y \<in> Upper L (insert x A)" 
14693  294 
show "s \<sqsubseteq> y" 
295 
proof (rule least_le [OF least_s], rule Upper_memI) 

296 
fix z 

297 
assume z: "z \<in> {a, x}" 

298 
then show "z \<sqsubseteq> y" 

299 
proof 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

300 
have y': "y \<in> Upper L A" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

301 
apply (rule subsetD [where A = "Upper L (insert x A)"]) 
14693  302 
apply (rule Upper_antimono) apply clarify apply assumption 
303 
done 

304 
assume "z = a" 

305 
with y' least_a show ?thesis by (fast dest: least_le) 

306 
next 

307 
assume "z \<in> {x}" 

308 
with y L show ?thesis by blast 

309 
qed 

23350  310 
qed (rule Upper_closed [THEN subsetD, OF y]) 
14551  311 
next 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

312 
from L show "insert x A \<subseteq> carrier L" by simp 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

313 
from least_s show "s \<in> carrier L" by simp 
14551  314 
qed 
23350  315 
qed (rule least_l) 
316 
qed (rule P) 

14551  317 
qed 
318 

319 
lemma (in lattice) finite_sup_least: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

320 
"[ finite A; A \<subseteq> carrier L; A ~= {} ] ==> least L (\<Squnion>A) (Upper L A)" 
22265  321 
proof (induct set: finite) 
14693  322 
case empty 
323 
then show ?case by simp 

14551  324 
next 
15328  325 
case (insert x A) 
14551  326 
show ?case 
327 
proof (cases "A = {}") 

328 
case True 

329 
with insert show ?thesis by (simp add: sup_of_singletonI) 

330 
next 

331 
case False 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

332 
with insert have "least L (\<Squnion>A) (Upper L A)" by simp 
14693  333 
with _ show ?thesis 
334 
by (rule sup_insertI) (simp_all add: insert [simplified]) 

14551  335 
qed 
336 
qed 

337 

338 
lemma (in lattice) finite_sup_insertI: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

339 
assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

340 
and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" 
14551  341 
shows "P (\<Squnion> (insert x A))" 
342 
proof (cases "A = {}") 

343 
case True with P and xA show ?thesis 

344 
by (simp add: sup_of_singletonI) 

345 
next 

346 
case False with P and xA show ?thesis 

347 
by (simp add: sup_insertI finite_sup_least) 

348 
qed 

349 

350 
lemma (in lattice) finite_sup_closed: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

351 
"[ finite A; A \<subseteq> carrier L; A ~= {} ] ==> \<Squnion>A \<in> carrier L" 
22265  352 
proof (induct set: finite) 
14551  353 
case empty then show ?case by simp 
354 
next 

15328  355 
case insert then show ?case 
14693  356 
by  (rule finite_sup_insertI, simp_all) 
14551  357 
qed 
358 

359 
lemma (in lattice) join_left: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

360 
"[ x \<in> carrier L; y \<in> carrier L ] ==> x \<sqsubseteq> x \<squnion> y" 
14693  361 
by (rule joinI [folded join_def]) (blast dest: least_mem) 
14551  362 

363 
lemma (in lattice) join_right: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

364 
"[ x \<in> carrier L; y \<in> carrier L ] ==> y \<sqsubseteq> x \<squnion> y" 
14693  365 
by (rule joinI [folded join_def]) (blast dest: least_mem) 
14551  366 

367 
lemma (in lattice) sup_of_two_least: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

368 
"[ x \<in> carrier L; y \<in> carrier L ] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})" 
14551  369 
proof (unfold sup_def) 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

370 
assume L: "x \<in> carrier L" "y \<in> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

371 
with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

372 
with L show "least L (THE xa. least L xa (Upper L {x, y})) (Upper L {x, y})" 
14551  373 
by (fast intro: theI2 least_unique) (* blast fails *) 
374 
qed 

375 

376 
lemma (in lattice) join_le: 

14693  377 
assumes sub: "x \<sqsubseteq> z" "y \<sqsubseteq> z" 
23350  378 
and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L" 
14551  379 
shows "x \<squnion> y \<sqsubseteq> z" 
23350  380 
proof (rule joinI [OF _ x y]) 
14551  381 
fix s 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

382 
assume "least L s (Upper L {x, y})" 
23350  383 
with sub z show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI) 
14551  384 
qed 
14693  385 

14551  386 
lemma (in lattice) join_assoc_lemma: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

387 
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" 
14693  388 
shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}" 
14551  389 
proof (rule finite_sup_insertI) 
14651  390 
 {* The textbook argument in Jacobson I, p 457 *} 
14551  391 
fix s 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

392 
assume sup: "least L s (Upper L {x, y, z})" 
14551  393 
show "x \<squnion> (y \<squnion> z) = s" 
394 
proof (rule anti_sym) 

395 
from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s" 

396 
by (fastsimp intro!: join_le elim: least_Upper_above) 

397 
next 

398 
from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)" 

399 
by (erule_tac least_le) 

400 
(blast intro!: Upper_memI intro: trans join_left join_right join_closed) 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

401 
qed (simp_all add: L least_carrier [OF sup]) 
14551  402 
qed (simp_all add: L) 
403 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

404 
lemma join_comm: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

405 
fixes L (structure) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

406 
shows "x \<squnion> y = y \<squnion> x" 
14551  407 
by (unfold join_def) (simp add: insert_commute) 
408 

409 
lemma (in lattice) join_assoc: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

410 
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" 
14551  411 
shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" 
412 
proof  

413 
have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm) 

14693  414 
also from L have "... = \<Squnion>{z, x, y}" by (simp add: join_assoc_lemma) 
415 
also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute) 

14551  416 
also from L have "... = x \<squnion> (y \<squnion> z)" by (simp add: join_assoc_lemma) 
417 
finally show ?thesis . 

418 
qed 

419 

14693  420 

14551  421 
subsubsection {* Infimum *} 
422 

423 
lemma (in lattice) meetI: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

424 
"[ !!i. greatest L i (Lower L {x, y}) ==> P i; 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

425 
x \<in> carrier L; y \<in> carrier L ] 
14551  426 
==> P (x \<sqinter> y)" 
427 
proof (unfold meet_def inf_def) 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

428 
assume L: "x \<in> carrier L" "y \<in> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

429 
and P: "!!g. greatest L g (Lower L {x, y}) ==> P g" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

430 
with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

431 
with L show "P (THE g. greatest L g (Lower L {x, y}))" 
14551  432 
by (fast intro: theI2 greatest_unique P) 
433 
qed 

434 

435 
lemma (in lattice) meet_closed [simp]: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

436 
"[ x \<in> carrier L; y \<in> carrier L ] ==> x \<sqinter> y \<in> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

437 
by (rule meetI) (rule greatest_carrier) 
14551  438 

14651  439 
lemma (in partial_order) inf_of_singletonI: (* only reflexivity needed ? *) 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

440 
"x \<in> carrier L ==> greatest L x (Lower L {x})" 
14551  441 
by (rule greatest_LowerI) fast+ 
442 

443 
lemma (in partial_order) inf_of_singleton [simp]: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

444 
"x \<in> carrier L ==> \<Sqinter> {x} = x" 
14551  445 
by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI) 
446 

447 
text {* Condition on A: infimum exists. *} 

448 

449 
lemma (in lattice) inf_insertI: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

450 
"[ !!i. greatest L i (Lower L (insert x A)) ==> P i; 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

451 
greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L ] 
14693  452 
==> P (\<Sqinter>(insert x A))" 
14551  453 
proof (unfold inf_def) 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

454 
assume L: "x \<in> carrier L" "A \<subseteq> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

455 
and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

456 
and greatest_a: "greatest L a (Lower L A)" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

457 
from L greatest_a have La: "a \<in> carrier L" by simp 
14551  458 
from L inf_of_two_exists greatest_a 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

459 
obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

460 
show "P (THE g. greatest L g (Lower L (insert x A)))" 
14693  461 
proof (rule theI2) 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

462 
show "greatest L i (Lower L (insert x A))" 
14551  463 
proof (rule greatest_LowerI) 
464 
fix z 

14693  465 
assume "z \<in> insert x A" 
466 
then show "i \<sqsubseteq> z" 

467 
proof 

468 
assume "z = x" then show ?thesis 

469 
by (simp add: greatest_Lower_above [OF greatest_i] L La) 

470 
next 

471 
assume "z \<in> A" 

472 
with L greatest_i greatest_a show ?thesis 

473 
by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above) 

474 
qed 

475 
next 

476 
fix y 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

477 
assume y: "y \<in> Lower L (insert x A)" 
14693  478 
show "y \<sqsubseteq> i" 
479 
proof (rule greatest_le [OF greatest_i], rule Lower_memI) 

480 
fix z 

481 
assume z: "z \<in> {a, x}" 

482 
then show "y \<sqsubseteq> z" 

483 
proof 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

484 
have y': "y \<in> Lower L A" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

485 
apply (rule subsetD [where A = "Lower L (insert x A)"]) 
14693  486 
apply (rule Lower_antimono) apply clarify apply assumption 
487 
done 

488 
assume "z = a" 

489 
with y' greatest_a show ?thesis by (fast dest: greatest_le) 

490 
next 

491 
assume "z \<in> {x}" 

492 
with y L show ?thesis by blast 

493 
qed 

23350  494 
qed (rule Lower_closed [THEN subsetD, OF y]) 
14693  495 
next 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

496 
from L show "insert x A \<subseteq> carrier L" by simp 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

497 
from greatest_i show "i \<in> carrier L" by simp 
14551  498 
qed 
499 
next 

500 
fix g 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

501 
assume greatest_g: "greatest L g (Lower L (insert x A))" 
14551  502 
show "g = i" 
503 
proof (rule greatest_unique) 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

504 
show "greatest L i (Lower L (insert x A))" 
14551  505 
proof (rule greatest_LowerI) 
14693  506 
fix z 
507 
assume "z \<in> insert x A" 

508 
then show "i \<sqsubseteq> z" 

509 
proof 

510 
assume "z = x" then show ?thesis 

511 
by (simp add: greatest_Lower_above [OF greatest_i] L La) 

512 
next 

513 
assume "z \<in> A" 

514 
with L greatest_i greatest_a show ?thesis 

515 
by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above) 

516 
qed 

14551  517 
next 
14693  518 
fix y 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

519 
assume y: "y \<in> Lower L (insert x A)" 
14693  520 
show "y \<sqsubseteq> i" 
521 
proof (rule greatest_le [OF greatest_i], rule Lower_memI) 

522 
fix z 

523 
assume z: "z \<in> {a, x}" 

524 
then show "y \<sqsubseteq> z" 

525 
proof 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

526 
have y': "y \<in> Lower L A" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

527 
apply (rule subsetD [where A = "Lower L (insert x A)"]) 
14693  528 
apply (rule Lower_antimono) apply clarify apply assumption 
529 
done 

530 
assume "z = a" 

531 
with y' greatest_a show ?thesis by (fast dest: greatest_le) 

532 
next 

533 
assume "z \<in> {x}" 

534 
with y L show ?thesis by blast 

14551  535 
qed 
23350  536 
qed (rule Lower_closed [THEN subsetD, OF y]) 
14551  537 
next 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

538 
from L show "insert x A \<subseteq> carrier L" by simp 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

539 
from greatest_i show "i \<in> carrier L" by simp 
14551  540 
qed 
23350  541 
qed (rule greatest_g) 
542 
qed (rule P) 

14551  543 
qed 
544 

545 
lemma (in lattice) finite_inf_greatest: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

546 
"[ finite A; A \<subseteq> carrier L; A ~= {} ] ==> greatest L (\<Sqinter>A) (Lower L A)" 
22265  547 
proof (induct set: finite) 
14551  548 
case empty then show ?case by simp 
549 
next 

15328  550 
case (insert x A) 
14551  551 
show ?case 
552 
proof (cases "A = {}") 

553 
case True 

554 
with insert show ?thesis by (simp add: inf_of_singletonI) 

555 
next 

556 
case False 

557 
from insert show ?thesis 

558 
proof (rule_tac inf_insertI) 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

559 
from False insert show "greatest L (\<Sqinter>A) (Lower L A)" by simp 
14551  560 
qed simp_all 
561 
qed 

562 
qed 

563 

564 
lemma (in lattice) finite_inf_insertI: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

565 
assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

566 
and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" 
14551  567 
shows "P (\<Sqinter> (insert x A))" 
568 
proof (cases "A = {}") 

569 
case True with P and xA show ?thesis 

570 
by (simp add: inf_of_singletonI) 

571 
next 

572 
case False with P and xA show ?thesis 

573 
by (simp add: inf_insertI finite_inf_greatest) 

574 
qed 

575 

576 
lemma (in lattice) finite_inf_closed: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

577 
"[ finite A; A \<subseteq> carrier L; A ~= {} ] ==> \<Sqinter>A \<in> carrier L" 
22265  578 
proof (induct set: finite) 
14551  579 
case empty then show ?case by simp 
580 
next 

15328  581 
case insert then show ?case 
14551  582 
by (rule_tac finite_inf_insertI) (simp_all) 
583 
qed 

584 

585 
lemma (in lattice) meet_left: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

586 
"[ x \<in> carrier L; y \<in> carrier L ] ==> x \<sqinter> y \<sqsubseteq> x" 
14693  587 
by (rule meetI [folded meet_def]) (blast dest: greatest_mem) 
14551  588 

589 
lemma (in lattice) meet_right: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

590 
"[ x \<in> carrier L; y \<in> carrier L ] ==> x \<sqinter> y \<sqsubseteq> y" 
14693  591 
by (rule meetI [folded meet_def]) (blast dest: greatest_mem) 
14551  592 

593 
lemma (in lattice) inf_of_two_greatest: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

594 
"[ x \<in> carrier L; y \<in> carrier L ] ==> 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

595 
greatest L (\<Sqinter> {x, y}) (Lower L {x, y})" 
14551  596 
proof (unfold inf_def) 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

597 
assume L: "x \<in> carrier L" "y \<in> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

598 
with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast 
14551  599 
with L 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

600 
show "greatest L (THE xa. greatest L xa (Lower L {x, y})) (Lower L {x, y})" 
14551  601 
by (fast intro: theI2 greatest_unique) (* blast fails *) 
602 
qed 

603 

604 
lemma (in lattice) meet_le: 

14693  605 
assumes sub: "z \<sqsubseteq> x" "z \<sqsubseteq> y" 
23350  606 
and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L" 
14551  607 
shows "z \<sqsubseteq> x \<sqinter> y" 
23350  608 
proof (rule meetI [OF _ x y]) 
14551  609 
fix i 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

610 
assume "greatest L i (Lower L {x, y})" 
23350  611 
with sub z show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI) 
14551  612 
qed 
14693  613 

14551  614 
lemma (in lattice) meet_assoc_lemma: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

615 
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" 
14693  616 
shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}" 
14551  617 
proof (rule finite_inf_insertI) 
618 
txt {* The textbook argument in Jacobson I, p 457 *} 

619 
fix i 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

620 
assume inf: "greatest L i (Lower L {x, y, z})" 
14551  621 
show "x \<sqinter> (y \<sqinter> z) = i" 
622 
proof (rule anti_sym) 

623 
from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)" 

624 
by (fastsimp intro!: meet_le elim: greatest_Lower_above) 

625 
next 

626 
from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i" 

627 
by (erule_tac greatest_le) 

628 
(blast intro!: Lower_memI intro: trans meet_left meet_right meet_closed) 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

629 
qed (simp_all add: L greatest_carrier [OF inf]) 
14551  630 
qed (simp_all add: L) 
631 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

632 
lemma meet_comm: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

633 
fixes L (structure) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

634 
shows "x \<sqinter> y = y \<sqinter> x" 
14551  635 
by (unfold meet_def) (simp add: insert_commute) 
636 

637 
lemma (in lattice) meet_assoc: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

638 
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" 
14551  639 
shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" 
640 
proof  

641 
have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm) 

642 
also from L have "... = \<Sqinter> {z, x, y}" by (simp add: meet_assoc_lemma) 

643 
also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute) 

644 
also from L have "... = x \<sqinter> (y \<sqinter> z)" by (simp add: meet_assoc_lemma) 

645 
finally show ?thesis . 

646 
qed 

647 

14693  648 

14551  649 
subsection {* Total Orders *} 
650 

651 
locale total_order = lattice + 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

652 
assumes total: "[ x \<in> carrier L; y \<in> carrier L ] ==> x \<sqsubseteq> y  y \<sqsubseteq> x" 
14551  653 

654 
text {* Introduction rule: the usual definition of total order *} 

655 

656 
lemma (in partial_order) total_orderI: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

657 
assumes total: "!!x y. [ x \<in> carrier L; y \<in> carrier L ] ==> x \<sqsubseteq> y  y \<sqsubseteq> x" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

658 
shows "total_order L" 
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19931
diff
changeset

659 
proof intro_locales 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

660 
show "lattice_axioms L" 
14551  661 
proof (rule lattice_axioms.intro) 
662 
fix x y 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

663 
assume L: "x \<in> carrier L" "y \<in> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

664 
show "EX s. least L s (Upper L {x, y})" 
14551  665 
proof  
666 
note total L 

667 
moreover 

668 
{ 

14693  669 
assume "x \<sqsubseteq> y" 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

670 
with L have "least L y (Upper L {x, y})" 
14693  671 
by (rule_tac least_UpperI) auto 
14551  672 
} 
673 
moreover 

674 
{ 

14693  675 
assume "y \<sqsubseteq> x" 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

676 
with L have "least L x (Upper L {x, y})" 
14693  677 
by (rule_tac least_UpperI) auto 
14551  678 
} 
679 
ultimately show ?thesis by blast 

680 
qed 

681 
next 

682 
fix x y 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

683 
assume L: "x \<in> carrier L" "y \<in> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

684 
show "EX i. greatest L i (Lower L {x, y})" 
14551  685 
proof  
686 
note total L 

687 
moreover 

688 
{ 

14693  689 
assume "y \<sqsubseteq> x" 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

690 
with L have "greatest L y (Lower L {x, y})" 
14693  691 
by (rule_tac greatest_LowerI) auto 
14551  692 
} 
693 
moreover 

694 
{ 

14693  695 
assume "x \<sqsubseteq> y" 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

696 
with L have "greatest L x (Lower L {x, y})" 
14693  697 
by (rule_tac greatest_LowerI) auto 
14551  698 
} 
699 
ultimately show ?thesis by blast 

700 
qed 

701 
qed 

702 
qed (assumption  rule total_order_axioms.intro)+ 

703 

14693  704 

14551  705 
subsection {* Complete lattices *} 
706 

707 
locale complete_lattice = lattice + 

708 
assumes sup_exists: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

709 
"[ A \<subseteq> carrier L ] ==> EX s. least L s (Upper L A)" 
14551  710 
and inf_exists: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

711 
"[ A \<subseteq> carrier L ] ==> EX i. greatest L i (Lower L A)" 
21041
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

712 

14551  713 
text {* Introduction rule: the usual definition of complete lattice *} 
714 

715 
lemma (in partial_order) complete_latticeI: 

716 
assumes sup_exists: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

717 
"!!A. [ A \<subseteq> carrier L ] ==> EX s. least L s (Upper L A)" 
14551  718 
and inf_exists: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

719 
"!!A. [ A \<subseteq> carrier L ] ==> EX i. greatest L i (Lower L A)" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

720 
shows "complete_lattice L" 
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19931
diff
changeset

721 
proof intro_locales 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

722 
show "lattice_axioms L" 
14693  723 
by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+ 
14551  724 
qed (assumption  rule complete_lattice_axioms.intro)+ 
725 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

726 
constdefs (structure L) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

727 
top :: "_ => 'a" ("\<top>\<index>") 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

728 
"\<top> == sup L (carrier L)" 
21041
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

729 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

730 
bottom :: "_ => 'a" ("\<bottom>\<index>") 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

731 
"\<bottom> == inf L (carrier L)" 
14551  732 

733 

734 
lemma (in complete_lattice) supI: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

735 
"[ !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L ] 
14651  736 
==> P (\<Squnion>A)" 
14551  737 
proof (unfold sup_def) 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

738 
assume L: "A \<subseteq> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

739 
and P: "!!l. least L l (Upper L A) ==> P l" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

740 
with sup_exists obtain s where "least L s (Upper L A)" by blast 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

741 
with L show "P (THE l. least L l (Upper L A))" 
14551  742 
by (fast intro: theI2 least_unique P) 
743 
qed 

744 

745 
lemma (in complete_lattice) sup_closed [simp]: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

746 
"A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L" 
14551  747 
by (rule supI) simp_all 
748 

749 
lemma (in complete_lattice) top_closed [simp, intro]: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

750 
"\<top> \<in> carrier L" 
14551  751 
by (unfold top_def) simp 
752 

753 
lemma (in complete_lattice) infI: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

754 
"[ !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L ] 
14693  755 
==> P (\<Sqinter>A)" 
14551  756 
proof (unfold inf_def) 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

757 
assume L: "A \<subseteq> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

758 
and P: "!!l. greatest L l (Lower L A) ==> P l" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

759 
with inf_exists obtain s where "greatest L s (Lower L A)" by blast 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

760 
with L show "P (THE l. greatest L l (Lower L A))" 
14551  761 
by (fast intro: theI2 greatest_unique P) 
762 
qed 

763 

764 
lemma (in complete_lattice) inf_closed [simp]: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

765 
"A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L" 
14551  766 
by (rule infI) simp_all 
767 

768 
lemma (in complete_lattice) bottom_closed [simp, intro]: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

769 
"\<bottom> \<in> carrier L" 
14551  770 
by (unfold bottom_def) simp 
771 

772 
text {* Jacobson: Theorem 8.1 *} 

773 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

774 
lemma Lower_empty [simp]: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

775 
"Lower L {} = carrier L" 
14551  776 
by (unfold Lower_def) simp 
777 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

778 
lemma Upper_empty [simp]: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

779 
"Upper L {} = carrier L" 
14551  780 
by (unfold Upper_def) simp 
781 

782 
theorem (in partial_order) complete_lattice_criterion1: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

783 
assumes top_exists: "EX g. greatest L g (carrier L)" 
14551  784 
and inf_exists: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

785 
"!!A. [ A \<subseteq> carrier L; A ~= {} ] ==> EX i. greatest L i (Lower L A)" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

786 
shows "complete_lattice L" 
14551  787 
proof (rule complete_latticeI) 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

788 
from top_exists obtain top where top: "greatest L top (carrier L)" .. 
14551  789 
fix A 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

790 
assume L: "A \<subseteq> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

791 
let ?B = "Upper L A" 
14551  792 
from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le) 
793 
then have B_non_empty: "?B ~= {}" by fast 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

794 
have B_L: "?B \<subseteq> carrier L" by simp 
14551  795 
from inf_exists [OF B_L B_non_empty] 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

796 
obtain b where b_inf_B: "greatest L b (Lower L ?B)" .. 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

797 
have "least L b (Upper L A)" 
14551  798 
apply (rule least_UpperI) 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

799 
apply (rule greatest_le [where A = "Lower L ?B"]) 
14551  800 
apply (rule b_inf_B) 
801 
apply (rule Lower_memI) 

802 
apply (erule UpperD) 

803 
apply assumption 

804 
apply (rule L) 

805 
apply (fast intro: L [THEN subsetD]) 

806 
apply (erule greatest_Lower_above [OF b_inf_B]) 

807 
apply simp 

808 
apply (rule L) 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

809 
apply (rule greatest_carrier [OF b_inf_B]) (* rename rule: _closed *) 
14551  810 
done 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

811 
then show "EX s. least L s (Upper L A)" .. 
14551  812 
next 
813 
fix A 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

814 
assume L: "A \<subseteq> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

815 
show "EX i. greatest L i (Lower L A)" 
14551  816 
proof (cases "A = {}") 
817 
case True then show ?thesis 

818 
by (simp add: top_exists) 

819 
next 

820 
case False with L show ?thesis 

821 
by (rule inf_exists) 

822 
qed 

823 
qed 

824 

825 
(* TODO: prove dual version *) 

826 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset

827 

14551  828 
subsection {* Examples *} 
829 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset

830 
subsubsection {* Powerset of a Set is a Complete Lattice *} 
14551  831 

832 
theorem powerset_is_complete_lattice: 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

833 
"complete_lattice ( carrier = Pow A, le = op \<subseteq> )" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

834 
(is "complete_lattice ?L") 
14551  835 
proof (rule partial_order.complete_latticeI) 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

836 
show "partial_order ?L" 
14551  837 
by (rule partial_order.intro) auto 
838 
next 

839 
fix B 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

840 
assume "B \<subseteq> carrier ?L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

841 
then have "least ?L (\<Union> B) (Upper ?L B)" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

842 
by (fastsimp intro!: least_UpperI simp: Upper_def) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

843 
then show "EX s. least ?L s (Upper ?L B)" .. 
14551  844 
next 
845 
fix B 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

846 
assume "B \<subseteq> carrier ?L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

847 
then have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)" 
14551  848 
txt {* @{term "\<Inter> B"} is not the infimum of @{term B}: 
849 
@{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *} 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

850 
by (fastsimp intro!: greatest_LowerI simp: Lower_def) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

851 
then show "EX i. greatest ?L i (Lower ?L B)" .. 
14551  852 
qed 
853 

14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

854 
text {* An other example, that of the lattice of subgroups of a group, 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

855 
can be found in Group theory (Section~\ref{sec:subgrouplattice}). *} 
14551  856 

14693  857 
end 