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