# HG changeset patch
# User huffman
# Date 1258655117 28800
# Node ID d280c5ebd7d7a3dc4222460b7d9540fa546ad434
# Parent  2f2d9eb37084097091049630a2c619feacda0965
add lemma isodefl_cprod

diff -r 2f2d9eb37084 -r d280c5ebd7d7 src/HOLCF/Representable.thy
--- a/src/HOLCF/Representable.thy	Thu Nov 19 09:04:58 2009 -0800
+++ b/src/HOLCF/Representable.thy	Thu Nov 19 10:25:17 2009 -0800
@@ -988,6 +988,15 @@
 apply (simp add: sprod_map_map isodefl_strict)
 done
 
+lemma isodefl_cprod:
+  "isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
+    isodefl (cprod_map\<cdot>d1\<cdot>d2) (cprod_defl\<cdot>t1\<cdot>t2)"
+apply (rule isodeflI)
+apply (simp add: cast_cprod_defl cast_isodefl)
+apply (simp add: emb_cprod_def prj_cprod_def)
+apply (simp add: cprod_map_map cfcomp1)
+done
+
 lemma isodefl_u:
   "isodefl d t \<Longrightarrow> isodefl (u_map\<cdot>d) (u_defl\<cdot>t)"
 apply (rule isodeflI)