--- a/src/HOL/Complete_Partial_Order.thy Tue Apr 14 11:44:17 2015 +0200
+++ b/src/HOL/Complete_Partial_Order.thy Tue Apr 14 13:56:34 2015 +0200
@@ -56,6 +56,17 @@
lemma chain_equality: "chain op = A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. x = y)"
by(auto simp add: chain_def)
+lemma chain_subset:
+ "\<lbrakk> chain ord A; B \<subseteq> A \<rbrakk>
+ \<Longrightarrow> chain ord B"
+by(rule chainI)(blast dest: chainD)
+
+lemma chain_imageI:
+ assumes chain: "chain le_a Y"
+ and mono: "\<And>x y. \<lbrakk> x \<in> Y; y \<in> Y; le_a x y \<rbrakk> \<Longrightarrow> le_b (f x) (f y)"
+ shows "chain le_b (f ` Y)"
+by(blast intro: chainI dest: chainD[OF chain] mono)
+
subsection {* Chain-complete partial orders *}
text {*
@@ -68,6 +79,12 @@
assumes ccpo_Sup_least: "\<lbrakk>chain (op \<le>) A; \<And>x. x \<in> A \<Longrightarrow> x \<le> z\<rbrakk> \<Longrightarrow> Sup A \<le> z"
begin
+lemma chain_singleton: "Complete_Partial_Order.chain op \<le> {x}"
+by(rule chainI) simp
+
+lemma ccpo_Sup_singleton [simp]: "\<Squnion>{x} = x"
+by(rule antisym)(auto intro: ccpo_Sup_least ccpo_Sup_upper simp add: chain_singleton)
+
subsection {* Transfinite iteration of a function *}
inductive_set iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set"