theory Corres_UL_C

lemma exec_handlers_use_hoare_nothrow:
  assumes valid': "E \<turnstile>\<^bsub>/F\<^esub> R' c Q', {}"
  and         ce: "E \<turnstile>\<^sub>h \<langle>c # hs, s'\<rangle> \<Rightarrow> (n, t)"
  and       asms: "s' \<in> R'"
  shows   "(t \<in> Normal ` Q' \<or> t \<in> Fault ` F) \<and> n = length hs" using valid' ce asms apply - apply (drule hoare_sound) apply (clarsimp elim: exec_Normal_elim_cases
    simp: Nondet_Monad.bind_def cvalid_def split_def HoarePartialDef.valid_def) apply (erule exec_handlers.cases) apply clarsimp apply (drule spec, drule spec, drule (1) mp) apply fastforce apply clarsimp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (t \<in> Normal ` Q' \<or> t \<in> Fault ` F) \<and> n = length hs proof (prove)
using this:
E\<turnstile>\<^bsub>/F\<^esub> R' c Q'
E\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, t)
s' \<in> R'

goal (1 subgoal):
 1. (t \<in> Normal ` Q' \<or> t \<in> Fault ` F) \<and> n = length hs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>E\<turnstile>\<^bsub>/F\<^esub> R' c Q'; E\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, t); s' \<in> R'\<rbrakk> \<Longrightarrow> (t \<in> Normal ` Q' \<or> t \<in> Fault ` F) \<and> n = length hs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>E\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, t); s' \<in> R'; E,{}\<Turnstile>\<^bsub>/F\<^esub> R' c Q',{}\<rbrakk> \<Longrightarrow> (t \<in> Normal ` Q' \<or> t \<in> Fault ` F) \<and> n = length hs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>E\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, t); s' \<in> R'; \<forall>s t. E\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` R' \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q'\<rbrakk> \<Longrightarrow> (t \<in> Normal ` Q' \<or> t \<in> Fault ` F) \<and> n = length hs proof (prove)
goal (3 subgoals):
 1. \<And>h s z hsa na ta. \<lbrakk>s' \<in> R'; \<forall>s t. E\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` R' \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q'; s' = s; c # hs = h # hsa; n = na; t = ta; E\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> Abrupt z; E\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (na, ta)\<rbrakk> \<Longrightarrow> (t \<in> Normal ` Q' \<or> t \<in> Fault ` F) \<and> n = length hs
 2. \<And>h s ta hsa. \<lbrakk>s' \<in> R'; \<forall>s t. E\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` R' \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q'; s' = s; c # hs = h # hsa; n = length hsa; t = ta; E\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> (t \<in> Normal ` Q' \<or> t \<in> Fault ` F) \<and> n = length hs
 3. \<And>s. \<lbrakk>s' \<in> R'; \<forall>s t. E\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` R' \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q'; s' = s; c # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> (t \<in> Normal ` Q' \<or> t \<in> Fault ` F) \<and> n = length hs proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>s' \<in> R'; \<forall>s t. E\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` R' \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q'; E\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt z; E\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> (t \<in> Normal ` Q' \<or> t \<in> Fault ` F) \<and> n = length hs
 2. \<And>h s ta hsa. \<lbrakk>s' \<in> R'; \<forall>s t. E\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` R' \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q'; s' = s; c # hs = h # hsa; n = length hsa; t = ta; E\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> (t \<in> Normal ` Q' \<or> t \<in> Fault ` F) \<and> n = length hs
 3. \<And>s. \<lbrakk>s' \<in> R'; \<forall>s t. E\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` R' \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q'; s' = s; c # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> (t \<in> Normal ` Q' \<or> t \<in> Fault ` F) \<and> n = length hs proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>s' \<in> R'; E\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Abrupt z; E\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (n, t); Normal s' \<in> Normal ` R' \<longrightarrow> Abrupt z \<notin> Fault ` F \<longrightarrow> Abrupt z \<in> Normal ` Q'\<rbrakk> \<Longrightarrow> (t \<in> Normal ` Q' \<or> t \<in> Fault ` F) \<and> n = length hs
 2. \<And>h s ta hsa. \<lbrakk>s' \<in> R'; \<forall>s t. E\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` R' \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q'; s' = s; c # hs = h # hsa; n = length hsa; t = ta; E\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> (t \<in> Normal ` Q' \<or> t \<in> Fault ` F) \<and> n = length hs
 3. \<And>s. \<lbrakk>s' \<in> R'; \<forall>s t. E\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` R' \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q'; s' = s; c # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> (t \<in> Normal ` Q' \<or> t \<in> Fault ` F) \<and> n = length hs proof (prove)
goal (2 subgoals):
 1. \<And>h s ta hsa. \<lbrakk>s' \<in> R'; \<forall>s t. E\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` R' \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q'; s' = s; c # hs = h # hsa; n = length hsa; t = ta; E\<turnstile> \<langle>h,Normal s\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> (t \<in> Normal ` Q' \<or> t \<in> Fault ` F) \<and> n = length hs
 2. \<And>s. \<lbrakk>s' \<in> R'; \<forall>s t. E\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` R' \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q'; s' = s; c # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> (t \<in> Normal ` Q' \<or> t \<in> Fault ` F) \<and> n = length hs proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s' \<in> R'; \<forall>s t. E\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` R' \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q'; s' = s; c # hs = []; n = 0; t = Abrupt s\<rbrakk> \<Longrightarrow> (t \<in> Normal ` Q' \<or> t \<in> Fault ` F) \<and> n = length hs proof (prove)
goal:
No subgoals!