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': Ts→T = (mxs, mxl⇩0, is, xt) in D"
  and "(D, D', fs, ms) ∈ set (PROG P)"
  and "(M', Ts', T', mxs', mxl⇩0', is', xt') ∈ set ms"
  shows "Ts = Ts' ∧ T = T' ∧ mxs = mxs' ∧ mxl⇩0 = mxl⇩0' ∧ 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': Ts→T = (mxs, mxl⇩0, is, xt) in D›
    ‹(M', Ts', T', mxs', mxl⇩0', 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↪⇘p⇙fs"
    and params: "(p, ins, outs) ∈ set (((ClassMain P, MethodMain P), [], []) # procs (PROG P))"
  hence "(P, C0, Main) ⊢ sourcenode a -Q:r↪⇘p⇙fs→ 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': Ts→T = (mxs, mxl0, is, xt) in D›
    have "PROG P ⊢ D sees M': Ts→T = (mxs, mxl0, is, xt) in D"
      by -(drule sees_method_idemp)
    with params have "PROG P ⊢ D sees M': Ts→T=(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'↩⇘p⇙f'"
    and params: "(p, ins, outs) ∈ set (((ClassMain P, MethodMain P), [], []) # procs (PROG P))"
  hence "(P, C0, Main) ⊢ sourcenode a -Q'↩⇘p⇙f'→ 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↪⇘p⇙fs"
    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): Ts→T = 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↪⇘p⇙fs"
  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↩⇘p⇙f"
    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: "∀V∈Use 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 "∀V∈Def 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: "∀V∈Use 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↪⇘p⇙fs"
    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': Ts→T = (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↪⇘p⇙fs"
    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↪⇘p⇙fs"
    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: "∀V∈ParamUses 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 "∀V∈rev (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'↩⇘p⇙f'"
    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