src/HOLCF/Sprod.thy
changeset 25881 d80bd899ea95
parent 25827 c2adeb1bae5c
child 25914 ff835e25ae87
     1.1 --- a/src/HOLCF/Sprod.thy	Thu Jan 10 05:36:03 2008 +0100
     1.2 +++ b/src/HOLCF/Sprod.thy	Thu Jan 10 05:37:18 2008 +0100
     1.3 @@ -62,7 +62,6 @@
     1.4  translations
     1.5    "\<Lambda>(CONST spair\<cdot>x\<cdot>y). t" == "CONST ssplit\<cdot>(\<Lambda> x y. t)"
     1.6  
     1.7 -
     1.8  subsection {* Case analysis *}
     1.9  
    1.10  lemma spair_Abs_Sprod:
    1.11 @@ -133,9 +132,6 @@
    1.12  apply (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma)
    1.13  done
    1.14  
    1.15 -lemma compact_spair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (:x, y:)"
    1.16 -by (rule compact_Sprod, simp add: Rep_Sprod_spair strictify_conv_if)
    1.17 -
    1.18  subsection {* Properties of @{term sfst} and @{term ssnd} *}
    1.19  
    1.20  lemma sfst_strict [simp]: "sfst\<cdot>\<bottom> = \<bottom>"
    1.21 @@ -180,6 +176,36 @@
    1.22  apply (simp add: less_sprod)
    1.23  done
    1.24  
    1.25 +lemma sfst_less_iff: "sfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> (:y, ssnd\<cdot>x:)"
    1.26 +apply (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp)
    1.27 +apply (simp add: less_sprod)
    1.28 +done
    1.29 +
    1.30 +lemma ssnd_less_iff: "ssnd\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> (:sfst\<cdot>x, y:)"
    1.31 +apply (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp)
    1.32 +apply (simp add: less_sprod)
    1.33 +done
    1.34 +
    1.35 +subsection {* Compactness *}
    1.36 +
    1.37 +lemma compact_sfst: "compact x \<Longrightarrow> compact (sfst\<cdot>x)"
    1.38 +by (rule compactI, simp add: sfst_less_iff)
    1.39 +
    1.40 +lemma compact_ssnd: "compact x \<Longrightarrow> compact (ssnd\<cdot>x)"
    1.41 +by (rule compactI, simp add: ssnd_less_iff)
    1.42 +
    1.43 +lemma compact_spair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (:x, y:)"
    1.44 +by (rule compact_Sprod, simp add: Rep_Sprod_spair strictify_conv_if)
    1.45 +
    1.46 +lemma compact_spair_iff:
    1.47 +  "compact (:x, y:) = (x = \<bottom> \<or> y = \<bottom> \<or> (compact x \<and> compact y))"
    1.48 +apply (safe elim!: compact_spair)
    1.49 +apply (drule compact_sfst, simp)
    1.50 +apply (drule compact_ssnd, simp)
    1.51 +apply simp
    1.52 +apply simp
    1.53 +done
    1.54 +
    1.55  subsection {* Properties of @{term ssplit} *}
    1.56  
    1.57  lemma ssplit1 [simp]: "ssplit\<cdot>f\<cdot>\<bottom> = \<bottom>"