added lemma cpair_eq, made cfst_strict and csnd_strict into simp rules

--- a/src/HOLCF/Cprod.thy	Tue May 24 05:03:54 2005 +0200
+++ b/src/HOLCF/Cprod.thy	Tue May 24 05:32:19 2005 +0200
@@ -280,6 +280,9 @@
         "<a,b> = <aa,ba>  ==> a=aa & b=ba"
 by (simp add: cpair_def beta_cfun_cprod)
 
+lemma cpair_eq [iff]: "(<a, b> = <a', b'>) = (a = a' & b = b')"
+by (blast dest!: inject_cpair)
+
 lemma inst_cprod_pcpo2: "UU = <UU,UU>"
 by (simp add: cpair_def beta_cfun_cprod inst_cprod_pcpo)
 
@@ -311,10 +314,10 @@
 lemma csnd2 [simp]: "csnd$<x,y> = y"
 by (simp add: cpair_def csnd_def beta_cfun_cprod cont_snd)
 
-lemma cfst_strict: "cfst$UU = UU"
+lemma cfst_strict [simp]: "cfst$UU = UU"
 by (simp add: inst_cprod_pcpo2)
 
-lemma csnd_strict: "csnd$UU = UU"
+lemma csnd_strict [simp]: "csnd$UU = UU"
 by (simp add: inst_cprod_pcpo2)
 
 lemma surjective_pairing_Cprod2: "<cfst$p, csnd$p> = p"