theory Corres_UL_C

lemma ccorresI':
  assumes rl: "\<And>s s' n z. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G'; \<Gamma> \<turnstile>\<^sub>h \<langle>c # hs, s'\<rangle> \<Rightarrow> (n, z); \<not> snd (m s)\<rbrakk> \<Longrightarrow>
  (\<exists>t'. z = Normal t' \<and> (\<exists>(r, t) \<in> fst (m s). (t, t') \<in> srel \<and> unif_rrel (n = length hs) rrel xf arrel axf r t'))"
  shows "ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c" unfolding ccorres_underlying_def apply - apply clarsimp apply (drule (4) rl) apply (case_tac t) apply simp apply simp apply simp apply simp done

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