rename lub_fun -> is_lub_fun, thelub_fun -> lub_fun
authorhuffman
Mon Dec 06 10:08:33 2010 -0800 (2010-12-06)
changeset 41030ff7d177128ef
parent 41029 f7d8cfa6e7fc
child 41031 9883d1417ce1
rename lub_fun -> is_lub_fun, thelub_fun -> lub_fun
NEWS
src/HOL/HOLCF/Cfun.thy
src/HOL/HOLCF/Fun_Cpo.thy
     1.1 --- a/NEWS	Mon Dec 06 08:59:58 2010 -0800
     1.2 +++ b/NEWS	Mon Dec 06 10:08:33 2010 -0800
     1.3 @@ -524,6 +524,8 @@
     1.4    unique_lub      ~> is_lub_unique
     1.5    is_ub_lub       ~> is_lub_rangeD1
     1.6    lub_bin_chain   ~> is_lub_bin_chain
     1.7 +  lub_fun         ~> is_lub_fun
     1.8 +  thelub_fun      ~> lub_fun
     1.9    thelub_Pair     ~> lub_Pair
    1.10    lub_cprod       ~> is_lub_prod
    1.11    thelub_cprod    ~> lub_prod
     2.1 --- a/src/HOL/HOLCF/Cfun.thy	Mon Dec 06 08:59:58 2010 -0800
     2.2 +++ b/src/HOL/HOLCF/Cfun.thy	Mon Dec 06 10:08:33 2010 -0800
     2.3 @@ -260,7 +260,7 @@
     2.4      \<Longrightarrow> (\<Squnion>i. \<Lambda> x. F i x) = (\<Lambda> x. \<Squnion>i. F i x)"
     2.5  apply (simp add: lub_cfun)
     2.6  apply (simp add: Abs_cfun_inverse2)
     2.7 -apply (simp add: thelub_fun ch2ch_lambda)
     2.8 +apply (simp add: lub_fun ch2ch_lambda)
     2.9  done
    2.10  
    2.11  lemmas lub_distribs = lub_APP lub_LAM
     3.1 --- a/src/HOL/HOLCF/Fun_Cpo.thy	Mon Dec 06 08:59:58 2010 -0800
     3.2 +++ b/src/HOL/HOLCF/Fun_Cpo.thy	Mon Dec 06 10:08:33 2010 -0800
     3.3 @@ -57,19 +57,13 @@
     3.4  lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
     3.5  by (simp add: chain_def below_fun_def)
     3.6  
     3.7 -text {* upper bounds of function chains yield upper bound in the po range *}
     3.8 -
     3.9 -lemma ub2ub_fun:
    3.10 -  "range S <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
    3.11 -by (auto simp add: is_ub_def below_fun_def)
    3.12 -
    3.13  text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
    3.14  
    3.15  lemma is_lub_lambda:
    3.16    "(\<And>x. range (\<lambda>i. Y i x) <<| f x) \<Longrightarrow> range Y <<| f"
    3.17  unfolding is_lub_def is_ub_def below_fun_def by simp
    3.18  
    3.19 -lemma lub_fun:
    3.20 +lemma is_lub_fun:
    3.21    "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
    3.22      \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)"
    3.23  apply (rule is_lub_lambda)
    3.24 @@ -77,13 +71,13 @@
    3.25  apply (erule ch2ch_fun)
    3.26  done
    3.27  
    3.28 -lemma thelub_fun:
    3.29 +lemma lub_fun:
    3.30    "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
    3.31      \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
    3.32 -by (rule lub_fun [THEN lub_eqI])
    3.33 +by (rule is_lub_fun [THEN lub_eqI])
    3.34  
    3.35  instance "fun"  :: (type, cpo) cpo
    3.36 -by intro_classes (rule exI, erule lub_fun)
    3.37 +by intro_classes (rule exI, erule is_lub_fun)
    3.38  
    3.39  subsection {* Chain-finiteness of function space *}
    3.40  
    3.41 @@ -135,12 +129,12 @@
    3.42  text {* The lub of a chain of monotone functions is monotone. *}
    3.43  
    3.44  lemma adm_monofun: "adm monofun"
    3.45 -by (rule admI, simp add: thelub_fun fun_chain_iff monofun_def lub_mono)
    3.46 +by (rule admI, simp add: lub_fun fun_chain_iff monofun_def lub_mono)
    3.47  
    3.48  text {* The lub of a chain of continuous functions is continuous. *}
    3.49  
    3.50  lemma adm_cont: "adm cont"
    3.51 -by (rule admI, simp add: thelub_fun fun_chain_iff)
    3.52 +by (rule admI, simp add: lub_fun fun_chain_iff)
    3.53  
    3.54  text {* Function application preserves monotonicity and continuity. *}
    3.55  
    3.56 @@ -150,7 +144,7 @@
    3.57  lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
    3.58  apply (rule contI2)
    3.59  apply (erule cont2mono [THEN mono2mono_fun])
    3.60 -apply (simp add: cont2contlubE thelub_fun ch2ch_cont)
    3.61 +apply (simp add: cont2contlubE lub_fun ch2ch_cont)
    3.62  done
    3.63  
    3.64  lemma cont_fun: "cont (\<lambda>f. f x)"
    3.65 @@ -174,6 +168,6 @@
    3.66  lemma contlub_lambda:
    3.67    "(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo))
    3.68      \<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))"
    3.69 -by (simp add: thelub_fun ch2ch_lambda)
    3.70 +by (simp add: lub_fun ch2ch_lambda)
    3.71  
    3.72  end