src/HOL/Lattices.thy
changeset 35028 108662d50512
parent 34973 ae634fad947e
child 35121 36c0a6dd8c6f
     1.1 --- a/src/HOL/Lattices.thy	Fri Feb 05 14:33:31 2010 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Fri Feb 05 14:33:50 2010 +0100
     1.3 @@ -16,13 +16,13 @@
     1.4    top ("\<top>") and
     1.5    bot ("\<bottom>")
     1.6  
     1.7 -class lower_semilattice = order +
     1.8 +class semilattice_inf = order +
     1.9    fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
    1.10    assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
    1.11    and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
    1.12    and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
    1.13  
    1.14 -class upper_semilattice = order +
    1.15 +class semilattice_sup = order +
    1.16    fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
    1.17    assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
    1.18    and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
    1.19 @@ -32,18 +32,18 @@
    1.20  text {* Dual lattice *}
    1.21  
    1.22  lemma dual_semilattice:
    1.23 -  "lower_semilattice (op \<ge>) (op >) sup"
    1.24 -by (rule lower_semilattice.intro, rule dual_order)
    1.25 +  "semilattice_inf (op \<ge>) (op >) sup"
    1.26 +by (rule semilattice_inf.intro, rule dual_order)
    1.27    (unfold_locales, simp_all add: sup_least)
    1.28  
    1.29  end
    1.30  
    1.31 -class lattice = lower_semilattice + upper_semilattice
    1.32 +class lattice = semilattice_inf + semilattice_sup
    1.33  
    1.34  
    1.35  subsubsection {* Intro and elim rules*}
    1.36  
    1.37 -context lower_semilattice
    1.38 +context semilattice_inf
    1.39  begin
    1.40  
    1.41  lemma le_infI1:
    1.42 @@ -69,13 +69,13 @@
    1.43    by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1])
    1.44  
    1.45  lemma mono_inf:
    1.46 -  fixes f :: "'a \<Rightarrow> 'b\<Colon>lower_semilattice"
    1.47 +  fixes f :: "'a \<Rightarrow> 'b\<Colon>semilattice_inf"
    1.48    shows "mono f \<Longrightarrow> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B"
    1.49    by (auto simp add: mono_def intro: Lattices.inf_greatest)
    1.50  
    1.51  end
    1.52  
    1.53 -context upper_semilattice
    1.54 +context semilattice_sup
    1.55  begin
    1.56  
    1.57  lemma le_supI1:
    1.58 @@ -103,7 +103,7 @@
    1.59    by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1])
    1.60  
    1.61  lemma mono_sup:
    1.62 -  fixes f :: "'a \<Rightarrow> 'b\<Colon>upper_semilattice"
    1.63 +  fixes f :: "'a \<Rightarrow> 'b\<Colon>semilattice_sup"
    1.64    shows "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)"
    1.65    by (auto simp add: mono_def intro: Lattices.sup_least)
    1.66  
    1.67 @@ -112,7 +112,7 @@
    1.68  
    1.69  subsubsection {* Equational laws *}
    1.70  
    1.71 -sublocale lower_semilattice < inf!: semilattice inf
    1.72 +sublocale semilattice_inf < inf!: semilattice inf
    1.73  proof
    1.74    fix a b c
    1.75    show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)"
    1.76 @@ -123,7 +123,7 @@
    1.77      by (rule antisym) auto
    1.78  qed
    1.79  
    1.80 -context lower_semilattice
    1.81 +context semilattice_inf
    1.82  begin
    1.83  
    1.84  lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
    1.85 @@ -151,7 +151,7 @@
    1.86  
    1.87  end
    1.88  
    1.89 -sublocale upper_semilattice < sup!: semilattice sup
    1.90 +sublocale semilattice_sup < sup!: semilattice sup
    1.91  proof
    1.92    fix a b c
    1.93    show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
    1.94 @@ -162,7 +162,7 @@
    1.95      by (rule antisym) auto
    1.96  qed
    1.97  
    1.98 -context upper_semilattice
    1.99 +context semilattice_sup
   1.100  begin
   1.101  
   1.102  lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
   1.103 @@ -195,7 +195,7 @@
   1.104  
   1.105  lemma dual_lattice:
   1.106    "lattice (op \<ge>) (op >) sup inf"
   1.107 -  by (rule lattice.intro, rule dual_semilattice, rule upper_semilattice.intro, rule dual_order)
   1.108 +  by (rule lattice.intro, rule dual_semilattice, rule semilattice_sup.intro, rule dual_order)
   1.109      (unfold_locales, auto)
   1.110  
   1.111  lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
   1.112 @@ -246,7 +246,7 @@
   1.113  
   1.114  subsubsection {* Strict order *}
   1.115  
   1.116 -context lower_semilattice
   1.117 +context semilattice_inf
   1.118  begin
   1.119  
   1.120  lemma less_infI1:
   1.121 @@ -259,13 +259,13 @@
   1.122  
   1.123  end
   1.124  
   1.125 -context upper_semilattice
   1.126 +context semilattice_sup
   1.127  begin
   1.128  
   1.129  lemma less_supI1:
   1.130    "x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b"
   1.131  proof -
   1.132 -  interpret dual: lower_semilattice "op \<ge>" "op >" sup
   1.133 +  interpret dual: semilattice_inf "op \<ge>" "op >" sup
   1.134      by (fact dual_semilattice)
   1.135    assume "x \<sqsubset> a"
   1.136    then show "x \<sqsubset> a \<squnion> b"
   1.137 @@ -275,7 +275,7 @@
   1.138  lemma less_supI2:
   1.139    "x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b"
   1.140  proof -
   1.141 -  interpret dual: lower_semilattice "op \<ge>" "op >" sup
   1.142 +  interpret dual: semilattice_inf "op \<ge>" "op >" sup
   1.143      by (fact dual_semilattice)
   1.144    assume "x \<sqsubset> b"
   1.145    then show "x \<sqsubset> a \<squnion> b"
   1.146 @@ -492,7 +492,7 @@
   1.147  
   1.148  subsection {* Uniqueness of inf and sup *}
   1.149  
   1.150 -lemma (in lower_semilattice) inf_unique:
   1.151 +lemma (in semilattice_inf) inf_unique:
   1.152    fixes f (infixl "\<triangle>" 70)
   1.153    assumes le1: "\<And>x y. x \<triangle> y \<sqsubseteq> x" and le2: "\<And>x y. x \<triangle> y \<sqsubseteq> y"
   1.154    and greatest: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z"
   1.155 @@ -504,7 +504,7 @@
   1.156    show "x \<sqinter> y \<sqsubseteq> x \<triangle> y" by (rule leI) simp_all
   1.157  qed
   1.158  
   1.159 -lemma (in upper_semilattice) sup_unique:
   1.160 +lemma (in semilattice_sup) sup_unique:
   1.161    fixes f (infixl "\<nabla>" 70)
   1.162    assumes ge1 [simp]: "\<And>x y. x \<sqsubseteq> x \<nabla> y" and ge2: "\<And>x y. y \<sqsubseteq> x \<nabla> y"
   1.163    and least: "\<And>x y z. y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<nabla> z \<sqsubseteq> x"
   1.164 @@ -527,10 +527,10 @@
   1.165      by (auto simp add: min_def max_def)
   1.166  qed (auto simp add: min_def max_def not_le less_imp_le)
   1.167  
   1.168 -lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
   1.169 +lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{semilattice_inf, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
   1.170    by (rule ext)+ (auto intro: antisym)
   1.171  
   1.172 -lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{upper_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
   1.173 +lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{semilattice_sup, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
   1.174    by (rule ext)+ (auto intro: antisym)
   1.175  
   1.176  lemmas le_maxI1 = min_max.sup_ge1