[STATEMENT]
lemma cont_pe [cont2cont, simp]: "cont plotkin_exists"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont plotkin_exists
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont plotkin_exists
[PROOF STEP]
proof (rule contI2[OF monofun_pe])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
fix Y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
assume Y: "chain (Y :: nat \<Rightarrow> ValD)"
[PROOF STATE]
proof (state)
this:
chain Y

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
let ?goal = "plotkin_exists (\<Squnion> i. Y i) \<sqsubseteq> (\<Squnion> i. plotkin_exists (Y i))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
have peY: "chain (\<lambda>i. plotkin_exists (Y i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chain (\<lambda>i. plotkin_exists (Y i))
[PROOF STEP]
by (rule chainI, simp add: monofunE[OF monofun_pe] chainE[OF Y])
[PROOF STATE]
proof (state)
this:
chain (\<lambda>i. plotkin_exists (Y i))

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
chain (\<lambda>i. plotkin_exists (Y i))

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
assume "\<exists>i. appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF"
[PROOF STATE]
proof (state)
this:
\<exists>i. appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF
[PROOF STEP]
obtain i where Yi: "appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF

goal (1 subgoal):
 1. (\<And>i. appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
have "Y i \<sqsubseteq> (\<Squnion> i. Y i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y i \<sqsubseteq> (\<Squnion>i. Y i)
[PROOF STEP]
using is_ub_thelub[OF Y, where x=i]
[PROOF STATE]
proof (prove)
using this:
Y i \<sqsubseteq> (\<Squnion>i. Y i)

goal (1 subgoal):
 1. Y i \<sqsubseteq> (\<Squnion>i. Y i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Y i \<sqsubseteq> (\<Squnion>i. Y i)

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Y i \<sqsubseteq> (\<Squnion>i. Y i)
[PROOF STEP]
have "appF\<cdot>(Y i)\<cdot>\<bottom> \<sqsubseteq> appF\<cdot>(\<Squnion> i. Y i)\<cdot>\<bottom>"
[PROOF STATE]
proof (prove)
using this:
Y i \<sqsubseteq> (\<Squnion>i. Y i)

goal (1 subgoal):
 1. appF\<cdot>(Y i)\<cdot>\<bottom> \<sqsubseteq> appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom>
[PROOF STEP]
by (fastforce intro: monofun_cfun)
[PROOF STATE]
proof (state)
this:
appF\<cdot>(Y i)\<cdot>\<bottom> \<sqsubseteq> appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom>

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
with Yi
[PROOF STATE]
proof (chain)
picking this:
appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF
appF\<cdot>(Y i)\<cdot>\<bottom> \<sqsubseteq> appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom>
[PROOF STEP]
have "ValFF \<sqsubseteq> appF\<cdot>(\<Squnion> i. Y i)\<cdot>\<bottom>"
[PROOF STATE]
proof (prove)
using this:
appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF
appF\<cdot>(Y i)\<cdot>\<bottom> \<sqsubseteq> appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom>

goal (1 subgoal):
 1. ValFF \<sqsubseteq> appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ValFF \<sqsubseteq> appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom>

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ValFF \<sqsubseteq> appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom>
[PROOF STEP]
have "appF\<cdot>(\<Squnion> i. Y i)\<cdot>\<bottom> = ValFF"
[PROOF STATE]
proof (prove)
using this:
ValFF \<sqsubseteq> appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom>

goal (1 subgoal):
 1. appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom> = ValFF
[PROOF STEP]
using ValD.nchotomy[where y="appF\<cdot>(\<Squnion> i. Y i)\<cdot>\<bottom>"]
[PROOF STATE]
proof (prove)
using this:
ValFF \<sqsubseteq> appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom>
appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom> = \<bottom> \<or> (\<exists>cfun. appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom> = ValF\<cdot>cfun) \<or> appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom> = ValTT \<or> appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom> = ValFF \<or> (\<exists>nat. appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom> = ValN\<cdot>nat)

goal (1 subgoal):
 1. appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom> = ValFF
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom> = ValFF

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom> = ValFF

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
from Yi
[PROOF STATE]
proof (chain)
picking this:
appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF
[PROOF STEP]
have "plotkin_exists (Y i) = ValFF"
[PROOF STATE]
proof (prove)
using this:
appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF

goal (1 subgoal):
 1. plotkin_exists (Y i) = ValFF
[PROOF STEP]
by (simp add: plotkin_exists_def)
[PROOF STATE]
proof (state)
this:
plotkin_exists (Y i) = ValFF

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
plotkin_exists (Y i) = ValFF
[PROOF STEP]
have "ValFF \<sqsubseteq> (\<Squnion> i. plotkin_exists (Y i))"
[PROOF STATE]
proof (prove)
using this:
plotkin_exists (Y i) = ValFF

goal (1 subgoal):
 1. ValFF \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
using is_ub_thelub[OF peY, where x=i]
[PROOF STATE]
proof (prove)
using this:
plotkin_exists (Y i) = ValFF
plotkin_exists (Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))

goal (1 subgoal):
 1. ValFF \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ValFF \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ValFF \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
have "ValFF = (\<Squnion> i. plotkin_exists (Y i))"
[PROOF STATE]
proof (prove)
using this:
ValFF \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))

goal (1 subgoal):
 1. ValFF = (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
using ValD.nchotomy[where y="\<Squnion> i. plotkin_exists (Y i)"]
[PROOF STATE]
proof (prove)
using this:
ValFF \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
(\<Squnion>i. plotkin_exists (Y i)) = \<bottom> \<or> (\<exists>cfun. (\<Squnion>i. plotkin_exists (Y i)) = ValF\<cdot>cfun) \<or> (\<Squnion>i. plotkin_exists (Y i)) = ValTT \<or> (\<Squnion>i. plotkin_exists (Y i)) = ValFF \<or> (\<exists>nat. (\<Squnion>i. plotkin_exists (Y i)) = ValN\<cdot>nat)

goal (1 subgoal):
 1. ValFF = (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ValFF = (\<Squnion>i. plotkin_exists (Y i))

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom> = ValFF
ValFF = (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
have ?goal
[PROOF STATE]
proof (prove)
using this:
appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom> = ValFF
ValFF = (\<Squnion>i. plotkin_exists (Y i))

goal (1 subgoal):
 1. plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
by (simp add: plotkin_exists_def)
[PROOF STATE]
proof (state)
this:
plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<exists>i. appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>i. appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<exists>i. appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
assume "\<exists>i j. appF\<cdot>(Y i)\<cdot>j = ValTT"
[PROOF STATE]
proof (state)
this:
\<exists>i j. appF\<cdot>(Y i)\<cdot>j = ValTT

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i j. appF\<cdot>(Y i)\<cdot>j = ValTT
[PROOF STEP]
obtain i j where Yij: "appF\<cdot>(Y i)\<cdot>j = ValTT"
[PROOF STATE]
proof (prove)
using this:
\<exists>i j. appF\<cdot>(Y i)\<cdot>j = ValTT

goal (1 subgoal):
 1. (\<And>i j. appF\<cdot>(Y i)\<cdot>j = ValTT \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
appF\<cdot>(Y i)\<cdot>j = ValTT

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
from Yij
[PROOF STATE]
proof (chain)
picking this:
appF\<cdot>(Y i)\<cdot>j = ValTT
[PROOF STEP]
have Yib: "appF\<cdot>(Y i)\<cdot>\<bottom> \<noteq> ValFF"
[PROOF STATE]
proof (prove)
using this:
appF\<cdot>(Y i)\<cdot>j = ValTT

goal (1 subgoal):
 1. appF\<cdot>(Y i)\<cdot>\<bottom> \<noteq> ValFF
[PROOF STEP]
using monofun_cfun_arg[where f="appF\<cdot>(Y i)" and x="\<bottom>" and y=j]
[PROOF STATE]
proof (prove)
using this:
appF\<cdot>(Y i)\<cdot>j = ValTT
\<bottom> \<sqsubseteq> j \<Longrightarrow> appF\<cdot>(Y i)\<cdot>\<bottom> \<sqsubseteq> appF\<cdot>(Y i)\<cdot>j

goal (1 subgoal):
 1. appF\<cdot>(Y i)\<cdot>\<bottom> \<noteq> ValFF
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
appF\<cdot>(Y i)\<cdot>\<bottom> \<noteq> ValFF

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
appF\<cdot>(Y i)\<cdot>\<bottom> \<noteq> ValFF

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
from Yij
[PROOF STATE]
proof (chain)
picking this:
appF\<cdot>(Y i)\<cdot>j = ValTT
[PROOF STEP]
have "appF\<cdot>(Y i)\<cdot>j \<sqsubseteq> appF\<cdot>(\<Squnion> i. Y i)\<cdot>j"
[PROOF STATE]
proof (prove)
using this:
appF\<cdot>(Y i)\<cdot>j = ValTT

goal (1 subgoal):
 1. appF\<cdot>(Y i)\<cdot>j \<sqsubseteq> appF\<cdot>(\<Squnion>i. Y i)\<cdot>j
[PROOF STEP]
using is_ub_thelub[OF Y, where x=i]
[PROOF STATE]
proof (prove)
using this:
appF\<cdot>(Y i)\<cdot>j = ValTT
Y i \<sqsubseteq> (\<Squnion>i. Y i)

goal (1 subgoal):
 1. appF\<cdot>(Y i)\<cdot>j \<sqsubseteq> appF\<cdot>(\<Squnion>i. Y i)\<cdot>j
[PROOF STEP]
by (fastforce intro: monofun_cfun)
[PROOF STATE]
proof (state)
this:
appF\<cdot>(Y i)\<cdot>j \<sqsubseteq> appF\<cdot>(\<Squnion>i. Y i)\<cdot>j

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
with Yij
[PROOF STATE]
proof (chain)
picking this:
appF\<cdot>(Y i)\<cdot>j = ValTT
appF\<cdot>(Y i)\<cdot>j \<sqsubseteq> appF\<cdot>(\<Squnion>i. Y i)\<cdot>j
[PROOF STEP]
have Yjlub: "appF\<cdot>(\<Squnion> i. Y i)\<cdot>j = ValTT"
[PROOF STATE]
proof (prove)
using this:
appF\<cdot>(Y i)\<cdot>j = ValTT
appF\<cdot>(Y i)\<cdot>j \<sqsubseteq> appF\<cdot>(\<Squnion>i. Y i)\<cdot>j

goal (1 subgoal):
 1. appF\<cdot>(\<Squnion>i. Y i)\<cdot>j = ValTT
[PROOF STEP]
using ValD.nchotomy[where y="appF\<cdot>(\<Squnion> i. Y i)\<cdot>j"]
[PROOF STATE]
proof (prove)
using this:
appF\<cdot>(Y i)\<cdot>j = ValTT
appF\<cdot>(Y i)\<cdot>j \<sqsubseteq> appF\<cdot>(\<Squnion>i. Y i)\<cdot>j
appF\<cdot>(\<Squnion>i. Y i)\<cdot>j = \<bottom> \<or> (\<exists>cfun. appF\<cdot>(\<Squnion>i. Y i)\<cdot>j = ValF\<cdot>cfun) \<or> appF\<cdot>(\<Squnion>i. Y i)\<cdot>j = ValTT \<or> appF\<cdot>(\<Squnion>i. Y i)\<cdot>j = ValFF \<or> (\<exists>nat. appF\<cdot>(\<Squnion>i. Y i)\<cdot>j = ValN\<cdot>nat)

goal (1 subgoal):
 1. appF\<cdot>(\<Squnion>i. Y i)\<cdot>j = ValTT
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
appF\<cdot>(\<Squnion>i. Y i)\<cdot>j = ValTT

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
appF\<cdot>(\<Squnion>i. Y i)\<cdot>j = ValTT

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
from Yjlub
[PROOF STATE]
proof (chain)
picking this:
appF\<cdot>(\<Squnion>i. Y i)\<cdot>j = ValTT
[PROOF STEP]
have "appF\<cdot>(\<Squnion> i. Y i)\<cdot>\<bottom> \<noteq> ValFF"
[PROOF STATE]
proof (prove)
using this:
appF\<cdot>(\<Squnion>i. Y i)\<cdot>j = ValTT

goal (1 subgoal):
 1. appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom> \<noteq> ValFF
[PROOF STEP]
using monofun_cfun_arg[where f="appF\<cdot>(\<Squnion> i. Y i)" and x="\<bottom>" and y=j]
[PROOF STATE]
proof (prove)
using this:
appF\<cdot>(\<Squnion>i. Y i)\<cdot>j = ValTT
\<bottom> \<sqsubseteq> j \<Longrightarrow> appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom> \<sqsubseteq> appF\<cdot>(\<Squnion>i. Y i)\<cdot>j

goal (1 subgoal):
 1. appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom> \<noteq> ValFF
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom> \<noteq> ValFF

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom> \<noteq> ValFF

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
from Yib Yij
[PROOF STATE]
proof (chain)
picking this:
appF\<cdot>(Y i)\<cdot>\<bottom> \<noteq> ValFF
appF\<cdot>(Y i)\<cdot>j = ValTT
[PROOF STEP]
have "plotkin_exists (Y i) = ValTT"
[PROOF STATE]
proof (prove)
using this:
appF\<cdot>(Y i)\<cdot>\<bottom> \<noteq> ValFF
appF\<cdot>(Y i)\<cdot>j = ValTT

goal (1 subgoal):
 1. plotkin_exists (Y i) = ValTT
[PROOF STEP]
by (auto simp add: plotkin_exists_def)
[PROOF STATE]
proof (state)
this:
plotkin_exists (Y i) = ValTT

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
plotkin_exists (Y i) = ValTT
[PROOF STEP]
have "ValTT \<sqsubseteq> (\<Squnion> i. plotkin_exists (Y i))"
[PROOF STATE]
proof (prove)
using this:
plotkin_exists (Y i) = ValTT

goal (1 subgoal):
 1. ValTT \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
using is_ub_thelub[OF peY, where x=i]
[PROOF STATE]
proof (prove)
using this:
plotkin_exists (Y i) = ValTT
plotkin_exists (Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))

goal (1 subgoal):
 1. ValTT \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ValTT \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ValTT \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
have "ValTT = (\<Squnion> i. plotkin_exists (Y i))"
[PROOF STATE]
proof (prove)
using this:
ValTT \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))

goal (1 subgoal):
 1. ValTT = (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
using ValD.nchotomy[where y="\<Squnion> i. plotkin_exists (Y i)"]
[PROOF STATE]
proof (prove)
using this:
ValTT \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
(\<Squnion>i. plotkin_exists (Y i)) = \<bottom> \<or> (\<exists>cfun. (\<Squnion>i. plotkin_exists (Y i)) = ValF\<cdot>cfun) \<or> (\<Squnion>i. plotkin_exists (Y i)) = ValTT \<or> (\<Squnion>i. plotkin_exists (Y i)) = ValFF \<or> (\<exists>nat. (\<Squnion>i. plotkin_exists (Y i)) = ValN\<cdot>nat)

goal (1 subgoal):
 1. ValTT = (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ValTT = (\<Squnion>i. plotkin_exists (Y i))

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
appF\<cdot>(Y i)\<cdot>\<bottom> \<noteq> ValFF
appF\<cdot>(\<Squnion>i. Y i)\<cdot>j = ValTT
appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom> \<noteq> ValFF
ValTT = (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
have ?goal
[PROOF STATE]
proof (prove)
using this:
appF\<cdot>(Y i)\<cdot>\<bottom> \<noteq> ValFF
appF\<cdot>(\<Squnion>i. Y i)\<cdot>j = ValTT
appF\<cdot>(\<Squnion>i. Y i)\<cdot>\<bottom> \<noteq> ValFF
ValTT = (\<Squnion>i. plotkin_exists (Y i))

goal (1 subgoal):
 1. plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
by (simp add: plotkin_exists_def)
[PROOF STATE]
proof (state)
this:
plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<exists>i j. appF\<cdot>(Y i)\<cdot>j = ValTT \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>i j. appF\<cdot>(Y i)\<cdot>j = ValTT \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<exists>i j. appF\<cdot>(Y i)\<cdot>j = ValTT \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
assume nFF: "\<not>(\<exists>i. appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF)" and nTT: "\<not>(\<exists>i j. appF\<cdot>(Y i)\<cdot>j = ValTT)"
[PROOF STATE]
proof (state)
this:
\<nexists>i. appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF
\<nexists>i j. appF\<cdot>(Y i)\<cdot>j = ValTT

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
with Y
[PROOF STATE]
proof (chain)
picking this:
chain Y
\<nexists>i. appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF
\<nexists>i j. appF\<cdot>(Y i)\<cdot>j = ValTT
[PROOF STEP]
have ?goal
[PROOF STATE]
proof (prove)
using this:
chain Y
\<nexists>i. appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF
\<nexists>i j. appF\<cdot>(Y i)\<cdot>j = ValTT

goal (1 subgoal):
 1. plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
unfolding plotkin_exists_def
[PROOF STATE]
proof (prove)
using this:
chain Y
\<nexists>i. appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF
\<nexists>i j. appF\<cdot>(Y i)\<cdot>j = ValTT

goal (1 subgoal):
 1. (if appF\<cdot>(Lub Y)\<cdot>\<bottom> = ValFF then ValFF else if \<exists>n. appF\<cdot>(Lub Y)\<cdot>n = ValTT then ValTT else \<bottom>) \<sqsubseteq> (\<Squnion>i. if appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF then ValFF else if \<exists>n. appF\<cdot>(Y i)\<cdot>n = ValTT then ValTT else \<bottom>)
[PROOF STEP]
using compact_below_lub_iff[OF ValD.compacts(2)]
            compact_below_lub_iff[OF ValD.compacts(3)]
[PROOF STATE]
proof (prove)
using this:
chain Y
\<nexists>i. appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF
\<nexists>i j. appF\<cdot>(Y i)\<cdot>j = ValTT
chain ?Y \<Longrightarrow> (ValTT \<sqsubseteq> (\<Squnion>i. ?Y i)) = (\<exists>i. ValTT \<sqsubseteq> ?Y i)
chain ?Y \<Longrightarrow> (ValFF \<sqsubseteq> (\<Squnion>i. ?Y i)) = (\<exists>i. ValFF \<sqsubseteq> ?Y i)

goal (1 subgoal):
 1. (if appF\<cdot>(Lub Y)\<cdot>\<bottom> = ValFF then ValFF else if \<exists>n. appF\<cdot>(Lub Y)\<cdot>n = ValTT then ValTT else \<bottom>) \<sqsubseteq> (\<Squnion>i. if appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF then ValFF else if \<exists>n. appF\<cdot>(Y i)\<cdot>n = ValTT then ValTT else \<bottom>)
[PROOF STEP]
by (simp add: contlub_cfun_arg contlub_cfun_fun)
[PROOF STATE]
proof (state)
this:
plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<nexists>i. appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF; \<nexists>i j. appF\<cdot>(Y i)\<cdot>j = ValTT\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. plotkin_exists (Y i))\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
\<exists>i j. appF\<cdot>(Y i)\<cdot>j = ValTT \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
\<lbrakk>\<nexists>i. appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF; \<nexists>i j. appF\<cdot>(Y i)\<cdot>j = ValTT\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
show ?goal
[PROOF STATE]
proof (prove)
using this:
\<exists>i. appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
\<exists>i j. appF\<cdot>(Y i)\<cdot>j = ValTT \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
\<lbrakk>\<nexists>i. appF\<cdot>(Y i)\<cdot>\<bottom> = ValFF; \<nexists>i j. appF\<cdot>(Y i)\<cdot>j = ValTT\<rbrakk> \<Longrightarrow> plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))

goal (1 subgoal):
 1. plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
plotkin_exists (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. plotkin_exists (Y i))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cont_pe2[cont2cont, simp]: "cont f \<Longrightarrow> cont (\<lambda>x. plotkin_exists (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont f \<Longrightarrow> cont (\<lambda>x. plotkin_exists (f x))
[PROOF STEP]
by (rule cont_apply) simp_all


[STATEMENT]
theorem pe_sat:
  "appFLv (ValF\<cdot>(\<Lambda> x. plotkin_exists x)) [PE_arg_rel] = PE_result_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. appFLv (ValF\<cdot>(\<Lambda> x. plotkin_exists x)) [PE_arg_rel] = PE_result_rel
[PROOF STEP]
unfolding PE_arg_rel_def PE_result_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. appFLv (ValF\<cdot>(\<Lambda> x. plotkin_exists x)) [\<lambda>i. ValF\<cdot>(case i of 0 \<Rightarrow> \<Lambda> uu_. ValFF | Suc n \<Rightarrow> \<Lambda> (ValN\<cdot>x). if x = Suc n then ValTT else \<bottom>)] = (\<lambda>i. case i of 0 \<Rightarrow> ValFF | Suc n \<Rightarrow> ValTT)
[PROOF STEP]
by (clarsimp simp: fun_eq_iff split: nat.splits)


[STATEMENT]
lemma adm_PE_base_lf_rep:
  "adm (\<lambda>x. x \<in> PE_base_lf_rep r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adm (\<lambda>x. x \<in> PE_base_lf_rep r)
[PROOF STEP]
unfolding PE_base_lf_rep_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adm (\<lambda>x. x \<in> (case r of (mR, pR) \<Rightarrow> {\<bottom>} \<union> {\<lambda>i. ValTT} \<union> {\<lambda>i. ValFF} \<union> (\<Union>n. {\<lambda>i. ValN\<cdot>n}) \<union> {f. f 1 = \<bottom> \<or> f 2 = \<bottom>}))
[PROOF STEP]
using adm_below_monic_exists[OF _ below_monic_fun_K[where f=ValN], where P="\<lambda>_. True"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>adm (\<lambda>_. True); below_monic_cfun ValN; cont (Rep_cfun (\<Lambda> c. (\<lambda>_. ValN\<cdot>c)))\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<exists>y. x = (\<Lambda> c. (\<lambda>_. ValN\<cdot>c))\<cdot>y \<and> True)

goal (1 subgoal):
 1. adm (\<lambda>x. x \<in> (case r of (mR, pR) \<Rightarrow> {\<bottom>} \<union> {\<lambda>i. ValTT} \<union> {\<lambda>i. ValFF} \<union> (\<Union>n. {\<lambda>i. ValN\<cdot>n}) \<union> {f. f 1 = \<bottom> \<or> f 2 = \<bottom>}))
[PROOF STEP]
by (auto intro!: adm_disj simp: cont_fun)


[STATEMENT]
lemma mono_PE_base_lf_rep:
  "mono PE_base_lf_rep"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono PE_base_lf_rep
[PROOF STEP]
unfolding PE_base_lf_rep_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (\<lambda>(mR, pR). {\<bottom>} \<union> {\<lambda>i. ValTT} \<union> {\<lambda>i. ValFF} \<union> (\<Union>n. {\<lambda>i. ValN\<cdot>n}) \<union> {f. f 1 = \<bottom> \<or> f 2 = \<bottom>})
[PROOF STEP]
by (blast intro!: monoI)


[STATEMENT]
lemma admS_PE_lf [intro, simp]:
  "PE_lf_rep r \<in> admS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PE_lf_rep r \<in> admS
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<bottom> \<in> PE_lf_rep r
 2. adm (\<lambda>x. x \<in> PE_lf_rep r)
[PROOF STEP]
show "\<bottom> \<in> PE_lf_rep r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bottom> \<in> PE_lf_rep r
[PROOF STEP]
unfolding PE_lf_rep_def PE_base_lf_rep_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bottom> \<in> (case r of (mR, pR) \<Rightarrow> {\<bottom>} \<union> {\<lambda>i. ValTT} \<union> {\<lambda>i. ValFF} \<union> (\<Union>n. {\<lambda>i. ValN\<cdot>n}) \<union> {f. f 1 = \<bottom> \<or> f 2 = \<bottom>}) \<union> fn_lf_rep r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bottom> \<in> PE_lf_rep r

goal (1 subgoal):
 1. adm (\<lambda>x. x \<in> PE_lf_rep r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. adm (\<lambda>x. x \<in> PE_lf_rep r)
[PROOF STEP]
show "adm (\<lambda>x. x \<in> PE_lf_rep r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adm (\<lambda>x. x \<in> PE_lf_rep r)
[PROOF STEP]
unfolding PE_lf_rep_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adm (\<lambda>x. x \<in> PE_base_lf_rep r \<union> fn_lf_rep r)
[PROOF STEP]
using adm_PE_base_lf_rep[of r] adm_fn[of r]
[PROOF STATE]
proof (prove)
using this:
adm (\<lambda>x. x \<in> PE_base_lf_rep r)
adm (\<lambda>x. x \<in> fn_lf_rep r)

goal (1 subgoal):
 1. adm (\<lambda>x. x \<in> PE_base_lf_rep r \<union> fn_lf_rep r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
adm (\<lambda>x. x \<in> PE_lf_rep r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mono_PE_lf:
  "mono PE_lf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono PE_lf
[PROOF STEP]
apply (rule monoI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. x \<le> y \<Longrightarrow> PE_lf x \<le> PE_lf y
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. x \<le> y \<Longrightarrow> PE_lf_rep x \<subseteq> PE_lf_rep y
[PROOF STEP]
unfolding PE_lf_rep_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. x \<le> y \<Longrightarrow> PE_base_lf_rep x \<union> fn_lf_rep x \<subseteq> PE_base_lf_rep y \<union> fn_lf_rep y
[PROOF STEP]
using mono_fn_lf_rep mono_PE_base_lf_rep
[PROOF STATE]
proof (prove)
using this:
mono fn_lf_rep
mono PE_base_lf_rep

goal (1 subgoal):
 1. \<And>x y. x \<le> y \<Longrightarrow> PE_base_lf_rep x \<union> fn_lf_rep x \<subseteq> PE_base_lf_rep y \<union> fn_lf_rep y
[PROOF STEP]
apply (blast dest: monoD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma min_inv_PE_lf:
  assumes "eRSV e R' S'"
  shows "eRSV (ValD_copy_rec\<cdot>e) (dual (PE_lf (dual S', undual R'))) (PE_lf (R', S'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eRSV (ValD_copy_rec\<cdot>e) (dual (PE_lf (dual S', undual R'))) (PE_lf (R', S'))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>d. d \<in> PE_lf_rep (dual S', undual R') \<Longrightarrow> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> PE_lf_rep (R', S')
[PROOF STEP]
apply (simp add: PE_lf_rep_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>d. d \<in> PE_base_lf_rep (dual S', undual R') \<or> d \<in> fn_lf_rep (dual S', undual R') \<Longrightarrow> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> PE_base_lf_rep (R', S') \<or> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> fn_lf_rep (R', S')
[PROOF STEP]
apply (elim disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>d. d \<in> PE_base_lf_rep (dual S', undual R') \<Longrightarrow> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> PE_base_lf_rep (R', S') \<or> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> fn_lf_rep (R', S')
 2. \<And>d. d \<in> fn_lf_rep (dual S', undual R') \<Longrightarrow> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> PE_base_lf_rep (R', S') \<or> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> fn_lf_rep (R', S')
[PROOF STEP]
apply (rule disjI1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>d. d \<in> PE_base_lf_rep (dual S', undual R') \<Longrightarrow> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> PE_base_lf_rep (R', S')
 2. \<And>d. d \<in> fn_lf_rep (dual S', undual R') \<Longrightarrow> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> PE_base_lf_rep (R', S') \<or> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> fn_lf_rep (R', S')
[PROOF STEP]
apply (auto simp: PE_base_lf_rep_def eta_cfun cfcomp1 cfun_eq_iff)[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>d. d \<in> fn_lf_rep (dual S', undual R') \<Longrightarrow> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> PE_base_lf_rep (R', S') \<or> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> fn_lf_rep (R', S')
[PROOF STEP]
apply (rule disjI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>d. d \<in> fn_lf_rep (dual S', undual R') \<Longrightarrow> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> fn_lf_rep (R', S')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eRSV e R' S'

goal (1 subgoal):
 1. \<And>d. d \<in> fn_lf_rep (dual S', undual R') \<Longrightarrow> (\<lambda>x. ValD_copy_rec\<cdot>e\<cdot>(d x)) \<in> fn_lf_rep (R', S')
[PROOF STEP]
apply (clarsimp simp: fn_lf_rep_def eta_cfun)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fs. \<lbrakk>eRSV e R' S'; \<forall>xs\<in>unlr S'. (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr (undual R')\<rbrakk> \<Longrightarrow> \<exists>fsa. (\<lambda>x. ValF\<cdot>(cfun_map\<cdot>e\<cdot>e\<cdot>(fs x))) = (\<lambda>i. ValF\<cdot>(fsa i)) \<and> (\<forall>xs\<in>unlr (undual R'). (\<lambda>j. fsa j\<cdot>(xs j)) \<in> unlr S')
[PROOF STEP]
apply (simp add: cfcomp1 cfun_map_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fs. \<lbrakk>eRSV e R' S'; \<forall>xs\<in>unlr S'. (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr (undual R')\<rbrakk> \<Longrightarrow> \<exists>fsa. (\<lambda>x. ValF\<cdot>(\<Lambda> xa. e\<cdot>(fs x\<cdot>(e\<cdot>xa)))) = (\<lambda>i. ValF\<cdot>(fsa i)) \<and> (\<forall>xs\<in>unlr (undual R'). (\<lambda>j. fsa j\<cdot>(xs j)) \<in> unlr S')
[PROOF STEP]
apply (rule_tac x="\<lambda>x. \<Lambda> xa. e\<cdot>(fs x\<cdot>(e\<cdot>xa))" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fs. \<lbrakk>eRSV e R' S'; \<forall>xs\<in>unlr S'. (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr (undual R')\<rbrakk> \<Longrightarrow> (\<lambda>x. ValF\<cdot>(\<Lambda> xa. e\<cdot>(fs x\<cdot>(e\<cdot>xa)))) = (\<lambda>i. ValF\<cdot>(\<Lambda> xa. e\<cdot>(fs i\<cdot>(e\<cdot>xa)))) \<and> (\<forall>xs\<in>unlr (undual R'). (\<lambda>j. (\<Lambda> xa. e\<cdot>(fs j\<cdot>(e\<cdot>xa)))\<cdot>(xs j)) \<in> unlr S')
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma PEI [intro, simp]:
  "\<bottom> \<in> unlr PE.delta"
  "(\<lambda>i. ValTT) \<in> unlr PE.delta"
  "(\<lambda>i. ValFF) \<in> unlr PE.delta"
  "(\<lambda>i. ValN\<cdot>n) \<in> unlr PE.delta"
  "f 1 = \<bottom> \<Longrightarrow> f \<in> unlr PE.delta"
  "f 2 = \<bottom> \<Longrightarrow> f \<in> unlr PE.delta"
  "\<lbrakk> \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. (fs j)\<cdot>(xs j)) \<in> unlr PE.delta \<rbrakk> \<Longrightarrow> (\<lambda>i. ValF\<cdot>(fs i)) \<in> unlr PE.delta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<bottom> \<in> unlr PE.delta &&& (\<lambda>i. ValTT) \<in> unlr PE.delta &&& (\<lambda>i. ValFF) \<in> unlr PE.delta) &&& ((\<lambda>i. ValN\<cdot>n) \<in> unlr PE.delta &&& (f 1 = \<bottom> \<Longrightarrow> f \<in> unlr PE.delta)) &&& (f 2 = \<bottom> \<Longrightarrow> f \<in> unlr PE.delta) &&& ((\<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta) \<Longrightarrow> (\<lambda>i. ValF\<cdot>(fs i)) \<in> unlr PE.delta)
[PROOF STEP]
by (subst PE.delta_sol, simp, subst PE_lf_rep_def,
      fastforce simp: PE_base_lf_rep_def fn_lf_rep_def eta_cfun cfcomp1)+


[STATEMENT]
lemma PE_fun_constI:
  "\<lbrakk> \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. f\<cdot>(xs j)) \<in> unlr PE.delta \<rbrakk> \<Longrightarrow> (\<lambda>i. ValF\<cdot>f) \<in> unlr PE.delta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. f\<cdot>(xs j)) \<in> unlr PE.delta) \<Longrightarrow> (\<lambda>i. ValF\<cdot>f) \<in> unlr PE.delta
[PROOF STEP]
using PEI(7)[where fs="\<lambda>_. f"]
[PROOF STATE]
proof (prove)
using this:
(\<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. f\<cdot>(xs j)) \<in> unlr PE.delta) \<Longrightarrow> (\<lambda>i. ValF\<cdot>f) \<in> unlr PE.delta

goal (1 subgoal):
 1. (\<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. f\<cdot>(xs j)) \<in> unlr PE.delta) \<Longrightarrow> (\<lambda>i. ValF\<cdot>f) \<in> unlr PE.delta
[PROOF STEP]
by simp


[STATEMENT]
lemma PEE:
  "\<lbrakk> a \<in> unlr PE.delta;
     (a = \<bottom> \<Longrightarrow> P);
     (a = (\<lambda>i. ValTT) \<Longrightarrow> P);
     (a = (\<lambda>i. ValFF) \<Longrightarrow> P);
     (\<And>n. a = (\<lambda>i. ValN\<cdot>n) \<Longrightarrow> P);
     (a 1 = \<bottom> \<Longrightarrow> P);
     (a 2 = \<bottom> \<Longrightarrow> P);
     (\<And>fs. \<lbrakk> a = (\<lambda>j. ValF\<cdot>(fs j)); \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. (fs j)\<cdot>(xs j)) \<in> unlr PE.delta \<rbrakk> \<Longrightarrow> P)
   \<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> unlr PE.delta; a = \<bottom> \<Longrightarrow> P; a = (\<lambda>i. ValTT) \<Longrightarrow> P; a = (\<lambda>i. ValFF) \<Longrightarrow> P; \<And>n. a = (\<lambda>i. ValN\<cdot>n) \<Longrightarrow> P; a 1 = \<bottom> \<Longrightarrow> P; a 2 = \<bottom> \<Longrightarrow> P; \<And>fs. \<lbrakk>a = (\<lambda>j. ValF\<cdot>(fs j)); \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply (subst (asm) PE.delta_sol)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> unlr (PE_lf (dual PE.delta, PE.delta)); a = \<bottom> \<Longrightarrow> P; a = (\<lambda>i. ValTT) \<Longrightarrow> P; a = (\<lambda>i. ValFF) \<Longrightarrow> P; \<And>n. a = (\<lambda>i. ValN\<cdot>n) \<Longrightarrow> P; a 1 = \<bottom> \<Longrightarrow> P; a 2 = \<bottom> \<Longrightarrow> P; \<And>fs. \<lbrakk>a = (\<lambda>j. ValF\<cdot>(fs j)); \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> PE_lf_rep (dual PE.delta, PE.delta); a = (\<lambda>i. ValTT) \<Longrightarrow> P; a = (\<lambda>i. ValFF) \<Longrightarrow> P; \<And>n. a = (\<lambda>i. ValN\<cdot>n) \<Longrightarrow> P; a (Suc 0) = \<bottom> \<Longrightarrow> P; a 2 = \<bottom> \<Longrightarrow> P; \<And>fs. \<lbrakk>a = (\<lambda>j. ValF\<cdot>(fs j)); \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply (subst (asm) PE_lf_rep_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> PE_base_lf_rep (dual PE.delta, PE.delta) \<union> fn_lf_rep (dual PE.delta, PE.delta); a = (\<lambda>i. ValTT) \<Longrightarrow> P; a = (\<lambda>i. ValFF) \<Longrightarrow> P; \<And>n. a = (\<lambda>i. ValN\<cdot>n) \<Longrightarrow> P; a (Suc 0) = \<bottom> \<Longrightarrow> P; a 2 = \<bottom> \<Longrightarrow> P; \<And>fs. \<lbrakk>a = (\<lambda>j. ValF\<cdot>(fs j)); \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply (fastforce simp: PE_base_lf_rep_def fn_lf_rep_def eta_cfun)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma PEE_strict_appI:
  assumes "xs \<in> unlr PE.delta"
  assumes "\<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta"
  shows "(\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs \<in> unlr PE.delta
?xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(?xs j)) \<in> unlr PE.delta

goal (1 subgoal):
 1. (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs \<in> unlr PE.delta; \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta
[PROOF STEP]
apply (erule PEE)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>\<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta; xs = \<bottom>\<rbrakk> \<Longrightarrow> (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta
 2. \<lbrakk>\<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta; xs = (\<lambda>i. ValTT)\<rbrakk> \<Longrightarrow> (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta
 3. \<lbrakk>\<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta; xs = (\<lambda>i. ValFF)\<rbrakk> \<Longrightarrow> (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta
 4. \<And>n. \<lbrakk>\<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta; xs = (\<lambda>i. ValN\<cdot>n)\<rbrakk> \<Longrightarrow> (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta
 5. \<lbrakk>\<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta; xs 1 = \<bottom>\<rbrakk> \<Longrightarrow> (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta
 6. \<lbrakk>\<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta; xs 2 = \<bottom>\<rbrakk> \<Longrightarrow> (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta
 7. \<And>fsa. \<lbrakk>\<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta; xs = (\<lambda>j. ValF\<cdot>(fsa j)); \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fsa j\<cdot>(xs j)) \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma logical_relation_PE:
  "logical_relation (unlr PE.delta)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. logical_relation (unlr PE.delta)
[PROOF STEP]
apply (rule logical_relationI)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>fs xs. \<lbrakk>fs \<in> unlr PE.delta; xs \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta
 2. \<And>fs xs. \<lbrakk>fs \<in> unlr PE.delta; xs \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> unlr PE.delta
 3. \<And>fs. (\<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta) \<Longrightarrow> (\<lambda>j. ValF\<cdot>(fs j)) \<in> unlr PE.delta
 4. \<And>fs. (\<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta) \<Longrightarrow> (\<lambda>j. ValF\<cdot>(strictify\<cdot>(fs j))) \<in> unlr PE.delta
 5. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr PE.delta
 6. \<And>cs ts es. \<lbrakk>cs \<in> unlr PE.delta; ts \<in> unlr PE.delta; es \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr PE.delta
 7. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr PE.delta
 8. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr PE.delta
 9. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> unlr PE.delta
[PROOF STEP]
(* Strict application *)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>fs xs. \<lbrakk>fs \<in> unlr PE.delta; xs \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta
 2. \<And>fs xs. \<lbrakk>fs \<in> unlr PE.delta; xs \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> unlr PE.delta
 3. \<And>fs. (\<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta) \<Longrightarrow> (\<lambda>j. ValF\<cdot>(fs j)) \<in> unlr PE.delta
 4. \<And>fs. (\<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta) \<Longrightarrow> (\<lambda>j. ValF\<cdot>(strictify\<cdot>(fs j))) \<in> unlr PE.delta
 5. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr PE.delta
 6. \<And>cs ts es. \<lbrakk>cs \<in> unlr PE.delta; ts \<in> unlr PE.delta; es \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr PE.delta
 7. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr PE.delta
 8. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr PE.delta
 9. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> unlr PE.delta
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>fs xs. \<lbrakk>fs \<in> unlr PE.delta; xs \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> unlr PE.delta
 2. \<And>fs xs. \<lbrakk>fs \<in> unlr PE.delta; xs \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta
 3. \<And>fs. (\<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta) \<Longrightarrow> (\<lambda>j. ValF\<cdot>(fs j)) \<in> unlr PE.delta
 4. \<And>fs. (\<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta) \<Longrightarrow> (\<lambda>j. ValF\<cdot>(strictify\<cdot>(fs j))) \<in> unlr PE.delta
 5. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr PE.delta
 6. \<And>cs ts es. \<lbrakk>cs \<in> unlr PE.delta; ts \<in> unlr PE.delta; es \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr PE.delta
 7. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr PE.delta
 8. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr PE.delta
 9. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> unlr PE.delta
[PROOF STEP]
apply (cut_tac fs="\<lambda>i. appF\<cdot>(fs i)" and xs=xs in PEE_strict_appI)
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<And>fs xs. \<lbrakk>fs \<in> unlr PE.delta; xs \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> xs \<in> unlr PE.delta
 2. \<And>fs xs xsa. \<lbrakk>fs \<in> unlr PE.delta; xs \<in> unlr PE.delta; xsa \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xsa j)) \<in> unlr PE.delta
 3. \<And>fs xs. \<lbrakk>fs \<in> unlr PE.delta; xs \<in> unlr PE.delta; (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. strictify\<cdot>(appF\<cdot>(fs j))\<cdot>(xs j)) \<in> unlr PE.delta
 4. \<And>fs xs. \<lbrakk>fs \<in> unlr PE.delta; xs \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta
 5. \<And>fs. (\<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta) \<Longrightarrow> (\<lambda>j. ValF\<cdot>(fs j)) \<in> unlr PE.delta
 6. \<And>fs. (\<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. strictify\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta) \<Longrightarrow> (\<lambda>j. ValF\<cdot>(strictify\<cdot>(fs j))) \<in> unlr PE.delta
 7. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr PE.delta
 8. \<And>cs ts es. \<lbrakk>cs \<in> unlr PE.delta; ts \<in> unlr PE.delta; es \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr PE.delta
 9. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr PE.delta
 10. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr PE.delta
A total of 11 subgoals...
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>fs xs xsa. \<lbrakk>fs \<in> unlr PE.delta; xs \<in> unlr PE.delta; xsa \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xsa j)) \<in> unlr PE.delta
 2. \<And>fs xs. \<lbrakk>fs \<in> unlr PE.delta; xs \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta
 3. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr PE.delta
 4. \<And>cs ts es. \<lbrakk>cs \<in> unlr PE.delta; ts \<in> unlr PE.delta; es \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr PE.delta
 5. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr PE.delta
 6. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr PE.delta
 7. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> unlr PE.delta
[PROOF STEP]
apply (auto elim: PEE)[1]
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>fs xs. \<lbrakk>fs \<in> unlr PE.delta; xs \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta
 2. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr PE.delta
 3. \<And>cs ts es. \<lbrakk>cs \<in> unlr PE.delta; ts \<in> unlr PE.delta; es \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr PE.delta
 4. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr PE.delta
 5. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr PE.delta
 6. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> unlr PE.delta
[PROOF STEP]
(* FIXME fixD *)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>fs xs. \<lbrakk>fs \<in> unlr PE.delta; xs \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta
 2. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr PE.delta
 3. \<And>cs ts es. \<lbrakk>cs \<in> unlr PE.delta; ts \<in> unlr PE.delta; es \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr PE.delta
 4. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr PE.delta
 5. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr PE.delta
 6. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> unlr PE.delta
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr PE.delta
 2. \<And>fs xs. \<lbrakk>fs \<in> unlr PE.delta; xs \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta
 3. \<And>cs ts es. \<lbrakk>cs \<in> unlr PE.delta; ts \<in> unlr PE.delta; es \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr PE.delta
 4. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr PE.delta
 5. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr PE.delta
 6. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> unlr PE.delta
[PROOF STEP]
apply (erule PEE)
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. \<And>xs. xs = \<bottom> \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr PE.delta
 2. \<And>xs. xs = (\<lambda>i. ValTT) \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr PE.delta
 3. \<And>xs. xs = (\<lambda>i. ValFF) \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr PE.delta
 4. \<And>xs n. xs = (\<lambda>i. ValN\<cdot>n) \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr PE.delta
 5. \<And>xs. xs 1 = \<bottom> \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr PE.delta
 6. \<And>xs. xs 2 = \<bottom> \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr PE.delta
 7. \<And>xs fs. \<lbrakk>xs = (\<lambda>j. ValF\<cdot>(fs j)); \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. fixD\<cdot>(xs j)) \<in> unlr PE.delta
 8. \<And>fs xs. \<lbrakk>fs \<in> unlr PE.delta; xs \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta
 9. \<And>cs ts es. \<lbrakk>cs \<in> unlr PE.delta; ts \<in> unlr PE.delta; es \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr PE.delta
 10. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr PE.delta
A total of 12 subgoals...
[PROOF STEP]
apply (simp_all add: fixD_def)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>xs fs. \<lbrakk>xs = (\<lambda>j. ValF\<cdot>(fs j)); \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. fix\<cdot>(fs j)) \<in> unlr PE.delta
 2. \<And>fs xs. \<lbrakk>fs \<in> unlr PE.delta; xs \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta
 3. \<And>cs ts es. \<lbrakk>cs \<in> unlr PE.delta; ts \<in> unlr PE.delta; es \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr PE.delta
 4. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr PE.delta
 5. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr PE.delta
 6. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> unlr PE.delta
[PROOF STEP]
apply (subst fix_argument_promote_fun)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>xs fs. \<lbrakk>xs = (\<lambda>j. ValF\<cdot>(fs j)); \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<mu> x. (\<lambda>xa. fs xa\<cdot>(x xa))) \<in> unlr PE.delta
 2. \<And>fs xs. \<lbrakk>fs \<in> unlr PE.delta; xs \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta
 3. \<And>cs ts es. \<lbrakk>cs \<in> unlr PE.delta; ts \<in> unlr PE.delta; es \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr PE.delta
 4. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr PE.delta
 5. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr PE.delta
 6. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> unlr PE.delta
[PROOF STEP]
apply (rule_tac F="\<Lambda> f. (\<lambda>x. fs x\<cdot>(f x))" in fix_ind)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>xs fs. \<lbrakk>xs = (\<lambda>j. ValF\<cdot>(fs j)); \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> adm (\<lambda>a. a \<in> unlr PE.delta)
 2. \<And>xs fs. \<lbrakk>xs = (\<lambda>j. ValF\<cdot>(fs j)); \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> \<bottom> \<in> unlr PE.delta
 3. \<And>xs fs x. \<lbrakk>xs = (\<lambda>j. ValF\<cdot>(fs j)); \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta; x \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<Lambda> f. (\<lambda>x. fs x\<cdot>(f x)))\<cdot>x \<in> unlr PE.delta
 4. \<And>fs xs. \<lbrakk>fs \<in> unlr PE.delta; xs \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta
 5. \<And>cs ts es. \<lbrakk>cs \<in> unlr PE.delta; ts \<in> unlr PE.delta; es \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr PE.delta
 6. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr PE.delta
 7. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr PE.delta
 8. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> unlr PE.delta
[PROOF STEP]
apply (simp_all split: nat.split add: cont_fun)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>fs xs. \<lbrakk>fs \<in> unlr PE.delta; xs \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. appF\<cdot>(fs j)\<cdot>(xs j)) \<in> unlr PE.delta
 2. \<And>cs ts es. \<lbrakk>cs \<in> unlr PE.delta; ts \<in> unlr PE.delta; es \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. cond\<cdot>(cs j)\<cdot>(ts j)\<cdot>(es j)) \<in> unlr PE.delta
 3. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. succ\<cdot>(xs j)) \<in> unlr PE.delta
 4. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. pred\<cdot>(xs j)) \<in> unlr PE.delta
 5. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. isZero\<cdot>(xs j)) \<in> unlr PE.delta
[PROOF STEP]
apply (auto elim: PEE simp: cond_def isZero_def pred_def succ_def eta_cfun split: nat.split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma PCF_consts_rel_PE:
  "PCF_consts_rel (unlr PE.delta)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PCF_consts_rel (unlr PE.delta)
[PROOF STEP]
by (rule PCF_consts_relI) simp_all


[STATEMENT]
lemma PCF_lr_PE_delta: "PCF_lr (unlr PE.delta)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PCF_lr (unlr PE.delta)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PCF_lr (unlr PE.delta)
[PROOF STEP]
using logical_relation_PE PCF_consts_rel_PE
[PROOF STATE]
proof (prove)
using this:
logical_relation (unlr PE.delta)
PCF_consts_rel (unlr PE.delta)

goal (1 subgoal):
 1. PCF_lr (unlr PE.delta)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma lr_PE_arg_rel: "PE_arg_rel \<in> unlr PE.delta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PE_arg_rel \<in> unlr PE.delta
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PE_arg_rel \<in> unlr PE.delta
[PROOF STEP]
unfolding PE_arg_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>i. ValF\<cdot>(case i of 0 \<Rightarrow> \<Lambda> uu_. ValFF | Suc n \<Rightarrow> \<Lambda> (ValN\<cdot>x). if x = Suc n then ValTT else \<bottom>)) \<in> unlr PE.delta
[PROOF STEP]
apply (rule PEI(7))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. (case j of 0 \<Rightarrow> \<Lambda> uu_. ValFF | Suc n \<Rightarrow> \<Lambda> (ValN\<cdot>x). if x = Suc n then ValTT else \<bottom>)\<cdot>(xs j)) \<in> unlr PE.delta
[PROOF STEP]
apply (erule PEE)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>xs. xs = \<bottom> \<Longrightarrow> (\<lambda>j. (case j of 0 \<Rightarrow> \<Lambda> uu_. ValFF | Suc n \<Rightarrow> \<Lambda> (ValN\<cdot>x). if x = Suc n then ValTT else \<bottom>)\<cdot>(xs j)) \<in> unlr PE.delta
 2. \<And>xs. xs = (\<lambda>i. ValTT) \<Longrightarrow> (\<lambda>j. (case j of 0 \<Rightarrow> \<Lambda> uu_. ValFF | Suc n \<Rightarrow> \<Lambda> (ValN\<cdot>x). if x = Suc n then ValTT else \<bottom>)\<cdot>(xs j)) \<in> unlr PE.delta
 3. \<And>xs. xs = (\<lambda>i. ValFF) \<Longrightarrow> (\<lambda>j. (case j of 0 \<Rightarrow> \<Lambda> uu_. ValFF | Suc n \<Rightarrow> \<Lambda> (ValN\<cdot>x). if x = Suc n then ValTT else \<bottom>)\<cdot>(xs j)) \<in> unlr PE.delta
 4. \<And>xs n. xs = (\<lambda>i. ValN\<cdot>n) \<Longrightarrow> (\<lambda>j. (case j of 0 \<Rightarrow> \<Lambda> uu_. ValFF | Suc n \<Rightarrow> \<Lambda> (ValN\<cdot>x). if x = Suc n then ValTT else \<bottom>)\<cdot>(xs j)) \<in> unlr PE.delta
 5. \<And>xs. xs 1 = \<bottom> \<Longrightarrow> (\<lambda>j. (case j of 0 \<Rightarrow> \<Lambda> uu_. ValFF | Suc n \<Rightarrow> \<Lambda> (ValN\<cdot>x). if x = Suc n then ValTT else \<bottom>)\<cdot>(xs j)) \<in> unlr PE.delta
 6. \<And>xs. xs 2 = \<bottom> \<Longrightarrow> (\<lambda>j. (case j of 0 \<Rightarrow> \<Lambda> uu_. ValFF | Suc n \<Rightarrow> \<Lambda> (ValN\<cdot>x). if x = Suc n then ValTT else \<bottom>)\<cdot>(xs j)) \<in> unlr PE.delta
 7. \<And>xs fs. \<lbrakk>xs = (\<lambda>j. ValF\<cdot>(fs j)); \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> (\<lambda>j. (case j of 0 \<Rightarrow> \<Lambda> uu_. ValFF | Suc n \<Rightarrow> \<Lambda> (ValN\<cdot>x). if x = Suc n then ValTT else \<bottom>)\<cdot>(xs j)) \<in> unlr PE.delta
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs n. xs = (\<lambda>i. ValN\<cdot>n) \<Longrightarrow> (\<lambda>j. (case j of 0 \<Rightarrow> \<Lambda> uu_. ValFF | Suc n \<Rightarrow> \<Lambda> (ValN\<cdot>x). if x = Suc n then ValTT else \<bottom>)\<cdot>(ValN\<cdot>n)) \<in> unlr PE.delta
[PROOF STEP]
apply (case_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs n. \<lbrakk>xs = (\<lambda>i. ValN\<cdot>n); n = 0\<rbrakk> \<Longrightarrow> (\<lambda>j. (case j of 0 \<Rightarrow> \<Lambda> uu_. ValFF | Suc n \<Rightarrow> \<Lambda> (ValN\<cdot>x). if x = Suc n then ValTT else \<bottom>)\<cdot>(ValN\<cdot>n)) \<in> unlr PE.delta
 2. \<And>xs n nat. \<lbrakk>xs = (\<lambda>i. ValN\<cdot>n); n = Suc nat\<rbrakk> \<Longrightarrow> (\<lambda>j. (case j of 0 \<Rightarrow> \<Lambda> uu_. ValFF | Suc n \<Rightarrow> \<Lambda> (ValN\<cdot>x). if x = Suc n then ValTT else \<bottom>)\<cdot>(ValN\<cdot>n)) \<in> unlr PE.delta
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs n nat. \<lbrakk>xs = (\<lambda>i. ValN\<cdot>n); n = Suc nat\<rbrakk> \<Longrightarrow> (\<lambda>j. (case j of 0 \<Rightarrow> \<Lambda> uu_. ValFF | Suc n \<Rightarrow> \<Lambda> (ValN\<cdot>x). if x = Suc n then ValTT else \<bottom>)\<cdot>(ValN\<cdot>n)) \<in> unlr PE.delta
[PROOF STEP]
apply (case_tac nat)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs n nat. \<lbrakk>xs = (\<lambda>i. ValN\<cdot>n); n = Suc nat; nat = 0\<rbrakk> \<Longrightarrow> (\<lambda>j. (case j of 0 \<Rightarrow> \<Lambda> uu_. ValFF | Suc n \<Rightarrow> \<Lambda> (ValN\<cdot>x). if x = Suc n then ValTT else \<bottom>)\<cdot>(ValN\<cdot>n)) \<in> unlr PE.delta
 2. \<And>xs n nat nata. \<lbrakk>xs = (\<lambda>i. ValN\<cdot>n); n = Suc nat; nat = Suc nata\<rbrakk> \<Longrightarrow> (\<lambda>j. (case j of 0 \<Rightarrow> \<Lambda> uu_. ValFF | Suc n \<Rightarrow> \<Lambda> (ValN\<cdot>x). if x = Suc n then ValTT else \<bottom>)\<cdot>(ValN\<cdot>n)) \<in> unlr PE.delta
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma lr_PE_result_rel: "PE_result_rel \<notin> unlr PE.delta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PE_result_rel \<notin> unlr PE.delta
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PE_result_rel \<notin> unlr PE.delta
[PROOF STEP]
unfolding PE_result_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>i. case i of 0 \<Rightarrow> ValFF | Suc n \<Rightarrow> ValTT) \<notin> unlr PE.delta
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>i. case i of 0 \<Rightarrow> ValFF | Suc n \<Rightarrow> ValTT) \<in> unlr PE.delta \<Longrightarrow> False
[PROOF STEP]
apply (erule PEE)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. (\<lambda>i. case i of 0 \<Rightarrow> ValFF | Suc n \<Rightarrow> ValTT) = \<bottom> \<Longrightarrow> False
 2. (\<lambda>i. case i of 0 \<Rightarrow> ValFF | Suc n \<Rightarrow> ValTT) = (\<lambda>i. ValTT) \<Longrightarrow> False
 3. (\<lambda>i. case i of 0 \<Rightarrow> ValFF | Suc n \<Rightarrow> ValTT) = (\<lambda>i. ValFF) \<Longrightarrow> False
 4. \<And>n. (\<lambda>i. case i of 0 \<Rightarrow> ValFF | Suc n \<Rightarrow> ValTT) = (\<lambda>i. ValN\<cdot>n) \<Longrightarrow> False
 5. (case 1 of 0 \<Rightarrow> ValFF | Suc n \<Rightarrow> ValTT) = \<bottom> \<Longrightarrow> False
 6. (case 2 of 0 \<Rightarrow> ValFF | Suc n \<Rightarrow> ValTT) = \<bottom> \<Longrightarrow> False
 7. \<And>fs. \<lbrakk>(\<lambda>i. case i of 0 \<Rightarrow> ValFF | Suc n \<Rightarrow> ValTT) = (\<lambda>j. ValF\<cdot>(fs j)); \<And>xs. xs \<in> unlr PE.delta \<Longrightarrow> (\<lambda>j. fs j\<cdot>(xs j)) \<in> unlr PE.delta\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (auto iff: fun_eq_iff split: nat.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem PE_is_not_definable: "\<not>(\<exists>f. definable f \<and> appFLv f [PE_arg_rel] = PE_result_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>f. definable f \<and> appFLv f [PE_arg_rel] = PE_result_rel
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>f. definable f \<and> appFLv f [PE_arg_rel] = PE_result_rel
[PROOF STEP]
apply (rule not_definable[where R="unlr PE.delta"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. PCF_lr (unlr PE.delta)
 2. set [PE_arg_rel] \<subseteq> unlr PE.delta
 3. PE_result_rel \<notin> unlr PE.delta
[PROOF STEP]
using lr_PE_arg_rel lr_PE_result_rel PCF_lr_PE_delta
[PROOF STATE]
proof (prove)
using this:
PE_arg_rel \<in> unlr PE.delta
PE_result_rel \<notin> unlr PE.delta
PCF_lr (unlr PE.delta)

goal (3 subgoals):
 1. PCF_lr (unlr PE.delta)
 2. set [PE_arg_rel] \<subseteq> unlr PE.delta
 3. PE_result_rel \<notin> unlr PE.delta
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem tok_id_identified:
 "n \<in> bad_tok_prik \<Longrightarrow> \<exists>s. s\<^sub>0 \<Turnstile> s \<and> \<langle>n, Hash (ID n (Sec_PubKey m))\<rangle> \<in> spied s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> bad_tok_prik \<Longrightarrow> \<exists>s. s\<^sub>0 \<Turnstile> s \<and> \<langle>n, Hash (ID n (Sec_PubKey m))\<rangle> \<in> spied s
[PROOF STEP]
by (rule exI [of _ "tok_id_hash n m"], drule tok_id_hash_rel [of _ m],
 simp add: tok_id_hash_def)


[STATEMENT]
lemma sec_id_identified_1:
 "{Tok_PriK n, Sec_PriK m, Rev_PriK} \<noteq> {Tok_PriK n', Rev_PriK}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {Tok_PriK n, Sec_PriK m, Rev_PriK} \<noteq> {Tok_PriK n', Rev_PriK}
[PROOF STEP]
by (simp add: set_eq_iff, rule exI [of _ "Sec_PriK m"], insert
 sec_prik_rev sec_prik_tok_prik, simp add: image_def, drule spec [of _ m], auto)


[STATEMENT]
lemma sec_id_identified_2:
 "(Spy, PubKey {Tok_PriK n, Rev_PriK}) \<notin> s\<^sub>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Spy, PubKey {Tok_PriK n, Rev_PriK}) \<notin> s\<^sub>0
[PROOF STEP]
by (insert tok_prik_rev sec_id_identified_1, simp add: image_def,
 drule spec [of _ n], auto simp: set_eq_iff)


[STATEMENT]
lemma sec_id_identified_3:
 "{Tok_PriK n, Rev_PriK} =
    {Tok_PriK n, Sec_PriK m, Rev_PriK} - {Sec_PriK m}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {Tok_PriK n, Rev_PriK} = {Tok_PriK n, Sec_PriK m, Rev_PriK} - {Sec_PriK m}
[PROOF STEP]
by (insert sec_prik_rev sec_prik_tok_prik, auto)


[STATEMENT]
lemma sec_id_identified_4:
 "PubK {Tok_PriK n, Sec_PriK m, Rev_PriK} =
    PubK (insert (Sec_PriK m) {Tok_PriK n, Rev_PriK})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PubK {Tok_PriK n, Sec_PriK m, Rev_PriK} = PubK {Sec_PriK m, Tok_PriK n, Rev_PriK}
[PROOF STEP]
by auto


[STATEMENT]
theorem sec_id_identified:
 "\<lbrakk>{m, m'} \<subseteq> bad_sec_prik; (n, m') \<in> bad_id\<rbrakk> \<Longrightarrow>
    \<exists>s. s\<^sub>0 \<Turnstile> s \<and> \<langle>n, Hash (ID n (Sec_PubKey m))\<rangle> \<in> spied s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{m, m'} \<subseteq> bad_sec_prik; (n, m') \<in> bad_id\<rbrakk> \<Longrightarrow> \<exists>s. s\<^sub>0 \<Turnstile> s \<and> \<langle>n, Hash (ID n (Sec_PubKey m))\<rangle> \<in> spied s
[PROOF STEP]
by (cases "(n, m) \<in> bad_id", blast, rule exI [of _ "sec_id_hash n m"],
 drule sec_id_hash_rel, simp_all add: sec_id_hash_def)


[STATEMENT]
lemma mono_top[simp]: "mono top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono \<top>
[PROOF STEP]
by (simp add: mono_def top_fun_def)


[STATEMENT]
lemma mono_choice[simp]: "mono S \<Longrightarrow> mono T \<Longrightarrow> mono (S \<sqinter> T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mono S; mono T\<rbrakk> \<Longrightarrow> mono (S \<sqinter> T)
[PROOF STEP]
apply (simp add: mono_def inf_fun_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x y. x \<sqsubseteq> y \<longrightarrow> S x \<sqsubseteq> S y; \<forall>x y. x \<sqsubseteq> y \<longrightarrow> T x \<sqsubseteq> T y\<rbrakk> \<Longrightarrow> \<forall>x y. x \<sqsubseteq> y \<longrightarrow> S x \<sqinter> T x \<sqsubseteq> S y \<and> S x \<sqinter> T x \<sqsubseteq> T y
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>x y. x \<sqsubseteq> y \<longrightarrow> S x \<sqsubseteq> S y; \<forall>x y. x \<sqsubseteq> y \<longrightarrow> T x \<sqsubseteq> T y; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> S x \<sqinter> T x \<sqsubseteq> S y
 2. \<And>x y. \<lbrakk>\<forall>x y. x \<sqsubseteq> y \<longrightarrow> S x \<sqsubseteq> S y; \<forall>x y. x \<sqsubseteq> y \<longrightarrow> T x \<sqsubseteq> T y; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> S x \<sqinter> T x \<sqsubseteq> T y
[PROOF STEP]
apply (rule_tac y = "S x" in order_trans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>x y. x \<sqsubseteq> y \<longrightarrow> S x \<sqsubseteq> S y; \<forall>x y. x \<sqsubseteq> y \<longrightarrow> T x \<sqsubseteq> T y; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> S x \<sqinter> T x \<sqsubseteq> S x
 2. \<And>x y. \<lbrakk>\<forall>x y. x \<sqsubseteq> y \<longrightarrow> S x \<sqsubseteq> S y; \<forall>x y. x \<sqsubseteq> y \<longrightarrow> T x \<sqsubseteq> T y; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> S x \<sqsubseteq> S y
 3. \<And>x y. \<lbrakk>\<forall>x y. x \<sqsubseteq> y \<longrightarrow> S x \<sqsubseteq> S y; \<forall>x y. x \<sqsubseteq> y \<longrightarrow> T x \<sqsubseteq> T y; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> S x \<sqinter> T x \<sqsubseteq> T y
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>x y. x \<sqsubseteq> y \<longrightarrow> S x \<sqsubseteq> S y; \<forall>x y. x \<sqsubseteq> y \<longrightarrow> T x \<sqsubseteq> T y; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> S x \<sqinter> T x \<sqsubseteq> T y
[PROOF STEP]
apply (rule_tac y = "T x" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>x y. x \<sqsubseteq> y \<longrightarrow> S x \<sqsubseteq> S y; \<forall>x y. x \<sqsubseteq> y \<longrightarrow> T x \<sqsubseteq> T y; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> S x \<sqinter> T x \<sqsubseteq> T x
 2. \<And>x y. \<lbrakk>\<forall>x y. x \<sqsubseteq> y \<longrightarrow> S x \<sqsubseteq> S y; \<forall>x y. x \<sqsubseteq> y \<longrightarrow> T x \<sqsubseteq> T y; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> T x \<sqsubseteq> T y
[PROOF STEP]
by simp_all


[STATEMENT]
lemma mono_assert [simp]: "mono {.p.}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono {. p .}
[PROOF STEP]
apply (simp add: assert_def mono_def, safe)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> p \<sqinter> x \<sqsubseteq> y
[PROOF STEP]
apply (rule_tac y = "x" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> p \<sqinter> x \<sqsubseteq> x
 2. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> y
[PROOF STEP]
by simp_all


[STATEMENT]
lemma mono_assume [simp]: "mono (assume P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono [. P .]
[PROOF STEP]
apply (simp add: assume_def mono_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. x \<sqsubseteq> y \<longrightarrow> x \<sqsubseteq> - P \<squnion> y
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> - P \<squnion> y
[PROOF STEP]
apply (rule_tac y = "y" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> y
 2. \<And>x y. x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> - P \<squnion> y
[PROOF STEP]
by simp_all


[STATEMENT]
lemma mono_demonic [simp]: "mono [:Q:]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono [: Q :]
[PROOF STEP]
apply (simp add: mono_def demonic_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. x \<sqsubseteq> y \<longrightarrow> {s. Q s \<sqsubseteq> x} \<subseteq> {s. Q s \<sqsubseteq> y}
[PROOF STEP]
by auto


[STATEMENT]
theorem demonic_bottom:
  "[:R:] (\<bottom>::('a::order_bot)) = {s . (R s) = \<bottom>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [: R :] \<bottom> = {s. R s = \<bottom>}
[PROOF STEP]
apply (unfold demonic_def, safe, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. R x \<sqsubseteq> \<bottom> \<Longrightarrow> R x = \<bottom>
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. R x \<sqsubseteq> \<bottom> \<Longrightarrow> R x \<sqsubseteq> \<bottom>
 2. \<And>x. R x \<sqsubseteq> \<bottom> \<Longrightarrow> \<bottom> \<sqsubseteq> R x
[PROOF STEP]
by auto


[STATEMENT]
theorem demonic_bottom_top [simp]:
  "[:(\<bottom>::_::order_bot):]  = \<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [: \<bottom> :] = \<top>
[PROOF STEP]
by (simp add: fun_eq_iff inf_fun_def sup_fun_def demonic_def top_fun_def bot_fun_def)


[STATEMENT]
theorem demonic_sup_inf:
  "[:Q \<squnion> Q':] = [:Q:] \<sqinter> [:Q':]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [: Q \<squnion> Q' :] = [: Q :] \<sqinter> [: Q' :]
[PROOF STEP]
by (simp add: fun_eq_iff sup_fun_def inf_fun_def demonic_def, blast)


[STATEMENT]
theorem angelic_bottom [simp]:
  "angelic R \<bottom>  = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {: R :} \<bottom> = {}
[PROOF STEP]
by (simp add: angelic_def inf_bot_bot)


[STATEMENT]
theorem angelic_disjunctive [simp]:
  "{:(R::('a \<Rightarrow> 'b::complete_distrib_lattice)):} \<in> Apply.Disjunctive"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {: R :} \<in> Apply.Disjunctive
[PROOF STEP]
by (simp add: Apply.Disjunctive_def angelic_def inf_Sup, blast)


[STATEMENT]
lemma grd_choice[simp]: "grd (S \<sqinter> T) = (grd S) \<squnion> (grd T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. grd (S \<sqinter> T) = grd S \<squnion> grd T
[PROOF STEP]
by (simp add: grd_def inf_fun_def)


[STATEMENT]
lemma grd_demonic: "grd [:Q:] = {s . \<exists> s' . s' \<in> (Q s) }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. grd [: Q :] = {s. \<exists>s'. s' \<in> Q s}
[PROOF STEP]
apply (simp add: grd_def demonic_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - {s. Q s = {}} = {s. \<exists>s'. s' \<in> Q s}
[PROOF STEP]
by blast


[STATEMENT]
lemma grd_demonic_2[simp]: "(s \<notin> grd [:Q:]) = (\<forall> s' . s' \<notin>  (Q s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s \<notin> grd [: Q :]) = (\<forall>s'. s' \<notin> Q s)
[PROOF STEP]
by (simp add: grd_demonic)


[STATEMENT]
theorem grd_angelic:
  "grd {:R:} = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. grd {: R :} = UNIV
[PROOF STEP]
by (simp add: grd_def)


[STATEMENT]
lemma singleton_eq_iff [iff]: "set {a} = set {b} \<longleftrightarrow> a=b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (set {a} = set {b}) = (a = b)
[PROOF STEP]
by simp


[STATEMENT]
lemma doubleton_eq_iff: "set {a,b} = set {c,d} \<longleftrightarrow> (a=c \<and> b=d) \<or> (a=d \<and> b=c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (set {a, b} = set {c, d}) = (a = c \<and> b = d \<or> a = d \<and> b = c)
[PROOF STEP]
by (simp add: Set.doubleton_eq_iff)


[STATEMENT]
lemma vpair_def': "vpair a b = set {set {a,a},set {a,b}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>a, b\<rangle> = set {set {a, a}, set {a, b}}
[PROOF STEP]
by (simp add: vpair_def)


[STATEMENT]
lemma vpair_iff [simp]: "vpair a b = vpair a' b' \<longleftrightarrow> a=a' \<and> b=b'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<langle>a, b\<rangle> = \<langle>a', b'\<rangle>) = (a = a' \<and> b = b')
[PROOF STEP]
unfolding vpair_def' doubleton_eq_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((a = a' \<and> a = a' \<or> a = a' \<and> a = a') \<and> (a = a' \<and> b = b' \<or> a = b' \<and> b = a') \<or> (a = a' \<and> a = b' \<or> a = b' \<and> a = a') \<and> (a = a' \<and> b = a' \<or> a = a' \<and> b = a')) = (a = a' \<and> b = b')
[PROOF STEP]
by auto


[STATEMENT]
lemma vfst_conv [simp]: "vfst \<langle>a,b\<rangle> = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfst \<langle>a, b\<rangle> = a
[PROOF STEP]
by (simp add: vfst_def)


[STATEMENT]
lemma vsnd_conv [simp]: "vsnd \<langle>a,b\<rangle> = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsnd \<langle>a, b\<rangle> = b
[PROOF STEP]
by (simp add: vsnd_def)


[STATEMENT]
lemma vsplit [simp]: "vsplit c \<langle>a,b\<rangle> = c a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsplit c \<langle>a, b\<rangle> = c a b
[PROOF STEP]
by (simp add: vsplit_def)


[STATEMENT]
lemma vpair_neq_fst: "\<langle>a,b\<rangle> \<noteq> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>a, b\<rangle> \<noteq> a
[PROOF STEP]
by (metis elts_of_set insertI1 mem_not_sym small_upair vpair_def')


[STATEMENT]
lemma vpair_neq_snd: "\<langle>a,b\<rangle> \<noteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>a, b\<rangle> \<noteq> b
[PROOF STEP]
by (metis elts_of_set insertI1 mem_not_sym small_upair subsetD subset_insertI vpair_def')


[STATEMENT]
lemma vpair_nonzero [simp]: "\<langle>x,y\<rangle> \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>x, y\<rangle> \<noteq> 0
[PROOF STEP]
by (metis elts_0 elts_of_set empty_not_insert small_upair vpair_def)


[STATEMENT]
lemma zero_notin_vpair: "0 \<notin> elts \<langle>x,y\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<notin> elts \<langle>x, y\<rangle>
[PROOF STEP]
by (auto simp: vpair_def)


[STATEMENT]
lemma inj_on_vpair [simp]: "inj_on (\<lambda>(x, y). \<langle>x, y\<rangle>) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>(x, y). \<langle>x, y\<rangle>) A
[PROOF STEP]
by (auto simp: inj_on_def)


[STATEMENT]
lemma pairs_iff_elts: "(x,y) \<in> pairs z \<longleftrightarrow> \<langle>x,y\<rangle> \<in> elts z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x, y) \<in> pairs z) = (\<langle>x, y\<rangle> \<in> elts z)
[PROOF STEP]
by (simp add: pairs_def)


[STATEMENT]
lemma VSigma_iff [simp]: "\<langle>a,b\<rangle> \<in> elts (VSigma A B) \<longleftrightarrow> a \<in> elts A \<and> b \<in> elts (B a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<langle>a, b\<rangle> \<in> elts (VSigma A B)) = (a \<in> elts A \<and> b \<in> elts (B a))
[PROOF STEP]
by (auto simp: VSigma_def UNION_singleton_eq_range)


[STATEMENT]
lemma VSigmaI [intro!]: "\<lbrakk> a \<in> elts A;  b \<in> elts (B a)\<rbrakk>  \<Longrightarrow> \<langle>a,b\<rangle> \<in> elts (VSigma A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> elts A; b \<in> elts (B a)\<rbrakk> \<Longrightarrow> \<langle>a, b\<rangle> \<in> elts (VSigma A B)
[PROOF STEP]
by simp


[STATEMENT]
lemma VSigmaE [elim!]:
  assumes "c \<in> elts (VSigma A B)"
  obtains x y where "x \<in> elts A" "y \<in> elts (B x)" "c=\<langle>x,y\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in> elts A; y \<in> elts (B x); c = \<langle>x, y\<rangle>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
c \<in> elts (VSigma A B)

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in> elts A; y \<in> elts (B x); c = \<langle>x, y\<rangle>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: VSigma_def split: if_split_asm)


[STATEMENT]
lemma VSigmaE2 [elim!]:
  assumes "\<langle>a,b\<rangle> \<in> elts (VSigma A B)" obtains "a \<in> elts A" and "b \<in> elts (B a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>a \<in> elts A; b \<in> elts (B a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<langle>a, b\<rangle> \<in> elts (VSigma A B)

goal (1 subgoal):
 1. (\<lbrakk>a \<in> elts A; b \<in> elts (B a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma VSigma_empty1 [simp]: "VSigma 0 B = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VSigma 0 B = 0
[PROOF STEP]
by auto


[STATEMENT]
lemma times_iff [simp]: "\<langle>a,b\<rangle> \<in> elts (vtimes A B) \<longleftrightarrow> a \<in> elts A \<and> b \<in> elts B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<langle>a, b\<rangle> \<in> elts (vtimes A B)) = (a \<in> elts A \<and> b \<in> elts B)
[PROOF STEP]
by simp


[STATEMENT]
lemma timesI [intro!]: "\<lbrakk>a \<in> elts A;  b \<in> elts B\<rbrakk>  \<Longrightarrow> \<langle>a,b\<rangle> \<in> elts (vtimes A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> elts A; b \<in> elts B\<rbrakk> \<Longrightarrow> \<langle>a, b\<rangle> \<in> elts (vtimes A B)
[PROOF STEP]
by simp


[STATEMENT]
lemma times_empty2 [simp]: "vtimes A 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vtimes A 0 = 0
[PROOF STEP]
using elts_0
[PROOF STATE]
proof (prove)
using this:
elts 0 = {}

goal (1 subgoal):
 1. vtimes A 0 = 0
[PROOF STEP]
by blast


[STATEMENT]
lemma times_empty_iff: "VSigma A B = 0 \<longleftrightarrow> A=0 \<or> (\<forall>x \<in> elts A. B x = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (VSigma A B = 0) = (A = 0 \<or> (\<forall>x\<in>elts A. B x = 0))
[PROOF STEP]
by (metis VSigmaE VSigmaI elts_0 empty_iff trad_foundation)


[STATEMENT]
lemma elts_VSigma: "elts (VSigma A B) = (\<lambda>(x,y). vpair x y) ` Sigma (elts A) (\<lambda>x. elts (B x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (VSigma A B) = (\<lambda>(x, y). \<langle>x, y\<rangle>) ` (SIGMA x:elts A. elts (B x))
[PROOF STEP]
by auto


[STATEMENT]
lemma small_Sigma [simp]:
  assumes A: "small A" and B: "\<And>x. x \<in> A \<Longrightarrow> small (B x)"
  shows "small (Sigma A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small (Sigma A B)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. small (Sigma A B)
[PROOF STEP]
obtain a where "elts a \<approx> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. elts a \<approx> A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson assms small_eqpoll)
[PROOF STATE]
proof (state)
this:
elts a \<approx> A

goal (1 subgoal):
 1. small (Sigma A B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
elts a \<approx> A
[PROOF STEP]
obtain f where f: "bij_betw f (elts a) A"
[PROOF STATE]
proof (prove)
using this:
elts a \<approx> A

goal (1 subgoal):
 1. (\<And>f. bij_betw f (elts a) A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eqpoll_def
[PROOF STATE]
proof (prove)
using this:
elts a \<approx> A
?A \<approx> ?B \<equiv> \<exists>f. bij_betw f ?A ?B

goal (1 subgoal):
 1. (\<And>f. bij_betw f (elts a) A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bij_betw f (elts a) A

goal (1 subgoal):
 1. small (Sigma A B)
[PROOF STEP]
have "\<exists>y. elts y \<approx> B x" if "x \<in> A" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. elts y \<approx> B x
[PROOF STEP]
using B small_eqpoll that
[PROOF STATE]
proof (prove)
using this:
?x \<in> A \<Longrightarrow> small (B ?x)
small ?A = (\<exists>x. elts x \<approx> ?A)
x \<in> A

goal (1 subgoal):
 1. \<exists>y. elts y \<approx> B x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?x \<in> A \<Longrightarrow> \<exists>y. elts y \<approx> B ?x

goal (1 subgoal):
 1. small (Sigma A B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> A \<Longrightarrow> \<exists>y. elts y \<approx> B ?x
[PROOF STEP]
obtain g where g: "\<And>x. x \<in> A \<Longrightarrow> elts (g x) \<approx> B x"
[PROOF STATE]
proof (prove)
using this:
?x \<in> A \<Longrightarrow> \<exists>y. elts y \<approx> B ?x

goal (1 subgoal):
 1. (\<And>g. (\<And>x. x \<in> A \<Longrightarrow> elts (g x) \<approx> B x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?x \<in> A \<Longrightarrow> elts (g ?x) \<approx> B ?x

goal (1 subgoal):
 1. small (Sigma A B)
[PROOF STEP]
with f
[PROOF STATE]
proof (chain)
picking this:
bij_betw f (elts a) A
?x \<in> A \<Longrightarrow> elts (g ?x) \<approx> B ?x
[PROOF STEP]
have "elts (VSigma a (g \<circ> f)) \<approx> Sigma A B"
[PROOF STATE]
proof (prove)
using this:
bij_betw f (elts a) A
?x \<in> A \<Longrightarrow> elts (g ?x) \<approx> B ?x

goal (1 subgoal):
 1. elts (VSigma a (g \<circ> f)) \<approx> Sigma A B
[PROOF STEP]
by (simp add: elts_VSigma Sigma_eqpoll_cong bij_betwE)
[PROOF STATE]
proof (state)
this:
elts (VSigma a (g \<circ> f)) \<approx> Sigma A B

goal (1 subgoal):
 1. small (Sigma A B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
elts (VSigma a (g \<circ> f)) \<approx> Sigma A B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
elts (VSigma a (g \<circ> f)) \<approx> Sigma A B

goal (1 subgoal):
 1. small (Sigma A B)
[PROOF STEP]
using small_eqpoll
[PROOF STATE]
proof (prove)
using this:
elts (VSigma a (g \<circ> f)) \<approx> Sigma A B
small ?A = (\<exists>x. elts x \<approx> ?A)

goal (1 subgoal):
 1. small (Sigma A B)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
small (Sigma A B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma small_Times [simp]:
  assumes "small A" "small B"  shows "small (A \<times> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small (A \<times> B)
[PROOF STEP]
by (simp add: assms)


[STATEMENT]
lemma small_Times_iff: "small (A \<times> B) \<longleftrightarrow> small A \<and> small B \<or> A={} \<or> B={}"  (is "_ = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small (A \<times> B) = (small A \<and> small B \<or> A = {} \<or> B = {})
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. small (A \<times> B) \<Longrightarrow> small A \<and> small B \<or> A = {} \<or> B = {}
 2. small A \<and> small B \<or> A = {} \<or> B = {} \<Longrightarrow> small (A \<times> B)
[PROOF STEP]
assume *: "small (A \<times> B)"
[PROOF STATE]
proof (state)
this:
small (A \<times> B)

goal (2 subgoals):
 1. small (A \<times> B) \<Longrightarrow> small A \<and> small B \<or> A = {} \<or> B = {}
 2. small A \<and> small B \<or> A = {} \<or> B = {} \<Longrightarrow> small (A \<times> B)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
small (A \<times> B)

goal (2 subgoals):
 1. small (A \<times> B) \<Longrightarrow> small A \<and> small B \<or> A = {} \<or> B = {}
 2. small A \<and> small B \<or> A = {} \<or> B = {} \<Longrightarrow> small (A \<times> B)
[PROOF STEP]
have "small A \<and> small B" if "x \<in> A" "y \<in> B" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small A \<and> small B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. small A \<and> small B
[PROOF STEP]
have "A \<subseteq> fst ` (A \<times> B)" "B \<subseteq> snd ` (A \<times> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> fst ` (A \<times> B) &&& B \<subseteq> snd ` (A \<times> B)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in> A
y \<in> B

goal (1 subgoal):
 1. A \<subseteq> fst ` (A \<times> B) &&& B \<subseteq> snd ` (A \<times> B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<subseteq> fst ` (A \<times> B)
B \<subseteq> snd ` (A \<times> B)

goal (1 subgoal):
 1. small A \<and> small B
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
y \<in> B
A \<subseteq> fst ` (A \<times> B)
B \<subseteq> snd ` (A \<times> B)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> A
y \<in> B
A \<subseteq> fst ` (A \<times> B)
B \<subseteq> snd ` (A \<times> B)

goal (1 subgoal):
 1. small A \<and> small B
[PROOF STEP]
by (metis * replacement smaller_than_small)
[PROOF STATE]
proof (state)
this:
small A \<and> small B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> A; ?y \<in> B\<rbrakk> \<Longrightarrow> small A \<and> small B

goal (2 subgoals):
 1. small (A \<times> B) \<Longrightarrow> small A \<and> small B \<or> A = {} \<or> B = {}
 2. small A \<and> small B \<or> A = {} \<or> B = {} \<Longrightarrow> small (A \<times> B)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> A; ?y \<in> B\<rbrakk> \<Longrightarrow> small A \<and> small B

goal (2 subgoals):
 1. small (A \<times> B) \<Longrightarrow> small A \<and> small B \<or> A = {} \<or> B = {}
 2. small A \<and> small B \<or> A = {} \<or> B = {} \<Longrightarrow> small (A \<times> B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x \<in> A; ?y \<in> B\<rbrakk> \<Longrightarrow> small A \<and> small B
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> A; ?y \<in> B\<rbrakk> \<Longrightarrow> small A \<and> small B

goal (1 subgoal):
 1. small A \<and> small B \<or> A = {} \<or> B = {}
[PROOF STEP]
by (metis equals0I)
[PROOF STATE]
proof (state)
this:
small A \<and> small B \<or> A = {} \<or> B = {}

goal (1 subgoal):
 1. small A \<and> small B \<or> A = {} \<or> B = {} \<Longrightarrow> small (A \<times> B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. small A \<and> small B \<or> A = {} \<or> B = {} \<Longrightarrow> small (A \<times> B)
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
small A \<and> small B \<or> A = {} \<or> B = {}

goal (1 subgoal):
 1. small A \<and> small B \<or> A = {} \<or> B = {} \<Longrightarrow> small (A \<times> B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
small A \<and> small B \<or> A = {} \<or> B = {}
[PROOF STEP]
show "small (A \<times> B)"
[PROOF STATE]
proof (prove)
using this:
small A \<and> small B \<or> A = {} \<or> B = {}

goal (1 subgoal):
 1. small (A \<times> B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
small (A \<times> B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Inl_nonzero [simp]:"Inl x \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFC_Cardinals.Inl x \<noteq> 0
[PROOF STEP]
by (metis Inl_def vpair_nonzero)


[STATEMENT]
lemma Inr_nonzero [simp]:"Inr x \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFC_Cardinals.Inr x \<noteq> 0
[PROOF STEP]
by (metis Inr_def vpair_nonzero)


[STATEMENT]
lemma Inl_in_sum_iff [iff]: "Inl a \<in> elts (A \<Uplus> B) \<longleftrightarrow> a \<in> elts A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ZFC_Cardinals.Inl a \<in> elts (A \<Uplus> B)) = (a \<in> elts A)
[PROOF STEP]
by (auto simp: sum_defs)


[STATEMENT]
lemma Inr_in_sum_iff [iff]: "Inr b \<in> elts (A \<Uplus> B) \<longleftrightarrow> b \<in> elts B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ZFC_Cardinals.Inr b \<in> elts (A \<Uplus> B)) = (b \<in> elts B)
[PROOF STEP]
by (auto simp: sum_defs)


[STATEMENT]
lemma sumE [elim!]:
  assumes u: "u \<in> elts (A \<Uplus> B)"
  obtains x where "x \<in> elts A" "u=Inl x" | y where "y \<in> elts B" "u=Inr y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrakk>x \<in> elts A; u = ZFC_Cardinals.Inl x\<rbrakk> \<Longrightarrow> thesis; \<And>y. \<lbrakk>y \<in> elts B; u = ZFC_Cardinals.Inr y\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using u
[PROOF STATE]
proof (prove)
using this:
u \<in> elts (A \<Uplus> B)

goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrakk>x \<in> elts A; u = ZFC_Cardinals.Inl x\<rbrakk> \<Longrightarrow> thesis; \<And>y. \<lbrakk>y \<in> elts B; u = ZFC_Cardinals.Inr y\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: sum_defs)


[STATEMENT]
lemma Inl_iff [iff]: "Inl a=Inl b \<longleftrightarrow> a=b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ZFC_Cardinals.Inl a = ZFC_Cardinals.Inl b) = (a = b)
[PROOF STEP]
by (simp add: sum_defs)


[STATEMENT]
lemma Inr_iff [iff]: "Inr a=Inr b \<longleftrightarrow> a=b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ZFC_Cardinals.Inr a = ZFC_Cardinals.Inr b) = (a = b)
[PROOF STEP]
by (simp add: sum_defs)


[STATEMENT]
lemma inj_on_Inl [simp]: "inj_on Inl A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on ZFC_Cardinals.Inl A
[PROOF STEP]
by (simp add: inj_on_def)


[STATEMENT]
lemma inj_on_Inr [simp]: "inj_on Inr A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on ZFC_Cardinals.Inr A
[PROOF STEP]
by (simp add: inj_on_def)


[STATEMENT]
lemma Inl_Inr_iff [iff]: "Inl a=Inr b \<longleftrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ZFC_Cardinals.Inl a = ZFC_Cardinals.Inr b) = False
[PROOF STEP]
by (simp add: sum_defs)


[STATEMENT]
lemma Inr_Inl_iff [iff]: "Inr b=Inl a \<longleftrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ZFC_Cardinals.Inr b = ZFC_Cardinals.Inl a) = False
[PROOF STEP]
by (simp add: sum_defs)


[STATEMENT]
lemma sum_empty [simp]: "0 \<Uplus> 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<Uplus> 0 = 0
[PROOF STEP]
by auto


[STATEMENT]
lemma elts_vsum: "elts (a \<Uplus> b) = Inl ` (elts a) \<union> Inr ` (elts b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (a \<Uplus> b) = ZFC_Cardinals.Inl ` elts a \<union> ZFC_Cardinals.Inr ` elts b
[PROOF STEP]
by auto


[STATEMENT]
lemma sum_iff: "u \<in> elts (A \<Uplus> B) \<longleftrightarrow> (\<exists>x. x \<in> elts A \<and> u=Inl x) \<or> (\<exists>y. y \<in> elts B \<and> u=Inr y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u \<in> elts (A \<Uplus> B)) = ((\<exists>x. x \<in> elts A \<and> u = ZFC_Cardinals.Inl x) \<or> (\<exists>y. y \<in> elts B \<and> u = ZFC_Cardinals.Inr y))
[PROOF STEP]
by blast


[STATEMENT]
lemma sum_subset_iff: "A\<Uplus>B \<le> C\<Uplus>D \<longleftrightarrow> A\<le>C \<and> B\<le>D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<Uplus> B \<le> C \<Uplus> D) = (A \<le> C \<and> B \<le> D)
[PROOF STEP]
by (auto simp: less_eq_V_def)


[STATEMENT]
lemma sum_equal_iff:
  fixes A :: V shows "A\<Uplus>B = C\<Uplus>D \<longleftrightarrow> A=C \<and> B=D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<Uplus> B = C \<Uplus> D) = (A = C \<and> B = D)
[PROOF STEP]
by (simp add: eq_iff sum_subset_iff)


[STATEMENT]
lemma sum_case_Inl [simp]: "sum_case f g (Inl x) = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_case f g (ZFC_Cardinals.Inl x) = f x
[PROOF STEP]
by (simp add: sum_case_def is_sum_def)