added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
authorhuffman
Tue Jul 12 18:26:44 2005 +0200 (2005-07-12)
changeset 16777555c8951f05c
parent 16776 a3899ac14a1c
child 16778 2162c0de4673
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
src/HOLCF/Sprod.ML
src/HOLCF/Sprod.thy
     1.1 --- a/src/HOLCF/Sprod.ML	Tue Jul 12 18:20:44 2005 +0200
     1.2 +++ b/src/HOLCF/Sprod.ML	Tue Jul 12 18:26:44 2005 +0200
     1.3 @@ -21,7 +21,8 @@
     1.4  val ssnd_strict = thm "ssnd_strict";
     1.5  val sfst_spair = thm "sfst_spair";
     1.6  val ssnd_spair = thm "ssnd_spair";
     1.7 -val sfstssnd_defined = thm "sfstssnd_defined";
     1.8 +val sfst_defined = thm "sfst_defined";
     1.9 +val ssnd_defined = thm "ssnd_defined";
    1.10  val surjective_pairing_Sprod2 = thm "surjective_pairing_Sprod2";
    1.11  val less_sprod = thm "less_sprod";
    1.12  val spair_less = thm "spair_less";
     2.1 --- a/src/HOLCF/Sprod.thy	Tue Jul 12 18:20:44 2005 +0200
     2.2 +++ b/src/HOLCF/Sprod.thy	Tue Jul 12 18:26:44 2005 +0200
     2.3 @@ -138,9 +138,18 @@
     2.4  lemma ssnd_spair [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>(:x, y:) = y"
     2.5  by (simp add: ssnd_def cont_Rep_Sprod Rep_Sprod_spair)
     2.6  
     2.7 -lemma sfstssnd_defined: "p \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>p \<noteq> \<bottom> \<and> ssnd\<cdot>p \<noteq> \<bottom>"
     2.8 +lemma sfst_defined_iff [simp]: "(sfst\<cdot>p = \<bottom>) = (p = \<bottom>)"
     2.9 +by (rule_tac p=p in sprodE, simp_all)
    2.10 +
    2.11 +lemma ssnd_defined_iff [simp]: "(ssnd\<cdot>p = \<bottom>) = (p = \<bottom>)"
    2.12  by (rule_tac p=p in sprodE, simp_all)
    2.13  
    2.14 +lemma sfst_defined: "p \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>p \<noteq> \<bottom>"
    2.15 +by simp
    2.16 +
    2.17 +lemma ssnd_defined: "p \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>p \<noteq> \<bottom>"
    2.18 +by simp
    2.19 +
    2.20  lemma surjective_pairing_Sprod2: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p"
    2.21  by (rule_tac p=p in sprodE, simp_all)
    2.22