src/HOL/Lattices.thy
changeset 24514 540eaf87e42d
parent 24345 86a3557a9ebb
child 24640 85a6c200ecd3
     1.1 --- a/src/HOL/Lattices.thy	Sat Sep 01 16:12:50 2007 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Sat Sep 01 18:17:36 2007 +0200
     1.3 @@ -513,11 +513,15 @@
     1.4  
     1.5  lemmas [code func del] = inf_set_eq sup_set_eq
     1.6  
     1.7 -lemmas mono_Int = mono_inf
     1.8 -  [where ?'a="?'a set", where ?'b="?'b set", unfolded inf_set_eq sup_set_eq]
     1.9 +lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
    1.10 +  apply (fold inf_set_eq sup_set_eq)
    1.11 +  apply (erule mono_inf)
    1.12 +  done
    1.13  
    1.14 -lemmas mono_Un = mono_sup
    1.15 -  [where ?'a="?'a set", where ?'b="?'b set", unfolded inf_set_eq sup_set_eq]
    1.16 +lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
    1.17 +  apply (fold inf_set_eq sup_set_eq)
    1.18 +  apply (erule mono_sup)
    1.19 +  done
    1.20  
    1.21  instance set :: (type) complete_lattice
    1.22    Inf_set_def: "Inf S \<equiv> \<Inter>S"
    1.23 @@ -581,9 +585,4 @@
    1.24  lemmas inf_aci = inf_ACI
    1.25  lemmas sup_aci = sup_ACI
    1.26  
    1.27 -ML {*
    1.28 -val sup_fun_eq = @{thm sup_fun_eq}
    1.29 -val sup_bool_eq = @{thm sup_bool_eq}
    1.30 -*}
    1.31 -
    1.32  end