# 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\f\\ \ fix\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