src/HOL/Algebra/Order.thy
author paulson <lp15@cam.ac.uk>
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