--- a/src/HOLCF/Sprod.ML Tue Jul 12 18:20:44 2005 +0200
+++ b/src/HOLCF/Sprod.ML Tue Jul 12 18:26:44 2005 +0200
@@ -21,7 +21,8 @@
val ssnd_strict = thm "ssnd_strict";
val sfst_spair = thm "sfst_spair";
val ssnd_spair = thm "ssnd_spair";
-val sfstssnd_defined = thm "sfstssnd_defined";
+val sfst_defined = thm "sfst_defined";
+val ssnd_defined = thm "ssnd_defined";
val surjective_pairing_Sprod2 = thm "surjective_pairing_Sprod2";
val less_sprod = thm "less_sprod";
val spair_less = thm "spair_less";
--- a/src/HOLCF/Sprod.thy Tue Jul 12 18:20:44 2005 +0200
+++ b/src/HOLCF/Sprod.thy Tue Jul 12 18:26:44 2005 +0200
@@ -138,9 +138,18 @@
lemma ssnd_spair [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>(:x, y:) = y"
by (simp add: ssnd_def cont_Rep_Sprod Rep_Sprod_spair)
-lemma sfstssnd_defined: "p \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>p \<noteq> \<bottom> \<and> ssnd\<cdot>p \<noteq> \<bottom>"
+lemma sfst_defined_iff [simp]: "(sfst\<cdot>p = \<bottom>) = (p = \<bottom>)"
+by (rule_tac p=p in sprodE, simp_all)
+
+lemma ssnd_defined_iff [simp]: "(ssnd\<cdot>p = \<bottom>) = (p = \<bottom>)"
by (rule_tac p=p in sprodE, simp_all)
+lemma sfst_defined: "p \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>p \<noteq> \<bottom>"
+by simp
+
+lemma ssnd_defined: "p \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>p \<noteq> \<bottom>"
+by simp
+
lemma surjective_pairing_Sprod2: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p"
by (rule_tac p=p in sprodE, simp_all)