theory Ctac

lemma ceqv_remove_eqv_skip':
  "\<lbrakk> \<And>s. ceqv \<Gamma> xf v s s' b Skip; \<And>s'. ceqv \<Gamma> xf v s s' a a'; xpres \<Gamma> xf v a \<rbrakk> \<Longrightarrow>
     ceqv \<Gamma> xf v s s' (a ;; b) a'" apply (rule ceqv_trans) apply (erule Seq_ceqv [OF ceqv_refl]) apply (simp add: xpres_ceqv) apply (clarsimp simp add: ceqv_def) apply (rule iffI) apply (erule exec_elim_cases, simp_all) apply (auto elim!: exec_elim_cases)[1] apply (rule exec.intros, simp) apply (cases s', simp_all) apply (rule exec.intros) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. ceqv \<Gamma> xf v s s' b SKIP; \<And>s'. ceqv \<Gamma> xf v s s' a a'; xpres \<Gamma> xf v a\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf v s s' (a;;
b) a' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s. ceqv \<Gamma> xf v s s' b SKIP; \<And>s'. ceqv \<Gamma> xf v s s' a a'; xpres \<Gamma> xf v a\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf v s s' (a;;
b) ?c'
 2. \<lbrakk>\<And>s. ceqv \<Gamma> xf v s s' b SKIP; \<And>s'. ceqv \<Gamma> xf v s s' a a'; xpres \<Gamma> xf v a\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf v s s' ?c' a' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s'. ceqv \<Gamma> xf v s s' a a'; xpres \<Gamma> xf v a\<rbrakk> \<Longrightarrow> xpres_strong \<Gamma> xf v a True ?pres_abr3 ?abnormal3
 2. \<lbrakk>\<And>s. ceqv \<Gamma> xf v s s' b SKIP; \<And>s'. ceqv \<Gamma> xf v s s' a a'; xpres \<Gamma> xf v a\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf v s s' (a;;
SKIP) a' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. ceqv \<Gamma> xf v s s' b SKIP; \<And>s'. ceqv \<Gamma> xf v s s' a a'; xpres \<Gamma> xf v a\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf v s s' (a;;
SKIP) a' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>sa. xf sa = xf s \<longrightarrow> \<Gamma>\<turnstile> \<langle>b,Normal sa\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>SKIP,Normal sa\<rangle> \<Rightarrow> s'; \<And>s'. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s'; xpres \<Gamma> xf (xf s) a; v = xf s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
SKIP,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>sa. xf sa = xf s \<longrightarrow> \<Gamma>\<turnstile> \<langle>b,Normal sa\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>SKIP,Normal sa\<rangle> \<Rightarrow> s'; \<And>s'. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s'; xpres \<Gamma> xf (xf s) a; v = xf s; \<Gamma>\<turnstile> \<langle>a;;
SKIP,Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s'
 2. \<lbrakk>\<And>sa. xf sa = xf s \<longrightarrow> \<Gamma>\<turnstile> \<langle>b,Normal sa\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>SKIP,Normal sa\<rangle> \<Rightarrow> s'; \<And>s'. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s'; xpres \<Gamma> xf (xf s) a; v = xf s; \<Gamma>\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
SKIP,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<And>sa s'a. \<lbrakk>\<And>s. xf s = xf sa \<longrightarrow> \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>SKIP,Normal s\<rangle> \<Rightarrow> s'; \<And>s'. \<Gamma>\<turnstile> \<langle>a,Normal sa\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>a',Normal sa\<rangle> \<Rightarrow> s'; xpres \<Gamma> xf (xf sa) a; v = xf sa; s = sa; \<Gamma>\<turnstile> \<langle>a',Normal sa\<rangle> \<Rightarrow> s'a; \<Gamma>\<turnstile> \<langle>SKIP,s'a\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a',Normal sa\<rangle> \<Rightarrow> s'
 2. \<lbrakk>\<And>sa. xf sa = xf s \<longrightarrow> \<Gamma>\<turnstile> \<langle>b,Normal sa\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>SKIP,Normal sa\<rangle> \<Rightarrow> s'; \<And>s'. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s'; xpres \<Gamma> xf (xf s) a; v = xf s; \<Gamma>\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
SKIP,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>sa. xf sa = xf s \<longrightarrow> \<Gamma>\<turnstile> \<langle>b,Normal sa\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>SKIP,Normal sa\<rangle> \<Rightarrow> s'; \<And>s'. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s'; xpres \<Gamma> xf (xf s) a; v = xf s; \<Gamma>\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
SKIP,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>sa. xf sa = xf s \<longrightarrow> \<Gamma>\<turnstile> \<langle>b,Normal sa\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>SKIP,Normal sa\<rangle> \<Rightarrow> s'; \<And>s'. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s'; xpres \<Gamma> xf (xf s) a; v = xf s; \<Gamma>\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>SKIP,s'\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<And>x1. \<lbrakk>\<And>sa. xf sa = xf s \<longrightarrow> \<Gamma>\<turnstile> \<langle>b,Normal sa\<rangle> \<Rightarrow> Normal x1 = \<Gamma>\<turnstile> \<langle>SKIP,Normal sa\<rangle> \<Rightarrow> Normal x1; \<And>s'. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s'; xpres \<Gamma> xf (xf s) a; v = xf s; \<Gamma>\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> Normal x1; s' = Normal x1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>SKIP,Normal x1\<rangle> \<Rightarrow> Normal x1 proof (prove)
goal:
No subgoals!