src/HOL/Lattice/Lattice.thy
 author nipkow Thu Dec 11 08:52:50 2008 +0100 (2008-12-11) changeset 29106 25e28a4070f3 parent 25469 f81b3be9dfdd child 35317 d57da4abb47d permissions -rw-r--r--
Testfile for Stefan's code generator
     1 (*  Title:      HOL/Lattice/Lattice.thy

     2     ID:         $Id$

     3     Author:     Markus Wenzel, TU Muenchen

     4 *)

     5

     6 header {* Lattices *}

     7

     8 theory Lattice imports Bounds begin

     9

    10 subsection {* Lattice operations *}

    11

    12 text {*

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

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

    15   as well).

    16 *}

    17

    18 axclass lattice \<subseteq> partial_order

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

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

    21

    22 text {*

    23   The @{text \<sqinter>} (meet) and @{text \<squnion>} (join) operations select such

    24   infimum and supremum elements.

    25 *}

    26

    27 definition

    28   meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "&&" 70) where

    29   "x && y = (THE inf. is_inf x y inf)"

    30 definition

    31   join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "||" 65) where

    32   "x || y = (THE sup. is_sup x y sup)"

    33

    34 notation (xsymbols)

    35   meet  (infixl "\<sqinter>" 70) and

    36   join  (infixl "\<squnion>" 65)

    37

    38 text {*

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

    40   exhibited as follows.

    41 *}

    42

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

    44 proof (unfold meet_def)

    45   assume "is_inf x y inf"

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

    47     by (rule the_equality) (rule is_inf_uniq [OF _ is_inf x y inf])

    48 qed

    49

    50 lemma meetI [intro?]:

    51     "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"

    52   by (rule meet_equality, rule is_infI) blast+

    53

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

    55 proof (unfold join_def)

    56   assume "is_sup x y sup"

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

    58     by (rule the_equality) (rule is_sup_uniq [OF _ is_sup x y sup])

    59 qed

    60

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

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

    63   by (rule join_equality, rule is_supI) blast+

    64

    65

    66 text {*

    67   \medskip The @{text \<sqinter>} and @{text \<squnion>} operations indeed determine

    68   bounds on a lattice structure.

    69 *}

    70

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

    72 proof (unfold meet_def)

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

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

    75     by (rule theI) (rule is_inf_uniq [OF _ is_inf x y inf])

    76 qed

    77

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

    79   by (rule is_inf_greatest) (rule is_inf_meet)

    80

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

    82   by (rule is_inf_lower) (rule is_inf_meet)

    83

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

    85   by (rule is_inf_lower) (rule is_inf_meet)

    86

    87

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

    89 proof (unfold join_def)

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

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

    92     by (rule theI) (rule is_sup_uniq [OF _ is_sup x y sup])

    93 qed

    94

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

    96   by (rule is_sup_least) (rule is_sup_join)

    97

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

    99   by (rule is_sup_upper) (rule is_sup_join)

   100

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

   102   by (rule is_sup_upper) (rule is_sup_join)

   103

   104

   105 subsection {* Duality *}

   106

   107 text {*

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

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

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

   111   of lattice theory.

   112 *}

   113

   114 instance dual :: (lattice) lattice

   115 proof

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

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

   118   proof -

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

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

   121       by (simp only: dual_inf)

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

   123   qed

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

   125   proof -

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

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

   128       by (simp only: dual_sup)

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

   130   qed

   131 qed

   132

   133 text {*

   134   Apparently, the @{text \<sqinter>} and @{text \<squnion>} operations are dual to each

   135   other.

   136 *}

   137

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

   139 proof -

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

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

   142   then show ?thesis ..

   143 qed

   144

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

   146 proof -

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

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

   149   then show ?thesis ..

   150 qed

   151

   152

   153 subsection {* Algebraic properties \label{sec:lattice-algebra} *}

   154

   155 text {*

   156   The @{text \<sqinter>} and @{text \<squnion>} operations have the following

   157   characteristic algebraic properties: associative (A), commutative

   158   (C), and absorptive (AB).

   159 *}

   160

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

   162 proof

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

   164   proof

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

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

   167     proof -

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

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

   170       finally show ?thesis .

   171     qed

   172   qed

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

   174   proof -

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

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

   177     finally show ?thesis .

   178   qed

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

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

   181   proof

   182     show "w \<sqsubseteq> x"

   183     proof -

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

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

   186       finally show ?thesis .

   187     qed

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

   189     proof

   190       show "w \<sqsubseteq> y"

   191       proof -

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

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

   194         finally show ?thesis .

   195       qed

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

   197     qed

   198   qed

   199 qed

   200

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

   202 proof -

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

   204     by (simp only: dual_join)

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

   206     by (rule meet_assoc)

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

   208     by (simp only: dual_join)

   209   finally show ?thesis ..

   210 qed

   211

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

   213 proof

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

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

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

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

   218 qed

   219

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

   221 proof -

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

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

   224     by (rule meet_commute)

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

   226     by (simp only: dual_join)

   227   finally show ?thesis ..

   228 qed

   229

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

   231 proof

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

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

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

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

   236 qed

   237

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

   239 proof -

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

   241     by (rule meet_join_absorb)

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

   243     by (simp only: dual_meet dual_join)

   244   then show ?thesis ..

   245 qed

   246

   247 text {*

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

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

   250 *}

   251

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

   253 proof -

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

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

   256   finally show ?thesis .

   257 qed

   258

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

   260 proof -

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

   262     by (rule meet_idem)

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

   264     by (simp only: dual_join)

   265   then show ?thesis ..

   266 qed

   267

   268 text {*

   269   Meet and join are trivial for related elements.

   270 *}

   271

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

   273 proof

   274   assume "x \<sqsubseteq> y"

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

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

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

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

   279 qed

   280

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

   282 proof -

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

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

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

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

   287   finally show ?thesis ..

   288 qed

   289

   290

   291 subsection {* Order versus algebraic structure *}

   292

   293 text {*

   294   The @{text \<sqinter>} and @{text \<squnion>} operations are connected with the

   295   underlying @{text \<sqsubseteq>} relation in a canonical manner.

   296 *}

   297

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

   299 proof

   300   assume "x \<sqsubseteq> y"

   301   then have "is_inf x y x" ..

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

   303 next

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

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

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

   307 qed

   308

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

   310 proof

   311   assume "x \<sqsubseteq> y"

   312   then have "is_sup x y y" ..

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

   314 next

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

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

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

   318 qed

   319

   320 text {*

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

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

   323

   324   Given a structure with binary operations @{text \<sqinter>} and @{text \<squnion>}

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

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

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

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

   329   supremum with respect to this ordering coincide with the original

   330   @{text \<sqinter>} and @{text \<squnion>} operations.

   331 *}

   332

   333

   334 subsection {* Example instances *}

   335

   336 subsubsection {* Linear orders *}

   337

   338 text {*

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

   340   are a (degenerate) example of lattice structures.

   341 *}

   342

   343 definition

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

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

   346 definition

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

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

   349

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

   351 proof

   352   let ?min = "minimum x y"

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

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

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

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

   357 qed

   358

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

   360 proof

   361   let ?max = "maximum x y"

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

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

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

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

   366 qed

   367

   368 instance linear_order \<subseteq> lattice

   369 proof

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

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

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

   373 qed

   374

   375 text {*

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

   377   minimum} and @{term maximum}.

   378 *}

   379

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

   381   by (rule meet_equality) (rule is_inf_minimum)

   382

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

   384   by (rule join_equality) (rule is_sup_maximum)

   385

   386

   387

   388 subsubsection {* Binary products *}

   389

   390 text {*

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

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

   393 *}

   394

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

   396 proof

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

   398   proof -

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

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

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

   402   qed

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

   404   proof -

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

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

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

   408   qed

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

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

   411   proof -

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

   413     proof

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

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

   416     qed

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

   418     proof

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

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

   421     qed

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

   423   qed

   424 qed

   425

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

   427 proof

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

   429   proof -

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

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

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

   433   qed

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

   435   proof -

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

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

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

   439   qed

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

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

   442   proof -

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

   444     proof

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

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

   447     qed

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

   449     proof

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

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

   452     qed

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

   454   qed

   455 qed

   456

   457 instance * :: (lattice, lattice) lattice

   458 proof

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

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

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

   462 qed

   463

   464 text {*

   465   The lattice operations on a binary product structure indeed coincide

   466   with the products of the original ones.

   467 *}

   468

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

   470   by (rule meet_equality) (rule is_inf_prod)

   471

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

   473   by (rule join_equality) (rule is_sup_prod)

   474

   475

   476 subsubsection {* General products *}

   477

   478 text {*

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

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

   481 *}

   482

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

   484 proof

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

   486   proof

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

   488   qed

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

   490   proof

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

   492   qed

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

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

   495   proof

   496     fix x

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

   498     proof

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

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

   501     qed

   502   qed

   503 qed

   504

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

   506 proof

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

   508   proof

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

   510   qed

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

   512   proof

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

   514   qed

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

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

   517   proof

   518     fix x

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

   520     proof

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

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

   523     qed

   524   qed

   525 qed

   526

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

   528 proof

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

   530   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!? *)

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

   532 qed

   533

   534 text {*

   535   The lattice operations on a general product structure (function

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

   537 *}

   538

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

   540   by (rule meet_equality) (rule is_inf_fun)

   541

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

   543   by (rule join_equality) (rule is_sup_fun)

   544

   545

   546 subsection {* Monotonicity and semi-morphisms *}

   547

   548 text {*

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

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

   551   commutativity.

   552 *}

   553

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

   555 proof -

   556   {

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

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

   559     proof

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

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

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

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

   564     qed

   565   } note this [elim?]

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

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

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

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

   570   finally show ?thesis .

   571 qed

   572

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

   574 proof -

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

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

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

   578     by (rule meet_mono)

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

   580     by (simp only: dual_join)

   581   then show ?thesis ..

   582 qed

   583

   584 text {*

   585   \medskip A semi-morphisms is a function @{text f} that preserves the

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

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

   588   these properties is equivalent with monotonicity.

   589 *}

   590

   591 theorem meet_semimorph:

   592   "(\<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)"

   593 proof

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

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

   596   assume "x \<sqsubseteq> y"

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

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

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

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

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

   602 next

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

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

   605   proof -

   606     fix x y

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

   608     proof

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

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

   611     qed

   612   qed

   613 qed

   614

   615 lemma join_semimorph:

   616   "(\<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)"

   617 proof

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

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

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

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

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

   623   also from x \<sqsubseteq> y have "x \<squnion> y = y" ..

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

   625 next

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

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

   628   proof -

   629     fix x y

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

   631     proof

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

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

   634     qed

   635   qed

   636 qed

   637

   638 end