# HG changeset patch
# User huffman
# Date 1116905539 -7200
# Node ID e23a61b3406f81174c3ec88f68fd9364540046ca
# Parent  32c3b7188c287ecdaf90feed76011c7d4423c935
added lemma cpair_eq, made cfst_strict and csnd_strict into simp rules

diff -r 32c3b7188c28 -r e23a61b3406f src/HOLCF/Cprod.thy
--- 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"