[STATEMENT]
lemma [simp]: "types (compP f P) = types P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. types (compP f P) = types P
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. types (compP f P) = types P
[PROOF STEP]
by auto


[STATEMENT]
lemma [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]
(*<*)
[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>)"
(*<*)(is "?A = ?B")
[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]
obtain ST LT where \<tau>: "\<tau> = (ST, LT)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ST LT. \<tau> = (ST, LT) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases \<tau>) simp
[PROOF STATE]
proof (state)
this:
\<tau> = (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]
then
[PROOF STATE]
proof (chain)
picking this:
\<tau> = (ST, LT)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<tau> = (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(cases i)
[PROOF STATE]
proof (state)
goal (18 subgoals):
 1. \<And>x1. \<lbrakk>\<tau> = (ST, LT); i = Load x1\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 2. \<And>x2. \<lbrakk>\<tau> = (ST, LT); i = Store x2\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 3. \<And>x3. \<lbrakk>\<tau> = (ST, LT); i = Push x3\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 4. \<And>x4. \<lbrakk>\<tau> = (ST, LT); i = New x4\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 5. \<And>x51 x52. \<lbrakk>\<tau> = (ST, LT); i = Getfield x51 x52\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 6. \<And>x61 x62 x63. \<lbrakk>\<tau> = (ST, LT); i = Getstatic x61 x62 x63\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 7. \<And>x71 x72. \<lbrakk>\<tau> = (ST, LT); i = Putfield x71 x72\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 8. \<And>x81 x82 x83. \<lbrakk>\<tau> = (ST, LT); i = Putstatic x81 x82 x83\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 9. \<And>x9. \<lbrakk>\<tau> = (ST, LT); i = Checkcast x9\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 10. \<And>x101 x102. \<lbrakk>\<tau> = (ST, LT); i = Invoke x101 x102\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
A total of 18 subgoals...
[PROOF STEP]
case Invoke
[PROOF STATE]
proof (state)
this:
i = Invoke x101_ x102_

goal (18 subgoals):
 1. \<And>x1. \<lbrakk>\<tau> = (ST, LT); i = Load x1\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 2. \<And>x2. \<lbrakk>\<tau> = (ST, LT); i = Store x2\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 3. \<And>x3. \<lbrakk>\<tau> = (ST, LT); i = Push x3\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 4. \<And>x4. \<lbrakk>\<tau> = (ST, LT); i = New x4\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 5. \<And>x51 x52. \<lbrakk>\<tau> = (ST, LT); i = Getfield x51 x52\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 6. \<And>x61 x62 x63. \<lbrakk>\<tau> = (ST, LT); i = Getstatic x61 x62 x63\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 7. \<And>x71 x72. \<lbrakk>\<tau> = (ST, LT); i = Putfield x71 x72\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 8. \<And>x81 x82 x83. \<lbrakk>\<tau> = (ST, LT); i = Putstatic x81 x82 x83\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 9. \<And>x9. \<lbrakk>\<tau> = (ST, LT); i = Checkcast x9\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 10. \<And>x101 x102. \<lbrakk>\<tau> = (ST, LT); i = Invoke x101 x102\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
A total of 18 subgoals...
[PROOF STEP]
show ?thesis
[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(rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) \<Longrightarrow> app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 2. app\<^sub>i (i, P, pc, mpc, T, \<tau>) \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>)
[PROOF STEP]
assume ?A
[PROOF STATE]
proof (state)
this:
app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>)

goal (2 subgoals):
 1. app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) \<Longrightarrow> app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 2. app\<^sub>i (i, P, pc, mpc, T, \<tau>) \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>)
[PROOF STEP]
show ?B
[PROOF STATE]
proof (prove)
using this:
app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>)

goal (1 subgoal):
 1. app\<^sub>i (i, P, pc, mpc, T, \<tau>)
[PROOF STEP]
using Invoke \<tau>
[PROOF STATE]
proof (prove)
using this:
app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>)
i = Invoke x101_ x102_
\<tau> = (ST, LT)

goal (1 subgoal):
 1. app\<^sub>i (i, P, pc, mpc, T, \<tau>)
[PROOF STEP]
by auto (fastforce dest!: sees_method_compPD)
[PROOF STATE]
proof (state)
this:
app\<^sub>i (i, P, pc, mpc, T, \<tau>)

goal (1 subgoal):
 1. app\<^sub>i (i, P, pc, mpc, T, \<tau>) \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. app\<^sub>i (i, P, pc, mpc, T, \<tau>) \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>)
[PROOF STEP]
assume ?B
[PROOF STATE]
proof (state)
this:
app\<^sub>i (i, P, pc, mpc, T, \<tau>)

goal (1 subgoal):
 1. app\<^sub>i (i, P, pc, mpc, T, \<tau>) \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
app\<^sub>i (i, P, pc, mpc, T, \<tau>)
[PROOF STEP]
show ?A
[PROOF STATE]
proof (prove)
using this:
app\<^sub>i (i, P, pc, mpc, T, \<tau>)

goal (1 subgoal):
 1. app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>)
[PROOF STEP]
using Invoke \<tau>
[PROOF STATE]
proof (prove)
using this:
app\<^sub>i (i, P, pc, mpc, T, \<tau>)
i = Invoke x101_ x102_
\<tau> = (ST, LT)

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

goal:
No subgoals!
[PROOF STEP]
qed
[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 (17 subgoals):
 1. \<And>x1. \<lbrakk>\<tau> = (ST, LT); i = Load x1\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 2. \<And>x2. \<lbrakk>\<tau> = (ST, LT); i = Store x2\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 3. \<And>x3. \<lbrakk>\<tau> = (ST, LT); i = Push x3\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 4. \<And>x4. \<lbrakk>\<tau> = (ST, LT); i = New x4\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 5. \<And>x51 x52. \<lbrakk>\<tau> = (ST, LT); i = Getfield x51 x52\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 6. \<And>x61 x62 x63. \<lbrakk>\<tau> = (ST, LT); i = Getstatic x61 x62 x63\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 7. \<And>x71 x72. \<lbrakk>\<tau> = (ST, LT); i = Putfield x71 x72\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 8. \<And>x81 x82 x83. \<lbrakk>\<tau> = (ST, LT); i = Putstatic x81 x82 x83\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 9. \<And>x9. \<lbrakk>\<tau> = (ST, LT); i = Checkcast x9\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 10. \<And>x111 x112 x113. \<lbrakk>\<tau> = (ST, LT); i = Invokestatic x111 x112 x113\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
A total of 17 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (17 subgoals):
 1. \<And>x1. \<lbrakk>\<tau> = (ST, LT); i = Load x1\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 2. \<And>x2. \<lbrakk>\<tau> = (ST, LT); i = Store x2\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 3. \<And>x3. \<lbrakk>\<tau> = (ST, LT); i = Push x3\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 4. \<And>x4. \<lbrakk>\<tau> = (ST, LT); i = New x4\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 5. \<And>x51 x52. \<lbrakk>\<tau> = (ST, LT); i = Getfield x51 x52\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 6. \<And>x61 x62 x63. \<lbrakk>\<tau> = (ST, LT); i = Getstatic x61 x62 x63\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 7. \<And>x71 x72. \<lbrakk>\<tau> = (ST, LT); i = Putfield x71 x72\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 8. \<And>x81 x82 x83. \<lbrakk>\<tau> = (ST, LT); i = Putstatic x81 x82 x83\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 9. \<And>x9. \<lbrakk>\<tau> = (ST, LT); i = Checkcast x9\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 10. \<And>x111 x112 x113. \<lbrakk>\<tau> = (ST, LT); i = Invokestatic x111 x112 x113\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
A total of 17 subgoals...
[PROOF STEP]
case (Invokestatic x111 x112 x113)
[PROOF STATE]
proof (state)
this:
i = Invokestatic x111 x112 x113

goal (17 subgoals):
 1. \<And>x1. \<lbrakk>\<tau> = (ST, LT); i = Load x1\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 2. \<And>x2. \<lbrakk>\<tau> = (ST, LT); i = Store x2\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 3. \<And>x3. \<lbrakk>\<tau> = (ST, LT); i = Push x3\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 4. \<And>x4. \<lbrakk>\<tau> = (ST, LT); i = New x4\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 5. \<And>x51 x52. \<lbrakk>\<tau> = (ST, LT); i = Getfield x51 x52\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 6. \<And>x61 x62 x63. \<lbrakk>\<tau> = (ST, LT); i = Getstatic x61 x62 x63\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 7. \<And>x71 x72. \<lbrakk>\<tau> = (ST, LT); i = Putfield x71 x72\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 8. \<And>x81 x82 x83. \<lbrakk>\<tau> = (ST, LT); i = Putstatic x81 x82 x83\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 9. \<And>x9. \<lbrakk>\<tau> = (ST, LT); i = Checkcast x9\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 10. \<And>x111 x112 x113. \<lbrakk>\<tau> = (ST, LT); i = Invokestatic x111 x112 x113\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
A total of 17 subgoals...
[PROOF STEP]
show ?thesis
[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(rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) \<Longrightarrow> app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 2. app\<^sub>i (i, P, pc, mpc, T, \<tau>) \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>)
[PROOF STEP]
assume ?A
[PROOF STATE]
proof (state)
this:
app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>)

goal (2 subgoals):
 1. app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) \<Longrightarrow> app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 2. app\<^sub>i (i, P, pc, mpc, T, \<tau>) \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>)
[PROOF STEP]
show ?B
[PROOF STATE]
proof (prove)
using this:
app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>)

goal (1 subgoal):
 1. app\<^sub>i (i, P, pc, mpc, T, \<tau>)
[PROOF STEP]
using Invokestatic \<tau>
[PROOF STATE]
proof (prove)
using this:
app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>)
i = Invokestatic x111 x112 x113
\<tau> = (ST, LT)

goal (1 subgoal):
 1. app\<^sub>i (i, P, pc, mpc, T, \<tau>)
[PROOF STEP]
by auto (fastforce dest!: sees_method_compPD)
[PROOF STATE]
proof (state)
this:
app\<^sub>i (i, P, pc, mpc, T, \<tau>)

goal (1 subgoal):
 1. app\<^sub>i (i, P, pc, mpc, T, \<tau>) \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. app\<^sub>i (i, P, pc, mpc, T, \<tau>) \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>)
[PROOF STEP]
assume ?B
[PROOF STATE]
proof (state)
this:
app\<^sub>i (i, P, pc, mpc, T, \<tau>)

goal (1 subgoal):
 1. app\<^sub>i (i, P, pc, mpc, T, \<tau>) \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
app\<^sub>i (i, P, pc, mpc, T, \<tau>)
[PROOF STEP]
show ?A
[PROOF STATE]
proof (prove)
using this:
app\<^sub>i (i, P, pc, mpc, T, \<tau>)

goal (1 subgoal):
 1. app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>)
[PROOF STEP]
using Invokestatic \<tau>
[PROOF STATE]
proof (prove)
using this:
app\<^sub>i (i, P, pc, mpc, T, \<tau>)
i = Invokestatic x111 x112 x113
\<tau> = (ST, LT)

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

goal:
No subgoals!
[PROOF STEP]
qed
[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 (16 subgoals):
 1. \<And>x1. \<lbrakk>\<tau> = (ST, LT); i = Load x1\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 2. \<And>x2. \<lbrakk>\<tau> = (ST, LT); i = Store x2\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 3. \<And>x3. \<lbrakk>\<tau> = (ST, LT); i = Push x3\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 4. \<And>x4. \<lbrakk>\<tau> = (ST, LT); i = New x4\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 5. \<And>x51 x52. \<lbrakk>\<tau> = (ST, LT); i = Getfield x51 x52\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 6. \<And>x61 x62 x63. \<lbrakk>\<tau> = (ST, LT); i = Getstatic x61 x62 x63\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 7. \<And>x71 x72. \<lbrakk>\<tau> = (ST, LT); i = Putfield x71 x72\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 8. \<And>x81 x82 x83. \<lbrakk>\<tau> = (ST, LT); i = Putstatic x81 x82 x83\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 9. \<And>x9. \<lbrakk>\<tau> = (ST, LT); i = Checkcast x9\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
 10. \<lbrakk>\<tau> = (ST, LT); i = Return\<rbrakk> \<Longrightarrow> app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)
A total of 16 subgoals...
[PROOF STEP]
qed auto
[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]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_relevant_entry (compP f P) i = is_relevant_entry P i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_relevant_entry (compP f P) i = is_relevant_entry P i
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_relevant_entry (compP f P) i = is_relevant_entry P i
[PROOF STEP]
fix pc e
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_relevant_entry (compP f P) i = is_relevant_entry P i
[PROOF STEP]
have "is_relevant_entry (compP f P) i pc e = is_relevant_entry P i pc e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_relevant_entry (compP f P) i pc e = is_relevant_entry P i pc e
[PROOF STEP]
by(cases i) (auto simp: is_relevant_entry_def)
[PROOF STATE]
proof (state)
this:
is_relevant_entry (compP f P) i pc e = is_relevant_entry P i pc e

goal (1 subgoal):
 1. is_relevant_entry (compP f P) i = is_relevant_entry P i
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
is_relevant_entry (compP f P) i ?pc2 ?e2 = is_relevant_entry P i ?pc2 ?e2

goal (1 subgoal):
 1. is_relevant_entry (compP f P) i = is_relevant_entry P i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_relevant_entry (compP f P) i ?pc2 ?e2 = is_relevant_entry P i ?pc2 ?e2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_relevant_entry (compP f P) i ?pc2 ?e2 = is_relevant_entry P i ?pc2 ?e2

goal (1 subgoal):
 1. is_relevant_entry (compP f P) i = is_relevant_entry P i
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
is_relevant_entry (compP f P) i = is_relevant_entry P i

goal:
No subgoals!
[PROOF STEP]
qed


[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]
(*<*)
[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]
(*<*)
[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]
by (simp add: app_def xcpt_app_def eff_def xcpt_eff_def norm_eff_def)
   (fastforce simp add: image_def)


[STATEMENT]
lemma [simp]:
assumes "app i P mpc T pc mxl xt \<tau>"
shows "eff i (compP f P) pc xt \<tau> = eff i P pc xt \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eff i (compP f P) pc xt \<tau> = eff i P pc xt \<tau>
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eff i (compP f P) pc xt \<tau> = eff i P pc xt \<tau>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
app i P mpc T pc mxl xt \<tau>

goal (1 subgoal):
 1. eff i (compP f P) pc xt \<tau> = eff i P pc xt \<tau>
[PROOF STEP]
proof(clarsimp simp: eff_def norm_eff_def xcpt_eff_def app_def, cases i)
[PROOF STATE]
proof (state)
goal (18 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>(Class C # 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); app i P mpc T pc mxl xt \<tau>; 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>(Class C # 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); app i P mpc T pc mxl xt \<tau>; 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>(Class C # 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); app i P mpc T pc mxl xt \<tau>; 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>(Class C # 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); app i P mpc T pc mxl xt \<tau>; 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 x51 x52. \<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>(Class C # 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); app i P mpc T pc mxl xt \<tau>; i = Getfield x51 x52\<rbrakk> \<Longrightarrow> eff\<^sub>i (i, compP f P, aa, ba) = eff\<^sub>i (i, P, aa, ba)
 6. \<And>aa ba x x61 x62 x63. \<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>(Class C # 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); app i P mpc T pc mxl xt \<tau>; i = Getstatic x61 x62 x63\<rbrakk> \<Longrightarrow> eff\<^sub>i (i, compP f P, aa, ba) = eff\<^sub>i (i, P, aa, ba)
 7. \<And>aa ba x x71 x72. \<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>(Class C # 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); app i P mpc T pc mxl xt \<tau>; i = Putfield x71 x72\<rbrakk> \<Longrightarrow> eff\<^sub>i (i, compP f P, aa, ba) = eff\<^sub>i (i, P, aa, ba)
 8. \<And>aa ba x x81 x82 x83. \<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>(Class C # 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); app i P mpc T pc mxl xt \<tau>; i = Putstatic x81 x82 x83\<rbrakk> \<Longrightarrow> eff\<^sub>i (i, compP f P, aa, ba) = eff\<^sub>i (i, P, aa, ba)
 9. \<And>aa ba x x9. \<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>(Class C # 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); app i P mpc T pc mxl xt \<tau>; i = Checkcast x9\<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>(Class C # 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); app i P mpc T pc mxl xt \<tau>; i = Invoke x101 x102\<rbrakk> \<Longrightarrow> eff\<^sub>i (i, compP f P, aa, ba) = eff\<^sub>i (i, P, aa, ba)
A total of 18 subgoals...
[PROOF STEP]
qed auto


[STATEMENT]
lemma [simp]: "subtype (compP f P) = subtype P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subtype (compP f P) = subtype P
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subtype (compP f P) = subtype P
[PROOF STEP]
by (rule ext)+ simp


[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]
(*<*)
[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]
(*<*)
[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_NonStatic:
  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]: "mxl\<^sub>0 \<equiv> max_vars e"
  assumes mxs: "max_stack e = mxs"
    and mxl: "Suc (length Ts + max_vars e) = mxl"
  assumes wf: "wf_prog p P" and wte: "P,E \<turnstile>\<^sub>1 e :: T" and \<D>: "\<D> e A"
    and \<B>: "\<B> e (size E)" and E_P: "set E \<subseteq> types P" and wid: "P \<turnstile> T \<le> T\<^sub>r"
  shows "wt_method (compP\<^sub>2 P) C NonStatic Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return])
    (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)"
(*<*)(is "wt_method ?P C ?b Ts T\<^sub>r mxs mxl\<^sub>0 ?is ?xt ?\<tau>s")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C NonStatic Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C NonStatic Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
let ?n = "length E + mxl\<^sub>0"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C NonStatic Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
have wt_compE: "P,T\<^sub>r,mxs \<turnstile> compE\<^sub>2 e, compxE\<^sub>2 e 0 (length []) [::]
        TC0.ty\<^sub>i' ?n [] E A # TC1.compT P ?n E A [] e @[TC0.after P ?n E A [] e]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> compE\<^sub>2 e, compxE\<^sub>2 e 0 (length []) [::] TC0.ty\<^sub>i' (length E + mxl\<^sub>0) [] E A # TC1.compT P (length E + mxl\<^sub>0) E A [] e @ [TC0.after P (length E + mxl\<^sub>0) E A [] e]
[PROOF STEP]
using mxs TC2.compT_wt_instrs [OF wte \<D> \<B>, of "[]" mxs ?n T\<^sub>r]
[PROOF STATE]
proof (prove)
using this:
max_stack e = mxs
\<lbrakk>length [] + max_stack e \<le> mxs; length E + max_vars e \<le> length E + mxl\<^sub>0\<rbrakk> \<Longrightarrow> \<turnstile> compE\<^sub>2 e, compxE\<^sub>2 e 0 (length []) [::] TC0.ty\<^sub>i' (length E + mxl\<^sub>0) [] E A # TC1.compT P (length E + mxl\<^sub>0) E A [] e @ [TC0.after P (length E + mxl\<^sub>0) E A [] e]

goal (1 subgoal):
 1. \<turnstile> compE\<^sub>2 e, compxE\<^sub>2 e 0 (length []) [::] TC0.ty\<^sub>i' (length E + mxl\<^sub>0) [] E A # TC1.compT P (length E + mxl\<^sub>0) E A [] e @ [TC0.after P (length E + mxl\<^sub>0) E A [] e]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<turnstile> compE\<^sub>2 e, compxE\<^sub>2 e 0 (length []) [::] TC0.ty\<^sub>i' (length E + mxl\<^sub>0) [] E A # TC1.compT P (length E + mxl\<^sub>0) E A [] e @ [TC0.after P (length E + mxl\<^sub>0) E A [] e]

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C NonStatic Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
have "OK (ty\<^sub>i' [T] E A') \<in> states P mxs mxl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OK (ty\<^sub>i' [T] E A') \<in> states P mxs mxl
[PROOF STEP]
using mxs WT\<^sub>1_is_type[OF wf wte E_P] max_stack1[OF wte] OK_ty\<^sub>i'_in_statesI[OF E_P]
[PROOF STATE]
proof (prove)
using this:
max_stack e = mxs
is_type P T
1 \<le> max_stack e
\<lbrakk>set ?ST \<subseteq> types P; length ?ST \<le> ?mxs\<rbrakk> \<Longrightarrow> OK (ty\<^sub>i' ?ST E ?A) \<in> states P ?mxs mxl

goal (1 subgoal):
 1. OK (ty\<^sub>i' [T] E A') \<in> states P mxs mxl
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
OK (ty\<^sub>i' [T] E A') \<in> states P mxs mxl

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C NonStatic Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
OK (ty\<^sub>i' [T] E A') \<in> states P mxs mxl

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C NonStatic Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
have "OK ` set (compT E A [] e) \<subseteq> states P mxs mxl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OK ` set (compT E A [] e) \<subseteq> states P mxs mxl
[PROOF STEP]
using mxs mxl wid compT_states(1)[OF wf wte E_P]
[PROOF STATE]
proof (prove)
using this:
max_stack e = mxs
Suc (length Ts + max_vars e) = mxl
subtype P T T\<^sub>r
\<lbrakk>set ?ST \<subseteq> types P; length ?ST + max_stack e \<le> ?mxs; length E + max_vars e \<le> mxl\<rbrakk> \<Longrightarrow> OK ` set (compT E ?A ?ST e) \<subseteq> states P ?mxs mxl

goal (1 subgoal):
 1. OK ` set (compT E A [] e) \<subseteq> states P mxs mxl
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
OK ` set (compT E A [] e) \<subseteq> states P mxs mxl

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C NonStatic Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
OK (ty\<^sub>i' [T] E A') \<in> states P mxs mxl
OK ` set (compT E A [] e) \<subseteq> states P mxs mxl
[PROOF STEP]
have "check_types ?P mxs ?n (map OK ?\<tau>s)"
[PROOF STATE]
proof (prove)
using this:
OK (ty\<^sub>i' [T] E A') \<in> states P mxs mxl
OK ` set (compT E A [] e) \<subseteq> states P mxs mxl

goal (1 subgoal):
 1. check_types (compP\<^sub>2 P) mxs (length E + mxl\<^sub>0) (map OK (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e))
[PROOF STEP]
using mxl wte E_P
[PROOF STATE]
proof (prove)
using this:
OK (ty\<^sub>i' [T] E A') \<in> states P mxs mxl
OK ` set (compT E A [] e) \<subseteq> states P mxs mxl
Suc (length Ts + max_vars e) = mxl
P,E \<turnstile>\<^sub>1 e :: T
set E \<subseteq> types P

goal (1 subgoal):
 1. check_types (compP\<^sub>2 P) mxs (length E + mxl\<^sub>0) (map OK (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e))
[PROOF STEP]
by (simp add: compT\<^sub>a_def after_def check_types_def)
[PROOF STATE]
proof (state)
this:
check_types (compP\<^sub>2 P) mxs (length E + mxl\<^sub>0) (map OK (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e))

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C NonStatic Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
check_types (compP\<^sub>2 P) mxs (length E + mxl\<^sub>0) (map OK (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e))

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C NonStatic Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
have "wt_start ?P C ?b Ts mxl\<^sub>0 ?\<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wt_start (compP\<^sub>2 P) C NonStatic Ts mxl\<^sub>0 (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
using mxl
[PROOF STATE]
proof (prove)
using this:
Suc (length Ts + max_vars e) = mxl

goal (1 subgoal):
 1. wt_start (compP\<^sub>2 P) C NonStatic Ts mxl\<^sub>0 (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
by (auto simp: wt_start_def ty\<^sub>i'_def ty\<^sub>l_def list_all2_conv_all_nth nth_Cons
             split: nat.split)
[PROOF STATE]
proof (state)
this:
wt_start (compP\<^sub>2 P) C NonStatic Ts mxl\<^sub>0 (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C NonStatic Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wt_start (compP\<^sub>2 P) C NonStatic Ts mxl\<^sub>0 (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C NonStatic Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
wt_start (compP\<^sub>2 P) C NonStatic Ts mxl\<^sub>0 (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C NonStatic Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
fix pc
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C NonStatic Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
assume pc: "pc < size ?is"
[PROOF STATE]
proof (state)
this:
pc < length (compE\<^sub>2 e @ [Return])

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C NonStatic Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pc < length (compE\<^sub>2 e @ [Return])
[PROOF STEP]
have "?P,T\<^sub>r,mxs,size ?is,?xt \<turnstile> ?is!pc,pc :: ?\<tau>s"
[PROOF STATE]
proof (prove)
using this:
pc < length (compE\<^sub>2 e @ [Return])

goal (1 subgoal):
 1. compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
[PROOF STEP]
proof(cases "pc < length (compE\<^sub>2 e)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>pc < length (compE\<^sub>2 e @ [Return]); pc < length (compE\<^sub>2 e)\<rbrakk> \<Longrightarrow> compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
 2. \<lbrakk>pc < length (compE\<^sub>2 e @ [Return]); \<not> pc < length (compE\<^sub>2 e)\<rbrakk> \<Longrightarrow> compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
pc < length (compE\<^sub>2 e)

goal (2 subgoals):
 1. \<lbrakk>pc < length (compE\<^sub>2 e @ [Return]); pc < length (compE\<^sub>2 e)\<rbrakk> \<Longrightarrow> compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
 2. \<lbrakk>pc < length (compE\<^sub>2 e @ [Return]); \<not> pc < length (compE\<^sub>2 e)\<rbrakk> \<Longrightarrow> compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pc < length (compE\<^sub>2 e)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pc < length (compE\<^sub>2 e)

goal (1 subgoal):
 1. compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
[PROOF STEP]
using mxs wte wt_compE
[PROOF STATE]
proof (prove)
using this:
pc < length (compE\<^sub>2 e)
max_stack e = mxs
P,E \<turnstile>\<^sub>1 e :: T
\<turnstile> compE\<^sub>2 e, compxE\<^sub>2 e 0 (length []) [::] TC0.ty\<^sub>i' (length E + mxl\<^sub>0) [] E A # TC1.compT P (length E + mxl\<^sub>0) E A [] e @ [TC0.after P (length E + mxl\<^sub>0) E A [] e]

goal (1 subgoal):
 1. compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
[PROOF STEP]
by (clarsimp simp: compT\<^sub>a_def mxl after_def wt_instrs_def)
[PROOF STATE]
proof (state)
this:
compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e

goal (1 subgoal):
 1. \<lbrakk>pc < length (compE\<^sub>2 e @ [Return]); \<not> pc < length (compE\<^sub>2 e)\<rbrakk> \<Longrightarrow> compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>pc < length (compE\<^sub>2 e @ [Return]); \<not> pc < length (compE\<^sub>2 e)\<rbrakk> \<Longrightarrow> compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> pc < length (compE\<^sub>2 e)

goal (1 subgoal):
 1. \<lbrakk>pc < length (compE\<^sub>2 e @ [Return]); \<not> pc < length (compE\<^sub>2 e)\<rbrakk> \<Longrightarrow> compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
[PROOF STEP]
have "length (compE\<^sub>2 e) = pc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (compE\<^sub>2 e) = pc
[PROOF STEP]
using less_antisym[OF False] pc
[PROOF STATE]
proof (prove)
using this:
pc < Suc (length (compE\<^sub>2 e)) \<Longrightarrow> length (compE\<^sub>2 e) = pc
pc < length (compE\<^sub>2 e @ [Return])

goal (1 subgoal):
 1. length (compE\<^sub>2 e) = pc
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (compE\<^sub>2 e) = pc

goal (1 subgoal):
 1. \<lbrakk>pc < length (compE\<^sub>2 e @ [Return]); \<not> pc < length (compE\<^sub>2 e)\<rbrakk> \<Longrightarrow> compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (compE\<^sub>2 e) = pc
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length (compE\<^sub>2 e) = pc

goal (1 subgoal):
 1. compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
[PROOF STEP]
using mxl wte E_P wid
[PROOF STATE]
proof (prove)
using this:
length (compE\<^sub>2 e) = pc
Suc (length Ts + max_vars e) = mxl
P,E \<turnstile>\<^sub>1 e :: T
set E \<subseteq> types P
subtype P T T\<^sub>r

goal (1 subgoal):
 1. compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
[PROOF STEP]
by (clarsimp simp: compT\<^sub>a_def after_def wt_defs xcpt_app_pcs xcpt_eff_pcs ty\<^sub>i'_def)
[PROOF STATE]
proof (state)
this:
compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C NonStatic Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?pc5 < length (compE\<^sub>2 e @ [Return]) \<Longrightarrow> compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! ?pc5,?pc5 :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C NonStatic Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?pc5 < length (compE\<^sub>2 e @ [Return]) \<Longrightarrow> compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! ?pc5,?pc5 :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C NonStatic Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
have "0 < size ?is" and "size ?\<tau>s = size ?is"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < length (compE\<^sub>2 e @ [Return]) &&& length (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e) = length (compE\<^sub>2 e @ [Return])
[PROOF STEP]
using wte
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile>\<^sub>1 e :: T

goal (1 subgoal):
 1. 0 < length (compE\<^sub>2 e @ [Return]) &&& length (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e) = length (compE\<^sub>2 e @ [Return])
[PROOF STEP]
by (simp_all add: compT\<^sub>a_def)
[PROOF STATE]
proof (state)
this:
0 < length (compE\<^sub>2 e @ [Return])
length (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e) = length (compE\<^sub>2 e @ [Return])

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C NonStatic Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
check_types (compP\<^sub>2 P) mxs (length E + mxl\<^sub>0) (map OK (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e))
wt_start (compP\<^sub>2 P) C NonStatic Ts mxl\<^sub>0 (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
?pc5 < length (compE\<^sub>2 e @ [Return]) \<Longrightarrow> compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! ?pc5,?pc5 :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
0 < length (compE\<^sub>2 e @ [Return])
length (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e) = length (compE\<^sub>2 e @ [Return])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
check_types (compP\<^sub>2 P) mxs (length E + mxl\<^sub>0) (map OK (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e))
wt_start (compP\<^sub>2 P) C NonStatic Ts mxl\<^sub>0 (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
?pc5 < length (compE\<^sub>2 e @ [Return]) \<Longrightarrow> compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! ?pc5,?pc5 :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
0 < length (compE\<^sub>2 e @ [Return])
length (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e) = length (compE\<^sub>2 e @ [Return])

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C NonStatic Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
by(simp add: wt_method_def)
[PROOF STATE]
proof (state)
this:
wt_method (compP\<^sub>2 P) C NonStatic Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma compT_method_Static:
  fixes e and A and C and Ts and mxl\<^sub>0
  defines [simp]: "E \<equiv> Ts"
    and [simp]: "A \<equiv> \<lfloor>{..<size Ts}\<rfloor>"
    and [simp]: "A' \<equiv> A \<squnion> \<A> e"
    and [simp]: "mxl\<^sub>0 \<equiv> max_vars e"
  assumes mxs: "max_stack e = mxs"
    and mxl: "length Ts + max_vars e = mxl"
  assumes wf: "wf_prog p P" and wte: "P,E \<turnstile>\<^sub>1 e :: T" and \<D>: "\<D> e A"
    and \<B>: "\<B> e (size E)" and E_P: "set E \<subseteq> types P" and wid: "P \<turnstile> T \<le> T\<^sub>r"
  shows "wt_method (compP\<^sub>2 P) C Static Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return])
    (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)"
(*<*)(is "wt_method ?P C ?b Ts T\<^sub>r mxs mxl\<^sub>0 ?is ?xt ?\<tau>s")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C Static Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C Static Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
let ?n = "length E + mxl\<^sub>0"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C Static Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
have wt_compE: "P,T\<^sub>r,mxs \<turnstile> compE\<^sub>2 e, compxE\<^sub>2 e 0 (length []) [::]
        TC0.ty\<^sub>i' ?n [] E A # TC1.compT P ?n E A [] e @[TC0.after P ?n E A [] e]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> compE\<^sub>2 e, compxE\<^sub>2 e 0 (length []) [::] TC0.ty\<^sub>i' (length E + mxl\<^sub>0) [] E A # TC1.compT P (length E + mxl\<^sub>0) E A [] e @ [TC0.after P (length E + mxl\<^sub>0) E A [] e]
[PROOF STEP]
using mxs TC2.compT_wt_instrs [OF wte \<D> \<B>, of "[]" mxs ?n T\<^sub>r]
[PROOF STATE]
proof (prove)
using this:
max_stack e = mxs
\<lbrakk>length [] + max_stack e \<le> mxs; length E + max_vars e \<le> length E + mxl\<^sub>0\<rbrakk> \<Longrightarrow> \<turnstile> compE\<^sub>2 e, compxE\<^sub>2 e 0 (length []) [::] TC0.ty\<^sub>i' (length E + mxl\<^sub>0) [] E A # TC1.compT P (length E + mxl\<^sub>0) E A [] e @ [TC0.after P (length E + mxl\<^sub>0) E A [] e]

goal (1 subgoal):
 1. \<turnstile> compE\<^sub>2 e, compxE\<^sub>2 e 0 (length []) [::] TC0.ty\<^sub>i' (length E + mxl\<^sub>0) [] E A # TC1.compT P (length E + mxl\<^sub>0) E A [] e @ [TC0.after P (length E + mxl\<^sub>0) E A [] e]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<turnstile> compE\<^sub>2 e, compxE\<^sub>2 e 0 (length []) [::] TC0.ty\<^sub>i' (length E + mxl\<^sub>0) [] E A # TC1.compT P (length E + mxl\<^sub>0) E A [] e @ [TC0.after P (length E + mxl\<^sub>0) E A [] e]

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C Static Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
have "OK (ty\<^sub>i' [T] E A') \<in> states P mxs mxl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OK (ty\<^sub>i' [T] E A') \<in> states P mxs mxl
[PROOF STEP]
using mxs WT\<^sub>1_is_type[OF wf wte E_P] max_stack1[OF wte] OK_ty\<^sub>i'_in_statesI[OF E_P]
[PROOF STATE]
proof (prove)
using this:
max_stack e = mxs
is_type P T
1 \<le> max_stack e
\<lbrakk>set ?ST \<subseteq> types P; length ?ST \<le> ?mxs\<rbrakk> \<Longrightarrow> OK (ty\<^sub>i' ?ST E ?A) \<in> states P ?mxs mxl

goal (1 subgoal):
 1. OK (ty\<^sub>i' [T] E A') \<in> states P mxs mxl
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
OK (ty\<^sub>i' [T] E A') \<in> states P mxs mxl

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C Static Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
OK (ty\<^sub>i' [T] E A') \<in> states P mxs mxl

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C Static Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
have "OK ` set (compT E A [] e) \<subseteq> states P mxs mxl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OK ` set (compT E A [] e) \<subseteq> states P mxs mxl
[PROOF STEP]
using mxs mxl wid compT_states(1)[OF wf wte E_P]
[PROOF STATE]
proof (prove)
using this:
max_stack e = mxs
length Ts + max_vars e = mxl
subtype P T T\<^sub>r
\<lbrakk>set ?ST \<subseteq> types P; length ?ST + max_stack e \<le> ?mxs; length E + max_vars e \<le> mxl\<rbrakk> \<Longrightarrow> OK ` set (compT E ?A ?ST e) \<subseteq> states P ?mxs mxl

goal (1 subgoal):
 1. OK ` set (compT E A [] e) \<subseteq> states P mxs mxl
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
OK ` set (compT E A [] e) \<subseteq> states P mxs mxl

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C Static Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
OK (ty\<^sub>i' [T] E A') \<in> states P mxs mxl
OK ` set (compT E A [] e) \<subseteq> states P mxs mxl
[PROOF STEP]
have "check_types ?P mxs ?n (map OK ?\<tau>s)"
[PROOF STATE]
proof (prove)
using this:
OK (ty\<^sub>i' [T] E A') \<in> states P mxs mxl
OK ` set (compT E A [] e) \<subseteq> states P mxs mxl

goal (1 subgoal):
 1. check_types (compP\<^sub>2 P) mxs (length E + mxl\<^sub>0) (map OK (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e))
[PROOF STEP]
using mxl wte E_P
[PROOF STATE]
proof (prove)
using this:
OK (ty\<^sub>i' [T] E A') \<in> states P mxs mxl
OK ` set (compT E A [] e) \<subseteq> states P mxs mxl
length Ts + max_vars e = mxl
P,E \<turnstile>\<^sub>1 e :: T
set E \<subseteq> types P

goal (1 subgoal):
 1. check_types (compP\<^sub>2 P) mxs (length E + mxl\<^sub>0) (map OK (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e))
[PROOF STEP]
by (simp add: compT\<^sub>a_def after_def check_types_def)
[PROOF STATE]
proof (state)
this:
check_types (compP\<^sub>2 P) mxs (length E + mxl\<^sub>0) (map OK (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e))

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C Static Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
check_types (compP\<^sub>2 P) mxs (length E + mxl\<^sub>0) (map OK (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e))

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C Static Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
have "wt_start ?P C ?b Ts mxl\<^sub>0 ?\<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wt_start (compP\<^sub>2 P) C Static Ts mxl\<^sub>0 (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
using mxl
[PROOF STATE]
proof (prove)
using this:
length Ts + max_vars e = mxl

goal (1 subgoal):
 1. wt_start (compP\<^sub>2 P) C Static Ts mxl\<^sub>0 (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
by (auto simp: wt_start_def ty\<^sub>i'_def ty\<^sub>l_def list_all2_conv_all_nth nth_Cons
             split: nat.split)
[PROOF STATE]
proof (state)
this:
wt_start (compP\<^sub>2 P) C Static Ts mxl\<^sub>0 (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C Static Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wt_start (compP\<^sub>2 P) C Static Ts mxl\<^sub>0 (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C Static Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
wt_start (compP\<^sub>2 P) C Static Ts mxl\<^sub>0 (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C Static Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
fix pc
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C Static Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
assume pc: "pc < size ?is"
[PROOF STATE]
proof (state)
this:
pc < length (compE\<^sub>2 e @ [Return])

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C Static Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pc < length (compE\<^sub>2 e @ [Return])
[PROOF STEP]
have "?P,T\<^sub>r,mxs,size ?is,?xt \<turnstile> ?is!pc,pc :: ?\<tau>s"
[PROOF STATE]
proof (prove)
using this:
pc < length (compE\<^sub>2 e @ [Return])

goal (1 subgoal):
 1. compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
[PROOF STEP]
proof(cases "pc < length (compE\<^sub>2 e)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>pc < length (compE\<^sub>2 e @ [Return]); pc < length (compE\<^sub>2 e)\<rbrakk> \<Longrightarrow> compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
 2. \<lbrakk>pc < length (compE\<^sub>2 e @ [Return]); \<not> pc < length (compE\<^sub>2 e)\<rbrakk> \<Longrightarrow> compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
pc < length (compE\<^sub>2 e)

goal (2 subgoals):
 1. \<lbrakk>pc < length (compE\<^sub>2 e @ [Return]); pc < length (compE\<^sub>2 e)\<rbrakk> \<Longrightarrow> compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
 2. \<lbrakk>pc < length (compE\<^sub>2 e @ [Return]); \<not> pc < length (compE\<^sub>2 e)\<rbrakk> \<Longrightarrow> compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pc < length (compE\<^sub>2 e)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pc < length (compE\<^sub>2 e)

goal (1 subgoal):
 1. compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
[PROOF STEP]
using mxs wte wt_compE
[PROOF STATE]
proof (prove)
using this:
pc < length (compE\<^sub>2 e)
max_stack e = mxs
P,E \<turnstile>\<^sub>1 e :: T
\<turnstile> compE\<^sub>2 e, compxE\<^sub>2 e 0 (length []) [::] TC0.ty\<^sub>i' (length E + mxl\<^sub>0) [] E A # TC1.compT P (length E + mxl\<^sub>0) E A [] e @ [TC0.after P (length E + mxl\<^sub>0) E A [] e]

goal (1 subgoal):
 1. compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
[PROOF STEP]
by (clarsimp simp: compT\<^sub>a_def mxl after_def wt_instrs_def)
[PROOF STATE]
proof (state)
this:
compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e

goal (1 subgoal):
 1. \<lbrakk>pc < length (compE\<^sub>2 e @ [Return]); \<not> pc < length (compE\<^sub>2 e)\<rbrakk> \<Longrightarrow> compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>pc < length (compE\<^sub>2 e @ [Return]); \<not> pc < length (compE\<^sub>2 e)\<rbrakk> \<Longrightarrow> compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> pc < length (compE\<^sub>2 e)

goal (1 subgoal):
 1. \<lbrakk>pc < length (compE\<^sub>2 e @ [Return]); \<not> pc < length (compE\<^sub>2 e)\<rbrakk> \<Longrightarrow> compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
[PROOF STEP]
have "length (compE\<^sub>2 e) = pc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (compE\<^sub>2 e) = pc
[PROOF STEP]
using less_antisym[OF False] pc
[PROOF STATE]
proof (prove)
using this:
pc < Suc (length (compE\<^sub>2 e)) \<Longrightarrow> length (compE\<^sub>2 e) = pc
pc < length (compE\<^sub>2 e @ [Return])

goal (1 subgoal):
 1. length (compE\<^sub>2 e) = pc
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (compE\<^sub>2 e) = pc

goal (1 subgoal):
 1. \<lbrakk>pc < length (compE\<^sub>2 e @ [Return]); \<not> pc < length (compE\<^sub>2 e)\<rbrakk> \<Longrightarrow> compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (compE\<^sub>2 e) = pc
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length (compE\<^sub>2 e) = pc

goal (1 subgoal):
 1. compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
[PROOF STEP]
using mxl wte E_P wid
[PROOF STATE]
proof (prove)
using this:
length (compE\<^sub>2 e) = pc
length Ts + max_vars e = mxl
P,E \<turnstile>\<^sub>1 e :: T
set E \<subseteq> types P
subtype P T T\<^sub>r

goal (1 subgoal):
 1. compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
[PROOF STEP]
by (clarsimp simp: compT\<^sub>a_def after_def wt_defs xcpt_app_pcs xcpt_eff_pcs ty\<^sub>i'_def)
[PROOF STATE]
proof (state)
this:
compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! pc,pc :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C Static Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?pc5 < length (compE\<^sub>2 e @ [Return]) \<Longrightarrow> compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! ?pc5,?pc5 :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C Static Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?pc5 < length (compE\<^sub>2 e @ [Return]) \<Longrightarrow> compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! ?pc5,?pc5 :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C Static Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
have "0 < size ?is" and "size ?\<tau>s = size ?is"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < length (compE\<^sub>2 e @ [Return]) &&& length (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e) = length (compE\<^sub>2 e @ [Return])
[PROOF STEP]
using wte
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile>\<^sub>1 e :: T

goal (1 subgoal):
 1. 0 < length (compE\<^sub>2 e @ [Return]) &&& length (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e) = length (compE\<^sub>2 e @ [Return])
[PROOF STEP]
by (simp_all add: compT\<^sub>a_def)
[PROOF STATE]
proof (state)
this:
0 < length (compE\<^sub>2 e @ [Return])
length (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e) = length (compE\<^sub>2 e @ [Return])

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C Static Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
check_types (compP\<^sub>2 P) mxs (length E + mxl\<^sub>0) (map OK (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e))
wt_start (compP\<^sub>2 P) C Static Ts mxl\<^sub>0 (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
?pc5 < length (compE\<^sub>2 e @ [Return]) \<Longrightarrow> compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! ?pc5,?pc5 :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
0 < length (compE\<^sub>2 e @ [Return])
length (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e) = length (compE\<^sub>2 e @ [Return])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
check_types (compP\<^sub>2 P) mxs (length E + mxl\<^sub>0) (map OK (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e))
wt_start (compP\<^sub>2 P) C Static Ts mxl\<^sub>0 (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
?pc5 < length (compE\<^sub>2 e @ [Return]) \<Longrightarrow> compP\<^sub>2 P,T\<^sub>r,mxs,length (compE\<^sub>2 e @ [Return]),compxE\<^sub>2 e 0 0 \<turnstile> (compE\<^sub>2 e @ [Return]) ! ?pc5,?pc5 :: ty\<^sub>i' [] E A # compT\<^sub>a E A [] e
0 < length (compE\<^sub>2 e @ [Return])
length (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e) = length (compE\<^sub>2 e @ [Return])

goal (1 subgoal):
 1. wt_method (compP\<^sub>2 P) C Static Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)
[PROOF STEP]
by(simp add: wt_method_def)
[PROOF STATE]
proof (state)
this:
wt_method (compP\<^sub>2 P) C Static Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return]) (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem wt_compP\<^sub>2:
assumes wf: "wf_J\<^sub>1_prog P" shows "wf_jvm_prog (compP\<^sub>2 P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_jvm_prog (compP\<^sub>2 P)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_jvm_prog (compP\<^sub>2 P)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_jvm_prog (compP\<^sub>2 P)
[PROOF STEP]
let ?\<Phi> = "compTP P" and ?f = compMb\<^sub>2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_jvm_prog (compP\<^sub>2 P)
[PROOF STEP]
let ?wf\<^sub>2 = "\<lambda>P C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt).
              wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (?\<Phi> C M)"
    and ?P = "compP ?f P"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_jvm_prog (compP\<^sub>2 P)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_jvm_prog (compP\<^sub>2 P)
[PROOF STEP]
fix C M b Ts T m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_jvm_prog (compP\<^sub>2 P)
[PROOF STEP]
let ?md = "(M,b,Ts,T,m)::expr\<^sub>1 mdecl"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_jvm_prog (compP\<^sub>2 P)
[PROOF STEP]
assume cM: "P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in C"
      and wfm: "wf_mdecl wf_J\<^sub>1_mdecl P C ?md"
[PROOF STATE]
proof (state)
this:
P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in C
wf_mdecl wf_J\<^sub>1_mdecl P C (M, b, Ts, T, m)

goal (1 subgoal):
 1. wf_jvm_prog (compP\<^sub>2 P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in C
wf_mdecl wf_J\<^sub>1_mdecl P C (M, b, Ts, T, m)
[PROOF STEP]
have Ts_types: "\<forall>T'\<in>set Ts. is_type P T'"
     and T_type: "is_type P T" and wfm\<^sub>1: "wf_J\<^sub>1_mdecl P C ?md"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in C
wf_mdecl wf_J\<^sub>1_mdecl P C (M, b, Ts, T, m)

goal (1 subgoal):
 1. \<forall>T'\<in>set Ts. is_type P T' &&& is_type P T &&& wf_J\<^sub>1_mdecl P C (M, b, Ts, T, m)
[PROOF STEP]
by(simp_all add: wf_mdecl_def)
[PROOF STATE]
proof (state)
this:
\<forall>T'\<in>set Ts. is_type P T'
is_type P T
wf_J\<^sub>1_mdecl P C (M, b, Ts, T, m)

goal (1 subgoal):
 1. wf_jvm_prog (compP\<^sub>2 P)
[PROOF STEP]
have Ts_P: "set Ts \<subseteq> types P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set Ts \<subseteq> types P
[PROOF STEP]
using sees_wf_mdecl[OF wf cM]
[PROOF STATE]
proof (prove)
using this:
wf_mdecl wf_J\<^sub>1_mdecl P C (M, b, Ts, T, m)

goal (1 subgoal):
 1. set Ts \<subseteq> types P
[PROOF STEP]
by (clarsimp simp: wf_mdecl_def)
[PROOF STATE]
proof (state)
this:
set Ts \<subseteq> types P

goal (1 subgoal):
 1. wf_jvm_prog (compP\<^sub>2 P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set Ts \<subseteq> types P
[PROOF STEP]
have CTs_P: "is_class P C \<and> set Ts \<subseteq> types P"
[PROOF STATE]
proof (prove)
using this:
set Ts \<subseteq> types P

goal (1 subgoal):
 1. is_class P C \<and> set Ts \<subseteq> types P
[PROOF STEP]
using sees_method_is_class[OF cM]
[PROOF STATE]
proof (prove)
using this:
set Ts \<subseteq> types P
is_class P C

goal (1 subgoal):
 1. is_class P C \<and> set Ts \<subseteq> types P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_class P C \<and> set Ts \<subseteq> types P

goal (1 subgoal):
 1. wf_jvm_prog (compP\<^sub>2 P)
[PROOF STEP]
have "?wf\<^sub>2 ?P C (M,b,Ts,T,?f b m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case (M, b, Ts, T, compMb\<^sub>2 b m) of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method (compP compMb\<^sub>2 P) C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)
[PROOF STEP]
proof(cases b)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b = Static \<Longrightarrow> case (M, b, Ts, T, compMb\<^sub>2 b m) of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method (compP compMb\<^sub>2 P) C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)
 2. b = NonStatic \<Longrightarrow> case (M, b, Ts, T, compMb\<^sub>2 b m) of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method (compP compMb\<^sub>2 P) C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)
[PROOF STEP]
case Static
[PROOF STATE]
proof (state)
this:
b = Static

goal (2 subgoals):
 1. b = Static \<Longrightarrow> case (M, b, Ts, T, compMb\<^sub>2 b m) of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method (compP compMb\<^sub>2 P) C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)
 2. b = NonStatic \<Longrightarrow> case (M, b, Ts, T, compMb\<^sub>2 b m) of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method (compP compMb\<^sub>2 P) C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = Static
[PROOF STEP]
obtain T' where wte: "P,Ts \<turnstile>\<^sub>1 m :: T'" and wid: "P \<turnstile> T' \<le> T"
         and \<D>: "\<D> m \<lfloor>{..<size Ts}\<rfloor>" and \<B>: "\<B> m (size Ts)"
[PROOF STATE]
proof (prove)
using this:
b = Static

goal (1 subgoal):
 1. (\<And>T'. \<lbrakk>P,Ts \<turnstile>\<^sub>1 m :: T'; subtype P T' T; \<D> m \<lfloor>{..<length Ts}\<rfloor>; \<B> m (length Ts)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfm\<^sub>1
[PROOF STATE]
proof (prove)
using this:
b = Static
wf_J\<^sub>1_mdecl P C (M, b, Ts, T, m)

goal (1 subgoal):
 1. (\<And>T'. \<lbrakk>P,Ts \<turnstile>\<^sub>1 m :: T'; subtype P T' T; \<D> m \<lfloor>{..<length Ts}\<rfloor>; \<B> m (length Ts)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp: wf_mdecl_def)
[PROOF STATE]
proof (state)
this:
P,Ts \<turnstile>\<^sub>1 m :: T'
subtype P T' T
\<D> m \<lfloor>{..<length Ts}\<rfloor>
\<B> m (length Ts)

goal (2 subgoals):
 1. b = Static \<Longrightarrow> case (M, b, Ts, T, compMb\<^sub>2 b m) of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method (compP compMb\<^sub>2 P) C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)
 2. b = NonStatic \<Longrightarrow> case (M, b, Ts, T, compMb\<^sub>2 b m) of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method (compP compMb\<^sub>2 P) C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case (M, b, Ts, T, compMb\<^sub>2 b m) of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method (compP compMb\<^sub>2 P) C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)
[PROOF STEP]
using Static cM TC2.compT_method_Static [OF _ _ wf wte \<D> \<B> Ts_P wid]
[PROOF STATE]
proof (prove)
using this:
b = Static
P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in C
\<lbrakk>max_stack m = ?mxs; length Ts + max_vars m = ?mxl\<rbrakk> \<Longrightarrow> wt_method (compP\<^sub>2 P) ?C Static Ts T ?mxs (max_vars m) (compE\<^sub>2 m @ [Return]) (compxE\<^sub>2 m 0 0) (TC0.ty\<^sub>i' ?mxl [] Ts \<lfloor>{..<length Ts}\<rfloor> # TC1.compT\<^sub>a P ?mxl Ts \<lfloor>{..<length Ts}\<rfloor> [] m)

goal (1 subgoal):
 1. case (M, b, Ts, T, compMb\<^sub>2 b m) of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method (compP compMb\<^sub>2 P) C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)
[PROOF STEP]
by(simp add: compTP_def)
[PROOF STATE]
proof (state)
this:
case (M, b, Ts, T, compMb\<^sub>2 b m) of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method (compP compMb\<^sub>2 P) C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)

goal (1 subgoal):
 1. b = NonStatic \<Longrightarrow> case (M, b, Ts, T, compMb\<^sub>2 b m) of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method (compP compMb\<^sub>2 P) C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b = NonStatic \<Longrightarrow> case (M, b, Ts, T, compMb\<^sub>2 b m) of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method (compP compMb\<^sub>2 P) C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)
[PROOF STEP]
case NonStatic
[PROOF STATE]
proof (state)
this:
b = NonStatic

goal (1 subgoal):
 1. b = NonStatic \<Longrightarrow> case (M, b, Ts, T, compMb\<^sub>2 b m) of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method (compP compMb\<^sub>2 P) C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = NonStatic
[PROOF STEP]
obtain T' where wte: "P,Class C#Ts \<turnstile>\<^sub>1 m :: T'" and wid: "P \<turnstile> T' \<le> T"
         and \<D>: "\<D> m \<lfloor>{..size Ts}\<rfloor>" and \<B>: "\<B> m (Suc (size Ts))"
[PROOF STATE]
proof (prove)
using this:
b = NonStatic

goal (1 subgoal):
 1. (\<And>T'. \<lbrakk>P,Class C # Ts \<turnstile>\<^sub>1 m :: T'; subtype P T' T; \<D> m \<lfloor>{..length Ts}\<rfloor>; \<B> m (Suc (length Ts))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfm\<^sub>1
[PROOF STATE]
proof (prove)
using this:
b = NonStatic
wf_J\<^sub>1_mdecl P C (M, b, Ts, T, m)

goal (1 subgoal):
 1. (\<And>T'. \<lbrakk>P,Class C # Ts \<turnstile>\<^sub>1 m :: T'; subtype P T' T; \<D> m \<lfloor>{..length Ts}\<rfloor>; \<B> m (Suc (length Ts))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp: wf_mdecl_def)
[PROOF STATE]
proof (state)
this:
P,Class C # Ts \<turnstile>\<^sub>1 m :: T'
subtype P T' T
\<D> m \<lfloor>{..length Ts}\<rfloor>
\<B> m (Suc (length Ts))

goal (1 subgoal):
 1. b = NonStatic \<Longrightarrow> case (M, b, Ts, T, compMb\<^sub>2 b m) of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method (compP compMb\<^sub>2 P) C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)
[PROOF STEP]
have Ts_P: "set Ts \<subseteq> types P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set Ts \<subseteq> types P
[PROOF STEP]
using sees_wf_mdecl[OF wf cM]
[PROOF STATE]
proof (prove)
using this:
wf_mdecl wf_J\<^sub>1_mdecl P C (M, b, Ts, T, m)

goal (1 subgoal):
 1. set Ts \<subseteq> types P
[PROOF STEP]
by (fastforce simp: wf_mdecl_def intro: sees_method_is_class)
[PROOF STATE]
proof (state)
this:
set Ts \<subseteq> types P

goal (1 subgoal):
 1. b = NonStatic \<Longrightarrow> case (M, b, Ts, T, compMb\<^sub>2 b m) of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method (compP compMb\<^sub>2 P) C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case (M, b, Ts, T, compMb\<^sub>2 b m) of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method (compP compMb\<^sub>2 P) C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)
[PROOF STEP]
using NonStatic cM
          TC2.compT_method_NonStatic [simplified, OF _ _ wf wte \<D> \<B> CTs_P wid]
[PROOF STATE]
proof (prove)
using this:
b = NonStatic
P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in C
\<lbrakk>max_stack m = ?mxs; Suc (length Ts + max_vars m) = ?mxl\<rbrakk> \<Longrightarrow> wt_method (compP compMb\<^sub>2 P) C NonStatic Ts T ?mxs (max_vars m) (compE\<^sub>2 m @ [Return]) (compxE\<^sub>2 m 0 0) (TC0.ty\<^sub>i' ?mxl [] (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> # TC1.compT\<^sub>a P ?mxl (Class C # Ts) \<lfloor>{..length Ts}\<rfloor> [] m)

goal (1 subgoal):
 1. case (M, b, Ts, T, compMb\<^sub>2 b m) of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method (compP compMb\<^sub>2 P) C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)
[PROOF STEP]
by(simp add: compTP_def)
[PROOF STATE]
proof (state)
this:
case (M, b, Ts, T, compMb\<^sub>2 b m) of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method (compP compMb\<^sub>2 P) C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
case (M, b, Ts, T, compMb\<^sub>2 b m) of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method (compP compMb\<^sub>2 P) C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)

goal (1 subgoal):
 1. wf_jvm_prog (compP\<^sub>2 P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
case (M, b, Ts, T, compMb\<^sub>2 b m) of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method (compP compMb\<^sub>2 P) C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)
[PROOF STEP]
have "wf_mdecl ?wf\<^sub>2 ?P C (M, b, Ts, T, ?f b m)"
[PROOF STATE]
proof (prove)
using this:
case (M, b, Ts, T, compMb\<^sub>2 b m) of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method (compP compMb\<^sub>2 P) C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)

goal (1 subgoal):
 1. wf_mdecl (\<lambda>Pa C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method Pa C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)) (compP compMb\<^sub>2 P) C (M, b, Ts, T, compMb\<^sub>2 b m)
[PROOF STEP]
using Ts_types T_type
[PROOF STATE]
proof (prove)
using this:
case (M, b, Ts, T, compMb\<^sub>2 b m) of (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method (compP compMb\<^sub>2 P) C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)
\<forall>T'\<in>set Ts. is_type P T'
is_type P T

goal (1 subgoal):
 1. wf_mdecl (\<lambda>Pa C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method Pa C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)) (compP compMb\<^sub>2 P) C (M, b, Ts, T, compMb\<^sub>2 b m)
[PROOF STEP]
by(simp add: wf_mdecl_def)
[PROOF STATE]
proof (state)
this:
wf_mdecl (\<lambda>Pa C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method Pa C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)) (compP compMb\<^sub>2 P) C (M, b, Ts, T, compMb\<^sub>2 b m)

goal (1 subgoal):
 1. wf_jvm_prog (compP\<^sub>2 P)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>P \<turnstile> ?C3 sees ?M3, ?b3 :  ?Ts3\<rightarrow>?T3 = ?m3 in ?C3; wf_mdecl wf_J\<^sub>1_mdecl P ?C3 (?M3, ?b3, ?Ts3, ?T3, ?m3)\<rbrakk> \<Longrightarrow> wf_mdecl (\<lambda>Pa C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method Pa C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)) (compP compMb\<^sub>2 P) ?C3 (?M3, ?b3, ?Ts3, ?T3, compMb\<^sub>2 ?b3 ?m3)

goal (1 subgoal):
 1. wf_jvm_prog (compP\<^sub>2 P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>P \<turnstile> ?C3 sees ?M3, ?b3 :  ?Ts3\<rightarrow>?T3 = ?m3 in ?C3; wf_mdecl wf_J\<^sub>1_mdecl P ?C3 (?M3, ?b3, ?Ts3, ?T3, ?m3)\<rbrakk> \<Longrightarrow> wf_mdecl (\<lambda>Pa C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method Pa C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)) (compP compMb\<^sub>2 P) ?C3 (?M3, ?b3, ?Ts3, ?T3, compMb\<^sub>2 ?b3 ?m3)
[PROOF STEP]
have "wf_prog ?wf\<^sub>2 (compP ?f P)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>P \<turnstile> ?C3 sees ?M3, ?b3 :  ?Ts3\<rightarrow>?T3 = ?m3 in ?C3; wf_mdecl wf_J\<^sub>1_mdecl P ?C3 (?M3, ?b3, ?Ts3, ?T3, ?m3)\<rbrakk> \<Longrightarrow> wf_mdecl (\<lambda>Pa C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method Pa C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)) (compP compMb\<^sub>2 P) ?C3 (?M3, ?b3, ?Ts3, ?T3, compMb\<^sub>2 ?b3 ?m3)

goal (1 subgoal):
 1. wf_prog (\<lambda>Pa C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method Pa C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)) (compP compMb\<^sub>2 P)
[PROOF STEP]
by(rule wf_prog_compPI[OF _ wf])
[PROOF STATE]
proof (state)
this:
wf_prog (\<lambda>Pa C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method Pa C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)) (compP compMb\<^sub>2 P)

goal (1 subgoal):
 1. wf_jvm_prog (compP\<^sub>2 P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf_prog (\<lambda>Pa C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method Pa C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)) (compP compMb\<^sub>2 P)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wf_prog (\<lambda>Pa C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method Pa C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (compTP P C M)) (compP compMb\<^sub>2 P)

goal (1 subgoal):
 1. wf_jvm_prog (compP\<^sub>2 P)
[PROOF STEP]
by (simp add: wf_jvm_prog_def wf_jvm_prog_phi_def) fast
[PROOF STATE]
proof (state)
this:
wf_jvm_prog (compP\<^sub>2 P)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem wt_J2JVM:
  "wf_J_prog P \<Longrightarrow> wf_jvm_prog (J2JVM P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_J_prog P \<Longrightarrow> wf_jvm_prog (J2JVM P)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_J_prog P \<Longrightarrow> wf_jvm_prog (J2JVM P)
[PROOF STEP]
by(simp only:o_def J2JVM_def)
  (blast intro:wt_compP\<^sub>2 compP\<^sub>1_pres_wf)


[STATEMENT]
lemma map_matrix_rat_of_int_mult:
  shows "map_matrix rat_of_int (A**B) = (map_matrix rat_of_int A)**(map_matrix rat_of_int B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_matrix rat_of_int (A ** B) = map_matrix rat_of_int A ** map_matrix rat_of_int B
[PROOF STEP]
unfolding map_matrix_def matrix_matrix_mult_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i j. rat_of_int ((\<chi>i j. \<Sum>k\<in>UNIV. A $ i $ k * B $ k $ j) $ i $ j)) = (\<chi>i j. \<Sum>k\<in>UNIV. (\<chi>i j. rat_of_int (A $ i $ j)) $ i $ k * (\<chi>i j. rat_of_int (B $ i $ j)) $ k $ j)
[PROOF STEP]
by auto


[STATEMENT]
lemma det_map_matrix:
  fixes A :: "int^'n::mod_type^'n::mod_type"
  shows "det (map_matrix rat_of_int A) = rat_of_int (det A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (map_matrix rat_of_int A) = rat_of_int (det A)
[PROOF STEP]
unfolding map_matrix_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (\<chi>i j. rat_of_int (A $ i $ j)) = rat_of_int (det A)
[PROOF STEP]
unfolding Determinants.det_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>p | p permutes UNIV. rat_of_int (sign p) * (\<Prod>i\<in>UNIV. (\<chi>i j. rat_of_int (A $ i $ j)) $ i $ p i)) = rat_of_int (\<Sum>p | p permutes UNIV. of_int (sign p) * (\<Prod>i\<in>UNIV. A $ i $ p i))
[PROOF STEP]
by auto


[STATEMENT]
lemma inv_Z_imp_inv_Q:
  fixes A :: "int^'n::mod_type^'n::mod_type"
  assumes inv_A: "invertible A"
  shows "invertible (map_matrix rat_of_int A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invertible (map_matrix rat_of_int A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. invertible (map_matrix rat_of_int A)
[PROOF STEP]
have "is_unit (det A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_unit (det A)
[PROOF STEP]
using inv_A invertible_iff_is_unit
[PROOF STATE]
proof (prove)
using this:
invertible A
invertible ?A = (det ?A dvd (1::?'a))

goal (1 subgoal):
 1. is_unit (det A)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_unit (det A)

goal (1 subgoal):
 1. invertible (map_matrix rat_of_int A)
[PROOF STEP]
hence "is_unit (det (map_matrix rat_of_int A))"
[PROOF STATE]
proof (prove)
using this:
is_unit (det A)

goal (1 subgoal):
 1. is_unit (det (map_matrix rat_of_int A))
[PROOF STEP]
by (simp add: det_map_matrix dvd_if_abs_eq)
[PROOF STATE]
proof (state)
this:
is_unit (det (map_matrix rat_of_int A))

goal (1 subgoal):
 1. invertible (map_matrix rat_of_int A)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
is_unit (det (map_matrix rat_of_int A))

goal (1 subgoal):
 1. invertible (map_matrix rat_of_int A)
[PROOF STEP]
using invertible_iff_is_unit
[PROOF STATE]
proof (prove)
using this:
is_unit (det (map_matrix rat_of_int A))
invertible ?A = (det ?A dvd (1::?'a))

goal (1 subgoal):
 1. invertible (map_matrix rat_of_int A)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
invertible (map_matrix rat_of_int A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma upper_triangular_Z_eq_Q:
  "upper_triangular (map_matrix rat_of_int A) = upper_triangular A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper_triangular (map_matrix rat_of_int A) = upper_triangular A
[PROOF STEP]
unfolding upper_triangular_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i j. j < i \<longrightarrow> map_matrix rat_of_int A $ i $ j = 0) = (\<forall>i j. j < i \<longrightarrow> A $ i $ j = 0)
[PROOF STEP]
by auto


[STATEMENT]
lemma invertible_and_upper_diagonal_not0:
  fixes H :: "int^'n::mod_type^'n::mod_type"
  assumes inv_H: "invertible (map_matrix rat_of_int H)" and up_H: "upper_triangular H"
  shows "H $ i $ i \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H $ i $ i \<noteq> 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H $ i $ i \<noteq> 0
[PROOF STEP]
let ?RAT_H = "(map_matrix rat_of_int H)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H $ i $ i \<noteq> 0
[PROOF STEP]
have up_RAT_H: "upper_triangular ?RAT_H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper_triangular (map_matrix rat_of_int H)
[PROOF STEP]
using up_H
[PROOF STATE]
proof (prove)
using this:
upper_triangular H

goal (1 subgoal):
 1. upper_triangular (map_matrix rat_of_int H)
[PROOF STEP]
unfolding upper_triangular_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i j. j < i \<longrightarrow> H $ i $ j = 0

goal (1 subgoal):
 1. \<forall>i j. j < i \<longrightarrow> map_matrix rat_of_int H $ i $ j = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
upper_triangular (map_matrix rat_of_int H)

goal (1 subgoal):
 1. H $ i $ i \<noteq> 0
[PROOF STEP]
have "is_unit (det ?RAT_H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_unit (det (map_matrix rat_of_int H))
[PROOF STEP]
using inv_H
[PROOF STATE]
proof (prove)
using this:
invertible (map_matrix rat_of_int H)

goal (1 subgoal):
 1. is_unit (det (map_matrix rat_of_int H))
[PROOF STEP]
using invertible_iff_is_unit
[PROOF STATE]
proof (prove)
using this:
invertible (map_matrix rat_of_int H)
invertible ?A = (det ?A dvd (1::?'a))

goal (1 subgoal):
 1. is_unit (det (map_matrix rat_of_int H))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_unit (det (map_matrix rat_of_int H))

goal (1 subgoal):
 1. H $ i $ i \<noteq> 0
[PROOF STEP]
hence "?RAT_H $ i $ i \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
is_unit (det (map_matrix rat_of_int H))

goal (1 subgoal):
 1. map_matrix rat_of_int H $ i $ i \<noteq> 0
[PROOF STEP]
using inv_H up_RAT_H is_unit_diagonal
[PROOF STATE]
proof (prove)
using this:
is_unit (det (map_matrix rat_of_int H))
invertible (map_matrix rat_of_int H)
upper_triangular (map_matrix rat_of_int H)
\<lbrakk>upper_triangular ?U; is_unit (det ?U)\<rbrakk> \<Longrightarrow> \<forall>i. is_unit (?U $ i $ i)

goal (1 subgoal):
 1. map_matrix rat_of_int H $ i $ i \<noteq> 0
[PROOF STEP]
by (metis not_is_unit_0)
[PROOF STATE]
proof (state)
this:
map_matrix rat_of_int H $ i $ i \<noteq> 0

goal (1 subgoal):
 1. H $ i $ i \<noteq> 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
map_matrix rat_of_int H $ i $ i \<noteq> 0

goal (1 subgoal):
 1. H $ i $ i \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
H $ i $ i \<noteq> 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma diagonal_least_nonzero:
  fixes H :: "int^'n::mod_type^'n::mod_type"
  assumes H: "Hermite associates residues H"
  and inv_H: "invertible (map_matrix rat_of_int H)" and up_H: "upper_triangular H"
  shows "(LEAST n. H $ i $ n \<noteq> 0) = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. H $ i $ n \<noteq> 0) = i
[PROOF STEP]
proof (rule Least_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. H $ i $ i \<noteq> 0
 2. \<And>y. H $ i $ y \<noteq> 0 \<Longrightarrow> i \<le> y
[PROOF STEP]
show "H $ i $ i \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H $ i $ i \<noteq> 0
[PROOF STEP]
by (rule invertible_and_upper_diagonal_not0[OF inv_H up_H])
[PROOF STATE]
proof (state)
this:
H $ i $ i \<noteq> 0

goal (1 subgoal):
 1. \<And>y. H $ i $ y \<noteq> 0 \<Longrightarrow> i \<le> y
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. H $ i $ y \<noteq> 0 \<Longrightarrow> i \<le> y
[PROOF STEP]
assume Hiy: "H $ i $ y \<noteq> 0"
[PROOF STATE]
proof (state)
this:
H $ i $ y \<noteq> 0

goal (1 subgoal):
 1. \<And>y. H $ i $ y \<noteq> 0 \<Longrightarrow> i \<le> y
[PROOF STEP]
show "i \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> y
[PROOF STEP]
using up_H
[PROOF STATE]
proof (prove)
using this:
upper_triangular H

goal (1 subgoal):
 1. i \<le> y
[PROOF STEP]
unfolding upper_triangular_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i j. j < i \<longrightarrow> H $ i $ j = 0

goal (1 subgoal):
 1. i \<le> y
[PROOF STEP]
by (metis (poly_guards_query) Hiy not_less)
[PROOF STATE]
proof (state)
this:
i \<le> y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma diagonal_in_associates:
  fixes H :: "int^'n::mod_type^'n::mod_type"
  assumes H: "Hermite associates residues H"
  and inv_H: "invertible (map_matrix rat_of_int H)" and up_H: "upper_triangular H"
  shows "H $ i $ i \<in> associates"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H $ i $ i \<in> associates
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H $ i $ i \<in> associates
[PROOF STEP]
have "H $ i $ i \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H $ i $ i \<noteq> 0
[PROOF STEP]
by (rule invertible_and_upper_diagonal_not0[OF inv_H up_H])
[PROOF STATE]
proof (state)
this:
H $ i $ i \<noteq> 0

goal (1 subgoal):
 1. H $ i $ i \<in> associates
[PROOF STEP]
hence "\<not> is_zero_row i H"
[PROOF STATE]
proof (prove)
using this:
H $ i $ i \<noteq> 0

goal (1 subgoal):
 1. \<not> is_zero_row i H
[PROOF STEP]
unfolding is_zero_row_def is_zero_row_upt_k_def ncols_def
[PROOF STATE]
proof (prove)
using this:
H $ i $ i \<noteq> 0

goal (1 subgoal):
 1. \<not> (\<forall>j. mod_type_class.to_nat j < CARD('n) \<longrightarrow> H $ i $ j = 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row i H

goal (1 subgoal):
 1. H $ i $ i \<in> associates
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row i H

goal (1 subgoal):
 1. H $ i $ i \<in> associates
[PROOF STEP]
using H
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row i H
Hermite associates residues H

goal (1 subgoal):
 1. H $ i $ i \<in> associates
[PROOF STEP]
unfolding Hermite_def
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row i H
Complete_set_non_associates associates \<and> Complete_set_residues residues \<and> echelon_form H \<and> (\<forall>i. \<not> is_zero_row i H \<longrightarrow> H $ i $ (LEAST n. H $ i $ n \<noteq> 0) \<in> associates) \<and> (\<forall>i. \<not> is_zero_row i H \<longrightarrow> (\<forall>j<i. H $ j $ (LEAST n. H $ i $ n \<noteq> 0) \<in> residues (H $ i $ (LEAST n. H $ i $ n \<noteq> 0))))

goal (1 subgoal):
 1. H $ i $ i \<in> associates
[PROOF STEP]
unfolding diagonal_least_nonzero[OF H inv_H up_H]
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row i H
Complete_set_non_associates associates \<and> Complete_set_residues residues \<and> echelon_form H \<and> (\<forall>i. \<not> is_zero_row i H \<longrightarrow> H $ i $ i \<in> associates) \<and> (\<forall>i. \<not> is_zero_row i H \<longrightarrow> (\<forall>j<i. H $ j $ i \<in> residues (H $ i $ i)))

goal (1 subgoal):
 1. H $ i $ i \<in> associates
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
H $ i $ i \<in> associates

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma above_diagonal_in_residues:
  fixes H :: "int^'n::mod_type^'n::mod_type"
  assumes H: "Hermite associates residues H"
  and inv_H: "invertible (map_matrix rat_of_int H)" and up_H: "upper_triangular H"
  and j_i: "j<i"
  shows "H $ j $ (LEAST n. H $ i $ n \<noteq> 0) \<in> residues (H $ i $ (LEAST n. H $ i $ n \<noteq> 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H $ j $ (LEAST n. H $ i $ n \<noteq> 0) \<in> residues (H $ i $ (LEAST n. H $ i $ n \<noteq> 0))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H $ j $ (LEAST n. H $ i $ n \<noteq> 0) \<in> residues (H $ i $ (LEAST n. H $ i $ n \<noteq> 0))
[PROOF STEP]
have "H $ i $ i \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H $ i $ i \<noteq> 0
[PROOF STEP]
by (rule invertible_and_upper_diagonal_not0[OF inv_H up_H])
[PROOF STATE]
proof (state)
this:
H $ i $ i \<noteq> 0

goal (1 subgoal):
 1. H $ j $ (LEAST n. H $ i $ n \<noteq> 0) \<in> residues (H $ i $ (LEAST n. H $ i $ n \<noteq> 0))
[PROOF STEP]
hence "\<not> is_zero_row i H"
[PROOF STATE]
proof (prove)
using this:
H $ i $ i \<noteq> 0

goal (1 subgoal):
 1. \<not> is_zero_row i H
[PROOF STEP]
unfolding is_zero_row_def is_zero_row_upt_k_def ncols_def
[PROOF STATE]
proof (prove)
using this:
H $ i $ i \<noteq> 0

goal (1 subgoal):
 1. \<not> (\<forall>j. mod_type_class.to_nat j < CARD('n) \<longrightarrow> H $ i $ j = 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row i H

goal (1 subgoal):
 1. H $ j $ (LEAST n. H $ i $ n \<noteq> 0) \<in> residues (H $ i $ (LEAST n. H $ i $ n \<noteq> 0))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row i H

goal (1 subgoal):
 1. H $ j $ (LEAST n. H $ i $ n \<noteq> 0) \<in> residues (H $ i $ (LEAST n. H $ i $ n \<noteq> 0))
[PROOF STEP]
using H j_i
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row i H
Hermite associates residues H
j < i

goal (1 subgoal):
 1. H $ j $ (LEAST n. H $ i $ n \<noteq> 0) \<in> residues (H $ i $ (LEAST n. H $ i $ n \<noteq> 0))
[PROOF STEP]
unfolding Hermite_def
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row i H
Complete_set_non_associates associates \<and> Complete_set_residues residues \<and> echelon_form H \<and> (\<forall>i. \<not> is_zero_row i H \<longrightarrow> H $ i $ (LEAST n. H $ i $ n \<noteq> 0) \<in> associates) \<and> (\<forall>i. \<not> is_zero_row i H \<longrightarrow> (\<forall>j<i. H $ j $ (LEAST n. H $ i $ n \<noteq> 0) \<in> residues (H $ i $ (LEAST n. H $ i $ n \<noteq> 0))))
j < i

goal (1 subgoal):
 1. H $ j $ (LEAST n. H $ i $ n \<noteq> 0) \<in> residues (H $ i $ (LEAST n. H $ i $ n \<noteq> 0))
[PROOF STEP]
unfolding diagonal_least_nonzero[OF H inv_H up_H]
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row i H
Complete_set_non_associates associates \<and> Complete_set_residues residues \<and> echelon_form H \<and> (\<forall>i. \<not> is_zero_row i H \<longrightarrow> H $ i $ i \<in> associates) \<and> (\<forall>i. \<not> is_zero_row i H \<longrightarrow> (\<forall>j<i. H $ j $ i \<in> residues (H $ i $ i)))
j < i

goal (1 subgoal):
 1. H $ j $ i \<in> residues (H $ i $ i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
H $ j $ (LEAST n. H $ i $ n \<noteq> 0) \<in> residues (H $ i $ (LEAST n. H $ i $ n \<noteq> 0))

goal:
No subgoals!
[PROOF STEP]
qed