theory Corres_UL_C

lemma ccorres_empty_handler_abrupt':
  assumes cc: "ccorres_underlying sr \<Gamma> rrel xf' arrel axf P P' [] a c"
  and   asms: "(s, s') \<in> sr" "P s" "s' \<in> P'" "\<not> snd (a s)"
  and     eh: "\<Gamma> \<turnstile>\<^sub>h \<langle>c # hs, s'\<rangle> \<Rightarrow> (n, t)"
  shows   "\<not> isAbr t" using cc asms eh apply - apply (erule exec_handlers.cases) apply clarsimp apply (frule (5) ccorres_empty_handler_abrupt) apply simp apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> isAbr t proof (prove)
using this:
ccorres_underlying sr \<Gamma> rrel xf' arrel axf P P' [] a c
(s, s') \<in> sr
P s
s' \<in> P'
\<not> snd (a s)
\<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, t)

goal (1 subgoal):
 1. \<not> isAbr t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorres_underlying sr \<Gamma> rrel xf' arrel axf P P' [] a c; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> \<not> isAbr t proof (prove)
goal (3 subgoals):
 1. \<And>h sa z hsa na ta. \<lbrakk>ccorres_underlying sr \<Gamma> rrel xf' arrel axf P P' [] a c; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; c # hs = h # hsa; n = na; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (na, ta)\<rbrakk> \<Longrightarrow> \<not> isAbr t
 2. \<And>h sa ta hsa. \<lbrakk>ccorres_underlying sr \<Gamma> rrel xf' arrel axf P P' [] a c; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; c # hs = h # hsa; n = length hsa; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> \<not> isAbr t
 3. \<And>sa. \<lbrakk>ccorres_underlying sr \<Gamma> rrel xf' arrel axf P P' [] a c; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; c # hs = []; n = 0; t = Abrupt sa\<rbrakk> \<Longrightarrow> \<not> isAbr t proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>ccorres_underlying sr \<Gamma> rrel xf' arrel axf P P' [] a c; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (n, t); isAbr t\<rbrakk> \<Longrightarrow> False
 2. \<And>h sa ta hsa. \<lbrakk>ccorres_underlying sr \<Gamma> rrel xf' arrel axf P P' [] a c; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; c # hs = h # hsa; n = length hsa; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> \<not> isAbr t
 3. \<And>sa. \<lbrakk>ccorres_underlying sr \<Gamma> rrel xf' arrel axf P P' [] a c; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; c # hs = []; n = 0; t = Abrupt sa\<rbrakk> \<Longrightarrow> \<not> isAbr t proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>ccorres_underlying sr \<Gamma> rrel xf' arrel axf P P' [] a c; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (n, t); isAbr t; \<not> isAbr (Abrupt z)\<rbrakk> \<Longrightarrow> False
 2. \<And>h sa ta hsa. \<lbrakk>ccorres_underlying sr \<Gamma> rrel xf' arrel axf P P' [] a c; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; c # hs = h # hsa; n = length hsa; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> \<not> isAbr t
 3. \<And>sa. \<lbrakk>ccorres_underlying sr \<Gamma> rrel xf' arrel axf P P' [] a c; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; c # hs = []; n = 0; t = Abrupt sa\<rbrakk> \<Longrightarrow> \<not> isAbr t proof (prove)
goal (2 subgoals):
 1. \<And>h sa ta hsa. \<lbrakk>ccorres_underlying sr \<Gamma> rrel xf' arrel axf P P' [] a c; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; c # hs = h # hsa; n = length hsa; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> \<not> isAbr t
 2. \<And>sa. \<lbrakk>ccorres_underlying sr \<Gamma> rrel xf' arrel axf P P' [] a c; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; c # hs = []; n = 0; t = Abrupt sa\<rbrakk> \<Longrightarrow> \<not> isAbr t proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>ccorres_underlying sr \<Gamma> rrel xf' arrel axf P P' [] a c; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; c # hs = []; n = 0; t = Abrupt sa\<rbrakk> \<Longrightarrow> \<not> isAbr t proof (prove)
goal:
No subgoals!