added lemma cpair_eq, made cfst_strict and csnd_strict into simp rules
authorhuffman
Tue May 24 05:32:19 2005 +0200 (2005-05-24)
changeset 16057e23a61b3406f
parent 16056 32c3b7188c28
child 16058 3d50b521ab16
added lemma cpair_eq, made cfst_strict and csnd_strict into simp rules
src/HOLCF/Cprod.thy
     1.1 --- a/src/HOLCF/Cprod.thy	Tue May 24 05:03:54 2005 +0200
     1.2 +++ b/src/HOLCF/Cprod.thy	Tue May 24 05:32:19 2005 +0200
     1.3 @@ -280,6 +280,9 @@
     1.4          "<a,b> = <aa,ba>  ==> a=aa & b=ba"
     1.5  by (simp add: cpair_def beta_cfun_cprod)
     1.6  
     1.7 +lemma cpair_eq [iff]: "(<a, b> = <a', b'>) = (a = a' & b = b')"
     1.8 +by (blast dest!: inject_cpair)
     1.9 +
    1.10  lemma inst_cprod_pcpo2: "UU = <UU,UU>"
    1.11  by (simp add: cpair_def beta_cfun_cprod inst_cprod_pcpo)
    1.12  
    1.13 @@ -311,10 +314,10 @@
    1.14  lemma csnd2 [simp]: "csnd$<x,y> = y"
    1.15  by (simp add: cpair_def csnd_def beta_cfun_cprod cont_snd)
    1.16  
    1.17 -lemma cfst_strict: "cfst$UU = UU"
    1.18 +lemma cfst_strict [simp]: "cfst$UU = UU"
    1.19  by (simp add: inst_cprod_pcpo2)
    1.20  
    1.21 -lemma csnd_strict: "csnd$UU = UU"
    1.22 +lemma csnd_strict [simp]: "csnd$UU = UU"
    1.23  by (simp add: inst_cprod_pcpo2)
    1.24  
    1.25  lemma surjective_pairing_Cprod2: "<cfst$p, csnd$p> = p"