[STATEMENT]
lemma [simp]: "PROG (Abs_wf_jvmprog (EP, Phi_EP)) = EP"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PROG (Abs_wf_jvmprog (EP, Phi_EP)) = EP
[PROOF STEP]
proof (cases "(EP, Phi_EP) \<in> wf_jvmprog")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (EP, Phi_EP) \<in> wf_jvmprog \<Longrightarrow> PROG (Abs_wf_jvmprog (EP, Phi_EP)) = EP
 2. (EP, Phi_EP) \<notin> wf_jvmprog \<Longrightarrow> PROG (Abs_wf_jvmprog (EP, Phi_EP)) = EP
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
(EP, Phi_EP) \<in> wf_jvmprog

goal (2 subgoals):
 1. (EP, Phi_EP) \<in> wf_jvmprog \<Longrightarrow> PROG (Abs_wf_jvmprog (EP, Phi_EP)) = EP
 2. (EP, Phi_EP) \<notin> wf_jvmprog \<Longrightarrow> PROG (Abs_wf_jvmprog (EP, Phi_EP)) = EP
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(EP, Phi_EP) \<in> wf_jvmprog

goal (1 subgoal):
 1. PROG (Abs_wf_jvmprog (EP, Phi_EP)) = EP
[PROOF STEP]
by (simp add: Abs_wf_jvmprog_inverse)
[PROOF STATE]
proof (state)
this:
PROG (Abs_wf_jvmprog (EP, Phi_EP)) = EP

goal (1 subgoal):
 1. (EP, Phi_EP) \<notin> wf_jvmprog \<Longrightarrow> PROG (Abs_wf_jvmprog (EP, Phi_EP)) = EP
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (EP, Phi_EP) \<notin> wf_jvmprog \<Longrightarrow> PROG (Abs_wf_jvmprog (EP, Phi_EP)) = EP
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
(EP, Phi_EP) \<notin> wf_jvmprog

goal (1 subgoal):
 1. (EP, Phi_EP) \<notin> wf_jvmprog \<Longrightarrow> PROG (Abs_wf_jvmprog (EP, Phi_EP)) = EP
[PROOF STEP]
with EP_wf
[PROOF STATE]
proof (chain)
picking this:
wf_jvm_prog\<^bsub>Phi_EP\<^esub> EP
(EP, Phi_EP) \<notin> wf_jvmprog
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wf_jvm_prog\<^bsub>Phi_EP\<^esub> EP
(EP, Phi_EP) \<notin> wf_jvmprog

goal (1 subgoal):
 1. PROG (Abs_wf_jvmprog (EP, Phi_EP)) = EP
[PROOF STEP]
by (simp add: wf_jvmprog_def)
[PROOF STATE]
proof (state)
this:
PROG (Abs_wf_jvmprog (EP, Phi_EP)) = EP

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [simp]: "TYPING (Abs_wf_jvmprog (EP, Phi_EP)) = Phi_EP"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TYPING (Abs_wf_jvmprog (EP, Phi_EP)) = Phi_EP
[PROOF STEP]
proof (cases "(EP, Phi_EP) \<in> wf_jvmprog")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (EP, Phi_EP) \<in> wf_jvmprog \<Longrightarrow> TYPING (Abs_wf_jvmprog (EP, Phi_EP)) = Phi_EP
 2. (EP, Phi_EP) \<notin> wf_jvmprog \<Longrightarrow> TYPING (Abs_wf_jvmprog (EP, Phi_EP)) = Phi_EP
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
(EP, Phi_EP) \<in> wf_jvmprog

goal (2 subgoals):
 1. (EP, Phi_EP) \<in> wf_jvmprog \<Longrightarrow> TYPING (Abs_wf_jvmprog (EP, Phi_EP)) = Phi_EP
 2. (EP, Phi_EP) \<notin> wf_jvmprog \<Longrightarrow> TYPING (Abs_wf_jvmprog (EP, Phi_EP)) = Phi_EP
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(EP, Phi_EP) \<in> wf_jvmprog

goal (1 subgoal):
 1. TYPING (Abs_wf_jvmprog (EP, Phi_EP)) = Phi_EP
[PROOF STEP]
by (simp add: Abs_wf_jvmprog_inverse)
[PROOF STATE]
proof (state)
this:
TYPING (Abs_wf_jvmprog (EP, Phi_EP)) = Phi_EP

goal (1 subgoal):
 1. (EP, Phi_EP) \<notin> wf_jvmprog \<Longrightarrow> TYPING (Abs_wf_jvmprog (EP, Phi_EP)) = Phi_EP
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (EP, Phi_EP) \<notin> wf_jvmprog \<Longrightarrow> TYPING (Abs_wf_jvmprog (EP, Phi_EP)) = Phi_EP
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
(EP, Phi_EP) \<notin> wf_jvmprog

goal (1 subgoal):
 1. (EP, Phi_EP) \<notin> wf_jvmprog \<Longrightarrow> TYPING (Abs_wf_jvmprog (EP, Phi_EP)) = Phi_EP
[PROOF STEP]
with EP_wf
[PROOF STATE]
proof (chain)
picking this:
wf_jvm_prog\<^bsub>Phi_EP\<^esub> EP
(EP, Phi_EP) \<notin> wf_jvmprog
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wf_jvm_prog\<^bsub>Phi_EP\<^esub> EP
(EP, Phi_EP) \<notin> wf_jvmprog

goal (1 subgoal):
 1. TYPING (Abs_wf_jvmprog (EP, Phi_EP)) = Phi_EP
[PROOF STEP]
by (simp add: wf_jvmprog_def)
[PROOF STATE]
proof (state)
this:
TYPING (Abs_wf_jvmprog (EP, Phi_EP)) = Phi_EP

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma method_in_EP_is_M:
  "EP \<turnstile> C sees M: Ts\<rightarrow>T = (mxs, mxl, is, xt) in D
  \<Longrightarrow> C = ''C'' \<and> M = ''M'' \<and> Ts = [] \<and> T = Void \<and> mxs = 1 \<and> mxl = 0 \<and>
  is = [Push Unit, instr.Return] \<and> xt = [] \<and> D = ''C''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. EP \<turnstile> C sees M: Ts\<rightarrow>T = (mxs, mxl, is, xt) in D \<Longrightarrow> C = ''C'' \<and> M = ''M'' \<and> Ts = [] \<and> T = Void \<and> mxs = 1 \<and> mxl = 0 \<and> is = [Push Unit, instr.Return] \<and> xt = [] \<and> D = ''C''
[PROOF STEP]
by (fastforce elim: Methods.cases
    simp: class_def SystemClasses_def ObjectC_def NullPointerC_def OutOfMemoryC_def ClassCastC_def
    if_split_eq1 EP_def Method_def)


[STATEMENT]
lemma [simp]:
  "\<exists>T Ts mxs mxl is. (\<exists>xt. EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = (mxs, mxl, is, xt) in ''C'') \<and> is \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>T Ts mxs mxl is. (\<exists>xt. EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = (mxs, mxl, is, xt) in ''C'') \<and> is \<noteq> []
[PROOF STEP]
using EP_wf
[PROOF STATE]
proof (prove)
using this:
wf_jvm_prog\<^bsub>Phi_EP\<^esub> EP

goal (1 subgoal):
 1. \<exists>T Ts mxs mxl is. (\<exists>xt. EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = (mxs, mxl, is, xt) in ''C'') \<and> is \<noteq> []
[PROOF STEP]
by (fastforce dest: mdecl_visible simp: wf_jvm_prog_phi_def EP_def)


[STATEMENT]
lemma [simp]:
  "\<exists>T Ts mxs mxl is. (\<exists>xt. EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = (mxs, mxl, is, xt) in ''C'') \<and>
  Suc 0 < length is"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>T Ts mxs mxl is. (\<exists>xt. EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = (mxs, mxl, is, xt) in ''C'') \<and> Suc 0 < length is
[PROOF STEP]
using EP_wf
[PROOF STATE]
proof (prove)
using this:
wf_jvm_prog\<^bsub>Phi_EP\<^esub> EP

goal (1 subgoal):
 1. \<exists>T Ts mxs mxl is. (\<exists>xt. EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = (mxs, mxl, is, xt) in ''C'') \<and> Suc 0 < length is
[PROOF STEP]
by (fastforce dest: mdecl_visible simp: wf_jvm_prog_phi_def EP_def)


[STATEMENT]
lemma C_sees_M_in_EP [simp]:
  "EP \<turnstile> ''C'' sees ''M'': []\<rightarrow>Void = (Suc 0, 0, [Push Unit, instr.Return], []) in ''C''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. EP \<turnstile> ''C'' sees ''M'': []\<rightarrow>Void = (Suc 0, 0, [Push Unit, instr.Return], []) in ''C''
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. EP \<turnstile> ''C'' sees ''M'': []\<rightarrow>Void = (Suc 0, 0, [Push Unit, instr.Return], []) in ''C''
[PROOF STEP]
have "EP \<turnstile> ''C'' sees_methods [''M'' \<mapsto> (([], Void, 1, 0, [Push Unit, instr.Return], []), ''C'')]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. EP \<turnstile> ''C'' sees_methods [''M'' \<mapsto> (([], Void, 1, 0, [Push Unit, instr.Return], []), ''C'')]
[PROOF STEP]
by (fastforce intro: Methods.intros simp: class_def SystemClasses_def ObjectC_def EP_def)
[PROOF STATE]
proof (state)
this:
EP \<turnstile> ''C'' sees_methods [''M'' \<mapsto> (([], Void, 1, 0, [Push Unit, instr.Return], []), ''C'')]

goal (1 subgoal):
 1. EP \<turnstile> ''C'' sees ''M'': []\<rightarrow>Void = (Suc 0, 0, [Push Unit, instr.Return], []) in ''C''
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
EP \<turnstile> ''C'' sees_methods [''M'' \<mapsto> (([], Void, 1, 0, [Push Unit, instr.Return], []), ''C'')]

goal (1 subgoal):
 1. EP \<turnstile> ''C'' sees ''M'': []\<rightarrow>Void = (Suc 0, 0, [Push Unit, instr.Return], []) in ''C''
[PROOF STEP]
by (fastforce simp: Method_def)
[PROOF STATE]
proof (state)
this:
EP \<turnstile> ''C'' sees ''M'': []\<rightarrow>Void = (Suc 0, 0, [Push Unit, instr.Return], []) in ''C''

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma instrs_of_EP_C_M [simp]:
  "instrs_of EP ''C'' ''M'' = [Push Unit, instr.Return]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. instrs_of EP ''C'' ''M'' = [Push Unit, instr.Return]
[PROOF STEP]
unfolding method_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (snd (snd (snd (snd (THE (D, Ts, T, m). EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = m in D)))))) = [Push Unit, instr.Return]
[PROOF STEP]
by (rule theI2 [where P = "\<lambda>(D, Ts, T, m). EP \<turnstile> ''C'' sees ''M'': Ts\<rightarrow>T = m in D"])
(auto dest: method_in_EP_is_M)


[STATEMENT]
lemma ClassMain_not_C [simp]: "ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<noteq> ''C''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<noteq> ''C''
[PROOF STEP]
by (fastforce intro: no_Call_in_ClassMain [where P="Abs_wf_jvmprog (EP, Phi_EP)"] C_sees_M_in_EP)


[STATEMENT]
lemma method_entry [dest!]: "(Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> \<Rightarrow>(C, M, None, Enter)
  \<Longrightarrow> (C = ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<and> M = MethodMain (Abs_wf_jvmprog (EP, Phi_EP)))
  \<or> (C = ''C'' \<and> M = ''M'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') \<turnstile> \<Rightarrow>(C, M, None, Enter) \<Longrightarrow> C = ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) \<and> M = MethodMain (Abs_wf_jvmprog (EP, Phi_EP)) \<or> C = ''C'' \<and> M = ''M''
[PROOF STEP]
by (fastforce elim: reachable.cases elim!: JVMCFG.cases dest!: method_in_EP_is_M)