author  haftmann 
Sun, 26 Feb 2012 20:10:14 +0100  
changeset 46691  72d81e789106 
parent 46689  f559866a7aa2 
child 46882  6242b4bc05bc 
permissions  rwrr 
21249  1 
(* Title: HOL/Lattices.thy 
2 
Author: Tobias Nipkow 

3 
*) 

4 

22454  5 
header {* Abstract lattices *} 
21249  6 

7 
theory Lattices 

35121  8 
imports Orderings Groups 
21249  9 
begin 
10 

35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

11 
subsection {* Abstract semilattice *} 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

12 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

13 
text {* 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

14 
This locales provide a basic structure for interpretation into 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

15 
bigger structures; extensions require careful thinking, otherwise 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

16 
undesired effects may occur due to interpretation. 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

17 
*} 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

18 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

19 
locale semilattice = abel_semigroup + 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

20 
assumes idem [simp]: "f a a = a" 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

21 
begin 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

22 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

23 
lemma left_idem [simp]: 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

24 
"f a (f a b) = f a b" 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

25 
by (simp add: assoc [symmetric]) 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

26 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

27 
end 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

28 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

29 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

30 
subsection {* Idempotent semigroup *} 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

31 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

32 
class ab_semigroup_idem_mult = ab_semigroup_mult + 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

33 
assumes mult_idem: "x * x = x" 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

34 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

35 
sublocale ab_semigroup_idem_mult < times!: semilattice times proof 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

36 
qed (fact mult_idem) 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

37 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

38 
context ab_semigroup_idem_mult 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

39 
begin 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

40 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

41 
lemmas mult_left_idem = times.left_idem 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

42 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

43 
end 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

44 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35121
diff
changeset

45 

46691  46 
subsection {* Syntactic infimum and supremum operations *} 
41082  47 

44845  48 
class inf = 
49 
fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70) 

25206  50 

44845  51 
class sup = 
52 
fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65) 

53 

46691  54 

55 
subsection {* Concrete lattices *} 

56 

57 
notation 

58 
less_eq (infix "\<sqsubseteq>" 50) and 

59 
less (infix "\<sqsubset>" 50) 

60 

44845  61 
class semilattice_inf = order + inf + 
22737  62 
assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x" 
63 
and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y" 

21733  64 
and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z" 
21249  65 

44845  66 
class semilattice_sup = order + sup + 
22737  67 
assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y" 
68 
and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y" 

21733  69 
and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x" 
26014  70 
begin 
71 

72 
text {* Dual lattice *} 

73 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

74 
lemma dual_semilattice: 
44845  75 
"class.semilattice_inf sup greater_eq greater" 
36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36352
diff
changeset

76 
by (rule class.semilattice_inf.intro, rule dual_order) 
27682  77 
(unfold_locales, simp_all add: sup_least) 
26014  78 

79 
end 

21249  80 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

81 
class lattice = semilattice_inf + semilattice_sup 
21249  82 

25382  83 

28562  84 
subsubsection {* Intro and elim rules*} 
21733  85 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

86 
context semilattice_inf 
21733  87 
begin 
21249  88 

32064  89 
lemma le_infI1: 
90 
"a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x" 

91 
by (rule order_trans) auto 

21249  92 

32064  93 
lemma le_infI2: 
94 
"b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x" 

95 
by (rule order_trans) auto 

21733  96 

32064  97 
lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b" 
36008  98 
by (rule inf_greatest) (* FIXME: duplicate lemma *) 
21249  99 

32064  100 
lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P" 
36008  101 
by (blast intro: order_trans inf_le1 inf_le2) 
21249  102 

21734  103 
lemma le_inf_iff [simp]: 
32064  104 
"x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z" 
105 
by (blast intro: le_infI elim: le_infE) 

21733  106 

32064  107 
lemma le_iff_inf: 
108 
"x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x" 

109 
by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1]) 

21249  110 

43753  111 
lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d" 
36008  112 
by (fast intro: inf_greatest le_infI1 le_infI2) 
113 

25206  114 
lemma mono_inf: 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

115 
fixes f :: "'a \<Rightarrow> 'b\<Colon>semilattice_inf" 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

116 
shows "mono f \<Longrightarrow> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B" 
25206  117 
by (auto simp add: mono_def intro: Lattices.inf_greatest) 
21733  118 

25206  119 
end 
21733  120 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

121 
context semilattice_sup 
21733  122 
begin 
21249  123 

32064  124 
lemma le_supI1: 
125 
"x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b" 

25062  126 
by (rule order_trans) auto 
21249  127 

32064  128 
lemma le_supI2: 
129 
"x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b" 

25062  130 
by (rule order_trans) auto 
21733  131 

32064  132 
lemma le_supI: 
133 
"a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x" 

36008  134 
by (rule sup_least) (* FIXME: duplicate lemma *) 
21249  135 

32064  136 
lemma le_supE: 
137 
"a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P" 

36008  138 
by (blast intro: order_trans sup_ge1 sup_ge2) 
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset

139 

32064  140 
lemma le_sup_iff [simp]: 
141 
"x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z" 

142 
by (blast intro: le_supI elim: le_supE) 

21733  143 

32064  144 
lemma le_iff_sup: 
145 
"x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y" 

146 
by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1]) 

21734  147 

43753  148 
lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d" 
36008  149 
by (fast intro: sup_least le_supI1 le_supI2) 
150 

25206  151 
lemma mono_sup: 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

152 
fixes f :: "'a \<Rightarrow> 'b\<Colon>semilattice_sup" 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

153 
shows "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)" 
25206  154 
by (auto simp add: mono_def intro: Lattices.sup_least) 
21733  155 

25206  156 
end 
23878  157 

21733  158 

32064  159 
subsubsection {* Equational laws *} 
21249  160 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

161 
sublocale semilattice_inf < inf!: semilattice inf 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

162 
proof 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

163 
fix a b c 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

164 
show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

165 
by (rule antisym) (auto intro: le_infI1 le_infI2) 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

166 
show "a \<sqinter> b = b \<sqinter> a" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

167 
by (rule antisym) auto 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

168 
show "a \<sqinter> a = a" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

169 
by (rule antisym) auto 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

170 
qed 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

171 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

172 
context semilattice_inf 
21733  173 
begin 
174 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

175 
lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

176 
by (fact inf.assoc) 
21733  177 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

178 
lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

179 
by (fact inf.commute) 
21733  180 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

181 
lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

182 
by (fact inf.left_commute) 
21733  183 

44921  184 
lemma inf_idem: "x \<sqinter> x = x" 
185 
by (fact inf.idem) (* already simp *) 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

186 

44918  187 
lemma inf_left_idem [simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y" 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

188 
by (fact inf.left_idem) 
21733  189 

32642
026e7c6a6d08
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
haftmann
parents:
32568
diff
changeset

190 
lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x" 
32064  191 
by (rule antisym) auto 
21733  192 

32642
026e7c6a6d08
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
haftmann
parents:
32568
diff
changeset

193 
lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y" 
32064  194 
by (rule antisym) auto 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

195 

32064  196 
lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem 
21733  197 

198 
end 

199 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

200 
sublocale semilattice_sup < sup!: semilattice sup 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

201 
proof 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

202 
fix a b c 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

203 
show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

204 
by (rule antisym) (auto intro: le_supI1 le_supI2) 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

205 
show "a \<squnion> b = b \<squnion> a" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

206 
by (rule antisym) auto 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

207 
show "a \<squnion> a = a" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

208 
by (rule antisym) auto 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

209 
qed 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

210 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

211 
context semilattice_sup 
21733  212 
begin 
21249  213 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

214 
lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

215 
by (fact sup.assoc) 
21733  216 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

217 
lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

218 
by (fact sup.commute) 
21733  219 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

220 
lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)" 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

221 
by (fact sup.left_commute) 
21733  222 

44921  223 
lemma sup_idem: "x \<squnion> x = x" 
224 
by (fact sup.idem) (* already simp *) 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

225 

44918  226 
lemma sup_left_idem [simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y" 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

227 
by (fact sup.left_idem) 
21733  228 

32642
026e7c6a6d08
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
haftmann
parents:
32568
diff
changeset

229 
lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x" 
32064  230 
by (rule antisym) auto 
21733  231 

32642
026e7c6a6d08
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
haftmann
parents:
32568
diff
changeset

232 
lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y" 
32064  233 
by (rule antisym) auto 
21249  234 

32064  235 
lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem 
21733  236 

237 
end 

21249  238 

21733  239 
context lattice 
240 
begin 

241 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

242 
lemma dual_lattice: 
44845  243 
"class.lattice sup (op \<ge>) (op >) inf" 
36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36352
diff
changeset

244 
by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order) 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

245 
(unfold_locales, auto) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

246 

44918  247 
lemma inf_sup_absorb [simp]: "x \<sqinter> (x \<squnion> y) = x" 
25102
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset

248 
by (blast intro: antisym inf_le1 inf_greatest sup_ge1) 
21733  249 

44918  250 
lemma sup_inf_absorb [simp]: "x \<squnion> (x \<sqinter> y) = x" 
25102
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset

251 
by (blast intro: antisym sup_ge1 sup_least inf_le1) 
21733  252 

32064  253 
lemmas inf_sup_aci = inf_aci sup_aci 
21734  254 

22454  255 
lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2 
256 

21734  257 
text{* Towards distributivity *} 
21249  258 

21734  259 
lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)" 
32064  260 
by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2) 
21734  261 

262 
lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)" 

32064  263 
by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2) 
21734  264 

265 
text{* If you have one of them, you have them all. *} 

21249  266 

21733  267 
lemma distrib_imp1: 
21249  268 
assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" 
269 
shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" 

270 
proof 

44918  271 
have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by simp 
272 
also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" 

273 
by (simp add: D inf_commute sup_assoc del: sup_inf_absorb) 

21249  274 
also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" 
44919  275 
by(simp add: inf_commute) 
21249  276 
also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D) 
277 
finally show ?thesis . 

278 
qed 

279 

21733  280 
lemma distrib_imp2: 
21249  281 
assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" 
282 
shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" 

283 
proof 

44918  284 
have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by simp 
285 
also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" 

286 
by (simp add: D sup_commute inf_assoc del: inf_sup_absorb) 

21249  287 
also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)" 
44919  288 
by(simp add: sup_commute) 
21249  289 
also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D) 
290 
finally show ?thesis . 

291 
qed 

292 

21733  293 
end 
21249  294 

32568  295 
subsubsection {* Strict order *} 
296 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

297 
context semilattice_inf 
32568  298 
begin 
299 

300 
lemma less_infI1: 

301 
"a \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x" 

32642
026e7c6a6d08
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
haftmann
parents:
32568
diff
changeset

302 
by (auto simp add: less_le inf_absorb1 intro: le_infI1) 
32568  303 

304 
lemma less_infI2: 

305 
"b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x" 

32642
026e7c6a6d08
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
haftmann
parents:
32568
diff
changeset

306 
by (auto simp add: less_le inf_absorb2 intro: le_infI2) 
32568  307 

308 
end 

309 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

310 
context semilattice_sup 
32568  311 
begin 
312 

313 
lemma less_supI1: 

34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

314 
"x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b" 
44921  315 
using dual_semilattice 
316 
by (rule semilattice_inf.less_infI1) 

32568  317 

318 
lemma less_supI2: 

34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

319 
"x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b" 
44921  320 
using dual_semilattice 
321 
by (rule semilattice_inf.less_infI2) 

32568  322 

323 
end 

324 

21249  325 

24164  326 
subsection {* Distributive lattices *} 
21249  327 

22454  328 
class distrib_lattice = lattice + 
21249  329 
assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" 
330 

21733  331 
context distrib_lattice 
332 
begin 

333 

334 
lemma sup_inf_distrib2: 

44921  335 
"(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)" 
336 
by (simp add: sup_commute sup_inf_distrib1) 

21249  337 

21733  338 
lemma inf_sup_distrib1: 
44921  339 
"x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" 
340 
by (rule distrib_imp2 [OF sup_inf_distrib1]) 

21249  341 

21733  342 
lemma inf_sup_distrib2: 
44921  343 
"(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)" 
344 
by (simp add: inf_commute inf_sup_distrib1) 

21249  345 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

346 
lemma dual_distrib_lattice: 
44845  347 
"class.distrib_lattice sup (op \<ge>) (op >) inf" 
36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36352
diff
changeset

348 
by (rule class.distrib_lattice.intro, rule dual_lattice) 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

349 
(unfold_locales, fact inf_sup_distrib1) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

350 

36008  351 
lemmas sup_inf_distrib = 
352 
sup_inf_distrib1 sup_inf_distrib2 

353 

354 
lemmas inf_sup_distrib = 

355 
inf_sup_distrib1 inf_sup_distrib2 

356 

21733  357 
lemmas distrib = 
21249  358 
sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2 
359 

21733  360 
end 
361 

21249  362 

34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

363 
subsection {* Bounded lattices and boolean algebras *} 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

364 

36352
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

365 
class bounded_lattice_bot = lattice + bot 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

366 
begin 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

367 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

368 
lemma inf_bot_left [simp]: 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

369 
"\<bottom> \<sqinter> x = \<bottom>" 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

370 
by (rule inf_absorb1) simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

371 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

372 
lemma inf_bot_right [simp]: 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

373 
"x \<sqinter> \<bottom> = \<bottom>" 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

374 
by (rule inf_absorb2) simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

375 

36352
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

376 
lemma sup_bot_left [simp]: 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

377 
"\<bottom> \<squnion> x = x" 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

378 
by (rule sup_absorb2) simp 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

379 

f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

380 
lemma sup_bot_right [simp]: 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

381 
"x \<squnion> \<bottom> = x" 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

382 
by (rule sup_absorb1) simp 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

383 

f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

384 
lemma sup_eq_bot_iff [simp]: 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

385 
"x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>" 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

386 
by (simp add: eq_iff) 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

387 

f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

388 
end 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

389 

f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

390 
class bounded_lattice_top = lattice + top 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

391 
begin 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

392 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

393 
lemma sup_top_left [simp]: 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

394 
"\<top> \<squnion> x = \<top>" 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

395 
by (rule sup_absorb1) simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

396 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

397 
lemma sup_top_right [simp]: 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

398 
"x \<squnion> \<top> = \<top>" 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

399 
by (rule sup_absorb2) simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

400 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

401 
lemma inf_top_left [simp]: 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

402 
"\<top> \<sqinter> x = x" 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

403 
by (rule inf_absorb2) simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

404 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

405 
lemma inf_top_right [simp]: 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

406 
"x \<sqinter> \<top> = x" 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

407 
by (rule inf_absorb1) simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

408 

36008  409 
lemma inf_eq_top_iff [simp]: 
410 
"x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>" 

411 
by (simp add: eq_iff) 

32568  412 

36352
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

413 
end 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

414 

f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

415 
class bounded_lattice = bounded_lattice_bot + bounded_lattice_top 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

416 
begin 
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

417 

f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

418 
lemma dual_bounded_lattice: 
44845  419 
"class.bounded_lattice sup greater_eq greater inf \<top> \<bottom>" 
36352
f71978e47cd5
add bounded_lattice_bot and bounded_lattice_top type classes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36096
diff
changeset

420 
by unfold_locales (auto simp add: less_le_not_le) 
32568  421 

34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

422 
end 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

423 

aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

424 
class boolean_algebra = distrib_lattice + bounded_lattice + minus + uminus + 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

425 
assumes inf_compl_bot: "x \<sqinter>  x = \<bottom>" 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

426 
and sup_compl_top: "x \<squnion>  x = \<top>" 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

427 
assumes diff_eq: "x  y = x \<sqinter>  y" 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

428 
begin 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

429 

aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

430 
lemma dual_boolean_algebra: 
44845  431 
"class.boolean_algebra (\<lambda>x y. x \<squnion>  y) uminus sup greater_eq greater inf \<top> \<bottom>" 
36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
36352
diff
changeset

432 
by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice) 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

433 
(unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq) 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

434 

44918  435 
lemma compl_inf_bot [simp]: 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

436 
" x \<sqinter> x = \<bottom>" 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

437 
by (simp add: inf_commute inf_compl_bot) 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

438 

44918  439 
lemma compl_sup_top [simp]: 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

440 
" x \<squnion> x = \<top>" 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

441 
by (simp add: sup_commute sup_compl_top) 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

442 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

443 
lemma compl_unique: 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

444 
assumes "x \<sqinter> y = \<bottom>" 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

445 
and "x \<squnion> y = \<top>" 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

446 
shows " x = y" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

447 
proof  
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

448 
have "(x \<sqinter>  x) \<squnion> ( x \<sqinter> y) = (x \<sqinter> y) \<squnion> ( x \<sqinter> y)" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

449 
using inf_compl_bot assms(1) by simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

450 
then have "( x \<sqinter> x) \<squnion> ( x \<sqinter> y) = (y \<sqinter> x) \<squnion> (y \<sqinter>  x)" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

451 
by (simp add: inf_commute) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

452 
then have " x \<sqinter> (x \<squnion> y) = y \<sqinter> (x \<squnion>  x)" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

453 
by (simp add: inf_sup_distrib1) 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

454 
then have " x \<sqinter> \<top> = y \<sqinter> \<top>" 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

455 
using sup_compl_top assms(2) by simp 
34209  456 
then show " x = y" by simp 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

457 
qed 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

458 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

459 
lemma double_compl [simp]: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

460 
" ( x) = x" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

461 
using compl_inf_bot compl_sup_top by (rule compl_unique) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

462 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

463 
lemma compl_eq_compl_iff [simp]: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

464 
" x =  y \<longleftrightarrow> x = y" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

465 
proof 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

466 
assume " x =  y" 
36008  467 
then have " ( x) =  ( y)" by (rule arg_cong) 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

468 
then show "x = y" by simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

469 
next 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

470 
assume "x = y" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

471 
then show " x =  y" by simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

472 
qed 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

473 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

474 
lemma compl_bot_eq [simp]: 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

475 
" \<bottom> = \<top>" 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

476 
proof  
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

477 
from sup_compl_top have "\<bottom> \<squnion>  \<bottom> = \<top>" . 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

478 
then show ?thesis by simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

479 
qed 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

480 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

481 
lemma compl_top_eq [simp]: 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

482 
" \<top> = \<bottom>" 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

483 
proof  
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

484 
from inf_compl_bot have "\<top> \<sqinter>  \<top> = \<bottom>" . 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

485 
then show ?thesis by simp 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

486 
qed 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

487 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

488 
lemma compl_inf [simp]: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

489 
" (x \<sqinter> y) =  x \<squnion>  y" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

490 
proof (rule compl_unique) 
36008  491 
have "(x \<sqinter> y) \<sqinter> ( x \<squnion>  y) = (y \<sqinter> (x \<sqinter>  x)) \<squnion> (x \<sqinter> (y \<sqinter>  y))" 
492 
by (simp only: inf_sup_distrib inf_aci) 

493 
then show "(x \<sqinter> y) \<sqinter> ( x \<squnion>  y) = \<bottom>" 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

494 
by (simp add: inf_compl_bot) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

495 
next 
36008  496 
have "(x \<sqinter> y) \<squnion> ( x \<squnion>  y) = ( y \<squnion> (x \<squnion>  x)) \<sqinter> ( x \<squnion> (y \<squnion>  y))" 
497 
by (simp only: sup_inf_distrib sup_aci) 

498 
then show "(x \<sqinter> y) \<squnion> ( x \<squnion>  y) = \<top>" 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

499 
by (simp add: sup_compl_top) 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

500 
qed 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

501 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

502 
lemma compl_sup [simp]: 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

503 
" (x \<squnion> y) =  x \<sqinter>  y" 
44921  504 
using dual_boolean_algebra 
505 
by (rule boolean_algebra.compl_inf) 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

506 

36008  507 
lemma compl_mono: 
508 
"x \<sqsubseteq> y \<Longrightarrow>  y \<sqsubseteq>  x" 

509 
proof  

510 
assume "x \<sqsubseteq> y" 

511 
then have "x \<squnion> y = y" by (simp only: le_iff_sup) 

512 
then have " (x \<squnion> y) =  y" by simp 

513 
then have " x \<sqinter>  y =  y" by simp 

514 
then have " y \<sqinter>  x =  y" by (simp only: inf_commute) 

515 
then show " y \<sqsubseteq>  x" by (simp only: le_iff_inf) 

516 
qed 

517 

44918  518 
lemma compl_le_compl_iff [simp]: 
43753  519 
" x \<sqsubseteq>  y \<longleftrightarrow> y \<sqsubseteq> x" 
43873  520 
by (auto dest: compl_mono) 
521 

522 
lemma compl_le_swap1: 

523 
assumes "y \<sqsubseteq>  x" shows "x \<sqsubseteq> y" 

524 
proof  

525 
from assms have " ( x) \<sqsubseteq>  y" by (simp only: compl_le_compl_iff) 

526 
then show ?thesis by simp 

527 
qed 

528 

529 
lemma compl_le_swap2: 

530 
assumes " y \<sqsubseteq> x" shows " x \<sqsubseteq> y" 

531 
proof  

532 
from assms have " x \<sqsubseteq>  ( y)" by (simp only: compl_le_compl_iff) 

533 
then show ?thesis by simp 

534 
qed 

535 

536 
lemma compl_less_compl_iff: (* TODO: declare [simp] ? *) 

537 
" x \<sqsubset>  y \<longleftrightarrow> y \<sqsubset> x" 

44919  538 
by (auto simp add: less_le) 
43873  539 

540 
lemma compl_less_swap1: 

541 
assumes "y \<sqsubset>  x" shows "x \<sqsubset>  y" 

542 
proof  

543 
from assms have " ( x) \<sqsubset>  y" by (simp only: compl_less_compl_iff) 

544 
then show ?thesis by simp 

545 
qed 

546 

547 
lemma compl_less_swap2: 

548 
assumes " y \<sqsubset> x" shows " x \<sqsubset> y" 

549 
proof  

550 
from assms have " x \<sqsubset>  ( y)" by (simp only: compl_less_compl_iff) 

551 
then show ?thesis by simp 

552 
qed 

36008  553 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

554 
end 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

555 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

556 

22454  557 
subsection {* Uniqueness of inf and sup *} 
558 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

559 
lemma (in semilattice_inf) inf_unique: 
22454  560 
fixes f (infixl "\<triangle>" 70) 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

561 
assumes le1: "\<And>x y. x \<triangle> y \<sqsubseteq> x" and le2: "\<And>x y. x \<triangle> y \<sqsubseteq> y" 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

562 
and greatest: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z" 
22737  563 
shows "x \<sqinter> y = x \<triangle> y" 
22454  564 
proof (rule antisym) 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

565 
show "x \<triangle> y \<sqsubseteq> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2) 
22454  566 
next 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

567 
have leI: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z" by (blast intro: greatest) 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

568 
show "x \<sqinter> y \<sqsubseteq> x \<triangle> y" by (rule leI) simp_all 
22454  569 
qed 
570 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

571 
lemma (in semilattice_sup) sup_unique: 
22454  572 
fixes f (infixl "\<nabla>" 70) 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

573 
assumes ge1 [simp]: "\<And>x y. x \<sqsubseteq> x \<nabla> y" and ge2: "\<And>x y. y \<sqsubseteq> x \<nabla> y" 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

574 
and least: "\<And>x y z. y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<nabla> z \<sqsubseteq> x" 
22737  575 
shows "x \<squnion> y = x \<nabla> y" 
22454  576 
proof (rule antisym) 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

577 
show "x \<squnion> y \<sqsubseteq> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2) 
22454  578 
next 
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

579 
have leI: "\<And>x y z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<nabla> y \<sqsubseteq> z" by (blast intro: least) 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

580 
show "x \<nabla> y \<sqsubseteq> x \<squnion> y" by (rule leI) simp_all 
22454  581 
qed 
36008  582 

22454  583 

22916  584 
subsection {* @{const min}/@{const max} on linear orders as 
585 
special case of @{const inf}/@{const sup} *} 

586 

44845  587 
sublocale linorder < min_max!: distrib_lattice min less_eq less max 
28823  588 
proof 
22916  589 
fix x y z 
32512  590 
show "max x (min y z) = min (max x y) (max x z)" 
591 
by (auto simp add: min_def max_def) 

22916  592 
qed (auto simp add: min_def max_def not_le less_imp_le) 
21249  593 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

594 
lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{semilattice_inf, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" 
25102
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset

595 
by (rule ext)+ (auto intro: antisym) 
21733  596 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

597 
lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{semilattice_sup, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" 
25102
db3e412c4cb1
antisymmetry not a default intro rule any longer
haftmann
parents:
25062
diff
changeset

598 
by (rule ext)+ (auto intro: antisym) 
21733  599 

21249  600 
lemmas le_maxI1 = min_max.sup_ge1 
601 
lemmas le_maxI2 = min_max.sup_ge2 

21381  602 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

603 
lemmas min_ac = min_max.inf_assoc min_max.inf_commute 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

604 
min_max.inf.left_commute 
21249  605 

34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

606 
lemmas max_ac = min_max.sup_assoc min_max.sup_commute 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

607 
min_max.sup.left_commute 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34209
diff
changeset

608 

21249  609 

46631
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

610 
subsection {* Lattice on @{typ bool} *} 
22454  611 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

612 
instantiation bool :: boolean_algebra 
25510  613 
begin 
614 

615 
definition 

41080  616 
bool_Compl_def [simp]: "uminus = Not" 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

617 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

618 
definition 
41080  619 
bool_diff_def [simp]: "A  B \<longleftrightarrow> A \<and> \<not> B" 
31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

620 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

621 
definition 
41080  622 
[simp]: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q" 
25510  623 

624 
definition 

41080  625 
[simp]: "P \<squnion> Q \<longleftrightarrow> P \<or> Q" 
25510  626 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

627 
instance proof 
41080  628 
qed auto 
22454  629 

25510  630 
end 
631 

32781  632 
lemma sup_boolI1: 
633 
"P \<Longrightarrow> P \<squnion> Q" 

41080  634 
by simp 
32781  635 

636 
lemma sup_boolI2: 

637 
"Q \<Longrightarrow> P \<squnion> Q" 

41080  638 
by simp 
32781  639 

640 
lemma sup_boolE: 

641 
"P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R" 

41080  642 
by auto 
32781  643 

23878  644 

46631
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

645 
subsection {* Lattice on @{typ "_ \<Rightarrow> _"} *} 
23878  646 

25510  647 
instantiation "fun" :: (type, lattice) lattice 
648 
begin 

649 

650 
definition 

41080  651 
"f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)" 
652 

46689  653 
lemma inf_apply (* CANDIDATE [simp, code] *): 
41080  654 
"(f \<sqinter> g) x = f x \<sqinter> g x" 
655 
by (simp add: inf_fun_def) 

25510  656 

657 
definition 

41080  658 
"f \<squnion> g = (\<lambda>x. f x \<squnion> g x)" 
659 

46689  660 
lemma sup_apply (* CANDIDATE [simp, code] *): 
41080  661 
"(f \<squnion> g) x = f x \<squnion> g x" 
662 
by (simp add: sup_fun_def) 

25510  663 

32780  664 
instance proof 
41080  665 
qed (simp_all add: le_fun_def inf_apply sup_apply) 
23878  666 

25510  667 
end 
23878  668 

41080  669 
instance "fun" :: (type, distrib_lattice) distrib_lattice proof 
670 
qed (rule ext, simp add: sup_inf_distrib1 inf_apply sup_apply) 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

671 

34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

672 
instance "fun" :: (type, bounded_lattice) bounded_lattice .. 
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
32781
diff
changeset

673 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

674 
instantiation "fun" :: (type, uminus) uminus 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

675 
begin 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

676 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

677 
definition 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

678 
fun_Compl_def: " A = (\<lambda>x.  A x)" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

679 

46689  680 
lemma uminus_apply (* CANDIDATE [simp, code] *): 
41080  681 
"( A) x =  (A x)" 
682 
by (simp add: fun_Compl_def) 

683 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

684 
instance .. 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

685 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

686 
end 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

687 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

688 
instantiation "fun" :: (type, minus) minus 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

689 
begin 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

690 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

691 
definition 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

692 
fun_diff_def: "A  B = (\<lambda>x. A x  B x)" 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

693 

46689  694 
lemma minus_apply (* CANDIDATE [simp, code] *): 
41080  695 
"(A  B) x = A x  B x" 
696 
by (simp add: fun_diff_def) 

697 

31991
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

698 
instance .. 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

699 

37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

700 
end 
37390299214a
added boolean_algebra type class; tuned lattice duals
haftmann
parents:
30729
diff
changeset

701 

41080  702 
instance "fun" :: (type, boolean_algebra) boolean_algebra proof 
703 
qed (rule ext, simp_all add: inf_apply sup_apply bot_apply top_apply uminus_apply minus_apply inf_compl_bot sup_compl_top diff_eq)+ 

26794  704 

46631
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

705 

2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

706 
subsection {* Lattice on unary and binary predicates *} 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

707 

2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

708 
lemma inf1I: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x" 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

709 
by (simp add: inf_fun_def) 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

710 

2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

711 
lemma inf2I: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y" 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

712 
by (simp add: inf_fun_def) 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

713 

2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

714 
lemma inf1E: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P" 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

715 
by (simp add: inf_fun_def) 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

716 

2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

717 
lemma inf2E: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P" 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

718 
by (simp add: inf_fun_def) 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

719 

2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

720 
lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x" 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

721 
by (simp add: inf_fun_def) 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

722 

2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

723 
lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y" 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

724 
by (simp add: inf_fun_def) 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

725 

2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

726 
lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x" 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

727 
by (simp add: inf_fun_def) 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

728 

2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

729 
lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y" 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

730 
by (simp add: inf_fun_def) 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

731 

2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

732 
lemma sup1I1: "A x \<Longrightarrow> (A \<squnion> B) x" 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

733 
by (simp add: sup_fun_def) 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

734 

2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

735 
lemma sup2I1: "A x y \<Longrightarrow> (A \<squnion> B) x y" 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

736 
by (simp add: sup_fun_def) 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

737 

2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

738 
lemma sup1I2: "B x \<Longrightarrow> (A \<squnion> B) x" 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

739 
by (simp add: sup_fun_def) 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

740 

2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

741 
lemma sup2I2: "B x y \<Longrightarrow> (A \<squnion> B) x y" 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

742 
by (simp add: sup_fun_def) 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

743 

2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

744 
lemma sup1E: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P" 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

745 
by (simp add: sup_fun_def) iprover 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

746 

2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

747 
lemma sup2E: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P" 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

748 
by (simp add: sup_fun_def) iprover 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

749 

2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

750 
text {* 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

751 
\medskip Classical introduction rule: no commitment to @{text A} vs 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

752 
@{text B}. 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

753 
*} 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

754 

2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

755 
lemma sup1CI: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x" 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

756 
by (auto simp add: sup_fun_def) 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

757 

2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

758 
lemma sup2CI: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y" 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

759 
by (auto simp add: sup_fun_def) 
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

760 

2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

761 

25062  762 
no_notation 
46691  763 
less_eq (infix "\<sqsubseteq>" 50) and 
764 
less (infix "\<sqsubset>" 50) 

25062  765 

21249  766 
end 
46631
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

767 