# HG changeset patch
# User huffman
# Date 1242070906 25200
# Node ID 2e9cc546e5b0e8cc0f3d854b55803639e0b32aff
# Parent  15cf300a742f947de6fc2eb475235a7aaf689c7e
use Pair/fst/snd instead of cpair/cfst/csnd

diff -r 15cf300a742f -r 2e9cc546e5b0 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Mon May 11 12:26:33 2009 -0700
+++ b/src/HOLCF/Sprod.thy	Mon May 11 12:41:46 2009 -0700
@@ -5,7 +5,7 @@
 header {* The type of strict products *}
 
 theory Sprod
-imports Cprod
+imports Bifinite
 begin
 
 defaultsort pcpo
@@ -13,7 +13,7 @@
 subsection {* Definition of strict product type *}
 
 pcpodef (Sprod)  ('a, 'b) "**" (infixr "**" 20) =
-        "{p::'a \<times> 'b. p = \<bottom> \<or> (cfst\<cdot>p \<noteq> \<bottom> \<and> csnd\<cdot>p \<noteq> \<bottom>)}"
+        "{p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
 by simp_all
 
 instance "**" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
@@ -28,23 +28,23 @@
   "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
 
 lemma spair_lemma:
-  "<strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a> \<in> Sprod"
+  "(strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a) \<in> Sprod"
 by (simp add: Sprod_def strictify_conv_if)
 
 subsection {* Definitions of constants *}
 
 definition
   sfst :: "('a ** 'b) \<rightarrow> 'a" where
-  "sfst = (\<Lambda> p. cfst\<cdot>(Rep_Sprod p))"
+  "sfst = (\<Lambda> p. fst (Rep_Sprod p))"
 
 definition
   ssnd :: "('a ** 'b) \<rightarrow> 'b" where
-  "ssnd = (\<Lambda> p. csnd\<cdot>(Rep_Sprod p))"
+  "ssnd = (\<Lambda> p. snd (Rep_Sprod p))"
 
 definition
   spair :: "'a \<rightarrow> 'b \<rightarrow> ('a ** 'b)" where
   "spair = (\<Lambda> a b. Abs_Sprod
-             <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>)"
+             (strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a))"
 
 definition
   ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c" where
@@ -62,7 +62,7 @@
 subsection {* Case analysis *}
 
 lemma Rep_Sprod_spair:
-  "Rep_Sprod (:a, b:) = <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>"
+  "Rep_Sprod (:a, b:) = (strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a)"
 unfolding spair_def
 by (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma)
 
@@ -73,7 +73,7 @@
 lemma Exh_Sprod:
   "z = \<bottom> \<or> (\<exists>a b. z = (:a, b:) \<and> a \<noteq> \<bottom> \<and> b \<noteq> \<bottom>)"
 apply (insert Rep_Sprod [of z])
-apply (simp add: Rep_Sprod_simps eq_cprod)
+apply (simp add: Rep_Sprod_simps Pair_fst_snd_eq)
 apply (simp add: Sprod_def)
 apply (erule disjE, simp)
 apply (simp add: strictify_conv_if)
@@ -162,7 +162,7 @@
 
 lemma below_sprod: "x \<sqsubseteq> y = (sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y)"
 apply (simp add: below_Sprod_def sfst_def ssnd_def cont_Rep_Sprod)
-apply (rule below_cprod)
+apply (simp only: below_prod_def)
 done
 
 lemma eq_sprod: "(x = y) = (sfst\<cdot>x = sfst\<cdot>y \<and> ssnd\<cdot>x = ssnd\<cdot>y)"