src/HOLCF/Cprod.thy
changeset 26029 46e84ca065f1
parent 26027 87cb69d27558
child 26035 9f8810c42604
     1.1 --- a/src/HOLCF/Cprod.thy	Thu Jan 31 22:00:31 2008 +0100
     1.2 +++ b/src/HOLCF/Cprod.thy	Fri Feb 01 02:38:41 2008 +0100
     1.3 @@ -72,17 +72,23 @@
     1.4  
     1.5  subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
     1.6  
     1.7 +lemma prod_lessI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"
     1.8 +unfolding less_cprod_def by simp
     1.9 +
    1.10 +lemma Pair_less_iff [simp]: "(a, b) \<sqsubseteq> (c, d) = (a \<sqsubseteq> c \<and> b \<sqsubseteq> d)"
    1.11 +unfolding less_cprod_def by simp
    1.12 +
    1.13  text {* Pair @{text "(_,_)"}  is monotone in both arguments *}
    1.14  
    1.15  lemma monofun_pair1: "monofun (\<lambda>x. (x, y))"
    1.16 -by (simp add: monofun_def less_cprod_def)
    1.17 +by (simp add: monofun_def)
    1.18  
    1.19  lemma monofun_pair2: "monofun (\<lambda>y. (x, y))"
    1.20 -by (simp add: monofun_def less_cprod_def)
    1.21 +by (simp add: monofun_def)
    1.22  
    1.23  lemma monofun_pair:
    1.24    "\<lbrakk>x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2\<rbrakk> \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)"
    1.25 -by (simp add: less_cprod_def)
    1.26 +by simp
    1.27  
    1.28  text {* @{term fst} and @{term snd} are monotone *}
    1.29