Theory JVMCFG_wf

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

inductive_set Def :: "wf_jvmprog  cfg_node  var set"
  for P :: "wf_jvmprog"
  and n :: "cfg_node"
where
  Def_Main_Heap:
  "n = (ClassMain P, MethodMain P, 0, Return)
   Heap  Def P n"
| Def_Main_Exception:
  "n = (ClassMain P, MethodMain P, 0, Return)
   Exception  Def P n"
| Def_Main_Stack_0:
  "n = (ClassMain P, MethodMain P, 0, Return)
   Stack 0  Def P n"
| Def_Load:
  " n = (C, M, pc, Enter);
  C  ClassMain P;
  instrs_of (PROG P) C M ! pc = Load idx;
  i = stkLength (P, C, M) pc
   Stack i  Def P n"
| Def_Store:
  " n = (C, M, pc, Enter);
  C  ClassMain P;
  instrs_of (PROG P) C M ! pc = Store idx 
   Local idx  Def P n"
| Def_Push:
  " n = (C, M, pc, Enter);
  C  ClassMain P;
  instrs_of (PROG P) C M ! pc = Push v;
  i = stkLength (P, C, M) pc 
   Stack i  Def P n"
| Def_IAdd:
  " n = (C, M, pc, Enter);
  C  ClassMain P;
  instrs_of (PROG P) C M ! pc = IAdd;
  i = stkLength (P, C, M) pc - 2 
   Stack i  Def P n"
| Def_CmpEq:
  " n = (C, M, pc, Enter);
  C  ClassMain P;
  instrs_of (PROG P) C M ! pc = CmpEq;
  i = stkLength (P, C, M) pc - 2 
   Stack i  Def P n"
| Def_New_Heap:
  " n = (C, M, pc, Normal);
  C  ClassMain P;
  instrs_of (PROG P) C M ! pc = New Cl 
   Heap  Def P n"
| Def_New_Stack:
  " n = (C, M, pc, Normal);
  C  ClassMain P;
  instrs_of (PROG P) C M ! pc = New Cl;
  i = stkLength (P, C, M) pc 
   Stack i  Def P n"
| Def_Exception:
  " n = (C, M, pc, Exceptional pco nt);
  C  ClassMain P 
   Exception  Def P n"
| Def_Exception_handle:
  " n = (C, M, pc, Exceptional pc' Enter);
  C  ClassMain P;
  i = stkLength (P, C, M) pc' - 1 
   Stack i  Def P n"
| Def_Exception_handle_return:
  " n = (C, M, pc, Exceptional pc' Return);
  C  ClassMain P;
  i = stkLength (P, C, M) pc' - 1 
   Stack i  Def P n"
| Def_Getfield:
  " n = (C, M, pc, Normal);
  C  ClassMain P;
  instrs_of (PROG P) C M ! pc = Getfield Cl Fd;
  i = stkLength (P, C, M) pc - 1 
   Stack i  Def P n"
| Def_Putfield:
  " n = (C, M, pc, Normal);
  C  ClassMain P;
  instrs_of (PROG P) C M ! pc = Putfield Cl Fd 
   Heap  Def P n"
| Def_Invoke_Return_Heap:
  " n = (C, M, pc, Return);
  C  ClassMain P;
  instrs_of (PROG P) C M ! pc = Invoke M' n' 
   Heap  Def P n"
| Def_Invoke_Return_Exception:
  " n = (C, M, pc, Return);
  C  ClassMain P;
  instrs_of (PROG P) C M ! pc = Invoke M' n' 
   Exception  Def P n"
| Def_Invoke_Return_Stack:
  " n = (C, M, pc, Return);
  C  ClassMain P;
  instrs_of (PROG P) C M ! pc = Invoke M' n';
  i = stkLength (P, C, M) (Suc pc) - 1 
   Stack i  Def P n"
| Def_Invoke_Call_Heap:
  " n = (C, M, None, Enter);
  C  ClassMain P 
   Heap  Def P n"
| Def_Invoke_Call_Local:
  " n = (C, M, None, Enter);
  C  ClassMain P;
  i < locLength (P, C, M) 0 
   Local i  Def P n"
| Def_Return:
  " n = (C, M, pc, Enter);
  C  ClassMain P;
  instrs_of (PROG P) C M ! pc = instr.Return 
   Stack 0  Def P n"

inductive_set Use :: "wf_jvmprog  cfg_node  var set"
  for P :: "wf_jvmprog"
  and n :: "cfg_node"
where
  Use_Main_Heap:
  "n = (ClassMain P, MethodMain P, 0, Normal)
   Heap  Use P n"
| Use_Load:
  " n = (C, M, pc, Enter);
  C  ClassMain P;
  instrs_of (PROG P) C M ! pc = Load idx 
   Local idx  Use P n"
| Use_Enter_Stack:
  " n = (C, M, pc, Enter);
  C  ClassMain P;
  case (instrs_of (PROG P) C M ! pc)
    of Store n'  d = 1
    | Getfield F Cl  d = 1
    | Putfield F Cl  d = 2
    | Checkcast Cl  d = 1
    | Invoke M' n'  d = Suc n'
    | IAdd  d  {1, 2}
    | IfFalse i  d = 1
    | CmpEq  d  {1 , 2}
    | Throw  d = 1
    | instr.Return  d = 1
    | _  False;
  i = stkLength (P, C, M) pc - d 
   Stack i  Use P n"
| Use_Enter_Local:
  " n = (C, M, pc, Enter);
  C  ClassMain P;
  instrs_of (PROG P) C M ! pc = Load n' 
   Local n'  Use P n"
| Use_Enter_Heap:
  " n = (C, M, pc, Enter);
  C  ClassMain P;
  case (instrs_of (PROG P) C M ! pc)
    of New Cl  True
    | Checkcast Cl  True
    | Throw  True
    | _  False 
   Heap  Use P n"
| Use_Normal_Heap:
  " n = (C, M, pc, Normal);
  C  ClassMain P;
  case (instrs_of (PROG P) C M ! pc)
    of New Cl  True
    | Getfield F Cl  True
    | Putfield F Cl  True
    | Invoke M' n'  True
    | _  False 
   Heap  Use P n"
| Use_Normal_Stack:
  " n = (C, M, pc, Normal);
  C  ClassMain P;
  case (instrs_of (PROG P) C M ! pc)
    of Getfield F Cl  d = 1
    | Putfield F Cl  d  {1, 2}
    | Invoke M' n'  d > 0  d  Suc n'
    | _  False;
  i = stkLength (P, C, M) pc - d 
   Stack i  Use P n"
| Use_Return_Heap:
  " n = (C, M, pc, Return);
  instrs_of (PROG P) C M ! pc = Invoke M' n'  C = ClassMain P 
   Heap  Use P n"
| Use_Return_Stack:
  " n = (C, M, pc, Return);
  (instrs_of (PROG P) C M ! pc = Invoke M' n'  i = stkLength (P, C, M) (Suc pc) - 1) 
  (C = ClassMain P  i = 0) 
   Stack i  Use P n"
| Use_Return_Exception:
  " n = (C, M, pc, Return);
  instrs_of (PROG P) C M ! pc = Invoke M' n'  C = ClassMain P 
   Exception  Use P n"
| Use_Exceptional_Stack:
  " n = (C, M, pc, Exceptional opc' nt);
  case (instrs_of (PROG P) C M ! pc)
    of Throw  True
    | _  False;
  i = stkLength (P, C, M) pc - 1 
   Stack i  Use P n"
| Use_Exceptional_Exception:
  " n = (C, M, pc, Exceptional pc' Return);
  instrs_of (PROG P) C M ! pc = Invoke M' n' 
   Exception  Use P n"
| Use_Method_Leave_Exception:
  " n = (C, M, None, Return);
  C  ClassMain P 
   Exception  Use P n"
| Use_Method_Leave_Heap:
  " n = (C, M, None, Return);
  C  ClassMain P 
   Heap  Use P n"
| Use_Method_Leave_Stack:
  " n = (C, M, None, Return);
  C  ClassMain P 
   Stack 0  Use P n"
| Use_Method_Entry_Heap:
  " n = (C, M, None, Enter);
  C  ClassMain P 
   Heap  Use P n"
| Use_Method_Entry_Local:
  " n = (C, M, None, Enter);
  C  ClassMain P;
  i < locLength (P, C, M) 0 
   Local i  Use P n"

fun ParamDefs :: "wf_jvmprog  cfg_node  var list"
where
  "ParamDefs P (C, M, pc, Return) = [Heap, Stack (stkLength (P, C, M) (Suc pc) - 1), Exception]"
  | "ParamDefs P (C, M, opc, nt) = []"

function ParamUses :: "wf_jvmprog  cfg_node  var set list"
where
  "ParamUses P (ClassMain P, MethodMain P, 0, Normal) = [{Heap},{}]"
  |
  "M  MethodMain P  opc  0  nt  Normal
   ParamUses P (ClassMain P, M, opc, nt) = []"
  |
  "C  ClassMain P
   ParamUses P (C, M, opc, nt) = (case opc of None  []
  | pc  (case nt of Normal  (case (instrs_of (PROG P) C M ! pc) of
      Invoke M' n  (
          {Heap} # rev (map (λn. {Stack (stkLength (P, C, M) pc - (Suc n))}) [0..<n + 1])
      )
      | _  [])
    | _  []
    )
  )"
  by atomize_elim auto
termination by lexicographic_order

lemma in_set_ParamDefsE:
  " V  set (ParamDefs P n);
  C M pc.  n = (C, M, pc, Return);
         V  {Heap, Stack (stkLength (P, C, M) (Suc pc) - 1), Exception}   thesis 
   thesis"
  by (cases "(P, n)" rule: ParamDefs.cases) auto

lemma in_set_ParamUsesE:
  assumes V_in_ParamUses: "V  (set (ParamUses P n))"
  obtains "n = (ClassMain P, MethodMain P, 0, Normal)" and "V = Heap"
  | C M pc M' n' i where "n = (C, M, pc, Normal)" and "instrs_of (PROG P) C M ! pc = Invoke M' n'"
    and "V = Heap  V = Stack (stkLength (P, C, M) pc - Suc i)" and "i < Suc n'" and "C  ClassMain P"
proof (cases "(P, n)" rule: ParamUses.cases)
  case 1 with V_in_ParamUses that show ?thesis by clarsimp
next
  case 2 with V_in_ParamUses that show ?thesis by clarsimp
next
  case (3 C P M pc nt)
  with V_in_ParamUses that show ?thesis
    using [[simproc del: list_to_set_comprehension]]
    by (cases nt, auto) (rename_tac a b, case_tac "instrs_of (PROG P) C M ! a", simp_all, fastforce)
qed

lemma sees_method_fun_wf:
  assumes "PROG P  D sees M': TsT = (mxs, mxl0, is, xt) in D"
  and "(D, D', fs, ms)  set (PROG P)"
  and "(M', Ts', T', mxs', mxl0', is', xt')  set ms"
  shows "Ts = Ts'  T = T'  mxs = mxs'  mxl0 = mxl0'  is = is'  xt = xt'"
proof -
  from distinct_class_names [of P] (D, D', fs, ms)  set (PROG P)
  have "class (PROG P) D = (D', fs, ms)"
    by (fastforce intro: map_of_SomeI simp: class_def)
  moreover with distinct_method_names have "distinct_fst ms"
    by fastforce
  ultimately show ?thesis using
    PROG P  D sees M': TsT = (mxs, mxl0, is, xt) in D
    (M', Ts', T', mxs', mxl0', is', xt')  set ms
    by (fastforce dest: visible_method_exists map_of_SomeD distinct_fst_isin_same_fst
      simp: distinct_fst_is_distinct_fst)
qed

interpretation JVMCFG_wf:
  CFG_wf  "sourcenode" "targetnode" "kind" "valid_edge (P, C0, Main)"
  "(ClassMain P, MethodMain P, None, Enter)"
  "(λ(C, M, pc, type). (C, M))" "get_return_edges P"
  "((ClassMain P, MethodMain P),[],[]) # procs (PROG P)"
  "(ClassMain P, MethodMain P)"
  "Def P" "Use P" "ParamDefs P" "ParamUses P"
  for P C0 Main
proof (unfold_locales)
  show "Def P (ClassMain P, MethodMain P, None, Enter) = {} 
    Use P (ClassMain P, MethodMain P, None, Enter) = {}"
    by (fastforce elim: Def.cases Use.cases)
next
  fix a Q r p fs ins outs
  assume "valid_edge (P, C0, Main) a"
    and "kind a = Q:r↪⇘pfs"
    and params: "(p, ins, outs)  set (((ClassMain P, MethodMain P), [], []) # procs (PROG P))"
  hence "(P, C0, Main)  sourcenode a -Q:r↪⇘pfs targetnode a"
    by (simp add: valid_edge_def)
  from this params show "length (ParamUses P (sourcenode a)) = length ins"
  proof cases
    case Main_Call
    with params show ?thesis
      by auto (erule in_set_procsE, auto dest: sees_method_idemp sees_method_fun)
  next
    case (CFG_Invoke_Call C M pc M' n ST LT D' Ts T mxs mxl0 "is" xt D Q' paramDefs)
    hence [simp]: "Q' = Q" and [simp]: "r = (C, M, pc)" and [simp]: "p = (D, M')"
      and [simp]: "fs = paramDefs"
      by simp_all
    from CFG_Invoke_Call obtain T' mxs' mpc' xt' where
      "PROG P,T',mxs',mpc',xt'  instrs_of (PROG P) C M ! pc,pc :: TYPING P C M"
      by (blast dest: reachable_node_impl_wt_instr)
    moreover from PROG P  D' sees M': TsT = (mxs, mxl0, is, xt) in D
    have "PROG P  D sees M': TsT = (mxs, mxl0, is, xt) in D"
      by -(drule sees_method_idemp)
    with params have "PROG P  D sees M': TsT=(mxs, mxl0, is, xt) in D"
      and "ins = Heap # map Local [0..<Suc (length Ts)]"
      by (fastforce elim: in_set_procsE dest: sees_method_fun)+
    ultimately show ?thesis using CFG_Invoke_Call
      by (fastforce dest: sees_method_fun list_all2_lengthD simp: min_def)
  qed simp_all
next
  fix a
  assume "valid_edge (P, C0, Main) a"
  thus "distinct (ParamDefs P (targetnode a))"
    by (clarsimp simp: valid_edge_def) (erule JVMCFG.cases, auto)
next
  fix a Q' p f' ins outs
  assume "valid_edge (P, C0, Main) a"
    and "kind a = Q'↩⇘pf'"
    and params: "(p, ins, outs)  set (((ClassMain P, MethodMain P), [], []) # procs (PROG P))"
  hence "(P, C0, Main)  sourcenode a -Q'↩⇘pf' targetnode a"
    by (simp add: valid_edge_def)
  from this params
  show "length (ParamDefs P (targetnode a)) = length outs"
    by cases (auto elim: in_set_procsE)
next
  fix n V
  assume params: "V  set (ParamDefs P n)"
    and vn: "CFG.valid_node sourcenode targetnode (valid_edge (P, C0, Main)) n"
  then obtain ek n'
    where ve:"valid_edge (P, C0, Main) (n, ek, n')  valid_edge (P, C0, Main) (n', ek, n)"
    by (fastforce simp: JVMCFG_Interpret.valid_node_def)
  from params obtain C M pc where [simp]: "n = (C, M, pc, Return)"
    and V: "V  {Heap, Stack (stkLength (P, C, M) (Suc pc) - 1), Exception}"
    by (blast elim: in_set_ParamDefsE)
  from ve show "V  Def P n"
  proof
    assume "valid_edge (P, C0, Main) (n, ek, n')"
    thus ?thesis unfolding valid_edge_def
    proof cases
      case Main_Return_to_Exit with V show ?thesis
        by (auto intro: Def_Main_Heap Def_Main_Stack_0 Def_Main_Exception simp: stkLength_def)
    next
      case CFG_Invoke_Return_Check_Normal with V show ?thesis
        by (fastforce intro: Def_Invoke_Return_Heap
          Def_Invoke_Return_Stack Def_Invoke_Return_Exception)
    next
      case CFG_Invoke_Return_Check_Exceptional with V show ?thesis
        by (fastforce intro: Def_Invoke_Return_Heap
          Def_Invoke_Return_Stack Def_Invoke_Return_Exception)
    next
      case CFG_Invoke_Return_Exceptional_prop with V show ?thesis
        by (fastforce intro: Def_Invoke_Return_Heap
          Def_Invoke_Return_Stack Def_Invoke_Return_Exception)
    qed simp_all
  next
    assume "valid_edge (P, C0, Main) (n', ek, n)"
    thus ?thesis unfolding valid_edge_def
    proof cases
      case Main_Call_LFalse with V show ?thesis
        by (auto intro: Def_Main_Heap Def_Main_Stack_0 Def_Main_Exception simp: stkLength_def)
    next
      case CFG_Invoke_False with V show ?thesis
        by (fastforce intro: Def_Invoke_Return_Heap
          Def_Invoke_Return_Stack Def_Invoke_Return_Exception)
    next
      case CFG_Return_from_Method with V show ?thesis
        by (fastforce elim!: JVMCFG.cases intro!: Def_Main_Stack_0
          intro: Def_Main_Heap Def_Main_Exception Def_Invoke_Return_Heap
          Def_Invoke_Return_Exception Def_Invoke_Return_Stack simp: stkLength_def)
    qed simp_all
  qed
next
  fix a Q r p fs ins outs V
  assume ve: "valid_edge (P, C0, Main) a"
    and kind: "kind a = Q:r↪⇘pfs"
    and params: "(p, ins, outs)  set (((ClassMain P, MethodMain P), [], []) # procs (PROG P))"
    and V: "V  set ins"
  from params V obtain D fs ms Ts T mb where "class (PROG P) (fst p) = (D, fs, ms)"
    and "method": "PROG P  (fst p) sees (snd p): TsT = mb in (fst p)"
    and ins: "ins = Heap # map Local [0..<Suc (length Ts)]"
    by (cases p) (fastforce elim: in_set_procsE)
  from ve kind show "V  Def P (targetnode a)" unfolding valid_edge_def
  proof cases
    case (Main_Call T' mxs mxl0 "is" xt D' initParams)
    with kind have "PROG P  D' sees Main: []T' = (mxs, mxl0, is, xt) in D'"
      and [simp]: "p = (D', Main)"
      by (auto dest: sees_method_idemp)
    with "method" have [simp]: "Ts = []" and [simp]: "T' = T" and [simp]: "mb = (mxs, mxl0, is, xt)"
      by (fastforce dest: sees_method_fun)+
    from Main_Call ins V show ?thesis
      by (fastforce intro!: Def_Invoke_Call_Heap Def_Invoke_Call_Local
        dest: sees_method_idemp wt_jvm_prog_impl_wt_start[OF wf_jvmprog_is_wf_typ]
        simp: locLength_def wt_start_def)
  next
    case (CFG_Invoke_Call C M pc M' n ST LT D' Ts' T' mxs mxl0 "is" xt D'')
    with kind have "PROG P  D'' sees M': Ts'T' = (mxs, mxl0, is, xt) in D''"
      and [simp]: "p = (D'', M')"
      by (auto dest: sees_method_idemp)
    with "method" have [simp]: "Ts' = Ts" and [simp]: "T' = T" and [simp]: "mb = (mxs, mxl0, is, xt)"
      by (fastforce dest: sees_method_fun)+
    from CFG_Invoke_Call ins V show ?thesis
      by (fastforce intro!: Def_Invoke_Call_Local Def_Invoke_Call_Heap
        dest: sees_method_idemp wt_jvm_prog_impl_wt_start[OF wf_jvmprog_is_wf_typ] list_all2_lengthD
        simp: locLength_def min_def wt_start_def)
  qed simp_all
next
  fix a Q r p fs
  assume "valid_edge (P, C0, Main) a" and "kind a = Q:r↪⇘pfs"
  thus "Def P (sourcenode a) = {}" unfolding valid_edge_def
    by cases (auto elim: Def.cases)
next
  fix n V
  assume "CFG.valid_node sourcenode targetnode (valid_edge (P, C0, Main)) n"
    and V: "V  (set (ParamUses P n))"
  then obtain ek n'
    where ve:"valid_edge (P, C0, Main) (n, ek, n')  valid_edge (P, C0, Main) (n', ek, n)"
    by (fastforce simp: JVMCFG_Interpret.valid_node_def)
  from V obtain C M pc M' n'' i where
    V: "n = (ClassMain P, MethodMain P, 0, Normal)  V = Heap 
    n = (C, M, pc, Normal)  instrs_of (PROG P) C M ! pc = Invoke M' n'' 
      (V = Heap  V = Stack (stkLength (P, C, M) pc - Suc i))  i < Suc n''  C  ClassMain P"
    by -(erule in_set_ParamUsesE, fastforce+)
  from ve show "V  Use P n"
  proof
    assume "valid_edge (P, C0, Main) (n, ek, n')"
    from this V show ?thesis unfolding valid_edge_def
    proof cases
      case Main_Call_LFalse with V show ?thesis by (fastforce intro: Use_Main_Heap)
    next
      case Main_Call with V show ?thesis by (fastforce intro: Use_Main_Heap)
    next
      case CFG_Invoke_Call with V show ?thesis
        by (fastforce intro: Use_Normal_Heap Use_Normal_Stack [where d="Suc i"])
    next
      case CFG_Invoke_False with V show ?thesis
        by (fastforce intro: Use_Normal_Heap Use_Normal_Stack [where d="Suc i"])
    qed simp_all
  next
    assume "valid_edge (P, C0, Main) (n', ek, n)"
    from this V show ?thesis unfolding valid_edge_def
    proof cases
      case Main_to_Call with V show ?thesis by (fastforce intro: Use_Main_Heap)
    next
      case CFG_Invoke_Check_NP_Normal with V show ?thesis
        by (fastforce intro: Use_Normal_Heap Use_Normal_Stack [where d="Suc i"])
    qed simp_all
  qed
next
  fix a Q p f ins outs V
  assume "valid_edge (P, C0, Main) a"
    and "kind a = Q↩⇘pf"
    and "(p, ins, outs)  set (((ClassMain P, MethodMain P), [], []) # procs (PROG P))"
    and "V  set outs"
  thus "V  Use P (sourcenode a)" unfolding valid_edge_def
    by (cases, simp_all)
  (fastforce elim: in_set_procsE
    intro: Use_Method_Leave_Heap Use_Method_Leave_Stack Use_Method_Leave_Exception)
next
  fix a V s
  assume ve: "valid_edge (P, C0, Main) a"
    and V_notin_Def: "V  Def P (sourcenode a)"
    and ik: "intra_kind (kind a)"
    and pred: "JVMCFG_Interpret.pred (kind a) s"
  show "JVMCFG_Interpret.state_val
    (CFG.transfer (((ClassMain P, MethodMain P), [], []) # procs (PROG P)) (kind a) s) V
    = JVMCFG_Interpret.state_val s V"
  proof (cases s)
    case Nil
    thus ?thesis by simp
  next
    case [simp]: Cons
    with ve V_notin_Def ik pred show ?thesis unfolding valid_edge_def
    proof cases
      case CFG_Load with V_notin_Def show ?thesis by (fastforce intro: Def_Load)
    next case CFG_Store with V_notin_Def show ?thesis by (fastforce intro: Def_Store)
    next case CFG_Push with V_notin_Def show ?thesis by (fastforce intro: Def_Push)
    next case CFG_IAdd with V_notin_Def show ?thesis by (fastforce intro: Def_IAdd)
    next case CFG_CmpEq with V_notin_Def show ?thesis by (fastforce intro: Def_CmpEq)
    next case CFG_New_Update with V_notin_Def show ?thesis
        by (fastforce intro: Def_New_Heap Def_New_Stack)
    next case CFG_New_Exceptional_prop with V_notin_Def show ?thesis
        by (fastforce intro: Def_Exception)
    next case CFG_New_Exceptional_handle with V_notin_Def show ?thesis
        by (fastforce intro: Def_Exception Def_Exception_handle)
    next case CFG_Getfield_Update with V_notin_Def show ?thesis
        by (fastforce intro: Def_Getfield split: prod.split)
    next case CFG_Getfield_Exceptional_prop with V_notin_Def show ?thesis
        by (fastforce intro: Def_Exception)
    next case CFG_Getfield_Exceptional_handle with V_notin_Def show ?thesis
        by (fastforce intro: Def_Exception Def_Exception_handle)
    next case CFG_Putfield_Update with V_notin_Def show ?thesis
        by (fastforce intro: Def_Putfield split: prod.split)
    next case CFG_Putfield_Exceptional_prop with V_notin_Def show ?thesis
        by (fastforce intro: Def_Exception)
    next case CFG_Putfield_Exceptional_handle with V_notin_Def show ?thesis
        by (fastforce intro: Def_Exception Def_Exception_handle)
    next case CFG_Checkcast_Exceptional_prop with V_notin_Def show ?thesis
        by (fastforce intro: Def_Exception)
    next case CFG_Checkcast_Exceptional_handle with V_notin_Def show ?thesis
        by (fastforce intro: Def_Exception Def_Exception_handle)
    next case CFG_Throw_prop with V_notin_Def show ?thesis by (fastforce intro: Def_Exception)
    next case CFG_Throw_handle with V_notin_Def show ?thesis
        by (fastforce intro: Def_Exception Def_Exception_handle)
    next case CFG_Invoke_NP_prop with V_notin_Def show ?thesis by (fastforce intro: Def_Exception)
    next case CFG_Invoke_NP_handle with V_notin_Def show ?thesis
        by (fastforce intro: Def_Exception Def_Exception_handle)
    next case CFG_Invoke_Return_Exceptional_handle with V_notin_Def show ?thesis
        by (fastforce intro: Def_Exception_handle_return Def_Exception)
    next case CFG_Return with V_notin_Def show ?thesis by (fastforce intro: Def_Return)
    qed (simp_all add: intra_kind_def)
  qed
next
  fix a s s'
  assume ve: "valid_edge (P, C0, Main) a"
    and use_Eq: "VUse P (sourcenode a). JVMCFG_Interpret.state_val s V
    = JVMCFG_Interpret.state_val s' V"
    and ik: "intra_kind (kind a)"
    and pred_s: "JVMCFG_Interpret.pred (kind a) s"
    and pred_s': "JVMCFG_Interpret.pred (kind a) s'"
  then obtain cfs C M pc cs cfs' C' M' pc' cs' where [simp]: "s = (cfs, (C, M, pc)) # cs"
    and [simp]: "s' = (cfs', (C', M', pc')) # cs'"
    by (cases s, fastforce) (cases s', fastforce+)
  from ve show "VDef P (sourcenode a).
             JVMCFG_Interpret.state_val
              (CFG.transfer (((ClassMain P, MethodMain P), [], []) # procs (PROG P)) (kind a) s) V =
             JVMCFG_Interpret.state_val
              (CFG.transfer (((ClassMain P, MethodMain P), [], []) # procs (PROG P)) (kind a) s') V"
    unfolding valid_edge_def
  proof cases
    case Main_Call with ik show ?thesis by (simp add: intra_kind_def)
  next case Main_Return_to_Exit with use_Eq show ?thesis
      by (fastforce elim: Def.cases intro: Use_Return_Heap Use_Return_Exception Use_Return_Stack)
  next case Method_LFalse with use_Eq show ?thesis
      by (fastforce elim: Def.cases intro: Use_Method_Entry_Heap Use_Method_Entry_Local) 
  next case Method_LTrue with use_Eq show ?thesis
      by (fastforce elim: Def.cases intro: Use_Method_Entry_Heap Use_Method_Entry_Local)
  next case CFG_Load with use_Eq show ?thesis
      by (fastforce elim: Def.cases intro: Use_Enter_Local)
  next case CFG_Store with use_Eq show ?thesis
      by (fastforce elim: Def.cases intro: Use_Enter_Stack)
  next case (CFG_IAdd C M pc)
    hence "Stack (stkLength (P, C, M) pc - 1)  Use P (sourcenode a)"
      and "Stack (stkLength (P, C, M) pc - 2)  Use P (sourcenode a)"
      by (fastforce intro: Use_Enter_Stack)+
    with use_Eq CFG_IAdd show ?thesis by (auto elim!: Def.cases)
  next case (CFG_CmpEq C  M pc)
    hence "Stack (stkLength (P, C, M) pc - 1)  Use P (sourcenode a)"
      and "Stack (stkLength (P, C, M) pc - 2)  Use P (sourcenode a)"
      by (fastforce intro: Use_Enter_Stack)+
    with use_Eq CFG_CmpEq show ?thesis by (auto elim!: Def.cases)
  next case CFG_New_Update
    hence "Heap  Use P (sourcenode a)" by (fastforce intro: Use_Normal_Heap)
    with use_Eq CFG_New_Update show ?thesis by (fastforce elim: Def.cases)
  next case (CFG_Getfield_Update C  M pc)
    hence "Heap  Use P (sourcenode a)"
      and "Stack (stkLength (P, C, M) pc - 1)  Use P (sourcenode a)"
      by (fastforce intro: Use_Normal_Heap Use_Normal_Stack)+
    with use_Eq CFG_Getfield_Update show ?thesis by (auto elim!: Def.cases split: prod.split)
  next case (CFG_Putfield_Update C  M pc)
    hence "Heap  Use P (sourcenode a)"
      and "Stack (stkLength (P, C, M) pc - 1)  Use P (sourcenode a)"
      and "Stack (stkLength (P, C, M) pc - 2)  Use P (sourcenode a)"
      by (fastforce intro: Use_Normal_Heap Use_Normal_Stack)+
    with use_Eq CFG_Putfield_Update show ?thesis by (auto elim!: Def.cases split: prod.split)
  next case (CFG_Throw_prop C  M pc)
    hence "Stack (stkLength (P, C, M) pc - 1)  Use P (sourcenode a)"
      by (fastforce intro: Use_Exceptional_Stack)
    with use_Eq CFG_Throw_prop show ?thesis by (fastforce elim: Def.cases)
  next case (CFG_Throw_handle C  M pc)
    hence "Stack (stkLength (P, C, M) pc - 1)  Use P (sourcenode a)"
      by (fastforce intro: Use_Exceptional_Stack)
    with use_Eq CFG_Throw_handle show ?thesis by (fastforce elim: Def.cases)
  next case CFG_Invoke_Call with ik show ?thesis by (simp add: intra_kind_def)
  next case CFG_Invoke_Return_Check_Normal with use_Eq show ?thesis
      by (fastforce elim: Def.cases intro: Use_Return_Heap Use_Return_Exception Use_Return_Stack)
  next case CFG_Invoke_Return_Check_Exceptional with use_Eq show ?thesis
      by (fastforce elim: Def.cases intro: Use_Return_Heap Use_Return_Exception Use_Return_Stack)
  next case CFG_Invoke_Return_Exceptional_handle with use_Eq show ?thesis
      by (fastforce elim: Def.cases intro: Use_Exceptional_Exception)
  next case CFG_Invoke_Return_Exceptional_prop with use_Eq show ?thesis
      by (fastforce elim: Def.cases intro: Use_Return_Heap Use_Return_Exception Use_Return_Stack)
  next case CFG_Return with use_Eq show ?thesis
      by (fastforce elim!: Def.cases intro: Use_Enter_Stack)
  next case CFG_Return_from_Method with ik show ?thesis by (simp add: intra_kind_def)
  qed (fastforce elim: Def.cases)+
next
  fix a s s'
  assume ve: "valid_edge (P, C0, Main) a"
    and pred: "JVMCFG_Interpret.pred (kind a) s"
    and "snd (hd s) = snd (hd s')"
    and use_Eq: "VUse P (sourcenode a).
           JVMCFG_Interpret.state_val s V = JVMCFG_Interpret.state_val s' V"
    and "length s = length s'"
  then obtain cfs C M pc cs cfs' cs' where [simp]: "s = (cfs, (C, M, pc)) # cs"
    and [simp]: "s' = (cfs', (C, M, pc)) # cs'" and length_cs: "length cs = length cs'"
    by (cases s, fastforce) (cases s', fastforce+)
  from ve pred show "JVMCFG_Interpret.pred (kind a) s'"
    unfolding valid_edge_def
  proof cases
    case Main_Call_LFalse with pred show ?thesis by simp
  next case Main_Call with pred use_Eq show ?thesis by simp
  next case Method_LTrue with pred use_Eq show ?thesis by simp
  next case CFG_Goto with pred use_Eq show ?thesis by simp
  next case (CFG_IfFalse_False C  M pc)
    hence "Stack (stkLength (P, C, M) pc - 1)  Use P (sourcenode a)"
      by (fastforce intro: Use_Enter_Stack)
    with use_Eq CFG_IfFalse_False pred show ?thesis by fastforce
  next case (CFG_IfFalse_True C  M pc)
    hence "Stack (stkLength (P, C, M) pc - 1)  Use P (sourcenode a)"
      by (fastforce intro: Use_Enter_Stack)
    with pred use_Eq CFG_IfFalse_True show ?thesis by fastforce
  next case CFG_New_Check_Normal
    hence "Heap  Use P (sourcenode a)"
      by (fastforce intro: Use_Enter_Heap)
    with pred use_Eq CFG_New_Check_Normal show ?thesis by fastforce
  next case CFG_New_Check_Exceptional 
    hence "Heap  Use P (sourcenode a)"
      by (fastforce intro: Use_Enter_Heap)
    with pred use_Eq CFG_New_Check_Exceptional show ?thesis by fastforce
  next case (CFG_Getfield_Check_Normal C  M pc)
    hence "Stack (stkLength (P, C, M) pc - 1)  Use P (sourcenode a)"
      by (fastforce intro: Use_Enter_Stack)
    with pred use_Eq CFG_Getfield_Check_Normal show ?thesis by fastforce
  next case (CFG_Getfield_Check_Exceptional C  M pc)
    hence "Stack (stkLength (P, C, M) pc - 1)  Use P (sourcenode a)"
      by (fastforce intro: Use_Enter_Stack)
    with pred use_Eq CFG_Getfield_Check_Exceptional  show ?thesis by fastforce
  next case (CFG_Putfield_Check_Normal C  M pc)
    hence "Stack (stkLength (P, C, M) pc - 2)  Use P (sourcenode a)"
      by (fastforce intro: Use_Enter_Stack)
    with pred use_Eq CFG_Putfield_Check_Normal show ?thesis by fastforce
  next case (CFG_Putfield_Check_Exceptional C  M pc)
    hence "Stack (stkLength (P, C, M) pc - 2)  Use P (sourcenode a)"
      by (fastforce intro: Use_Enter_Stack)
    with pred use_Eq CFG_Putfield_Check_Exceptional show ?thesis by fastforce
  next case (CFG_Checkcast_Check_Normal C  M pc)
    hence "Stack (stkLength (P, C, M) pc - 1)  Use P (sourcenode a)"
      and "Heap  Use P (sourcenode a)"
      by (fastforce intro: Use_Enter_Stack Use_Enter_Heap)+
    with pred use_Eq CFG_Checkcast_Check_Normal show ?thesis by fastforce
  next case (CFG_Checkcast_Check_Exceptional C  M pc)
    hence "Stack (stkLength (P, C, M) pc - 1)  Use P (sourcenode a)"
      and "Heap  Use P (sourcenode a)"
      by (fastforce intro: Use_Enter_Stack Use_Enter_Heap)+
    with pred use_Eq CFG_Checkcast_Check_Exceptional show ?thesis by fastforce
  next case (CFG_Throw_Check C  M pc)
    hence "Stack (stkLength (P, C, M) pc - 1)  Use P (sourcenode a)"
      and "Heap  Use P (sourcenode a)"
      by (fastforce intro: Use_Enter_Stack Use_Enter_Heap)+
    with pred use_Eq CFG_Throw_Check show ?thesis by fastforce
  next case (CFG_Invoke_Check_NP_Normal C  M pc M' n)
    hence "Stack (stkLength (P, C, M) pc - (Suc n))  Use P (sourcenode a)"
      by (fastforce intro: Use_Enter_Stack)
    with pred use_Eq CFG_Invoke_Check_NP_Normal show ?thesis by fastforce
  next case (CFG_Invoke_Check_NP_Exceptional C  M pc M' n)
    hence "Stack (stkLength (P, C, M) pc - (Suc n))  Use P (sourcenode a)"
      by (fastforce intro: Use_Enter_Stack)
    with pred use_Eq CFG_Invoke_Check_NP_Exceptional show ?thesis by fastforce
  next case (CFG_Invoke_Call C  M pc M' n)
    hence "Stack (stkLength (P, C, M) pc - (Suc n))  Use P (sourcenode a)"
      and "Heap  Use P (sourcenode a)"
      by (fastforce intro: Use_Normal_Heap Use_Normal_Stack)+
    with pred use_Eq CFG_Invoke_Call show ?thesis by fastforce
  next case CFG_Invoke_Return_Check_Normal
    hence "Exception  Use P (sourcenode a)"
      by (fastforce intro: Use_Return_Exception)
    with pred use_Eq CFG_Invoke_Return_Check_Normal show ?thesis by fastforce
  next case CFG_Invoke_Return_Check_Exceptional
    hence "Exception  Use P (sourcenode a)" and "Heap  Use P (sourcenode a)"
      by (fastforce intro: Use_Return_Exception Use_Return_Heap)+
    with pred use_Eq CFG_Invoke_Return_Check_Exceptional show ?thesis by fastforce
  next case CFG_Invoke_Return_Exceptional_prop
    hence "Exception  Use P (sourcenode a)" and "Heap  Use P (sourcenode a)"
      by (fastforce intro: Use_Return_Exception Use_Return_Heap)+
    with pred use_Eq CFG_Invoke_Return_Exceptional_prop show ?thesis by fastforce
  next case CFG_Return_from_Method with pred length_cs show ?thesis by clarsimp
  qed auto
next
  fix a Q r p fs ins outs
  assume "valid_edge (P, C0, Main) a"
    and kind: "kind a = Q:r↪⇘pfs"
    and params: "(p, ins, outs)  set (((ClassMain P, MethodMain P), [], []) # procs (PROG P))"
  thus "length fs = length ins" unfolding valid_edge_def
  proof cases
    case (Main_Call  T mxs mxl0 "is" xt D)
    with kind params have [simp]: "p = (D, Main)"
      and "PROG P  D sees Main: []T = (mxs, mxl0, is, xt) in D"
      and "ins = Heap # map Local [0..<Suc 0]"
      by (auto elim!: in_set_procsE dest: sees_method_fun sees_method_idemp)
    with Main_Call kind show ?thesis
      by auto
  next
    case (CFG_Invoke_Call C  M pc M' n ST LT D' Ts T mxs mxl0 "is" xt D)
    with kind params have [simp]: "p = (D, M')"
      and "PROG P  D' sees M': TsT = (mxs, mxl0, is, xt) in D"
      and "ins = Heap # map Local [0..<Suc (length Ts)]"
      by (auto elim!: in_set_procsE dest: sees_method_fun sees_method_idemp)
    moreover with (P, C0, Main)  (C, M, pc, Normal) C  ClassMain P
      instrs_of (PROG P) C M ! pc = Invoke M' n TYPING P C M ! pc = (ST, LT)
      ST ! n = Class D' have "n = length Ts"
      by (fastforce dest!: reachable_node_impl_wt_instr dest: sees_method_fun list_all2_lengthD)
    ultimately show ?thesis using CFG_Invoke_Call kind by auto
  qed simp_all
next
  fix a Q r p fs a' Q' r' p' fs' s s'
  assume ve_a: "valid_edge (P, C0, Main) a"
    and kind_a: "kind a = Q:r↪⇘pfs"
    and ve_a': "valid_edge (P, C0, Main) a'"
    and kind_a': "kind a' = Q':r'↪⇘p'fs'"
    and src: "sourcenode a = sourcenode a'"
    and pred_s: "JVMCFG_Interpret.pred (kind a) s"
    and pred_s': "JVMCFG_Interpret.pred (kind a') s"
  then obtain cfs C M pc cs cfs' C' M' pc' cs' 
    where [simp]: "s = (cfs, (C, M, pc)) # cs" 
    by (cases s) fastforce+
  with ve_a kind_a show "a = a'" unfolding valid_edge_def
  proof cases
    case Main_Call with ve_a' kind_a' src pred_s pred_s' show ?thesis unfolding valid_edge_def
      by (cases a, cases a') (fastforce elim: JVMCFG.cases dest: sees_method_fun)
  next
    case CFG_Invoke_Call
    note invoke_call1 = this
    from ve_a' kind_a' show ?thesis unfolding valid_edge_def
    proof cases
      case Main_Call with CFG_Invoke_Call src have False by simp
      thus ?thesis by simp
    next
      case CFG_Invoke_Call with src invoke_call1 show ?thesis
        by clarsimp (cases a, cases a', fastforce dest: sees_method_fun)
    qed simp_all
  qed simp_all
next
  fix a Q r p fs i ins outs s s'
  assume ve: "valid_edge (P, C0, Main) a"
    and kind: "kind a = Q:r↪⇘pfs"
    and "i < length ins"
    and "(p, ins, outs)  set (((ClassMain P, MethodMain P), [], []) # procs (PROG P))"
    and "JVMCFG_Interpret.pred (kind a) s"
    and "JVMCFG_Interpret.pred (kind a) s'"
    and use_Eq: "VParamUses P (sourcenode a) ! i.
           JVMCFG_Interpret.state_val s V = JVMCFG_Interpret.state_val s' V"
  then obtain cfs C M pc cs cfs' C' M' pc' cs' where [simp]: "s = (cfs, (C, M, pc)) # cs"
    and [simp]: "s' = (cfs', (C', M', pc')) # cs'"
    by (cases s, fastforce) (cases s', fastforce+)
  from ve kind
  show "JVMCFG_Interpret.params fs (JVMCFG_Interpret.state_val s) ! i =
          JVMCFG_Interpret.params fs (JVMCFG_Interpret.state_val s') ! i"
    unfolding valid_edge_def
  proof cases
    case Main_Call with kind use_Eq i < length ins show ?thesis
      by (cases i) auto
  next
    case CFG_Invoke_Call
    { fix P C M pc n st st' i
      have "Vrev (map (λn. {Stack (stkLength (P, C, M) pc - Suc n)}) [0..<n]) ! i. st V = st' V
         JVMCFG_Interpret.params
        (rev (map (λi s. s (Stack (stkLength (P, C, M) pc - Suc i))) [0..<n])) st ! i =
        JVMCFG_Interpret.params
        (rev (map (λi s. s (Stack (stkLength (P, C, M) pc - Suc i))) [0..<n])) st' ! i"
        by (induct n arbitrary: i) (simp, case_tac i, auto)
    }
    note stack_params = this
    from CFG_Invoke_Call kind use_Eq i < length ins show ?thesis
      by (cases i, auto) (case_tac nat, auto intro: stack_params)
  qed simp_all
next
  fix a Q' p f' ins outs vmap vmap'
  assume "valid_edge (P, C0, Main) a"
    and "kind a = Q'↩⇘pf'"
    and "(p, ins, outs)  set (((ClassMain P, MethodMain P), [], []) # procs (PROG P))"
  thus "f' vmap vmap' = vmap'(ParamDefs P (targetnode a) [:=] map vmap outs)"
    unfolding valid_edge_def
    by (cases, simp_all) (fastforce elim: in_set_procsE simp: fun_upd_twist)
next
  fix a a'
  { fix P n f n' e n''
    assume "P  n -f n'" and "P  n -e n''"
    hence "e = f  n' = n''"
      by cases (simp_all, (fastforce elim: JVMCFG.cases)+)
  }
  note upd_det = this
  { fix P n Q n' Q' n'' s
    assume "P  n -(Q) n'" and edge': "P  n -(Q') n''" and trg: "n'  n''"
    hence "(Q s  ¬ Q' s)  (Q' s  ¬ Q s)"
    proof cases
      case CFG_Throw_Check with edge' trg show ?thesis by cases fastforce+
    qed (simp_all, (fastforce elim: JVMCFG.cases)+)
  }
  note pred_det = this
  assume "valid_edge (P, C0, Main) a"
    and ve': "valid_edge (P, C0, Main) a'"
    and src: "sourcenode a = sourcenode a'"
    and trg: "targetnode a  targetnode a'"
    and "intra_kind (kind a)"
    and "intra_kind (kind a')"
  thus "Q Q'. kind a = (Q)  kind a' = (Q')  (s. (Q s  ¬ Q' s)  (Q' s  ¬ Q s))"
    unfolding valid_edge_def intra_kind_def
    by (auto dest: upd_det pred_det)
qed

interpretation JVMCFGExit_wf :
  CFGExit_wf "sourcenode" "targetnode" "kind" "valid_edge (P, C0, Main)"
  "(ClassMain P, MethodMain P, None, Enter)"
  "(λ(C, M, pc, type). (C, M))" "get_return_edges P"
  "((ClassMain P, MethodMain P),[],[]) # procs (PROG P)"
  "(ClassMain P, MethodMain P)"
  "(ClassMain P, MethodMain P, None, Return)"
  "Def P" "Use P" "ParamDefs P" "ParamUses P"
proof
  show "Def P (ClassMain P, MethodMain P, None, nodeType.Return) = {} 
    Use P (ClassMain P, MethodMain P, None, nodeType.Return) = {}"
    by (fastforce elim: Def.cases Use.cases)
qed

end