src/HOL/Algebra/Complete_Lattice.thy
author paulson <lp15@cam.ac.uk>
Sat Jun 30 15:44:04 2018 +0100 (12 months ago)
changeset 68551 b680e74eb6f2
parent 68488 dfbd80c3d180
child 68684 9a42b84f8838
permissions -rw-r--r--
More on Algebra by Paulo and Martin
ballarin@65099
     1
(*  Title:      HOL/Algebra/Complete_Lattice.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 Complete_Lattice
ballarin@66579
    10
imports Lattice
ballarin@65099
    11
begin
ballarin@65099
    12
ballarin@65099
    13
section \<open>Complete Lattices\<close>
ballarin@65099
    14
ballarin@65099
    15
locale weak_complete_lattice = weak_partial_order +
ballarin@65099
    16
  assumes sup_exists:
wenzelm@67091
    17
    "[| A \<subseteq> carrier L |] ==> \<exists>s. least L s (Upper L A)"
ballarin@65099
    18
    and inf_exists:
wenzelm@67091
    19
    "[| A \<subseteq> carrier L |] ==> \<exists>i. greatest L i (Lower L A)"
ballarin@65099
    20
ballarin@65099
    21
sublocale weak_complete_lattice \<subseteq> weak_lattice
ballarin@65099
    22
proof
ballarin@65099
    23
  fix x y
ballarin@65099
    24
  assume a: "x \<in> carrier L" "y \<in> carrier L"
ballarin@65099
    25
  thus "\<exists>s. is_lub L s {x, y}"
ballarin@65099
    26
    by (rule_tac sup_exists[of "{x, y}"], auto)
ballarin@65099
    27
  from a show "\<exists>s. is_glb L s {x, y}"
ballarin@65099
    28
    by (rule_tac inf_exists[of "{x, y}"], auto)
ballarin@65099
    29
qed
ballarin@65099
    30
ballarin@65099
    31
text \<open>Introduction rule: the usual definition of complete lattice\<close>
ballarin@65099
    32
ballarin@65099
    33
lemma (in weak_partial_order) weak_complete_latticeI:
ballarin@65099
    34
  assumes sup_exists:
wenzelm@67091
    35
    "!!A. [| A \<subseteq> carrier L |] ==> \<exists>s. least L s (Upper L A)"
ballarin@65099
    36
    and inf_exists:
wenzelm@67091
    37
    "!!A. [| A \<subseteq> carrier L |] ==> \<exists>i. greatest L i (Lower L A)"
ballarin@65099
    38
  shows "weak_complete_lattice L"
ballarin@65099
    39
  by standard (auto intro: sup_exists inf_exists)
ballarin@65099
    40
ballarin@65099
    41
lemma (in weak_complete_lattice) dual_weak_complete_lattice:
ballarin@65099
    42
  "weak_complete_lattice (inv_gorder L)"
ballarin@65099
    43
proof -
ballarin@65099
    44
  interpret dual: weak_lattice "inv_gorder L"
ballarin@65099
    45
    by (metis dual_weak_lattice)
ballarin@65099
    46
  show ?thesis
lp15@68488
    47
    by (unfold_locales) (simp_all add:inf_exists sup_exists)
ballarin@65099
    48
qed
ballarin@65099
    49
ballarin@65099
    50
lemma (in weak_complete_lattice) supI:
ballarin@65099
    51
  "[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |]
ballarin@65099
    52
  ==> P (\<Squnion>A)"
ballarin@65099
    53
proof (unfold sup_def)
ballarin@65099
    54
  assume L: "A \<subseteq> carrier L"
ballarin@65099
    55
    and P: "!!l. least L l (Upper L A) ==> P l"
ballarin@65099
    56
  with sup_exists obtain s where "least L s (Upper L A)" by blast
ballarin@65099
    57
  with L show "P (SOME l. least L l (Upper L A))"
ballarin@65099
    58
  by (fast intro: someI2 weak_least_unique P)
ballarin@65099
    59
qed
ballarin@65099
    60
ballarin@65099
    61
lemma (in weak_complete_lattice) sup_closed [simp]:
ballarin@65099
    62
  "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L"
ballarin@65099
    63
  by (rule supI) simp_all
ballarin@65099
    64
ballarin@65099
    65
lemma (in weak_complete_lattice) sup_cong:
ballarin@65099
    66
  assumes "A \<subseteq> carrier L" "B \<subseteq> carrier L" "A {.=} B"
ballarin@65099
    67
  shows "\<Squnion> A .= \<Squnion> B"
ballarin@65099
    68
proof -
ballarin@65099
    69
  have "\<And> x. is_lub L x A \<longleftrightarrow> is_lub L x B"
ballarin@65099
    70
    by (rule least_Upper_cong_r, simp_all add: assms)
ballarin@65099
    71
  moreover have "\<Squnion> B \<in> carrier L"
ballarin@65099
    72
    by (simp add: assms(2))
ballarin@65099
    73
  ultimately show ?thesis
ballarin@65099
    74
    by (simp add: sup_def)
ballarin@65099
    75
qed
ballarin@65099
    76
ballarin@65099
    77
sublocale weak_complete_lattice \<subseteq> weak_bounded_lattice
ballarin@65099
    78
  apply (unfold_locales)
ballarin@65099
    79
  apply (metis Upper_empty empty_subsetI sup_exists)
ballarin@65099
    80
  apply (metis Lower_empty empty_subsetI inf_exists)
ballarin@65099
    81
done
ballarin@65099
    82
ballarin@65099
    83
lemma (in weak_complete_lattice) infI:
ballarin@65099
    84
  "[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |]
ballarin@65099
    85
  ==> P (\<Sqinter>A)"
ballarin@65099
    86
proof (unfold inf_def)
ballarin@65099
    87
  assume L: "A \<subseteq> carrier L"
ballarin@65099
    88
    and P: "!!l. greatest L l (Lower L A) ==> P l"
ballarin@65099
    89
  with inf_exists obtain s where "greatest L s (Lower L A)" by blast
ballarin@65099
    90
  with L show "P (SOME l. greatest L l (Lower L A))"
ballarin@65099
    91
  by (fast intro: someI2 weak_greatest_unique P)
ballarin@65099
    92
qed
ballarin@65099
    93
ballarin@65099
    94
lemma (in weak_complete_lattice) inf_closed [simp]:
ballarin@65099
    95
  "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L"
ballarin@65099
    96
  by (rule infI) simp_all
ballarin@65099
    97
ballarin@65099
    98
lemma (in weak_complete_lattice) inf_cong:
ballarin@65099
    99
  assumes "A \<subseteq> carrier L" "B \<subseteq> carrier L" "A {.=} B"
ballarin@65099
   100
  shows "\<Sqinter> A .= \<Sqinter> B"
ballarin@65099
   101
proof -
ballarin@65099
   102
  have "\<And> x. is_glb L x A \<longleftrightarrow> is_glb L x B"
ballarin@65099
   103
    by (rule greatest_Lower_cong_r, simp_all add: assms)
ballarin@65099
   104
  moreover have "\<Sqinter> B \<in> carrier L"
ballarin@65099
   105
    by (simp add: assms(2))
ballarin@65099
   106
  ultimately show ?thesis
ballarin@65099
   107
    by (simp add: inf_def)
ballarin@65099
   108
qed
ballarin@65099
   109
ballarin@65099
   110
theorem (in weak_partial_order) weak_complete_lattice_criterion1:
wenzelm@67091
   111
  assumes top_exists: "\<exists>g. greatest L g (carrier L)"
ballarin@65099
   112
    and inf_exists:
wenzelm@67091
   113
      "\<And>A. [| A \<subseteq> carrier L; A \<noteq> {} |] ==> \<exists>i. greatest L i (Lower L A)"
ballarin@65099
   114
  shows "weak_complete_lattice L"
ballarin@65099
   115
proof (rule weak_complete_latticeI)
ballarin@65099
   116
  from top_exists obtain top where top: "greatest L top (carrier L)" ..
ballarin@65099
   117
  fix A
ballarin@65099
   118
  assume L: "A \<subseteq> carrier L"
ballarin@65099
   119
  let ?B = "Upper L A"
ballarin@65099
   120
  from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)
wenzelm@67091
   121
  then have B_non_empty: "?B \<noteq> {}" by fast
ballarin@65099
   122
  have B_L: "?B \<subseteq> carrier L" by simp
ballarin@65099
   123
  from inf_exists [OF B_L B_non_empty]
ballarin@65099
   124
  obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
lp15@68488
   125
  then have bcarr: "b \<in> carrier L"
lp15@68488
   126
    by auto
ballarin@65099
   127
  have "least L b (Upper L A)"
lp15@68488
   128
  proof (rule least_UpperI)
lp15@68488
   129
    show "\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> b"
lp15@68488
   130
      by (meson L Lower_memI Upper_memD b_inf_B greatest_le set_mp)
lp15@68488
   131
    show "\<And>y. y \<in> Upper L A \<Longrightarrow> b \<sqsubseteq> y"
lp15@68488
   132
      by (meson B_L b_inf_B greatest_Lower_below)
lp15@68488
   133
  qed (use bcarr L in auto)
wenzelm@67091
   134
  then show "\<exists>s. least L s (Upper L A)" ..
ballarin@65099
   135
next
ballarin@65099
   136
  fix A
ballarin@65099
   137
  assume L: "A \<subseteq> carrier L"
wenzelm@67091
   138
  show "\<exists>i. greatest L i (Lower L A)"
lp15@68488
   139
    by (metis L Lower_empty inf_exists top_exists)
ballarin@65099
   140
qed
ballarin@65099
   141
ballarin@65099
   142
ballarin@65099
   143
text \<open>Supremum\<close>
ballarin@65099
   144
ballarin@65099
   145
declare (in partial_order) weak_sup_of_singleton [simp del]
ballarin@65099
   146
ballarin@65099
   147
lemma (in partial_order) sup_of_singleton [simp]:
ballarin@65099
   148
  "x \<in> carrier L ==> \<Squnion>{x} = x"
ballarin@65099
   149
  using weak_sup_of_singleton unfolding eq_is_equal .
ballarin@65099
   150
ballarin@65099
   151
lemma (in upper_semilattice) join_assoc_lemma:
ballarin@65099
   152
  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
ballarin@65099
   153
  shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}"
ballarin@65099
   154
  using weak_join_assoc_lemma L unfolding eq_is_equal .
ballarin@65099
   155
ballarin@65099
   156
lemma (in upper_semilattice) join_assoc:
ballarin@65099
   157
  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
ballarin@65099
   158
  shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
ballarin@65099
   159
  using weak_join_assoc L unfolding eq_is_equal .
ballarin@65099
   160
ballarin@65099
   161
ballarin@65099
   162
text \<open>Infimum\<close>
ballarin@65099
   163
ballarin@65099
   164
declare (in partial_order) weak_inf_of_singleton [simp del]
ballarin@65099
   165
ballarin@65099
   166
lemma (in partial_order) inf_of_singleton [simp]:
ballarin@65099
   167
  "x \<in> carrier L ==> \<Sqinter>{x} = x"
ballarin@65099
   168
  using weak_inf_of_singleton unfolding eq_is_equal .
ballarin@65099
   169
ballarin@65099
   170
text \<open>Condition on \<open>A\<close>: infimum exists.\<close>
ballarin@65099
   171
ballarin@65099
   172
lemma (in lower_semilattice) meet_assoc_lemma:
ballarin@65099
   173
  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
ballarin@65099
   174
  shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}"
ballarin@65099
   175
  using weak_meet_assoc_lemma L unfolding eq_is_equal .
ballarin@65099
   176
ballarin@65099
   177
lemma (in lower_semilattice) meet_assoc:
ballarin@65099
   178
  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
ballarin@65099
   179
  shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
ballarin@65099
   180
  using weak_meet_assoc L unfolding eq_is_equal .
ballarin@65099
   181
ballarin@65099
   182
ballarin@65099
   183
subsection \<open>Infimum Laws\<close>
ballarin@65099
   184
ballarin@65099
   185
context weak_complete_lattice
ballarin@65099
   186
begin
ballarin@65099
   187
ballarin@65099
   188
lemma inf_glb: 
ballarin@65099
   189
  assumes "A \<subseteq> carrier L"
ballarin@65099
   190
  shows "greatest L (\<Sqinter>A) (Lower L A)"
ballarin@65099
   191
proof -
ballarin@65099
   192
  obtain i where "greatest L i (Lower L A)"
ballarin@65099
   193
    by (metis assms inf_exists)
ballarin@65099
   194
  thus ?thesis
lp15@68488
   195
    by (metis inf_def someI_ex)
ballarin@65099
   196
qed
ballarin@65099
   197
ballarin@65099
   198
lemma inf_lower:
ballarin@65099
   199
  assumes "A \<subseteq> carrier L" "x \<in> A"
ballarin@65099
   200
  shows "\<Sqinter>A \<sqsubseteq> x"
ballarin@65099
   201
  by (metis assms greatest_Lower_below inf_glb)
ballarin@65099
   202
ballarin@65099
   203
lemma inf_greatest: 
ballarin@65099
   204
  assumes "A \<subseteq> carrier L" "z \<in> carrier L" 
ballarin@65099
   205
          "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x)"
ballarin@65099
   206
  shows "z \<sqsubseteq> \<Sqinter>A"
ballarin@65099
   207
  by (metis Lower_memI assms greatest_le inf_glb)
ballarin@65099
   208
ballarin@65099
   209
lemma weak_inf_empty [simp]: "\<Sqinter>{} .= \<top>"
ballarin@65099
   210
  by (metis Lower_empty empty_subsetI inf_glb top_greatest weak_greatest_unique)
ballarin@65099
   211
ballarin@65099
   212
lemma weak_inf_carrier [simp]: "\<Sqinter>carrier L .= \<bottom>"
ballarin@65099
   213
  by (metis bottom_weak_eq inf_closed inf_lower subset_refl)
ballarin@65099
   214
ballarin@65099
   215
lemma weak_inf_insert [simp]: 
lp15@68488
   216
  assumes "a \<in> carrier L" "A \<subseteq> carrier L"
lp15@68488
   217
  shows "\<Sqinter>insert a A .= a \<sqinter> \<Sqinter>A"
lp15@68488
   218
proof (rule weak_le_antisym)
lp15@68488
   219
  show "\<Sqinter>insert a A \<sqsubseteq> a \<sqinter> \<Sqinter>A"
lp15@68488
   220
    by (simp add: assms inf_lower local.inf_greatest meet_le)
lp15@68488
   221
  show aA: "a \<sqinter> \<Sqinter>A \<in> carrier L"
lp15@68488
   222
    using assms by simp
lp15@68488
   223
  show "a \<sqinter> \<Sqinter>A \<sqsubseteq> \<Sqinter>insert a A"
lp15@68488
   224
    apply (rule inf_greatest)
lp15@68488
   225
    using assms apply (simp_all add: aA)
lp15@68488
   226
    by (meson aA inf_closed inf_lower local.le_trans meet_left meet_right subsetCE)
lp15@68488
   227
  show "\<Sqinter>insert a A \<in> carrier L"
lp15@68488
   228
    using assms by (force intro: le_trans inf_closed meet_right meet_left inf_lower)
lp15@68488
   229
qed
ballarin@65099
   230
ballarin@65099
   231
subsection \<open>Supremum Laws\<close>
ballarin@65099
   232
ballarin@65099
   233
lemma sup_lub: 
ballarin@65099
   234
  assumes "A \<subseteq> carrier L"
ballarin@65099
   235
  shows "least L (\<Squnion>A) (Upper L A)"
ballarin@65099
   236
    by (metis Upper_is_closed assms least_closed least_cong supI sup_closed sup_exists weak_least_unique)
ballarin@65099
   237
ballarin@65099
   238
lemma sup_upper: 
ballarin@65099
   239
  assumes "A \<subseteq> carrier L" "x \<in> A"
ballarin@65099
   240
  shows "x \<sqsubseteq> \<Squnion>A"
ballarin@65099
   241
  by (metis assms least_Upper_above supI)
ballarin@65099
   242
ballarin@65099
   243
lemma sup_least:
ballarin@65099
   244
  assumes "A \<subseteq> carrier L" "z \<in> carrier L" 
ballarin@65099
   245
          "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z)" 
ballarin@65099
   246
  shows "\<Squnion>A \<sqsubseteq> z"
ballarin@65099
   247
  by (metis Upper_memI assms least_le sup_lub)
ballarin@65099
   248
ballarin@65099
   249
lemma weak_sup_empty [simp]: "\<Squnion>{} .= \<bottom>"
ballarin@65099
   250
  by (metis Upper_empty bottom_least empty_subsetI sup_lub weak_least_unique)
ballarin@65099
   251
ballarin@65099
   252
lemma weak_sup_carrier [simp]: "\<Squnion>carrier L .= \<top>"
ballarin@65099
   253
  by (metis Lower_closed Lower_empty sup_closed sup_upper top_closed top_higher weak_le_antisym)
ballarin@65099
   254
ballarin@65099
   255
lemma weak_sup_insert [simp]: 
lp15@68488
   256
  assumes "a \<in> carrier L" "A \<subseteq> carrier L"
lp15@68488
   257
  shows "\<Squnion>insert a A .= a \<squnion> \<Squnion>A"
lp15@68488
   258
proof (rule weak_le_antisym)
lp15@68488
   259
  show aA: "a \<squnion> \<Squnion>A \<in> carrier L"
lp15@68488
   260
    using assms by simp
lp15@68488
   261
  show "\<Squnion>insert a A \<sqsubseteq> a \<squnion> \<Squnion>A"
lp15@68488
   262
    apply (rule sup_least)
lp15@68488
   263
    using assms apply (simp_all add: aA)
lp15@68488
   264
    by (meson aA join_left join_right local.le_trans subsetCE sup_closed sup_upper)
lp15@68488
   265
  show "a \<squnion> \<Squnion>A \<sqsubseteq> \<Squnion>insert a A"
lp15@68488
   266
    by (simp add: assms join_le local.sup_least sup_upper)
lp15@68488
   267
  show "\<Squnion>insert a A \<in> carrier L"
lp15@68488
   268
    using assms by (force intro: le_trans inf_closed meet_right meet_left inf_lower)
lp15@68488
   269
qed
ballarin@65099
   270
ballarin@65099
   271
end
ballarin@65099
   272
ballarin@65099
   273
ballarin@65099
   274
subsection \<open>Fixed points of a lattice\<close>
ballarin@65099
   275
ballarin@65099
   276
definition "fps L f = {x \<in> carrier L. f x .=\<^bsub>L\<^esub> x}"
ballarin@65099
   277
ballarin@65099
   278
abbreviation "fpl L f \<equiv> L\<lparr>carrier := fps L f\<rparr>"
ballarin@65099
   279
ballarin@65099
   280
lemma (in weak_partial_order) 
ballarin@65099
   281
  use_fps: "x \<in> fps L f \<Longrightarrow> f x .= x"
ballarin@65099
   282
  by (simp add: fps_def)
ballarin@65099
   283
ballarin@65099
   284
lemma fps_carrier [simp]:
ballarin@65099
   285
  "fps L f \<subseteq> carrier L"
ballarin@65099
   286
  by (auto simp add: fps_def)
ballarin@65099
   287
ballarin@65099
   288
lemma (in weak_complete_lattice) fps_sup_image: 
ballarin@65099
   289
  assumes "f \<in> carrier L \<rightarrow> carrier L" "A \<subseteq> fps L f" 
ballarin@65099
   290
  shows "\<Squnion> (f ` A) .= \<Squnion> A"
ballarin@65099
   291
proof -
ballarin@65099
   292
  from assms(2) have AL: "A \<subseteq> carrier L"
ballarin@65099
   293
    by (auto simp add: fps_def)
ballarin@65099
   294
  show ?thesis
ballarin@65099
   295
  proof (rule sup_cong, simp_all add: AL)
ballarin@65099
   296
    from assms(1) AL show "f ` A \<subseteq> carrier L"
lp15@68488
   297
      by auto
lp15@68488
   298
    then have *: "\<And>b. \<lbrakk>A \<subseteq> {x \<in> carrier L. f x .= x}; b \<in> A\<rbrakk> \<Longrightarrow> \<exists>a\<in>f ` A. b .= a"
lp15@68488
   299
      by (meson AL assms(2) image_eqI local.sym subsetCE use_fps)
ballarin@65099
   300
    from assms(2) show "f ` A {.=} A"
lp15@68488
   301
      by (auto simp add: fps_def intro: set_eqI2 [OF _ *])
ballarin@65099
   302
  qed
ballarin@65099
   303
qed
ballarin@65099
   304
ballarin@65099
   305
lemma (in weak_complete_lattice) fps_idem:
lp15@68488
   306
  assumes "f \<in> carrier L \<rightarrow> carrier L" "Idem f"
lp15@68488
   307
  shows "fps L f {.=} f ` carrier L"
lp15@68488
   308
proof (rule set_eqI2)
lp15@68488
   309
  show "\<And>a. a \<in> fps L f \<Longrightarrow> \<exists>b\<in>f ` carrier L. a .= b"
lp15@68488
   310
    using assms by (force simp add: fps_def intro: local.sym)
lp15@68488
   311
  show "\<And>b. b \<in> f ` carrier L \<Longrightarrow> \<exists>a\<in>fps L f. b .= a"
lp15@68488
   312
    using assms by (force simp add: idempotent_def fps_def)
lp15@68488
   313
qed
ballarin@65099
   314
ballarin@65099
   315
context weak_complete_lattice
ballarin@65099
   316
begin
ballarin@65099
   317
ballarin@65099
   318
lemma weak_sup_pre_fixed_point: 
ballarin@65099
   319
  assumes "f \<in> carrier L \<rightarrow> carrier L" "isotone L L f" "A \<subseteq> fps L f"
ballarin@65099
   320
  shows "(\<Squnion>\<^bsub>L\<^esub> A) \<sqsubseteq>\<^bsub>L\<^esub> f (\<Squnion>\<^bsub>L\<^esub> A)"
ballarin@65099
   321
proof (rule sup_least)
ballarin@65099
   322
  from assms(3) show AL: "A \<subseteq> carrier L"
ballarin@65099
   323
    by (auto simp add: fps_def)
ballarin@65099
   324
  thus fA: "f (\<Squnion>A) \<in> carrier L"
ballarin@65099
   325
    by (simp add: assms funcset_carrier[of f L L])
ballarin@65099
   326
  fix x
ballarin@65099
   327
  assume xA: "x \<in> A"
ballarin@65099
   328
  hence "x \<in> fps L f"
ballarin@65099
   329
    using assms subsetCE by blast
ballarin@65099
   330
  hence "f x .=\<^bsub>L\<^esub> x"
ballarin@65099
   331
    by (auto simp add: fps_def)
ballarin@65099
   332
  moreover have "f x \<sqsubseteq>\<^bsub>L\<^esub> f (\<Squnion>\<^bsub>L\<^esub>A)"
ballarin@65099
   333
    by (meson AL assms(2) subsetCE sup_closed sup_upper use_iso1 xA)
ballarin@65099
   334
  ultimately show "x \<sqsubseteq>\<^bsub>L\<^esub> f (\<Squnion>\<^bsub>L\<^esub>A)"
ballarin@65099
   335
    by (meson AL fA assms(1) funcset_carrier le_cong local.refl subsetCE xA)
ballarin@65099
   336
qed
ballarin@65099
   337
ballarin@65099
   338
lemma weak_sup_post_fixed_point: 
ballarin@65099
   339
  assumes "f \<in> carrier L \<rightarrow> carrier L" "isotone L L f" "A \<subseteq> fps L f"
ballarin@65099
   340
  shows "f (\<Sqinter>\<^bsub>L\<^esub> A) \<sqsubseteq>\<^bsub>L\<^esub> (\<Sqinter>\<^bsub>L\<^esub> A)"
ballarin@65099
   341
proof (rule inf_greatest)
ballarin@65099
   342
  from assms(3) show AL: "A \<subseteq> carrier L"
ballarin@65099
   343
    by (auto simp add: fps_def)
ballarin@65099
   344
  thus fA: "f (\<Sqinter>A) \<in> carrier L"
ballarin@65099
   345
    by (simp add: assms funcset_carrier[of f L L])
ballarin@65099
   346
  fix x
ballarin@65099
   347
  assume xA: "x \<in> A"
ballarin@65099
   348
  hence "x \<in> fps L f"
ballarin@65099
   349
    using assms subsetCE by blast
ballarin@65099
   350
  hence "f x .=\<^bsub>L\<^esub> x"
ballarin@65099
   351
    by (auto simp add: fps_def)
ballarin@65099
   352
  moreover have "f (\<Sqinter>\<^bsub>L\<^esub>A) \<sqsubseteq>\<^bsub>L\<^esub> f x"
ballarin@65099
   353
    by (meson AL assms(2) inf_closed inf_lower subsetCE use_iso1 xA)   
ballarin@65099
   354
  ultimately show "f (\<Sqinter>\<^bsub>L\<^esub>A) \<sqsubseteq>\<^bsub>L\<^esub> x"
ballarin@65099
   355
    by (meson AL assms(1) fA funcset_carrier le_cong_r subsetCE xA)
ballarin@65099
   356
qed
ballarin@65099
   357
ballarin@65099
   358
ballarin@65099
   359
subsubsection \<open>Least fixed points\<close>
ballarin@65099
   360
ballarin@65099
   361
lemma LFP_closed [intro, simp]:
ballarin@66580
   362
  "LFP f \<in> carrier L"
ballarin@66580
   363
  by (metis (lifting) LEAST_FP_def inf_closed mem_Collect_eq subsetI)
ballarin@65099
   364
ballarin@65099
   365
lemma LFP_lowerbound: 
ballarin@65099
   366
  assumes "x \<in> carrier L" "f x \<sqsubseteq> x" 
ballarin@66580
   367
  shows "LFP f \<sqsubseteq> x"
ballarin@66580
   368
  by (auto intro:inf_lower assms simp add:LEAST_FP_def)
ballarin@65099
   369
ballarin@65099
   370
lemma LFP_greatest: 
ballarin@65099
   371
  assumes "x \<in> carrier L" 
ballarin@65099
   372
          "(\<And>u. \<lbrakk> u \<in> carrier L; f u \<sqsubseteq> u \<rbrakk> \<Longrightarrow> x \<sqsubseteq> u)"
ballarin@66580
   373
  shows "x \<sqsubseteq> LFP f"
ballarin@66580
   374
  by (auto simp add:LEAST_FP_def intro:inf_greatest assms)
ballarin@65099
   375
ballarin@65099
   376
lemma LFP_lemma2: 
ballarin@65099
   377
  assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
ballarin@66580
   378
  shows "f (LFP f) \<sqsubseteq> LFP f"
lp15@68488
   379
proof (rule LFP_greatest)
lp15@68488
   380
  have f: "\<And>x. x \<in> carrier L \<Longrightarrow> f x \<in> carrier L"
lp15@68488
   381
    using assms by (auto simp add: Pi_def)
lp15@68488
   382
  with assms show "f (LFP f) \<in> carrier L"
lp15@68488
   383
    by blast
lp15@68488
   384
  show "\<And>u. \<lbrakk>u \<in> carrier L; f u \<sqsubseteq> u\<rbrakk> \<Longrightarrow> f (LFP f) \<sqsubseteq> u"
lp15@68488
   385
    by (meson LFP_closed LFP_lowerbound assms(1) f local.le_trans use_iso1)
lp15@68488
   386
qed
ballarin@65099
   387
ballarin@65099
   388
lemma LFP_lemma3: 
ballarin@65099
   389
  assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
ballarin@66580
   390
  shows "LFP f \<sqsubseteq> f (LFP f)"
lp15@68488
   391
  using assms by (simp add: Pi_def) (metis LFP_closed LFP_lemma2 LFP_lowerbound assms(2) use_iso2)
ballarin@65099
   392
ballarin@65099
   393
lemma LFP_weak_unfold: 
ballarin@66580
   394
  "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> LFP f .= f (LFP f)"
ballarin@65099
   395
  by (auto intro: LFP_lemma2 LFP_lemma3 funcset_mem)
ballarin@65099
   396
ballarin@65099
   397
lemma LFP_fixed_point [intro]:
ballarin@65099
   398
  assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
ballarin@66580
   399
  shows "LFP f \<in> fps L f"
ballarin@65099
   400
proof -
ballarin@66580
   401
  have "f (LFP f) \<in> carrier L"
ballarin@65099
   402
    using assms(2) by blast
ballarin@65099
   403
  with assms show ?thesis
ballarin@65099
   404
    by (simp add: LFP_weak_unfold fps_def local.sym)
ballarin@65099
   405
qed
ballarin@65099
   406
ballarin@65099
   407
lemma LFP_least_fixed_point:
ballarin@65099
   408
  assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L" "x \<in> fps L f"
ballarin@66580
   409
  shows "LFP f \<sqsubseteq> x"
ballarin@65099
   410
  using assms by (force intro: LFP_lowerbound simp add: fps_def)
ballarin@65099
   411
  
ballarin@65099
   412
lemma LFP_idem: 
ballarin@65099
   413
  assumes "f \<in> carrier L \<rightarrow> carrier L" "Mono f" "Idem f"
ballarin@66580
   414
  shows "LFP f .= (f \<bottom>)"
ballarin@65099
   415
proof (rule weak_le_antisym)
ballarin@65099
   416
  from assms(1) show fb: "f \<bottom> \<in> carrier L"
ballarin@65099
   417
    by (rule funcset_mem, simp)
ballarin@66580
   418
  from assms show mf: "LFP f \<in> carrier L"
ballarin@65099
   419
    by blast
ballarin@66580
   420
  show "LFP f \<sqsubseteq> f \<bottom>"
ballarin@65099
   421
  proof -
ballarin@65099
   422
    have "f (f \<bottom>) .= f \<bottom>"
ballarin@65099
   423
      by (auto simp add: fps_def fb assms(3) idempotent)
ballarin@65099
   424
    moreover have "f (f \<bottom>) \<in> carrier L"
ballarin@65099
   425
      by (rule funcset_mem[of f "carrier L"], simp_all add: assms fb)
ballarin@65099
   426
    ultimately show ?thesis
ballarin@65099
   427
      by (auto intro: LFP_lowerbound simp add: fb)
ballarin@65099
   428
  qed
ballarin@66580
   429
  show "f \<bottom> \<sqsubseteq> LFP f"
ballarin@65099
   430
  proof -
ballarin@66580
   431
    have "f \<bottom> \<sqsubseteq> f (LFP f)"
ballarin@65099
   432
      by (auto intro: use_iso1[of _ f] simp add: assms)
ballarin@66580
   433
    moreover have "... .= LFP f"
ballarin@65099
   434
      using assms(1) assms(2) fps_def by force
ballarin@66580
   435
    moreover from assms(1) have "f (LFP f) \<in> carrier L"
ballarin@65099
   436
      by (auto)
ballarin@65099
   437
    ultimately show ?thesis
ballarin@65099
   438
      using fb by blast
ballarin@65099
   439
  qed
ballarin@65099
   440
qed
ballarin@65099
   441
ballarin@65099
   442
ballarin@65099
   443
subsubsection \<open>Greatest fixed points\<close>
ballarin@65099
   444
  
ballarin@65099
   445
lemma GFP_closed [intro, simp]:
ballarin@66580
   446
  "GFP f \<in> carrier L"
ballarin@66580
   447
  by (auto intro:sup_closed simp add:GREATEST_FP_def)
ballarin@65099
   448
  
ballarin@65099
   449
lemma GFP_upperbound:
ballarin@65099
   450
  assumes "x \<in> carrier L" "x \<sqsubseteq> f x"
ballarin@66580
   451
  shows "x \<sqsubseteq> GFP f"
ballarin@66580
   452
  by (auto intro:sup_upper assms simp add:GREATEST_FP_def)
ballarin@65099
   453
ballarin@65099
   454
lemma GFP_least: 
ballarin@65099
   455
  assumes "x \<in> carrier L" 
ballarin@65099
   456
          "(\<And>u. \<lbrakk> u \<in> carrier L; u \<sqsubseteq> f u \<rbrakk> \<Longrightarrow> u \<sqsubseteq> x)"
ballarin@66580
   457
  shows "GFP f \<sqsubseteq> x"
ballarin@66580
   458
  by (auto simp add:GREATEST_FP_def intro:sup_least assms)
ballarin@65099
   459
ballarin@65099
   460
lemma GFP_lemma2:
ballarin@65099
   461
  assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
ballarin@66580
   462
  shows "GFP f \<sqsubseteq> f (GFP f)"
lp15@68488
   463
proof (rule GFP_least)
lp15@68488
   464
  have f: "\<And>x. x \<in> carrier L \<Longrightarrow> f x \<in> carrier L"
lp15@68488
   465
    using assms by (auto simp add: Pi_def)
lp15@68488
   466
  with assms show "f (GFP f) \<in> carrier L"
lp15@68488
   467
    by blast
lp15@68488
   468
  show "\<And>u. \<lbrakk>u \<in> carrier L; u \<sqsubseteq> f u\<rbrakk> \<Longrightarrow> u \<sqsubseteq> f (GFP f)"
lp15@68488
   469
    by (meson GFP_closed GFP_upperbound le_trans assms(1) f local.le_trans use_iso1)
lp15@68488
   470
qed
ballarin@65099
   471
ballarin@65099
   472
lemma GFP_lemma3:
ballarin@65099
   473
  assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
ballarin@66580
   474
  shows "f (GFP f) \<sqsubseteq> GFP f"
ballarin@65099
   475
  by (metis GFP_closed GFP_lemma2 GFP_upperbound assms funcset_mem use_iso2)
ballarin@65099
   476
  
ballarin@65099
   477
lemma GFP_weak_unfold: 
ballarin@66580
   478
  "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> GFP f .= f (GFP f)"
ballarin@65099
   479
  by (auto intro: GFP_lemma2 GFP_lemma3 funcset_mem)
ballarin@65099
   480
ballarin@65099
   481
lemma (in weak_complete_lattice) GFP_fixed_point [intro]:
ballarin@65099
   482
  assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
ballarin@66580
   483
  shows "GFP f \<in> fps L f"
ballarin@65099
   484
  using assms
ballarin@65099
   485
proof -
ballarin@66580
   486
  have "f (GFP f) \<in> carrier L"
ballarin@65099
   487
    using assms(2) by blast
ballarin@65099
   488
  with assms show ?thesis
ballarin@65099
   489
    by (simp add: GFP_weak_unfold fps_def local.sym)
ballarin@65099
   490
qed
ballarin@65099
   491
ballarin@65099
   492
lemma GFP_greatest_fixed_point:
ballarin@65099
   493
  assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L" "x \<in> fps L f"
ballarin@66580
   494
  shows "x \<sqsubseteq> GFP f"
ballarin@65099
   495
  using assms 
ballarin@65099
   496
  by (rule_tac GFP_upperbound, auto simp add: fps_def, meson PiE local.sym weak_refl)
ballarin@65099
   497
    
ballarin@65099
   498
lemma GFP_idem: 
ballarin@65099
   499
  assumes "f \<in> carrier L \<rightarrow> carrier L" "Mono f" "Idem f"
ballarin@66580
   500
  shows "GFP f .= (f \<top>)"
ballarin@65099
   501
proof (rule weak_le_antisym)
ballarin@65099
   502
  from assms(1) show fb: "f \<top> \<in> carrier L"
ballarin@65099
   503
    by (rule funcset_mem, simp)
ballarin@66580
   504
  from assms show mf: "GFP f \<in> carrier L"
ballarin@65099
   505
    by blast
ballarin@66580
   506
  show "f \<top> \<sqsubseteq> GFP f"
ballarin@65099
   507
  proof -
ballarin@65099
   508
    have "f (f \<top>) .= f \<top>"
ballarin@65099
   509
      by (auto simp add: fps_def fb assms(3) idempotent)
ballarin@65099
   510
    moreover have "f (f \<top>) \<in> carrier L"
ballarin@65099
   511
      by (rule funcset_mem[of f "carrier L"], simp_all add: assms fb)
ballarin@65099
   512
    ultimately show ?thesis
ballarin@65099
   513
      by (rule_tac GFP_upperbound, simp_all add: fb local.sym)
ballarin@65099
   514
  qed
ballarin@66580
   515
  show "GFP f \<sqsubseteq> f \<top>"
ballarin@65099
   516
  proof -
ballarin@66580
   517
    have "GFP f \<sqsubseteq> f (GFP f)"
ballarin@65099
   518
      by (simp add: GFP_lemma2 assms(1) assms(2))
ballarin@65099
   519
    moreover have "... \<sqsubseteq> f \<top>"
ballarin@65099
   520
      by (auto intro: use_iso1[of _ f] simp add: assms)
ballarin@66580
   521
    moreover from assms(1) have "f (GFP f) \<in> carrier L"
ballarin@65099
   522
      by (auto)
ballarin@65099
   523
    ultimately show ?thesis
ballarin@65099
   524
      using fb local.le_trans by blast
ballarin@65099
   525
  qed
ballarin@65099
   526
qed
ballarin@65099
   527
ballarin@65099
   528
end
ballarin@65099
   529
ballarin@65099
   530
wenzelm@67226
   531
subsection \<open>Complete lattices where \<open>eq\<close> is the Equality\<close>
ballarin@65099
   532
ballarin@65099
   533
locale complete_lattice = partial_order +
ballarin@65099
   534
  assumes sup_exists:
wenzelm@67091
   535
    "[| A \<subseteq> carrier L |] ==> \<exists>s. least L s (Upper L A)"
ballarin@65099
   536
    and inf_exists:
wenzelm@67091
   537
    "[| A \<subseteq> carrier L |] ==> \<exists>i. greatest L i (Lower L A)"
ballarin@65099
   538
ballarin@65099
   539
sublocale complete_lattice \<subseteq> lattice
ballarin@65099
   540
proof
ballarin@65099
   541
  fix x y
ballarin@65099
   542
  assume a: "x \<in> carrier L" "y \<in> carrier L"
ballarin@65099
   543
  thus "\<exists>s. is_lub L s {x, y}"
ballarin@65099
   544
    by (rule_tac sup_exists[of "{x, y}"], auto)
ballarin@65099
   545
  from a show "\<exists>s. is_glb L s {x, y}"
ballarin@65099
   546
    by (rule_tac inf_exists[of "{x, y}"], auto)
ballarin@65099
   547
qed
ballarin@65099
   548
ballarin@65099
   549
sublocale complete_lattice \<subseteq> weak?: weak_complete_lattice
ballarin@65099
   550
  by standard (auto intro: sup_exists inf_exists)
ballarin@65099
   551
ballarin@65099
   552
lemma complete_lattice_lattice [simp]: 
ballarin@65099
   553
  assumes "complete_lattice X"
ballarin@65099
   554
  shows "lattice X"
ballarin@65099
   555
proof -
ballarin@65099
   556
  interpret c: complete_lattice X
ballarin@65099
   557
    by (simp add: assms)
ballarin@65099
   558
  show ?thesis
ballarin@65099
   559
    by (unfold_locales)
ballarin@65099
   560
qed
ballarin@65099
   561
ballarin@65099
   562
text \<open>Introduction rule: the usual definition of complete lattice\<close>
ballarin@65099
   563
ballarin@65099
   564
lemma (in partial_order) complete_latticeI:
ballarin@65099
   565
  assumes sup_exists:
wenzelm@67091
   566
    "!!A. [| A \<subseteq> carrier L |] ==> \<exists>s. least L s (Upper L A)"
ballarin@65099
   567
    and inf_exists:
wenzelm@67091
   568
    "!!A. [| A \<subseteq> carrier L |] ==> \<exists>i. greatest L i (Lower L A)"
ballarin@65099
   569
  shows "complete_lattice L"
ballarin@65099
   570
  by standard (auto intro: sup_exists inf_exists)
ballarin@65099
   571
ballarin@65099
   572
theorem (in partial_order) complete_lattice_criterion1:
wenzelm@67091
   573
  assumes top_exists: "\<exists>g. greatest L g (carrier L)"
ballarin@65099
   574
    and inf_exists:
wenzelm@67091
   575
      "!!A. [| A \<subseteq> carrier L; A \<noteq> {} |] ==> \<exists>i. greatest L i (Lower L A)"
ballarin@65099
   576
  shows "complete_lattice L"
ballarin@65099
   577
proof (rule complete_latticeI)
ballarin@65099
   578
  from top_exists obtain top where top: "greatest L top (carrier L)" ..
ballarin@65099
   579
  fix A
ballarin@65099
   580
  assume L: "A \<subseteq> carrier L"
ballarin@65099
   581
  let ?B = "Upper L A"
ballarin@65099
   582
  from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)
wenzelm@67091
   583
  then have B_non_empty: "?B \<noteq> {}" by fast
ballarin@65099
   584
  have B_L: "?B \<subseteq> carrier L" by simp
ballarin@65099
   585
  from inf_exists [OF B_L B_non_empty]
ballarin@65099
   586
  obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
lp15@68488
   587
  then have bcarr: "b \<in> carrier L"
lp15@68488
   588
    by blast
ballarin@65099
   589
  have "least L b (Upper L A)"
lp15@68488
   590
  proof (rule least_UpperI)
lp15@68488
   591
    show "\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> b"
lp15@68488
   592
      by (meson L Lower_memI Upper_memD b_inf_B greatest_le set_rev_mp)
lp15@68488
   593
    show "\<And>y. y \<in> Upper L A \<Longrightarrow> b \<sqsubseteq> y"
lp15@68488
   594
      by (auto elim: greatest_Lower_below [OF b_inf_B])
lp15@68488
   595
  qed (use L bcarr in auto)
wenzelm@67091
   596
  then show "\<exists>s. least L s (Upper L A)" ..
ballarin@65099
   597
next
ballarin@65099
   598
  fix A
ballarin@65099
   599
  assume L: "A \<subseteq> carrier L"
wenzelm@67091
   600
  show "\<exists>i. greatest L i (Lower L A)"
ballarin@65099
   601
  proof (cases "A = {}")
ballarin@65099
   602
    case True then show ?thesis
ballarin@65099
   603
      by (simp add: top_exists)
ballarin@65099
   604
  next
ballarin@65099
   605
    case False with L show ?thesis
ballarin@65099
   606
      by (rule inf_exists)
ballarin@65099
   607
  qed
ballarin@65099
   608
qed
ballarin@65099
   609
ballarin@65099
   610
(* TODO: prove dual version *)
ballarin@65099
   611
ballarin@65099
   612
subsection \<open>Fixed points\<close>
ballarin@65099
   613
ballarin@65099
   614
context complete_lattice
ballarin@65099
   615
begin
ballarin@65099
   616
ballarin@65099
   617
lemma LFP_unfold: 
ballarin@66580
   618
  "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> LFP f = f (LFP f)"
ballarin@65099
   619
  using eq_is_equal weak.LFP_weak_unfold by auto
ballarin@65099
   620
ballarin@65099
   621
lemma LFP_const:
ballarin@66580
   622
  "t \<in> carrier L \<Longrightarrow> LFP (\<lambda> x. t) = t"
ballarin@65099
   623
  by (simp add: local.le_antisym weak.LFP_greatest weak.LFP_lowerbound)
ballarin@65099
   624
ballarin@65099
   625
lemma LFP_id:
ballarin@66580
   626
  "LFP id = \<bottom>"
ballarin@65099
   627
  by (simp add: local.le_antisym weak.LFP_lowerbound)
ballarin@65099
   628
ballarin@65099
   629
lemma GFP_unfold:
ballarin@66580
   630
  "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> GFP f = f (GFP f)"
ballarin@65099
   631
  using eq_is_equal weak.GFP_weak_unfold by auto
ballarin@65099
   632
ballarin@65099
   633
lemma GFP_const:
ballarin@66580
   634
  "t \<in> carrier L \<Longrightarrow> GFP (\<lambda> x. t) = t"
ballarin@65099
   635
  by (simp add: local.le_antisym weak.GFP_least weak.GFP_upperbound)
ballarin@65099
   636
ballarin@65099
   637
lemma GFP_id:
ballarin@66580
   638
  "GFP id = \<top>"
ballarin@65099
   639
  using weak.GFP_upperbound by auto
ballarin@65099
   640
ballarin@65099
   641
end
ballarin@65099
   642
ballarin@65099
   643
ballarin@65099
   644
subsection \<open>Interval complete lattices\<close>
ballarin@65099
   645
  
ballarin@65099
   646
context weak_complete_lattice
ballarin@65099
   647
begin
ballarin@65099
   648
lp15@68488
   649
  lemma at_least_at_most_Sup: "\<lbrakk> a \<in> carrier L; b \<in> carrier L; a \<sqsubseteq> b \<rbrakk> \<Longrightarrow> \<Squnion> \<lbrace>a..b\<rbrace> .= b"
lp15@68488
   650
    by (rule weak_le_antisym [OF sup_least sup_upper]) (auto simp add: at_least_at_most_closed)
ballarin@65099
   651
lp15@68488
   652
  lemma at_least_at_most_Inf: "\<lbrakk> a \<in> carrier L; b \<in> carrier L; a \<sqsubseteq> b \<rbrakk> \<Longrightarrow> \<Sqinter> \<lbrace>a..b\<rbrace> .= a"
lp15@68488
   653
    by (rule weak_le_antisym [OF inf_lower inf_greatest]) (auto simp add: at_least_at_most_closed)
ballarin@65099
   654
ballarin@65099
   655
end
ballarin@65099
   656
ballarin@65099
   657
lemma weak_complete_lattice_interval:
ballarin@65099
   658
  assumes "weak_complete_lattice L" "a \<in> carrier L" "b \<in> carrier L" "a \<sqsubseteq>\<^bsub>L\<^esub> b"
ballarin@65099
   659
  shows "weak_complete_lattice (L \<lparr> carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub> \<rparr>)"
ballarin@65099
   660
proof -
ballarin@65099
   661
  interpret L: weak_complete_lattice L
ballarin@65099
   662
    by (simp add: assms)
ballarin@65099
   663
  interpret weak_partial_order "L \<lparr> carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub> \<rparr>"
ballarin@65099
   664
  proof -
ballarin@65099
   665
    have "\<lbrace>a..b\<rbrace>\<^bsub>L\<^esub> \<subseteq> carrier L"
lp15@68488
   666
      by (auto simp add: at_least_at_most_def)
ballarin@65099
   667
    thus "weak_partial_order (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>)"
ballarin@65099
   668
      by (simp add: L.weak_partial_order_axioms weak_partial_order_subset)
ballarin@65099
   669
  qed
ballarin@65099
   670
ballarin@65099
   671
  show ?thesis
ballarin@65099
   672
  proof
ballarin@65099
   673
    fix A
ballarin@65099
   674
    assume a: "A \<subseteq> carrier (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>)"
ballarin@65099
   675
    show "\<exists>s. is_lub (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>) s A"
ballarin@65099
   676
    proof (cases "A = {}")
ballarin@65099
   677
      case True
ballarin@65099
   678
      thus ?thesis
ballarin@65099
   679
        by (rule_tac x="a" in exI, auto simp add: least_def assms)
ballarin@65099
   680
    next
ballarin@65099
   681
      case False
ballarin@65099
   682
      show ?thesis
ballarin@65099
   683
      proof (rule_tac x="\<Squnion>\<^bsub>L\<^esub> A" in exI, rule least_UpperI, simp_all)
ballarin@65099
   684
        show b:"\<And> x. x \<in> A \<Longrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> \<Squnion>\<^bsub>L\<^esub>A"
ballarin@65099
   685
          using a by (auto intro: L.sup_upper, meson L.at_least_at_most_closed L.sup_upper subset_trans)
ballarin@65099
   686
        show "\<And>y. y \<in> Upper (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>) A \<Longrightarrow> \<Squnion>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> y"
ballarin@65099
   687
          using a L.at_least_at_most_closed by (rule_tac L.sup_least, auto intro: funcset_mem simp add: Upper_def)
ballarin@65099
   688
        from a show "A \<subseteq> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
ballarin@65099
   689
          by (auto)
ballarin@65099
   690
        from a show "\<Squnion>\<^bsub>L\<^esub>A \<in> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
ballarin@65099
   691
          apply (rule_tac L.at_least_at_most_member)
ballarin@65099
   692
          apply (auto)
ballarin@65099
   693
          apply (meson L.at_least_at_most_closed L.sup_closed subset_trans)
ballarin@65099
   694
          apply (meson False L.at_least_at_most_closed L.at_least_at_most_lower L.le_trans L.sup_closed b all_not_in_conv assms(2) contra_subsetD subset_trans)
ballarin@65099
   695
          apply (rule L.sup_least)
ballarin@65099
   696
          apply (auto simp add: assms)
ballarin@65099
   697
          using L.at_least_at_most_closed apply blast
ballarin@65099
   698
        done
ballarin@65099
   699
      qed
ballarin@65099
   700
    qed
ballarin@65099
   701
    show "\<exists>s. is_glb (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>) s A"
ballarin@65099
   702
    proof (cases "A = {}")
ballarin@65099
   703
      case True
ballarin@65099
   704
      thus ?thesis
ballarin@65099
   705
        by (rule_tac x="b" in exI, auto simp add: greatest_def assms)
ballarin@65099
   706
    next
ballarin@65099
   707
      case False
ballarin@65099
   708
      show ?thesis
ballarin@65099
   709
      proof (rule_tac x="\<Sqinter>\<^bsub>L\<^esub> A" in exI, rule greatest_LowerI, simp_all)
ballarin@65099
   710
        show b:"\<And>x. x \<in> A \<Longrightarrow> \<Sqinter>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> x"
ballarin@65099
   711
          using a L.at_least_at_most_closed by (force intro!: L.inf_lower)
ballarin@65099
   712
        show "\<And>y. y \<in> Lower (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>) A \<Longrightarrow> y \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>L\<^esub>A"
ballarin@65099
   713
           using a L.at_least_at_most_closed by (rule_tac L.inf_greatest, auto intro: funcset_carrier' simp add: Lower_def)
ballarin@65099
   714
        from a show "A \<subseteq> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
ballarin@65099
   715
          by (auto)
ballarin@65099
   716
        from a show "\<Sqinter>\<^bsub>L\<^esub>A \<in> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
ballarin@65099
   717
          apply (rule_tac L.at_least_at_most_member)
ballarin@65099
   718
          apply (auto)
ballarin@65099
   719
          apply (meson L.at_least_at_most_closed L.inf_closed subset_trans)
ballarin@65099
   720
          apply (meson L.at_least_at_most_closed L.at_least_at_most_lower L.inf_greatest assms(2) set_rev_mp subset_trans)
ballarin@65099
   721
          apply (meson False L.at_least_at_most_closed L.at_least_at_most_upper L.inf_closed L.le_trans b all_not_in_conv assms(3) contra_subsetD subset_trans)            
ballarin@65099
   722
        done
ballarin@65099
   723
      qed
ballarin@65099
   724
    qed
ballarin@65099
   725
  qed
ballarin@65099
   726
qed
ballarin@65099
   727
ballarin@65099
   728
ballarin@65099
   729
subsection \<open>Knaster-Tarski theorem and variants\<close>
ballarin@65099
   730
  
ballarin@65099
   731
text \<open>The set of fixed points of a complete lattice is itself a complete lattice\<close>
ballarin@65099
   732
ballarin@65099
   733
theorem Knaster_Tarski:
ballarin@65099
   734
  assumes "weak_complete_lattice L" "f \<in> carrier L \<rightarrow> carrier L" "isotone L L f"
ballarin@65099
   735
  shows "weak_complete_lattice (fpl L f)" (is "weak_complete_lattice ?L'")
ballarin@65099
   736
proof -
ballarin@65099
   737
  interpret L: weak_complete_lattice L
ballarin@65099
   738
    by (simp add: assms)
ballarin@65099
   739
  interpret weak_partial_order ?L'
ballarin@65099
   740
  proof -
ballarin@65099
   741
    have "{x \<in> carrier L. f x .=\<^bsub>L\<^esub> x} \<subseteq> carrier L"
ballarin@65099
   742
      by (auto)
ballarin@65099
   743
    thus "weak_partial_order ?L'"
ballarin@65099
   744
      by (simp add: L.weak_partial_order_axioms weak_partial_order_subset)
ballarin@65099
   745
  qed
ballarin@65099
   746
  show ?thesis
ballarin@65099
   747
  proof (unfold_locales, simp_all)
ballarin@65099
   748
    fix A
ballarin@65099
   749
    assume A: "A \<subseteq> fps L f"
ballarin@65099
   750
    show "\<exists>s. is_lub (fpl L f) s A"
ballarin@65099
   751
    proof
ballarin@65099
   752
      from A have AL: "A \<subseteq> carrier L"
ballarin@65099
   753
        by (meson fps_carrier subset_eq)
ballarin@65099
   754
ballarin@65099
   755
      let ?w = "\<Squnion>\<^bsub>L\<^esub> A"
ballarin@65099
   756
      have w: "f (\<Squnion>\<^bsub>L\<^esub>A) \<in> carrier L"
ballarin@65099
   757
        by (rule funcset_mem[of f "carrier L"], simp_all add: AL assms(2))
ballarin@65099
   758
ballarin@65099
   759
      have pf_w: "(\<Squnion>\<^bsub>L\<^esub> A) \<sqsubseteq>\<^bsub>L\<^esub> f (\<Squnion>\<^bsub>L\<^esub> A)"
ballarin@65099
   760
        by (simp add: A L.weak_sup_pre_fixed_point assms(2) assms(3))
ballarin@65099
   761
ballarin@65099
   762
      have f_top_chain: "f ` \<lbrace>?w..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub> \<subseteq> \<lbrace>?w..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>"
ballarin@65099
   763
      proof (auto simp add: at_least_at_most_def)
ballarin@65099
   764
        fix x
ballarin@65099
   765
        assume b: "x \<in> carrier L" "\<Squnion>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> x"
ballarin@65099
   766
        from b show fx: "f x \<in> carrier L"
ballarin@65099
   767
          using assms(2) by blast
ballarin@65099
   768
        show "\<Squnion>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> f x"
ballarin@65099
   769
        proof -
ballarin@65099
   770
          have "?w \<sqsubseteq>\<^bsub>L\<^esub> f ?w"
ballarin@65099
   771
          proof (rule_tac L.sup_least, simp_all add: AL w)
ballarin@65099
   772
            fix y
ballarin@65099
   773
            assume c: "y \<in> A" 
ballarin@65099
   774
            hence y: "y \<in> fps L f"
ballarin@65099
   775
              using A subsetCE by blast
ballarin@65099
   776
            with assms have "y .=\<^bsub>L\<^esub> f y"
ballarin@65099
   777
            proof -
ballarin@65099
   778
              from y have "y \<in> carrier L"
ballarin@65099
   779
                by (simp add: fps_def)
ballarin@65099
   780
              moreover hence "f y \<in> carrier L"
ballarin@65099
   781
                by (rule_tac funcset_mem[of f "carrier L"], simp_all add: assms)
ballarin@65099
   782
              ultimately show ?thesis using y
ballarin@65099
   783
                by (rule_tac L.sym, simp_all add: L.use_fps)
ballarin@65099
   784
            qed              
ballarin@65099
   785
            moreover have "y \<sqsubseteq>\<^bsub>L\<^esub> \<Squnion>\<^bsub>L\<^esub>A"
ballarin@65099
   786
              by (simp add: AL L.sup_upper c(1))
ballarin@65099
   787
            ultimately show "y \<sqsubseteq>\<^bsub>L\<^esub> f (\<Squnion>\<^bsub>L\<^esub>A)"
ballarin@65099
   788
              by (meson fps_def AL funcset_mem L.refl L.weak_complete_lattice_axioms assms(2) assms(3) c(1) isotone_def rev_subsetD weak_complete_lattice.sup_closed weak_partial_order.le_cong)
ballarin@65099
   789
          qed
ballarin@65099
   790
          thus ?thesis
ballarin@65099
   791
            by (meson AL funcset_mem L.le_trans L.sup_closed assms(2) assms(3) b(1) b(2) use_iso2)
ballarin@65099
   792
        qed
ballarin@65099
   793
   
ballarin@65099
   794
        show "f x \<sqsubseteq>\<^bsub>L\<^esub> \<top>\<^bsub>L\<^esub>"
ballarin@65099
   795
          by (simp add: fx)
ballarin@65099
   796
      qed
ballarin@65099
   797
  
ballarin@65099
   798
      let ?L' = "L\<lparr> carrier := \<lbrace>?w..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub> \<rparr>"
ballarin@65099
   799
ballarin@65099
   800
      interpret L': weak_complete_lattice ?L'
ballarin@65099
   801
        by (auto intro: weak_complete_lattice_interval simp add: L.weak_complete_lattice_axioms AL)
ballarin@65099
   802
ballarin@65099
   803
      let ?L'' = "L\<lparr> carrier := fps L f \<rparr>"
ballarin@65099
   804
ballarin@66580
   805
      show "is_lub ?L'' (LFP\<^bsub>?L'\<^esub> f) A"
ballarin@65099
   806
      proof (rule least_UpperI, simp_all)
ballarin@65099
   807
        fix x
ballarin@65099
   808
        assume "x \<in> Upper ?L'' A"
ballarin@66580
   809
        hence "LFP\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>?L'\<^esub> x"
ballarin@65099
   810
          apply (rule_tac L'.LFP_lowerbound)
ballarin@65099
   811
          apply (auto simp add: Upper_def)
ballarin@65099
   812
          apply (simp add: A AL L.at_least_at_most_member L.sup_least set_rev_mp)          
ballarin@65099
   813
          apply (simp add: Pi_iff assms(2) fps_def, rule_tac L.weak_refl)
ballarin@65099
   814
          apply (auto)
ballarin@65099
   815
          apply (rule funcset_mem[of f "carrier L"], simp_all add: assms(2))
ballarin@65099
   816
        done
ballarin@66580
   817
        thus " LFP\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> x"
ballarin@65099
   818
          by (simp)
ballarin@65099
   819
      next
ballarin@65099
   820
        fix x
ballarin@65099
   821
        assume xA: "x \<in> A"
ballarin@66580
   822
        show "x \<sqsubseteq>\<^bsub>L\<^esub> LFP\<^bsub>?L'\<^esub> f"
ballarin@65099
   823
        proof -
ballarin@66580
   824
          have "LFP\<^bsub>?L'\<^esub> f \<in> carrier ?L'"
ballarin@65099
   825
            by blast
ballarin@65099
   826
          thus ?thesis
ballarin@65099
   827
            by (simp, meson AL L.at_least_at_most_closed L.at_least_at_most_lower L.le_trans L.sup_closed L.sup_upper xA subsetCE)
ballarin@65099
   828
        qed
ballarin@65099
   829
      next
ballarin@65099
   830
        show "A \<subseteq> fps L f"
ballarin@65099
   831
          by (simp add: A)
ballarin@65099
   832
      next
ballarin@66580
   833
        show "LFP\<^bsub>?L'\<^esub> f \<in> fps L f"
ballarin@65099
   834
        proof (auto simp add: fps_def)
ballarin@66580
   835
          have "LFP\<^bsub>?L'\<^esub> f \<in> carrier ?L'"
ballarin@65099
   836
            by (rule L'.LFP_closed)
ballarin@66580
   837
          thus c:"LFP\<^bsub>?L'\<^esub> f \<in> carrier L"
ballarin@65099
   838
             by (auto simp add: at_least_at_most_def)
ballarin@66580
   839
          have "LFP\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (LFP\<^bsub>?L'\<^esub> f)"
ballarin@65099
   840
          proof (rule "L'.LFP_weak_unfold", simp_all)
ballarin@65099
   841
            show "f \<in> \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub> \<rightarrow> \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>"
ballarin@65099
   842
              apply (auto simp add: Pi_def at_least_at_most_def)
ballarin@65099
   843
              using assms(2) apply blast
ballarin@65099
   844
              apply (meson AL funcset_mem L.le_trans L.sup_closed assms(2) assms(3) pf_w use_iso2)
ballarin@65099
   845
              using assms(2) apply blast
ballarin@65099
   846
            done
ballarin@65099
   847
            from assms(3) show "Mono\<^bsub>L\<lparr>carrier := \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>\<rparr>\<^esub> f"
ballarin@65099
   848
              apply (auto simp add: isotone_def)
ballarin@65099
   849
              using L'.weak_partial_order_axioms apply blast
ballarin@65099
   850
              apply (meson L.at_least_at_most_closed subsetCE)
ballarin@65099
   851
            done
ballarin@65099
   852
          qed
ballarin@66580
   853
          thus "f (LFP\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> LFP\<^bsub>?L'\<^esub> f"
ballarin@65099
   854
            by (simp add: L.equivalence_axioms funcset_carrier' c assms(2) equivalence.sym) 
ballarin@65099
   855
        qed
ballarin@65099
   856
      qed
ballarin@65099
   857
    qed
ballarin@65099
   858
    show "\<exists>i. is_glb (L\<lparr>carrier := fps L f\<rparr>) i A"
ballarin@65099
   859
    proof
ballarin@65099
   860
      from A have AL: "A \<subseteq> carrier L"
ballarin@65099
   861
        by (meson fps_carrier subset_eq)
ballarin@65099
   862
ballarin@65099
   863
      let ?w = "\<Sqinter>\<^bsub>L\<^esub> A"
ballarin@65099
   864
      have w: "f (\<Sqinter>\<^bsub>L\<^esub>A) \<in> carrier L"
ballarin@65099
   865
        by (simp add: AL funcset_carrier' assms(2))
ballarin@65099
   866
ballarin@65099
   867
      have pf_w: "f (\<Sqinter>\<^bsub>L\<^esub> A) \<sqsubseteq>\<^bsub>L\<^esub> (\<Sqinter>\<^bsub>L\<^esub> A)"
ballarin@65099
   868
        by (simp add: A L.weak_sup_post_fixed_point assms(2) assms(3))
ballarin@65099
   869
ballarin@65099
   870
      have f_bot_chain: "f ` \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub> \<subseteq> \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub>"
ballarin@65099
   871
      proof (auto simp add: at_least_at_most_def)
ballarin@65099
   872
        fix x
ballarin@65099
   873
        assume b: "x \<in> carrier L" "x \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>L\<^esub>A"
ballarin@65099
   874
        from b show fx: "f x \<in> carrier L"
ballarin@65099
   875
          using assms(2) by blast
ballarin@65099
   876
        show "f x \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>L\<^esub>A"
ballarin@65099
   877
        proof -
ballarin@65099
   878
          have "f ?w \<sqsubseteq>\<^bsub>L\<^esub> ?w"
ballarin@65099
   879
          proof (rule_tac L.inf_greatest, simp_all add: AL w)
ballarin@65099
   880
            fix y
ballarin@65099
   881
            assume c: "y \<in> A" 
ballarin@65099
   882
            with assms have "y .=\<^bsub>L\<^esub> f y"
ballarin@65099
   883
              by (metis (no_types, lifting) A funcset_carrier'[OF assms(2)] L.sym fps_def mem_Collect_eq subset_eq)
ballarin@65099
   884
            moreover have "\<Sqinter>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> y"
ballarin@65099
   885
              by (simp add: AL L.inf_lower c)
ballarin@65099
   886
            ultimately show "f (\<Sqinter>\<^bsub>L\<^esub>A) \<sqsubseteq>\<^bsub>L\<^esub> y"
ballarin@65099
   887
              by (meson AL L.inf_closed L.le_trans c pf_w set_rev_mp w)
ballarin@65099
   888
          qed
ballarin@65099
   889
          thus ?thesis
ballarin@65099
   890
            by (meson AL L.inf_closed L.le_trans assms(3) b(1) b(2) fx use_iso2 w)
ballarin@65099
   891
        qed
ballarin@65099
   892
   
ballarin@65099
   893
        show "\<bottom>\<^bsub>L\<^esub> \<sqsubseteq>\<^bsub>L\<^esub> f x"
ballarin@65099
   894
          by (simp add: fx)
ballarin@65099
   895
      qed
ballarin@65099
   896
  
ballarin@65099
   897
      let ?L' = "L\<lparr> carrier := \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub> \<rparr>"
ballarin@65099
   898
ballarin@65099
   899
      interpret L': weak_complete_lattice ?L'
ballarin@65099
   900
        by (auto intro!: weak_complete_lattice_interval simp add: L.weak_complete_lattice_axioms AL)
ballarin@65099
   901
ballarin@65099
   902
      let ?L'' = "L\<lparr> carrier := fps L f \<rparr>"
ballarin@65099
   903
ballarin@66580
   904
      show "is_glb ?L'' (GFP\<^bsub>?L'\<^esub> f) A"
ballarin@65099
   905
      proof (rule greatest_LowerI, simp_all)
ballarin@65099
   906
        fix x
ballarin@65099
   907
        assume "x \<in> Lower ?L'' A"
ballarin@66580
   908
        hence "x \<sqsubseteq>\<^bsub>?L'\<^esub> GFP\<^bsub>?L'\<^esub> f"
ballarin@65099
   909
          apply (rule_tac L'.GFP_upperbound)
ballarin@65099
   910
          apply (auto simp add: Lower_def)
ballarin@65099
   911
          apply (meson A AL L.at_least_at_most_member L.bottom_lower L.weak_complete_lattice_axioms fps_carrier subsetCE weak_complete_lattice.inf_greatest)
ballarin@65099
   912
          apply (simp add: funcset_carrier' L.sym assms(2) fps_def)          
ballarin@65099
   913
        done
ballarin@66580
   914
        thus "x \<sqsubseteq>\<^bsub>L\<^esub> GFP\<^bsub>?L'\<^esub> f"
ballarin@65099
   915
          by (simp)
ballarin@65099
   916
      next
ballarin@65099
   917
        fix x
ballarin@65099
   918
        assume xA: "x \<in> A"
ballarin@66580
   919
        show "GFP\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> x"
ballarin@65099
   920
        proof -
ballarin@66580
   921
          have "GFP\<^bsub>?L'\<^esub> f \<in> carrier ?L'"
ballarin@65099
   922
            by blast
ballarin@65099
   923
          thus ?thesis
ballarin@65099
   924
            by (simp, meson AL L.at_least_at_most_closed L.at_least_at_most_upper L.inf_closed L.inf_lower L.le_trans subsetCE xA)     
ballarin@65099
   925
        qed
ballarin@65099
   926
      next
ballarin@65099
   927
        show "A \<subseteq> fps L f"
ballarin@65099
   928
          by (simp add: A)
ballarin@65099
   929
      next
ballarin@66580
   930
        show "GFP\<^bsub>?L'\<^esub> f \<in> fps L f"
ballarin@65099
   931
        proof (auto simp add: fps_def)
ballarin@66580
   932
          have "GFP\<^bsub>?L'\<^esub> f \<in> carrier ?L'"
ballarin@65099
   933
            by (rule L'.GFP_closed)
ballarin@66580
   934
          thus c:"GFP\<^bsub>?L'\<^esub> f \<in> carrier L"
ballarin@65099
   935
             by (auto simp add: at_least_at_most_def)
ballarin@66580
   936
          have "GFP\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (GFP\<^bsub>?L'\<^esub> f)"
ballarin@65099
   937
          proof (rule "L'.GFP_weak_unfold", simp_all)
ballarin@65099
   938
            show "f \<in> \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub> \<rightarrow> \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub>"
ballarin@65099
   939
              apply (auto simp add: Pi_def at_least_at_most_def)
ballarin@65099
   940
              using assms(2) apply blast
ballarin@65099
   941
              apply (simp add: funcset_carrier' assms(2))
ballarin@65099
   942
              apply (meson AL funcset_carrier L.inf_closed L.le_trans assms(2) assms(3) pf_w use_iso2)
ballarin@65099
   943
            done
ballarin@65099
   944
            from assms(3) show "Mono\<^bsub>L\<lparr>carrier := \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub>\<rparr>\<^esub> f"
ballarin@65099
   945
              apply (auto simp add: isotone_def)
ballarin@65099
   946
              using L'.weak_partial_order_axioms apply blast
ballarin@65099
   947
              using L.at_least_at_most_closed apply (blast intro: funcset_carrier')
ballarin@65099
   948
            done
ballarin@65099
   949
          qed
ballarin@66580
   950
          thus "f (GFP\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> GFP\<^bsub>?L'\<^esub> f"
ballarin@65099
   951
            by (simp add: L.equivalence_axioms funcset_carrier' c assms(2) equivalence.sym) 
ballarin@65099
   952
        qed
ballarin@65099
   953
      qed
ballarin@65099
   954
    qed
ballarin@65099
   955
  qed
ballarin@65099
   956
qed
ballarin@65099
   957
ballarin@65099
   958
theorem Knaster_Tarski_top:
ballarin@65099
   959
  assumes "weak_complete_lattice L" "isotone L L f" "f \<in> carrier L \<rightarrow> carrier L"
ballarin@66580
   960
  shows "\<top>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> GFP\<^bsub>L\<^esub> f"
ballarin@65099
   961
proof -
ballarin@65099
   962
  interpret L: weak_complete_lattice L
ballarin@65099
   963
    by (simp add: assms)
ballarin@65099
   964
  interpret L': weak_complete_lattice "fpl L f"
ballarin@65099
   965
    by (rule Knaster_Tarski, simp_all add: assms)
ballarin@65099
   966
  show ?thesis
ballarin@65099
   967
  proof (rule L.weak_le_antisym, simp_all)
ballarin@66580
   968
    show "\<top>\<^bsub>fpl L f\<^esub> \<sqsubseteq>\<^bsub>L\<^esub> GFP\<^bsub>L\<^esub> f"
ballarin@65099
   969
      by (rule L.GFP_greatest_fixed_point, simp_all add: assms L'.top_closed[simplified])
ballarin@66580
   970
    show "GFP\<^bsub>L\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> \<top>\<^bsub>fpl L f\<^esub>"
ballarin@65099
   971
    proof -
ballarin@66580
   972
      have "GFP\<^bsub>L\<^esub> f \<in> fps L f"
ballarin@65099
   973
        by (rule L.GFP_fixed_point, simp_all add: assms)
ballarin@66580
   974
      hence "GFP\<^bsub>L\<^esub> f \<in> carrier (fpl L f)"
ballarin@65099
   975
        by simp
ballarin@66580
   976
      hence "GFP\<^bsub>L\<^esub> f \<sqsubseteq>\<^bsub>fpl L f\<^esub> \<top>\<^bsub>fpl L f\<^esub>"
ballarin@65099
   977
        by (rule L'.top_higher)
ballarin@65099
   978
      thus ?thesis
ballarin@65099
   979
        by simp
ballarin@65099
   980
    qed
ballarin@65099
   981
    show "\<top>\<^bsub>fpl L f\<^esub> \<in> carrier L"
ballarin@65099
   982
    proof -
ballarin@65099
   983
      have "carrier (fpl L f) \<subseteq> carrier L"
ballarin@65099
   984
        by (auto simp add: fps_def)
ballarin@65099
   985
      with L'.top_closed show ?thesis
ballarin@65099
   986
        by blast
ballarin@65099
   987
    qed
ballarin@65099
   988
  qed
ballarin@65099
   989
qed
ballarin@65099
   990
ballarin@65099
   991
theorem Knaster_Tarski_bottom:
ballarin@65099
   992
  assumes "weak_complete_lattice L" "isotone L L f" "f \<in> carrier L \<rightarrow> carrier L"
ballarin@66580
   993
  shows "\<bottom>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> LFP\<^bsub>L\<^esub> f"
ballarin@65099
   994
proof -
ballarin@65099
   995
  interpret L: weak_complete_lattice L
ballarin@65099
   996
    by (simp add: assms)
ballarin@65099
   997
  interpret L': weak_complete_lattice "fpl L f"
ballarin@65099
   998
    by (rule Knaster_Tarski, simp_all add: assms)
ballarin@65099
   999
  show ?thesis
ballarin@65099
  1000
  proof (rule L.weak_le_antisym, simp_all)
ballarin@66580
  1001
    show "LFP\<^bsub>L\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> \<bottom>\<^bsub>fpl L f\<^esub>"
ballarin@65099
  1002
      by (rule L.LFP_least_fixed_point, simp_all add: assms L'.bottom_closed[simplified])
ballarin@66580
  1003
    show "\<bottom>\<^bsub>fpl L f\<^esub> \<sqsubseteq>\<^bsub>L\<^esub> LFP\<^bsub>L\<^esub> f"
ballarin@65099
  1004
    proof -
ballarin@66580
  1005
      have "LFP\<^bsub>L\<^esub> f \<in> fps L f"
ballarin@65099
  1006
        by (rule L.LFP_fixed_point, simp_all add: assms)
ballarin@66580
  1007
      hence "LFP\<^bsub>L\<^esub> f \<in> carrier (fpl L f)"
ballarin@65099
  1008
        by simp
ballarin@66580
  1009
      hence "\<bottom>\<^bsub>fpl L f\<^esub> \<sqsubseteq>\<^bsub>fpl L f\<^esub> LFP\<^bsub>L\<^esub> f"
ballarin@65099
  1010
        by (rule L'.bottom_lower)
ballarin@65099
  1011
      thus ?thesis
ballarin@65099
  1012
        by simp
ballarin@65099
  1013
    qed
ballarin@65099
  1014
    show "\<bottom>\<^bsub>fpl L f\<^esub> \<in> carrier L"
ballarin@65099
  1015
    proof -
ballarin@65099
  1016
      have "carrier (fpl L f) \<subseteq> carrier L"
ballarin@65099
  1017
        by (auto simp add: fps_def)
ballarin@65099
  1018
      with L'.bottom_closed show ?thesis
ballarin@65099
  1019
        by blast
ballarin@65099
  1020
    qed
ballarin@65099
  1021
  qed
ballarin@65099
  1022
qed
ballarin@65099
  1023
ballarin@65099
  1024
text \<open>If a function is both idempotent and isotone then the image of the function forms a complete lattice\<close>
ballarin@65099
  1025
  
ballarin@65099
  1026
theorem Knaster_Tarski_idem:
ballarin@65099
  1027
  assumes "complete_lattice L" "f \<in> carrier L \<rightarrow> carrier L" "isotone L L f" "idempotent L f"
ballarin@65099
  1028
  shows "complete_lattice (L\<lparr>carrier := f ` carrier L\<rparr>)"
ballarin@65099
  1029
proof -
ballarin@65099
  1030
  interpret L: complete_lattice L
ballarin@65099
  1031
    by (simp add: assms)
ballarin@65099
  1032
  have "fps L f = f ` carrier L"
ballarin@65099
  1033
    using L.weak.fps_idem[OF assms(2) assms(4)]
ballarin@65099
  1034
    by (simp add: L.set_eq_is_eq)
ballarin@65099
  1035
  then interpret L': weak_complete_lattice "(L\<lparr>carrier := f ` carrier L\<rparr>)"
ballarin@65099
  1036
    by (metis Knaster_Tarski L.weak.weak_complete_lattice_axioms assms(2) assms(3))
ballarin@65099
  1037
  show ?thesis
ballarin@65099
  1038
    using L'.sup_exists L'.inf_exists
ballarin@65099
  1039
    by (unfold_locales, auto simp add: L.eq_is_equal)
ballarin@65099
  1040
qed
ballarin@65099
  1041
ballarin@65099
  1042
theorem Knaster_Tarski_idem_extremes:
ballarin@65099
  1043
  assumes "weak_complete_lattice L" "isotone L L f" "idempotent L f" "f \<in> carrier L \<rightarrow> carrier L"
ballarin@65099
  1044
  shows "\<top>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> f (\<top>\<^bsub>L\<^esub>)" "\<bottom>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> f (\<bottom>\<^bsub>L\<^esub>)"
ballarin@65099
  1045
proof -
ballarin@65099
  1046
  interpret L: weak_complete_lattice "L"
ballarin@65099
  1047
    by (simp_all add: assms)
ballarin@65099
  1048
  interpret L': weak_complete_lattice "fpl L f"
ballarin@65099
  1049
    by (rule Knaster_Tarski, simp_all add: assms)
ballarin@65099
  1050
  have FA: "fps L f \<subseteq> carrier L"
ballarin@65099
  1051
    by (auto simp add: fps_def)
ballarin@65099
  1052
  show "\<top>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> f (\<top>\<^bsub>L\<^esub>)"
ballarin@65099
  1053
  proof -
ballarin@65099
  1054
    from FA have "\<top>\<^bsub>fpl L f\<^esub> \<in> carrier L"
ballarin@65099
  1055
    proof -
ballarin@65099
  1056
      have "\<top>\<^bsub>fpl L f\<^esub> \<in> fps L f"
ballarin@65099
  1057
        using L'.top_closed by auto
ballarin@65099
  1058
      thus ?thesis
ballarin@65099
  1059
        using FA by blast
ballarin@65099
  1060
    qed
ballarin@65099
  1061
    moreover with assms have "f \<top>\<^bsub>L\<^esub> \<in> carrier L"
ballarin@65099
  1062
      by (auto)
ballarin@65099
  1063
ballarin@65099
  1064
    ultimately show ?thesis
ballarin@65099
  1065
      using L.trans[OF Knaster_Tarski_top[of L f] L.GFP_idem[of f]]
ballarin@65099
  1066
      by (simp_all add: assms)
ballarin@65099
  1067
  qed
ballarin@65099
  1068
  show "\<bottom>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> f (\<bottom>\<^bsub>L\<^esub>)"
ballarin@65099
  1069
  proof -
ballarin@65099
  1070
    from FA have "\<bottom>\<^bsub>fpl L f\<^esub> \<in> carrier L"
ballarin@65099
  1071
    proof -
ballarin@65099
  1072
      have "\<bottom>\<^bsub>fpl L f\<^esub> \<in> fps L f"
ballarin@65099
  1073
        using L'.bottom_closed by auto
ballarin@65099
  1074
      thus ?thesis
ballarin@65099
  1075
        using FA by blast
ballarin@65099
  1076
    qed
ballarin@65099
  1077
    moreover with assms have "f \<bottom>\<^bsub>L\<^esub> \<in> carrier L"
ballarin@65099
  1078
      by (auto)
ballarin@65099
  1079
ballarin@65099
  1080
    ultimately show ?thesis
ballarin@65099
  1081
      using L.trans[OF Knaster_Tarski_bottom[of L f] L.LFP_idem[of f]]
ballarin@65099
  1082
      by (simp_all add: assms)
ballarin@65099
  1083
  qed
ballarin@65099
  1084
qed
ballarin@65099
  1085
ballarin@66187
  1086
theorem Knaster_Tarski_idem_inf_eq:
ballarin@66187
  1087
  assumes "weak_complete_lattice L" "isotone L L f" "idempotent L f" "f \<in> carrier L \<rightarrow> carrier L"
ballarin@66187
  1088
          "A \<subseteq> fps L f"
ballarin@66187
  1089
  shows "\<Sqinter>\<^bsub>fpl L f\<^esub> A .=\<^bsub>L\<^esub> f (\<Sqinter>\<^bsub>L\<^esub> A)"
ballarin@66187
  1090
proof -
ballarin@66187
  1091
  interpret L: weak_complete_lattice "L"
ballarin@66187
  1092
    by (simp_all add: assms)
ballarin@66187
  1093
  interpret L': weak_complete_lattice "fpl L f"
ballarin@66187
  1094
    by (rule Knaster_Tarski, simp_all add: assms)
ballarin@66187
  1095
  have FA: "fps L f \<subseteq> carrier L"
ballarin@66187
  1096
    by (auto simp add: fps_def)
ballarin@66187
  1097
  have A: "A \<subseteq> carrier L"
ballarin@66187
  1098
    using FA assms(5) by blast
ballarin@66187
  1099
  have fA: "f (\<Sqinter>\<^bsub>L\<^esub>A) \<in> fps L f"
ballarin@66187
  1100
    by (metis (no_types, lifting) A L.idempotent L.inf_closed PiE assms(3) assms(4) fps_def mem_Collect_eq)
ballarin@66187
  1101
  have infA: "\<Sqinter>\<^bsub>fpl L f\<^esub>A \<in> fps L f"
ballarin@66187
  1102
    by (rule L'.inf_closed[simplified], simp add: assms)
ballarin@66187
  1103
  show ?thesis
ballarin@66187
  1104
  proof (rule L.weak_le_antisym)
ballarin@66187
  1105
    show ic: "\<Sqinter>\<^bsub>fpl L f\<^esub>A \<in> carrier L"
ballarin@66187
  1106
      using FA infA by blast
ballarin@66187
  1107
    show fc: "f (\<Sqinter>\<^bsub>L\<^esub>A) \<in> carrier L"
ballarin@66187
  1108
      using FA fA by blast
ballarin@66187
  1109
    show "f (\<Sqinter>\<^bsub>L\<^esub>A) \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>fpl L f\<^esub>A"
ballarin@66187
  1110
    proof -
ballarin@66187
  1111
      have "\<And>x. x \<in> A \<Longrightarrow> f (\<Sqinter>\<^bsub>L\<^esub>A) \<sqsubseteq>\<^bsub>L\<^esub> x"
ballarin@66187
  1112
        by (meson A FA L.inf_closed L.inf_lower L.le_trans L.weak_sup_post_fixed_point assms(2) assms(4) assms(5) fA subsetCE)
ballarin@66187
  1113
      hence "f (\<Sqinter>\<^bsub>L\<^esub>A) \<sqsubseteq>\<^bsub>fpl L f\<^esub> \<Sqinter>\<^bsub>fpl L f\<^esub>A"
ballarin@66187
  1114
        by (rule_tac L'.inf_greatest, simp_all add: fA assms(3,5))
ballarin@66187
  1115
      thus ?thesis
ballarin@66187
  1116
        by (simp)
ballarin@66187
  1117
    qed
ballarin@66187
  1118
    show "\<Sqinter>\<^bsub>fpl L f\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> f (\<Sqinter>\<^bsub>L\<^esub>A)"
ballarin@66187
  1119
    proof -
ballarin@66187
  1120
      have "\<And>x. x \<in> A \<Longrightarrow> \<Sqinter>\<^bsub>fpl L f\<^esub>A \<sqsubseteq>\<^bsub>fpl L f\<^esub> x"
ballarin@66187
  1121
        by (rule L'.inf_lower, simp_all add: assms)
ballarin@66187
  1122
      hence "\<Sqinter>\<^bsub>fpl L f\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> (\<Sqinter>\<^bsub>L\<^esub>A)"
ballarin@66187
  1123
        apply (rule_tac L.inf_greatest, simp_all add: A)
ballarin@66187
  1124
        using FA infA apply blast
ballarin@66187
  1125
        done
ballarin@66187
  1126
      hence 1:"f(\<Sqinter>\<^bsub>fpl L f\<^esub>A) \<sqsubseteq>\<^bsub>L\<^esub> f(\<Sqinter>\<^bsub>L\<^esub>A)"
ballarin@66187
  1127
        by (metis (no_types, lifting) A FA L.inf_closed assms(2) infA subsetCE use_iso1)
ballarin@66187
  1128
      have 2:"\<Sqinter>\<^bsub>fpl L f\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> f (\<Sqinter>\<^bsub>fpl L f\<^esub>A)"
ballarin@66187
  1129
        by (metis (no_types, lifting) FA L.sym L.use_fps L.weak_complete_lattice_axioms PiE assms(4) infA subsetCE weak_complete_lattice_def weak_partial_order.weak_refl)
ballarin@66187
  1130
        
ballarin@66187
  1131
      show ?thesis  
ballarin@66187
  1132
        using FA fA infA by (auto intro!: L.le_trans[OF 2 1] ic fc, metis FA PiE assms(4) subsetCE)
ballarin@66187
  1133
    qed
ballarin@66187
  1134
  qed
ballarin@66187
  1135
qed  
ballarin@65099
  1136
ballarin@65099
  1137
subsection \<open>Examples\<close>
ballarin@65099
  1138
ballarin@65099
  1139
subsubsection \<open>The Powerset of a Set is a Complete Lattice\<close>
ballarin@65099
  1140
ballarin@65099
  1141
theorem powerset_is_complete_lattice:
nipkow@67399
  1142
  "complete_lattice \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr>"
ballarin@65099
  1143
  (is "complete_lattice ?L")
ballarin@65099
  1144
proof (rule partial_order.complete_latticeI)
ballarin@65099
  1145
  show "partial_order ?L"
ballarin@65099
  1146
    by standard auto
ballarin@65099
  1147
next
ballarin@65099
  1148
  fix B
ballarin@65099
  1149
  assume "B \<subseteq> carrier ?L"
ballarin@65099
  1150
  then have "least ?L (\<Union> B) (Upper ?L B)"
ballarin@65099
  1151
    by (fastforce intro!: least_UpperI simp: Upper_def)
wenzelm@67091
  1152
  then show "\<exists>s. least ?L s (Upper ?L B)" ..
ballarin@65099
  1153
next
ballarin@65099
  1154
  fix B
ballarin@65099
  1155
  assume "B \<subseteq> carrier ?L"
ballarin@65099
  1156
  then have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
ballarin@65099
  1157
    txt \<open>@{term "\<Inter> B"} is not the infimum of @{term B}:
ballarin@65099
  1158
      @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! \<close>
ballarin@65099
  1159
    by (fastforce intro!: greatest_LowerI simp: Lower_def)
wenzelm@67091
  1160
  then show "\<exists>i. greatest ?L i (Lower ?L B)" ..
ballarin@65099
  1161
qed
ballarin@65099
  1162
ballarin@66579
  1163
text \<open>Another example, that of the lattice of subgroups of a group,
ballarin@66579
  1164
  can be found in Group theory (Section~\ref{sec:subgroup-lattice}).\<close>
ballarin@65099
  1165
ballarin@65099
  1166
ballarin@65099
  1167
subsection \<open>Limit preserving functions\<close>
ballarin@65099
  1168
ballarin@65099
  1169
definition weak_sup_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
ballarin@65099
  1170
"weak_sup_pres X Y f \<equiv> complete_lattice X \<and> complete_lattice Y \<and> (\<forall> A \<subseteq> carrier X. A \<noteq> {} \<longrightarrow> f (\<Squnion>\<^bsub>X\<^esub> A) = (\<Squnion>\<^bsub>Y\<^esub> (f ` A)))"
ballarin@65099
  1171
ballarin@65099
  1172
definition sup_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
ballarin@65099
  1173
"sup_pres X Y f \<equiv> complete_lattice X \<and> complete_lattice Y \<and> (\<forall> A \<subseteq> carrier X. f (\<Squnion>\<^bsub>X\<^esub> A) = (\<Squnion>\<^bsub>Y\<^esub> (f ` A)))"
ballarin@65099
  1174
ballarin@65099
  1175
definition weak_inf_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
ballarin@65099
  1176
"weak_inf_pres X Y f \<equiv> complete_lattice X \<and> complete_lattice Y \<and> (\<forall> A \<subseteq> carrier X. A \<noteq> {} \<longrightarrow> f (\<Sqinter>\<^bsub>X\<^esub> A) = (\<Sqinter>\<^bsub>Y\<^esub> (f ` A)))"
ballarin@65099
  1177
ballarin@65099
  1178
definition inf_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
ballarin@65099
  1179
"inf_pres X Y f \<equiv> complete_lattice X \<and> complete_lattice Y \<and> (\<forall> A \<subseteq> carrier X. f (\<Sqinter>\<^bsub>X\<^esub> A) = (\<Sqinter>\<^bsub>Y\<^esub> (f ` A)))"
ballarin@65099
  1180
ballarin@65099
  1181
lemma weak_sup_pres:
ballarin@65099
  1182
  "sup_pres X Y f \<Longrightarrow> weak_sup_pres X Y f"
ballarin@65099
  1183
  by (simp add: sup_pres_def weak_sup_pres_def)
ballarin@65099
  1184
ballarin@65099
  1185
lemma weak_inf_pres:
ballarin@65099
  1186
  "inf_pres X Y f \<Longrightarrow> weak_inf_pres X Y f"
ballarin@65099
  1187
  by (simp add: inf_pres_def weak_inf_pres_def)
ballarin@65099
  1188
ballarin@65099
  1189
lemma sup_pres_is_join_pres:
ballarin@65099
  1190
  assumes "weak_sup_pres X Y f"
ballarin@65099
  1191
  shows "join_pres X Y f"
ballarin@65099
  1192
  using assms
ballarin@65099
  1193
  apply (simp add: join_pres_def weak_sup_pres_def, safe)
ballarin@65099
  1194
  apply (rename_tac x y)
ballarin@65099
  1195
  apply (drule_tac x="{x, y}" in spec)
ballarin@65099
  1196
  apply (auto simp add: join_def)
ballarin@65099
  1197
done
ballarin@65099
  1198
ballarin@65099
  1199
lemma inf_pres_is_meet_pres:
ballarin@65099
  1200
  assumes "weak_inf_pres X Y f"
ballarin@65099
  1201
  shows "meet_pres X Y f"
ballarin@65099
  1202
  using assms
ballarin@65099
  1203
  apply (simp add: meet_pres_def weak_inf_pres_def, safe)
ballarin@65099
  1204
  apply (rename_tac x y)
ballarin@65099
  1205
  apply (drule_tac x="{x, y}" in spec)
ballarin@65099
  1206
  apply (auto simp add: meet_def)
ballarin@65099
  1207
done
ballarin@65099
  1208
ballarin@65099
  1209
end