# HG changeset patch
# User huffman
# Date 1121185604 -7200
# Node ID 555c8951f05cd248030e42912ed578de7c4a59a9
# Parent  a3899ac14a1c515576ed2625a359256a8010805c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined

diff -r a3899ac14a1c -r 555c8951f05c src/HOLCF/Sprod.ML
--- 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";
diff -r a3899ac14a1c -r 555c8951f05c src/HOLCF/Sprod.thy
--- 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)