src/HOL/Algebra/Order.thy
 author wenzelm Tue Oct 10 19:23:03 2017 +0200 (2017-10-10) changeset 66831 29ea2b900a05 parent 66453 cc19f7ca2ed6 child 67091 1393c2340eec permissions -rw-r--r--
tuned: each session has at most one defining entry;
1 (*  Title:      HOL/Algebra/Order.thy
2     Author:     Clemens Ballarin, started 7 November 2003
3     Copyright:  Clemens Ballarin
5 Most congruence rules by Stephan Hohe.
6 With additional contributions from Alasdair Armstrong and Simon Foster.
7 *)
9 theory Order
10 imports
11   "HOL-Library.FuncSet"
12   Congruence
13 begin
15 section \<open>Orders\<close>
17 subsection \<open>Partial Orders\<close>
19 record 'a gorder = "'a eq_object" +
20   le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
22 abbreviation inv_gorder :: "_ \<Rightarrow> 'a gorder" where
23   "inv_gorder L \<equiv>
24    \<lparr> carrier = carrier L,
25      eq = op .=\<^bsub>L\<^esub>,
26      le = (\<lambda> x y. y \<sqsubseteq>\<^bsub>L \<^esub>x) \<rparr>"
28 lemma inv_gorder_inv:
29   "inv_gorder (inv_gorder L) = L"
30   by simp
32 locale weak_partial_order = equivalence L for L (structure) +
33   assumes le_refl [intro, simp]:
34       "x \<in> carrier L ==> x \<sqsubseteq> x"
35     and weak_le_antisym [intro]:
36       "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x .= y"
37     and le_trans [trans]:
38       "[| x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
39     and le_cong:
40       "\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow>
41       x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"
43 definition
44   lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
45   where "x \<sqsubset>\<^bsub>L\<^esub> y \<longleftrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> y & x .\<noteq>\<^bsub>L\<^esub> y"
48 subsubsection \<open>The order relation\<close>
50 context weak_partial_order
51 begin
53 lemma le_cong_l [intro, trans]:
54   "\<lbrakk> x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
55   by (auto intro: le_cong [THEN iffD2])
57 lemma le_cong_r [intro, trans]:
58   "\<lbrakk> x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
59   by (auto intro: le_cong [THEN iffD1])
61 lemma weak_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"
62   by (simp add: le_cong_l)
64 end
66 lemma weak_llessI:
67   fixes R (structure)
68   assumes "x \<sqsubseteq> y" and "~(x .= y)"
69   shows "x \<sqsubset> y"
70   using assms unfolding lless_def by simp
72 lemma lless_imp_le:
73   fixes R (structure)
74   assumes "x \<sqsubset> y"
75   shows "x \<sqsubseteq> y"
76   using assms unfolding lless_def by simp
78 lemma weak_lless_imp_not_eq:
79   fixes R (structure)
80   assumes "x \<sqsubset> y"
81   shows "\<not> (x .= y)"
82   using assms unfolding lless_def by simp
84 lemma weak_llessE:
85   fixes R (structure)
86   assumes p: "x \<sqsubset> y" and e: "\<lbrakk>x \<sqsubseteq> y; \<not> (x .= y)\<rbrakk> \<Longrightarrow> P"
87   shows "P"
88   using p by (blast dest: lless_imp_le weak_lless_imp_not_eq e)
90 lemma (in weak_partial_order) lless_cong_l [trans]:
91   assumes xx': "x .= x'"
92     and xy: "x' \<sqsubset> y"
93     and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
94   shows "x \<sqsubset> y"
95   using assms unfolding lless_def by (auto intro: trans sym)
97 lemma (in weak_partial_order) lless_cong_r [trans]:
98   assumes xy: "x \<sqsubset> y"
99     and  yy': "y .= y'"
100     and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
101   shows "x \<sqsubset> y'"
102   using assms unfolding lless_def by (auto intro: trans sym)  (*slow*)
105 lemma (in weak_partial_order) lless_antisym:
106   assumes "a \<in> carrier L" "b \<in> carrier L"
107     and "a \<sqsubset> b" "b \<sqsubset> a"
108   shows "P"
109   using assms
110   by (elim weak_llessE) auto
112 lemma (in weak_partial_order) lless_trans [trans]:
113   assumes "a \<sqsubset> b" "b \<sqsubset> c"
114     and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"
115   shows "a \<sqsubset> c"
116   using assms unfolding lless_def by (blast dest: le_trans intro: sym)
118 lemma weak_partial_order_subset:
119   assumes "weak_partial_order L" "A \<subseteq> carrier L"
120   shows "weak_partial_order (L\<lparr> carrier := A \<rparr>)"
121 proof -
122   interpret L: weak_partial_order L
123     by (simp add: assms)
124   interpret equivalence "(L\<lparr> carrier := A \<rparr>)"
125     by (simp add: L.equivalence_axioms assms(2) equivalence_subset)
126   show ?thesis
127     apply (unfold_locales, simp_all)
128     using assms(2) apply auto
129     using assms(2) apply auto
130     apply (meson L.le_trans assms(2) contra_subsetD)
131     apply (meson L.le_cong assms(2) subsetCE)
132   done
133 qed
136 subsubsection \<open>Upper and lower bounds of a set\<close>
138 definition
139   Upper :: "[_, 'a set] => 'a set"
140   where "Upper L A = {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq>\<^bsub>L\<^esub> u)} \<inter> carrier L"
142 definition
143   Lower :: "[_, 'a set] => 'a set"
144   where "Lower L A = {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq>\<^bsub>L\<^esub> x)} \<inter> carrier L"
146 lemma Upper_closed [intro!, simp]:
147   "Upper L A \<subseteq> carrier L"
148   by (unfold Upper_def) clarify
150 lemma Upper_memD [dest]:
151   fixes L (structure)
152   shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u \<and> u \<in> carrier L"
153   by (unfold Upper_def) blast
155 lemma (in weak_partial_order) Upper_elemD [dest]:
156   "[| u .\<in> Upper L A; u \<in> carrier L; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
157   unfolding Upper_def elem_def
158   by (blast dest: sym)
160 lemma Upper_memI:
161   fixes L (structure)
162   shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"
163   by (unfold Upper_def) blast
165 lemma (in weak_partial_order) Upper_elemI:
166   "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x .\<in> Upper L A"
167   unfolding Upper_def by blast
169 lemma Upper_antimono:
170   "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
171   by (unfold Upper_def) blast
173 lemma (in weak_partial_order) Upper_is_closed [simp]:
174   "A \<subseteq> carrier L ==> is_closed (Upper L A)"
175   by (rule is_closedI) (blast intro: Upper_memI)+
177 lemma (in weak_partial_order) Upper_mem_cong:
178   assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
179     and aa': "a .= a'"
180     and aelem: "a \<in> Upper L A"
181   shows "a' \<in> Upper L A"
182 proof (rule Upper_memI[OF _ a'carr])
183   fix y
184   assume yA: "y \<in> A"
185   hence "y \<sqsubseteq> a" by (intro Upper_memD[OF aelem, THEN conjunct1] Acarr)
186   also note aa'
187   finally
188       show "y \<sqsubseteq> a'"
189       by (simp add: a'carr subsetD[OF Acarr yA] subsetD[OF Upper_closed aelem])
190 qed
192 lemma (in weak_partial_order) Upper_cong:
193   assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
194     and AA': "A {.=} A'"
195   shows "Upper L A = Upper L A'"
196 unfolding Upper_def
197 apply rule
198  apply (rule, clarsimp) defer 1
199  apply (rule, clarsimp) defer 1
200 proof -
201   fix x a'
202   assume carr: "x \<in> carrier L" "a' \<in> carrier L"
203     and a'A': "a' \<in> A'"
204   assume aLxCond[rule_format]: "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> a \<sqsubseteq> x"
206   from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
207   from this obtain a
208       where aA: "a \<in> A"
209       and a'a: "a' .= a"
210       by auto
211   note [simp] = subsetD[OF Acarr aA] carr
213   note a'a
214   also have "a \<sqsubseteq> x" by (simp add: aLxCond aA)
215   finally show "a' \<sqsubseteq> x" by simp
216 next
217   fix x a
218   assume carr: "x \<in> carrier L" "a \<in> carrier L"
219     and aA: "a \<in> A"
220   assume a'LxCond[rule_format]: "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> a' \<sqsubseteq> x"
222   from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
223   from this obtain a'
224       where a'A': "a' \<in> A'"
225       and aa': "a .= a'"
226       by auto
227   note [simp] = subsetD[OF A'carr a'A'] carr
229   note aa'
230   also have "a' \<sqsubseteq> x" by (simp add: a'LxCond a'A')
231   finally show "a \<sqsubseteq> x" by simp
232 qed
234 lemma Lower_closed [intro!, simp]:
235   "Lower L A \<subseteq> carrier L"
236   by (unfold Lower_def) clarify
238 lemma Lower_memD [dest]:
239   fixes L (structure)
240   shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x \<and> l \<in> carrier L"
241   by (unfold Lower_def) blast
243 lemma Lower_memI:
244   fixes L (structure)
245   shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A"
246   by (unfold Lower_def) blast
248 lemma Lower_antimono:
249   "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
250   by (unfold Lower_def) blast
252 lemma (in weak_partial_order) Lower_is_closed [simp]:
253   "A \<subseteq> carrier L \<Longrightarrow> is_closed (Lower L A)"
254   by (rule is_closedI) (blast intro: Lower_memI dest: sym)+
256 lemma (in weak_partial_order) Lower_mem_cong:
257   assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
258     and aa': "a .= a'"
259     and aelem: "a \<in> Lower L A"
260   shows "a' \<in> Lower L A"
261 using assms Lower_closed[of L A]
262 by (intro Lower_memI) (blast intro: le_cong_l[OF aa'[symmetric]])
264 lemma (in weak_partial_order) Lower_cong:
265   assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
266     and AA': "A {.=} A'"
267   shows "Lower L A = Lower L A'"
268 unfolding Lower_def
269 apply rule
270  apply clarsimp defer 1
271  apply clarsimp defer 1
272 proof -
273   fix x a'
274   assume carr: "x \<in> carrier L" "a' \<in> carrier L"
275     and a'A': "a' \<in> A'"
276   assume "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> x \<sqsubseteq> a"
277   hence aLxCond: "\<And>a. \<lbrakk>a \<in> A; a \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a" by fast
279   from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
280   from this obtain a
281       where aA: "a \<in> A"
282       and a'a: "a' .= a"
283       by auto
285   from aA and subsetD[OF Acarr aA]
286       have "x \<sqsubseteq> a" by (rule aLxCond)
287   also note a'a[symmetric]
288   finally
289       show "x \<sqsubseteq> a'" by (simp add: carr subsetD[OF Acarr aA])
290 next
291   fix x a
292   assume carr: "x \<in> carrier L" "a \<in> carrier L"
293     and aA: "a \<in> A"
294   assume "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> x \<sqsubseteq> a'"
295   hence a'LxCond: "\<And>a'. \<lbrakk>a' \<in> A'; a' \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a'" by fast+
297   from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
298   from this obtain a'
299       where a'A': "a' \<in> A'"
300       and aa': "a .= a'"
301       by auto
302   from a'A' and subsetD[OF A'carr a'A']
303       have "x \<sqsubseteq> a'" by (rule a'LxCond)
304   also note aa'[symmetric]
305   finally show "x \<sqsubseteq> a" by (simp add: carr subsetD[OF A'carr a'A'])
306 qed
308 text \<open>Jacobson: Theorem 8.1\<close>
310 lemma Lower_empty [simp]:
311   "Lower L {} = carrier L"
312   by (unfold Lower_def) simp
314 lemma Upper_empty [simp]:
315   "Upper L {} = carrier L"
316   by (unfold Upper_def) simp
319 subsubsection \<open>Least and greatest, as predicate\<close>
321 definition
322   least :: "[_, 'a, 'a set] => bool"
323   where "least L l A \<longleftrightarrow> A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq>\<^bsub>L\<^esub> x)"
325 definition
326   greatest :: "[_, 'a, 'a set] => bool"
327   where "greatest L g A \<longleftrightarrow> A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq>\<^bsub>L\<^esub> g)"
329 text (in weak_partial_order) \<open>Could weaken these to @{term "l \<in> carrier L \<and> l
330   .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}.\<close>
332 lemma least_closed [intro, simp]:
333   "least L l A ==> l \<in> carrier L"
334   by (unfold least_def) fast
336 lemma least_mem:
337   "least L l A ==> l \<in> A"
338   by (unfold least_def) fast
340 lemma (in weak_partial_order) weak_least_unique:
341   "[| least L x A; least L y A |] ==> x .= y"
342   by (unfold least_def) blast
344 lemma least_le:
345   fixes L (structure)
346   shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a"
347   by (unfold least_def) fast
349 lemma (in weak_partial_order) least_cong:
350   "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> least L x A = least L x' A"
351   by (unfold least_def) (auto dest: sym)
353 abbreviation is_lub :: "[_, 'a, 'a set] => bool"
354 where "is_lub L x A \<equiv> least L x (Upper L A)"
356 text (in weak_partial_order) \<open>@{const least} is not congruent in the second parameter for
357   @{term "A {.=} A'"}\<close>
359 lemma (in weak_partial_order) least_Upper_cong_l:
360   assumes "x .= x'"
361     and "x \<in> carrier L" "x' \<in> carrier L"
362     and "A \<subseteq> carrier L"
363   shows "least L x (Upper L A) = least L x' (Upper L A)"
364   apply (rule least_cong) using assms by auto
366 lemma (in weak_partial_order) least_Upper_cong_r:
367   assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L" (* unneccessary with current Upper? *)
368     and AA': "A {.=} A'"
369   shows "least L x (Upper L A) = least L x (Upper L A')"
370 apply (subgoal_tac "Upper L A = Upper L A'", simp)
371 by (rule Upper_cong) fact+
373 lemma least_UpperI:
374   fixes L (structure)
375   assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"
376     and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y"
377     and L: "A \<subseteq> carrier L"  "s \<in> carrier L"
378   shows "least L s (Upper L A)"
379 proof -
380   have "Upper L A \<subseteq> carrier L" by simp
381   moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def)
382   moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast
383   ultimately show ?thesis by (simp add: least_def)
384 qed
386 lemma least_Upper_above:
387   fixes L (structure)
388   shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
389   by (unfold least_def) blast
391 lemma greatest_closed [intro, simp]:
392   "greatest L l A ==> l \<in> carrier L"
393   by (unfold greatest_def) fast
395 lemma greatest_mem:
396   "greatest L l A ==> l \<in> A"
397   by (unfold greatest_def) fast
399 lemma (in weak_partial_order) weak_greatest_unique:
400   "[| greatest L x A; greatest L y A |] ==> x .= y"
401   by (unfold greatest_def) blast
403 lemma greatest_le:
404   fixes L (structure)
405   shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"
406   by (unfold greatest_def) fast
408 lemma (in weak_partial_order) greatest_cong:
409   "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==>
410   greatest L x A = greatest L x' A"
411   by (unfold greatest_def) (auto dest: sym)
413 abbreviation is_glb :: "[_, 'a, 'a set] => bool"
414 where "is_glb L x A \<equiv> greatest L x (Lower L A)"
416 text (in weak_partial_order) \<open>@{const greatest} is not congruent in the second parameter for
417   @{term "A {.=} A'"} \<close>
419 lemma (in weak_partial_order) greatest_Lower_cong_l:
420   assumes "x .= x'"
421     and "x \<in> carrier L" "x' \<in> carrier L"
422     and "A \<subseteq> carrier L" (* unneccessary with current Lower *)
423   shows "greatest L x (Lower L A) = greatest L x' (Lower L A)"
424   apply (rule greatest_cong) using assms by auto
426 lemma (in weak_partial_order) greatest_Lower_cong_r:
427   assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L"
428     and AA': "A {.=} A'"
429   shows "greatest L x (Lower L A) = greatest L x (Lower L A')"
430 apply (subgoal_tac "Lower L A = Lower L A'", simp)
431 by (rule Lower_cong) fact+
433 lemma greatest_LowerI:
434   fixes L (structure)
435   assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"
436     and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i"
437     and L: "A \<subseteq> carrier L"  "i \<in> carrier L"
438   shows "greatest L i (Lower L A)"
439 proof -
440   have "Lower L A \<subseteq> carrier L" by simp
441   moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def)
442   moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast
443   ultimately show ?thesis by (simp add: greatest_def)
444 qed
446 lemma greatest_Lower_below:
447   fixes L (structure)
448   shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
449   by (unfold greatest_def) blast
451 lemma Lower_dual [simp]:
452   "Lower (inv_gorder L) A = Upper L A"
453   by (simp add:Upper_def Lower_def)
455 lemma Upper_dual [simp]:
456   "Upper (inv_gorder L) A = Lower L A"
457   by (simp add:Upper_def Lower_def)
459 lemma least_dual [simp]:
460   "least (inv_gorder L) x A = greatest L x A"
461   by (simp add:least_def greatest_def)
463 lemma greatest_dual [simp]:
464   "greatest (inv_gorder L) x A = least L x A"
465   by (simp add:least_def greatest_def)
467 lemma (in weak_partial_order) dual_weak_order:
468   "weak_partial_order (inv_gorder L)"
469   apply (unfold_locales)
470   apply (simp_all)
471   apply (metis sym)
472   apply (metis trans)
473   apply (metis weak_le_antisym)
474   apply (metis le_trans)
475   apply (metis le_cong_l le_cong_r sym)
476 done
478 lemma dual_weak_order_iff:
479   "weak_partial_order (inv_gorder A) \<longleftrightarrow> weak_partial_order A"
480 proof
481   assume "weak_partial_order (inv_gorder A)"
482   then interpret dpo: weak_partial_order "inv_gorder A"
483   rewrites "carrier (inv_gorder A) = carrier A"
484   and   "le (inv_gorder A)      = (\<lambda> x y. le A y x)"
485   and   "eq (inv_gorder A)      = eq A"
486     by (simp_all)
487   show "weak_partial_order A"
488     by (unfold_locales, auto intro: dpo.sym dpo.trans dpo.le_trans)
489 next
490   assume "weak_partial_order A"
491   thus "weak_partial_order (inv_gorder A)"
492     by (metis weak_partial_order.dual_weak_order)
493 qed
496 subsubsection \<open>Intervals\<close>
498 definition
499   at_least_at_most :: "('a, 'c) gorder_scheme \<Rightarrow> 'a => 'a => 'a set" ("(1\<lbrace>_.._\<rbrace>\<index>)")
500   where "\<lbrace>l..u\<rbrace>\<^bsub>A\<^esub> = {x \<in> carrier A. l \<sqsubseteq>\<^bsub>A\<^esub> x \<and> x \<sqsubseteq>\<^bsub>A\<^esub> u}"
502 context weak_partial_order
503 begin
505   lemma at_least_at_most_upper [dest]:
506     "x \<in> \<lbrace>a..b\<rbrace> \<Longrightarrow> x \<sqsubseteq> b"
507     by (simp add: at_least_at_most_def)
509   lemma at_least_at_most_lower [dest]:
510     "x \<in> \<lbrace>a..b\<rbrace> \<Longrightarrow> a \<sqsubseteq> x"
511     by (simp add: at_least_at_most_def)
513   lemma at_least_at_most_closed: "\<lbrace>a..b\<rbrace> \<subseteq> carrier L"
514     by (auto simp add: at_least_at_most_def)
516   lemma at_least_at_most_member [intro]:
517     "\<lbrakk> x \<in> carrier L; a \<sqsubseteq> x; x \<sqsubseteq> b \<rbrakk> \<Longrightarrow> x \<in> \<lbrace>a..b\<rbrace>"
518     by (simp add: at_least_at_most_def)
520 end
523 subsubsection \<open>Isotone functions\<close>
525 definition isotone :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
526   where
527   "isotone A B f \<equiv>
528    weak_partial_order A \<and> weak_partial_order B \<and>
529    (\<forall>x\<in>carrier A. \<forall>y\<in>carrier A. x \<sqsubseteq>\<^bsub>A\<^esub> y \<longrightarrow> f x \<sqsubseteq>\<^bsub>B\<^esub> f y)"
531 lemma isotoneI [intro?]:
532   fixes f :: "'a \<Rightarrow> 'b"
533   assumes "weak_partial_order L1"
534           "weak_partial_order L2"
535           "(\<And>x y. \<lbrakk> x \<in> carrier L1; y \<in> carrier L1; x \<sqsubseteq>\<^bsub>L1\<^esub> y \<rbrakk>
536                    \<Longrightarrow> f x \<sqsubseteq>\<^bsub>L2\<^esub> f y)"
537   shows "isotone L1 L2 f"
538   using assms by (auto simp add:isotone_def)
540 abbreviation Monotone :: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" ("Mono\<index>")
541   where "Monotone L f \<equiv> isotone L L f"
543 lemma use_iso1:
544   "\<lbrakk>isotone A A f; x \<in> carrier A; y \<in> carrier A; x \<sqsubseteq>\<^bsub>A\<^esub> y\<rbrakk> \<Longrightarrow>
545    f x \<sqsubseteq>\<^bsub>A\<^esub> f y"
546   by (simp add: isotone_def)
548 lemma use_iso2:
549   "\<lbrakk>isotone A B f; x \<in> carrier A; y \<in> carrier A; x \<sqsubseteq>\<^bsub>A\<^esub> y\<rbrakk> \<Longrightarrow>
550    f x \<sqsubseteq>\<^bsub>B\<^esub> f y"
551   by (simp add: isotone_def)
553 lemma iso_compose:
554   "\<lbrakk>f \<in> carrier A \<rightarrow> carrier B; isotone A B f; g \<in> carrier B \<rightarrow> carrier C; isotone B C g\<rbrakk> \<Longrightarrow>
555    isotone A C (g \<circ> f)"
556   by (simp add: isotone_def, safe, metis Pi_iff)
558 lemma (in weak_partial_order) inv_isotone [simp]:
559   "isotone (inv_gorder A) (inv_gorder B) f = isotone A B f"
560   by (auto simp add:isotone_def dual_weak_order dual_weak_order_iff)
563 subsubsection \<open>Idempotent functions\<close>
565 definition idempotent ::
566   "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" ("Idem\<index>") where
567   "idempotent L f \<equiv> \<forall>x\<in>carrier L. f (f x) .=\<^bsub>L\<^esub> f x"
569 lemma (in weak_partial_order) idempotent:
570   "\<lbrakk> Idem f; x \<in> carrier L \<rbrakk> \<Longrightarrow> f (f x) .= f x"
571   by (auto simp add: idempotent_def)
574 subsubsection \<open>Order embeddings\<close>
576 definition order_emb :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
577   where
578   "order_emb A B f \<equiv> weak_partial_order A
579                    \<and> weak_partial_order B
580                    \<and> (\<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f x \<sqsubseteq>\<^bsub>B\<^esub> f y \<longleftrightarrow> x \<sqsubseteq>\<^bsub>A\<^esub> y )"
582 lemma order_emb_isotone: "order_emb A B f \<Longrightarrow> isotone A B f"
583   by (auto simp add: isotone_def order_emb_def)
586 subsubsection \<open>Commuting functions\<close>
588 definition commuting :: "('a, 'c) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" where
589 "commuting A f g = (\<forall>x\<in>carrier A. (f \<circ> g) x .=\<^bsub>A\<^esub> (g \<circ> f) x)"
591 subsection \<open>Partial orders where \<open>eq\<close> is the Equality\<close>
593 locale partial_order = weak_partial_order +
594   assumes eq_is_equal: "op .= = op ="
595 begin
597 declare weak_le_antisym [rule del]
599 lemma le_antisym [intro]:
600   "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y"
601   using weak_le_antisym unfolding eq_is_equal .
603 lemma lless_eq:
604   "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y & x \<noteq> y"
605   unfolding lless_def by (simp add: eq_is_equal)
607 lemma set_eq_is_eq: "A {.=} B \<longleftrightarrow> A = B"
608   by (auto simp add: set_eq_def elem_def eq_is_equal)
610 end
612 lemma (in partial_order) dual_order:
613   "partial_order (inv_gorder L)"
614 proof -
615   interpret dwo: weak_partial_order "inv_gorder L"
616     by (metis dual_weak_order)
617   show ?thesis
618     by (unfold_locales, simp add:eq_is_equal)
619 qed
621 lemma dual_order_iff:
622   "partial_order (inv_gorder A) \<longleftrightarrow> partial_order A"
623 proof
624   assume assm:"partial_order (inv_gorder A)"
625   then interpret po: partial_order "inv_gorder A"
626   rewrites "carrier (inv_gorder A) = carrier A"
627   and   "le (inv_gorder A)      = (\<lambda> x y. le A y x)"
628   and   "eq (inv_gorder A)      = eq A"
629     by (simp_all)
630   show "partial_order A"
631     apply (unfold_locales, simp_all)
632     apply (metis po.sym, metis po.trans)
633     apply (metis po.weak_le_antisym, metis po.le_trans)
634     apply (metis (full_types) po.eq_is_equal, metis po.eq_is_equal)
635   done
636 next
637   assume "partial_order A"
638   thus "partial_order (inv_gorder A)"
639     by (metis partial_order.dual_order)
640 qed
642 text \<open>Least and greatest, as predicate\<close>
644 lemma (in partial_order) least_unique:
645   "[| least L x A; least L y A |] ==> x = y"
646   using weak_least_unique unfolding eq_is_equal .
648 lemma (in partial_order) greatest_unique:
649   "[| greatest L x A; greatest L y A |] ==> x = y"
650   using weak_greatest_unique unfolding eq_is_equal .
653 subsection \<open>Bounded Orders\<close>
655 definition
656   top :: "_ => 'a" ("\<top>\<index>") where
657   "\<top>\<^bsub>L\<^esub> = (SOME x. greatest L x (carrier L))"
659 definition
660   bottom :: "_ => 'a" ("\<bottom>\<index>") where
661   "\<bottom>\<^bsub>L\<^esub> = (SOME x. least L x (carrier L))"
663 locale weak_partial_order_bottom = weak_partial_order L for L (structure) +
664   assumes bottom_exists: "\<exists> x. least L x (carrier L)"
665 begin
667 lemma bottom_least: "least L \<bottom> (carrier L)"
668 proof -
669   obtain x where "least L x (carrier L)"
670     by (metis bottom_exists)
672   thus ?thesis
673     by (auto intro:someI2 simp add: bottom_def)
674 qed
676 lemma bottom_closed [simp, intro]:
677   "\<bottom> \<in> carrier L"
678   by (metis bottom_least least_mem)
680 lemma bottom_lower [simp, intro]:
681   "x \<in> carrier L \<Longrightarrow> \<bottom> \<sqsubseteq> x"
682   by (metis bottom_least least_le)
684 end
686 locale weak_partial_order_top = weak_partial_order L for L (structure) +
687   assumes top_exists: "\<exists> x. greatest L x (carrier L)"
688 begin
690 lemma top_greatest: "greatest L \<top> (carrier L)"
691 proof -
692   obtain x where "greatest L x (carrier L)"
693     by (metis top_exists)
695   thus ?thesis
696     by (auto intro:someI2 simp add: top_def)
697 qed
699 lemma top_closed [simp, intro]:
700   "\<top> \<in> carrier L"
701   by (metis greatest_mem top_greatest)
703 lemma top_higher [simp, intro]:
704   "x \<in> carrier L \<Longrightarrow> x \<sqsubseteq> \<top>"
705   by (metis greatest_le top_greatest)
707 end
710 subsection \<open>Total Orders\<close>
712 locale weak_total_order = weak_partial_order +
713   assumes total: "\<lbrakk> x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
715 text \<open>Introduction rule: the usual definition of total order\<close>
717 lemma (in weak_partial_order) weak_total_orderI:
718   assumes total: "!!x y. \<lbrakk> x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
719   shows "weak_total_order L"
720   by unfold_locales (rule total)
723 subsection \<open>Total orders where \<open>eq\<close> is the Equality\<close>
725 locale total_order = partial_order +
726   assumes total_order_total: "\<lbrakk> x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
728 sublocale total_order < weak?: weak_total_order
729   by unfold_locales (rule total_order_total)
731 text \<open>Introduction rule: the usual definition of total order\<close>
733 lemma (in partial_order) total_orderI:
734   assumes total: "!!x y. \<lbrakk> x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
735   shows "total_order L"
736   by unfold_locales (rule total)
738 end