theory Ctac

lemma Catch_ceqv:
  assumes ca: "\<And>t t'. ceqv \<Gamma> xf v t t' a a'"
  and     cb: "\<And>t t'. ceqv \<Gamma> xf v t t' b b'"
  and     xp: "xpres_strong \<Gamma> xf v a pnorm True abnormal"
  shows   "ceqv \<Gamma> xf v t t' (Catch a b) (Catch a' b')" apply (rule ceqvI) apply rule apply (erule exec_Normal_elim_cases) apply (drule (1) ceqvD1 [OF _ _ ca]) apply (rule exec.CatchMatch, assumption) apply (erule ceqvD1 [OF _ _ cb]) apply (erule (1) xpres_exec_Abrupt[OF xpres_ceqv[OF xp ca] TrueI]) apply (rule exec.CatchMiss) apply (erule (1) ceqvD1 [OF _ _ ca]) apply assumption apply (erule exec_Normal_elim_cases) apply (drule (1) ceqvD2 [OF _ _ ca]) apply (rule exec.CatchMatch, assumption) apply (erule ceqvD2 [OF _ _ cb]) apply (rule xpres_exec_Abrupt[OF xpres_ceqv[OF xp ca] TrueI, rotated], assumption) apply (erule (1) ceqvD1 [OF _ _ ca]) apply (rule exec.CatchMiss) apply (erule (1) ceqvD2 [OF _ _ ca]) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv \<Gamma> xf v t t' (TRY
  a
CATCH b
END) (TRY
  a'
CATCH b'
END) proof (prove)
goal (1 subgoal):
 1. xf t = v \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a
CATCH b
END,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>TRY
  a'
CATCH b'
END,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>TRY
  a
CATCH b
END,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a'
CATCH b'
END,Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>TRY
  a'
CATCH b'
END,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a
CATCH b
END,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> Abrupt s'; \<Gamma>\<turnstile> \<langle>b,Normal s'\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a'
CATCH b'
END,Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> t'; \<not> isAbr t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a'
CATCH b'
END,Normal t\<rangle> \<Rightarrow> t'
 3. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>TRY
  a'
CATCH b'
END,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a
CATCH b
END,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>b,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> Abrupt s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a'
CATCH b'
END,Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> t'; \<not> isAbr t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a'
CATCH b'
END,Normal t\<rangle> \<Rightarrow> t'
 3. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>TRY
  a'
CATCH b'
END,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a
CATCH b
END,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>b,Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> Abrupt s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b',Normal s'\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> t'; \<not> isAbr t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a'
CATCH b'
END,Normal t\<rangle> \<Rightarrow> t'
 3. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>TRY
  a'
CATCH b'
END,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a
CATCH b
END,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> Abrupt s'\<rbrakk> \<Longrightarrow> xf s' = v
 2. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> t'; \<not> isAbr t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a'
CATCH b'
END,Normal t\<rangle> \<Rightarrow> t'
 3. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>TRY
  a'
CATCH b'
END,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a
CATCH b
END,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> t'; \<not> isAbr t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a'
CATCH b'
END,Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>TRY
  a'
CATCH b'
END,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a
CATCH b
END,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> t'; \<not> isAbr t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> t'; \<not> isAbr t'\<rbrakk> \<Longrightarrow> \<not> isAbr t'
 3. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>TRY
  a'
CATCH b'
END,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a
CATCH b
END,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> t'; \<not> isAbr t'\<rbrakk> \<Longrightarrow> \<not> isAbr t'
 2. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>TRY
  a'
CATCH b'
END,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a
CATCH b
END,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>TRY
  a'
CATCH b'
END,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a
CATCH b
END,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> Abrupt s'; \<Gamma>\<turnstile> \<langle>b',Normal s'\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a
CATCH b
END,Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> t'; \<not> isAbr t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a
CATCH b
END,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>b',Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> Abrupt s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a
CATCH b
END,Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> t'; \<not> isAbr t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a
CATCH b
END,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>b',Normal s'\<rangle> \<Rightarrow> t'; \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> Abrupt s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,Normal s'\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> t'; \<not> isAbr t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a
CATCH b
END,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> Abrupt s'\<rbrakk> \<Longrightarrow> xf s' = v
 2. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> t'; \<not> isAbr t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a
CATCH b
END,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> Abrupt s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> Abrupt s'
 2. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> t'; \<not> isAbr t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a
CATCH b
END,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> t'; \<not> isAbr t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  a
CATCH b
END,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> t'; \<not> isAbr t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a,Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> t'; \<not> isAbr t'\<rbrakk> \<Longrightarrow> \<not> isAbr t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>a',Normal t\<rangle> \<Rightarrow> t'; \<not> isAbr t'\<rbrakk> \<Longrightarrow> \<not> isAbr t' proof (prove)
goal:
No subgoals!