author ballarin Tue, 29 Jul 2008 16:19:19 +0200 changeset 27700 ef4b26efa8b6 parent 27699 489e3f33af0e child 27701 ed7a2e0fab59
Renamed theorems; New theory on divisibility.
```--- 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 @@
*)

-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])

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])

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```