# 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 \ range (\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 \ range (\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: