[STATEMENT]
lemma successor_set_finite:
  "JVM_CFG_Interpret.valid_node prog n
  \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and>
                      targetnode a' = n'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. JVM_CFG_Interpret.valid_node prog n \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. JVM_CFG_Interpret.valid_node prog n \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
assume valid_node: "JVM_CFG_Interpret.valid_node prog n"
[PROOF STATE]
proof (state)
this:
JVM_CFG_Interpret.valid_node prog n

goal (1 subgoal):
 1. JVM_CFG_Interpret.valid_node prog n \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
obtain P C0 Main where [simp]: "prog = (P, C0, Main)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P C0 Main. prog = (P, C0, Main) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases prog, fastforce)
[PROOF STATE]
proof (state)
this:
prog = (P, C0, Main)

goal (1 subgoal):
 1. JVM_CFG_Interpret.valid_node prog n \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
note P_wf = wf_jvmprog_is_wf [of P]
[PROOF STATE]
proof (state)
this:
wf_jvm_prog\<^bsub>P\<^bsub>\<Phi>\<^esub>\<^esub> P\<^bsub>wf\<^esub>

goal (1 subgoal):
 1. JVM_CFG_Interpret.valid_node prog n \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
proof (cases n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = (_Entry_) \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x21 x22. n = (_ x21,x22 _) \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
case Entry
[PROOF STATE]
proof (state)
this:
n = (_Entry_)

goal (2 subgoals):
 1. n = (_Entry_) \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x21 x22. n = (_ x21,x22 _) \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
n = (_Entry_)

goal (1 subgoal):
 1. finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
by (rule_tac B="{(_Exit_), (_ [(C0, Main, 0)],None _)}" in finite_subset,
        auto dest: JVMCFG_EntryD)
[PROOF STATE]
proof (state)
this:
finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}

goal (1 subgoal):
 1. \<And>x21 x22. n = (_ x21,x22 _) \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. n = (_ x21,x22 _) \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
case [simp]: (Node cs x)
[PROOF STATE]
proof (state)
this:
n = (_ cs,x _)

goal (1 subgoal):
 1. \<And>x21 x22. n = (_ x21,x22 _) \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
proof (cases cs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cs = [] \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>a list. cs = a # list \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
cs = []

goal (2 subgoals):
 1. cs = [] \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>a list. cs = a # list \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
cs = []

goal (1 subgoal):
 1. finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
by (rule_tac B="{}" in finite_subset,
          auto elim: JVM_CFG.cases)
[PROOF STATE]
proof (state)
this:
finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}

goal (1 subgoal):
 1. \<And>a list. cs = a # list \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. cs = a # list \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
case [simp]: (Cons a cs')
[PROOF STATE]
proof (state)
this:
cs = a # cs'

goal (1 subgoal):
 1. \<And>a list. cs = a # list \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
obtain C M pc where [simp]: "a = (C,M,pc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C M pc. a = (C, M, pc) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases a, fastforce)
[PROOF STATE]
proof (state)
this:
a = (C, M, pc)

goal (1 subgoal):
 1. \<And>a list. cs = a # list \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
have finite_classes: "finite {C. is_class (P\<^bsub>wf\<^esub>) C}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {C. is_class P\<^bsub>wf\<^esub> C}
[PROOF STEP]
by (rule finite_is_class)
[PROOF STATE]
proof (state)
this:
finite {C. is_class P\<^bsub>wf\<^esub> C}

goal (1 subgoal):
 1. \<And>a list. cs = a # list \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
from valid_node
[PROOF STATE]
proof (chain)
picking this:
JVM_CFG_Interpret.valid_node prog n
[PROOF STEP]
have "is_class (P\<^bsub>wf\<^esub>) C"
[PROOF STATE]
proof (prove)
using this:
JVM_CFG_Interpret.valid_node prog n

goal (1 subgoal):
 1. is_class P\<^bsub>wf\<^esub> C
[PROOF STEP]
apply (auto simp: JVM_CFG_Interpret.valid_node_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b. \<lbrakk>(P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -aa\<rightarrow> b; valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); valid_node (P, C0, Main) b\<rbrakk> \<Longrightarrow> \<exists>a aa b. class P\<^bsub>wf\<^esub> C = \<lfloor>(a, aa, b)\<rfloor>
 2. \<And>a aa. \<lbrakk>(P, C0, Main) \<turnstile> a -aa\<rightarrow> (_ (C, M, pc) # cs',x _); valid_node (P, C0, Main) a; valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _)\<rbrakk> \<Longrightarrow> \<exists>a aa b. class P\<^bsub>wf\<^esub> C = \<lfloor>(a, aa, b)\<rfloor>
[PROOF STEP]
apply (cases x, auto)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b. \<lbrakk>(P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',None _) -aa\<rightarrow> b; valid_callstack (P, C0, Main) ((C, M, pc) # cs'); valid_node (P, C0, Main) b; x = None\<rbrakk> \<Longrightarrow> \<exists>a aa b. class P\<^bsub>wf\<^esub> C = \<lfloor>(a, aa, b)\<rfloor>
 2. \<And>aa b a ba Q f. \<lbrakk>(P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',\<lfloor>(a, ba)\<rfloor> _) -aa\<rightarrow> b; valid_node (P, C0, Main) b; x = \<lfloor>(a, ba)\<rfloor>; valid_callstack (P, C0, Main) ((C, M, pc) # cs'); valid_callstack (P, C0, Main) a; (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (C, M, pc) # cs',\<lfloor>(a, ba)\<rfloor> _); (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',\<lfloor>(a, ba)\<rfloor> _) -\<Up>f\<rightarrow> (_ a,None _)\<rbrakk> \<Longrightarrow> \<exists>a aa b. class P\<^bsub>wf\<^esub> C = \<lfloor>(a, aa, b)\<rfloor>
 3. \<And>a aa. \<lbrakk>(P, C0, Main) \<turnstile> a -aa\<rightarrow> (_ (C, M, pc) # cs',x _); valid_node (P, C0, Main) a; valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _)\<rbrakk> \<Longrightarrow> \<exists>a aa b. class P\<^bsub>wf\<^esub> C = \<lfloor>(a, aa, b)\<rfloor>
[PROOF STEP]
apply (cases cs', auto dest!: sees_method_is_class)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b a ba Q f. \<lbrakk>(P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',\<lfloor>(a, ba)\<rfloor> _) -aa\<rightarrow> b; valid_node (P, C0, Main) b; x = \<lfloor>(a, ba)\<rfloor>; valid_callstack (P, C0, Main) ((C, M, pc) # cs'); valid_callstack (P, C0, Main) a; (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (C, M, pc) # cs',\<lfloor>(a, ba)\<rfloor> _); (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',\<lfloor>(a, ba)\<rfloor> _) -\<Up>f\<rightarrow> (_ a,None _)\<rbrakk> \<Longrightarrow> \<exists>a aa b. class P\<^bsub>wf\<^esub> C = \<lfloor>(a, aa, b)\<rfloor>
 2. \<And>a aa. \<lbrakk>(P, C0, Main) \<turnstile> a -aa\<rightarrow> (_ (C, M, pc) # cs',x _); valid_node (P, C0, Main) a; valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _)\<rbrakk> \<Longrightarrow> \<exists>a aa b. class P\<^bsub>wf\<^esub> C = \<lfloor>(a, aa, b)\<rfloor>
[PROOF STEP]
apply (cases cs', auto dest!: sees_method_is_class)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa. \<lbrakk>(P, C0, Main) \<turnstile> a -aa\<rightarrow> (_ (C, M, pc) # cs',x _); valid_node (P, C0, Main) a; valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _)\<rbrakk> \<Longrightarrow> \<exists>a aa b. class P\<^bsub>wf\<^esub> C = \<lfloor>(a, aa, b)\<rfloor>
[PROOF STEP]
apply (cases cs', auto dest!: sees_method_is_class)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa. \<lbrakk>(P, C0, Main) \<turnstile> a -aa\<rightarrow> (_ [(C, M, pc)],x _); valid_node (P, C0, Main) a; valid_node (P, C0, Main) (_ [(C, M, pc)],x _); cs' = []\<rbrakk> \<Longrightarrow> \<exists>a aa b. class P\<^bsub>wf\<^esub> C = \<lfloor>(a, aa, b)\<rfloor>
 2. \<And>a aa ab ac b list. \<lbrakk>(P, C0, Main) \<turnstile> a -aa\<rightarrow> (_ (C, M, pc) # (ab, ac, b) # list,x _); valid_node (P, C0, Main) a; valid_node (P, C0, Main) (_ (C, M, pc) # (ab, ac, b) # list,x _); cs' = (ab, ac, b) # list\<rbrakk> \<Longrightarrow> \<exists>a aa b. class P\<^bsub>wf\<^esub> C = \<lfloor>(a, aa, b)\<rfloor>
[PROOF STEP]
apply (cases x, auto dest!: sees_method_is_class)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab ac b list. \<lbrakk>(P, C0, Main) \<turnstile> a -aa\<rightarrow> (_ (C, M, pc) # (ab, ac, b) # list,x _); valid_node (P, C0, Main) a; valid_node (P, C0, Main) (_ (C, M, pc) # (ab, ac, b) # list,x _); cs' = (ab, ac, b) # list\<rbrakk> \<Longrightarrow> \<exists>a aa b. class P\<^bsub>wf\<^esub> C = \<lfloor>(a, aa, b)\<rfloor>
[PROOF STEP]
by (cases x, auto dest!: sees_method_is_class)
[PROOF STATE]
proof (state)
this:
is_class P\<^bsub>wf\<^esub> C

goal (1 subgoal):
 1. \<And>a list. cs = a # list \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
proof (cases "instrs_of (P\<^bsub>wf\<^esub>) C M ! pc")
[PROOF STATE]
proof (state)
goal (15 subgoals):
 1. \<And>x1. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Load x1 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x2. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Store x2 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. \<And>x3. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Push x3 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. \<And>x4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = New x4 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. \<And>x51 x52. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Getfield x51 x52 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. \<And>x61 x62. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield x61 x62 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. \<And>x7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast x7 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 8. \<And>x81 x82. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke x81 x82 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 9. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 10. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
A total of 15 subgoals...
[PROOF STEP]
case (Load nat)
[PROOF STATE]
proof (state)
this:
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Load nat

goal (15 subgoals):
 1. \<And>x1. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Load x1 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x2. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Store x2 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. \<And>x3. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Push x3 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. \<And>x4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = New x4 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. \<And>x51 x52. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Getfield x51 x52 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. \<And>x61 x62. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield x61 x62 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. \<And>x7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast x7 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 8. \<And>x81 x82. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke x81 x82 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 9. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 10. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
A total of 15 subgoals...
[PROOF STEP]
with valid_node
[PROOF STATE]
proof (chain)
picking this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Load nat
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Load nat

goal (1 subgoal):
 1. finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Load nat\<rbrakk> \<Longrightarrow> finite {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'}
[PROOF STEP]
apply (rule_tac B="{(_ (C,M,Suc pc)#cs',x _)}" in finite_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Load nat\<rbrakk> \<Longrightarrow> {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'} \<subseteq> {(_ (C, M, Suc pc) # cs',x _)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Load nat\<rbrakk> \<Longrightarrow> finite {(_ (C, M, Suc pc) # cs',x _)}
[PROOF STEP]
by (auto elim: JVM_CFG.cases)
[PROOF STATE]
proof (state)
this:
finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}

goal (14 subgoals):
 1. \<And>x2. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Store x2 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x3. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Push x3 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. \<And>x4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = New x4 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. \<And>x51 x52. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Getfield x51 x52 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. \<And>x61 x62. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield x61 x62 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. \<And>x7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast x7 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. \<And>x81 x82. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke x81 x82 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 8. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 9. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 10. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
A total of 14 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (14 subgoals):
 1. \<And>x2. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Store x2 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x3. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Push x3 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. \<And>x4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = New x4 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. \<And>x51 x52. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Getfield x51 x52 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. \<And>x61 x62. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield x61 x62 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. \<And>x7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast x7 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. \<And>x81 x82. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke x81 x82 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 8. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 9. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 10. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
A total of 14 subgoals...
[PROOF STEP]
case (Store nat)
[PROOF STATE]
proof (state)
this:
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Store nat

goal (14 subgoals):
 1. \<And>x2. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Store x2 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x3. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Push x3 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. \<And>x4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = New x4 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. \<And>x51 x52. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Getfield x51 x52 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. \<And>x61 x62. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield x61 x62 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. \<And>x7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast x7 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. \<And>x81 x82. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke x81 x82 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 8. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 9. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 10. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
A total of 14 subgoals...
[PROOF STEP]
with valid_node
[PROOF STATE]
proof (chain)
picking this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Store nat
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Store nat

goal (1 subgoal):
 1. finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Store nat\<rbrakk> \<Longrightarrow> finite {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'}
[PROOF STEP]
apply (rule_tac B="{(_ (C,M,Suc pc)#cs',x _)}" in finite_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Store nat\<rbrakk> \<Longrightarrow> {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'} \<subseteq> {(_ (C, M, Suc pc) # cs',x _)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Store nat\<rbrakk> \<Longrightarrow> finite {(_ (C, M, Suc pc) # cs',x _)}
[PROOF STEP]
by (auto elim: JVM_CFG.cases)
[PROOF STATE]
proof (state)
this:
finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}

goal (13 subgoals):
 1. \<And>x3. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Push x3 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = New x4 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. \<And>x51 x52. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Getfield x51 x52 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. \<And>x61 x62. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield x61 x62 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. \<And>x7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast x7 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. \<And>x81 x82. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke x81 x82 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 8. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 9. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 10. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
A total of 13 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<And>x3. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Push x3 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = New x4 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. \<And>x51 x52. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Getfield x51 x52 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. \<And>x61 x62. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield x61 x62 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. \<And>x7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast x7 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. \<And>x81 x82. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke x81 x82 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 8. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 9. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 10. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
A total of 13 subgoals...
[PROOF STEP]
case (Push val)
[PROOF STATE]
proof (state)
this:
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Push val

goal (13 subgoals):
 1. \<And>x3. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Push x3 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = New x4 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. \<And>x51 x52. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Getfield x51 x52 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. \<And>x61 x62. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield x61 x62 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. \<And>x7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast x7 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. \<And>x81 x82. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke x81 x82 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 8. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 9. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 10. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
A total of 13 subgoals...
[PROOF STEP]
with valid_node
[PROOF STATE]
proof (chain)
picking this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Push val
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Push val

goal (1 subgoal):
 1. finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Push val\<rbrakk> \<Longrightarrow> finite {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'}
[PROOF STEP]
apply (rule_tac B="{(_ (C,M,Suc pc)#cs',x _)}" in finite_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Push val\<rbrakk> \<Longrightarrow> {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'} \<subseteq> {(_ (C, M, Suc pc) # cs',x _)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Push val\<rbrakk> \<Longrightarrow> finite {(_ (C, M, Suc pc) # cs',x _)}
[PROOF STEP]
by (auto elim: JVM_CFG.cases)
[PROOF STATE]
proof (state)
this:
finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}

goal (12 subgoals):
 1. \<And>x4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = New x4 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x51 x52. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Getfield x51 x52 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. \<And>x61 x62. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield x61 x62 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. \<And>x7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast x7 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. \<And>x81 x82. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke x81 x82 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 8. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 9. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 10. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
A total of 12 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (12 subgoals):
 1. \<And>x4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = New x4 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x51 x52. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Getfield x51 x52 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. \<And>x61 x62. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield x61 x62 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. \<And>x7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast x7 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. \<And>x81 x82. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke x81 x82 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 8. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 9. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 10. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
A total of 12 subgoals...
[PROOF STEP]
case (New C')
[PROOF STATE]
proof (state)
this:
instrs_of P\<^bsub>wf\<^esub> C M ! pc = New C'

goal (12 subgoals):
 1. \<And>x4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = New x4 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x51 x52. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Getfield x51 x52 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. \<And>x61 x62. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield x61 x62 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. \<And>x7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast x7 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. \<And>x81 x82. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke x81 x82 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 8. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 9. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 10. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
A total of 12 subgoals...
[PROOF STEP]
with valid_node
[PROOF STATE]
proof (chain)
picking this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = New C'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = New C'

goal (1 subgoal):
 1. finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = New C'\<rbrakk> \<Longrightarrow> finite {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'}
[PROOF STEP]
apply (rule_tac B="{(_ (C,M,pc)#cs',\<lfloor>((C,M,Suc pc)#cs',False)\<rfloor> _),
            (_ (C,M,pc)#cs',\<lfloor>(find_handler_for P OutOfMemory ((C,M,pc)#cs'),True)\<rfloor> _),
            (_ fst(the(x)),None _)}" in finite_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = New C'\<rbrakk> \<Longrightarrow> {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'} \<subseteq> {(_ (C, M, pc) # cs',\<lfloor>((C, M, Suc pc) # cs', False)\<rfloor> _), (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P OutOfMemory ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = New C'\<rbrakk> \<Longrightarrow> finite {(_ (C, M, pc) # cs',\<lfloor>((C, M, Suc pc) # cs', False)\<rfloor> _), (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P OutOfMemory ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)}
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = New C'; xa \<in> {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'}\<rbrakk> \<Longrightarrow> xa \<in> {(_ (C, M, pc) # cs',\<lfloor>((C, M, Suc pc) # cs', False)\<rfloor> _), (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P OutOfMemory ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = New C'\<rbrakk> \<Longrightarrow> finite {(_ (C, M, pc) # cs',\<lfloor>((C, M, Suc pc) # cs', False)\<rfloor> _), (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P OutOfMemory ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)}
[PROOF STEP]
apply (clarsimp simp del: find_handler_for.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa a. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = New C'; (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> xa; valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); valid_node (P, C0, Main) xa; xa \<noteq> (_ (C, M, pc) # cs',\<lfloor>((C, M, Suc pc) # cs', False)\<rfloor> _); xa \<noteq> (_ fst (the x),None _)\<rbrakk> \<Longrightarrow> xa = (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P OutOfMemory ((C, M, pc) # cs'), True)\<rfloor> _)
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = New C'\<rbrakk> \<Longrightarrow> finite {(_ (C, M, pc) # cs',\<lfloor>((C, M, Suc pc) # cs', False)\<rfloor> _), (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P OutOfMemory ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)}
[PROOF STEP]
by (erule JVM_CFG.cases, simp_all del: find_handler_for.simps)
[PROOF STATE]
proof (state)
this:
finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}

goal (11 subgoals):
 1. \<And>x51 x52. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Getfield x51 x52 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x61 x62. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield x61 x62 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. \<And>x7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast x7 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. \<And>x81 x82. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke x81 x82 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 8. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 9. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 10. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
A total of 11 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<And>x51 x52. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Getfield x51 x52 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x61 x62. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield x61 x62 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. \<And>x7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast x7 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. \<And>x81 x82. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke x81 x82 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 8. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 9. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 10. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
A total of 11 subgoals...
[PROOF STEP]
case (Getfield Fd C')
[PROOF STATE]
proof (state)
this:
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Getfield Fd C'

goal (11 subgoals):
 1. \<And>x51 x52. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Getfield x51 x52 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x61 x62. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield x61 x62 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. \<And>x7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast x7 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. \<And>x81 x82. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke x81 x82 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 8. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 9. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 10. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
A total of 11 subgoals...
[PROOF STEP]
with valid_node
[PROOF STATE]
proof (chain)
picking this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Getfield Fd C'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Getfield Fd C'

goal (1 subgoal):
 1. finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Getfield Fd C'\<rbrakk> \<Longrightarrow> finite {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'}
[PROOF STEP]
apply (rule_tac B="{(_ (C,M,pc)#cs',\<lfloor>((C,M,Suc pc)#cs',False)\<rfloor> _),
            (_ (C,M,pc)#cs',\<lfloor>(find_handler_for P NullPointer ((C,M,pc)#cs'),True)\<rfloor> _),
            (_ fst(the(x)),None _)}" in finite_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Getfield Fd C'\<rbrakk> \<Longrightarrow> {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'} \<subseteq> {(_ (C, M, pc) # cs',\<lfloor>((C, M, Suc pc) # cs', False)\<rfloor> _), (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P NullPointer ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Getfield Fd C'\<rbrakk> \<Longrightarrow> finite {(_ (C, M, pc) # cs',\<lfloor>((C, M, Suc pc) # cs', False)\<rfloor> _), (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P NullPointer ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)}
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Getfield Fd C'; xa \<in> {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'}\<rbrakk> \<Longrightarrow> xa \<in> {(_ (C, M, pc) # cs',\<lfloor>((C, M, Suc pc) # cs', False)\<rfloor> _), (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P NullPointer ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Getfield Fd C'\<rbrakk> \<Longrightarrow> finite {(_ (C, M, pc) # cs',\<lfloor>((C, M, Suc pc) # cs', False)\<rfloor> _), (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P NullPointer ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)}
[PROOF STEP]
apply (clarsimp simp del: find_handler_for.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa a. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Getfield Fd C'; (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> xa; valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); valid_node (P, C0, Main) xa; xa \<noteq> (_ (C, M, pc) # cs',\<lfloor>((C, M, Suc pc) # cs', False)\<rfloor> _); xa \<noteq> (_ fst (the x),None _)\<rbrakk> \<Longrightarrow> xa = (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P NullPointer ((C, M, pc) # cs'), True)\<rfloor> _)
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Getfield Fd C'\<rbrakk> \<Longrightarrow> finite {(_ (C, M, pc) # cs',\<lfloor>((C, M, Suc pc) # cs', False)\<rfloor> _), (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P NullPointer ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)}
[PROOF STEP]
by (erule JVM_CFG.cases, simp_all del: find_handler_for.simps)
[PROOF STATE]
proof (state)
this:
finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}

goal (10 subgoals):
 1. \<And>x61 x62. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield x61 x62 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast x7 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. \<And>x81 x82. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke x81 x82 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 8. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 9. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 10. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>x61 x62. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield x61 x62 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast x7 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. \<And>x81 x82. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke x81 x82 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 8. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 9. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 10. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
case (Putfield Fd C')
[PROOF STATE]
proof (state)
this:
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield Fd C'

goal (10 subgoals):
 1. \<And>x61 x62. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield x61 x62 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast x7 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. \<And>x81 x82. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke x81 x82 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 8. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 9. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 10. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
with valid_node
[PROOF STATE]
proof (chain)
picking this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield Fd C'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield Fd C'

goal (1 subgoal):
 1. finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield Fd C'\<rbrakk> \<Longrightarrow> finite {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'}
[PROOF STEP]
apply (rule_tac B="{(_ (C,M,pc)#cs',\<lfloor>((C,M,Suc pc)#cs',False)\<rfloor> _),
            (_ (C,M,pc)#cs',\<lfloor>(find_handler_for P NullPointer ((C,M,pc)#cs'),True)\<rfloor> _),
            (_ fst(the(x)),None _)}" in finite_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield Fd C'\<rbrakk> \<Longrightarrow> {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'} \<subseteq> {(_ (C, M, pc) # cs',\<lfloor>((C, M, Suc pc) # cs', False)\<rfloor> _), (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P NullPointer ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield Fd C'\<rbrakk> \<Longrightarrow> finite {(_ (C, M, pc) # cs',\<lfloor>((C, M, Suc pc) # cs', False)\<rfloor> _), (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P NullPointer ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)}
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield Fd C'; xa \<in> {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'}\<rbrakk> \<Longrightarrow> xa \<in> {(_ (C, M, pc) # cs',\<lfloor>((C, M, Suc pc) # cs', False)\<rfloor> _), (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P NullPointer ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield Fd C'\<rbrakk> \<Longrightarrow> finite {(_ (C, M, pc) # cs',\<lfloor>((C, M, Suc pc) # cs', False)\<rfloor> _), (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P NullPointer ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)}
[PROOF STEP]
apply (clarsimp simp del: find_handler_for.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa a. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield Fd C'; (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> xa; valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); valid_node (P, C0, Main) xa; xa \<noteq> (_ (C, M, pc) # cs',\<lfloor>((C, M, Suc pc) # cs', False)\<rfloor> _); xa \<noteq> (_ fst (the x),None _)\<rbrakk> \<Longrightarrow> xa = (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P NullPointer ((C, M, pc) # cs'), True)\<rfloor> _)
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Putfield Fd C'\<rbrakk> \<Longrightarrow> finite {(_ (C, M, pc) # cs',\<lfloor>((C, M, Suc pc) # cs', False)\<rfloor> _), (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P NullPointer ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)}
[PROOF STEP]
by (erule JVM_CFG.cases, simp_all del: find_handler_for.simps)
[PROOF STATE]
proof (state)
this:
finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}

goal (9 subgoals):
 1. \<And>x7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast x7 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x81 x82. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke x81 x82 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 8. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 9. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>x7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast x7 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x81 x82. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke x81 x82 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 8. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 9. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
case (Checkcast C')
[PROOF STATE]
proof (state)
this:
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast C'

goal (9 subgoals):
 1. \<And>x7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast x7 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x81 x82. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke x81 x82 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 8. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 9. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
with valid_node
[PROOF STATE]
proof (chain)
picking this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast C'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast C'

goal (1 subgoal):
 1. finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast C'\<rbrakk> \<Longrightarrow> finite {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'}
[PROOF STEP]
apply (rule_tac B="{(_ (C,M,Suc pc)#cs',None _),
            (_ (C,M,pc)#cs',\<lfloor>(find_handler_for P ClassCast ((C,M,pc)#cs'),True)\<rfloor> _),
            (_ fst(the(x)),None _)}" in finite_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast C'\<rbrakk> \<Longrightarrow> {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'} \<subseteq> {(_ (C, M, Suc pc) # cs',None _), (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P ClassCast ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast C'\<rbrakk> \<Longrightarrow> finite {(_ (C, M, Suc pc) # cs',None _), (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P ClassCast ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)}
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast C'; xa \<in> {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'}\<rbrakk> \<Longrightarrow> xa \<in> {(_ (C, M, Suc pc) # cs',None _), (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P ClassCast ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast C'\<rbrakk> \<Longrightarrow> finite {(_ (C, M, Suc pc) # cs',None _), (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P ClassCast ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)}
[PROOF STEP]
apply (clarsimp simp del: find_handler_for.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa a. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast C'; (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> xa; valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); valid_node (P, C0, Main) xa; xa \<noteq> (_ (C, M, Suc pc) # cs',None _); xa \<noteq> (_ fst (the x),None _)\<rbrakk> \<Longrightarrow> xa = (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P ClassCast ((C, M, pc) # cs'), True)\<rfloor> _)
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Checkcast C'\<rbrakk> \<Longrightarrow> finite {(_ (C, M, Suc pc) # cs',None _), (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P ClassCast ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)}
[PROOF STEP]
by (erule JVM_CFG.cases, simp_all del: find_handler_for.simps)
[PROOF STATE]
proof (state)
this:
finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}

goal (8 subgoals):
 1. \<And>x81 x82. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke x81 x82 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 8. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>x81 x82. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke x81 x82 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 8. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
case (Invoke M' n')
[PROOF STATE]
proof (state)
this:
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke M' n'

goal (8 subgoals):
 1. \<And>x81 x82. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke x81 x82 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 8. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
with finite_classes valid_node
[PROOF STATE]
proof (chain)
picking this:
finite {C. is_class P\<^bsub>wf\<^esub> C}
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke M' n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite {C. is_class P\<^bsub>wf\<^esub> C}
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke M' n'

goal (1 subgoal):
 1. finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite {C. \<exists>a aa b. class P\<^bsub>wf\<^esub> C = \<lfloor>(a, aa, b)\<rfloor>}; JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke M' n'\<rbrakk> \<Longrightarrow> finite {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'}
[PROOF STEP]
apply (rule_tac B="
            {n'. (\<exists>D. is_class (P\<^bsub>wf\<^esub>) D \<and> n' = (_ (C,M,pc)#cs',\<lfloor>((D,M',0)#(C,M,pc)#cs',False)\<rfloor> _))}
            \<union> {(_ (C,M,pc)#cs',\<lfloor>(find_handler_for P NullPointer ((C,M,pc)#cs'),True)\<rfloor> _),
               (_ fst(the(x)),None _)}"
            in finite_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite {C. \<exists>a aa b. class P\<^bsub>wf\<^esub> C = \<lfloor>(a, aa, b)\<rfloor>}; JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke M' n'\<rbrakk> \<Longrightarrow> {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'} \<subseteq> {n'. \<exists>D. is_class P\<^bsub>wf\<^esub> D \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((D, M', 0) # (C, M, pc) # cs', False)\<rfloor> _)} \<union> {(_ (C, M, pc) # cs',\<lfloor>(find_handler_for P NullPointer ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)}
 2. \<lbrakk>finite {C. \<exists>a aa b. class P\<^bsub>wf\<^esub> C = \<lfloor>(a, aa, b)\<rfloor>}; JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke M' n'\<rbrakk> \<Longrightarrow> finite ({n'. \<exists>D. is_class P\<^bsub>wf\<^esub> D \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((D, M', 0) # (C, M, pc) # cs', False)\<rfloor> _)} \<union> {(_ (C, M, pc) # cs',\<lfloor>(find_handler_for P NullPointer ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)})
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>finite {C. \<exists>a aa b. class P\<^bsub>wf\<^esub> C = \<lfloor>(a, aa, b)\<rfloor>}; JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke M' n'; xa \<in> {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'}\<rbrakk> \<Longrightarrow> xa \<in> {n'. \<exists>D. is_class P\<^bsub>wf\<^esub> D \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((D, M', 0) # (C, M, pc) # cs', False)\<rfloor> _)} \<union> {(_ (C, M, pc) # cs',\<lfloor>(find_handler_for P NullPointer ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)}
 2. \<lbrakk>finite {C. \<exists>a aa b. class P\<^bsub>wf\<^esub> C = \<lfloor>(a, aa, b)\<rfloor>}; JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke M' n'\<rbrakk> \<Longrightarrow> finite ({n'. \<exists>D. is_class P\<^bsub>wf\<^esub> D \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((D, M', 0) # (C, M, pc) # cs', False)\<rfloor> _)} \<union> {(_ (C, M, pc) # cs',\<lfloor>(find_handler_for P NullPointer ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)})
[PROOF STEP]
apply (clarsimp simp del: find_handler_for.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa a. \<lbrakk>finite {C. \<exists>a aa b. class P\<^bsub>wf\<^esub> C = \<lfloor>(a, aa, b)\<rfloor>}; JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke M' n'; (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> xa; valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); valid_node (P, C0, Main) xa; xa \<noteq> (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P NullPointer ((C, M, pc) # cs'), True)\<rfloor> _); \<forall>D. (\<forall>a aa b. class P\<^bsub>wf\<^esub> D \<noteq> \<lfloor>(a, aa, b)\<rfloor>) \<or> xa \<noteq> (_ (C, M, pc) # cs',\<lfloor>((D, M', 0) # (C, M, pc) # cs', False)\<rfloor> _)\<rbrakk> \<Longrightarrow> xa = (_ fst (the x),None _)
 2. \<lbrakk>finite {C. \<exists>a aa b. class P\<^bsub>wf\<^esub> C = \<lfloor>(a, aa, b)\<rfloor>}; JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke M' n'\<rbrakk> \<Longrightarrow> finite ({n'. \<exists>D. is_class P\<^bsub>wf\<^esub> D \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((D, M', 0) # (C, M, pc) # cs', False)\<rfloor> _)} \<union> {(_ (C, M, pc) # cs',\<lfloor>(find_handler_for P NullPointer ((C, M, pc) # cs'), True)\<rfloor> _), (_ fst (the x),None _)})
[PROOF STEP]
apply (erule JVM_CFG.cases, simp_all del: find_handler_for.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa a prog Pa cd stk_length ek D. \<lbrakk>finite {C. \<exists>a aa b. class Pa\<^bsub>wf\<^esub> C = \<lfloor>(a, aa, b)\<rfloor>}; JVM_CFG_Interpret.valid_node (Pa, C0, Main) (_ (C, M, pc) # cs',None _); locLength Pa D M' 0 - Suc (fst (snd (snd (snd (snd (method Pa\<^bsub>wf\<^esub> D M')))))) = n'; valid_callstack (Pa, C0, Main) ((C, M, pc) # cs'); (\<exists>a b. Pa\<^bsub>\<Phi>\<^esub> D M' ! 0 = \<lfloor>(a, b)\<rfloor>) \<and> (\<exists>T Ts mxs mxl is. (\<exists>xt. Pa\<^bsub>wf\<^esub> \<turnstile> D sees M': Ts\<rightarrow>T = (mxs, mxl, is, xt) in D) \<and> is \<noteq> []) \<and> (\<exists>Q. (Pa, C0, Main) \<turnstile> (_ (C, M, pc) # cs',None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (C, M, pc) # cs',\<lfloor>((D, M', 0) # (C, M, pc) # cs', False)\<rfloor> _)) \<and> (\<exists>f. (Pa, C0, Main) \<turnstile> (_ (C, M, pc) # cs',\<lfloor>((D, M', 0) # (C, M, pc) # cs', False)\<rfloor> _) -\<Up>f\<rightarrow> (_ (D, M', 0) # (C, M, pc) # cs',None _)); \<forall>a aa b. class Pa\<^bsub>wf\<^esub> D \<noteq> \<lfloor>(a, aa, b)\<rfloor>; P = Pa; x = None; a = (\<lambda>(h, stk, loc). stk (length cs', stkLength Pa C M pc - Suc n') \<noteq> Null \<and> fst (method Pa\<^bsub>wf\<^esub> (cname_of h (the_Addr (stk (length cs', stkLength Pa C M pc - Suc n')))) M') = D)\<^sub>\<surd>; xa = (_ (C, M, pc) # cs',\<lfloor>((D, M', 0) # (C, M, pc) # cs', False)\<rfloor> _); prog = (Pa, C0, Main); instrs_of Pa\<^bsub>wf\<^esub> C M ! pc = Invoke M' n'; cd = length cs'; stk_length = stkLength Pa C M pc; ek = (\<lambda>(h, stk, loc). stk (length cs', stkLength Pa C M pc - Suc n') \<noteq> Null \<and> fst (method Pa\<^bsub>wf\<^esub> (cname_of h (the_Addr (stk (length cs', stkLength Pa C M pc - Suc n')))) M') = D)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (clarsimp simp del: find_handler_for.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>D ac ba T Ts mxs mxl is Q f xt. \<lbrakk>finite {C. \<exists>a aa b. class P\<^bsub>wf\<^esub> C = \<lfloor>(a, aa, b)\<rfloor>}; JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',None _); valid_callstack (P, C0, Main) ((C, M, pc) # cs'); \<forall>a aa b. class P\<^bsub>wf\<^esub> D \<noteq> \<lfloor>(a, aa, b)\<rfloor>; x = None; instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke M' (length ba - Suc mxl); n' = length ba - Suc mxl; P\<^bsub>\<Phi>\<^esub> D M' ! 0 = \<lfloor>(ac, ba)\<rfloor>; (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (C, M, pc) # cs',\<lfloor>((D, M', 0) # (C, M, pc) # cs', False)\<rfloor> _); (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',\<lfloor>((D, M', 0) # (C, M, pc) # cs', False)\<rfloor> _) -\<Up>f\<rightarrow> (_ (D, M', 0) # (C, M, pc) # cs',None _); is \<noteq> []; P\<^bsub>wf\<^esub> \<turnstile> D sees M': Ts\<rightarrow>T = (mxs, mxl, is, xt) in D\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule sees_method_is_class)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>D ac ba T Ts mxs mxl is Q f xt. \<lbrakk>finite {C. \<exists>a aa b. class P\<^bsub>wf\<^esub> C = \<lfloor>(a, aa, b)\<rfloor>}; JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',None _); valid_callstack (P, C0, Main) ((C, M, pc) # cs'); \<forall>a aa b. class P\<^bsub>wf\<^esub> D \<noteq> \<lfloor>(a, aa, b)\<rfloor>; x = None; instrs_of P\<^bsub>wf\<^esub> C M ! pc = Invoke M' (length ba - Suc mxl); n' = length ba - Suc mxl; P\<^bsub>\<Phi>\<^esub> D M' ! 0 = \<lfloor>(ac, ba)\<rfloor>; (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (C, M, pc) # cs',\<lfloor>((D, M', 0) # (C, M, pc) # cs', False)\<rfloor> _); (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',\<lfloor>((D, M', 0) # (C, M, pc) # cs', False)\<rfloor> _) -\<Up>f\<rightarrow> (_ (D, M', 0) # (C, M, pc) # cs',None _); is \<noteq> []; is_class P\<^bsub>wf\<^esub> D\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (clarsimp simp del: find_handler_for.simps)
[PROOF STATE]
proof (state)
this:
finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}

goal (7 subgoals):
 1. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
case Return
[PROOF STATE]
proof (state)
this:
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return

goal (7 subgoals):
 1. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 7. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
with valid_node
[PROOF STATE]
proof (chain)
picking this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return

goal (1 subgoal):
 1. finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return\<rbrakk> \<Longrightarrow> finite {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'}
[PROOF STEP]
apply (rule_tac B="
            {(_ (fst(hd(cs')),fst(snd(hd(cs'))),Suc(snd(snd(hd(cs')))))#(tl cs'),None _),
             (_Exit_)}" in finite_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return\<rbrakk> \<Longrightarrow> {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'} \<subseteq> {(_ (fst (hd cs'), fst (snd (hd cs')), Suc (snd (snd (hd cs')))) # tl cs',None _), (_Exit_)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return\<rbrakk> \<Longrightarrow> finite {(_ (fst (hd cs'), fst (snd (hd cs')), Suc (snd (snd (hd cs')))) # tl cs',None _), (_Exit_)}
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return; xa \<in> {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'}\<rbrakk> \<Longrightarrow> xa \<in> {(_ (fst (hd cs'), fst (snd (hd cs')), Suc (snd (snd (hd cs')))) # tl cs',None _), (_Exit_)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return\<rbrakk> \<Longrightarrow> finite {(_ (fst (hd cs'), fst (snd (hd cs')), Suc (snd (snd (hd cs')))) # tl cs',None _), (_Exit_)}
[PROOF STEP]
apply (clarsimp simp del: find_handler_for.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa a. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return; (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> xa; valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); valid_node (P, C0, Main) xa; xa \<noteq> (_Exit_)\<rbrakk> \<Longrightarrow> xa = (_ (fst (hd cs'), fst (snd (hd cs')), Suc (snd (snd (hd cs')))) # tl cs',None _)
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Return\<rbrakk> \<Longrightarrow> finite {(_ (fst (hd cs'), fst (snd (hd cs')), Suc (snd (snd (hd cs')))) # tl cs',None _), (_Exit_)}
[PROOF STEP]
by (erule JVM_CFG.cases, simp_all del: find_handler_for.simps)
[PROOF STATE]
proof (state)
this:
finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}

goal (6 subgoals):
 1. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
case Pop
[PROOF STATE]
proof (state)
this:
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop

goal (6 subgoals):
 1. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 6. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
with valid_node
[PROOF STATE]
proof (chain)
picking this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop

goal (1 subgoal):
 1. finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop\<rbrakk> \<Longrightarrow> finite {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'}
[PROOF STEP]
apply (rule_tac B="{(_ (C,M,Suc pc)#cs',None _)}" in finite_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop\<rbrakk> \<Longrightarrow> {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'} \<subseteq> {(_ (C, M, Suc pc) # cs',None _)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Pop\<rbrakk> \<Longrightarrow> finite {(_ (C, M, Suc pc) # cs',None _)}
[PROOF STEP]
by (auto elim: JVM_CFG.cases)
[PROOF STATE]
proof (state)
this:
finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}

goal (5 subgoals):
 1. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
case IAdd
[PROOF STATE]
proof (state)
this:
instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd

goal (5 subgoals):
 1. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 5. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
with valid_node
[PROOF STATE]
proof (chain)
picking this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd

goal (1 subgoal):
 1. finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd\<rbrakk> \<Longrightarrow> finite {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'}
[PROOF STEP]
apply (rule_tac B="{(_ (C,M,Suc pc)#cs',None _)}" in finite_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd\<rbrakk> \<Longrightarrow> {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'} \<subseteq> {(_ (C, M, Suc pc) # cs',None _)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = IAdd\<rbrakk> \<Longrightarrow> finite {(_ (C, M, Suc pc) # cs',None _)}
[PROOF STEP]
by (auto elim: JVM_CFG.cases)
[PROOF STATE]
proof (state)
this:
finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}

goal (4 subgoals):
 1. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
case (Goto i)
[PROOF STATE]
proof (state)
this:
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto i

goal (4 subgoals):
 1. \<And>x12. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto x12 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 4. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
with valid_node
[PROOF STATE]
proof (chain)
picking this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto i

goal (1 subgoal):
 1. finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto i\<rbrakk> \<Longrightarrow> finite {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'}
[PROOF STEP]
apply (rule_tac B="{(_ (C,M,nat (int pc + i))#cs',None _)}" in finite_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto i\<rbrakk> \<Longrightarrow> {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'} \<subseteq> {(_ (C, M, nat (int pc + i)) # cs',None _)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Goto i\<rbrakk> \<Longrightarrow> finite {(_ (C, M, nat (int pc + i)) # cs',None _)}
[PROOF STEP]
by (auto elim: JVM_CFG.cases)
[PROOF STATE]
proof (state)
this:
finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}

goal (3 subgoals):
 1. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
case CmpEq
[PROOF STATE]
proof (state)
this:
instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq

goal (3 subgoals):
 1. instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 3. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
with valid_node
[PROOF STATE]
proof (chain)
picking this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq

goal (1 subgoal):
 1. finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq\<rbrakk> \<Longrightarrow> finite {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'}
[PROOF STEP]
apply (rule_tac B="{(_ (C,M,Suc pc)#cs',None _)}" in finite_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq\<rbrakk> \<Longrightarrow> {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'} \<subseteq> {(_ (C, M, Suc pc) # cs',None _)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = CmpEq\<rbrakk> \<Longrightarrow> finite {(_ (C, M, Suc pc) # cs',None _)}
[PROOF STEP]
by (auto elim: JVM_CFG.cases)
[PROOF STATE]
proof (state)
this:
finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}

goal (2 subgoals):
 1. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
case (IfFalse i)
[PROOF STATE]
proof (state)
this:
instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse i

goal (2 subgoals):
 1. \<And>x14. instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse x14 \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
 2. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
with valid_node
[PROOF STATE]
proof (chain)
picking this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse i

goal (1 subgoal):
 1. finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse i\<rbrakk> \<Longrightarrow> finite {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'}
[PROOF STEP]
apply (rule_tac B="{(_ (C,M,Suc pc)#cs',None _),
            (_ (C,M,nat (int pc + i))#cs',None _)}" in finite_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse i\<rbrakk> \<Longrightarrow> {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'} \<subseteq> {(_ (C, M, Suc pc) # cs',None _), (_ (C, M, nat (int pc + i)) # cs',None _)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = IfFalse i\<rbrakk> \<Longrightarrow> finite {(_ (C, M, Suc pc) # cs',None _), (_ (C, M, nat (int pc + i)) # cs',None _)}
[PROOF STEP]
by (auto elim: JVM_CFG.cases)
[PROOF STATE]
proof (state)
this:
finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}

goal (1 subgoal):
 1. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
case Throw
[PROOF STATE]
proof (state)
this:
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw

goal (1 subgoal):
 1. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
have "finite {(l,pc'). l < Suc (length cs') \<and>
          pc' < (\<Sum>i\<le>(length cs'). (length (instrs_of (P\<^bsub>wf\<^esub>) (fst (((C, M, pc) # cs') ! i))
          (fst (snd (((C, M, pc) # cs') ! i))))))}"
          (is "finite ?f1")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {(l, pc'). l < Suc (length cs') \<and> pc' < (\<Sum>i\<le>length cs'. length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! i)) (fst (snd (((C, M, pc) # cs') ! i)))))}
[PROOF STEP]
by (auto intro: finite_cartesian_product bounded_nat_set_is_finite)
[PROOF STATE]
proof (state)
this:
finite {(l, pc'). l < Suc (length cs') \<and> pc' < (\<Sum>i\<le>length cs'. length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! i)) (fst (snd (((C, M, pc) # cs') ! i)))))}

goal (1 subgoal):
 1. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
hence f_1: "finite {(l,pc'). l < length ((C, M, pc) # cs') \<and>
            pc' < length (instrs_of (P\<^bsub>wf\<^esub>) (fst(((C,M,pc)#cs')!l)) (fst(snd(((C,M,pc)#cs')!l))))}"
[PROOF STATE]
proof (prove)
using this:
finite {(l, pc'). l < Suc (length cs') \<and> pc' < (\<Sum>i\<le>length cs'. length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! i)) (fst (snd (((C, M, pc) # cs') ! i)))))}

goal (1 subgoal):
 1. finite {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))}
[PROOF STEP]
apply (rule_tac B="?f1" in finite_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite {(l, pc'). l < Suc (length cs') \<and> pc' < (\<Sum>i\<le>length cs'. length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! i)) (fst (snd (((C, M, pc) # cs') ! i)))))} \<Longrightarrow> {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))} \<subseteq> {(l, pc'). l < Suc (length cs') \<and> pc' < (\<Sum>i\<le>length cs'. length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! i)) (fst (snd (((C, M, pc) # cs') ! i)))))}
 2. finite {(l, pc'). l < Suc (length cs') \<and> pc' < (\<Sum>i\<le>length cs'. length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! i)) (fst (snd (((C, M, pc) # cs') ! i)))))} \<Longrightarrow> finite {(l, pc'). l < Suc (length cs') \<and> pc' < (\<Sum>i\<le>length cs'. length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! i)) (fst (snd (((C, M, pc) # cs') ! i)))))}
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a < Suc (length cs'); b < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! a)) (fst (snd (((C, M, pc) # cs') ! a))))\<rbrakk> \<Longrightarrow> b < (\<Sum>i\<le>length cs'. length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! i)) (fst (snd (((C, M, pc) # cs') ! i)))))
 2. finite {(l, pc'). l < Suc (length cs') \<and> pc' < (\<Sum>i\<le>length cs'. length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! i)) (fst (snd (((C, M, pc) # cs') ! i)))))} \<Longrightarrow> finite {(l, pc'). l < Suc (length cs') \<and> pc' < (\<Sum>i\<le>length cs'. length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! i)) (fst (snd (((C, M, pc) # cs') ! i)))))}
[PROOF STEP]
apply (rule less_le_trans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>a < Suc (length cs'); b < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! a)) (fst (snd (((C, M, pc) # cs') ! a))))\<rbrakk> \<Longrightarrow> b < ?y8 a b
 2. \<And>a b. \<lbrakk>a < Suc (length cs'); b < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! a)) (fst (snd (((C, M, pc) # cs') ! a))))\<rbrakk> \<Longrightarrow> ?y8 a b \<le> (\<Sum>i\<le>length cs'. length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! i)) (fst (snd (((C, M, pc) # cs') ! i)))))
 3. finite {(l, pc'). l < Suc (length cs') \<and> pc' < (\<Sum>i\<le>length cs'. length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! i)) (fst (snd (((C, M, pc) # cs') ! i)))))} \<Longrightarrow> finite {(l, pc'). l < Suc (length cs') \<and> pc' < (\<Sum>i\<le>length cs'. length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! i)) (fst (snd (((C, M, pc) # cs') ! i)))))}
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>a < Suc (length cs'); b < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! a)) (fst (snd (((C, M, pc) # cs') ! a))))\<rbrakk> \<Longrightarrow> ?y8 a b \<le> (\<Sum>i\<le>length cs'. length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! i)) (fst (snd (((C, M, pc) # cs') ! i)))))
 2. finite {(l, pc'). l < Suc (length cs') \<and> pc' < (\<Sum>i\<le>length cs'. length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! i)) (fst (snd (((C, M, pc) # cs') ! i)))))} \<Longrightarrow> finite {(l, pc'). l < Suc (length cs') \<and> pc' < (\<Sum>i\<le>length cs'. length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! i)) (fst (snd (((C, M, pc) # cs') ! i)))))}
 3. \<And>a b. \<lbrakk>a < Suc (length cs'); b < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! a)) (fst (snd (((C, M, pc) # cs') ! a))))\<rbrakk> \<Longrightarrow> b < ?y8 a b
[PROOF STEP]
apply (rule_tac A="{a}" in sum_mono2)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>a < Suc (length cs'); b < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! a)) (fst (snd (((C, M, pc) # cs') ! a))))\<rbrakk> \<Longrightarrow> finite {..length cs'}
 2. \<And>a b. \<lbrakk>a < Suc (length cs'); b < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! a)) (fst (snd (((C, M, pc) # cs') ! a))))\<rbrakk> \<Longrightarrow> {a} \<subseteq> {..length cs'}
 3. \<And>a b ba. \<lbrakk>a < Suc (length cs'); b < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! a)) (fst (snd (((C, M, pc) # cs') ! a)))); ba \<in> {..length cs'} - {a}\<rbrakk> \<Longrightarrow> 0 \<le> length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! ba)) (fst (snd (((C, M, pc) # cs') ! ba))))
 4. finite {(l, pc'). l < Suc (length cs') \<and> pc' < (\<Sum>i\<le>length cs'. length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! i)) (fst (snd (((C, M, pc) # cs') ! i)))))} \<Longrightarrow> finite {(l, pc'). l < Suc (length cs') \<and> pc' < (\<Sum>i\<le>length cs'. length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! i)) (fst (snd (((C, M, pc) # cs') ! i)))))}
 5. \<And>a b. \<lbrakk>a < Suc (length cs'); b < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! a)) (fst (snd (((C, M, pc) # cs') ! a))))\<rbrakk> \<Longrightarrow> b < (\<Sum>i\<in>{a}. length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! i)) (fst (snd (((C, M, pc) # cs') ! i)))))
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
finite {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))}

goal (1 subgoal):
 1. instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw \<Longrightarrow> finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
from valid_node Throw
[PROOF STATE]
proof (chain)
picking this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
JVM_CFG_Interpret.valid_node prog n
instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw

goal (1 subgoal):
 1. finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'}
[PROOF STEP]
apply (rule_tac B="
            {n'. \<exists>Cx Mx pc' h cs'' pcx. (C,M,pc)#cs' = cs''@[(Cx,Mx,pcx)]@h \<and>
              pc' < length (instrs_of (P\<^bsub>wf\<^esub>) Cx Mx) \<and>
              n' = (_ (C,M,pc)#cs',\<lfloor>((Cx,Mx,pc')#h,True)\<rfloor> _)}
            \<union> {(_ fst(the(x)),None _), (_Exit_), (_ (C,M,pc)#cs',\<lfloor>([],True)\<rfloor> _)}"
            in finite_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'} \<subseteq> {n'. \<exists>Cx Mx pc' h cs'' pcx. (C, M, pc) # cs' = cs'' @ [(Cx, Mx, pcx)] @ h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)} \<union> {(_ fst (the x),None _), (_Exit_), (_ (C, M, pc) # cs',\<lfloor>([], True)\<rfloor> _)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ({n'. \<exists>Cx Mx pc' h cs'' pcx. (C, M, pc) # cs' = cs'' @ [(Cx, Mx, pcx)] @ h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)} \<union> {(_ fst (the x),None _), (_Exit_), (_ (C, M, pc) # cs',\<lfloor>([], True)\<rfloor> _)})
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; xa \<in> {n'. (\<exists>a. (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> n') \<and> valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _) \<and> valid_node (P, C0, Main) n'}\<rbrakk> \<Longrightarrow> xa \<in> {n'. \<exists>Cx Mx pc' h cs'' pcx. (C, M, pc) # cs' = cs'' @ [(Cx, Mx, pcx)] @ h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)} \<union> {(_ fst (the x),None _), (_Exit_), (_ (C, M, pc) # cs',\<lfloor>([], True)\<rfloor> _)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ({n'. \<exists>Cx Mx pc' h cs'' pcx. (C, M, pc) # cs' = cs'' @ [(Cx, Mx, pcx)] @ h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)} \<union> {(_ fst (the x),None _), (_Exit_), (_ (C, M, pc) # cs',\<lfloor>([], True)\<rfloor> _)})
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa a. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',x _) -a\<rightarrow> xa; valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); valid_node (P, C0, Main) xa; xa \<noteq> (_ fst (the x),None _); xa \<noteq> (_Exit_); \<forall>Cx Mx pc'. pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<longrightarrow> (\<forall>h. (\<forall>cs'' pcx. (C, M, pc) # cs' \<noteq> cs'' @ (Cx, Mx, pcx) # h) \<or> xa \<noteq> (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _))\<rbrakk> \<Longrightarrow> xa = (_ (C, M, pc) # cs',\<lfloor>([], True)\<rfloor> _)
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ({n'. \<exists>Cx Mx pc' h cs'' pcx. (C, M, pc) # cs' = cs'' @ [(Cx, Mx, pcx)] @ h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)} \<union> {(_ fst (the x),None _), (_Exit_), (_ (C, M, pc) # cs',\<lfloor>([], True)\<rfloor> _)})
[PROOF STEP]
apply (erule JVM_CFG.cases, simp_all del: find_handler_for.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa a prog Pa cd stk_length cs'a ek. \<lbrakk>JVM_CFG_Interpret.valid_node (Pa, C0, Main) (_ (C, M, pc) # cs',None _); valid_callstack (Pa, C0, Main) ((C, M, pc) # cs'); valid_callstack (Pa, C0, Main) cs'a \<and> (\<exists>Q. (Pa, C0, Main) \<turnstile> (_ (C, M, pc) # cs',None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (C, M, pc) # cs',\<lfloor>(cs'a, True)\<rfloor> _)) \<and> (\<exists>f. (Pa, C0, Main) \<turnstile> (_ (C, M, pc) # cs',\<lfloor>(cs'a, True)\<rfloor> _) -\<Up>f\<rightarrow> (_ cs'a,None _)); \<forall>Cx Mx pc'. pc' < length (instrs_of Pa\<^bsub>wf\<^esub> Cx Mx) \<longrightarrow> (\<forall>h. (\<forall>cs'' pcx. (C, M, pc) # cs' \<noteq> cs'' @ (Cx, Mx, pcx) # h) \<or> cs'a \<noteq> (Cx, Mx, pc') # h); P = Pa; x = None; a = (\<lambda>(h, stk, loc). stk (length cs', stkLength Pa C M pc - Suc 0) = Null \<and> find_handler_for Pa NullPointer ((C, M, pc) # cs') = cs'a \<or> stk (length cs', stkLength Pa C M pc - Suc 0) \<noteq> Null \<and> find_handler_for Pa (cname_of h (the_Addr (stk (length cs', stkLength Pa C M pc - Suc 0)))) ((C, M, pc) # cs') = cs'a)\<^sub>\<surd>; xa = (_ (C, M, pc) # cs',\<lfloor>(cs'a, True)\<rfloor> _); prog = (Pa, C0, Main); instrs_of Pa\<^bsub>wf\<^esub> C M ! pc = Throw; cd = length cs'; stk_length = stkLength Pa C M pc; \<exists>Exc. find_handler_for Pa Exc ((C, M, pc) # cs') = cs'a; ek = (\<lambda>(h, stk, loc). stk (length cs', stkLength Pa C M pc - Suc 0) = Null \<and> find_handler_for Pa NullPointer ((C, M, pc) # cs') = cs'a \<or> stk (length cs', stkLength Pa C M pc - Suc 0) \<noteq> Null \<and> find_handler_for Pa (cname_of h (the_Addr (stk (length cs', stkLength Pa C M pc - Suc 0)))) ((C, M, pc) # cs') = cs'a)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> cs'a = []
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite {n'. \<exists>Cx Mx pc' h. (\<exists>cs'' pcx. (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h) \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)}
[PROOF STEP]
apply (clarsimp simp del: find_handler_for.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Exc Q f. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',None _); valid_callstack (P, C0, Main) ((C, M, pc) # cs'); \<forall>Cx Mx pc'. pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<longrightarrow> (\<forall>h. (\<forall>cs'' pcx. (C, M, pc) # cs' \<noteq> cs'' @ (Cx, Mx, pcx) # h) \<or> find_handler_for P Exc ((C, M, pc) # cs') \<noteq> (Cx, Mx, pc') # h); x = None; instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; valid_callstack (P, C0, Main) (find_handler_for P Exc ((C, M, pc) # cs')); (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P Exc ((C, M, pc) # cs'), True)\<rfloor> _); (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P Exc ((C, M, pc) # cs'), True)\<rfloor> _) -\<Up>f\<rightarrow> (_ find_handler_for P Exc ((C, M, pc) # cs'),None _)\<rbrakk> \<Longrightarrow> find_handler_for P Exc ((C, M, pc) # cs') = []
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite {n'. \<exists>Cx Mx pc' h. (\<exists>cs'' pcx. (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h) \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)}
[PROOF STEP]
apply (case_tac "find_handler_for P Exc ((C,M,pc)#cs')", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Exc Q f a list. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',None _); valid_callstack (P, C0, Main) ((C, M, pc) # cs'); \<forall>Cx Mx pc'. pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<longrightarrow> (\<forall>h. (\<forall>cs'' pcx. (C, M, pc) # cs' \<noteq> cs'' @ (Cx, Mx, pcx) # h) \<or> find_handler_for P Exc ((C, M, pc) # cs') \<noteq> (Cx, Mx, pc') # h); x = None; instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; valid_callstack (P, C0, Main) (find_handler_for P Exc ((C, M, pc) # cs')); (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P Exc ((C, M, pc) # cs'), True)\<rfloor> _); (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',\<lfloor>(find_handler_for P Exc ((C, M, pc) # cs'), True)\<rfloor> _) -\<Up>f\<rightarrow> (_ find_handler_for P Exc ((C, M, pc) # cs'),None _); find_handler_for P Exc ((C, M, pc) # cs') = a # list\<rbrakk> \<Longrightarrow> find_handler_for P Exc ((C, M, pc) # cs') = []
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite {n'. \<exists>Cx Mx pc' h. (\<exists>cs'' pcx. (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h) \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)}
[PROOF STEP]
apply (clarsimp simp del: find_handler_for.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Exc Q f a aa b list. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',None _); valid_callstack (P, C0, Main) ((C, M, pc) # cs'); b < length (instrs_of P\<^bsub>wf\<^esub> a aa) \<longrightarrow> (\<forall>h. (\<forall>cs'' pcx. (C, M, pc) # cs' \<noteq> cs'' @ (a, aa, pcx) # h) \<or> list \<noteq> h); x = None; instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; valid_callstack (P, C0, Main) ((a, aa, b) # list); (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (C, M, pc) # cs',\<lfloor>((a, aa, b) # list, True)\<rfloor> _); (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',\<lfloor>((a, aa, b) # list, True)\<rfloor> _) -\<Up>f\<rightarrow> (_ (a, aa, b) # list,None _); find_handler_for P Exc ((C, M, pc) # cs') = (a, aa, b) # list\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite {n'. \<exists>Cx Mx pc' h. (\<exists>cs'' pcx. (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h) \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)}
[PROOF STEP]
apply (erule impE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Exc Q f a aa b list. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',None _); valid_callstack (P, C0, Main) ((C, M, pc) # cs'); x = None; instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; valid_callstack (P, C0, Main) ((a, aa, b) # list); (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (C, M, pc) # cs',\<lfloor>((a, aa, b) # list, True)\<rfloor> _); (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',\<lfloor>((a, aa, b) # list, True)\<rfloor> _) -\<Up>f\<rightarrow> (_ (a, aa, b) # list,None _); find_handler_for P Exc ((C, M, pc) # cs') = (a, aa, b) # list\<rbrakk> \<Longrightarrow> b < length (instrs_of P\<^bsub>wf\<^esub> a aa)
 2. \<And>Exc Q f a aa b list. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',None _); valid_callstack (P, C0, Main) ((C, M, pc) # cs'); x = None; instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; valid_callstack (P, C0, Main) ((a, aa, b) # list); (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (C, M, pc) # cs',\<lfloor>((a, aa, b) # list, True)\<rfloor> _); (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',\<lfloor>((a, aa, b) # list, True)\<rfloor> _) -\<Up>f\<rightarrow> (_ (a, aa, b) # list,None _); find_handler_for P Exc ((C, M, pc) # cs') = (a, aa, b) # list; \<forall>h. (\<forall>cs'' pcx. (C, M, pc) # cs' \<noteq> cs'' @ (a, aa, pcx) # h) \<or> list \<noteq> h\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite {n'. \<exists>Cx Mx pc' h. (\<exists>cs'' pcx. (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h) \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)}
[PROOF STEP]
apply (case_tac "list", fastforce, fastforce)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Exc Q f a aa b list. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',None _); valid_callstack (P, C0, Main) ((C, M, pc) # cs'); x = None; instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; valid_callstack (P, C0, Main) ((a, aa, b) # list); (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (C, M, pc) # cs',\<lfloor>((a, aa, b) # list, True)\<rfloor> _); (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',\<lfloor>((a, aa, b) # list, True)\<rfloor> _) -\<Up>f\<rightarrow> (_ (a, aa, b) # list,None _); find_handler_for P Exc ((C, M, pc) # cs') = (a, aa, b) # list; \<forall>h. (\<forall>cs'' pcx. (C, M, pc) # cs' \<noteq> cs'' @ (a, aa, pcx) # h) \<or> list \<noteq> h\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite {n'. \<exists>Cx Mx pc' h. (\<exists>cs'' pcx. (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h) \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)}
[PROOF STEP]
apply (frule find_handler_for_tl_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Exc Q f a aa b list. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',None _); valid_callstack (P, C0, Main) ((C, M, pc) # cs'); x = None; instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; valid_callstack (P, C0, Main) ((a, aa, b) # list); (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ (C, M, pc) # cs',\<lfloor>((a, aa, b) # list, True)\<rfloor> _); (P, C0, Main) \<turnstile> (_ (C, M, pc) # cs',\<lfloor>((a, aa, b) # list, True)\<rfloor> _) -\<Up>f\<rightarrow> (_ (a, aa, b) # list,None _); find_handler_for P Exc ((C, M, pc) # cs') = (a, aa, b) # list; \<forall>h. (\<forall>cs'' pcx. (C, M, pc) # cs' \<noteq> cs'' @ (a, aa, pcx) # h) \<or> list \<noteq> h; \<exists>cs'' pca. (C, M, pc) # cs' = cs'' @ [(a, aa, pca)] @ list\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite {n'. \<exists>Cx Mx pc' h. (\<exists>cs'' pcx. (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h) \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)}
[PROOF STEP]
apply (clarsimp simp del: find_handler_for.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Exc Q f a aa b list cs'' pca. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ cs'' @ (a, aa, pca) # list,None _); valid_callstack (P, C0, Main) (cs'' @ (a, aa, pca) # list); x = None; instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; valid_callstack (P, C0, Main) ((a, aa, b) # list); (P, C0, Main) \<turnstile> (_ cs'' @ (a, aa, pca) # list,None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ cs'' @ (a, aa, pca) # list,\<lfloor>((a, aa, b) # list, True)\<rfloor> _); (P, C0, Main) \<turnstile> (_ cs'' @ (a, aa, pca) # list,\<lfloor>((a, aa, b) # list, True)\<rfloor> _) -\<Up>f\<rightarrow> (_ (a, aa, b) # list,None _); find_handler_for P Exc (cs'' @ (a, aa, pca) # list) = (a, aa, b) # list; \<forall>h. (\<forall>cs''a pcx. cs'' @ (a, aa, pca) # list \<noteq> cs''a @ (a, aa, pcx) # h) \<or> list \<noteq> h; (C, M, pc) # cs' = cs'' @ (a, aa, pca) # list\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite {n'. \<exists>Cx Mx pc' h. (\<exists>cs'' pcx. (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h) \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)}
[PROOF STEP]
apply (erule_tac x="list" in allE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Exc Q f a aa b list cs'' pca. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ cs'' @ (a, aa, pca) # list,None _); valid_callstack (P, C0, Main) (cs'' @ (a, aa, pca) # list); x = None; instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; valid_callstack (P, C0, Main) ((a, aa, b) # list); (P, C0, Main) \<turnstile> (_ cs'' @ (a, aa, pca) # list,None _) -(Q)\<^sub>\<surd>\<rightarrow> (_ cs'' @ (a, aa, pca) # list,\<lfloor>((a, aa, b) # list, True)\<rfloor> _); (P, C0, Main) \<turnstile> (_ cs'' @ (a, aa, pca) # list,\<lfloor>((a, aa, b) # list, True)\<rfloor> _) -\<Up>f\<rightarrow> (_ (a, aa, b) # list,None _); find_handler_for P Exc (cs'' @ (a, aa, pca) # list) = (a, aa, b) # list; (C, M, pc) # cs' = cs'' @ (a, aa, pca) # list; (\<forall>cs''a pcx. cs'' @ (a, aa, pca) # list \<noteq> cs''a @ (a, aa, pcx) # list) \<or> list \<noteq> list\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite {n'. \<exists>Cx Mx pc' h. (\<exists>cs'' pcx. (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h) \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)}
[PROOF STEP]
apply (clarsimp simp del: find_handler_for.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite {n'. \<exists>Cx Mx pc' h. (\<exists>cs'' pcx. (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h) \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)}
[PROOF STEP]
apply (subgoal_tac
            "finite (
              (\<lambda>(Cx,Mx,pc',h,cs'',pcx).  (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) `
              {(Cx,Mx,pc',h,cs'',pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and>
                pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)})")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)})\<rbrakk> \<Longrightarrow> finite {n'. \<exists>Cx Mx pc' h. (\<exists>cs'' pcx. (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h) \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ((\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)})
[PROOF STEP]
apply (case_tac "((\<lambda>(Cx, Mx, pc', h, cs'', pcx).
             (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) `
             {(Cx, Mx, pc', h, cs'', pcx).
               (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and>
               pc' < length (instrs_of (P\<^bsub>wf\<^esub>) Cx Mx)}) =
             {n'. \<exists>Cx Mx pc' h.
                (\<exists>cs'' pcx. (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h) \<and>
                pc' < length (instrs_of (P\<^bsub>wf\<^esub>) Cx Mx) \<and>
                n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)}")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)}); (\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)} = {n'. \<exists>Cx Mx pc' h. (\<exists>cs'' pcx. (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h) \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)}\<rbrakk> \<Longrightarrow> finite {n'. \<exists>Cx Mx pc' h. (\<exists>cs'' pcx. (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h) \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)}); (\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)} \<noteq> {n'. \<exists>Cx Mx pc' h. (\<exists>cs'' pcx. (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h) \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)}\<rbrakk> \<Longrightarrow> finite {n'. \<exists>Cx Mx pc' h. (\<exists>cs'' pcx. (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h) \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)}
 3. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ((\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)})
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)}); (\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)} \<noteq> {n'. \<exists>Cx Mx pc' h. (\<exists>cs'' pcx. (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h) \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)}\<rbrakk> \<Longrightarrow> finite {n'. \<exists>Cx Mx pc' h. (\<exists>cs'' pcx. (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h) \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ((\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)})
[PROOF STEP]
apply (erule notE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)})\<rbrakk> \<Longrightarrow> (\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)} = {n'. \<exists>Cx Mx pc' h. (\<exists>cs'' pcx. (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h) \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ((\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)})
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)})\<rbrakk> \<Longrightarrow> (\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)} \<subseteq> {n'. \<exists>Cx Mx pc' h. (\<exists>cs'' pcx. (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h) \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)})\<rbrakk> \<Longrightarrow> {n'. \<exists>Cx Mx pc' h. (\<exists>cs'' pcx. (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h) \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)} \<subseteq> (\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)}
 3. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ((\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)})
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)})\<rbrakk> \<Longrightarrow> {n'. \<exists>Cx Mx pc' h. (\<exists>cs'' pcx. (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h) \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx) \<and> n' = (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)} \<subseteq> (\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ((\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)})
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Cx Mx pc' h cs'' pcx. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ cs'' @ (Cx, Mx, pcx) # h,x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>x. case x of (Cxa, Mxa, pc', ha, cs''a, pcxa) \<Rightarrow> (_ cs'' @ (Cx, Mx, pcx) # h,\<lfloor>((Cxa, Mxa, pc') # ha, True)\<rfloor> _)) ` {(Cxa, Mxa, pc', ha, cs''a, pcxa). cs'' @ (Cx, Mx, pcx) # h = cs''a @ (Cxa, Mxa, pcxa) # ha \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cxa Mxa)}); (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h; pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)\<rbrakk> \<Longrightarrow> (_ cs'' @ (Cx, Mx, pcx) # h,\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _) \<in> (\<lambda>x. case x of (Cxa, Mxa, pc', ha, cs''a, pcxa) \<Rightarrow> (_ cs'' @ (Cx, Mx, pcx) # h,\<lfloor>((Cxa, Mxa, pc') # ha, True)\<rfloor> _)) ` {(Cxa, Mxa, pc', ha, cs''a, pcxa). cs'' @ (Cx, Mx, pcx) # h = cs''a @ (Cxa, Mxa, pcxa) # ha \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cxa Mxa)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ((\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)})
[PROOF STEP]
apply (rule_tac x="(Cx,Mx,pc',h,cs'',pcx)" in image_eqI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Cx Mx pc' h cs'' pcx. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ cs'' @ (Cx, Mx, pcx) # h,x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>x. case x of (Cxa, Mxa, pc', ha, cs''a, pcxa) \<Rightarrow> (_ cs'' @ (Cx, Mx, pcx) # h,\<lfloor>((Cxa, Mxa, pc') # ha, True)\<rfloor> _)) ` {(Cxa, Mxa, pc', ha, cs''a, pcxa). cs'' @ (Cx, Mx, pcx) # h = cs''a @ (Cxa, Mxa, pcxa) # ha \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cxa Mxa)}); (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h; pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)\<rbrakk> \<Longrightarrow> (_ cs'' @ (Cx, Mx, pcx) # h,\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _) = (case (Cx, Mx, pc', h, cs'', pcx) of (Cxa, Mxa, pc', ha, cs''a, pcxa) \<Rightarrow> (_ cs'' @ (Cx, Mx, pcx) # h,\<lfloor>((Cxa, Mxa, pc') # ha, True)\<rfloor> _))
 2. \<And>Cx Mx pc' h cs'' pcx. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ cs'' @ (Cx, Mx, pcx) # h,x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>x. case x of (Cxa, Mxa, pc', ha, cs''a, pcxa) \<Rightarrow> (_ cs'' @ (Cx, Mx, pcx) # h,\<lfloor>((Cxa, Mxa, pc') # ha, True)\<rfloor> _)) ` {(Cxa, Mxa, pc', ha, cs''a, pcxa). cs'' @ (Cx, Mx, pcx) # h = cs''a @ (Cxa, Mxa, pcxa) # ha \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cxa Mxa)}); (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h; pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)\<rbrakk> \<Longrightarrow> (Cx, Mx, pc', h, cs'', pcx) \<in> {(Cxa, Mxa, pc', ha, cs''a, pcxa). cs'' @ (Cx, Mx, pcx) # h = cs''a @ (Cxa, Mxa, pcxa) # ha \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cxa Mxa)}
 3. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ((\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)})
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Cx Mx pc' h cs'' pcx. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ cs'' @ (Cx, Mx, pcx) # h,x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>x. case x of (Cxa, Mxa, pc', ha, cs''a, pcxa) \<Rightarrow> (_ cs'' @ (Cx, Mx, pcx) # h,\<lfloor>((Cxa, Mxa, pc') # ha, True)\<rfloor> _)) ` {(Cxa, Mxa, pc', ha, cs''a, pcxa). cs'' @ (Cx, Mx, pcx) # h = cs''a @ (Cxa, Mxa, pcxa) # ha \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cxa Mxa)}); (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h; pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)\<rbrakk> \<Longrightarrow> (Cx, Mx, pc', h, cs'', pcx) \<in> {(Cxa, Mxa, pc', ha, cs''a, pcxa). cs'' @ (Cx, Mx, pcx) # h = cs''a @ (Cxa, Mxa, pcxa) # ha \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cxa Mxa)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ((\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)})
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ((\<lambda>(Cx, Mx, pc', h, cs'', pcx). (_ (C, M, pc) # cs',\<lfloor>((Cx, Mx, pc') # h, True)\<rfloor> _)) ` {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)})
[PROOF STEP]
apply (rule finite_imageI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)}
[PROOF STEP]
apply (subgoal_tac "finite (
            (\<lambda>(l, pc'). (fst(((C, M, pc)#cs') ! l),
                         fst(snd(((C, M, pc)#cs') ! l)),
                         pc',
                         drop l cs',
                         take l ((C, M, pc)#cs'),
                         snd(snd(((C, M, pc)#cs') ! l))
                        )
            ) ` {(l, pc'). l < length ((C,M,pc)#cs') \<and>
                           pc' < length (instrs_of (P\<^bsub>wf\<^esub>) (fst(((C, M, pc)#cs') ! l))
                                                        (fst(snd(((C, M, pc)#cs') ! l))))})")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))})\<rbrakk> \<Longrightarrow> finite {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ((\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))})
[PROOF STEP]
apply (case_tac "((\<lambda>(l, pc').
             (fst (((C, M, pc) # cs') ! l),
              fst (snd (((C, M, pc) # cs') ! l)),
              pc',
              drop l cs',
              take l ((C, M, pc) # cs'),
              snd (snd (((C, M, pc) # cs') ! l))
             )) ` {(l, pc'). l < length ((C,M,pc)#cs') \<and>
                             pc' < length (instrs_of (P\<^bsub>wf\<^esub>) (fst (((C, M, pc) # cs') ! l))
                                                          (fst (snd (((C, M, pc) # cs') ! l))))})
             = {(Cx, Mx, pc', h, cs'', pcx).
                (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and>
                pc' < length (instrs_of (P\<^bsub>wf\<^esub>) Cx Mx)}")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))}); (\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))} = {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)}\<rbrakk> \<Longrightarrow> finite {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))}); (\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))} \<noteq> {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)}\<rbrakk> \<Longrightarrow> finite {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)}
 3. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ((\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))})
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))}); (\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))} \<noteq> {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)}\<rbrakk> \<Longrightarrow> finite {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ((\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))})
[PROOF STEP]
apply (erule notE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))})\<rbrakk> \<Longrightarrow> (\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))} = {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ((\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))})
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))})\<rbrakk> \<Longrightarrow> (\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))} \<subseteq> {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))})\<rbrakk> \<Longrightarrow> {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)} \<subseteq> (\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))}
 3. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ((\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))})
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ae ba. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>x. case x of (l, pc') \<Rightarrow> (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < Suc (length cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))}); ae < Suc (length cs'); ba < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! ae)) (fst (snd (((C, M, pc) # cs') ! ae))))\<rbrakk> \<Longrightarrow> (C, M, pc) # cs' = take ae ((C, M, pc) # cs') @ ((C, M, pc) # cs') ! ae # drop ae cs'
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))})\<rbrakk> \<Longrightarrow> {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)} \<subseteq> (\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))}
 3. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ((\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))})
[PROOF STEP]
apply (rule id_take_nth_drop [of _ "(C,M,pc)#cs'", simplified])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ae ba. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>x. case x of (l, pc') \<Rightarrow> (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < Suc (length cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))}); ae < Suc (length cs'); ba < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! ae)) (fst (snd (((C, M, pc) # cs') ! ae))))\<rbrakk> \<Longrightarrow> ae < Suc (length cs')
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))})\<rbrakk> \<Longrightarrow> {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)} \<subseteq> (\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))}
 3. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ((\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))})
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))})\<rbrakk> \<Longrightarrow> {(Cx, Mx, pc', h, cs'', pcx). (C, M, pc) # cs' = cs'' @ (Cx, Mx, pcx) # h \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> Cx Mx)} \<subseteq> (\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ((\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))})
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab ac ad b. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ ad @ (a, aa, b) # ac,x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>x. case x of (l, pc') \<Rightarrow> (fst ((ad @ (a, aa, b) # ac) ! l), fst (snd ((ad @ (a, aa, b) # ac) ! l)), pc', drop l cs', take l ad @ take (l - length ad) ((a, aa, b) # ac), snd (snd ((ad @ (a, aa, b) # ac) ! l)))) ` {(l, pc'). l < Suc (length cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst ((ad @ (a, aa, b) # ac) ! l)) (fst (snd ((ad @ (a, aa, b) # ac) ! l))))}); (C, M, pc) # cs' = ad @ (a, aa, b) # ac; ab < length (instrs_of P\<^bsub>wf\<^esub> a aa)\<rbrakk> \<Longrightarrow> (a, aa, ab, ac, ad, b) \<in> (\<lambda>x. case x of (l, pc') \<Rightarrow> (fst ((ad @ (a, aa, b) # ac) ! l), fst (snd ((ad @ (a, aa, b) # ac) ! l)), pc', drop l cs', take l ad @ take (l - length ad) ((a, aa, b) # ac), snd (snd ((ad @ (a, aa, b) # ac) ! l)))) ` {(l, pc'). l < Suc (length cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst ((ad @ (a, aa, b) # ac) ! l)) (fst (snd ((ad @ (a, aa, b) # ac) ! l))))}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ((\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))})
[PROOF STEP]
apply (rule_tac x="(length ad,ab)" in image_eqI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a aa ab ac ad b. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ ad @ (a, aa, b) # ac,x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>x. case x of (l, pc') \<Rightarrow> (fst ((ad @ (a, aa, b) # ac) ! l), fst (snd ((ad @ (a, aa, b) # ac) ! l)), pc', drop l cs', take l ad @ take (l - length ad) ((a, aa, b) # ac), snd (snd ((ad @ (a, aa, b) # ac) ! l)))) ` {(l, pc'). l < Suc (length cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst ((ad @ (a, aa, b) # ac) ! l)) (fst (snd ((ad @ (a, aa, b) # ac) ! l))))}); (C, M, pc) # cs' = ad @ (a, aa, b) # ac; ab < length (instrs_of P\<^bsub>wf\<^esub> a aa)\<rbrakk> \<Longrightarrow> (a, aa, ab, ac, ad, b) = (case (length ad, ab) of (l, pc') \<Rightarrow> (fst ((ad @ (a, aa, b) # ac) ! l), fst (snd ((ad @ (a, aa, b) # ac) ! l)), pc', drop l cs', take l ad @ take (l - length ad) ((a, aa, b) # ac), snd (snd ((ad @ (a, aa, b) # ac) ! l))))
 2. \<And>a aa ab ac ad b. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ ad @ (a, aa, b) # ac,x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>x. case x of (l, pc') \<Rightarrow> (fst ((ad @ (a, aa, b) # ac) ! l), fst (snd ((ad @ (a, aa, b) # ac) ! l)), pc', drop l cs', take l ad @ take (l - length ad) ((a, aa, b) # ac), snd (snd ((ad @ (a, aa, b) # ac) ! l)))) ` {(l, pc'). l < Suc (length cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst ((ad @ (a, aa, b) # ac) ! l)) (fst (snd ((ad @ (a, aa, b) # ac) ! l))))}); (C, M, pc) # cs' = ad @ (a, aa, b) # ac; ab < length (instrs_of P\<^bsub>wf\<^esub> a aa)\<rbrakk> \<Longrightarrow> (length ad, ab) \<in> {(l, pc'). l < Suc (length cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst ((ad @ (a, aa, b) # ac) ! l)) (fst (snd ((ad @ (a, aa, b) # ac) ! l))))}
 3. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ((\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))})
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a aa ab ac ad b. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ ad @ (a, aa, b) # ac,x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>x. case x of (l, pc') \<Rightarrow> (fst ((ad @ (a, aa, b) # ac) ! l), fst (snd ((ad @ (a, aa, b) # ac) ! l)), pc', drop l cs', take l ad @ take (l - length ad) ((a, aa, b) # ac), snd (snd ((ad @ (a, aa, b) # ac) ! l)))) ` {(l, pc'). l < Suc (length cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst ((ad @ (a, aa, b) # ac) ! l)) (fst (snd ((ad @ (a, aa, b) # ac) ! l))))}); (C, M, pc) # cs' = ad @ (a, aa, b) # ac; ab < length (instrs_of P\<^bsub>wf\<^esub> a aa)\<rbrakk> \<Longrightarrow> ac = drop (length ad) cs'
 2. \<And>a aa ab ac ad b. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ ad @ (a, aa, b) # ac,x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>x. case x of (l, pc') \<Rightarrow> (fst ((ad @ (a, aa, b) # ac) ! l), fst (snd ((ad @ (a, aa, b) # ac) ! l)), pc', drop l cs', take l ad @ take (l - length ad) ((a, aa, b) # ac), snd (snd ((ad @ (a, aa, b) # ac) ! l)))) ` {(l, pc'). l < Suc (length cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst ((ad @ (a, aa, b) # ac) ! l)) (fst (snd ((ad @ (a, aa, b) # ac) ! l))))}); (C, M, pc) # cs' = ad @ (a, aa, b) # ac; ab < length (instrs_of P\<^bsub>wf\<^esub> a aa)\<rbrakk> \<Longrightarrow> (length ad, ab) \<in> {(l, pc'). l < Suc (length cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst ((ad @ (a, aa, b) # ac) ! l)) (fst (snd ((ad @ (a, aa, b) # ac) ! l))))}
 3. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ((\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))})
[PROOF STEP]
apply (case_tac ad, clarsimp, clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab ac ad b. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ ad @ (a, aa, b) # ac,x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>x. case x of (l, pc') \<Rightarrow> (fst ((ad @ (a, aa, b) # ac) ! l), fst (snd ((ad @ (a, aa, b) # ac) ! l)), pc', drop l cs', take l ad @ take (l - length ad) ((a, aa, b) # ac), snd (snd ((ad @ (a, aa, b) # ac) ! l)))) ` {(l, pc'). l < Suc (length cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst ((ad @ (a, aa, b) # ac) ! l)) (fst (snd ((ad @ (a, aa, b) # ac) ! l))))}); (C, M, pc) # cs' = ad @ (a, aa, b) # ac; ab < length (instrs_of P\<^bsub>wf\<^esub> a aa)\<rbrakk> \<Longrightarrow> (length ad, ab) \<in> {(l, pc'). l < Suc (length cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst ((ad @ (a, aa, b) # ac) ! l)) (fst (snd ((ad @ (a, aa, b) # ac) ! l))))}
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ((\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))})
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab ac ad b. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ ad @ (a, aa, b) # ac,x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw; finite ((\<lambda>x. case x of (l, pc') \<Rightarrow> (fst ((ad @ (a, aa, b) # ac) ! l), fst (snd ((ad @ (a, aa, b) # ac) ! l)), pc', drop l cs', take l ad @ take (l - length ad) ((a, aa, b) # ac), snd (snd ((ad @ (a, aa, b) # ac) ! l)))) ` {(l, pc'). l < Suc (length cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst ((ad @ (a, aa, b) # ac) ! l)) (fst (snd ((ad @ (a, aa, b) # ac) ! l))))}); (C, M, pc) # cs' = ad @ (a, aa, b) # ac; ab < length (instrs_of P\<^bsub>wf\<^esub> a aa)\<rbrakk> \<Longrightarrow> length ad < Suc (length cs')
 2. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ((\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))})
[PROOF STEP]
apply (case_tac ad, clarsimp, clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite ((\<lambda>(l, pc'). (fst (((C, M, pc) # cs') ! l), fst (snd (((C, M, pc) # cs') ! l)), pc', drop l cs', take l ((C, M, pc) # cs'), snd (snd (((C, M, pc) # cs') ! l)))) ` {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))})
[PROOF STEP]
apply (rule finite_imageI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>JVM_CFG_Interpret.valid_node (P, C0, Main) (_ (C, M, pc) # cs',x _); instrs_of P\<^bsub>wf\<^esub> C M ! pc = Throw\<rbrakk> \<Longrightarrow> finite {(l, pc'). l < length ((C, M, pc) # cs') \<and> pc' < length (instrs_of P\<^bsub>wf\<^esub> (fst (((C, M, pc) # cs') ! l)) (fst (snd (((C, M, pc) # cs') ! l))))}
[PROOF STEP]
by (rule f_1)
[PROOF STATE]
proof (state)
this:
finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite {n'. \<exists>a'. valid_edge prog a' \<and> sourcenode a' = n \<and> targetnode a' = n'}

goal:
No subgoals!
[PROOF STEP]
qed