[STATEMENT]
lemma ccpo_Sup_mono:
  assumes C: "Complete_Partial_Order.chain (\<le>) A"
    "Complete_Partial_Order.chain (\<le>) B"
  assumes B: "\<forall>x\<in>A. \<exists>y\<in>B. x\<le>y"
  shows "Sup A \<le> Sup B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup A \<le> Sup B
[PROOF STEP]
proof (rule ccpo_Sup_least)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Complete_Partial_Order.chain (\<le>) A
 2. \<And>x. x \<in> A \<Longrightarrow> x \<le> Sup B
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Complete_Partial_Order.chain (\<le>) A
 2. \<And>x. x \<in> A \<Longrightarrow> x \<le> Sup B
[PROOF STEP]
assume "x\<in>A"
[PROOF STATE]
proof (state)
this:
x \<in> A

goal (2 subgoals):
 1. Complete_Partial_Order.chain (\<le>) A
 2. \<And>x. x \<in> A \<Longrightarrow> x \<le> Sup B
[PROOF STEP]
with B
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>A. \<exists>y\<in>B. x \<le> y
x \<in> A
[PROOF STEP]
obtain y where I: "y\<in>B" and L: "x\<le>y"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. \<exists>y\<in>B. x \<le> y
x \<in> A

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> B; x \<le> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<in> B
x \<le> y

goal (2 subgoals):
 1. Complete_Partial_Order.chain (\<le>) A
 2. \<And>x. x \<in> A \<Longrightarrow> x \<le> Sup B
[PROOF STEP]
note L
[PROOF STATE]
proof (state)
this:
x \<le> y

goal (2 subgoals):
 1. Complete_Partial_Order.chain (\<le>) A
 2. \<And>x. x \<in> A \<Longrightarrow> x \<le> Sup B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<le> y

goal (2 subgoals):
 1. Complete_Partial_Order.chain (\<le>) A
 2. \<And>x. x \<in> A \<Longrightarrow> x \<le> Sup B
[PROOF STEP]
from I ccpo_Sup_upper
[PROOF STATE]
proof (chain)
picking this:
y \<in> B
\<lbrakk>Complete_Partial_Order.chain (\<le>) ?A; ?x \<in> ?A\<rbrakk> \<Longrightarrow> ?x \<le> Sup ?A
[PROOF STEP]
have "y\<le>Sup B"
[PROOF STATE]
proof (prove)
using this:
y \<in> B
\<lbrakk>Complete_Partial_Order.chain (\<le>) ?A; ?x \<in> ?A\<rbrakk> \<Longrightarrow> ?x \<le> Sup ?A

goal (1 subgoal):
 1. y \<le> Sup B
[PROOF STEP]
by (blast intro: C)
[PROOF STATE]
proof (state)
this:
y \<le> Sup B

goal (2 subgoals):
 1. Complete_Partial_Order.chain (\<le>) A
 2. \<And>x. x \<in> A \<Longrightarrow> x \<le> Sup B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x \<le> Sup B
[PROOF STEP]
show "x\<le>Sup B"
[PROOF STATE]
proof (prove)
using this:
x \<le> Sup B

goal (1 subgoal):
 1. x \<le> Sup B
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x \<le> Sup B

goal (1 subgoal):
 1. Complete_Partial_Order.chain (\<le>) A
[PROOF STEP]
qed (rule C)