src/HOL/Lattice/Bounds.thy
 author wenzelm Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) changeset 63915 bab633745c7f parent 61986 2461779da2b8 permissions -rw-r--r--
tuned proofs;
 wenzelm@10157  1 (* Title: HOL/Lattice/Bounds.thy  wenzelm@10157  2  Author: Markus Wenzel, TU Muenchen  wenzelm@10157  3 *)  wenzelm@10157  4 wenzelm@61986  5 section \Bounds\  wenzelm@10157  6 haftmann@16417  7 theory Bounds imports Orders begin  wenzelm@10157  8 wenzelm@36176  9 hide_const (open) inf sup  haftmann@22426  10 wenzelm@61986  11 subsection \Infimum and supremum\  wenzelm@10157  12 wenzelm@61986  13 text \  wenzelm@10157  14  Given a partial order, we define infimum (greatest lower bound) and  wenzelm@61986  15  supremum (least upper bound) wrt.\ \\\ for two and for any  wenzelm@10157  16  number of elements.  wenzelm@61986  17 \  wenzelm@10157  18 wenzelm@19736  19 definition  wenzelm@21404  20  is_inf :: "'a::partial_order \ 'a \ 'a \ bool" where  wenzelm@19736  21  "is_inf x y inf = (inf \ x \ inf \ y \ (\z. z \ x \ z \ y \ z \ inf))"  wenzelm@10157  22 wenzelm@21404  23 definition  wenzelm@21404  24  is_sup :: "'a::partial_order \ 'a \ 'a \ bool" where  wenzelm@19736  25  "is_sup x y sup = (x \ sup \ y \ sup \ (\z. x \ z \ y \ z \ sup \ z))"  wenzelm@10157  26 wenzelm@21404  27 definition  wenzelm@21404  28  is_Inf :: "'a::partial_order set \ 'a \ bool" where  wenzelm@19736  29  "is_Inf A inf = ((\x \ A. inf \ x) \ (\z. (\x \ A. z \ x) \ z \ inf))"  wenzelm@10157  30 wenzelm@21404  31 definition  wenzelm@21404  32  is_Sup :: "'a::partial_order set \ 'a \ bool" where  wenzelm@19736  33  "is_Sup A sup = ((\x \ A. x \ sup) \ (\z. (\x \ A. x \ z) \ sup \ z))"  wenzelm@10157  34 wenzelm@61986  35 text \  wenzelm@10157  36  These definitions entail the following basic properties of boundary  wenzelm@10157  37  elements.  wenzelm@61986  38 \  wenzelm@10157  39 wenzelm@10157  40 lemma is_infI [intro?]: "inf \ x \ inf \ y \  wenzelm@10157  41  (\z. z \ x \ z \ y \ z \ inf) \ is_inf x y inf"  wenzelm@10157  42  by (unfold is_inf_def) blast  wenzelm@10157  43 wenzelm@10157  44 lemma is_inf_greatest [elim?]:  wenzelm@10157  45  "is_inf x y inf \ z \ x \ z \ y \ z \ inf"  wenzelm@10157  46  by (unfold is_inf_def) blast  wenzelm@10157  47 wenzelm@10157  48 lemma is_inf_lower [elim?]:  wenzelm@10157  49  "is_inf x y inf \ (inf \ x \ inf \ y \ C) \ C"  wenzelm@10157  50  by (unfold is_inf_def) blast  wenzelm@10157  51 wenzelm@10157  52 wenzelm@10157  53 lemma is_supI [intro?]: "x \ sup \ y \ sup \  wenzelm@10157  54  (\z. x \ z \ y \ z \ sup \ z) \ is_sup x y sup"  wenzelm@10157  55  by (unfold is_sup_def) blast  wenzelm@10157  56 wenzelm@10157  57 lemma is_sup_least [elim?]:  wenzelm@10157  58  "is_sup x y sup \ x \ z \ y \ z \ sup \ z"  wenzelm@10157  59  by (unfold is_sup_def) blast  wenzelm@10157  60 wenzelm@10157  61 lemma is_sup_upper [elim?]:  wenzelm@10157  62  "is_sup x y sup \ (x \ sup \ y \ sup \ C) \ C"  wenzelm@10157  63  by (unfold is_sup_def) blast  wenzelm@10157  64 wenzelm@10157  65 wenzelm@10157  66 lemma is_InfI [intro?]: "(\x. x \ A \ inf \ x) \  wenzelm@10157  67  (\z. (\x \ A. z \ x) \ z \ inf) \ is_Inf A inf"  wenzelm@10157  68  by (unfold is_Inf_def) blast  wenzelm@10157  69 wenzelm@10157  70 lemma is_Inf_greatest [elim?]:  wenzelm@10157  71  "is_Inf A inf \ (\x. x \ A \ z \ x) \ z \ inf"  wenzelm@10157  72  by (unfold is_Inf_def) blast  wenzelm@10157  73 wenzelm@10157  74 lemma is_Inf_lower [dest?]:  wenzelm@10157  75  "is_Inf A inf \ x \ A \ inf \ x"  wenzelm@10157  76  by (unfold is_Inf_def) blast  wenzelm@10157  77 wenzelm@10157  78 wenzelm@10157  79 lemma is_SupI [intro?]: "(\x. x \ A \ x \ sup) \  wenzelm@10157  80  (\z. (\x \ A. x \ z) \ sup \ z) \ is_Sup A sup"  wenzelm@10157  81  by (unfold is_Sup_def) blast  wenzelm@10157  82 wenzelm@10157  83 lemma is_Sup_least [elim?]:  wenzelm@10157  84  "is_Sup A sup \ (\x. x \ A \ x \ z) \ sup \ z"  wenzelm@10157  85  by (unfold is_Sup_def) blast  wenzelm@10157  86 wenzelm@10157  87 lemma is_Sup_upper [dest?]:  wenzelm@10157  88  "is_Sup A sup \ x \ A \ x \ sup"  wenzelm@10157  89  by (unfold is_Sup_def) blast  wenzelm@10157  90 wenzelm@10157  91 wenzelm@61986  92 subsection \Duality\  wenzelm@10157  93 wenzelm@61986  94 text \  wenzelm@10157  95  Infimum and supremum are dual to each other.  wenzelm@61986  96 \  wenzelm@10157  97 wenzelm@10157  98 theorem dual_inf [iff?]:  wenzelm@10157  99  "is_inf (dual x) (dual y) (dual sup) = is_sup x y sup"  wenzelm@10157  100  by (simp add: is_inf_def is_sup_def dual_all [symmetric] dual_leq)  wenzelm@10157  101 wenzelm@10157  102 theorem dual_sup [iff?]:  wenzelm@10157  103  "is_sup (dual x) (dual y) (dual inf) = is_inf x y inf"  wenzelm@10157  104  by (simp add: is_inf_def is_sup_def dual_all [symmetric] dual_leq)  wenzelm@10157  105 wenzelm@10157  106 theorem dual_Inf [iff?]:  nipkow@10834  107  "is_Inf (dual  A) (dual sup) = is_Sup A sup"  wenzelm@10157  108  by (simp add: is_Inf_def is_Sup_def dual_all [symmetric] dual_leq)  wenzelm@10157  109 wenzelm@10157  110 theorem dual_Sup [iff?]:  nipkow@10834  111  "is_Sup (dual  A) (dual inf) = is_Inf A inf"  wenzelm@10157  112  by (simp add: is_Inf_def is_Sup_def dual_all [symmetric] dual_leq)  wenzelm@10157  113 wenzelm@10157  114 wenzelm@61986  115 subsection \Uniqueness\  wenzelm@10157  116 wenzelm@61986  117 text \  wenzelm@10157  118  Infima and suprema on partial orders are unique; this is mainly due  wenzelm@10157  119  to anti-symmetry of the underlying relation.  wenzelm@61986  120 \  wenzelm@10157  121 wenzelm@10157  122 theorem is_inf_uniq: "is_inf x y inf \ is_inf x y inf' \ inf = inf'"  wenzelm@10157  123 proof -  wenzelm@10157  124  assume inf: "is_inf x y inf"  wenzelm@10157  125  assume inf': "is_inf x y inf'"  wenzelm@10157  126  show ?thesis  wenzelm@10157  127  proof (rule leq_antisym)  wenzelm@10157  128  from inf' show "inf \ inf'"  wenzelm@10157  129  proof (rule is_inf_greatest)  wenzelm@10157  130  from inf show "inf \ x" ..  wenzelm@10157  131  from inf show "inf \ y" ..  wenzelm@10157  132  qed  wenzelm@10157  133  from inf show "inf' \ inf"  wenzelm@10157  134  proof (rule is_inf_greatest)  wenzelm@10157  135  from inf' show "inf' \ x" ..  wenzelm@10157  136  from inf' show "inf' \ y" ..  wenzelm@10157  137  qed  wenzelm@10157  138  qed  wenzelm@10157  139 qed  wenzelm@10157  140 wenzelm@10157  141 theorem is_sup_uniq: "is_sup x y sup \ is_sup x y sup' \ sup = sup'"  wenzelm@10157  142 proof -  wenzelm@10157  143  assume sup: "is_sup x y sup" and sup': "is_sup x y sup'"  wenzelm@10157  144  have "dual sup = dual sup'"  wenzelm@10157  145  proof (rule is_inf_uniq)  wenzelm@10157  146  from sup show "is_inf (dual x) (dual y) (dual sup)" ..  wenzelm@10157  147  from sup' show "is_inf (dual x) (dual y) (dual sup')" ..  wenzelm@10157  148  qed  wenzelm@23373  149  then show "sup = sup'" ..  wenzelm@10157  150 qed  wenzelm@10157  151 wenzelm@10157  152 theorem is_Inf_uniq: "is_Inf A inf \ is_Inf A inf' \ inf = inf'"  wenzelm@10157  153 proof -  wenzelm@10157  154  assume inf: "is_Inf A inf"  wenzelm@10157  155  assume inf': "is_Inf A inf'"  wenzelm@10157  156  show ?thesis  wenzelm@10157  157  proof (rule leq_antisym)  wenzelm@10157  158  from inf' show "inf \ inf'"  wenzelm@10157  159  proof (rule is_Inf_greatest)  wenzelm@10157  160  fix x assume "x \ A"  wenzelm@23373  161  with inf show "inf \ x" ..  wenzelm@10157  162  qed  wenzelm@10157  163  from inf show "inf' \ inf"  wenzelm@10157  164  proof (rule is_Inf_greatest)  wenzelm@10157  165  fix x assume "x \ A"  wenzelm@23373  166  with inf' show "inf' \ x" ..  wenzelm@10157  167  qed  wenzelm@10157  168  qed  wenzelm@10157  169 qed  wenzelm@10157  170 wenzelm@10157  171 theorem is_Sup_uniq: "is_Sup A sup \ is_Sup A sup' \ sup = sup'"  wenzelm@10157  172 proof -  wenzelm@10157  173  assume sup: "is_Sup A sup" and sup': "is_Sup A sup'"  wenzelm@10157  174  have "dual sup = dual sup'"  wenzelm@10157  175  proof (rule is_Inf_uniq)  nipkow@10834  176  from sup show "is_Inf (dual  A) (dual sup)" ..  nipkow@10834  177  from sup' show "is_Inf (dual  A) (dual sup')" ..  wenzelm@10157  178  qed  wenzelm@23373  179  then show "sup = sup'" ..  wenzelm@10157  180 qed  wenzelm@10157  181 wenzelm@10157  182 wenzelm@61986  183 subsection \Related elements\  wenzelm@10157  184 wenzelm@61986  185 text \  wenzelm@10157  186  The binary bound of related elements is either one of the argument.  wenzelm@61986  187 \  wenzelm@10157  188 wenzelm@10157  189 theorem is_inf_related [elim?]: "x \ y \ is_inf x y x"  wenzelm@10157  190 proof -  wenzelm@10157  191  assume "x \ y"  wenzelm@10157  192  show ?thesis  wenzelm@10157  193  proof  wenzelm@10157  194  show "x \ x" ..  wenzelm@23393  195  show "x \ y" by fact  wenzelm@23393  196  fix z assume "z \ x" and "z \ y" show "z \ x" by fact  wenzelm@10157  197  qed  wenzelm@10157  198 qed  wenzelm@10157  199 wenzelm@10157  200 theorem is_sup_related [elim?]: "x \ y \ is_sup x y y"  wenzelm@10157  201 proof -  wenzelm@10157  202  assume "x \ y"  wenzelm@10157  203  show ?thesis  wenzelm@10157  204  proof  wenzelm@23393  205  show "x \ y" by fact  wenzelm@10157  206  show "y \ y" ..  wenzelm@10157  207  fix z assume "x \ z" and "y \ z"  wenzelm@23393  208  show "y \ z" by fact  wenzelm@10157  209  qed  wenzelm@10157  210 qed  wenzelm@10157  211 wenzelm@10157  212 wenzelm@61986  213 subsection \General versus binary bounds \label{sec:gen-bin-bounds}\  wenzelm@10157  214 wenzelm@61986  215 text \  wenzelm@10157  216  General bounds of two-element sets coincide with binary bounds.  wenzelm@61986  217 \  wenzelm@10157  218 wenzelm@10157  219 theorem is_Inf_binary: "is_Inf {x, y} inf = is_inf x y inf"  wenzelm@10157  220 proof -  wenzelm@10157  221  let ?A = "{x, y}"  wenzelm@10157  222  show ?thesis  wenzelm@10157  223  proof  wenzelm@10157  224  assume is_Inf: "is_Inf ?A inf"  wenzelm@10157  225  show "is_inf x y inf"  wenzelm@10157  226  proof  wenzelm@10157  227  have "x \ ?A" by simp  wenzelm@10157  228  with is_Inf show "inf \ x" ..  wenzelm@10157  229  have "y \ ?A" by simp  wenzelm@10157  230  with is_Inf show "inf \ y" ..  wenzelm@10157  231  fix z assume zx: "z \ x" and zy: "z \ y"  wenzelm@10157  232  from is_Inf show "z \ inf"  wenzelm@10157  233  proof (rule is_Inf_greatest)  wenzelm@10157  234  fix a assume "a \ ?A"  wenzelm@23373  235  then have "a = x \ a = y" by blast  wenzelm@23373  236  then show "z \ a"  wenzelm@10157  237  proof  wenzelm@10157  238  assume "a = x"  wenzelm@10157  239  with zx show ?thesis by simp  wenzelm@10157  240  next  wenzelm@10157  241  assume "a = y"  wenzelm@10157  242  with zy show ?thesis by simp  wenzelm@10157  243  qed  wenzelm@10157  244  qed  wenzelm@10157  245  qed  wenzelm@10157  246  next  wenzelm@10157  247  assume is_inf: "is_inf x y inf"  wenzelm@10157  248  show "is_Inf {x, y} inf"  wenzelm@10157  249  proof  wenzelm@10157  250  fix a assume "a \ ?A"  wenzelm@23373  251  then have "a = x \ a = y" by blast  wenzelm@23373  252  then show "inf \ a"  wenzelm@10157  253  proof  wenzelm@10157  254  assume "a = x"  wenzelm@10157  255  also from is_inf have "inf \ x" ..  wenzelm@10157  256  finally show ?thesis .  wenzelm@10157  257  next  wenzelm@10157  258  assume "a = y"  wenzelm@10157  259  also from is_inf have "inf \ y" ..  wenzelm@10157  260  finally show ?thesis .  wenzelm@10157  261  qed  wenzelm@10157  262  next  wenzelm@10157  263  fix z assume z: "\a \ ?A. z \ a"  wenzelm@10157  264  from is_inf show "z \ inf"  wenzelm@10157  265  proof (rule is_inf_greatest)  wenzelm@10157  266  from z show "z \ x" by blast  wenzelm@10157  267  from z show "z \ y" by blast  wenzelm@10157  268  qed  wenzelm@10157  269  qed  wenzelm@10157  270  qed  wenzelm@10157  271 qed  wenzelm@10157  272 wenzelm@10157  273 theorem is_Sup_binary: "is_Sup {x, y} sup = is_sup x y sup"  wenzelm@10157  274 proof -  nipkow@10834  275  have "is_Sup {x, y} sup = is_Inf (dual  {x, y}) (dual sup)"  wenzelm@10157  276  by (simp only: dual_Inf)  nipkow@10834  277  also have "dual  {x, y} = {dual x, dual y}"  wenzelm@10157  278  by simp  wenzelm@10157  279  also have "is_Inf \ (dual sup) = is_inf (dual x) (dual y) (dual sup)"  wenzelm@10157  280  by (rule is_Inf_binary)  wenzelm@10157  281  also have "\ = is_sup x y sup"  wenzelm@10157  282  by (simp only: dual_inf)  wenzelm@10157  283  finally show ?thesis .  wenzelm@10157  284 qed  wenzelm@10157  285 wenzelm@10157  286 wenzelm@61986  287 subsection \Connecting general bounds \label{sec:connect-bounds}\  wenzelm@10157  288 wenzelm@61986  289 text \  wenzelm@10157  290  Either kind of general bounds is sufficient to express the other.  wenzelm@10157  291  The least upper bound (supremum) is the same as the the greatest  wenzelm@10157  292  lower bound of the set of all upper bounds; the dual statements  wenzelm@10157  293  holds as well; the dual statement holds as well.  wenzelm@61986  294 \  wenzelm@10157  295 wenzelm@10157  296 theorem Inf_Sup: "is_Inf {b. \a \ A. a \ b} sup \ is_Sup A sup"  wenzelm@10157  297 proof -  wenzelm@10157  298  let ?B = "{b. \a \ A. a \ b}"  wenzelm@10157  299  assume is_Inf: "is_Inf ?B sup"  wenzelm@10157  300  show "is_Sup A sup"  wenzelm@10157  301  proof  wenzelm@10157  302  fix x assume x: "x \ A"  wenzelm@10157  303  from is_Inf show "x \ sup"  wenzelm@10157  304  proof (rule is_Inf_greatest)  wenzelm@10157  305  fix y assume "y \ ?B"  wenzelm@23373  306  then have "\a \ A. a \ y" ..  wenzelm@10157  307  from this x show "x \ y" ..  wenzelm@10157  308  qed  wenzelm@10157  309  next  wenzelm@10157  310  fix z assume "\x \ A. x \ z"  wenzelm@23373  311  then have "z \ ?B" ..  wenzelm@10157  312  with is_Inf show "sup \ z" ..  wenzelm@10157  313  qed  wenzelm@10157  314 qed  wenzelm@10157  315 wenzelm@10157  316 theorem Sup_Inf: "is_Sup {b. \a \ A. b \ a} inf \ is_Inf A inf"  wenzelm@10157  317 proof -  wenzelm@10157  318  assume "is_Sup {b. \a \ A. b \ a} inf"  wenzelm@23373  319  then have "is_Inf (dual  {b. \a \ A. dual a \ dual b}) (dual inf)"  wenzelm@10157  320  by (simp only: dual_Inf dual_leq)  nipkow@10834  321  also have "dual  {b. \a \ A. dual a \ dual b} = {b'. \a' \ dual  A. a' \ b'}"  paulson@11265  322  by (auto iff: dual_ball dual_Collect simp add: image_Collect) (* FIXME !? *)  wenzelm@10157  323  finally have "is_Inf \ (dual inf)" .  wenzelm@23373  324  then have "is_Sup (dual  A) (dual inf)"  wenzelm@10157  325  by (rule Inf_Sup)  wenzelm@23373  326  then show ?thesis ..  wenzelm@10157  327 qed  wenzelm@10157  328 wenzelm@10157  329 end