--- a/src/HOLCF/Cfun.thy Wed May 06 09:08:47 2009 +0200
+++ b/src/HOLCF/Cfun.thy Wed May 06 00:57:29 2009 -0700
@@ -345,21 +345,11 @@
assumes f: "cont (\<lambda>p. f (fst p) (snd p))"
shows "cont (\<lambda>x. \<Lambda> y. f x y)"
proof (rule cont2cont_LAM)
- fix x :: 'a
- have "cont (\<lambda>y. (x, y))"
- by (rule cont_pair2)
- with f have "cont (\<lambda>y. f (fst (x, y)) (snd (x, y)))"
- by (rule cont2cont_app3)
- thus "cont (\<lambda>y. f x y)"
- by (simp only: fst_conv snd_conv)
+ fix x :: 'a show "cont (\<lambda>y. f x y)"
+ using f by (rule cont_fst_snd_D2)
next
- fix y :: 'b
- have "cont (\<lambda>x. (x, y))"
- by (rule cont_pair1)
- with f have "cont (\<lambda>x. f (fst (x, y)) (snd (x, y)))"
- by (rule cont2cont_app3)
- thus "cont (\<lambda>x. f x y)"
- by (simp only: fst_conv snd_conv)
+ fix y :: 'b show "cont (\<lambda>x. f x y)"
+ using f by (rule cont_fst_snd_D1)
qed
lemma cont2cont_LAM_discrete [cont2cont]:
--- a/src/HOLCF/Cont.thy Wed May 06 09:08:47 2009 +0200
+++ b/src/HOLCF/Cont.thy Wed May 06 00:57:29 2009 -0700
@@ -180,31 +180,31 @@
text {* application of functions is continuous *}
-lemma cont2cont_apply:
+lemma cont_apply:
fixes f :: "'a::cpo \<Rightarrow> 'b::cpo \<Rightarrow> 'c::cpo" and t :: "'a \<Rightarrow> 'b"
- assumes f1: "\<And>y. cont (\<lambda>x. f x y)"
- assumes f2: "\<And>x. cont (\<lambda>y. f x y)"
- assumes t: "cont (\<lambda>x. t x)"
+ assumes 1: "cont (\<lambda>x. t x)"
+ 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])
fix x y :: "'a" assume "x \<sqsubseteq> y"
then show "f x (t x) \<sqsubseteq> f y (t y)"
- by (auto intro: cont2monofunE [OF f1]
- cont2monofunE [OF f2]
- cont2monofunE [OF t]
+ by (auto intro: cont2monofunE [OF 1]
+ cont2monofunE [OF 2]
+ cont2monofunE [OF 3]
trans_less)
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)))"
- by (simp only: cont2contlubE [OF t] ch2ch_cont [OF t]
- cont2contlubE [OF f1] ch2ch_cont [OF f1]
- cont2contlubE [OF f2] ch2ch_cont [OF f2]
+ 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)
qed
-lemma cont2cont_compose:
+lemma cont_compose:
"\<lbrakk>cont c; cont (\<lambda>x. f x)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. c (f x))"
-by (rule cont2cont_apply [OF cont_const])
+by (rule cont_apply [OF _ _ cont_const])
text {* if-then-else is continuous *}
--- a/src/HOLCF/Product_Cpo.thy Wed May 06 09:08:47 2009 +0200
+++ b/src/HOLCF/Product_Cpo.thy Wed May 06 00:57:29 2009 -0700
@@ -206,14 +206,54 @@
assumes f: "cont (\<lambda>x. f x)"
assumes g: "cont (\<lambda>x. g x)"
shows "cont (\<lambda>x. (f x, g x))"
-apply (rule cont2cont_apply [OF _ cont_pair1 f])
-apply (rule cont2cont_apply [OF _ cont_pair2 g])
+apply (rule cont_apply [OF f cont_pair1])
+apply (rule cont_apply [OF g cont_pair2])
apply (rule cont_const)
done
-lemmas cont2cont_fst [cont2cont] = cont2cont_compose [OF cont_fst]
+lemmas cont2cont_fst [cont2cont] = cont_compose [OF cont_fst]
+
+lemmas cont2cont_snd [cont2cont] = cont_compose [OF cont_snd]
+
+lemma cont2cont_split:
+ assumes f1: "\<And>a b. cont (\<lambda>x. f x a b)"
+ assumes f2: "\<And>x b. cont (\<lambda>a. f x a b)"
+ assumes f3: "\<And>x a. cont (\<lambda>b. f x a b)"
+ assumes g: "cont (\<lambda>x. g x)"
+ shows "cont (\<lambda>x. split (\<lambda>a b. f x a b) (g x))"
+unfolding split_def
+apply (rule cont_apply [OF g])
+apply (rule cont_apply [OF cont_fst f2])
+apply (rule cont_apply [OF cont_snd f3])
+apply (rule cont_const)
+apply (rule f1)
+done
+
+lemma cont_fst_snd_D1:
+ "cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>x. f x y)"
+by (drule cont_compose [OF _ cont_pair1], simp)
-lemmas cont2cont_snd [cont2cont] = cont2cont_compose [OF cont_snd]
+lemma cont_fst_snd_D2:
+ "cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>y. f x y)"
+by (drule cont_compose [OF _ cont_pair2], simp)
+
+lemma cont2cont_split' [cont2cont]:
+ assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))"
+ assumes g: "cont (\<lambda>x. g x)"
+ shows "cont (\<lambda>x. split (f x) (g x))"
+proof -
+ note f1 = f [THEN cont_fst_snd_D1]
+ note f2 = f [THEN cont_fst_snd_D2, THEN cont_fst_snd_D1]
+ note f3 = f [THEN cont_fst_snd_D2, THEN cont_fst_snd_D2]
+ show ?thesis
+ unfolding split_def
+ apply (rule cont_apply [OF g])
+ apply (rule cont_apply [OF cont_fst f2])
+ apply (rule cont_apply [OF cont_snd f3])
+ apply (rule cont_const)
+ apply (rule f1)
+ done
+qed
subsection {* Compactness and chain-finiteness *}
--- a/src/HOLCF/Sum_Cpo.thy Wed May 06 09:08:47 2009 +0200
+++ b/src/HOLCF/Sum_Cpo.thy Wed May 06 00:57:29 2009 -0700
@@ -130,17 +130,14 @@
subsection {* Continuity of @{term Inl}, @{term Inr}, @{term sum_case} *}
-lemma cont2cont_Inl [simp]: "cont f \<Longrightarrow> cont (\<lambda>x. Inl (f x))"
-by (fast intro: contI is_lub_Inl elim: contE)
-
-lemma cont2cont_Inr [simp]: "cont f \<Longrightarrow> cont (\<lambda>x. Inr (f x))"
-by (fast intro: contI is_lub_Inr elim: contE)
-
lemma cont_Inl: "cont Inl"
-by (rule cont2cont_Inl [OF cont_id])
+by (intro contI is_lub_Inl cpo_lubI)
lemma cont_Inr: "cont Inr"
-by (rule cont2cont_Inr [OF cont_id])
+by (intro contI is_lub_Inr cpo_lubI)
+
+lemmas cont2cont_Inl [cont2cont] = cont_compose [OF cont_Inl]
+lemmas cont2cont_Inr [cont2cont] = cont_compose [OF cont_Inr]
lemmas ch2ch_Inl [simp] = ch2ch_cont [OF cont_Inl]
lemmas ch2ch_Inr [simp] = ch2ch_cont [OF cont_Inr]
@@ -161,16 +158,33 @@
apply (simp add: cont2contlubE [OF cont_Inr, symmetric] contE)
done
-lemma cont2cont_sum_case [simp]:
+lemma cont2cont_sum_case:
assumes f1: "\<And>a. cont (\<lambda>x. f x a)" and f2: "\<And>x. cont (\<lambda>a. f x a)"
assumes g1: "\<And>b. cont (\<lambda>x. g x b)" and g2: "\<And>x. cont (\<lambda>b. g x b)"
assumes h: "cont (\<lambda>x. h x)"
shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
-apply (rule cont2cont_app2 [OF cont2cont_lambda _ h])
+apply (rule cont_apply [OF h])
+apply (rule cont_sum_case2 [OF f2 g2])
apply (rule cont_sum_case1 [OF f1 g1])
-apply (rule cont_sum_case2 [OF f2 g2])
done
+lemma cont2cont_sum_case' [cont2cont]:
+ assumes f: "cont (\<lambda>p. f (fst p) (snd p))"
+ assumes g: "cont (\<lambda>p. g (fst p) (snd p))"
+ assumes h: "cont (\<lambda>x. h x)"
+ shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
+proof -
+ note f1 = f [THEN cont_fst_snd_D1]
+ note f2 = f [THEN cont_fst_snd_D2]
+ note g1 = g [THEN cont_fst_snd_D1]
+ note g2 = g [THEN cont_fst_snd_D2]
+ show ?thesis
+ apply (rule cont_apply [OF h])
+ apply (rule cont_sum_case2 [OF f2 g2])
+ apply (rule cont_sum_case1 [OF f1 g1])
+ done
+qed
+
subsection {* Compactness and chain-finiteness *}
lemma compact_Inl: "compact a \<Longrightarrow> compact (Inl a)"