dropped redundant theorems
authorhaftmann
Thu Mar 13 08:56:08 2014 +0100 (2014-03-13)
changeset 56076e52fc7c37ed3
parent 56075 c6d4425f1fdc
child 56077 d397030fb27e
dropped redundant theorems
NEWS
src/HOL/Complete_Lattices.thy
     1.1 --- a/NEWS	Thu Mar 13 08:56:08 2014 +0100
     1.2 +++ b/NEWS	Thu Mar 13 08:56:08 2014 +0100
     1.3 @@ -104,6 +104,8 @@
     1.4    can be restored like this:  declare/using [[simp_legacy_precond]]
     1.5    This configuration option will disappear again in the future.
     1.6  
     1.7 +* Dropped facts INF_comp, SUP_comp.  INCOMPATIBILITY.
     1.8 +
     1.9  * HOL-Word:
    1.10    * Abandoned fact collection "word_arith_alts", which is a
    1.11    duplicate of "word_arith_wis".
     2.1 --- a/src/HOL/Complete_Lattices.thy	Thu Mar 13 08:56:08 2014 +0100
     2.2 +++ b/src/HOL/Complete_Lattices.thy	Thu Mar 13 08:56:08 2014 +0100
     2.3 @@ -20,10 +20,6 @@
     2.4  definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
     2.5    INF_def: "INFI A f = \<Sqinter>(f ` A)"
     2.6  
     2.7 -lemma INF_comp: -- {* FIXME drop *}
     2.8 -  "INFI A (g \<circ> f) = INFI (f ` A) g"
     2.9 -  by (simp add: INF_def image_comp)
    2.10 -
    2.11  lemma INF_image [simp]: "INFI (f`A) g = INFI A (\<lambda>x. g (f x))"
    2.12    by (simp add: INF_def image_image)
    2.13  
    2.14 @@ -39,10 +35,6 @@
    2.15  definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    2.16    SUP_def: "SUPR A f = \<Squnion>(f ` A)"
    2.17  
    2.18 -lemma SUP_comp: -- {* FIXME drop *}
    2.19 -  "SUPR A (g \<circ> f) = SUPR (f ` A) g"
    2.20 -  by (simp add: SUP_def image_comp)
    2.21 -
    2.22  lemma SUP_image [simp]: "SUPR (f`A) g = SUPR A (%x. g (f x))"
    2.23    by (simp add: SUP_def image_image)
    2.24