equal
deleted
inserted
replaced
96 lemma boundedE: |
96 lemma boundedE: |
97 assumes "a \<preceq> b * c" |
97 assumes "a \<preceq> b * c" |
98 obtains "a \<preceq> b" and "a \<preceq> c" |
98 obtains "a \<preceq> b" and "a \<preceq> c" |
99 using assms by (blast intro: trans cobounded1 cobounded2) |
99 using assms by (blast intro: trans cobounded1 cobounded2) |
100 |
100 |
101 lemma bounded_iff (* [simp] CANDIDATE *): |
101 lemma bounded_iff [simp]: |
102 "a \<preceq> b * c \<longleftrightarrow> a \<preceq> b \<and> a \<preceq> c" |
102 "a \<preceq> b * c \<longleftrightarrow> a \<preceq> b \<and> a \<preceq> c" |
103 by (blast intro: boundedI elim: boundedE) |
103 by (blast intro: boundedI elim: boundedE) |
104 |
104 |
105 lemma strict_boundedE: |
105 lemma strict_boundedE: |
106 assumes "a \<prec> b * c" |
106 assumes "a \<prec> b * c" |
107 obtains "a \<prec> b" and "a \<prec> c" |
107 obtains "a \<prec> b" and "a \<prec> c" |
108 using assms by (auto simp add: commute strict_iff_order bounded_iff elim: orderE intro!: that)+ |
108 using assms by (auto simp add: commute strict_iff_order elim: orderE intro!: that)+ |
109 |
109 |
110 lemma coboundedI1: |
110 lemma coboundedI1: |
111 "a \<preceq> c \<Longrightarrow> a * b \<preceq> c" |
111 "a \<preceq> c \<Longrightarrow> a * b \<preceq> c" |
112 by (rule trans) auto |
112 by (rule trans) auto |
113 |
113 |
126 |
126 |
127 lemma mono: "a \<preceq> c \<Longrightarrow> b \<preceq> d \<Longrightarrow> a * b \<preceq> c * d" |
127 lemma mono: "a \<preceq> c \<Longrightarrow> b \<preceq> d \<Longrightarrow> a * b \<preceq> c * d" |
128 by (blast intro: boundedI coboundedI1 coboundedI2) |
128 by (blast intro: boundedI coboundedI1 coboundedI2) |
129 |
129 |
130 lemma absorb1: "a \<preceq> b \<Longrightarrow> a * b = a" |
130 lemma absorb1: "a \<preceq> b \<Longrightarrow> a * b = a" |
131 by (rule antisym) (auto simp add: bounded_iff refl) |
131 by (rule antisym) (auto simp add: refl) |
132 |
132 |
133 lemma absorb2: "b \<preceq> a \<Longrightarrow> a * b = b" |
133 lemma absorb2: "b \<preceq> a \<Longrightarrow> a * b = b" |
134 by (rule antisym) (auto simp add: bounded_iff refl) |
134 by (rule antisym) (auto simp add: refl) |
135 |
135 |
136 lemma absorb_iff1: "a \<preceq> b \<longleftrightarrow> a * b = a" |
136 lemma absorb_iff1: "a \<preceq> b \<longleftrightarrow> a * b = a" |
137 using order_iff by auto |
137 using order_iff by auto |
138 |
138 |
139 lemma absorb_iff2: "b \<preceq> a \<longleftrightarrow> a * b = b" |
139 lemma absorb_iff2: "b \<preceq> a \<longleftrightarrow> a * b = b" |
208 by (fact inf_greatest) (* FIXME: duplicate lemma *) |
208 by (fact inf_greatest) (* FIXME: duplicate lemma *) |
209 |
209 |
210 lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P" |
210 lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P" |
211 by (blast intro: order_trans inf_le1 inf_le2) |
211 by (blast intro: order_trans inf_le1 inf_le2) |
212 |
212 |
213 lemma le_inf_iff [simp]: |
213 lemma le_inf_iff: |
214 "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z" |
214 "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z" |
215 by (blast intro: le_infI elim: le_infE) |
215 by (blast intro: le_infI elim: le_infE) |
216 |
216 |
217 lemma le_iff_inf: |
217 lemma le_iff_inf: |
218 "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x" |
218 "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x" |
219 by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1]) |
219 by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1] simp add: le_inf_iff) |
220 |
220 |
221 lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d" |
221 lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d" |
222 by (fast intro: inf_greatest le_infI1 le_infI2) |
222 by (fast intro: inf_greatest le_infI1 le_infI2) |
223 |
223 |
224 lemma mono_inf: |
224 lemma mono_inf: |
245 |
245 |
246 lemma le_supE: |
246 lemma le_supE: |
247 "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P" |
247 "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P" |
248 by (blast intro: order_trans sup_ge1 sup_ge2) |
248 by (blast intro: order_trans sup_ge1 sup_ge2) |
249 |
249 |
250 lemma le_sup_iff [simp]: |
250 lemma le_sup_iff: |
251 "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z" |
251 "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z" |
252 by (blast intro: le_supI elim: le_supE) |
252 by (blast intro: le_supI elim: le_supE) |
253 |
253 |
254 lemma le_iff_sup: |
254 lemma le_iff_sup: |
255 "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y" |
255 "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y" |
256 by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1]) |
256 by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1] simp add: le_sup_iff) |
257 |
257 |
258 lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d" |
258 lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d" |
259 by (fast intro: sup_least le_supI1 le_supI2) |
259 by (fast intro: sup_least le_supI1 le_supI2) |
260 |
260 |
261 lemma mono_sup: |
261 lemma mono_sup: |
273 |
273 |
274 sublocale inf!: semilattice inf |
274 sublocale inf!: semilattice inf |
275 proof |
275 proof |
276 fix a b c |
276 fix a b c |
277 show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)" |
277 show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)" |
278 by (rule antisym) (auto intro: le_infI1 le_infI2) |
278 by (rule antisym) (auto intro: le_infI1 le_infI2 simp add: le_inf_iff) |
279 show "a \<sqinter> b = b \<sqinter> a" |
279 show "a \<sqinter> b = b \<sqinter> a" |
280 by (rule antisym) auto |
280 by (rule antisym) (auto simp add: le_inf_iff) |
281 show "a \<sqinter> a = a" |
281 show "a \<sqinter> a = a" |
282 by (rule antisym) auto |
282 by (rule antisym) (auto simp add: le_inf_iff) |
283 qed |
283 qed |
284 |
284 |
285 sublocale inf!: semilattice_order inf less_eq less |
285 sublocale inf!: semilattice_order inf less_eq less |
286 by default (auto simp add: le_iff_inf less_le) |
286 by default (auto simp add: le_iff_inf less_le) |
287 |
287 |
318 |
318 |
319 sublocale sup!: semilattice sup |
319 sublocale sup!: semilattice sup |
320 proof |
320 proof |
321 fix a b c |
321 fix a b c |
322 show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)" |
322 show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)" |
323 by (rule antisym) (auto intro: le_supI1 le_supI2) |
323 by (rule antisym) (auto intro: le_supI1 le_supI2 simp add: le_sup_iff) |
324 show "a \<squnion> b = b \<squnion> a" |
324 show "a \<squnion> b = b \<squnion> a" |
325 by (rule antisym) auto |
325 by (rule antisym) (auto simp add: le_sup_iff) |
326 show "a \<squnion> a = a" |
326 show "a \<squnion> a = a" |
327 by (rule antisym) auto |
327 by (rule antisym) (auto simp add: le_sup_iff) |
328 qed |
328 qed |
329 |
329 |
330 sublocale sup!: semilattice_order sup greater_eq greater |
330 sublocale sup!: semilattice_order sup greater_eq greater |
331 by default (auto simp add: le_iff_sup sup.commute less_le) |
331 by default (auto simp add: le_iff_sup sup.commute less_le) |
332 |
332 |