src/HOL/Lattice/Lattice.thy
 author wenzelm Tue Sep 26 20:54:40 2017 +0200 (23 months ago) changeset 66695 91500c024c7f parent 61986 2461779da2b8 child 69597 ff784d5a5bfb permissions -rw-r--r--
tuned;
     1 (*  Title:      HOL/Lattice/Lattice.thy

     2     Author:     Markus Wenzel, TU Muenchen

     3 *)

     4

     5 section \<open>Lattices\<close>

     6

     7 theory Lattice imports Bounds begin

     8

     9 subsection \<open>Lattice operations\<close>

    10

    11 text \<open>

    12   A \emph{lattice} is a partial order with infimum and supremum of any

    13   two elements (thus any \emph{finite} number of elements have bounds

    14   as well).

    15 \<close>

    16

    17 class lattice =

    18   assumes ex_inf: "\<exists>inf. is_inf x y inf"

    19   assumes ex_sup: "\<exists>sup. is_sup x y sup"

    20

    21 text \<open>

    22   The \<open>\<sqinter>\<close> (meet) and \<open>\<squnion>\<close> (join) operations select such

    23   infimum and supremum elements.

    24 \<close>

    25

    26 definition

    27   meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<sqinter>" 70) where

    28   "x \<sqinter> y = (THE inf. is_inf x y inf)"

    29 definition

    30   join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<squnion>" 65) where

    31   "x \<squnion> y = (THE sup. is_sup x y sup)"

    32

    33 text \<open>

    34   Due to unique existence of bounds, the lattice operations may be

    35   exhibited as follows.

    36 \<close>

    37

    38 lemma meet_equality [elim?]: "is_inf x y inf \<Longrightarrow> x \<sqinter> y = inf"

    39 proof (unfold meet_def)

    40   assume "is_inf x y inf"

    41   then show "(THE inf. is_inf x y inf) = inf"

    42     by (rule the_equality) (rule is_inf_uniq [OF _ \<open>is_inf x y inf\<close>])

    43 qed

    44

    45 lemma meetI [intro?]:

    46     "inf \<sqsubseteq> x \<Longrightarrow> inf \<sqsubseteq> y \<Longrightarrow> (\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> inf) \<Longrightarrow> x \<sqinter> y = inf"

    47   by (rule meet_equality, rule is_infI) blast+

    48

    49 lemma join_equality [elim?]: "is_sup x y sup \<Longrightarrow> x \<squnion> y = sup"

    50 proof (unfold join_def)

    51   assume "is_sup x y sup"

    52   then show "(THE sup. is_sup x y sup) = sup"

    53     by (rule the_equality) (rule is_sup_uniq [OF _ \<open>is_sup x y sup\<close>])

    54 qed

    55

    56 lemma joinI [intro?]: "x \<sqsubseteq> sup \<Longrightarrow> y \<sqsubseteq> sup \<Longrightarrow>

    57     (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> sup \<sqsubseteq> z) \<Longrightarrow> x \<squnion> y = sup"

    58   by (rule join_equality, rule is_supI) blast+

    59

    60

    61 text \<open>

    62   \medskip The \<open>\<sqinter>\<close> and \<open>\<squnion>\<close> operations indeed determine

    63   bounds on a lattice structure.

    64 \<close>

    65

    66 lemma is_inf_meet [intro?]: "is_inf x y (x \<sqinter> y)"

    67 proof (unfold meet_def)

    68   from ex_inf obtain inf where "is_inf x y inf" ..

    69   then show "is_inf x y (THE inf. is_inf x y inf)"

    70     by (rule theI) (rule is_inf_uniq [OF _ \<open>is_inf x y inf\<close>])

    71 qed

    72

    73 lemma meet_greatest [intro?]: "z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> x \<sqinter> y"

    74   by (rule is_inf_greatest) (rule is_inf_meet)

    75

    76 lemma meet_lower1 [intro?]: "x \<sqinter> y \<sqsubseteq> x"

    77   by (rule is_inf_lower) (rule is_inf_meet)

    78

    79 lemma meet_lower2 [intro?]: "x \<sqinter> y \<sqsubseteq> y"

    80   by (rule is_inf_lower) (rule is_inf_meet)

    81

    82

    83 lemma is_sup_join [intro?]: "is_sup x y (x \<squnion> y)"

    84 proof (unfold join_def)

    85   from ex_sup obtain sup where "is_sup x y sup" ..

    86   then show "is_sup x y (THE sup. is_sup x y sup)"

    87     by (rule theI) (rule is_sup_uniq [OF _ \<open>is_sup x y sup\<close>])

    88 qed

    89

    90 lemma join_least [intro?]: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"

    91   by (rule is_sup_least) (rule is_sup_join)

    92

    93 lemma join_upper1 [intro?]: "x \<sqsubseteq> x \<squnion> y"

    94   by (rule is_sup_upper) (rule is_sup_join)

    95

    96 lemma join_upper2 [intro?]: "y \<sqsubseteq> x \<squnion> y"

    97   by (rule is_sup_upper) (rule is_sup_join)

    98

    99

   100 subsection \<open>Duality\<close>

   101

   102 text \<open>

   103   The class of lattices is closed under formation of dual structures.

   104   This means that for any theorem of lattice theory, the dualized

   105   statement holds as well; this important fact simplifies many proofs

   106   of lattice theory.

   107 \<close>

   108

   109 instance dual :: (lattice) lattice

   110 proof

   111   fix x' y' :: "'a::lattice dual"

   112   show "\<exists>inf'. is_inf x' y' inf'"

   113   proof -

   114     have "\<exists>sup. is_sup (undual x') (undual y') sup" by (rule ex_sup)

   115     then have "\<exists>sup. is_inf (dual (undual x')) (dual (undual y')) (dual sup)"

   116       by (simp only: dual_inf)

   117     then show ?thesis by (simp add: dual_ex [symmetric])

   118   qed

   119   show "\<exists>sup'. is_sup x' y' sup'"

   120   proof -

   121     have "\<exists>inf. is_inf (undual x') (undual y') inf" by (rule ex_inf)

   122     then have "\<exists>inf. is_sup (dual (undual x')) (dual (undual y')) (dual inf)"

   123       by (simp only: dual_sup)

   124     then show ?thesis by (simp add: dual_ex [symmetric])

   125   qed

   126 qed

   127

   128 text \<open>

   129   Apparently, the \<open>\<sqinter>\<close> and \<open>\<squnion>\<close> operations are dual to each

   130   other.

   131 \<close>

   132

   133 theorem dual_meet [intro?]: "dual (x \<sqinter> y) = dual x \<squnion> dual y"

   134 proof -

   135   from is_inf_meet have "is_sup (dual x) (dual y) (dual (x \<sqinter> y))" ..

   136   then have "dual x \<squnion> dual y = dual (x \<sqinter> y)" ..

   137   then show ?thesis ..

   138 qed

   139

   140 theorem dual_join [intro?]: "dual (x \<squnion> y) = dual x \<sqinter> dual y"

   141 proof -

   142   from is_sup_join have "is_inf (dual x) (dual y) (dual (x \<squnion> y))" ..

   143   then have "dual x \<sqinter> dual y = dual (x \<squnion> y)" ..

   144   then show ?thesis ..

   145 qed

   146

   147

   148 subsection \<open>Algebraic properties \label{sec:lattice-algebra}\<close>

   149

   150 text \<open>

   151   The \<open>\<sqinter>\<close> and \<open>\<squnion>\<close> operations have the following

   152   characteristic algebraic properties: associative (A), commutative

   153   (C), and absorptive (AB).

   154 \<close>

   155

   156 theorem meet_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"

   157 proof

   158   show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x \<sqinter> y"

   159   proof

   160     show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x" ..

   161     show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y"

   162     proof -

   163       have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..

   164       also have "\<dots> \<sqsubseteq> y" ..

   165       finally show ?thesis .

   166     qed

   167   qed

   168   show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> z"

   169   proof -

   170     have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..

   171     also have "\<dots> \<sqsubseteq> z" ..

   172     finally show ?thesis .

   173   qed

   174   fix w assume "w \<sqsubseteq> x \<sqinter> y" and "w \<sqsubseteq> z"

   175   show "w \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"

   176   proof

   177     show "w \<sqsubseteq> x"

   178     proof -

   179       have "w \<sqsubseteq> x \<sqinter> y" by fact

   180       also have "\<dots> \<sqsubseteq> x" ..

   181       finally show ?thesis .

   182     qed

   183     show "w \<sqsubseteq> y \<sqinter> z"

   184     proof

   185       show "w \<sqsubseteq> y"

   186       proof -

   187         have "w \<sqsubseteq> x \<sqinter> y" by fact

   188         also have "\<dots> \<sqsubseteq> y" ..

   189         finally show ?thesis .

   190       qed

   191       show "w \<sqsubseteq> z" by fact

   192     qed

   193   qed

   194 qed

   195

   196 theorem join_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"

   197 proof -

   198   have "dual ((x \<squnion> y) \<squnion> z) = (dual x \<sqinter> dual y) \<sqinter> dual z"

   199     by (simp only: dual_join)

   200   also have "\<dots> = dual x \<sqinter> (dual y \<sqinter> dual z)"

   201     by (rule meet_assoc)

   202   also have "\<dots> = dual (x \<squnion> (y \<squnion> z))"

   203     by (simp only: dual_join)

   204   finally show ?thesis ..

   205 qed

   206

   207 theorem meet_commute: "x \<sqinter> y = y \<sqinter> x"

   208 proof

   209   show "y \<sqinter> x \<sqsubseteq> x" ..

   210   show "y \<sqinter> x \<sqsubseteq> y" ..

   211   fix z assume "z \<sqsubseteq> y" and "z \<sqsubseteq> x"

   212   then show "z \<sqsubseteq> y \<sqinter> x" ..

   213 qed

   214

   215 theorem join_commute: "x \<squnion> y = y \<squnion> x"

   216 proof -

   217   have "dual (x \<squnion> y) = dual x \<sqinter> dual y" ..

   218   also have "\<dots> = dual y \<sqinter> dual x"

   219     by (rule meet_commute)

   220   also have "\<dots> = dual (y \<squnion> x)"

   221     by (simp only: dual_join)

   222   finally show ?thesis ..

   223 qed

   224

   225 theorem meet_join_absorb: "x \<sqinter> (x \<squnion> y) = x"

   226 proof

   227   show "x \<sqsubseteq> x" ..

   228   show "x \<sqsubseteq> x \<squnion> y" ..

   229   fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> x \<squnion> y"

   230   show "z \<sqsubseteq> x" by fact

   231 qed

   232

   233 theorem join_meet_absorb: "x \<squnion> (x \<sqinter> y) = x"

   234 proof -

   235   have "dual x \<sqinter> (dual x \<squnion> dual y) = dual x"

   236     by (rule meet_join_absorb)

   237   then have "dual (x \<squnion> (x \<sqinter> y)) = dual x"

   238     by (simp only: dual_meet dual_join)

   239   then show ?thesis ..

   240 qed

   241

   242 text \<open>

   243   \medskip Some further algebraic properties hold as well.  The

   244   property idempotent (I) is a basic algebraic consequence of (AB).

   245 \<close>

   246

   247 theorem meet_idem: "x \<sqinter> x = x"

   248 proof -

   249   have "x \<sqinter> (x \<squnion> (x \<sqinter> x)) = x" by (rule meet_join_absorb)

   250   also have "x \<squnion> (x \<sqinter> x) = x" by (rule join_meet_absorb)

   251   finally show ?thesis .

   252 qed

   253

   254 theorem join_idem: "x \<squnion> x = x"

   255 proof -

   256   have "dual x \<sqinter> dual x = dual x"

   257     by (rule meet_idem)

   258   then have "dual (x \<squnion> x) = dual x"

   259     by (simp only: dual_join)

   260   then show ?thesis ..

   261 qed

   262

   263 text \<open>

   264   Meet and join are trivial for related elements.

   265 \<close>

   266

   267 theorem meet_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"

   268 proof

   269   assume "x \<sqsubseteq> y"

   270   show "x \<sqsubseteq> x" ..

   271   show "x \<sqsubseteq> y" by fact

   272   fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"

   273   show "z \<sqsubseteq> x" by fact

   274 qed

   275

   276 theorem join_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"

   277 proof -

   278   assume "x \<sqsubseteq> y" then have "dual y \<sqsubseteq> dual x" ..

   279   then have "dual y \<sqinter> dual x = dual y" by (rule meet_related)

   280   also have "dual y \<sqinter> dual x = dual (y \<squnion> x)" by (simp only: dual_join)

   281   also have "y \<squnion> x = x \<squnion> y" by (rule join_commute)

   282   finally show ?thesis ..

   283 qed

   284

   285

   286 subsection \<open>Order versus algebraic structure\<close>

   287

   288 text \<open>

   289   The \<open>\<sqinter>\<close> and \<open>\<squnion>\<close> operations are connected with the

   290   underlying \<open>\<sqsubseteq>\<close> relation in a canonical manner.

   291 \<close>

   292

   293 theorem meet_connection: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"

   294 proof

   295   assume "x \<sqsubseteq> y"

   296   then have "is_inf x y x" ..

   297   then show "x \<sqinter> y = x" ..

   298 next

   299   have "x \<sqinter> y \<sqsubseteq> y" ..

   300   also assume "x \<sqinter> y = x"

   301   finally show "x \<sqsubseteq> y" .

   302 qed

   303

   304 theorem join_connection: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"

   305 proof

   306   assume "x \<sqsubseteq> y"

   307   then have "is_sup x y y" ..

   308   then show "x \<squnion> y = y" ..

   309 next

   310   have "x \<sqsubseteq> x \<squnion> y" ..

   311   also assume "x \<squnion> y = y"

   312   finally show "x \<sqsubseteq> y" .

   313 qed

   314

   315 text \<open>

   316   \medskip The most fundamental result of the meta-theory of lattices

   317   is as follows (we do not prove it here).

   318

   319   Given a structure with binary operations \<open>\<sqinter>\<close> and \<open>\<squnion>\<close>

   320   such that (A), (C), and (AB) hold (cf.\

   321   \S\ref{sec:lattice-algebra}).  This structure represents a lattice,

   322   if the relation @{term "x \<sqsubseteq> y"} is defined as @{term "x \<sqinter> y = x"}

   323   (alternatively as @{term "x \<squnion> y = y"}).  Furthermore, infimum and

   324   supremum with respect to this ordering coincide with the original

   325   \<open>\<sqinter>\<close> and \<open>\<squnion>\<close> operations.

   326 \<close>

   327

   328

   329 subsection \<open>Example instances\<close>

   330

   331 subsubsection \<open>Linear orders\<close>

   332

   333 text \<open>

   334   Linear orders with @{term minimum} and @{term maximum} operations

   335   are a (degenerate) example of lattice structures.

   336 \<close>

   337

   338 definition

   339   minimum :: "'a::linear_order \<Rightarrow> 'a \<Rightarrow> 'a" where

   340   "minimum x y = (if x \<sqsubseteq> y then x else y)"

   341 definition

   342   maximum :: "'a::linear_order \<Rightarrow> 'a \<Rightarrow> 'a" where

   343   "maximum x y = (if x \<sqsubseteq> y then y else x)"

   344

   345 lemma is_inf_minimum: "is_inf x y (minimum x y)"

   346 proof

   347   let ?min = "minimum x y"

   348   from leq_linear show "?min \<sqsubseteq> x" by (auto simp add: minimum_def)

   349   from leq_linear show "?min \<sqsubseteq> y" by (auto simp add: minimum_def)

   350   fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"

   351   with leq_linear show "z \<sqsubseteq> ?min" by (auto simp add: minimum_def)

   352 qed

   353

   354 lemma is_sup_maximum: "is_sup x y (maximum x y)"      (* FIXME dualize!? *)

   355 proof

   356   let ?max = "maximum x y"

   357   from leq_linear show "x \<sqsubseteq> ?max" by (auto simp add: maximum_def)

   358   from leq_linear show "y \<sqsubseteq> ?max" by (auto simp add: maximum_def)

   359   fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"

   360   with leq_linear show "?max \<sqsubseteq> z" by (auto simp add: maximum_def)

   361 qed

   362

   363 instance linear_order \<subseteq> lattice

   364 proof

   365   fix x y :: "'a::linear_order"

   366   from is_inf_minimum show "\<exists>inf. is_inf x y inf" ..

   367   from is_sup_maximum show "\<exists>sup. is_sup x y sup" ..

   368 qed

   369

   370 text \<open>

   371   The lattice operations on linear orders indeed coincide with @{term

   372   minimum} and @{term maximum}.

   373 \<close>

   374

   375 theorem meet_mimimum: "x \<sqinter> y = minimum x y"

   376   by (rule meet_equality) (rule is_inf_minimum)

   377

   378 theorem meet_maximum: "x \<squnion> y = maximum x y"

   379   by (rule join_equality) (rule is_sup_maximum)

   380

   381

   382

   383 subsubsection \<open>Binary products\<close>

   384

   385 text \<open>

   386   The class of lattices is closed under direct binary products (cf.\

   387   \S\ref{sec:prod-order}).

   388 \<close>

   389

   390 lemma is_inf_prod: "is_inf p q (fst p \<sqinter> fst q, snd p \<sqinter> snd q)"

   391 proof

   392   show "(fst p \<sqinter> fst q, snd p \<sqinter> snd q) \<sqsubseteq> p"

   393   proof -

   394     have "fst p \<sqinter> fst q \<sqsubseteq> fst p" ..

   395     moreover have "snd p \<sqinter> snd q \<sqsubseteq> snd p" ..

   396     ultimately show ?thesis by (simp add: leq_prod_def)

   397   qed

   398   show "(fst p \<sqinter> fst q, snd p \<sqinter> snd q) \<sqsubseteq> q"

   399   proof -

   400     have "fst p \<sqinter> fst q \<sqsubseteq> fst q" ..

   401     moreover have "snd p \<sqinter> snd q \<sqsubseteq> snd q" ..

   402     ultimately show ?thesis by (simp add: leq_prod_def)

   403   qed

   404   fix r assume rp: "r \<sqsubseteq> p" and rq: "r \<sqsubseteq> q"

   405   show "r \<sqsubseteq> (fst p \<sqinter> fst q, snd p \<sqinter> snd q)"

   406   proof -

   407     have "fst r \<sqsubseteq> fst p \<sqinter> fst q"

   408     proof

   409       from rp show "fst r \<sqsubseteq> fst p" by (simp add: leq_prod_def)

   410       from rq show "fst r \<sqsubseteq> fst q" by (simp add: leq_prod_def)

   411     qed

   412     moreover have "snd r \<sqsubseteq> snd p \<sqinter> snd q"

   413     proof

   414       from rp show "snd r \<sqsubseteq> snd p" by (simp add: leq_prod_def)

   415       from rq show "snd r \<sqsubseteq> snd q" by (simp add: leq_prod_def)

   416     qed

   417     ultimately show ?thesis by (simp add: leq_prod_def)

   418   qed

   419 qed

   420

   421 lemma is_sup_prod: "is_sup p q (fst p \<squnion> fst q, snd p \<squnion> snd q)"  (* FIXME dualize!? *)

   422 proof

   423   show "p \<sqsubseteq> (fst p \<squnion> fst q, snd p \<squnion> snd q)"

   424   proof -

   425     have "fst p \<sqsubseteq> fst p \<squnion> fst q" ..

   426     moreover have "snd p \<sqsubseteq> snd p \<squnion> snd q" ..

   427     ultimately show ?thesis by (simp add: leq_prod_def)

   428   qed

   429   show "q \<sqsubseteq> (fst p \<squnion> fst q, snd p \<squnion> snd q)"

   430   proof -

   431     have "fst q \<sqsubseteq> fst p \<squnion> fst q" ..

   432     moreover have "snd q \<sqsubseteq> snd p \<squnion> snd q" ..

   433     ultimately show ?thesis by (simp add: leq_prod_def)

   434   qed

   435   fix r assume "pr": "p \<sqsubseteq> r" and qr: "q \<sqsubseteq> r"

   436   show "(fst p \<squnion> fst q, snd p \<squnion> snd q) \<sqsubseteq> r"

   437   proof -

   438     have "fst p \<squnion> fst q \<sqsubseteq> fst r"

   439     proof

   440       from "pr" show "fst p \<sqsubseteq> fst r" by (simp add: leq_prod_def)

   441       from qr show "fst q \<sqsubseteq> fst r" by (simp add: leq_prod_def)

   442     qed

   443     moreover have "snd p \<squnion> snd q \<sqsubseteq> snd r"

   444     proof

   445       from "pr" show "snd p \<sqsubseteq> snd r" by (simp add: leq_prod_def)

   446       from qr show "snd q \<sqsubseteq> snd r" by (simp add: leq_prod_def)

   447     qed

   448     ultimately show ?thesis by (simp add: leq_prod_def)

   449   qed

   450 qed

   451

   452 instance prod :: (lattice, lattice) lattice

   453 proof

   454   fix p q :: "'a::lattice \<times> 'b::lattice"

   455   from is_inf_prod show "\<exists>inf. is_inf p q inf" ..

   456   from is_sup_prod show "\<exists>sup. is_sup p q sup" ..

   457 qed

   458

   459 text \<open>

   460   The lattice operations on a binary product structure indeed coincide

   461   with the products of the original ones.

   462 \<close>

   463

   464 theorem meet_prod: "p \<sqinter> q = (fst p \<sqinter> fst q, snd p \<sqinter> snd q)"

   465   by (rule meet_equality) (rule is_inf_prod)

   466

   467 theorem join_prod: "p \<squnion> q = (fst p \<squnion> fst q, snd p \<squnion> snd q)"

   468   by (rule join_equality) (rule is_sup_prod)

   469

   470

   471 subsubsection \<open>General products\<close>

   472

   473 text \<open>

   474   The class of lattices is closed under general products (function

   475   spaces) as well (cf.\ \S\ref{sec:fun-order}).

   476 \<close>

   477

   478 lemma is_inf_fun: "is_inf f g (\<lambda>x. f x \<sqinter> g x)"

   479 proof

   480   show "(\<lambda>x. f x \<sqinter> g x) \<sqsubseteq> f"

   481   proof

   482     fix x show "f x \<sqinter> g x \<sqsubseteq> f x" ..

   483   qed

   484   show "(\<lambda>x. f x \<sqinter> g x) \<sqsubseteq> g"

   485   proof

   486     fix x show "f x \<sqinter> g x \<sqsubseteq> g x" ..

   487   qed

   488   fix h assume hf: "h \<sqsubseteq> f" and hg: "h \<sqsubseteq> g"

   489   show "h \<sqsubseteq> (\<lambda>x. f x \<sqinter> g x)"

   490   proof

   491     fix x

   492     show "h x \<sqsubseteq> f x \<sqinter> g x"

   493     proof

   494       from hf show "h x \<sqsubseteq> f x" ..

   495       from hg show "h x \<sqsubseteq> g x" ..

   496     qed

   497   qed

   498 qed

   499

   500 lemma is_sup_fun: "is_sup f g (\<lambda>x. f x \<squnion> g x)"   (* FIXME dualize!? *)

   501 proof

   502   show "f \<sqsubseteq> (\<lambda>x. f x \<squnion> g x)"

   503   proof

   504     fix x show "f x \<sqsubseteq> f x \<squnion> g x" ..

   505   qed

   506   show "g \<sqsubseteq> (\<lambda>x. f x \<squnion> g x)"

   507   proof

   508     fix x show "g x \<sqsubseteq> f x \<squnion> g x" ..

   509   qed

   510   fix h assume fh: "f \<sqsubseteq> h" and gh: "g \<sqsubseteq> h"

   511   show "(\<lambda>x. f x \<squnion> g x) \<sqsubseteq> h"

   512   proof

   513     fix x

   514     show "f x \<squnion> g x \<sqsubseteq> h x"

   515     proof

   516       from fh show "f x \<sqsubseteq> h x" ..

   517       from gh show "g x \<sqsubseteq> h x" ..

   518     qed

   519   qed

   520 qed

   521

   522 instance "fun" :: (type, lattice) lattice

   523 proof

   524   fix f g :: "'a \<Rightarrow> 'b::lattice"

   525   show "\<exists>inf. is_inf f g inf" by rule (rule is_inf_fun) (* FIXME @{text "from \<dots> show \<dots> .."} does not work!? unification incompleteness!? *)

   526   show "\<exists>sup. is_sup f g sup" by rule (rule is_sup_fun)

   527 qed

   528

   529 text \<open>

   530   The lattice operations on a general product structure (function

   531   space) indeed emerge by point-wise lifting of the original ones.

   532 \<close>

   533

   534 theorem meet_fun: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"

   535   by (rule meet_equality) (rule is_inf_fun)

   536

   537 theorem join_fun: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"

   538   by (rule join_equality) (rule is_sup_fun)

   539

   540

   541 subsection \<open>Monotonicity and semi-morphisms\<close>

   542

   543 text \<open>

   544   The lattice operations are monotone in both argument positions.  In

   545   fact, monotonicity of the second position is trivial due to

   546   commutativity.

   547 \<close>

   548

   549 theorem meet_mono: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> w \<Longrightarrow> x \<sqinter> y \<sqsubseteq> z \<sqinter> w"

   550 proof -

   551   {

   552     fix a b c :: "'a::lattice"

   553     assume "a \<sqsubseteq> c" have "a \<sqinter> b \<sqsubseteq> c \<sqinter> b"

   554     proof

   555       have "a \<sqinter> b \<sqsubseteq> a" ..

   556       also have "\<dots> \<sqsubseteq> c" by fact

   557       finally show "a \<sqinter> b \<sqsubseteq> c" .

   558       show "a \<sqinter> b \<sqsubseteq> b" ..

   559     qed

   560   } note this [elim?]

   561   assume "x \<sqsubseteq> z" then have "x \<sqinter> y \<sqsubseteq> z \<sqinter> y" ..

   562   also have "\<dots> = y \<sqinter> z" by (rule meet_commute)

   563   also assume "y \<sqsubseteq> w" then have "y \<sqinter> z \<sqsubseteq> w \<sqinter> z" ..

   564   also have "\<dots> = z \<sqinter> w" by (rule meet_commute)

   565   finally show ?thesis .

   566 qed

   567

   568 theorem join_mono: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> w \<Longrightarrow> x \<squnion> y \<sqsubseteq> z \<squnion> w"

   569 proof -

   570   assume "x \<sqsubseteq> z" then have "dual z \<sqsubseteq> dual x" ..

   571   moreover assume "y \<sqsubseteq> w" then have "dual w \<sqsubseteq> dual y" ..

   572   ultimately have "dual z \<sqinter> dual w \<sqsubseteq> dual x \<sqinter> dual y"

   573     by (rule meet_mono)

   574   then have "dual (z \<squnion> w) \<sqsubseteq> dual (x \<squnion> y)"

   575     by (simp only: dual_join)

   576   then show ?thesis ..

   577 qed

   578

   579 text \<open>

   580   \medskip A semi-morphisms is a function \<open>f\<close> that preserves the

   581   lattice operations in the following manner: @{term "f (x \<sqinter> y) \<sqsubseteq> f x

   582   \<sqinter> f y"} and @{term "f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)"}, respectively.  Any of

   583   these properties is equivalent with monotonicity.

   584 \<close>

   585

   586 theorem meet_semimorph:

   587   "(\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y) \<equiv> (\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y)"

   588 proof

   589   assume morph: "\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"

   590   fix x y :: "'a::lattice"

   591   assume "x \<sqsubseteq> y"

   592   then have "x \<sqinter> y = x" ..

   593   then have "x = x \<sqinter> y" ..

   594   also have "f \<dots> \<sqsubseteq> f x \<sqinter> f y" by (rule morph)

   595   also have "\<dots> \<sqsubseteq> f y" ..

   596   finally show "f x \<sqsubseteq> f y" .

   597 next

   598   assume mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"

   599   show "\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"

   600   proof -

   601     fix x y

   602     show "f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"

   603     proof

   604       have "x \<sqinter> y \<sqsubseteq> x" .. then show "f (x \<sqinter> y) \<sqsubseteq> f x" by (rule mono)

   605       have "x \<sqinter> y \<sqsubseteq> y" .. then show "f (x \<sqinter> y) \<sqsubseteq> f y" by (rule mono)

   606     qed

   607   qed

   608 qed

   609

   610 lemma join_semimorph:

   611   "(\<And>x y. f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)) \<equiv> (\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y)"

   612 proof

   613   assume morph: "\<And>x y. f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)"

   614   fix x y :: "'a::lattice"

   615   assume "x \<sqsubseteq> y" then have "x \<squnion> y = y" ..

   616   have "f x \<sqsubseteq> f x \<squnion> f y" ..

   617   also have "\<dots> \<sqsubseteq> f (x \<squnion> y)" by (rule morph)

   618   also from \<open>x \<sqsubseteq> y\<close> have "x \<squnion> y = y" ..

   619   finally show "f x \<sqsubseteq> f y" .

   620 next

   621   assume mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"

   622   show "\<And>x y. f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)"

   623   proof -

   624     fix x y

   625     show "f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)"

   626     proof

   627       have "x \<sqsubseteq> x \<squnion> y" .. then show "f x \<sqsubseteq> f (x \<squnion> y)" by (rule mono)

   628       have "y \<sqsubseteq> x \<squnion> y" .. then show "f y \<sqsubseteq> f (x \<squnion> y)" by (rule mono)

   629     qed

   630   qed

   631 qed

   632

   633 end