# HG changeset patch
# User huffman
# Date 1265566515 28800
# Node ID f0ecf952b864083c82df8c0d795e8f4c930d3b70
# Parent  c3e3ac3ca0919ff4041a23a577eeb494deb986ff
add lemma iterate_below_fix

diff -r c3e3ac3ca091 -r f0ecf952b864 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Sat Feb 06 16:32:34 2010 +0100
+++ b/src/HOLCF/Fix.thy	Sun Feb 07 10:15:15 2010 -0800
@@ -73,6 +73,10 @@
 apply simp
 done
 
+lemma iterate_below_fix: "iterate n\<cdot>f\<cdot>\<bottom> \<sqsubseteq> fix\<cdot>f"
+  unfolding fix_def2
+  using chain_iterate by (rule is_ub_thelub)
+
 text {*
   Kleene's fixed point theorems for continuous functions in pointed
   omega cpo's