# HG changeset patch
# User huffman
# Date 1129074217 -7200
# Node ID 2922be3544f8587c052df054506dcb70cec8b905
# Parent  5d9c9e284d1647e3d1073f8124322ca66440ba50
added compactness lemmas; cleaned up

diff -r 5d9c9e284d16 -r 2922be3544f8 src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Tue Oct 11 23:47:29 2005 +0200
+++ b/src/HOLCF/Cprod.thy	Wed Oct 12 01:43:37 2005 +0200
@@ -274,6 +274,9 @@
 lemma eq_cprod: "(x = y) = (cfst\<cdot>x = cfst\<cdot>y \<and> csnd\<cdot>x = csnd\<cdot>y)"
 by (auto simp add: po_eq_conv less_cprod)
 
+lemma compact_cpair [simp]: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact <x, y>"
+by (rule compactI, simp add: less_cprod)
+
 lemma lub_cprod2: 
   "chain S \<Longrightarrow> range S <<| <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
 apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd)
diff -r 5d9c9e284d16 -r 2922be3544f8 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Tue Oct 11 23:47:29 2005 +0200
+++ b/src/HOLCF/Sprod.thy	Wed Oct 12 01:43:37 2005 +0200
@@ -110,6 +110,15 @@
 lemma inst_sprod_pcpo2: "UU = (:UU,UU:)"
 by simp
 
+lemma Rep_Sprod_spair:
+  "Rep_Sprod (:a, b:) = <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>"
+apply (unfold spair_def)
+apply (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma)
+done
+
+lemma compact_spair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (:x, y:)"
+by (rule compact_Sprod, simp add: Rep_Sprod_spair strictify_conv_if)
+
 subsection {* Properties of @{term sfst} and @{term ssnd} *}
 
 lemma sfst_strict [simp]: "sfst\<cdot>\<bottom> = \<bottom>"
@@ -118,12 +127,6 @@
 lemma ssnd_strict [simp]: "ssnd\<cdot>\<bottom> = \<bottom>"
 by (simp add: ssnd_def cont_Rep_Sprod Rep_Sprod_strict)
 
-lemma Rep_Sprod_spair:
-  "Rep_Sprod (:a, b:) = <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>"
-apply (unfold spair_def)
-apply (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma)
-done
-
 lemma sfst_spair [simp]: "y \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>(:x, y:) = x"
 by (simp add: sfst_def cont_Rep_Sprod Rep_Sprod_spair)
 
diff -r 5d9c9e284d16 -r 2922be3544f8 src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Tue Oct 11 23:47:29 2005 +0200
+++ b/src/HOLCF/Ssum.thy	Wed Oct 12 01:43:37 2005 +0200
@@ -48,6 +48,12 @@
 lemma Rep_Ssum_sinr: "Rep_Ssum (sinr\<cdot>b) = <\<bottom>, b>"
 by (unfold sinr_def, simp add: cont_Abs_Ssum Abs_Ssum_inverse Ssum_def)
 
+lemma compact_sinl [simp]: "compact x \<Longrightarrow> compact (sinl\<cdot>x)"
+by (rule compact_Ssum, simp add: Rep_Ssum_sinl)
+
+lemma compact_sinr [simp]: "compact x \<Longrightarrow> compact (sinr\<cdot>x)"
+by (rule compact_Ssum, simp add: Rep_Ssum_sinr)
+
 lemma sinl_strict [simp]: "sinl\<cdot>\<bottom> = \<bottom>"
 by (simp add: sinl_Abs_Ssum Abs_Ssum_strict cpair_strict)
 
@@ -67,14 +73,10 @@
 by (rule sinr_eq [THEN iffD1])
 
 lemma sinl_defined_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)"
-apply (rule sinl_strict [THEN subst])
-apply (rule sinl_eq)
-done
+by (cut_tac sinl_eq [of "x" "\<bottom>"], simp)
 
 lemma sinr_defined_iff [simp]: "(sinr\<cdot>x = \<bottom>) = (x = \<bottom>)"
-apply (rule sinr_strict [THEN subst])
-apply (rule sinr_eq)
-done
+by (cut_tac sinr_eq [of "x" "\<bottom>"], simp)
 
 lemma sinl_defined [intro!]: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>"
 by simp