[STATEMENT]
lemma red_preserves_sconf:
  "\<lbrakk> P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow> \<langle>e',s'\<rangle>; P,E,hp s \<turnstile> e : T; P,E \<turnstile> s \<surd>; wwf_prog P\<rbrakk>
\<Longrightarrow> P,E \<turnstile> s' \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow> \<langle>e',s'\<rangle>; P,E,hp s \<turnstile> e : T; P,E \<turnstile> s \<surd>; wwf_prog P\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
by(fastforce intro:red_preserves_hconf red_preserves_lconf
            simp add:sconf_def)


[STATEMENT]
lemma reds_preserves_sconf:
  "\<lbrakk> P,E \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>] \<langle>es',s'\<rangle>; P,E,hp s \<turnstile> es [:] Ts; P,E \<turnstile> s \<surd>; wwf_prog P\<rbrakk>
\<Longrightarrow> P,E \<turnstile> s' \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,E \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>] \<langle>es',s'\<rangle>; P,E,hp s \<turnstile> es [:] Ts; P,E \<turnstile> s \<surd>; wwf_prog P\<rbrakk> \<Longrightarrow> P,E \<turnstile> s' \<surd>
[PROOF STEP]
by(fastforce intro:reds_preserves_hconf reds_preserves_lconf
            simp add:sconf_def)


[STATEMENT]
lemma wt_blocks:
 "\<And>E. \<lbrakk> length Vs = length Ts; length vs = length Ts;
         \<forall>T' \<in> set Ts. is_type P T'\<rbrakk> \<Longrightarrow>
       (P,E,h \<turnstile> blocks(Vs,Ts,vs,e) : T) =
  (P,E(Vs[\<mapsto>]Ts),h \<turnstile> e:T \<and>
  (\<exists>Ts'. map (P \<turnstile> typeof\<^bsub>h\<^esub>) vs = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] Ts))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>E. \<lbrakk>length Vs = length Ts; length vs = length Ts; \<forall>T'\<in>set Ts. is_type P T'\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (Vs, Ts, vs, e) : T) = (P,E(Vs [\<mapsto>] Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] Ts))
[PROOF STEP]
proof(induct Vs Ts vs e rule:blocks_old_induct)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>aj ak al E. \<lbrakk>length [] = length []; length (aj # ak) = length []; Ball (set []) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks ([], [], aj # ak, al) : T) = (P,E([] [\<mapsto>] []),h \<turnstile> al : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (aj # ak) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] []))
 2. \<And>ad ae a b E. \<lbrakk>length [] = length (ad # ae); length a = length (ad # ae); Ball (set (ad # ae)) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks ([], ad # ae, a, b) : T) = (P,E([] [\<mapsto>] ad # ae),h \<turnstile> b : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> a = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (ad # ae)))
 3. \<And>V Vs a b E. \<lbrakk>length (V # Vs) = length []; length a = length []; Ball (set []) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (V # Vs, [], a, b) : T) = (P,E(V # Vs [\<mapsto>] []),h \<turnstile> b : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> a = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] []))
 4. \<And>V Vs Ta Ts aw E. \<lbrakk>length (V # Vs) = length (Ta # Ts); length [] = length (Ta # Ts); Ball (set (Ta # Ts)) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (V # Vs, Ta # Ts, [], aw) : T) = (P,E(V # Vs [\<mapsto>] Ta # Ts),h \<turnstile> aw : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> [] = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (Ta # Ts)))
 5. \<And>V Vs Ta Ts v vs e E. \<lbrakk>\<And>E. \<lbrakk>length Vs = length Ts; length vs = length Ts; Ball (set Ts) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (Vs, Ts, vs, e) : T) = (P,E(Vs [\<mapsto>] Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] Ts)); length (V # Vs) = length (Ta # Ts); length (v # vs) = length (Ta # Ts); Ball (set (Ta # Ts)) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (V # Vs, Ta # Ts, v # vs, e) : T) = (P,E(V # Vs [\<mapsto>] Ta # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (Ta # Ts)))
 6. \<And>e E. \<lbrakk>length [] = length []; length [] = length []; Ball (set []) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks ([], [], [], e) : T) = (P,E([] [\<mapsto>] []),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> [] = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] []))
[PROOF STEP]
case (5 V Vs T' Ts v vs e)
[PROOF STATE]
proof (state)
this:
\<lbrakk>length Vs = length Ts; length vs = length Ts; \<forall>a\<in>set Ts. is_type P a\<rbrakk> \<Longrightarrow> (P,?E,h \<turnstile> blocks (Vs, Ts, vs, e) : T) = (P,?E(Vs [\<mapsto>] Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] Ts))
length (V # Vs) = length (T' # Ts)
length (v # vs) = length (T' # Ts)
\<forall>a\<in>set (T' # Ts). is_type P a

goal (6 subgoals):
 1. \<And>aj ak al E. \<lbrakk>length [] = length []; length (aj # ak) = length []; Ball (set []) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks ([], [], aj # ak, al) : T) = (P,E([] [\<mapsto>] []),h \<turnstile> al : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (aj # ak) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] []))
 2. \<And>ad ae a b E. \<lbrakk>length [] = length (ad # ae); length a = length (ad # ae); Ball (set (ad # ae)) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks ([], ad # ae, a, b) : T) = (P,E([] [\<mapsto>] ad # ae),h \<turnstile> b : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> a = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (ad # ae)))
 3. \<And>V Vs a b E. \<lbrakk>length (V # Vs) = length []; length a = length []; Ball (set []) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (V # Vs, [], a, b) : T) = (P,E(V # Vs [\<mapsto>] []),h \<turnstile> b : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> a = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] []))
 4. \<And>V Vs Ta Ts aw E. \<lbrakk>length (V # Vs) = length (Ta # Ts); length [] = length (Ta # Ts); Ball (set (Ta # Ts)) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (V # Vs, Ta # Ts, [], aw) : T) = (P,E(V # Vs [\<mapsto>] Ta # Ts),h \<turnstile> aw : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> [] = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (Ta # Ts)))
 5. \<And>V Vs Ta Ts v vs e E. \<lbrakk>\<And>E. \<lbrakk>length Vs = length Ts; length vs = length Ts; Ball (set Ts) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (Vs, Ts, vs, e) : T) = (P,E(Vs [\<mapsto>] Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] Ts)); length (V # Vs) = length (Ta # Ts); length (v # vs) = length (Ta # Ts); Ball (set (Ta # Ts)) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (V # Vs, Ta # Ts, v # vs, e) : T) = (P,E(V # Vs [\<mapsto>] Ta # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (Ta # Ts)))
 6. \<And>e E. \<lbrakk>length [] = length []; length [] = length []; Ball (set []) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks ([], [], [], e) : T) = (P,E([] [\<mapsto>] []),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> [] = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] []))
[PROOF STEP]
have length:"length (V#Vs) = length (T'#Ts)" "length (v#vs) = length (T'#Ts)"
    and type:"\<forall>S \<in> set (T'#Ts). is_type P S"
    and IH:"\<And>E. \<lbrakk>length Vs = length Ts; length vs = length Ts;
                  \<forall>S \<in> set Ts. is_type P S\<rbrakk>
     \<Longrightarrow> (P,E,h \<turnstile> blocks (Vs, Ts, vs, e) : T) =
         (P,E(Vs [\<mapsto>] Ts),h \<turnstile> e : T \<and>
            (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] Ts))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (length (V # Vs) = length (T' # Ts) &&& length (v # vs) = length (T' # Ts)) &&& \<forall>S\<in>set (T' # Ts). is_type P S &&& (\<And>E. \<lbrakk>length Vs = length Ts; length vs = length Ts; \<forall>S\<in>set Ts. is_type P S\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (Vs, Ts, vs, e) : T) = (P,E(Vs [\<mapsto>] Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] Ts)))
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
length (V # Vs) = length (T' # Ts)
length (v # vs) = length (T' # Ts)
\<forall>S\<in>set (T' # Ts). is_type P S
\<lbrakk>length Vs = length Ts; length vs = length Ts; \<forall>S\<in>set Ts. is_type P S\<rbrakk> \<Longrightarrow> (P,?E,h \<turnstile> blocks (Vs, Ts, vs, e) : T) = (P,?E(Vs [\<mapsto>] Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] Ts))

goal (6 subgoals):
 1. \<And>aj ak al E. \<lbrakk>length [] = length []; length (aj # ak) = length []; Ball (set []) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks ([], [], aj # ak, al) : T) = (P,E([] [\<mapsto>] []),h \<turnstile> al : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (aj # ak) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] []))
 2. \<And>ad ae a b E. \<lbrakk>length [] = length (ad # ae); length a = length (ad # ae); Ball (set (ad # ae)) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks ([], ad # ae, a, b) : T) = (P,E([] [\<mapsto>] ad # ae),h \<turnstile> b : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> a = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (ad # ae)))
 3. \<And>V Vs a b E. \<lbrakk>length (V # Vs) = length []; length a = length []; Ball (set []) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (V # Vs, [], a, b) : T) = (P,E(V # Vs [\<mapsto>] []),h \<turnstile> b : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> a = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] []))
 4. \<And>V Vs Ta Ts aw E. \<lbrakk>length (V # Vs) = length (Ta # Ts); length [] = length (Ta # Ts); Ball (set (Ta # Ts)) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (V # Vs, Ta # Ts, [], aw) : T) = (P,E(V # Vs [\<mapsto>] Ta # Ts),h \<turnstile> aw : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> [] = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (Ta # Ts)))
 5. \<And>V Vs Ta Ts v vs e E. \<lbrakk>\<And>E. \<lbrakk>length Vs = length Ts; length vs = length Ts; Ball (set Ts) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (Vs, Ts, vs, e) : T) = (P,E(Vs [\<mapsto>] Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] Ts)); length (V # Vs) = length (Ta # Ts); length (v # vs) = length (Ta # Ts); Ball (set (Ta # Ts)) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (V # Vs, Ta # Ts, v # vs, e) : T) = (P,E(V # Vs [\<mapsto>] Ta # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (Ta # Ts)))
 6. \<And>e E. \<lbrakk>length [] = length []; length [] = length []; Ball (set []) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks ([], [], [], e) : T) = (P,E([] [\<mapsto>] []),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> [] = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] []))
[PROOF STEP]
from type
[PROOF STATE]
proof (chain)
picking this:
\<forall>S\<in>set (T' # Ts). is_type P S
[PROOF STEP]
have typeT':"is_type P T'" and type':"\<forall>S \<in> set Ts. is_type P S"
[PROOF STATE]
proof (prove)
using this:
\<forall>S\<in>set (T' # Ts). is_type P S

goal (1 subgoal):
 1. is_type P T' &&& \<forall>S\<in>set Ts. is_type P S
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
is_type P T'
\<forall>S\<in>set Ts. is_type P S

goal (6 subgoals):
 1. \<And>aj ak al E. \<lbrakk>length [] = length []; length (aj # ak) = length []; Ball (set []) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks ([], [], aj # ak, al) : T) = (P,E([] [\<mapsto>] []),h \<turnstile> al : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (aj # ak) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] []))
 2. \<And>ad ae a b E. \<lbrakk>length [] = length (ad # ae); length a = length (ad # ae); Ball (set (ad # ae)) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks ([], ad # ae, a, b) : T) = (P,E([] [\<mapsto>] ad # ae),h \<turnstile> b : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> a = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (ad # ae)))
 3. \<And>V Vs a b E. \<lbrakk>length (V # Vs) = length []; length a = length []; Ball (set []) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (V # Vs, [], a, b) : T) = (P,E(V # Vs [\<mapsto>] []),h \<turnstile> b : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> a = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] []))
 4. \<And>V Vs Ta Ts aw E. \<lbrakk>length (V # Vs) = length (Ta # Ts); length [] = length (Ta # Ts); Ball (set (Ta # Ts)) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (V # Vs, Ta # Ts, [], aw) : T) = (P,E(V # Vs [\<mapsto>] Ta # Ts),h \<turnstile> aw : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> [] = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (Ta # Ts)))
 5. \<And>V Vs Ta Ts v vs e E. \<lbrakk>\<And>E. \<lbrakk>length Vs = length Ts; length vs = length Ts; Ball (set Ts) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (Vs, Ts, vs, e) : T) = (P,E(Vs [\<mapsto>] Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] Ts)); length (V # Vs) = length (Ta # Ts); length (v # vs) = length (Ta # Ts); Ball (set (Ta # Ts)) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (V # Vs, Ta # Ts, v # vs, e) : T) = (P,E(V # Vs [\<mapsto>] Ta # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (Ta # Ts)))
 6. \<And>e E. \<lbrakk>length [] = length []; length [] = length []; Ball (set []) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks ([], [], [], e) : T) = (P,E([] [\<mapsto>] []),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> [] = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] []))
[PROOF STEP]
from length
[PROOF STATE]
proof (chain)
picking this:
length (V # Vs) = length (T' # Ts)
length (v # vs) = length (T' # Ts)
[PROOF STEP]
have "length Vs = length Ts" "length vs = length Ts"
[PROOF STATE]
proof (prove)
using this:
length (V # Vs) = length (T' # Ts)
length (v # vs) = length (T' # Ts)

goal (1 subgoal):
 1. length Vs = length Ts &&& length vs = length Ts
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
length Vs = length Ts
length vs = length Ts

goal (6 subgoals):
 1. \<And>aj ak al E. \<lbrakk>length [] = length []; length (aj # ak) = length []; Ball (set []) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks ([], [], aj # ak, al) : T) = (P,E([] [\<mapsto>] []),h \<turnstile> al : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (aj # ak) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] []))
 2. \<And>ad ae a b E. \<lbrakk>length [] = length (ad # ae); length a = length (ad # ae); Ball (set (ad # ae)) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks ([], ad # ae, a, b) : T) = (P,E([] [\<mapsto>] ad # ae),h \<turnstile> b : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> a = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (ad # ae)))
 3. \<And>V Vs a b E. \<lbrakk>length (V # Vs) = length []; length a = length []; Ball (set []) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (V # Vs, [], a, b) : T) = (P,E(V # Vs [\<mapsto>] []),h \<turnstile> b : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> a = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] []))
 4. \<And>V Vs Ta Ts aw E. \<lbrakk>length (V # Vs) = length (Ta # Ts); length [] = length (Ta # Ts); Ball (set (Ta # Ts)) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (V # Vs, Ta # Ts, [], aw) : T) = (P,E(V # Vs [\<mapsto>] Ta # Ts),h \<turnstile> aw : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> [] = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (Ta # Ts)))
 5. \<And>V Vs Ta Ts v vs e E. \<lbrakk>\<And>E. \<lbrakk>length Vs = length Ts; length vs = length Ts; Ball (set Ts) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (Vs, Ts, vs, e) : T) = (P,E(Vs [\<mapsto>] Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] Ts)); length (V # Vs) = length (Ta # Ts); length (v # vs) = length (Ta # Ts); Ball (set (Ta # Ts)) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (V # Vs, Ta # Ts, v # vs, e) : T) = (P,E(V # Vs [\<mapsto>] Ta # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (Ta # Ts)))
 6. \<And>e E. \<lbrakk>length [] = length []; length [] = length []; Ball (set []) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks ([], [], [], e) : T) = (P,E([] [\<mapsto>] []),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> [] = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] []))
[PROOF STEP]
from IH[OF this type']
[PROOF STATE]
proof (chain)
picking this:
(P,?E,h \<turnstile> blocks (Vs, Ts, vs, e) : T) = (P,?E(Vs [\<mapsto>] Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] Ts))
[PROOF STEP]
have eq:"(P,E(V \<mapsto> T'),h \<turnstile> blocks (Vs,Ts,vs,e) : T) =
  (P,E(V \<mapsto> T')(Vs [\<mapsto>] Ts),h \<turnstile> e : T \<and>
   (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] Ts))"
[PROOF STATE]
proof (prove)
using this:
(P,?E,h \<turnstile> blocks (Vs, Ts, vs, e) : T) = (P,?E(Vs [\<mapsto>] Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] Ts))

goal (1 subgoal):
 1. (P,E(V \<mapsto> T'),h \<turnstile> blocks (Vs, Ts, vs, e) : T) = (P,E(V \<mapsto> T', Vs [\<mapsto>] Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] Ts))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(P,E(V \<mapsto> T'),h \<turnstile> blocks (Vs, Ts, vs, e) : T) = (P,E(V \<mapsto> T', Vs [\<mapsto>] Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] Ts))

goal (6 subgoals):
 1. \<And>aj ak al E. \<lbrakk>length [] = length []; length (aj # ak) = length []; Ball (set []) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks ([], [], aj # ak, al) : T) = (P,E([] [\<mapsto>] []),h \<turnstile> al : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (aj # ak) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] []))
 2. \<And>ad ae a b E. \<lbrakk>length [] = length (ad # ae); length a = length (ad # ae); Ball (set (ad # ae)) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks ([], ad # ae, a, b) : T) = (P,E([] [\<mapsto>] ad # ae),h \<turnstile> b : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> a = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (ad # ae)))
 3. \<And>V Vs a b E. \<lbrakk>length (V # Vs) = length []; length a = length []; Ball (set []) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (V # Vs, [], a, b) : T) = (P,E(V # Vs [\<mapsto>] []),h \<turnstile> b : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> a = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] []))
 4. \<And>V Vs Ta Ts aw E. \<lbrakk>length (V # Vs) = length (Ta # Ts); length [] = length (Ta # Ts); Ball (set (Ta # Ts)) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (V # Vs, Ta # Ts, [], aw) : T) = (P,E(V # Vs [\<mapsto>] Ta # Ts),h \<turnstile> aw : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> [] = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (Ta # Ts)))
 5. \<And>V Vs Ta Ts v vs e E. \<lbrakk>\<And>E. \<lbrakk>length Vs = length Ts; length vs = length Ts; Ball (set Ts) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (Vs, Ts, vs, e) : T) = (P,E(Vs [\<mapsto>] Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] Ts)); length (V # Vs) = length (Ta # Ts); length (v # vs) = length (Ta # Ts); Ball (set (Ta # Ts)) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (V # Vs, Ta # Ts, v # vs, e) : T) = (P,E(V # Vs [\<mapsto>] Ta # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (Ta # Ts)))
 6. \<And>e E. \<lbrakk>length [] = length []; length [] = length []; Ball (set []) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks ([], [], [], e) : T) = (P,E([] [\<mapsto>] []),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> [] = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] []))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T) = (P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts)))
[PROOF STEP]
proof(rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T \<Longrightarrow> P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts))
 2. P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts)) \<Longrightarrow> P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T
[PROOF STEP]
assume "P,E,h \<turnstile> blocks (V#Vs,T'#Ts,v#vs,e) : T"
[PROOF STATE]
proof (state)
this:
P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T

goal (2 subgoals):
 1. P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T \<Longrightarrow> P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts))
 2. P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts)) \<Longrightarrow> P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T
[PROOF STEP]
have wt:"P,E(V \<mapsto> T'),h \<turnstile> V:=Val v : T'"
      and blocks:"P,E(V \<mapsto> T'),h \<turnstile> blocks (Vs,Ts,vs,e) : T"
[PROOF STATE]
proof (prove)
using this:
P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T

goal (1 subgoal):
 1. P,E(V \<mapsto> T'),h \<turnstile> V:=Val v : T' &&& P,E(V \<mapsto> T'),h \<turnstile> blocks (Vs, Ts, vs, e) : T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P,E(V \<mapsto> T'),h \<turnstile> V:=Val v : T'
P,E(V \<mapsto> T'),h \<turnstile> blocks (Vs, Ts, vs, e) : T

goal (2 subgoals):
 1. P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T \<Longrightarrow> P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts))
 2. P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts)) \<Longrightarrow> P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T
[PROOF STEP]
from blocks eq
[PROOF STATE]
proof (chain)
picking this:
P,E(V \<mapsto> T'),h \<turnstile> blocks (Vs, Ts, vs, e) : T
(P,E(V \<mapsto> T'),h \<turnstile> blocks (Vs, Ts, vs, e) : T) = (P,E(V \<mapsto> T', Vs [\<mapsto>] Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] Ts))
[PROOF STEP]
obtain Ts' where wte:"P,E(V \<mapsto> T')(Vs [\<mapsto>] Ts),h \<turnstile> e : T"
      and typeof:"map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts'" and subs:"P \<turnstile> Ts' [\<le>] Ts"
[PROOF STATE]
proof (prove)
using this:
P,E(V \<mapsto> T'),h \<turnstile> blocks (Vs, Ts, vs, e) : T
(P,E(V \<mapsto> T'),h \<turnstile> blocks (Vs, Ts, vs, e) : T) = (P,E(V \<mapsto> T', Vs [\<mapsto>] Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] Ts))

goal (1 subgoal):
 1. (\<And>Ts'. \<lbrakk>P,E(V \<mapsto> T', Vs [\<mapsto>] Ts),h \<turnstile> e : T; map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts'; P \<turnstile> Ts' [\<le>] Ts\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P,E(V \<mapsto> T', Vs [\<mapsto>] Ts),h \<turnstile> e : T
map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts'
P \<turnstile> Ts' [\<le>] Ts

goal (2 subgoals):
 1. P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T \<Longrightarrow> P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts))
 2. P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts)) \<Longrightarrow> P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T
[PROOF STEP]
from wt
[PROOF STATE]
proof (chain)
picking this:
P,E(V \<mapsto> T'),h \<turnstile> V:=Val v : T'
[PROOF STEP]
obtain T'' where "P \<turnstile> typeof\<^bsub>h\<^esub> v = Some T''" and "P \<turnstile> T'' \<le> T'"
[PROOF STATE]
proof (prove)
using this:
P,E(V \<mapsto> T'),h \<turnstile> V:=Val v : T'

goal (1 subgoal):
 1. (\<And>T''. \<lbrakk>P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T''\<rfloor>; P \<turnstile> T'' \<le> T'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T''\<rfloor>
P \<turnstile> T'' \<le> T'

goal (2 subgoals):
 1. P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T \<Longrightarrow> P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts))
 2. P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts)) \<Longrightarrow> P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T
[PROOF STEP]
with wte typeof subs
[PROOF STATE]
proof (chain)
picking this:
P,E(V \<mapsto> T', Vs [\<mapsto>] Ts),h \<turnstile> e : T
map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts'
P \<turnstile> Ts' [\<le>] Ts
P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T''\<rfloor>
P \<turnstile> T'' \<le> T'
[PROOF STEP]
show "P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and>
          (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts))"
[PROOF STATE]
proof (prove)
using this:
P,E(V \<mapsto> T', Vs [\<mapsto>] Ts),h \<turnstile> e : T
map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts'
P \<turnstile> Ts' [\<le>] Ts
P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T''\<rfloor>
P \<turnstile> T'' \<le> T'

goal (1 subgoal):
 1. P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts))

goal (1 subgoal):
 1. P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts)) \<Longrightarrow> P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts)) \<Longrightarrow> P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T
[PROOF STEP]
assume "P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and>
      (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts))"
[PROOF STATE]
proof (state)
this:
P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts))

goal (1 subgoal):
 1. P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts)) \<Longrightarrow> P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts))
[PROOF STEP]
obtain Ts' where wte:"P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T"
      and typeof:"map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts'"
      and subs:"P \<turnstile> Ts' [\<le>] (T'#Ts)"
[PROOF STATE]
proof (prove)
using this:
P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts))

goal (1 subgoal):
 1. (\<And>Ts'. \<lbrakk>P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T; map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts'; P \<turnstile> Ts' [\<le>] (T' # Ts)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T
map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts'
P \<turnstile> Ts' [\<le>] (T' # Ts)

goal (1 subgoal):
 1. P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts)) \<Longrightarrow> P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T
[PROOF STEP]
from subs
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> Ts' [\<le>] (T' # Ts)
[PROOF STEP]
obtain U Us where Ts':"Ts' = U#Us"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> Ts' [\<le>] (T' # 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. P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts)) \<Longrightarrow> P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T
[PROOF STEP]
with wte typeof subs eq
[PROOF STATE]
proof (chain)
picking this:
P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T
map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts'
P \<turnstile> Ts' [\<le>] (T' # Ts)
(P,E(V \<mapsto> T'),h \<turnstile> blocks (Vs, Ts, vs, e) : T) = (P,E(V \<mapsto> T', Vs [\<mapsto>] Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] Ts))
Ts' = U # Us
[PROOF STEP]
have blocks:"P,E(V \<mapsto> T'),h \<turnstile> blocks (Vs,Ts,vs,e) : T"
[PROOF STATE]
proof (prove)
using this:
P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T
map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts'
P \<turnstile> Ts' [\<le>] (T' # Ts)
(P,E(V \<mapsto> T'),h \<turnstile> blocks (Vs, Ts, vs, e) : T) = (P,E(V \<mapsto> T', Vs [\<mapsto>] Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> vs = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] Ts))
Ts' = U # Us

goal (1 subgoal):
 1. P,E(V \<mapsto> T'),h \<turnstile> blocks (Vs, Ts, vs, e) : T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P,E(V \<mapsto> T'),h \<turnstile> blocks (Vs, Ts, vs, e) : T

goal (1 subgoal):
 1. P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts)) \<Longrightarrow> P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T
[PROOF STEP]
from Ts' typeof subs
[PROOF STATE]
proof (chain)
picking this:
Ts' = U # Us
map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts'
P \<turnstile> Ts' [\<le>] (T' # Ts)
[PROOF STEP]
have "P \<turnstile> typeof\<^bsub>h\<^esub> v = Some U"
      and "P \<turnstile> U \<le> T'"
[PROOF STATE]
proof (prove)
using this:
Ts' = U # Us
map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts'
P \<turnstile> Ts' [\<le>] (T' # Ts)

goal (1 subgoal):
 1. P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>U\<rfloor> &&& P \<turnstile> U \<le> T'
[PROOF STEP]
by (auto simp:fun_of_def)
[PROOF STATE]
proof (state)
this:
P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>U\<rfloor>
P \<turnstile> U \<le> T'

goal (1 subgoal):
 1. P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts)) \<Longrightarrow> P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T
[PROOF STEP]
hence wtval:"P,E(V \<mapsto> T'),h \<turnstile> V:=Val v : T'"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>U\<rfloor>
P \<turnstile> U \<le> T'

goal (1 subgoal):
 1. P,E(V \<mapsto> T'),h \<turnstile> V:=Val v : T'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P,E(V \<mapsto> T'),h \<turnstile> V:=Val v : T'

goal (1 subgoal):
 1. P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts)) \<Longrightarrow> P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T
[PROOF STEP]
with blocks typeT'
[PROOF STATE]
proof (chain)
picking this:
P,E(V \<mapsto> T'),h \<turnstile> blocks (Vs, Ts, vs, e) : T
is_type P T'
P,E(V \<mapsto> T'),h \<turnstile> V:=Val v : T'
[PROOF STEP]
show "P,E,h \<turnstile> blocks (V#Vs,T'#Ts,v#vs,e) : T"
[PROOF STATE]
proof (prove)
using this:
P,E(V \<mapsto> T'),h \<turnstile> blocks (Vs, Ts, vs, e) : T
is_type P T'
P,E(V \<mapsto> T'),h \<turnstile> V:=Val v : T'

goal (1 subgoal):
 1. P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(P,E,h \<turnstile> blocks (V # Vs, T' # Ts, v # vs, e) : T) = (P,E(V # Vs [\<mapsto>] T' # Ts),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (v # vs) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (T' # Ts)))

goal (5 subgoals):
 1. \<And>aj ak al E. \<lbrakk>length [] = length []; length (aj # ak) = length []; Ball (set []) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks ([], [], aj # ak, al) : T) = (P,E([] [\<mapsto>] []),h \<turnstile> al : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> (aj # ak) = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] []))
 2. \<And>ad ae a b E. \<lbrakk>length [] = length (ad # ae); length a = length (ad # ae); Ball (set (ad # ae)) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks ([], ad # ae, a, b) : T) = (P,E([] [\<mapsto>] ad # ae),h \<turnstile> b : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> a = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (ad # ae)))
 3. \<And>V Vs a b E. \<lbrakk>length (V # Vs) = length []; length a = length []; Ball (set []) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (V # Vs, [], a, b) : T) = (P,E(V # Vs [\<mapsto>] []),h \<turnstile> b : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> a = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] []))
 4. \<And>V Vs Ta Ts aw E. \<lbrakk>length (V # Vs) = length (Ta # Ts); length [] = length (Ta # Ts); Ball (set (Ta # Ts)) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks (V # Vs, Ta # Ts, [], aw) : T) = (P,E(V # Vs [\<mapsto>] Ta # Ts),h \<turnstile> aw : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> [] = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] (Ta # Ts)))
 5. \<And>e E. \<lbrakk>length [] = length []; length [] = length []; Ball (set []) (is_type P)\<rbrakk> \<Longrightarrow> (P,E,h \<turnstile> blocks ([], [], [], e) : T) = (P,E([] [\<mapsto>] []),h \<turnstile> e : T \<and> (\<exists>Ts'. map P \<turnstile> typeof\<^bsub>h\<^esub> [] = map Some Ts' \<and> P \<turnstile> Ts' [\<le>] []))
[PROOF STEP]
qed auto