src/HOLCF/Ssum.thy

 syntax (xsymbols)
   "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)
 syntax (HTML output)
   "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)
 
-
 subsection {* Definitions of constructors *}
 
 definition
   sinl :: "'a \<rightarrow> ('a ++ 'b)" where
   "sinl = (\<Lambda> a. Abs_Ssum <strictify\<cdot>(\<Lambda> _. TT)\<cdot>a, a, \<bottom>>)"

 lemma Rep_Ssum_sinr: "Rep_Ssum (sinr\<cdot>b) = <strictify\<cdot>(\<Lambda> _. FF)\<cdot>b, \<bottom>, b>"
 by (simp add: sinr_Abs_Ssum Abs_Ssum_inverse sinr_Ssum)
 
 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)"
 by (simp add: less_Ssum_def Rep_Ssum_sinl strictify_conv_if)
 

 lemma sinl_defined [intro!]: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>"
 by simp
 
 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: 
   "z = \<bottom> \<or> (\<exists>a. z = sinl\<cdot>a \<and> a \<noteq> \<bottom>) \<or> (\<exists>b. z = sinr\<cdot>b \<and> b \<noteq> \<bottom>)"

 lemma sscase4 [simp]: "sscase\<cdot>sinl\<cdot>sinr\<cdot>z = z"
 by (cases z, simp_all)
 
 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)
 apply (rule_tac p=y in ssumE, simp_all add: flat_less_iff)
 apply (rule_tac p=y in ssumE, simp_all add: flat_less_iff)