[STATEMENT]
lemma states_compP [simp]: "states (compP f P) mxs mxl = states P mxs mxl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. states (compP f P) mxs mxl = states P mxs mxl
[PROOF STEP]
by (simp add: JVM_states_unfold)


[STATEMENT]
lemma [simp]: "app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
[PROOF STEP]
fix ST LT
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
[PROOF STEP]
have "app\<^sub>i (i, compP f P, pc, mpc, T, (ST, LT)) = app\<^sub>i (i, P, pc, mpc, T, (ST, LT))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
[PROOF STEP]
proof(cases i)
[PROOF STATE]
proof (state)
goal (24 subgoals):
 1. \<And>x1. i = Load x1 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 2. \<And>x2. i = Store x2 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 3. \<And>x3. i = Push x3 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 4. \<And>x4. i = New x4 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 5. \<And>x5. i = NewArray x5 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 6. i = ALoad \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 7. i = AStore \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 8. i = ALength \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 9. \<And>x91 x92. i = Getfield x91 x92 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 10. \<And>x101 x102. i = Putfield x101 x102 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
A total of 24 subgoals...
[PROOF STEP]
case (Invoke M n)
[PROOF STATE]
proof (state)
this:
i = Invoke M n

goal (24 subgoals):
 1. \<And>x1. i = Load x1 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 2. \<And>x2. i = Store x2 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 3. \<And>x3. i = Push x3 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 4. \<And>x4. i = New x4 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 5. \<And>x5. i = NewArray x5 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 6. i = ALoad \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 7. i = AStore \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 8. i = ALength \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 9. \<And>x91 x92. i = Getfield x91 x92 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 10. \<And>x101 x102. i = Putfield x101 x102 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
A total of 24 subgoals...
[PROOF STEP]
have "\<And>C Ts D. (\<exists>T m. compP f P \<turnstile> C sees M: Ts\<rightarrow>T = m in D) \<longleftrightarrow> (\<exists>T m. P \<turnstile> C sees M: Ts\<rightarrow>T = m in D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C Ts D. (\<exists>T m. compP f P \<turnstile> C sees M: Ts\<rightarrow>T = m in D) = (\<exists>T m. P \<turnstile> C sees M: Ts\<rightarrow>T = m in D)
[PROOF STEP]
by(auto dest!: sees_method_compPD dest: sees_method_compP)
[PROOF STATE]
proof (state)
this:
(\<exists>T m. compP f P \<turnstile> ?C sees M: ?Ts\<rightarrow>T = m in ?D) = (\<exists>T m. P \<turnstile> ?C sees M: ?Ts\<rightarrow>T = m in ?D)

goal (24 subgoals):
 1. \<And>x1. i = Load x1 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 2. \<And>x2. i = Store x2 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 3. \<And>x3. i = Push x3 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 4. \<And>x4. i = New x4 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 5. \<And>x5. i = NewArray x5 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 6. i = ALoad \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 7. i = AStore \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 8. i = ALength \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 9. \<And>x91 x92. i = Getfield x91 x92 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 10. \<And>x101 x102. i = Putfield x101 x102 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
A total of 24 subgoals...
[PROOF STEP]
with Invoke
[PROOF STATE]
proof (chain)
picking this:
i = Invoke M n
(\<exists>T m. compP f P \<turnstile> ?C sees M: ?Ts\<rightarrow>T = m in ?D) = (\<exists>T m. P \<turnstile> ?C sees M: ?Ts\<rightarrow>T = m in ?D)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i = Invoke M n
(\<exists>T m. compP f P \<turnstile> ?C sees M: ?Ts\<rightarrow>T = m in ?D) = (\<exists>T m. P \<turnstile> ?C sees M: ?Ts\<rightarrow>T = m in ?D)

goal (1 subgoal):
 1. app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)

goal (23 subgoals):
 1. \<And>x1. i = Load x1 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 2. \<And>x2. i = Store x2 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 3. \<And>x3. i = Push x3 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 4. \<And>x4. i = New x4 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 5. \<And>x5. i = NewArray x5 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 6. i = ALoad \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 7. i = AStore \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 8. i = ALength \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 9. \<And>x91 x92. i = Getfield x91 x92 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
 10. \<And>x101 x102. i = Putfield x101 x102 \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)
A total of 23 subgoals...
[PROOF STEP]
qed(simp_all)
[PROOF STATE]
proof (state)
this:
app\<^sub>i (i, compP f P, pc, mpc, T, ST, LT) = app\<^sub>i (i, P, pc, mpc, T, ST, LT)

goal (1 subgoal):
 1. app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
app\<^sub>i (i, compP f P, pc, mpc, T, ?ST2, ?LT2) = app\<^sub>i (i, P, pc, mpc, T, ?ST2, ?LT2)

goal (1 subgoal):
 1. app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
app\<^sub>i (i, compP f P, pc, mpc, T, ?ST2, ?LT2) = app\<^sub>i (i, P, pc, mpc, T, ?ST2, ?LT2)

goal (1 subgoal):
 1. app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
[PROOF STEP]
by(cases \<tau>) simp
[PROOF STATE]
proof (state)
this:
app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [simp]: "is_relevant_entry (compP f P) i = is_relevant_entry P i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_relevant_entry (compP f P) i = is_relevant_entry P i
[PROOF STEP]
apply (rule ext)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. is_relevant_entry (compP f P) i x xa = is_relevant_entry P i x xa
[PROOF STEP]
apply (unfold is_relevant_entry_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. (let (fa, t, C, h, d) = xa in (case C of None \<Rightarrow> True | \<lfloor>C'\<rfloor> \<Rightarrow> is_relevant_class i (compP f P) C') \<and> x \<in> {fa..<t}) = (let (f, t, C, h, d) = xa in (case C of None \<Rightarrow> True | \<lfloor>C'\<rfloor> \<Rightarrow> is_relevant_class i P C') \<and> x \<in> {f..<t})
[PROOF STEP]
apply (cases i)
[PROOF STATE]
proof (prove)
goal (24 subgoals):
 1. \<And>x xa x1. i = Load x1 \<Longrightarrow> (let (fa, t, C, h, d) = xa in (case C of None \<Rightarrow> True | \<lfloor>C'\<rfloor> \<Rightarrow> is_relevant_class i (compP f P) C') \<and> x \<in> {fa..<t}) = (let (f, t, C, h, d) = xa in (case C of None \<Rightarrow> True | \<lfloor>C'\<rfloor> \<Rightarrow> is_relevant_class i P C') \<and> x \<in> {f..<t})
 2. \<And>x xa x2. i = Store x2 \<Longrightarrow> (let (fa, t, C, h, d) = xa in (case C of None \<Rightarrow> True | \<lfloor>C'\<rfloor> \<Rightarrow> is_relevant_class i (compP f P) C') \<and> x \<in> {fa..<t}) = (let (f, t, C, h, d) = xa in (case C of None \<Rightarrow> True | \<lfloor>C'\<rfloor> \<Rightarrow> is_relevant_class i P C') \<and> x \<in> {f..<t})
 3. \<And>x xa x3. i = Push x3 \<Longrightarrow> (let (fa, t, C, h, d) = xa in (case C of None \<Rightarrow> True | \<lfloor>C'\<rfloor> \<Rightarrow> is_relevant_class i (compP f P) C') \<and> x \<in> {fa..<t}) = (let (f, t, C, h, d) = xa in (case C of None \<Rightarrow> True | \<lfloor>C'\<rfloor> \<Rightarrow> is_relevant_class i P C') \<and> x \<in> {f..<t})
 4. \<And>x xa x4. i = New x4 \<Longrightarrow> (let (fa, t, C, h, d) = xa in (case C of None \<Rightarrow> True | \<lfloor>C'\<rfloor> \<Rightarrow> is_relevant_class i (compP f P) C') \<and> x \<in> {fa..<t}) = (let (f, t, C, h, d) = xa in (case C of None \<Rightarrow> True | \<lfloor>C'\<rfloor> \<Rightarrow> is_relevant_class i P C') \<and> x \<in> {f..<t})
 5. \<And>x xa x5. i = NewArray x5 \<Longrightarrow> (let (fa, t, C, h, d) = xa in (case C of None \<Rightarrow> True | \<lfloor>C'\<rfloor> \<Rightarrow> is_relevant_class i (compP f P) C') \<and> x \<in> {fa..<t}) = (let (f, t, C, h, d) = xa in (case C of None \<Rightarrow> True | \<lfloor>C'\<rfloor> \<Rightarrow> is_relevant_class i P C') \<and> x \<in> {f..<t})
 6. \<And>x xa. i = ALoad \<Longrightarrow> (let (fa, t, C, h, d) = xa in (case C of None \<Rightarrow> True | \<lfloor>C'\<rfloor> \<Rightarrow> is_relevant_class i (compP f P) C') \<and> x \<in> {fa..<t}) = (let (f, t, C, h, d) = xa in (case C of None \<Rightarrow> True | \<lfloor>C'\<rfloor> \<Rightarrow> is_relevant_class i P C') \<and> x \<in> {f..<t})
 7. \<And>x xa. i = AStore \<Longrightarrow> (let (fa, t, C, h, d) = xa in (case C of None \<Rightarrow> True | \<lfloor>C'\<rfloor> \<Rightarrow> is_relevant_class i (compP f P) C') \<and> x \<in> {fa..<t}) = (let (f, t, C, h, d) = xa in (case C of None \<Rightarrow> True | \<lfloor>C'\<rfloor> \<Rightarrow> is_relevant_class i P C') \<and> x \<in> {f..<t})
 8. \<And>x xa. i = ALength \<Longrightarrow> (let (fa, t, C, h, d) = xa in (case C of None \<Rightarrow> True | \<lfloor>C'\<rfloor> \<Rightarrow> is_relevant_class i (compP f P) C') \<and> x \<in> {fa..<t}) = (let (f, t, C, h, d) = xa in (case C of None \<Rightarrow> True | \<lfloor>C'\<rfloor> \<Rightarrow> is_relevant_class i P C') \<and> x \<in> {f..<t})
 9. \<And>x xa x91 x92. i = Getfield x91 x92 \<Longrightarrow> (let (fa, t, C, h, d) = xa in (case C of None \<Rightarrow> True | \<lfloor>C'\<rfloor> \<Rightarrow> is_relevant_class i (compP f P) C') \<and> x \<in> {fa..<t}) = (let (f, t, C, h, d) = xa in (case C of None \<Rightarrow> True | \<lfloor>C'\<rfloor> \<Rightarrow> is_relevant_class i P C') \<and> x \<in> {f..<t})
 10. \<And>x xa x101 x102. i = Putfield x101 x102 \<Longrightarrow> (let (fa, t, C, h, d) = xa in (case C of None \<Rightarrow> True | \<lfloor>C'\<rfloor> \<Rightarrow> is_relevant_class i (compP f P) C') \<and> x \<in> {fa..<t}) = (let (f, t, C, h, d) = xa in (case C of None \<Rightarrow> True | \<lfloor>C'\<rfloor> \<Rightarrow> is_relevant_class i P C') \<and> x \<in> {f..<t})
A total of 24 subgoals...
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [simp]: "relevant_entries (compP f P) i pc xt = relevant_entries P i pc xt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. relevant_entries (compP f P) i pc xt = relevant_entries P i pc xt
[PROOF STEP]
by (simp add: relevant_entries_def)


[STATEMENT]
lemma [simp]: "app i (compP f P) mpc T pc mxl xt \<tau> = app i P mpc T pc mxl xt \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app i (compP f P) mpc T pc mxl xt \<tau> = app i P mpc T pc mxl xt \<tau>
[PROOF STEP]
apply (simp add: app_def xcpt_app_def eff_def xcpt_eff_def norm_eff_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a b. \<tau> = \<lfloor>(a, b)\<rfloor> \<longrightarrow> (app\<^sub>i (i, P, pc, mpc, T, a, b) \<and> (\<forall>(fa, t, C, ab)\<in>set (relevant_entries P i pc xt). (case C of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_class (compP f P) x) \<and> (case ab of (h, d) \<Rightarrow> d \<le> length a \<and> d < mpc)) \<and> (\<forall>(pc', \<tau>')\<in>(\<lambda>pc'. (pc', \<lfloor>eff\<^sub>i (i, compP f P, a, b)\<rfloor>)) ` set (succs i (a, b) pc) \<union> (\<lambda>(f, t, C, h, d). (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length a - d) a, b)\<rfloor>)) ` set (relevant_entries P i pc xt). pc' < mxl)) = (app\<^sub>i (i, P, pc, mpc, T, a, b) \<and> (\<forall>(f, t, C, ab)\<in>set (relevant_entries P i pc xt). (case C of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_class P x) \<and> (case ab of (h, d) \<Rightarrow> d \<le> length a \<and> d < mpc)) \<and> (\<forall>(pc', \<tau>')\<in>(\<lambda>pc'. (pc', \<lfloor>eff\<^sub>i (i, P, a, b)\<rfloor>)) ` set (succs i (a, b) pc) \<union> (\<lambda>(f, t, C, h, d). (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length a - d) a, b)\<rfloor>)) ` set (relevant_entries P i pc xt). pc' < mxl))
[PROOF STEP]
apply (fastforce simp add: image_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [simp]: "app i P mpc T pc mxl xt \<tau> \<Longrightarrow> eff i (compP f P) pc xt \<tau> = eff i P pc xt \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app i P mpc T pc mxl xt \<tau> \<Longrightarrow> eff i (compP f P) pc xt \<tau> = eff i P pc xt \<tau>
[PROOF STEP]
apply (clarsimp simp add: eff_def norm_eff_def xcpt_eff_def app_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa ba x. \<lbrakk>\<tau> = \<lfloor>(aa, ba)\<rfloor>; app\<^sub>i (i, P, pc, mpc, T, aa, ba); xcpt_app i P pc mpc xt (aa, ba); \<forall>x\<in>(\<lambda>pc'. (pc', \<lfloor>eff\<^sub>i (i, P, aa, ba)\<rfloor>)) ` set (succs i (aa, ba) pc) \<union> (\<lambda>x. case x of (f, t, C, h, d) \<Rightarrow> (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length aa - d) aa, ba)\<rfloor>)) ` set (relevant_entries P i pc xt). case x of (pc', \<tau>') \<Rightarrow> pc' < mxl; x \<in> set (succs i (aa, ba) pc)\<rbrakk> \<Longrightarrow> eff\<^sub>i (i, compP f P, aa, ba) = eff\<^sub>i (i, P, aa, ba)
[PROOF STEP]
apply (cases i)
[PROOF STATE]
proof (prove)
goal (24 subgoals):
 1. \<And>aa ba x x1. \<lbrakk>\<tau> = \<lfloor>(aa, ba)\<rfloor>; app\<^sub>i (i, P, pc, mpc, T, aa, ba); xcpt_app i P pc mpc xt (aa, ba); \<forall>x\<in>(\<lambda>pc'. (pc', \<lfloor>eff\<^sub>i (i, P, aa, ba)\<rfloor>)) ` set (succs i (aa, ba) pc) \<union> (\<lambda>x. case x of (f, t, C, h, d) \<Rightarrow> (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length aa - d) aa, ba)\<rfloor>)) ` set (relevant_entries P i pc xt). case x of (pc', \<tau>') \<Rightarrow> pc' < mxl; x \<in> set (succs i (aa, ba) pc); i = Load x1\<rbrakk> \<Longrightarrow> eff\<^sub>i (i, compP f P, aa, ba) = eff\<^sub>i (i, P, aa, ba)
 2. \<And>aa ba x x2. \<lbrakk>\<tau> = \<lfloor>(aa, ba)\<rfloor>; app\<^sub>i (i, P, pc, mpc, T, aa, ba); xcpt_app i P pc mpc xt (aa, ba); \<forall>x\<in>(\<lambda>pc'. (pc', \<lfloor>eff\<^sub>i (i, P, aa, ba)\<rfloor>)) ` set (succs i (aa, ba) pc) \<union> (\<lambda>x. case x of (f, t, C, h, d) \<Rightarrow> (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length aa - d) aa, ba)\<rfloor>)) ` set (relevant_entries P i pc xt). case x of (pc', \<tau>') \<Rightarrow> pc' < mxl; x \<in> set (succs i (aa, ba) pc); i = Store x2\<rbrakk> \<Longrightarrow> eff\<^sub>i (i, compP f P, aa, ba) = eff\<^sub>i (i, P, aa, ba)
 3. \<And>aa ba x x3. \<lbrakk>\<tau> = \<lfloor>(aa, ba)\<rfloor>; app\<^sub>i (i, P, pc, mpc, T, aa, ba); xcpt_app i P pc mpc xt (aa, ba); \<forall>x\<in>(\<lambda>pc'. (pc', \<lfloor>eff\<^sub>i (i, P, aa, ba)\<rfloor>)) ` set (succs i (aa, ba) pc) \<union> (\<lambda>x. case x of (f, t, C, h, d) \<Rightarrow> (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length aa - d) aa, ba)\<rfloor>)) ` set (relevant_entries P i pc xt). case x of (pc', \<tau>') \<Rightarrow> pc' < mxl; x \<in> set (succs i (aa, ba) pc); i = Push x3\<rbrakk> \<Longrightarrow> eff\<^sub>i (i, compP f P, aa, ba) = eff\<^sub>i (i, P, aa, ba)
 4. \<And>aa ba x x4. \<lbrakk>\<tau> = \<lfloor>(aa, ba)\<rfloor>; app\<^sub>i (i, P, pc, mpc, T, aa, ba); xcpt_app i P pc mpc xt (aa, ba); \<forall>x\<in>(\<lambda>pc'. (pc', \<lfloor>eff\<^sub>i (i, P, aa, ba)\<rfloor>)) ` set (succs i (aa, ba) pc) \<union> (\<lambda>x. case x of (f, t, C, h, d) \<Rightarrow> (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length aa - d) aa, ba)\<rfloor>)) ` set (relevant_entries P i pc xt). case x of (pc', \<tau>') \<Rightarrow> pc' < mxl; x \<in> set (succs i (aa, ba) pc); i = New x4\<rbrakk> \<Longrightarrow> eff\<^sub>i (i, compP f P, aa, ba) = eff\<^sub>i (i, P, aa, ba)
 5. \<And>aa ba x x5. \<lbrakk>\<tau> = \<lfloor>(aa, ba)\<rfloor>; app\<^sub>i (i, P, pc, mpc, T, aa, ba); xcpt_app i P pc mpc xt (aa, ba); \<forall>x\<in>(\<lambda>pc'. (pc', \<lfloor>eff\<^sub>i (i, P, aa, ba)\<rfloor>)) ` set (succs i (aa, ba) pc) \<union> (\<lambda>x. case x of (f, t, C, h, d) \<Rightarrow> (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length aa - d) aa, ba)\<rfloor>)) ` set (relevant_entries P i pc xt). case x of (pc', \<tau>') \<Rightarrow> pc' < mxl; x \<in> set (succs i (aa, ba) pc); i = NewArray x5\<rbrakk> \<Longrightarrow> eff\<^sub>i (i, compP f P, aa, ba) = eff\<^sub>i (i, P, aa, ba)
 6. \<And>aa ba x. \<lbrakk>\<tau> = \<lfloor>(aa, ba)\<rfloor>; app\<^sub>i (i, P, pc, mpc, T, aa, ba); xcpt_app i P pc mpc xt (aa, ba); \<forall>x\<in>(\<lambda>pc'. (pc', \<lfloor>eff\<^sub>i (i, P, aa, ba)\<rfloor>)) ` set (succs i (aa, ba) pc) \<union> (\<lambda>x. case x of (f, t, C, h, d) \<Rightarrow> (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length aa - d) aa, ba)\<rfloor>)) ` set (relevant_entries P i pc xt). case x of (pc', \<tau>') \<Rightarrow> pc' < mxl; x \<in> set (succs i (aa, ba) pc); i = ALoad\<rbrakk> \<Longrightarrow> eff\<^sub>i (i, compP f P, aa, ba) = eff\<^sub>i (i, P, aa, ba)
 7. \<And>aa ba x. \<lbrakk>\<tau> = \<lfloor>(aa, ba)\<rfloor>; app\<^sub>i (i, P, pc, mpc, T, aa, ba); xcpt_app i P pc mpc xt (aa, ba); \<forall>x\<in>(\<lambda>pc'. (pc', \<lfloor>eff\<^sub>i (i, P, aa, ba)\<rfloor>)) ` set (succs i (aa, ba) pc) \<union> (\<lambda>x. case x of (f, t, C, h, d) \<Rightarrow> (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length aa - d) aa, ba)\<rfloor>)) ` set (relevant_entries P i pc xt). case x of (pc', \<tau>') \<Rightarrow> pc' < mxl; x \<in> set (succs i (aa, ba) pc); i = AStore\<rbrakk> \<Longrightarrow> eff\<^sub>i (i, compP f P, aa, ba) = eff\<^sub>i (i, P, aa, ba)
 8. \<And>aa ba x. \<lbrakk>\<tau> = \<lfloor>(aa, ba)\<rfloor>; app\<^sub>i (i, P, pc, mpc, T, aa, ba); xcpt_app i P pc mpc xt (aa, ba); \<forall>x\<in>(\<lambda>pc'. (pc', \<lfloor>eff\<^sub>i (i, P, aa, ba)\<rfloor>)) ` set (succs i (aa, ba) pc) \<union> (\<lambda>x. case x of (f, t, C, h, d) \<Rightarrow> (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length aa - d) aa, ba)\<rfloor>)) ` set (relevant_entries P i pc xt). case x of (pc', \<tau>') \<Rightarrow> pc' < mxl; x \<in> set (succs i (aa, ba) pc); i = ALength\<rbrakk> \<Longrightarrow> eff\<^sub>i (i, compP f P, aa, ba) = eff\<^sub>i (i, P, aa, ba)
 9. \<And>aa ba x x91 x92. \<lbrakk>\<tau> = \<lfloor>(aa, ba)\<rfloor>; app\<^sub>i (i, P, pc, mpc, T, aa, ba); xcpt_app i P pc mpc xt (aa, ba); \<forall>x\<in>(\<lambda>pc'. (pc', \<lfloor>eff\<^sub>i (i, P, aa, ba)\<rfloor>)) ` set (succs i (aa, ba) pc) \<union> (\<lambda>x. case x of (f, t, C, h, d) \<Rightarrow> (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length aa - d) aa, ba)\<rfloor>)) ` set (relevant_entries P i pc xt). case x of (pc', \<tau>') \<Rightarrow> pc' < mxl; x \<in> set (succs i (aa, ba) pc); i = Getfield x91 x92\<rbrakk> \<Longrightarrow> eff\<^sub>i (i, compP f P, aa, ba) = eff\<^sub>i (i, P, aa, ba)
 10. \<And>aa ba x x101 x102. \<lbrakk>\<tau> = \<lfloor>(aa, ba)\<rfloor>; app\<^sub>i (i, P, pc, mpc, T, aa, ba); xcpt_app i P pc mpc xt (aa, ba); \<forall>x\<in>(\<lambda>pc'. (pc', \<lfloor>eff\<^sub>i (i, P, aa, ba)\<rfloor>)) ` set (succs i (aa, ba) pc) \<union> (\<lambda>x. case x of (f, t, C, h, d) \<Rightarrow> (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length aa - d) aa, ba)\<rfloor>)) ` set (relevant_entries P i pc xt). case x of (pc', \<tau>') \<Rightarrow> pc' < mxl; x \<in> set (succs i (aa, ba) pc); i = Putfield x101 x102\<rbrakk> \<Longrightarrow> eff\<^sub>i (i, compP f P, aa, ba) = eff\<^sub>i (i, P, aa, ba)
A total of 24 subgoals...
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [simp]: "widen (compP f P) = widen P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. widen (compP f P) = widen P
[PROOF STEP]
apply (rule ext)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. compP f P \<turnstile> x \<le> xa = P \<turnstile> x \<le> xa
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [simp]: "compP f P \<turnstile> \<tau> \<le>' \<tau>' = P \<turnstile> \<tau> \<le>' \<tau>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compP f P \<turnstile> \<tau> \<le>' \<tau>' = P \<turnstile> \<tau> \<le>' \<tau>'
[PROOF STEP]
by (simp add: sup_state_opt_def sup_state_def sup_ty_opt_def)


[STATEMENT]
lemma [simp]: "compP f P,T,mpc,mxl,xt \<turnstile> i,pc :: \<tau>s = P,T,mpc,mxl,xt \<turnstile> i,pc :: \<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compP f P,T,mpc,mxl,xt \<turnstile> i,pc :: \<tau>s = P,T,mpc,mxl,xt \<turnstile> i,pc :: \<tau>s
[PROOF STEP]
by (simp add: wt_instr_def cong: conj_cong)


[STATEMENT]
lemma compT_method:
  fixes e and A and C and Ts and mxl\<^sub>0
  defines [simp]: "E \<equiv> Class C # Ts"
      and [simp]: "A \<equiv> \<lfloor>{..size Ts}\<rfloor>"
      and [simp]: "A' \<equiv> A \<squnion> \<A> e"
      and [simp]: "mxs \<equiv> max_stack e"
      and [simp]: "mxl\<^sub>0 \<equiv> max_vars e"
      and [simp]: "mxl \<equiv> 1 + size Ts + mxl\<^sub>0"
  assumes wf_prog: "wf_prog p P"
  shows "\<lbrakk> P,E \<turnstile>1 e :: T; \<D> e A; \<B> e (size E); set E \<subseteq> types P; P \<turnstile> T \<le> T' \<rbrakk> \<Longrightarrow>
   wt_method (compP2 P) C Ts T' mxs mxl\<^sub>0 (compE2 e @ [Return]) (compxE2 e 0 0)
      (TC0.ty\<^sub>i' mxl [] E A # TC0.compTa P mxl E A [] e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,E \<turnstile>1 e :: T; \<D> e A; \<B> e (length E); set E \<subseteq> types P; P \<turnstile> T \<le> T'\<rbrakk> \<Longrightarrow> wt_method (compP2 P) C Ts T' mxs mxl\<^sub>0 (compE2 e @ [Return]) (compxE2 e 0 0) (TC0.ty\<^sub>i' mxl [] E A # TC0.compTa P mxl E A [] e)
[PROOF STEP]
using wf_prog
[PROOF STATE]
proof (prove)
using this:
wf_prog p P

goal (1 subgoal):
 1. \<lbrakk>P,E \<turnstile>1 e :: T; \<D> e A; \<B> e (length E); set E \<subseteq> types P; P \<turnstile> T \<le> T'\<rbrakk> \<Longrightarrow> wt_method (compP2 P) C Ts T' mxs mxl\<^sub>0 (compE2 e @ [Return]) (compxE2 e 0 0) (TC0.ty\<^sub>i' mxl [] E A # TC0.compTa P mxl E A [] e)
[PROOF STEP]
apply(simp add:wt_method_def TC0.compTa_def TC0.after_def compP2_def compMb2_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P\<rbrakk> \<Longrightarrow> check_types (compP (\<lambda>C M Ts T body. (max_stack body, max_vars body, compE2 body @ [Return], compxE2 body 0 0)) P) (max_stack e) (Suc (length Ts + max_vars e)) (OK (TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor>) # map OK (TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e) @ [OK (TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>))]) \<and> wt_start (compP (\<lambda>C M Ts T body. (max_stack body, max_vars body, compE2 body @ [Return], compxE2 body 0 0)) P) C Ts (max_vars e) (TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<forall>pc. (pc < length (compE2 e) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<not> pc < length (compE2 e) \<longrightarrow> pc < Suc (length (compE2 e)) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]))
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P\<rbrakk> \<Longrightarrow> check_types (compP (\<lambda>C M Ts T body. (max_stack body, max_vars body, compE2 body @ [Return], compxE2 body 0 0)) P) (max_stack e) (Suc (length Ts + max_vars e)) (OK (TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor>) # map OK (TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e) @ [OK (TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>))])
 2. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P\<rbrakk> \<Longrightarrow> wt_start (compP (\<lambda>C M Ts T body. (max_stack body, max_vars body, compE2 body @ [Return], compxE2 body 0 0)) P) C Ts (max_vars e) (TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<forall>pc. (pc < length (compE2 e) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<not> pc < length (compE2 e) \<longrightarrow> pc < Suc (length (compE2 e)) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]))
[PROOF STEP]
apply(simp add:check_types_def TC0.OK_ty\<^sub>i'_in_statesI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P\<rbrakk> \<Longrightarrow> OK (TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)) \<in> states P (max_stack e) (Suc (length Ts + max_vars e)) \<and> OK ` set (TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e) \<subseteq> states P (max_stack e) (Suc (length Ts + max_vars e))
 2. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P\<rbrakk> \<Longrightarrow> wt_start (compP (\<lambda>C M Ts T body. (max_stack body, max_vars body, compE2 body @ [Return], compxE2 body 0 0)) P) C Ts (max_vars e) (TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<forall>pc. (pc < length (compE2 e) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<not> pc < length (compE2 e) \<longrightarrow> pc < Suc (length (compE2 e)) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]))
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P\<rbrakk> \<Longrightarrow> OK (TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)) \<in> states P (max_stack e) (Suc (length Ts + max_vars e))
 2. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P\<rbrakk> \<Longrightarrow> OK ` set (TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e) \<subseteq> states P (max_stack e) (Suc (length Ts + max_vars e))
 3. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P\<rbrakk> \<Longrightarrow> wt_start (compP (\<lambda>C M Ts T body. (max_stack body, max_vars body, compE2 body @ [Return], compxE2 body 0 0)) P) C Ts (max_vars e) (TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<forall>pc. (pc < length (compE2 e) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<not> pc < length (compE2 e) \<longrightarrow> pc < Suc (length (compE2 e)) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]))
[PROOF STEP]
apply(frule WT1_is_type[OF wf_prog])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P\<rbrakk> \<Longrightarrow> set (Class C # Ts) \<subseteq> types P
 2. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; is_type P T\<rbrakk> \<Longrightarrow> OK (TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)) \<in> states P (max_stack e) (Suc (length Ts + max_vars e))
 3. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P\<rbrakk> \<Longrightarrow> OK ` set (TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e) \<subseteq> states P (max_stack e) (Suc (length Ts + max_vars e))
 4. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P\<rbrakk> \<Longrightarrow> wt_start (compP (\<lambda>C M Ts T body. (max_stack body, max_vars body, compE2 body @ [Return], compxE2 body 0 0)) P) C Ts (max_vars e) (TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<forall>pc. (pc < length (compE2 e) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<not> pc < length (compE2 e) \<longrightarrow> pc < Suc (length (compE2 e)) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; is_type P T\<rbrakk> \<Longrightarrow> OK (TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)) \<in> states P (max_stack e) (Suc (length Ts + max_vars e))
 2. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P\<rbrakk> \<Longrightarrow> OK ` set (TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e) \<subseteq> states P (max_stack e) (Suc (length Ts + max_vars e))
 3. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P\<rbrakk> \<Longrightarrow> wt_start (compP (\<lambda>C M Ts T body. (max_stack body, max_vars body, compE2 body @ [Return], compxE2 body 0 0)) P) C Ts (max_vars e) (TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<forall>pc. (pc < length (compE2 e) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<not> pc < length (compE2 e) \<longrightarrow> pc < Suc (length (compE2 e)) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]))
[PROOF STEP]
apply(insert max_stack1[of e])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; is_type P T; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> OK (TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)) \<in> states P (max_stack e) (Suc (length Ts + max_vars e))
 2. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> OK ` set (TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e) \<subseteq> states P (max_stack e) (Suc (length Ts + max_vars e))
 3. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> wt_start (compP (\<lambda>C M Ts T body. (max_stack body, max_vars body, compE2 body @ [Return], compxE2 body 0 0)) P) C Ts (max_vars e) (TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<forall>pc. (pc < length (compE2 e) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<not> pc < length (compE2 e) \<longrightarrow> pc < Suc (length (compE2 e)) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]))
[PROOF STEP]
apply(fastforce intro!: TC0.OK_ty\<^sub>i'_in_statesI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> OK ` set (TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e) \<subseteq> states P (max_stack e) (Suc (length Ts + max_vars e))
 2. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> wt_start (compP (\<lambda>C M Ts T body. (max_stack body, max_vars body, compE2 body @ [Return], compxE2 body 0 0)) P) C Ts (max_vars e) (TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<forall>pc. (pc < length (compE2 e) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<not> pc < length (compE2 e) \<longrightarrow> pc < Suc (length (compE2 e)) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]))
[PROOF STEP]
apply(erule (1) TC1.compT_states[OF TC1.intro])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> set (Class C # Ts) \<subseteq> types P
 2. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> set [] \<subseteq> types P
 3. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> length [] + max_stack e \<le> max_stack e
 4. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> length (Class C # Ts) + max_vars e \<le> Suc (length Ts + max_vars e)
 5. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> wt_start (compP (\<lambda>C M Ts T body. (max_stack body, max_vars body, compE2 body @ [Return], compxE2 body 0 0)) P) C Ts (max_vars e) (TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<forall>pc. (pc < length (compE2 e) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<not> pc < length (compE2 e) \<longrightarrow> pc < Suc (length (compE2 e)) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> set [] \<subseteq> types P
 2. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> length [] + max_stack e \<le> max_stack e
 3. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> length (Class C # Ts) + max_vars e \<le> Suc (length Ts + max_vars e)
 4. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> wt_start (compP (\<lambda>C M Ts T body. (max_stack body, max_vars body, compE2 body @ [Return], compxE2 body 0 0)) P) C Ts (max_vars e) (TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<forall>pc. (pc < length (compE2 e) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<not> pc < length (compE2 e) \<longrightarrow> pc < Suc (length (compE2 e)) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> length [] + max_stack e \<le> max_stack e
 2. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> length (Class C # Ts) + max_vars e \<le> Suc (length Ts + max_vars e)
 3. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> wt_start (compP (\<lambda>C M Ts T body. (max_stack body, max_vars body, compE2 body @ [Return], compxE2 body 0 0)) P) C Ts (max_vars e) (TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<forall>pc. (pc < length (compE2 e) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<not> pc < length (compE2 e) \<longrightarrow> pc < Suc (length (compE2 e)) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> length (Class C # Ts) + max_vars e \<le> Suc (length Ts + max_vars e)
 2. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> wt_start (compP (\<lambda>C M Ts T body. (max_stack body, max_vars body, compE2 body @ [Return], compxE2 body 0 0)) P) C Ts (max_vars e) (TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<forall>pc. (pc < length (compE2 e) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<not> pc < length (compE2 e) \<longrightarrow> pc < Suc (length (compE2 e)) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> wt_start (compP (\<lambda>C M Ts T body. (max_stack body, max_vars body, compE2 body @ [Return], compxE2 body 0 0)) P) C Ts (max_vars e) (TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<forall>pc. (pc < length (compE2 e) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<not> pc < length (compE2 e) \<longrightarrow> pc < Suc (length (compE2 e)) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]))
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> wt_start (compP (\<lambda>C M Ts T body. (max_stack body, max_vars body, compE2 body @ [Return], compxE2 body 0 0)) P) C Ts (max_vars e) (TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)])
 2. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> \<forall>pc. (pc < length (compE2 e) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<not> pc < length (compE2 e) \<longrightarrow> pc < Suc (length (compE2 e)) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)])
[PROOF STEP]
apply(fastforce simp add:wt_start_def TC0.ty\<^sub>i'_def TC0.ty\<^sub>l_def list_all2_conv_all_nth nth_Cons split:nat.split dest:less_antisym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> \<forall>pc. (pc < length (compE2 e) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<not> pc < length (compE2 e) \<longrightarrow> pc < Suc (length (compE2 e)) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)])
[PROOF STEP]
apply (frule (1) TC3.compT_wt_instrs[OF TC3.intro[OF TC1.intro], where ST = "[]" and mxs = "max_stack e" and mxl = "1 + size Ts + max_vars e"])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> \<D> e ?A108
 2. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> \<B> e (length (Class C # Ts))
 3. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> length [] + max_stack e \<le> max_stack e
 4. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> length (Class C # Ts) + max_vars e \<le> 1 + length Ts + max_vars e
 5. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> set (Class C # Ts) \<subseteq> types P
 6. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e; TC2.wt_instrs P ?T\<^sub>r108 (max_stack e) (compE2 e) (compxE2 e 0 (length [])) (TC0.ty\<^sub>i' (1 + length Ts + max_vars e) [] (Class C # Ts) ?A108 # TC0.compT P (1 + length Ts + max_vars e) (Class C # Ts) ?A108 [] e @ [TC0.after P (1 + length Ts + max_vars e) (Class C # Ts) ?A108 [] e])\<rbrakk> \<Longrightarrow> \<forall>pc. (pc < length (compE2 e) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<not> pc < length (compE2 e) \<longrightarrow> pc < Suc (length (compE2 e)) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)])
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> \<B> e (length (Class C # Ts))
 2. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> length [] + max_stack e \<le> max_stack e
 3. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> length (Class C # Ts) + max_vars e \<le> 1 + length Ts + max_vars e
 4. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> set (Class C # Ts) \<subseteq> types P
 5. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e; TC2.wt_instrs P ?T\<^sub>r108 (max_stack e) (compE2 e) (compxE2 e 0 (length [])) (TC0.ty\<^sub>i' (1 + length Ts + max_vars e) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (1 + length Ts + max_vars e) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.after P (1 + length Ts + max_vars e) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e])\<rbrakk> \<Longrightarrow> \<forall>pc. (pc < length (compE2 e) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<not> pc < length (compE2 e) \<longrightarrow> pc < Suc (length (compE2 e)) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)])
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> length [] + max_stack e \<le> max_stack e
 2. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> length (Class C # Ts) + max_vars e \<le> 1 + length Ts + max_vars e
 3. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> set (Class C # Ts) \<subseteq> types P
 4. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e; TC2.wt_instrs P ?T\<^sub>r108 (max_stack e) (compE2 e) (compxE2 e 0 (length [])) (TC0.ty\<^sub>i' (1 + length Ts + max_vars e) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (1 + length Ts + max_vars e) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.after P (1 + length Ts + max_vars e) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e])\<rbrakk> \<Longrightarrow> \<forall>pc. (pc < length (compE2 e) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<not> pc < length (compE2 e) \<longrightarrow> pc < Suc (length (compE2 e)) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)])
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> length (Class C # Ts) + max_vars e \<le> 1 + length Ts + max_vars e
 2. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> set (Class C # Ts) \<subseteq> types P
 3. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e; TC2.wt_instrs P ?T\<^sub>r108 (max_stack e) (compE2 e) (compxE2 e 0 (length [])) (TC0.ty\<^sub>i' (1 + length Ts + max_vars e) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (1 + length Ts + max_vars e) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.after P (1 + length Ts + max_vars e) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e])\<rbrakk> \<Longrightarrow> \<forall>pc. (pc < length (compE2 e) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<not> pc < length (compE2 e) \<longrightarrow> pc < Suc (length (compE2 e)) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)])
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e\<rbrakk> \<Longrightarrow> set (Class C # Ts) \<subseteq> types P
 2. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e; TC2.wt_instrs P ?T\<^sub>r108 (max_stack e) (compE2 e) (compxE2 e 0 (length [])) (TC0.ty\<^sub>i' (1 + length Ts + max_vars e) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (1 + length Ts + max_vars e) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.after P (1 + length Ts + max_vars e) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e])\<rbrakk> \<Longrightarrow> \<forall>pc. (pc < length (compE2 e) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<not> pc < length (compE2 e) \<longrightarrow> pc < Suc (length (compE2 e)) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)])
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); is_class P C \<and> set Ts \<subseteq> types P; P \<turnstile> T \<le> T'; wf_prog p P; 1 \<le> max_stack e; TC2.wt_instrs P ?T\<^sub>r108 (max_stack e) (compE2 e) (compxE2 e 0 (length [])) (TC0.ty\<^sub>i' (1 + length Ts + max_vars e) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (1 + length Ts + max_vars e) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.after P (1 + length Ts + max_vars e) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e])\<rbrakk> \<Longrightarrow> \<forall>pc. (pc < length (compE2 e) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<not> pc < length (compE2 e) \<longrightarrow> pc < Suc (length (compE2 e)) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)])
[PROOF STEP]
apply (clarsimp simp:TC2.wt_instrs_def TC0.after_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); P \<turnstile> T \<le> T'; wf_prog p P; Suc 0 \<le> max_stack e; is_class P C; set Ts \<subseteq> types P; pcs (compxE2 e 0 0) \<subseteq> {0..<length (compE2 e)}; \<forall>pc<length (compE2 e). P,?T\<^sub>r108,max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]\<rbrakk> \<Longrightarrow> (pc < length (compE2 e) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]) \<and> (\<not> pc < length (compE2 e) \<longrightarrow> pc < Suc (length (compE2 e)) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)])
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pc. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); P \<turnstile> T \<le> T'; wf_prog p P; Suc 0 \<le> max_stack e; is_class P C; set Ts \<subseteq> types P; pcs (compxE2 e 0 0) \<subseteq> {0..<length (compE2 e)}; \<forall>pc<length (compE2 e). P,?T\<^sub>r108,max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]\<rbrakk> \<Longrightarrow> pc < length (compE2 e) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]
 2. \<And>pc. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); P \<turnstile> T \<le> T'; wf_prog p P; Suc 0 \<le> max_stack e; is_class P C; set Ts \<subseteq> types P; pcs (compxE2 e 0 0) \<subseteq> {0..<length (compE2 e)}; \<forall>pc<length (compE2 e). P,?T\<^sub>r108,max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]\<rbrakk> \<Longrightarrow> \<not> pc < length (compE2 e) \<longrightarrow> pc < Suc (length (compE2 e)) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]
[PROOF STEP]
apply (fastforce)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); P \<turnstile> T \<le> T'; wf_prog p P; Suc 0 \<le> max_stack e; is_class P C; set Ts \<subseteq> types P; pcs (compxE2 e 0 0) \<subseteq> {0..<length (compE2 e)}; \<forall>pc<length (compE2 e). P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]\<rbrakk> \<Longrightarrow> \<not> pc < length (compE2 e) \<longrightarrow> pc < Suc (length (compE2 e)) \<longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]
[PROOF STEP]
apply(clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); P \<turnstile> T \<le> T'; wf_prog p P; Suc 0 \<le> max_stack e; is_class P C; set Ts \<subseteq> types P; pcs (compxE2 e 0 0) \<subseteq> {0..<length (compE2 e)}; \<forall>pc<length (compE2 e). P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]; \<not> pc < length (compE2 e); pc < Suc (length (compE2 e))\<rbrakk> \<Longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]
[PROOF STEP]
apply(drule (1) less_antisym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); P \<turnstile> T \<le> T'; wf_prog p P; Suc 0 \<le> max_stack e; is_class P C; set Ts \<subseteq> types P; pcs (compxE2 e 0 0) \<subseteq> {0..<length (compE2 e)}; \<forall>pc<length (compE2 e). P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> compE2 e ! pc,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]; pc < Suc (length (compE2 e)); length (compE2 e) = pc\<rbrakk> \<Longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]
[PROOF STEP]
apply(thin_tac "\<forall>x. P x" for P)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc. \<lbrakk>P,Class C # Ts \<turnstile>1 e :: T; \<D> e \<lfloor>{..length Ts}\<rfloor>; \<B> e (Suc (length Ts)); P \<turnstile> T \<le> T'; wf_prog p P; Suc 0 \<le> max_stack e; is_class P C; set Ts \<subseteq> types P; pcs (compxE2 e 0 0) \<subseteq> {0..<length (compE2 e)}; pc < Suc (length (compE2 e)); length (compE2 e) = pc\<rbrakk> \<Longrightarrow> P,T',max_stack e,Suc (length (compE2 e)),compxE2 e 0 0 \<turnstile> Return,pc :: TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compT P (Suc (length Ts + max_vars e)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] e @ [TC0.ty\<^sub>i' (Suc (length Ts + max_vars e)) [T] (Class C # Ts) (\<A> e \<squnion> \<lfloor>{..length Ts}\<rfloor>)]
[PROOF STEP]
apply(clarsimp simp:TC2.wt_defs xcpt_app_pcs xcpt_eff_pcs TC0.ty\<^sub>i'_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem wt_compTP_compP2:
  "wf_J1_prog P \<Longrightarrow> wf_jvm_prog\<^bsub>compTP P\<^esub> (compP2 P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_J1_prog P \<Longrightarrow> wf_jvm_prog\<^bsub>compTP P\<^esub> (compP2 P)
[PROOF STEP]
apply (simp add: wf_jvm_prog_phi_def compP2_def compMb2_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_J1_prog P \<Longrightarrow> wf_prog (\<lambda>Pa C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method Pa C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)) (compP (\<lambda>C M Ts T body. (max_stack body, max_vars body, compE2 body @ [Return], compxE2 body 0 0)) P)
[PROOF STEP]
apply (rule wf_prog_compPI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C M Ts T m. \<lbrakk>wf_J1_prog P; P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>m\<rfloor> in C; wf_mdecl ?wf\<^sub>1 P C (M, Ts, T, \<lfloor>m\<rfloor>)\<rbrakk> \<Longrightarrow> wf_mdecl (\<lambda>Pa C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method Pa C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)) (compP (\<lambda>C M Ts T body. (max_stack body, max_vars body, compE2 body @ [Return], compxE2 body 0 0)) P) C (M, Ts, T, \<lfloor>(max_stack m, max_vars m, compE2 m @ [Return], compxE2 m 0 0)\<rfloor>)
 2. wf_J1_prog P \<Longrightarrow> wf_prog ?wf\<^sub>1 P
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wf_J1_prog P \<Longrightarrow> wf_prog ?wf\<^sub>1 P
 2. \<And>C M Ts T m. \<lbrakk>wf_J1_prog P; P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>m\<rfloor> in C; wf_mdecl ?wf\<^sub>1 P C (M, Ts, T, \<lfloor>m\<rfloor>)\<rbrakk> \<Longrightarrow> wf_mdecl (\<lambda>Pa C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method Pa C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)) (compP (\<lambda>C M Ts T body. (max_stack body, max_vars body, compE2 body @ [Return], compxE2 body 0 0)) P) C (M, Ts, T, \<lfloor>(max_stack m, max_vars m, compE2 m @ [Return], compxE2 m 0 0)\<rfloor>)
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C M Ts T m. \<lbrakk>wf_J1_prog P; P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>m\<rfloor> in C; wf_mdecl wf_J1_mdecl P C (M, Ts, T, \<lfloor>m\<rfloor>)\<rbrakk> \<Longrightarrow> wf_mdecl (\<lambda>Pa C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method Pa C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)) (compP (\<lambda>C M Ts T body. (max_stack body, max_vars body, compE2 body @ [Return], compxE2 body 0 0)) P) C (M, Ts, T, \<lfloor>(max_stack m, max_vars m, compE2 m @ [Return], compxE2 m 0 0)\<rfloor>)
[PROOF STEP]
apply (clarsimp simp add: wf_mdecl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C M Ts T m T'. \<lbrakk>wf_J1_prog P; P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>m\<rfloor> in C; \<forall>x\<in>set Ts. is_type P x; is_type P T; \<D> m \<lfloor>{..length Ts}\<rfloor>; P,Class C # Ts \<turnstile>1 m :: T'; P \<turnstile> T' \<le> T; \<B> m (Suc (length Ts)); syncvars m\<rbrakk> \<Longrightarrow> wt_method (compP (\<lambda>C M Ts T body. (max_stack body, max_vars body, compE2 body @ [Return], compxE2 body 0 0)) P) C Ts T (max_stack m) (max_vars m) (compE2 m @ [Return]) (compxE2 m 0 0) (compTP P C M)
[PROOF STEP]
apply (simp add: compTP_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C M Ts T m T'. \<lbrakk>wf_J1_prog P; P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>m\<rfloor> in C; \<forall>x\<in>set Ts. is_type P x; is_type P T; \<D> m \<lfloor>{..length Ts}\<rfloor>; P,Class C # Ts \<turnstile>1 m :: T'; P \<turnstile> T' \<le> T; \<B> m (Suc (length Ts)); syncvars m\<rbrakk> \<Longrightarrow> wt_method (compP (\<lambda>C M Ts T body. (max_stack body, max_vars body, compE2 body @ [Return], compxE2 body 0 0)) P) C Ts T (max_stack m) (max_vars m) (compE2 m @ [Return]) (compxE2 m 0 0) (TC0.ty\<^sub>i' (Suc (length Ts + max_vars m)) [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC0.compTa P (Suc (length Ts + max_vars m)) (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] m)
[PROOF STEP]
apply (rule compT_method [simplified compP2_def compMb2_def, simplified])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>C M Ts T m T'. \<lbrakk>wf_J1_prog P; P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>m\<rfloor> in C; \<forall>x\<in>set Ts. is_type P x; is_type P T; \<D> m \<lfloor>{..length Ts}\<rfloor>; P,Class C # Ts \<turnstile>1 m :: T'; P \<turnstile> T' \<le> T; \<B> m (Suc (length Ts)); syncvars m\<rbrakk> \<Longrightarrow> wf_prog (?p19 C M Ts T m T') P
 2. \<And>C M Ts T m T'. \<lbrakk>wf_J1_prog P; P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>m\<rfloor> in C; \<forall>x\<in>set Ts. is_type P x; is_type P T; \<D> m \<lfloor>{..length Ts}\<rfloor>; P,Class C # Ts \<turnstile>1 m :: T'; P \<turnstile> T' \<le> T; \<B> m (Suc (length Ts)); syncvars m\<rbrakk> \<Longrightarrow> P,Class C # Ts \<turnstile>1 m :: ?T19 C M Ts T m T'
 3. \<And>C M Ts T m T'. \<lbrakk>wf_J1_prog P; P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>m\<rfloor> in C; \<forall>x\<in>set Ts. is_type P x; is_type P T; \<D> m \<lfloor>{..length Ts}\<rfloor>; P,Class C # Ts \<turnstile>1 m :: T'; P \<turnstile> T' \<le> T; \<B> m (Suc (length Ts)); syncvars m\<rbrakk> \<Longrightarrow> \<D> m \<lfloor>{..length Ts}\<rfloor>
 4. \<And>C M Ts T m T'. \<lbrakk>wf_J1_prog P; P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>m\<rfloor> in C; \<forall>x\<in>set Ts. is_type P x; is_type P T; \<D> m \<lfloor>{..length Ts}\<rfloor>; P,Class C # Ts \<turnstile>1 m :: T'; P \<turnstile> T' \<le> T; \<B> m (Suc (length Ts)); syncvars m\<rbrakk> \<Longrightarrow> \<B> m (Suc (length Ts))
 5. \<And>C M Ts T m T'. \<lbrakk>wf_J1_prog P; P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>m\<rfloor> in C; \<forall>x\<in>set Ts. is_type P x; is_type P T; \<D> m \<lfloor>{..length Ts}\<rfloor>; P,Class C # Ts \<turnstile>1 m :: T'; P \<turnstile> T' \<le> T; \<B> m (Suc (length Ts)); syncvars m\<rbrakk> \<Longrightarrow> is_class P C \<and> set Ts \<subseteq> types P
 6. \<And>C M Ts T m T'. \<lbrakk>wf_J1_prog P; P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>m\<rfloor> in C; \<forall>x\<in>set Ts. is_type P x; is_type P T; \<D> m \<lfloor>{..length Ts}\<rfloor>; P,Class C # Ts \<turnstile>1 m :: T'; P \<turnstile> T' \<le> T; \<B> m (Suc (length Ts)); syncvars m\<rbrakk> \<Longrightarrow> P \<turnstile> ?T19 C M Ts T m T' \<le> T
[PROOF STEP]
apply assumption+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C M Ts T m T'. \<lbrakk>wf_J1_prog P; P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>m\<rfloor> in C; \<forall>x\<in>set Ts. is_type P x; is_type P T; \<D> m \<lfloor>{..length Ts}\<rfloor>; P,Class C # Ts \<turnstile>1 m :: T'; P \<turnstile> T' \<le> T; \<B> m (Suc (length Ts)); syncvars m\<rbrakk> \<Longrightarrow> is_class P C \<and> set Ts \<subseteq> types P
 2. \<And>C M Ts T m T'. \<lbrakk>wf_J1_prog P; P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>m\<rfloor> in C; \<forall>x\<in>set Ts. is_type P x; is_type P T; \<D> m \<lfloor>{..length Ts}\<rfloor>; P,Class C # Ts \<turnstile>1 m :: T'; P \<turnstile> T' \<le> T; \<B> m (Suc (length Ts)); syncvars m\<rbrakk> \<Longrightarrow> P \<turnstile> T' \<le> T
[PROOF STEP]
apply (drule (1) sees_wf_mdecl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C M Ts T m T'. \<lbrakk>P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>m\<rfloor> in C; \<forall>x\<in>set Ts. is_type P x; is_type P T; \<D> m \<lfloor>{..length Ts}\<rfloor>; P,Class C # Ts \<turnstile>1 m :: T'; P \<turnstile> T' \<le> T; \<B> m (Suc (length Ts)); syncvars m; wf_mdecl wf_J1_mdecl P C (M, Ts, T, \<lfloor>m\<rfloor>)\<rbrakk> \<Longrightarrow> is_class P C \<and> set Ts \<subseteq> types P
 2. \<And>C M Ts T m T'. \<lbrakk>wf_J1_prog P; P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>m\<rfloor> in C; \<forall>x\<in>set Ts. is_type P x; is_type P T; \<D> m \<lfloor>{..length Ts}\<rfloor>; P,Class C # Ts \<turnstile>1 m :: T'; P \<turnstile> T' \<le> T; \<B> m (Suc (length Ts)); syncvars m\<rbrakk> \<Longrightarrow> P \<turnstile> T' \<le> T
[PROOF STEP]
apply (simp add: wf_mdecl_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C M Ts T m T'. \<lbrakk>P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>m\<rfloor> in C; \<forall>x\<in>set Ts. is_type P x; is_type P T; \<D> m \<lfloor>{..length Ts}\<rfloor>; P,Class C # Ts \<turnstile>1 m :: T'; P \<turnstile> T' \<le> T; \<B> m (Suc (length Ts)); syncvars m; \<exists>T'. P,Class C # Ts \<turnstile>1 m :: T' \<and> P \<turnstile> T' \<le> T\<rbrakk> \<Longrightarrow> is_class P C \<and> set Ts \<subseteq> types P
 2. \<And>C M Ts T m T'. \<lbrakk>wf_J1_prog P; P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>m\<rfloor> in C; \<forall>x\<in>set Ts. is_type P x; is_type P T; \<D> m \<lfloor>{..length Ts}\<rfloor>; P,Class C # Ts \<turnstile>1 m :: T'; P \<turnstile> T' \<le> T; \<B> m (Suc (length Ts)); syncvars m\<rbrakk> \<Longrightarrow> P \<turnstile> T' \<le> T
[PROOF STEP]
apply (fastforce intro: sees_method_is_class)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C M Ts T m T'. \<lbrakk>wf_J1_prog P; P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>m\<rfloor> in C; \<forall>x\<in>set Ts. is_type P x; is_type P T; \<D> m \<lfloor>{..length Ts}\<rfloor>; P,Class C # Ts \<turnstile>1 m :: T'; P \<turnstile> T' \<le> T; \<B> m (Suc (length Ts)); syncvars m\<rbrakk> \<Longrightarrow> P \<turnstile> T' \<le> T
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem wt_compP2:
  "wf_J1_prog P \<Longrightarrow> wf_jvm_prog (compP2 P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_J1_prog P \<Longrightarrow> wf_jvm_prog (compP2 P)
[PROOF STEP]
by(auto simp add: wf_jvm_prog_def intro: wt_compTP_compP2)