theory Ctac

lemma Cond_ceqv:
  assumes be: "\<And>t. xf t = v \<longrightarrow> (t \<in> x) = (t \<in> x')"
  and     ca: "ceqv \<Gamma> xf v t t' a a'"
  and     cb: "ceqv \<Gamma> xf v t t' b b'"
  shows   "ceqv \<Gamma> xf v t t' (Cond x a b) (Cond x' a' b')" apply (rule ceqvI) apply rule apply (erule exec_Normal_elim_cases) apply (frule (1) iffD1 [OF be [rule_format]]) apply (erule exec.CondTrue) apply (erule (1) ceqvD1 [OF _ _ ca]) apply (subst (asm) be) apply assumption apply (erule exec.CondFalse) apply (erule (1) ceqvD1 [OF _ _ cb]) 
  (* clag *)
    apply (erule exec_Normal_elim_cases) apply (frule (1) iffD2 [OF be [ rule_format]]) apply (erule exec.CondTrue) apply (erule (1) ceqvD2 [OF _ _ ca]) apply (subst (asm) be [rule_format, symmetric]) apply assumption apply (erule exec.CondFalse) apply (erule (1) ceqvD2 [OF _ _ cb]) done

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