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