--- a/src/HOL/Algebra/Lattice.thy Tue Jul 29 16:17:45 2008 +0200
+++ b/src/HOL/Algebra/Lattice.thy Tue Jul 29 16:19:19 2008 +0200
@@ -5,17 +5,11 @@
Copyright: Clemens Ballarin
*)
-theory Lattice imports Main begin
+theory Lattice imports Congruence begin
section {* Orders and Lattices *}
-text {* Object with a carrier set. *}
-
-record 'a partial_object =
- carrier :: "'a set"
-
-
subsection {* Partial Orders *}
record 'a order = "'a partial_object" +
@@ -71,7 +65,7 @@
"Upper L A \<subseteq> carrier L"
by (unfold Upper_def) clarify
-lemma UpperD [dest]:
+lemma Upper_memD [dest]:
fixes L (structure)
shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
by (unfold Upper_def) blast
@@ -92,7 +86,7 @@
"Lower L A \<subseteq> carrier L"
by (unfold Lower_def) clarify
-lemma LowerD [dest]:
+lemma Lower_memD [dest]:
fixes L (structure)
shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x"
by (unfold Lower_def) blast
@@ -109,7 +103,7 @@
subsubsection {* least *}
-lemma least_carrier [intro, simp]:
+lemma least_closed [intro, simp]:
shows "least L l A ==> l \<in> carrier L"
by (unfold least_def) fast
@@ -142,7 +136,7 @@
subsubsection {* greatest *}
-lemma greatest_carrier [intro, simp]:
+lemma greatest_closed [intro, simp]:
shows "greatest L l A ==> l \<in> carrier L"
by (unfold greatest_def) fast
@@ -186,7 +180,7 @@
shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
by (unfold least_def) blast
-lemma greatest_Lower_above:
+lemma greatest_Lower_below:
fixes L (structure)
shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
by (unfold greatest_def) blast
@@ -207,7 +201,7 @@
lemma (in lattice) join_closed [simp]:
"[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L"
- by (rule joinI) (rule least_carrier)
+ by (rule joinI) (rule least_closed)
lemma (in partial_order) sup_of_singletonI: (* only reflexivity needed ? *)
"x \<in> carrier L ==> least L x (Upper L {x})"
@@ -402,7 +396,7 @@
from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)"
by (erule_tac least_le)
(blast intro!: Upper_memI intro: trans join_left join_right join_closed)
- qed (simp_all add: L least_carrier [OF sup])
+ qed (simp_all add: L least_closed [OF sup])
qed (simp_all add: L)
lemma join_comm:
@@ -438,7 +432,7 @@
lemma (in lattice) meet_closed [simp]:
"[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L"
- by (rule meetI) (rule greatest_carrier)
+ by (rule meetI) (rule greatest_closed)
lemma (in partial_order) inf_of_singletonI: (* only reflexivity needed ? *)
"x \<in> carrier L ==> greatest L x (Lower L {x})"
@@ -470,11 +464,11 @@
then show "i \<sqsubseteq> z"
proof
assume "z = x" then show ?thesis
- by (simp add: greatest_Lower_above [OF greatest_i] L La)
+ by (simp add: greatest_Lower_below [OF greatest_i] L La)
next
assume "z \<in> A"
with L greatest_i greatest_a show ?thesis
- by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above)
+ by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_below)
qed
next
fix y
@@ -514,11 +508,11 @@
then show "i \<sqsubseteq> z"
proof
assume "z = x" then show ?thesis
- by (simp add: greatest_Lower_above [OF greatest_i] L La)
+ by (simp add: greatest_Lower_below [OF greatest_i] L La)
next
assume "z \<in> A"
with L greatest_i greatest_a show ?thesis
- by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above)
+ by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_below)
qed
next
fix y
@@ -629,12 +623,12 @@
show "x \<sqinter> (y \<sqinter> z) = i"
proof (rule anti_sym)
from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
- by (fastsimp intro!: meet_le elim: greatest_Lower_above)
+ by (fastsimp intro!: meet_le elim: greatest_Lower_below)
next
from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i"
by (erule_tac greatest_le)
(blast intro!: Lower_memI intro: trans meet_left meet_right meet_closed)
- qed (simp_all add: L greatest_carrier [OF inf])
+ qed (simp_all add: L greatest_closed [OF inf])
qed (simp_all add: L)
lemma meet_comm:
@@ -809,14 +803,14 @@
apply (rule greatest_le [where A = "Lower L ?B"])
apply (rule b_inf_B)
apply (rule Lower_memI)
- apply (erule UpperD)
+ apply (erule Upper_memD)
apply assumption
apply (rule L)
apply (fast intro: L [THEN subsetD])
- apply (erule greatest_Lower_above [OF b_inf_B])
+ apply (erule greatest_Lower_below [OF b_inf_B])
apply simp
apply (rule L)
-apply (rule greatest_carrier [OF b_inf_B]) (* rename rule: _closed *)
+apply (rule greatest_closed [OF b_inf_B])
done
then show "EX s. least L s (Upper L A)" ..
next