[STATEMENT]
lemma EP_wf: "wf_jvm_prog\<^bsub>Phi_EP\<^esub> EP"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_jvm_prog\<^bsub>Phi_EP\<^esub> EP
[PROOF STEP]
unfolding wf_jvm_prog_phi_def wf_prog_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_syscls EP \<and> (\<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c) \<and> distinct_fst EP
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. wf_syscls EP
 2. (\<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c) \<and> distinct_fst EP
[PROOF STEP]
show "wf_syscls EP"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_syscls EP
[PROOF STEP]
by (simp add: EP_def wf_syscls_def SystemClasses_def sys_xcpts_def
                  ObjectC_def NullPointerC_def OutOfMemoryC_def ClassCastC_def)
[PROOF STATE]
proof (state)
this:
wf_syscls EP

goal (1 subgoal):
 1. (\<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c) \<and> distinct_fst EP
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c) \<and> distinct_fst EP
[PROOF STEP]
have distinct_EP: "distinct_fst EP"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_fst EP
[PROOF STEP]
by (auto simp:
      EP_def SystemClasses_def ObjectC_def NullPointerC_def OutOfMemoryC_def ClassCastC_def)
[PROOF STATE]
proof (state)
this:
distinct_fst EP

goal (1 subgoal):
 1. (\<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c) \<and> distinct_fst EP
[PROOF STEP]
have classes_wf:
    "\<forall>c\<in>set EP.
        wf_cdecl
         (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M))
         EP c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. c \<in> set EP \<Longrightarrow> wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c
[PROOF STEP]
fix C
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. c \<in> set EP \<Longrightarrow> wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c
[PROOF STEP]
assume C_in_EP: "C \<in> set EP"
[PROOF STATE]
proof (state)
this:
C \<in> set EP

goal (1 subgoal):
 1. \<And>c. c \<in> set EP \<Longrightarrow> wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c
[PROOF STEP]
show "wf_cdecl
         (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M))
         EP C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C
[PROOF STEP]
proof (cases "C \<in> set SystemClasses")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. C \<in> set SystemClasses \<Longrightarrow> wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C
 2. C \<notin> set SystemClasses \<Longrightarrow> wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
C \<in> set SystemClasses

goal (2 subgoals):
 1. C \<in> set SystemClasses \<Longrightarrow> wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C
 2. C \<notin> set SystemClasses \<Longrightarrow> wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
C \<in> set SystemClasses

goal (1 subgoal):
 1. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C
[PROOF STEP]
by (auto simp: wf_cdecl_def SystemClasses_def ObjectC_def NullPointerC_def
                       OutOfMemoryC_def ClassCastC_def EP_def class_def)
[PROOF STATE]
proof (state)
this:
wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C

goal (1 subgoal):
 1. C \<notin> set SystemClasses \<Longrightarrow> wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C \<notin> set SystemClasses \<Longrightarrow> wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
C \<notin> set SystemClasses

goal (1 subgoal):
 1. C \<notin> set SystemClasses \<Longrightarrow> wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C
[PROOF STEP]
with C_in_EP
[PROOF STATE]
proof (chain)
picking this:
C \<in> set EP
C \<notin> set SystemClasses
[PROOF STEP]
have [simp]: "C = (''C'', the (class EP ''C''))"
[PROOF STATE]
proof (prove)
using this:
C \<in> set EP
C \<notin> set SystemClasses

goal (1 subgoal):
 1. C = (''C'', the (class EP ''C''))
[PROOF STEP]
by (auto simp: EP_def SystemClasses_def class_def)
[PROOF STATE]
proof (state)
this:
C = (''C'', the (class EP ''C''))

goal (1 subgoal):
 1. C \<notin> set SystemClasses \<Longrightarrow> wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C
[PROOF STEP]
apply (auto dest!: i_max_2D
                     simp: wf_cdecl_def class_def EP_def wf_mdecl_def wt_method_def Phi_EP_def
                           wt_start_def check_types_def states_def JVM_SemiType.sl_def
                           stk_esl_def upto_esl_def loc_sl_def SemiType.esl_def
                           SemiType.sup_def Err.sl_def Err.le_def err_def Listn.sl_def
                           Err.esl_def Opt.esl_def Product.esl_def relevant_entries_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<exists>a aa b. map_of SystemClasses Object = \<lfloor>(a, aa, b)\<rfloor>
 2. \<And>D' Ts' T' a aa ab b. (''C'', Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])]) # SystemClasses \<turnstile> Object sees ''M'': Ts'\<rightarrow>T' = (a, aa, ab, b) in D' \<Longrightarrow> Ts' = []
 3. \<And>D' Ts' T' a aa ab b. (''C'', Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])]) # SystemClasses \<turnstile> Object sees ''M'': Ts'\<rightarrow>T' = (a, aa, ab, b) in D' \<Longrightarrow> T' = Void
[PROOF STEP]
apply (fastforce simp: SystemClasses_def ObjectC_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>D' Ts' T' a aa ab b. (''C'', Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])]) # SystemClasses \<turnstile> Object sees ''M'': Ts'\<rightarrow>T' = (a, aa, ab, b) in D' \<Longrightarrow> Ts' = []
 2. \<And>D' Ts' T' a aa ab b. (''C'', Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])]) # SystemClasses \<turnstile> Object sees ''M'': Ts'\<rightarrow>T' = (a, aa, ab, b) in D' \<Longrightarrow> T' = Void
[PROOF STEP]
apply (clarsimp simp: Method_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>D' Ts' T' a aa ab b Mm. \<lbrakk>(''C'', Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])]) # SystemClasses \<turnstile> Object sees_methods Mm; Mm ''M'' = \<lfloor>((Ts', T', a, aa, ab, b), D')\<rfloor>\<rbrakk> \<Longrightarrow> Ts' = []
 2. \<And>D' Ts' T' a aa ab b. (''C'', Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])]) # SystemClasses \<turnstile> Object sees ''M'': Ts'\<rightarrow>T' = (a, aa, ab, b) in D' \<Longrightarrow> T' = Void
[PROOF STEP]
apply (cases rule: Methods.cases,
                (fastforce simp: class_def SystemClasses_def ObjectC_def)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>D' Ts' T' a aa ab b. (''C'', Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])]) # SystemClasses \<turnstile> Object sees ''M'': Ts'\<rightarrow>T' = (a, aa, ab, b) in D' \<Longrightarrow> T' = Void
[PROOF STEP]
apply (clarsimp simp: Method_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>D' Ts' T' a aa ab b Mm. \<lbrakk>(''C'', Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])]) # SystemClasses \<turnstile> Object sees_methods Mm; Mm ''M'' = \<lfloor>((Ts', T', a, aa, ab, b), D')\<rfloor>\<rbrakk> \<Longrightarrow> T' = Void
[PROOF STEP]
by (cases rule: Methods.cases,
            (fastforce simp: class_def SystemClasses_def ObjectC_def)+)
[PROOF STATE]
proof (state)
this:
wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c

goal (1 subgoal):
 1. (\<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c) \<and> distinct_fst EP
[PROOF STEP]
with distinct_EP
[PROOF STATE]
proof (chain)
picking this:
distinct_fst EP
\<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c
[PROOF STEP]
show "(\<forall>c\<in>set EP.
    wf_cdecl
      (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M))
      EP c) \<and>
    distinct_fst EP"
[PROOF STATE]
proof (prove)
using this:
distinct_fst EP
\<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c

goal (1 subgoal):
 1. (\<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c) \<and> distinct_fst EP
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c) \<and> distinct_fst EP

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [simp]: "Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>wf\<^esub> = EP"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>wf\<^esub> = EP
[PROOF STEP]
proof (cases "(EP, Phi_EP) \<in> wf_jvmprog")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (EP, Phi_EP) \<in> wf_jvmprog \<Longrightarrow> Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>wf\<^esub> = EP
 2. (EP, Phi_EP) \<notin> wf_jvmprog \<Longrightarrow> Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>wf\<^esub> = EP
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
(EP, Phi_EP) \<in> wf_jvmprog

goal (2 subgoals):
 1. (EP, Phi_EP) \<in> wf_jvmprog \<Longrightarrow> Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>wf\<^esub> = EP
 2. (EP, Phi_EP) \<notin> wf_jvmprog \<Longrightarrow> Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>wf\<^esub> = EP
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(EP, Phi_EP) \<in> wf_jvmprog

goal (1 subgoal):
 1. Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>wf\<^esub> = EP
[PROOF STEP]
by (simp add: Abs_wf_jvmprog_inverse)
[PROOF STATE]
proof (state)
this:
Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>wf\<^esub> = EP

goal (1 subgoal):
 1. (EP, Phi_EP) \<notin> wf_jvmprog \<Longrightarrow> Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>wf\<^esub> = EP
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (EP, Phi_EP) \<notin> wf_jvmprog \<Longrightarrow> Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>wf\<^esub> = EP
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
(EP, Phi_EP) \<notin> wf_jvmprog

goal (1 subgoal):
 1. (EP, Phi_EP) \<notin> wf_jvmprog \<Longrightarrow> Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>wf\<^esub> = EP
[PROOF STEP]
with EP_wf
[PROOF STATE]
proof (chain)
picking this:
wf_jvm_prog\<^bsub>Phi_EP\<^esub> EP
(EP, Phi_EP) \<notin> wf_jvmprog
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wf_jvm_prog\<^bsub>Phi_EP\<^esub> EP
(EP, Phi_EP) \<notin> wf_jvmprog

goal (1 subgoal):
 1. Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>wf\<^esub> = EP
[PROOF STEP]
by (simp add: wf_jvmprog_def)
[PROOF STATE]
proof (state)
this:
Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>wf\<^esub> = EP

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [simp]: "Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>\<Phi>\<^esub> = Phi_EP"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>\<Phi>\<^esub> = Phi_EP
[PROOF STEP]
proof (cases "(EP, Phi_EP) \<in> wf_jvmprog")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (EP, Phi_EP) \<in> wf_jvmprog \<Longrightarrow> Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>\<Phi>\<^esub> = Phi_EP
 2. (EP, Phi_EP) \<notin> wf_jvmprog \<Longrightarrow> Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>\<Phi>\<^esub> = Phi_EP
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
(EP, Phi_EP) \<in> wf_jvmprog

goal (2 subgoals):
 1. (EP, Phi_EP) \<in> wf_jvmprog \<Longrightarrow> Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>\<Phi>\<^esub> = Phi_EP
 2. (EP, Phi_EP) \<notin> wf_jvmprog \<Longrightarrow> Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>\<Phi>\<^esub> = Phi_EP
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(EP, Phi_EP) \<in> wf_jvmprog

goal (1 subgoal):
 1. Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>\<Phi>\<^esub> = Phi_EP
[PROOF STEP]
by (simp add: Abs_wf_jvmprog_inverse)
[PROOF STATE]
proof (state)
this:
Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>\<Phi>\<^esub> = Phi_EP

goal (1 subgoal):
 1. (EP, Phi_EP) \<notin> wf_jvmprog \<Longrightarrow> Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>\<Phi>\<^esub> = Phi_EP
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (EP, Phi_EP) \<notin> wf_jvmprog \<Longrightarrow> Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>\<Phi>\<^esub> = Phi_EP
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
(EP, Phi_EP) \<notin> wf_jvmprog

goal (1 subgoal):
 1. (EP, Phi_EP) \<notin> wf_jvmprog \<Longrightarrow> Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>\<Phi>\<^esub> = Phi_EP
[PROOF STEP]
with EP_wf
[PROOF STATE]
proof (chain)
picking this:
wf_jvm_prog\<^bsub>Phi_EP\<^esub> EP
(EP, Phi_EP) \<notin> wf_jvmprog
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wf_jvm_prog\<^bsub>Phi_EP\<^esub> EP
(EP, Phi_EP) \<notin> wf_jvmprog

goal (1 subgoal):
 1. Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>\<Phi>\<^esub> = Phi_EP
[PROOF STEP]
by (simp add: wf_jvmprog_def)
[PROOF STATE]
proof (state)
this:
Abs_wf_jvmprog (EP, Phi_EP)\<^bsub>\<Phi>\<^esub> = Phi_EP

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma method_in_EP_is_M:
  "EP \<turnstile> C sees M: Ts\<rightarrow>T = (mxs, mxl, is, xt) in D
  \<Longrightarrow> C = ''C'' \<and>
     M = ''M'' \<and>
     Ts = [] \<and>
     T = Void \<and>
     mxs = 1 \<and>
     mxl = 0 \<and>
     is = [Push Unit, Return] \<and>
     xt = [] \<and>
     D = ''C''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. EP \<turnstile> C sees M: Ts\<rightarrow>T = (mxs, mxl, is, xt) in D \<Longrightarrow> C = ''C'' \<and> M = ''M'' \<and> Ts = [] \<and> T = Void \<and> mxs = 1 \<and> mxl = 0 \<and> is = [Push Unit, Return] \<and> xt = [] \<and> D = ''C''
[PROOF STEP]
apply (clarsimp simp: Method_def EP_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Mm. \<lbrakk>(''C'', Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])]) # SystemClasses \<turnstile> C sees_methods Mm; Mm M = \<lfloor>((Ts, T, mxs, mxl, is, xt), D)\<rfloor>\<rbrakk> \<Longrightarrow> C = ''C'' \<and> M = ''M'' \<and> Ts = [] \<and> T = Void \<and> mxs = Suc 0 \<and> mxl = 0 \<and> is = [Push Unit, Return] \<and> xt = [] \<and> D = ''C''
[PROOF STEP]
apply (erule Methods.cases, clarsimp simp: class_def SystemClasses_def ObjectC_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Mm Ca Da fs ms Mma Mm'. \<lbrakk>Mm M = \<lfloor>((Ts, T, mxs, mxl, is, xt), D)\<rfloor>; C = Ca; Mm = Mm'; class ((''C'', Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])]) # SystemClasses) Ca = \<lfloor>(Da, fs, ms)\<rfloor>; Ca \<noteq> Object; (''C'', Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])]) # SystemClasses \<turnstile> Da sees_methods Mma; Mm' = Mma ++ (map_option (\<lambda>m. (m, Ca)) \<circ> map_of ms)\<rbrakk> \<Longrightarrow> C = ''C'' \<and> M = ''M'' \<and> Ts = [] \<and> T = Void \<and> mxs = Suc 0 \<and> mxl = 0 \<and> is = [Push Unit, Return] \<and> xt = [] \<and> D = ''C''
[PROOF STEP]
apply (clarsimp simp: class_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Da fs ms Mma. \<lbrakk>(if C = ''C'' then \<lfloor>(Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])])\<rfloor> else map_of SystemClasses C) = \<lfloor>(Da, fs, ms)\<rfloor>; C \<noteq> Object; (''C'', Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])]) # SystemClasses \<turnstile> Da sees_methods Mma; map_of ms M = \<lfloor>(Ts, T, mxs, mxl, is, xt)\<rfloor> \<and> C = D \<or> map_of ms M = None \<and> Mma M = \<lfloor>((Ts, T, mxs, mxl, is, xt), D)\<rfloor>\<rbrakk> \<Longrightarrow> C = ''C'' \<and> M = ''M'' \<and> Ts = [] \<and> T = Void \<and> mxs = Suc 0 \<and> mxl = 0 \<and> is = [Push Unit, Return] \<and> xt = [] \<and> D = ''C''
[PROOF STEP]
apply (erule Methods.cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Da fs ms Mma Daa fsa msa Mm. \<lbrakk>(if C = ''C'' then \<lfloor>(Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])])\<rfloor> else map_of SystemClasses C) = \<lfloor>(Da, fs, ms)\<rfloor>; C \<noteq> Object; map_of ms M = \<lfloor>(Ts, T, mxs, mxl, is, xt)\<rfloor> \<and> C = D \<or> map_of ms M = None \<and> Mma M = \<lfloor>((Ts, T, mxs, mxl, is, xt), D)\<rfloor>; Da = Object; Mma = Mm; class ((''C'', Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])]) # SystemClasses) Object = \<lfloor>(Daa, fsa, msa)\<rfloor>; Mm = map_option (\<lambda>m. (m, Object)) \<circ> map_of msa\<rbrakk> \<Longrightarrow> C = ''C'' \<and> M = ''M'' \<and> Ts = [] \<and> T = Void \<and> mxs = Suc 0 \<and> mxl = 0 \<and> is = [Push Unit, Return] \<and> xt = [] \<and> D = ''C''
 2. \<And>Da fs ms Mma Ca Daa fsa msa Mm Mm'. \<lbrakk>(if C = ''C'' then \<lfloor>(Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])])\<rfloor> else map_of SystemClasses C) = \<lfloor>(Da, fs, ms)\<rfloor>; C \<noteq> Object; map_of ms M = \<lfloor>(Ts, T, mxs, mxl, is, xt)\<rfloor> \<and> C = D \<or> map_of ms M = None \<and> Mma M = \<lfloor>((Ts, T, mxs, mxl, is, xt), D)\<rfloor>; Da = Ca; Mma = Mm'; class ((''C'', Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])]) # SystemClasses) Ca = \<lfloor>(Daa, fsa, msa)\<rfloor>; Ca \<noteq> Object; (''C'', Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])]) # SystemClasses \<turnstile> Daa sees_methods Mm; Mm' = Mm ++ (map_option (\<lambda>m. (m, Ca)) \<circ> map_of msa)\<rbrakk> \<Longrightarrow> C = ''C'' \<and> M = ''M'' \<and> Ts = [] \<and> T = Void \<and> mxs = Suc 0 \<and> mxl = 0 \<and> is = [Push Unit, Return] \<and> xt = [] \<and> D = ''C''
[PROOF STEP]
by (fastforce simp: class_def SystemClasses_def ObjectC_def NullPointerC_def
                       OutOfMemoryC_def ClassCastC_def if_split_eq1)+


[STATEMENT]
lemma [simp]:
  "\<exists>T Ts mxs mxl is. (\<exists>xt. EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = (mxs, mxl, is, xt) in ''C'') \<and> is \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>T Ts mxs mxl is. (\<exists>xt. EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = (mxs, mxl, is, xt) in ''C'') \<and> is \<noteq> []
[PROOF STEP]
using EP_wf
[PROOF STATE]
proof (prove)
using this:
wf_jvm_prog\<^bsub>Phi_EP\<^esub> EP

goal (1 subgoal):
 1. \<exists>T Ts mxs mxl is. (\<exists>xt. EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = (mxs, mxl, is, xt) in ''C'') \<and> is \<noteq> []
[PROOF STEP]
by (fastforce dest: mdecl_visible simp: wf_jvm_prog_phi_def EP_def)


[STATEMENT]
lemma [simp]:
  "\<exists>T Ts mxs mxl is. (\<exists>xt. EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = (mxs, mxl, is, xt) in ''C'') \<and>
  Suc 0 < length is"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>T Ts mxs mxl is. (\<exists>xt. EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = (mxs, mxl, is, xt) in ''C'') \<and> Suc 0 < length is
[PROOF STEP]
using EP_wf
[PROOF STATE]
proof (prove)
using this:
wf_jvm_prog\<^bsub>Phi_EP\<^esub> EP

goal (1 subgoal):
 1. \<exists>T Ts mxs mxl is. (\<exists>xt. EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = (mxs, mxl, is, xt) in ''C'') \<and> Suc 0 < length is
[PROOF STEP]
by (fastforce dest: mdecl_visible simp: wf_jvm_prog_phi_def EP_def)


[STATEMENT]
lemma C_sees_M_in_EP [simp]:
  "EP \<turnstile> ''C'' sees ''M'': []\<rightarrow>Void = (1, 0, [Push Unit, Return], []) in ''C''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. EP \<turnstile> ''C'' sees ''M'': []\<rightarrow>Void = (1, 0, [Push Unit, Return], []) in ''C''
[PROOF STEP]
apply (auto simp: Method_def EP_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Mm. (''C'', Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])]) # SystemClasses \<turnstile> ''C'' sees_methods Mm \<and> Mm ''M'' = \<lfloor>(([], Void, Suc 0, 0, [Push Unit, Return], []), ''C'')\<rfloor>
[PROOF STEP]
apply (rule_tac x="Map.empty(''M'' \<mapsto> (([], Void, 1, 0, [Push Unit, Return], []),''C''))" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (''C'', Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])]) # SystemClasses \<turnstile> ''C'' sees_methods [''M'' \<mapsto> (([], Void, 1, 0, [Push Unit, Return], []), ''C'')] \<and> [''M'' \<mapsto> (([], Void, 1, 0, [Push Unit, Return], []), ''C'')] ''M'' = \<lfloor>(([], Void, Suc 0, 0, [Push Unit, Return], []), ''C'')\<rfloor>
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (''C'', Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])]) # SystemClasses \<turnstile> ''C'' sees_methods [''M'' \<mapsto> (([], Void, Suc 0, 0, [Push Unit, Return], []), ''C'')]
[PROOF STEP]
apply (rule Methods.intros(2))
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. class ((''C'', Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])]) # SystemClasses) ''C'' = \<lfloor>(?D3, ?fs3, ?ms3)\<rfloor>
 2. ''C'' \<noteq> Object
 3. (''C'', Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])]) # SystemClasses \<turnstile> ?D3 sees_methods ?Mm3
 4. [''M'' \<mapsto> (([], Void, Suc 0, 0, [Push Unit, Return], []), ''C'')] = ?Mm3 ++ (map_option (\<lambda>m. (m, ''C'')) \<circ> map_of ?ms3)
[PROOF STEP]
apply (fastforce simp: class_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ''C'' \<noteq> Object
 2. (''C'', Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])]) # SystemClasses \<turnstile> Object sees_methods ?Mm3
 3. [''M'' \<mapsto> (([], Void, Suc 0, 0, [Push Unit, Return], []), ''C'')] = ?Mm3 ++ (map_option (\<lambda>m. (m, ''C'')) \<circ> map_of [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])])
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (''C'', Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])]) # SystemClasses \<turnstile> Object sees_methods ?Mm3
 2. [''M'' \<mapsto> (([], Void, Suc 0, 0, [Push Unit, Return], []), ''C'')] = ?Mm3 ++ (map_option (\<lambda>m. (m, ''C'')) \<circ> map_of [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])])
[PROOF STEP]
apply (rule Methods.intros(1))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. class ((''C'', Object, [], [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])]) # SystemClasses) Object = \<lfloor>(?D15, ?fs15, ?ms15)\<rfloor>
 2. ?Mm3 = map_option (\<lambda>m. (m, Object)) \<circ> map_of ?ms15
 3. [''M'' \<mapsto> (([], Void, Suc 0, 0, [Push Unit, Return], []), ''C'')] = ?Mm3 ++ (map_option (\<lambda>m. (m, ''C'')) \<circ> map_of [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])])
[PROOF STEP]
apply (fastforce simp: class_def SystemClasses_def ObjectC_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ?Mm3 = map_option (\<lambda>m. (m, Object)) \<circ> map_of []
 2. [''M'' \<mapsto> (([], Void, Suc 0, 0, [Push Unit, Return], []), ''C'')] = ?Mm3 ++ (map_option (\<lambda>m. (m, ''C'')) \<circ> map_of [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])])
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [''M'' \<mapsto> (([], Void, Suc 0, 0, [Push Unit, Return], []), ''C'')] = Map.empty ++ (map_option (\<lambda>m. (m, ''C'')) \<circ> map_of [(''M'', [], Void, Suc 0, 0, [Push Unit, Return], [])])
[PROOF STEP]
by fastforce


[STATEMENT]
lemma instrs_of_EP_C_M [simp]:
  "instrs_of EP ''C'' ''M'' = [Push Unit, Return]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. instrs_of EP ''C'' ''M'' = [Push Unit, Return]
[PROOF STEP]
using C_sees_M_in_EP
[PROOF STATE]
proof (prove)
using this:
EP \<turnstile> ''C'' sees ''M'': []\<rightarrow>Void = (1, 0, [Push Unit, Return], []) in ''C''

goal (1 subgoal):
 1. instrs_of EP ''C'' ''M'' = [Push Unit, Return]
[PROOF STEP]
apply (simp add: method_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. EP \<turnstile> ''C'' sees ''M'': []\<rightarrow>Void = (Suc 0, 0, [Push Unit, Return], []) in ''C'' \<Longrightarrow> fst (snd (snd (snd (snd (snd (THE (D, Ts, T, m). EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = m in D)))))) = [Push Unit, Return]
[PROOF STEP]
apply (rule theI2)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. EP \<turnstile> ''C'' sees ''M'': []\<rightarrow>Void = (Suc 0, 0, [Push Unit, Return], []) in ''C'' \<Longrightarrow> case ?a1 of (D, Ts, T, m) \<Rightarrow> EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = m in D
 2. \<And>x. \<lbrakk>EP \<turnstile> ''C'' sees ''M'': []\<rightarrow>Void = (Suc 0, 0, [Push Unit, Return], []) in ''C''; case x of (D, Ts, T, m) \<Rightarrow> EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = m in D\<rbrakk> \<Longrightarrow> x = ?a1
 3. \<And>x. \<lbrakk>EP \<turnstile> ''C'' sees ''M'': []\<rightarrow>Void = (Suc 0, 0, [Push Unit, Return], []) in ''C''; case x of (D, Ts, T, m) \<Rightarrow> EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = m in D\<rbrakk> \<Longrightarrow> fst (snd (snd (snd (snd (snd x))))) = [Push Unit, Return]
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>EP \<turnstile> ''C'' sees ''M'': []\<rightarrow>Void = (Suc 0, 0, [Push Unit, Return], []) in ''C''; case x of (D, Ts, T, m) \<Rightarrow> EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = m in D\<rbrakk> \<Longrightarrow> x = (''C'', [], Void, Suc 0, 0, [Push Unit, Return], [])
 2. \<And>x. \<lbrakk>EP \<turnstile> ''C'' sees ''M'': []\<rightarrow>Void = (Suc 0, 0, [Push Unit, Return], []) in ''C''; case x of (D, Ts, T, m) \<Rightarrow> EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = m in D\<rbrakk> \<Longrightarrow> fst (snd (snd (snd (snd (snd x))))) = [Push Unit, Return]
[PROOF STEP]
apply (clarsimp dest!: method_in_EP_is_M)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>EP \<turnstile> ''C'' sees ''M'': []\<rightarrow>Void = (Suc 0, 0, [Push Unit, Return], []) in ''C''; case x of (D, Ts, T, m) \<Rightarrow> EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = m in D\<rbrakk> \<Longrightarrow> fst (snd (snd (snd (snd (snd x))))) = [Push Unit, Return]
[PROOF STEP]
by (clarsimp dest!: method_in_EP_is_M)


[STATEMENT]
lemma valid_node_in_EP_D:
  "valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') n
  \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') n \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') n \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
assume vn: "valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') n"
[PROOF STATE]
proof (state)
this:
valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') n

goal (1 subgoal):
 1. valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') n \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
proof (cases n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = (_Entry_) \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
 2. \<And>x21 x22. n = (_ x21,x22 _) \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
case Entry
[PROOF STATE]
proof (state)
this:
n = (_Entry_)

goal (2 subgoals):
 1. n = (_Entry_) \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
 2. \<And>x21 x22. n = (_ x21,x22 _) \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
n = (_Entry_)

goal (1 subgoal):
 1. n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}

goal (1 subgoal):
 1. \<And>x21 x22. n = (_ x21,x22 _) \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. n = (_ x21,x22 _) \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
case [simp]: (Node cs opt)
[PROOF STATE]
proof (state)
this:
n = (_ cs,opt _)

goal (1 subgoal):
 1. \<And>x21 x22. n = (_ x21,x22 _) \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
proof (cases opt)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. opt = None \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
 2. \<And>a. opt = \<lfloor>a\<rfloor> \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
case [simp]: None
[PROOF STATE]
proof (state)
this:
opt = None

goal (2 subgoals):
 1. opt = None \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
 2. \<And>a. opt = \<lfloor>a\<rfloor> \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
from vn
[PROOF STATE]
proof (chain)
picking this:
valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') n

goal (1 subgoal):
 1. n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
apply (cases cs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') n; cs = []\<rbrakk> \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
 2. \<And>a list. \<lbrakk>valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') n; cs = a # list\<rbrakk> \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') n; cs = a # list\<rbrakk> \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
apply (case_tac list)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') n; cs = a # list; list = []\<rbrakk> \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
 2. \<And>a list aa lista. \<lbrakk>valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') n; cs = a # list; list = aa # lista\<rbrakk> \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b a T ba Ts mxs mxl is xt. \<lbrakk>cs = [(''C'', ''M'', b)]; b \<noteq> Suc 0; Phi_EP ''C'' ''M'' ! b = \<lfloor>(a, ba)\<rfloor>; b < length is; EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = (mxs, mxl, is, xt) in ''C''\<rbrakk> \<Longrightarrow> b = 0
 2. \<And>a list aa lista. \<lbrakk>valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') n; cs = a # list; list = aa # lista\<rbrakk> \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
apply (drule method_in_EP_is_M)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b a T ba Ts mxs mxl is xt. \<lbrakk>cs = [(''C'', ''M'', b)]; b \<noteq> Suc 0; Phi_EP ''C'' ''M'' ! b = \<lfloor>(a, ba)\<rfloor>; b < length is; ''C'' = ''C'' \<and> ''M'' = ''M'' \<and> Ts = [] \<and> T = Void \<and> mxs = 1 \<and> mxl = 0 \<and> is = [Push Unit, Return] \<and> xt = [] \<and> ''C'' = ''C''\<rbrakk> \<Longrightarrow> b = 0
 2. \<And>a list aa lista. \<lbrakk>valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') n; cs = a # list; list = aa # lista\<rbrakk> \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list aa lista. \<lbrakk>valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') n; cs = a # list; list = aa # lista\<rbrakk> \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba lista ad bb T Ts mxs mxl is xt. \<lbrakk>cs = (a, aa, b) # (ab, ac, ba) # lista; instrs_of EP ab ac ! ba = Invoke aa (length (snd (the (Phi_EP a aa ! 0))) - Suc mxl); Phi_EP a aa ! b = \<lfloor>(ad, bb)\<rfloor>; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((ab, ac, ba) # lista); b < length is; EP \<turnstile> a sees aa: Ts\<rightarrow>T = (mxs, mxl, is, xt) in a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule method_in_EP_is_M)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba lista ad bb T Ts mxs mxl is xt. \<lbrakk>cs = (a, aa, b) # (ab, ac, ba) # lista; instrs_of EP ab ac ! ba = Invoke aa (length (snd (the (Phi_EP a aa ! 0))) - Suc mxl); Phi_EP a aa ! b = \<lfloor>(ad, bb)\<rfloor>; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((ab, ac, ba) # lista); b < length is; a = ''C'' \<and> aa = ''M'' \<and> Ts = [] \<and> T = Void \<and> mxs = 1 \<and> mxl = 0 \<and> is = [Push Unit, Return] \<and> xt = [] \<and> a = ''C''\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b ab ac ba lista ad bb. \<lbrakk>cs = (''C'', ''M'', b) # (ab, ac, ba) # lista; instrs_of EP ab ac ! ba = Invoke ''M'' (length (snd (the (Phi_EP ''C'' ''M'' ! 0))) - Suc 0); Phi_EP ''C'' ''M'' ! b = \<lfloor>(ad, bb)\<rfloor>; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((ab, ac, ba) # lista); b < Suc (Suc 0)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (case_tac lista)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b ab ac ba lista ad bb. \<lbrakk>cs = (''C'', ''M'', b) # (ab, ac, ba) # lista; instrs_of EP ab ac ! ba = Invoke ''M'' (length (snd (the (Phi_EP ''C'' ''M'' ! 0))) - Suc 0); Phi_EP ''C'' ''M'' ! b = \<lfloor>(ad, bb)\<rfloor>; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((ab, ac, ba) # lista); b < Suc (Suc 0); lista = []\<rbrakk> \<Longrightarrow> False
 2. \<And>b ab ac ba lista ad bb a list. \<lbrakk>cs = (''C'', ''M'', b) # (ab, ac, ba) # lista; instrs_of EP ab ac ! ba = Invoke ''M'' (length (snd (the (Phi_EP ''C'' ''M'' ! 0))) - Suc 0); Phi_EP ''C'' ''M'' ! b = \<lfloor>(ad, bb)\<rfloor>; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((ab, ac, ba) # lista); b < Suc (Suc 0); lista = a # list\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b ba ad bb a T bc Ts mxs mxl is xt. \<lbrakk>cs = [(''C'', ''M'', b), (''C'', ''M'', ba)]; [Push Unit, Return] ! ba = Invoke ''M'' (length (snd (the (Phi_EP ''C'' ''M'' ! 0))) - Suc 0); Phi_EP ''C'' ''M'' ! b = \<lfloor>(ad, bb)\<rfloor>; b < Suc (Suc 0); Phi_EP ''C'' ''M'' ! ba = \<lfloor>(a, bc)\<rfloor>; ba < length is; EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = (mxs, mxl, is, xt) in ''C''\<rbrakk> \<Longrightarrow> False
 2. \<And>b ab ac ba lista ad bb a list. \<lbrakk>cs = (''C'', ''M'', b) # (ab, ac, ba) # lista; instrs_of EP ab ac ! ba = Invoke ''M'' (length (snd (the (Phi_EP ''C'' ''M'' ! 0))) - Suc 0); Phi_EP ''C'' ''M'' ! b = \<lfloor>(ad, bb)\<rfloor>; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((ab, ac, ba) # lista); b < Suc (Suc 0); lista = a # list\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule method_in_EP_is_M)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b ba ad bb a T bc Ts mxs mxl is xt. \<lbrakk>cs = [(''C'', ''M'', b), (''C'', ''M'', ba)]; [Push Unit, Return] ! ba = Invoke ''M'' (length (snd (the (Phi_EP ''C'' ''M'' ! 0))) - Suc 0); Phi_EP ''C'' ''M'' ! b = \<lfloor>(ad, bb)\<rfloor>; b < Suc (Suc 0); Phi_EP ''C'' ''M'' ! ba = \<lfloor>(a, bc)\<rfloor>; ba < length is; ''C'' = ''C'' \<and> ''M'' = ''M'' \<and> Ts = [] \<and> T = Void \<and> mxs = 1 \<and> mxl = 0 \<and> is = [Push Unit, Return] \<and> xt = [] \<and> ''C'' = ''C''\<rbrakk> \<Longrightarrow> False
 2. \<And>b ab ac ba lista ad bb a list. \<lbrakk>cs = (''C'', ''M'', b) # (ab, ac, ba) # lista; instrs_of EP ab ac ! ba = Invoke ''M'' (length (snd (the (Phi_EP ''C'' ''M'' ! 0))) - Suc 0); Phi_EP ''C'' ''M'' ! b = \<lfloor>(ad, bb)\<rfloor>; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((ab, ac, ba) # lista); b < Suc (Suc 0); lista = a # list\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b ba ad bb a bc. \<lbrakk>cs = [(''C'', ''M'', b), (''C'', ''M'', ba)]; [Push Unit, Return] ! ba = Invoke ''M'' (length (snd (the (Phi_EP ''C'' ''M'' ! 0))) - Suc 0); Phi_EP ''C'' ''M'' ! b = \<lfloor>(ad, bb)\<rfloor>; b < Suc (Suc 0); Phi_EP ''C'' ''M'' ! ba = \<lfloor>(a, bc)\<rfloor>; ba < Suc (Suc 0)\<rbrakk> \<Longrightarrow> False
 2. \<And>b ab ac ba lista ad bb a list. \<lbrakk>cs = (''C'', ''M'', b) # (ab, ac, ba) # lista; instrs_of EP ab ac ! ba = Invoke ''M'' (length (snd (the (Phi_EP ''C'' ''M'' ! 0))) - Suc 0); Phi_EP ''C'' ''M'' ! b = \<lfloor>(ad, bb)\<rfloor>; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((ab, ac, ba) # lista); b < Suc (Suc 0); lista = a # list\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (case_tac ba, clarsimp, clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b ab ac ba lista ad bb a list. \<lbrakk>cs = (''C'', ''M'', b) # (ab, ac, ba) # lista; instrs_of EP ab ac ! ba = Invoke ''M'' (length (snd (the (Phi_EP ''C'' ''M'' ! 0))) - Suc 0); Phi_EP ''C'' ''M'' ! b = \<lfloor>(ad, bb)\<rfloor>; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((ab, ac, ba) # lista); b < Suc (Suc 0); lista = a # list\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b ab ac ba ad bb a aa bc list ae bd T Ts mxs mxl is xt. \<lbrakk>cs = (''C'', ''M'', b) # (ab, ac, ba) # (a, aa, bc) # list; is ! ba = Invoke ''M'' (length (snd (the (Phi_EP ''C'' ''M'' ! 0))) - Suc 0); Phi_EP ''C'' ''M'' ! b = \<lfloor>(ad, bb)\<rfloor>; b < Suc (Suc 0); instrs_of EP a aa ! bc = Invoke ac (length (snd (the (Phi_EP ab ac ! 0))) - Suc mxl); Phi_EP ab ac ! ba = \<lfloor>(ae, bd)\<rfloor>; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((a, aa, bc) # list); ba < length is; EP \<turnstile> ab sees ac: Ts\<rightarrow>T = (mxs, mxl, is, xt) in ab\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule method_in_EP_is_M)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b ab ac ba ad bb a aa bc list ae bd T Ts mxs mxl is xt. \<lbrakk>cs = (''C'', ''M'', b) # (ab, ac, ba) # (a, aa, bc) # list; is ! ba = Invoke ''M'' (length (snd (the (Phi_EP ''C'' ''M'' ! 0))) - Suc 0); Phi_EP ''C'' ''M'' ! b = \<lfloor>(ad, bb)\<rfloor>; b < Suc (Suc 0); instrs_of EP a aa ! bc = Invoke ac (length (snd (the (Phi_EP ab ac ! 0))) - Suc mxl); Phi_EP ab ac ! ba = \<lfloor>(ae, bd)\<rfloor>; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((a, aa, bc) # list); ba < length is; ab = ''C'' \<and> ac = ''M'' \<and> Ts = [] \<and> T = Void \<and> mxs = 1 \<and> mxl = 0 \<and> is = [Push Unit, Return] \<and> xt = [] \<and> ab = ''C''\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b ba ad bb a aa bc list ae bd. \<lbrakk>cs = (''C'', ''M'', b) # (''C'', ''M'', ba) # (a, aa, bc) # list; [Push Unit, Return] ! ba = Invoke ''M'' (length (snd (the (Phi_EP ''C'' ''M'' ! 0))) - Suc 0); Phi_EP ''C'' ''M'' ! b = \<lfloor>(ad, bb)\<rfloor>; b < Suc (Suc 0); instrs_of EP a aa ! bc = Invoke ''M'' (length (snd (the (Phi_EP ''C'' ''M'' ! 0))) - Suc 0); Phi_EP ''C'' ''M'' ! ba = \<lfloor>(ae, bd)\<rfloor>; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((a, aa, bc) # list); ba < Suc (Suc 0)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (case_tac ba, clarsimp, clarsimp)
[PROOF STATE]
proof (state)
this:
n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}

goal (1 subgoal):
 1. \<And>a. opt = \<lfloor>a\<rfloor> \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. opt = \<lfloor>a\<rfloor> \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
case [simp]: (Some f)
[PROOF STATE]
proof (state)
this:
opt = \<lfloor>f\<rfloor>

goal (1 subgoal):
 1. \<And>a. opt = \<lfloor>a\<rfloor> \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
obtain cs'' xf where [simp]: "f = (cs'', xf)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>cs'' xf. f = (cs'', xf) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases f, fastforce)
[PROOF STATE]
proof (state)
this:
f = (cs'', xf)

goal (1 subgoal):
 1. \<And>a. opt = \<lfloor>a\<rfloor> \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
from vn
[PROOF STATE]
proof (chain)
picking this:
valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') n

goal (1 subgoal):
 1. n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
apply (cases cs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') n; cs = []\<rbrakk> \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
 2. \<And>a list. \<lbrakk>valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') n; cs = a # list\<rbrakk> \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Q f. \<lbrakk>cs = []; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') cs''; (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_Exit_) -(Q)\<^sub>\<surd>\<rightarrow> (_ [],\<lfloor>(cs'', xf)\<rfloor> _); (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ [],\<lfloor>(cs'', xf)\<rfloor> _) -\<Up>f\<rightarrow> (_ cs'',None _)\<rbrakk> \<Longrightarrow> False
 2. \<And>a list. \<lbrakk>valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') n; cs = a # list\<rbrakk> \<Longrightarrow> n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}
[PROOF STEP]
apply (erule JVM_CFG.cases, clarsimp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b list Q f. \<lbrakk>cs = (a, aa, b) # list; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((a, aa, b) # list); valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') cs''; (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ (a, aa, b) # list,None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (a, aa, b) # list,\<lfloor>(cs'', xf)\<rfloor> _); (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ (a, aa, b) # list,\<lfloor>(cs'', xf)\<rfloor> _) -\<Up>f\<rightarrow> (_ cs'',None _)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (case_tac list)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa b list Q f. \<lbrakk>cs = (a, aa, b) # list; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((a, aa, b) # list); valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') cs''; (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ (a, aa, b) # list,None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (a, aa, b) # list,\<lfloor>(cs'', xf)\<rfloor> _); (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ (a, aa, b) # list,\<lfloor>(cs'', xf)\<rfloor> _) -\<Up>f\<rightarrow> (_ cs'',None _); list = []\<rbrakk> \<Longrightarrow> False
 2. \<And>a aa b list Q f ab lista. \<lbrakk>cs = (a, aa, b) # list; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((a, aa, b) # list); valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') cs''; (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ (a, aa, b) # list,None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (a, aa, b) # list,\<lfloor>(cs'', xf)\<rfloor> _); (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ (a, aa, b) # list,\<lfloor>(cs'', xf)\<rfloor> _) -\<Up>f\<rightarrow> (_ cs'',None _); list = ab # lista\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b Q f a T ba Ts mxs mxl is xt. \<lbrakk>cs = [(''C'', ''M'', b)]; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') cs''; (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ [(''C'', ''M'', b)],None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ [(''C'', ''M'', b)],\<lfloor>(cs'', xf)\<rfloor> _); (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ [(''C'', ''M'', b)],\<lfloor>(cs'', xf)\<rfloor> _) -\<Up>f\<rightarrow> (_ cs'',None _); Phi_EP ''C'' ''M'' ! b = \<lfloor>(a, ba)\<rfloor>; b < length is; EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = (mxs, mxl, is, xt) in ''C''\<rbrakk> \<Longrightarrow> False
 2. \<And>a aa b list Q f ab lista. \<lbrakk>cs = (a, aa, b) # list; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((a, aa, b) # list); valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') cs''; (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ (a, aa, b) # list,None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (a, aa, b) # list,\<lfloor>(cs'', xf)\<rfloor> _); (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ (a, aa, b) # list,\<lfloor>(cs'', xf)\<rfloor> _) -\<Up>f\<rightarrow> (_ cs'',None _); list = ab # lista\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule method_in_EP_is_M)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b Q f a T ba Ts mxs mxl is xt. \<lbrakk>cs = [(''C'', ''M'', b)]; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') cs''; (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ [(''C'', ''M'', b)],None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ [(''C'', ''M'', b)],\<lfloor>(cs'', xf)\<rfloor> _); (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ [(''C'', ''M'', b)],\<lfloor>(cs'', xf)\<rfloor> _) -\<Up>f\<rightarrow> (_ cs'',None _); Phi_EP ''C'' ''M'' ! b = \<lfloor>(a, ba)\<rfloor>; b < length is; EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = (mxs, mxl, is, xt) in ''C''; ''C'' = ''C'' \<and> ''M'' = ''M'' \<and> Ts = [] \<and> T = Void \<and> mxs = 1 \<and> mxl = 0 \<and> is = [Push Unit, Return] \<and> xt = [] \<and> ''C'' = ''C''\<rbrakk> \<Longrightarrow> False
 2. \<And>a aa b list Q f ab lista. \<lbrakk>cs = (a, aa, b) # list; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((a, aa, b) # list); valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') cs''; (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ (a, aa, b) # list,None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (a, aa, b) # list,\<lfloor>(cs'', xf)\<rfloor> _); (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ (a, aa, b) # list,\<lfloor>(cs'', xf)\<rfloor> _) -\<Up>f\<rightarrow> (_ cs'',None _); list = ab # lista\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (case_tac b)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>b Q f a T ba Ts mxs mxl is xt. \<lbrakk>cs = [(''C'', ''M'', b)]; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') cs''; (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ [(''C'', ''M'', b)],None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ [(''C'', ''M'', b)],\<lfloor>(cs'', xf)\<rfloor> _); (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ [(''C'', ''M'', b)],\<lfloor>(cs'', xf)\<rfloor> _) -\<Up>f\<rightarrow> (_ cs'',None _); Phi_EP ''C'' ''M'' ! b = \<lfloor>(a, ba)\<rfloor>; b < length is; EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = (mxs, mxl, is, xt) in ''C''; ''C'' = ''C'' \<and> ''M'' = ''M'' \<and> Ts = [] \<and> T = Void \<and> mxs = 1 \<and> mxl = 0 \<and> is = [Push Unit, Return] \<and> xt = [] \<and> ''C'' = ''C''; b = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>b Q f a T ba Ts mxs mxl is xt nat. \<lbrakk>cs = [(''C'', ''M'', b)]; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') cs''; (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ [(''C'', ''M'', b)],None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ [(''C'', ''M'', b)],\<lfloor>(cs'', xf)\<rfloor> _); (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ [(''C'', ''M'', b)],\<lfloor>(cs'', xf)\<rfloor> _) -\<Up>f\<rightarrow> (_ cs'',None _); Phi_EP ''C'' ''M'' ! b = \<lfloor>(a, ba)\<rfloor>; b < length is; EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = (mxs, mxl, is, xt) in ''C''; ''C'' = ''C'' \<and> ''M'' = ''M'' \<and> Ts = [] \<and> T = Void \<and> mxs = 1 \<and> mxl = 0 \<and> is = [Push Unit, Return] \<and> xt = [] \<and> ''C'' = ''C''; b = Suc nat\<rbrakk> \<Longrightarrow> False
 3. \<And>a aa b list Q f ab lista. \<lbrakk>cs = (a, aa, b) # list; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((a, aa, b) # list); valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') cs''; (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ (a, aa, b) # list,None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (a, aa, b) # list,\<lfloor>(cs'', xf)\<rfloor> _); (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ (a, aa, b) # list,\<lfloor>(cs'', xf)\<rfloor> _) -\<Up>f\<rightarrow> (_ cs'',None _); list = ab # lista\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule JVM_CFG.cases, clarsimp+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Q f a ba. \<lbrakk>cs = [(''C'', ''M'', Suc 0)]; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') cs''; (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ [(''C'', ''M'', Suc 0)],None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ [(''C'', ''M'', Suc 0)],\<lfloor>(cs'', xf)\<rfloor> _); (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ [(''C'', ''M'', Suc 0)],\<lfloor>(cs'', xf)\<rfloor> _) -\<Up>f\<rightarrow> (_ cs'',None _); Phi_EP ''C'' ''M'' ! Suc 0 = \<lfloor>(a, ba)\<rfloor>; EP \<turnstile> ''C'' sees ''M'': []\<rightarrow>Void = (Suc 0, 0, [Push Unit, Return], []) in ''C''\<rbrakk> \<Longrightarrow> False
 2. \<And>a aa b list Q f ab lista. \<lbrakk>cs = (a, aa, b) # list; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((a, aa, b) # list); valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') cs''; (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ (a, aa, b) # list,None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (a, aa, b) # list,\<lfloor>(cs'', xf)\<rfloor> _); (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ (a, aa, b) # list,\<lfloor>(cs'', xf)\<rfloor> _) -\<Up>f\<rightarrow> (_ cs'',None _); list = ab # lista\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule JVM_CFG.cases, clarsimp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b Q f ab ac ba lista ad bb T Ts mxs mxl is xt. \<lbrakk>cs = (a, aa, b) # (ab, ac, ba) # lista; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') cs''; (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ (a, aa, b) # (ab, ac, ba) # lista,None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (a, aa, b) # (ab, ac, ba) # lista,\<lfloor>(cs'', xf)\<rfloor> _); (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ (a, aa, b) # (ab, ac, ba) # lista,\<lfloor>(cs'', xf)\<rfloor> _) -\<Up>f\<rightarrow> (_ cs'',None _); instrs_of EP ab ac ! ba = Invoke aa (length (snd (the (Phi_EP a aa ! 0))) - Suc mxl); Phi_EP a aa ! b = \<lfloor>(ad, bb)\<rfloor>; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((ab, ac, ba) # lista); b < length is; EP \<turnstile> a sees aa: Ts\<rightarrow>T = (mxs, mxl, is, xt) in a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule method_in_EP_is_M)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b Q f ab ac ba lista ad bb T Ts mxs mxl is xt. \<lbrakk>cs = (a, aa, b) # (ab, ac, ba) # lista; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') cs''; (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ (a, aa, b) # (ab, ac, ba) # lista,None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (a, aa, b) # (ab, ac, ba) # lista,\<lfloor>(cs'', xf)\<rfloor> _); (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ (a, aa, b) # (ab, ac, ba) # lista,\<lfloor>(cs'', xf)\<rfloor> _) -\<Up>f\<rightarrow> (_ cs'',None _); instrs_of EP ab ac ! ba = Invoke aa (length (snd (the (Phi_EP a aa ! 0))) - Suc mxl); Phi_EP a aa ! b = \<lfloor>(ad, bb)\<rfloor>; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((ab, ac, ba) # lista); b < length is; EP \<turnstile> a sees aa: Ts\<rightarrow>T = (mxs, mxl, is, xt) in a; a = ''C'' \<and> aa = ''M'' \<and> Ts = [] \<and> T = Void \<and> mxs = 1 \<and> mxl = 0 \<and> is = [Push Unit, Return] \<and> xt = [] \<and> a = ''C''\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (case_tac b)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa b Q f ab ac ba lista ad bb T Ts mxs mxl is xt. \<lbrakk>cs = (a, aa, b) # (ab, ac, ba) # lista; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') cs''; (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ (a, aa, b) # (ab, ac, ba) # lista,None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (a, aa, b) # (ab, ac, ba) # lista,\<lfloor>(cs'', xf)\<rfloor> _); (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ (a, aa, b) # (ab, ac, ba) # lista,\<lfloor>(cs'', xf)\<rfloor> _) -\<Up>f\<rightarrow> (_ cs'',None _); instrs_of EP ab ac ! ba = Invoke aa (length (snd (the (Phi_EP a aa ! 0))) - Suc mxl); Phi_EP a aa ! b = \<lfloor>(ad, bb)\<rfloor>; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((ab, ac, ba) # lista); b < length is; EP \<turnstile> a sees aa: Ts\<rightarrow>T = (mxs, mxl, is, xt) in a; a = ''C'' \<and> aa = ''M'' \<and> Ts = [] \<and> T = Void \<and> mxs = 1 \<and> mxl = 0 \<and> is = [Push Unit, Return] \<and> xt = [] \<and> a = ''C''; b = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>a aa b Q f ab ac ba lista ad bb T Ts mxs mxl is xt nat. \<lbrakk>cs = (a, aa, b) # (ab, ac, ba) # lista; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') cs''; (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ (a, aa, b) # (ab, ac, ba) # lista,None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (a, aa, b) # (ab, ac, ba) # lista,\<lfloor>(cs'', xf)\<rfloor> _); (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ (a, aa, b) # (ab, ac, ba) # lista,\<lfloor>(cs'', xf)\<rfloor> _) -\<Up>f\<rightarrow> (_ cs'',None _); instrs_of EP ab ac ! ba = Invoke aa (length (snd (the (Phi_EP a aa ! 0))) - Suc mxl); Phi_EP a aa ! b = \<lfloor>(ad, bb)\<rfloor>; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((ab, ac, ba) # lista); b < length is; EP \<turnstile> a sees aa: Ts\<rightarrow>T = (mxs, mxl, is, xt) in a; a = ''C'' \<and> aa = ''M'' \<and> Ts = [] \<and> T = Void \<and> mxs = 1 \<and> mxl = 0 \<and> is = [Push Unit, Return] \<and> xt = [] \<and> a = ''C''; b = Suc nat\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule JVM_CFG.cases, clarsimp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Q f ab ac ba lista ad bb. \<lbrakk>cs = (''C'', ''M'', Suc 0) # (ab, ac, ba) # lista; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') cs''; (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ (''C'', ''M'', Suc 0) # (ab, ac, ba) # lista,None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (''C'', ''M'', Suc 0) # (ab, ac, ba) # lista,\<lfloor>(cs'', xf)\<rfloor> _); (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ (''C'', ''M'', Suc 0) # (ab, ac, ba) # lista,\<lfloor>(cs'', xf)\<rfloor> _) -\<Up>f\<rightarrow> (_ cs'',None _); instrs_of EP ab ac ! ba = Invoke ''M'' (length (snd (the (Phi_EP ''C'' ''M'' ! 0))) - Suc 0); Phi_EP ''C'' ''M'' ! Suc 0 = \<lfloor>(ad, bb)\<rfloor>; valid_callstack (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((ab, ac, ba) # lista); EP \<turnstile> ''C'' sees ''M'': []\<rightarrow>Void = (Suc 0, 0, [Push Unit, Return], []) in ''C''\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (erule JVM_CFG.cases, clarsimp+)
[PROOF STATE]
proof (state)
this:
n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n \<in> {(_Entry_), (_ [(''C'', ''M'', 0)],None _), (_ [(''C'', ''M'', 1)],None _), (_Exit_)}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma EP_C_M_0_valid [simp]:
  "JVM_CFG_Interpret.valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'')
    (_ [(''C'', ''M'', 0)],None _)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. JVM_CFG_Interpret.valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') (_ [(''C'', ''M'', 0)],None _)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. JVM_CFG_Interpret.valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') (_ [(''C'', ''M'', 0)],None _)
[PROOF STEP]
have "valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'')
    ((_Entry_), (\<lambda>s. True)\<^sub>\<surd>, (_ [(''C'', ''M'', 0)],None _))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((_Entry_), (\<lambda>s. True)\<^sub>\<surd>, (_ [(''C'', ''M'', 0)],None _))
[PROOF STEP]
apply (auto simp: Phi_EP_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_Entry_) -(\<lambda>s. True)\<^sub>\<surd>\<rightarrow> (_ [(''C'', ''M'', 0)],None _)
[PROOF STEP]
by rule auto
[PROOF STATE]
proof (state)
this:
valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((_Entry_), (\<lambda>s. True)\<^sub>\<surd>, (_ [(''C'', ''M'', 0)],None _))

goal (1 subgoal):
 1. JVM_CFG_Interpret.valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') (_ [(''C'', ''M'', 0)],None _)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((_Entry_), (\<lambda>s. True)\<^sub>\<surd>, (_ [(''C'', ''M'', 0)],None _))

goal (1 subgoal):
 1. JVM_CFG_Interpret.valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') (_ [(''C'', ''M'', 0)],None _)
[PROOF STEP]
by (fastforce simp: JVM_CFG_Interpret.valid_node_def)
[PROOF STATE]
proof (state)
this:
JVM_CFG_Interpret.valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') (_ [(''C'', ''M'', 0)],None _)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma EP_C_M_Suc_0_valid [simp]:
  "JVM_CFG_Interpret.valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'')
    (_ [(''C'', ''M'', Suc 0)],None _)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. JVM_CFG_Interpret.valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') (_ [(''C'', ''M'', Suc 0)],None _)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. JVM_CFG_Interpret.valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') (_ [(''C'', ''M'', Suc 0)],None _)
[PROOF STEP]
have "valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'')
    ((_ [(''C'', ''M'', Suc 0)],None _), \<Up>id, (_Exit_))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((_ [(''C'', ''M'', Suc 0)],None _), \<Up>id, (_Exit_))
[PROOF STEP]
apply (auto simp: Phi_EP_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> (_ [(''C'', ''M'', Suc 0)],None _) -\<Up>id\<rightarrow> (_Exit_)
[PROOF STEP]
by rule auto
[PROOF STATE]
proof (state)
this:
valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((_ [(''C'', ''M'', Suc 0)],None _), \<Up>id, (_Exit_))

goal (1 subgoal):
 1. JVM_CFG_Interpret.valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') (_ [(''C'', ''M'', Suc 0)],None _)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ((_ [(''C'', ''M'', Suc 0)],None _), \<Up>id, (_Exit_))

goal (1 subgoal):
 1. JVM_CFG_Interpret.valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') (_ [(''C'', ''M'', Suc 0)],None _)
[PROOF STEP]
by (fastforce simp: JVM_CFG_Interpret.valid_node_def)
[PROOF STATE]
proof (state)
this:
JVM_CFG_Interpret.valid_node (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') (_ [(''C'', ''M'', Suc 0)],None _)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_handler_for_tl_eq:
  "find_handler_for P Exc cs = (C,M,pcx)#cs' \<Longrightarrow> \<exists>cs'' pc. cs = cs'' @ [(C,M,pc)] @ cs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_handler_for P Exc cs = (C, M, pcx) # cs' \<Longrightarrow> \<exists>cs'' pc. cs = cs'' @ [(C, M, pc)] @ cs'
[PROOF STEP]
by (induct cs, auto)


[STATEMENT]
lemma valid_callstack_tl:
  "valid_callstack prog ((C,M,pc)#cs) \<Longrightarrow> valid_callstack prog cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_callstack prog ((C, M, pc) # cs) \<Longrightarrow> valid_callstack prog cs
[PROOF STEP]
by (cases prog, cases cs, auto)


[STATEMENT]
lemma find_handler_Throw_Invoke_pc_in_range:
  "\<lbrakk>cs = (C',M',pc')#cs'; valid_callstack (P,C0,Main) cs;
  instrs_of (P\<^bsub>wf\<^esub>) C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of (P\<^bsub>wf\<^esub>) C' M' ! pc' = Invoke M'' n'');
  find_handler_for P Exc cs = (C,M,pc)#cs'' \<rbrakk>
  \<Longrightarrow> pc < length (instrs_of (P\<^bsub>wf\<^esub>) C M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cs = (C', M', pc') # cs'; valid_callstack (P, C0, Main) cs; instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n''); find_handler_for P Exc cs = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
proof (induct cs arbitrary: C' M' pc' cs')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C' M' pc' cs'. \<lbrakk>[] = (C', M', pc') # cs'; valid_callstack (P, C0, Main) []; instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n''); find_handler_for P Exc [] = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
 2. \<And>a cs C' M' pc' cs'. \<lbrakk>\<And>C' M' pc' cs'. \<lbrakk>cs = (C', M', pc') # cs'; valid_callstack (P, C0, Main) cs; instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n''); find_handler_for P Exc cs = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M); a # cs = (C', M', pc') # cs'; valid_callstack (P, C0, Main) (a # cs); instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n''); find_handler_for P Exc (a # cs) = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
[] = (C', M', pc') # cs'
valid_callstack (P, C0, Main) []
instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n'')
find_handler_for P Exc [] = (C, M, pc) # cs''

goal (2 subgoals):
 1. \<And>C' M' pc' cs'. \<lbrakk>[] = (C', M', pc') # cs'; valid_callstack (P, C0, Main) []; instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n''); find_handler_for P Exc [] = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
 2. \<And>a cs C' M' pc' cs'. \<lbrakk>\<And>C' M' pc' cs'. \<lbrakk>cs = (C', M', pc') # cs'; valid_callstack (P, C0, Main) cs; instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n''); find_handler_for P Exc cs = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M); a # cs = (C', M', pc') # cs'; valid_callstack (P, C0, Main) (a # cs); instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n''); find_handler_for P Exc (a # cs) = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
[] = (C', M', pc') # cs'
valid_callstack (P, C0, Main) []
instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n'')
find_handler_for P Exc [] = (C, M, pc) # cs''

goal (1 subgoal):
 1. pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pc < length (instrs_of P\<^bsub>wf\<^esub> C M)

goal (1 subgoal):
 1. \<And>a cs C' M' pc' cs'. \<lbrakk>\<And>C' M' pc' cs'. \<lbrakk>cs = (C', M', pc') # cs'; valid_callstack (P, C0, Main) cs; instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n''); find_handler_for P Exc cs = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M); a # cs = (C', M', pc') # cs'; valid_callstack (P, C0, Main) (a # cs); instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n''); find_handler_for P Exc (a # cs) = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a cs C' M' pc' cs'. \<lbrakk>\<And>C' M' pc' cs'. \<lbrakk>cs = (C', M', pc') # cs'; valid_callstack (P, C0, Main) cs; instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n''); find_handler_for P Exc cs = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M); a # cs = (C', M', pc') # cs'; valid_callstack (P, C0, Main) (a # cs); instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n''); find_handler_for P Exc (a # cs) = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
case (Cons a cs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>cs = (?C', ?M', ?pc') # ?cs'; valid_callstack (P, C0, Main) cs; instrs_of P\<^bsub>wf\<^esub> ?C' ?M' ! ?pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> ?C' ?M' ! ?pc' = Invoke M'' n''); find_handler_for P Exc cs = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
a # cs = (C', M', pc') # cs'
valid_callstack (P, C0, Main) (a # cs)
instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n'')
find_handler_for P Exc (a # cs) = (C, M, pc) # cs''

goal (1 subgoal):
 1. \<And>a cs C' M' pc' cs'. \<lbrakk>\<And>C' M' pc' cs'. \<lbrakk>cs = (C', M', pc') # cs'; valid_callstack (P, C0, Main) cs; instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n''); find_handler_for P Exc cs = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M); a # cs = (C', M', pc') # cs'; valid_callstack (P, C0, Main) (a # cs); instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n''); find_handler_for P Exc (a # cs) = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
hence [simp]: "a = (C',M',pc')" and [simp]: "cs = cs'"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>cs = (?C', ?M', ?pc') # ?cs'; valid_callstack (P, C0, Main) cs; instrs_of P\<^bsub>wf\<^esub> ?C' ?M' ! ?pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> ?C' ?M' ! ?pc' = Invoke M'' n''); find_handler_for P Exc cs = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
a # cs = (C', M', pc') # cs'
valid_callstack (P, C0, Main) (a # cs)
instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n'')
find_handler_for P Exc (a # cs) = (C, M, pc) # cs''

goal (1 subgoal):
 1. a = (C', M', pc') &&& cs = cs'
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
a = (C', M', pc')
cs = cs'

goal (1 subgoal):
 1. \<And>a cs C' M' pc' cs'. \<lbrakk>\<And>C' M' pc' cs'. \<lbrakk>cs = (C', M', pc') # cs'; valid_callstack (P, C0, Main) cs; instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n''); find_handler_for P Exc cs = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M); a # cs = (C', M', pc') # cs'; valid_callstack (P, C0, Main) (a # cs); instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n''); find_handler_for P Exc (a # cs) = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
note IH = \<open>\<And>C' M' pc' cs'.
           \<lbrakk>cs = (C', M', pc') # cs'; valid_callstack (P, C0, Main) cs;
            instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or>
            (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n'');
            find_handler_for P Exc cs = (C, M, pc) # cs''\<rbrakk>
           \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>cs = (?C', ?M', ?pc') # ?cs'; valid_callstack (P, C0, Main) cs; instrs_of P\<^bsub>wf\<^esub> ?C' ?M' ! ?pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> ?C' ?M' ! ?pc' = Invoke M'' n''); find_handler_for P Exc cs = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)

goal (1 subgoal):
 1. \<And>a cs C' M' pc' cs'. \<lbrakk>\<And>C' M' pc' cs'. \<lbrakk>cs = (C', M', pc') # cs'; valid_callstack (P, C0, Main) cs; instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n''); find_handler_for P Exc cs = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M); a # cs = (C', M', pc') # cs'; valid_callstack (P, C0, Main) (a # cs); instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n''); find_handler_for P Exc (a # cs) = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
note throw = \<open>instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n'')\<close>
[PROOF STATE]
proof (state)
this:
instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n'')

goal (1 subgoal):
 1. \<And>a cs C' M' pc' cs'. \<lbrakk>\<And>C' M' pc' cs'. \<lbrakk>cs = (C', M', pc') # cs'; valid_callstack (P, C0, Main) cs; instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n''); find_handler_for P Exc cs = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M); a # cs = (C', M', pc') # cs'; valid_callstack (P, C0, Main) (a # cs); instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n''); find_handler_for P Exc (a # cs) = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
note fhf = \<open>find_handler_for P Exc (a # cs) = (C, M, pc) # cs''\<close>
[PROOF STATE]
proof (state)
this:
find_handler_for P Exc (a # cs) = (C, M, pc) # cs''

goal (1 subgoal):
 1. \<And>a cs C' M' pc' cs'. \<lbrakk>\<And>C' M' pc' cs'. \<lbrakk>cs = (C', M', pc') # cs'; valid_callstack (P, C0, Main) cs; instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n''); find_handler_for P Exc cs = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M); a # cs = (C', M', pc') # cs'; valid_callstack (P, C0, Main) (a # cs); instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n''); find_handler_for P Exc (a # cs) = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
note v_cs_a_cs = \<open>valid_callstack (P, C0, Main) (a # cs)\<close>
[PROOF STATE]
proof (state)
this:
valid_callstack (P, C0, Main) (a # cs)

goal (1 subgoal):
 1. \<And>a cs C' M' pc' cs'. \<lbrakk>\<And>C' M' pc' cs'. \<lbrakk>cs = (C', M', pc') # cs'; valid_callstack (P, C0, Main) cs; instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n''); find_handler_for P Exc cs = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M); a # cs = (C', M', pc') # cs'; valid_callstack (P, C0, Main) (a # cs); instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n''); find_handler_for P Exc (a # cs) = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
proof (cases "match_ex_table (P\<^bsub>wf\<^esub>) Exc pc' (ex_table_of (P\<^bsub>wf\<^esub>) C' M')")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = None \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
 2. \<And>a. match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = \<lfloor>a\<rfloor> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = None

goal (2 subgoals):
 1. match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = None \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
 2. \<And>a. match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = \<lfloor>a\<rfloor> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
with fhf
[PROOF STATE]
proof (chain)
picking this:
find_handler_for P Exc (a # cs) = (C, M, pc) # cs''
match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = None
[PROOF STEP]
have fhf_tl: "find_handler_for P Exc cs = (C,M,pc)#cs''"
[PROOF STATE]
proof (prove)
using this:
find_handler_for P Exc (a # cs) = (C, M, pc) # cs''
match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = None

goal (1 subgoal):
 1. find_handler_for P Exc cs = (C, M, pc) # cs''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
find_handler_for P Exc cs = (C, M, pc) # cs''

goal (2 subgoals):
 1. match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = None \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
 2. \<And>a. match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = \<lfloor>a\<rfloor> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
from v_cs_a_cs
[PROOF STATE]
proof (chain)
picking this:
valid_callstack (P, C0, Main) (a # cs)
[PROOF STEP]
have "valid_callstack (P, C0, Main) cs"
[PROOF STATE]
proof (prove)
using this:
valid_callstack (P, C0, Main) (a # cs)

goal (1 subgoal):
 1. valid_callstack (P, C0, Main) cs
[PROOF STEP]
by (auto dest: valid_callstack_tl)
[PROOF STATE]
proof (state)
this:
valid_callstack (P, C0, Main) cs

goal (2 subgoals):
 1. match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = None \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
 2. \<And>a. match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = \<lfloor>a\<rfloor> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
from v_cs_a_cs
[PROOF STATE]
proof (chain)
picking this:
valid_callstack (P, C0, Main) (a # cs)
[PROOF STEP]
have "cs \<noteq> [] \<longrightarrow> (let (C,M,pc) = hd cs in \<exists>n. instrs_of (P\<^bsub>wf\<^esub>) C M ! pc = Invoke M' n)"
[PROOF STATE]
proof (prove)
using this:
valid_callstack (P, C0, Main) (a # cs)

goal (1 subgoal):
 1. cs \<noteq> [] \<longrightarrow> (let (C, M, pc) = hd cs in \<exists>n. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke M' n)
[PROOF STEP]
by (cases cs', auto)
[PROOF STATE]
proof (state)
this:
cs \<noteq> [] \<longrightarrow> (let (C, M, pc) = hd cs in \<exists>n. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke M' n)

goal (2 subgoals):
 1. match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = None \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
 2. \<And>a. match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = \<lfloor>a\<rfloor> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
with IH None fhf_tl \<open>valid_callstack (P, C0, Main) cs\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>cs = (?C', ?M', ?pc') # ?cs'; valid_callstack (P, C0, Main) cs; instrs_of P\<^bsub>wf\<^esub> ?C' ?M' ! ?pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> ?C' ?M' ! ?pc' = Invoke M'' n''); find_handler_for P Exc cs = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = None
find_handler_for P Exc cs = (C, M, pc) # cs''
valid_callstack (P, C0, Main) cs
cs \<noteq> [] \<longrightarrow> (let (C, M, pc) = hd cs in \<exists>n. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke M' n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>cs = (?C', ?M', ?pc') # ?cs'; valid_callstack (P, C0, Main) cs; instrs_of P\<^bsub>wf\<^esub> ?C' ?M' ! ?pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> ?C' ?M' ! ?pc' = Invoke M'' n''); find_handler_for P Exc cs = (C, M, pc) # cs''\<rbrakk> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = None
find_handler_for P Exc cs = (C, M, pc) # cs''
valid_callstack (P, C0, Main) cs
cs \<noteq> [] \<longrightarrow> (let (C, M, pc) = hd cs in \<exists>n. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke M' n)

goal (1 subgoal):
 1. pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
by (cases cs) fastforce+
[PROOF STATE]
proof (state)
this:
pc < length (instrs_of P\<^bsub>wf\<^esub> C M)

goal (1 subgoal):
 1. \<And>a. match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = \<lfloor>a\<rfloor> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = \<lfloor>a\<rfloor> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
case (Some xte)
[PROOF STATE]
proof (state)
this:
match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = \<lfloor>xte\<rfloor>

goal (1 subgoal):
 1. \<And>a. match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = \<lfloor>a\<rfloor> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
with fhf
[PROOF STATE]
proof (chain)
picking this:
find_handler_for P Exc (a # cs) = (C, M, pc) # cs''
match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = \<lfloor>xte\<rfloor>
[PROOF STEP]
have [simp]: "C' = C" and [simp]: "M' = M"
[PROOF STATE]
proof (prove)
using this:
find_handler_for P Exc (a # cs) = (C, M, pc) # cs''
match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = \<lfloor>xte\<rfloor>

goal (1 subgoal):
 1. C' = C &&& M' = M
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
C' = C
M' = M

goal (1 subgoal):
 1. \<And>a. match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = \<lfloor>a\<rfloor> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
from v_cs_a_cs fhf Some
[PROOF STATE]
proof (chain)
picking this:
valid_callstack (P, C0, Main) (a # cs)
find_handler_for P Exc (a # cs) = (C, M, pc) # cs''
match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = \<lfloor>xte\<rfloor>
[PROOF STEP]
obtain Ts T mxs mxl "is" xt where wt_class:
      "(P\<^bsub>wf\<^esub>) \<turnstile> C sees M: Ts\<rightarrow>T = (mxs, mxl, is, xt) in C \<and>
      pc' < length is \<and> (P\<^bsub>\<Phi>\<^esub>) C M ! pc' \<noteq> None"
[PROOF STATE]
proof (prove)
using this:
valid_callstack (P, C0, Main) (a # cs)
find_handler_for P Exc (a # cs) = (C, M, pc) # cs''
match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = \<lfloor>xte\<rfloor>

goal (1 subgoal):
 1. (\<And>Ts T mxs mxl is xt. P\<^bsub>wf\<^esub> \<turnstile> C sees M: Ts\<rightarrow>T = (mxs, mxl, is, xt) in C \<and> pc' < length is \<and> P\<^bsub>\<Phi>\<^esub> C M ! pc' \<noteq> None \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases cs) fastforce+
[PROOF STATE]
proof (state)
this:
P\<^bsub>wf\<^esub> \<turnstile> C sees M: Ts\<rightarrow>T = (mxs, mxl, is, xt) in C \<and> pc' < length is \<and> P\<^bsub>\<Phi>\<^esub> C M ! pc' \<noteq> None

goal (1 subgoal):
 1. \<And>a. match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = \<lfloor>a\<rfloor> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
with wf_jvmprog_is_wf [of P]
[PROOF STATE]
proof (chain)
picking this:
wf_jvm_prog\<^bsub>P\<^bsub>\<Phi>\<^esub>\<^esub> P\<^bsub>wf\<^esub>
P\<^bsub>wf\<^esub> \<turnstile> C sees M: Ts\<rightarrow>T = (mxs, mxl, is, xt) in C \<and> pc' < length is \<and> P\<^bsub>\<Phi>\<^esub> C M ! pc' \<noteq> None
[PROOF STEP]
have wt_instr:"(P\<^bsub>wf\<^esub>),T,mxs,length is,xt \<turnstile> is ! pc',pc' :: (P\<^bsub>\<Phi>\<^esub>) C M"
[PROOF STATE]
proof (prove)
using this:
wf_jvm_prog\<^bsub>P\<^bsub>\<Phi>\<^esub>\<^esub> P\<^bsub>wf\<^esub>
P\<^bsub>wf\<^esub> \<turnstile> C sees M: Ts\<rightarrow>T = (mxs, mxl, is, xt) in C \<and> pc' < length is \<and> P\<^bsub>\<Phi>\<^esub> C M ! pc' \<noteq> None

goal (1 subgoal):
 1. P\<^bsub>wf\<^esub>,T,mxs,length is,xt \<turnstile> is ! pc',pc' :: P\<^bsub>\<Phi>\<^esub> C M
[PROOF STEP]
by (fastforce dest!: wt_jvm_prog_impl_wt_instr)
[PROOF STATE]
proof (state)
this:
P\<^bsub>wf\<^esub>,T,mxs,length is,xt \<turnstile> is ! pc',pc' :: P\<^bsub>\<Phi>\<^esub> C M

goal (1 subgoal):
 1. \<And>a. match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = \<lfloor>a\<rfloor> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
from Some fhf
[PROOF STATE]
proof (chain)
picking this:
match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = \<lfloor>xte\<rfloor>
find_handler_for P Exc (a # cs) = (C, M, pc) # cs''
[PROOF STEP]
obtain f t D d where "(f,t,D,pc,d)\<in> set (ex_table_of (P\<^bsub>wf\<^esub>) C M) \<and>
      matches_ex_entry (P\<^bsub>wf\<^esub>) Exc pc' (f,t,D,pc,d)"
[PROOF STATE]
proof (prove)
using this:
match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = \<lfloor>xte\<rfloor>
find_handler_for P Exc (a # cs) = (C, M, pc) # cs''

goal (1 subgoal):
 1. (\<And>f t D d. (f, t, D, pc, d) \<in> set (ex_table_of P\<^bsub>wf\<^esub> C M) \<and> matches_ex_entry P\<^bsub>wf\<^esub> Exc pc' (f, t, D, pc, d) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases xte, fastforce dest: match_ex_table_SomeD)
[PROOF STATE]
proof (state)
this:
(f, t, D, pc, d) \<in> set (ex_table_of P\<^bsub>wf\<^esub> C M) \<and> matches_ex_entry P\<^bsub>wf\<^esub> Exc pc' (f, t, D, pc, d)

goal (1 subgoal):
 1. \<And>a. match_ex_table P\<^bsub>wf\<^esub> Exc pc' (ex_table_of P\<^bsub>wf\<^esub> C' M') = \<lfloor>a\<rfloor> \<Longrightarrow> pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
with wt_instr throw wt_class
[PROOF STATE]
proof (chain)
picking this:
P\<^bsub>wf\<^esub>,T,mxs,length is,xt \<turnstile> is ! pc',pc' :: P\<^bsub>\<Phi>\<^esub> C M
instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n'')
P\<^bsub>wf\<^esub> \<turnstile> C sees M: Ts\<rightarrow>T = (mxs, mxl, is, xt) in C \<and> pc' < length is \<and> P\<^bsub>\<Phi>\<^esub> C M ! pc' \<noteq> None
(f, t, D, pc, d) \<in> set (ex_table_of P\<^bsub>wf\<^esub> C M) \<and> matches_ex_entry P\<^bsub>wf\<^esub> Exc pc' (f, t, D, pc, d)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P\<^bsub>wf\<^esub>,T,mxs,length is,xt \<turnstile> is ! pc',pc' :: P\<^bsub>\<Phi>\<^esub> C M
instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Throw \<or> (\<exists>M'' n''. instrs_of P\<^bsub>wf\<^esub> C' M' ! pc' = Invoke M'' n'')
P\<^bsub>wf\<^esub> \<turnstile> C sees M: Ts\<rightarrow>T = (mxs, mxl, is, xt) in C \<and> pc' < length is \<and> P\<^bsub>\<Phi>\<^esub> C M ! pc' \<noteq> None
(f, t, D, pc, d) \<in> set (ex_table_of P\<^bsub>wf\<^esub> C M) \<and> matches_ex_entry P\<^bsub>wf\<^esub> Exc pc' (f, t, D, pc, d)

goal (1 subgoal):
 1. pc < length (instrs_of P\<^bsub>wf\<^esub> C M)
[PROOF STEP]
by (fastforce simp: relevant_entries_def is_relevant_entry_def matches_ex_entry_def)
[PROOF STATE]
proof (state)
this:
pc < length (instrs_of P\<^bsub>wf\<^esub> C M)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pc < length (instrs_of P\<^bsub>wf\<^esub> C M)

goal:
No subgoals!
[PROOF STEP]
qed