theory Ctac

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. ceqv \<Gamma> xf () s s' b SKIP) \<Longrightarrow> ceqv \<Gamma> xf () s s' (a;;
b) a proof (prove)
goal (2 subgoals):
 1. (\<And>s. ceqv \<Gamma> xf () s s' b SKIP) \<Longrightarrow> ceqv \<Gamma> xf () s s' (a;;
b) ?c'
 2. (\<And>s. ceqv \<Gamma> xf () s s' b SKIP) \<Longrightarrow> ceqv \<Gamma> xf () s s' ?c' a proof (prove)
goal (2 subgoals):
 1. xpres_strong \<Gamma> xf () a True ?pres_abr3 False
 2. (\<And>s. ceqv \<Gamma> xf () s s' b SKIP) \<Longrightarrow> ceqv \<Gamma> xf () s s' (a;;
SKIP) a proof (prove)
goal (1 subgoal):
 1. (\<And>s. ceqv \<Gamma> xf () s s' b SKIP) \<Longrightarrow> ceqv \<Gamma> xf () s s' (a;;
SKIP) a proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>SKIP,Normal s\<rangle> \<Rightarrow> s') \<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>s. \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>SKIP,Normal s\<rangle> \<Rightarrow> 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>s. \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>SKIP,Normal s\<rangle> \<Rightarrow> 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>s. \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>SKIP,Normal s\<rangle> \<Rightarrow> 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. (\<And>s. \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>SKIP,Normal s\<rangle> \<Rightarrow> s') \<Longrightarrow> \<Gamma>\<turnstile> \<langle>SKIP,s'\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<And>x1. \<lbrakk>\<And>s. \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> Normal x1 = \<Gamma>\<turnstile> \<langle>SKIP,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!