--- a/src/HOLCF/Cfun.thy Mon Mar 22 16:02:51 2010 -0700
+++ b/src/HOLCF/Cfun.thy Mon Mar 22 20:54:52 2010 -0700
@@ -185,23 +185,20 @@
done
lemmas monofun_Rep_CFun = cont_Rep_CFun [THEN cont2mono]
-lemmas contlub_Rep_CFun = cont_Rep_CFun [THEN cont2contlub]
lemmas monofun_Rep_CFun1 = cont_Rep_CFun1 [THEN cont2mono, standard]
-lemmas contlub_Rep_CFun1 = cont_Rep_CFun1 [THEN cont2contlub, standard]
lemmas monofun_Rep_CFun2 = cont_Rep_CFun2 [THEN cont2mono, standard]
-lemmas contlub_Rep_CFun2 = cont_Rep_CFun2 [THEN cont2contlub, standard]
text {* contlub, cont properties of @{term Rep_CFun} in each argument *}
lemma contlub_cfun_arg: "chain Y \<Longrightarrow> f\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. f\<cdot>(Y i))"
-by (rule contlub_Rep_CFun2 [THEN contlubE])
+by (rule cont_Rep_CFun2 [THEN cont2contlubE])
lemma cont_cfun_arg: "chain Y \<Longrightarrow> range (\<lambda>i. f\<cdot>(Y i)) <<| f\<cdot>(\<Squnion>i. Y i)"
by (rule cont_Rep_CFun2 [THEN contE])
lemma contlub_cfun_fun: "chain F \<Longrightarrow> (\<Squnion>i. F i)\<cdot>x = (\<Squnion>i. F i\<cdot>x)"
-by (rule contlub_Rep_CFun1 [THEN contlubE])
+by (rule cont_Rep_CFun1 [THEN cont2contlubE])
lemma cont_cfun_fun: "chain F \<Longrightarrow> range (\<lambda>i. F i\<cdot>x) <<| (\<Squnion>i. F i)\<cdot>x"
by (rule cont_Rep_CFun1 [THEN contE])
@@ -530,26 +527,16 @@
apply (auto simp add: monofun_cfun_arg)
done
-(*FIXME: long proof*)
-lemma contlub_strictify2: "contlub (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
-apply (rule contlubI)
-apply (case_tac "(\<Squnion>i. Y i) = \<bottom>")
-apply (drule (1) chain_UU_I)
-apply simp
-apply (simp del: if_image_distrib)
-apply (simp only: contlub_cfun_arg)
-apply (rule lub_equal2)
-apply (rule chain_mono2 [THEN exE])
-apply (erule chain_UU_I_inverse2)
-apply (assumption)
-apply (rule_tac x=x in exI, clarsimp)
-apply (erule chain_monofun)
-apply (erule monofun_strictify2 [THEN ch2ch_monofun])
+lemma cont_strictify2: "cont (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
+apply (rule contI2)
+apply (rule monofun_strictify2)
+apply (case_tac "(\<Squnion>i. Y i) = \<bottom>", simp)
+apply (simp add: contlub_cfun_arg del: if_image_distrib)
+apply (drule chain_UU_I_inverse2, clarify, rename_tac j)
+apply (rule lub_mono2, rule_tac x=j in exI, simp_all)
+apply (auto dest!: chain_mono_less)
done
-lemmas cont_strictify2 =
- monocontlub2cont [OF monofun_strictify2 contlub_strictify2, standard]
-
lemma strictify_conv_if: "strictify\<cdot>f\<cdot>x = (if x = \<bottom> then \<bottom> else f\<cdot>x)"
unfolding strictify_def
by (simp add: cont_strictify1 cont_strictify2 cont2cont_LAM)
--- a/src/HOLCF/Cont.thy Mon Mar 22 16:02:51 2010 -0700
+++ b/src/HOLCF/Cont.thy Mon Mar 22 20:54:52 2010 -0700
@@ -22,22 +22,17 @@
monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" -- "monotonicity" where
"monofun f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
+(*
definition
contlub :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool" -- "first cont. def" where
"contlub f = (\<forall>Y. chain Y \<longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i)))"
+*)
definition
- cont :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool" -- "secnd cont. def" where
+ cont :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"
+where
"cont f = (\<forall>Y. chain Y \<longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i))"
-lemma contlubI:
- "\<lbrakk>\<And>Y. chain Y \<Longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))\<rbrakk> \<Longrightarrow> contlub f"
-by (simp add: contlub_def)
-
-lemma contlubE:
- "\<lbrakk>contlub f; chain Y\<rbrakk> \<Longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))"
-by (simp add: contlub_def)
-
lemma contI:
"\<lbrakk>\<And>Y. chain Y \<Longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> cont f"
by (simp add: cont_def)
@@ -74,16 +69,7 @@
apply (erule ub_rangeD)
done
-text {* left to right: @{prop "monofun f \<and> contlub f \<Longrightarrow> cont f"} *}
-
-lemma monocontlub2cont: "\<lbrakk>monofun f; contlub f\<rbrakk> \<Longrightarrow> cont f"
-apply (rule contI)
-apply (rule thelubE)
-apply (erule (1) ch2ch_monofun)
-apply (erule (1) contlubE [symmetric])
-done
-
-text {* first a lemma about binary chains *}
+text {* a lemma about binary chains *}
lemma binchain_cont:
"\<lbrakk>cont f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> range (\<lambda>i::nat. f (if i = 0 then x else y)) <<| f y"
@@ -95,8 +81,7 @@
apply (erule lub_bin_chain [THEN thelubI])
done
-text {* right to left: @{prop "cont f \<Longrightarrow> monofun f \<and> contlub f"} *}
-text {* part1: @{prop "cont f \<Longrightarrow> monofun f"} *}
+text {* continuity implies monotonicity *}
lemma cont2mono: "cont f \<Longrightarrow> monofun f"
apply (rule monofunI)
@@ -109,33 +94,30 @@
lemmas ch2ch_cont = cont2mono [THEN ch2ch_monofun]
-text {* right to left: @{prop "cont f \<Longrightarrow> monofun f \<and> contlub f"} *}
-text {* part2: @{prop "cont f \<Longrightarrow> contlub f"} *}
+text {* continuity implies preservation of lubs *}
-lemma cont2contlub: "cont f \<Longrightarrow> contlub f"
-apply (rule contlubI)
+lemma cont2contlubE:
+ "\<lbrakk>cont f; chain Y\<rbrakk> \<Longrightarrow> f (\<Squnion> i. Y i) = (\<Squnion> i. f (Y i))"
apply (rule thelubI [symmetric])
apply (erule (1) contE)
done
-lemmas cont2contlubE = cont2contlub [THEN contlubE]
-
lemma contI2:
assumes mono: "monofun f"
assumes below: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk>
\<Longrightarrow> f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))"
shows "cont f"
-apply (rule monocontlub2cont)
-apply (rule mono)
-apply (rule contlubI)
+apply (rule contI)
+apply (rule thelubE)
+apply (erule ch2ch_monofun [OF mono])
apply (rule below_antisym)
-apply (rule below, assumption)
-apply (erule ch2ch_monofun [OF mono])
apply (rule is_lub_thelub)
apply (erule ch2ch_monofun [OF mono])
apply (rule ub2ub_monofun [OF mono])
apply (rule is_lubD1)
apply (erule cpo_lubI)
+apply (rule below, assumption)
+apply (erule ch2ch_monofun [OF mono])
done
subsection {* Continuity simproc *}
@@ -190,7 +172,7 @@
assumes 2: "\<And>x. cont (\<lambda>y. f x y)"
assumes 3: "\<And>y. cont (\<lambda>x. f x y)"
shows "cont (\<lambda>x. (f x) (t x))"
-proof (rule monocontlub2cont [OF monofunI contlubI])
+proof (rule contI2 [OF monofunI])
fix x y :: "'a" assume "x \<sqsubseteq> y"
then show "f x (t x) \<sqsubseteq> f y (t y)"
by (auto intro: cont2monofunE [OF 1]
@@ -199,11 +181,11 @@
below_trans)
next
fix Y :: "nat \<Rightarrow> 'a" assume "chain Y"
- then show "f (\<Squnion>i. Y i) (t (\<Squnion>i. Y i)) = (\<Squnion>i. f (Y i) (t (Y i)))"
+ then show "f (\<Squnion>i. Y i) (t (\<Squnion>i. Y i)) \<sqsubseteq> (\<Squnion>i. f (Y i) (t (Y i)))"
by (simp only: cont2contlubE [OF 1] ch2ch_cont [OF 1]
cont2contlubE [OF 2] ch2ch_cont [OF 2]
cont2contlubE [OF 3] ch2ch_cont [OF 3]
- diag_lub)
+ diag_lub below_refl)
qed
lemma cont_compose:
@@ -234,9 +216,7 @@
by (rule cont2mono [THEN monofun_finch2finch])
lemma chfindom_monofun2cont: "monofun f \<Longrightarrow> cont (f::'a::chfin \<Rightarrow> 'b::cpo)"
-apply (rule monocontlub2cont)
-apply assumption
-apply (rule contlubI)
+apply (erule contI2)
apply (frule chfin2finch)
apply (clarsimp simp add: finite_chain_def)
apply (subgoal_tac "max_in_chain i (\<lambda>i. f (Y i))")
--- a/src/HOLCF/FOCUS/Fstreams.thy Mon Mar 22 16:02:51 2010 -0700
+++ b/src/HOLCF/FOCUS/Fstreams.thy Mon Mar 22 20:54:52 2010 -0700
@@ -324,15 +324,6 @@
lemma cpo_cont_lemma:
"[| monofun (f::'a::cpo => 'b::cpo); (!Y. chain Y --> f (lub(range Y)) << (LUB i. f (Y i))) |] ==> cont f"
-apply (rule monocontlub2cont, auto)
-apply (simp add: contlub_def, auto)
-apply (erule_tac x="Y" in allE, auto)
-apply (simp add: po_eq_conv)
-apply (frule cpo,auto)
-apply (frule is_lubD1)
-apply (frule ub2ub_monofun, auto)
-apply (drule thelubI, auto)
-apply (rule is_lub_thelub, auto)
-by (erule ch2ch_monofun, simp)
+by (erule contI2, simp)
end
--- a/src/HOLCF/Ffun.thy Mon Mar 22 16:02:51 2010 -0700
+++ b/src/HOLCF/Ffun.thy Mon Mar 22 20:54:52 2010 -0700
@@ -196,22 +196,13 @@
text {* the lub of a chain of continuous functions is continuous *}
-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 (rule contI2)
apply (erule monofun_lub_fun)
apply (simp add: cont2mono)
-apply (erule (1) contlub_lub_fun)
+apply (simp add: thelub_fun cont2contlubE)
+apply (simp add: diag_lub ch2ch_fun ch2ch_cont)
done
lemma cont2cont_lub:
@@ -224,9 +215,8 @@
done
lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
-apply (rule monocontlub2cont)
+apply (rule contI2)
apply (erule cont2mono [THEN mono2mono_fun])
-apply (rule contlubI)
apply (simp add: cont2contlubE)
apply (simp add: thelub_fun ch2ch_cont)
done
@@ -242,14 +232,10 @@
lemma cont2cont_lambda [simp]:
assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "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 (erule cont2contlubE [OF f])
+apply (rule contI2)
apply (simp add: mono2mono_lambda cont2mono f)
+apply (rule below_fun_ext)
+apply (simp add: thelub_fun cont2contlubE [OF f])
done
text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
@@ -272,23 +258,12 @@
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)
+apply (erule cont_apply [where t=t])
+apply (erule spec)
+apply (erule cont2cont_fun)
+done
lemmas cont2cont_app2 = cont2cont_app [rule_format]
--- a/src/HOLCF/Product_Cpo.thy Mon Mar 22 16:02:51 2010 -0700
+++ b/src/HOLCF/Product_Cpo.thy Mon Mar 22 20:54:52 2010 -0700
@@ -203,26 +203,16 @@
apply (erule cpo_lubI)
done
-lemma contlub_fst: "contlub fst"
-apply (rule contlubI)
+lemma cont_fst: "cont fst"
+apply (rule contI)
apply (simp add: thelub_cprod)
-done
-
-lemma contlub_snd: "contlub snd"
-apply (rule contlubI)
-apply (simp add: thelub_cprod)
-done
-
-lemma cont_fst: "cont fst"
-apply (rule monocontlub2cont)
-apply (rule monofun_fst)
-apply (rule contlub_fst)
+apply (erule cpo_lubI [OF ch2ch_fst])
done
lemma cont_snd: "cont snd"
-apply (rule monocontlub2cont)
-apply (rule monofun_snd)
-apply (rule contlub_snd)
+apply (rule contI)
+apply (simp add: thelub_cprod)
+apply (erule cpo_lubI [OF ch2ch_snd])
done
lemma cont2cont_Pair [cont2cont]:
--- a/src/HOLCF/ex/Stream.thy Mon Mar 22 16:02:51 2010 -0700
+++ b/src/HOLCF/ex/Stream.thy Mon Mar 22 20:54:52 2010 -0700
@@ -920,11 +920,8 @@
apply (simp add: chain_def,auto)
by (rule monofun_cfun_arg,simp)
-lemma contlub_scons: "contlub (%x. a && x)"
-by (simp add: contlub_Rep_CFun2)
-
lemma contlub_scons_lemma: "chain S ==> (LUB i. a && S i) = a && (LUB i. S i)"
-by (rule contlubE [OF contlub_Rep_CFun2, symmetric])
+by (rule cont2contlubE [OF cont_Rep_CFun2, symmetric])
lemma finite_lub_sconc: "chain Y ==> (stream_finite x) ==>
(LUB i. x ooo Y i) = (x ooo (LUB i. Y i))"
@@ -940,9 +937,6 @@
apply (drule finite_lub_sconc,auto simp add: slen_infinite)
done
-lemma contlub_sconc: "contlub (%y. x ooo y)"
-by (rule cont_sconc [THEN cont2contlub])
-
lemma monofun_sconc: "monofun (%y. x ooo y)"
by (simp add: monofun_def sconc_mono)