theory Corres_UL_C

lemma ccorresI [case_names fail nofail]:
  assumes fc:
  "\<And>s s' n z. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (m s); \<Gamma> \<turnstile>\<^sub>h \<langle>c # hs, s'\<rangle> \<Rightarrow> (n, z); isAbr z \<or> isFault z \<or> z = Stuck \<rbrakk>
  \<Longrightarrow> False"
  and nfc: "\<And>n t' s s'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> G'; \<Gamma> \<turnstile>\<^sub>h \<langle>c # hs, s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (m s)\<rbrakk>
  \<Longrightarrow> (\<exists>(r, t) \<in> fst (m s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) rrel xf arrel axf r t')"
  shows "ccorres_underlying sr \<Gamma> rrel xf arrel axf G G' hs m c" unfolding ccorres_underlying_def apply - apply clarsimp apply (case_tac t) apply simp apply (erule(4) nfc) apply simp apply (erule (4) fc) apply simp apply simp apply (erule (4) fc) apply simp apply simp apply (erule (4) fc) apply simp done

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