# HG changeset patch
# User Andreas Lochbihler
# Date 1429012594 -7200
# Node ID 279472fa0b1d6a79e3d0b091eb7cda94893214fb
# Parent  3630ecde4e7c1df296e7b09d836ee71348c8a763
move some lemmas from AFP/Coinductive

diff -r 3630ecde4e7c -r 279472fa0b1d src/HOL/Complete_Partial_Order.thy
--- 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"