theory Ctac

lemma Guard_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'"
  shows   "ceqv \<Gamma> xf v t t' (Guard f x a) (Guard f x' a')" apply (rule ceqvI) apply rule apply (erule exec_Normal_elim_cases) apply (frule (1) iffD1 [OF be [rule_format]]) apply (erule exec.Guard) apply (erule (1) ceqvD1 [OF _ _ ca]) apply (subst (asm) be) apply assumption apply simp apply (erule exec.GuardFault) apply (erule exec_Normal_elim_cases) apply (frule (1) iffD2 [OF be [rule_format]]) apply (erule exec.Guard) apply (erule (1) ceqvD2 [OF _ _ ca]) apply (subst (asm) be [rule_format, symmetric]) apply assumption apply simp apply (erule exec.GuardFault) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv \<Gamma> xf v t t' (Guard f x a) (Guard f x' a') proof (prove)
goal (1 subgoal):
 1. xf t = v \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x a,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>Guard f x' a',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>Guard f x a,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x' a',Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>Guard f x' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x a,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>Guard f x' a',Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xf t = v; t' = Fault f; t \<notin> x\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x' a',Normal t\<rangle> \<Rightarrow> t'
 3. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>Guard f x' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x a,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>Guard f x' a',Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xf t = v; t' = Fault f; t \<notin> x\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x' a',Normal t\<rangle> \<Rightarrow> t'
 3. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>Guard f x' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x a,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' = Fault f; t \<notin> x\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x' a',Normal t\<rangle> \<Rightarrow> t'
 3. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>Guard f x' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x a,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xf t = v; t' = Fault f; t \<notin> x\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x' a',Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>Guard f x' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x a,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>xf t = v; t' = Fault f\<rbrakk> \<Longrightarrow> xf t = v
 2. \<lbrakk>xf t = v; t' = Fault f; t \<notin> x'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x' a',Normal t\<rangle> \<Rightarrow> t'
 3. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>Guard f x' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x a,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xf t = v; t' = Fault f; t \<notin> x'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x' a',Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>Guard f x' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x a,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xf t = v; t' = Fault f; t \<notin> x'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x' a',Normal t\<rangle> \<Rightarrow> Fault f
 2. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>Guard f x' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x a,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>Guard f x' a',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x a,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>Guard f x a,Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xf t = v; t' = Fault f; t \<notin> x'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x a,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>Guard f x a,Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xf t = v; t' = Fault f; t \<notin> x'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x a,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' = Fault f; t \<notin> x'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x a,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xf t = v; t' = Fault f; t \<notin> x'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x a,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xf t = v; t' = Fault f\<rbrakk> \<Longrightarrow> xf t = v
 2. \<lbrakk>xf t = v; t' = Fault f; t \<notin> x\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x a,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xf t = v; t' = Fault f; t \<notin> x\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x a,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xf t = v; t' = Fault f; t \<notin> x\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Guard f x a,Normal t\<rangle> \<Rightarrow> Fault f proof (prove)
goal:
No subgoals!