theory Corres_UL_C

lemma ceqvhD1:
  assumes lhs: "\<Gamma> \<turnstile>\<^sub>h \<langle>a # hs, s\<rangle> \<Rightarrow> (n, s')"
  and     xf:  "xf s = v"
  and     ceq: "\<And>s'. ceqv \<Gamma> xf v s s' a b"
  shows   "\<Gamma> \<turnstile>\<^sub>h \<langle>b # hs, s\<rangle> \<Rightarrow> (n, s')" using lhs xf apply - apply (ind_cases "\<Gamma> \<turnstile>\<^sub>h \<langle>a # hs, s\<rangle> \<Rightarrow> (n, s')") apply (rule EHAbrupt) apply (erule (1) ceqvD1 [OF _ _ ceq]) apply assumption apply simp apply (rule EHOther) apply (erule (1) ceqvD1 [OF _ _ ceq]) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^sub>h \<langle>b # hs,s\<rangle> \<Rightarrow> (n, s') proof (prove)
using this:
\<Gamma>\<turnstile>\<^sub>h \<langle>a # hs,s\<rangle> \<Rightarrow> (n, s')
xf s = v

goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^sub>h \<langle>b # hs,s\<rangle> \<Rightarrow> (n, s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile>\<^sub>h \<langle>a # hs,s\<rangle> \<Rightarrow> (n, s'); xf s = v\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>b # hs,s\<rangle> \<Rightarrow> (n, s') proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>xf s = v; \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (n, s')\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>b # hs,s\<rangle> \<Rightarrow> (n, s')
 2. \<lbrakk>xf s = v; n = length hs; \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'; \<not> isAbr s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>b # hs,s\<rangle> \<Rightarrow> (n, s') proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>xf s = v; \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (n, s')\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> Abrupt (?z5 z)
 2. \<And>z. \<lbrakk>xf s = v; \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (n, s')\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,?z5 z\<rangle> \<Rightarrow> (n, s')
 3. \<lbrakk>xf s = v; n = length hs; \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'; \<not> isAbr s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>b # hs,s\<rangle> \<Rightarrow> (n, s') proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>xf s = v; \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (n, s')\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (n, s')
 2. \<lbrakk>xf s = v; n = length hs; \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'; \<not> isAbr s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>b # hs,s\<rangle> \<Rightarrow> (n, s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xf s = v; n = length hs; \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'; \<not> isAbr s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>b # hs,s\<rangle> \<Rightarrow> (n, s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xf s = v; n = length hs; \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'; \<not> isAbr s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>b # hs,s\<rangle> \<Rightarrow> (length hs, s') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xf s = v; n = length hs; \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'; \<not> isAbr s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s'
 2. \<lbrakk>xf s = v; n = length hs; \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'; \<not> isAbr s'\<rbrakk> \<Longrightarrow> \<not> isAbr s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xf s = v; n = length hs; \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'; \<not> isAbr s'\<rbrakk> \<Longrightarrow> \<not> isAbr s' proof (prove)
goal:
No subgoals!