rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs

--- a/src/HOLCF/Cfun.thy	Thu Sep 30 17:06:25 2010 -0700
+++ b/src/HOLCF/Cfun.thy	Thu Sep 30 18:46:19 2010 -0700
@@ -373,13 +373,7 @@
   fixes f :: "'a::cpo \<Rightarrow> 'b::cpo \<Rightarrow> 'c::cpo"
   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 show "cont (\<lambda>y. f x y)"
-    using f by (rule cont_fst_snd_D2)
-next
-  fix y :: 'b show "cont (\<lambda>x. f x y)"
-    using f by (rule cont_fst_snd_D1)
-qed
+using assms by (simp add: cont2cont_LAM prod_cont_iff)
 
 lemma cont2cont_LAM_discrete [simp, cont2cont]:
   "(\<And>y::'a::discrete_cpo. cont (\<lambda>x. f x y)) \<Longrightarrow> cont (\<lambda>x. \<Lambda> y. f x y)"

--- a/src/HOLCF/Library/List_Cpo.thy	Thu Sep 30 17:06:25 2010 -0700
+++ b/src/HOLCF/Library/List_Cpo.thy	Thu Sep 30 18:46:19 2010 -0700
@@ -185,14 +185,7 @@
   assumes g: "cont (\<lambda>x. g x)"
   assumes h: "cont (\<lambda>p. h (fst p) (fst (snd p)) (snd (snd p)))"
   shows "cont (\<lambda>x. case f x of [] \<Rightarrow> g x | y # ys \<Rightarrow> h x y ys)"
-proof -
-  have "\<And>y ys. cont (\<lambda>x. h x (fst (y, ys)) (snd (y, ys)))"
-    by (rule h [THEN cont_fst_snd_D1])
-  hence h1: "\<And>y ys. cont (\<lambda>x. h x y ys)" by simp
-  note h2 = h [THEN cont_fst_snd_D2, THEN cont_fst_snd_D1]
-  note h3 = h [THEN cont_fst_snd_D2, THEN cont_fst_snd_D2]
-  from f g h1 h2 h3 show ?thesis by (rule cont2cont_list_case)
-qed
+using assms by (simp add: cont2cont_list_case prod_cont_iff)
 
 text {* The simple version (due to Joachim Breitner) is needed if the
   element type of the list is not a cpo. *}

--- a/src/HOLCF/Library/Sum_Cpo.thy	Thu Sep 30 17:06:25 2010 -0700
+++ b/src/HOLCF/Library/Sum_Cpo.thy	Thu Sep 30 18:46:19 2010 -0700
@@ -173,17 +173,7 @@
   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
+using assms by (simp add: cont2cont_sum_case prod_cont_iff)
 
 subsection {* Compactness and chain-finiteness *}
 

--- a/src/HOLCF/Product_Cpo.thy	Thu Sep 30 17:06:25 2010 -0700
+++ b/src/HOLCF/Product_Cpo.thy	Thu Sep 30 18:46:19 2010 -0700
@@ -234,7 +234,7 @@
 
 lemmas cont2cont_snd [simp, cont2cont] = cont_compose [OF cont_snd]
 
-lemma cont2cont_split:
+lemma cont2cont_prod_case:
   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)"
@@ -248,6 +248,25 @@
 apply (rule f1)
 done
 
+lemma prod_contI:
+  assumes f1: "\<And>y. cont (\<lambda>x. f (x, y))"
+  assumes f2: "\<And>x. cont (\<lambda>y. f (x, y))"
+  shows "cont f"
+proof -
+  have "cont (\<lambda>(x, y). f (x, y))"
+    by (intro cont2cont_prod_case f1 f2 cont2cont)
+  thus "cont f"
+    by (simp only: split_eta)
+qed
+
+lemma prod_cont_iff:
+  "cont f \<longleftrightarrow> (\<forall>y. cont (\<lambda>x. f (x, y))) \<and> (\<forall>x. cont (\<lambda>y. f (x, y)))"
+apply safe
+apply (erule cont_compose [OF _ cont_pair1])
+apply (erule cont_compose [OF _ cont_pair2])
+apply (simp only: prod_contI)
+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)
@@ -256,23 +275,11 @@
   "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' [simp, cont2cont]:
+lemma cont2cont_prod_case' [simp, 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
+  shows "cont (\<lambda>x. prod_case (f x) (g x))"
+using assms by (simp add: cont2cont_prod_case prod_cont_iff)
 
 text {* The simple version (due to Joachim Breitner) is needed if
   either element type of the pair is not a cpo. *}

--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Sep 30 17:06:25 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Sep 30 18:46:19 2010 -0700
@@ -36,7 +36,7 @@
 
 val beta_rules =
   @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
-  @{thms cont2cont_fst cont2cont_snd cont2cont_Pair cont2cont_split'};
+  @{thms cont2cont_fst cont2cont_snd cont2cont_Pair cont2cont_prod_case'};
 
 val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules);