src/HOLCF/Sprod.thy
changeset 16777 555c8951f05c
parent 16751 7af6723ad741
child 16920 ded12c9e88c2
     1.1 --- a/src/HOLCF/Sprod.thy	Tue Jul 12 18:20:44 2005 +0200
     1.2 +++ b/src/HOLCF/Sprod.thy	Tue Jul 12 18:26:44 2005 +0200
     1.3 @@ -138,9 +138,18 @@
     1.4  lemma ssnd_spair [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>(:x, y:) = y"
     1.5  by (simp add: ssnd_def cont_Rep_Sprod Rep_Sprod_spair)
     1.6  
     1.7 -lemma sfstssnd_defined: "p \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>p \<noteq> \<bottom> \<and> ssnd\<cdot>p \<noteq> \<bottom>"
     1.8 +lemma sfst_defined_iff [simp]: "(sfst\<cdot>p = \<bottom>) = (p = \<bottom>)"
     1.9 +by (rule_tac p=p in sprodE, simp_all)
    1.10 +
    1.11 +lemma ssnd_defined_iff [simp]: "(ssnd\<cdot>p = \<bottom>) = (p = \<bottom>)"
    1.12  by (rule_tac p=p in sprodE, simp_all)
    1.13  
    1.14 +lemma sfst_defined: "p \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>p \<noteq> \<bottom>"
    1.15 +by simp
    1.16 +
    1.17 +lemma ssnd_defined: "p \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>p \<noteq> \<bottom>"
    1.18 +by simp
    1.19 +
    1.20  lemma surjective_pairing_Sprod2: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p"
    1.21  by (rule_tac p=p in sprodE, simp_all)
    1.22