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.5  by(auto simp add: chain_def)
     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"