src/HOL/Lattice/Lattice.thy
 author haftmann Wed Jun 30 16:46:44 2010 +0200 (2010-06-30) changeset 37659 14cabf5fa710 parent 35317 d57da4abb47d child 37678 0040bafffdef permissions -rw-r--r--
more speaking names
     1 (*  Title:      HOL/Lattice/Lattice.thy

     2     Author:     Markus Wenzel, TU Muenchen

     3 *)

     4

     5 header {* Lattices *}

     6

     7 theory Lattice imports Bounds begin

     8

     9 subsection {* Lattice operations *}

    10

    11 text {*

    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 *}

    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 {*

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

    23   infimum and supremum elements.

    24 *}

    25

    26 definition

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

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

    29 definition

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

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

    32

    33 notation (xsymbols)

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

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

    36

    37 text {*

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

    39   exhibited as follows.

    40 *}

    41

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

    43 proof (unfold meet_def)

    44   assume "is_inf x y inf"

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

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

    47 qed

    48

    49 lemma meetI [intro?]:

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

    51   by (rule meet_equality, rule is_infI) blast+

    52

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

    54 proof (unfold join_def)

    55   assume "is_sup x y sup"

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

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

    58 qed

    59

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

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

    62   by (rule join_equality, rule is_supI) blast+

    63

    64

    65 text {*

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

    67   bounds on a lattice structure.

    68 *}

    69

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

    71 proof (unfold meet_def)

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

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

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

    75 qed

    76

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

    78   by (rule is_inf_greatest) (rule is_inf_meet)

    79

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

    81   by (rule is_inf_lower) (rule is_inf_meet)

    82

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

    84   by (rule is_inf_lower) (rule is_inf_meet)

    85

    86

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

    88 proof (unfold join_def)

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

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

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

    92 qed

    93

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

    95   by (rule is_sup_least) (rule is_sup_join)

    96

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

    98   by (rule is_sup_upper) (rule is_sup_join)

    99

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

   101   by (rule is_sup_upper) (rule is_sup_join)

   102

   103

   104 subsection {* Duality *}

   105

   106 text {*

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

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

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

   110   of lattice theory.

   111 *}

   112

   113 instance dual :: (lattice) lattice

   114 proof

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

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

   117   proof -

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

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

   120       by (simp only: dual_inf)

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

   122   qed

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

   124   proof -

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

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

   127       by (simp only: dual_sup)

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

   129   qed

   130 qed

   131

   132 text {*

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

   134   other.

   135 *}

   136

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

   138 proof -

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

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

   141   then show ?thesis ..

   142 qed

   143

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

   145 proof -

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

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

   148   then show ?thesis ..

   149 qed

   150

   151

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

   153

   154 text {*

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

   156   characteristic algebraic properties: associative (A), commutative

   157   (C), and absorptive (AB).

   158 *}

   159

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

   161 proof

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

   163   proof

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

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

   166     proof -

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

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

   169       finally show ?thesis .

   170     qed

   171   qed

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

   173   proof -

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

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

   176     finally show ?thesis .

   177   qed

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

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

   180   proof

   181     show "w \<sqsubseteq> x"

   182     proof -

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

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

   185       finally show ?thesis .

   186     qed

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

   188     proof

   189       show "w \<sqsubseteq> y"

   190       proof -

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

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

   193         finally show ?thesis .

   194       qed

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

   196     qed

   197   qed

   198 qed

   199

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

   201 proof -

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

   203     by (simp only: dual_join)

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

   205     by (rule meet_assoc)

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

   207     by (simp only: dual_join)

   208   finally show ?thesis ..

   209 qed

   210

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

   212 proof

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

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

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

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

   217 qed

   218

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

   220 proof -

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

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

   223     by (rule meet_commute)

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

   225     by (simp only: dual_join)

   226   finally show ?thesis ..

   227 qed

   228

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

   230 proof

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

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

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

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

   235 qed

   236

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

   238 proof -

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

   240     by (rule meet_join_absorb)

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

   242     by (simp only: dual_meet dual_join)

   243   then show ?thesis ..

   244 qed

   245

   246 text {*

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

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

   249 *}

   250

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

   252 proof -

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

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

   255   finally show ?thesis .

   256 qed

   257

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

   259 proof -

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

   261     by (rule meet_idem)

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

   263     by (simp only: dual_join)

   264   then show ?thesis ..

   265 qed

   266

   267 text {*

   268   Meet and join are trivial for related elements.

   269 *}

   270

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

   272 proof

   273   assume "x \<sqsubseteq> y"

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

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

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

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

   278 qed

   279

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

   281 proof -

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

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

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

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

   286   finally show ?thesis ..

   287 qed

   288

   289

   290 subsection {* Order versus algebraic structure *}

   291

   292 text {*

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

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

   295 *}

   296

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

   298 proof

   299   assume "x \<sqsubseteq> y"

   300   then have "is_inf x y x" ..

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

   302 next

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

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

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

   306 qed

   307

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

   309 proof

   310   assume "x \<sqsubseteq> y"

   311   then have "is_sup x y y" ..

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

   313 next

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

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

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

   317 qed

   318

   319 text {*

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

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

   322

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

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

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

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

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

   328   supremum with respect to this ordering coincide with the original

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

   330 *}

   331

   332

   333 subsection {* Example instances *}

   334

   335 subsubsection {* Linear orders *}

   336

   337 text {*

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

   339   are a (degenerate) example of lattice structures.

   340 *}

   341

   342 definition

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

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

   345 definition

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

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

   348

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

   350 proof

   351   let ?min = "minimum x y"

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

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

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

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

   356 qed

   357

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

   359 proof

   360   let ?max = "maximum x y"

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

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

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

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

   365 qed

   366

   367 instance linear_order \<subseteq> lattice

   368 proof

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

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

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

   372 qed

   373

   374 text {*

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

   376   minimum} and @{term maximum}.

   377 *}

   378

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

   380   by (rule meet_equality) (rule is_inf_minimum)

   381

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

   383   by (rule join_equality) (rule is_sup_maximum)

   384

   385

   386

   387 subsubsection {* Binary products *}

   388

   389 text {*

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

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

   392 *}

   393

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

   395 proof

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

   397   proof -

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

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

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

   401   qed

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

   403   proof -

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

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

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

   407   qed

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

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

   410   proof -

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

   412     proof

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

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

   415     qed

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

   417     proof

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

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

   420     qed

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

   422   qed

   423 qed

   424

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

   426 proof

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

   428   proof -

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

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

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

   432   qed

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

   434   proof -

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

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

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

   438   qed

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

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

   441   proof -

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

   443     proof

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

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

   446     qed

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

   448     proof

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

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

   451     qed

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

   453   qed

   454 qed

   455

   456 instance * :: (lattice, lattice) lattice

   457 proof

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

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

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

   461 qed

   462

   463 text {*

   464   The lattice operations on a binary product structure indeed coincide

   465   with the products of the original ones.

   466 *}

   467

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

   469   by (rule meet_equality) (rule is_inf_prod)

   470

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

   472   by (rule join_equality) (rule is_sup_prod)

   473

   474

   475 subsubsection {* General products *}

   476

   477 text {*

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

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

   480 *}

   481

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

   483 proof

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

   485   proof

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

   487   qed

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

   489   proof

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

   491   qed

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

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

   494   proof

   495     fix x

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

   497     proof

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

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

   500     qed

   501   qed

   502 qed

   503

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

   505 proof

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

   507   proof

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

   509   qed

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

   511   proof

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

   513   qed

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

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

   516   proof

   517     fix x

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

   519     proof

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

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

   522     qed

   523   qed

   524 qed

   525

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

   527 proof

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

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

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

   531 qed

   532

   533 text {*

   534   The lattice operations on a general product structure (function

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

   536 *}

   537

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

   539   by (rule meet_equality) (rule is_inf_fun)

   540

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

   542   by (rule join_equality) (rule is_sup_fun)

   543

   544

   545 subsection {* Monotonicity and semi-morphisms *}

   546

   547 text {*

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

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

   550   commutativity.

   551 *}

   552

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

   554 proof -

   555   {

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

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

   558     proof

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

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

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

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

   563     qed

   564   } note this [elim?]

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

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

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

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

   569   finally show ?thesis .

   570 qed

   571

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

   573 proof -

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

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

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

   577     by (rule meet_mono)

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

   579     by (simp only: dual_join)

   580   then show ?thesis ..

   581 qed

   582

   583 text {*

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

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

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

   587   these properties is equivalent with monotonicity.

   588 *}

   589

   590 theorem meet_semimorph:

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

   592 proof

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

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

   595   assume "x \<sqsubseteq> y"

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

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

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

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

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

   601 next

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

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

   604   proof -

   605     fix x y

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

   607     proof

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

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

   610     qed

   611   qed

   612 qed

   613

   614 lemma join_semimorph:

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

   616 proof

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

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

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

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

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

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

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

   624 next

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

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

   627   proof -

   628     fix x y

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

   630     proof

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

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

   633     qed

   634   qed

   635 qed

   636

   637 end