equal
deleted
inserted
replaced
53 lemma monofunE: |
53 lemma monofunE: |
54 "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y" |
54 "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y" |
55 by (simp add: monofun_def) |
55 by (simp add: monofun_def) |
56 |
56 |
57 |
57 |
58 subsection {* @{prop "monofun f \<and> contlub f \<equiv> cont f"} *} |
58 subsection {* Equivalence of alternate definition *} |
59 |
59 |
60 text {* monotone functions map chains to chains *} |
60 text {* monotone functions map chains to chains *} |
61 |
61 |
62 lemma ch2ch_monofun: "\<lbrakk>monofun f; chain Y\<rbrakk> \<Longrightarrow> chain (\<lambda>i. f (Y i))" |
62 lemma ch2ch_monofun: "\<lbrakk>monofun f; chain Y\<rbrakk> \<Longrightarrow> chain (\<lambda>i. f (Y i))" |
63 apply (rule chainI) |
63 apply (rule chainI) |