# HG changeset patch
# User huffman
# Date 1269322901 25200
# Node ID 676c6005ad03f3a8b8314ee1c1dd667eeac28cd9
# Parent  68397d86d45438c9bb53d9d9155cfb0352f434d8
add lemmas fst_monofun, snd_monofun

diff -r 68397d86d454 -r 676c6005ad03 src/HOLCF/Product_Cpo.thy
--- a/src/HOLCF/Product_Cpo.thy	Mon Mar 22 21:37:48 2010 -0700
+++ b/src/HOLCF/Product_Cpo.thy	Mon Mar 22 22:41:41 2010 -0700
@@ -84,6 +84,12 @@
 
 text {* @{term fst} and @{term snd} are monotone *}
 
+lemma fst_monofun: "x \<sqsubseteq> y \<Longrightarrow> fst x \<sqsubseteq> fst y"
+unfolding below_prod_def by simp
+
+lemma snd_monofun: "x \<sqsubseteq> y \<Longrightarrow> snd x \<sqsubseteq> snd y"
+unfolding below_prod_def by simp
+
 lemma monofun_fst: "monofun fst"
 by (simp add: monofun_def below_prod_def)