[STATEMENT]
lemma [iff]: "OK None \<in> states P mxs mxl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OK None \<in> states P mxs mxl
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OK None \<in> states P mxs mxl
[PROOF STEP]
by(simp add: JVM_states_unfold)


[STATEMENT]
lemma (in TC0) after_in_states:
assumes wf: "wf_prog p P" and wt: "P,E \<turnstile>\<^sub>1 e :: T"
  and Etypes: "set E \<subseteq> types P" and STtypes: "set ST \<subseteq> types P"
  and stack: "size ST + max_stack e \<le> mxs"
shows "OK (after E A ST e) \<in> states P mxs mxl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OK (after E A ST e) \<in> states P mxs mxl
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OK (after E A ST e) \<in> states P mxs mxl
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. OK (after E A ST e) \<in> states P mxs mxl
[PROOF STEP]
have "size ST + 1 \<le> mxs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ST + 1 \<le> mxs
[PROOF STEP]
using max_stack1[where e=e] wt stack
[PROOF STATE]
proof (prove)
using this:
?P,?E \<turnstile>\<^sub>1 e :: ?T \<Longrightarrow> 1 \<le> max_stack e
P,E \<turnstile>\<^sub>1 e :: T
length ST + max_stack e \<le> mxs

goal (1 subgoal):
 1. length ST + 1 \<le> mxs
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
length ST + 1 \<le> mxs

goal (1 subgoal):
 1. OK (after E A ST e) \<in> states P mxs mxl
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length ST + 1 \<le> mxs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length ST + 1 \<le> mxs

goal (1 subgoal):
 1. OK (after E A ST e) \<in> states P mxs mxl
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length ST + 1 \<le> mxs
wf_prog p P
P,E \<turnstile>\<^sub>1 e :: T
set E \<subseteq> types P
set ST \<subseteq> types P
length ST + max_stack e \<le> mxs

goal (1 subgoal):
 1. OK (after E A ST e) \<in> states P mxs mxl
[PROOF STEP]
by(simp add: after_def ty\<^sub>i'_def JVM_states_unfold ty\<^sub>l_in_types)
      (blast intro!:nlistsI WT\<^sub>1_is_type)
[PROOF STATE]
proof (state)
this:
OK (after E A ST e) \<in> states P mxs mxl

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in TC0) OK_ty\<^sub>i'_in_statesI[simp]:
  "\<lbrakk> set E \<subseteq> types P; set ST \<subseteq> types P; size ST \<le> mxs \<rbrakk>
  \<Longrightarrow> OK (ty\<^sub>i' ST E A) \<in> states P mxs mxl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set E \<subseteq> types P; set ST \<subseteq> types P; length ST \<le> mxs\<rbrakk> \<Longrightarrow> OK (ty\<^sub>i' ST E A) \<in> states P mxs mxl
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set E \<subseteq> types P; set ST \<subseteq> types P; length ST \<le> mxs\<rbrakk> \<Longrightarrow> OK (ty\<^sub>i' ST E A) \<in> states P mxs mxl
[PROOF STEP]
by(simp add:ty\<^sub>i'_def JVM_states_unfold ty\<^sub>l_in_types)
  (blast intro!:nlistsI)


[STATEMENT]
lemma is_class_type_aux: "is_class P C \<Longrightarrow> is_type P (Class C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_class P C \<Longrightarrow> is_type P (Class C)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_class P C \<Longrightarrow> is_type P (Class C)
[PROOF STEP]
by(simp)