# HG changeset patch
# User nipkow
# Date 1362922563 -3600
# Node ID dbc4a77488b2c2cbf4f16c4172301f211014b8dc
# Parent  f193d44d49185a507680b68e011595493ea3c2c8
stepwise instantiation is more modular

diff -r f193d44d4918 -r dbc4a77488b2 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Sun Mar 10 10:10:01 2013 +0100
+++ b/src/HOL/Lattices.thy	Sun Mar 10 14:36:03 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)