src/HOL/Lattice/Bounds.thy
 author nipkow Thu Dec 11 08:52:50 2008 +0100 (2008-12-11) changeset 29106 25e28a4070f3 parent 27193 740159cfbf0e child 35317 d57da4abb47d permissions -rw-r--r--
Testfile for Stefan's code generator
     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