src/HOL/Lattice/Lattice.thy
author wenzelm
Thu May 24 17:25:53 2012 +0200 (2012-05-24)
changeset 47988 e4b69e10b990
parent 37678 0040bafffdef
child 58879 143c85e3cdb5
permissions -rw-r--r--
tuned proofs;
     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 prod :: (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