theory SIMPL_Lemmas

lemma Abrupt_result:
  "\<Gamma> \<turnstile> \<langle>c, s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'" proof (induct c arbitrary: s) case While thus ?case by - (erule exec_elim_cases, simp_all) qed (fastforce elim: exec_elim_cases)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t' proof (state)
goal (11 subgoals):
 1. \<And>s. \<Gamma>\<turnstile> \<langle>SKIP,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 2. \<And>x s. \<Gamma>\<turnstile> \<langle>Basic x,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 3. \<And>x s. \<Gamma>\<turnstile> \<langle>Spec x,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 4. \<And>c1 c2 s. \<lbrakk>\<And>s. \<Gamma>\<turnstile> \<langle>c1,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'; \<And>s. \<Gamma>\<turnstile> \<langle>c2,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'; \<Gamma>\<turnstile> \<langle>c1;;
c2,s\<rangle> \<Rightarrow> Abrupt t'\<rbrakk> \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 5. \<And>x1 c1 c2 s. \<lbrakk>\<And>s. \<Gamma>\<turnstile> \<langle>c1,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'; \<And>s. \<Gamma>\<turnstile> \<langle>c2,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'; \<Gamma>\<turnstile> \<langle>Cond x1 c1 c2,s\<rangle> \<Rightarrow> Abrupt t'\<rbrakk> \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 6. \<And>x1 c s. \<lbrakk>\<And>s. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'; \<Gamma>\<turnstile> \<langle>While x1 c,s\<rangle> \<Rightarrow> Abrupt t'\<rbrakk> \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 7. \<And>x s. \<Gamma>\<turnstile> \<langle>Call x,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 8. \<And>x s. \<lbrakk>\<And>xa s. \<lbrakk>xa \<in> range x; \<Gamma>\<turnstile> \<langle>xa,s\<rangle> \<Rightarrow> Abrupt t'\<rbrakk> \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'; \<Gamma>\<turnstile> \<langle>DynCom x,s\<rangle> \<Rightarrow> Abrupt t'\<rbrakk> \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 9. \<And>x1 x2a c s. \<lbrakk>\<And>s. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'; \<Gamma>\<turnstile> \<langle>Guard x1 x2a c,s\<rangle> \<Rightarrow> Abrupt t'\<rbrakk> \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 10. \<And>s. \<Gamma>\<turnstile> \<langle>THROW,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
A total of 11 subgoals... proof (state)
this:
\<Gamma>\<turnstile> \<langle>c_,?s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. ?s = Normal t) \<or> ?s = Abrupt t'
\<Gamma>\<turnstile> \<langle>While x1_ c_,s\<rangle> \<Rightarrow> Abrupt t'

goal (11 subgoals):
 1. \<And>s. \<Gamma>\<turnstile> \<langle>SKIP,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 2. \<And>x s. \<Gamma>\<turnstile> \<langle>Basic x,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 3. \<And>x s. \<Gamma>\<turnstile> \<langle>Spec x,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 4. \<And>c1 c2 s. \<lbrakk>\<And>s. \<Gamma>\<turnstile> \<langle>c1,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'; \<And>s. \<Gamma>\<turnstile> \<langle>c2,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'; \<Gamma>\<turnstile> \<langle>c1;;
c2,s\<rangle> \<Rightarrow> Abrupt t'\<rbrakk> \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 5. \<And>x1 c1 c2 s. \<lbrakk>\<And>s. \<Gamma>\<turnstile> \<langle>c1,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'; \<And>s. \<Gamma>\<turnstile> \<langle>c2,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'; \<Gamma>\<turnstile> \<langle>Cond x1 c1 c2,s\<rangle> \<Rightarrow> Abrupt t'\<rbrakk> \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 6. \<And>x1 c s. \<lbrakk>\<And>s. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'; \<Gamma>\<turnstile> \<langle>While x1 c,s\<rangle> \<Rightarrow> Abrupt t'\<rbrakk> \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 7. \<And>x s. \<Gamma>\<turnstile> \<langle>Call x,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 8. \<And>x s. \<lbrakk>\<And>xa s. \<lbrakk>xa \<in> range x; \<Gamma>\<turnstile> \<langle>xa,s\<rangle> \<Rightarrow> Abrupt t'\<rbrakk> \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'; \<Gamma>\<turnstile> \<langle>DynCom x,s\<rangle> \<Rightarrow> Abrupt t'\<rbrakk> \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 9. \<And>x1 x2a c s. \<lbrakk>\<And>s. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'; \<Gamma>\<turnstile> \<langle>Guard x1 x2a c,s\<rangle> \<Rightarrow> Abrupt t'\<rbrakk> \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 10. \<And>s. \<Gamma>\<turnstile> \<langle>THROW,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
A total of 11 subgoals... proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>c_,?s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. ?s = Normal t) \<or> ?s = Abrupt t'
\<Gamma>\<turnstile> \<langle>While x1_ c_,s\<rangle> \<Rightarrow> Abrupt t'

goal (1 subgoal):
 1. (\<exists>t. s = Normal t) \<or> s = Abrupt t' proof (state)
this:
(\<exists>t. s = Normal t) \<or> s = Abrupt t'

goal (10 subgoals):
 1. \<And>s. \<Gamma>\<turnstile> \<langle>SKIP,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 2. \<And>x s. \<Gamma>\<turnstile> \<langle>Basic x,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 3. \<And>x s. \<Gamma>\<turnstile> \<langle>Spec x,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 4. \<And>c1 c2 s. \<lbrakk>\<And>s. \<Gamma>\<turnstile> \<langle>c1,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'; \<And>s. \<Gamma>\<turnstile> \<langle>c2,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'; \<Gamma>\<turnstile> \<langle>c1;;
c2,s\<rangle> \<Rightarrow> Abrupt t'\<rbrakk> \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 5. \<And>x1 c1 c2 s. \<lbrakk>\<And>s. \<Gamma>\<turnstile> \<langle>c1,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'; \<And>s. \<Gamma>\<turnstile> \<langle>c2,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'; \<Gamma>\<turnstile> \<langle>Cond x1 c1 c2,s\<rangle> \<Rightarrow> Abrupt t'\<rbrakk> \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 6. \<And>x s. \<Gamma>\<turnstile> \<langle>Call x,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 7. \<And>x s. \<lbrakk>\<And>xa s. \<lbrakk>xa \<in> range x; \<Gamma>\<turnstile> \<langle>xa,s\<rangle> \<Rightarrow> Abrupt t'\<rbrakk> \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'; \<Gamma>\<turnstile> \<langle>DynCom x,s\<rangle> \<Rightarrow> Abrupt t'\<rbrakk> \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 8. \<And>x1 x2a c s. \<lbrakk>\<And>s. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'; \<Gamma>\<turnstile> \<langle>Guard x1 x2a c,s\<rangle> \<Rightarrow> Abrupt t'\<rbrakk> \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 9. \<And>s. \<Gamma>\<turnstile> \<langle>THROW,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'
 10. \<And>c1 c2 s. \<lbrakk>\<And>s. \<Gamma>\<turnstile> \<langle>c1,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'; \<And>s. \<Gamma>\<turnstile> \<langle>c2,s\<rangle> \<Rightarrow> Abrupt t' \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'; \<Gamma>\<turnstile> \<langle>TRY
  c1
CATCH c2
END,s\<rangle> \<Rightarrow> Abrupt t'\<rbrakk> \<Longrightarrow> (\<exists>t. s = Normal t) \<or> s = Abrupt t'