# HG changeset patch
# User huffman
# Date 1201829921 -3600
# Node ID 46e84ca065f1490e6467001c8ce005189e302502
# Parent  74668c3a8f70cf9eeca8b56b9a3efd4be4867fb8
add lemmas prod_lessI and Pair_less_iff [simp]

diff -r 74668c3a8f70 -r 46e84ca065f1 src/HOLCF/Cprod.thy
--- 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 *}
 
diff -r 74668c3a8f70 -r 46e84ca065f1 src/HOLCF/FOCUS/Fstreams.thy
--- 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")