src/HOLCF/Ffun.thy
changeset 26028 74668c3a8f70
parent 26025 ca6876116bb4
child 26452 ed657432b8b9
     1.1 --- a/src/HOLCF/Ffun.thy	Thu Jan 31 21:48:14 2008 +0100
     1.2 +++ b/src/HOLCF/Ffun.thy	Thu Jan 31 22:00:31 2008 +0100
     1.3 @@ -65,23 +65,29 @@
     1.4  text {* upper bounds of function chains yield upper bound in the po range *}
     1.5  
     1.6  lemma ub2ub_fun:
     1.7 -  "range (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::po) <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
     1.8 +  "range S <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
     1.9  by (auto simp add: is_ub_def less_fun_def)
    1.10  
    1.11  text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
    1.12  
    1.13 +lemma is_lub_lambda:
    1.14 +  assumes f: "\<And>x. range (\<lambda>i. Y i x) <<| f x"
    1.15 +  shows "range Y <<| f"
    1.16 +apply (rule is_lubI)
    1.17 +apply (rule ub_rangeI)
    1.18 +apply (rule less_fun_ext)
    1.19 +apply (rule is_ub_lub [OF f])
    1.20 +apply (rule less_fun_ext)
    1.21 +apply (rule is_lub_lub [OF f])
    1.22 +apply (erule ub2ub_fun)
    1.23 +done
    1.24 +
    1.25  lemma lub_fun:
    1.26    "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
    1.27      \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)"
    1.28 -apply (rule is_lubI)
    1.29 -apply (rule ub_rangeI)
    1.30 -apply (rule less_fun_ext)
    1.31 -apply (rule is_ub_thelub)
    1.32 +apply (rule is_lub_lambda)
    1.33 +apply (rule cpo_lubI)
    1.34  apply (erule ch2ch_fun)
    1.35 -apply (rule less_fun_ext)
    1.36 -apply (rule is_lub_thelub)
    1.37 -apply (erule ch2ch_fun)
    1.38 -apply (erule ub2ub_fun)
    1.39  done
    1.40  
    1.41  lemma thelub_fun: