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