stepwise instantiation is more modular
authornipkow
Sun Mar 10 14:36:03 2013 +0100 (2013-03-10)
changeset 51387dbc4a77488b2
parent 51385 f193d44d4918
child 51388 1f5497c8ce8c
stepwise instantiation is more modular
src/HOL/Lattices.thy
     1.1 --- a/src/HOL/Lattices.thy	Sun Mar 10 10:10:01 2013 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Sun Mar 10 14:36:03 2013 +0100
     1.3 @@ -649,17 +649,10 @@
     1.4  
     1.5  subsection {* Lattice on @{typ "_ \<Rightarrow> _"} *}
     1.6  
     1.7 -instantiation "fun" :: (type, lattice) lattice
     1.8 +instantiation "fun" :: (type, semilattice_sup) semilattice_sup
     1.9  begin
    1.10  
    1.11  definition
    1.12 -  "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
    1.13 -
    1.14 -lemma inf_apply [simp, code]:
    1.15 -  "(f \<sqinter> g) x = f x \<sqinter> g x"
    1.16 -  by (simp add: inf_fun_def)
    1.17 -
    1.18 -definition
    1.19    "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
    1.20  
    1.21  lemma sup_apply [simp, code]:
    1.22 @@ -671,6 +664,23 @@
    1.23  
    1.24  end
    1.25  
    1.26 +instantiation "fun" :: (type, semilattice_inf) semilattice_inf
    1.27 +begin
    1.28 +
    1.29 +definition
    1.30 +  "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
    1.31 +
    1.32 +lemma inf_apply [simp, code]:
    1.33 +  "(f \<sqinter> g) x = f x \<sqinter> g x"
    1.34 +  by (simp add: inf_fun_def)
    1.35 +
    1.36 +instance proof
    1.37 +qed (simp_all add: le_fun_def)
    1.38 +
    1.39 +end
    1.40 +
    1.41 +instance "fun" :: (type, lattice) lattice ..
    1.42 +
    1.43  instance "fun" :: (type, distrib_lattice) distrib_lattice proof
    1.44  qed (rule ext, simp add: sup_inf_distrib1)
    1.45