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;
     1 (*  Title:      HOL/Lattice/Bounds.thy

     2     Author:     Markus Wenzel, TU Muenchen

     3 *)

     4

     5 section \<open>Bounds\<close>

     6

     7 theory Bounds imports Orders begin

     8

     9 hide_const (open) inf sup

    10

    11 subsection \<open>Infimum and supremum\<close>

    12

    13 text \<open>

    14   Given a partial order, we define infimum (greatest lower bound) and

    15   supremum (least upper bound) wrt.\ \<open>\<sqsubseteq>\<close> for two and for any

    16   number of elements.

    17 \<close>

    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 \<open>

    36   These definitions entail the following basic properties of boundary

    37   elements.

    38 \<close>

    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 \<open>Duality\<close>

    93

    94 text \<open>

    95   Infimum and supremum are dual to each other.

    96 \<close>

    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 \<open>Uniqueness\<close>

   116

   117 text \<open>

   118   Infima and suprema on partial orders are unique; this is mainly due

   119   to anti-symmetry of the underlying relation.

   120 \<close>

   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 \<open>Related elements\<close>

   184

   185 text \<open>

   186   The binary bound of related elements is either one of the argument.

   187 \<close>

   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 \<open>General versus binary bounds \label{sec:gen-bin-bounds}\<close>

   214

   215 text \<open>

   216   General bounds of two-element sets coincide with binary bounds.

   217 \<close>

   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 \<open>Connecting general bounds \label{sec:connect-bounds}\<close>

   288

   289 text \<open>

   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 \<close>

   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