make up_eq and up_less into simp rules
authorhuffman
Wed Jun 08 23:43:19 2005 +0200 (2005-06-08)
changeset 1632650a613925c4e
parent 16325 a6431098a929
child 16327 cd2cd49e6c8f
make up_eq and up_less into simp rules
src/HOLCF/Up.thy
     1.1 --- a/src/HOLCF/Up.thy	Wed Jun 08 16:11:09 2005 +0200
     1.2 +++ b/src/HOLCF/Up.thy	Wed Jun 08 23:43:19 2005 +0200
     1.3 @@ -285,7 +285,7 @@
     1.4  lemma up_inject: "up\<cdot>x = up\<cdot>y \<Longrightarrow> x = y"
     1.5  by (simp add: up_def cont_Iup)
     1.6  
     1.7 -lemma up_eq: "(up\<cdot>x = up\<cdot>y) = (x = y)"
     1.8 +lemma up_eq [simp]: "(up\<cdot>x = up\<cdot>y) = (x = y)"
     1.9  by (rule iffI, erule up_inject, simp)
    1.10  
    1.11  lemma up_defined [simp]: " up\<cdot>x \<noteq> \<bottom>"
    1.12 @@ -294,7 +294,7 @@
    1.13  lemma not_up_less_UU [simp]: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>"
    1.14  by (simp add: eq_UU_iff [symmetric])
    1.15  
    1.16 -lemma up_less: "(up\<cdot>x \<sqsubseteq> up\<cdot>y) = (x \<sqsubseteq> y)"
    1.17 +lemma up_less [simp]: "(up\<cdot>x \<sqsubseteq> up\<cdot>y) = (x \<sqsubseteq> y)"
    1.18  by (simp add: up_def cont_Iup)
    1.19  
    1.20  lemma upE1: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"