--- a/src/HOLCF/Cprod.thy Thu Jan 31 22:00:31 2008 +0100
+++ b/src/HOLCF/Cprod.thy Fri Feb 01 02:38:41 2008 +0100
@@ -72,17 +72,23 @@
subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
+lemma prod_lessI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"
+unfolding less_cprod_def by simp
+
+lemma Pair_less_iff [simp]: "(a, b) \<sqsubseteq> (c, d) = (a \<sqsubseteq> c \<and> b \<sqsubseteq> d)"
+unfolding less_cprod_def by simp
+
text {* Pair @{text "(_,_)"} is monotone in both arguments *}
lemma monofun_pair1: "monofun (\<lambda>x. (x, y))"
-by (simp add: monofun_def less_cprod_def)
+by (simp add: monofun_def)
lemma monofun_pair2: "monofun (\<lambda>y. (x, y))"
-by (simp add: monofun_def less_cprod_def)
+by (simp add: monofun_def)
lemma monofun_pair:
"\<lbrakk>x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2\<rbrakk> \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)"
-by (simp add: less_cprod_def)
+by simp
text {* @{term fst} and @{term snd} are monotone *}
--- a/src/HOLCF/FOCUS/Fstreams.thy Thu Jan 31 22:00:31 2008 +0100
+++ b/src/HOLCF/FOCUS/Fstreams.thy Fri Feb 01 02:38:41 2008 +0100
@@ -291,7 +291,6 @@
"[| chain Y; lub (range Y) = (a, <m> ooo ms); (a::'a::flat) ~= UU |] ==> EX j t. Y j = (a, <m> ooo t)"
apply (frule lub_Pair_not_UU_lemma, auto)
apply (drule_tac x="j" in is_ub_thelub, auto)
-apply (simp add: less_cprod_def, clarsimp)
apply (drule ax_flat, clarsimp)
by (drule fstreams_prefix' [THEN iffD1], auto)
@@ -304,12 +303,11 @@
apply (induct_tac i, auto)
apply (drule fstreams_lub_lemma2, auto)
apply (rule_tac x="j" in exI, auto)
-apply (simp add: less_cprod_def)
apply (case_tac "max_in_chain j Y")
apply (frule lub_finch1 [THEN thelubI], auto)
apply (rule_tac x="j" in exI)
apply (erule subst) back back
-apply (simp add: less_cprod_def sconc_mono)
+apply (simp add: sconc_mono)
apply (simp add: max_in_chain_def, auto)
apply (rule_tac x="ja" in exI)
apply (subgoal_tac "Y j << Y ja")