theory Simpl_Rewrite

lemma com_eq_While':
  assumes eq: "c \<sim> c'"
  assumes W: "\<Gamma> \<turnstile> \<langle>While b c,s\<rangle> \<Rightarrow> s'"
  shows "\<Gamma> \<turnstile> \<langle>While b c',s\<rangle> \<Rightarrow> s'" using W proof (induct "While b c" s s') case WhileTrue with eq show ?case unfolding com_eq_def by (auto elim: exec.WhileTrue) next case WhileFalse then show ?case by (rule exec.WhileFalse) qed auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b c',s\<rangle> \<Rightarrow> s' proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>While b c,s\<rangle> \<Rightarrow> s'

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b c',s\<rangle> \<Rightarrow> s' proof (state)
goal (5 subgoals):
 1. \<And>f. \<Gamma>\<turnstile> \<langle>While b c',Fault f\<rangle> \<Rightarrow> Fault f
 2. \<And>s s' t. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; c = While b c \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b c',Normal s\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<Gamma>\<turnstile> \<langle>While b c',s'\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b c',Normal s\<rangle> \<Rightarrow> t
 3. \<And>s. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b c',Normal s\<rangle> \<Rightarrow> Normal s
 4. \<Gamma>\<turnstile> \<langle>While b c',Stuck\<rangle> \<Rightarrow> Stuck
 5. \<And>s. \<Gamma>\<turnstile> \<langle>While b c',Abrupt s\<rangle> \<Rightarrow> Abrupt s proof (state)
this:
s_ \<in> b
\<Gamma>\<turnstile> \<langle>c,Normal s_\<rangle> \<Rightarrow> s'_
c = While b c \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b c',Normal s_\<rangle> \<Rightarrow> s'_
\<Gamma>\<turnstile> \<langle>While b c,s'_\<rangle> \<Rightarrow> t_
\<Gamma>\<turnstile> \<langle>While b c',s'_\<rangle> \<Rightarrow> t_

goal (5 subgoals):
 1. \<And>f. \<Gamma>\<turnstile> \<langle>While b c',Fault f\<rangle> \<Rightarrow> Fault f
 2. \<And>s s' t. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; c = While b c \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b c',Normal s\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; \<Gamma>\<turnstile> \<langle>While b c',s'\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b c',Normal s\<rangle> \<Rightarrow> t
 3. \<And>s. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b c',Normal s\<rangle> \<Rightarrow> Normal s
 4. \<Gamma>\<turnstile> \<langle>While b c',Stuck\<rangle> \<Rightarrow> Stuck
 5. \<And>s. \<Gamma>\<turnstile> \<langle>While b c',Abrupt s\<rangle> \<Rightarrow> Abrupt s proof (chain)
picking this:
c \<sim> c'
s_ \<in> b
\<Gamma>\<turnstile> \<langle>c,Normal s_\<rangle> \<Rightarrow> s'_
c = While b c \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b c',Normal s_\<rangle> \<Rightarrow> s'_
\<Gamma>\<turnstile> \<langle>While b c,s'_\<rangle> \<Rightarrow> t_
\<Gamma>\<turnstile> \<langle>While b c',s'_\<rangle> \<Rightarrow> t_ proof (prove)
using this:
c \<sim> c'
s_ \<in> b
\<Gamma>\<turnstile> \<langle>c,Normal s_\<rangle> \<Rightarrow> s'_
c = While b c \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b c',Normal s_\<rangle> \<Rightarrow> s'_
\<Gamma>\<turnstile> \<langle>While b c,s'_\<rangle> \<Rightarrow> t_
\<Gamma>\<turnstile> \<langle>While b c',s'_\<rangle> \<Rightarrow> t_

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b c',Normal s_\<rangle> \<Rightarrow> t_ proof (prove)
using this:
True \<longrightarrow> (\<forall>s s'. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>c',s\<rangle> \<Rightarrow> s')
s_ \<in> b
\<Gamma>\<turnstile> \<langle>c,Normal s_\<rangle> \<Rightarrow> s'_
c = While b c \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b c',Normal s_\<rangle> \<Rightarrow> s'_
\<Gamma>\<turnstile> \<langle>While b c,s'_\<rangle> \<Rightarrow> t_
\<Gamma>\<turnstile> \<langle>While b c',s'_\<rangle> \<Rightarrow> t_

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b c',Normal s_\<rangle> \<Rightarrow> t_ proof (state)
this:
\<Gamma>\<turnstile> \<langle>While b c',Normal s_\<rangle> \<Rightarrow> t_

goal (4 subgoals):
 1. \<And>f. \<Gamma>\<turnstile> \<langle>While b c',Fault f\<rangle> \<Rightarrow> Fault f
 2. \<And>s. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b c',Normal s\<rangle> \<Rightarrow> Normal s
 3. \<Gamma>\<turnstile> \<langle>While b c',Stuck\<rangle> \<Rightarrow> Stuck
 4. \<And>s. \<Gamma>\<turnstile> \<langle>While b c',Abrupt s\<rangle> \<Rightarrow> Abrupt s proof (state)
goal (4 subgoals):
 1. \<And>f. \<Gamma>\<turnstile> \<langle>While b c',Fault f\<rangle> \<Rightarrow> Fault f
 2. \<And>s. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b c',Normal s\<rangle> \<Rightarrow> Normal s
 3. \<Gamma>\<turnstile> \<langle>While b c',Stuck\<rangle> \<Rightarrow> Stuck
 4. \<And>s. \<Gamma>\<turnstile> \<langle>While b c',Abrupt s\<rangle> \<Rightarrow> Abrupt s proof (state)
this:
s_ \<notin> b

goal (4 subgoals):
 1. \<And>f. \<Gamma>\<turnstile> \<langle>While b c',Fault f\<rangle> \<Rightarrow> Fault f
 2. \<And>s. s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While b c',Normal s\<rangle> \<Rightarrow> Normal s
 3. \<Gamma>\<turnstile> \<langle>While b c',Stuck\<rangle> \<Rightarrow> Stuck
 4. \<And>s. \<Gamma>\<turnstile> \<langle>While b c',Abrupt s\<rangle> \<Rightarrow> Abrupt s proof (chain)
picking this:
s_ \<notin> b proof (prove)
using this:
s_ \<notin> b

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>While b c',Normal s_\<rangle> \<Rightarrow> Normal s_ proof (state)
this:
\<Gamma>\<turnstile> \<langle>While b c',Normal s_\<rangle> \<Rightarrow> Normal s_

goal (3 subgoals):
 1. \<And>f. \<Gamma>\<turnstile> \<langle>While b c',Fault f\<rangle> \<Rightarrow> Fault f
 2. \<Gamma>\<turnstile> \<langle>While b c',Stuck\<rangle> \<Rightarrow> Stuck
 3. \<And>s. \<Gamma>\<turnstile> \<langle>While b c',Abrupt s\<rangle> \<Rightarrow> Abrupt s