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