Theory JVMCFG

chapter ‹A Control Flow Graph for Jinja Byte Code›

section ‹Formalizing the CFG›

theory JVMCFG imports "../StaticInter/BasicDefs" Jinja.BVExample begin

declare lesub_list_impl_same_size [simp del]
declare nlistsE_length [simp del]

subsection ‹Type definitions›

subsubsection ‹Wellformed Programs›

definition "wf_jvmprog = {(P, Phi). wf_jvm_prog⇘Phi⇙ P}"

typedef wf_jvmprog = "wf_jvmprog"
proof
  show "(E, Phi) ∈ wf_jvmprog"
    unfolding wf_jvmprog_def by (auto intro: wf_prog)
qed

hide_const Phi E

abbreviation PROG :: "wf_jvmprog ⇒ jvm_prog"
  where "PROG P ≡ fst(Rep_wf_jvmprog(P))"

abbreviation TYPING :: "wf_jvmprog ⇒ ty⇩P"
  where "TYPING P ≡ snd(Rep_wf_jvmprog(P))"

lemma wf_jvmprog_is_wf_typ: "wf_jvm_prog⇘TYPING P⇙ (PROG P)"
using Rep_wf_jvmprog [of P]
  by (auto simp: wf_jvmprog_def split_beta)

lemma wf_jvmprog_is_wf: "wf_jvm_prog (PROG P)"
  using wf_jvmprog_is_wf_typ unfolding wf_jvm_prog_def
  by blast

subsubsection ‹Interprocedural CFG›

type_synonym jvm_method = "wf_jvmprog × cname × mname"
datatype var = Heap | Local "nat" | Stack "nat" | Exception
datatype val = Hp "heap" | Value "Value.val"

type_synonym state = "var ⇀ val"

definition valid_state :: "state ⇒ bool"
  where "valid_state s ≡ (∀val. s Heap ≠ Some (Value val))
  ∧ (s Exception = None ∨ (∃addr. s Exception = Some (Value (Addr addr))))
  ∧ (∀var. var ≠ Heap ∧ var ≠ Exception ⟶ (∀h. s var ≠ Some (Hp h)))"

fun the_Heap :: "val ⇒ heap"
  where "the_Heap (Hp h) = h"

fun the_Value :: "val ⇒ Value.val"
  where "the_Value (Value v) = v"

abbreviation heap_of :: "state ⇒ heap"
  where "heap_of s ≡ the_Heap (the (s Heap))"

abbreviation exc_flag :: "state ⇒ addr option"
  where "exc_flag s ≡ case (s Exception) of None ⇒ None
  | Some v ⇒ Some (THE a. v = Value (Addr a))"

abbreviation stkAt :: "state ⇒ nat ⇒ Value.val"
  where "stkAt s n ≡ the_Value (the (s (Stack n)))"

abbreviation locAt :: "state ⇒ nat ⇒ Value.val"
  where "locAt s n ≡ the_Value (the (s (Local n)))"

datatype nodeType = Enter | Normal | Return | Exceptional "pc option" "nodeType"
type_synonym cfg_node = "cname × mname × pc option × nodeType"

type_synonym
  cfg_edge = "cfg_node × (var, val, cname × mname × pc, cname × mname) edge_kind × cfg_node"

definition ClassMain :: "wf_jvmprog ⇒ cname"
  where "ClassMain P ≡ SOME Name. ¬ is_class (PROG P) Name"

definition MethodMain :: "wf_jvmprog ⇒ mname"
  where "MethodMain P ≡ SOME Name.
  ∀C D fs ms. class (PROG P) C = ⌊(D, fs, ms)⌋ ⟶ (∀m ∈ set ms. Name ≠ fst m)"

definition stkLength :: "jvm_method ⇒ pc ⇒ nat"
  where
  "stkLength m pc ≡ let (P, C, M) = m in (
  if (C = ClassMain P) then 1 else (
    length (fst(the(((TYPING P) C M) ! pc)))
  ))"

definition locLength :: "jvm_method ⇒ pc ⇒ nat"
  where
  "locLength m pc ≡ let (P, C, M) = m in (
  if (C = ClassMain P) then 1 else (
    length (snd(the(((TYPING P) C M) ! pc)))
  ))"

lemma ex_new_class_name: "∃C. ¬ is_class P C"
proof -
  have "¬ finite (UNIV :: cname set)"
    by (rule infinite_UNIV_listI)
  hence "∃C. C ∉ set (map fst P)"
    by -(rule ex_new_if_finite, auto)
  then obtain C where "C ∉ set (map fst P)"
    by blast
  have "¬ is_class P C"
  proof
    assume "is_class P C"
    then obtain D fs ms where "class P C = ⌊(D, fs, ms)⌋"
      by auto
    with ‹C ∉ set (map fst P)› show False
      by (auto dest: map_of_SomeD intro!: image_eqI simp: class_def)
  qed
  thus ?thesis
    by blast
qed

lemma ClassMain_unique_in_P:
  assumes "is_class (PROG P) C"
  shows "ClassMain P ≠ C"
proof -
  from ex_new_class_name [of "PROG P"] obtain D where "¬ is_class (PROG P) D"
    by blast
  with ‹is_class (PROG P) C› show ?thesis
    unfolding ClassMain_def
    by -(rule someI2, fastforce+)
qed

lemma map_of_fstD: "⟦ map_of xs a = ⌊b⌋; ∀x ∈ set xs. fst x ≠ a ⟧ ⟹ False"
  by (induct xs, auto)

lemma map_of_fstE: "⟦ map_of xs a = ⌊b⌋; ∃x ∈ set xs. fst x = a ⟹ thesis ⟧ ⟹ thesis"
  by (induct xs) (auto split: if_split_asm)

lemma ex_unique_method_name:
  "∃Name. ∀C D fs ms. class (PROG P) C = ⌊(D, fs, ms)⌋ ⟶ (∀m∈set ms. Name ≠ fst m)"
proof -
  from wf_jvmprog_is_wf [of P]
  have "distinct_fst (PROG P)"
    by (simp add: wf_jvm_prog_def wf_jvm_prog_phi_def wf_prog_def)
  hence "{C. ∃D fs ms. class (PROG P) C = ⌊(D, fs, ms)⌋} = fst ` set (PROG P)"
    by (fastforce elim: map_of_fstE simp: class_def intro: map_of_SomeI)
  hence "finite {C. ∃D fs ms. class (PROG P) C = ⌊(D, fs, ms)⌋}"
    by auto
  moreover have "{ms. ∃C D fs. class (PROG P) C = ⌊(D, fs, ms)⌋}
    = snd ` snd ` the ` (λC. class (PROG P) C) ` {C. ∃D fs ms. class (PROG P) C = ⌊(D, fs, ms)⌋}"
    by (fastforce intro: rev_image_eqI map_of_SomeI simp: class_def)
  ultimately have "finite {ms. ∃C D fs. class (PROG P) C = ⌊(D, fs, ms)⌋}"
    by auto
  moreover have "¬ finite (UNIV :: mname set)"
    by (rule infinite_UNIV_listI)
  ultimately
  have "∃Name. Name ∉ fst ` (⋃ms ∈ {ms. ∃C D fs. class (PROG P) C = ⌊(D, fs, ms)⌋}. set ms)"
    by -(rule ex_new_if_finite, auto)
  thus ?thesis
    by fastforce
qed

lemma MethodMain_unique_in_P:
  assumes "PROG P ⊢ D sees M:Ts→T = mb in C"
  shows "MethodMain P ≠ M"
proof -
  from ex_unique_method_name [of P] obtain M'
    where "⋀C D fs ms. class (PROG P) C = ⌊(D, fs, ms)⌋ ⟹ (∀m ∈ set ms. M' ≠ fst m)"
    by blast
  with ‹PROG P ⊢ D sees M:Ts→T = mb in C›
  show ?thesis
    unfolding MethodMain_def
    by -(rule someI2_ex, fastforce, fastforce dest!: visible_method_exists elim: map_of_fstE)
qed

lemma ClassMain_is_no_class [dest!]: "is_class (PROG P) (ClassMain P) ⟹ False"
proof (erule rev_notE)
  from ex_new_class_name [of "PROG P"] obtain C where "¬ is_class (PROG P) C"
    by blast
  thus "¬ is_class (PROG P) (ClassMain P)" unfolding ClassMain_def
    by (rule someI)
qed

lemma MethodMain_not_seen [dest!]: "PROG P ⊢ C sees (MethodMain P):Ts→T = mb in D ⟹ False"
  by (fastforce dest: MethodMain_unique_in_P)

lemma no_Call_from_ClassMain [dest!]: "PROG P ⊢ ClassMain P sees M:Ts→T = mb in C ⟹ False"
  by (fastforce dest: sees_method_is_class)

lemma no_Call_in_ClassMain [dest!]: "PROG P ⊢ C sees M:Ts→T = mb in ClassMain P ⟹ False"
  by (fastforce dest: sees_method_idemp)

inductive JVMCFG :: "jvm_method ⇒ cfg_node ⇒ (var, val, cname × mname × pc, cname × mname) edge_kind ⇒ cfg_node ⇒ bool" (‹ _ ⊢ _ -_→ _›)
  and reachable :: "jvm_method ⇒ cfg_node ⇒ bool" (‹ _ ⊢ ⇒_›)
  where
    Entry_reachable: "(P, C0, Main) ⊢ ⇒(ClassMain P, MethodMain P, None, Enter)"
  | reachable_step: "⟦ P ⊢ ⇒n; P ⊢ n -(e)→ n' ⟧ ⟹ P ⊢ ⇒n'"
  | Main_to_Call: "(P, C0, Main) ⊢ ⇒(ClassMain P, MethodMain P, ⌊0⌋, Enter)
  ⟹ (P, C0, Main) ⊢ (ClassMain P, MethodMain P, ⌊0⌋, Enter) -⇑id→ (ClassMain P, MethodMain P, ⌊0⌋, Normal)"
  | Main_Call_LFalse: "(P, C0, Main) ⊢ ⇒(ClassMain P, MethodMain P, ⌊0⌋, Normal)
  ⟹ (P, C0, Main) ⊢ (ClassMain P, MethodMain P, ⌊0⌋, Normal) -(λs. False)⇩√→ (ClassMain P, MethodMain P, ⌊0⌋, Return)"
  | Main_Call: "⟦ (P, C0, Main) ⊢ ⇒(ClassMain P, MethodMain P, ⌊0⌋, Normal);
     PROG P ⊢ C0 sees Main:[]→T = (mxs, mxl⇩0, is, xt) in D;
     initParams = [(λs. s Heap),(λs. ⌊Value Null⌋)];
     ek = (λ(s, ret). True):(ClassMain P, MethodMain P, 0)↪⇘(D, Main)⇙initParams ⟧
  ⟹ (P, C0, Main) ⊢ (ClassMain P, MethodMain P, ⌊0⌋, Normal) -(ek)→ (D, Main, None, Enter)"
  | Main_Return_to_Exit: "(P, C0, Main) ⊢ ⇒(ClassMain P, MethodMain P, ⌊0⌋, Return)
  ⟹ (P, C0, Main) ⊢ (ClassMain P, MethodMain P, ⌊0⌋, Return) -(⇑id)→ (ClassMain P, MethodMain P, None, Return)"
  | Method_LFalse: "(P, C0, Main) ⊢ ⇒(C, M, None, Enter)
  ⟹ (P, C0, Main) ⊢ (C, M, None, Enter) -(λs. False)⇩√→ (C, M, None, Return)"
  | Method_LTrue: "(P, C0, Main) ⊢ ⇒(C, M, None, Enter)
  ⟹ (P, C0, Main) ⊢ (C, M, None, Enter) -(λs. True)⇩√→ (C, M, ⌊0⌋, Enter)"
  | CFG_Load: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter); instrs_of (PROG P) C M ! pc = Load n;
    ek = ⇑(λs. s(Stack (stkLength (P, C, M) pc) := s (Local n))) ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Enter) -(ek)→ (C, M, ⌊Suc pc⌋, Enter)"
  | CFG_Store: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter); instrs_of (PROG P) C M ! pc = Store n;
    ek = ⇑(λs. s(Local n := s (Stack (stkLength (P, C, M) pc - 1)))) ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Enter) -(ek)→ (C, M, ⌊Suc pc⌋, Enter)"
  | CFG_Push: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter); instrs_of (PROG P) C M ! pc = Push v;
    ek = ⇑(λs. s(Stack (stkLength (P, C, M) pc) ↦ Value v)) ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Enter) -(ek)→ (C, M, ⌊Suc pc⌋, Enter)"
  | CFG_Pop: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter); instrs_of (PROG P) C M ! pc = Pop;
    ek = ⇑id ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Enter) -(ek)→ (C, M, ⌊Suc pc⌋, Enter)"
  | CFG_IAdd: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter); instrs_of (PROG P) C M ! pc = IAdd;
    ek = ⇑(λs. let i1 = the_Intg (stkAt s (stkLength (P, C, M) pc - 1));
                   i2 = the_Intg (stkAt s (stkLength (P, C, M) pc - 2))
                in s(Stack (stkLength (P, C, M) pc - 2) ↦ Value (Intg (i1 + i2)))) ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Enter) -(ek)→ (C, M, ⌊Suc pc⌋, Enter)"
  | CFG_Goto: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter); instrs_of (PROG P) C M ! pc = Goto i ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Enter) -((λs. True)⇩√)→ (C, M, ⌊nat (int pc + i)⌋, Enter)"
  | CFG_CmpEq: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter); instrs_of (PROG P) C M ! pc = CmpEq;
    ek = ⇑(λs. let e1 = stkAt s (stkLength (P, C, M) pc - 1);
                   e2 = stkAt s (stkLength (P, C, M) pc - 2)
                in s(Stack (stkLength (P, C, M) pc - 2) ↦ Value (Bool (e1 = e2)))) ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Enter) -(ek)→ (C, M, ⌊Suc pc⌋, Enter)"
  | CFG_IfFalse_False: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter);
    instrs_of (PROG P) C M ! pc = IfFalse i;
    i ≠ 1;
    ek = (λs. stkAt s (stkLength(P, C, M) pc - 1) = Bool False)⇩√ ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Enter) -(ek)→ (C, M, ⌊nat (int pc + i)⌋, Enter)"
  | CFG_IfFalse_True: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter);
    instrs_of (PROG P) C M ! pc = IfFalse i;
    ek = (λs. stkAt s (stkLength(P, C, M) pc - 1) ≠ Bool False ∨ i = 1)⇩√ ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Enter) -(ek)→ (C, M, ⌊Suc pc⌋, Enter)"
  | CFG_New_Check_Normal: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter);
    instrs_of (PROG P) C M ! pc = New Cl;
    ek = (λs. new_Addr (heap_of s) ≠ None)⇩√ ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Enter) -(ek)→ (C, M, ⌊pc⌋, Normal)"
  | CFG_New_Check_Exceptional: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter);
    instrs_of (PROG P) C M ! pc = New Cl;
    pc' = (case (match_ex_table (PROG P) OutOfMemory pc (ex_table_of (PROG P) C M)) of
             None ⇒ None
           | Some (pc'', d) ⇒ ⌊pc''⌋);
    ek = (λs. new_Addr (heap_of s) = None)⇩√ ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Enter) -(ek)→ (C, M, ⌊pc⌋, Exceptional pc' Enter)"
  | CFG_New_Update: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Normal);
    instrs_of (PROG P) C M ! pc = New Cl;
    ek = ⇑(λs. let a = the (new_Addr (heap_of s))
                in s(Heap ↦ Hp ((heap_of s)(a ↦ blank (PROG P) Cl)),
                    Stack (stkLength(P, C, M) pc) ↦ Value (Addr a))) ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Normal) -(ek)→ (C, M, ⌊Suc pc⌋, Enter)"
  | CFG_New_Exceptional_prop: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional None Enter);
    instrs_of (PROG P) C M ! pc = New Cl;
    ek = ⇑(λs. s(Exception ↦ Value (Addr (addr_of_sys_xcpt OutOfMemory)))) ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Exceptional None Enter) -(ek)→ (C, M, None, Return)"
  | CFG_New_Exceptional_handle: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter);
    instrs_of (PROG P) C M ! pc = New Cl;
    ek = ⇑(λs. (s(Exception := None))
                (Stack (stkLength (P, C, M) pc' - 1) ↦ Value (Addr (addr_of_sys_xcpt OutOfMemory)))) ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter) -(ek)→ (C, M, ⌊pc'⌋, Enter)"
  | CFG_Getfield_Check_Normal: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter);
    instrs_of (PROG P) C M ! pc = Getfield F Cl;
    ek = (λs. stkAt s (stkLength (P, C, M) pc - 1) ≠ Null)⇩√ ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Enter) -(ek)→ (C, M, ⌊pc⌋, Normal)"
  | CFG_Getfield_Check_Exceptional: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter);
    instrs_of (PROG P) C M ! pc = Getfield F Cl;
    pc' = (case (match_ex_table (PROG P) NullPointer pc (ex_table_of (PROG P) C M)) of
             None ⇒ None
           | Some (pc'', d) ⇒ ⌊pc''⌋);
    ek = (λs. stkAt s (stkLength (P, C, M) pc - 1) = Null)⇩√ ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Enter) -(ek)→ (C, M, ⌊pc⌋, Exceptional pc' Enter)"
  | CFG_Getfield_Update: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Normal);
    instrs_of (PROG P) C M ! pc = Getfield F Cl;
    ek = ⇑(λs. let (D, fs) = the (heap_of s (the_Addr (stkAt s (stkLength (P, C, M) pc - 1))))
                 in s(Stack (stkLength(P, C, M) pc - 1) ↦ Value (the (fs (F, Cl))))) ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Normal) -(ek)→ (C, M, ⌊Suc pc⌋, Enter)"
  | CFG_Getfield_Exceptional_prop: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional None Enter);
    instrs_of (PROG P) C M ! pc = Getfield F Cl;
    ek = ⇑(λs. s(Exception ↦ Value (Addr (addr_of_sys_xcpt NullPointer)))) ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Exceptional None Enter) -(ek)→ (C, M, None, Return)"
  | CFG_Getfield_Exceptional_handle: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter);
    instrs_of (PROG P) C M ! pc = Getfield F Cl;
    ek = ⇑(λs. (s(Exception := None))
                (Stack (stkLength (P, C, M) pc' - 1) ↦ Value (Addr (addr_of_sys_xcpt NullPointer)))) ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter) -(ek)→ (C, M, ⌊pc'⌋, Enter)"
  | CFG_Putfield_Check_Normal: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter);
    instrs_of (PROG P) C M ! pc = Putfield F Cl;
    ek = (λs. stkAt s (stkLength (P, C, M) pc - 2) ≠ Null)⇩√ ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Enter) -(ek)→ (C, M, ⌊pc⌋, Normal)"
  | CFG_Putfield_Check_Exceptional: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter);
    instrs_of (PROG P) C M ! pc = Putfield F Cl;
    pc' = (case (match_ex_table (PROG P) NullPointer pc (ex_table_of (PROG P) C M)) of
             None ⇒ None
           | Some (pc'', d) ⇒ ⌊pc''⌋);
    ek = (λs. stkAt s (stkLength (P, C, M) pc - 2) = Null)⇩√ ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Enter) -(ek)→ (C, M, ⌊pc⌋, Exceptional pc' Enter)"
  | CFG_Putfield_Update: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Normal);
    instrs_of (PROG P) C M ! pc = Putfield F Cl;
    ek = ⇑(λs. let v = stkAt s (stkLength (P, C, M) pc - 1);
                   r = stkAt s (stkLength (P, C, M) pc - 2);
                   a = the_Addr r;
                   (D, fs) = the (heap_of s a);
                   h' = (heap_of s)(a ↦ (D, fs((F, Cl) ↦ v)))
                 in s(Heap ↦ Hp h')) ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Normal) -(ek)→ (C, M, ⌊Suc pc⌋, Enter)"
  | CFG_Putfield_Exceptional_prop: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional None Enter);
    instrs_of (PROG P) C M ! pc = Putfield F Cl;
    ek = ⇑(λs. s(Exception ↦ Value (Addr (addr_of_sys_xcpt NullPointer)))) ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Exceptional None Enter) -(ek)→ (C, M, None, Return)"
  | CFG_Putfield_Exceptional_handle: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter);
    instrs_of (PROG P) C M ! pc = Putfield F Cl;
    ek = ⇑(λs. (s(Exception := None))
                (Stack (stkLength (P, C, M) pc' - 1) ↦ Value (Addr (addr_of_sys_xcpt NullPointer)))) ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter) -(ek)→ (C, M, ⌊pc'⌋, Enter)"
  | CFG_Checkcast_Check_Normal: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter);
    instrs_of (PROG P) C M ! pc = Checkcast Cl;
    ek = (λs. cast_ok (PROG P) Cl (heap_of s) (stkAt s (stkLength (P, C, M) pc - 1)))⇩√ ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Enter) -(ek)→ (C, M, ⌊Suc pc⌋, Enter)"
  | CFG_Checkcast_Check_Exceptional: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter);
    instrs_of (PROG P) C M ! pc = Checkcast Cl;
    pc' = (case (match_ex_table (PROG P) ClassCast pc (ex_table_of (PROG P) C M)) of
             None ⇒ None
           | Some (pc'', d) ⇒ ⌊pc''⌋);
    ek = (λs. ¬ cast_ok (PROG P) Cl (heap_of s) (stkAt s (stkLength (P, C, M) pc - 1)))⇩√ ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Enter) -(ek)→ (C, M, ⌊pc⌋, Exceptional pc' Enter)"
  | CFG_Checkcast_Exceptional_prop: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional None Enter);
    instrs_of (PROG P) C M ! pc = Checkcast Cl;
    ek = ⇑(λs. s(Exception ↦ Value (Addr (addr_of_sys_xcpt ClassCast)))) ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Exceptional None Enter) -(ek)→ (C, M, None, Return)"
  | CFG_Checkcast_Exceptional_handle: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter);
    instrs_of (PROG P) C M ! pc = Checkcast Cl;
    ek = ⇑(λs. (s(Exception := None))
                (Stack (stkLength (P, C, M) pc' - 1) ↦ Value (Addr (addr_of_sys_xcpt ClassCast)))) ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter) -(ek)→ (C, M, ⌊pc'⌋, Enter)"
  | CFG_Throw_Check: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter);
    instrs_of (PROG P) C M ! pc = Throw;
    pc' = None ∨ match_ex_table (PROG P) Exc pc (ex_table_of (PROG P) C M) = ⌊(the pc', d)⌋;
    ek = (λs. let v = stkAt s (stkLength (P, C, M) pc - 1);
                  Cl = if (v = Null) then NullPointer else (cname_of (heap_of s) (the_Addr v))
               in case pc' of
                  None ⇒ match_ex_table (PROG P) Cl pc (ex_table_of (PROG P) C M) = None
                | Some pc'' ⇒ ∃d. match_ex_table (PROG P) Cl pc (ex_table_of (PROG P) C M)
                                  = ⌊(pc'', d)⌋
    )⇩√ ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Enter) -(ek)→ (C, M, ⌊pc⌋, Exceptional pc' Enter)"

  | CFG_Throw_prop: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional None Enter);
    instrs_of (PROG P) C M ! pc = Throw;
    ek = ⇑(λs. s(Exception ↦ Value (stkAt s (stkLength (P, C, M) pc - 1)))) ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Exceptional None Enter) -(ek)→ (C, M, None, Return)"
  | CFG_Throw_handle: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter);
    pc' ≠ length (instrs_of (PROG P) C M);
    instrs_of (PROG P) C M ! pc = Throw;
    ek = ⇑(λs. (s(Exception := None))
                (Stack (stkLength (P, C, M) pc' - 1) ↦ Value (stkAt s (stkLength (P, C, M) pc - 1)))) ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter) -(ek)→ (C, M, ⌊pc'⌋, Enter)"
  | CFG_Invoke_Check_NP_Normal: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter);
    instrs_of (PROG P) C M ! pc = Invoke M' n;
    ek = (λs. stkAt s (stkLength (P, C, M) pc - Suc n) ≠ Null)⇩√ ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Enter) -(ek)→ (C, M, ⌊pc⌋, Normal)"
  | CFG_Invoke_Check_NP_Exceptional: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter);
    instrs_of (PROG P) C M ! pc = Invoke M' n;
    pc' = (case (match_ex_table (PROG P) NullPointer pc (ex_table_of (PROG P) C M)) of
             None ⇒ None
           | Some (pc'', d) ⇒ ⌊pc''⌋);
    ek = (λs. stkAt s (stkLength (P, C, M) pc - Suc n) = Null)⇩√ ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Enter) -(ek)→ (C, M, ⌊pc⌋, Exceptional pc' Enter)"
  | CFG_Invoke_NP_prop: "⟦ C ≠ ClassMain P;
    (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional None Enter);
    instrs_of (PROG P) C M ! pc = Invoke M' n;
    ek = ⇑(λs. s(Exception ↦ Value (Addr (addr_of_sys_xcpt NullPointer)))) ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Exceptional None Enter) -(ek)→ (C, M, None, Return)"
  | CFG_Invoke_NP_handle: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter);
    instrs_of (PROG P) C M ! pc = Invoke M' n;
    ek = ⇑(λs. (s(Exception := None))
                (Stack (stkLength (P, C, M) pc' - 1) ↦ Value (Addr (addr_of_sys_xcpt NullPointer)))) ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter) -(ek)→ (C, M, ⌊pc'⌋, Enter)"
  | CFG_Invoke_Call: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Normal);
    instrs_of (PROG P) C M ! pc = Invoke M' n;
    TYPING P C M ! pc = ⌊(ST, LT)⌋;
    ST ! n = Class D';
    PROG P ⊢ D' sees M':Ts→T = (mxs, mxl⇩0, is, xt) in D;
    Q = (λ(s, ret). let r = stkAt s (stkLength (P, C, M) pc - Suc n);
                        C' = fst (the (heap_of s (the_Addr r)))
                     in D = fst (method (PROG P) C' M'));
    paramDefs = (λs. s Heap)
                # (λs. s (Stack (stkLength (P, C, M) pc - Suc n)))
                # (rev (map (λi. (λs. s (Stack (stkLength (P, C, M) pc - Suc i)))) [0..<n]));
    ek = Q:(C, M, pc)↪⇘(D,M')⇙paramDefs
  ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Normal) -(ek)→ (D, M', None, Enter)"
  | CFG_Invoke_False: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Normal);
    instrs_of (PROG P) C M ! pc = Invoke M' n;
    ek = (λs. False)⇩√
  ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Normal) -(ek)→ (C, M, ⌊pc⌋, Return)"
  | CFG_Invoke_Return_Check_Normal: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Return);
    instrs_of (PROG P) C M ! pc = Invoke M' n;
    (TYPING P) C M ! pc = ⌊(ST, LT)⌋;
    ST ! n ≠ NT;
    ek = (λs. s Exception = None)⇩√
  ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Return) -(ek)→ (C, M, ⌊Suc pc⌋, Enter)"
  | CFG_Invoke_Return_Check_Exceptional: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Return);
    instrs_of (PROG P) C M ! pc = Invoke M' n;
    match_ex_table (PROG P) Exc pc (ex_table_of (PROG P) C M) = ⌊(pc', diff)⌋;
    pc' ≠ length (instrs_of (PROG P) C M);
    ek = (λs. ∃v d. s Exception = ⌊v⌋ ∧
                  match_ex_table (PROG P) (cname_of (heap_of s) (the_Addr (the_Value v))) pc (ex_table_of (PROG P) C M) = ⌊(pc', d)⌋)⇩√
  ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Return) -(ek)→ (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Return)"
  | CFG_Invoke_Return_Exceptional_handle: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Return);
    instrs_of (PROG P) C M ! pc = Invoke M' n;
    ek = ⇑(λs. s(Exception := None,
                 Stack (stkLength (P, C, M) pc' - 1) := s Exception)) ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Return) -(ek)→ (C, M, ⌊pc'⌋, Enter)"
  | CFG_Invoke_Return_Exceptional_prop: "⟦ C ≠ ClassMain P;
    (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Return);
    instrs_of (PROG P) C M ! pc = Invoke M' n;
    ek = (λs. ∃v. s Exception = ⌊v⌋ ∧
              match_ex_table (PROG P) (cname_of (heap_of s) (the_Addr (the_Value v))) pc (ex_table_of (PROG P) C M) = None)⇩√ ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Return) -(ek)→ (C, M, None, Return)"
  | CFG_Return: "⟦ C ≠ ClassMain P; (P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter);
    instrs_of (PROG P) C M ! pc = instr.Return;
    ek = ⇑(λs. s(Stack 0 := s (Stack (stkLength (P, C, M) pc - 1))))
  ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, ⌊pc⌋, Enter) -(ek)→ (C, M, None, Return)"
  | CFG_Return_from_Method: "⟦ (P, C0, Main) ⊢ ⇒(C, M, None, Return);
    (P, C0, Main) ⊢ (C', M', ⌊pc'⌋, Normal) -(Q':(C', M', pc')↪⇘(C,M)⇙ps)→ (C, M, None, Enter);
    Q = (λ(s, ret). ret = (C', M', pc'));
    stateUpdate = (λs s'. s'(Heap := s Heap,
                            Exception := s Exception,
                            Stack (stkLength (P, C', M') (Suc pc') - 1) := s (Stack 0))
                  );
    ek = Q↩⇘(C, M)⇙stateUpdate
  ⟧
  ⟹ (P, C0, Main) ⊢ (C, M, None, Return) -(ek)→ (C', M', ⌊pc'⌋, Return)"


(* This takes veeeery long *)
lemma JVMCFG_edge_det: "⟦ P ⊢ n -(et)→ n'; P ⊢ n -(et')→ n' ⟧ ⟹ et = et'"
  by (erule JVMCFG.cases) (erule JVMCFG.cases, (fastforce dest: sees_method_fun)+)+

lemma sourcenode_reachable: "P ⊢ n -(ek)→ n' ⟹ P ⊢ ⇒n"
  by (erule JVMCFG.cases, auto)

lemma targetnode_reachable:
  assumes edge: "P ⊢ n -(ek)→ n'"
  shows "P ⊢ ⇒n'"
proof -
  from edge have "P ⊢ ⇒n"
    by -(drule sourcenode_reachable)
  with edge show ?thesis
    by -(rule JVMCFG_reachable.intros)
qed

lemmas JVMCFG_reachable_inducts = JVMCFG_reachable.inducts[split_format (complete)]

lemma ClassMain_imp_MethodMain:
  "(P, C0, Main) ⊢ (C', M', pc', nt') -ek→ (ClassMain P, M, pc, nt) ⟹ M = MethodMain P"
  "(P, C0, Main) ⊢ ⇒(ClassMain P, M, pc, nt) ⟹ M = MethodMain P"
proof (induct P=="P" C0≡"C0" Main≡Main C' M' pc' nt' ek C''=="ClassMain P" M pc nt and
              P=="P" C0≡"C0" Main≡Main C'=="ClassMain P" M pc nt
       rule: JVMCFG_reachable_inducts)
  case CFG_Return_from_Method
  thus ?case
    by (fastforce elim: JVMCFG.cases)
qed auto

lemma ClassMain_no_Call_target [dest!]:
  "(P, C0, Main) ⊢ (C, M, pc, nt) -Q:(C', M', pc')↪⇘(D,M'')⇙paramDefs→ (ClassMain P, M''', pc'', nt')
  ⟹ False"
  and
  "(P, C0, Main) ⊢ ⇒(C, M, pc, nt) ⟹ True"
  by (induct  P C0 Main C M pc nt ek=="Q:(C', M', pc')↪⇘(D,M'')⇙paramDefs"
                         C''=="ClassMain P" M''' pc'' nt' and
               P C0 Main C M pc nt
    rule: JVMCFG_reachable_inducts) auto

lemma method_of_src_and_trg_exists:
  "⟦ (P, C0, Main) ⊢ (C', M', pc', nt') -ek→ (C, M, pc, nt); C ≠ ClassMain P; C' ≠ ClassMain P ⟧
  ⟹ (∃Ts T mb. (PROG P) ⊢ C sees M:Ts→T = mb in C) ∧
     (∃Ts T mb. (PROG P) ⊢ C' sees M':Ts→T = mb in C')"
  and method_of_reachable_node_exists:
  "⟦ (P, C0, Main) ⊢ ⇒(C, M, pc, nt); C ≠ ClassMain P ⟧
  ⟹ ∃Ts T mb. (PROG P) ⊢ C sees M:Ts→T = mb in C"
proof (induct rule: JVMCFG_reachable_inducts)
  case CFG_Invoke_Call
  thus ?case
    by (blast dest: sees_method_idemp)
next
  case (reachable_step P C0 Main C M pc nt ek C' M' pc' nt')
  show ?case
  proof (cases "C = ClassMain P")
    case True
    with ‹(P, C0, Main) ⊢ (C, M, pc, nt) -ek→ (C', M', pc', nt')› ‹C' ≠ ClassMain P›
    show ?thesis
    proof cases
      case Main_Call
      thus ?thesis
        by (blast dest: sees_method_idemp)
    qed auto
  next
    case False
    with reachable_step show ?thesis
      by simp
  qed
qed simp_all

lemma "⟦ (P, C0, Main) ⊢ (C', M', pc', nt') -ek→ (C, M, pc, nt); C ≠ ClassMain P; C' ≠ ClassMain P ⟧
  ⟹ (case pc of None ⇒ True |
    ⌊pc''⌋ ⇒ (TYPING P) C M ! pc'' ≠ None ∧ pc'' < length (instrs_of (PROG P) C M)) ∧
  (case pc' of None ⇒ True |
    ⌊pc''⌋ ⇒ (TYPING P) C' M' ! pc'' ≠ None ∧ pc'' < length (instrs_of (PROG P) C' M'))"
  and instr_of_reachable_node_typable: "⟦ (P, C0, Main) ⊢ ⇒(C, M, pc, nt); C ≠ ClassMain P ⟧
  ⟹ case pc of None ⇒ True |
  ⌊pc''⌋ ⇒ (TYPING P) C M ! pc'' ≠ None ∧ pc'' < length (instrs_of (PROG P) C M)"
proof (induct rule: JVMCFG_reachable_inducts)
  case (CFG_Load C P C0 Main M pc n ek)
  from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter)› ‹C ≠ ClassMain P›
  obtain Ts T mxs mxl⇩0 "is" xt where "PROG P ⊢ C sees M:Ts→T = (mxs, mxl⇩0, is, xt) in C"
    and "instrs_of (PROG P) C M = is"
    by -(drule method_of_reachable_node_exists, auto)
  with CFG_Load show ?case
    by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
  case (CFG_Store C P C0 Main M pc n ek)
  from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter)› ‹C ≠ ClassMain P›
  obtain Ts T mxs mxl⇩0 "is" xt where "PROG P ⊢ C sees M:Ts→T = (mxs, mxl⇩0, is, xt) in C"
    and "instrs_of (PROG P) C M = is"
    by -(drule method_of_reachable_node_exists, auto)
  with CFG_Store show ?case
    by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
  case (CFG_Push C P C0 Main M pc v ek)
  from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter)› ‹C ≠ ClassMain P›
  obtain Ts T mxs mxl⇩0 "is" xt where "PROG P ⊢ C sees M:Ts→T = (mxs, mxl⇩0, is, xt) in C"
    and "instrs_of (PROG P) C M = is"
    by -(drule method_of_reachable_node_exists, auto)
  with CFG_Push show ?case
    by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
  case (CFG_Pop C P C0 Main M pc ek)
  from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter)› ‹C ≠ ClassMain P›
  obtain Ts T mxs mxl⇩0 "is" xt where "PROG P ⊢ C sees M:Ts→T = (mxs, mxl⇩0, is, xt) in C"
    and "instrs_of (PROG P) C M = is"
    by -(drule method_of_reachable_node_exists, auto)
  with CFG_Pop show ?case
    by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
  case (CFG_IAdd C P C0 Main M pc ek)
  from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter)› ‹C ≠ ClassMain P›
  obtain Ts T mxs mxl⇩0 "is" xt where "PROG P ⊢ C sees M:Ts→T = (mxs, mxl⇩0, is, xt) in C"
    and "instrs_of (PROG P) C M = is"
    by -(drule method_of_reachable_node_exists, auto)
  with CFG_IAdd show ?case
    by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
  case (CFG_Goto C P C0 Main M pc i)
  from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter)› ‹C ≠ ClassMain P›
  obtain Ts T mxs mxl⇩0 "is" xt where "PROG P ⊢ C sees M:Ts→T = (mxs, mxl⇩0, is, xt) in C"
    and "instrs_of (PROG P) C M = is"
    by -(drule method_of_reachable_node_exists, auto)
  with CFG_Goto show ?case
    by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
  case (CFG_CmpEq C P C0 Main M pc ek)
  from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter)› ‹C ≠ ClassMain P›
  obtain Ts T mxs mxl⇩0 "is" xt where "PROG P ⊢ C sees M:Ts→T = (mxs, mxl⇩0, is, xt) in C"
    and "instrs_of (PROG P) C M = is"
    by -(drule method_of_reachable_node_exists, auto)
  with CFG_CmpEq show ?case
    by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
  case (CFG_IfFalse_False C P C0 Main M pc i ek)
  from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter)› ‹C ≠ ClassMain P›
  obtain Ts T mxs mxl⇩0 "is" xt where "PROG P ⊢ C sees M:Ts→T = (mxs, mxl⇩0, is, xt) in C"
    and "instrs_of (PROG P) C M = is"
    by -(drule method_of_reachable_node_exists, auto)
  with CFG_IfFalse_False show ?case
    by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
  case (CFG_IfFalse_True C P C0 Main M pc i ek)
  from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter)› ‹C ≠ ClassMain P›
  obtain Ts T mxs mxl⇩0 "is" xt where "PROG P ⊢ C sees M:Ts→T = (mxs, mxl⇩0, is, xt) in C"
    and "instrs_of (PROG P) C M = is"
    by -(drule method_of_reachable_node_exists, auto)
  with CFG_IfFalse_True show ?case
    using [[simproc del: list_to_set_comprehension]] by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
  case (CFG_New_Update C P C0 Main M pc Cl ek)
  from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Normal)› ‹C ≠ ClassMain P›
  obtain Ts T mxs mxl⇩0 "is" xt where "PROG P ⊢ C sees M:Ts→T = (mxs, mxl⇩0, is, xt) in C"
    and "instrs_of (PROG P) C M = is"
    by -(drule method_of_reachable_node_exists, auto)
  with CFG_New_Update show ?case
    by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
  case (CFG_New_Exceptional_handle C P C0 Main M pc pc' Cl ek)
  hence "TYPING P C M ! pc ≠ None" and "pc < length (instrs_of (PROG P) C M)"
    by simp_all
  moreover from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)› ‹C ≠ ClassMain P›
  obtain Ts T mxs mxl⇩0 where
    "PROG P ⊢ C sees M:Ts→T = (mxs, mxl⇩0, instrs_of (PROG P) C M, ex_table_of (PROG P) C M) in C"
    by (fastforce dest: method_of_reachable_node_exists)
  with ‹pc < length (instrs_of (PROG P) C M)› ‹instrs_of (PROG P) C M ! pc = New Cl›
  have "PROG P,T,mxs,length (instrs_of (PROG P) C M),ex_table_of (PROG P) C M
    ⊢ New Cl,pc :: TYPING P C M"
    by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
  moreover from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)› ‹C ≠ ClassMain P›
    ‹instrs_of (PROG P) C M ! pc = New Cl› obtain d'
    where "match_ex_table (PROG P) OutOfMemory pc (ex_table_of (PROG P) C M) = ⌊(pc', d')⌋"
    by cases (fastforce elim: JVMCFG.cases)
  hence "∃(f, t, D, h, d)∈set (ex_table_of (PROG P) C M).
    matches_ex_entry (PROG P) OutOfMemory pc (f, t, D, h, d) ∧ h = pc' ∧ d = d'"
    by -(drule match_ex_table_SomeD)
  ultimately show ?case using ‹instrs_of (PROG P) C M ! pc = New Cl›
    by (fastforce simp: relevant_entries_def is_relevant_entry_def matches_ex_entry_def)
next
  case (CFG_Getfield_Update C P C0 Main M pc F Cl ek)
  from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Normal)› ‹C ≠ ClassMain P›
  obtain Ts T mxs mxl⇩0 "is" xt where "PROG P ⊢ C sees M:Ts→T = (mxs, mxl⇩0, is, xt) in C"
    and "instrs_of (PROG P) C M = is"
    by -(drule method_of_reachable_node_exists, auto)
  with CFG_Getfield_Update show ?case
    by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
  case (CFG_Getfield_Exceptional_handle C P C0 Main M pc pc' F Cl ek)
  hence "TYPING P C M ! pc ≠ None" and "pc < length (instrs_of (PROG P) C M)"
    by simp_all
  moreover from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)› ‹C ≠ ClassMain P›
  obtain Ts T mxs mxl⇩0 where
    "PROG P ⊢ C sees M:Ts→T = (mxs, mxl⇩0, instrs_of (PROG P) C M, ex_table_of (PROG P) C M) in C"
    by (fastforce dest: method_of_reachable_node_exists)
  with ‹pc < length (instrs_of (PROG P) C M)› ‹instrs_of (PROG P) C M ! pc = Getfield F Cl›
  have "PROG P,T,mxs,length (instrs_of (PROG P) C M),ex_table_of (PROG P) C M
    ⊢ Getfield F Cl,pc :: TYPING P C M"
    by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
  moreover from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)› ‹C ≠ ClassMain P›
    ‹instrs_of (PROG P) C M ! pc = Getfield F Cl› obtain d'
    where "match_ex_table (PROG P) NullPointer pc (ex_table_of (PROG P) C M) = ⌊(pc', d')⌋"
    by cases (fastforce elim: JVMCFG.cases)
  hence "∃(f, t, D, h, d)∈set (ex_table_of (PROG P) C M).
    matches_ex_entry (PROG P) NullPointer pc (f, t, D, h, d) ∧ h = pc' ∧ d = d'"
    by -(drule match_ex_table_SomeD)
  ultimately show ?case using ‹instrs_of (PROG P) C M ! pc = Getfield F Cl›
    by (fastforce simp: relevant_entries_def is_relevant_entry_def matches_ex_entry_def)
next
  case (CFG_Putfield_Update C P C0 Main M pc F Cl ek)
  from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Normal)› ‹C ≠ ClassMain P›
  obtain Ts T mxs mxl⇩0 "is" xt where "PROG P ⊢ C sees M:Ts→T = (mxs, mxl⇩0, is, xt) in C"
    and "instrs_of (PROG P) C M = is"
    by -(drule method_of_reachable_node_exists, auto)
  with CFG_Putfield_Update show ?case
    by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
  case (CFG_Putfield_Exceptional_handle C P C0 Main M pc pc' F Cl ek)
  hence "TYPING P C M ! pc ≠ None" and "pc < length (instrs_of (PROG P) C M)"
    by simp_all
  moreover from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)› ‹C ≠ ClassMain P›
  obtain Ts T mxs mxl⇩0 where
    "PROG P ⊢ C sees M:Ts→T = (mxs, mxl⇩0, instrs_of (PROG P) C M, ex_table_of (PROG P) C M) in C"
    by (fastforce dest: method_of_reachable_node_exists)
  with ‹pc < length (instrs_of (PROG P) C M)› ‹instrs_of (PROG P) C M ! pc = Putfield F Cl›
  have "PROG P,T,mxs,length (instrs_of (PROG P) C M),ex_table_of (PROG P) C M
    ⊢ Putfield F Cl,pc :: TYPING P C M"
    by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
  moreover from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)› ‹C ≠ ClassMain P›
    ‹instrs_of (PROG P) C M ! pc = Putfield F Cl› obtain d'
    where "match_ex_table (PROG P) NullPointer pc (ex_table_of (PROG P) C M) = ⌊(pc', d')⌋"
    by cases (fastforce elim: JVMCFG.cases)
  hence "∃(f, t, D, h, d)∈set (ex_table_of (PROG P) C M).
    matches_ex_entry (PROG P) NullPointer pc (f, t, D, h, d) ∧ h = pc' ∧ d = d'"
    by -(drule match_ex_table_SomeD)
  ultimately show ?case using ‹instrs_of (PROG P) C M ! pc = Putfield F Cl›
    by (fastforce simp: relevant_entries_def is_relevant_entry_def matches_ex_entry_def)
next
  case (CFG_Checkcast_Check_Normal C P C0 Main M pc Cl ek)
  from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter)› ‹C ≠ ClassMain P›
  obtain Ts T mxs mxl⇩0 "is" xt where "PROG P ⊢ C sees M:Ts→T = (mxs, mxl⇩0, is, xt) in C"
    and "instrs_of (PROG P) C M = is"
    by -(drule method_of_reachable_node_exists, auto)
  with CFG_Checkcast_Check_Normal show ?case
    by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
  case (CFG_Checkcast_Exceptional_handle C P C0 Main M pc pc' Cl ek)
  hence "TYPING P C M ! pc ≠ None" and "pc < length (instrs_of (PROG P) C M)"
    by simp_all
  moreover from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)› ‹C ≠ ClassMain P›
  obtain Ts T mxs mxl⇩0 where
    "PROG P ⊢ C sees M:Ts→T = (mxs, mxl⇩0, instrs_of (PROG P) C M, ex_table_of (PROG P) C M) in C"
    by (fastforce dest: method_of_reachable_node_exists)
  with ‹pc < length (instrs_of (PROG P) C M)› ‹instrs_of (PROG P) C M ! pc = Checkcast Cl›
  have "PROG P,T,mxs,length (instrs_of (PROG P) C M),ex_table_of (PROG P) C M
    ⊢ Checkcast Cl,pc :: TYPING P C M"
    by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
  moreover from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)› ‹C ≠ ClassMain P›
    ‹instrs_of (PROG P) C M ! pc = Checkcast Cl› obtain d'
    where "match_ex_table (PROG P) ClassCast pc (ex_table_of (PROG P) C M) = ⌊(pc', d')⌋"
    by cases (fastforce elim: JVMCFG.cases)
  hence "∃(f, t, D, h, d)∈set (ex_table_of (PROG P) C M).
    matches_ex_entry (PROG P) ClassCast pc (f, t, D, h, d) ∧ h = pc' ∧ d = d'"
    by -(drule match_ex_table_SomeD)
  ultimately show ?case using ‹instrs_of (PROG P) C M ! pc = Checkcast Cl›
    by (fastforce simp: relevant_entries_def is_relevant_entry_def matches_ex_entry_def)
next
  case (CFG_Throw_handle C P C0 Main M pc pc' ek)
  hence "TYPING P C M ! pc ≠ None" and "pc < length (instrs_of (PROG P) C M)"
    by simp_all
  moreover from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)› ‹C ≠ ClassMain P›
  obtain Ts T mxs mxl⇩0 where
    "PROG P ⊢ C sees M:Ts→T = (mxs, mxl⇩0, instrs_of (PROG P) C M, ex_table_of (PROG P) C M) in C"
    by (fastforce dest: method_of_reachable_node_exists)
  with ‹pc < length (instrs_of (PROG P) C M)› ‹instrs_of (PROG P) C M ! pc = Throw›
  have "PROG P,T,mxs,length (instrs_of (PROG P) C M),ex_table_of (PROG P) C M
    ⊢ Throw,pc :: TYPING P C M"
    by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
  moreover from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)› ‹C ≠ ClassMain P›
    ‹instrs_of (PROG P) C M ! pc = Throw› obtain d' Exc
    where "match_ex_table (PROG P) Exc pc (ex_table_of (PROG P) C M) = ⌊(pc', d')⌋"
    by cases (fastforce elim: JVMCFG.cases)
  hence "∃(f, t, D, h, d)∈set (ex_table_of (PROG P) C M).
    matches_ex_entry (PROG P) Exc pc (f, t, D, h, d) ∧ h = pc' ∧ d = d'"
    by -(drule match_ex_table_SomeD)
  ultimately show ?case using ‹instrs_of (PROG P) C M ! pc = Throw›
    by (fastforce simp: relevant_entries_def is_relevant_entry_def matches_ex_entry_def)
next
  case (CFG_Invoke_NP_handle C P C0 Main M pc pc' M' n ek)
  hence "TYPING P C M ! pc ≠ None" and "pc < length (instrs_of (PROG P) C M)"
    by simp_all
  moreover from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)› ‹C ≠ ClassMain P›
  obtain Ts T mxs mxl⇩0 where
    "PROG P ⊢ C sees M:Ts→T = (mxs, mxl⇩0, instrs_of (PROG P) C M, ex_table_of (PROG P) C M) in C"
    by (fastforce dest: method_of_reachable_node_exists)
  with ‹pc < length (instrs_of (PROG P) C M)› ‹instrs_of (PROG P) C M ! pc = Invoke M' n›
  have "PROG P,T,mxs,length (instrs_of (PROG P) C M),ex_table_of (PROG P) C M
    ⊢ Invoke M' n,pc :: TYPING P C M"
    by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
  moreover from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)› ‹C ≠ ClassMain P›
    ‹instrs_of (PROG P) C M ! pc = Invoke M' n› obtain d'
    where "match_ex_table (PROG P) NullPointer pc (ex_table_of (PROG P) C M) = ⌊(pc', d')⌋"
    by cases (fastforce elim: JVMCFG.cases)
  hence "∃(f, t, D, h, d)∈set (ex_table_of (PROG P) C M).
    matches_ex_entry (PROG P) NullPointer pc (f, t, D, h, d) ∧ h = pc' ∧ d = d'"
    by -(drule match_ex_table_SomeD)
  ultimately show ?case using ‹instrs_of (PROG P) C M ! pc = Invoke M' n›
    by (fastforce simp: relevant_entries_def is_relevant_entry_def matches_ex_entry_def)
next
  case (CFG_Invoke_Return_Exceptional_handle C P C0 Main M pc pc' M' n ek)
  hence "TYPING P C M ! pc ≠ None" and "pc < length (instrs_of (PROG P) C M)"
    by simp_all
  moreover from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Return)› ‹C ≠ ClassMain P›
  obtain Ts T mxs mxl⇩0 where
    "PROG P ⊢ C sees M:Ts→T = (mxs, mxl⇩0, instrs_of (PROG P) C M, ex_table_of (PROG P) C M) in C"
    by (fastforce dest: method_of_reachable_node_exists)
  with ‹pc < length (instrs_of (PROG P) C M)› ‹instrs_of (PROG P) C M ! pc = Invoke M' n›
  have "PROG P,T,mxs,length (instrs_of (PROG P) C M),ex_table_of (PROG P) C M
    ⊢ Invoke M' n,pc :: TYPING P C M"
    by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
  moreover from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Return)› ‹C ≠ ClassMain P›
    ‹instrs_of (PROG P) C M ! pc = Invoke M' n› obtain d' Exc
    where "match_ex_table (PROG P) Exc pc (ex_table_of (PROG P) C M) = ⌊(pc', d')⌋"
    by cases (fastforce elim: JVMCFG.cases)
  hence "∃(f, t, D, h, d)∈set (ex_table_of (PROG P) C M).
    matches_ex_entry (PROG P) Exc pc (f, t, D, h, d) ∧ h = pc' ∧ d = d'"
    by -(drule match_ex_table_SomeD)
  ultimately show ?case using ‹instrs_of (PROG P) C M ! pc = Invoke M' n›
    by (fastforce simp: relevant_entries_def is_relevant_entry_def matches_ex_entry_def)
next
  case (CFG_Invoke_Return_Check_Normal C P C0 Main M pc M' n ST LT ek)
  from ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Return)› ‹C ≠ ClassMain P›
  obtain Ts T mxs mxl⇩0 "is" xt where "PROG P ⊢ C sees M:Ts→T = (mxs, mxl⇩0, is, xt) in C"
    and "instrs_of (PROG P) C M = is"
    by -(drule method_of_reachable_node_exists, auto)
  with CFG_Invoke_Return_Check_Normal show ?case
    by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next 
  case (Method_LTrue P C0 Main C M)
  from ‹(P, C0, Main) ⊢ ⇒(C, M, None, Enter)› ‹C ≠ ClassMain P›
  obtain Ts T mxs mxl⇩0 "is" xt where "PROG P ⊢ C sees M:Ts→T = (mxs, mxl⇩0, is, xt) in C"
    and "instrs_of (PROG P) C M = is"
    by -(drule method_of_reachable_node_exists, auto)
  with Method_LTrue show ?case
    by (fastforce dest!: wt_jvm_prog_impl_wt_start [OF wf_jvmprog_is_wf_typ] simp: wt_start_def)
next
  case (reachable_step P C0 Main C M opc nt ek C' M' opc' nt')
  thus ?case
    by (cases "C = ClassMain P") (fastforce elim: JVMCFG.cases, simp)
qed simp_all

lemma reachable_node_impl_wt_instr:
  assumes "(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, nt)"
  and "C ≠ ClassMain P"
  shows "∃T mxs mpc xt. PROG P,T,mxs,mpc,xt ⊢ (instrs_of (PROG P) C M ! pc),pc :: TYPING P C M"
proof -
  from ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, nt)›
    method_of_reachable_node_exists [of P C0 Main C M "⌊pc⌋" nt]
    instr_of_reachable_node_typable [of P C0 Main C M "⌊pc⌋" nt]
  obtain Ts T mxs mxl⇩0 "is" xt
    where "PROG P ⊢ C sees M:Ts→T = (mxs, mxl⇩0, is, xt) in C"
    and "TYPING P C M ! pc ≠ None"
    and "pc < length (instrs_of (PROG P) C M)"
    by fastforce+
  with wf_jvmprog_is_wf_typ [of P]
  have "PROG P,T,mxs,length is,xt ⊢ instrs_of (PROG P) C M ! pc,pc :: TYPING P C M"
    by (fastforce dest!: wt_jvm_prog_impl_wt_instr)
  thus ?thesis
    by blast
qed

lemma
  "⟦ (P, C0, Main) ⊢ (C, M, pc, nt) -ek→ (C', M', pc', nt'); C ≠ ClassMain P ∨ C' ≠ ClassMain P ⟧
  ⟹ ∃T mb D. PROG P ⊢ C0 sees Main:[]→T = mb in D"
  and reachable_node_impl_Main_ex:
  "⟦ (P, C0, Main) ⊢ ⇒(C, M, pc, nt); C ≠ ClassMain P⟧
  ⟹ ∃T mb D. PROG P ⊢ C0 sees Main:[]→T = mb in D"
  by (induct rule: JVMCFG_reachable_inducts) fastforce+

end