[STATEMENT]
lemma step_preserves_sconf:
assumes wf: "wf_C_prog P" and step: "P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>"
shows "\<And>T. \<lbrakk> P,E,hp s \<turnstile> e : T; P,E \<turnstile> s \<surd> \<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>T. \<lbrakk>P,E,hp s \<turnstile> e : T; P,E \<turnstile> s \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>

goal (1 subgoal):
 1. \<And>T. \<lbrakk>P,E,hp s \<turnstile> e : T; P,E \<turnstile> s \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
proof (induct rule:converse_rtrancl_induct2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>T. \<lbrakk>P,E,hp s' \<turnstile> e' : T; P,E \<turnstile> s' \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
 2. \<And>a b aa ba T. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E,hp ba \<turnstile> aa : T; P,E \<turnstile> ba \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,hp b \<turnstile> a : T; P,E \<turnstile> b \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
case refl
[PROOF STATE]
proof (state)
this:
P,E,hp s' \<turnstile> e' : T
P,E \<turnstile> s' \<surd>

goal (2 subgoals):
 1. \<And>T. \<lbrakk>P,E,hp s' \<turnstile> e' : T; P,E \<turnstile> s' \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
 2. \<And>a b aa ba T. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E,hp ba \<turnstile> aa : T; P,E \<turnstile> ba \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,hp b \<turnstile> a : T; P,E \<turnstile> b \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,E \<turnstile> s' \<surd>
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> s' \<surd>

goal (1 subgoal):
 1. \<And>a b aa ba T. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E,hp ba \<turnstile> aa : T; P,E \<turnstile> ba \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,hp b \<turnstile> a : T; P,E \<turnstile> b \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba T. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E,hp ba \<turnstile> aa : T; P,E \<turnstile> ba \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,hp b \<turnstile> a : T; P,E \<turnstile> b \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
case step
[PROOF STATE]
proof (state)
this:
((a___, b___), a_, b_) \<in> Red P E
P,E \<turnstile> \<langle>a_,b_\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>
\<lbrakk>P,E,hp b_ \<turnstile> a_ : ?T; P,E \<turnstile> b_ \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
P,E,hp b___ \<turnstile> a___ : T
P,E \<turnstile> b___ \<surd>

goal (1 subgoal):
 1. \<And>a b aa ba T. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E,hp ba \<turnstile> aa : T; P,E \<turnstile> ba \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,hp b \<turnstile> a : T; P,E \<turnstile> b \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
((a___, b___), a_, b_) \<in> Red P E
P,E \<turnstile> \<langle>a_,b_\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>
\<lbrakk>P,E,hp b_ \<turnstile> a_ : ?T; P,E \<turnstile> b_ \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
P,E,hp b___ \<turnstile> a___ : T
P,E \<turnstile> b___ \<surd>

goal (1 subgoal):
 1. P,E \<turnstile> s' \<surd>
[PROOF STEP]
using wf
[PROOF STATE]
proof (prove)
using this:
((a___, b___), a_, b_) \<in> Red P E
P,E \<turnstile> \<langle>a_,b_\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>
\<lbrakk>P,E,hp b_ \<turnstile> a_ : ?T; P,E \<turnstile> b_ \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
P,E,hp b___ \<turnstile> a___ : T
P,E \<turnstile> b___ \<surd>
wf_C_prog P

goal (1 subgoal):
 1. P,E \<turnstile> s' \<surd>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,E \<turnstile> \<langle>a___,b___\<rangle> \<rightarrow> \<langle>a_,b_\<rangle>; P,E \<turnstile> \<langle>a_,b_\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E,fst b_ \<turnstile> a_ : T; P,E \<turnstile> b_ \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,fst b___ \<turnstile> a___ : T; P,E \<turnstile> b___ \<surd>; wf_C_prog P\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
apply (frule subject_reduction[OF wf])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>P,E \<turnstile> \<langle>a___,b___\<rangle> \<rightarrow> \<langle>a_,b_\<rangle>; P,E \<turnstile> \<langle>a_,b_\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E,fst b_ \<turnstile> a_ : T; P,E \<turnstile> b_ \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,fst b___ \<turnstile> a___ : T; P,E \<turnstile> b___ \<surd>; wf_C_prog P\<rbrakk> \<Longrightarrow> P,E \<turnstile> b___ \<surd>
 2. \<lbrakk>P,E \<turnstile> \<langle>a___,b___\<rangle> \<rightarrow> \<langle>a_,b_\<rangle>; P,E \<turnstile> \<langle>a_,b_\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E,fst b_ \<turnstile> a_ : T; P,E \<turnstile> b_ \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,fst b___ \<turnstile> a___ : T; P,E \<turnstile> b___ \<surd>; wf_C_prog P\<rbrakk> \<Longrightarrow> P,E,hp b___ \<turnstile> a___ : ?T7
 3. \<lbrakk>P,E \<turnstile> \<langle>a___,b___\<rangle> \<rightarrow> \<langle>a_,b_\<rangle>; P,E \<turnstile> \<langle>a_,b_\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E,fst b_ \<turnstile> a_ : T; P,E \<turnstile> b_ \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,fst b___ \<turnstile> a___ : T; P,E \<turnstile> b___ \<surd>; wf_C_prog P; P,E,hp b_ \<turnstile> a_ :\<^bsub>NT\<^esub> ?T7\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
apply (rule step.prems)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P,E \<turnstile> \<langle>a___,b___\<rangle> \<rightarrow> \<langle>a_,b_\<rangle>; P,E \<turnstile> \<langle>a_,b_\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E,fst b_ \<turnstile> a_ : T; P,E \<turnstile> b_ \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,fst b___ \<turnstile> a___ : T; P,E \<turnstile> b___ \<surd>; wf_C_prog P\<rbrakk> \<Longrightarrow> P,E,hp b___ \<turnstile> a___ : ?T7
 2. \<lbrakk>P,E \<turnstile> \<langle>a___,b___\<rangle> \<rightarrow> \<langle>a_,b_\<rangle>; P,E \<turnstile> \<langle>a_,b_\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E,fst b_ \<turnstile> a_ : T; P,E \<turnstile> b_ \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,fst b___ \<turnstile> a___ : T; P,E \<turnstile> b___ \<surd>; wf_C_prog P; P,E,hp b_ \<turnstile> a_ :\<^bsub>NT\<^esub> ?T7\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
apply (rule step.prems)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,E \<turnstile> \<langle>a___,b___\<rangle> \<rightarrow> \<langle>a_,b_\<rangle>; P,E \<turnstile> \<langle>a_,b_\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E,fst b_ \<turnstile> a_ : T; P,E \<turnstile> b_ \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,fst b___ \<turnstile> a___ : T; P,E \<turnstile> b___ \<surd>; wf_C_prog P; P,E,hp b_ \<turnstile> a_ :\<^bsub>NT\<^esub> T\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
apply (cases T)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>P,E \<turnstile> \<langle>a___,b___\<rangle> \<rightarrow> \<langle>a_,b_\<rangle>; P,E \<turnstile> \<langle>a_,b_\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E,fst b_ \<turnstile> a_ : T; P,E \<turnstile> b_ \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,fst b___ \<turnstile> a___ : T; P,E \<turnstile> b___ \<surd>; wf_C_prog P; P,E,hp b_ \<turnstile> a_ :\<^bsub>NT\<^esub> T; T = Void\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
 2. \<lbrakk>P,E \<turnstile> \<langle>a___,b___\<rangle> \<rightarrow> \<langle>a_,b_\<rangle>; P,E \<turnstile> \<langle>a_,b_\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E,fst b_ \<turnstile> a_ : T; P,E \<turnstile> b_ \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,fst b___ \<turnstile> a___ : T; P,E \<turnstile> b___ \<surd>; wf_C_prog P; P,E,hp b_ \<turnstile> a_ :\<^bsub>NT\<^esub> T; T = Boolean\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
 3. \<lbrakk>P,E \<turnstile> \<langle>a___,b___\<rangle> \<rightarrow> \<langle>a_,b_\<rangle>; P,E \<turnstile> \<langle>a_,b_\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E,fst b_ \<turnstile> a_ : T; P,E \<turnstile> b_ \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,fst b___ \<turnstile> a___ : T; P,E \<turnstile> b___ \<surd>; wf_C_prog P; P,E,hp b_ \<turnstile> a_ :\<^bsub>NT\<^esub> T; T = Integer\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
 4. \<lbrakk>P,E \<turnstile> \<langle>a___,b___\<rangle> \<rightarrow> \<langle>a_,b_\<rangle>; P,E \<turnstile> \<langle>a_,b_\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E,fst b_ \<turnstile> a_ : T; P,E \<turnstile> b_ \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,fst b___ \<turnstile> a___ : T; P,E \<turnstile> b___ \<surd>; wf_C_prog P; P,E,hp b_ \<turnstile> a_ :\<^bsub>NT\<^esub> T; T = NT\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
 5. \<And>x5. \<lbrakk>P,E \<turnstile> \<langle>a___,b___\<rangle> \<rightarrow> \<langle>a_,b_\<rangle>; P,E \<turnstile> \<langle>a_,b_\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E,fst b_ \<turnstile> a_ : T; P,E \<turnstile> b_ \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,fst b___ \<turnstile> a___ : T; P,E \<turnstile> b___ \<surd>; wf_C_prog P; P,E,hp b_ \<turnstile> a_ :\<^bsub>NT\<^esub> T; T = Class x5\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
apply (auto dest:red_preserves_sconf intro:wf_prog_wwf_prog)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> s' \<surd>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma steps_preserves_sconf:
assumes wf: "wf_C_prog P" and step: "P,E \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>"
shows "\<And>Ts. \<lbrakk> P,E,hp s \<turnstile> es [:] Ts; P,E \<turnstile> s \<surd> \<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Ts. \<lbrakk>P,E,hp s \<turnstile> es [:] Ts; P,E \<turnstile> s \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>

goal (1 subgoal):
 1. \<And>Ts. \<lbrakk>P,E,hp s \<turnstile> es [:] Ts; P,E \<turnstile> s \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
proof (induct rule:converse_rtrancl_induct2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Ts. \<lbrakk>P,E,hp s' \<turnstile> es' [:] Ts; P,E \<turnstile> s' \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
 2. \<And>a b aa ba Ts. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; \<And>Ts. \<lbrakk>P,E,hp ba \<turnstile> aa [:] Ts; P,E \<turnstile> ba \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,hp b \<turnstile> a [:] Ts; P,E \<turnstile> b \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
case refl
[PROOF STATE]
proof (state)
this:
P,E,hp s' \<turnstile> es' [:] Ts
P,E \<turnstile> s' \<surd>

goal (2 subgoals):
 1. \<And>Ts. \<lbrakk>P,E,hp s' \<turnstile> es' [:] Ts; P,E \<turnstile> s' \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
 2. \<And>a b aa ba Ts. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; \<And>Ts. \<lbrakk>P,E,hp ba \<turnstile> aa [:] Ts; P,E \<turnstile> ba \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,hp b \<turnstile> a [:] Ts; P,E \<turnstile> b \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,E \<turnstile> s' \<surd>
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> s' \<surd>

goal (1 subgoal):
 1. \<And>a b aa ba Ts. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; \<And>Ts. \<lbrakk>P,E,hp ba \<turnstile> aa [:] Ts; P,E \<turnstile> ba \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,hp b \<turnstile> a [:] Ts; P,E \<turnstile> b \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba Ts. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; \<And>Ts. \<lbrakk>P,E,hp ba \<turnstile> aa [:] Ts; P,E \<turnstile> ba \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,hp b \<turnstile> a [:] Ts; P,E \<turnstile> b \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
case (step es s es'' s'' Ts)
[PROOF STATE]
proof (state)
this:
((es, s), es'', s'') \<in> Reds P E
P,E \<turnstile> \<langle>es'',s''\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>
\<lbrakk>P,E,hp s'' \<turnstile> es'' [:] ?Ts; P,E \<turnstile> s'' \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
P,E,hp s \<turnstile> es [:] Ts
P,E \<turnstile> s \<surd>

goal (1 subgoal):
 1. \<And>a b aa ba Ts. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; \<And>Ts. \<lbrakk>P,E,hp ba \<turnstile> aa [:] Ts; P,E \<turnstile> ba \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,hp b \<turnstile> a [:] Ts; P,E \<turnstile> b \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
have Reds:"((es, s), es'', s'') \<in> Reds P E"
    and reds:"P,E \<turnstile> \<langle>es'',s''\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>"
    and wtes:"P,E,hp s \<turnstile> es [:] Ts"
    and sconf:"P,E \<turnstile> s \<surd>"
    and IH:"\<And>Ts. \<lbrakk>P,E,hp s'' \<turnstile> es'' [:] Ts; P,E \<turnstile> s'' \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((es, s), es'', s'') \<in> Reds P E &&& P,E \<turnstile> \<langle>es'',s''\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>) &&& P,E,hp s \<turnstile> es [:] Ts &&& P,E \<turnstile> s \<surd> &&& (\<And>Ts. \<lbrakk>P,E,hp s'' \<turnstile> es'' [:] Ts; P,E \<turnstile> s'' \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>)
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
((es, s), es'', s'') \<in> Reds P E
P,E \<turnstile> \<langle>es'',s''\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>
P,E,hp s \<turnstile> es [:] Ts
P,E \<turnstile> s \<surd>
\<lbrakk>P,E,hp s'' \<turnstile> es'' [:] ?Ts; P,E \<turnstile> s'' \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>

goal (1 subgoal):
 1. \<And>a b aa ba Ts. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; \<And>Ts. \<lbrakk>P,E,hp ba \<turnstile> aa [:] Ts; P,E \<turnstile> ba \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,hp b \<turnstile> a [:] Ts; P,E \<turnstile> b \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
from Reds
[PROOF STATE]
proof (chain)
picking this:
((es, s), es'', s'') \<in> Reds P E
[PROOF STEP]
have reds1:"P,E \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>] \<langle>es'',s''\<rangle>"
[PROOF STATE]
proof (prove)
using this:
((es, s), es'', s'') \<in> Reds P E

goal (1 subgoal):
 1. P,E \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>] \<langle>es'',s''\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>] \<langle>es'',s''\<rangle>

goal (1 subgoal):
 1. \<And>a b aa ba Ts. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; \<And>Ts. \<lbrakk>P,E,hp ba \<turnstile> aa [:] Ts; P,E \<turnstile> ba \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,hp b \<turnstile> a [:] Ts; P,E \<turnstile> b \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
from subjects_reduction[OF wf this sconf wtes]
[PROOF STATE]
proof (chain)
picking this:
P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> Ts
[PROOF STEP]
have type:"types_conf P E (hp s'') es'' Ts"
[PROOF STATE]
proof (prove)
using this:
P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> Ts

goal (1 subgoal):
 1. P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> Ts
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> Ts

goal (1 subgoal):
 1. \<And>a b aa ba Ts. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; \<And>Ts. \<lbrakk>P,E,hp ba \<turnstile> aa [:] Ts; P,E \<turnstile> ba \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,hp b \<turnstile> a [:] Ts; P,E \<turnstile> b \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
from reds1 wtes sconf wf
[PROOF STATE]
proof (chain)
picking this:
P,E \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>] \<langle>es'',s''\<rangle>
P,E,hp s \<turnstile> es [:] Ts
P,E \<turnstile> s \<surd>
wf_C_prog P
[PROOF STEP]
have sconf':"P,E \<turnstile> s'' \<surd>"
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>] \<langle>es'',s''\<rangle>
P,E,hp s \<turnstile> es [:] Ts
P,E \<turnstile> s \<surd>
wf_C_prog P

goal (1 subgoal):
 1. P,E \<turnstile> s'' \<surd>
[PROOF STEP]
by(fastforce intro:wf_prog_wwf_prog reds_preserves_sconf)
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> s'' \<surd>

goal (1 subgoal):
 1. \<And>a b aa ba Ts. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; \<And>Ts. \<lbrakk>P,E,hp ba \<turnstile> aa [:] Ts; P,E \<turnstile> ba \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,hp b \<turnstile> a [:] Ts; P,E \<turnstile> b \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
from type
[PROOF STATE]
proof (chain)
picking this:
P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> Ts
[PROOF STEP]
have "\<exists>Ts'. P,E,hp s'' \<turnstile> es'' [:] Ts'"
[PROOF STATE]
proof (prove)
using this:
P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> Ts

goal (1 subgoal):
 1. \<exists>Ts'. P,E,hp s'' \<turnstile> es'' [:] Ts'
[PROOF STEP]
proof (induct Ts arbitrary: es'')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>es''. P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> [] \<Longrightarrow> Ex (WTrts P E (hp s'') es'')
 2. \<And>a Ts es''. \<lbrakk>\<And>es''. P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> Ts \<Longrightarrow> Ex (WTrts P E (hp s'') es''); P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> a # Ts\<rbrakk> \<Longrightarrow> Ex (WTrts P E (hp s'') es'')
[PROOF STEP]
fix esi
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>es''. P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> [] \<Longrightarrow> Ex (WTrts P E (hp s'') es'')
 2. \<And>a Ts es''. \<lbrakk>\<And>es''. P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> Ts \<Longrightarrow> Ex (WTrts P E (hp s'') es''); P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> a # Ts\<rbrakk> \<Longrightarrow> Ex (WTrts P E (hp s'') es'')
[PROOF STEP]
assume "types_conf P E (hp s'') esi []"
[PROOF STATE]
proof (state)
this:
P,E,hp s'' \<turnstile> esi [:]\<^bsub>NT\<^esub> []

goal (2 subgoals):
 1. \<And>es''. P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> [] \<Longrightarrow> Ex (WTrts P E (hp s'') es'')
 2. \<And>a Ts es''. \<lbrakk>\<And>es''. P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> Ts \<Longrightarrow> Ex (WTrts P E (hp s'') es''); P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> a # Ts\<rbrakk> \<Longrightarrow> Ex (WTrts P E (hp s'') es'')
[PROOF STEP]
thus "\<exists>Ts'. P,E,hp s'' \<turnstile> esi [:] Ts'"
[PROOF STATE]
proof (prove)
using this:
P,E,hp s'' \<turnstile> esi [:]\<^bsub>NT\<^esub> []

goal (1 subgoal):
 1. \<exists>Ts'. P,E,hp s'' \<turnstile> esi [:] Ts'
[PROOF STEP]
proof(induct esi)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P,E,hp s'' \<turnstile> [] [:]\<^bsub>NT\<^esub> [] \<Longrightarrow> Ex (WTrts P E (hp s'') [])
 2. \<And>a esi. \<lbrakk>P,E,hp s'' \<turnstile> esi [:]\<^bsub>NT\<^esub> [] \<Longrightarrow> Ex (WTrts P E (hp s'') esi); P,E,hp s'' \<turnstile> a # esi [:]\<^bsub>NT\<^esub> []\<rbrakk> \<Longrightarrow> Ex (WTrts P E (hp s'') (a # esi))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
P,E,hp s'' \<turnstile> [] [:]\<^bsub>NT\<^esub> []

goal (2 subgoals):
 1. P,E,hp s'' \<turnstile> [] [:]\<^bsub>NT\<^esub> [] \<Longrightarrow> Ex (WTrts P E (hp s'') [])
 2. \<And>a esi. \<lbrakk>P,E,hp s'' \<turnstile> esi [:]\<^bsub>NT\<^esub> [] \<Longrightarrow> Ex (WTrts P E (hp s'') esi); P,E,hp s'' \<turnstile> a # esi [:]\<^bsub>NT\<^esub> []\<rbrakk> \<Longrightarrow> Ex (WTrts P E (hp s'') (a # esi))
[PROOF STEP]
thus "\<exists>Ts'. P,E,hp s'' \<turnstile> [] [:] Ts'"
[PROOF STATE]
proof (prove)
using this:
P,E,hp s'' \<turnstile> [] [:]\<^bsub>NT\<^esub> []

goal (1 subgoal):
 1. \<exists>Ts'. P,E,hp s'' \<turnstile> [] [:] Ts'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>Ts'. P,E,hp s'' \<turnstile> [] [:] Ts'

goal (1 subgoal):
 1. \<And>a esi. \<lbrakk>P,E,hp s'' \<turnstile> esi [:]\<^bsub>NT\<^esub> [] \<Longrightarrow> Ex (WTrts P E (hp s'') esi); P,E,hp s'' \<turnstile> a # esi [:]\<^bsub>NT\<^esub> []\<rbrakk> \<Longrightarrow> Ex (WTrts P E (hp s'') (a # esi))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a esi. \<lbrakk>P,E,hp s'' \<turnstile> esi [:]\<^bsub>NT\<^esub> [] \<Longrightarrow> Ex (WTrts P E (hp s'') esi); P,E,hp s'' \<turnstile> a # esi [:]\<^bsub>NT\<^esub> []\<rbrakk> \<Longrightarrow> Ex (WTrts P E (hp s'') (a # esi))
[PROOF STEP]
fix ex esx
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a esi. \<lbrakk>P,E,hp s'' \<turnstile> esi [:]\<^bsub>NT\<^esub> [] \<Longrightarrow> Ex (WTrts P E (hp s'') esi); P,E,hp s'' \<turnstile> a # esi [:]\<^bsub>NT\<^esub> []\<rbrakk> \<Longrightarrow> Ex (WTrts P E (hp s'') (a # esi))
[PROOF STEP]
assume "types_conf P E (hp s'') (ex#esx) []"
[PROOF STATE]
proof (state)
this:
P,E,hp s'' \<turnstile> ex # esx [:]\<^bsub>NT\<^esub> []

goal (1 subgoal):
 1. \<And>a esi. \<lbrakk>P,E,hp s'' \<turnstile> esi [:]\<^bsub>NT\<^esub> [] \<Longrightarrow> Ex (WTrts P E (hp s'') esi); P,E,hp s'' \<turnstile> a # esi [:]\<^bsub>NT\<^esub> []\<rbrakk> \<Longrightarrow> Ex (WTrts P E (hp s'') (a # esi))
[PROOF STEP]
thus "\<exists>Ts'. P,E,hp s'' \<turnstile> ex#esx [:] Ts'"
[PROOF STATE]
proof (prove)
using this:
P,E,hp s'' \<turnstile> ex # esx [:]\<^bsub>NT\<^esub> []

goal (1 subgoal):
 1. \<exists>Ts'. P,E,hp s'' \<turnstile> ex # esx [:] Ts'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>Ts'. P,E,hp s'' \<turnstile> ex # esx [:] Ts'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>Ts'. P,E,hp s'' \<turnstile> esi [:] Ts'

goal (1 subgoal):
 1. \<And>a Ts es''. \<lbrakk>\<And>es''. P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> Ts \<Longrightarrow> Ex (WTrts P E (hp s'') es''); P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> a # Ts\<rbrakk> \<Longrightarrow> Ex (WTrts P E (hp s'') es'')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a Ts es''. \<lbrakk>\<And>es''. P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> Ts \<Longrightarrow> Ex (WTrts P E (hp s'') es''); P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> a # Ts\<rbrakk> \<Longrightarrow> Ex (WTrts P E (hp s'') es'')
[PROOF STEP]
fix T' Ts' esi
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a Ts es''. \<lbrakk>\<And>es''. P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> Ts \<Longrightarrow> Ex (WTrts P E (hp s'') es''); P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> a # Ts\<rbrakk> \<Longrightarrow> Ex (WTrts P E (hp s'') es'')
[PROOF STEP]
assume type':"types_conf P E (hp s'') esi (T'#Ts')"
      and IH:"\<And>es''. types_conf P E (hp s'') es'' Ts' \<Longrightarrow>
                      \<exists>Ts''. P,E,hp s'' \<turnstile> es'' [:] Ts''"
[PROOF STATE]
proof (state)
this:
P,E,hp s'' \<turnstile> esi [:]\<^bsub>NT\<^esub> T' # Ts'
P,E,hp s'' \<turnstile> ?es'' [:]\<^bsub>NT\<^esub> Ts' \<Longrightarrow> \<exists>Ts''. P,E,hp s'' \<turnstile> ?es'' [:] Ts''

goal (1 subgoal):
 1. \<And>a Ts es''. \<lbrakk>\<And>es''. P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> Ts \<Longrightarrow> Ex (WTrts P E (hp s'') es''); P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> a # Ts\<rbrakk> \<Longrightarrow> Ex (WTrts P E (hp s'') es'')
[PROOF STEP]
from type'
[PROOF STATE]
proof (chain)
picking this:
P,E,hp s'' \<turnstile> esi [:]\<^bsub>NT\<^esub> T' # Ts'
[PROOF STEP]
show "\<exists>Ts'. P,E,hp s'' \<turnstile> esi [:] Ts'"
[PROOF STATE]
proof (prove)
using this:
P,E,hp s'' \<turnstile> esi [:]\<^bsub>NT\<^esub> T' # Ts'

goal (1 subgoal):
 1. \<exists>Ts'. P,E,hp s'' \<turnstile> esi [:] Ts'
[PROOF STEP]
proof(induct esi)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P,E,hp s'' \<turnstile> [] [:]\<^bsub>NT\<^esub> T' # Ts' \<Longrightarrow> Ex (WTrts P E (hp s'') [])
 2. \<And>a esi. \<lbrakk>P,E,hp s'' \<turnstile> esi [:]\<^bsub>NT\<^esub> T' # Ts' \<Longrightarrow> Ex (WTrts P E (hp s'') esi); P,E,hp s'' \<turnstile> a # esi [:]\<^bsub>NT\<^esub> T' # Ts'\<rbrakk> \<Longrightarrow> Ex (WTrts P E (hp s'') (a # esi))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
P,E,hp s'' \<turnstile> [] [:]\<^bsub>NT\<^esub> T' # Ts'

goal (2 subgoals):
 1. P,E,hp s'' \<turnstile> [] [:]\<^bsub>NT\<^esub> T' # Ts' \<Longrightarrow> Ex (WTrts P E (hp s'') [])
 2. \<And>a esi. \<lbrakk>P,E,hp s'' \<turnstile> esi [:]\<^bsub>NT\<^esub> T' # Ts' \<Longrightarrow> Ex (WTrts P E (hp s'') esi); P,E,hp s'' \<turnstile> a # esi [:]\<^bsub>NT\<^esub> T' # Ts'\<rbrakk> \<Longrightarrow> Ex (WTrts P E (hp s'') (a # esi))
[PROOF STEP]
thus "\<exists>Ts'. P,E,hp s'' \<turnstile> [] [:] Ts'"
[PROOF STATE]
proof (prove)
using this:
P,E,hp s'' \<turnstile> [] [:]\<^bsub>NT\<^esub> T' # Ts'

goal (1 subgoal):
 1. \<exists>Ts'. P,E,hp s'' \<turnstile> [] [:] Ts'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>Ts'. P,E,hp s'' \<turnstile> [] [:] Ts'

goal (1 subgoal):
 1. \<And>a esi. \<lbrakk>P,E,hp s'' \<turnstile> esi [:]\<^bsub>NT\<^esub> T' # Ts' \<Longrightarrow> Ex (WTrts P E (hp s'') esi); P,E,hp s'' \<turnstile> a # esi [:]\<^bsub>NT\<^esub> T' # Ts'\<rbrakk> \<Longrightarrow> Ex (WTrts P E (hp s'') (a # esi))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a esi. \<lbrakk>P,E,hp s'' \<turnstile> esi [:]\<^bsub>NT\<^esub> T' # Ts' \<Longrightarrow> Ex (WTrts P E (hp s'') esi); P,E,hp s'' \<turnstile> a # esi [:]\<^bsub>NT\<^esub> T' # Ts'\<rbrakk> \<Longrightarrow> Ex (WTrts P E (hp s'') (a # esi))
[PROOF STEP]
fix ex esx
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a esi. \<lbrakk>P,E,hp s'' \<turnstile> esi [:]\<^bsub>NT\<^esub> T' # Ts' \<Longrightarrow> Ex (WTrts P E (hp s'') esi); P,E,hp s'' \<turnstile> a # esi [:]\<^bsub>NT\<^esub> T' # Ts'\<rbrakk> \<Longrightarrow> Ex (WTrts P E (hp s'') (a # esi))
[PROOF STEP]
assume "types_conf P E (hp s'') (ex#esx) (T'#Ts')"
[PROOF STATE]
proof (state)
this:
P,E,hp s'' \<turnstile> ex # esx [:]\<^bsub>NT\<^esub> T' # Ts'

goal (1 subgoal):
 1. \<And>a esi. \<lbrakk>P,E,hp s'' \<turnstile> esi [:]\<^bsub>NT\<^esub> T' # Ts' \<Longrightarrow> Ex (WTrts P E (hp s'') esi); P,E,hp s'' \<turnstile> a # esi [:]\<^bsub>NT\<^esub> T' # Ts'\<rbrakk> \<Longrightarrow> Ex (WTrts P E (hp s'') (a # esi))
[PROOF STEP]
hence type':"P,E,hp s'' \<turnstile> ex :\<^bsub>NT\<^esub> T'"
        and types':"types_conf P E (hp s'') esx Ts'"
[PROOF STATE]
proof (prove)
using this:
P,E,hp s'' \<turnstile> ex # esx [:]\<^bsub>NT\<^esub> T' # Ts'

goal (1 subgoal):
 1. P,E,hp s'' \<turnstile> ex :\<^bsub>NT\<^esub> T' &&& P,E,hp s'' \<turnstile> esx [:]\<^bsub>NT\<^esub> Ts'
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
P,E,hp s'' \<turnstile> ex :\<^bsub>NT\<^esub> T'
P,E,hp s'' \<turnstile> esx [:]\<^bsub>NT\<^esub> Ts'

goal (1 subgoal):
 1. \<And>a esi. \<lbrakk>P,E,hp s'' \<turnstile> esi [:]\<^bsub>NT\<^esub> T' # Ts' \<Longrightarrow> Ex (WTrts P E (hp s'') esi); P,E,hp s'' \<turnstile> a # esi [:]\<^bsub>NT\<^esub> T' # Ts'\<rbrakk> \<Longrightarrow> Ex (WTrts P E (hp s'') (a # esi))
[PROOF STEP]
from type'
[PROOF STATE]
proof (chain)
picking this:
P,E,hp s'' \<turnstile> ex :\<^bsub>NT\<^esub> T'
[PROOF STEP]
obtain Tx where type'':"P,E,hp s'' \<turnstile> ex : Tx"
[PROOF STATE]
proof (prove)
using this:
P,E,hp s'' \<turnstile> ex :\<^bsub>NT\<^esub> T'

goal (1 subgoal):
 1. (\<And>Tx. P,E,hp s'' \<turnstile> ex : Tx \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases T') auto
[PROOF STATE]
proof (state)
this:
P,E,hp s'' \<turnstile> ex : Tx

goal (1 subgoal):
 1. \<And>a esi. \<lbrakk>P,E,hp s'' \<turnstile> esi [:]\<^bsub>NT\<^esub> T' # Ts' \<Longrightarrow> Ex (WTrts P E (hp s'') esi); P,E,hp s'' \<turnstile> a # esi [:]\<^bsub>NT\<^esub> T' # Ts'\<rbrakk> \<Longrightarrow> Ex (WTrts P E (hp s'') (a # esi))
[PROOF STEP]
from IH[OF types']
[PROOF STATE]
proof (chain)
picking this:
\<exists>Ts''. P,E,hp s'' \<turnstile> esx [:] Ts''
[PROOF STEP]
obtain Tsx where "P,E,hp s'' \<turnstile> esx [:] Tsx"
[PROOF STATE]
proof (prove)
using this:
\<exists>Ts''. P,E,hp s'' \<turnstile> esx [:] Ts''

goal (1 subgoal):
 1. (\<And>Tsx. P,E,hp s'' \<turnstile> esx [:] Tsx \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P,E,hp s'' \<turnstile> esx [:] Tsx

goal (1 subgoal):
 1. \<And>a esi. \<lbrakk>P,E,hp s'' \<turnstile> esi [:]\<^bsub>NT\<^esub> T' # Ts' \<Longrightarrow> Ex (WTrts P E (hp s'') esi); P,E,hp s'' \<turnstile> a # esi [:]\<^bsub>NT\<^esub> T' # Ts'\<rbrakk> \<Longrightarrow> Ex (WTrts P E (hp s'') (a # esi))
[PROOF STEP]
with type''
[PROOF STATE]
proof (chain)
picking this:
P,E,hp s'' \<turnstile> ex : Tx
P,E,hp s'' \<turnstile> esx [:] Tsx
[PROOF STEP]
show "\<exists>Ts'. P,E,hp s'' \<turnstile> ex#esx [:] Ts'"
[PROOF STATE]
proof (prove)
using this:
P,E,hp s'' \<turnstile> ex : Tx
P,E,hp s'' \<turnstile> esx [:] Tsx

goal (1 subgoal):
 1. \<exists>Ts'. P,E,hp s'' \<turnstile> ex # esx [:] Ts'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>Ts'. P,E,hp s'' \<turnstile> ex # esx [:] Ts'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>Ts'. P,E,hp s'' \<turnstile> esi [:] Ts'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>Ts'. P,E,hp s'' \<turnstile> es'' [:] Ts'

goal (1 subgoal):
 1. \<And>a b aa ba Ts. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; \<And>Ts. \<lbrakk>P,E,hp ba \<turnstile> aa [:] Ts; P,E \<turnstile> ba \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,hp b \<turnstile> a [:] Ts; P,E \<turnstile> b \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>Ts'. P,E,hp s'' \<turnstile> es'' [:] Ts'
[PROOF STEP]
obtain Ts' where "P,E,hp s'' \<turnstile> es'' [:] Ts'"
[PROOF STATE]
proof (prove)
using this:
\<exists>Ts'. P,E,hp s'' \<turnstile> es'' [:] Ts'

goal (1 subgoal):
 1. (\<And>Ts'. P,E,hp s'' \<turnstile> es'' [:] Ts' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P,E,hp s'' \<turnstile> es'' [:] Ts'

goal (1 subgoal):
 1. \<And>a b aa ba Ts. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; \<And>Ts. \<lbrakk>P,E,hp ba \<turnstile> aa [:] Ts; P,E \<turnstile> ba \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>; P,E,hp b \<turnstile> a [:] Ts; P,E \<turnstile> b \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
from IH[OF this sconf']
[PROOF STATE]
proof (chain)
picking this:
P,E \<turnstile> s' \<surd>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> s' \<surd>

goal (1 subgoal):
 1. P,E \<turnstile> s' \<surd>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> s' \<surd>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma step_preserves_defass:
assumes wf: "wf_C_prog P" and step: "P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>"
shows "\<D> e \<lfloor>dom(lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom(lcl s')\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>

goal (1 subgoal):
 1. \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>
[PROOF STEP]
proof (induct rule:converse_rtrancl_induct2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<D> e' \<lfloor>dom (lcl s')\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>
 2. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<D> aa \<lfloor>dom (lcl ba)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> a \<lfloor>dom (lcl b)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>
[PROOF STEP]
case refl
[PROOF STATE]
proof (state)
this:
\<D> e' \<lfloor>dom (lcl s')\<rfloor>

goal (2 subgoals):
 1. \<D> e' \<lfloor>dom (lcl s')\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>
 2. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<D> aa \<lfloor>dom (lcl ba)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> a \<lfloor>dom (lcl b)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<D> e' \<lfloor>dom (lcl s')\<rfloor>

goal (1 subgoal):
 1. \<D> e' \<lfloor>dom (lcl s')\<rfloor>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<D> e' \<lfloor>dom (lcl s')\<rfloor>

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<D> aa \<lfloor>dom (lcl ba)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> a \<lfloor>dom (lcl b)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<D> aa \<lfloor>dom (lcl ba)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> a \<lfloor>dom (lcl b)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>
[PROOF STEP]
case (step e s e' s')
[PROOF STATE]
proof (state)
this:
((e, s), e', s') \<in> Red P E
P,E \<turnstile> \<langle>e',s'\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>
\<D> e' \<lfloor>dom (lcl s')\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>
\<D> e \<lfloor>dom (lcl s)\<rfloor>

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<D> aa \<lfloor>dom (lcl ba)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> a \<lfloor>dom (lcl b)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
((e, s), e', s') \<in> Red P E
P,E \<turnstile> \<langle>e',s'\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>
\<D> e' \<lfloor>dom (lcl s')\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>
\<D> e \<lfloor>dom (lcl s)\<rfloor>

goal (1 subgoal):
 1. \<D> e' \<lfloor>dom (lcl s')\<rfloor>
[PROOF STEP]
by(cases s,cases s')(auto dest:red_preserves_defass[OF wf])
[PROOF STATE]
proof (state)
this:
\<D> e' \<lfloor>dom (lcl s')\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma step_preserves_type:
assumes wf: "wf_C_prog P" and step: "P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>"
shows "\<And>T. \<lbrakk> P,E \<turnstile> s \<surd>; P,E,hp s \<turnstile> e:T \<rbrakk>
    \<Longrightarrow> P,E,(hp s') \<turnstile> e' :\<^bsub>NT\<^esub> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>T. \<lbrakk>P,E \<turnstile> s \<surd>; P,E,hp s \<turnstile> e : T\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>

goal (1 subgoal):
 1. \<And>T. \<lbrakk>P,E \<turnstile> s \<surd>; P,E,hp s \<turnstile> e : T\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
proof (induct rule:converse_rtrancl_induct2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>T. \<lbrakk>P,E \<turnstile> s' \<surd>; P,E,hp s' \<turnstile> e' : T\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. \<And>a b aa ba T. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E \<turnstile> ba \<surd>; P,E,hp ba \<turnstile> aa : T\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T; P,E \<turnstile> b \<surd>; P,E,hp b \<turnstile> a : T\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
case refl
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> s' \<surd>
P,E,hp s' \<turnstile> e' : T

goal (2 subgoals):
 1. \<And>T. \<lbrakk>P,E \<turnstile> s' \<surd>; P,E,hp s' \<turnstile> e' : T\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. \<And>a b aa ba T. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E \<turnstile> ba \<surd>; P,E,hp ba \<turnstile> aa : T\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T; P,E \<turnstile> b \<surd>; P,E,hp b \<turnstile> a : T\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> s' \<surd>
P,E,hp s' \<turnstile> e' : T

goal (1 subgoal):
 1. P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
by -(rule wt_same_type_typeconf)
[PROOF STATE]
proof (state)
this:
P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T

goal (1 subgoal):
 1. \<And>a b aa ba T. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E \<turnstile> ba \<surd>; P,E,hp ba \<turnstile> aa : T\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T; P,E \<turnstile> b \<surd>; P,E,hp b \<turnstile> a : T\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba T. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E \<turnstile> ba \<surd>; P,E,hp ba \<turnstile> aa : T\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T; P,E \<turnstile> b \<surd>; P,E,hp b \<turnstile> a : T\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
case (step e s e'' s'' T)
[PROOF STATE]
proof (state)
this:
((e, s), e'', s'') \<in> Red P E
P,E \<turnstile> \<langle>e'',s''\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>
\<lbrakk>P,E \<turnstile> s'' \<surd>; P,E,hp s'' \<turnstile> e'' : ?T\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> ?T
P,E \<turnstile> s \<surd>
P,E,hp s \<turnstile> e : T

goal (1 subgoal):
 1. \<And>a b aa ba T. \<lbrakk>((a, b), aa, ba) \<in> Red P E; P,E \<turnstile> \<langle>aa,ba\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E \<turnstile> ba \<surd>; P,E,hp ba \<turnstile> aa : T\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T; P,E \<turnstile> b \<surd>; P,E,hp b \<turnstile> a : T\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
((e, s), e'', s'') \<in> Red P E
P,E \<turnstile> \<langle>e'',s''\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>
\<lbrakk>P,E \<turnstile> s'' \<surd>; P,E,hp s'' \<turnstile> e'' : ?T\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> ?T
P,E \<turnstile> s \<surd>
P,E,hp s \<turnstile> e : T

goal (1 subgoal):
 1. P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
using wf
[PROOF STATE]
proof (prove)
using this:
((e, s), e'', s'') \<in> Red P E
P,E \<turnstile> \<langle>e'',s''\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>
\<lbrakk>P,E \<turnstile> s'' \<surd>; P,E,hp s'' \<turnstile> e'' : ?T\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> ?T
P,E \<turnstile> s \<surd>
P,E,hp s \<turnstile> e : T
wf_C_prog P

goal (1 subgoal):
 1. P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow> \<langle>e'',s''\<rangle>; P,E \<turnstile> \<langle>e'',s''\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E \<turnstile> s'' \<surd>; P,E,fst s'' \<turnstile> e'' : T\<rbrakk> \<Longrightarrow> P,E,fst s' \<turnstile> e' :\<^bsub>NT\<^esub> T; P,E \<turnstile> s \<surd>; P,E,fst s \<turnstile> e : T; wf_C_prog P\<rbrakk> \<Longrightarrow> P,E,fst s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
apply (frule subject_reduction[OF wf])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow> \<langle>e'',s''\<rangle>; P,E \<turnstile> \<langle>e'',s''\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E \<turnstile> s'' \<surd>; P,E,fst s'' \<turnstile> e'' : T\<rbrakk> \<Longrightarrow> P,E,fst s' \<turnstile> e' :\<^bsub>NT\<^esub> T; P,E \<turnstile> s \<surd>; P,E,fst s \<turnstile> e : T; wf_C_prog P\<rbrakk> \<Longrightarrow> P,E \<turnstile> s \<surd>
 2. \<lbrakk>P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow> \<langle>e'',s''\<rangle>; P,E \<turnstile> \<langle>e'',s''\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E \<turnstile> s'' \<surd>; P,E,fst s'' \<turnstile> e'' : T\<rbrakk> \<Longrightarrow> P,E,fst s' \<turnstile> e' :\<^bsub>NT\<^esub> T; P,E \<turnstile> s \<surd>; P,E,fst s \<turnstile> e : T; wf_C_prog P\<rbrakk> \<Longrightarrow> P,E,hp s \<turnstile> e : ?T7
 3. \<lbrakk>P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow> \<langle>e'',s''\<rangle>; P,E \<turnstile> \<langle>e'',s''\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. \<lbrakk>P,E \<turnstile> s'' \<surd>; P,E,fst s'' \<turnstile> e'' : T\<rbrakk> \<Longrightarrow> P,E,fst s' \<turnstile> e' :\<^bsub>NT\<^esub> T; P,E \<turnstile> s \<surd>; P,E,fst s \<turnstile> e : T; wf_C_prog P; P,E,hp s'' \<turnstile> e'' :\<^bsub>NT\<^esub> ?T7\<rbrakk> \<Longrightarrow> P,E,fst s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
apply (auto dest!:red_preserves_sconf intro:wf_prog_wwf_prog)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,E \<turnstile> \<langle>e'',s''\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. P,E,fst s'' \<turnstile> e'' : T \<Longrightarrow> P,E,fst s' \<turnstile> e' :\<^bsub>NT\<^esub> T; P,E \<turnstile> s \<surd>; P,E,fst s \<turnstile> e : T; wf_C_prog P; P,E,fst s'' \<turnstile> e'' :\<^bsub>NT\<^esub> T; P,E \<turnstile> s'' \<surd>\<rbrakk> \<Longrightarrow> P,E,fst s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
apply(cases T)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>P,E \<turnstile> \<langle>e'',s''\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. P,E,fst s'' \<turnstile> e'' : T \<Longrightarrow> P,E,fst s' \<turnstile> e' :\<^bsub>NT\<^esub> T; P,E \<turnstile> s \<surd>; P,E,fst s \<turnstile> e : T; wf_C_prog P; P,E,fst s'' \<turnstile> e'' :\<^bsub>NT\<^esub> T; P,E \<turnstile> s'' \<surd>; T = Void\<rbrakk> \<Longrightarrow> P,E,fst s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 2. \<lbrakk>P,E \<turnstile> \<langle>e'',s''\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. P,E,fst s'' \<turnstile> e'' : T \<Longrightarrow> P,E,fst s' \<turnstile> e' :\<^bsub>NT\<^esub> T; P,E \<turnstile> s \<surd>; P,E,fst s \<turnstile> e : T; wf_C_prog P; P,E,fst s'' \<turnstile> e'' :\<^bsub>NT\<^esub> T; P,E \<turnstile> s'' \<surd>; T = Boolean\<rbrakk> \<Longrightarrow> P,E,fst s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 3. \<lbrakk>P,E \<turnstile> \<langle>e'',s''\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. P,E,fst s'' \<turnstile> e'' : T \<Longrightarrow> P,E,fst s' \<turnstile> e' :\<^bsub>NT\<^esub> T; P,E \<turnstile> s \<surd>; P,E,fst s \<turnstile> e : T; wf_C_prog P; P,E,fst s'' \<turnstile> e'' :\<^bsub>NT\<^esub> T; P,E \<turnstile> s'' \<surd>; T = Integer\<rbrakk> \<Longrightarrow> P,E,fst s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 4. \<lbrakk>P,E \<turnstile> \<langle>e'',s''\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. P,E,fst s'' \<turnstile> e'' : T \<Longrightarrow> P,E,fst s' \<turnstile> e' :\<^bsub>NT\<^esub> T; P,E \<turnstile> s \<surd>; P,E,fst s \<turnstile> e : T; wf_C_prog P; P,E,fst s'' \<turnstile> e'' :\<^bsub>NT\<^esub> T; P,E \<turnstile> s'' \<surd>; T = NT\<rbrakk> \<Longrightarrow> P,E,fst s' \<turnstile> e' :\<^bsub>NT\<^esub> T
 5. \<And>x5. \<lbrakk>P,E \<turnstile> \<langle>e'',s''\<rangle> \<rightarrow>* \<langle>e',s'\<rangle>; \<And>T. P,E,fst s'' \<turnstile> e'' : T \<Longrightarrow> P,E,fst s' \<turnstile> e' :\<^bsub>NT\<^esub> T; P,E \<turnstile> s \<surd>; P,E,fst s \<turnstile> e : T; wf_C_prog P; P,E,fst s'' \<turnstile> e'' :\<^bsub>NT\<^esub> T; P,E \<turnstile> s'' \<surd>; T = Class x5\<rbrakk> \<Longrightarrow> P,E,fst s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
apply fastforce+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma types_conf_conf_types_conf:
  "\<lbrakk>types_conf P E h es Ts; conformable Ts Ts'\<rbrakk> \<Longrightarrow> types_conf P E h es Ts'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts; conformable Ts Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'
[PROOF STEP]
proof (induct Ts arbitrary: Ts' es)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Ts' es. \<lbrakk>P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> []; conformable [] Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'
 2. \<And>a Ts Ts' es. \<lbrakk>\<And>Ts' es. \<lbrakk>P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts; conformable Ts Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'; P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> a # Ts; conformable (a # Ts) Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> []
conformable [] Ts'

goal (2 subgoals):
 1. \<And>Ts' es. \<lbrakk>P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> []; conformable [] Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'
 2. \<And>a Ts Ts' es. \<lbrakk>\<And>Ts' es. \<lbrakk>P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts; conformable Ts Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'; P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> a # Ts; conformable (a # Ts) Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> []
conformable [] Ts'

goal (1 subgoal):
 1. P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'
[PROOF STEP]
by (cases Ts') (auto split: if_split_asm)
[PROOF STATE]
proof (state)
this:
P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'

goal (1 subgoal):
 1. \<And>a Ts Ts' es. \<lbrakk>\<And>Ts' es. \<lbrakk>P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts; conformable Ts Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'; P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> a # Ts; conformable (a # Ts) Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a Ts Ts' es. \<lbrakk>\<And>Ts' es. \<lbrakk>P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts; conformable Ts Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'; P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> a # Ts; conformable (a # Ts) Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'
[PROOF STEP]
case (Cons T'' Ts'')
[PROOF STATE]
proof (state)
this:
\<lbrakk>P,E,h \<turnstile> ?es [:]\<^bsub>NT\<^esub> Ts''; conformable Ts'' ?Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> ?es [:]\<^bsub>NT\<^esub> ?Ts'
P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> T'' # Ts''
conformable (T'' # Ts'') Ts'

goal (1 subgoal):
 1. \<And>a Ts Ts' es. \<lbrakk>\<And>Ts' es. \<lbrakk>P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts; conformable Ts Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'; P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> a # Ts; conformable (a # Ts) Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'
[PROOF STEP]
have type:"types_conf P E h es (T''#Ts'')"
    and conf:"conformable (T''#Ts'') Ts'"
    and IH:"\<And>Ts' es. \<lbrakk>types_conf P E h es Ts''; conformable Ts'' Ts'\<rbrakk>
                   \<Longrightarrow> types_conf P E h es Ts'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> T'' # Ts'' &&& conformable (T'' # Ts'') Ts' &&& (\<And>Ts' es. \<lbrakk>P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts''; conformable Ts'' Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts')
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> T'' # Ts''
conformable (T'' # Ts'') Ts'
\<lbrakk>P,E,h \<turnstile> ?es [:]\<^bsub>NT\<^esub> Ts''; conformable Ts'' ?Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> ?es [:]\<^bsub>NT\<^esub> ?Ts'

goal (1 subgoal):
 1. \<And>a Ts Ts' es. \<lbrakk>\<And>Ts' es. \<lbrakk>P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts; conformable Ts Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'; P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> a # Ts; conformable (a # Ts) Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'
[PROOF STEP]
from type
[PROOF STATE]
proof (chain)
picking this:
P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> T'' # Ts''
[PROOF STEP]
obtain e' es' where es:"es = e'#es'"
[PROOF STATE]
proof (prove)
using this:
P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> T'' # Ts''

goal (1 subgoal):
 1. (\<And>e' es'. es = e' # es' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases es) auto
[PROOF STATE]
proof (state)
this:
es = e' # es'

goal (1 subgoal):
 1. \<And>a Ts Ts' es. \<lbrakk>\<And>Ts' es. \<lbrakk>P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts; conformable Ts Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'; P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> a # Ts; conformable (a # Ts) Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'
[PROOF STEP]
with type
[PROOF STATE]
proof (chain)
picking this:
P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> T'' # Ts''
es = e' # es'
[PROOF STEP]
have type':"P,E,h \<turnstile> e' :\<^bsub>NT\<^esub> T''"
    and types': "types_conf P E h es' Ts''"
[PROOF STATE]
proof (prove)
using this:
P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> T'' # Ts''
es = e' # es'

goal (1 subgoal):
 1. P,E,h \<turnstile> e' :\<^bsub>NT\<^esub> T'' &&& P,E,h \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts''
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
P,E,h \<turnstile> e' :\<^bsub>NT\<^esub> T''
P,E,h \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts''

goal (1 subgoal):
 1. \<And>a Ts Ts' es. \<lbrakk>\<And>Ts' es. \<lbrakk>P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts; conformable Ts Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'; P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> a # Ts; conformable (a # Ts) Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'
[PROOF STEP]
from conf
[PROOF STATE]
proof (chain)
picking this:
conformable (T'' # Ts'') Ts'
[PROOF STEP]
obtain U Us where Ts': "Ts' = U#Us"
[PROOF STATE]
proof (prove)
using this:
conformable (T'' # Ts'') Ts'

goal (1 subgoal):
 1. (\<And>U Us. Ts' = U # Us \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases Ts') auto
[PROOF STATE]
proof (state)
this:
Ts' = U # Us

goal (1 subgoal):
 1. \<And>a Ts Ts' es. \<lbrakk>\<And>Ts' es. \<lbrakk>P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts; conformable Ts Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'; P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> a # Ts; conformable (a # Ts) Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'
[PROOF STEP]
with conf
[PROOF STATE]
proof (chain)
picking this:
conformable (T'' # Ts'') Ts'
Ts' = U # Us
[PROOF STEP]
have disj:"T'' = U \<or> (\<exists>C. T'' = NT \<and> U = Class C)"
    and conf':"conformable Ts'' Us"
[PROOF STATE]
proof (prove)
using this:
conformable (T'' # Ts'') Ts'
Ts' = U # Us

goal (1 subgoal):
 1. T'' = U \<or> (\<exists>C. T'' = NT \<and> U = Class C) &&& conformable Ts'' Us
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
T'' = U \<or> (\<exists>C. T'' = NT \<and> U = Class C)
conformable Ts'' Us

goal (1 subgoal):
 1. \<And>a Ts Ts' es. \<lbrakk>\<And>Ts' es. \<lbrakk>P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts; conformable Ts Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'; P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> a # Ts; conformable (a # Ts) Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'
[PROOF STEP]
from type' disj
[PROOF STATE]
proof (chain)
picking this:
P,E,h \<turnstile> e' :\<^bsub>NT\<^esub> T''
T'' = U \<or> (\<exists>C. T'' = NT \<and> U = Class C)
[PROOF STEP]
have "P,E,h \<turnstile> e' :\<^bsub>NT\<^esub> U"
[PROOF STATE]
proof (prove)
using this:
P,E,h \<turnstile> e' :\<^bsub>NT\<^esub> T''
T'' = U \<or> (\<exists>C. T'' = NT \<and> U = Class C)

goal (1 subgoal):
 1. P,E,h \<turnstile> e' :\<^bsub>NT\<^esub> U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P,E,h \<turnstile> e' :\<^bsub>NT\<^esub> U

goal (1 subgoal):
 1. \<And>a Ts Ts' es. \<lbrakk>\<And>Ts' es. \<lbrakk>P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts; conformable Ts Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'; P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> a # Ts; conformable (a # Ts) Ts'\<rbrakk> \<Longrightarrow> P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'
[PROOF STEP]
with IH[OF types' conf'] Ts' es
[PROOF STATE]
proof (chain)
picking this:
P,E,h \<turnstile> es' [:]\<^bsub>NT\<^esub> Us
Ts' = U # Us
es = e' # es'
P,E,h \<turnstile> e' :\<^bsub>NT\<^esub> U
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P,E,h \<turnstile> es' [:]\<^bsub>NT\<^esub> Us
Ts' = U # Us
es = e' # es'
P,E,h \<turnstile> e' :\<^bsub>NT\<^esub> U

goal (1 subgoal):
 1. P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma types_conf_Wtrt_conf:
  "types_conf P E h es Ts \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' Ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' Ts
[PROOF STEP]
proof (induct Ts arbitrary: es)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>es. P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> [] \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' []
 2. \<And>a Ts es. \<lbrakk>\<And>es. P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' Ts; P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> a # Ts\<rbrakk> \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' (a # Ts)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> []

goal (2 subgoals):
 1. \<And>es. P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> [] \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' []
 2. \<And>a Ts es. \<lbrakk>\<And>es. P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' Ts; P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> a # Ts\<rbrakk> \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' (a # Ts)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> []

goal (1 subgoal):
 1. \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' []
[PROOF STEP]
by (cases es) (auto split:if_split_asm)
[PROOF STATE]
proof (state)
this:
\<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' []

goal (1 subgoal):
 1. \<And>a Ts es. \<lbrakk>\<And>es. P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' Ts; P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> a # Ts\<rbrakk> \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' (a # Ts)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a Ts es. \<lbrakk>\<And>es. P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' Ts; P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> a # Ts\<rbrakk> \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' (a # Ts)
[PROOF STEP]
case (Cons T'' Ts'')
[PROOF STATE]
proof (state)
this:
P,E,h \<turnstile> ?es [:]\<^bsub>NT\<^esub> Ts'' \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> ?es [:] Ts' \<and> conformable Ts' Ts''
P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> T'' # Ts''

goal (1 subgoal):
 1. \<And>a Ts es. \<lbrakk>\<And>es. P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' Ts; P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> a # Ts\<rbrakk> \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' (a # Ts)
[PROOF STEP]
have type:"types_conf P E h es (T''#Ts'')"
    and IH:"\<And>es. types_conf P E h es Ts'' \<Longrightarrow>
                  \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' Ts''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> T'' # Ts'' &&& (\<And>es. P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts'' \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' Ts'')
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> T'' # Ts''
P,E,h \<turnstile> ?es [:]\<^bsub>NT\<^esub> Ts'' \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> ?es [:] Ts' \<and> conformable Ts' Ts''

goal (1 subgoal):
 1. \<And>a Ts es. \<lbrakk>\<And>es. P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' Ts; P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> a # Ts\<rbrakk> \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' (a # Ts)
[PROOF STEP]
from type
[PROOF STATE]
proof (chain)
picking this:
P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> T'' # Ts''
[PROOF STEP]
obtain e' es' where es:"es = e'#es'"
[PROOF STATE]
proof (prove)
using this:
P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> T'' # Ts''

goal (1 subgoal):
 1. (\<And>e' es'. es = e' # es' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases es) auto
[PROOF STATE]
proof (state)
this:
es = e' # es'

goal (1 subgoal):
 1. \<And>a Ts es. \<lbrakk>\<And>es. P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' Ts; P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> a # Ts\<rbrakk> \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' (a # Ts)
[PROOF STEP]
with type
[PROOF STATE]
proof (chain)
picking this:
P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> T'' # Ts''
es = e' # es'
[PROOF STEP]
have type':"P,E,h \<turnstile> e' :\<^bsub>NT\<^esub> T''"
    and types': "types_conf P E h es' Ts''"
[PROOF STATE]
proof (prove)
using this:
P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> T'' # Ts''
es = e' # es'

goal (1 subgoal):
 1. P,E,h \<turnstile> e' :\<^bsub>NT\<^esub> T'' &&& P,E,h \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts''
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
P,E,h \<turnstile> e' :\<^bsub>NT\<^esub> T''
P,E,h \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts''

goal (1 subgoal):
 1. \<And>a Ts es. \<lbrakk>\<And>es. P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' Ts; P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> a # Ts\<rbrakk> \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' (a # Ts)
[PROOF STEP]
from type'
[PROOF STATE]
proof (chain)
picking this:
P,E,h \<turnstile> e' :\<^bsub>NT\<^esub> T''
[PROOF STEP]
obtain T' where "P,E,h \<turnstile> e' : T'" and
    "T' = T'' \<or> (\<exists>C. T' = NT \<and> T'' = Class C)"
[PROOF STATE]
proof (prove)
using this:
P,E,h \<turnstile> e' :\<^bsub>NT\<^esub> T''

goal (1 subgoal):
 1. (\<And>T'. \<lbrakk>P,E,h \<turnstile> e' : T'; T' = T'' \<or> (\<exists>C. T' = NT \<and> T'' = Class C)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases T'') auto
[PROOF STATE]
proof (state)
this:
P,E,h \<turnstile> e' : T'
T' = T'' \<or> (\<exists>C. T' = NT \<and> T'' = Class C)

goal (1 subgoal):
 1. \<And>a Ts es. \<lbrakk>\<And>es. P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> Ts \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' Ts; P,E,h \<turnstile> es [:]\<^bsub>NT\<^esub> a # Ts\<rbrakk> \<Longrightarrow> \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' (a # Ts)
[PROOF STEP]
with IH[OF types'] es
[PROOF STATE]
proof (chain)
picking this:
\<exists>Ts'. P,E,h \<turnstile> es' [:] Ts' \<and> conformable Ts' Ts''
es = e' # es'
P,E,h \<turnstile> e' : T'
T' = T'' \<or> (\<exists>C. T' = NT \<and> T'' = Class C)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>Ts'. P,E,h \<turnstile> es' [:] Ts' \<and> conformable Ts' Ts''
es = e' # es'
P,E,h \<turnstile> e' : T'
T' = T'' \<or> (\<exists>C. T' = NT \<and> T'' = Class C)

goal (1 subgoal):
 1. \<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' (T'' # Ts'')
[PROOF STEP]
by(auto,rule_tac x="T''#Ts'" in exI,simp,rule_tac x="NT#Ts'" in exI,simp)
[PROOF STATE]
proof (state)
this:
\<exists>Ts'. P,E,h \<turnstile> es [:] Ts' \<and> conformable Ts' (T'' # Ts'')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma steps_preserves_types:
assumes wf: "wf_C_prog P" and steps: "P,E \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>"
shows "\<And>Ts. \<lbrakk> P,E \<turnstile> s \<surd>; P,E,hp s \<turnstile> es [:] Ts\<rbrakk>
  \<Longrightarrow> types_conf P E (hp s') es' Ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Ts. \<lbrakk>P,E \<turnstile> s \<surd>; P,E,hp s \<turnstile> es [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts
[PROOF STEP]
using steps
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>

goal (1 subgoal):
 1. \<And>Ts. \<lbrakk>P,E \<turnstile> s \<surd>; P,E,hp s \<turnstile> es [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts
[PROOF STEP]
proof (induct rule:converse_rtrancl_induct2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Ts. \<lbrakk>P,E \<turnstile> s' \<surd>; P,E,hp s' \<turnstile> es' [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts
 2. \<And>a b aa ba Ts. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; \<And>Ts. \<lbrakk>P,E \<turnstile> ba \<surd>; P,E,hp ba \<turnstile> aa [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts; P,E \<turnstile> b \<surd>; P,E,hp b \<turnstile> a [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts
[PROOF STEP]
case refl
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> s' \<surd>
P,E,hp s' \<turnstile> es' [:] Ts

goal (2 subgoals):
 1. \<And>Ts. \<lbrakk>P,E \<turnstile> s' \<surd>; P,E,hp s' \<turnstile> es' [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts
 2. \<And>a b aa ba Ts. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; \<And>Ts. \<lbrakk>P,E \<turnstile> ba \<surd>; P,E,hp ba \<turnstile> aa [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts; P,E \<turnstile> b \<surd>; P,E,hp b \<turnstile> a [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> s' \<surd>
P,E,hp s' \<turnstile> es' [:] Ts

goal (1 subgoal):
 1. P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts
[PROOF STEP]
by -(rule wts_same_types_typesconf)
[PROOF STATE]
proof (state)
this:
P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts

goal (1 subgoal):
 1. \<And>a b aa ba Ts. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; \<And>Ts. \<lbrakk>P,E \<turnstile> ba \<surd>; P,E,hp ba \<turnstile> aa [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts; P,E \<turnstile> b \<surd>; P,E,hp b \<turnstile> a [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba Ts. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; \<And>Ts. \<lbrakk>P,E \<turnstile> ba \<surd>; P,E,hp ba \<turnstile> aa [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts; P,E \<turnstile> b \<surd>; P,E,hp b \<turnstile> a [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts
[PROOF STEP]
case (step es s es'' s'' Ts)
[PROOF STATE]
proof (state)
this:
((es, s), es'', s'') \<in> Reds P E
P,E \<turnstile> \<langle>es'',s''\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>
\<lbrakk>P,E \<turnstile> s'' \<surd>; P,E,hp s'' \<turnstile> es'' [:] ?Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> ?Ts
P,E \<turnstile> s \<surd>
P,E,hp s \<turnstile> es [:] Ts

goal (1 subgoal):
 1. \<And>a b aa ba Ts. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; \<And>Ts. \<lbrakk>P,E \<turnstile> ba \<surd>; P,E,hp ba \<turnstile> aa [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts; P,E \<turnstile> b \<surd>; P,E,hp b \<turnstile> a [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts
[PROOF STEP]
have Reds:"((es, s), es'', s'') \<in> Reds P E"
    and steps:"P,E \<turnstile> \<langle>es'',s''\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>"
    and sconf:"P,E \<turnstile> s \<surd>" and wtes:"P,E,hp s \<turnstile> es [:] Ts"
    and IH:"\<And>Ts. \<lbrakk>P,E \<turnstile> s'' \<surd>; P,E,hp s'' \<turnstile> es'' [:] Ts \<rbrakk>
               \<Longrightarrow> types_conf P E (hp s') es' Ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((es, s), es'', s'') \<in> Reds P E &&& P,E \<turnstile> \<langle>es'',s''\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>) &&& P,E \<turnstile> s \<surd> &&& P,E,hp s \<turnstile> es [:] Ts &&& (\<And>Ts. \<lbrakk>P,E \<turnstile> s'' \<surd>; P,E,hp s'' \<turnstile> es'' [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts)
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
((es, s), es'', s'') \<in> Reds P E
P,E \<turnstile> \<langle>es'',s''\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>
P,E \<turnstile> s \<surd>
P,E,hp s \<turnstile> es [:] Ts
\<lbrakk>P,E \<turnstile> s'' \<surd>; P,E,hp s'' \<turnstile> es'' [:] ?Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> ?Ts

goal (1 subgoal):
 1. \<And>a b aa ba Ts. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; \<And>Ts. \<lbrakk>P,E \<turnstile> ba \<surd>; P,E,hp ba \<turnstile> aa [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts; P,E \<turnstile> b \<surd>; P,E,hp b \<turnstile> a [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts
[PROOF STEP]
from Reds
[PROOF STATE]
proof (chain)
picking this:
((es, s), es'', s'') \<in> Reds P E
[PROOF STEP]
have step:"P,E \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>] \<langle>es'',s''\<rangle>"
[PROOF STATE]
proof (prove)
using this:
((es, s), es'', s'') \<in> Reds P E

goal (1 subgoal):
 1. P,E \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>] \<langle>es'',s''\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>] \<langle>es'',s''\<rangle>

goal (1 subgoal):
 1. \<And>a b aa ba Ts. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; \<And>Ts. \<lbrakk>P,E \<turnstile> ba \<surd>; P,E,hp ba \<turnstile> aa [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts; P,E \<turnstile> b \<surd>; P,E,hp b \<turnstile> a [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts
[PROOF STEP]
with wtes sconf wf
[PROOF STATE]
proof (chain)
picking this:
P,E,hp s \<turnstile> es [:] Ts
P,E \<turnstile> s \<surd>
wf_C_prog P
P,E \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>] \<langle>es'',s''\<rangle>
[PROOF STEP]
have sconf':"P,E \<turnstile> s'' \<surd>"
[PROOF STATE]
proof (prove)
using this:
P,E,hp s \<turnstile> es [:] Ts
P,E \<turnstile> s \<surd>
wf_C_prog P
P,E \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>] \<langle>es'',s''\<rangle>

goal (1 subgoal):
 1. P,E \<turnstile> s'' \<surd>
[PROOF STEP]
by(auto intro:reds_preserves_sconf wf_prog_wwf_prog)
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> s'' \<surd>

goal (1 subgoal):
 1. \<And>a b aa ba Ts. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; \<And>Ts. \<lbrakk>P,E \<turnstile> ba \<surd>; P,E,hp ba \<turnstile> aa [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts; P,E \<turnstile> b \<surd>; P,E,hp b \<turnstile> a [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts
[PROOF STEP]
from wtes
[PROOF STATE]
proof (chain)
picking this:
P,E,hp s \<turnstile> es [:] Ts
[PROOF STEP]
have "length es = length Ts"
[PROOF STATE]
proof (prove)
using this:
P,E,hp s \<turnstile> es [:] Ts

goal (1 subgoal):
 1. length es = length Ts
[PROOF STEP]
by(fastforce dest:WTrts_same_length)
[PROOF STATE]
proof (state)
this:
length es = length Ts

goal (1 subgoal):
 1. \<And>a b aa ba Ts. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; \<And>Ts. \<lbrakk>P,E \<turnstile> ba \<surd>; P,E,hp ba \<turnstile> aa [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts; P,E \<turnstile> b \<surd>; P,E,hp b \<turnstile> a [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts
[PROOF STEP]
from step sconf wtes
[PROOF STATE]
proof (chain)
picking this:
P,E \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>] \<langle>es'',s''\<rangle>
P,E \<turnstile> s \<surd>
P,E,hp s \<turnstile> es [:] Ts
[PROOF STEP]
have type': "types_conf P E (hp s'') es'' Ts"
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>] \<langle>es'',s''\<rangle>
P,E \<turnstile> s \<surd>
P,E,hp s \<turnstile> es [:] Ts

goal (1 subgoal):
 1. P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> Ts
[PROOF STEP]
by (rule subjects_reduction[OF wf])
[PROOF STATE]
proof (state)
this:
P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> Ts

goal (1 subgoal):
 1. \<And>a b aa ba Ts. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; \<And>Ts. \<lbrakk>P,E \<turnstile> ba \<surd>; P,E,hp ba \<turnstile> aa [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts; P,E \<turnstile> b \<surd>; P,E,hp b \<turnstile> a [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> Ts
[PROOF STEP]
obtain Ts' where wtes'':"P,E,hp s'' \<turnstile> es'' [:] Ts'"
    and conf:"conformable Ts' Ts"
[PROOF STATE]
proof (prove)
using this:
P,E,hp s'' \<turnstile> es'' [:]\<^bsub>NT\<^esub> Ts

goal (1 subgoal):
 1. (\<And>Ts'. \<lbrakk>P,E,hp s'' \<turnstile> es'' [:] Ts'; conformable Ts' Ts\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest:types_conf_Wtrt_conf)
[PROOF STATE]
proof (state)
this:
P,E,hp s'' \<turnstile> es'' [:] Ts'
conformable Ts' Ts

goal (1 subgoal):
 1. \<And>a b aa ba Ts. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; \<And>Ts. \<lbrakk>P,E \<turnstile> ba \<surd>; P,E,hp ba \<turnstile> aa [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts; P,E \<turnstile> b \<surd>; P,E,hp b \<turnstile> a [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts
[PROOF STEP]
from IH[OF sconf' wtes'']
[PROOF STATE]
proof (chain)
picking this:
P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts'
[PROOF STEP]
have "types_conf P E (hp s') es' Ts'"
[PROOF STATE]
proof (prove)
using this:
P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts'

goal (1 subgoal):
 1. P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts'

goal (1 subgoal):
 1. \<And>a b aa ba Ts. \<lbrakk>((a, b), aa, ba) \<in> Reds P E; P,E \<turnstile> \<langle>aa,ba\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle>; \<And>Ts. \<lbrakk>P,E \<turnstile> ba \<surd>; P,E,hp ba \<turnstile> aa [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts; P,E \<turnstile> b \<surd>; P,E,hp b \<turnstile> a [:] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts
[PROOF STEP]
with conf
[PROOF STATE]
proof (chain)
picking this:
conformable Ts' Ts
P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
conformable Ts' Ts
P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts'

goal (1 subgoal):
 1. P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts
[PROOF STEP]
by(fastforce intro:types_conf_conf_types_conf)
[PROOF STATE]
proof (state)
this:
P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eval_preserves_sconf:
  "\<lbrakk> wf_C_prog P; P,E \<turnstile> \<langle>e,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>; P,E \<turnstile> e::T; P,E \<turnstile> s \<surd> \<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_C_prog P; P,E \<turnstile> \<langle>e,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>; P,E \<turnstile> e :: T; P,E \<turnstile> s \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
by(blast intro:step_preserves_sconf big_by_small WT_implies_WTrt wf_prog_wwf_prog)


[STATEMENT]
lemma evals_preserves_sconf:
  "\<lbrakk> wf_C_prog P; P,E \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>es',s'\<rangle>; P,E \<turnstile> es [::] Ts; P,E \<turnstile> s \<surd> \<rbrakk>
  \<Longrightarrow> P,E \<turnstile> s' \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_C_prog P; P,E \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>es',s'\<rangle>; P,E \<turnstile> es [::] Ts; P,E \<turnstile> s \<surd>\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
by(blast intro:steps_preserves_sconf bigs_by_smalls WTs_implies_WTrts
                 wf_prog_wwf_prog)


[STATEMENT]
lemma eval_preserves_type: assumes wf: "wf_C_prog P"
shows "\<lbrakk> P,E \<turnstile> \<langle>e,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>; P,E \<turnstile> s \<surd>; P,E \<turnstile> e::T \<rbrakk>
   \<Longrightarrow> P,E,(hp s') \<turnstile> e' :\<^bsub>NT\<^esub> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,E \<turnstile> \<langle>e,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>; P,E \<turnstile> s \<surd>; P,E \<turnstile> e :: T\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
using wf
[PROOF STATE]
proof (prove)
using this:
wf_C_prog P

goal (1 subgoal):
 1. \<lbrakk>P,E \<turnstile> \<langle>e,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>; P,E \<turnstile> s \<surd>; P,E \<turnstile> e :: T\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
by (auto dest!:big_by_small[OF wf_prog_wwf_prog[OF wf]] WT_implies_WTrt
           intro:wf_prog_wwf_prog
           dest!:step_preserves_type[OF wf])


[STATEMENT]
lemma evals_preserves_types: assumes wf: "wf_C_prog P"
shows "\<lbrakk> P,E \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>es',s'\<rangle>; P,E \<turnstile> s \<surd>; P,E \<turnstile> es [::] Ts \<rbrakk>
  \<Longrightarrow> types_conf P E (hp s') es' Ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,E \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>es',s'\<rangle>; P,E \<turnstile> s \<surd>; P,E \<turnstile> es [::] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts
[PROOF STEP]
using wf
[PROOF STATE]
proof (prove)
using this:
wf_C_prog P

goal (1 subgoal):
 1. \<lbrakk>P,E \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>es',s'\<rangle>; P,E \<turnstile> s \<surd>; P,E \<turnstile> es [::] Ts\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> es' [:]\<^bsub>NT\<^esub> Ts
[PROOF STEP]
by (auto dest!:bigs_by_smalls[OF wf_prog_wwf_prog[OF wf]] WTs_implies_WTrts
           intro:wf_prog_wwf_prog
           dest!:steps_preserves_types[OF wf])


[STATEMENT]
theorem Subject_reduction: assumes wf: "wf_C_prog P"
shows "P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow> \<langle>e',s'\<rangle> \<Longrightarrow> P,E,s \<turnstile> e : T \<surd>
       \<Longrightarrow> P,E,(hp s') \<turnstile> e' :\<^bsub>NT\<^esub> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow> \<langle>e',s'\<rangle>; P,E,s \<turnstile> e : T \<surd>\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
using wf
[PROOF STATE]
proof (prove)
using this:
wf_C_prog P

goal (1 subgoal):
 1. \<lbrakk>P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow> \<langle>e',s'\<rangle>; P,E,s \<turnstile> e : T \<surd>\<rbrakk> \<Longrightarrow> P,E,hp s' \<turnstile> e' :\<^bsub>NT\<^esub> T
[PROOF STEP]
by (force elim!:red_preserves_sconf intro:wf_prog_wwf_prog
            dest:subject_reduction[OF wf] simp:wf_config_def)