src/HOL/Algebra/Order.thy
 author wenzelm Sat Nov 04 15:24:40 2017 +0100 (20 months ago) changeset 67003 49850a679c2c parent 66453 cc19f7ca2ed6 child 67091 1393c2340eec permissions -rw-r--r--
more robust sorted_entries;
```     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   "HOL-Library.FuncSet"
```
```    12   Congruence
```
```    13 begin
```
```    14
```
```    15 section \<open>Orders\<close>
```
```    16
```
```    17 subsection \<open>Partial Orders\<close>
```
```    18
```
```    19 record 'a gorder = "'a eq_object" +
```
```    20   le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
```
```    21
```
```    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>"
```
```    27
```
```    28 lemma inv_gorder_inv:
```
```    29   "inv_gorder (inv_gorder L) = L"
```
```    30   by simp
```
```    31
```
```    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"
```
```    42
```
```    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"
```
```    46
```
```    47
```
```    48 subsubsection \<open>The order relation\<close>
```
```    49
```
```    50 context weak_partial_order
```
```    51 begin
```
```    52
```
```    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])
```
```    56
```
```    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])
```
```    60
```
```    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)
```
```    63
```
```    64 end
```
```    65
```
```    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
```
```    71
```
```    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
```
```    77
```
```    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
```
```    83
```
```    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)
```
```    89
```
```    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)
```
```    96
```
```    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*)
```
```   103
```
```   104
```
```   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
```
```   111
```
```   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)
```
```   117
```
```   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
```
```   134
```
```   135
```
```   136 subsubsection \<open>Upper and lower bounds of a set\<close>
```
```   137
```
```   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"
```
```   141
```
```   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"
```
```   145
```
```   146 lemma Upper_closed [intro!, simp]:
```
```   147   "Upper L A \<subseteq> carrier L"
```
```   148   by (unfold Upper_def) clarify
```
```   149
```
```   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
```
```   154
```
```   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)
```
```   159
```
```   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
```
```   164
```
```   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
```
```   168
```
```   169 lemma Upper_antimono:
```
```   170   "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
```
```   171   by (unfold Upper_def) blast
```
```   172
```
```   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)+
```
```   176
```
```   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
```
```   191
```
```   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"
```
```   205
```
```   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
```
```   212
```
```   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"
```
```   221
```
```   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
```
```   228
```
```   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
```
```   233
```
```   234 lemma Lower_closed [intro!, simp]:
```
```   235   "Lower L A \<subseteq> carrier L"
```
```   236   by (unfold Lower_def) clarify
```
```   237
```
```   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
```
```   242
```
```   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
```
```   247
```
```   248 lemma Lower_antimono:
```
```   249   "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
```
```   250   by (unfold Lower_def) blast
```
```   251
```
```   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)+
```
```   255
```
```   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]])
```
```   263
```
```   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
```
```   278
```
```   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
```
```   284
```
```   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+
```
```   296
```
```   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
```
```   307
```
```   308 text \<open>Jacobson: Theorem 8.1\<close>
```
```   309
```
```   310 lemma Lower_empty [simp]:
```
```   311   "Lower L {} = carrier L"
```
```   312   by (unfold Lower_def) simp
```
```   313
```
```   314 lemma Upper_empty [simp]:
```
```   315   "Upper L {} = carrier L"
```
```   316   by (unfold Upper_def) simp
```
```   317
```
```   318
```
```   319 subsubsection \<open>Least and greatest, as predicate\<close>
```
```   320
```
```   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)"
```
```   324
```
```   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)"
```
```   328
```
```   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>
```
```   331
```
```   332 lemma least_closed [intro, simp]:
```
```   333   "least L l A ==> l \<in> carrier L"
```
```   334   by (unfold least_def) fast
```
```   335
```
```   336 lemma least_mem:
```
```   337   "least L l A ==> l \<in> A"
```
```   338   by (unfold least_def) fast
```
```   339
```
```   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
```
```   343
```
```   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
```
```   348
```
```   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)
```
```   352
```
```   353 abbreviation is_lub :: "[_, 'a, 'a set] => bool"
```
```   354 where "is_lub L x A \<equiv> least L x (Upper L A)"
```
```   355
```
```   356 text (in weak_partial_order) \<open>@{const least} is not congruent in the second parameter for
```
```   357   @{term "A {.=} A'"}\<close>
```
```   358
```
```   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
```
```   365
```
```   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+
```
```   372
```
```   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
```
```   385
```
```   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
```
```   390
```
```   391 lemma greatest_closed [intro, simp]:
```
```   392   "greatest L l A ==> l \<in> carrier L"
```
```   393   by (unfold greatest_def) fast
```
```   394
```
```   395 lemma greatest_mem:
```
```   396   "greatest L l A ==> l \<in> A"
```
```   397   by (unfold greatest_def) fast
```
```   398
```
```   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
```
```   402
```
```   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
```
```   407
```
```   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)
```
```   412
```
```   413 abbreviation is_glb :: "[_, 'a, 'a set] => bool"
```
```   414 where "is_glb L x A \<equiv> greatest L x (Lower L A)"
```
```   415
```
```   416 text (in weak_partial_order) \<open>@{const greatest} is not congruent in the second parameter for
```
```   417   @{term "A {.=} A'"} \<close>
```
```   418
```
```   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
```
```   425
```
```   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+
```
```   432
```
```   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
```
```   445
```
```   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
```
```   450
```
```   451 lemma Lower_dual [simp]:
```
```   452   "Lower (inv_gorder L) A = Upper L A"
```
```   453   by (simp add:Upper_def Lower_def)
```
```   454
```
```   455 lemma Upper_dual [simp]:
```
```   456   "Upper (inv_gorder L) A = Lower L A"
```
```   457   by (simp add:Upper_def Lower_def)
```
```   458
```
```   459 lemma least_dual [simp]:
```
```   460   "least (inv_gorder L) x A = greatest L x A"
```
```   461   by (simp add:least_def greatest_def)
```
```   462
```
```   463 lemma greatest_dual [simp]:
```
```   464   "greatest (inv_gorder L) x A = least L x A"
```
```   465   by (simp add:least_def greatest_def)
```
```   466
```
```   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
```
```   477
```
```   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
```
```   494
```
```   495
```
```   496 subsubsection \<open>Intervals\<close>
```
```   497
```
```   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}"
```
```   501
```
```   502 context weak_partial_order
```
```   503 begin
```
```   504
```
```   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)
```
```   508
```
```   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)
```
```   512
```
```   513   lemma at_least_at_most_closed: "\<lbrace>a..b\<rbrace> \<subseteq> carrier L"
```
```   514     by (auto simp add: at_least_at_most_def)
```
```   515
```
```   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)
```
```   519
```
```   520 end
```
```   521
```
```   522
```
```   523 subsubsection \<open>Isotone functions\<close>
```
```   524
```
```   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)"
```
```   530
```
```   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)
```
```   539
```
```   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"
```
```   542
```
```   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)
```
```   547
```
```   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)
```
```   552
```
```   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)
```
```   557
```
```   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)
```
```   561
```
```   562
```
```   563 subsubsection \<open>Idempotent functions\<close>
```
```   564
```
```   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"
```
```   568
```
```   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)
```
```   572
```
```   573
```
```   574 subsubsection \<open>Order embeddings\<close>
```
```   575
```
```   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 )"
```
```   581
```
```   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)
```
```   584
```
```   585
```
```   586 subsubsection \<open>Commuting functions\<close>
```
```   587
```
```   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)"
```
```   590
```
```   591 subsection \<open>Partial orders where \<open>eq\<close> is the Equality\<close>
```
```   592
```
```   593 locale partial_order = weak_partial_order +
```
```   594   assumes eq_is_equal: "op .= = op ="
```
```   595 begin
```
```   596
```
```   597 declare weak_le_antisym [rule del]
```
```   598
```
```   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 .
```
```   602
```
```   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)
```
```   606
```
```   607 lemma set_eq_is_eq: "A {.=} B \<longleftrightarrow> A = B"
```
```   608   by (auto simp add: set_eq_def elem_def eq_is_equal)
```
```   609
```
```   610 end
```
```   611
```
```   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
```
```   620
```
```   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
```
```   641
```
```   642 text \<open>Least and greatest, as predicate\<close>
```
```   643
```
```   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 .
```
```   647
```
```   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 .
```
```   651
```
```   652
```
```   653 subsection \<open>Bounded Orders\<close>
```
```   654
```
```   655 definition
```
```   656   top :: "_ => 'a" ("\<top>\<index>") where
```
```   657   "\<top>\<^bsub>L\<^esub> = (SOME x. greatest L x (carrier L))"
```
```   658
```
```   659 definition
```
```   660   bottom :: "_ => 'a" ("\<bottom>\<index>") where
```
```   661   "\<bottom>\<^bsub>L\<^esub> = (SOME x. least L x (carrier L))"
```
```   662
```
```   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
```
```   666
```
```   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)
```
```   671
```
```   672   thus ?thesis
```
```   673     by (auto intro:someI2 simp add: bottom_def)
```
```   674 qed
```
```   675
```
```   676 lemma bottom_closed [simp, intro]:
```
```   677   "\<bottom> \<in> carrier L"
```
```   678   by (metis bottom_least least_mem)
```
```   679
```
```   680 lemma bottom_lower [simp, intro]:
```
```   681   "x \<in> carrier L \<Longrightarrow> \<bottom> \<sqsubseteq> x"
```
```   682   by (metis bottom_least least_le)
```
```   683
```
```   684 end
```
```   685
```
```   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
```
```   689
```
```   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)
```
```   694
```
```   695   thus ?thesis
```
```   696     by (auto intro:someI2 simp add: top_def)
```
```   697 qed
```
```   698
```
```   699 lemma top_closed [simp, intro]:
```
```   700   "\<top> \<in> carrier L"
```
```   701   by (metis greatest_mem top_greatest)
```
```   702
```
```   703 lemma top_higher [simp, intro]:
```
```   704   "x \<in> carrier L \<Longrightarrow> x \<sqsubseteq> \<top>"
```
```   705   by (metis greatest_le top_greatest)
```
```   706
```
```   707 end
```
```   708
```
```   709
```
```   710 subsection \<open>Total Orders\<close>
```
```   711
```
```   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"
```
```   714
```
```   715 text \<open>Introduction rule: the usual definition of total order\<close>
```
```   716
```
```   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)
```
```   721
```
```   722
```
```   723 subsection \<open>Total orders where \<open>eq\<close> is the Equality\<close>
```
```   724
```
```   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"
```
```   727
```
```   728 sublocale total_order < weak?: weak_total_order
```
```   729   by unfold_locales (rule total_order_total)
```
```   730
```
```   731 text \<open>Introduction rule: the usual definition of total order\<close>
```
```   732
```
```   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)
```
```   737
```
```   738 end
```