--- 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);