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