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