reformulate lemma cont2cont_lub and move to Cont.thy
authorhuffman
Tue Oct 12 05:48:15 2010 -0700 (2010-10-12)
changeset 400049f6ed6840e8d
parent 40003 427106657e04
child 40005 3e3611136a13
reformulate lemma cont2cont_lub and move to Cont.thy
src/HOLCF/Cont.thy
src/HOLCF/Fix.thy
src/HOLCF/Fun_Cpo.thy
     1.1 --- a/src/HOLCF/Cont.thy	Tue Oct 12 05:25:21 2010 -0700
     1.2 +++ b/src/HOLCF/Cont.thy	Tue Oct 12 05:48:15 2010 -0700
     1.3 @@ -22,12 +22,6 @@
     1.4    monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"  -- "monotonicity"  where
     1.5    "monofun f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
     1.6  
     1.7 -(*
     1.8 -definition
     1.9 -  contlub :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"  -- "first cont. def" where
    1.10 -  "contlub f = (\<forall>Y. chain Y \<longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i)))"
    1.11 -*)
    1.12 -
    1.13  definition
    1.14    cont :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"
    1.15  where
    1.16 @@ -176,6 +170,17 @@
    1.17    "\<lbrakk>cont c; cont (\<lambda>x. f x)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. c (f x))"
    1.18  by (rule cont_apply [OF _ _ cont_const])
    1.19  
    1.20 +text {* Least upper bounds preserve continuity *}
    1.21 +
    1.22 +lemma cont2cont_lub [simp]:
    1.23 +  assumes chain: "\<And>x. chain (\<lambda>i. F i x)" and cont: "\<And>i. cont (\<lambda>x. F i x)"
    1.24 +  shows "cont (\<lambda>x. \<Squnion>i. F i x)"
    1.25 +apply (rule contI2)
    1.26 +apply (simp add: monofunI cont2monofunE [OF cont] lub_mono chain)
    1.27 +apply (simp add: cont2contlubE [OF cont])
    1.28 +apply (simp add: diag_lub ch2ch_cont [OF cont] chain)
    1.29 +done
    1.30 +
    1.31  text {* if-then-else is continuous *}
    1.32  
    1.33  lemma cont_if [simp, cont2cont]:
     2.1 --- a/src/HOLCF/Fix.thy	Tue Oct 12 05:25:21 2010 -0700
     2.2 +++ b/src/HOLCF/Fix.thy	Tue Oct 12 05:48:15 2010 -0700
     2.3 @@ -60,13 +60,7 @@
     2.4  text {* direct connection between @{term fix} and iteration *}
     2.5  
     2.6  lemma fix_def2: "fix\<cdot>F = (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)"
     2.7 -apply (unfold fix_def)
     2.8 -apply (rule beta_cfun)
     2.9 -apply (rule cont2cont_lub)
    2.10 -apply (rule ch2ch_lambda)
    2.11 -apply (rule chain_iterate)
    2.12 -apply simp
    2.13 -done
    2.14 +unfolding fix_def by simp
    2.15  
    2.16  lemma iterate_below_fix: "iterate n\<cdot>f\<cdot>\<bottom> \<sqsubseteq> fix\<cdot>f"
    2.17    unfolding fix_def2
     3.1 --- a/src/HOLCF/Fun_Cpo.thy	Tue Oct 12 05:25:21 2010 -0700
     3.2 +++ b/src/HOLCF/Fun_Cpo.thy	Tue Oct 12 05:48:15 2010 -0700
     3.3 @@ -204,10 +204,6 @@
     3.4  apply (simp add: diag_lub ch2ch_fun ch2ch_cont)
     3.5  done
     3.6  
     3.7 -lemma cont2cont_lub:
     3.8 -  "\<lbrakk>chain F; \<And>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i x)"
     3.9 -by (simp add: thelub_fun [symmetric] cont_lub_fun)
    3.10 -
    3.11  lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
    3.12  apply (rule monofunI)
    3.13  apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun])