src/HOL/Complete_Partial_Order.thy
 changeset 60061 279472fa0b1d parent 60057 86fa63ce8156 child 60758 d8d85a8172b5
```     1.1 --- a/src/HOL/Complete_Partial_Order.thy	Tue Apr 14 11:44:17 2015 +0200
1.2 +++ b/src/HOL/Complete_Partial_Order.thy	Tue Apr 14 13:56:34 2015 +0200
1.3 @@ -56,6 +56,17 @@
1.4  lemma chain_equality: "chain op = A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. x = y)"
1.6
1.7 +lemma chain_subset:
1.8 +  "\<lbrakk> chain ord A; B \<subseteq> A \<rbrakk>
1.9 +  \<Longrightarrow> chain ord B"
1.10 +by(rule chainI)(blast dest: chainD)
1.11 +
1.12 +lemma chain_imageI:
1.13 +  assumes chain: "chain le_a Y"
1.14 +  and mono: "\<And>x y. \<lbrakk> x \<in> Y; y \<in> Y; le_a x y \<rbrakk> \<Longrightarrow> le_b (f x) (f y)"
1.15 +  shows "chain le_b (f ` Y)"
1.16 +by(blast intro: chainI dest: chainD[OF chain] mono)
1.17 +
1.18  subsection {* Chain-complete partial orders *}
1.19
1.20  text {*
1.21 @@ -68,6 +79,12 @@
1.22    assumes ccpo_Sup_least: "\<lbrakk>chain (op \<le>) A; \<And>x. x \<in> A \<Longrightarrow> x \<le> z\<rbrakk> \<Longrightarrow> Sup A \<le> z"
1.23  begin
1.24
1.25 +lemma chain_singleton: "Complete_Partial_Order.chain op \<le> {x}"
1.26 +by(rule chainI) simp
1.27 +
1.28 +lemma ccpo_Sup_singleton [simp]: "\<Squnion>{x} = x"
1.29 +by(rule antisym)(auto intro: ccpo_Sup_least ccpo_Sup_upper simp add: chain_singleton)
1.30 +
1.31  subsection {* Transfinite iteration of a function *}
1.32
1.33  inductive_set iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set"
```