src/HOLCF/Cfun.thy
changeset 27413 3154f3765cc7
parent 27274 1c97c471db82
child 29049 4e5b9e508e1e
     1.1 --- a/src/HOLCF/Cfun.thy	Tue Jul 01 01:28:44 2008 +0200
     1.2 +++ b/src/HOLCF/Cfun.thy	Tue Jul 01 02:19:53 2008 +0200
     1.3 @@ -192,16 +192,16 @@
     1.4  
     1.5  text {* contlub, cont properties of @{term Rep_CFun} in each argument *}
     1.6  
     1.7 -lemma contlub_cfun_arg: "chain Y \<Longrightarrow> f\<cdot>(lub (range Y)) = (\<Squnion>i. f\<cdot>(Y i))"
     1.8 +lemma contlub_cfun_arg: "chain Y \<Longrightarrow> f\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. f\<cdot>(Y i))"
     1.9  by (rule contlub_Rep_CFun2 [THEN contlubE])
    1.10  
    1.11 -lemma cont_cfun_arg: "chain Y \<Longrightarrow> range (\<lambda>i. f\<cdot>(Y i)) <<| f\<cdot>(lub (range Y))"
    1.12 +lemma cont_cfun_arg: "chain Y \<Longrightarrow> range (\<lambda>i. f\<cdot>(Y i)) <<| f\<cdot>(\<Squnion>i. Y i)"
    1.13  by (rule cont_Rep_CFun2 [THEN contE])
    1.14  
    1.15 -lemma contlub_cfun_fun: "chain F \<Longrightarrow> lub (range F)\<cdot>x = (\<Squnion>i. F i\<cdot>x)"
    1.16 +lemma contlub_cfun_fun: "chain F \<Longrightarrow> (\<Squnion>i. F i)\<cdot>x = (\<Squnion>i. F i\<cdot>x)"
    1.17  by (rule contlub_Rep_CFun1 [THEN contlubE])
    1.18  
    1.19 -lemma cont_cfun_fun: "chain F \<Longrightarrow> range (\<lambda>i. F i\<cdot>x) <<| lub (range F)\<cdot>x"
    1.20 +lemma cont_cfun_fun: "chain F \<Longrightarrow> range (\<lambda>i. F i\<cdot>x) <<| (\<Squnion>i. F i)\<cdot>x"
    1.21  by (rule cont_Rep_CFun1 [THEN contE])
    1.22  
    1.23  text {* monotonicity of application *}
    1.24 @@ -295,7 +295,7 @@
    1.25  lemma lub_cfun: "chain F \<Longrightarrow> range F <<| (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
    1.26  by (simp only: contlub_cfun_fun [symmetric] eta_cfun thelubE)
    1.27  
    1.28 -lemma thelub_cfun: "chain F \<Longrightarrow> lub (range F) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
    1.29 +lemma thelub_cfun: "chain F \<Longrightarrow> (\<Squnion>i. F i) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
    1.30  by (rule lub_cfun [THEN thelubI])
    1.31  
    1.32  subsection {* Continuity simplification procedure *}
    1.33 @@ -351,7 +351,7 @@
    1.34  text {* some lemmata for functions with flat/chfin domain/range types *}
    1.35  
    1.36  lemma chfin_Rep_CFunR: "chain (Y::nat => 'a::cpo->'b::chfin)  
    1.37 -      ==> !s. ? n. lub(range(Y))$s = Y n$s"
    1.38 +      ==> !s. ? n. (LUB i. Y i)$s = Y n$s"
    1.39  apply (rule allI)
    1.40  apply (subst contlub_cfun_fun)
    1.41  apply assumption
    1.42 @@ -510,7 +510,7 @@
    1.43  (*FIXME: long proof*)
    1.44  lemma contlub_strictify2: "contlub (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
    1.45  apply (rule contlubI)
    1.46 -apply (case_tac "lub (range Y) = \<bottom>")
    1.47 +apply (case_tac "(\<Squnion>i. Y i) = \<bottom>")
    1.48  apply (drule (1) chain_UU_I)
    1.49  apply simp
    1.50  apply (simp del: if_image_distrib)