src/HOL/Algebra/Order.thy
 author paulson Sat Jun 30 15:44:04 2018 +0100 (12 months ago) changeset 68551 b680e74eb6f2 parent 68073 fad29d2a17a5 child 69597 ff784d5a5bfb permissions -rw-r--r--
More on Algebra by Paulo and Martin
```     1 (*  Title:      HOL/Algebra/Order.thy
```
```     2     Author:     Clemens Ballarin, started 7 November 2003
```
```     3     Copyright:  Clemens Ballarin
```
```     4
```
```     5 Most congruence rules by Stephan Hohe.
```
```     6 With additional contributions from Alasdair Armstrong and Simon Foster.
```
```     7 *)
```
```     8
```
```     9 theory Order
```
```    10   imports
```
```    11     Congruence
```
```    12 begin
```
```    13
```
```    14 section \<open>Orders\<close>
```
```    15
```
```    16 subsection \<open>Partial Orders\<close>
```
```    17
```
```    18 record 'a gorder = "'a eq_object" +
```
```    19   le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
```
```    20
```
```    21 abbreviation inv_gorder :: "_ \<Rightarrow> 'a gorder" where
```
```    22   "inv_gorder L \<equiv>
```
```    23    \<lparr> carrier = carrier L,
```
```    24      eq = (.=\<^bsub>L\<^esub>),
```
```    25      le = (\<lambda> x y. y \<sqsubseteq>\<^bsub>L \<^esub>x) \<rparr>"
```
```    26
```
```    27 lemma inv_gorder_inv:
```
```    28   "inv_gorder (inv_gorder L) = L"
```
```    29   by simp
```
```    30
```
```    31 locale weak_partial_order = equivalence L for L (structure) +
```
```    32   assumes le_refl [intro, simp]:
```
```    33       "x \<in> carrier L \<Longrightarrow> x \<sqsubseteq> x"
```
```    34     and weak_le_antisym [intro]:
```
```    35       "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L\<rbrakk> \<Longrightarrow> x .= y"
```
```    36     and le_trans [trans]:
```
```    37       "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
```
```    38     and le_cong:
```
```    39       "\<lbrakk>x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L\<rbrakk> \<Longrightarrow>
```
```    40       x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"
```
```    41
```
```    42 definition
```
```    43   lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
```
```    44   where "x \<sqsubset>\<^bsub>L\<^esub> y \<longleftrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> y \<and> x .\<noteq>\<^bsub>L\<^esub> y"
```
```    45
```
```    46 subsubsection \<open>The order relation\<close>
```
```    47
```
```    48 context weak_partial_order
```
```    49 begin
```
```    50
```
```    51 lemma le_cong_l [intro, trans]:
```
```    52   "\<lbrakk>x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
```
```    53   by (auto intro: le_cong [THEN iffD2])
```
```    54
```
```    55 lemma le_cong_r [intro, trans]:
```
```    56   "\<lbrakk>x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
```
```    57   by (auto intro: le_cong [THEN iffD1])
```
```    58
```
```    59 lemma weak_refl [intro, simp]: "\<lbrakk>x .= y; x \<in> carrier L; y \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"
```
```    60   by (simp add: le_cong_l)
```
```    61
```
```    62 end
```
```    63
```
```    64 lemma weak_llessI:
```
```    65   fixes R (structure)
```
```    66   assumes "x \<sqsubseteq> y" and "\<not>(x .= y)"
```
```    67   shows "x \<sqsubset> y"
```
```    68   using assms unfolding lless_def by simp
```
```    69
```
```    70 lemma lless_imp_le:
```
```    71   fixes R (structure)
```
```    72   assumes "x \<sqsubset> y"
```
```    73   shows "x \<sqsubseteq> y"
```
```    74   using assms unfolding lless_def by simp
```
```    75
```
```    76 lemma weak_lless_imp_not_eq:
```
```    77   fixes R (structure)
```
```    78   assumes "x \<sqsubset> y"
```
```    79   shows "\<not> (x .= y)"
```
```    80   using assms unfolding lless_def by simp
```
```    81
```
```    82 lemma weak_llessE:
```
```    83   fixes R (structure)
```
```    84   assumes p: "x \<sqsubset> y" and e: "\<lbrakk>x \<sqsubseteq> y; \<not> (x .= y)\<rbrakk> \<Longrightarrow> P"
```
```    85   shows "P"
```
```    86   using p by (blast dest: lless_imp_le weak_lless_imp_not_eq e)
```
```    87
```
```    88 lemma (in weak_partial_order) lless_cong_l [trans]:
```
```    89   assumes xx': "x .= x'"
```
```    90     and xy: "x' \<sqsubset> y"
```
```    91     and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
```
```    92   shows "x \<sqsubset> y"
```
```    93   using assms unfolding lless_def by (auto intro: trans sym)
```
```    94
```
```    95 lemma (in weak_partial_order) lless_cong_r [trans]:
```
```    96   assumes xy: "x \<sqsubset> y"
```
```    97     and  yy': "y .= y'"
```
```    98     and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
```
```    99   shows "x \<sqsubset> y'"
```
```   100   using assms unfolding lless_def by (auto intro: trans sym)  (*slow*)
```
```   101
```
```   102
```
```   103 lemma (in weak_partial_order) lless_antisym:
```
```   104   assumes "a \<in> carrier L" "b \<in> carrier L"
```
```   105     and "a \<sqsubset> b" "b \<sqsubset> a"
```
```   106   shows "P"
```
```   107   using assms
```
```   108   by (elim weak_llessE) auto
```
```   109
```
```   110 lemma (in weak_partial_order) lless_trans [trans]:
```
```   111   assumes "a \<sqsubset> b" "b \<sqsubset> c"
```
```   112     and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"
```
```   113   shows "a \<sqsubset> c"
```
```   114   using assms unfolding lless_def by (blast dest: le_trans intro: sym)
```
```   115
```
```   116 lemma weak_partial_order_subset:
```
```   117   assumes "weak_partial_order L" "A \<subseteq> carrier L"
```
```   118   shows "weak_partial_order (L\<lparr> carrier := A \<rparr>)"
```
```   119 proof -
```
```   120   interpret L: weak_partial_order L
```
```   121     by (simp add: assms)
```
```   122   interpret equivalence "(L\<lparr> carrier := A \<rparr>)"
```
```   123     by (simp add: L.equivalence_axioms assms(2) equivalence_subset)
```
```   124   show ?thesis
```
```   125     apply (unfold_locales, simp_all)
```
```   126     using assms(2) apply auto[1]
```
```   127     using assms(2) apply auto[1]
```
```   128     apply (meson L.le_trans assms(2) contra_subsetD)
```
```   129     apply (meson L.le_cong assms(2) subsetCE)
```
```   130   done
```
```   131 qed
```
```   132
```
```   133
```
```   134 subsubsection \<open>Upper and lower bounds of a set\<close>
```
```   135
```
```   136 definition
```
```   137   Upper :: "[_, 'a set] => 'a set"
```
```   138   where "Upper L A = {u. (\<forall>x. x \<in> A \<inter> carrier L \<longrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> u)} \<inter> carrier L"
```
```   139
```
```   140 definition
```
```   141   Lower :: "[_, 'a set] => 'a set"
```
```   142   where "Lower L A = {l. (\<forall>x. x \<in> A \<inter> carrier L \<longrightarrow> l \<sqsubseteq>\<^bsub>L\<^esub> x)} \<inter> carrier L"
```
```   143
```
```   144 lemma Lower_dual [simp]:
```
```   145   "Lower (inv_gorder L) A = Upper L A"
```
```   146   by (simp add:Upper_def Lower_def)
```
```   147
```
```   148 lemma Upper_dual [simp]:
```
```   149   "Upper (inv_gorder L) A = Lower L A"
```
```   150   by (simp add:Upper_def Lower_def)
```
```   151
```
```   152 lemma (in weak_partial_order) equivalence_dual: "equivalence (inv_gorder L)"
```
```   153   by (rule equivalence.intro) (auto simp: intro: sym trans)
```
```   154
```
```   155 lemma  (in weak_partial_order) dual_weak_order: "weak_partial_order (inv_gorder L)"
```
```   156   by intro_locales (auto simp add: weak_partial_order_axioms_def le_cong intro: equivalence_dual le_trans)
```
```   157
```
```   158 lemma (in weak_partial_order) dual_eq_iff [simp]: "A {.=}\<^bsub>inv_gorder L\<^esub> A' \<longleftrightarrow> A {.=} A'"
```
```   159   by (auto simp: set_eq_def elem_def)
```
```   160
```
```   161 lemma dual_weak_order_iff:
```
```   162   "weak_partial_order (inv_gorder A) \<longleftrightarrow> weak_partial_order A"
```
```   163 proof
```
```   164   assume "weak_partial_order (inv_gorder A)"
```
```   165   then interpret dpo: weak_partial_order "inv_gorder A"
```
```   166   rewrites "carrier (inv_gorder A) = carrier A"
```
```   167   and   "le (inv_gorder A)      = (\<lambda> x y. le A y x)"
```
```   168   and   "eq (inv_gorder A)      = eq A"
```
```   169     by (simp_all)
```
```   170   show "weak_partial_order A"
```
```   171     by (unfold_locales, auto intro: dpo.sym dpo.trans dpo.le_trans)
```
```   172 next
```
```   173   assume "weak_partial_order A"
```
```   174   thus "weak_partial_order (inv_gorder A)"
```
```   175     by (metis weak_partial_order.dual_weak_order)
```
```   176 qed
```
```   177
```
```   178 lemma Upper_closed [iff]:
```
```   179   "Upper L A \<subseteq> carrier L"
```
```   180   by (unfold Upper_def) clarify
```
```   181
```
```   182 lemma Upper_memD [dest]:
```
```   183   fixes L (structure)
```
```   184   shows "\<lbrakk>u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u \<and> u \<in> carrier L"
```
```   185   by (unfold Upper_def) blast
```
```   186
```
```   187 lemma (in weak_partial_order) Upper_elemD [dest]:
```
```   188   "\<lbrakk>u .\<in> Upper L A; u \<in> carrier L; x \<in> A; A \<subseteq> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u"
```
```   189   unfolding Upper_def elem_def
```
```   190   by (blast dest: sym)
```
```   191
```
```   192 lemma Upper_memI:
```
```   193   fixes L (structure)
```
```   194   shows "\<lbrakk>!! y. y \<in> A \<Longrightarrow> y \<sqsubseteq> x; x \<in> carrier L\<rbrakk> \<Longrightarrow> x \<in> Upper L A"
```
```   195   by (unfold Upper_def) blast
```
```   196
```
```   197 lemma (in weak_partial_order) Upper_elemI:
```
```   198   "\<lbrakk>!! y. y \<in> A \<Longrightarrow> y \<sqsubseteq> x; x \<in> carrier L\<rbrakk> \<Longrightarrow> x .\<in> Upper L A"
```
```   199   unfolding Upper_def by blast
```
```   200
```
```   201 lemma Upper_antimono:
```
```   202   "A \<subseteq> B \<Longrightarrow> Upper L B \<subseteq> Upper L A"
```
```   203   by (unfold Upper_def) blast
```
```   204
```
```   205 lemma (in weak_partial_order) Upper_is_closed [simp]:
```
```   206   "A \<subseteq> carrier L \<Longrightarrow> is_closed (Upper L A)"
```
```   207   by (rule is_closedI) (blast intro: Upper_memI)+
```
```   208
```
```   209 lemma (in weak_partial_order) Upper_mem_cong:
```
```   210   assumes  "a' \<in> carrier L" "A \<subseteq> carrier L" "a .= a'" "a \<in> Upper L A"
```
```   211   shows "a' \<in> Upper L A"
```
```   212   by (metis assms Upper_closed Upper_is_closed closure_of_eq complete_classes)
```
```   213
```
```   214 lemma (in weak_partial_order) Upper_semi_cong:
```
```   215   assumes "A \<subseteq> carrier L" "A {.=} A'"
```
```   216   shows "Upper L A \<subseteq> Upper L A'"
```
```   217   unfolding Upper_def
```
```   218    by clarsimp (meson assms equivalence.refl equivalence_axioms le_cong set_eqD2 subset_eq)
```
```   219
```
```   220 lemma (in weak_partial_order) Upper_cong:
```
```   221   assumes "A \<subseteq> carrier L" "A' \<subseteq> carrier L" "A {.=} A'"
```
```   222   shows "Upper L A = Upper L A'"
```
```   223   using assms by (simp add: Upper_semi_cong set_eq_sym subset_antisym)
```
```   224
```
```   225 lemma Lower_closed [intro!, simp]:
```
```   226   "Lower L A \<subseteq> carrier L"
```
```   227   by (unfold Lower_def) clarify
```
```   228
```
```   229 lemma Lower_memD [dest]:
```
```   230   fixes L (structure)
```
```   231   shows "\<lbrakk>l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L\<rbrakk> \<Longrightarrow> l \<sqsubseteq> x \<and> l \<in> carrier L"
```
```   232   by (unfold Lower_def) blast
```
```   233
```
```   234 lemma Lower_memI:
```
```   235   fixes L (structure)
```
```   236   shows "\<lbrakk>!! y. y \<in> A \<Longrightarrow> x \<sqsubseteq> y; x \<in> carrier L\<rbrakk> \<Longrightarrow> x \<in> Lower L A"
```
```   237   by (unfold Lower_def) blast
```
```   238
```
```   239 lemma Lower_antimono:
```
```   240   "A \<subseteq> B \<Longrightarrow> Lower L B \<subseteq> Lower L A"
```
```   241   by (unfold Lower_def) blast
```
```   242
```
```   243 lemma (in weak_partial_order) Lower_is_closed [simp]:
```
```   244   "A \<subseteq> carrier L \<Longrightarrow> is_closed (Lower L A)"
```
```   245   by (rule is_closedI) (blast intro: Lower_memI dest: sym)+
```
```   246
```
```   247 lemma (in weak_partial_order) Lower_mem_cong:
```
```   248   assumes "a' \<in> carrier L"  "A \<subseteq> carrier L" "a .= a'" "a \<in> Lower L A"
```
```   249   shows "a' \<in> Lower L A"
```
```   250   by (meson assms Lower_closed Lower_is_closed is_closed_eq subsetCE)
```
```   251
```
```   252 lemma (in weak_partial_order) Lower_cong:
```
```   253   assumes "A \<subseteq> carrier L" "A' \<subseteq> carrier L" "A {.=} A'"
```
```   254   shows "Lower L A = Lower L A'"
```
```   255   unfolding Upper_dual [symmetric]
```
```   256   by (rule weak_partial_order.Upper_cong [OF dual_weak_order]) (simp_all add: assms)
```
```   257
```
```   258 text \<open>Jacobson: Theorem 8.1\<close>
```
```   259
```
```   260 lemma Lower_empty [simp]:
```
```   261   "Lower L {} = carrier L"
```
```   262   by (unfold Lower_def) simp
```
```   263
```
```   264 lemma Upper_empty [simp]:
```
```   265   "Upper L {} = carrier L"
```
```   266   by (unfold Upper_def) simp
```
```   267
```
```   268
```
```   269 subsubsection \<open>Least and greatest, as predicate\<close>
```
```   270
```
```   271 definition
```
```   272   least :: "[_, 'a, 'a set] => bool"
```
```   273   where "least L l A \<longleftrightarrow> A \<subseteq> carrier L \<and> l \<in> A \<and> (\<forall>x\<in>A. l \<sqsubseteq>\<^bsub>L\<^esub> x)"
```
```   274
```
```   275 definition
```
```   276   greatest :: "[_, 'a, 'a set] => bool"
```
```   277   where "greatest L g A \<longleftrightarrow> A \<subseteq> carrier L \<and> g \<in> A \<and> (\<forall>x\<in>A. x \<sqsubseteq>\<^bsub>L\<^esub> g)"
```
```   278
```
```   279 text (in weak_partial_order) \<open>Could weaken these to @{term "l \<in> carrier L \<and> l .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}.\<close>
```
```   280
```
```   281 lemma least_dual [simp]:
```
```   282   "least (inv_gorder L) x A = greatest L x A"
```
```   283   by (simp add:least_def greatest_def)
```
```   284
```
```   285 lemma greatest_dual [simp]:
```
```   286   "greatest (inv_gorder L) x A = least L x A"
```
```   287   by (simp add:least_def greatest_def)
```
```   288
```
```   289 lemma least_closed [intro, simp]:
```
```   290   "least L l A \<Longrightarrow> l \<in> carrier L"
```
```   291   by (unfold least_def) fast
```
```   292
```
```   293 lemma least_mem:
```
```   294   "least L l A \<Longrightarrow> l \<in> A"
```
```   295   by (unfold least_def) fast
```
```   296
```
```   297 lemma (in weak_partial_order) weak_least_unique:
```
```   298   "\<lbrakk>least L x A; least L y A\<rbrakk> \<Longrightarrow> x .= y"
```
```   299   by (unfold least_def) blast
```
```   300
```
```   301 lemma least_le:
```
```   302   fixes L (structure)
```
```   303   shows "\<lbrakk>least L x A; a \<in> A\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a"
```
```   304   by (unfold least_def) fast
```
```   305
```
```   306 lemma (in weak_partial_order) least_cong:
```
```   307   "\<lbrakk>x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A\<rbrakk> \<Longrightarrow> least L x A = least L x' A"
```
```   308   unfolding least_def
```
```   309   by (meson is_closed_eq is_closed_eq_rev le_cong local.refl subset_iff)
```
```   310
```
```   311 abbreviation is_lub :: "[_, 'a, 'a set] => bool"
```
```   312 where "is_lub L x A \<equiv> least L x (Upper L A)"
```
```   313
```
```   314 text (in weak_partial_order) \<open>@{const least} is not congruent in the second parameter for
```
```   315   @{term "A {.=} A'"}\<close>
```
```   316
```
```   317 lemma (in weak_partial_order) least_Upper_cong_l:
```
```   318   assumes "x .= x'"
```
```   319     and "x \<in> carrier L" "x' \<in> carrier L"
```
```   320     and "A \<subseteq> carrier L"
```
```   321   shows "least L x (Upper L A) = least L x' (Upper L A)"
```
```   322   apply (rule least_cong) using assms by auto
```
```   323
```
```   324 lemma (in weak_partial_order) least_Upper_cong_r:
```
```   325   assumes "A \<subseteq> carrier L" "A' \<subseteq> carrier L" "A {.=} A'"
```
```   326   shows "least L x (Upper L A) = least L x (Upper L A')"
```
```   327   using Upper_cong assms by auto
```
```   328
```
```   329 lemma least_UpperI:
```
```   330   fixes L (structure)
```
```   331   assumes above: "!! x. x \<in> A \<Longrightarrow> x \<sqsubseteq> s"
```
```   332     and below: "!! y. y \<in> Upper L A \<Longrightarrow> s \<sqsubseteq> y"
```
```   333     and L: "A \<subseteq> carrier L"  "s \<in> carrier L"
```
```   334   shows "least L s (Upper L A)"
```
```   335 proof -
```
```   336   have "Upper L A \<subseteq> carrier L" by simp
```
```   337   moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def)
```
```   338   moreover from below have "\<forall>x \<in> Upper L A. s \<sqsubseteq> x" by fast
```
```   339   ultimately show ?thesis by (simp add: least_def)
```
```   340 qed
```
```   341
```
```   342 lemma least_Upper_above:
```
```   343   fixes L (structure)
```
```   344   shows "\<lbrakk>least L s (Upper L A); x \<in> A; A \<subseteq> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> s"
```
```   345   by (unfold least_def) blast
```
```   346
```
```   347 lemma greatest_closed [intro, simp]:
```
```   348   "greatest L l A \<Longrightarrow> l \<in> carrier L"
```
```   349   by (unfold greatest_def) fast
```
```   350
```
```   351 lemma greatest_mem:
```
```   352   "greatest L l A \<Longrightarrow> l \<in> A"
```
```   353   by (unfold greatest_def) fast
```
```   354
```
```   355 lemma (in weak_partial_order) weak_greatest_unique:
```
```   356   "\<lbrakk>greatest L x A; greatest L y A\<rbrakk> \<Longrightarrow> x .= y"
```
```   357   by (unfold greatest_def) blast
```
```   358
```
```   359 lemma greatest_le:
```
```   360   fixes L (structure)
```
```   361   shows "\<lbrakk>greatest L x A; a \<in> A\<rbrakk> \<Longrightarrow> a \<sqsubseteq> x"
```
```   362   by (unfold greatest_def) fast
```
```   363
```
```   364 lemma (in weak_partial_order) greatest_cong:
```
```   365   "\<lbrakk>x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A\<rbrakk> \<Longrightarrow>
```
```   366   greatest L x A = greatest L x' A"
```
```   367   unfolding greatest_def
```
```   368   by (meson is_closed_eq_rev le_cong_r local.sym subset_eq)
```
```   369
```
```   370 abbreviation is_glb :: "[_, 'a, 'a set] => bool"
```
```   371 where "is_glb L x A \<equiv> greatest L x (Lower L A)"
```
```   372
```
```   373 text (in weak_partial_order) \<open>@{const greatest} is not congruent in the second parameter for
```
```   374   @{term "A {.=} A'"} \<close>
```
```   375
```
```   376 lemma (in weak_partial_order) greatest_Lower_cong_l:
```
```   377   assumes "x .= x'"
```
```   378     and "x \<in> carrier L" "x' \<in> carrier L"
```
```   379   shows "greatest L x (Lower L A) = greatest L x' (Lower L A)"
```
```   380 proof -
```
```   381   have "\<forall>A. is_closed (Lower L (A \<inter> carrier L))"
```
```   382     by simp
```
```   383   then show ?thesis
```
```   384     by (simp add: Lower_def assms greatest_cong)
```
```   385 qed
```
```   386
```
```   387 lemma (in weak_partial_order) greatest_Lower_cong_r:
```
```   388   assumes "A \<subseteq> carrier L" "A' \<subseteq> carrier L" "A {.=} A'"
```
```   389   shows "greatest L x (Lower L A) = greatest L x (Lower L A')"
```
```   390   using Lower_cong assms by auto
```
```   391
```
```   392 lemma greatest_LowerI:
```
```   393   fixes L (structure)
```
```   394   assumes below: "!! x. x \<in> A \<Longrightarrow> i \<sqsubseteq> x"
```
```   395     and above: "!! y. y \<in> Lower L A \<Longrightarrow> y \<sqsubseteq> i"
```
```   396     and L: "A \<subseteq> carrier L"  "i \<in> carrier L"
```
```   397   shows "greatest L i (Lower L A)"
```
```   398 proof -
```
```   399   have "Lower L A \<subseteq> carrier L" by simp
```
```   400   moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def)
```
```   401   moreover from above have "\<forall>x \<in> Lower L A. x \<sqsubseteq> i" by fast
```
```   402   ultimately show ?thesis by (simp add: greatest_def)
```
```   403 qed
```
```   404
```
```   405 lemma greatest_Lower_below:
```
```   406   fixes L (structure)
```
```   407   shows "\<lbrakk>greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L\<rbrakk> \<Longrightarrow> i \<sqsubseteq> x"
```
```   408   by (unfold greatest_def) blast
```
```   409
```
```   410
```
```   411 subsubsection \<open>Intervals\<close>
```
```   412
```
```   413 definition
```
```   414   at_least_at_most :: "('a, 'c) gorder_scheme \<Rightarrow> 'a => 'a => 'a set" ("(1\<lbrace>_.._\<rbrace>\<index>)")
```
```   415   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}"
```
```   416
```
```   417 context weak_partial_order
```
```   418 begin
```
```   419
```
```   420   lemma at_least_at_most_upper [dest]:
```
```   421     "x \<in> \<lbrace>a..b\<rbrace> \<Longrightarrow> x \<sqsubseteq> b"
```
```   422     by (simp add: at_least_at_most_def)
```
```   423
```
```   424   lemma at_least_at_most_lower [dest]:
```
```   425     "x \<in> \<lbrace>a..b\<rbrace> \<Longrightarrow> a \<sqsubseteq> x"
```
```   426     by (simp add: at_least_at_most_def)
```
```   427
```
```   428   lemma at_least_at_most_closed: "\<lbrace>a..b\<rbrace> \<subseteq> carrier L"
```
```   429     by (auto simp add: at_least_at_most_def)
```
```   430
```
```   431   lemma at_least_at_most_member [intro]:
```
```   432     "\<lbrakk>x \<in> carrier L; a \<sqsubseteq> x; x \<sqsubseteq> b\<rbrakk> \<Longrightarrow> x \<in> \<lbrace>a..b\<rbrace>"
```
```   433     by (simp add: at_least_at_most_def)
```
```   434
```
```   435 end
```
```   436
```
```   437
```
```   438 subsubsection \<open>Isotone functions\<close>
```
```   439
```
```   440 definition isotone :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
```
```   441   where
```
```   442   "isotone A B f \<equiv>
```
```   443    weak_partial_order A \<and> weak_partial_order B \<and>
```
```   444    (\<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)"
```
```   445
```
```   446 lemma isotoneI [intro?]:
```
```   447   fixes f :: "'a \<Rightarrow> 'b"
```
```   448   assumes "weak_partial_order L1"
```
```   449           "weak_partial_order L2"
```
```   450           "(\<And>x y. \<lbrakk>x \<in> carrier L1; y \<in> carrier L1; x \<sqsubseteq>\<^bsub>L1\<^esub> y\<rbrakk>
```
```   451                    \<Longrightarrow> f x \<sqsubseteq>\<^bsub>L2\<^esub> f y)"
```
```   452   shows "isotone L1 L2 f"
```
```   453   using assms by (auto simp add:isotone_def)
```
```   454
```
```   455 abbreviation Monotone :: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" ("Mono\<index>")
```
```   456   where "Monotone L f \<equiv> isotone L L f"
```
```   457
```
```   458 lemma use_iso1:
```
```   459   "\<lbrakk>isotone A A f; x \<in> carrier A; y \<in> carrier A; x \<sqsubseteq>\<^bsub>A\<^esub> y\<rbrakk> \<Longrightarrow>
```
```   460    f x \<sqsubseteq>\<^bsub>A\<^esub> f y"
```
```   461   by (simp add: isotone_def)
```
```   462
```
```   463 lemma use_iso2:
```
```   464   "\<lbrakk>isotone A B f; x \<in> carrier A; y \<in> carrier A; x \<sqsubseteq>\<^bsub>A\<^esub> y\<rbrakk> \<Longrightarrow>
```
```   465    f x \<sqsubseteq>\<^bsub>B\<^esub> f y"
```
```   466   by (simp add: isotone_def)
```
```   467
```
```   468 lemma iso_compose:
```
```   469   "\<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>
```
```   470    isotone A C (g \<circ> f)"
```
```   471   by (simp add: isotone_def, safe, metis Pi_iff)
```
```   472
```
```   473 lemma (in weak_partial_order) inv_isotone [simp]:
```
```   474   "isotone (inv_gorder A) (inv_gorder B) f = isotone A B f"
```
```   475   by (auto simp add:isotone_def dual_weak_order dual_weak_order_iff)
```
```   476
```
```   477
```
```   478 subsubsection \<open>Idempotent functions\<close>
```
```   479
```
```   480 definition idempotent ::
```
```   481   "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" ("Idem\<index>") where
```
```   482   "idempotent L f \<equiv> \<forall>x\<in>carrier L. f (f x) .=\<^bsub>L\<^esub> f x"
```
```   483
```
```   484 lemma (in weak_partial_order) idempotent:
```
```   485   "\<lbrakk>Idem f; x \<in> carrier L\<rbrakk> \<Longrightarrow> f (f x) .= f x"
```
```   486   by (auto simp add: idempotent_def)
```
```   487
```
```   488
```
```   489 subsubsection \<open>Order embeddings\<close>
```
```   490
```
```   491 definition order_emb :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
```
```   492   where
```
```   493   "order_emb A B f \<equiv> weak_partial_order A
```
```   494                    \<and> weak_partial_order B
```
```   495                    \<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 )"
```
```   496
```
```   497 lemma order_emb_isotone: "order_emb A B f \<Longrightarrow> isotone A B f"
```
```   498   by (auto simp add: isotone_def order_emb_def)
```
```   499
```
```   500
```
```   501 subsubsection \<open>Commuting functions\<close>
```
```   502
```
```   503 definition commuting :: "('a, 'c) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" where
```
```   504 "commuting A f g = (\<forall>x\<in>carrier A. (f \<circ> g) x .=\<^bsub>A\<^esub> (g \<circ> f) x)"
```
```   505
```
```   506 subsection \<open>Partial orders where \<open>eq\<close> is the Equality\<close>
```
```   507
```
```   508 locale partial_order = weak_partial_order +
```
```   509   assumes eq_is_equal: "(.=) = (=)"
```
```   510 begin
```
```   511
```
```   512 declare weak_le_antisym [rule del]
```
```   513
```
```   514 lemma le_antisym [intro]:
```
```   515   "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L\<rbrakk> \<Longrightarrow> x = y"
```
```   516   using weak_le_antisym unfolding eq_is_equal .
```
```   517
```
```   518 lemma lless_eq:
```
```   519   "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
```
```   520   unfolding lless_def by (simp add: eq_is_equal)
```
```   521
```
```   522 lemma set_eq_is_eq: "A {.=} B \<longleftrightarrow> A = B"
```
```   523   by (auto simp add: set_eq_def elem_def eq_is_equal)
```
```   524
```
```   525 end
```
```   526
```
```   527 lemma (in partial_order) dual_order:
```
```   528   "partial_order (inv_gorder L)"
```
```   529 proof -
```
```   530   interpret dwo: weak_partial_order "inv_gorder L"
```
```   531     by (metis dual_weak_order)
```
```   532   show ?thesis
```
```   533     by (unfold_locales, simp add:eq_is_equal)
```
```   534 qed
```
```   535
```
```   536 lemma dual_order_iff:
```
```   537   "partial_order (inv_gorder A) \<longleftrightarrow> partial_order A"
```
```   538 proof
```
```   539   assume assm:"partial_order (inv_gorder A)"
```
```   540   then interpret po: partial_order "inv_gorder A"
```
```   541   rewrites "carrier (inv_gorder A) = carrier A"
```
```   542   and   "le (inv_gorder A)      = (\<lambda> x y. le A y x)"
```
```   543   and   "eq (inv_gorder A)      = eq A"
```
```   544     by (simp_all)
```
```   545   show "partial_order A"
```
```   546     apply (unfold_locales, simp_all add: po.sym)
```
```   547     apply (metis po.trans)
```
```   548     apply (metis po.weak_le_antisym, metis po.le_trans)
```
```   549     apply (metis (full_types) po.eq_is_equal, metis po.eq_is_equal)
```
```   550   done
```
```   551 next
```
```   552   assume "partial_order A"
```
```   553   thus "partial_order (inv_gorder A)"
```
```   554     by (metis partial_order.dual_order)
```
```   555 qed
```
```   556
```
```   557 text \<open>Least and greatest, as predicate\<close>
```
```   558
```
```   559 lemma (in partial_order) least_unique:
```
```   560   "\<lbrakk>least L x A; least L y A\<rbrakk> \<Longrightarrow> x = y"
```
```   561   using weak_least_unique unfolding eq_is_equal .
```
```   562
```
```   563 lemma (in partial_order) greatest_unique:
```
```   564   "\<lbrakk>greatest L x A; greatest L y A\<rbrakk> \<Longrightarrow> x = y"
```
```   565   using weak_greatest_unique unfolding eq_is_equal .
```
```   566
```
```   567
```
```   568 subsection \<open>Bounded Orders\<close>
```
```   569
```
```   570 definition
```
```   571   top :: "_ => 'a" ("\<top>\<index>") where
```
```   572   "\<top>\<^bsub>L\<^esub> = (SOME x. greatest L x (carrier L))"
```
```   573
```
```   574 definition
```
```   575   bottom :: "_ => 'a" ("\<bottom>\<index>") where
```
```   576   "\<bottom>\<^bsub>L\<^esub> = (SOME x. least L x (carrier L))"
```
```   577
```
```   578 locale weak_partial_order_bottom = weak_partial_order L for L (structure) +
```
```   579   assumes bottom_exists: "\<exists> x. least L x (carrier L)"
```
```   580 begin
```
```   581
```
```   582 lemma bottom_least: "least L \<bottom> (carrier L)"
```
```   583 proof -
```
```   584   obtain x where "least L x (carrier L)"
```
```   585     by (metis bottom_exists)
```
```   586
```
```   587   thus ?thesis
```
```   588     by (auto intro:someI2 simp add: bottom_def)
```
```   589 qed
```
```   590
```
```   591 lemma bottom_closed [simp, intro]:
```
```   592   "\<bottom> \<in> carrier L"
```
```   593   by (metis bottom_least least_mem)
```
```   594
```
```   595 lemma bottom_lower [simp, intro]:
```
```   596   "x \<in> carrier L \<Longrightarrow> \<bottom> \<sqsubseteq> x"
```
```   597   by (metis bottom_least least_le)
```
```   598
```
```   599 end
```
```   600
```
```   601 locale weak_partial_order_top = weak_partial_order L for L (structure) +
```
```   602   assumes top_exists: "\<exists> x. greatest L x (carrier L)"
```
```   603 begin
```
```   604
```
```   605 lemma top_greatest: "greatest L \<top> (carrier L)"
```
```   606 proof -
```
```   607   obtain x where "greatest L x (carrier L)"
```
```   608     by (metis top_exists)
```
```   609
```
```   610   thus ?thesis
```
```   611     by (auto intro:someI2 simp add: top_def)
```
```   612 qed
```
```   613
```
```   614 lemma top_closed [simp, intro]:
```
```   615   "\<top> \<in> carrier L"
```
```   616   by (metis greatest_mem top_greatest)
```
```   617
```
```   618 lemma top_higher [simp, intro]:
```
```   619   "x \<in> carrier L \<Longrightarrow> x \<sqsubseteq> \<top>"
```
```   620   by (metis greatest_le top_greatest)
```
```   621
```
```   622 end
```
```   623
```
```   624
```
```   625 subsection \<open>Total Orders\<close>
```
```   626
```
```   627 locale weak_total_order = weak_partial_order +
```
```   628   assumes total: "\<lbrakk>x \<in> carrier L; y \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
```
```   629
```
```   630 text \<open>Introduction rule: the usual definition of total order\<close>
```
```   631
```
```   632 lemma (in weak_partial_order) weak_total_orderI:
```
```   633   assumes total: "!!x y. \<lbrakk>x \<in> carrier L; y \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
```
```   634   shows "weak_total_order L"
```
```   635   by unfold_locales (rule total)
```
```   636
```
```   637
```
```   638 subsection \<open>Total orders where \<open>eq\<close> is the Equality\<close>
```
```   639
```
```   640 locale total_order = partial_order +
```
```   641   assumes total_order_total: "\<lbrakk>x \<in> carrier L; y \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
```
```   642
```
```   643 sublocale total_order < weak?: weak_total_order
```
```   644   by unfold_locales (rule total_order_total)
```
```   645
```
```   646 text \<open>Introduction rule: the usual definition of total order\<close>
```
```   647
```
```   648 lemma (in partial_order) total_orderI:
```
```   649   assumes total: "!!x y. \<lbrakk>x \<in> carrier L; y \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
```
```   650   shows "total_order L"
```
```   651   by unfold_locales (rule total)
```
```   652
```
```   653 end
```