src/HOL/Lattice/Bounds.thy

updated NEWS

+
−(*  Title:      HOL/Lattice/Bounds.thy
+
−    Author:     Markus Wenzel, TU Muenchen
+
−*)
+
−
+
−section \<open>Bounds\<close>
+
−
+
−theory Bounds imports Orders begin
+
−
+
−hide_const (open) inf sup
+
−
+
−subsection \<open>Infimum and supremum\<close>
+
−
+
−text \<open>
+
−  Given a partial order, we define infimum (greatest lower bound) and
+
−  supremum (least upper bound) wrt.\ \<open>\<sqsubseteq>\<close> for two and for any
+
−  number of elements.
+
−\<close>
+
−
+
−definition
+
−  is_inf :: "'a::partial_order \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
+
−  "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))"
+
−
+
−definition
+
−  is_sup :: "'a::partial_order \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
+
−  "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))"
+
−
+
−definition
+
−  is_Inf :: "'a::partial_order set \<Rightarrow> 'a \<Rightarrow> bool" where
+
−  "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))"
+
−
+
−definition
+
−  is_Sup :: "'a::partial_order set \<Rightarrow> 'a \<Rightarrow> bool" where
+
−  "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))"
+
−
+
−text \<open>
+
−  These definitions entail the following basic properties of boundary
+
−  elements.
+
−\<close>
+
−
+
−lemma is_infI [intro?]: "inf \<sqsubseteq> x \<Longrightarrow> inf \<sqsubseteq> y \<Longrightarrow>
+
−    (\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> inf) \<Longrightarrow> is_inf x y inf"
+
−  by (unfold is_inf_def) blast
+
−
+
−lemma is_inf_greatest [elim?]:
+
−    "is_inf x y inf \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> inf"
+
−  by (unfold is_inf_def) blast
+
−
+
−lemma is_inf_lower [elim?]:
+
−    "is_inf x y inf \<Longrightarrow> (inf \<sqsubseteq> x \<Longrightarrow> inf \<sqsubseteq> y \<Longrightarrow> C) \<Longrightarrow> C"
+
−  by (unfold is_inf_def) blast
+
−
+
−
+
−lemma is_supI [intro?]: "x \<sqsubseteq> sup \<Longrightarrow> y \<sqsubseteq> sup \<Longrightarrow>
+
−    (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> sup \<sqsubseteq> z) \<Longrightarrow> is_sup x y sup"
+
−  by (unfold is_sup_def) blast
+
−
+
−lemma is_sup_least [elim?]:
+
−    "is_sup x y sup \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> sup \<sqsubseteq> z"
+
−  by (unfold is_sup_def) blast
+
−
+
−lemma is_sup_upper [elim?]:
+
−    "is_sup x y sup \<Longrightarrow> (x \<sqsubseteq> sup \<Longrightarrow> y \<sqsubseteq> sup \<Longrightarrow> C) \<Longrightarrow> C"
+
−  by (unfold is_sup_def) blast
+
−
+
−
+
−lemma is_InfI [intro?]: "(\<And>x. x \<in> A \<Longrightarrow> inf \<sqsubseteq> x) \<Longrightarrow>
+
−    (\<And>z. (\<forall>x \<in> A. z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> inf) \<Longrightarrow> is_Inf A inf"
+
−  by (unfold is_Inf_def) blast
+
−
+
−lemma is_Inf_greatest [elim?]:
+
−    "is_Inf A inf \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> inf"
+
−  by (unfold is_Inf_def) blast
+
−
+
−lemma is_Inf_lower [dest?]:
+
−    "is_Inf A inf \<Longrightarrow> x \<in> A \<Longrightarrow> inf \<sqsubseteq> x"
+
−  by (unfold is_Inf_def) blast
+
−
+
−
+
−lemma is_SupI [intro?]: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> sup) \<Longrightarrow>
+
−    (\<And>z. (\<forall>x \<in> A. x \<sqsubseteq> z) \<Longrightarrow> sup \<sqsubseteq> z) \<Longrightarrow> is_Sup A sup"
+
−  by (unfold is_Sup_def) blast
+
−
+
−lemma is_Sup_least [elim?]:
+
−    "is_Sup A sup \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> sup \<sqsubseteq> z"
+
−  by (unfold is_Sup_def) blast
+
−
+
−lemma is_Sup_upper [dest?]:
+
−    "is_Sup A sup \<Longrightarrow> x \<in> A \<Longrightarrow> x \<sqsubseteq> sup"
+
−  by (unfold is_Sup_def) blast
+
−
+
−
+
−subsection \<open>Duality\<close>
+
−
+
−text \<open>
+
−  Infimum and supremum are dual to each other.
+
−\<close>
+
−
+
−theorem dual_inf [iff?]:
+
−    "is_inf (dual x) (dual y) (dual sup) = is_sup x y sup"
+
−  by (simp add: is_inf_def is_sup_def dual_all [symmetric] dual_leq)
+
−
+
−theorem dual_sup [iff?]:
+
−    "is_sup (dual x) (dual y) (dual inf) = is_inf x y inf"
+
−  by (simp add: is_inf_def is_sup_def dual_all [symmetric] dual_leq)
+
−
+
−theorem dual_Inf [iff?]:
+
−    "is_Inf (dual ` A) (dual sup) = is_Sup A sup"
+
−  by (simp add: is_Inf_def is_Sup_def dual_all [symmetric] dual_leq)
+
−
+
−theorem dual_Sup [iff?]:
+
−    "is_Sup (dual ` A) (dual inf) = is_Inf A inf"
+
−  by (simp add: is_Inf_def is_Sup_def dual_all [symmetric] dual_leq)
+
−
+
−
+
−subsection \<open>Uniqueness\<close>
+
−
+
−text \<open>
+
−  Infima and suprema on partial orders are unique; this is mainly due
+
−  to anti-symmetry of the underlying relation.
+
−\<close>
+
−
+
−theorem is_inf_uniq: "is_inf x y inf \<Longrightarrow> is_inf x y inf' \<Longrightarrow> inf = inf'"
+
−proof -
+
−  assume inf: "is_inf x y inf"
+
−  assume inf': "is_inf x y inf'"
+
−  show ?thesis
+
−  proof (rule leq_antisym)
+
−    from inf' show "inf \<sqsubseteq> inf'"
+
−    proof (rule is_inf_greatest)
+
−      from inf show "inf \<sqsubseteq> x" ..
+
−      from inf show "inf \<sqsubseteq> y" ..
+
−    qed
+
−    from inf show "inf' \<sqsubseteq> inf"
+
−    proof (rule is_inf_greatest)
+
−      from inf' show "inf' \<sqsubseteq> x" ..
+
−      from inf' show "inf' \<sqsubseteq> y" ..
+
−    qed
+
−  qed
+
−qed
+
−
+
−theorem is_sup_uniq: "is_sup x y sup \<Longrightarrow> is_sup x y sup' \<Longrightarrow> sup = sup'"
+
−proof -
+
−  assume sup: "is_sup x y sup" and sup': "is_sup x y sup'"
+
−  have "dual sup = dual sup'"
+
−  proof (rule is_inf_uniq)
+
−    from sup show "is_inf (dual x) (dual y) (dual sup)" ..
+
−    from sup' show "is_inf (dual x) (dual y) (dual sup')" ..
+
−  qed
+
−  then show "sup = sup'" ..
+
−qed
+
−
+
−theorem is_Inf_uniq: "is_Inf A inf \<Longrightarrow> is_Inf A inf' \<Longrightarrow> inf = inf'"
+
−proof -
+
−  assume inf: "is_Inf A inf"
+
−  assume inf': "is_Inf A inf'"
+
−  show ?thesis
+
−  proof (rule leq_antisym)
+
−    from inf' show "inf \<sqsubseteq> inf'"
+
−    proof (rule is_Inf_greatest)
+
−      fix x assume "x \<in> A"
+
−      with inf show "inf \<sqsubseteq> x" ..
+
−    qed
+
−    from inf show "inf' \<sqsubseteq> inf"
+
−    proof (rule is_Inf_greatest)
+
−      fix x assume "x \<in> A"
+
−      with inf' show "inf' \<sqsubseteq> x" ..
+
−    qed
+
−  qed
+
−qed
+
−
+
−theorem is_Sup_uniq: "is_Sup A sup \<Longrightarrow> is_Sup A sup' \<Longrightarrow> sup = sup'"
+
−proof -
+
−  assume sup: "is_Sup A sup" and sup': "is_Sup A sup'"
+
−  have "dual sup = dual sup'"
+
−  proof (rule is_Inf_uniq)
+
−    from sup show "is_Inf (dual ` A) (dual sup)" ..
+
−    from sup' show "is_Inf (dual ` A) (dual sup')" ..
+
−  qed
+
−  then show "sup = sup'" ..
+
−qed
+
−
+
−
+
−subsection \<open>Related elements\<close>
+
−
+
−text \<open>
+
−  The binary bound of related elements is either one of the argument.
+
−\<close>
+
−
+
−theorem is_inf_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_inf x y x"
+
−proof -
+
−  assume "x \<sqsubseteq> y"
+
−  show ?thesis
+
−  proof
+
−    show "x \<sqsubseteq> x" ..
+
−    show "x \<sqsubseteq> y" by fact
+
−    fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" by fact
+
−  qed
+
−qed
+
−
+
−theorem is_sup_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_sup x y y"
+
−proof -
+
−  assume "x \<sqsubseteq> y"
+
−  show ?thesis
+
−  proof
+
−    show "x \<sqsubseteq> y" by fact
+
−    show "y \<sqsubseteq> y" ..
+
−    fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
+
−    show "y \<sqsubseteq> z" by fact
+
−  qed
+
−qed
+
−
+
−
+
−subsection \<open>General versus binary bounds \label{sec:gen-bin-bounds}\<close>
+
−
+
−text \<open>
+
−  General bounds of two-element sets coincide with binary bounds.
+
−\<close>
+
−
+
−theorem is_Inf_binary: "is_Inf {x, y} inf = is_inf x y inf"
+
−proof -
+
−  let ?A = "{x, y}"
+
−  show ?thesis
+
−  proof
+
−    assume is_Inf: "is_Inf ?A inf"
+
−    show "is_inf x y inf"
+
−    proof
+
−      have "x \<in> ?A" by simp
+
−      with is_Inf show "inf \<sqsubseteq> x" ..
+
−      have "y \<in> ?A" by simp
+
−      with is_Inf show "inf \<sqsubseteq> y" ..
+
−      fix z assume zx: "z \<sqsubseteq> x" and zy: "z \<sqsubseteq> y"
+
−      from is_Inf show "z \<sqsubseteq> inf"
+
−      proof (rule is_Inf_greatest)
+
−        fix a assume "a \<in> ?A"
+
−        then have "a = x \<or> a = y" by blast
+
−        then show "z \<sqsubseteq> a"
+
−        proof
+
−          assume "a = x"
+
−          with zx show ?thesis by simp
+
−        next
+
−          assume "a = y"
+
−          with zy show ?thesis by simp
+
−        qed
+
−      qed
+
−    qed
+
−  next
+
−    assume is_inf: "is_inf x y inf"
+
−    show "is_Inf {x, y} inf"
+
−    proof
+
−      fix a assume "a \<in> ?A"
+
−      then have "a = x \<or> a = y" by blast
+
−      then show "inf \<sqsubseteq> a"
+
−      proof
+
−        assume "a = x"
+
−        also from is_inf have "inf \<sqsubseteq> x" ..
+
−        finally show ?thesis .
+
−      next
+
−        assume "a = y"
+
−        also from is_inf have "inf \<sqsubseteq> y" ..
+
−        finally show ?thesis .
+
−      qed
+
−    next
+
−      fix z assume z: "\<forall>a \<in> ?A. z \<sqsubseteq> a"
+
−      from is_inf show "z \<sqsubseteq> inf"
+
−      proof (rule is_inf_greatest)
+
−        from z show "z \<sqsubseteq> x" by blast
+
−        from z show "z \<sqsubseteq> y" by blast
+
−      qed
+
−    qed
+
−  qed
+
−qed
+
−
+
−theorem is_Sup_binary: "is_Sup {x, y} sup = is_sup x y sup"
+
−proof -
+
−  have "is_Sup {x, y} sup = is_Inf (dual ` {x, y}) (dual sup)"
+
−    by (simp only: dual_Inf)
+
−  also have "dual ` {x, y} = {dual x, dual y}"
+
−    by simp
+
−  also have "is_Inf \<dots> (dual sup) = is_inf (dual x) (dual y) (dual sup)"
+
−    by (rule is_Inf_binary)
+
−  also have "\<dots> = is_sup x y sup"
+
−    by (simp only: dual_inf)
+
−  finally show ?thesis .
+
−qed
+
−
+
−
+
−subsection \<open>Connecting general bounds \label{sec:connect-bounds}\<close>
+
−
+
−text \<open>
+
−  Either kind of general bounds is sufficient to express the other.
+
−  The least upper bound (supremum) is the same as the the greatest
+
−  lower bound of the set of all upper bounds; the dual statements
+
−  holds as well; the dual statement holds as well.
+
−\<close>
+
−
+
−theorem Inf_Sup: "is_Inf {b. \<forall>a \<in> A. a \<sqsubseteq> b} sup \<Longrightarrow> is_Sup A sup"
+
−proof -
+
−  let ?B = "{b. \<forall>a \<in> A. a \<sqsubseteq> b}"
+
−  assume is_Inf: "is_Inf ?B sup"
+
−  show "is_Sup A sup"
+
−  proof
+
−    fix x assume x: "x \<in> A"
+
−    from is_Inf show "x \<sqsubseteq> sup"
+
−    proof (rule is_Inf_greatest)
+
−      fix y assume "y \<in> ?B"
+
−      then have "\<forall>a \<in> A. a \<sqsubseteq> y" ..
+
−      from this x show "x \<sqsubseteq> y" ..
+
−    qed
+
−  next
+
−    fix z assume "\<forall>x \<in> A. x \<sqsubseteq> z"
+
−    then have "z \<in> ?B" ..
+
−    with is_Inf show "sup \<sqsubseteq> z" ..
+
−  qed
+
−qed
+
−
+
−theorem Sup_Inf: "is_Sup {b. \<forall>a \<in> A. b \<sqsubseteq> a} inf \<Longrightarrow> is_Inf A inf"
+
−proof -
+
−  assume "is_Sup {b. \<forall>a \<in> A. b \<sqsubseteq> a} inf"
+
−  then have "is_Inf (dual ` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b}) (dual inf)"
+
−    by (simp only: dual_Inf dual_leq)
+
−  also have "dual ` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b} = {b'. \<forall>a' \<in> dual ` A. a' \<sqsubseteq> b'}"
+
−    by (auto iff: dual_ball dual_Collect simp add: image_Collect)  (* FIXME !? *)
+
−  finally have "is_Inf \<dots> (dual inf)" .
+
−  then have "is_Sup (dual ` A) (dual inf)"
+
−    by (rule Inf_Sup)
+
−  then show ?thesis ..
+
−qed
+
−
+
−end