src/HOLCF/Porder.thy
changeset 17372 d73f67e90a95
parent 16318 45b12a01382f
child 17810 3bdf516d93d8
equal deleted inserted replaced
17371:923ef4a8c672 17372:d73f67e90a95
   263 apply (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI)
   263 apply (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI)
   264 done
   264 done
   265 
   265 
   266 text {* the lub of a constant chain is the constant *}
   266 text {* the lub of a constant chain is the constant *}
   267 
   267 
       
   268 lemma chain_const: "chain (\<lambda>i. c)"
       
   269 by (simp add: chainI)
       
   270 
   268 lemma lub_const: "range(%x. c) <<| c"
   271 lemma lub_const: "range(%x. c) <<| c"
   269 apply (blast dest: ub_rangeD intro: is_lubI ub_rangeI)
   272 apply (blast dest: ub_rangeD intro: is_lubI ub_rangeI)
   270 done
   273 done
   271 
   274 
   272 lemmas thelub_const = lub_const [THEN thelubI, standard]
   275 lemmas thelub_const = lub_const [THEN thelubI, standard]