[STATEMENT]
lemma fixes e :: "'addr expr1" and es :: "'addr expr1 list"
  shows compE1_Goto_not_same: "\<lbrakk> compE2 e ! pc = Goto i; pc < length (compE2 e) \<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc"
  and compEs2_Goto_not_same: "\<lbrakk> compEs2 es ! pc = Goto i; pc < length (compEs2 es) \<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>compE2 e ! pc = Goto i; pc < length (compE2 e)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc) &&& (\<lbrakk>compEs2 es ! pc = Goto i; pc < length (compEs2 es)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc)
[PROOF STEP]
apply(induct e and es arbitrary: pc i and pc i rule: compE2.induct compEs2.induct)
[PROOF STATE]
proof (prove)
goal (25 subgoals):
 1. \<And>x pc i. \<lbrakk>compE2 (new x) ! pc = Goto i; pc < length (compE2 (new x))\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc
 2. \<And>x1 x2 pc i. \<lbrakk>\<And>pc i. \<lbrakk>compE2 x2 ! pc = Goto i; pc < length (compE2 x2)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; compE2 (newA x1\<lfloor>x2\<rceil>) ! pc = Goto i; pc < length (compE2 (newA x1\<lfloor>x2\<rceil>))\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc
 3. \<And>x1 x2 pc i. \<lbrakk>\<And>pc i. \<lbrakk>compE2 x2 ! pc = Goto i; pc < length (compE2 x2)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; compE2 (Cast x1 x2) ! pc = Goto i; pc < length (compE2 (Cast x1 x2))\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc
 4. \<And>x1 x2 pc i. \<lbrakk>\<And>pc i. \<lbrakk>compE2 x1 ! pc = Goto i; pc < length (compE2 x1)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; compE2 (x1 instanceof x2) ! pc = Goto i; pc < length (compE2 (x1 instanceof x2))\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc
 5. \<And>x pc i. \<lbrakk>compE2 (Val x) ! pc = Goto i; pc < length (compE2 (Val x))\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc
 6. \<And>x1 x2 x3 pc i. \<lbrakk>\<And>pc i. \<lbrakk>compE2 x1 ! pc = Goto i; pc < length (compE2 x1)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<And>pc i. \<lbrakk>compE2 x3 ! pc = Goto i; pc < length (compE2 x3)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; compE2 (x1 \<guillemotleft>x2\<guillemotright> x3) ! pc = Goto i; pc < length (compE2 (x1 \<guillemotleft>x2\<guillemotright> x3))\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc
 7. \<And>x pc i. \<lbrakk>compE2 (Var x) ! pc = Goto i; pc < length (compE2 (Var x))\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc
 8. \<And>x1 x2 pc i. \<lbrakk>\<And>pc i. \<lbrakk>compE2 x2 ! pc = Goto i; pc < length (compE2 x2)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; compE2 (x1:=x2) ! pc = Goto i; pc < length (compE2 (x1:=x2))\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc
 9. \<And>x1 x2 pc i. \<lbrakk>\<And>pc i. \<lbrakk>compE2 x1 ! pc = Goto i; pc < length (compE2 x1)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<And>pc i. \<lbrakk>compE2 x2 ! pc = Goto i; pc < length (compE2 x2)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; compE2 (x1\<lfloor>x2\<rceil>) ! pc = Goto i; pc < length (compE2 (x1\<lfloor>x2\<rceil>))\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc
 10. \<And>x1 x2 x3 pc i. \<lbrakk>\<And>pc i. \<lbrakk>compE2 x1 ! pc = Goto i; pc < length (compE2 x1)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<And>pc i. \<lbrakk>compE2 x2 ! pc = Goto i; pc < length (compE2 x2)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<And>pc i. \<lbrakk>compE2 x3 ! pc = Goto i; pc < length (compE2 x3)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; compE2 (x1\<lfloor>x2\<rceil> := x3) ! pc = Goto i; pc < length (compE2 (x1\<lfloor>x2\<rceil> := x3))\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc
A total of 25 subgoals...
[PROOF STEP]
apply(auto simp add: nth_Cons nth_append split: if_split_asm bop.split_asm nat.splits)
[PROOF STATE]
proof (prove)
goal (16 subgoals):
 1. \<And>x1 x3 pc i. \<lbrakk>pc < Suc (length (compE2 x1) + length (compE2 x3)); \<And>pc i. \<lbrakk>compE2 x1 ! pc = Goto i; pc < length (compE2 x1)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<And>pc i. \<lbrakk>compE2 x3 ! pc = Goto i; pc < length (compE2 x3)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<not> pc < length (compE2 x1); pc - length (compE2 x1) < length (compE2 x3); compE2 x3 ! (pc - length (compE2 x1)) = Goto i; nat (int pc + i) = pc\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2 pc i. \<lbrakk>pc < Suc (length (compE2 x1) + length (compE2 x2)); \<And>pc i. \<lbrakk>compE2 x1 ! pc = Goto i; pc < length (compE2 x1)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<And>pc i. \<lbrakk>compE2 x2 ! pc = Goto i; pc < length (compE2 x2)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<not> pc < length (compE2 x1); pc - length (compE2 x1) < length (compE2 x2); compE2 x2 ! (pc - length (compE2 x1)) = Goto i; nat (int pc + i) = pc\<rbrakk> \<Longrightarrow> False
 3. \<And>x1 x2 x3 pc i. \<lbrakk>pc < Suc (Suc (length (compE2 x1) + (length (compE2 x2) + length (compE2 x3)))); \<And>pc i. \<lbrakk>compE2 x1 ! pc = Goto i; pc < length (compE2 x1)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<And>pc i. \<lbrakk>compE2 x2 ! pc = Goto i; pc < length (compE2 x2)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<And>pc i. \<lbrakk>compE2 x3 ! pc = Goto i; pc < length (compE2 x3)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<not> pc < length (compE2 x1); pc - length (compE2 x1) < length (compE2 x2); compE2 x2 ! (pc - length (compE2 x1)) = Goto i; nat (int pc + i) = pc\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2 x3 pc i. \<lbrakk>pc < Suc (Suc (length (compE2 x1) + (length (compE2 x2) + length (compE2 x3)))); \<And>pc i. \<lbrakk>compE2 x1 ! pc = Goto i; pc < length (compE2 x1)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<And>pc i. \<lbrakk>compE2 x2 ! pc = Goto i; pc < length (compE2 x2)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<And>pc i. \<lbrakk>compE2 x3 ! pc = Goto i; pc < length (compE2 x3)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<not> pc < length (compE2 x1); \<not> pc - length (compE2 x1) < length (compE2 x2); pc - (length (compE2 x1) + length (compE2 x2)) < length (compE2 x3); compE2 x3 ! (pc - (length (compE2 x1) + length (compE2 x2))) = Goto i; nat (int pc + i) = pc\<rbrakk> \<Longrightarrow> False
 5. \<And>x1 x4 pc i. \<lbrakk>pc < Suc (Suc (length (compE2 x1) + length (compE2 x4))); \<And>pc i. \<lbrakk>compE2 x1 ! pc = Goto i; pc < length (compE2 x1)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<And>pc i. \<lbrakk>compE2 x4 ! pc = Goto i; pc < length (compE2 x4)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<not> pc < length (compE2 x1); pc - length (compE2 x1) < length (compE2 x4); compE2 x4 ! (pc - length (compE2 x1)) = Goto i; nat (int pc + i) = pc\<rbrakk> \<Longrightarrow> False
 6. \<And>x1 x4 x5 pc i. \<lbrakk>pc < Suc (length (compE2 x1) + (length (compE2 x4) + length (compE2 x5))); \<And>pc i. \<lbrakk>compE2 x1 ! pc = Goto i; pc < length (compE2 x1)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<And>pc i. \<lbrakk>compE2 x4 ! pc = Goto i; pc < length (compE2 x4)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<And>pc i. \<lbrakk>compE2 x5 ! pc = Goto i; pc < length (compE2 x5)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<not> pc < length (compE2 x1); pc - length (compE2 x1) < length (compE2 x4); compE2 x4 ! (pc - length (compE2 x1)) = Goto i; nat (int pc + i) = pc\<rbrakk> \<Longrightarrow> False
 7. \<And>x1 x4 x5 pc i. \<lbrakk>pc < Suc (length (compE2 x1) + (length (compE2 x4) + length (compE2 x5))); \<And>pc i. \<lbrakk>compE2 x1 ! pc = Goto i; pc < length (compE2 x1)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<And>pc i. \<lbrakk>compE2 x4 ! pc = Goto i; pc < length (compE2 x4)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<And>pc i. \<lbrakk>compE2 x5 ! pc = Goto i; pc < length (compE2 x5)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<not> pc < length (compE2 x1); \<not> pc - length (compE2 x1) < length (compE2 x4); pc - (length (compE2 x1) + length (compE2 x4)) < length (compE2 x5); compE2 x5 ! (pc - (length (compE2 x1) + length (compE2 x4))) = Goto i; nat (int pc + i) = pc\<rbrakk> \<Longrightarrow> False
 8. \<And>x1 x3 pc i. \<lbrakk>pc < Suc (length (compE2 x1) + length (compEs2 x3)); \<And>pc i. \<lbrakk>compE2 x1 ! pc = Goto i; pc < length (compE2 x1)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<And>pc i. \<lbrakk>compEs2 x3 ! pc = Goto i; pc < length (compEs2 x3)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<not> pc < length (compE2 x1); pc - length (compE2 x1) < length (compEs2 x3); compEs2 x3 ! (pc - length (compE2 x1)) = Goto i; nat (int pc + i) = pc\<rbrakk> \<Longrightarrow> False
 9. \<And>x4 pc i. \<lbrakk>pc < Suc (Suc (length (compE2 x4))); \<And>pc i. \<lbrakk>compE2 x4 ! pc = Goto i; pc < length (compE2 x4)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<not> pc < Suc (Suc 0); compE2 x4 ! (pc - Suc (Suc 0)) = Goto i; nat (int pc + i) = pc\<rbrakk> \<Longrightarrow> False
 10. \<And>x2 x3 pc i x2c. \<lbrakk>pc < Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (length (compE2 x2) + length (compE2 x3)))))))))); \<And>pc i. \<lbrakk>compE2 x2 ! pc = Goto i; pc < length (compE2 x2)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<And>pc i. \<lbrakk>compE2 x3 ! pc = Goto i; pc < length (compE2 x3)\<rbrakk> \<Longrightarrow> nat (int pc + i) \<noteq> pc; \<not> pc < length (compE2 x2); pc - length (compE2 x2) = Suc (Suc (Suc x2c)); x2c < length (compE2 x3); compE2 x3 ! x2c = Goto i; nat (int pc + i) = pc\<rbrakk> \<Longrightarrow> False
A total of 16 subgoals...
[PROOF STEP]
apply fastforce+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma wf_ciI:
  "\<lbrakk> ci_stk_offer ci;
    \<And>ins P h stk loc C M pc frs. ci ins P h stk loc C M pc frs \<Longrightarrow> check_instr' ins P h stk loc C M pc frs;
    \<And>ins P h stk loc C M pc pc' frs. \<lbrakk> ci ins P h stk loc C M pc frs; ins_jump_ok ins pc' \<rbrakk> \<Longrightarrow> ci ins P h stk loc C M pc' frs \<rbrakk>
  \<Longrightarrow> wf_ci ci"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ci_stk_offer ci; \<And>ins P h stk loc C M pc frs. ci ins P h stk loc C M pc frs \<Longrightarrow> check_instr' ins P h stk loc C M pc frs; \<And>ins P h stk loc C M pc pc' frs. \<lbrakk>ci ins P h stk loc C M pc frs; ins_jump_ok ins pc'\<rbrakk> \<Longrightarrow> ci ins P h stk loc C M pc' frs\<rbrakk> \<Longrightarrow> wf_ci ci
[PROOF STEP]
unfolding wf_ci_def le_fun_def le_bool_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ci_stk_offer ci; \<And>ins P h stk loc C M pc frs. ci ins P h stk loc C M pc frs \<Longrightarrow> check_instr' ins P h stk loc C M pc frs; \<And>ins P h stk loc C M pc pc' frs. \<lbrakk>ci ins P h stk loc C M pc frs; ins_jump_ok ins pc'\<rbrakk> \<Longrightarrow> ci ins P h stk loc C M pc' frs\<rbrakk> \<Longrightarrow> ci_stk_offer ci \<and> (\<forall>x xa xb xc xd xe xf xg xh. ci x xa xb xc xd xe xf xg xh \<longrightarrow> check_instr' x xa xb xc xd xe xf xg xh) \<and> (\<forall>ins P h stk loc C M pc pc' frs. ci ins P h stk loc C M pc frs \<longrightarrow> ins_jump_ok ins pc' \<longrightarrow> ci ins P h stk loc C M pc' frs)
[PROOF STEP]
by blast


[STATEMENT]
lemma check_instr'_pc:
  "\<lbrakk> check_instr' ins P h stk loc C M pc frs; ins_jump_ok ins pc' \<rbrakk> \<Longrightarrow> check_instr' ins P h stk loc C M pc' frs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>check_instr' ins P h stk loc C M pc frs; ins_jump_ok ins pc'\<rbrakk> \<Longrightarrow> check_instr' ins P h stk loc C M pc' frs
[PROOF STEP]
by(cases ins) auto


[STATEMENT]
lemma wf_ci_check_instr' [iff]:
  "wf_ci check_instr'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_ci check_instr'
[PROOF STEP]
apply(rule wf_ciI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ci_stk_offer check_instr'
 2. \<And>ins P h stk loc C M pc frs. check_instr' ins P h stk loc C M pc frs \<Longrightarrow> check_instr' ins P h stk loc C M pc frs
 3. \<And>ins P h stk loc C M pc pc' frs. \<lbrakk>check_instr' ins P h stk loc C M pc frs; ins_jump_ok ins pc'\<rbrakk> \<Longrightarrow> check_instr' ins P h stk loc C M pc' frs
[PROOF STEP]
apply(rule check_instr'_stk_offer)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ins P h stk loc C M pc frs. check_instr' ins P h stk loc C M pc frs \<Longrightarrow> check_instr' ins P h stk loc C M pc frs
 2. \<And>ins P h stk loc C M pc pc' frs. \<lbrakk>check_instr' ins P h stk loc C M pc frs; ins_jump_ok ins pc'\<rbrakk> \<Longrightarrow> check_instr' ins P h stk loc C M pc' frs
[PROOF STEP]
apply(assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ins P h stk loc C M pc pc' frs. \<lbrakk>check_instr' ins P h stk loc C M pc frs; ins_jump_ok ins pc'\<rbrakk> \<Longrightarrow> check_instr' ins P h stk loc C M pc' frs
[PROOF STEP]
apply(erule (1) check_instr'_pc)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma jump_ok_ins_jump_ok:
  "\<lbrakk> jump_ok ins n n'; pc < length ins \<rbrakk> \<Longrightarrow> ins_jump_ok (ins ! pc) (pc + n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>jump_ok ins n n'; pc < length ins\<rbrakk> \<Longrightarrow> ins_jump_ok (ins ! pc) (pc + n)
[PROOF STEP]
apply(induct ins arbitrary: n n' pc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n n' pc. \<lbrakk>jump_ok [] n n'; pc < length []\<rbrakk> \<Longrightarrow> ins_jump_ok ([] ! pc) (pc + n)
 2. \<And>a ins n n' pc. \<lbrakk>\<And>n n' pc. \<lbrakk>jump_ok ins n n'; pc < length ins\<rbrakk> \<Longrightarrow> ins_jump_ok (ins ! pc) (pc + n); jump_ok (a # ins) n n'; pc < length (a # ins)\<rbrakk> \<Longrightarrow> ins_jump_ok ((a # ins) ! pc) (pc + n)
[PROOF STEP]
apply(fastforce simp add: nth_Cons' gr0_conv_Suc split: instr.split_asm)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma check_instr_pc:
  "\<lbrakk> check_instr ins P h stk loc C M pc frs; ins_jump_ok ins pc' \<rbrakk> \<Longrightarrow> check_instr ins P h stk loc C M pc' frs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>check_instr ins P h stk loc C M pc frs; ins_jump_ok ins pc'\<rbrakk> \<Longrightarrow> check_instr ins P h stk loc C M pc' frs
[PROOF STEP]
by(cases ins) auto


[STATEMENT]
lemma wf_ci_check_instr [iff]:
  "wf_ci check_instr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_ci check_instr
[PROOF STEP]
apply(rule wf_ciI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ci_stk_offer check_instr
 2. \<And>ins P h stk loc C M pc frs. check_instr ins P h stk loc C M pc frs \<Longrightarrow> check_instr' ins P h stk loc C M pc frs
 3. \<And>ins P h stk loc C M pc pc' frs. \<lbrakk>check_instr ins P h stk loc C M pc frs; ins_jump_ok ins pc'\<rbrakk> \<Longrightarrow> check_instr ins P h stk loc C M pc' frs
[PROOF STEP]
apply(rule check_instr_stk_offer)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ins P h stk loc C M pc frs. check_instr ins P h stk loc C M pc frs \<Longrightarrow> check_instr' ins P h stk loc C M pc frs
 2. \<And>ins P h stk loc C M pc pc' frs. \<lbrakk>check_instr ins P h stk loc C M pc frs; ins_jump_ok ins pc'\<rbrakk> \<Longrightarrow> check_instr ins P h stk loc C M pc' frs
[PROOF STEP]
apply(erule check_instr_imp_check_instr')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ins P h stk loc C M pc pc' frs. \<lbrakk>check_instr ins P h stk loc C M pc frs; ins_jump_ok ins pc'\<rbrakk> \<Longrightarrow> check_instr ins P h stk loc C M pc' frs
[PROOF STEP]
apply(erule (1) check_instr_pc)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma wf_ciD1: "wf_ci ci \<Longrightarrow> ci_stk_offer ci"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_ci ci \<Longrightarrow> ci_stk_offer ci
[PROOF STEP]
unfolding wf_ci_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ci_stk_offer ci \<and> ci \<le> check_instr' \<and> (\<forall>ins P h stk loc C M pc pc' frs. ci ins P h stk loc C M pc frs \<longrightarrow> ins_jump_ok ins pc' \<longrightarrow> ci ins P h stk loc C M pc' frs) \<Longrightarrow> ci_stk_offer ci
[PROOF STEP]
by blast


[STATEMENT]
lemma wf_ciD2: "\<lbrakk> wf_ci ci; ci ins P h stk loc C M pc frs \<rbrakk> \<Longrightarrow> check_instr' ins P h stk loc C M pc frs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_ci ci; ci ins P h stk loc C M pc frs\<rbrakk> \<Longrightarrow> check_instr' ins P h stk loc C M pc frs
[PROOF STEP]
unfolding wf_ci_def le_fun_def le_bool_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ci_stk_offer ci \<and> (\<forall>x xa xb xc xd xe xf xg xh. ci x xa xb xc xd xe xf xg xh \<longrightarrow> check_instr' x xa xb xc xd xe xf xg xh) \<and> (\<forall>ins P h stk loc C M pc pc' frs. ci ins P h stk loc C M pc frs \<longrightarrow> ins_jump_ok ins pc' \<longrightarrow> ci ins P h stk loc C M pc' frs); ci ins P h stk loc C M pc frs\<rbrakk> \<Longrightarrow> check_instr' ins P h stk loc C M pc frs
[PROOF STEP]
by blast


[STATEMENT]
lemma wf_ciD3: "\<lbrakk> wf_ci ci; ci ins P h stk loc C M pc frs; ins_jump_ok ins pc' \<rbrakk> \<Longrightarrow> ci ins P h stk loc C M pc' frs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_ci ci; ci ins P h stk loc C M pc frs; ins_jump_ok ins pc'\<rbrakk> \<Longrightarrow> ci ins P h stk loc C M pc' frs
[PROOF STEP]
unfolding wf_ci_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ci_stk_offer ci \<and> ci \<le> check_instr' \<and> (\<forall>ins P h stk loc C M pc pc' frs. ci ins P h stk loc C M pc frs \<longrightarrow> ins_jump_ok ins pc' \<longrightarrow> ci ins P h stk loc C M pc' frs); ci ins P h stk loc C M pc frs; ins_jump_ok ins pc'\<rbrakk> \<Longrightarrow> ci ins P h stk loc C M pc' frs
[PROOF STEP]
by blast


[STATEMENT]
lemma check_instr'_ins_jump_ok: "check_instr' ins P h stk loc C M pc frs \<Longrightarrow> ins_jump_ok ins pc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_instr' ins P h stk loc C M pc frs \<Longrightarrow> ins_jump_ok ins pc
[PROOF STEP]
by(cases ins) auto


[STATEMENT]
lemma wf_ci_ins_jump_ok:
  assumes wf: "wf_ci ci"
  and ci: "ci ins P h stk loc C M pc frs"
  and pc': "pc \<le> pc'"
  shows "ins_jump_ok ins pc'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ins_jump_ok ins pc'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ins_jump_ok ins pc'
[PROOF STEP]
from wf ci
[PROOF STATE]
proof (chain)
picking this:
wf_ci ci
ci ins P h stk loc C M pc frs
[PROOF STEP]
have "check_instr' ins P h stk loc C M pc frs"
[PROOF STATE]
proof (prove)
using this:
wf_ci ci
ci ins P h stk loc C M pc frs

goal (1 subgoal):
 1. check_instr' ins P h stk loc C M pc frs
[PROOF STEP]
by(rule wf_ciD2)
[PROOF STATE]
proof (state)
this:
check_instr' ins P h stk loc C M pc frs

goal (1 subgoal):
 1. ins_jump_ok ins pc'
[PROOF STEP]
with pc'
[PROOF STATE]
proof (chain)
picking this:
pc \<le> pc'
check_instr' ins P h stk loc C M pc frs
[PROOF STEP]
have "check_instr' ins P h stk loc C M pc' frs"
[PROOF STATE]
proof (prove)
using this:
pc \<le> pc'
check_instr' ins P h stk loc C M pc frs

goal (1 subgoal):
 1. check_instr' ins P h stk loc C M pc' frs
[PROOF STEP]
by(cases ins) auto
[PROOF STATE]
proof (state)
this:
check_instr' ins P h stk loc C M pc' frs

goal (1 subgoal):
 1. ins_jump_ok ins pc'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
check_instr' ins P h stk loc C M pc' frs

goal (1 subgoal):
 1. ins_jump_ok ins pc'
[PROOF STEP]
by(rule check_instr'_ins_jump_ok)
[PROOF STATE]
proof (state)
this:
ins_jump_ok ins pc'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_ciD3': "\<lbrakk> wf_ci ci; ci ins P h stk loc C M pc frs; pc \<le> pc' \<rbrakk> \<Longrightarrow> ci ins P h stk loc C M pc' frs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_ci ci; ci ins P h stk loc C M pc frs; pc \<le> pc'\<rbrakk> \<Longrightarrow> ci ins P h stk loc C M pc' frs
[PROOF STEP]
apply(frule (2) wf_ci_ins_jump_ok)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_ci ci; ci ins P h stk loc C M pc frs; pc \<le> pc'; ins_jump_ok ins pc'\<rbrakk> \<Longrightarrow> ci ins P h stk loc C M pc' frs
[PROOF STEP]
apply(erule (2) wf_ciD3)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ci_app_check_instr' [simp]: "ci_app (Abs_check_instr check_instr') = check_instr'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ci_app (Abs_check_instr check_instr') = check_instr'
[PROOF STEP]
by(simp add: Abs_check_instr_inverse)


[STATEMENT]
lemma (in JVM_heap_base) ci_app_check_instr [simp]: "ci_app (Abs_check_instr check_instr) = check_instr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ci_app (Abs_check_instr check_instr) = check_instr
[PROOF STEP]
by(simp add: Abs_check_instr_inverse)


[STATEMENT]
lemma wf_ci_stk_offerD:
  "ci_app ci ins P h stk loc C M pc frs \<Longrightarrow> ci_app ci ins P h (stk @ stk') loc C M pc frs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ci_app ci ins P h stk loc C M pc frs \<Longrightarrow> ci_app ci ins P h (stk @ stk') loc C M pc frs
[PROOF STEP]
apply(rule ci_stk_offerD[OF wf_ciD1])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ci_app ci ins P h stk loc C M pc frs \<Longrightarrow> wf_ci (\<lambda>a b c d e f g h i. c)
 2. ci_app ci ins P h stk loc C M pc frs \<Longrightarrow> ci_app ci ins P h (stk @ stk') loc C M pc frs
[PROOF STEP]
back
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ci_app ci ins P h stk loc C M pc frs \<Longrightarrow> wf_ci (ci_app ci)
 2. ci_app ci ins P h stk loc C M pc frs \<Longrightarrow> ci_app ci ins P h stk loc C M pc frs
[PROOF STEP]
by(rule ci_app [simplified])


[STATEMENT]
lemma wf_ciD2_ci_app:
  "ci_app ci ins P h stk loc C M pc frs \<Longrightarrow> check_instr' ins P h stk loc C M pc frs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ci_app ci ins P h stk loc C M pc frs \<Longrightarrow> check_instr' ins P h stk loc C M pc frs
[PROOF STEP]
apply(cases ci)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>ci_app ci ins P h stk loc C M pc frs; ci = Abs_check_instr y; y \<in> Collect wf_ci\<rbrakk> \<Longrightarrow> check_instr' ins P h stk loc C M pc frs
[PROOF STEP]
apply(simp add: Abs_check_instr_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>y ins P h stk loc C M pc frs; ci = Abs_check_instr y; wf_ci y\<rbrakk> \<Longrightarrow> check_instr' ins P h stk loc C M pc frs
[PROOF STEP]
apply(erule (1) wf_ciD2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma wf_ciD3_ci_app:
  "\<lbrakk> ci_app ci ins P h stk loc C M pc frs; ins_jump_ok ins pc' \<rbrakk> \<Longrightarrow> ci_app ci ins P h stk loc C M pc' frs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ci_app ci ins P h stk loc C M pc frs; ins_jump_ok ins pc'\<rbrakk> \<Longrightarrow> ci_app ci ins P h stk loc C M pc' frs
[PROOF STEP]
apply(cases ci)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>ci_app ci ins P h stk loc C M pc frs; ins_jump_ok ins pc'; ci = Abs_check_instr y; y \<in> Collect wf_ci\<rbrakk> \<Longrightarrow> ci_app ci ins P h stk loc C M pc' frs
[PROOF STEP]
apply(simp add: Abs_check_instr_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>y ins P h stk loc C M pc frs; ins_jump_ok ins pc'; ci = Abs_check_instr y; wf_ci y\<rbrakk> \<Longrightarrow> y ins P h stk loc C M pc' frs
[PROOF STEP]
apply(erule (2) wf_ciD3)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma wf_ciD3'_ci_app: "\<lbrakk> ci_app ci ins P h stk loc C M pc frs; pc \<le> pc' \<rbrakk> \<Longrightarrow> ci_app ci ins P h stk loc C M pc' frs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ci_app ci ins P h stk loc C M pc frs; pc \<le> pc'\<rbrakk> \<Longrightarrow> ci_app ci ins P h stk loc C M pc' frs
[PROOF STEP]
apply(cases ci)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>ci_app ci ins P h stk loc C M pc frs; pc \<le> pc'; ci = Abs_check_instr y; y \<in> Collect wf_ci\<rbrakk> \<Longrightarrow> ci_app ci ins P h stk loc C M pc' frs
[PROOF STEP]
apply(simp add: Abs_check_instr_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>y ins P h stk loc C M pc frs; pc \<le> pc'; ci = Abs_check_instr y; wf_ci y\<rbrakk> \<Longrightarrow> y ins P h stk loc C M pc' frs
[PROOF STEP]
apply(erule (2) wf_ciD3')
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma exec_meth_instr:
  "exec_meth ci P ins xt t h (stk, loc, pc, None) ta h' (stk', loc', pc', xcp) \<longleftrightarrow>
   (ta, xcp, h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc [] \<and> pc < length ins \<and> ci_app ci (ins ! pc) P h stk loc undefined undefined pc []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci P ins xt t h (stk, loc, pc, None) ta h' (stk', loc', pc', xcp) = ((ta, xcp, h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc [] \<and> pc < length ins \<and> ci_app ci (ins ! pc) P h stk loc undefined undefined pc [])
[PROOF STEP]
by(auto elim: exec_meth.cases intro: exec_instr)


[STATEMENT]
lemma exec_meth_xcpt:
  "exec_meth ci P ins xt t h (stk, loc, pc, \<lfloor>xcp\<rfloor>) ta h (stk', loc', pc', xcp') \<longleftrightarrow>
   (\<exists>d. match_ex_table P (cname_of h xcp) pc xt = \<lfloor>(pc', d)\<rfloor> \<and> ta = \<epsilon> \<and> stk' = (Addr xcp # drop (size stk - d) stk) \<and> loc' = loc \<and> xcp' = None \<and> d \<le> length stk)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci P ins xt t h (stk, loc, pc, \<lfloor>xcp\<rfloor>) ta h (stk', loc', pc', xcp') = (\<exists>d. match_ex_table P (cname_of h xcp) pc xt = \<lfloor>(pc', d)\<rfloor> \<and> ta = \<lbrace>\<rbrace> \<and> stk' = Addr xcp # drop (length stk - d) stk \<and> loc' = loc \<and> xcp' = None \<and> d \<le> length stk)
[PROOF STEP]
by(auto elim: exec_meth.cases intro: exec_catch)


[STATEMENT]
lemma exec_meth_length_compE2D [dest]:
  "exec_meth ci P (compE2 e) (compxE2 e 0 d) t h (stk, loc, pc, xcp) ta h' s' \<Longrightarrow> pc < length (compE2 e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci P (compE2 e) (compxE2 e 0 d) t h (stk, loc, pc, xcp) ta h' s' \<Longrightarrow> pc < length (compE2 e)
[PROOF STEP]
apply(erule exec_meth.cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>taa xcpa h'a stk' loc' pc' pca ha stka loca. \<lbrakk>h = ha; (stk, loc, pc, xcp) = (stka, loca, pca, None); ta = taa; h' = h'a; s' = (stk', loc', pc', xcpa); (taa, xcpa, h'a, [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (compE2 e ! pca) P t ha stka loca undefined undefined pca []; pca < length (compE2 e); ci_app ci (compE2 e ! pca) P ha stka loca undefined undefined pca []\<rbrakk> \<Longrightarrow> pc < length (compE2 e)
 2. \<And>ha xcpa pca pc' da stka loca. \<lbrakk>h = ha; (stk, loc, pc, xcp) = (stka, loca, pca, \<lfloor>xcpa\<rfloor>); ta = \<lbrace>\<rbrace>; h' = ha; s' = (Addr xcpa # drop (length stka - da) stka, loca, pc', None); match_ex_table P (cname_of ha xcpa) pca (compxE2 e 0 d) = \<lfloor>(pc', da)\<rfloor>; da \<le> length stka\<rbrakk> \<Longrightarrow> pc < length (compE2 e)
[PROOF STEP]
apply(auto dest: match_ex_table_pc_length_compE2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma exec_meth_length_compEs2D [dest]:
  "exec_meth ci P (compEs2 es) (compxEs2 es 0 0) t h (stk, loc, pc, xcp) ta h' s' \<Longrightarrow> pc < length (compEs2 es)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci P (compEs2 es) (compxEs2 es 0 0) t h (stk, loc, pc, xcp) ta h' s' \<Longrightarrow> pc < length (compEs2 es)
[PROOF STEP]
apply(erule exec_meth.cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>taa xcpa h'a stk' loc' pc' pca ha stka loca. \<lbrakk>h = ha; (stk, loc, pc, xcp) = (stka, loca, pca, None); ta = taa; h' = h'a; s' = (stk', loc', pc', xcpa); (taa, xcpa, h'a, [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (compEs2 es ! pca) P t ha stka loca undefined undefined pca []; pca < length (compEs2 es); ci_app ci (compEs2 es ! pca) P ha stka loca undefined undefined pca []\<rbrakk> \<Longrightarrow> pc < length (compEs2 es)
 2. \<And>ha xcpa pca pc' d stka loca. \<lbrakk>h = ha; (stk, loc, pc, xcp) = (stka, loca, pca, \<lfloor>xcpa\<rfloor>); ta = \<lbrace>\<rbrace>; h' = ha; s' = (Addr xcpa # drop (length stka - d) stka, loca, pc', None); match_ex_table P (cname_of ha xcpa) pca (compxEs2 es 0 0) = \<lfloor>(pc', d)\<rfloor>; d \<le> length stka\<rbrakk> \<Longrightarrow> pc < length (compEs2 es)
[PROOF STEP]
apply(auto dest: match_ex_table_pc_length_compEs2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma exec_instr_stk_offer:
  assumes check: "check_instr' (ins ! pc) P h stk loc C M pc frs"
  and exec: "(ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs"
  shows "(ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
check_instr' (ins ! pc) P h stk loc C M pc frs
(ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs

goal (1 subgoal):
 1. (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
[PROOF STEP]
proof(cases "ins ! pc")
[PROOF STATE]
proof (state)
goal (24 subgoals):
 1. \<And>x1. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = Load x1\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 2. \<And>x2. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = Store x2\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 3. \<And>x3. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = Push x3\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 4. \<And>x4. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = New x4\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 5. \<And>x5. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = NewArray x5\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 6. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = ALoad\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 7. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = AStore\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 8. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = ALength\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 9. \<And>x91 x92. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = Getfield x91 x92\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 10. \<And>x101 x102. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = Putfield x101 x102\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
A total of 24 subgoals...
[PROOF STEP]
case (Invoke M n)
[PROOF STATE]
proof (state)
this:
ins ! pc = Invoke M n

goal (24 subgoals):
 1. \<And>x1. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = Load x1\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 2. \<And>x2. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = Store x2\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 3. \<And>x3. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = Push x3\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 4. \<And>x4. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = New x4\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 5. \<And>x5. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = NewArray x5\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 6. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = ALoad\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 7. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = AStore\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 8. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = ALength\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 9. \<And>x91 x92. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = Getfield x91 x92\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 10. \<And>x101 x102. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = Putfield x101 x102\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
A total of 24 subgoals...
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ins ! pc = Invoke M n

goal (1 subgoal):
 1. (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
[PROOF STEP]
using exec check
[PROOF STATE]
proof (prove)
using this:
ins ! pc = Invoke M n
(ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs
check_instr' (ins ! pc) P h stk loc C M pc frs

goal (1 subgoal):
 1. (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
[PROOF STEP]
by(auto split: if_split_asm extCallRet.splits split del: if_split simp add: split_beta nth_append min_def extRet2JVM_def)
[PROOF STATE]
proof (state)
this:
(ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs

goal (23 subgoals):
 1. \<And>x1. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = Load x1\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 2. \<And>x2. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = Store x2\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 3. \<And>x3. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = Push x3\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 4. \<And>x4. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = New x4\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 5. \<And>x5. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = NewArray x5\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 6. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = ALoad\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 7. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = AStore\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 8. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = ALength\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 9. \<And>x91 x92. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = Getfield x91 x92\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
 10. \<And>x101 x102. \<lbrakk>check_instr' (ins ! pc) P h stk loc C M pc frs; (ta', xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h stk loc C M pc frs; ins ! pc = Putfield x101 x102\<rbrakk> \<Longrightarrow> (ta', xcp', h', (stk' @ stk'', loc', C, M, pc') # frs) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc C M pc frs
A total of 23 subgoals...
[PROOF STEP]
qed(force simp add: nth_append is_Ref_def has_method_def nth_Cons split_beta hd_append tl_append neq_Nil_conv split: list.split if_split_asm nat.splits sum.split_asm)+


[STATEMENT]
lemma exec_meth_stk_offer:
  assumes exec: "exec_meth ci P ins xt t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
[PROOF STEP]
using exec
[PROOF STATE]
proof (prove)
using this:
exec_meth ci P ins xt t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) pc xt = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
[PROOF STEP]
case (exec_catch xcp d)
[PROOF STATE]
proof (state)
this:
xcp = \<lfloor>xcp\<rfloor>
ta = \<lbrace>\<rbrace>
h' = h
stk' = Addr xcp # drop (length stk - d) stk
loc' = loc
xcp' = None
match_ex_table P (cname_of h xcp) pc xt = \<lfloor>(pc', d)\<rfloor>
d \<le> length stk

goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) pc xt = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
[PROOF STEP]
from \<open>match_ex_table P (cname_of h xcp) pc xt = \<lfloor>(pc', d)\<rfloor>\<close>
[PROOF STATE]
proof (chain)
picking this:
match_ex_table P (cname_of h xcp) pc xt = \<lfloor>(pc', d)\<rfloor>
[PROOF STEP]
have "match_ex_table P (cname_of h xcp) pc (stack_xlift (length stk'') xt) = \<lfloor>(pc', length stk'' + d)\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
match_ex_table P (cname_of h xcp) pc xt = \<lfloor>(pc', d)\<rfloor>

goal (1 subgoal):
 1. match_ex_table P (cname_of h xcp) pc (stack_xlift (length stk'') xt) = \<lfloor>(pc', length stk'' + d)\<rfloor>
[PROOF STEP]
by(simp add: match_ex_table_stack_xlift)
[PROOF STATE]
proof (state)
this:
match_ex_table P (cname_of h xcp) pc (stack_xlift (length stk'') xt) = \<lfloor>(pc', length stk'' + d)\<rfloor>

goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) pc xt = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
match_ex_table P (cname_of h xcp) pc (stack_xlift (length stk'') xt) = \<lfloor>(pc', length stk'' + d)\<rfloor>

goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) pc xt = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
[PROOF STEP]
have "length stk'' + d \<le> length (stk @ stk'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length stk'' + d \<le> length (stk @ stk'')
[PROOF STEP]
using \<open>d \<le> length stk\<close>
[PROOF STATE]
proof (prove)
using this:
d \<le> length stk

goal (1 subgoal):
 1. length stk'' + d \<le> length (stk @ stk'')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length stk'' + d \<le> length (stk @ stk'')

goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) pc xt = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
match_ex_table P (cname_of h xcp) pc (stack_xlift (length stk'') xt) = \<lfloor>(pc', length stk'' + d)\<rfloor>
length stk'' + d \<le> length (stk @ stk'')
[PROOF STEP]
have "exec_meth ci P ins (stack_xlift (length stk'') xt) t h ((stk @ stk''), loc, pc, \<lfloor>xcp\<rfloor>) \<epsilon> h ((Addr xcp # drop (length (stk @ stk'') - (length stk'' + d)) (stk @ stk'')), loc, pc', None)"
[PROOF STATE]
proof (prove)
using this:
match_ex_table P (cname_of h xcp) pc (stack_xlift (length stk'') xt) = \<lfloor>(pc', length stk'' + d)\<rfloor>
length stk'' + d \<le> length (stk @ stk'')

goal (1 subgoal):
 1. exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, \<lfloor>xcp\<rfloor>) \<lbrace>\<rbrace> h (Addr xcp # drop (length (stk @ stk'') - (length stk'' + d)) (stk @ stk''), loc, pc', None)
[PROOF STEP]
by(rule exec_meth.exec_catch)
[PROOF STATE]
proof (state)
this:
exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, \<lfloor>xcp\<rfloor>) \<lbrace>\<rbrace> h (Addr xcp # drop (length (stk @ stk'') - (length stk'' + d)) (stk @ stk''), loc, pc', None)

goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table P (cname_of h xcpa) pc xt = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
[PROOF STEP]
with exec_catch
[PROOF STATE]
proof (chain)
picking this:
xcp = \<lfloor>xcp\<rfloor>
ta = \<lbrace>\<rbrace>
h' = h
stk' = Addr xcp # drop (length stk - d) stk
loc' = loc
xcp' = None
match_ex_table P (cname_of h xcp) pc xt = \<lfloor>(pc', d)\<rfloor>
d \<le> length stk
exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, \<lfloor>xcp\<rfloor>) \<lbrace>\<rbrace> h (Addr xcp # drop (length (stk @ stk'') - (length stk'' + d)) (stk @ stk''), loc, pc', None)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xcp = \<lfloor>xcp\<rfloor>
ta = \<lbrace>\<rbrace>
h' = h
stk' = Addr xcp # drop (length stk - d) stk
loc' = loc
xcp' = None
match_ex_table P (cname_of h xcp) pc xt = \<lfloor>(pc', d)\<rfloor>
d \<le> length stk
exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, \<lfloor>xcp\<rfloor>) \<lbrace>\<rbrace> h (Addr xcp # drop (length (stk @ stk'') - (length stk'' + d)) (stk @ stk''), loc, pc', None)

goal (1 subgoal):
 1. exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')

goal (1 subgoal):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
[PROOF STEP]
case exec_instr
[PROOF STATE]
proof (state)
this:
xcp = None
(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []
pc < length ins
ci_app ci (ins ! pc) P h stk loc undefined undefined pc []

goal (1 subgoal):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
[PROOF STEP]
note ciins = \<open>ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<close>
[PROOF STATE]
proof (state)
this:
ci_app ci (ins ! pc) P h stk loc undefined undefined pc []

goal (1 subgoal):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
[PROOF STEP]
hence "ci_app ci (ins ! pc) P h (stk @ stk'') loc undefined undefined pc []"
[PROOF STATE]
proof (prove)
using this:
ci_app ci (ins ! pc) P h stk loc undefined undefined pc []

goal (1 subgoal):
 1. ci_app ci (ins ! pc) P h (stk @ stk'') loc undefined undefined pc []
[PROOF STEP]
by(rule wf_ci_stk_offerD)
[PROOF STATE]
proof (state)
this:
ci_app ci (ins ! pc) P h (stk @ stk'') loc undefined undefined pc []

goal (1 subgoal):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ci_app ci (ins ! pc) P h (stk @ stk'') loc undefined undefined pc []

goal (1 subgoal):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
[PROOF STEP]
from ciins
[PROOF STATE]
proof (chain)
picking this:
ci_app ci (ins ! pc) P h stk loc undefined undefined pc []
[PROOF STEP]
have "check_instr' (ins ! pc) P h stk loc undefined undefined  pc []"
[PROOF STATE]
proof (prove)
using this:
ci_app ci (ins ! pc) P h stk loc undefined undefined pc []

goal (1 subgoal):
 1. check_instr' (ins ! pc) P h stk loc undefined undefined pc []
[PROOF STEP]
by(rule wf_ciD2_ci_app)
[PROOF STATE]
proof (state)
this:
check_instr' (ins ! pc) P h stk loc undefined undefined pc []

goal (1 subgoal):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
[PROOF STEP]
hence "(ta, xcp', h', [(stk' @ stk'', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc undefined undefined pc []"
[PROOF STATE]
proof (prove)
using this:
check_instr' (ins ! pc) P h stk loc undefined undefined pc []

goal (1 subgoal):
 1. (ta, xcp', h', [(stk' @ stk'', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc undefined undefined pc []
[PROOF STEP]
using \<open>(ta, xcp', h', [(stk', loc', undefined,undefined , pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []\<close>
[PROOF STATE]
proof (prove)
using this:
check_instr' (ins ! pc) P h stk loc undefined undefined pc []
(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []

goal (1 subgoal):
 1. (ta, xcp', h', [(stk' @ stk'', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc undefined undefined pc []
[PROOF STEP]
by(rule exec_instr_stk_offer)
[PROOF STATE]
proof (state)
this:
(ta, xcp', h', [(stk' @ stk'', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc undefined undefined pc []

goal (1 subgoal):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ci_app ci (ins ! pc) P h (stk @ stk'') loc undefined undefined pc []
(ta, xcp', h', [(stk' @ stk'', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc undefined undefined pc []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ci_app ci (ins ! pc) P h (stk @ stk'') loc undefined undefined pc []
(ta, xcp', h', [(stk' @ stk'', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc undefined undefined pc []

goal (1 subgoal):
 1. exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
[PROOF STEP]
using exec_instr
[PROOF STATE]
proof (prove)
using this:
ci_app ci (ins ! pc) P h (stk @ stk'') loc undefined undefined pc []
(ta, xcp', h', [(stk' @ stk'', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h (stk @ stk'') loc undefined undefined pc []
xcp = None
(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []
pc < length ins
ci_app ci (ins ! pc) P h stk loc undefined undefined pc []

goal (1 subgoal):
 1. exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')
[PROOF STEP]
by(auto intro: exec_meth.exec_instr)
[PROOF STATE]
proof (state)
this:
exec_meth ci P ins (stack_xlift (length stk'') xt) t h (stk @ stk'', loc, pc, xcp) ta h' (stk' @ stk'', loc', pc', xcp')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exec_meth_append_xt [intro]:
  "exec_meth ci P ins xt t h s ta h' s'
  \<Longrightarrow> exec_meth ci P (ins @ ins') (xt @ xt') t h s ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci P ins xt t h s ta h' s' \<Longrightarrow> exec_meth ci P (ins @ ins') (xt @ xt') t h s ta h' s'
[PROOF STEP]
apply(erule exec_meth.cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>taa xcp h'a stk' loc' pc' pc ha stk loc. \<lbrakk>h = ha; s = (stk, loc, pc, None); ta = taa; h' = h'a; s' = (stk', loc', pc', xcp); (taa, xcp, h'a, [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t ha stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P ha stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P (ins @ ins') (xt @ xt') t h s ta h' s'
 2. \<And>ha xcp pc pc' d stk loc. \<lbrakk>h = ha; s = (stk, loc, pc, \<lfloor>xcp\<rfloor>); ta = \<lbrace>\<rbrace>; h' = ha; s' = (Addr xcp # drop (length stk - d) stk, loc, pc', None); match_ex_table P (cname_of ha xcp) pc xt = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P (ins @ ins') (xt @ xt') t h s ta h' s'
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab ac ad b xcp stk' loc' pc' pc stk loc. \<lbrakk>s = (stk, loc, pc, None); ta = (a, aa, ab, ac, ad, b); s' = (stk', loc', pc', xcp); ((a, aa, ab, ac, ad, b), xcp, h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> exec_meth ci P (ins @ ins') (xt @ xt') t h (stk, loc, pc, None) (a, aa, ab, ac, ad, b) h' (stk', loc', pc', xcp)
 2. \<And>xcp pc pc' d stk loc. \<lbrakk>s = (stk, loc, pc, \<lfloor>xcp\<rfloor>); ta = \<lbrace>\<rbrace>; h' = h; s' = (Addr xcp # drop (length stk - d) stk, loc, pc', None); match_ex_table P (cname_of h xcp) pc xt = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P (ins @ ins') (xt @ xt') t h (stk, loc, pc, \<lfloor>xcp\<rfloor>) \<lbrace>\<rbrace> h (Addr xcp # drop (length stk - d) stk, loc, pc', None)
[PROOF STEP]
apply(rule exec_instr)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a aa ab ac ad b xcp stk' loc' pc' pc stk loc. \<lbrakk>s = (stk, loc, pc, None); ta = (a, aa, ab, ac, ad, b); s' = (stk', loc', pc', xcp); ((a, aa, ab, ac, ad, b), xcp, h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> ((a, aa, ab, ac, ad, b), xcp, h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr ((ins @ ins') ! pc) P t h stk loc undefined undefined pc []
 2. \<And>a aa ab ac ad b xcp stk' loc' pc' pc stk loc. \<lbrakk>s = (stk, loc, pc, None); ta = (a, aa, ab, ac, ad, b); s' = (stk', loc', pc', xcp); ((a, aa, ab, ac, ad, b), xcp, h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> pc < length (ins @ ins')
 3. \<And>a aa ab ac ad b xcp stk' loc' pc' pc stk loc. \<lbrakk>s = (stk, loc, pc, None); ta = (a, aa, ab, ac, ad, b); s' = (stk', loc', pc', xcp); ((a, aa, ab, ac, ad, b), xcp, h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> ci_app ci ((ins @ ins') ! pc) P h stk loc undefined undefined pc []
 4. \<And>xcp pc pc' d stk loc. \<lbrakk>s = (stk, loc, pc, \<lfloor>xcp\<rfloor>); ta = \<lbrace>\<rbrace>; h' = h; s' = (Addr xcp # drop (length stk - d) stk, loc, pc', None); match_ex_table P (cname_of h xcp) pc xt = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P (ins @ ins') (xt @ xt') t h (stk, loc, pc, \<lfloor>xcp\<rfloor>) \<lbrace>\<rbrace> h (Addr xcp # drop (length stk - d) stk, loc, pc', None)
[PROOF STEP]
apply(clarsimp simp add: nth_append)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a aa ab ac ad b xcp stk' loc' pc' pc stk loc. \<lbrakk>s = (stk, loc, pc, None); ta = (a, aa, ab, ac, ad, b); s' = (stk', loc', pc', xcp); ((a, aa, ab, ac, ad, b), xcp, h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> pc < length (ins @ ins')
 2. \<And>a aa ab ac ad b xcp stk' loc' pc' pc stk loc. \<lbrakk>s = (stk, loc, pc, None); ta = (a, aa, ab, ac, ad, b); s' = (stk', loc', pc', xcp); ((a, aa, ab, ac, ad, b), xcp, h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> ci_app ci ((ins @ ins') ! pc) P h stk loc undefined undefined pc []
 3. \<And>xcp pc pc' d stk loc. \<lbrakk>s = (stk, loc, pc, \<lfloor>xcp\<rfloor>); ta = \<lbrace>\<rbrace>; h' = h; s' = (Addr xcp # drop (length stk - d) stk, loc, pc', None); match_ex_table P (cname_of h xcp) pc xt = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P (ins @ ins') (xt @ xt') t h (stk, loc, pc, \<lfloor>xcp\<rfloor>) \<lbrace>\<rbrace> h (Addr xcp # drop (length stk - d) stk, loc, pc', None)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab ac ad b xcp stk' loc' pc' pc stk loc. \<lbrakk>s = (stk, loc, pc, None); ta = (a, aa, ab, ac, ad, b); s' = (stk', loc', pc', xcp); ((a, aa, ab, ac, ad, b), xcp, h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pc) P t h stk loc undefined undefined pc []; pc < length ins; ci_app ci (ins ! pc) P h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> ci_app ci ((ins @ ins') ! pc) P h stk loc undefined undefined pc []
 2. \<And>xcp pc pc' d stk loc. \<lbrakk>s = (stk, loc, pc, \<lfloor>xcp\<rfloor>); ta = \<lbrace>\<rbrace>; h' = h; s' = (Addr xcp # drop (length stk - d) stk, loc, pc', None); match_ex_table P (cname_of h xcp) pc xt = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P (ins @ ins') (xt @ xt') t h (stk, loc, pc, \<lfloor>xcp\<rfloor>) \<lbrace>\<rbrace> h (Addr xcp # drop (length stk - d) stk, loc, pc', None)
[PROOF STEP]
apply(simp add: nth_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xcp pc pc' d stk loc. \<lbrakk>s = (stk, loc, pc, \<lfloor>xcp\<rfloor>); ta = \<lbrace>\<rbrace>; h' = h; s' = (Addr xcp # drop (length stk - d) stk, loc, pc', None); match_ex_table P (cname_of h xcp) pc xt = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> exec_meth ci P (ins @ ins') (xt @ xt') t h (stk, loc, pc, \<lfloor>xcp\<rfloor>) \<lbrace>\<rbrace> h (Addr xcp # drop (length stk - d) stk, loc, pc', None)
[PROOF STEP]
apply(rule exec_catch)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xcp pc pc' d stk loc. \<lbrakk>s = (stk, loc, pc, \<lfloor>xcp\<rfloor>); ta = \<lbrace>\<rbrace>; h' = h; s' = (Addr xcp # drop (length stk - d) stk, loc, pc', None); match_ex_table P (cname_of h xcp) pc xt = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> match_ex_table P (cname_of h xcp) pc (xt @ xt') = \<lfloor>(pc', d)\<rfloor>
 2. \<And>xcp pc pc' d stk loc. \<lbrakk>s = (stk, loc, pc, \<lfloor>xcp\<rfloor>); ta = \<lbrace>\<rbrace>; h' = h; s' = (Addr xcp # drop (length stk - d) stk, loc, pc', None); match_ex_table P (cname_of h xcp) pc xt = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> d \<le> length stk
[PROOF STEP]
by(simp)


[STATEMENT]
lemma exec_meth_append [intro]:
  "exec_meth ci P ins xt t h s ta h' s' \<Longrightarrow> exec_meth ci P (ins @ ins') xt t h s ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci P ins xt t h s ta h' s' \<Longrightarrow> exec_meth ci P (ins @ ins') xt t h s ta h' s'
[PROOF STEP]
by(rule exec_meth_append_xt[where xt'="[]", simplified])