--- a/src/HOL/Lattices.thy Sun Mar 10 11:21:16 2013 +0100
+++ b/src/HOL/Lattices.thy Sun Mar 10 14:36:18 2013 +0100
@@ -649,17 +649,10 @@
subsection {* Lattice on @{typ "_ \<Rightarrow> _"} *}
-instantiation "fun" :: (type, lattice) lattice
+instantiation "fun" :: (type, semilattice_sup) semilattice_sup
begin
definition
- "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
-
-lemma inf_apply [simp, code]:
- "(f \<sqinter> g) x = f x \<sqinter> g x"
- by (simp add: inf_fun_def)
-
-definition
"f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
lemma sup_apply [simp, code]:
@@ -671,6 +664,23 @@
end
+instantiation "fun" :: (type, semilattice_inf) semilattice_inf
+begin
+
+definition
+ "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
+
+lemma inf_apply [simp, code]:
+ "(f \<sqinter> g) x = f x \<sqinter> g x"
+ by (simp add: inf_fun_def)
+
+instance proof
+qed (simp_all add: le_fun_def)
+
+end
+
+instance "fun" :: (type, lattice) lattice ..
+
instance "fun" :: (type, distrib_lattice) distrib_lattice proof
qed (rule ext, simp add: sup_inf_distrib1)