theory Ctac

lemma Seq_weak_ceqv: (* A weaker form where xpres doesn't hold for a *)
  assumes ra: "\<And>t'. ceqv \<Gamma> xf v t t' a a'"
  shows   "ceqv \<Gamma> xf v t t' (a ;; b) (a' ;; b)" apply - apply (rule ceqvI) apply rule apply (erule exec_Normal_elim_cases) apply rule apply (erule (2) ceqvD1 [OF _ _ ra]) 
  (* clag *)
    apply (erule exec_Normal_elim_cases) apply rule apply (erule (2) ceqvD2 [OF _ _ ra]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv \<Gamma> xf v t t' (a;;
b) (a';;
b) proof (prove)
goal (1 subgoal):
 1. ceqv \<Gamma> xf v t t' (a;;
b) (a';;
b) proof (prove)
goal (1 subgoal):
 1. xf t = v \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>a';;
b,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a;;
b,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a';;
b,Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a';;
b,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a';;
b,Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a';;
b,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> ?s'7 s'
 2. \<And>s'. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,?s'7 s'\<rangle> \<Rightarrow> t'
 3. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a';;
b,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a';;
b,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a';;
b,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a;;
b,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> ?s'17 s'
 2. \<And>s'. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>b,s'\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,?s'17 s'\<rangle> \<Rightarrow> t' proof (prove)
goal:
No subgoals!