[STATEMENT]
lemma (in ccpo) mcont_if_bot:
  fixes bot and lub ("\<Or>") and ord (infix "\<sqsubseteq>" 60)
  assumes ccpo: "class.ccpo lub (\<sqsubseteq>) lt"
  and mono: "\<And>x y. \<lbrakk> x \<le> y; \<not> x \<le> bound \<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
  and cont: "\<And>Y. \<lbrakk> Complete_Partial_Order.chain (\<le>) Y; Y \<noteq> {}; \<And>x. x \<in> Y \<Longrightarrow> \<not> x \<le> bound \<rbrakk> \<Longrightarrow> f (\<Squnion>Y) = \<Or>(f ` Y)"
  and bot: "\<And>x. \<not> x \<le> bound \<Longrightarrow> bot \<sqsubseteq> f x"
  shows "mcont Sup (\<le>) lub (\<sqsubseteq>) (\<lambda>x. if x \<le> bound then bot else f x)" (is "mcont _ _ _ _ ?g")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mcont Sup (\<le>) \<Or> (\<sqsubseteq>) (\<lambda>x. if x \<le> bound then bot else f x)
[PROOF STEP]
proof(intro mcontI contI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. monotone (\<le>) (\<sqsubseteq>) (\<lambda>x. if x \<le> bound then bot else f x)
 2. \<And>Y. \<lbrakk>Complete_Partial_Order.chain (\<le>) Y; Y \<noteq> {}\<rbrakk> \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
interpret c: ccpo lub "(\<sqsubseteq>)" lt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.ccpo \<Or> (\<sqsubseteq>) lt
[PROOF STEP]
by(fact ccpo)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. monotone (\<le>) (\<sqsubseteq>) (\<lambda>x. if x \<le> bound then bot else f x)
 2. \<And>Y. \<lbrakk>Complete_Partial_Order.chain (\<le>) Y; Y \<noteq> {}\<rbrakk> \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
show "monotone (\<le>) (\<sqsubseteq>) ?g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone (\<le>) (\<sqsubseteq>) (\<lambda>x. if x \<le> bound then bot else f x)
[PROOF STEP]
by(rule monotone_if_bot)(simp_all add: mono bot)
[PROOF STATE]
proof (state)
this:
monotone (\<le>) (\<sqsubseteq>) (\<lambda>x. if x \<le> bound then bot else f x)

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>Complete_Partial_Order.chain (\<le>) Y; Y \<noteq> {}\<rbrakk> \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
fix Y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Y. \<lbrakk>Complete_Partial_Order.chain (\<le>) Y; Y \<noteq> {}\<rbrakk> \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
assume chain: "Complete_Partial_Order.chain (\<le>) Y" and Y: "Y \<noteq> {}"
[PROOF STATE]
proof (state)
this:
Complete_Partial_Order.chain (\<le>) Y
Y \<noteq> {}

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>Complete_Partial_Order.chain (\<le>) Y; Y \<noteq> {}\<rbrakk> \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
show "?g (\<Squnion>Y) = \<Or>(?g ` Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
proof(cases "Y \<subseteq> {x. x \<le> bound}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
 2. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Y \<subseteq> {x. x \<le> bound}

goal (2 subgoals):
 1. Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
 2. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
hence "\<Squnion>Y \<le> bound"
[PROOF STATE]
proof (prove)
using this:
Y \<subseteq> {x. x \<le> bound}

goal (1 subgoal):
 1. \<Squnion> Y \<le> bound
[PROOF STEP]
using chain
[PROOF STATE]
proof (prove)
using this:
Y \<subseteq> {x. x \<le> bound}
Complete_Partial_Order.chain (\<le>) Y

goal (1 subgoal):
 1. \<Squnion> Y \<le> bound
[PROOF STEP]
by(auto intro: ccpo_Sup_least)
[PROOF STATE]
proof (state)
this:
\<Squnion> Y \<le> bound

goal (2 subgoals):
 1. Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
 2. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Squnion> Y \<le> bound

goal (2 subgoals):
 1. Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
 2. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
have "Y \<inter> {x. \<not> x \<le> bound} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y \<inter> {x. \<not> x \<le> bound} = {}
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
Y \<subseteq> {x. x \<le> bound}

goal (1 subgoal):
 1. Y \<inter> {x. \<not> x \<le> bound} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Y \<inter> {x. \<not> x \<le> bound} = {}

goal (2 subgoals):
 1. Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
 2. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Squnion> Y \<le> bound
Y \<inter> {x. \<not> x \<le> bound} = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Squnion> Y \<le> bound
Y \<inter> {x. \<not> x \<le> bound} = {}

goal (1 subgoal):
 1. (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
using True Y
[PROOF STATE]
proof (prove)
using this:
\<Squnion> Y \<le> bound
Y \<inter> {x. \<not> x \<le> bound} = {}
Y \<subseteq> {x. x \<le> bound}
Y \<noteq> {}

goal (1 subgoal):
 1. (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
by (auto simp add: image_constant_conv cong del: c.SUP_cong_simp)
[PROOF STATE]
proof (state)
this:
(if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> Y \<subseteq> {x. x \<le> bound}

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
let ?Y = "Y \<inter> {x. \<not> x \<le> bound}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
have chain': "Complete_Partial_Order.chain (\<le>) ?Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complete_Partial_Order.chain (\<le>) (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
using chain
[PROOF STATE]
proof (prove)
using this:
Complete_Partial_Order.chain (\<le>) Y

goal (1 subgoal):
 1. Complete_Partial_Order.chain (\<le>) (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
by(rule chain_subset) simp
[PROOF STATE]
proof (state)
this:
Complete_Partial_Order.chain (\<le>) (Y \<inter> {x. \<not> x \<le> bound})

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
\<not> Y \<subseteq> {x. x \<le> bound}
[PROOF STEP]
obtain y where ybound: "\<not> y \<le> bound" and y: "y \<in> Y"
[PROOF STATE]
proof (prove)
using this:
\<not> Y \<subseteq> {x. x \<le> bound}

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

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
hence "\<not> \<Squnion>Y \<le> bound"
[PROOF STATE]
proof (prove)
using this:
\<not> y \<le> bound
y \<in> Y

goal (1 subgoal):
 1. \<not> \<Squnion> Y \<le> bound
[PROOF STEP]
by (metis ccpo_Sup_upper chain order.trans)
[PROOF STATE]
proof (state)
this:
\<not> \<Squnion> Y \<le> bound

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
hence "?g (\<Squnion>Y) = f (\<Squnion>Y)"
[PROOF STATE]
proof (prove)
using this:
\<not> \<Squnion> Y \<le> bound

goal (1 subgoal):
 1. (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = f (\<Squnion> Y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = f (\<Squnion> Y)

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = f (\<Squnion> Y)

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
have "\<Squnion>Y \<le> \<Squnion>?Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion> Y \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
using chain
[PROOF STATE]
proof (prove)
using this:
Complete_Partial_Order.chain (\<le>) Y

goal (1 subgoal):
 1. \<Squnion> Y \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
proof(rule ccpo_Sup_least)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Y \<Longrightarrow> x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Y \<Longrightarrow> x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
assume x: "x \<in> Y"
[PROOF STATE]
proof (state)
this:
x \<in> Y

goal (1 subgoal):
 1. \<And>x. x \<in> Y \<Longrightarrow> x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
show "x \<le> \<Squnion>?Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
proof(cases "x \<le> bound")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<le> bound \<Longrightarrow> x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
 2. \<not> x \<le> bound \<Longrightarrow> x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x \<le> bound

goal (2 subgoals):
 1. x \<le> bound \<Longrightarrow> x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
 2. \<not> x \<le> bound \<Longrightarrow> x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
with chainD[OF chain x y]
[PROOF STATE]
proof (chain)
picking this:
x \<le> y \<or> y \<le> x
x \<le> bound
[PROOF STEP]
have "x \<le> y"
[PROOF STATE]
proof (prove)
using this:
x \<le> y \<or> y \<le> x
x \<le> bound

goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
using ybound
[PROOF STATE]
proof (prove)
using this:
x \<le> y \<or> y \<le> x
x \<le> bound
\<not> y \<le> bound

goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
by(auto intro: order_trans)
[PROOF STATE]
proof (state)
this:
x \<le> y

goal (2 subgoals):
 1. x \<le> bound \<Longrightarrow> x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
 2. \<not> x \<le> bound \<Longrightarrow> x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<le> y

goal (1 subgoal):
 1. x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
by(rule order_trans)(auto intro: ccpo_Sup_upper[OF chain'] simp add: y ybound)
[PROOF STATE]
proof (state)
this:
x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})

goal (1 subgoal):
 1. \<not> x \<le> bound \<Longrightarrow> x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
qed(auto intro: ccpo_Sup_upper[OF chain'] simp add: x)
[PROOF STATE]
proof (state)
this:
x \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Squnion> Y \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
hence "\<Squnion>Y = \<Squnion>?Y"
[PROOF STATE]
proof (prove)
using this:
\<Squnion> Y \<le> \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})

goal (1 subgoal):
 1. \<Squnion> Y = \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})
[PROOF STEP]
by(rule order.antisym)(blast intro: ccpo_Sup_least[OF chain'] ccpo_Sup_upper[OF chain])
[PROOF STATE]
proof (state)
this:
\<Squnion> Y = \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
hence "f (\<Squnion>Y) = f (\<Squnion>?Y)"
[PROOF STATE]
proof (prove)
using this:
\<Squnion> Y = \<Squnion> (Y \<inter> {x. \<not> x \<le> bound})

goal (1 subgoal):
 1. f (\<Squnion> Y) = f (\<Squnion> (Y \<inter> {x. \<not> x \<le> bound}))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (\<Squnion> Y) = f (\<Squnion> (Y \<inter> {x. \<not> x \<le> bound}))

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f (\<Squnion> Y) = f (\<Squnion> (Y \<inter> {x. \<not> x \<le> bound}))

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
have "f (\<Squnion>?Y) = \<Or>(f ` ?Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (\<Squnion> (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))
[PROOF STEP]
using chain'
[PROOF STATE]
proof (prove)
using this:
Complete_Partial_Order.chain (\<le>) (Y \<inter> {x. \<not> x \<le> bound})

goal (1 subgoal):
 1. f (\<Squnion> (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))
[PROOF STEP]
by(rule cont)(insert y ybound, auto)
[PROOF STATE]
proof (state)
this:
f (\<Squnion> (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f (\<Squnion> (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
have "\<Or>(f ` ?Y) = \<Or>(?g ` Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
proof(cases "Y \<inter> {x. x \<le> bound} = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Y \<inter> {x. x \<le> bound} = {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
 2. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Y \<inter> {x. x \<le> bound} = {}

goal (2 subgoals):
 1. Y \<inter> {x. x \<le> bound} = {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
 2. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
hence "f ` ?Y = ?g ` Y"
[PROOF STATE]
proof (prove)
using this:
Y \<inter> {x. x \<le> bound} = {}

goal (1 subgoal):
 1. f ` (Y \<inter> {x. \<not> x \<le> bound}) = (\<lambda>x. if x \<le> bound then bot else f x) ` Y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f ` (Y \<inter> {x. \<not> x \<le> bound}) = (\<lambda>x. if x \<le> bound then bot else f x) ` Y

goal (2 subgoals):
 1. Y \<inter> {x. x \<le> bound} = {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
 2. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f ` (Y \<inter> {x. \<not> x \<le> bound}) = (\<lambda>x. if x \<le> bound then bot else f x) ` Y

goal (1 subgoal):
 1. \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
by(rule arg_cong)
[PROOF STATE]
proof (state)
this:
\<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)

goal (1 subgoal):
 1. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Y \<inter> {x. x \<le> bound} \<noteq> {}

goal (1 subgoal):
 1. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
have chain'': "Complete_Partial_Order.chain (\<sqsubseteq>) (insert bot (f ` ?Y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complete_Partial_Order.chain (\<sqsubseteq>) (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound})))
[PROOF STEP]
using chain
[PROOF STATE]
proof (prove)
using this:
Complete_Partial_Order.chain (\<le>) Y

goal (1 subgoal):
 1. Complete_Partial_Order.chain (\<sqsubseteq>) (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound})))
[PROOF STEP]
by(auto intro!: chainI bot dest: chainD intro: mono)
[PROOF STATE]
proof (state)
this:
Complete_Partial_Order.chain (\<sqsubseteq>) (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound})))

goal (1 subgoal):
 1. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
hence chain''': "Complete_Partial_Order.chain (\<sqsubseteq>) (f ` ?Y)"
[PROOF STATE]
proof (prove)
using this:
Complete_Partial_Order.chain (\<sqsubseteq>) (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound})))

goal (1 subgoal):
 1. Complete_Partial_Order.chain (\<sqsubseteq>) (f ` (Y \<inter> {x. \<not> x \<le> bound}))
[PROOF STEP]
by(rule chain_subset) blast
[PROOF STATE]
proof (state)
this:
Complete_Partial_Order.chain (\<sqsubseteq>) (f ` (Y \<inter> {x. \<not> x \<le> bound}))

goal (1 subgoal):
 1. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
have "bot \<sqsubseteq> \<Or>(f ` ?Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bot \<sqsubseteq> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))
[PROOF STEP]
using y ybound
[PROOF STATE]
proof (prove)
using this:
y \<in> Y
\<not> y \<le> bound

goal (1 subgoal):
 1. bot \<sqsubseteq> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))
[PROOF STEP]
by(blast intro: c.order_trans[OF bot] c.ccpo_Sup_upper[OF chain'''])
[PROOF STATE]
proof (state)
this:
bot \<sqsubseteq> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))

goal (1 subgoal):
 1. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
hence "\<Or>(insert bot (f ` ?Y)) \<sqsubseteq> \<Or>(f ` ?Y)"
[PROOF STATE]
proof (prove)
using this:
bot \<sqsubseteq> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))

goal (1 subgoal):
 1. \<Or> (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound}))) \<sqsubseteq> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))
[PROOF STEP]
using chain''
[PROOF STATE]
proof (prove)
using this:
bot \<sqsubseteq> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))
Complete_Partial_Order.chain (\<sqsubseteq>) (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound})))

goal (1 subgoal):
 1. \<Or> (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound}))) \<sqsubseteq> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))
[PROOF STEP]
by(auto intro: c.ccpo_Sup_least c.ccpo_Sup_upper[OF chain'''])
[PROOF STATE]
proof (state)
this:
\<Or> (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound}))) \<sqsubseteq> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))

goal (1 subgoal):
 1. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
with _
[PROOF STATE]
proof (chain)
picking this:
PROP ?psi \<Longrightarrow> PROP ?psi
\<Or> (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound}))) \<sqsubseteq> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))
[PROOF STEP]
have "\<dots> = \<Or>(insert bot (f ` ?Y))"
[PROOF STATE]
proof (prove)
using this:
PROP ?psi \<Longrightarrow> PROP ?psi
\<Or> (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound}))) \<sqsubseteq> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound}))

goal (1 subgoal):
 1. \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound})))
[PROOF STEP]
by(rule c.order.antisym)(blast intro: c.ccpo_Sup_least[OF chain'''] c.ccpo_Sup_upper[OF chain''])
[PROOF STATE]
proof (state)
this:
\<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound})))

goal (1 subgoal):
 1. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> (insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound})))

goal (1 subgoal):
 1. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
have "insert bot (f ` ?Y) = ?g ` Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound})) = (\<lambda>x. if x \<le> bound then bot else f x) ` Y
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
Y \<inter> {x. x \<le> bound} \<noteq> {}

goal (1 subgoal):
 1. insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound})) = (\<lambda>x. if x \<le> bound then bot else f x) ` Y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert bot (f ` (Y \<inter> {x. \<not> x \<le> bound})) = (\<lambda>x. if x \<le> bound then bot else f x) ` Y

goal (1 subgoal):
 1. Y \<inter> {x. x \<le> bound} \<noteq> {} \<Longrightarrow> \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)

goal (1 subgoal):
 1. \<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Or> (f ` (Y \<inter> {x. \<not> x \<le> bound})) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)

goal (1 subgoal):
 1. \<not> Y \<subseteq> {x. x \<le> bound} \<Longrightarrow> (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)

goal (1 subgoal):
 1. (if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(if \<Squnion> Y \<le> bound then bot else f (\<Squnion> Y)) = \<Or> ((\<lambda>x. if x \<le> bound then bot else f x) ` Y)

goal:
No subgoals!
[PROOF STEP]
qed