# HG changeset patch
# User huffman
# Date 1241596649 25200
# Node ID 85b4843d99392ac14284e522a0130ee794eeacb2
# Parent  996ae76c9eda49b29fe75b774f899da6655d830a
replace cont2cont_apply with cont_apply; add new cont2cont lemmas

diff -r 996ae76c9eda -r 85b4843d9939 src/HOLCF/Cfun.thy
--- 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]:
diff -r 996ae76c9eda -r 85b4843d9939 src/HOLCF/Cont.thy
--- 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 *}
 
diff -r 996ae76c9eda -r 85b4843d9939 src/HOLCF/Product_Cpo.thy
--- 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 *}
 
diff -r 996ae76c9eda -r 85b4843d9939 src/HOLCF/Sum_Cpo.thy
--- 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)"