src/HOL/Lattice/Lattice.thy
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 61986 2461779da2b8
child 69597 ff784d5a5bfb
permissions -rw-r--r--
tuned;
     1 (*  Title:      HOL/Lattice/Lattice.thy
     2     Author:     Markus Wenzel, TU Muenchen
     3 *)
     4 
     5 section \<open>Lattices\<close>
     6 
     7 theory Lattice imports Bounds begin
     8 
     9 subsection \<open>Lattice operations\<close>
    10 
    11 text \<open>
    12   A \emph{lattice} is a partial order with infimum and supremum of any
    13   two elements (thus any \emph{finite} number of elements have bounds
    14   as well).
    15 \<close>
    16 
    17 class lattice =
    18   assumes ex_inf: "\<exists>inf. is_inf x y inf"
    19   assumes ex_sup: "\<exists>sup. is_sup x y sup"
    20 
    21 text \<open>
    22   The \<open>\<sqinter>\<close> (meet) and \<open>\<squnion>\<close> (join) operations select such
    23   infimum and supremum elements.
    24 \<close>
    25 
    26 definition
    27   meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<sqinter>" 70) where
    28   "x \<sqinter> y = (THE inf. is_inf x y inf)"
    29 definition
    30   join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<squnion>" 65) where
    31   "x \<squnion> y = (THE sup. is_sup x y sup)"
    32 
    33 text \<open>
    34   Due to unique existence of bounds, the lattice operations may be
    35   exhibited as follows.
    36 \<close>
    37 
    38 lemma meet_equality [elim?]: "is_inf x y inf \<Longrightarrow> x \<sqinter> y = inf"
    39 proof (unfold meet_def)
    40   assume "is_inf x y inf"
    41   then show "(THE inf. is_inf x y inf) = inf"
    42     by (rule the_equality) (rule is_inf_uniq [OF _ \<open>is_inf x y inf\<close>])
    43 qed
    44 
    45 lemma meetI [intro?]:
    46     "inf \<sqsubseteq> x \<Longrightarrow> inf \<sqsubseteq> y \<Longrightarrow> (\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> inf) \<Longrightarrow> x \<sqinter> y = inf"
    47   by (rule meet_equality, rule is_infI) blast+
    48 
    49 lemma join_equality [elim?]: "is_sup x y sup \<Longrightarrow> x \<squnion> y = sup"
    50 proof (unfold join_def)
    51   assume "is_sup x y sup"
    52   then show "(THE sup. is_sup x y sup) = sup"
    53     by (rule the_equality) (rule is_sup_uniq [OF _ \<open>is_sup x y sup\<close>])
    54 qed
    55 
    56 lemma joinI [intro?]: "x \<sqsubseteq> sup \<Longrightarrow> y \<sqsubseteq> sup \<Longrightarrow>
    57     (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> sup \<sqsubseteq> z) \<Longrightarrow> x \<squnion> y = sup"
    58   by (rule join_equality, rule is_supI) blast+
    59 
    60 
    61 text \<open>
    62   \medskip The \<open>\<sqinter>\<close> and \<open>\<squnion>\<close> operations indeed determine
    63   bounds on a lattice structure.
    64 \<close>
    65 
    66 lemma is_inf_meet [intro?]: "is_inf x y (x \<sqinter> y)"
    67 proof (unfold meet_def)
    68   from ex_inf obtain inf where "is_inf x y inf" ..
    69   then show "is_inf x y (THE inf. is_inf x y inf)"
    70     by (rule theI) (rule is_inf_uniq [OF _ \<open>is_inf x y inf\<close>])
    71 qed
    72 
    73 lemma meet_greatest [intro?]: "z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> x \<sqinter> y"
    74   by (rule is_inf_greatest) (rule is_inf_meet)
    75 
    76 lemma meet_lower1 [intro?]: "x \<sqinter> y \<sqsubseteq> x"
    77   by (rule is_inf_lower) (rule is_inf_meet)
    78 
    79 lemma meet_lower2 [intro?]: "x \<sqinter> y \<sqsubseteq> y"
    80   by (rule is_inf_lower) (rule is_inf_meet)
    81 
    82 
    83 lemma is_sup_join [intro?]: "is_sup x y (x \<squnion> y)"
    84 proof (unfold join_def)
    85   from ex_sup obtain sup where "is_sup x y sup" ..
    86   then show "is_sup x y (THE sup. is_sup x y sup)"
    87     by (rule theI) (rule is_sup_uniq [OF _ \<open>is_sup x y sup\<close>])
    88 qed
    89 
    90 lemma join_least [intro?]: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
    91   by (rule is_sup_least) (rule is_sup_join)
    92 
    93 lemma join_upper1 [intro?]: "x \<sqsubseteq> x \<squnion> y"
    94   by (rule is_sup_upper) (rule is_sup_join)
    95 
    96 lemma join_upper2 [intro?]: "y \<sqsubseteq> x \<squnion> y"
    97   by (rule is_sup_upper) (rule is_sup_join)
    98 
    99 
   100 subsection \<open>Duality\<close>
   101 
   102 text \<open>
   103   The class of lattices is closed under formation of dual structures.
   104   This means that for any theorem of lattice theory, the dualized
   105   statement holds as well; this important fact simplifies many proofs
   106   of lattice theory.
   107 \<close>
   108 
   109 instance dual :: (lattice) lattice
   110 proof
   111   fix x' y' :: "'a::lattice dual"
   112   show "\<exists>inf'. is_inf x' y' inf'"
   113   proof -
   114     have "\<exists>sup. is_sup (undual x') (undual y') sup" by (rule ex_sup)
   115     then have "\<exists>sup. is_inf (dual (undual x')) (dual (undual y')) (dual sup)"
   116       by (simp only: dual_inf)
   117     then show ?thesis by (simp add: dual_ex [symmetric])
   118   qed
   119   show "\<exists>sup'. is_sup x' y' sup'"
   120   proof -
   121     have "\<exists>inf. is_inf (undual x') (undual y') inf" by (rule ex_inf)
   122     then have "\<exists>inf. is_sup (dual (undual x')) (dual (undual y')) (dual inf)"
   123       by (simp only: dual_sup)
   124     then show ?thesis by (simp add: dual_ex [symmetric])
   125   qed
   126 qed
   127 
   128 text \<open>
   129   Apparently, the \<open>\<sqinter>\<close> and \<open>\<squnion>\<close> operations are dual to each
   130   other.
   131 \<close>
   132 
   133 theorem dual_meet [intro?]: "dual (x \<sqinter> y) = dual x \<squnion> dual y"
   134 proof -
   135   from is_inf_meet have "is_sup (dual x) (dual y) (dual (x \<sqinter> y))" ..
   136   then have "dual x \<squnion> dual y = dual (x \<sqinter> y)" ..
   137   then show ?thesis ..
   138 qed
   139 
   140 theorem dual_join [intro?]: "dual (x \<squnion> y) = dual x \<sqinter> dual y"
   141 proof -
   142   from is_sup_join have "is_inf (dual x) (dual y) (dual (x \<squnion> y))" ..
   143   then have "dual x \<sqinter> dual y = dual (x \<squnion> y)" ..
   144   then show ?thesis ..
   145 qed
   146 
   147 
   148 subsection \<open>Algebraic properties \label{sec:lattice-algebra}\<close>
   149 
   150 text \<open>
   151   The \<open>\<sqinter>\<close> and \<open>\<squnion>\<close> operations have the following
   152   characteristic algebraic properties: associative (A), commutative
   153   (C), and absorptive (AB).
   154 \<close>
   155 
   156 theorem meet_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
   157 proof
   158   show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x \<sqinter> y"
   159   proof
   160     show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x" ..
   161     show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y"
   162     proof -
   163       have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..
   164       also have "\<dots> \<sqsubseteq> y" ..
   165       finally show ?thesis .
   166     qed
   167   qed
   168   show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> z"
   169   proof -
   170     have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..
   171     also have "\<dots> \<sqsubseteq> z" ..
   172     finally show ?thesis .
   173   qed
   174   fix w assume "w \<sqsubseteq> x \<sqinter> y" and "w \<sqsubseteq> z"
   175   show "w \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
   176   proof
   177     show "w \<sqsubseteq> x"
   178     proof -
   179       have "w \<sqsubseteq> x \<sqinter> y" by fact
   180       also have "\<dots> \<sqsubseteq> x" ..
   181       finally show ?thesis .
   182     qed
   183     show "w \<sqsubseteq> y \<sqinter> z"
   184     proof
   185       show "w \<sqsubseteq> y"
   186       proof -
   187         have "w \<sqsubseteq> x \<sqinter> y" by fact
   188         also have "\<dots> \<sqsubseteq> y" ..
   189         finally show ?thesis .
   190       qed
   191       show "w \<sqsubseteq> z" by fact
   192     qed
   193   qed
   194 qed
   195 
   196 theorem join_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
   197 proof -
   198   have "dual ((x \<squnion> y) \<squnion> z) = (dual x \<sqinter> dual y) \<sqinter> dual z"
   199     by (simp only: dual_join)
   200   also have "\<dots> = dual x \<sqinter> (dual y \<sqinter> dual z)"
   201     by (rule meet_assoc)
   202   also have "\<dots> = dual (x \<squnion> (y \<squnion> z))"
   203     by (simp only: dual_join)
   204   finally show ?thesis ..
   205 qed
   206 
   207 theorem meet_commute: "x \<sqinter> y = y \<sqinter> x"
   208 proof
   209   show "y \<sqinter> x \<sqsubseteq> x" ..
   210   show "y \<sqinter> x \<sqsubseteq> y" ..
   211   fix z assume "z \<sqsubseteq> y" and "z \<sqsubseteq> x"
   212   then show "z \<sqsubseteq> y \<sqinter> x" ..
   213 qed
   214 
   215 theorem join_commute: "x \<squnion> y = y \<squnion> x"
   216 proof -
   217   have "dual (x \<squnion> y) = dual x \<sqinter> dual y" ..
   218   also have "\<dots> = dual y \<sqinter> dual x"
   219     by (rule meet_commute)
   220   also have "\<dots> = dual (y \<squnion> x)"
   221     by (simp only: dual_join)
   222   finally show ?thesis ..
   223 qed
   224 
   225 theorem meet_join_absorb: "x \<sqinter> (x \<squnion> y) = x"
   226 proof
   227   show "x \<sqsubseteq> x" ..
   228   show "x \<sqsubseteq> x \<squnion> y" ..
   229   fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> x \<squnion> y"
   230   show "z \<sqsubseteq> x" by fact
   231 qed
   232 
   233 theorem join_meet_absorb: "x \<squnion> (x \<sqinter> y) = x"
   234 proof -
   235   have "dual x \<sqinter> (dual x \<squnion> dual y) = dual x"
   236     by (rule meet_join_absorb)
   237   then have "dual (x \<squnion> (x \<sqinter> y)) = dual x"
   238     by (simp only: dual_meet dual_join)
   239   then show ?thesis ..
   240 qed
   241 
   242 text \<open>
   243   \medskip Some further algebraic properties hold as well.  The
   244   property idempotent (I) is a basic algebraic consequence of (AB).
   245 \<close>
   246 
   247 theorem meet_idem: "x \<sqinter> x = x"
   248 proof -
   249   have "x \<sqinter> (x \<squnion> (x \<sqinter> x)) = x" by (rule meet_join_absorb)
   250   also have "x \<squnion> (x \<sqinter> x) = x" by (rule join_meet_absorb)
   251   finally show ?thesis .
   252 qed
   253 
   254 theorem join_idem: "x \<squnion> x = x"
   255 proof -
   256   have "dual x \<sqinter> dual x = dual x"
   257     by (rule meet_idem)
   258   then have "dual (x \<squnion> x) = dual x"
   259     by (simp only: dual_join)
   260   then show ?thesis ..
   261 qed
   262 
   263 text \<open>
   264   Meet and join are trivial for related elements.
   265 \<close>
   266 
   267 theorem meet_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
   268 proof
   269   assume "x \<sqsubseteq> y"
   270   show "x \<sqsubseteq> x" ..
   271   show "x \<sqsubseteq> y" by fact
   272   fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"
   273   show "z \<sqsubseteq> x" by fact
   274 qed
   275 
   276 theorem join_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
   277 proof -
   278   assume "x \<sqsubseteq> y" then have "dual y \<sqsubseteq> dual x" ..
   279   then have "dual y \<sqinter> dual x = dual y" by (rule meet_related)
   280   also have "dual y \<sqinter> dual x = dual (y \<squnion> x)" by (simp only: dual_join)
   281   also have "y \<squnion> x = x \<squnion> y" by (rule join_commute)
   282   finally show ?thesis ..
   283 qed
   284 
   285 
   286 subsection \<open>Order versus algebraic structure\<close>
   287 
   288 text \<open>
   289   The \<open>\<sqinter>\<close> and \<open>\<squnion>\<close> operations are connected with the
   290   underlying \<open>\<sqsubseteq>\<close> relation in a canonical manner.
   291 \<close>
   292 
   293 theorem meet_connection: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
   294 proof
   295   assume "x \<sqsubseteq> y"
   296   then have "is_inf x y x" ..
   297   then show "x \<sqinter> y = x" ..
   298 next
   299   have "x \<sqinter> y \<sqsubseteq> y" ..
   300   also assume "x \<sqinter> y = x"
   301   finally show "x \<sqsubseteq> y" .
   302 qed
   303 
   304 theorem join_connection: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
   305 proof
   306   assume "x \<sqsubseteq> y"
   307   then have "is_sup x y y" ..
   308   then show "x \<squnion> y = y" ..
   309 next
   310   have "x \<sqsubseteq> x \<squnion> y" ..
   311   also assume "x \<squnion> y = y"
   312   finally show "x \<sqsubseteq> y" .
   313 qed
   314 
   315 text \<open>
   316   \medskip The most fundamental result of the meta-theory of lattices
   317   is as follows (we do not prove it here).
   318 
   319   Given a structure with binary operations \<open>\<sqinter>\<close> and \<open>\<squnion>\<close>
   320   such that (A), (C), and (AB) hold (cf.\
   321   \S\ref{sec:lattice-algebra}).  This structure represents a lattice,
   322   if the relation @{term "x \<sqsubseteq> y"} is defined as @{term "x \<sqinter> y = x"}
   323   (alternatively as @{term "x \<squnion> y = y"}).  Furthermore, infimum and
   324   supremum with respect to this ordering coincide with the original
   325   \<open>\<sqinter>\<close> and \<open>\<squnion>\<close> operations.
   326 \<close>
   327 
   328 
   329 subsection \<open>Example instances\<close>
   330 
   331 subsubsection \<open>Linear orders\<close>
   332 
   333 text \<open>
   334   Linear orders with @{term minimum} and @{term maximum} operations
   335   are a (degenerate) example of lattice structures.
   336 \<close>
   337 
   338 definition
   339   minimum :: "'a::linear_order \<Rightarrow> 'a \<Rightarrow> 'a" where
   340   "minimum x y = (if x \<sqsubseteq> y then x else y)"
   341 definition
   342   maximum :: "'a::linear_order \<Rightarrow> 'a \<Rightarrow> 'a" where
   343   "maximum x y = (if x \<sqsubseteq> y then y else x)"
   344 
   345 lemma is_inf_minimum: "is_inf x y (minimum x y)"
   346 proof
   347   let ?min = "minimum x y"
   348   from leq_linear show "?min \<sqsubseteq> x" by (auto simp add: minimum_def)
   349   from leq_linear show "?min \<sqsubseteq> y" by (auto simp add: minimum_def)
   350   fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"
   351   with leq_linear show "z \<sqsubseteq> ?min" by (auto simp add: minimum_def)
   352 qed
   353 
   354 lemma is_sup_maximum: "is_sup x y (maximum x y)"      (* FIXME dualize!? *)
   355 proof
   356   let ?max = "maximum x y"
   357   from leq_linear show "x \<sqsubseteq> ?max" by (auto simp add: maximum_def)
   358   from leq_linear show "y \<sqsubseteq> ?max" by (auto simp add: maximum_def)
   359   fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
   360   with leq_linear show "?max \<sqsubseteq> z" by (auto simp add: maximum_def)
   361 qed
   362 
   363 instance linear_order \<subseteq> lattice
   364 proof
   365   fix x y :: "'a::linear_order"
   366   from is_inf_minimum show "\<exists>inf. is_inf x y inf" ..
   367   from is_sup_maximum show "\<exists>sup. is_sup x y sup" ..
   368 qed
   369 
   370 text \<open>
   371   The lattice operations on linear orders indeed coincide with @{term
   372   minimum} and @{term maximum}.
   373 \<close>
   374 
   375 theorem meet_mimimum: "x \<sqinter> y = minimum x y"
   376   by (rule meet_equality) (rule is_inf_minimum)
   377 
   378 theorem meet_maximum: "x \<squnion> y = maximum x y"
   379   by (rule join_equality) (rule is_sup_maximum)
   380 
   381 
   382 
   383 subsubsection \<open>Binary products\<close>
   384 
   385 text \<open>
   386   The class of lattices is closed under direct binary products (cf.\
   387   \S\ref{sec:prod-order}).
   388 \<close>
   389 
   390 lemma is_inf_prod: "is_inf p q (fst p \<sqinter> fst q, snd p \<sqinter> snd q)"
   391 proof
   392   show "(fst p \<sqinter> fst q, snd p \<sqinter> snd q) \<sqsubseteq> p"
   393   proof -
   394     have "fst p \<sqinter> fst q \<sqsubseteq> fst p" ..
   395     moreover have "snd p \<sqinter> snd q \<sqsubseteq> snd p" ..
   396     ultimately show ?thesis by (simp add: leq_prod_def)
   397   qed
   398   show "(fst p \<sqinter> fst q, snd p \<sqinter> snd q) \<sqsubseteq> q"
   399   proof -
   400     have "fst p \<sqinter> fst q \<sqsubseteq> fst q" ..
   401     moreover have "snd p \<sqinter> snd q \<sqsubseteq> snd q" ..
   402     ultimately show ?thesis by (simp add: leq_prod_def)
   403   qed
   404   fix r assume rp: "r \<sqsubseteq> p" and rq: "r \<sqsubseteq> q"
   405   show "r \<sqsubseteq> (fst p \<sqinter> fst q, snd p \<sqinter> snd q)"
   406   proof -
   407     have "fst r \<sqsubseteq> fst p \<sqinter> fst q"
   408     proof
   409       from rp show "fst r \<sqsubseteq> fst p" by (simp add: leq_prod_def)
   410       from rq show "fst r \<sqsubseteq> fst q" by (simp add: leq_prod_def)
   411     qed
   412     moreover have "snd r \<sqsubseteq> snd p \<sqinter> snd q"
   413     proof
   414       from rp show "snd r \<sqsubseteq> snd p" by (simp add: leq_prod_def)
   415       from rq show "snd r \<sqsubseteq> snd q" by (simp add: leq_prod_def)
   416     qed
   417     ultimately show ?thesis by (simp add: leq_prod_def)
   418   qed
   419 qed
   420 
   421 lemma is_sup_prod: "is_sup p q (fst p \<squnion> fst q, snd p \<squnion> snd q)"  (* FIXME dualize!? *)
   422 proof
   423   show "p \<sqsubseteq> (fst p \<squnion> fst q, snd p \<squnion> snd q)"
   424   proof -
   425     have "fst p \<sqsubseteq> fst p \<squnion> fst q" ..
   426     moreover have "snd p \<sqsubseteq> snd p \<squnion> snd q" ..
   427     ultimately show ?thesis by (simp add: leq_prod_def)
   428   qed
   429   show "q \<sqsubseteq> (fst p \<squnion> fst q, snd p \<squnion> snd q)"
   430   proof -
   431     have "fst q \<sqsubseteq> fst p \<squnion> fst q" ..
   432     moreover have "snd q \<sqsubseteq> snd p \<squnion> snd q" ..
   433     ultimately show ?thesis by (simp add: leq_prod_def)
   434   qed
   435   fix r assume "pr": "p \<sqsubseteq> r" and qr: "q \<sqsubseteq> r"
   436   show "(fst p \<squnion> fst q, snd p \<squnion> snd q) \<sqsubseteq> r"
   437   proof -
   438     have "fst p \<squnion> fst q \<sqsubseteq> fst r"
   439     proof
   440       from "pr" show "fst p \<sqsubseteq> fst r" by (simp add: leq_prod_def)
   441       from qr show "fst q \<sqsubseteq> fst r" by (simp add: leq_prod_def)
   442     qed
   443     moreover have "snd p \<squnion> snd q \<sqsubseteq> snd r"
   444     proof
   445       from "pr" show "snd p \<sqsubseteq> snd r" by (simp add: leq_prod_def)
   446       from qr show "snd q \<sqsubseteq> snd r" by (simp add: leq_prod_def)
   447     qed
   448     ultimately show ?thesis by (simp add: leq_prod_def)
   449   qed
   450 qed
   451 
   452 instance prod :: (lattice, lattice) lattice
   453 proof
   454   fix p q :: "'a::lattice \<times> 'b::lattice"
   455   from is_inf_prod show "\<exists>inf. is_inf p q inf" ..
   456   from is_sup_prod show "\<exists>sup. is_sup p q sup" ..
   457 qed
   458 
   459 text \<open>
   460   The lattice operations on a binary product structure indeed coincide
   461   with the products of the original ones.
   462 \<close>
   463 
   464 theorem meet_prod: "p \<sqinter> q = (fst p \<sqinter> fst q, snd p \<sqinter> snd q)"
   465   by (rule meet_equality) (rule is_inf_prod)
   466 
   467 theorem join_prod: "p \<squnion> q = (fst p \<squnion> fst q, snd p \<squnion> snd q)"
   468   by (rule join_equality) (rule is_sup_prod)
   469 
   470 
   471 subsubsection \<open>General products\<close>
   472 
   473 text \<open>
   474   The class of lattices is closed under general products (function
   475   spaces) as well (cf.\ \S\ref{sec:fun-order}).
   476 \<close>
   477 
   478 lemma is_inf_fun: "is_inf f g (\<lambda>x. f x \<sqinter> g x)"
   479 proof
   480   show "(\<lambda>x. f x \<sqinter> g x) \<sqsubseteq> f"
   481   proof
   482     fix x show "f x \<sqinter> g x \<sqsubseteq> f x" ..
   483   qed
   484   show "(\<lambda>x. f x \<sqinter> g x) \<sqsubseteq> g"
   485   proof
   486     fix x show "f x \<sqinter> g x \<sqsubseteq> g x" ..
   487   qed
   488   fix h assume hf: "h \<sqsubseteq> f" and hg: "h \<sqsubseteq> g"
   489   show "h \<sqsubseteq> (\<lambda>x. f x \<sqinter> g x)"
   490   proof
   491     fix x
   492     show "h x \<sqsubseteq> f x \<sqinter> g x"
   493     proof
   494       from hf show "h x \<sqsubseteq> f x" ..
   495       from hg show "h x \<sqsubseteq> g x" ..
   496     qed
   497   qed
   498 qed
   499 
   500 lemma is_sup_fun: "is_sup f g (\<lambda>x. f x \<squnion> g x)"   (* FIXME dualize!? *)
   501 proof
   502   show "f \<sqsubseteq> (\<lambda>x. f x \<squnion> g x)"
   503   proof
   504     fix x show "f x \<sqsubseteq> f x \<squnion> g x" ..
   505   qed
   506   show "g \<sqsubseteq> (\<lambda>x. f x \<squnion> g x)"
   507   proof
   508     fix x show "g x \<sqsubseteq> f x \<squnion> g x" ..
   509   qed
   510   fix h assume fh: "f \<sqsubseteq> h" and gh: "g \<sqsubseteq> h"
   511   show "(\<lambda>x. f x \<squnion> g x) \<sqsubseteq> h"
   512   proof
   513     fix x
   514     show "f x \<squnion> g x \<sqsubseteq> h x"
   515     proof
   516       from fh show "f x \<sqsubseteq> h x" ..
   517       from gh show "g x \<sqsubseteq> h x" ..
   518     qed
   519   qed
   520 qed
   521 
   522 instance "fun" :: (type, lattice) lattice
   523 proof
   524   fix f g :: "'a \<Rightarrow> 'b::lattice"
   525   show "\<exists>inf. is_inf f g inf" by rule (rule is_inf_fun) (* FIXME @{text "from \<dots> show \<dots> .."} does not work!? unification incompleteness!? *)
   526   show "\<exists>sup. is_sup f g sup" by rule (rule is_sup_fun)
   527 qed
   528 
   529 text \<open>
   530   The lattice operations on a general product structure (function
   531   space) indeed emerge by point-wise lifting of the original ones.
   532 \<close>
   533 
   534 theorem meet_fun: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
   535   by (rule meet_equality) (rule is_inf_fun)
   536 
   537 theorem join_fun: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
   538   by (rule join_equality) (rule is_sup_fun)
   539 
   540 
   541 subsection \<open>Monotonicity and semi-morphisms\<close>
   542 
   543 text \<open>
   544   The lattice operations are monotone in both argument positions.  In
   545   fact, monotonicity of the second position is trivial due to
   546   commutativity.
   547 \<close>
   548 
   549 theorem meet_mono: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> w \<Longrightarrow> x \<sqinter> y \<sqsubseteq> z \<sqinter> w"
   550 proof -
   551   {
   552     fix a b c :: "'a::lattice"
   553     assume "a \<sqsubseteq> c" have "a \<sqinter> b \<sqsubseteq> c \<sqinter> b"
   554     proof
   555       have "a \<sqinter> b \<sqsubseteq> a" ..
   556       also have "\<dots> \<sqsubseteq> c" by fact
   557       finally show "a \<sqinter> b \<sqsubseteq> c" .
   558       show "a \<sqinter> b \<sqsubseteq> b" ..
   559     qed
   560   } note this [elim?]
   561   assume "x \<sqsubseteq> z" then have "x \<sqinter> y \<sqsubseteq> z \<sqinter> y" ..
   562   also have "\<dots> = y \<sqinter> z" by (rule meet_commute)
   563   also assume "y \<sqsubseteq> w" then have "y \<sqinter> z \<sqsubseteq> w \<sqinter> z" ..
   564   also have "\<dots> = z \<sqinter> w" by (rule meet_commute)
   565   finally show ?thesis .
   566 qed
   567 
   568 theorem join_mono: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> w \<Longrightarrow> x \<squnion> y \<sqsubseteq> z \<squnion> w"
   569 proof -
   570   assume "x \<sqsubseteq> z" then have "dual z \<sqsubseteq> dual x" ..
   571   moreover assume "y \<sqsubseteq> w" then have "dual w \<sqsubseteq> dual y" ..
   572   ultimately have "dual z \<sqinter> dual w \<sqsubseteq> dual x \<sqinter> dual y"
   573     by (rule meet_mono)
   574   then have "dual (z \<squnion> w) \<sqsubseteq> dual (x \<squnion> y)"
   575     by (simp only: dual_join)
   576   then show ?thesis ..
   577 qed
   578 
   579 text \<open>
   580   \medskip A semi-morphisms is a function \<open>f\<close> that preserves the
   581   lattice operations in the following manner: @{term "f (x \<sqinter> y) \<sqsubseteq> f x
   582   \<sqinter> f y"} and @{term "f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)"}, respectively.  Any of
   583   these properties is equivalent with monotonicity.
   584 \<close>
   585 
   586 theorem meet_semimorph:
   587   "(\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y) \<equiv> (\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y)"
   588 proof
   589   assume morph: "\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"
   590   fix x y :: "'a::lattice"
   591   assume "x \<sqsubseteq> y"
   592   then have "x \<sqinter> y = x" ..
   593   then have "x = x \<sqinter> y" ..
   594   also have "f \<dots> \<sqsubseteq> f x \<sqinter> f y" by (rule morph)
   595   also have "\<dots> \<sqsubseteq> f y" ..
   596   finally show "f x \<sqsubseteq> f y" .
   597 next
   598   assume mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
   599   show "\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"
   600   proof -
   601     fix x y
   602     show "f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"
   603     proof
   604       have "x \<sqinter> y \<sqsubseteq> x" .. then show "f (x \<sqinter> y) \<sqsubseteq> f x" by (rule mono)
   605       have "x \<sqinter> y \<sqsubseteq> y" .. then show "f (x \<sqinter> y) \<sqsubseteq> f y" by (rule mono)
   606     qed
   607   qed
   608 qed
   609 
   610 lemma join_semimorph:
   611   "(\<And>x y. f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)) \<equiv> (\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y)"
   612 proof
   613   assume morph: "\<And>x y. f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)"
   614   fix x y :: "'a::lattice"
   615   assume "x \<sqsubseteq> y" then have "x \<squnion> y = y" ..
   616   have "f x \<sqsubseteq> f x \<squnion> f y" ..
   617   also have "\<dots> \<sqsubseteq> f (x \<squnion> y)" by (rule morph)
   618   also from \<open>x \<sqsubseteq> y\<close> have "x \<squnion> y = y" ..
   619   finally show "f x \<sqsubseteq> f y" .
   620 next
   621   assume mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
   622   show "\<And>x y. f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)"
   623   proof -
   624     fix x y
   625     show "f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)"
   626     proof
   627       have "x \<sqsubseteq> x \<squnion> y" .. then show "f x \<sqsubseteq> f (x \<squnion> y)" by (rule mono)
   628       have "y \<sqsubseteq> x \<squnion> y" .. then show "f y \<sqsubseteq> f (x \<squnion> y)" by (rule mono)
   629     qed
   630   qed
   631 qed
   632 
   633 end