theory Corres_UL_C

lemma ccorresE:
  assumes cc: "ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c"
  and ps: "(s, s') \<in> srel" "G s" "s' \<in> G'"  "\<not> snd (m s)" "\<Gamma>\<turnstile>\<^sub>h \<langle>c#hs , s'\<rangle> \<Rightarrow> (n, x)"
  and nc: "\<And>t' r t. \<lbrakk>x = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel;
                           unif_rrel (n = length hs) rrel xf arrel axf r t';
                           n \<le> length hs \<rbrakk> \<Longrightarrow> P"
  shows P using cc ps nc unfolding ccorres_underlying_def apply clarsimp apply (drule (1) bspec) apply simp apply (elim allE, drule (1) mp) apply (cases x) apply (clarsimp dest!: exec_handlers_Cons_le) apply simp apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P proof (prove)
using this:
ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c
(s, s') \<in> srel
G s
s' \<in> G'
\<not> snd (m s)
\<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, x)
\<lbrakk>x = Normal ?t'; (?r, ?t) \<in> fst (m s); (?t, ?t') \<in> srel; unif_rrel (n = length hs) rrel xf arrel axf ?r ?t'; n \<le> length hs\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P proof (prove)
using this:
\<forall>(s, s')\<in>srel. G s \<and> s' \<in> G' \<and> \<not> snd (m s) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (m s). (t, s'') \<in> srel \<and> unif_rrel (n = length hs) rrel xf arrel axf r s'' | _ \<Rightarrow> False))
(s, s') \<in> srel
G s
s' \<in> G'
\<not> snd (m s)
\<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, x)
\<lbrakk>x = Normal ?t'; (?r, ?t) \<in> fst (m s); (?t, ?t') \<in> srel; unif_rrel (n = length hs) rrel xf arrel axf ?r ?t'; n \<le> length hs\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>srel. case x of (s, s') \<Rightarrow> G s \<and> s' \<in> G' \<and> \<not> snd (m s) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (m s). (t, s'') \<in> srel \<and> unif_rrel (n = length hs) rrel xf arrel axf r s'' | _ \<Rightarrow> False)); (s, s') \<in> srel; G s; s' \<in> G'; \<not> snd (m s); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, x); \<And>t' r t. \<lbrakk>x = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (n = length hs) rrel xf arrel axf r t'; n \<le> length hs\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G'; \<not> snd (m s); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, x); \<And>t' r t. \<lbrakk>x = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (n = length hs) rrel xf arrel axf r t'; n \<le> length hs\<rbrakk> \<Longrightarrow> P; case (s, s') of (s, s') \<Rightarrow> G s \<and> s' \<in> G' \<and> \<not> snd (m s) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (m s). (t, s'') \<in> srel \<and> unif_rrel (n = length hs) rrel xf arrel axf r s'' | _ \<Rightarrow> False))\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G'; \<not> snd (m s); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, x); \<And>t' r t. \<lbrakk>x = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (n = length hs) rrel xf arrel axf r t'; n \<le> length hs\<rbrakk> \<Longrightarrow> P; \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (m s). (t, s'') \<in> srel \<and> unif_rrel (n = length hs) rrel xf arrel axf r s'' | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G'; \<not> snd (m s); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, x); \<And>t' r t. \<lbrakk>x = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (n = length hs) rrel xf arrel axf r t'; n \<le> length hs\<rbrakk> \<Longrightarrow> P; case x of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (m s). (t, s'') \<in> srel \<and> unif_rrel (n = length hs) rrel xf arrel axf r s'' | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> P proof (prove)
goal (4 subgoals):
 1. \<And>x1. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G'; \<not> snd (m s); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, x); \<And>t' r t. \<lbrakk>x = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (n = length hs) rrel xf arrel axf r t'; n \<le> length hs\<rbrakk> \<Longrightarrow> P; case x of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (m s). (t, s'') \<in> srel \<and> unif_rrel (n = length hs) rrel xf arrel axf r s'' | _ \<Rightarrow> False; x = Normal x1\<rbrakk> \<Longrightarrow> P
 2. \<And>x2. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G'; \<not> snd (m s); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, x); \<And>t' r t. \<lbrakk>x = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (n = length hs) rrel xf arrel axf r t'; n \<le> length hs\<rbrakk> \<Longrightarrow> P; case x of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (m s). (t, s'') \<in> srel \<and> unif_rrel (n = length hs) rrel xf arrel axf r s'' | _ \<Rightarrow> False; x = Abrupt x2\<rbrakk> \<Longrightarrow> P
 3. \<And>x3. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G'; \<not> snd (m s); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, x); \<And>t' r t. \<lbrakk>x = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (n = length hs) rrel xf arrel axf r t'; n \<le> length hs\<rbrakk> \<Longrightarrow> P; case x of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (m s). (t, s'') \<in> srel \<and> unif_rrel (n = length hs) rrel xf arrel axf r s'' | _ \<Rightarrow> False; x = Fault x3\<rbrakk> \<Longrightarrow> P
 4. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G'; \<not> snd (m s); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, x); \<And>t' r t. \<lbrakk>x = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (n = length hs) rrel xf arrel axf r t'; n \<le> length hs\<rbrakk> \<Longrightarrow> P; case x of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (m s). (t, s'') \<in> srel \<and> unif_rrel (n = length hs) rrel xf arrel axf r s'' | _ \<Rightarrow> False; x = Stuck\<rbrakk> \<Longrightarrow> P proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G'; \<not> snd (m s); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, x); \<And>t' r t. \<lbrakk>x = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (n = length hs) rrel xf arrel axf r t'; n \<le> length hs\<rbrakk> \<Longrightarrow> P; case x of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (m s). (t, s'') \<in> srel \<and> unif_rrel (n = length hs) rrel xf arrel axf r s'' | _ \<Rightarrow> False; x = Abrupt x2\<rbrakk> \<Longrightarrow> P
 2. \<And>x3. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G'; \<not> snd (m s); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, x); \<And>t' r t. \<lbrakk>x = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (n = length hs) rrel xf arrel axf r t'; n \<le> length hs\<rbrakk> \<Longrightarrow> P; case x of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (m s). (t, s'') \<in> srel \<and> unif_rrel (n = length hs) rrel xf arrel axf r s'' | _ \<Rightarrow> False; x = Fault x3\<rbrakk> \<Longrightarrow> P
 3. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G'; \<not> snd (m s); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, x); \<And>t' r t. \<lbrakk>x = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (n = length hs) rrel xf arrel axf r t'; n \<le> length hs\<rbrakk> \<Longrightarrow> P; case x of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (m s). (t, s'') \<in> srel \<and> unif_rrel (n = length hs) rrel xf arrel axf r s'' | _ \<Rightarrow> False; x = Stuck\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<And>x3. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G'; \<not> snd (m s); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, x); \<And>t' r t. \<lbrakk>x = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (n = length hs) rrel xf arrel axf r t'; n \<le> length hs\<rbrakk> \<Longrightarrow> P; case x of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (m s). (t, s'') \<in> srel \<and> unif_rrel (n = length hs) rrel xf arrel axf r s'' | _ \<Rightarrow> False; x = Fault x3\<rbrakk> \<Longrightarrow> P
 2. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G'; \<not> snd (m s); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, x); \<And>t' r t. \<lbrakk>x = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (n = length hs) rrel xf arrel axf r t'; n \<le> length hs\<rbrakk> \<Longrightarrow> P; case x of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (m s). (t, s'') \<in> srel \<and> unif_rrel (n = length hs) rrel xf arrel axf r s'' | _ \<Rightarrow> False; x = Stuck\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G'; \<not> snd (m s); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, x); \<And>t' r t. \<lbrakk>x = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (n = length hs) rrel xf arrel axf r t'; n \<le> length hs\<rbrakk> \<Longrightarrow> P; case x of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (m s). (t, s'') \<in> srel \<and> unif_rrel (n = length hs) rrel xf arrel axf r s'' | _ \<Rightarrow> False; x = Stuck\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals!