# HG changeset patch
# User huffman
# Date 1199940200 -3600
# Node ID c58e380d9f7dd8531439fe47411340f7a54173ed
# Parent  d80bd899ea951a718c422f28795949ee711fcb7c
new compactness lemmas; removed duplicated flat_less_iff

diff -r d80bd899ea95 -r c58e380d9f7d src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Thu Jan 10 05:37:18 2008 +0100
+++ b/src/HOLCF/Ssum.thy	Thu Jan 10 05:43:20 2008 +0100
@@ -32,7 +32,6 @@
 syntax (HTML output)
   "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)
 
-
 subsection {* Definitions of constructors *}
 
 definition
@@ -63,14 +62,6 @@
 
 subsection {* Properties of @{term sinl} and @{term sinr} *}
 
-text {* Compactness *}
-
-lemma compact_sinl [simp]: "compact x \<Longrightarrow> compact (sinl\<cdot>x)"
-by (rule compact_Ssum, simp add: Rep_Ssum_sinl strictify_conv_if)
-
-lemma compact_sinr [simp]: "compact x \<Longrightarrow> compact (sinr\<cdot>x)"
-by (rule compact_Ssum, simp add: Rep_Ssum_sinr strictify_conv_if)
-
 text {* Ordering *}
 
 lemma sinl_less [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
@@ -125,6 +116,28 @@
 lemma sinr_defined [intro!]: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>"
 by simp
 
+text {* Compactness *}
+
+lemma compact_sinl: "compact x \<Longrightarrow> compact (sinl\<cdot>x)"
+by (rule compact_Ssum, simp add: Rep_Ssum_sinl strictify_conv_if)
+
+lemma compact_sinr: "compact x \<Longrightarrow> compact (sinr\<cdot>x)"
+by (rule compact_Ssum, simp add: Rep_Ssum_sinr strictify_conv_if)
+
+lemma compact_sinlD: "compact (sinl\<cdot>x) \<Longrightarrow> compact x"
+unfolding compact_def
+by (drule adm_subst [OF cont_Rep_CFun2 [where f=sinl]], simp)
+
+lemma compact_sinrD: "compact (sinr\<cdot>x) \<Longrightarrow> compact x"
+unfolding compact_def
+by (drule adm_subst [OF cont_Rep_CFun2 [where f=sinr]], simp)
+
+lemma compact_sinl_iff [simp]: "compact (sinl\<cdot>x) = compact x"
+by (safe elim!: compact_sinl compact_sinlD)
+
+lemma compact_sinr_iff [simp]: "compact (sinr\<cdot>x) = compact x"
+by (safe elim!: compact_sinr compact_sinrD)
+
 subsection {* Case analysis *}
 
 lemma Exh_Ssum: 
@@ -194,11 +207,6 @@
 
 subsection {* Strict sum preserves flatness *}
 
-lemma flat_less_iff:
-  fixes x y :: "'a::flat"
-  shows "(x \<sqsubseteq> y) = (x = \<bottom> \<or> x = y)"
-by (safe dest!: ax_flat [rule_format])
-
 instance "++" :: (flat, flat) flat
 apply (intro_classes, clarify)
 apply (rule_tac p=x in ssumE, simp)