# HG changeset patch
# User huffman
# Date 1118185186 -7200
# Node ID 45b12a01382fef1e4c9babdfae986922b5938aea
# Parent  868eddbcaf6e5cc2fca78551b542c67dcd16728f
added theorems is_ub_range_shift and is_lub_range_shift

diff -r 868eddbcaf6e -r 45b12a01382f src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Wed Jun 08 00:18:26 2005 +0200
+++ b/src/HOLCF/Porder.thy	Wed Jun 08 00:59:46 2005 +0200
@@ -174,7 +174,7 @@
 
 lemma chain_shift: "chain Y ==> chain (%i. Y (i + j))"
 apply (rule chainI)
-apply clarsimp
+apply simp
 apply (erule chainE)
 done
 
@@ -193,6 +193,22 @@
 lemmas is_ub_lub = is_lubD1 [THEN ub_rangeD, standard]
   -- {* @{thm is_ub_lub} *} (* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1 *)
 
+lemma is_ub_range_shift:
+  "chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <| x = range S <| x"
+apply (rule iffI)
+apply (rule ub_rangeI)
+apply (rule_tac y="S (i + j)" in trans_less)
+apply (erule chain_mono3)
+apply (rule le_add1)
+apply (erule ub_rangeD)
+apply (rule ub_rangeI)
+apply (erule ub_rangeD)
+done
+
+lemma is_lub_range_shift:
+  "chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <<| x = range S <<| x"
+by (simp add: is_lub_def is_ub_range_shift)
+
 text {* results about finite chains *}
 
 lemma lub_finch1: