src/HOL/Algebra/Lattice.thy
 author paulson Sat Jun 30 15:44:04 2018 +0100 (12 months ago) changeset 68551 b680e74eb6f2 parent 67443 3abf6a722518 child 69700 7a92cbec7030 permissions -rw-r--r--
More on Algebra by Paulo and Martin
```     1 (*  Title:      HOL/Algebra/Lattice.thy
```
```     2     Author:     Clemens Ballarin, started 7 November 2003
```
```     3     Copyright:  Clemens Ballarin
```
```     4
```
```     5 Most congruence rules by Stephan Hohe.
```
```     6 With additional contributions from Alasdair Armstrong and Simon Foster.
```
```     7 *)
```
```     8
```
```     9 theory Lattice
```
```    10 imports Order
```
```    11 begin
```
```    12
```
```    13 section \<open>Lattices\<close>
```
```    14
```
```    15 subsection \<open>Supremum and infimum\<close>
```
```    16
```
```    17 definition
```
```    18   sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_"  90)
```
```    19   where "\<Squnion>\<^bsub>L\<^esub>A = (SOME x. least L x (Upper L A))"
```
```    20
```
```    21 definition
```
```    22   inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_"  90)
```
```    23   where "\<Sqinter>\<^bsub>L\<^esub>A = (SOME x. greatest L x (Lower L A))"
```
```    24
```
```    25 definition supr ::
```
```    26   "('a, 'b) gorder_scheme \<Rightarrow> 'c set \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> 'a "
```
```    27   where "supr L A f = \<Squnion>\<^bsub>L\<^esub>(f ` A)"
```
```    28
```
```    29 definition infi ::
```
```    30   "('a, 'b) gorder_scheme \<Rightarrow> 'c set \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> 'a "
```
```    31   where "infi L A f = \<Sqinter>\<^bsub>L\<^esub>(f ` A)"
```
```    32
```
```    33 syntax
```
```    34   "_inf1"     :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a" ("(3IINF\<index> _./ _)" [0, 10] 10)
```
```    35   "_inf"      :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a"  ("(3IINF\<index> _:_./ _)" [0, 0, 10] 10)
```
```    36   "_sup1"     :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SSUP\<index> _./ _)" [0, 10] 10)
```
```    37   "_sup"      :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a"  ("(3SSUP\<index> _:_./ _)" [0, 0, 10] 10)
```
```    38
```
```    39 translations
```
```    40   "IINF\<^bsub>L\<^esub> x. B"     == "CONST infi L CONST UNIV (%x. B)"
```
```    41   "IINF\<^bsub>L\<^esub> x:A. B"   == "CONST infi L A (%x. B)"
```
```    42   "SSUP\<^bsub>L\<^esub> x. B"     == "CONST supr L CONST UNIV (%x. B)"
```
```    43   "SSUP\<^bsub>L\<^esub> x:A. B"   == "CONST supr L A (%x. B)"
```
```    44
```
```    45 definition
```
```    46   join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
```
```    47   where "x \<squnion>\<^bsub>L\<^esub> y = \<Squnion>\<^bsub>L\<^esub>{x, y}"
```
```    48
```
```    49 definition
```
```    50   meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
```
```    51   where "x \<sqinter>\<^bsub>L\<^esub> y = \<Sqinter>\<^bsub>L\<^esub>{x, y}"
```
```    52
```
```    53 definition
```
```    54   LEAST_FP :: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("LFP\<index>") where
```
```    55   "LEAST_FP L f = \<Sqinter>\<^bsub>L\<^esub> {u \<in> carrier L. f u \<sqsubseteq>\<^bsub>L\<^esub> u}"    \<comment> \<open>least fixed point\<close>
```
```    56
```
```    57 definition
```
```    58   GREATEST_FP:: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("GFP\<index>") where
```
```    59   "GREATEST_FP L f = \<Squnion>\<^bsub>L\<^esub> {u \<in> carrier L. u \<sqsubseteq>\<^bsub>L\<^esub> f u}"    \<comment> \<open>greatest fixed point\<close>
```
```    60
```
```    61
```
```    62 subsection \<open>Dual operators\<close>
```
```    63
```
```    64 lemma sup_dual [simp]:
```
```    65   "\<Squnion>\<^bsub>inv_gorder L\<^esub>A = \<Sqinter>\<^bsub>L\<^esub>A"
```
```    66   by (simp add: sup_def inf_def)
```
```    67
```
```    68 lemma inf_dual [simp]:
```
```    69   "\<Sqinter>\<^bsub>inv_gorder L\<^esub>A = \<Squnion>\<^bsub>L\<^esub>A"
```
```    70   by (simp add: sup_def inf_def)
```
```    71
```
```    72 lemma join_dual [simp]:
```
```    73   "p \<squnion>\<^bsub>inv_gorder L\<^esub> q = p \<sqinter>\<^bsub>L\<^esub> q"
```
```    74   by (simp add:join_def meet_def)
```
```    75
```
```    76 lemma meet_dual [simp]:
```
```    77   "p \<sqinter>\<^bsub>inv_gorder L\<^esub> q = p \<squnion>\<^bsub>L\<^esub> q"
```
```    78   by (simp add:join_def meet_def)
```
```    79
```
```    80 lemma top_dual [simp]:
```
```    81   "\<top>\<^bsub>inv_gorder L\<^esub> = \<bottom>\<^bsub>L\<^esub>"
```
```    82   by (simp add: top_def bottom_def)
```
```    83
```
```    84 lemma bottom_dual [simp]:
```
```    85   "\<bottom>\<^bsub>inv_gorder L\<^esub> = \<top>\<^bsub>L\<^esub>"
```
```    86   by (simp add: top_def bottom_def)
```
```    87
```
```    88 lemma LFP_dual [simp]:
```
```    89   "LEAST_FP (inv_gorder L) f = GREATEST_FP L f"
```
```    90   by (simp add:LEAST_FP_def GREATEST_FP_def)
```
```    91
```
```    92 lemma GFP_dual [simp]:
```
```    93   "GREATEST_FP (inv_gorder L) f = LEAST_FP L f"
```
```    94   by (simp add:LEAST_FP_def GREATEST_FP_def)
```
```    95
```
```    96
```
```    97 subsection \<open>Lattices\<close>
```
```    98
```
```    99 locale weak_upper_semilattice = weak_partial_order +
```
```   100   assumes sup_of_two_exists:
```
```   101     "[| x \<in> carrier L; y \<in> carrier L |] ==> \<exists>s. least L s (Upper L {x, y})"
```
```   102
```
```   103 locale weak_lower_semilattice = weak_partial_order +
```
```   104   assumes inf_of_two_exists:
```
```   105     "[| x \<in> carrier L; y \<in> carrier L |] ==> \<exists>s. greatest L s (Lower L {x, y})"
```
```   106
```
```   107 locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice
```
```   108
```
```   109 lemma (in weak_lattice) dual_weak_lattice:
```
```   110   "weak_lattice (inv_gorder L)"
```
```   111 proof -
```
```   112   interpret dual: weak_partial_order "inv_gorder L"
```
```   113     by (metis dual_weak_order)
```
```   114
```
```   115   show ?thesis
```
```   116     apply (unfold_locales)
```
```   117     apply (simp_all add: inf_of_two_exists sup_of_two_exists)
```
```   118   done
```
```   119 qed
```
```   120
```
```   121
```
```   122 subsubsection \<open>Supremum\<close>
```
```   123
```
```   124 lemma (in weak_upper_semilattice) joinI:
```
```   125   "[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]
```
```   126   ==> P (x \<squnion> y)"
```
```   127 proof (unfold join_def sup_def)
```
```   128   assume L: "x \<in> carrier L"  "y \<in> carrier L"
```
```   129     and P: "!!l. least L l (Upper L {x, y}) ==> P l"
```
```   130   with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
```
```   131   with L show "P (SOME l. least L l (Upper L {x, y}))"
```
```   132     by (fast intro: someI2 P)
```
```   133 qed
```
```   134
```
```   135 lemma (in weak_upper_semilattice) join_closed [simp]:
```
```   136   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L"
```
```   137   by (rule joinI) (rule least_closed)
```
```   138
```
```   139 lemma (in weak_upper_semilattice) join_cong_l:
```
```   140   assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
```
```   141     and xx': "x .= x'"
```
```   142   shows "x \<squnion> y .= x' \<squnion> y"
```
```   143 proof (rule joinI, rule joinI)
```
```   144   fix a b
```
```   145   from xx' carr
```
```   146       have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
```
```   147
```
```   148   assume leasta: "least L a (Upper L {x, y})"
```
```   149   assume "least L b (Upper L {x', y})"
```
```   150   with carr
```
```   151       have leastb: "least L b (Upper L {x, y})"
```
```   152       by (simp add: least_Upper_cong_r[OF _ _ seq])
```
```   153
```
```   154   from leasta leastb
```
```   155       show "a .= b" by (rule weak_least_unique)
```
```   156 qed (rule carr)+
```
```   157
```
```   158 lemma (in weak_upper_semilattice) join_cong_r:
```
```   159   assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
```
```   160     and yy': "y .= y'"
```
```   161   shows "x \<squnion> y .= x \<squnion> y'"
```
```   162 proof (rule joinI, rule joinI)
```
```   163   fix a b
```
```   164   have "{x, y} = {y, x}" by fast
```
```   165   also from carr yy'
```
```   166       have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
```
```   167   also have "{y', x} = {x, y'}" by fast
```
```   168   finally
```
```   169       have seq: "{x, y} {.=} {x, y'}" .
```
```   170
```
```   171   assume leasta: "least L a (Upper L {x, y})"
```
```   172   assume "least L b (Upper L {x, y'})"
```
```   173   with carr
```
```   174       have leastb: "least L b (Upper L {x, y})"
```
```   175       by (simp add: least_Upper_cong_r[OF _ _ seq])
```
```   176
```
```   177   from leasta leastb
```
```   178       show "a .= b" by (rule weak_least_unique)
```
```   179 qed (rule carr)+
```
```   180
```
```   181 lemma (in weak_partial_order) sup_of_singletonI:      (* only reflexivity needed ? *)
```
```   182   "x \<in> carrier L ==> least L x (Upper L {x})"
```
```   183   by (rule least_UpperI) auto
```
```   184
```
```   185 lemma (in weak_partial_order) weak_sup_of_singleton [simp]:
```
```   186   "x \<in> carrier L ==> \<Squnion>{x} .= x"
```
```   187   unfolding sup_def
```
```   188   by (rule someI2) (auto intro: weak_least_unique sup_of_singletonI)
```
```   189
```
```   190 lemma (in weak_partial_order) sup_of_singleton_closed [simp]:
```
```   191   "x \<in> carrier L \<Longrightarrow> \<Squnion>{x} \<in> carrier L"
```
```   192   unfolding sup_def
```
```   193   by (rule someI2) (auto intro: sup_of_singletonI)
```
```   194
```
```   195 text \<open>Condition on \<open>A\<close>: supremum exists.\<close>
```
```   196
```
```   197 lemma (in weak_upper_semilattice) sup_insertI:
```
```   198   "[| !!s. least L s (Upper L (insert x A)) ==> P s;
```
```   199   least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |]
```
```   200   ==> P (\<Squnion>(insert x A))"
```
```   201 proof (unfold sup_def)
```
```   202   assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
```
```   203     and P: "!!l. least L l (Upper L (insert x A)) ==> P l"
```
```   204     and least_a: "least L a (Upper L A)"
```
```   205   from L least_a have La: "a \<in> carrier L" by simp
```
```   206   from L sup_of_two_exists least_a
```
```   207   obtain s where least_s: "least L s (Upper L {a, x})" by blast
```
```   208   show "P (SOME l. least L l (Upper L (insert x A)))"
```
```   209   proof (rule someI2)
```
```   210     show "least L s (Upper L (insert x A))"
```
```   211     proof (rule least_UpperI)
```
```   212       fix z
```
```   213       assume "z \<in> insert x A"
```
```   214       then show "z \<sqsubseteq> s"
```
```   215       proof
```
```   216         assume "z = x" then show ?thesis
```
```   217           by (simp add: least_Upper_above [OF least_s] L La)
```
```   218       next
```
```   219         assume "z \<in> A"
```
```   220         with L least_s least_a show ?thesis
```
```   221           by (rule_tac le_trans [where y = a]) (auto dest: least_Upper_above)
```
```   222       qed
```
```   223     next
```
```   224       fix y
```
```   225       assume y: "y \<in> Upper L (insert x A)"
```
```   226       show "s \<sqsubseteq> y"
```
```   227       proof (rule least_le [OF least_s], rule Upper_memI)
```
```   228         fix z
```
```   229         assume z: "z \<in> {a, x}"
```
```   230         then show "z \<sqsubseteq> y"
```
```   231         proof
```
```   232           have y': "y \<in> Upper L A"
```
```   233             apply (rule subsetD [where A = "Upper L (insert x A)"])
```
```   234              apply (rule Upper_antimono)
```
```   235              apply blast
```
```   236             apply (rule y)
```
```   237             done
```
```   238           assume "z = a"
```
```   239           with y' least_a show ?thesis by (fast dest: least_le)
```
```   240         next
```
```   241           assume "z \<in> {x}"  (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *)
```
```   242           with y L show ?thesis by blast
```
```   243         qed
```
```   244       qed (rule Upper_closed [THEN subsetD, OF y])
```
```   245     next
```
```   246       from L show "insert x A \<subseteq> carrier L" by simp
```
```   247       from least_s show "s \<in> carrier L" by simp
```
```   248     qed
```
```   249   qed (rule P)
```
```   250 qed
```
```   251
```
```   252 lemma (in weak_upper_semilattice) finite_sup_least:
```
```   253   "[| finite A; A \<subseteq> carrier L; A \<noteq> {} |] ==> least L (\<Squnion>A) (Upper L A)"
```
```   254 proof (induct set: finite)
```
```   255   case empty
```
```   256   then show ?case by simp
```
```   257 next
```
```   258   case (insert x A)
```
```   259   show ?case
```
```   260   proof (cases "A = {}")
```
```   261     case True
```
```   262     with insert show ?thesis
```
```   263       by simp (simp add: least_cong [OF weak_sup_of_singleton] sup_of_singletonI)
```
```   264         (* The above step is hairy; least_cong can make simp loop.
```
```   265         Would want special version of simp to apply least_cong. *)
```
```   266   next
```
```   267     case False
```
```   268     with insert have "least L (\<Squnion>A) (Upper L A)" by simp
```
```   269     with _ show ?thesis
```
```   270       by (rule sup_insertI) (simp_all add: insert [simplified])
```
```   271   qed
```
```   272 qed
```
```   273
```
```   274 lemma (in weak_upper_semilattice) finite_sup_insertI:
```
```   275   assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"
```
```   276     and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
```
```   277   shows "P (\<Squnion> (insert x A))"
```
```   278 proof (cases "A = {}")
```
```   279   case True with P and xA show ?thesis
```
```   280     by (simp add: finite_sup_least)
```
```   281 next
```
```   282   case False with P and xA show ?thesis
```
```   283     by (simp add: sup_insertI finite_sup_least)
```
```   284 qed
```
```   285
```
```   286 lemma (in weak_upper_semilattice) finite_sup_closed [simp]:
```
```   287   "[| finite A; A \<subseteq> carrier L; A \<noteq> {} |] ==> \<Squnion>A \<in> carrier L"
```
```   288 proof (induct set: finite)
```
```   289   case empty then show ?case by simp
```
```   290 next
```
```   291   case insert then show ?case
```
```   292     by - (rule finite_sup_insertI, simp_all)
```
```   293 qed
```
```   294
```
```   295 lemma (in weak_upper_semilattice) join_left:
```
```   296   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y"
```
```   297   by (rule joinI [folded join_def]) (blast dest: least_mem)
```
```   298
```
```   299 lemma (in weak_upper_semilattice) join_right:
```
```   300   "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y"
```
```   301   by (rule joinI [folded join_def]) (blast dest: least_mem)
```
```   302
```
```   303 lemma (in weak_upper_semilattice) sup_of_two_least:
```
```   304   "[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})"
```
```   305 proof (unfold sup_def)
```
```   306   assume L: "x \<in> carrier L"  "y \<in> carrier L"
```
```   307   with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
```
```   308   with L show "least L (SOME z. least L z (Upper L {x, y})) (Upper L {x, y})"
```
```   309   by (fast intro: someI2 weak_least_unique)  (* blast fails *)
```
```   310 qed
```
```   311
```
```   312 lemma (in weak_upper_semilattice) join_le:
```
```   313   assumes sub: "x \<sqsubseteq> z"  "y \<sqsubseteq> z"
```
```   314     and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
```
```   315   shows "x \<squnion> y \<sqsubseteq> z"
```
```   316 proof (rule joinI [OF _ x y])
```
```   317   fix s
```
```   318   assume "least L s (Upper L {x, y})"
```
```   319   with sub z show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI)
```
```   320 qed
```
```   321
```
```   322 lemma (in weak_lattice) weak_le_iff_meet:
```
```   323   assumes "x \<in> carrier L" "y \<in> carrier L"
```
```   324   shows "x \<sqsubseteq> y \<longleftrightarrow> (x \<squnion> y) .= y"
```
```   325   by (meson assms(1) assms(2) join_closed join_le join_left join_right le_cong_r local.le_refl weak_le_antisym)
```
```   326
```
```   327 lemma (in weak_upper_semilattice) weak_join_assoc_lemma:
```
```   328   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
```
```   329   shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}"
```
```   330 proof (rule finite_sup_insertI)
```
```   331   \<comment> \<open>The textbook argument in Jacobson I, p 457\<close>
```
```   332   fix s
```
```   333   assume sup: "least L s (Upper L {x, y, z})"
```
```   334   show "x \<squnion> (y \<squnion> z) .= s"
```
```   335   proof (rule weak_le_antisym)
```
```   336     from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"
```
```   337       by (fastforce intro!: join_le elim: least_Upper_above)
```
```   338   next
```
```   339     from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)"
```
```   340     by (erule_tac least_le)
```
```   341       (blast intro!: Upper_memI intro: le_trans join_left join_right join_closed)
```
```   342   qed (simp_all add: L least_closed [OF sup])
```
```   343 qed (simp_all add: L)
```
```   344
```
```   345 text \<open>Commutativity holds for \<open>=\<close>.\<close>
```
```   346
```
```   347 lemma join_comm:
```
```   348   fixes L (structure)
```
```   349   shows "x \<squnion> y = y \<squnion> x"
```
```   350   by (unfold join_def) (simp add: insert_commute)
```
```   351
```
```   352 lemma (in weak_upper_semilattice) weak_join_assoc:
```
```   353   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
```
```   354   shows "(x \<squnion> y) \<squnion> z .= x \<squnion> (y \<squnion> z)"
```
```   355 proof -
```
```   356   (* FIXME: could be simplified by improved simp: uniform use of .=,
```
```   357      omit [symmetric] in last step. *)
```
```   358   have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm)
```
```   359   also from L have "... .= \<Squnion>{z, x, y}" by (simp add: weak_join_assoc_lemma)
```
```   360   also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute)
```
```   361   also from L have "... .= x \<squnion> (y \<squnion> z)" by (simp add: weak_join_assoc_lemma [symmetric])
```
```   362   finally show ?thesis by (simp add: L)
```
```   363 qed
```
```   364
```
```   365
```
```   366 subsubsection \<open>Infimum\<close>
```
```   367
```
```   368 lemma (in weak_lower_semilattice) meetI:
```
```   369   "[| !!i. greatest L i (Lower L {x, y}) ==> P i;
```
```   370   x \<in> carrier L; y \<in> carrier L |]
```
```   371   ==> P (x \<sqinter> y)"
```
```   372 proof (unfold meet_def inf_def)
```
```   373   assume L: "x \<in> carrier L"  "y \<in> carrier L"
```
```   374     and P: "!!g. greatest L g (Lower L {x, y}) ==> P g"
```
```   375   with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast
```
```   376   with L show "P (SOME g. greatest L g (Lower L {x, y}))"
```
```   377   by (fast intro: someI2 weak_greatest_unique P)
```
```   378 qed
```
```   379
```
```   380 lemma (in weak_lower_semilattice) meet_closed [simp]:
```
```   381   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L"
```
```   382   by (rule meetI) (rule greatest_closed)
```
```   383
```
```   384 lemma (in weak_lower_semilattice) meet_cong_l:
```
```   385   assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
```
```   386     and xx': "x .= x'"
```
```   387   shows "x \<sqinter> y .= x' \<sqinter> y"
```
```   388 proof (rule meetI, rule meetI)
```
```   389   fix a b
```
```   390   from xx' carr
```
```   391       have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
```
```   392
```
```   393   assume greatesta: "greatest L a (Lower L {x, y})"
```
```   394   assume "greatest L b (Lower L {x', y})"
```
```   395   with carr
```
```   396       have greatestb: "greatest L b (Lower L {x, y})"
```
```   397       by (simp add: greatest_Lower_cong_r[OF _ _ seq])
```
```   398
```
```   399   from greatesta greatestb
```
```   400       show "a .= b" by (rule weak_greatest_unique)
```
```   401 qed (rule carr)+
```
```   402
```
```   403 lemma (in weak_lower_semilattice) meet_cong_r:
```
```   404   assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
```
```   405     and yy': "y .= y'"
```
```   406   shows "x \<sqinter> y .= x \<sqinter> y'"
```
```   407 proof (rule meetI, rule meetI)
```
```   408   fix a b
```
```   409   have "{x, y} = {y, x}" by fast
```
```   410   also from carr yy'
```
```   411       have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
```
```   412   also have "{y', x} = {x, y'}" by fast
```
```   413   finally
```
```   414       have seq: "{x, y} {.=} {x, y'}" .
```
```   415
```
```   416   assume greatesta: "greatest L a (Lower L {x, y})"
```
```   417   assume "greatest L b (Lower L {x, y'})"
```
```   418   with carr
```
```   419       have greatestb: "greatest L b (Lower L {x, y})"
```
```   420       by (simp add: greatest_Lower_cong_r[OF _ _ seq])
```
```   421
```
```   422   from greatesta greatestb
```
```   423       show "a .= b" by (rule weak_greatest_unique)
```
```   424 qed (rule carr)+
```
```   425
```
```   426 lemma (in weak_partial_order) inf_of_singletonI:      (* only reflexivity needed ? *)
```
```   427   "x \<in> carrier L ==> greatest L x (Lower L {x})"
```
```   428   by (rule greatest_LowerI) auto
```
```   429
```
```   430 lemma (in weak_partial_order) weak_inf_of_singleton [simp]:
```
```   431   "x \<in> carrier L ==> \<Sqinter>{x} .= x"
```
```   432   unfolding inf_def
```
```   433   by (rule someI2) (auto intro: weak_greatest_unique inf_of_singletonI)
```
```   434
```
```   435 lemma (in weak_partial_order) inf_of_singleton_closed:
```
```   436   "x \<in> carrier L ==> \<Sqinter>{x} \<in> carrier L"
```
```   437   unfolding inf_def
```
```   438   by (rule someI2) (auto intro: inf_of_singletonI)
```
```   439
```
```   440 text \<open>Condition on \<open>A\<close>: infimum exists.\<close>
```
```   441
```
```   442 lemma (in weak_lower_semilattice) inf_insertI:
```
```   443   "[| !!i. greatest L i (Lower L (insert x A)) ==> P i;
```
```   444   greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |]
```
```   445   ==> P (\<Sqinter>(insert x A))"
```
```   446 proof (unfold inf_def)
```
```   447   assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
```
```   448     and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g"
```
```   449     and greatest_a: "greatest L a (Lower L A)"
```
```   450   from L greatest_a have La: "a \<in> carrier L" by simp
```
```   451   from L inf_of_two_exists greatest_a
```
```   452   obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast
```
```   453   show "P (SOME g. greatest L g (Lower L (insert x A)))"
```
```   454   proof (rule someI2)
```
```   455     show "greatest L i (Lower L (insert x A))"
```
```   456     proof (rule greatest_LowerI)
```
```   457       fix z
```
```   458       assume "z \<in> insert x A"
```
```   459       then show "i \<sqsubseteq> z"
```
```   460       proof
```
```   461         assume "z = x" then show ?thesis
```
```   462           by (simp add: greatest_Lower_below [OF greatest_i] L La)
```
```   463       next
```
```   464         assume "z \<in> A"
```
```   465         with L greatest_i greatest_a show ?thesis
```
```   466           by (rule_tac le_trans [where y = a]) (auto dest: greatest_Lower_below)
```
```   467       qed
```
```   468     next
```
```   469       fix y
```
```   470       assume y: "y \<in> Lower L (insert x A)"
```
```   471       show "y \<sqsubseteq> i"
```
```   472       proof (rule greatest_le [OF greatest_i], rule Lower_memI)
```
```   473         fix z
```
```   474         assume z: "z \<in> {a, x}"
```
```   475         then show "y \<sqsubseteq> z"
```
```   476         proof
```
```   477           have y': "y \<in> Lower L A"
```
```   478             apply (rule subsetD [where A = "Lower L (insert x A)"])
```
```   479             apply (rule Lower_antimono)
```
```   480              apply blast
```
```   481             apply (rule y)
```
```   482             done
```
```   483           assume "z = a"
```
```   484           with y' greatest_a show ?thesis by (fast dest: greatest_le)
```
```   485         next
```
```   486           assume "z \<in> {x}"
```
```   487           with y L show ?thesis by blast
```
```   488         qed
```
```   489       qed (rule Lower_closed [THEN subsetD, OF y])
```
```   490     next
```
```   491       from L show "insert x A \<subseteq> carrier L" by simp
```
```   492       from greatest_i show "i \<in> carrier L" by simp
```
```   493     qed
```
```   494   qed (rule P)
```
```   495 qed
```
```   496
```
```   497 lemma (in weak_lower_semilattice) finite_inf_greatest:
```
```   498   "[| finite A; A \<subseteq> carrier L; A \<noteq> {} |] ==> greatest L (\<Sqinter>A) (Lower L A)"
```
```   499 proof (induct set: finite)
```
```   500   case empty then show ?case by simp
```
```   501 next
```
```   502   case (insert x A)
```
```   503   show ?case
```
```   504   proof (cases "A = {}")
```
```   505     case True
```
```   506     with insert show ?thesis
```
```   507       by simp (simp add: greatest_cong [OF weak_inf_of_singleton]
```
```   508         inf_of_singleton_closed inf_of_singletonI)
```
```   509   next
```
```   510     case False
```
```   511     from insert show ?thesis
```
```   512     proof (rule_tac inf_insertI)
```
```   513       from False insert show "greatest L (\<Sqinter>A) (Lower L A)" by simp
```
```   514     qed simp_all
```
```   515   qed
```
```   516 qed
```
```   517
```
```   518 lemma (in weak_lower_semilattice) finite_inf_insertI:
```
```   519   assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"
```
```   520     and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
```
```   521   shows "P (\<Sqinter> (insert x A))"
```
```   522 proof (cases "A = {}")
```
```   523   case True with P and xA show ?thesis
```
```   524     by (simp add: finite_inf_greatest)
```
```   525 next
```
```   526   case False with P and xA show ?thesis
```
```   527     by (simp add: inf_insertI finite_inf_greatest)
```
```   528 qed
```
```   529
```
```   530 lemma (in weak_lower_semilattice) finite_inf_closed [simp]:
```
```   531   "[| finite A; A \<subseteq> carrier L; A \<noteq> {} |] ==> \<Sqinter>A \<in> carrier L"
```
```   532 proof (induct set: finite)
```
```   533   case empty then show ?case by simp
```
```   534 next
```
```   535   case insert then show ?case
```
```   536     by (rule_tac finite_inf_insertI) (simp_all)
```
```   537 qed
```
```   538
```
```   539 lemma (in weak_lower_semilattice) meet_left:
```
```   540   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x"
```
```   541   by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
```
```   542
```
```   543 lemma (in weak_lower_semilattice) meet_right:
```
```   544   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y"
```
```   545   by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
```
```   546
```
```   547 lemma (in weak_lower_semilattice) inf_of_two_greatest:
```
```   548   "[| x \<in> carrier L; y \<in> carrier L |] ==>
```
```   549   greatest L (\<Sqinter>{x, y}) (Lower L {x, y})"
```
```   550 proof (unfold inf_def)
```
```   551   assume L: "x \<in> carrier L"  "y \<in> carrier L"
```
```   552   with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast
```
```   553   with L
```
```   554   show "greatest L (SOME z. greatest L z (Lower L {x, y})) (Lower L {x, y})"
```
```   555   by (fast intro: someI2 weak_greatest_unique)  (* blast fails *)
```
```   556 qed
```
```   557
```
```   558 lemma (in weak_lower_semilattice) meet_le:
```
```   559   assumes sub: "z \<sqsubseteq> x"  "z \<sqsubseteq> y"
```
```   560     and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
```
```   561   shows "z \<sqsubseteq> x \<sqinter> y"
```
```   562 proof (rule meetI [OF _ x y])
```
```   563   fix i
```
```   564   assume "greatest L i (Lower L {x, y})"
```
```   565   with sub z show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI)
```
```   566 qed
```
```   567
```
```   568 lemma (in weak_lattice) weak_le_iff_join:
```
```   569   assumes "x \<in> carrier L" "y \<in> carrier L"
```
```   570   shows "x \<sqsubseteq> y \<longleftrightarrow> x .= (x \<sqinter> y)"
```
```   571   by (meson assms(1) assms(2) local.le_refl local.le_trans meet_closed meet_le meet_left meet_right weak_le_antisym weak_refl)
```
```   572
```
```   573 lemma (in weak_lower_semilattice) weak_meet_assoc_lemma:
```
```   574   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
```
```   575   shows "x \<sqinter> (y \<sqinter> z) .= \<Sqinter>{x, y, z}"
```
```   576 proof (rule finite_inf_insertI)
```
```   577   txt \<open>The textbook argument in Jacobson I, p 457\<close>
```
```   578   fix i
```
```   579   assume inf: "greatest L i (Lower L {x, y, z})"
```
```   580   show "x \<sqinter> (y \<sqinter> z) .= i"
```
```   581   proof (rule weak_le_antisym)
```
```   582     from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
```
```   583       by (fastforce intro!: meet_le elim: greatest_Lower_below)
```
```   584   next
```
```   585     from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i"
```
```   586     by (erule_tac greatest_le)
```
```   587       (blast intro!: Lower_memI intro: le_trans meet_left meet_right meet_closed)
```
```   588   qed (simp_all add: L greatest_closed [OF inf])
```
```   589 qed (simp_all add: L)
```
```   590
```
```   591 lemma meet_comm:
```
```   592   fixes L (structure)
```
```   593   shows "x \<sqinter> y = y \<sqinter> x"
```
```   594   by (unfold meet_def) (simp add: insert_commute)
```
```   595
```
```   596 lemma (in weak_lower_semilattice) weak_meet_assoc:
```
```   597   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
```
```   598   shows "(x \<sqinter> y) \<sqinter> z .= x \<sqinter> (y \<sqinter> z)"
```
```   599 proof -
```
```   600   (* FIXME: improved simp, see weak_join_assoc above *)
```
```   601   have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm)
```
```   602   also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: weak_meet_assoc_lemma)
```
```   603   also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute)
```
```   604   also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: weak_meet_assoc_lemma [symmetric])
```
```   605   finally show ?thesis by (simp add: L)
```
```   606 qed
```
```   607
```
```   608 text \<open>Total orders are lattices.\<close>
```
```   609
```
```   610 sublocale weak_total_order \<subseteq> weak?: weak_lattice
```
```   611 proof
```
```   612   fix x y
```
```   613   assume L: "x \<in> carrier L"  "y \<in> carrier L"
```
```   614   show "\<exists>s. least L s (Upper L {x, y})"
```
```   615   proof -
```
```   616     note total L
```
```   617     moreover
```
```   618     {
```
```   619       assume "x \<sqsubseteq> y"
```
```   620       with L have "least L y (Upper L {x, y})"
```
```   621         by (rule_tac least_UpperI) auto
```
```   622     }
```
```   623     moreover
```
```   624     {
```
```   625       assume "y \<sqsubseteq> x"
```
```   626       with L have "least L x (Upper L {x, y})"
```
```   627         by (rule_tac least_UpperI) auto
```
```   628     }
```
```   629     ultimately show ?thesis by blast
```
```   630   qed
```
```   631 next
```
```   632   fix x y
```
```   633   assume L: "x \<in> carrier L"  "y \<in> carrier L"
```
```   634   show "\<exists>i. greatest L i (Lower L {x, y})"
```
```   635   proof -
```
```   636     note total L
```
```   637     moreover
```
```   638     {
```
```   639       assume "y \<sqsubseteq> x"
```
```   640       with L have "greatest L y (Lower L {x, y})"
```
```   641         by (rule_tac greatest_LowerI) auto
```
```   642     }
```
```   643     moreover
```
```   644     {
```
```   645       assume "x \<sqsubseteq> y"
```
```   646       with L have "greatest L x (Lower L {x, y})"
```
```   647         by (rule_tac greatest_LowerI) auto
```
```   648     }
```
```   649     ultimately show ?thesis by blast
```
```   650   qed
```
```   651 qed
```
```   652
```
```   653
```
```   654 subsection \<open>Weak Bounded Lattices\<close>
```
```   655
```
```   656 locale weak_bounded_lattice =
```
```   657   weak_lattice +
```
```   658   weak_partial_order_bottom +
```
```   659   weak_partial_order_top
```
```   660 begin
```
```   661
```
```   662 lemma bottom_meet: "x \<in> carrier L \<Longrightarrow> \<bottom> \<sqinter> x .= \<bottom>"
```
```   663   by (metis bottom_least least_def meet_closed meet_left weak_le_antisym)
```
```   664
```
```   665 lemma bottom_join: "x \<in> carrier L \<Longrightarrow> \<bottom> \<squnion> x .= x"
```
```   666   by (metis bottom_least join_closed join_le join_right le_refl least_def weak_le_antisym)
```
```   667
```
```   668 lemma bottom_weak_eq:
```
```   669   "\<lbrakk> b \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> b \<sqsubseteq> x \<rbrakk> \<Longrightarrow> b .= \<bottom>"
```
```   670   by (metis bottom_closed bottom_lower weak_le_antisym)
```
```   671
```
```   672 lemma top_join: "x \<in> carrier L \<Longrightarrow> \<top> \<squnion> x .= \<top>"
```
```   673   by (metis join_closed join_left top_closed top_higher weak_le_antisym)
```
```   674
```
```   675 lemma top_meet: "x \<in> carrier L \<Longrightarrow> \<top> \<sqinter> x .= x"
```
```   676   by (metis le_refl meet_closed meet_le meet_right top_closed top_higher weak_le_antisym)
```
```   677
```
```   678 lemma top_weak_eq:  "\<lbrakk> t \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> x \<sqsubseteq> t \<rbrakk> \<Longrightarrow> t .= \<top>"
```
```   679   by (metis top_closed top_higher weak_le_antisym)
```
```   680
```
```   681 end
```
```   682
```
```   683 sublocale weak_bounded_lattice \<subseteq> weak_partial_order ..
```
```   684
```
```   685
```
```   686 subsection \<open>Lattices where \<open>eq\<close> is the Equality\<close>
```
```   687
```
```   688 locale upper_semilattice = partial_order +
```
```   689   assumes sup_of_two_exists:
```
```   690     "[| x \<in> carrier L; y \<in> carrier L |] ==> \<exists>s. least L s (Upper L {x, y})"
```
```   691
```
```   692 sublocale upper_semilattice \<subseteq> weak?: weak_upper_semilattice
```
```   693   by unfold_locales (rule sup_of_two_exists)
```
```   694
```
```   695 locale lower_semilattice = partial_order +
```
```   696   assumes inf_of_two_exists:
```
```   697     "[| x \<in> carrier L; y \<in> carrier L |] ==> \<exists>s. greatest L s (Lower L {x, y})"
```
```   698
```
```   699 sublocale lower_semilattice \<subseteq> weak?: weak_lower_semilattice
```
```   700   by unfold_locales (rule inf_of_two_exists)
```
```   701
```
```   702 locale lattice = upper_semilattice + lower_semilattice
```
```   703
```
```   704 sublocale lattice \<subseteq> weak_lattice ..
```
```   705
```
```   706 lemma (in lattice) dual_lattice:
```
```   707   "lattice (inv_gorder L)"
```
```   708 proof -
```
```   709   interpret dual: weak_lattice "inv_gorder L"
```
```   710     by (metis dual_weak_lattice)
```
```   711
```
```   712   show ?thesis
```
```   713     apply (unfold_locales)
```
```   714     apply (simp_all add: inf_of_two_exists sup_of_two_exists)
```
```   715     apply (simp add:eq_is_equal)
```
```   716   done
```
```   717 qed
```
```   718
```
```   719 lemma (in lattice) le_iff_join:
```
```   720   assumes "x \<in> carrier L" "y \<in> carrier L"
```
```   721   shows "x \<sqsubseteq> y \<longleftrightarrow> x = (x \<sqinter> y)"
```
```   722   by (simp add: assms(1) assms(2) eq_is_equal weak_le_iff_join)
```
```   723
```
```   724 lemma (in lattice) le_iff_meet:
```
```   725   assumes "x \<in> carrier L" "y \<in> carrier L"
```
```   726   shows "x \<sqsubseteq> y \<longleftrightarrow> (x \<squnion> y) = y"
```
```   727   by (simp add: assms(1) assms(2) eq_is_equal weak_le_iff_meet)
```
```   728
```
```   729 text \<open> Total orders are lattices. \<close>
```
```   730
```
```   731 sublocale total_order \<subseteq> weak?: lattice
```
```   732   by standard (auto intro: weak.weak.sup_of_two_exists weak.weak.inf_of_two_exists)
```
```   733
```
```   734 text \<open>Functions that preserve joins and meets\<close>
```
```   735
```
```   736 definition join_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
```
```   737 "join_pres X Y f \<equiv> lattice X \<and> lattice Y \<and> (\<forall> x \<in> carrier X. \<forall> y \<in> carrier X. f (x \<squnion>\<^bsub>X\<^esub> y) = f x \<squnion>\<^bsub>Y\<^esub> f y)"
```
```   738
```
```   739 definition meet_pres :: "('a, 'c) gorder_scheme \<Rightarrow> ('b, 'd) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
```
```   740 "meet_pres X Y f \<equiv> lattice X \<and> lattice Y \<and> (\<forall> x \<in> carrier X. \<forall> y \<in> carrier X. f (x \<sqinter>\<^bsub>X\<^esub> y) = f x \<sqinter>\<^bsub>Y\<^esub> f y)"
```
```   741
```
```   742 lemma join_pres_isotone:
```
```   743   assumes "f \<in> carrier X \<rightarrow> carrier Y" "join_pres X Y f"
```
```   744   shows "isotone X Y f"
```
```   745   using assms
```
```   746   apply (rule_tac isotoneI)
```
```   747   apply (auto simp add: join_pres_def lattice.le_iff_meet funcset_carrier)
```
```   748   using lattice_def partial_order_def upper_semilattice_def apply blast
```
```   749   using lattice_def partial_order_def upper_semilattice_def apply blast
```
```   750   apply fastforce
```
```   751 done
```
```   752
```
```   753 lemma meet_pres_isotone:
```
```   754   assumes "f \<in> carrier X \<rightarrow> carrier Y" "meet_pres X Y f"
```
```   755   shows "isotone X Y f"
```
```   756   using assms
```
```   757   apply (rule_tac isotoneI)
```
```   758   apply (auto simp add: meet_pres_def lattice.le_iff_join funcset_carrier)
```
```   759   using lattice_def partial_order_def upper_semilattice_def apply blast
```
```   760   using lattice_def partial_order_def upper_semilattice_def apply blast
```
```   761   apply fastforce
```
```   762 done
```
```   763
```
```   764
```
```   765 subsection \<open>Bounded Lattices\<close>
```
```   766
```
```   767 locale bounded_lattice =
```
```   768   lattice +
```
```   769   weak_partial_order_bottom +
```
```   770   weak_partial_order_top
```
```   771
```
```   772 sublocale bounded_lattice \<subseteq> weak_bounded_lattice ..
```
```   773
```
```   774 context bounded_lattice
```
```   775 begin
```
```   776
```
```   777 lemma bottom_eq:
```
```   778   "\<lbrakk> b \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> b \<sqsubseteq> x \<rbrakk> \<Longrightarrow> b = \<bottom>"
```
```   779   by (metis bottom_closed bottom_lower le_antisym)
```
```   780
```
```   781 lemma top_eq:  "\<lbrakk> t \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> x \<sqsubseteq> t \<rbrakk> \<Longrightarrow> t = \<top>"
```
```   782   by (metis le_antisym top_closed top_higher)
```
```   783
```
```   784 end
```
```   785
```
```   786 end
```