# HG changeset patch
# User oheimb
# Date 991320674 -7200
# Node ID 442b9bc808a5468df80e2f4d77673da04f1a03f7
# Parent  100edbd42dba5df99522a7ff378077f5cb3e25fb
added lub_range_mono and lub_range_shift

diff -r 100edbd42dba -r 442b9bc808a5 src/HOLCF/Pcpo.ML
--- a/src/HOLCF/Pcpo.ML	Thu May 31 16:50:17 2001 +0200
+++ b/src/HOLCF/Pcpo.ML	Thu May 31 16:51:14 2001 +0200
@@ -41,6 +41,30 @@
 by (blast_tac (claset() addDs [cpo] addIs [lubI RS is_lub_lub]) 1);
 qed "is_lub_thelub";
 
+Goal "[| range X <= range Y;  chain Y; chain (X::nat=>'a::cpo) |] ==> lub(range X) << lub(range Y)";
+by (etac is_lub_thelub 1);
+by (rtac ub_rangeI 1);
+by (subgoal_tac "? j. X i = Y j" 1);
+by  (Clarsimp_tac 1);
+by  (etac is_ub_thelub 1);
+by Auto_tac;
+qed "lub_range_mono";
+
+Goal "chain (Y::nat=>'a::cpo) ==> lub(range (%i. Y(i + j))) = lub(range Y)";
+by (rtac antisym_less 1);
+br lub_range_mono 1;
+by    (Fast_tac 1);
+by   (atac 1);
+be  chain_shift 1;
+br is_lub_thelub 1;
+ba  1;
+br ub_rangeI 1;
+br trans_less 1;
+br  is_ub_thelub 2;
+be  chain_shift 2;
+be chain_mono3 1;
+br le_add1 1;
+qed "lub_range_shift";
 
 Goal "chain Y ==> max_in_chain i Y = (lub(range(Y)) = ((Y i)::'a::cpo))";
 by (rtac iffI 1);