# 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 \ y \ fst x \ fst y" +unfolding below_prod_def by simp + +lemma snd_monofun: "x \ y \ snd x \ snd y" +unfolding below_prod_def by simp + lemma monofun_fst: "monofun fst" by (simp add: monofun_def below_prod_def)