some lemmas about strict order in lattices
authorhaftmann
Mon Sep 14 08:36:57 2009 +0200 (2009-09-14)
changeset 3256889518a3074e1
parent 32561 fdbfa0e35e78
child 32569 c4c12ef9d4d1
some lemmas about strict order in lattices
src/HOL/Lattices.thy
     1.1 --- a/src/HOL/Lattices.thy	Fri Sep 11 09:05:26 2009 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Mon Sep 14 08:36:57 2009 +0200
     1.3 @@ -12,7 +12,9 @@
     1.4  
     1.5  notation
     1.6    less_eq  (infix "\<sqsubseteq>" 50) and
     1.7 -  less  (infix "\<sqsubset>" 50)
     1.8 +  less  (infix "\<sqsubset>" 50) and
     1.9 +  top ("\<top>") and
    1.10 +  bot ("\<bottom>")
    1.11  
    1.12  class lower_semilattice = order +
    1.13    fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
    1.14 @@ -220,6 +222,46 @@
    1.15  
    1.16  end
    1.17  
    1.18 +subsubsection {* Strict order *}
    1.19 +
    1.20 +context lower_semilattice
    1.21 +begin
    1.22 +
    1.23 +lemma less_infI1:
    1.24 +  "a \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
    1.25 +  by (auto simp add: less_le intro: le_infI1)
    1.26 +
    1.27 +lemma less_infI2:
    1.28 +  "b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
    1.29 +  by (auto simp add: less_le intro: le_infI2)
    1.30 +
    1.31 +end
    1.32 +
    1.33 +context upper_semilattice
    1.34 +begin
    1.35 +
    1.36 +lemma less_supI1:
    1.37 +  "x < a \<Longrightarrow> x < a \<squnion> b"
    1.38 +proof -
    1.39 +  interpret dual: lower_semilattice "op \<ge>" "op >" sup
    1.40 +    by (fact dual_semilattice)
    1.41 +  assume "x < a"
    1.42 +  then show "x < a \<squnion> b"
    1.43 +    by (fact dual.less_infI1)
    1.44 +qed
    1.45 +
    1.46 +lemma less_supI2:
    1.47 +  "x < b \<Longrightarrow> x < a \<squnion> b"
    1.48 +proof -
    1.49 +  interpret dual: lower_semilattice "op \<ge>" "op >" sup
    1.50 +    by (fact dual_semilattice)
    1.51 +  assume "x < b"
    1.52 +  then show "x < a \<squnion> b"
    1.53 +    by (fact dual.less_infI2)
    1.54 +qed
    1.55 +
    1.56 +end
    1.57 +
    1.58  
    1.59  subsection {* Distributive lattices *}
    1.60  
    1.61 @@ -306,6 +348,40 @@
    1.62    "x \<squnion> bot = x"
    1.63    by (rule sup_absorb1) simp
    1.64  
    1.65 +lemma inf_eq_top_eq1:
    1.66 +  assumes "A \<sqinter> B = \<top>"
    1.67 +  shows "A = \<top>"
    1.68 +proof (cases "B = \<top>")
    1.69 +  case True with assms show ?thesis by simp
    1.70 +next
    1.71 +  case False with top_greatest have "B < \<top>" by (auto intro: neq_le_trans)
    1.72 +  then have "A \<sqinter> B < \<top>" by (rule less_infI2)
    1.73 +  with assms show ?thesis by simp
    1.74 +qed
    1.75 +
    1.76 +lemma inf_eq_top_eq2:
    1.77 +  assumes "A \<sqinter> B = \<top>"
    1.78 +  shows "B = \<top>"
    1.79 +  by (rule inf_eq_top_eq1, unfold inf_commute [of B]) (fact assms)
    1.80 +
    1.81 +lemma sup_eq_bot_eq1:
    1.82 +  assumes "A \<squnion> B = \<bottom>"
    1.83 +  shows "A = \<bottom>"
    1.84 +proof -
    1.85 +  interpret dual: boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" top bot
    1.86 +    by (rule dual_boolean_algebra)
    1.87 +  from dual.inf_eq_top_eq1 assms show ?thesis .
    1.88 +qed
    1.89 +
    1.90 +lemma sup_eq_bot_eq2:
    1.91 +  assumes "A \<squnion> B = \<bottom>"
    1.92 +  shows "B = \<bottom>"
    1.93 +proof -
    1.94 +  interpret dual: boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" top bot
    1.95 +    by (rule dual_boolean_algebra)
    1.96 +  from dual.inf_eq_top_eq2 assms show ?thesis .
    1.97 +qed
    1.98 +
    1.99  lemma compl_unique:
   1.100    assumes "x \<sqinter> y = bot"
   1.101      and "x \<squnion> y = top"
   1.102 @@ -517,6 +593,8 @@
   1.103    less_eq  (infix "\<sqsubseteq>" 50) and
   1.104    less (infix "\<sqsubset>" 50) and
   1.105    inf  (infixl "\<sqinter>" 70) and
   1.106 -  sup  (infixl "\<squnion>" 65)
   1.107 +  sup  (infixl "\<squnion>" 65) and
   1.108 +  top ("\<top>") and
   1.109 +  bot ("\<bottom>")
   1.110  
   1.111  end