add/change some lemmas about lattices
authorhuffman
Sun Mar 28 12:49:14 2010 -0700 (2010-03-28)
changeset 3600823dfa8678c7c
parent 36007 095b1022e2ae
child 36009 9cdbc5ffc15c
add/change some lemmas about lattices
src/HOL/Lattices.thy
src/HOL/Predicate.thy
     1.1 --- a/src/HOL/Lattices.thy	Sun Mar 28 10:34:02 2010 -0700
     1.2 +++ b/src/HOL/Lattices.thy	Sun Mar 28 12:49:14 2010 -0700
     1.3 @@ -90,10 +90,10 @@
     1.4    by (rule order_trans) auto
     1.5  
     1.6  lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
     1.7 -  by (blast intro: inf_greatest)
     1.8 +  by (rule inf_greatest) (* FIXME: duplicate lemma *)
     1.9  
    1.10  lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
    1.11 -  by (blast intro: order_trans le_infI1 le_infI2)
    1.12 +  by (blast intro: order_trans inf_le1 inf_le2)
    1.13  
    1.14  lemma le_inf_iff [simp]:
    1.15    "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
    1.16 @@ -103,6 +103,9 @@
    1.17    "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
    1.18    by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1])
    1.19  
    1.20 +lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d"
    1.21 +  by (fast intro: inf_greatest le_infI1 le_infI2)
    1.22 +
    1.23  lemma mono_inf:
    1.24    fixes f :: "'a \<Rightarrow> 'b\<Colon>semilattice_inf"
    1.25    shows "mono f \<Longrightarrow> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B"
    1.26 @@ -123,11 +126,11 @@
    1.27  
    1.28  lemma le_supI:
    1.29    "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
    1.30 -  by (blast intro: sup_least)
    1.31 +  by (rule sup_least) (* FIXME: duplicate lemma *)
    1.32  
    1.33  lemma le_supE:
    1.34    "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
    1.35 -  by (blast intro: le_supI1 le_supI2 order_trans)
    1.36 +  by (blast intro: order_trans sup_ge1 sup_ge2)
    1.37  
    1.38  lemma le_sup_iff [simp]:
    1.39    "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
    1.40 @@ -137,6 +140,9 @@
    1.41    "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
    1.42    by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1])
    1.43  
    1.44 +lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d"
    1.45 +  by (fast intro: sup_least le_supI1 le_supI2)
    1.46 +
    1.47  lemma mono_sup:
    1.48    fixes f :: "'a \<Rightarrow> 'b\<Colon>semilattice_sup"
    1.49    shows "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)"
    1.50 @@ -345,6 +351,12 @@
    1.51    by (rule distrib_lattice.intro, rule dual_lattice)
    1.52      (unfold_locales, fact inf_sup_distrib1)
    1.53  
    1.54 +lemmas sup_inf_distrib =
    1.55 +  sup_inf_distrib1 sup_inf_distrib2
    1.56 +
    1.57 +lemmas inf_sup_distrib =
    1.58 +  inf_sup_distrib1 inf_sup_distrib2
    1.59 +
    1.60  lemmas distrib =
    1.61    sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
    1.62  
    1.63 @@ -393,39 +405,13 @@
    1.64    "x \<squnion> \<bottom> = x"
    1.65    by (rule sup_absorb1) simp
    1.66  
    1.67 -lemma inf_eq_top_eq1:
    1.68 -  assumes "A \<sqinter> B = \<top>"
    1.69 -  shows "A = \<top>"
    1.70 -proof (cases "B = \<top>")
    1.71 -  case True with assms show ?thesis by simp
    1.72 -next
    1.73 -  case False with top_greatest have "B \<sqsubset> \<top>" by (auto intro: neq_le_trans)
    1.74 -  then have "A \<sqinter> B \<sqsubset> \<top>" by (rule less_infI2)
    1.75 -  with assms show ?thesis by simp
    1.76 -qed
    1.77 -
    1.78 -lemma inf_eq_top_eq2:
    1.79 -  assumes "A \<sqinter> B = \<top>"
    1.80 -  shows "B = \<top>"
    1.81 -  by (rule inf_eq_top_eq1, unfold inf_commute [of B]) (fact assms)
    1.82 +lemma inf_eq_top_iff [simp]:
    1.83 +  "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
    1.84 +  by (simp add: eq_iff)
    1.85  
    1.86 -lemma sup_eq_bot_eq1:
    1.87 -  assumes "A \<squnion> B = \<bottom>"
    1.88 -  shows "A = \<bottom>"
    1.89 -proof -
    1.90 -  interpret dual: bounded_lattice "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom>
    1.91 -    by (rule dual_bounded_lattice)
    1.92 -  from dual.inf_eq_top_eq1 assms show ?thesis .
    1.93 -qed
    1.94 -
    1.95 -lemma sup_eq_bot_eq2:
    1.96 -  assumes "A \<squnion> B = \<bottom>"
    1.97 -  shows "B = \<bottom>"
    1.98 -proof -
    1.99 -  interpret dual: bounded_lattice "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom>
   1.100 -    by (rule dual_bounded_lattice)
   1.101 -  from dual.inf_eq_top_eq2 assms show ?thesis .
   1.102 -qed
   1.103 +lemma sup_eq_bot_iff [simp]:
   1.104 +  "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
   1.105 +  by (simp add: eq_iff)
   1.106  
   1.107  end
   1.108  
   1.109 @@ -472,10 +458,7 @@
   1.110    "- x = - y \<longleftrightarrow> x = y"
   1.111  proof
   1.112    assume "- x = - y"
   1.113 -  then have "- x \<sqinter> y = \<bottom>"
   1.114 -    and "- x \<squnion> y = \<top>"
   1.115 -    by (simp_all add: compl_inf_bot compl_sup_top)
   1.116 -  then have "- (- x) = y" by (rule compl_unique)
   1.117 +  then have "- (- x) = - (- y)" by (rule arg_cong)
   1.118    then show "x = y" by simp
   1.119  next
   1.120    assume "x = y"
   1.121 @@ -499,18 +482,14 @@
   1.122  lemma compl_inf [simp]:
   1.123    "- (x \<sqinter> y) = - x \<squnion> - y"
   1.124  proof (rule compl_unique)
   1.125 -  have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = ((x \<sqinter> y) \<sqinter> - x) \<squnion> ((x \<sqinter> y) \<sqinter> - y)"
   1.126 -    by (rule inf_sup_distrib1)
   1.127 -  also have "... = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))"
   1.128 -    by (simp only: inf_commute inf_assoc inf_left_commute)
   1.129 -  finally show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = \<bottom>"
   1.130 +  have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))"
   1.131 +    by (simp only: inf_sup_distrib inf_aci)
   1.132 +  then show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = \<bottom>"
   1.133      by (simp add: inf_compl_bot)
   1.134  next
   1.135 -  have "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = (x \<squnion> (- x \<squnion> - y)) \<sqinter> (y \<squnion> (- x \<squnion> - y))"
   1.136 -    by (rule sup_inf_distrib2)
   1.137 -  also have "... = (- y \<squnion> (x \<squnion> - x)) \<sqinter> (- x \<squnion> (y \<squnion> - y))"
   1.138 -    by (simp only: sup_commute sup_assoc sup_left_commute)
   1.139 -  finally show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = \<top>"
   1.140 +  have "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = (- y \<squnion> (x \<squnion> - x)) \<sqinter> (- x \<squnion> (y \<squnion> - y))"
   1.141 +    by (simp only: sup_inf_distrib sup_aci)
   1.142 +  then show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = \<top>"
   1.143      by (simp add: sup_compl_top)
   1.144  qed
   1.145  
   1.146 @@ -522,6 +501,21 @@
   1.147    then show ?thesis by simp
   1.148  qed
   1.149  
   1.150 +lemma compl_mono:
   1.151 +  "x \<sqsubseteq> y \<Longrightarrow> - y \<sqsubseteq> - x"
   1.152 +proof -
   1.153 +  assume "x \<sqsubseteq> y"
   1.154 +  then have "x \<squnion> y = y" by (simp only: le_iff_sup)
   1.155 +  then have "- (x \<squnion> y) = - y" by simp
   1.156 +  then have "- x \<sqinter> - y = - y" by simp
   1.157 +  then have "- y \<sqinter> - x = - y" by (simp only: inf_commute)
   1.158 +  then show "- y \<sqsubseteq> - x" by (simp only: le_iff_inf)
   1.159 +qed
   1.160 +
   1.161 +lemma compl_le_compl_iff: (* TODO: declare [simp] ? *)
   1.162 +  "- x \<le> - y \<longleftrightarrow> y \<le> x"
   1.163 +by (auto dest: compl_mono)
   1.164 +
   1.165  end
   1.166  
   1.167  
   1.168 @@ -550,7 +544,7 @@
   1.169    have leI: "\<And>x y z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<nabla> y \<sqsubseteq> z" by (blast intro: least)
   1.170    show "x \<nabla> y \<sqsubseteq> x \<squnion> y" by (rule leI) simp_all
   1.171  qed
   1.172 -  
   1.173 +
   1.174  
   1.175  subsection {* @{const min}/@{const max} on linear orders as
   1.176    special case of @{const inf}/@{const sup} *}
     2.1 --- a/src/HOL/Predicate.thy	Sun Mar 28 10:34:02 2010 -0700
     2.2 +++ b/src/HOL/Predicate.thy	Sun Mar 28 12:49:14 2010 -0700
     2.3 @@ -516,7 +516,7 @@
     2.4  
     2.5  lemma is_empty_sup:
     2.6    "is_empty (A \<squnion> B) \<longleftrightarrow> is_empty A \<and> is_empty B"
     2.7 -  by (auto simp add: is_empty_def intro: sup_eq_bot_eq1 sup_eq_bot_eq2)
     2.8 +  by (auto simp add: is_empty_def)
     2.9  
    2.10  definition singleton :: "(unit => 'a) \<Rightarrow> 'a pred \<Rightarrow> 'a" where
    2.11    "singleton dfault A = (if \<exists>!x. eval A x then THE x. eval A x else dfault ())"