Theory JVMCFG_wf

theory JVMCFG_wf imports JVMInterpretation "../Basic/CFGExit_wf" begin

section ‹Instantiation of the ‹CFG_wf› locale›

subsection ‹Variables and Values›

datatype jinja_var = HeapVar "addr" | Stk "nat" "nat" | Loc "nat" "nat"
datatype jinja_val = Object "obj option" | Primitive "val"

fun state_val :: "state ⇒ jinja_var ⇒ jinja_val"
where
  "state_val (h, stk, loc) (HeapVar a) = Object (h a)"
| "state_val (h, stk, loc) (Stk cd idx) = Primitive (stk (cd, idx))"
| "state_val (h, stk, loc) (Loc cd idx) = Primitive (loc (cd, idx))"


subsection ‹The ‹Def› and ‹Use› sets›

inductive_set Def :: "wf_jvmprog ⇒ j_node ⇒ jinja_var set"
  for P :: "wf_jvmprog"
  and n :: "j_node"
where
  Def_Load:
  "⟦ n = (_ (C, M, pc)#cs,None _);
  instrs_of (P⇘wf⇙) C M ! pc = Load idx;
  cd = length cs;
  i = stkLength P C M pc⟧
  ⟹ Stk cd i ∈ Def P n"

| Def_Store:
  "⟦ n = (_ (C, M, pc)#cs,None _);
  instrs_of (P⇘wf⇙) C M ! pc = Store idx;
  cd = length cs ⟧
  ⟹ Loc cd idx ∈ Def P n"

| Def_Push:
  "⟦ n = (_ (C, M, pc)#cs,None _);
  instrs_of (P⇘wf⇙) C M ! pc = Push v;
  cd = length cs;
  i = stkLength P C M pc ⟧
  ⟹ Stk cd i ∈ Def P n"

| Def_New_Normal_Stk:
  "⟦ n = (_ (C, M, pc)#cs,⌊(cs',False)⌋ _);
  instrs_of (P⇘wf⇙) C M ! pc = New Cl;
  cd = length cs;
  i = stkLength P C M pc ⟧
  ⟹ Stk cd i ∈ Def P n"

| Def_New_Normal_Heap:
  "⟦ n = (_ (C, M, pc)#cs,⌊(cs',False)⌋ _);
  instrs_of (P⇘wf⇙) C M ! pc = New Cl ⟧
  ⟹ HeapVar a ∈ Def P n"

| Def_Exc_Stk:
  "⟦ n = (_ (C, M, pc)#cs,⌊(cs',True)⌋ _);
  cs' ≠ [];
  cd = length cs' - 1;
  (C',M',pc') = hd cs';
  i = stkLength P C' M' pc' - 1⟧
  ⟹ Stk cd i ∈ Def P n"

| Def_Getfield_Stk:
  "⟦ n = (_ (C, M, pc)#cs,⌊(cs',False)⌋ _);
  instrs_of (P⇘wf⇙) C M ! pc = Getfield Fd Cl;
  cd = length cs;
  i = stkLength P C M pc - 1 ⟧
  ⟹ Stk cd i ∈ Def P n"

| Def_Putfield_Heap:
  "⟦ n = (_ (C, M, pc)#cs,⌊(cs',False)⌋ _);
  instrs_of (P⇘wf⇙) C M ! pc = Putfield Fd Cl ⟧
  ⟹ HeapVar a ∈ Def P n"

| Def_Invoke_Loc:
  "⟦ n = (_ (C, M, pc)#cs,⌊(cs',False)⌋ _);
  instrs_of (P⇘wf⇙) C M ! pc = Invoke M' n';
  cs' ≠ [];
  hd cs' = (C',M',0);
  i < locLength P C' M' 0;
  cd = Suc (length cs) ⟧
  ⟹ Loc cd i ∈ Def P n"

| Def_Return_Stk:
  "⟦ n = (_ (C, M, pc)#(D,M',pc')#cs,None _);
  instrs_of (P⇘wf⇙) C M ! pc = Return;
  cd = length cs;
  i = stkLength P D M' (Suc pc') - 1 ⟧
  ⟹ Stk cd i ∈ Def P n"

| Def_IAdd_Stk:
  "⟦ n = (_ (C, M, pc)#cs,None _);
  instrs_of (P⇘wf⇙) C M ! pc = IAdd;
  cd = length cs;
  i = stkLength P C M pc - 2 ⟧
  ⟹ Stk cd i ∈ Def P n"

| Def_CmpEq_Stk:
  "⟦ n = (_ (C, M, pc)#cs,None _);
  instrs_of (P⇘wf⇙) C M ! pc = CmpEq;
  cd = length cs;
  i = stkLength P C M pc - 2 ⟧
  ⟹ Stk cd i ∈ Def P n"

inductive_set Use :: "wf_jvmprog ⇒ j_node ⇒ jinja_var set"
  for P :: "wf_jvmprog"
  and n :: "j_node"
where
  Use_Load:
  "⟦ n = (_ (C, M, pc)#cs,None _);
  instrs_of (P⇘wf⇙) C M ! pc = Load idx;
  cd = length cs ⟧
  ⟹ (Loc cd idx) ∈ Use P n"

| Use_Store:
  "⟦ n = (_ (C, M, pc)#cs,None _);
  instrs_of (P⇘wf⇙) C M ! pc = Store idx;
  cd = length cs;
  Suc i = (stkLength P C M pc) ⟧
  ⟹ (Stk cd i) ∈ Use P n"

| Use_New:
  "⟦ n = (_ (C, M, pc)#cs,x _);
  x = None ∨ x = ⌊(cs',False)⌋;
  instrs_of (P⇘wf⇙) C M ! pc = New Cl ⟧
  ⟹ HeapVar a ∈ Use P n"

| Use_Getfield_Stk:
  "⟦ n = (_ (C, M, pc)#cs,x _);
  x = None ∨ x = ⌊(cs',False)⌋;
  instrs_of (P⇘wf⇙) C M ! pc = Getfield Fd Cl;
  cd = length cs;
  Suc i = stkLength P C M pc ⟧
  ⟹ Stk cd i ∈ Use P n"

| Use_Getfield_Heap:
  "⟦ n = (_ (C, M, pc)#cs,⌊(cs',False)⌋ _);
  instrs_of (P⇘wf⇙) C M ! pc = Getfield Fd Cl ⟧
  ⟹ HeapVar a ∈ Use P n"

| Use_Putfield_Stk_Pred:
  "⟦ n = (_ (C, M, pc)#cs,None _);
  instrs_of (P⇘wf⇙) C M ! pc = Putfield Fd Cl;
  cd = length cs;
  i = stkLength P C M pc - 2 ⟧
  ⟹ Stk cd i ∈ Use P n"

| Use_Putfield_Stk_Update:
  "⟦ n = (_ (C, M, pc)#cs,⌊(cs',False)⌋ _);
  instrs_of (P⇘wf⇙) C M ! pc = Putfield Fd Cl;
  cd = length cs;
  i = stkLength P C M pc - 2 ∨ i = stkLength P C M pc - 1 ⟧
  ⟹ Stk cd i ∈ Use P n"

| Use_Putfield_Heap:
  "⟦ n = (_ (C, M, pc)#cs,⌊(cs',False)⌋ _);
  instrs_of (P⇘wf⇙) C M ! pc = Putfield Fd Cl ⟧
  ⟹ HeapVar a ∈ Use P n"

| Use_Checkcast_Stk:
  "⟦ n = (_ (C, M, pc)#cs,x _);
  x = None ∨ x = ⌊(cs',False)⌋;
  instrs_of (P⇘wf⇙) C M ! pc = Checkcast Cl;
  cd = length cs;
  i = stkLength P C M pc - Suc 0 ⟧
  ⟹ Stk cd i ∈ Use P n"

| Use_Checkcast_Heap:
  "⟦ n = (_ (C, M, pc)#cs,None _);
  instrs_of (P⇘wf⇙) C M ! pc = Checkcast Cl ⟧
  ⟹ HeapVar a ∈ Use P n"

| Use_Invoke_Stk_Pred:
  "⟦ n = (_ (C, M, pc)#cs,None _);
  instrs_of (P⇘wf⇙) C M ! pc = Invoke M' n';
  cd = length cs;
  i = stkLength P C M pc - Suc n' ⟧
  ⟹ Stk cd i ∈ Use P n"

| Use_Invoke_Heap_Pred:
  "⟦ n = (_ (C, M, pc)#cs,None _);
  instrs_of (P⇘wf⇙) C M ! pc = Invoke M' n' ⟧
  ⟹ HeapVar a ∈ Use P n"

| Use_Invoke_Stk_Update:
  "⟦ n = (_ (C, M, pc)#cs,⌊(cs',False)⌋ _);
  instrs_of (P⇘wf⇙) C M ! pc = Invoke M' n';
  cd = length cs;
  i < stkLength P C M pc;
  i ≥ stkLength P C M pc - Suc n' ⟧
  ⟹ Stk cd i ∈ Use P n"

| Use_Return_Stk:
  "⟦ n = (_ (C, M, pc)#(D,M',pc')#cs,None _);
  instrs_of (P⇘wf⇙) C M ! pc = Return;
  cd = Suc (length cs);
  i = stkLength P C M pc - 1 ⟧
  ⟹ Stk cd i ∈ Use P n"

| Use_IAdd_Stk:
  "⟦ n = (_ (C, M, pc)#cs,None _);
  instrs_of (P⇘wf⇙) C M ! pc = IAdd;
  cd = length cs;
  i = stkLength P C M pc - 1 ∨ i = stkLength P C M pc - 2 ⟧
  ⟹ Stk cd i ∈ Use P n"

| Use_IfFalse_Stk:
  "⟦ n = (_ (C, M, pc)#cs,None _);
  instrs_of (P⇘wf⇙) C M ! pc = (IfFalse b);
  cd = length cs;
  i = stkLength P C M pc - 1 ⟧
  ⟹ Stk cd i ∈ Use P n"

| Use_CmpEq_Stk:
  "⟦ n = (_ (C, M, pc)#cs,None _);
  instrs_of (P⇘wf⇙) C M ! pc = CmpEq;
  cd = length cs;
  i = stkLength P C M pc - 1 ∨ i = stkLength P C M pc - 2 ⟧
  ⟹ Stk cd i ∈ Use P n"

| Use_Throw_Stk:
  "⟦ n = (_ (C, M, pc)#cs,x _);
  x = None ∨ x = ⌊(cs',True)⌋;
  instrs_of (P⇘wf⇙) C M ! pc = Throw;
  cd = length cs;
  i = stkLength P C M pc - 1 ⟧
  ⟹ Stk cd i ∈ Use P n"

| Use_Throw_Heap:
  "⟦ n = (_ (C, M, pc)#cs,x _);
  x = None ∨ x = ⌊(cs',True)⌋;
  instrs_of (P⇘wf⇙) C M ! pc = Throw ⟧
  ⟹ HeapVar a ∈ Use P n"

declare correct_state_def [simp del]

lemma edge_transfer_uses_only_Use:
  "⟦valid_edge (P,C0,Main) a; ∀V ∈ Use P (sourcenode a). state_val s V = state_val s' V⟧
  ⟹ ∀V ∈ Def P (sourcenode a). state_val (BasicDefs.transfer (kind a) s) V =
                                  state_val (BasicDefs.transfer (kind a) s') V"
proof
  fix V
  assume ve: "valid_edge (P, C0, Main) a"
    and use_eq: "∀V∈Use P (sourcenode a). state_val s V = state_val s' V"
    and v_in_def: "V ∈ Def P (sourcenode a)"
  obtain h stk loc where [simp]: "s = (h,stk,loc)" by (cases s, fastforce)
  obtain h' stk' loc' where [simp]: "s' = (h',stk',loc')" by (cases s', fastforce)
  note P_wf = wf_jvmprog_is_wf [of P]
  from ve
  have ex_edge: "(P,C0,Main) ⊢ (sourcenode a)-kind a→(targetnode a)"
    and vn: "valid_node (P,C0,Main) (sourcenode a)"
    by simp_all
  show "state_val (transfer (kind a) s) V = state_val (transfer (kind a) s') V"
  proof (cases "sourcenode a")
    case [simp]: (Node cs x)
    from vn ex_edge have "cs ≠ []"
      by (cases x, auto elim: JVM_CFG.cases)
    then obtain C M pc cs' where [simp]: "cs = (C, M, pc)#cs'" by (cases cs, fastforce+)
    with vn obtain ST LT where wt: "((P⇘Φ⇙) C M ! pc) = ⌊(ST,LT)⌋"
      by (cases cs', (cases x, auto)+)
    show ?thesis
    proof (cases "instrs_of (P⇘wf⇙) C M ! pc")
      case [simp]: (Load n)
      from ex_edge have [simp]: "x = None"
        by (auto elim!: JVM_CFG.cases)
      hence "Loc (length cs') n ∈ Use P (sourcenode a)"
        by (auto intro!: Use_Load)
      with use_eq have "state_val s (Loc (length cs') n) = state_val s' (Loc (length cs') n)"
        by (simp del: state_val.simps)
      with v_in_def ex_edge show ?thesis
        by (auto elim!: Def.cases
                  elim: JVM_CFG.cases
                  simp: split_beta)
    next
      case [simp]: (Store n)
      from ex_edge have [simp]:"x = None"
        by (auto elim!: JVM_CFG.cases)
      have "ST ≠ []"
      proof -
        from vn
        obtain Ts T mxs mxl "is" xt
          where C_sees_M: "P⇘wf⇙ ⊢ C sees M: Ts→T = (mxs, mxl, is, xt) in C"
          by (cases cs', auto)
        with vn
        have "pc < length is"
          by (cases cs', auto dest: sees_method_fun)
        from P_wf C_sees_M
        have "wt_method (P⇘wf⇙) C Ts T mxs mxl is xt (P⇘Φ⇙ C M)"
          by (auto dest: sees_wf_mdecl simp: wf_jvm_prog_phi_def wf_mdecl_def)
        with Store C_sees_M wt ‹pc < length is›
        show ?thesis
          by (fastforce simp: wt_method_def)
      qed
      then obtain ST1 STr where [simp]: "ST = ST1#STr"
        by (cases ST, fastforce+)
      from wt
        have "Stk (length cs') (length ST - 1) ∈ Use P (sourcenode a)"
          (is "?stk_top ∈ ?Use_src")
          by -(rule Use_Store, fastforce+)
      with use_eq have "state_val s ?stk_top = state_val s' ?stk_top"
        by (simp del: state_val.simps)
      with v_in_def ex_edge wt show ?thesis
        by (auto elim!: Def.cases
                  elim: JVM_CFG.cases
                  simp: split_beta)
    next
      case [simp]: (Push val)
      from ex_edge have "x = None"
        by (auto elim!: JVM_CFG.cases)
      with v_in_def ex_edge show ?thesis
        by (auto elim!: Def.cases
                  elim: JVM_CFG.cases)
    next
      case [simp]: (New Cl)
      show ?thesis
      proof (cases x)
        case None
        with v_in_def have False
          by (auto elim: Def.cases)
        thus ?thesis by simp
      next
        case (Some x')
        then obtain cs'' xf where [simp]: "x = ⌊(cs'',xf)⌋"
          by (cases x', fastforce)
        have "¬ xf ⟶ (∀addr. HeapVar addr ∈ Use P (sourcenode a))"
          by (fastforce intro: Use_New)
        with use_eq
        have "¬ xf ⟶ (∀addr. state_val s (HeapVar addr) = state_val s' (HeapVar addr))"
          by (simp del: state_val.simps)
        hence "¬ xf ⟶ h = h'"
          by (auto intro: ext)
        with v_in_def ex_edge show ?thesis
          by (auto elim!: Def.cases
                    elim: JVM_CFG.cases)
      qed
    next
      case [simp]: (Getfield Fd Cl)
      show ?thesis
      proof (cases x)
        case None
        with v_in_def have False
          by (auto elim: Def.cases)
        thus ?thesis by simp
      next
        case (Some x')
        then obtain cs'' xf where [simp]: "x = ⌊(cs'',xf)⌋"
          by (cases x', fastforce)
        have "ST ≠ []"
        proof -
          from vn obtain T Ts mxs mxl "is" xt
            where sees_M: "(P⇘wf⇙) ⊢ C sees M:Ts→T = (mxs,mxl,is,xt) in C"
            by (cases cs', auto)
          with vn
          have "pc < length is"
            by (cases cs', auto dest: sees_method_fun)
          from P_wf sees_M have "wt_method (P⇘wf⇙) C Ts T mxs mxl is xt (P⇘Φ⇙ C M)"
            by (auto dest: sees_wf_mdecl simp: wf_jvm_prog_phi_def wf_mdecl_def)
          with Getfield sees_M wt ‹pc < length is› show ?thesis
            by (fastforce simp: wt_method_def)
        qed
        then obtain ST1 STr where [simp]: "ST = ST1#STr" by (cases ST, fastforce)
        from wt
        have "¬ xf ⟶ (Stk (length cs') (length ST - 1) ∈ Use P (sourcenode a))"
          (is "?xf ⟶ ?stk_top ∈ ?Use_src")
          by (auto intro!: Use_Getfield_Stk)
        with use_eq 
        have stk_top_eq: "¬ xf ⟶ state_val s ?stk_top = state_val s' ?stk_top"
          by (simp del: state_val.simps)
        have "¬ xf ⟶ (∀addr. HeapVar addr ∈ Use P (sourcenode a))"
          by (auto intro!: Use_Getfield_Heap)
        with use_eq
        have "¬ xf ⟶ (∀addr. state_val s (HeapVar addr) = state_val s' (HeapVar addr))"
          by (simp del: state_val.simps)
        hence "¬ xf ⟶ h = h'"
          by (auto intro: ext)
        with ex_edge v_in_def stk_top_eq wt
        show ?thesis
          by (auto elim!: Def.cases
                    elim: JVM_CFG.cases
                    simp: split_beta)
      qed
    next
      case [simp]: (Putfield Fd Cl)
      show ?thesis
      proof (cases x)
        case None
        with v_in_def have False
          by (auto elim: Def.cases)
        thus ?thesis by simp
      next
        case (Some x')
        then obtain cs'' xf where [simp]: "x = ⌊(cs'',xf)⌋" 
          by (cases x', fastforce)
        have "length ST > 1"
        proof -
          from vn obtain T Ts mxs mxl "is" xt
            where sees_M: "(P⇘wf⇙) ⊢ C sees M:Ts→T = (mxs,mxl,is,xt) in C"
            by (cases cs', auto)
          with vn
          have "pc < length is"
            by (cases cs', auto dest: sees_method_fun)
          from P_wf sees_M have "wt_method (P⇘wf⇙) C Ts T mxs mxl is xt (P⇘Φ⇙ C M)"
            by (auto dest: sees_wf_mdecl simp: wf_jvm_prog_phi_def wf_mdecl_def)
          with Putfield sees_M ‹pc < length is› wt show ?thesis
            by (fastforce simp: wt_method_def)
        qed
        then obtain ST1 STr' where "ST = ST1#STr' ∧ length STr' > 0"
          by (cases ST, fastforce+)
        then obtain ST2 STr where [simp]: "ST = ST1#ST2#STr"
          by (cases STr', fastforce+)
        from wt
        have "¬ xf ⟶ (Stk (length cs') (length ST - 1) ∈ Use P (sourcenode a))"
          (is "?xf ⟶ ?stk_top ∈ ?Use_src")
          by (fastforce intro: Use_Putfield_Stk_Update)
        with use_eq have stk_top:"(¬ xf) ⟶ state_val s ?stk_top = state_val s' ?stk_top"
          by (simp del: state_val.simps)
        from wt
        have "¬ xf ⟶ (Stk (length cs') (length ST - 2) ∈ Use P (sourcenode a))"
          (is "?xf ⟶ ?stk_nxt ∈ ?Use_src")
          by (fastforce intro: Use_Putfield_Stk_Update)
        with use_eq
        have stk_nxt:"(¬ xf) ⟶ state_val s ?stk_nxt = state_val s' ?stk_nxt"
          by (simp del: state_val.simps)
        have "¬ xf ⟶ (∀addr. HeapVar addr ∈ Use P (sourcenode a))"
          by (fastforce intro: Use_Putfield_Heap)
        with use_eq
        have "¬ xf ⟶ (∀addr. state_val s (HeapVar addr) = state_val s' (HeapVar addr))"
          by (simp del: state_val.simps)
        hence "¬ xf ⟶ h = h'"
          by (auto intro: ext)
        with ex_edge v_in_def stk_top stk_nxt wt show ?thesis
          by (auto elim!: Def.cases
                   elim: JVM_CFG.cases
                   simp: split_beta)
      qed
    next
      case [simp]: (Checkcast Cl)
      show ?thesis
      proof (cases x)
        case None
        with v_in_def have False
          by (auto elim: Def.cases)
        thus ?thesis by simp
      next
        case (Some x')
        with ex_edge obtain cs''
          where "x = ⌊(cs'',True)⌋"
          by (auto elim!: JVM_CFG.cases)
        with v_in_def ex_edge show ?thesis
          by (auto elim!: Def.cases
                    elim: JVM_CFG.cases)
      qed
    next
      case [simp]: (Invoke M' n')
      show ?thesis
      proof (cases x)
        case None
        with v_in_def have False
          by (auto elim: Def.cases)
        thus ?thesis by simp
      next
        case (Some x')
        then obtain cs'' xf where [simp]: "x = ⌊(cs'',xf)⌋"
          by (cases x', fastforce)
        show ?thesis
        proof (cases xf)
          case True
          with v_in_def ex_edge show ?thesis
            by (auto elim!: Def.cases
                      elim: JVM_CFG.cases)
        next
          case [simp]: False
          have "length ST > n'"
          proof -
            from vn obtain T Ts mxs mxl "is" xt
              where sees_M: "(P⇘wf⇙) ⊢ C sees M:Ts→T = (mxs,mxl,is,xt) in C"
              by (cases cs', auto)
            with vn
            have "pc < length is"
              by (cases cs', auto dest: sees_method_fun)
            from P_wf sees_M have "wt_method (P⇘wf⇙) C Ts T mxs mxl is xt (P⇘Φ⇙ C M)"
              by (auto dest: sees_wf_mdecl simp: wf_jvm_prog_phi_def wf_mdecl_def)
            with Invoke sees_M ‹pc < length is› wt show ?thesis
              by (fastforce simp: wt_method_def)
          qed
          moreover obtain STn where "STn = take n' ST" by fastforce
          moreover obtain STs where "STs = ST ! n'" by fastforce
          moreover obtain STr where "STr = drop (Suc n') ST" by fastforce
          ultimately have [simp]:" ST = STn@STs#STr ∧ length STn = n'"
            by (auto simp: id_take_nth_drop)
          from wt
          have "∀i. i ≤ n' ⟶ Stk (length cs') (length ST - Suc i) ∈ Use P (sourcenode a)"
            by (fastforce intro: Use_Invoke_Stk_Update)
          with use_eq
          have
            "∀i. i ≤ n' ⟶ state_val s (Stk (length cs') (length ST - Suc i)) =
                           state_val s' (Stk (length cs') (length ST - Suc i))"
            by (simp del: state_val.simps)
          hence stk_eq:
            "∀i. i ≤ n' ⟶ state_val s (Stk (length cs') (i + length STr)) =
                           state_val s' (Stk (length cs') (i + length STr))"
            by (clarsimp, erule_tac x="n' - i" in allE, auto simp: add.commute)
          from ex_edge obtain C'
            where trg: "targetnode a = (_ (C',M',0)#(C, M, pc)#cs',None _)"
            by (fastforce elim: JVM_CFG.cases)
          with ex_edge stk_eq v_in_def wt
          show ?thesis
            by (auto elim!: Def.cases) (erule JVM_CFG.cases, auto simp: split_beta add.commute)
        qed
      qed
    next
      case [simp]: Return
      show ?thesis
      proof (cases x)
        case [simp]: None
        show ?thesis
        proof (cases cs')
          case Nil
          with v_in_def show ?thesis
            by (auto elim!: Def.cases)
        next
          case (Cons aa list)
          then obtain C' M' pc' cs'' where [simp]: "cs' = (C',M',pc')#cs''"
            by (cases aa, fastforce)
          from wt
          have "Stk (length cs') (length ST - 1) ∈ Use P (sourcenode a)"
            by (fastforce intro: Use_Return_Stk)
          with use_eq
          have "state_val s (Stk (length cs') (length ST - 1)) =
                state_val s' (Stk (length cs') (length ST - 1))"
            by (simp del: state_val.simps)
          with v_in_def ex_edge wt show ?thesis
            by (auto elim!: Def.cases
                      elim: JVM_CFG.cases
                      simp: split_beta)
        qed
      next
        case (Some x')
        with ex_edge show ?thesis
          by (auto elim: JVM_CFG.cases)
      qed
    next
      case Pop
      with v_in_def ex_edge show ?thesis
        by (auto elim!: Def.cases elim: JVM_CFG.cases)
    next
      case [simp]: IAdd
      show ?thesis
      proof (cases x)
        case [simp]: None
        from wt
        have "Stk (length cs') (length ST - 1) ∈ Use P (sourcenode a)"
          (is "?stk_top ∈ ?Use")
          by (auto intro!: Use_IAdd_Stk)
        with use_eq
        have stk_top:"state_val s ?stk_top = state_val s' ?stk_top"
          by (simp del: state_val.simps)
        from wt
        have "Stk (length cs') (length ST - 2) ∈ Use P (sourcenode a)"
          (is "?stk_snd ∈ ?Use")
          by (auto intro!: Use_IAdd_Stk)
        with use_eq
        have stk_snd:"state_val s ?stk_snd = state_val s' ?stk_snd"
          by (simp del: state_val.simps)
        with v_in_def ex_edge stk_top wt show ?thesis
          by (auto elim!: Def.cases
                    elim: JVM_CFG.cases
                    simp: split_beta)
      next
        case (Some x')
        with ex_edge show ?thesis
          by (auto elim: JVM_CFG.cases)
      qed
    next
      case [simp]: (IfFalse b)
      show ?thesis
      proof (cases x)
        case [simp]: None
        from wt
        have "Stk (length cs') (length ST - 1) ∈ Use P (sourcenode a)"
          (is "?stk_top ∈ ?Use")
          by (auto intro!: Use_IfFalse_Stk)
        with use_eq
        have stk_top:"state_val s ?stk_top = state_val s' ?stk_top"
          by (simp del: state_val.simps)
        with v_in_def ex_edge wt show ?thesis
          by (auto elim!: Def.cases)
      next
        case (Some x')
        with ex_edge show ?thesis
          by (auto elim: JVM_CFG.cases)
      qed
    next
      case [simp]: CmpEq
      show ?thesis
      proof (cases x)
        case [simp]: None
        have "Stk (length cs') (stkLength P C M pc - 1) ∈ Use P (sourcenode a)"
          (is "?stk_top ∈ ?Use")
          by (auto intro!: Use_CmpEq_Stk)
        with use_eq
        have stk_top:"state_val s ?stk_top = state_val s' ?stk_top"
          by (simp del: state_val.simps)
        have "Stk (length cs') (stkLength P C M pc - 2) ∈ Use P (sourcenode a)"
          (is "?stk_snd ∈ ?Use")
          by (auto intro!: Use_CmpEq_Stk)
        with use_eq
        have stk_snd:"state_val s ?stk_snd = state_val s' ?stk_snd"
          by (simp del: state_val.simps)
        with v_in_def ex_edge stk_top wt show ?thesis
          by (auto elim!: Def.cases
                    elim: JVM_CFG.cases)
      next
        case (Some x')
        with ex_edge show ?thesis
          by (auto elim: JVM_CFG.cases)
      qed
    next
      case (Goto i)
      with ex_edge v_in_def show ?thesis
        by (auto elim!: Def.cases
                  elim: JVM_CFG.cases)
    next
      case [simp]: Throw
      show ?thesis
      proof (cases x)
        case [simp]: None
        have "Stk (length cs') (stkLength P C M pc - 1) ∈ Use P (sourcenode a)"
          (is "?stk_top ∈ ?Use")
          by (auto intro!: Use_Throw_Stk)
        with use_eq
        have stk_top:"state_val s ?stk_top = state_val s' ?stk_top"
          by (simp del: state_val.simps)
        with v_in_def show ?thesis
          by (auto elim!: Def.cases)
      next
        case (Some x')
        then obtain cs'' xf where [simp]: "x = ⌊(cs'',xf)⌋"
          by (cases x', fastforce)
        hence "xf ⟶ Stk (length cs') (stkLength P C M pc - 1) ∈ Use P (sourcenode a)"
          (is "xf ⟶ ?stk_top ∈ ?Use")
          by (fastforce intro: Use_Throw_Stk)
        with use_eq
        have stk_top:"xf ⟶ state_val s ?stk_top = state_val s' ?stk_top"
          by (simp del: state_val.simps)
        with v_in_def ex_edge show ?thesis
          by (auto elim!: Def.cases
                    elim: JVM_CFG.cases)
      qed
    qed
  next
    case Entry
    with vn v_in_def show ?thesis
      by -(erule Def.cases, auto)
  qed
qed

lemma CFG_edge_Uses_pred_equal:
  "⟦ valid_edge (P,C0,Main) a;
  pred (kind a) s; 
  ∀V ∈ Use P (sourcenode a). state_val s V = state_val s' V⟧
  ⟹ pred (kind a) s'"
proof -
  assume ve: "valid_edge (P,C0,Main) a"
    and pred: "pred (kind a) s"
    and use_eq: "∀V∈Use P (sourcenode a). state_val s V = state_val s' V"
  obtain h stk loc where [simp]: "s = (h,stk,loc)" by (cases s, blast)
  obtain h' stk' loc' where [simp]: "s' = (h',stk',loc')" by (cases s', blast)
  from ve
  have vn: "valid_node (P,C0,Main) (sourcenode a)"
    and ex_edge: "(P,C0,Main) ⊢ (sourcenode a)-kind a→(targetnode a)"
    by simp_all
  note P_wf = wf_jvmprog_is_wf [of P]
  show "pred (kind a) s'"
  proof (cases "sourcenode a")
    case [simp]: (Node cs x)
    from ve have "cs ≠ []"
      by (cases x, auto elim: JVM_CFG.cases)
    then obtain C M pc cs' where [simp]: "cs = (C, M, pc)#cs'" by (cases cs, fastforce+)
    from vn obtain ST LT where wt: "((P⇘Φ⇙) C M ! pc) = ⌊(ST,LT)⌋"
      by (cases cs', (cases x, auto)+)
    show ?thesis
    proof (cases "instrs_of (P⇘wf⇙) C M ! pc")
      case (Load nat)
      with ex_edge show ?thesis
        by (auto elim: JVM_CFG.cases)
    next
      case (Store nat)
      with ex_edge show ?thesis
        by (auto elim: JVM_CFG.cases)
    next
      case (Push val)
      with ex_edge show ?thesis
        by (auto elim: JVM_CFG.cases)
    next
      case [simp]: (New Cl)
      show ?thesis
      proof (cases x)
        case None
        hence "∀addr. HeapVar addr ∈ Use P (sourcenode a)"
          by (auto intro!: Use_New)
        with use_eq have "∀addr. state_val s (HeapVar addr) = state_val s' (HeapVar addr)"
          by (simp del: state_val.simps)
        hence "h = h'"
          by (auto intro: ext)
        with ex_edge pred show ?thesis
          by (auto elim!: JVM_CFG.cases)
      next
        case (Some x')
        with ex_edge show ?thesis
          by (auto elim: JVM_CFG.cases)
      qed
    next
      case [simp]: (Getfield Fd Cl)
      have "ST ≠ []"
      proof -
        from vn obtain T Ts mxs mxl "is" xt
          where sees_M: "(P⇘wf⇙) ⊢ C sees M:Ts→T = (mxs,mxl,is,xt) in C"
          by (cases cs', (cases x, auto)+)
        with vn
        have "pc < length is"
          by (cases cs', (cases x, auto dest: sees_method_fun)+)
        from P_wf sees_M have "wt_method (P⇘wf⇙) C Ts T mxs mxl is xt (P⇘Φ⇙ C M)"
          by (auto dest: sees_wf_mdecl simp: wf_jvm_prog_phi_def wf_mdecl_def)
        with Getfield wt sees_M ‹pc < length is› show ?thesis
          by (fastforce simp: wt_method_def)
      qed
      then obtain ST1 STr where [simp]: "ST = ST1#STr" by (cases ST, fastforce+)
      show ?thesis
      proof (cases x)
        case [simp]: None
        from wt
        have "Stk (length cs') (length ST - 1) ∈ Use P (sourcenode a)"
          (is "?stk_top ∈ ?Use")
          by (fastforce intro: Use_Getfield_Stk)
        with use_eq have "state_val s ?stk_top = state_val s' ?stk_top"
          by (simp del: state_val.simps)
        with ex_edge pred wt show ?thesis
          by (auto elim: JVM_CFG.cases)
      next
        case (Some x')
        with ex_edge show ?thesis
          by (auto elim: JVM_CFG.cases)
      qed
    next
      case [simp]: (Putfield Fd Cl)
      have "length ST > 1"
      proof -
        from vn obtain T Ts mxs mxl "is" xt
          where sees_M: "(P⇘wf⇙) ⊢ C sees M:Ts→T = (mxs,mxl,is,xt) in C"
          by (cases cs', (cases x, auto)+)
        with vn
        have "pc < length is"
          by (cases cs', (cases x, auto dest: sees_method_fun)+)
        from P_wf sees_M have "wt_method (P⇘wf⇙) C Ts T mxs mxl is xt (P⇘Φ⇙ C M)"
          by (auto dest: sees_wf_mdecl simp: wf_jvm_prog_phi_def wf_mdecl_def)
        with Putfield wt sees_M ‹pc < length is› show ?thesis
          by (fastforce simp: wt_method_def)
      qed
      then obtain ST1 STr' where "ST = ST1#STr' ∧ STr' ≠ []" by (cases ST, fastforce+)
      then obtain ST2 STr where [simp]: "ST = ST1#ST2#STr" by (cases STr', fastforce+)
      show ?thesis
      proof (cases x)
        case [simp]: None
        with wt
        have "Stk (length cs') (length ST - 2) ∈ Use P (sourcenode a)"
          (is "?stk_top ∈ ?Use")
          by (fastforce intro: Use_Putfield_Stk_Pred)
        with use_eq have "state_val s ?stk_top = state_val s' ?stk_top"
          by (simp del: state_val.simps)
        with ex_edge pred wt show ?thesis
          by (auto elim: JVM_CFG.cases)
      next
        case (Some x')
        with ex_edge show ?thesis
          by (auto elim: JVM_CFG.cases)
      qed
    next
      case [simp]: (Checkcast Cl)
      have "ST ≠ []"
      proof -
        from vn obtain T Ts mxs mxl "is" xt
          where sees_M: "(P⇘wf⇙) ⊢ C sees M:Ts→T = (mxs,mxl,is,xt) in C"
          by (cases cs', (cases x, auto)+)
        with vn
        have "pc < length is"
          by (cases cs', (cases x, auto dest: sees_method_fun)+)
        from P_wf sees_M have "wt_method (P⇘wf⇙) C Ts T mxs mxl is xt (P⇘Φ⇙ C M)"
          by (auto dest: sees_wf_mdecl simp: wf_jvm_prog_phi_def wf_mdecl_def)
        with Checkcast wt sees_M ‹pc < length is› show ?thesis
          by (fastforce simp: wt_method_def)
      qed
      then obtain ST1 STr where [simp]: "ST = ST1#STr" by (cases ST, fastforce+)
      show ?thesis
      proof (cases x)
        case [simp]: None
        from wt
        have "Stk (length cs') (stkLength P C M pc - Suc 0) ∈ Use P (sourcenode a)"
          (is "?stk_top ∈ ?Use")
          by (fastforce intro: Use_Checkcast_Stk)
        with use_eq
        have stk_top: "state_val s ?stk_top = state_val s' ?stk_top"
          by (simp del: state_val.simps)
        have "∀addr. HeapVar addr ∈ Use P (sourcenode a)"
          by (fastforce intro: Use_Checkcast_Heap)
        with use_eq
        have "∀addr. state_val s (HeapVar addr) = state_val s' (HeapVar addr)"
          by (simp del: state_val.simps)
        hence "h = h'"
          by (auto intro: ext)
        with ex_edge stk_top pred wt show ?thesis
          by (auto elim: JVM_CFG.cases)
      next
        case (Some x')
        with ex_edge show ?thesis
          by (auto elim: JVM_CFG.cases)
      qed
    next
      case [simp]: (Invoke M' n')
      have "length ST > n'"
      proof -
        from vn obtain T Ts mxs mxl "is" xt
          where sees_M: "(P⇘wf⇙) ⊢ C sees M:Ts→T = (mxs,mxl,is,xt) in C"
          by (cases cs', (cases x, auto)+)
        with vn
        have "pc < length is"
          by (cases cs', (cases x, auto dest: sees_method_fun)+)
        from P_wf sees_M have "wt_method (P⇘wf⇙) C Ts T mxs mxl is xt (P⇘Φ⇙ C M)"
          by (auto dest: sees_wf_mdecl simp: wf_jvm_prog_phi_def wf_mdecl_def)
        with Invoke wt sees_M ‹pc < length is› show ?thesis
          by (fastforce simp: wt_method_def)
      qed
      moreover obtain STn where "STn = take n' ST" by fastforce
      moreover obtain STs where "STs = ST ! n'" by fastforce
      moreover obtain STr where "STr = drop (Suc n') ST" by fastforce
      ultimately have [simp]:" ST = STn@STs#STr ∧ length STn = n'"
        by (auto simp: id_take_nth_drop)
      show ?thesis
      proof (cases x)
        case [simp]: None
        with wt
        have "Stk (length cs') (stkLength P C M pc - Suc n') ∈ Use P (sourcenode a)"
          (is "?stk_top ∈ ?Use")
          by (fastforce intro: Use_Invoke_Stk_Pred)
        with use_eq
        have stk_top: "state_val s ?stk_top = state_val s' ?stk_top"
          by (simp del: state_val.simps)
        have "∀addr. HeapVar addr ∈ Use P (sourcenode a)"
          by (fastforce intro: Use_Invoke_Heap_Pred)
        with use_eq
        have "∀addr. state_val s (HeapVar addr) = state_val s' (HeapVar addr)"
          by (simp del: state_val.simps)
        hence "h = h'"
          by (auto intro: ext)
        with ex_edge stk_top pred wt show ?thesis
          by (auto elim: JVM_CFG.cases)
      next
        case (Some x')
        with ex_edge show ?thesis
          by (auto elim: JVM_CFG.cases)
      qed
    next
      case Return
      with ex_edge show ?thesis
        by (auto elim: JVM_CFG.cases)
    next
      case Pop
      with ex_edge show ?thesis
        by (auto elim: JVM_CFG.cases)
    next
      case IAdd
      with ex_edge show ?thesis
        by (auto elim: JVM_CFG.cases)
    next
      case [simp]: (IfFalse b)
      show ?thesis
      proof (cases x)
        case [simp]: None
        have "Stk (length cs') (stkLength P C M pc - 1) ∈ Use P (sourcenode a)"
          (is "?stk_top ∈ ?Use")
          by (fastforce intro: Use_IfFalse_Stk)
        with use_eq
        have "state_val s ?stk_top = state_val s' ?stk_top"
          by (simp del: state_val.simps)
        with ex_edge pred wt show ?thesis
          by (auto elim: JVM_CFG.cases)
      next
        case (Some x')
        with ex_edge show ?thesis
          by (auto elim: JVM_CFG.cases)
      qed
    next
      case CmpEq
      with ex_edge show ?thesis
        by (auto elim: JVM_CFG.cases)
    next
      case (Goto i)
      with ex_edge show ?thesis
        by (auto elim: JVM_CFG.cases)
    next
      case [simp]: Throw
      have "ST ≠ []"
      proof -
        from vn obtain T Ts mxs mxl "is" xt
          where sees_M: "(P⇘wf⇙) ⊢ C sees M:Ts→T = (mxs,mxl,is,xt) in C"
          by (cases cs', (cases x, auto)+)
        with vn
        have "pc < length is"
          by (cases cs', (cases x, auto dest: sees_method_fun)+)
        from P_wf sees_M have "wt_method (P⇘wf⇙) C Ts T mxs mxl is xt (P⇘Φ⇙ C M)"
          by (auto dest: sees_wf_mdecl simp: wf_jvm_prog_phi_def wf_mdecl_def)
        with Throw wt sees_M ‹pc < length is› show ?thesis
          by (fastforce simp: wt_method_def)
      qed
      then obtain ST1 STr where [simp]: "ST = ST1#STr" by (cases ST, fastforce+)
      show ?thesis
      proof (cases x)
        case [simp]: None
        from wt
        have "Stk (length cs') (stkLength P C M pc - 1) ∈ Use P (sourcenode a)"
          (is "?stk_top ∈ ?Use")
          by (fastforce intro: Use_Throw_Stk)
        with use_eq
        have stk_top: "state_val s ?stk_top = state_val s' ?stk_top"
          by (simp del: state_val.simps)
        have "∀addr. HeapVar addr ∈ Use P (sourcenode a)"
          by (fastforce intro: Use_Throw_Heap)
        with use_eq
        have "∀addr. state_val s (HeapVar addr) = state_val s' (HeapVar addr)"
          by (simp del: state_val.simps)
        hence "h = h'"
          by (auto intro: ext)
        with ex_edge pred stk_top wt show ?thesis
          by (auto elim!: JVM_CFG.cases)
      next
        case (Some x')
        with ex_edge show ?thesis
          by (auto elim: JVM_CFG.cases)
      qed
    qed
  next
    case Entry
    with ex_edge pred show ?thesis
      by (auto elim: JVM_CFG.cases)
  qed
qed


lemma edge_no_Def_equal:
  "⟦ valid_edge (P, C0, Main) a;
     V ∉ Def P (sourcenode a) ⟧
  ⟹ state_val (transfer (kind a) s) V = state_val s V"
proof -
  assume ve:"valid_edge (P, C0, Main) a"
    and v_not_def: "V ∉ Def P (sourcenode a)"
  obtain h stk loc where [simp]: "(s::state) = (h, stk, loc)" by (cases s, blast)
  from ve have vn: "valid_node (P, C0, Main) (sourcenode a)"
    and ex_edge: "(P, C0, Main) ⊢ (sourcenode a)-kind a→(targetnode a)"
    by simp_all
  show "state_val (transfer (kind a) s) V = state_val s V"
  proof (cases "sourcenode a")
    case [simp]: (Node cs x)
    with ve have "cs ≠ []"
      by (cases x, auto elim: JVM_CFG.cases)
    then obtain C M pc cs' where [simp]: "cs = (C, M, pc)#cs'" by (cases cs, fastforce+)
    with vn obtain ST LT where wt: "((P⇘Φ⇙) C M ! pc) = ⌊(ST,LT)⌋"
      by (cases cs', (cases x, auto)+)
    show ?thesis
    proof (cases "instrs_of (P⇘wf⇙) C M ! pc")
      case [simp]: (Load nat)
      from ex_edge have "x = None"
        by (auto elim: JVM_CFG.cases)
      with v_not_def have "V ≠ Stk (length cs') (stkLength P C M pc)"
        by (auto intro!: Def_Load)
      with ex_edge show ?thesis
        by (auto elim!: JVM_CFG.cases, cases V, auto)
    next
      case [simp]: (Store nat)
      with ex_edge have "x = None"
        by (auto elim: JVM_CFG.cases)
      with v_not_def have "V ≠ Loc (length cs') nat"
        by (auto intro!: Def_Store)
      with ex_edge show ?thesis
        by (auto elim!: JVM_CFG.cases, cases V, auto)
    next
      case [simp]: (Push val)
      with ex_edge have "x = None"
        by (auto elim: JVM_CFG.cases)
      with v_not_def have "V ≠ Stk (length cs') (stkLength P C M pc)"
        by (auto intro!: Def_Push)
      with ex_edge show ?thesis
        by (auto elim!: JVM_CFG.cases, cases V, auto)
    next
      case [simp]: (New Cl)
      show ?thesis
      proof (cases x)
        case None
        with ex_edge show ?thesis
          by (auto elim: JVM_CFG.cases)
      next
        case (Some x')
        then obtain cs'' xf where [simp]: "x = ⌊(cs'',xf)⌋"
          by (cases x', fastforce)
        with ex_edge v_not_def show ?thesis
          apply (auto elim!: JVM_CFG.cases)
            apply (cases V, auto intro!: Def_New_Normal_Stk Def_New_Normal_Heap)
           by (cases V, auto intro!: Def_Exc_Stk)+
     qed
   next
     case [simp]: (Getfield F Cl)
     show ?thesis
     proof (cases x)
       case None
       with ex_edge show ?thesis
         by (auto elim: JVM_CFG.cases)
     next
       case (Some x')
       then obtain cs'' xf where [simp]: "x = ⌊(cs'',xf)⌋"
         by (cases x', fastforce)
       with ex_edge v_not_def show ?thesis
         apply (auto elim!: JVM_CFG.cases simp: split_beta)
           apply (cases V, auto intro!: Def_Getfield_Stk)
          by (cases V, auto intro!: Def_Exc_Stk)+
     qed
   next
     case [simp]: (Putfield Fd Cl)
     show ?thesis
     proof (cases x)
       case None
       with ex_edge show ?thesis
         by (auto elim: JVM_CFG.cases)
     next
       case (Some x')
       then obtain cs'' xf where [simp]: "x = ⌊(cs'',xf)⌋"
         by (cases x', fastforce)
       with ex_edge v_not_def show ?thesis
         apply (auto elim!: JVM_CFG.cases simp: split_beta)
           apply (cases V, auto intro!: Def_Putfield_Heap)
          by (cases V, auto intro!: Def_Exc_Stk)+
     qed
   next
     case [simp]: (Checkcast Cl)
     show ?thesis
     proof (cases x)
       case None
       with ex_edge show ?thesis
         by (auto elim: JVM_CFG.cases)
     next
       case (Some x')
       then obtain cs'' xf where [simp]: "x = ⌊(cs'',xf)⌋"
         by (cases x', fastforce)
       with ex_edge v_not_def show ?thesis
         apply (auto elim!: JVM_CFG.cases)
          by (cases V, auto intro!: Def_Exc_Stk)+
     qed
   next
     case [simp]: (Invoke M' n')
     show ?thesis
     proof (cases x)
       case None
       with ex_edge show ?thesis
         by (auto elim: JVM_CFG.cases)
     next
       case (Some x')
       then obtain cs'' xf where [simp]: "x = ⌊(cs'',xf)⌋"
         by (cases x', fastforce)
       from ex_edge v_not_def show ?thesis
         apply (auto elim!: JVM_CFG.cases)
           apply (cases V, auto intro!: Def_Invoke_Loc)
          by (cases V, auto intro!: Def_Exc_Stk)+
     qed
   next
     case Return
     with ex_edge v_not_def show ?thesis
       apply (auto elim!: JVM_CFG.cases)
       by (cases V, auto intro!: Def_Return_Stk)
   next
     case Pop
     with ex_edge show ?thesis
       by (auto elim: JVM_CFG.cases)
   next
     case IAdd
     with ex_edge v_not_def show ?thesis
       apply (auto elim!: JVM_CFG.cases)
       by (cases V, auto intro!: Def_IAdd_Stk)
   next
     case (IfFalse b)
     with ex_edge show ?thesis
       by (auto elim: JVM_CFG.cases)
   next
     case CmpEq
     with ex_edge v_not_def show ?thesis
       apply (auto elim!: JVM_CFG.cases)
       by (cases V, auto intro!: Def_CmpEq_Stk)
   next
     case (Goto i)
     with ex_edge show ?thesis
       by (auto elim: JVM_CFG.cases)
   next
     case [simp]: Throw
     show ?thesis
     proof (cases x)
       case None
       with ex_edge show ?thesis
         by (auto elim: JVM_CFG.cases)
     next
       case (Some x')
       then obtain cs'' xf where [simp]: "x = ⌊(cs'',xf)⌋"
         by (cases x', fastforce)
       from ex_edge v_not_def show ?thesis
         apply (auto elim!: JVM_CFG.cases)
          by (cases V, auto intro!: Def_Exc_Stk)+
      qed
    qed
  next
    case Entry
    with ex_edge show ?thesis
      by (auto elim: JVM_CFG.cases)
  qed
qed

interpretation JVM_CFG_wf: CFG_wf
  "sourcenode" "targetnode" "kind" "valid_edge prog" "(_Entry_)"
  "Def (fst prog)" "Use (fst prog)" "state_val"
  for prog
proof (unfold_locales)
  show "Def (fst prog) (_Entry_) = {} ∧ Use (fst prog) (_Entry_) = {}"
    by (auto elim: Def.cases Use.cases)
next
  fix a V s
  assume ve:"valid_edge prog a"
    and v_not_def: "V ∉ Def (fst prog) (sourcenode a)"
  thus "state_val (transfer (kind a) s) V = state_val s V"
    by -(cases prog,
    rule edge_no_Def_equal [of "fst prog" "fst (snd prog)" "snd (snd prog)"], auto)
next
  fix a s s'
  assume ve: "valid_edge prog a"
    and use_eq: "∀V∈Use (fst prog) (sourcenode a). state_val s V = state_val s' V"
  thus "∀V∈Def (fst prog) (sourcenode a).
    state_val (transfer (kind a) s) V = state_val (transfer (kind a) s') V"
    by -(cases prog,
      rule edge_transfer_uses_only_Use [of "fst prog" "fst(snd prog)" "snd(snd prog)"], auto)
next
  fix a s s'
  assume ve: "valid_edge prog a"
    and pred: "pred (kind a) s"
    and use_eq: "∀V∈Use (fst prog) (sourcenode a). state_val s V = state_val s' V"
  thus "pred (kind a) s'"
    by -(cases prog,
      rule CFG_edge_Uses_pred_equal [of "fst prog" "fst(snd prog)" "snd(snd prog)"], auto)
next
  fix a a'
  assume ve_a: "valid_edge prog a"
    and ve_a': "valid_edge prog a'"
    and src_eq: "sourcenode a = sourcenode a'"
    and trg_neq: "targetnode a ≠ targetnode a'"
  hence "prog ⊢ (sourcenode a)-kind a→(targetnode a)"
    and "prog ⊢ (sourcenode a')-kind a'→(targetnode a')"
    by simp_all
  with src_eq trg_neq
  show "∃Q Q'. kind a = (Q)⇩√ ∧ kind a' = (Q')⇩√ ∧ (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))"
    apply (cases prog, auto)
    apply (erule JVM_CFG.cases, erule_tac [!] JVM_CFG.cases)
    (* This takes veeery long! *)
    by simp_all
qed

interpretation JVM_CFGExit_wf: CFGExit_wf
  "sourcenode" "targetnode" "kind" "valid_edge prog" "(_Entry_)"
  "Def (fst prog)" "Use (fst prog)" "state_val" "(_Exit_)"
proof
  show "Def (fst prog) (_Exit_) = {} ∧ Use (fst prog) (_Exit_) = {}"
    by(fastforce elim:Def.cases Use.cases)
qed

  
end