theory Corres_UL_C

lemma exec_handlers_SkipD:
  "\<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs, s\<rangle> \<Rightarrow> (n, s') \<Longrightarrow> s' = Normal s \<and> n = length hs" apply (erule exec_handlers.cases) apply clarsimp apply (erule exec_Normal_elim_cases) apply simp apply clarsimp apply (erule exec_Normal_elim_cases) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^sub>h \<langle>SKIP # hs,s\<rangle> \<Rightarrow> (n, s') \<Longrightarrow> s' = Normal s \<and> n = length hs proof (prove)
goal (3 subgoals):
 1. \<And>h sa z hsa na t. \<lbrakk>s = sa; SKIP # hs = h # hsa; n = na; s' = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (na, t)\<rbrakk> \<Longrightarrow> s' = Normal s \<and> n = length hs
 2. \<And>h sa t hsa. \<lbrakk>s = sa; SKIP # hs = h # hsa; n = length hsa; s' = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> s' = Normal s \<and> n = length hs
 3. \<And>sa. \<lbrakk>s = sa; SKIP # hs = []; n = 0; s' = Abrupt sa\<rbrakk> \<Longrightarrow> s' = Normal s \<and> n = length hs proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>\<Gamma>\<turnstile> \<langle>SKIP,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (n, s')\<rbrakk> \<Longrightarrow> s' = Normal s \<and> n = length hs
 2. \<And>h sa t hsa. \<lbrakk>s = sa; SKIP # hs = h # hsa; n = length hsa; s' = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> s' = Normal s \<and> n = length hs
 3. \<And>sa. \<lbrakk>s = sa; SKIP # hs = []; n = 0; s' = Abrupt sa\<rbrakk> \<Longrightarrow> s' = Normal s \<and> n = length hs proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>\<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (n, s'); Abrupt z = Normal s\<rbrakk> \<Longrightarrow> s' = Normal s \<and> n = length hs
 2. \<And>h sa t hsa. \<lbrakk>s = sa; SKIP # hs = h # hsa; n = length hsa; s' = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> s' = Normal s \<and> n = length hs
 3. \<And>sa. \<lbrakk>s = sa; SKIP # hs = []; n = 0; s' = Abrupt sa\<rbrakk> \<Longrightarrow> s' = Normal s \<and> n = length hs proof (prove)
goal (2 subgoals):
 1. \<And>h sa t hsa. \<lbrakk>s = sa; SKIP # hs = h # hsa; n = length hsa; s' = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> s' = Normal s \<and> n = length hs
 2. \<And>sa. \<lbrakk>s = sa; SKIP # hs = []; n = 0; s' = Abrupt sa\<rbrakk> \<Longrightarrow> s' = Normal s \<and> n = length hs proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n = length hs; \<Gamma>\<turnstile> \<langle>SKIP,Normal s\<rangle> \<Rightarrow> s'; \<not> isAbr s'\<rbrakk> \<Longrightarrow> s' = Normal s
 2. \<And>sa. \<lbrakk>s = sa; SKIP # hs = []; n = 0; s' = Abrupt sa\<rbrakk> \<Longrightarrow> s' = Normal s \<and> n = length hs proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n = length hs; \<not> isAbr s'; s' = Normal s\<rbrakk> \<Longrightarrow> s' = Normal s
 2. \<And>sa. \<lbrakk>s = sa; SKIP # hs = []; n = 0; s' = Abrupt sa\<rbrakk> \<Longrightarrow> s' = Normal s \<and> n = length hs proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>s = sa; SKIP # hs = []; n = 0; s' = Abrupt sa\<rbrakk> \<Longrightarrow> s' = Normal s \<and> n = length hs proof (prove)
goal:
No subgoals!