[STATEMENT]
lemma compE\<^sub>1_pres_wt: "\<And>Vs Ts U.
  \<lbrakk> P,[Vs[\<mapsto>]Ts] \<turnstile> e :: U; size Ts = size Vs \<rbrakk>
  \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs e :: U"
and  "\<And>Vs Ts Us.
  \<lbrakk> P,[Vs[\<mapsto>]Ts] \<turnstile> es [::] Us; size Ts = size Vs \<rbrakk>
  \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compEs\<^sub>1 Vs es [::] Us"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> e :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs e :: U) &&& (\<And>Vs Ts Us. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> es [::] Us; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compEs\<^sub>1 Vs es [::] Us)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> e :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs e :: U) &&& (\<And>Vs Ts Us. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> es [::] Us; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compEs\<^sub>1 Vs es [::] Us)
[PROOF STEP]
proof(induct e and es rule: compE\<^sub>1.induct compEs\<^sub>1.induct)
[PROOF STATE]
proof (state)
goal (17 subgoals):
 1. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> new x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (new x) :: U
 2. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> Cast x1 x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Cast x1 x2) :: U
 3. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> Val x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Val x) :: U
 4. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1 \<guillemotleft>x2\<guillemotright> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3) :: U
 5. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> Var x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Var x) :: U
 6. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1:=x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1:=x2) :: U
 7. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3}) :: U
 8. \<And>x1 x2 x3 x4 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x4 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} := x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4) :: U
 9. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts Us. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 [::] Us; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compEs\<^sub>1 Vs x3 [::] Us; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2(x3) :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2(x3)) :: U
 10. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> {x1:x2; x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs {x1:x2; x3} :: U
A total of 17 subgoals...
[PROOF STEP]
case Var
[PROOF STATE]
proof (state)
this:
P,[Vs [\<mapsto>] Ts] \<turnstile> Var x_ :: U
length Ts = length Vs

goal (17 subgoals):
 1. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> new x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (new x) :: U
 2. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> Cast x1 x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Cast x1 x2) :: U
 3. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> Val x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Val x) :: U
 4. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1 \<guillemotleft>x2\<guillemotright> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3) :: U
 5. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> Var x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Var x) :: U
 6. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1:=x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1:=x2) :: U
 7. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3}) :: U
 8. \<And>x1 x2 x3 x4 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x4 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} := x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4) :: U
 9. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts Us. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 [::] Us; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compEs\<^sub>1 Vs x3 [::] Us; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2(x3) :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2(x3)) :: U
 10. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> {x1:x2; x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs {x1:x2; x3} :: U
A total of 17 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P,[Vs [\<mapsto>] Ts] \<turnstile> Var x_ :: U
length Ts = length Vs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P,[Vs [\<mapsto>] Ts] \<turnstile> Var x_ :: U
length Ts = length Vs

goal (1 subgoal):
 1. compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Var x_) :: U
[PROOF STEP]
by (fastforce simp:map_upds_apply_eq_Some split:if_split_asm)
[PROOF STATE]
proof (state)
this:
compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Var x_) :: U

goal (16 subgoals):
 1. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> new x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (new x) :: U
 2. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> Cast x1 x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Cast x1 x2) :: U
 3. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> Val x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Val x) :: U
 4. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1 \<guillemotleft>x2\<guillemotright> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3) :: U
 5. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1:=x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1:=x2) :: U
 6. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3}) :: U
 7. \<And>x1 x2 x3 x4 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x4 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} := x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4) :: U
 8. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts Us. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 [::] Us; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compEs\<^sub>1 Vs x3 [::] Us; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2(x3) :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2(x3)) :: U
 9. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> {x1:x2; x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs {x1:x2; x3} :: U
 10. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1;; x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1;; x2) :: U
A total of 16 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (16 subgoals):
 1. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> new x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (new x) :: U
 2. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> Cast x1 x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Cast x1 x2) :: U
 3. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> Val x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Val x) :: U
 4. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1 \<guillemotleft>x2\<guillemotright> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3) :: U
 5. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1:=x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1:=x2) :: U
 6. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3}) :: U
 7. \<And>x1 x2 x3 x4 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x4 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} := x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4) :: U
 8. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts Us. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 [::] Us; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compEs\<^sub>1 Vs x3 [::] Us; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2(x3) :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2(x3)) :: U
 9. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> {x1:x2; x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs {x1:x2; x3} :: U
 10. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1;; x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1;; x2) :: U
A total of 16 subgoals...
[PROOF STEP]
case LAss
[PROOF STATE]
proof (state)
this:
\<lbrakk>P,[?Vs [\<mapsto>] ?Ts] \<turnstile> x2_ :: ?U; length ?Ts = length ?Vs\<rbrakk> \<Longrightarrow> compP f P,?Ts \<turnstile>\<^sub>1 compE\<^sub>1 ?Vs x2_ :: ?U
P,[Vs [\<mapsto>] Ts] \<turnstile> x1_:=x2_ :: U
length Ts = length Vs

goal (16 subgoals):
 1. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> new x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (new x) :: U
 2. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> Cast x1 x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Cast x1 x2) :: U
 3. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> Val x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Val x) :: U
 4. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1 \<guillemotleft>x2\<guillemotright> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3) :: U
 5. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1:=x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1:=x2) :: U
 6. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3}) :: U
 7. \<And>x1 x2 x3 x4 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x4 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} := x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4) :: U
 8. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts Us. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 [::] Us; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compEs\<^sub>1 Vs x3 [::] Us; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2(x3) :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2(x3)) :: U
 9. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> {x1:x2; x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs {x1:x2; x3} :: U
 10. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1;; x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1;; x2) :: U
A total of 16 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>P,[?Vs [\<mapsto>] ?Ts] \<turnstile> x2_ :: ?U; length ?Ts = length ?Vs\<rbrakk> \<Longrightarrow> compP f P,?Ts \<turnstile>\<^sub>1 compE\<^sub>1 ?Vs x2_ :: ?U
P,[Vs [\<mapsto>] Ts] \<turnstile> x1_:=x2_ :: U
length Ts = length Vs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>P,[?Vs [\<mapsto>] ?Ts] \<turnstile> x2_ :: ?U; length ?Ts = length ?Vs\<rbrakk> \<Longrightarrow> compP f P,?Ts \<turnstile>\<^sub>1 compE\<^sub>1 ?Vs x2_ :: ?U
P,[Vs [\<mapsto>] Ts] \<turnstile> x1_:=x2_ :: U
length Ts = length Vs

goal (1 subgoal):
 1. compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1_:=x2_) :: U
[PROOF STEP]
by (fastforce simp:map_upds_apply_eq_Some split:if_split_asm)
[PROOF STATE]
proof (state)
this:
compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1_:=x2_) :: U

goal (15 subgoals):
 1. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> new x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (new x) :: U
 2. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> Cast x1 x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Cast x1 x2) :: U
 3. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> Val x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Val x) :: U
 4. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1 \<guillemotleft>x2\<guillemotright> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3) :: U
 5. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3}) :: U
 6. \<And>x1 x2 x3 x4 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x4 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} := x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4) :: U
 7. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts Us. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 [::] Us; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compEs\<^sub>1 Vs x3 [::] Us; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2(x3) :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2(x3)) :: U
 8. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> {x1:x2; x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs {x1:x2; x3} :: U
 9. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1;; x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1;; x2) :: U
 10. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> if (x1) x2 else x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (if (x1) x2 else x3) :: U
A total of 15 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (15 subgoals):
 1. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> new x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (new x) :: U
 2. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> Cast x1 x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Cast x1 x2) :: U
 3. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> Val x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Val x) :: U
 4. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1 \<guillemotleft>x2\<guillemotright> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3) :: U
 5. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3}) :: U
 6. \<And>x1 x2 x3 x4 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x4 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} := x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4) :: U
 7. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts Us. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 [::] Us; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compEs\<^sub>1 Vs x3 [::] Us; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2(x3) :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2(x3)) :: U
 8. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> {x1:x2; x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs {x1:x2; x3} :: U
 9. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1;; x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1;; x2) :: U
 10. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> if (x1) x2 else x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (if (x1) x2 else x3) :: U
A total of 15 subgoals...
[PROOF STEP]
case Call
[PROOF STATE]
proof (state)
this:
\<lbrakk>P,[?Vs [\<mapsto>] ?Ts] \<turnstile> x1_ :: ?U; length ?Ts = length ?Vs\<rbrakk> \<Longrightarrow> compP f P,?Ts \<turnstile>\<^sub>1 compE\<^sub>1 ?Vs x1_ :: ?U
\<lbrakk>P,[?Vs [\<mapsto>] ?Ts] \<turnstile> x3_ [::] ?Us; length ?Ts = length ?Vs\<rbrakk> \<Longrightarrow> compP f P,?Ts \<turnstile>\<^sub>1 compEs\<^sub>1 ?Vs x3_ [::] ?Us
P,[Vs [\<mapsto>] Ts] \<turnstile> x1_\<bullet>x2_(x3_) :: U
length Ts = length Vs

goal (15 subgoals):
 1. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> new x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (new x) :: U
 2. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> Cast x1 x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Cast x1 x2) :: U
 3. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> Val x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Val x) :: U
 4. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1 \<guillemotleft>x2\<guillemotright> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3) :: U
 5. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3}) :: U
 6. \<And>x1 x2 x3 x4 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x4 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} := x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4) :: U
 7. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts Us. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 [::] Us; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compEs\<^sub>1 Vs x3 [::] Us; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2(x3) :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2(x3)) :: U
 8. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> {x1:x2; x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs {x1:x2; x3} :: U
 9. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1;; x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1;; x2) :: U
 10. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> if (x1) x2 else x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (if (x1) x2 else x3) :: U
A total of 15 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>P,[?Vs [\<mapsto>] ?Ts] \<turnstile> x1_ :: ?U; length ?Ts = length ?Vs\<rbrakk> \<Longrightarrow> compP f P,?Ts \<turnstile>\<^sub>1 compE\<^sub>1 ?Vs x1_ :: ?U
\<lbrakk>P,[?Vs [\<mapsto>] ?Ts] \<turnstile> x3_ [::] ?Us; length ?Ts = length ?Vs\<rbrakk> \<Longrightarrow> compP f P,?Ts \<turnstile>\<^sub>1 compEs\<^sub>1 ?Vs x3_ [::] ?Us
P,[Vs [\<mapsto>] Ts] \<turnstile> x1_\<bullet>x2_(x3_) :: U
length Ts = length Vs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>P,[?Vs [\<mapsto>] ?Ts] \<turnstile> x1_ :: ?U; length ?Ts = length ?Vs\<rbrakk> \<Longrightarrow> compP f P,?Ts \<turnstile>\<^sub>1 compE\<^sub>1 ?Vs x1_ :: ?U
\<lbrakk>P,[?Vs [\<mapsto>] ?Ts] \<turnstile> x3_ [::] ?Us; length ?Ts = length ?Vs\<rbrakk> \<Longrightarrow> compP f P,?Ts \<turnstile>\<^sub>1 compEs\<^sub>1 ?Vs x3_ [::] ?Us
P,[Vs [\<mapsto>] Ts] \<turnstile> x1_\<bullet>x2_(x3_) :: U
length Ts = length Vs

goal (1 subgoal):
 1. compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1_\<bullet>x2_(x3_)) :: U
[PROOF STEP]
by (fastforce dest!: sees_method_compP[where f = f])
[PROOF STATE]
proof (state)
this:
compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1_\<bullet>x2_(x3_)) :: U

goal (14 subgoals):
 1. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> new x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (new x) :: U
 2. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> Cast x1 x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Cast x1 x2) :: U
 3. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> Val x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Val x) :: U
 4. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1 \<guillemotleft>x2\<guillemotright> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3) :: U
 5. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3}) :: U
 6. \<And>x1 x2 x3 x4 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x4 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} := x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4) :: U
 7. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> {x1:x2; x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs {x1:x2; x3} :: U
 8. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1;; x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1;; x2) :: U
 9. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> if (x1) x2 else x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (if (x1) x2 else x3) :: U
 10. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> while (x1) x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (while (x1) x2) :: U
A total of 14 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (14 subgoals):
 1. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> new x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (new x) :: U
 2. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> Cast x1 x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Cast x1 x2) :: U
 3. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> Val x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Val x) :: U
 4. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1 \<guillemotleft>x2\<guillemotright> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3) :: U
 5. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3}) :: U
 6. \<And>x1 x2 x3 x4 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x4 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} := x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4) :: U
 7. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> {x1:x2; x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs {x1:x2; x3} :: U
 8. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1;; x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1;; x2) :: U
 9. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> if (x1) x2 else x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (if (x1) x2 else x3) :: U
 10. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> while (x1) x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (while (x1) x2) :: U
A total of 14 subgoals...
[PROOF STEP]
case Block
[PROOF STATE]
proof (state)
this:
\<lbrakk>P,[?Vs [\<mapsto>] ?Ts] \<turnstile> x3_ :: ?U; length ?Ts = length ?Vs\<rbrakk> \<Longrightarrow> compP f P,?Ts \<turnstile>\<^sub>1 compE\<^sub>1 ?Vs x3_ :: ?U
P,[Vs [\<mapsto>] Ts] \<turnstile> {x1_:x2_; x3_} :: U
length Ts = length Vs

goal (14 subgoals):
 1. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> new x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (new x) :: U
 2. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> Cast x1 x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Cast x1 x2) :: U
 3. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> Val x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Val x) :: U
 4. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1 \<guillemotleft>x2\<guillemotright> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3) :: U
 5. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3}) :: U
 6. \<And>x1 x2 x3 x4 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x4 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} := x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4) :: U
 7. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> {x1:x2; x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs {x1:x2; x3} :: U
 8. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1;; x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1;; x2) :: U
 9. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> if (x1) x2 else x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (if (x1) x2 else x3) :: U
 10. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> while (x1) x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (while (x1) x2) :: U
A total of 14 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>P,[?Vs [\<mapsto>] ?Ts] \<turnstile> x3_ :: ?U; length ?Ts = length ?Vs\<rbrakk> \<Longrightarrow> compP f P,?Ts \<turnstile>\<^sub>1 compE\<^sub>1 ?Vs x3_ :: ?U
P,[Vs [\<mapsto>] Ts] \<turnstile> {x1_:x2_; x3_} :: U
length Ts = length Vs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>P,[?Vs [\<mapsto>] ?Ts] \<turnstile> x3_ :: ?U; length ?Ts = length ?Vs\<rbrakk> \<Longrightarrow> compP f P,?Ts \<turnstile>\<^sub>1 compE\<^sub>1 ?Vs x3_ :: ?U
P,[Vs [\<mapsto>] Ts] \<turnstile> {x1_:x2_; x3_} :: U
length Ts = length Vs

goal (1 subgoal):
 1. compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs {x1_:x2_; x3_} :: U
[PROOF STEP]
by (fastforce simp:nth_append)
[PROOF STATE]
proof (state)
this:
compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs {x1_:x2_; x3_} :: U

goal (13 subgoals):
 1. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> new x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (new x) :: U
 2. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> Cast x1 x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Cast x1 x2) :: U
 3. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> Val x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Val x) :: U
 4. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1 \<guillemotleft>x2\<guillemotright> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3) :: U
 5. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3}) :: U
 6. \<And>x1 x2 x3 x4 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x4 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} := x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4) :: U
 7. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1;; x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1;; x2) :: U
 8. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> if (x1) x2 else x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (if (x1) x2 else x3) :: U
 9. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> while (x1) x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (while (x1) x2) :: U
 10. \<And>x Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> throw x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (throw x) :: U
A total of 13 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> new x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (new x) :: U
 2. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> Cast x1 x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Cast x1 x2) :: U
 3. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> Val x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Val x) :: U
 4. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1 \<guillemotleft>x2\<guillemotright> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3) :: U
 5. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3}) :: U
 6. \<And>x1 x2 x3 x4 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x4 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} := x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4) :: U
 7. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1;; x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1;; x2) :: U
 8. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> if (x1) x2 else x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (if (x1) x2 else x3) :: U
 9. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> while (x1) x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (while (x1) x2) :: U
 10. \<And>x Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> throw x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (throw x) :: U
A total of 13 subgoals...
[PROOF STEP]
case TryCatch
[PROOF STATE]
proof (state)
this:
\<lbrakk>P,[?Vs [\<mapsto>] ?Ts] \<turnstile> x1_ :: ?U; length ?Ts = length ?Vs\<rbrakk> \<Longrightarrow> compP f P,?Ts \<turnstile>\<^sub>1 compE\<^sub>1 ?Vs x1_ :: ?U
\<lbrakk>P,[?Vs [\<mapsto>] ?Ts] \<turnstile> x4_ :: ?U; length ?Ts = length ?Vs\<rbrakk> \<Longrightarrow> compP f P,?Ts \<turnstile>\<^sub>1 compE\<^sub>1 ?Vs x4_ :: ?U
P,[Vs [\<mapsto>] Ts] \<turnstile> try x1_ catch(x2_ x3_) x4_ :: U
length Ts = length Vs

goal (13 subgoals):
 1. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> new x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (new x) :: U
 2. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> Cast x1 x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Cast x1 x2) :: U
 3. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> Val x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Val x) :: U
 4. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1 \<guillemotleft>x2\<guillemotright> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3) :: U
 5. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3}) :: U
 6. \<And>x1 x2 x3 x4 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x4 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} := x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4) :: U
 7. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1;; x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1;; x2) :: U
 8. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> if (x1) x2 else x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (if (x1) x2 else x3) :: U
 9. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> while (x1) x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (while (x1) x2) :: U
 10. \<And>x Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> throw x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (throw x) :: U
A total of 13 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>P,[?Vs [\<mapsto>] ?Ts] \<turnstile> x1_ :: ?U; length ?Ts = length ?Vs\<rbrakk> \<Longrightarrow> compP f P,?Ts \<turnstile>\<^sub>1 compE\<^sub>1 ?Vs x1_ :: ?U
\<lbrakk>P,[?Vs [\<mapsto>] ?Ts] \<turnstile> x4_ :: ?U; length ?Ts = length ?Vs\<rbrakk> \<Longrightarrow> compP f P,?Ts \<turnstile>\<^sub>1 compE\<^sub>1 ?Vs x4_ :: ?U
P,[Vs [\<mapsto>] Ts] \<turnstile> try x1_ catch(x2_ x3_) x4_ :: U
length Ts = length Vs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>P,[?Vs [\<mapsto>] ?Ts] \<turnstile> x1_ :: ?U; length ?Ts = length ?Vs\<rbrakk> \<Longrightarrow> compP f P,?Ts \<turnstile>\<^sub>1 compE\<^sub>1 ?Vs x1_ :: ?U
\<lbrakk>P,[?Vs [\<mapsto>] ?Ts] \<turnstile> x4_ :: ?U; length ?Ts = length ?Vs\<rbrakk> \<Longrightarrow> compP f P,?Ts \<turnstile>\<^sub>1 compE\<^sub>1 ?Vs x4_ :: ?U
P,[Vs [\<mapsto>] Ts] \<turnstile> try x1_ catch(x2_ x3_) x4_ :: U
length Ts = length Vs

goal (1 subgoal):
 1. compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (try x1_ catch(x2_ x3_) x4_) :: U
[PROOF STEP]
by (fastforce simp:nth_append)
[PROOF STATE]
proof (state)
this:
compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (try x1_ catch(x2_ x3_) x4_) :: U

goal (12 subgoals):
 1. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> new x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (new x) :: U
 2. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> Cast x1 x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Cast x1 x2) :: U
 3. \<And>x Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> Val x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (Val x) :: U
 4. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1 \<guillemotleft>x2\<guillemotright> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3) :: U
 5. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3}) :: U
 6. \<And>x1 x2 x3 x4 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x4 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1\<bullet>x2{x3} := x4 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4) :: U
 7. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> x1;; x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (x1;; x2) :: U
 8. \<And>x1 x2 x3 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x3 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> if (x1) x2 else x3 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (if (x1) x2 else x3) :: U
 9. \<And>x1 x2 Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x1 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x1 :: U; \<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x2 :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> while (x1) x2 :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (while (x1) x2) :: U
 10. \<And>x Vs Ts U. \<lbrakk>\<And>Vs Ts U. \<lbrakk>P,[Vs [\<mapsto>] Ts] \<turnstile> x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs x :: U; P,[Vs [\<mapsto>] Ts] \<turnstile> throw x :: U; length Ts = length Vs\<rbrakk> \<Longrightarrow> compP f P,Ts \<turnstile>\<^sub>1 compE\<^sub>1 Vs (throw x) :: U
A total of 12 subgoals...
[PROOF STEP]
qed fastforce+


[STATEMENT]
lemma \<B>: "\<And>Vs n. size Vs = n \<Longrightarrow> \<B> (compE\<^sub>1 Vs e) n"
and \<B>s: "\<And>Vs n. size Vs = n \<Longrightarrow> \<B>s (compEs\<^sub>1 Vs es) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Vs n. length Vs = n \<Longrightarrow> \<B> (compE\<^sub>1 Vs e) n) &&& (\<And>Vs n. length Vs = n \<Longrightarrow> \<B>s (compEs\<^sub>1 Vs es) n)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Vs n. length Vs = n \<Longrightarrow> \<B> (compE\<^sub>1 Vs e) n) &&& (\<And>Vs n. length Vs = n \<Longrightarrow> \<B>s (compEs\<^sub>1 Vs es) n)
[PROOF STEP]
by (induct e and es rule: \<B>.induct \<B>s.induct)
        (force | simp,metis length_append_singleton)+


[STATEMENT]
lemma image_last_index: "A \<subseteq> set(xs@[x]) \<Longrightarrow> last_index (xs @ [x]) ` A =
  (if x \<in> A then insert (size xs) (last_index xs ` (A-{x})) else last_index xs ` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> set (xs @ [x]) \<Longrightarrow> last_index (xs @ [x]) ` A = (if x \<in> A then insert (length xs) (last_index xs ` (A - {x})) else last_index xs ` A)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> set (xs @ [x]) \<Longrightarrow> last_index (xs @ [x]) ` A = (if x \<in> A then insert (length xs) (last_index xs ` (A - {x})) else last_index xs ` A)
[PROOF STEP]
by(auto simp:image_def)


[STATEMENT]
lemma A_compE\<^sub>1_None[simp]:
      "\<And>Vs. \ e = None \<Longrightarrow> \ (compE\<^sub>1 Vs e) = None"
and "\<And>Vs. \s es = None \<Longrightarrow> \s (compEs\<^sub>1 Vs es) = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Vs. \ e = None \<Longrightarrow> \ (compE\<^sub>1 Vs e) = None) &&& (\<And>Vs. \s es = None \<Longrightarrow> \s (compEs\<^sub>1 Vs es) = None)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Vs. \ e = None \<Longrightarrow> \ (compE\<^sub>1 Vs e) = None) &&& (\<And>Vs. \s es = None \<Longrightarrow> \s (compEs\<^sub>1 Vs es) = None)
[PROOF STEP]
by(induct e and es rule: compE\<^sub>1.induct compEs\<^sub>1.induct)(auto simp:hyperset_defs)