theory SIMPL_Lemmas

lemma exec_Seq_cong:
  "\<lbrakk> \<And>s''. \<Gamma> \<turnstile> \<langle>a, Normal s\<rangle> \<Rightarrow> s'' = \<Gamma> \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> s'';
     \<And>s''. \<Gamma> \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> Normal s''
         \<Longrightarrow> \<Gamma> \<turnstile> \<langle>b, Normal s''\<rangle> \<Rightarrow> s' = \<Gamma> \<turnstile> \<langle>d, Normal s''\<rangle> \<Rightarrow> s' \<rbrakk>
       \<Longrightarrow> \<Gamma> \<turnstile> \<langle>a ;; b, Normal s\<rangle> \<Rightarrow> s' = \<Gamma> \<turnstile> \<langle>c ;; d, Normal s\<rangle> \<Rightarrow> s'" apply (rule iffI) apply (erule exec_Normal_elim_cases) apply (case_tac "s'a", auto elim!: exec_elim_cases intro: exec.intros)[1] apply (erule exec_Normal_elim_cases) apply (case_tac "s'a", auto elim!: exec_elim_cases intro: exec.intros)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s''. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'' = \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s''; \<And>s''. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal s'' \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,Normal s''\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>d,Normal s''\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>c;;
d,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s''. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'' = \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s''; \<And>s''. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal s'' \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,Normal s''\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>d,Normal s''\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>a;;
b,Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c;;
d,Normal s\<rangle> \<Rightarrow> s'
 2. \<lbrakk>\<And>s''. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'' = \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s''; \<And>s''. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal s'' \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,Normal s''\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>d,Normal s''\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>c;;
d,Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<And>s'a. \<lbrakk>\<And>s''. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'' = \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s''; \<And>s''. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal s'' \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,Normal s''\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>d,Normal s''\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'a; \<Gamma>\<turnstile> \<langle>b,s'a\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c;;
d,Normal s\<rangle> \<Rightarrow> s'
 2. \<lbrakk>\<And>s''. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'' = \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s''; \<And>s''. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal s'' \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,Normal s''\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>d,Normal s''\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>c;;
d,Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s''. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'' = \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s''; \<And>s''. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal s'' \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,Normal s''\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>d,Normal s''\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>c;;
d,Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<And>s'a. \<lbrakk>\<And>s''. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'' = \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s''; \<And>s''. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal s'' \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,Normal s''\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>d,Normal s''\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'a; \<Gamma>\<turnstile> \<langle>d,s'a\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!