theory SIMPL_Lemmas

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

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

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

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