src/HOLCF/Up.thy
changeset 25131 2c8caac48ade
parent 19105 3aabd46340e0
child 25785 dbe118fe3180
     1.1 --- a/src/HOLCF/Up.thy	Sun Oct 21 14:21:45 2007 +0200
     1.2 +++ b/src/HOLCF/Up.thy	Sun Oct 21 14:21:48 2007 +0200
     1.3 @@ -115,7 +115,7 @@
     1.4  by (rule ext, rule up_lemma3 [symmetric])
     1.5  
     1.6  lemma up_lemma6:
     1.7 -  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk>  
     1.8 +  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk>
     1.9        \<Longrightarrow> range Y <<| Iup (\<Squnion>i. THE a. Iup a = Y(i + j))"
    1.10  apply (rule_tac j1 = j in is_lub_range_shift [THEN iffD1])
    1.11  apply assumption
    1.12 @@ -197,16 +197,17 @@
    1.13  
    1.14  subsection {* Continuous versions of constants *}
    1.15  
    1.16 -constdefs  
    1.17 -  up  :: "'a \<rightarrow> 'a u"
    1.18 -  "up \<equiv> \<Lambda> x. Iup x"
    1.19 +definition
    1.20 +  up  :: "'a \<rightarrow> 'a u" where
    1.21 +  "up = (\<Lambda> x. Iup x)"
    1.22  
    1.23 -  fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b"
    1.24 -  "fup \<equiv> \<Lambda> f p. Ifup f p"
    1.25 +definition
    1.26 +  fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b" where
    1.27 +  "fup = (\<Lambda> f p. Ifup f p)"
    1.28  
    1.29  translations
    1.30 -  "case l of up\<cdot>x \<Rightarrow> t" == "fup\<cdot>(\<Lambda> x. t)\<cdot>l"
    1.31 -  "\<Lambda>(up\<cdot>x). t" == "fup\<cdot>(\<Lambda> x. t)"
    1.32 +  "case l of CONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
    1.33 +  "\<Lambda>(CONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
    1.34  
    1.35  text {* continuous versions of lemmas for @{typ "('a)u"} *}
    1.36