author haftmann Sun, 26 May 2013 19:45:54 +0200 changeset 52152 b561cdce6c4c parent 52151 de43876e77bf child 52153 f5773a46cf05
examples for interpretation into target
 src/HOL/Lattices.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Lattices.thy	Sun May 26 14:02:03 2013 +0200
+++ b/src/HOL/Lattices.thy	Sun May 26 19:45:54 2013 +0200
@@ -49,9 +49,7 @@
obtains "a = a * b"
using assms by (unfold order_iff)

-end
-
-sublocale semilattice_order < ordering less_eq less
+sublocale ordering less_eq less
proof
fix a b
show "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
@@ -79,9 +77,6 @@
then show "a \<preceq> c" by (rule orderI)
qed

-context semilattice_order
-begin
-
lemma cobounded1 [simp]:
"a * b \<preceq> a"
@@ -132,10 +127,13 @@
end

locale semilattice_neutr_order = semilattice_neutr + semilattice_order
+begin

-sublocale semilattice_neutr_order < ordering_top less_eq less 1
+sublocale ordering_top less_eq less 1

+end
+
notation times (infixl "*" 70)
notation Groups.one ("1")

@@ -255,7 +253,10 @@

subsubsection {* Equational laws *}

-sublocale semilattice_inf < inf!: semilattice inf
+context semilattice_inf
+begin
+
+sublocale inf!: semilattice inf
proof
fix a b c
show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)"
@@ -266,26 +267,9 @@
by (rule antisym) auto
qed

-sublocale semilattice_sup < sup!: semilattice sup
-proof
-  fix a b c
-  show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
-    by (rule antisym) (auto intro: le_supI1 le_supI2)
-  show "a \<squnion> b = b \<squnion> a"
-    by (rule antisym) auto
-  show "a \<squnion> a = a"
-    by (rule antisym) auto
-qed
-
-sublocale semilattice_inf < inf!: semilattice_order inf less_eq less
+sublocale inf!: semilattice_order inf less_eq less
by default (auto simp add: le_iff_inf less_le)

-sublocale semilattice_sup < sup!: semilattice_order sup greater_eq greater
-  by default (auto simp add: le_iff_sup sup.commute less_le)
-
-context semilattice_inf
-begin
-
lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
by (fact inf.assoc)

@@ -317,6 +301,20 @@
context semilattice_sup
begin

+sublocale sup!: semilattice sup
+proof
+  fix a b c
+  show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
+    by (rule antisym) (auto intro: le_supI1 le_supI2)
+  show "a \<squnion> b = b \<squnion> a"
+    by (rule antisym) auto
+  show "a \<squnion> a = a"
+    by (rule antisym) auto
+qed
+
+sublocale sup!: semilattice_order sup greater_eq greater
+  by default (auto simp add: le_iff_sup sup.commute less_le)
+
lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
by (fact sup.assoc)

@@ -469,8 +467,9 @@
subsection {* Bounded lattices and boolean algebras *}

class bounded_semilattice_inf_top = semilattice_inf + top
+begin

-sublocale bounded_semilattice_inf_top < inf_top!: semilattice_neutr inf top
+sublocale inf_top!: semilattice_neutr inf top
+ inf_top!: semilattice_neutr_order inf top less_eq less
proof
fix x
@@ -478,9 +477,12 @@
by (rule inf_absorb1) simp
qed

-class bounded_semilattice_sup_bot = semilattice_sup + bot
+end

-sublocale bounded_semilattice_sup_bot < sup_bot!: semilattice_neutr sup bot
+class bounded_semilattice_sup_bot = semilattice_sup + bot
+begin
+
+sublocale sup_bot!: semilattice_neutr sup bot
+ sup_bot!: semilattice_neutr_order sup bot greater_eq greater
proof
fix x
@@ -488,6 +490,8 @@
by (rule sup_absorb1) simp
qed

+end
+
class bounded_lattice_bot = lattice + bot
begin
```