theory Corres_UL_C

lemma ccorres_from_vcg_nofail0:
  "(\<forall>\<sigma>. \<Gamma> \<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> srel \<and> \<not> snd (a \<sigma>)}
  c
  {s. \<exists>(rv, \<sigma>') \<in> fst (a \<sigma>). (\<sigma>', s) \<in> srel \<and> rrel rv (xf s)})
  \<Longrightarrow> ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] a c" apply (rule ccorresI') apply (drule_tac x = s in spec) apply (drule hoare_sound) apply (simp add: HoarePartialDef.valid_def cvalid_def) apply (erule exec_handlers.cases) apply clarsimp apply (drule spec, drule spec, drule (1) mp) apply clarsimp apply clarsimp apply (drule spec, drule spec, drule (1) mp) apply clarsimp apply (erule bexI [rotated]) apply (simp add: unif_rrel_simps) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> srel \<and> \<not> snd (a \<sigma>)} c {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> srel \<and> rrel rv (xf s)} \<Longrightarrow> ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] a c proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>\<forall>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> srel \<and> \<not> snd (a \<sigma>)} c {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> srel \<and> rrel rv (xf s)}; (s, s') \<in> srel; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>[c],s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(r, t)\<in>fst (a s). (t, t') \<in> srel \<and> unif_rrel (n = length []) rrel xf arrel axf r t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> srel; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>[c],s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); \<Gamma>\<turnstile> {sa. P s \<and> sa \<in> P' \<and> (s, sa) \<in> srel \<and> \<not> snd (a s)} c {sa. \<exists>(rv, \<sigma>')\<in>fst (a s). (\<sigma>', sa) \<in> srel \<and> rrel rv (xf sa)}\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(r, t)\<in>fst (a s). (t, t') \<in> srel \<and> unif_rrel (n = length []) rrel xf arrel axf r t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> srel; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>[c],s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); \<Gamma>,{}\<Turnstile>\<^bsub>/{}\<^esub> {sa. P s \<and> sa \<in> P' \<and> (s, sa) \<in> srel \<and> \<not> snd (a s)} c {sa. \<exists>(rv, \<sigma>')\<in>fst (a s). (\<sigma>', sa) \<in> srel \<and> rrel rv (xf sa)},{}\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(r, t)\<in>fst (a s). (t, t') \<in> srel \<and> unif_rrel (n = length []) rrel xf arrel axf r t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> srel; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>[c],s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); \<forall>sa t. \<Gamma>\<turnstile> \<langle>c,sa\<rangle> \<Rightarrow> t \<longrightarrow> sa \<in> Normal ` {sa \<in> P'. (s, sa) \<in> srel} \<longrightarrow> t \<in> Normal ` {sa. \<exists>(rv, \<sigma>')\<in>fst (a s). (\<sigma>', sa) \<in> srel \<and> rrel rv (xf sa)}\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> unif_rrel (n = 0) rrel xf arrel axf r t') proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z h sa za hs na t. \<lbrakk>(s, s') \<in> srel; P s; s' \<in> P'; \<not> snd (a s); \<forall>sa t. \<Gamma>\<turnstile> \<langle>c,sa\<rangle> \<Rightarrow> t \<longrightarrow> sa \<in> Normal ` {sa \<in> P'. (s, sa) \<in> srel} \<longrightarrow> t \<in> Normal ` {sa. \<exists>(rv, \<sigma>')\<in>fst (a s). (\<sigma>', sa) \<in> srel \<and> rrel rv (xf sa)}; s' = sa; [c] = h # hs; n = na; z = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> Abrupt za; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,za\<rangle> \<Rightarrow> (na, t)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> unif_rrel (n = 0) rrel xf arrel axf r t')
 2. \<And>s s' n z h sa t hs. \<lbrakk>(s, s') \<in> srel; P s; s' \<in> P'; \<not> snd (a s); \<forall>sa t. \<Gamma>\<turnstile> \<langle>c,sa\<rangle> \<Rightarrow> t \<longrightarrow> sa \<in> Normal ` {sa \<in> P'. (s, sa) \<in> srel} \<longrightarrow> t \<in> Normal ` {sa. \<exists>(rv, \<sigma>')\<in>fst (a s). (\<sigma>', sa) \<in> srel \<and> rrel rv (xf sa)}; s' = sa; [c] = h # hs; n = length hs; z = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> unif_rrel (n = 0) rrel xf arrel axf r t')
 3. \<And>s s' n z sa. \<lbrakk>(s, s') \<in> srel; P s; s' \<in> P'; \<not> snd (a s); \<forall>sa t. \<Gamma>\<turnstile> \<langle>c,sa\<rangle> \<Rightarrow> t \<longrightarrow> sa \<in> Normal ` {sa \<in> P'. (s, sa) \<in> srel} \<longrightarrow> t \<in> Normal ` {sa. \<exists>(rv, \<sigma>')\<in>fst (a s). (\<sigma>', sa) \<in> srel \<and> rrel rv (xf sa)}; s' = sa; [c] = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> unif_rrel (n = 0) rrel xf arrel axf r t') proof (prove)
goal (3 subgoals):
 1. \<And>s sa za na t. \<lbrakk>(s, sa) \<in> srel; P s; sa \<in> P'; \<not> snd (a s); \<forall>sa t. \<Gamma>\<turnstile> \<langle>c,sa\<rangle> \<Rightarrow> t \<longrightarrow> sa \<in> Normal ` {sa \<in> P'. (s, sa) \<in> srel} \<longrightarrow> t \<in> Normal ` {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> srel \<and> rrel rv (xf sa)}; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> Abrupt za; \<Gamma>\<turnstile>\<^sub>h \<langle>[],za\<rangle> \<Rightarrow> (na, t)\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> unif_rrel (na = 0) rrel xf arrel axf r t')
 2. \<And>s s' n z h sa t hs. \<lbrakk>(s, s') \<in> srel; P s; s' \<in> P'; \<not> snd (a s); \<forall>sa t. \<Gamma>\<turnstile> \<langle>c,sa\<rangle> \<Rightarrow> t \<longrightarrow> sa \<in> Normal ` {sa \<in> P'. (s, sa) \<in> srel} \<longrightarrow> t \<in> Normal ` {sa. \<exists>(rv, \<sigma>')\<in>fst (a s). (\<sigma>', sa) \<in> srel \<and> rrel rv (xf sa)}; s' = sa; [c] = h # hs; n = length hs; z = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> unif_rrel (n = 0) rrel xf arrel axf r t')
 3. \<And>s s' n z sa. \<lbrakk>(s, s') \<in> srel; P s; s' \<in> P'; \<not> snd (a s); \<forall>sa t. \<Gamma>\<turnstile> \<langle>c,sa\<rangle> \<Rightarrow> t \<longrightarrow> sa \<in> Normal ` {sa \<in> P'. (s, sa) \<in> srel} \<longrightarrow> t \<in> Normal ` {sa. \<exists>(rv, \<sigma>')\<in>fst (a s). (\<sigma>', sa) \<in> srel \<and> rrel rv (xf sa)}; s' = sa; [c] = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> unif_rrel (n = 0) rrel xf arrel axf r t') proof (prove)
goal (3 subgoals):
 1. \<And>s sa za na t. \<lbrakk>(s, sa) \<in> srel; P s; sa \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> Abrupt za; \<Gamma>\<turnstile>\<^sub>h \<langle>[],za\<rangle> \<Rightarrow> (na, t); Normal sa \<in> Normal ` {sa \<in> P'. (s, sa) \<in> srel} \<longrightarrow> Abrupt za \<in> Normal ` {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> srel \<and> rrel rv (xf sa)}\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> unif_rrel (na = 0) rrel xf arrel axf r t')
 2. \<And>s s' n z h sa t hs. \<lbrakk>(s, s') \<in> srel; P s; s' \<in> P'; \<not> snd (a s); \<forall>sa t. \<Gamma>\<turnstile> \<langle>c,sa\<rangle> \<Rightarrow> t \<longrightarrow> sa \<in> Normal ` {sa \<in> P'. (s, sa) \<in> srel} \<longrightarrow> t \<in> Normal ` {sa. \<exists>(rv, \<sigma>')\<in>fst (a s). (\<sigma>', sa) \<in> srel \<and> rrel rv (xf sa)}; s' = sa; [c] = h # hs; n = length hs; z = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> unif_rrel (n = 0) rrel xf arrel axf r t')
 3. \<And>s s' n z sa. \<lbrakk>(s, s') \<in> srel; P s; s' \<in> P'; \<not> snd (a s); \<forall>sa t. \<Gamma>\<turnstile> \<langle>c,sa\<rangle> \<Rightarrow> t \<longrightarrow> sa \<in> Normal ` {sa \<in> P'. (s, sa) \<in> srel} \<longrightarrow> t \<in> Normal ` {sa. \<exists>(rv, \<sigma>')\<in>fst (a s). (\<sigma>', sa) \<in> srel \<and> rrel rv (xf sa)}; s' = sa; [c] = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> unif_rrel (n = 0) rrel xf arrel axf r t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z h sa t hs. \<lbrakk>(s, s') \<in> srel; P s; s' \<in> P'; \<not> snd (a s); \<forall>sa t. \<Gamma>\<turnstile> \<langle>c,sa\<rangle> \<Rightarrow> t \<longrightarrow> sa \<in> Normal ` {sa \<in> P'. (s, sa) \<in> srel} \<longrightarrow> t \<in> Normal ` {sa. \<exists>(rv, \<sigma>')\<in>fst (a s). (\<sigma>', sa) \<in> srel \<and> rrel rv (xf sa)}; s' = sa; [c] = h # hs; n = length hs; z = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> unif_rrel (n = 0) rrel xf arrel axf r t')
 2. \<And>s s' n z sa. \<lbrakk>(s, s') \<in> srel; P s; s' \<in> P'; \<not> snd (a s); \<forall>sa t. \<Gamma>\<turnstile> \<langle>c,sa\<rangle> \<Rightarrow> t \<longrightarrow> sa \<in> Normal ` {sa \<in> P'. (s, sa) \<in> srel} \<longrightarrow> t \<in> Normal ` {sa. \<exists>(rv, \<sigma>')\<in>fst (a s). (\<sigma>', sa) \<in> srel \<and> rrel rv (xf sa)}; s' = sa; [c] = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> unif_rrel (n = 0) rrel xf arrel axf r t') proof (prove)
goal (2 subgoals):
 1. \<And>s sa t. \<lbrakk>(s, sa) \<in> srel; P s; sa \<in> P'; \<not> snd (a s); \<forall>sa t. \<Gamma>\<turnstile> \<langle>c,sa\<rangle> \<Rightarrow> t \<longrightarrow> sa \<in> Normal ` {sa \<in> P'. (s, sa) \<in> srel} \<longrightarrow> t \<in> Normal ` {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> srel \<and> rrel rv (xf sa)}; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> unif_rrel True rrel xf arrel axf r t')
 2. \<And>s s' n z sa. \<lbrakk>(s, s') \<in> srel; P s; s' \<in> P'; \<not> snd (a s); \<forall>sa t. \<Gamma>\<turnstile> \<langle>c,sa\<rangle> \<Rightarrow> t \<longrightarrow> sa \<in> Normal ` {sa \<in> P'. (s, sa) \<in> srel} \<longrightarrow> t \<in> Normal ` {sa. \<exists>(rv, \<sigma>')\<in>fst (a s). (\<sigma>', sa) \<in> srel \<and> rrel rv (xf sa)}; s' = sa; [c] = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> unif_rrel (n = 0) rrel xf arrel axf r t') proof (prove)
goal (2 subgoals):
 1. \<And>s sa t. \<lbrakk>(s, sa) \<in> srel; P s; sa \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t; Normal sa \<in> Normal ` {sa \<in> P'. (s, sa) \<in> srel} \<longrightarrow> t \<in> Normal ` {sa. \<exists>x\<in>fst (a s). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', sa) \<in> srel \<and> rrel rv (xf sa)}\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> unif_rrel True rrel xf arrel axf r t')
 2. \<And>s s' n z sa. \<lbrakk>(s, s') \<in> srel; P s; s' \<in> P'; \<not> snd (a s); \<forall>sa t. \<Gamma>\<turnstile> \<langle>c,sa\<rangle> \<Rightarrow> t \<longrightarrow> sa \<in> Normal ` {sa \<in> P'. (s, sa) \<in> srel} \<longrightarrow> t \<in> Normal ` {sa. \<exists>(rv, \<sigma>')\<in>fst (a s). (\<sigma>', sa) \<in> srel \<and> rrel rv (xf sa)}; s' = sa; [c] = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> unif_rrel (n = 0) rrel xf arrel axf r t') proof (prove)
goal (2 subgoals):
 1. \<And>s sa x aa b. \<lbrakk>(s, sa) \<in> srel; P s; sa \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> Normal x; (aa, b) \<in> fst (a s); (b, x) \<in> srel; rrel aa (xf x)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (a s). case xa of (r, t) \<Rightarrow> (t, x) \<in> srel \<and> unif_rrel True rrel xf arrel axf r x
 2. \<And>s s' n z sa. \<lbrakk>(s, s') \<in> srel; P s; s' \<in> P'; \<not> snd (a s); \<forall>sa t. \<Gamma>\<turnstile> \<langle>c,sa\<rangle> \<Rightarrow> t \<longrightarrow> sa \<in> Normal ` {sa \<in> P'. (s, sa) \<in> srel} \<longrightarrow> t \<in> Normal ` {sa. \<exists>(rv, \<sigma>')\<in>fst (a s). (\<sigma>', sa) \<in> srel \<and> rrel rv (xf sa)}; s' = sa; [c] = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> unif_rrel (n = 0) rrel xf arrel axf r t') proof (prove)
goal (2 subgoals):
 1. \<And>s sa x aa b. \<lbrakk>(s, sa) \<in> srel; P s; sa \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> Normal x; (b, x) \<in> srel; rrel aa (xf x)\<rbrakk> \<Longrightarrow> case (aa, b) of (r, t) \<Rightarrow> (t, x) \<in> srel \<and> unif_rrel True rrel xf arrel axf r x
 2. \<And>s s' n z sa. \<lbrakk>(s, s') \<in> srel; P s; s' \<in> P'; \<not> snd (a s); \<forall>sa t. \<Gamma>\<turnstile> \<langle>c,sa\<rangle> \<Rightarrow> t \<longrightarrow> sa \<in> Normal ` {sa \<in> P'. (s, sa) \<in> srel} \<longrightarrow> t \<in> Normal ` {sa. \<exists>(rv, \<sigma>')\<in>fst (a s). (\<sigma>', sa) \<in> srel \<and> rrel rv (xf sa)}; s' = sa; [c] = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> unif_rrel (n = 0) rrel xf arrel axf r t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z sa. \<lbrakk>(s, s') \<in> srel; P s; s' \<in> P'; \<not> snd (a s); \<forall>sa t. \<Gamma>\<turnstile> \<langle>c,sa\<rangle> \<Rightarrow> t \<longrightarrow> sa \<in> Normal ` {sa \<in> P'. (s, sa) \<in> srel} \<longrightarrow> t \<in> Normal ` {sa. \<exists>(rv, \<sigma>')\<in>fst (a s). (\<sigma>', sa) \<in> srel \<and> rrel rv (xf sa)}; s' = sa; [c] = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> unif_rrel (n = 0) rrel xf arrel axf r t') proof (prove)
goal:
No subgoals!