theory Corres_C

lemma wfhandlers_ccatchbrk:
  "wfhandlers (catchbrk_C # hs) = wfhandlers hs" unfolding wfhandlers_def ccatchbrk_def apply rule apply (intro allI impI) apply (drule_tac x = \<Gamma> in spec) apply ((drule spec)+, erule mp) apply simp apply (rule EHAbrupt) apply rule apply simp apply rule apply fastforce apply (intro allI impI) apply (drule_tac x = \<Gamma> in spec) apply ((drule spec)+, erule mp) apply simp apply (erule conjE) apply (erule exec_handlers.cases) apply (fastforce elim: exec_Normal_elim_cases)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wfhandlers (catchbrk_C # hs) = wfhandlers hs proof (prove)
goal (1 subgoal):
 1. (\<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s) = (\<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s) proof (prove)
goal (2 subgoals):
 1. \<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s \<Longrightarrow> \<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s
 2. \<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s \<Longrightarrow> \<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s proof (prove)
goal (2 subgoals):
 1. \<And>\<Gamma> s t n. \<lbrakk>\<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s; global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> t = Normal s
 2. \<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s \<Longrightarrow> \<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s proof (prove)
goal (2 subgoals):
 1. \<And>\<Gamma> s t n. \<lbrakk>global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t); \<forall>s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s\<rbrakk> \<Longrightarrow> t = Normal s
 2. \<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s \<Longrightarrow> \<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s proof (prove)
goal (2 subgoals):
 1. \<And>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<Longrightarrow> global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,s\<rangle> \<Rightarrow> (?n14 \<Gamma> s t n, t)
 2. \<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s \<Longrightarrow> \<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s proof (prove)
goal (2 subgoals):
 1. \<And>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,s\<rangle> \<Rightarrow> (?n14 \<Gamma> s t n, t)
 2. \<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s \<Longrightarrow> \<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s proof (prove)
goal (3 subgoals):
 1. \<And>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<Longrightarrow> \<Gamma>\<turnstile> \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI,Normal s\<rangle> \<Rightarrow> Abrupt (?z18 \<Gamma> s t n)
 2. \<And>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,?z18 \<Gamma> s t n\<rangle> \<Rightarrow> (?n14 \<Gamma> s t n, t)
 3. \<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s \<Longrightarrow> \<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s proof (prove)
goal (4 subgoals):
 1. \<And>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<Longrightarrow> s \<notin> \<lbrace>\<acute>global_exn_var = Break\<rbrace>
 2. \<And>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<Longrightarrow> \<Gamma>\<turnstile> \<langle>THROW,Normal s\<rangle> \<Rightarrow> Abrupt (?z18 \<Gamma> s t n)
 3. \<And>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,?z18 \<Gamma> s t n\<rangle> \<Rightarrow> (?n14 \<Gamma> s t n, t)
 4. \<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s \<Longrightarrow> \<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s proof (prove)
goal (3 subgoals):
 1. \<And>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<Longrightarrow> \<Gamma>\<turnstile> \<langle>THROW,Normal s\<rangle> \<Rightarrow> Abrupt (?z18 \<Gamma> s t n)
 2. \<And>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,?z18 \<Gamma> s t n\<rangle> \<Rightarrow> (?n14 \<Gamma> s t n, t)
 3. \<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s \<Longrightarrow> \<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s proof (prove)
goal (2 subgoals):
 1. \<And>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (?n14 \<Gamma> s t n, t)
 2. \<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s \<Longrightarrow> \<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s proof (prove)
goal (1 subgoal):
 1. \<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s \<Longrightarrow> \<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s proof (prove)
goal (1 subgoal):
 1. \<And>\<Gamma> s t n. \<lbrakk>\<forall>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s; global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,s\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> t = Normal s proof (prove)
goal (1 subgoal):
 1. \<And>\<Gamma> s t n. \<lbrakk>global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,s\<rangle> \<Rightarrow> (n, t); \<forall>s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> t = Normal s\<rbrakk> \<Longrightarrow> t = Normal s proof (prove)
goal (1 subgoal):
 1. \<And>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,s\<rangle> \<Rightarrow> (n, t) \<Longrightarrow> global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (?n39 \<Gamma> s t n, t) proof (prove)
goal (1 subgoal):
 1. \<And>\<Gamma> s t n. global_exn_var_' s = Return \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,s\<rangle> \<Rightarrow> (n, t) \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (?n39 \<Gamma> s t n, t) proof (prove)
goal (1 subgoal):
 1. \<And>\<Gamma> s t n. \<lbrakk>global_exn_var_' s = Return; \<Gamma>\<turnstile>\<^sub>h \<langle>IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs,s\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (?n39 \<Gamma> s t n, t) proof (prove)
goal (3 subgoals):
 1. \<And>\<Gamma> s t n h sa z hsa na ta. \<lbrakk>global_exn_var_' s = Return; s = sa; IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs = h # hsa; n = na; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (na, ta)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (?n39 \<Gamma> s t n, t)
 2. \<And>\<Gamma> s t n h sa ta hsa. \<lbrakk>global_exn_var_' s = Return; s = sa; IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs = h # hsa; n = length hsa; t = ta; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> ta; \<not> isAbr ta\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (?n39 \<Gamma> s t n, t)
 3. \<And>\<Gamma> s t n sa. \<lbrakk>global_exn_var_' s = Return; s = sa; IF \<acute>global_exn_var = Break THEN
  SKIP
ELSE
  THROW
FI # hs = []; n = 0; t = Abrupt sa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s\<rangle> \<Rightarrow> (?n39 \<Gamma> s t n, t) proof (prove)
goal:
No subgoals!