src/HOLCF/Porder.thy
changeset 16318 45b12a01382f
parent 16092 a1a481ee9425
child 17372 d73f67e90a95
equal deleted inserted replaced
16317:868eddbcaf6e 16318:45b12a01382f
   172 apply blast
   172 apply blast
   173 done
   173 done
   174 
   174 
   175 lemma chain_shift: "chain Y ==> chain (%i. Y (i + j))"
   175 lemma chain_shift: "chain Y ==> chain (%i. Y (i + j))"
   176 apply (rule chainI)
   176 apply (rule chainI)
   177 apply clarsimp
   177 apply simp
   178 apply (erule chainE)
   178 apply (erule chainE)
   179 done
   179 done
   180 
   180 
   181 text {* technical lemmas about (least) upper bounds of chains *}
   181 text {* technical lemmas about (least) upper bounds of chains *}
   182 
   182 
   190 apply blast
   190 apply blast
   191 done
   191 done
   192 
   192 
   193 lemmas is_ub_lub = is_lubD1 [THEN ub_rangeD, standard]
   193 lemmas is_ub_lub = is_lubD1 [THEN ub_rangeD, standard]
   194   -- {* @{thm is_ub_lub} *} (* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1 *)
   194   -- {* @{thm is_ub_lub} *} (* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1 *)
       
   195 
       
   196 lemma is_ub_range_shift:
       
   197   "chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <| x = range S <| x"
       
   198 apply (rule iffI)
       
   199 apply (rule ub_rangeI)
       
   200 apply (rule_tac y="S (i + j)" in trans_less)
       
   201 apply (erule chain_mono3)
       
   202 apply (rule le_add1)
       
   203 apply (erule ub_rangeD)
       
   204 apply (rule ub_rangeI)
       
   205 apply (erule ub_rangeD)
       
   206 done
       
   207 
       
   208 lemma is_lub_range_shift:
       
   209   "chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <<| x = range S <<| x"
       
   210 by (simp add: is_lub_def is_ub_range_shift)
   195 
   211 
   196 text {* results about finite chains *}
   212 text {* results about finite chains *}
   197 
   213 
   198 lemma lub_finch1: 
   214 lemma lub_finch1: 
   199         "[| chain C; max_in_chain i C|] ==> range C <<| C i"
   215         "[| chain C; max_in_chain i C|] ==> range C <<| C i"