diff -r ed7d12bcf8f8 -r 108662d50512 src/HOL/Lattices.thy --- a/src/HOL/Lattices.thy Fri Feb 05 14:33:31 2010 +0100 +++ b/src/HOL/Lattices.thy Fri Feb 05 14:33:50 2010 +0100 @@ -16,13 +16,13 @@ top ("\") and bot ("\") -class lower_semilattice = order + +class semilattice_inf = order + fixes inf :: "'a \ 'a \ 'a" (infixl "\" 70) assumes inf_le1 [simp]: "x \ y \ x" and inf_le2 [simp]: "x \ y \ y" and inf_greatest: "x \ y \ x \ z \ x \ y \ z" -class upper_semilattice = order + +class semilattice_sup = order + fixes sup :: "'a \ 'a \ 'a" (infixl "\" 65) assumes sup_ge1 [simp]: "x \ x \ y" and sup_ge2 [simp]: "y \ x \ y" @@ -32,18 +32,18 @@ text {* Dual lattice *} lemma dual_semilattice: - "lower_semilattice (op \) (op >) sup" -by (rule lower_semilattice.intro, rule dual_order) + "semilattice_inf (op \) (op >) sup" +by (rule semilattice_inf.intro, rule dual_order) (unfold_locales, simp_all add: sup_least) end -class lattice = lower_semilattice + upper_semilattice +class lattice = semilattice_inf + semilattice_sup subsubsection {* Intro and elim rules*} -context lower_semilattice +context semilattice_inf begin lemma le_infI1: @@ -69,13 +69,13 @@ by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1]) lemma mono_inf: - fixes f :: "'a \ 'b\lower_semilattice" + fixes f :: "'a \ 'b\semilattice_inf" shows "mono f \ f (A \ B) \ f A \ f B" by (auto simp add: mono_def intro: Lattices.inf_greatest) end -context upper_semilattice +context semilattice_sup begin lemma le_supI1: @@ -103,7 +103,7 @@ by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1]) lemma mono_sup: - fixes f :: "'a \ 'b\upper_semilattice" + fixes f :: "'a \ 'b\semilattice_sup" shows "mono f \ f A \ f B \ f (A \ B)" by (auto simp add: mono_def intro: Lattices.sup_least) @@ -112,7 +112,7 @@ subsubsection {* Equational laws *} -sublocale lower_semilattice < inf!: semilattice inf +sublocale semilattice_inf < inf!: semilattice inf proof fix a b c show "(a \ b) \ c = a \ (b \ c)" @@ -123,7 +123,7 @@ by (rule antisym) auto qed -context lower_semilattice +context semilattice_inf begin lemma inf_assoc: "(x \ y) \ z = x \ (y \ z)" @@ -151,7 +151,7 @@ end -sublocale upper_semilattice < sup!: semilattice sup +sublocale semilattice_sup < sup!: semilattice sup proof fix a b c show "(a \ b) \ c = a \ (b \ c)" @@ -162,7 +162,7 @@ by (rule antisym) auto qed -context upper_semilattice +context semilattice_sup begin lemma sup_assoc: "(x \ y) \ z = x \ (y \ z)" @@ -195,7 +195,7 @@ lemma dual_lattice: "lattice (op \) (op >) sup inf" - by (rule lattice.intro, rule dual_semilattice, rule upper_semilattice.intro, rule dual_order) + by (rule lattice.intro, rule dual_semilattice, rule semilattice_sup.intro, rule dual_order) (unfold_locales, auto) lemma inf_sup_absorb: "x \ (x \ y) = x" @@ -246,7 +246,7 @@ subsubsection {* Strict order *} -context lower_semilattice +context semilattice_inf begin lemma less_infI1: @@ -259,13 +259,13 @@ end -context upper_semilattice +context semilattice_sup begin lemma less_supI1: "x \ a \ x \ a \ b" proof - - interpret dual: lower_semilattice "op \" "op >" sup + interpret dual: semilattice_inf "op \" "op >" sup by (fact dual_semilattice) assume "x \ a" then show "x \ a \ b" @@ -275,7 +275,7 @@ lemma less_supI2: "x \ b \ x \ a \ b" proof - - interpret dual: lower_semilattice "op \" "op >" sup + interpret dual: semilattice_inf "op \" "op >" sup by (fact dual_semilattice) assume "x \ b" then show "x \ a \ b" @@ -492,7 +492,7 @@ subsection {* Uniqueness of inf and sup *} -lemma (in lower_semilattice) inf_unique: +lemma (in semilattice_inf) inf_unique: fixes f (infixl "\" 70) assumes le1: "\x y. x \ y \ x" and le2: "\x y. x \ y \ y" and greatest: "\x y z. x \ y \ x \ z \ x \ y \ z" @@ -504,7 +504,7 @@ show "x \ y \ x \ y" by (rule leI) simp_all qed -lemma (in upper_semilattice) sup_unique: +lemma (in semilattice_sup) sup_unique: fixes f (infixl "\" 70) assumes ge1 [simp]: "\x y. x \ x \ y" and ge2: "\x y. y \ x \ y" and least: "\x y z. y \ x \ z \ x \ y \ z \ x" @@ -527,10 +527,10 @@ by (auto simp add: min_def max_def) qed (auto simp add: min_def max_def not_le less_imp_le) -lemma inf_min: "inf = (min \ 'a\{lower_semilattice, linorder} \ 'a \ 'a)" +lemma inf_min: "inf = (min \ 'a\{semilattice_inf, linorder} \ 'a \ 'a)" by (rule ext)+ (auto intro: antisym) -lemma sup_max: "sup = (max \ 'a\{upper_semilattice, linorder} \ 'a \ 'a)" +lemma sup_max: "sup = (max \ 'a\{semilattice_sup, linorder} \ 'a \ 'a)" by (rule ext)+ (auto intro: antisym) lemmas le_maxI1 = min_max.sup_ge1