author Andreas Lochbihler Tue, 14 Apr 2015 13:56:34 +0200 changeset 60061 279472fa0b1d parent 60060 3630ecde4e7c child 60062 4c5de5a860ee
move some lemmas from AFP/Coinductive
```--- 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"```