--- a/src/HOLCF/Cont.thy Wed Jan 02 18:54:21 2008 +0100
+++ b/src/HOLCF/Cont.thy Wed Jan 02 18:57:40 2008 +0100
@@ -8,7 +8,7 @@
header {* Continuity and monotonicity *}
theory Cont
-imports Ffun
+imports Pcpo
begin
text {*
@@ -56,19 +56,6 @@
"\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
by (simp add: monofun_def)
-text {*
- The following results are about application for functions in @{typ "'a=>'b"}
-*}
-
-lemma monofun_fun_fun: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
-by (simp add: less_fun_def)
-
-lemma monofun_fun_arg: "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
-by (rule monofunE)
-
-lemma monofun_fun: "\<lbrakk>monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> g y"
-by (rule trans_less [OF monofun_fun_arg monofun_fun_fun])
-
subsection {* @{prop "monofun f \<and> contlub f \<equiv> cont f"} *}
@@ -185,124 +172,6 @@
lemma cont_if: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. if b then f x else g x)"
by (induct b) simp_all
-subsection {* Propagation of monotonicity and continuity *}
-
-text {* the lub of a chain of monotone functions is monotone *}
-
-lemma monofun_lub_fun:
- "\<lbrakk>chain (F::nat \<Rightarrow> 'a \<Rightarrow> 'b::cpo); \<forall>i. monofun (F i)\<rbrakk>
- \<Longrightarrow> monofun (\<Squnion>i. F i)"
-apply (rule monofunI)
-apply (simp add: thelub_fun)
-apply (rule lub_mono [rule_format])
-apply (erule ch2ch_fun)
-apply (erule ch2ch_fun)
-apply (simp add: monofunE)
-done
-
-text {* the lub of a chain of continuous functions is continuous *}
-
-declare range_composition [simp del]
-
-lemma contlub_lub_fun:
- "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> contlub (\<Squnion>i. F i)"
-apply (rule contlubI)
-apply (simp add: thelub_fun)
-apply (simp add: cont2contlubE)
-apply (rule ex_lub)
-apply (erule ch2ch_fun)
-apply (simp add: ch2ch_cont)
-done
-
-lemma cont_lub_fun:
- "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)"
-apply (rule monocontlub2cont)
-apply (erule monofun_lub_fun)
-apply (simp add: cont2mono)
-apply (erule (1) contlub_lub_fun)
-done
-
-lemma cont2cont_lub:
- "\<lbrakk>chain F; \<And>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i x)"
-by (simp add: thelub_fun [symmetric] cont_lub_fun)
-
-lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
-apply (rule monofunI)
-apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun])
-done
-
-lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
-apply (rule monocontlub2cont)
-apply (erule cont2mono [THEN mono2mono_fun])
-apply (rule contlubI)
-apply (simp add: cont2contlubE)
-apply (simp add: thelub_fun ch2ch_cont)
-done
-
-text {* Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"} *}
-
-lemma mono2mono_lambda: "(\<And>y. monofun (\<lambda>x. f x y)) \<Longrightarrow> monofun f"
-apply (rule monofunI)
-apply (rule less_fun_ext)
-apply (blast dest: monofunE)
-done
-
-lemma cont2cont_lambda: "(\<And>y. cont (\<lambda>x. f x y)) \<Longrightarrow> cont f"
-apply (subgoal_tac "monofun f")
-apply (rule monocontlub2cont)
-apply assumption
-apply (rule contlubI)
-apply (rule ext)
-apply (simp add: thelub_fun ch2ch_monofun)
-apply (blast dest: cont2contlubE)
-apply (simp add: mono2mono_lambda cont2mono)
-done
-
-text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
-
-lemma contlub_lambda:
- "(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo))
- \<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))"
-by (simp add: thelub_fun ch2ch_lambda)
-
-lemma contlub_abstraction:
- "\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow>
- (\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))"
-apply (rule thelub_fun [symmetric])
-apply (rule ch2ch_cont)
-apply (simp add: cont2cont_lambda)
-apply assumption
-done
-
-lemma mono2mono_app:
- "\<lbrakk>monofun f; \<forall>x. monofun (f x); monofun t\<rbrakk> \<Longrightarrow> monofun (\<lambda>x. (f x) (t x))"
-apply (rule monofunI)
-apply (simp add: monofun_fun monofunE)
-done
-
-lemma cont2contlub_app:
- "\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> contlub (\<lambda>x. (f x) (t x))"
-apply (rule contlubI)
-apply (subgoal_tac "chain (\<lambda>i. f (Y i))")
-apply (subgoal_tac "chain (\<lambda>i. t (Y i))")
-apply (simp add: cont2contlubE thelub_fun)
-apply (rule diag_lub)
-apply (erule ch2ch_fun)
-apply (drule spec)
-apply (erule (1) ch2ch_cont)
-apply (erule (1) ch2ch_cont)
-apply (erule (1) ch2ch_cont)
-done
-
-lemma cont2cont_app:
- "\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. (f x) (t x))"
-by (blast intro: monocontlub2cont mono2mono_app cont2mono cont2contlub_app)
-
-lemmas cont2cont_app2 = cont2cont_app [rule_format]
-
-lemma cont2cont_app3: "\<lbrakk>cont f; cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. f (t x))"
-by (rule cont2cont_app2 [OF cont_const])
-
subsection {* Finite chains and flat pcpos *}
text {* monotone functions map finite chains to finite chains *}