[STATEMENT]
lemma mmulti_join_link:
  assumes "A_pos \<noteq> []"
      and "list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) (A_pos @ A_neg) L"
    shows "mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A_pos \<noteq> []
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) (A_pos @ A_neg) L

goal (1 subgoal):
 1. mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
proof (induction A_pos A_neg L rule: mmulti_join.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n A_pos A_neg L. \<lbrakk>\<And>x xa x2 xb y xc ya xd yb xe yc xf yba xg yaa xh yab xi yd xj ye xk yf xl yg. \<lbrakk>\<not> length A_pos + length A_neg \<noteq> length L; x = take (length A_pos) L; xa = drop (length A_pos) L; dominate_True A_pos x = None; dominate_False A_pos x A_neg xa = Some x2; (xb, y) = x2; (xc, ya) = xb; (xd, yb) = xc; (xe, yc) = yb; (xf, yba) = ya; (xg, yaa) = yba; (xh, yab) = y; (xi, yd) = xh; (xj, ye) = yd; (xk, yf) = yab; (xl, yg) = yf; xd @ xe # yc \<noteq> []; list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((xd @ xe # yc) @ xf @ yaa) ((xi @ bin_join n xe xj False xg xl # ye) @ xk @ yg)\<rbrakk> \<Longrightarrow> mmulti_join n (xd @ xe # yc) (xf @ yaa) ((xi @ bin_join n xe xj False xg xl # ye) @ xk @ yg) = mmulti_join' (xd @ xe # yc) (xf @ yaa) ((xi @ bin_join n xe xj False xg xl # ye) @ xk @ yg); \<And>x xa x2 xb y xc ya xd yb xe yaa xf yab xg yac xh yc xi yd xj ye. \<lbrakk>\<not> length A_pos + length A_neg \<noteq> length L; x = take (length A_pos) L; xa = drop (length A_pos) L; dominate_True A_pos x = Some x2; (xb, y) = x2; (xc, ya) = xb; (xd, yb) = ya; (xe, yaa) = yb; (xf, yab) = yaa; (xg, yac) = y; (xh, yc) = yac; (xi, yd) = yc; (xj, ye) = yd; xc @ (xd \<union> xf) # xe @ yab \<noteq> []; list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((xc @ (xd \<union> xf) # xe @ yab) @ A_neg) ((xg @ bin_join n xd xh True xf xj # xi @ ye) @ xa)\<rbrakk> \<Longrightarrow> mmulti_join n (xc @ (xd \<union> xf) # xe @ yab) A_neg ((xg @ bin_join n xd xh True xf xj # xi @ ye) @ xa) = mmulti_join' (xc @ (xd \<union> xf) # xe @ yab) A_neg ((xg @ bin_join n xd xh True xf xj # xi @ ye) @ xa); A_pos \<noteq> []; list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) (A_pos @ A_neg) L\<rbrakk> \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
case (1 n A_pos A_neg L)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> length A_pos + length A_neg \<noteq> length L; ?x = take (length A_pos) L; ?xa = drop (length A_pos) L; dominate_True A_pos ?x = None; dominate_False A_pos ?x A_neg ?xa = Some ?x2.0; (?xb, ?y) = ?x2.0; (?xc, ?ya) = ?xb; (?xd, ?yb) = ?xc; (?xe, ?yc) = ?yb; (?xf, ?yba) = ?ya; (?xg, ?yaa) = ?yba; (?xh, ?yab) = ?y; (?xi, ?yd) = ?xh; (?xj, ?ye) = ?yd; (?xk, ?yf) = ?yab; (?xl, ?yg) = ?yf; ?xd @ ?xe # ?yc \<noteq> []; list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((?xd @ ?xe # ?yc) @ ?xf @ ?yaa) ((?xi @ bin_join n ?xe ?xj False ?xg ?xl # ?ye) @ ?xk @ ?yg)\<rbrakk> \<Longrightarrow> mmulti_join n (?xd @ ?xe # ?yc) (?xf @ ?yaa) ((?xi @ bin_join n ?xe ?xj False ?xg ?xl # ?ye) @ ?xk @ ?yg) = mmulti_join' (?xd @ ?xe # ?yc) (?xf @ ?yaa) ((?xi @ bin_join n ?xe ?xj False ?xg ?xl # ?ye) @ ?xk @ ?yg)
\<lbrakk>\<not> length A_pos + length A_neg \<noteq> length L; ?x = take (length A_pos) L; ?xa = drop (length A_pos) L; dominate_True A_pos ?x = Some ?x2.0; (?xb, ?y) = ?x2.0; (?xc, ?ya) = ?xb; (?xd, ?yb) = ?ya; (?xe, ?yaa) = ?yb; (?xf, ?yab) = ?yaa; (?xg, ?yac) = ?y; (?xh, ?yc) = ?yac; (?xi, ?yd) = ?yc; (?xj, ?ye) = ?yd; ?xc @ (?xd \<union> ?xf) # ?xe @ ?yab \<noteq> []; list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((?xc @ (?xd \<union> ?xf) # ?xe @ ?yab) @ A_neg) ((?xg @ bin_join n ?xd ?xh True ?xf ?xj # ?xi @ ?ye) @ ?xa)\<rbrakk> \<Longrightarrow> mmulti_join n (?xc @ (?xd \<union> ?xf) # ?xe @ ?yab) A_neg ((?xg @ bin_join n ?xd ?xh True ?xf ?xj # ?xi @ ?ye) @ ?xa) = mmulti_join' (?xc @ (?xd \<union> ?xf) # ?xe @ ?yab) A_neg ((?xg @ bin_join n ?xd ?xh True ?xf ?xj # ?xi @ ?ye) @ ?xa)
A_pos \<noteq> []
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) (A_pos @ A_neg) L

goal (1 subgoal):
 1. \<And>n A_pos A_neg L. \<lbrakk>\<And>x xa x2 xb y xc ya xd yb xe yc xf yba xg yaa xh yab xi yd xj ye xk yf xl yg. \<lbrakk>\<not> length A_pos + length A_neg \<noteq> length L; x = take (length A_pos) L; xa = drop (length A_pos) L; dominate_True A_pos x = None; dominate_False A_pos x A_neg xa = Some x2; (xb, y) = x2; (xc, ya) = xb; (xd, yb) = xc; (xe, yc) = yb; (xf, yba) = ya; (xg, yaa) = yba; (xh, yab) = y; (xi, yd) = xh; (xj, ye) = yd; (xk, yf) = yab; (xl, yg) = yf; xd @ xe # yc \<noteq> []; list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((xd @ xe # yc) @ xf @ yaa) ((xi @ bin_join n xe xj False xg xl # ye) @ xk @ yg)\<rbrakk> \<Longrightarrow> mmulti_join n (xd @ xe # yc) (xf @ yaa) ((xi @ bin_join n xe xj False xg xl # ye) @ xk @ yg) = mmulti_join' (xd @ xe # yc) (xf @ yaa) ((xi @ bin_join n xe xj False xg xl # ye) @ xk @ yg); \<And>x xa x2 xb y xc ya xd yb xe yaa xf yab xg yac xh yc xi yd xj ye. \<lbrakk>\<not> length A_pos + length A_neg \<noteq> length L; x = take (length A_pos) L; xa = drop (length A_pos) L; dominate_True A_pos x = Some x2; (xb, y) = x2; (xc, ya) = xb; (xd, yb) = ya; (xe, yaa) = yb; (xf, yab) = yaa; (xg, yac) = y; (xh, yc) = yac; (xi, yd) = yc; (xj, ye) = yd; xc @ (xd \<union> xf) # xe @ yab \<noteq> []; list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((xc @ (xd \<union> xf) # xe @ yab) @ A_neg) ((xg @ bin_join n xd xh True xf xj # xi @ ye) @ xa)\<rbrakk> \<Longrightarrow> mmulti_join n (xc @ (xd \<union> xf) # xe @ yab) A_neg ((xg @ bin_join n xd xh True xf xj # xi @ ye) @ xa) = mmulti_join' (xc @ (xd \<union> xf) # xe @ yab) A_neg ((xg @ bin_join n xd xh True xf xj # xi @ ye) @ xa); A_pos \<noteq> []; list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) (A_pos @ A_neg) L\<rbrakk> \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
define L_pos where "L_pos = take (length A_pos) L"
[PROOF STATE]
proof (state)
this:
L_pos = take (length A_pos) L

goal (1 subgoal):
 1. \<And>n A_pos A_neg L. \<lbrakk>\<And>x xa x2 xb y xc ya xd yb xe yc xf yba xg yaa xh yab xi yd xj ye xk yf xl yg. \<lbrakk>\<not> length A_pos + length A_neg \<noteq> length L; x = take (length A_pos) L; xa = drop (length A_pos) L; dominate_True A_pos x = None; dominate_False A_pos x A_neg xa = Some x2; (xb, y) = x2; (xc, ya) = xb; (xd, yb) = xc; (xe, yc) = yb; (xf, yba) = ya; (xg, yaa) = yba; (xh, yab) = y; (xi, yd) = xh; (xj, ye) = yd; (xk, yf) = yab; (xl, yg) = yf; xd @ xe # yc \<noteq> []; list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((xd @ xe # yc) @ xf @ yaa) ((xi @ bin_join n xe xj False xg xl # ye) @ xk @ yg)\<rbrakk> \<Longrightarrow> mmulti_join n (xd @ xe # yc) (xf @ yaa) ((xi @ bin_join n xe xj False xg xl # ye) @ xk @ yg) = mmulti_join' (xd @ xe # yc) (xf @ yaa) ((xi @ bin_join n xe xj False xg xl # ye) @ xk @ yg); \<And>x xa x2 xb y xc ya xd yb xe yaa xf yab xg yac xh yc xi yd xj ye. \<lbrakk>\<not> length A_pos + length A_neg \<noteq> length L; x = take (length A_pos) L; xa = drop (length A_pos) L; dominate_True A_pos x = Some x2; (xb, y) = x2; (xc, ya) = xb; (xd, yb) = ya; (xe, yaa) = yb; (xf, yab) = yaa; (xg, yac) = y; (xh, yc) = yac; (xi, yd) = yc; (xj, ye) = yd; xc @ (xd \<union> xf) # xe @ yab \<noteq> []; list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((xc @ (xd \<union> xf) # xe @ yab) @ A_neg) ((xg @ bin_join n xd xh True xf xj # xi @ ye) @ xa)\<rbrakk> \<Longrightarrow> mmulti_join n (xc @ (xd \<union> xf) # xe @ yab) A_neg ((xg @ bin_join n xd xh True xf xj # xi @ ye) @ xa) = mmulti_join' (xc @ (xd \<union> xf) # xe @ yab) A_neg ((xg @ bin_join n xd xh True xf xj # xi @ ye) @ xa); A_pos \<noteq> []; list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) (A_pos @ A_neg) L\<rbrakk> \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
define L_neg where "L_neg = drop (length A_pos) L"
[PROOF STATE]
proof (state)
this:
L_neg = drop (length A_pos) L

goal (1 subgoal):
 1. \<And>n A_pos A_neg L. \<lbrakk>\<And>x xa x2 xb y xc ya xd yb xe yc xf yba xg yaa xh yab xi yd xj ye xk yf xl yg. \<lbrakk>\<not> length A_pos + length A_neg \<noteq> length L; x = take (length A_pos) L; xa = drop (length A_pos) L; dominate_True A_pos x = None; dominate_False A_pos x A_neg xa = Some x2; (xb, y) = x2; (xc, ya) = xb; (xd, yb) = xc; (xe, yc) = yb; (xf, yba) = ya; (xg, yaa) = yba; (xh, yab) = y; (xi, yd) = xh; (xj, ye) = yd; (xk, yf) = yab; (xl, yg) = yf; xd @ xe # yc \<noteq> []; list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((xd @ xe # yc) @ xf @ yaa) ((xi @ bin_join n xe xj False xg xl # ye) @ xk @ yg)\<rbrakk> \<Longrightarrow> mmulti_join n (xd @ xe # yc) (xf @ yaa) ((xi @ bin_join n xe xj False xg xl # ye) @ xk @ yg) = mmulti_join' (xd @ xe # yc) (xf @ yaa) ((xi @ bin_join n xe xj False xg xl # ye) @ xk @ yg); \<And>x xa x2 xb y xc ya xd yb xe yaa xf yab xg yac xh yc xi yd xj ye. \<lbrakk>\<not> length A_pos + length A_neg \<noteq> length L; x = take (length A_pos) L; xa = drop (length A_pos) L; dominate_True A_pos x = Some x2; (xb, y) = x2; (xc, ya) = xb; (xd, yb) = ya; (xe, yaa) = yb; (xf, yab) = yaa; (xg, yac) = y; (xh, yc) = yac; (xi, yd) = yc; (xj, ye) = yd; xc @ (xd \<union> xf) # xe @ yab \<noteq> []; list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((xc @ (xd \<union> xf) # xe @ yab) @ A_neg) ((xg @ bin_join n xd xh True xf xj # xi @ ye) @ xa)\<rbrakk> \<Longrightarrow> mmulti_join n (xc @ (xd \<union> xf) # xe @ yab) A_neg ((xg @ bin_join n xd xh True xf xj # xi @ ye) @ xa) = mmulti_join' (xc @ (xd \<union> xf) # xe @ yab) A_neg ((xg @ bin_join n xd xh True xf xj # xi @ ye) @ xa); A_pos \<noteq> []; list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) (A_pos @ A_neg) L\<rbrakk> \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
have L_def: "L = L_pos @ L_neg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L = L_pos @ L_neg
[PROOF STEP]
using L_pos_def L_neg_def
[PROOF STATE]
proof (prove)
using this:
L_pos = take (length A_pos) L
L_neg = drop (length A_pos) L

goal (1 subgoal):
 1. L = L_pos @ L_neg
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L = L_pos @ L_neg

goal (1 subgoal):
 1. \<And>n A_pos A_neg L. \<lbrakk>\<And>x xa x2 xb y xc ya xd yb xe yc xf yba xg yaa xh yab xi yd xj ye xk yf xl yg. \<lbrakk>\<not> length A_pos + length A_neg \<noteq> length L; x = take (length A_pos) L; xa = drop (length A_pos) L; dominate_True A_pos x = None; dominate_False A_pos x A_neg xa = Some x2; (xb, y) = x2; (xc, ya) = xb; (xd, yb) = xc; (xe, yc) = yb; (xf, yba) = ya; (xg, yaa) = yba; (xh, yab) = y; (xi, yd) = xh; (xj, ye) = yd; (xk, yf) = yab; (xl, yg) = yf; xd @ xe # yc \<noteq> []; list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((xd @ xe # yc) @ xf @ yaa) ((xi @ bin_join n xe xj False xg xl # ye) @ xk @ yg)\<rbrakk> \<Longrightarrow> mmulti_join n (xd @ xe # yc) (xf @ yaa) ((xi @ bin_join n xe xj False xg xl # ye) @ xk @ yg) = mmulti_join' (xd @ xe # yc) (xf @ yaa) ((xi @ bin_join n xe xj False xg xl # ye) @ xk @ yg); \<And>x xa x2 xb y xc ya xd yb xe yaa xf yab xg yac xh yc xi yd xj ye. \<lbrakk>\<not> length A_pos + length A_neg \<noteq> length L; x = take (length A_pos) L; xa = drop (length A_pos) L; dominate_True A_pos x = Some x2; (xb, y) = x2; (xc, ya) = xb; (xd, yb) = ya; (xe, yaa) = yb; (xf, yab) = yaa; (xg, yac) = y; (xh, yc) = yac; (xi, yd) = yc; (xj, ye) = yd; xc @ (xd \<union> xf) # xe @ yab \<noteq> []; list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((xc @ (xd \<union> xf) # xe @ yab) @ A_neg) ((xg @ bin_join n xd xh True xf xj # xi @ ye) @ xa)\<rbrakk> \<Longrightarrow> mmulti_join n (xc @ (xd \<union> xf) # xe @ yab) A_neg ((xg @ bin_join n xd xh True xf xj # xi @ ye) @ xa) = mmulti_join' (xc @ (xd \<union> xf) # xe @ yab) A_neg ((xg @ bin_join n xd xh True xf xj # xi @ ye) @ xa); A_pos \<noteq> []; list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) (A_pos @ A_neg) L\<rbrakk> \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
have lens_match: "length A_pos = length L_pos" "length A_neg = length L_neg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length A_pos = length L_pos &&& length A_neg = length L_neg
[PROOF STEP]
using L_pos_def L_neg_def 1(4)[unfolded L_def]
[PROOF STATE]
proof (prove)
using this:
L_pos = take (length A_pos) L
L_neg = drop (length A_pos) L
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) (A_pos @ A_neg) (L_pos @ L_neg)

goal (1 subgoal):
 1. length A_pos = length L_pos &&& length A_neg = length L_neg
[PROOF STEP]
by (auto dest: list_all2_lengthD)
[PROOF STATE]
proof (state)
this:
length A_pos = length L_pos
length A_neg = length L_neg

goal (1 subgoal):
 1. \<And>n A_pos A_neg L. \<lbrakk>\<And>x xa x2 xb y xc ya xd yb xe yc xf yba xg yaa xh yab xi yd xj ye xk yf xl yg. \<lbrakk>\<not> length A_pos + length A_neg \<noteq> length L; x = take (length A_pos) L; xa = drop (length A_pos) L; dominate_True A_pos x = None; dominate_False A_pos x A_neg xa = Some x2; (xb, y) = x2; (xc, ya) = xb; (xd, yb) = xc; (xe, yc) = yb; (xf, yba) = ya; (xg, yaa) = yba; (xh, yab) = y; (xi, yd) = xh; (xj, ye) = yd; (xk, yf) = yab; (xl, yg) = yf; xd @ xe # yc \<noteq> []; list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((xd @ xe # yc) @ xf @ yaa) ((xi @ bin_join n xe xj False xg xl # ye) @ xk @ yg)\<rbrakk> \<Longrightarrow> mmulti_join n (xd @ xe # yc) (xf @ yaa) ((xi @ bin_join n xe xj False xg xl # ye) @ xk @ yg) = mmulti_join' (xd @ xe # yc) (xf @ yaa) ((xi @ bin_join n xe xj False xg xl # ye) @ xk @ yg); \<And>x xa x2 xb y xc ya xd yb xe yaa xf yab xg yac xh yc xi yd xj ye. \<lbrakk>\<not> length A_pos + length A_neg \<noteq> length L; x = take (length A_pos) L; xa = drop (length A_pos) L; dominate_True A_pos x = Some x2; (xb, y) = x2; (xc, ya) = xb; (xd, yb) = ya; (xe, yaa) = yb; (xf, yab) = yaa; (xg, yac) = y; (xh, yc) = yac; (xi, yd) = yc; (xj, ye) = yd; xc @ (xd \<union> xf) # xe @ yab \<noteq> []; list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((xc @ (xd \<union> xf) # xe @ yab) @ A_neg) ((xg @ bin_join n xd xh True xf xj # xi @ ye) @ xa)\<rbrakk> \<Longrightarrow> mmulti_join n (xc @ (xd \<union> xf) # xe @ yab) A_neg ((xg @ bin_join n xd xh True xf xj # xi @ ye) @ xa) = mmulti_join' (xc @ (xd \<union> xf) # xe @ yab) A_neg ((xg @ bin_join n xd xh True xf xj # xi @ ye) @ xa); A_pos \<noteq> []; list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) (A_pos @ A_neg) L\<rbrakk> \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length A_pos = length L_pos
length A_neg = length L_neg
[PROOF STEP]
have lens_sum: "length A_pos + length A_neg = length L"
[PROOF STATE]
proof (prove)
using this:
length A_pos = length L_pos
length A_neg = length L_neg

goal (1 subgoal):
 1. length A_pos + length A_neg = length L
[PROOF STEP]
by (auto simp add: L_def)
[PROOF STATE]
proof (state)
this:
length A_pos + length A_neg = length L

goal (1 subgoal):
 1. \<And>n A_pos A_neg L. \<lbrakk>\<And>x xa x2 xb y xc ya xd yb xe yc xf yba xg yaa xh yab xi yd xj ye xk yf xl yg. \<lbrakk>\<not> length A_pos + length A_neg \<noteq> length L; x = take (length A_pos) L; xa = drop (length A_pos) L; dominate_True A_pos x = None; dominate_False A_pos x A_neg xa = Some x2; (xb, y) = x2; (xc, ya) = xb; (xd, yb) = xc; (xe, yc) = yb; (xf, yba) = ya; (xg, yaa) = yba; (xh, yab) = y; (xi, yd) = xh; (xj, ye) = yd; (xk, yf) = yab; (xl, yg) = yf; xd @ xe # yc \<noteq> []; list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((xd @ xe # yc) @ xf @ yaa) ((xi @ bin_join n xe xj False xg xl # ye) @ xk @ yg)\<rbrakk> \<Longrightarrow> mmulti_join n (xd @ xe # yc) (xf @ yaa) ((xi @ bin_join n xe xj False xg xl # ye) @ xk @ yg) = mmulti_join' (xd @ xe # yc) (xf @ yaa) ((xi @ bin_join n xe xj False xg xl # ye) @ xk @ yg); \<And>x xa x2 xb y xc ya xd yb xe yaa xf yab xg yac xh yc xi yd xj ye. \<lbrakk>\<not> length A_pos + length A_neg \<noteq> length L; x = take (length A_pos) L; xa = drop (length A_pos) L; dominate_True A_pos x = Some x2; (xb, y) = x2; (xc, ya) = xb; (xd, yb) = ya; (xe, yaa) = yb; (xf, yab) = yaa; (xg, yac) = y; (xh, yc) = yac; (xi, yd) = yc; (xj, ye) = yd; xc @ (xd \<union> xf) # xe @ yab \<noteq> []; list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((xc @ (xd \<union> xf) # xe @ yab) @ A_neg) ((xg @ bin_join n xd xh True xf xj # xi @ ye) @ xa)\<rbrakk> \<Longrightarrow> mmulti_join n (xc @ (xd \<union> xf) # xe @ yab) A_neg ((xg @ bin_join n xd xh True xf xj # xi @ ye) @ xa) = mmulti_join' (xc @ (xd \<union> xf) # xe @ yab) A_neg ((xg @ bin_join n xd xh True xf xj # xi @ ye) @ xa); A_pos \<noteq> []; list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) (A_pos @ A_neg) L\<rbrakk> \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
proof (cases "dominate_True A_pos L_pos")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dominate_True A_pos L_pos = None \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
 2. \<And>a. dominate_True A_pos L_pos = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
dominate_True A_pos L_pos = None

goal (2 subgoals):
 1. dominate_True A_pos L_pos = None \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
 2. \<And>a. dominate_True A_pos L_pos = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
note dom_True = None
[PROOF STATE]
proof (state)
this:
dominate_True A_pos L_pos = None

goal (2 subgoals):
 1. dominate_True A_pos L_pos = None \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
 2. \<And>a. dominate_True A_pos L_pos = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
proof (cases "dominate_False A_pos L_pos A_neg L_neg")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dominate_False A_pos L_pos A_neg L_neg = None \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
 2. \<And>a. dominate_False A_pos L_pos A_neg L_neg = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
dominate_False A_pos L_pos A_neg L_neg = None

goal (2 subgoals):
 1. dominate_False A_pos L_pos A_neg L_neg = None \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
 2. \<And>a. dominate_False A_pos L_pos A_neg L_neg = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
by (subst mmulti_join.simps)
           (simp del: dominate_True.simps dominate_False.simps mmulti_join.simps
            mmulti_join'.simps add: Let_def dom_True L_pos_def[symmetric] None
            L_neg_def[symmetric] lens_sum split: option.splits)
[PROOF STATE]
proof (state)
this:
mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L

goal (1 subgoal):
 1. \<And>a. dominate_False A_pos L_pos A_neg L_neg = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. dominate_False A_pos L_pos A_neg L_neg = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
case (Some a)
[PROOF STATE]
proof (state)
this:
dominate_False A_pos L_pos A_neg L_neg = Some a

goal (1 subgoal):
 1. \<And>a. dominate_False A_pos L_pos A_neg L_neg = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dominate_False A_pos L_pos A_neg L_neg = Some a
[PROOF STEP]
obtain A_zs A_x A_xs A_ws A_y A_ys zs x xs ws y ys where
        dom_False: "dominate_False A_pos L_pos A_neg L_neg =
        Some (((A_zs, A_x, A_xs), A_ws, A_y, A_ys), ((zs, x, xs), ws, y, ys))"
[PROOF STATE]
proof (prove)
using this:
dominate_False A_pos L_pos A_neg L_neg = Some a

goal (1 subgoal):
 1. (\<And>A_zs A_x A_xs A_ws A_y A_ys zs x xs ws y ys. dominate_False A_pos L_pos A_neg L_neg = Some (((A_zs, A_x, A_xs), A_ws, A_y, A_ys), (zs, x, xs), ws, y, ys) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases a) auto
[PROOF STATE]
proof (state)
this:
dominate_False A_pos L_pos A_neg L_neg = Some (((A_zs, A_x, A_xs), A_ws, A_y, A_ys), (zs, x, xs), ws, y, ys)

goal (1 subgoal):
 1. \<And>a. dominate_False A_pos L_pos A_neg L_neg = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
note list_all2 = 1(4)[unfolded L_def dominate_False_sound[OF dom_False lens_match]]
[PROOF STATE]
proof (state)
this:
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs) @ A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)

goal (1 subgoal):
 1. \<And>a. dominate_False A_pos L_pos A_neg L_neg = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
have lens: "length A_ws = length ws" "length A_xs = length xs"
        "length A_ys = length ys" "length A_zs = length zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (length A_ws = length ws &&& length A_xs = length xs) &&& length A_ys = length ys &&& length A_zs = length zs
[PROOF STEP]
using dominate_False_sound[OF dom_False lens_match]
[PROOF STATE]
proof (prove)
using this:
A_pos = A_zs @ A_x # A_xs
A_neg = A_ws @ A_y # A_ys
L_pos = zs @ x # xs
L_neg = ws @ y # ys
length A_ws = length ws
length A_xs = length xs
length A_ys = length ys
length A_zs = length zs
A_y \<subseteq> A_x

goal (1 subgoal):
 1. (length A_ws = length ws &&& length A_xs = length xs) &&& length A_ys = length ys &&& length A_zs = length zs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length A_ws = length ws
length A_xs = length xs
length A_ys = length ys
length A_zs = length zs

goal (1 subgoal):
 1. \<And>a. dominate_False A_pos L_pos A_neg L_neg = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
have sub: "A_y \<subseteq> A_x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A_y \<subseteq> A_x
[PROOF STEP]
using dominate_False_sound[OF dom_False lens_match]
[PROOF STATE]
proof (prove)
using this:
A_pos = A_zs @ A_x # A_xs
A_neg = A_ws @ A_y # A_ys
L_pos = zs @ x # xs
L_neg = ws @ y # ys
length A_ws = length ws
length A_xs = length xs
length A_ys = length ys
length A_zs = length zs
A_y \<subseteq> A_x

goal (1 subgoal):
 1. A_y \<subseteq> A_x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A_y \<subseteq> A_x

goal (1 subgoal):
 1. \<And>a. dominate_False A_pos L_pos A_neg L_neg = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
have list_all2': "list_all2 (\<lambda>A X. table n A X \<and> wf_set n A)
        ((A_zs @ A_x # A_xs) @ (A_ws @ A_ys)) ((zs @ join x False y # xs) @ (ws @ ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs) @ A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
[PROOF STEP]
using list_all2_opt_False[OF list_all2 lens sub]
[PROOF STATE]
proof (prove)
using this:
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs) @ A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)

goal (1 subgoal):
 1. list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs) @ A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs) @ A_ws @ A_ys) ((zs @ join x False y # xs) @ ws @ ys)

goal (1 subgoal):
 1. \<And>a. dominate_False A_pos L_pos A_neg L_neg = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
have tabs: "table n A_x x" "table n A_y y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. table n A_x x &&& table n A_y y
[PROOF STEP]
using list_all2
[PROOF STATE]
proof (prove)
using this:
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs) @ A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)

goal (1 subgoal):
 1. table n A_x x &&& table n A_y y
[PROOF STEP]
by (auto simp add: lens list_all2_append)
[PROOF STATE]
proof (state)
this:
table n A_x x
table n A_y y

goal (1 subgoal):
 1. \<And>a. dominate_False A_pos L_pos A_neg L_neg = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
have bin_join_conv: "join x False y = bin_join n A_x x False A_y y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. join x False y = bin_join n A_x x False A_y y
[PROOF STEP]
using bin_join_table[OF tabs, symmetric]
[PROOF STATE]
proof (prove)
using this:
join x ?pos y = bin_join n A_x x ?pos A_y y

goal (1 subgoal):
 1. join x False y = bin_join n A_x x False A_y y
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
join x False y = bin_join n A_x x False A_y y

goal (1 subgoal):
 1. \<And>a. dominate_False A_pos L_pos A_neg L_neg = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
have mmulti: "mmulti_join n A_pos A_neg L = mmulti_join n (A_zs @ A_x # A_xs) (A_ws @ A_ys)
        ((zs @ bin_join n A_x x False A_y y # xs) @ (ws @ ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mmulti_join n A_pos A_neg L = mmulti_join n (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ bin_join n A_x x False A_y y # xs) @ ws @ ys)
[PROOF STEP]
by (subst mmulti_join.simps)
           (simp del: dominate_True.simps dominate_False.simps mmulti_join.simps
            add: Let_def dom_True L_pos_def[symmetric] L_neg_def[symmetric] dom_False lens_sum)
[PROOF STATE]
proof (state)
this:
mmulti_join n A_pos A_neg L = mmulti_join n (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ bin_join n A_x x False A_y y # xs) @ ws @ ys)

goal (1 subgoal):
 1. \<And>a. dominate_False A_pos L_pos A_neg L_neg = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
unfolding mmulti
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mmulti_join n (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ bin_join n A_x x False A_y y # xs) @ ws @ ys) = mmulti_join' A_pos A_neg L
[PROOF STEP]
unfolding L_def dominate_False_sound[OF dom_False lens_match]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mmulti_join n (A_zs @ A_x # A_xs) (A_ws @ A_ys) ((zs @ bin_join n A_x x False A_y y # xs) @ ws @ ys) = mmulti_join' (A_zs @ A_x # A_xs) (A_ws @ A_y # A_ys) ((zs @ x # xs) @ ws @ y # ys)
[PROOF STEP]
by (rule 1(1)[OF _ L_pos_def L_neg_def dom_True dom_False,
            OF _ _ _ _ _ _ _ _ _ _ _ _ _ list_all2'[unfolded bin_join_conv],
            unfolded mmulti_join'_opt_False[OF list_all2 lens sub, symmetric,
            unfolded bin_join_conv]])
           (auto simp add: lens_sum)
[PROOF STATE]
proof (state)
this:
mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L

goal (1 subgoal):
 1. \<And>a. dominate_True A_pos L_pos = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. dominate_True A_pos L_pos = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
case (Some a)
[PROOF STATE]
proof (state)
this:
dominate_True A_pos L_pos = Some a

goal (1 subgoal):
 1. \<And>a. dominate_True A_pos L_pos = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dominate_True A_pos L_pos = Some a
[PROOF STEP]
obtain A_zs A_x A_xs A_y A_ys zs x xs y ys where dom_True: "dominate_True A_pos L_pos =
      Some ((A_zs, A_x, A_xs, A_y, A_ys), (zs, x, xs, y, ys))"
[PROOF STATE]
proof (prove)
using this:
dominate_True A_pos L_pos = Some a

goal (1 subgoal):
 1. (\<And>A_zs A_x A_xs A_y A_ys zs x xs y ys. dominate_True A_pos L_pos = Some ((A_zs, A_x, A_xs, A_y, A_ys), zs, x, xs, y, ys) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases a) auto
[PROOF STATE]
proof (state)
this:
dominate_True A_pos L_pos = Some ((A_zs, A_x, A_xs, A_y, A_ys), zs, x, xs, y, ys)

goal (1 subgoal):
 1. \<And>a. dominate_True A_pos L_pos = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
note list_all2 = 1(4)[unfolded L_def dominate_True_sound[OF dom_True lens_match(1)]]
[PROOF STATE]
proof (state)
this:
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs @ A_y # A_ys) @ A_neg) ((zs @ x # xs @ y # ys) @ L_neg)

goal (1 subgoal):
 1. \<And>a. dominate_True A_pos L_pos = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
have lens: "length A_xs = length xs" "length A_ys = length ys" "length A_zs = length zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length A_xs = length xs &&& length A_ys = length ys &&& length A_zs = length zs
[PROOF STEP]
using dominate_True_sound[OF dom_True lens_match(1)]
[PROOF STATE]
proof (prove)
using this:
A_pos = A_zs @ A_x # A_xs @ A_y # A_ys
L_pos = zs @ x # xs @ y # ys
length A_xs = length xs
length A_ys = length ys
length A_zs = length zs

goal (1 subgoal):
 1. length A_xs = length xs &&& length A_ys = length ys &&& length A_zs = length zs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length A_xs = length xs
length A_ys = length ys
length A_zs = length zs

goal (1 subgoal):
 1. \<And>a. dominate_True A_pos L_pos = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
have list_all2': "list_all2 (\<lambda>A X. table n A X \<and> wf_set n A)
      ((A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) @ A_neg) ((zs @ join x True y # xs @ ys) @ L_neg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) @ A_neg) ((zs @ join x True y # xs @ ys) @ L_neg)
[PROOF STEP]
using list_all2_opt_True[OF list_all2 lens]
[PROOF STATE]
proof (prove)
using this:
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) @ A_neg) ((zs @ join x True y # xs @ ys) @ L_neg)

goal (1 subgoal):
 1. list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) @ A_neg) ((zs @ join x True y # xs @ ys) @ L_neg)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) @ A_neg) ((zs @ join x True y # xs @ ys) @ L_neg)

goal (1 subgoal):
 1. \<And>a. dominate_True A_pos L_pos = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
have tabs: "table n A_x x" "table n A_y y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. table n A_x x &&& table n A_y y
[PROOF STEP]
using list_all2
[PROOF STATE]
proof (prove)
using this:
list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) ((A_zs @ A_x # A_xs @ A_y # A_ys) @ A_neg) ((zs @ x # xs @ y # ys) @ L_neg)

goal (1 subgoal):
 1. table n A_x x &&& table n A_y y
[PROOF STEP]
by (auto simp add: lens list_all2_append)
[PROOF STATE]
proof (state)
this:
table n A_x x
table n A_y y

goal (1 subgoal):
 1. \<And>a. dominate_True A_pos L_pos = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
have bin_join_conv: "join x True y = bin_join n A_x x True A_y y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. join x True y = bin_join n A_x x True A_y y
[PROOF STEP]
using bin_join_table[OF tabs, symmetric]
[PROOF STATE]
proof (prove)
using this:
join x ?pos y = bin_join n A_x x ?pos A_y y

goal (1 subgoal):
 1. join x True y = bin_join n A_x x True A_y y
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
join x True y = bin_join n A_x x True A_y y

goal (1 subgoal):
 1. \<And>a. dominate_True A_pos L_pos = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
have mmulti: "mmulti_join n A_pos A_neg L = mmulti_join n (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys)
      A_neg ((zs @ bin_join n A_x x True A_y y # xs @ ys) @ L_neg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mmulti_join n A_pos A_neg L = mmulti_join n (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ bin_join n A_x x True A_y y # xs @ ys) @ L_neg)
[PROOF STEP]
by (subst mmulti_join.simps)
         (simp del: dominate_True.simps dominate_False.simps mmulti_join.simps
          add: Let_def dom_True L_pos_def[symmetric] L_neg_def lens_sum)
[PROOF STATE]
proof (state)
this:
mmulti_join n A_pos A_neg L = mmulti_join n (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ bin_join n A_x x True A_y y # xs @ ys) @ L_neg)

goal (1 subgoal):
 1. \<And>a. dominate_True A_pos L_pos = Some a \<Longrightarrow> mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L
[PROOF STEP]
unfolding mmulti
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mmulti_join n (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ bin_join n A_x x True A_y y # xs @ ys) @ L_neg) = mmulti_join' A_pos A_neg L
[PROOF STEP]
unfolding L_def dominate_True_sound[OF dom_True lens_match(1)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mmulti_join n (A_zs @ (A_x \<union> A_y) # A_xs @ A_ys) A_neg ((zs @ bin_join n A_x x True A_y y # xs @ ys) @ L_neg) = mmulti_join' (A_zs @ A_x # A_xs @ A_y # A_ys) A_neg ((zs @ x # xs @ y # ys) @ L_neg)
[PROOF STEP]
by (rule 1(2)[OF _ L_pos_def L_neg_def dom_True,
          OF _ _ _ _ _ _ _ _ _ _ _ list_all2'[unfolded bin_join_conv],
          unfolded mmulti_join'_opt_True[OF list_all2 lens, symmetric,
          unfolded bin_join_conv]])
         (auto simp add: lens_sum)
[PROOF STATE]
proof (state)
this:
mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mmulti_join n A_pos A_neg L = mmulti_join' A_pos A_neg L

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mmulti_join_correct:
  assumes "A_pos \<noteq> []"
      and "list_all2 (\<lambda>A X. table n A X \<and> wf_set n A) (A_pos @ A_neg) L"
  shows "z \<in> mmulti_join n A_pos A_neg L \<longleftrightarrow> wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and>
    list_all2 (\<lambda>A X. restrict A z \<in> X) A_pos (take (length A_pos) L) \<and>
    list_all2 (\<lambda>A X. restrict A z \<notin> X) A_neg (drop (length A_pos) L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z \<in> mmulti_join n A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))
[PROOF STEP]
unfolding mmulti_join_link[OF assms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))
[PROOF STEP]
using mmulti_join'_correct[OF assms]
[PROOF STATE]
proof (prove)
using this:
(?z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) ?z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A ?z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A ?z)) A_neg (drop (length A_pos) L))

goal (1 subgoal):
 1. (z \<in> mmulti_join' A_pos A_neg L) = (wf_tuple n (\<Union>A\<in>set A_pos. A) z \<and> list_all2 (\<lambda>A. (\<in>) (restrict A z)) A_pos (take (length A_pos) L) \<and> list_all2 (\<lambda>A. (\<notin>) (restrict A z)) A_neg (drop (length A_pos) L))
[PROOF STEP]
.


[STATEMENT]
lemma conf_Null [simp]: "P,h \<turnstile> Null :\<le> T  =  P \<turnstile> NT \<le> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P,h \<turnstile> Null :\<le> T) = P \<turnstile> NT \<le> T
[PROOF STEP]
unfolding conf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>T'. typeof\<^bsub>h\<^esub> Null = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T) = P \<turnstile> NT \<le> T
[PROOF STEP]
by(simp (no_asm))


[STATEMENT]
lemma typeof_conf[simp]: "typeof\<^bsub>h\<^esub> v = Some T \<Longrightarrow> P,h \<turnstile> v :\<le> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor> \<Longrightarrow> P,h \<turnstile> v :\<le> T
[PROOF STEP]
unfolding conf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor> \<Longrightarrow> \<exists>T'. typeof\<^bsub>h\<^esub> v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
by (cases v) auto


[STATEMENT]
lemma typeof_lit_conf[simp]: "typeof v = Some T \<Longrightarrow> P,h \<turnstile> v :\<le> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. typeof v = \<lfloor>T\<rfloor> \<Longrightarrow> P,h \<turnstile> v :\<le> T
[PROOF STEP]
by (rule typeof_conf[OF typeof_lit_typeof])


[STATEMENT]
lemma defval_conf[simp]: "P,h \<turnstile> default_val T :\<le> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,h \<turnstile> default_val T :\<le> T
[PROOF STEP]
unfolding conf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>T'. typeof\<^bsub>h\<^esub> (default_val T) = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
by (cases T) auto


[STATEMENT]
lemma conf_widen: "P,h \<turnstile> v :\<le> T \<Longrightarrow> P \<turnstile> T \<le> T' \<Longrightarrow> P,h \<turnstile> v :\<le> T'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,h \<turnstile> v :\<le> T; P \<turnstile> T \<le> T'\<rbrakk> \<Longrightarrow> P,h \<turnstile> v :\<le> T'
[PROOF STEP]
unfolding conf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>T'. typeof\<^bsub>h\<^esub> v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T; P \<turnstile> T \<le> T'\<rbrakk> \<Longrightarrow> \<exists>T'a. typeof\<^bsub>h\<^esub> v = \<lfloor>T'a\<rfloor> \<and> P \<turnstile> T'a \<le> T'
[PROOF STEP]
by (cases v) (auto intro: widen_trans)


[STATEMENT]
lemma conf_sys_xcpt:
  "\<lbrakk>preallocated h; C \<in> sys_xcpts\<rbrakk> \<Longrightarrow> P,h \<turnstile> Addr (addr_of_sys_xcpt C) :\<le> Class C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>preallocated h; C \<in> sys_xcpts\<rbrakk> \<Longrightarrow> P,h \<turnstile> Addr (addr_of_sys_xcpt C) :\<le> Class C
[PROOF STEP]
by(simp add: conf_def typeof_addr_sys_xcp)


[STATEMENT]
lemma conf_NT [iff]: "P,h \<turnstile> v :\<le> NT = (v = Null)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P,h \<turnstile> v :\<le> NT) = (v = Null)
[PROOF STEP]
by (auto simp add: conf_def)


[STATEMENT]
lemma is_IntgI: "P,h \<turnstile> v :\<le> Integer \<Longrightarrow> is_Intg v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,h \<turnstile> v :\<le> Integer \<Longrightarrow> is_Intg v
[PROOF STEP]
by (unfold conf_def) auto


[STATEMENT]
lemma is_BoolI: "P,h \<turnstile> v :\<le> Boolean \<Longrightarrow> is_Bool v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,h \<turnstile> v :\<le> Boolean \<Longrightarrow> is_Bool v
[PROOF STEP]
by (unfold conf_def) auto


[STATEMENT]
lemma is_RefI: "P,h \<turnstile> v :\<le> T \<Longrightarrow> is_refT T \<Longrightarrow> is_Ref v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,h \<turnstile> v :\<le> T; is_refT T\<rbrakk> \<Longrightarrow> is_Ref v
[PROOF STEP]
by(cases v)(auto elim: is_refT.cases simp add: conf_def is_Ref_def)


[STATEMENT]
lemma non_npD:
  "\<lbrakk> v \<noteq> Null; P,h \<turnstile> v :\<le> Class C; C \<noteq> Object \<rbrakk>
  \<Longrightarrow> \<exists>a C'. v = Addr a \<and> typeof_addr h a = \<lfloor>Class_type C'\<rfloor> \<and> P \<turnstile> C' \<preceq>\<^sup>* C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v \<noteq> Null; P,h \<turnstile> v :\<le> Class C; C \<noteq> Object\<rbrakk> \<Longrightarrow> \<exists>a C'. v = Addr a \<and> typeof_addr h a = \<lfloor>Class_type C'\<rfloor> \<and> P \<turnstile> C' \<preceq>\<^sup>* C
[PROOF STEP]
by(cases v)(auto simp add: conf_def widen_Class)


[STATEMENT]
lemma non_npD2:
  "\<lbrakk>v \<noteq> Null; P,h \<turnstile> v :\<le> Class C \<rbrakk>
  \<Longrightarrow> \<exists>a hT. v = Addr a \<and> typeof_addr h a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT \<preceq>\<^sup>* C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v \<noteq> Null; P,h \<turnstile> v :\<le> Class C\<rbrakk> \<Longrightarrow> \<exists>a hT. v = Addr a \<and> typeof_addr h a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT \<preceq>\<^sup>* C
[PROOF STEP]
by(cases v)(auto simp add: conf_def widen_Class)


[STATEMENT]
lemma conf_hext: "\<lbrakk> h \<unlhd> h'; P,h \<turnstile> v :\<le> T \<rbrakk> \<Longrightarrow> P,h' \<turnstile> v :\<le> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h \<unlhd> h'; P,h \<turnstile> v :\<le> T\<rbrakk> \<Longrightarrow> P,h' \<turnstile> v :\<le> T
[PROOF STEP]
unfolding conf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h \<unlhd> h'; \<exists>T'. typeof\<^bsub>h\<^esub> v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T\<rbrakk> \<Longrightarrow> \<exists>T'. typeof\<^bsub>h'\<^esub> v = \<lfloor>T'\<rfloor> \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
by(cases v)(auto dest: typeof_addr_hext_mono)


[STATEMENT]
lemma conf_heap_ops_mono:
  assumes "P,h \<turnstile> v :\<le> T"
  shows conf_allocate_mono: "(h', a) \<in> allocate h hT \<Longrightarrow> P,h' \<turnstile> v :\<le> T"
  and conf_heap_write_mono: "heap_write h a al v' h' \<Longrightarrow> P,h' \<turnstile> v :\<le> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((h', a) \<in> allocate h hT \<Longrightarrow> P,h' \<turnstile> v :\<le> T) &&& (heap_write h a al v' h' \<Longrightarrow> P,h' \<turnstile> v :\<le> T)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P,h \<turnstile> v :\<le> T

goal (1 subgoal):
 1. ((h', a) \<in> allocate h hT \<Longrightarrow> P,h' \<turnstile> v :\<le> T) &&& (heap_write h a al v' h' \<Longrightarrow> P,h' \<turnstile> v :\<le> T)
[PROOF STEP]
by(auto intro: conf_hext dest: hext_heap_ops)


[STATEMENT]
lemma confs_widens [trans]: "\<lbrakk>P,h \<turnstile> vs [:\<le>] Ts; P \<turnstile> Ts [\<le>] Ts'\<rbrakk> \<Longrightarrow> P,h \<turnstile> vs [:\<le>] Ts'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,h \<turnstile> vs [:\<le>] Ts; P \<turnstile> Ts [\<le>] Ts'\<rbrakk> \<Longrightarrow> P,h \<turnstile> vs [:\<le>] Ts'
[PROOF STEP]
by (rule list_all2_trans)(rule conf_widen)


[STATEMENT]
lemma confs_rev: "P,h \<turnstile> rev s [:\<le>] t = (P,h \<turnstile> s [:\<le>] rev t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P,h \<turnstile> rev s [:\<le>] t) = (P,h \<turnstile> s [:\<le>] rev t)
[PROOF STEP]
by(rule list_all2_rev1)


[STATEMENT]
lemma confs_conv_map:
  "P,h \<turnstile> vs [:\<le>] Ts' = (\<exists>Ts. map typeof\<^bsub>h\<^esub> vs = map Some Ts \<and> P \<turnstile> Ts [\<le>] Ts')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P,h \<turnstile> vs [:\<le>] Ts') = (\<exists>Ts. map typeof\<^bsub>h\<^esub> vs = map Some Ts \<and> P \<turnstile> Ts [\<le>] Ts')
[PROOF STEP]
apply(induct vs arbitrary: Ts')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Ts'. (P,h \<turnstile> [] [:\<le>] Ts') = (\<exists>Ts. map typeof\<^bsub>h\<^esub> [] = map Some Ts \<and> P \<turnstile> Ts [\<le>] Ts')
 2. \<And>a vs Ts'. (\<And>Ts'. (P,h \<turnstile> vs [:\<le>] Ts') = (\<exists>Ts. map typeof\<^bsub>h\<^esub> vs = map Some Ts \<and> P \<turnstile> Ts [\<le>] Ts')) \<Longrightarrow> (P,h \<turnstile> a # vs [:\<le>] Ts') = (\<exists>Ts. map typeof\<^bsub>h\<^esub> (a # vs) = map Some Ts \<and> P \<turnstile> Ts [\<le>] Ts')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a vs Ts'. (\<And>Ts'. (P,h \<turnstile> vs [:\<le>] Ts') = (\<exists>Ts. map typeof\<^bsub>h\<^esub> vs = map Some Ts \<and> P \<turnstile> Ts [\<le>] Ts')) \<Longrightarrow> (P,h \<turnstile> a # vs [:\<le>] Ts') = (\<exists>Ts. map typeof\<^bsub>h\<^esub> (a # vs) = map Some Ts \<and> P \<turnstile> Ts [\<le>] Ts')
[PROOF STEP]
apply(case_tac Ts')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a vs Ts'. \<lbrakk>\<And>Ts'. (P,h \<turnstile> vs [:\<le>] Ts') = (\<exists>Ts. map typeof\<^bsub>h\<^esub> vs = map Some Ts \<and> P \<turnstile> Ts [\<le>] Ts'); Ts' = []\<rbrakk> \<Longrightarrow> (P,h \<turnstile> a # vs [:\<le>] Ts') = (\<exists>Ts. map typeof\<^bsub>h\<^esub> (a # vs) = map Some Ts \<and> P \<turnstile> Ts [\<le>] Ts')
 2. \<And>a vs Ts' aa list. \<lbrakk>\<And>Ts'. (P,h \<turnstile> vs [:\<le>] Ts') = (\<exists>Ts. map typeof\<^bsub>h\<^esub> vs = map Some Ts \<and> P \<turnstile> Ts [\<le>] Ts'); Ts' = aa # list\<rbrakk> \<Longrightarrow> (P,h \<turnstile> a # vs [:\<le>] Ts') = (\<exists>Ts. map typeof\<^bsub>h\<^esub> (a # vs) = map Some Ts \<and> P \<turnstile> Ts [\<le>] Ts')
[PROOF STEP]
apply(auto simp add:conf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a vs aa list T' Ts. \<lbrakk>\<And>Ts'. (P,h \<turnstile> vs [:\<le>] Ts') = P \<turnstile> Ts [\<le>] Ts'; typeof\<^bsub>h\<^esub> a = \<lfloor>T'\<rfloor>; P \<turnstile> T' \<le> aa; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] list\<rbrakk> \<Longrightarrow> \<exists>Tsa. \<lfloor>T'\<rfloor> # map Some Ts = map Some Tsa \<and> P \<turnstile> Tsa [\<le>] (aa # list)
[PROOF STEP]
apply(rule_tac x="T' # Ts" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a vs aa list T' Ts. \<lbrakk>\<And>Ts'. (P,h \<turnstile> vs [:\<le>] Ts') = P \<turnstile> Ts [\<le>] Ts'; typeof\<^bsub>h\<^esub> a = \<lfloor>T'\<rfloor>; P \<turnstile> T' \<le> aa; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] list\<rbrakk> \<Longrightarrow> \<lfloor>T'\<rfloor> # map Some Ts = map Some (T' # Ts) \<and> P \<turnstile> (T' # Ts) [\<le>] (aa # list)
[PROOF STEP]
apply(simp add: fun_of_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma confs_Cons2: "P,h \<turnstile> xs [:\<le>] y#ys = (\<exists>z zs. xs = z#zs \<and> P,h \<turnstile> z :\<le> y \<and> P,h \<turnstile> zs [:\<le>] ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P,h \<turnstile> xs [:\<le>] y # ys) = (\<exists>z zs. xs = z # zs \<and> P,h \<turnstile> z :\<le> y \<and> P,h \<turnstile> zs [:\<le>] ys)
[PROOF STEP]
by (rule list_all2_Cons2)


[STATEMENT]
lemma confs_hext: "P,h \<turnstile> vs [:\<le>] Ts \<Longrightarrow> h \<unlhd> h' \<Longrightarrow> P,h' \<turnstile> vs [:\<le>] Ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,h \<turnstile> vs [:\<le>] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,h' \<turnstile> vs [:\<le>] Ts
[PROOF STEP]
by (erule list_all2_mono, erule conf_hext, assumption)


[STATEMENT]
lemma lconf_upd:
  "\<lbrakk> P,h \<turnstile> l (:\<le>) E; P,h \<turnstile> v :\<le> T; E V = Some T \<rbrakk> \<Longrightarrow> P,h \<turnstile> l(V\<mapsto>v) (:\<le>) E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,h \<turnstile> l (:\<le>) E; P,h \<turnstile> v :\<le> T; E V = \<lfloor>T\<rfloor>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l(V \<mapsto> v) (:\<le>) E
[PROOF STEP]
unfolding lconf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>V v. l V = \<lfloor>v\<rfloor> \<longrightarrow> (\<exists>T. E V = \<lfloor>T\<rfloor> \<and> P,h \<turnstile> v :\<le> T); P,h \<turnstile> v :\<le> T; E V = \<lfloor>T\<rfloor>\<rbrakk> \<Longrightarrow> \<forall>Va va. (l(V \<mapsto> v)) Va = \<lfloor>va\<rfloor> \<longrightarrow> (\<exists>T. E Va = \<lfloor>T\<rfloor> \<and> P,h \<turnstile> va :\<le> T)
[PROOF STEP]
by auto


[STATEMENT]
lemma lconf_empty [iff]: "P,h \<turnstile> Map.empty (:\<le>) E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,h \<turnstile> Map.empty (:\<le>) E
[PROOF STEP]
by(simp add:lconf_def)


[STATEMENT]
lemma lconf_upd2: "\<lbrakk>P,h \<turnstile> l (:\<le>) E; P,h \<turnstile> v :\<le> T\<rbrakk> \<Longrightarrow> P,h \<turnstile> l(V\<mapsto>v) (:\<le>) E(V\<mapsto>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,h \<turnstile> l (:\<le>) E; P,h \<turnstile> v :\<le> T\<rbrakk> \<Longrightarrow> P,h \<turnstile> l(V \<mapsto> v) (:\<le>) E(V \<mapsto> T)
[PROOF STEP]
by(simp add:lconf_def)


[STATEMENT]
lemma lconf_hext: "\<lbrakk> P,h \<turnstile> l (:\<le>) E; h \<unlhd> h' \<rbrakk> \<Longrightarrow> P,h' \<turnstile> l (:\<le>) E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,h \<turnstile> l (:\<le>) E; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,h' \<turnstile> l (:\<le>) E
[PROOF STEP]
unfolding lconf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>V v. l V = \<lfloor>v\<rfloor> \<longrightarrow> (\<exists>T. E V = \<lfloor>T\<rfloor> \<and> P,h \<turnstile> v :\<le> T); h \<unlhd> h'\<rbrakk> \<Longrightarrow> \<forall>V v. l V = \<lfloor>v\<rfloor> \<longrightarrow> (\<exists>T. E V = \<lfloor>T\<rfloor> \<and> P,h' \<turnstile> v :\<le> T)
[PROOF STEP]
by(fast elim: conf_hext)


[STATEMENT]
lemma tconfI: "\<lbrakk> typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread \<rbrakk> \<Longrightarrow> P,h \<turnstile> t \<surd>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> P,h \<turnstile> t \<surd>t
[PROOF STEP]
by(simp add: tconf_def)


[STATEMENT]
lemma tconfD: "P,h \<turnstile> t \<surd>t \<Longrightarrow> \<exists>C. typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor> \<and> P \<turnstile> C \<preceq>\<^sup>* Thread"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,h \<turnstile> t \<surd>t \<Longrightarrow> \<exists>C. typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor> \<and> P \<turnstile> C \<preceq>\<^sup>* Thread
[PROOF STEP]
by(auto simp add: tconf_def)


[STATEMENT]
lemma tconf_hext_mono: "\<lbrakk> P,h \<turnstile> t \<surd>t; h \<unlhd> h' \<rbrakk> \<Longrightarrow> P,h' \<turnstile> t \<surd>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,h \<turnstile> t \<surd>t; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,h' \<turnstile> t \<surd>t
[PROOF STEP]
by(auto simp add: tconf_def dest: typeof_addr_hext_mono)


[STATEMENT]
lemma tconf_heap_ops_mono:
  assumes "P,h \<turnstile> t \<surd>t"
  shows tconf_allocate_mono: "(h', a) \<in> allocate h hT \<Longrightarrow> P,h' \<turnstile> t \<surd>t"
  and tconf_heap_write_mono: "heap_write h a al v h' \<Longrightarrow> P,h' \<turnstile> t \<surd>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((h', a) \<in> allocate h hT \<Longrightarrow> P,h' \<turnstile> t \<surd>t) &&& (heap_write h a al v h' \<Longrightarrow> P,h' \<turnstile> t \<surd>t)
[PROOF STEP]
using tconf_hext_mono[OF assms, of h']
[PROOF STATE]
proof (prove)
using this:
h \<unlhd> h' \<Longrightarrow> P,h' \<turnstile> t \<surd>t

goal (1 subgoal):
 1. ((h', a) \<in> allocate h hT \<Longrightarrow> P,h' \<turnstile> t \<surd>t) &&& (heap_write h a al v h' \<Longrightarrow> P,h' \<turnstile> t \<surd>t)
[PROOF STEP]
by(blast intro: hext_heap_ops)+


[STATEMENT]
lemma tconf_start_heap_start_tid:
  "\<lbrakk> start_heap_ok; wf_syscls P \<rbrakk> \<Longrightarrow> P,start_heap \<turnstile> start_tid \<surd>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>start_heap_ok; wf_syscls P\<rbrakk> \<Longrightarrow> P,start_heap \<turnstile> start_tid \<surd>t
[PROOF STEP]
unfolding start_tid_def start_heap_def start_heap_ok_def start_heap_data_def initialization_list_def addr_of_sys_xcpt_def start_addrs_def sys_xcpts_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>snd (snd (foldl create_initial_object (empty_heap, [], True) [Thread, NullPointer, ClassCast, OutOfMemory, ArrayIndexOutOfBounds, ArrayStore, NegativeArraySize, ArithmeticException, IllegalMonitorState, IllegalThreadState, InterruptedException])); wf_syscls P\<rbrakk> \<Longrightarrow> P,fst (foldl create_initial_object (empty_heap, [], True) [Thread, NullPointer, ClassCast, OutOfMemory, ArrayIndexOutOfBounds, ArrayStore, NegativeArraySize, ArithmeticException, IllegalMonitorState, IllegalThreadState, InterruptedException]) \<turnstile> addr2thread_id (hd (fst (snd (foldl create_initial_object (empty_heap, [], True) [Thread, NullPointer, ClassCast, OutOfMemory, ArrayIndexOutOfBounds, ArrayStore, NegativeArraySize, ArithmeticException, IllegalMonitorState, IllegalThreadState, InterruptedException])))) \<surd>t
[PROOF STEP]
apply(clarsimp split: prod.split_asm simp add: create_initial_object_simps split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j. \<lbrakk>wf_syscls P; allocate empty_heap (Class_type Thread) \<noteq> {}; (SOME ha. ha \<in> allocate empty_heap (Class_type Thread)) = (x1, x2); allocate x1 (Class_type NullPointer) \<noteq> {}; (SOME ha. ha \<in> allocate x1 (Class_type NullPointer)) = (x1a, x2a); allocate x1a (Class_type ClassCast) \<noteq> {}; (SOME ha. ha \<in> allocate x1a (Class_type ClassCast)) = (x1b, x2b); allocate x1b (Class_type OutOfMemory) \<noteq> {}; (SOME ha. ha \<in> allocate x1b (Class_type OutOfMemory)) = (x1c, x2c); allocate x1c (Class_type ArrayIndexOutOfBounds) \<noteq> {}; (SOME ha. ha \<in> allocate x1c (Class_type ArrayIndexOutOfBounds)) = (x1d, x2d); allocate x1d (Class_type ArrayStore) \<noteq> {}; (SOME ha. ha \<in> allocate x1d (Class_type ArrayStore)) = (x1e, x2e); allocate x1e (Class_type NegativeArraySize) \<noteq> {}; (SOME ha. ha \<in> allocate x1e (Class_type NegativeArraySize)) = (x1f, x2f); allocate x1f (Class_type ArithmeticException) \<noteq> {}; (SOME ha. ha \<in> allocate x1f (Class_type ArithmeticException)) = (x1g, x2g); allocate x1g (Class_type IllegalMonitorState) \<noteq> {}; (SOME ha. ha \<in> allocate x1g (Class_type IllegalMonitorState)) = (x1h, x2h); allocate x1h (Class_type IllegalThreadState) \<noteq> {}; (SOME ha. ha \<in> allocate x1h (Class_type IllegalThreadState)) = (x1i, x2i); allocate x1i (Class_type InterruptedException) \<noteq> {}; (SOME ha. ha \<in> allocate x1i (Class_type InterruptedException)) = (x1j, x2j)\<rbrakk> \<Longrightarrow> P,x1j \<turnstile> addr2thread_id x2 \<surd>t
[PROOF STEP]
apply(erule not_empty_pairE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi aj bj. \<lbrakk>wf_syscls P; (SOME ha. ha \<in> allocate empty_heap (Class_type Thread)) = (x1, x2); (SOME ha. ha \<in> allocate x1 (Class_type NullPointer)) = (x1a, x2a); (SOME ha. ha \<in> allocate x1a (Class_type ClassCast)) = (x1b, x2b); (SOME ha. ha \<in> allocate x1b (Class_type OutOfMemory)) = (x1c, x2c); (SOME ha. ha \<in> allocate x1c (Class_type ArrayIndexOutOfBounds)) = (x1d, x2d); (SOME ha. ha \<in> allocate x1d (Class_type ArrayStore)) = (x1e, x2e); (SOME ha. ha \<in> allocate x1e (Class_type NegativeArraySize)) = (x1f, x2f); (SOME ha. ha \<in> allocate x1f (Class_type ArithmeticException)) = (x1g, x2g); (SOME ha. ha \<in> allocate x1g (Class_type IllegalMonitorState)) = (x1h, x2h); (SOME ha. ha \<in> allocate x1h (Class_type IllegalThreadState)) = (x1i, x2i); (SOME ha. ha \<in> allocate x1i (Class_type InterruptedException)) = (x1j, x2j); (a, b) \<in> allocate empty_heap (Class_type Thread); (aa, ba) \<in> allocate x1 (Class_type NullPointer); (ab, bb) \<in> allocate x1a (Class_type ClassCast); (ac, bc) \<in> allocate x1b (Class_type OutOfMemory); (ad, bd) \<in> allocate x1c (Class_type ArrayIndexOutOfBounds); (ae, be) \<in> allocate x1d (Class_type ArrayStore); (af, bf) \<in> allocate x1e (Class_type NegativeArraySize); (ag, bg) \<in> allocate x1f (Class_type ArithmeticException); (ah, bh) \<in> allocate x1g (Class_type IllegalMonitorState); (ai, bi) \<in> allocate x1h (Class_type IllegalThreadState); (aj, bj) \<in> allocate x1i (Class_type InterruptedException)\<rbrakk> \<Longrightarrow> P,x1j \<turnstile> addr2thread_id x2 \<surd>t
[PROOF STEP]
apply(drule (1) allocate_Eps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi aj bj. \<lbrakk>wf_syscls P; (SOME ha. ha \<in> allocate empty_heap (Class_type Thread)) = (x1, x2); (SOME ha. ha \<in> allocate x1 (Class_type NullPointer)) = (x1a, x2a); (SOME ha. ha \<in> allocate x1a (Class_type ClassCast)) = (x1b, x2b); (SOME ha. ha \<in> allocate x1b (Class_type OutOfMemory)) = (x1c, x2c); (SOME ha. ha \<in> allocate x1c (Class_type ArrayIndexOutOfBounds)) = (x1d, x2d); (SOME ha. ha \<in> allocate x1d (Class_type ArrayStore)) = (x1e, x2e); (SOME ha. ha \<in> allocate x1e (Class_type NegativeArraySize)) = (x1f, x2f); (SOME ha. ha \<in> allocate x1f (Class_type ArithmeticException)) = (x1g, x2g); (SOME ha. ha \<in> allocate x1g (Class_type IllegalMonitorState)) = (x1h, x2h); (SOME ha. ha \<in> allocate x1h (Class_type IllegalThreadState)) = (x1i, x2i); (SOME ha. ha \<in> allocate x1i (Class_type InterruptedException)) = (x1j, x2j); (aa, ba) \<in> allocate x1 (Class_type NullPointer); (ab, bb) \<in> allocate x1a (Class_type ClassCast); (ac, bc) \<in> allocate x1b (Class_type OutOfMemory); (ad, bd) \<in> allocate x1c (Class_type ArrayIndexOutOfBounds); (ae, be) \<in> allocate x1d (Class_type ArrayStore); (af, bf) \<in> allocate x1e (Class_type NegativeArraySize); (ag, bg) \<in> allocate x1f (Class_type ArithmeticException); (ah, bh) \<in> allocate x1g (Class_type IllegalMonitorState); (ai, bi) \<in> allocate x1h (Class_type IllegalThreadState); (aj, bj) \<in> allocate x1i (Class_type InterruptedException); (x1, x2) \<in> allocate empty_heap (Class_type Thread)\<rbrakk> \<Longrightarrow> P,x1j \<turnstile> addr2thread_id x2 \<surd>t
[PROOF STEP]
apply(drule (1) allocate_Eps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi aj bj. \<lbrakk>wf_syscls P; (SOME ha. ha \<in> allocate empty_heap (Class_type Thread)) = (x1, x2); (SOME ha. ha \<in> allocate x1 (Class_type NullPointer)) = (x1a, x2a); (SOME ha. ha \<in> allocate x1a (Class_type ClassCast)) = (x1b, x2b); (SOME ha. ha \<in> allocate x1b (Class_type OutOfMemory)) = (x1c, x2c); (SOME ha. ha \<in> allocate x1c (Class_type ArrayIndexOutOfBounds)) = (x1d, x2d); (SOME ha. ha \<in> allocate x1d (Class_type ArrayStore)) = (x1e, x2e); (SOME ha. ha \<in> allocate x1e (Class_type NegativeArraySize)) = (x1f, x2f); (SOME ha. ha \<in> allocate x1f (Class_type ArithmeticException)) = (x1g, x2g); (SOME ha. ha \<in> allocate x1g (Class_type IllegalMonitorState)) = (x1h, x2h); (SOME ha. ha \<in> allocate x1h (Class_type IllegalThreadState)) = (x1i, x2i); (SOME ha. ha \<in> allocate x1i (Class_type InterruptedException)) = (x1j, x2j); (ab, bb) \<in> allocate x1a (Class_type ClassCast); (ac, bc) \<in> allocate x1b (Class_type OutOfMemory); (ad, bd) \<in> allocate x1c (Class_type ArrayIndexOutOfBounds); (ae, be) \<in> allocate x1d (Class_type ArrayStore); (af, bf) \<in> allocate x1e (Class_type NegativeArraySize); (ag, bg) \<in> allocate x1f (Class_type ArithmeticException); (ah, bh) \<in> allocate x1g (Class_type IllegalMonitorState); (ai, bi) \<in> allocate x1h (Class_type IllegalThreadState); (aj, bj) \<in> allocate x1i (Class_type InterruptedException); (x1, x2) \<in> allocate empty_heap (Class_type Thread); (x1a, x2a) \<in> allocate x1 (Class_type NullPointer)\<rbrakk> \<Longrightarrow> P,x1j \<turnstile> addr2thread_id x2 \<surd>t
[PROOF STEP]
apply(drule (1) allocate_Eps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi aj bj. \<lbrakk>wf_syscls P; (SOME ha. ha \<in> allocate empty_heap (Class_type Thread)) = (x1, x2); (SOME ha. ha \<in> allocate x1 (Class_type NullPointer)) = (x1a, x2a); (SOME ha. ha \<in> allocate x1a (Class_type ClassCast)) = (x1b, x2b); (SOME ha. ha \<in> allocate x1b (Class_type OutOfMemory)) = (x1c, x2c); (SOME ha. ha \<in> allocate x1c (Class_type ArrayIndexOutOfBounds)) = (x1d, x2d); (SOME ha. ha \<in> allocate x1d (Class_type ArrayStore)) = (x1e, x2e); (SOME ha. ha \<in> allocate x1e (Class_type NegativeArraySize)) = (x1f, x2f); (SOME ha. ha \<in> allocate x1f (Class_type ArithmeticException)) = (x1g, x2g); (SOME ha. ha \<in> allocate x1g (Class_type IllegalMonitorState)) = (x1h, x2h); (SOME ha. ha \<in> allocate x1h (Class_type IllegalThreadState)) = (x1i, x2i); (SOME ha. ha \<in> allocate x1i (Class_type InterruptedException)) = (x1j, x2j); (ac, bc) \<in> allocate x1b (Class_type OutOfMemory); (ad, bd) \<in> allocate x1c (Class_type ArrayIndexOutOfBounds); (ae, be) \<in> allocate x1d (Class_type ArrayStore); (af, bf) \<in> allocate x1e (Class_type NegativeArraySize); (ag, bg) \<in> allocate x1f (Class_type ArithmeticException); (ah, bh) \<in> allocate x1g (Class_type IllegalMonitorState); (ai, bi) \<in> allocate x1h (Class_type IllegalThreadState); (aj, bj) \<in> allocate x1i (Class_type InterruptedException); (x1, x2) \<in> allocate empty_heap (Class_type Thread); (x1a, x2a) \<in> allocate x1 (Class_type NullPointer); (x1b, x2b) \<in> allocate x1a (Class_type ClassCast)\<rbrakk> \<Longrightarrow> P,x1j \<turnstile> addr2thread_id x2 \<surd>t
[PROOF STEP]
apply(drule (1) allocate_Eps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi aj bj. \<lbrakk>wf_syscls P; (SOME ha. ha \<in> allocate empty_heap (Class_type Thread)) = (x1, x2); (SOME ha. ha \<in> allocate x1 (Class_type NullPointer)) = (x1a, x2a); (SOME ha. ha \<in> allocate x1a (Class_type ClassCast)) = (x1b, x2b); (SOME ha. ha \<in> allocate x1b (Class_type OutOfMemory)) = (x1c, x2c); (SOME ha. ha \<in> allocate x1c (Class_type ArrayIndexOutOfBounds)) = (x1d, x2d); (SOME ha. ha \<in> allocate x1d (Class_type ArrayStore)) = (x1e, x2e); (SOME ha. ha \<in> allocate x1e (Class_type NegativeArraySize)) = (x1f, x2f); (SOME ha. ha \<in> allocate x1f (Class_type ArithmeticException)) = (x1g, x2g); (SOME ha. ha \<in> allocate x1g (Class_type IllegalMonitorState)) = (x1h, x2h); (SOME ha. ha \<in> allocate x1h (Class_type IllegalThreadState)) = (x1i, x2i); (SOME ha. ha \<in> allocate x1i (Class_type InterruptedException)) = (x1j, x2j); (ad, bd) \<in> allocate x1c (Class_type ArrayIndexOutOfBounds); (ae, be) \<in> allocate x1d (Class_type ArrayStore); (af, bf) \<in> allocate x1e (Class_type NegativeArraySize); (ag, bg) \<in> allocate x1f (Class_type ArithmeticException); (ah, bh) \<in> allocate x1g (Class_type IllegalMonitorState); (ai, bi) \<in> allocate x1h (Class_type IllegalThreadState); (aj, bj) \<in> allocate x1i (Class_type InterruptedException); (x1, x2) \<in> allocate empty_heap (Class_type Thread); (x1a, x2a) \<in> allocate x1 (Class_type NullPointer); (x1b, x2b) \<in> allocate x1a (Class_type ClassCast); (x1c, x2c) \<in> allocate x1b (Class_type OutOfMemory)\<rbrakk> \<Longrightarrow> P,x1j \<turnstile> addr2thread_id x2 \<surd>t
[PROOF STEP]
apply(drule (1) allocate_Eps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi aj bj. \<lbrakk>wf_syscls P; (SOME ha. ha \<in> allocate empty_heap (Class_type Thread)) = (x1, x2); (SOME ha. ha \<in> allocate x1 (Class_type NullPointer)) = (x1a, x2a); (SOME ha. ha \<in> allocate x1a (Class_type ClassCast)) = (x1b, x2b); (SOME ha. ha \<in> allocate x1b (Class_type OutOfMemory)) = (x1c, x2c); (SOME ha. ha \<in> allocate x1c (Class_type ArrayIndexOutOfBounds)) = (x1d, x2d); (SOME ha. ha \<in> allocate x1d (Class_type ArrayStore)) = (x1e, x2e); (SOME ha. ha \<in> allocate x1e (Class_type NegativeArraySize)) = (x1f, x2f); (SOME ha. ha \<in> allocate x1f (Class_type ArithmeticException)) = (x1g, x2g); (SOME ha. ha \<in> allocate x1g (Class_type IllegalMonitorState)) = (x1h, x2h); (SOME ha. ha \<in> allocate x1h (Class_type IllegalThreadState)) = (x1i, x2i); (SOME ha. ha \<in> allocate x1i (Class_type InterruptedException)) = (x1j, x2j); (ae, be) \<in> allocate x1d (Class_type ArrayStore); (af, bf) \<in> allocate x1e (Class_type NegativeArraySize); (ag, bg) \<in> allocate x1f (Class_type ArithmeticException); (ah, bh) \<in> allocate x1g (Class_type IllegalMonitorState); (ai, bi) \<in> allocate x1h (Class_type IllegalThreadState); (aj, bj) \<in> allocate x1i (Class_type InterruptedException); (x1, x2) \<in> allocate empty_heap (Class_type Thread); (x1a, x2a) \<in> allocate x1 (Class_type NullPointer); (x1b, x2b) \<in> allocate x1a (Class_type ClassCast); (x1c, x2c) \<in> allocate x1b (Class_type OutOfMemory); (x1d, x2d) \<in> allocate x1c (Class_type ArrayIndexOutOfBounds)\<rbrakk> \<Longrightarrow> P,x1j \<turnstile> addr2thread_id x2 \<surd>t
[PROOF STEP]
apply(drule (1) allocate_Eps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi aj bj. \<lbrakk>wf_syscls P; (SOME ha. ha \<in> allocate empty_heap (Class_type Thread)) = (x1, x2); (SOME ha. ha \<in> allocate x1 (Class_type NullPointer)) = (x1a, x2a); (SOME ha. ha \<in> allocate x1a (Class_type ClassCast)) = (x1b, x2b); (SOME ha. ha \<in> allocate x1b (Class_type OutOfMemory)) = (x1c, x2c); (SOME ha. ha \<in> allocate x1c (Class_type ArrayIndexOutOfBounds)) = (x1d, x2d); (SOME ha. ha \<in> allocate x1d (Class_type ArrayStore)) = (x1e, x2e); (SOME ha. ha \<in> allocate x1e (Class_type NegativeArraySize)) = (x1f, x2f); (SOME ha. ha \<in> allocate x1f (Class_type ArithmeticException)) = (x1g, x2g); (SOME ha. ha \<in> allocate x1g (Class_type IllegalMonitorState)) = (x1h, x2h); (SOME ha. ha \<in> allocate x1h (Class_type IllegalThreadState)) = (x1i, x2i); (SOME ha. ha \<in> allocate x1i (Class_type InterruptedException)) = (x1j, x2j); (af, bf) \<in> allocate x1e (Class_type NegativeArraySize); (ag, bg) \<in> allocate x1f (Class_type ArithmeticException); (ah, bh) \<in> allocate x1g (Class_type IllegalMonitorState); (ai, bi) \<in> allocate x1h (Class_type IllegalThreadState); (aj, bj) \<in> allocate x1i (Class_type InterruptedException); (x1, x2) \<in> allocate empty_heap (Class_type Thread); (x1a, x2a) \<in> allocate x1 (Class_type NullPointer); (x1b, x2b) \<in> allocate x1a (Class_type ClassCast); (x1c, x2c) \<in> allocate x1b (Class_type OutOfMemory); (x1d, x2d) \<in> allocate x1c (Class_type ArrayIndexOutOfBounds); (x1e, x2e) \<in> allocate x1d (Class_type ArrayStore)\<rbrakk> \<Longrightarrow> P,x1j \<turnstile> addr2thread_id x2 \<surd>t
[PROOF STEP]
apply(drule (1) allocate_Eps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi aj bj. \<lbrakk>wf_syscls P; (SOME ha. ha \<in> allocate empty_heap (Class_type Thread)) = (x1, x2); (SOME ha. ha \<in> allocate x1 (Class_type NullPointer)) = (x1a, x2a); (SOME ha. ha \<in> allocate x1a (Class_type ClassCast)) = (x1b, x2b); (SOME ha. ha \<in> allocate x1b (Class_type OutOfMemory)) = (x1c, x2c); (SOME ha. ha \<in> allocate x1c (Class_type ArrayIndexOutOfBounds)) = (x1d, x2d); (SOME ha. ha \<in> allocate x1d (Class_type ArrayStore)) = (x1e, x2e); (SOME ha. ha \<in> allocate x1e (Class_type NegativeArraySize)) = (x1f, x2f); (SOME ha. ha \<in> allocate x1f (Class_type ArithmeticException)) = (x1g, x2g); (SOME ha. ha \<in> allocate x1g (Class_type IllegalMonitorState)) = (x1h, x2h); (SOME ha. ha \<in> allocate x1h (Class_type IllegalThreadState)) = (x1i, x2i); (SOME ha. ha \<in> allocate x1i (Class_type InterruptedException)) = (x1j, x2j); (ag, bg) \<in> allocate x1f (Class_type ArithmeticException); (ah, bh) \<in> allocate x1g (Class_type IllegalMonitorState); (ai, bi) \<in> allocate x1h (Class_type IllegalThreadState); (aj, bj) \<in> allocate x1i (Class_type InterruptedException); (x1, x2) \<in> allocate empty_heap (Class_type Thread); (x1a, x2a) \<in> allocate x1 (Class_type NullPointer); (x1b, x2b) \<in> allocate x1a (Class_type ClassCast); (x1c, x2c) \<in> allocate x1b (Class_type OutOfMemory); (x1d, x2d) \<in> allocate x1c (Class_type ArrayIndexOutOfBounds); (x1e, x2e) \<in> allocate x1d (Class_type ArrayStore); (x1f, x2f) \<in> allocate x1e (Class_type NegativeArraySize)\<rbrakk> \<Longrightarrow> P,x1j \<turnstile> addr2thread_id x2 \<surd>t
[PROOF STEP]
apply(drule (1) allocate_Eps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi aj bj. \<lbrakk>wf_syscls P; (SOME ha. ha \<in> allocate empty_heap (Class_type Thread)) = (x1, x2); (SOME ha. ha \<in> allocate x1 (Class_type NullPointer)) = (x1a, x2a); (SOME ha. ha \<in> allocate x1a (Class_type ClassCast)) = (x1b, x2b); (SOME ha. ha \<in> allocate x1b (Class_type OutOfMemory)) = (x1c, x2c); (SOME ha. ha \<in> allocate x1c (Class_type ArrayIndexOutOfBounds)) = (x1d, x2d); (SOME ha. ha \<in> allocate x1d (Class_type ArrayStore)) = (x1e, x2e); (SOME ha. ha \<in> allocate x1e (Class_type NegativeArraySize)) = (x1f, x2f); (SOME ha. ha \<in> allocate x1f (Class_type ArithmeticException)) = (x1g, x2g); (SOME ha. ha \<in> allocate x1g (Class_type IllegalMonitorState)) = (x1h, x2h); (SOME ha. ha \<in> allocate x1h (Class_type IllegalThreadState)) = (x1i, x2i); (SOME ha. ha \<in> allocate x1i (Class_type InterruptedException)) = (x1j, x2j); (ah, bh) \<in> allocate x1g (Class_type IllegalMonitorState); (ai, bi) \<in> allocate x1h (Class_type IllegalThreadState); (aj, bj) \<in> allocate x1i (Class_type InterruptedException); (x1, x2) \<in> allocate empty_heap (Class_type Thread); (x1a, x2a) \<in> allocate x1 (Class_type NullPointer); (x1b, x2b) \<in> allocate x1a (Class_type ClassCast); (x1c, x2c) \<in> allocate x1b (Class_type OutOfMemory); (x1d, x2d) \<in> allocate x1c (Class_type ArrayIndexOutOfBounds); (x1e, x2e) \<in> allocate x1d (Class_type ArrayStore); (x1f, x2f) \<in> allocate x1e (Class_type NegativeArraySize); (x1g, x2g) \<in> allocate x1f (Class_type ArithmeticException)\<rbrakk> \<Longrightarrow> P,x1j \<turnstile> addr2thread_id x2 \<surd>t
[PROOF STEP]
apply(drule (1) allocate_Eps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi aj bj. \<lbrakk>wf_syscls P; (SOME ha. ha \<in> allocate empty_heap (Class_type Thread)) = (x1, x2); (SOME ha. ha \<in> allocate x1 (Class_type NullPointer)) = (x1a, x2a); (SOME ha. ha \<in> allocate x1a (Class_type ClassCast)) = (x1b, x2b); (SOME ha. ha \<in> allocate x1b (Class_type OutOfMemory)) = (x1c, x2c); (SOME ha. ha \<in> allocate x1c (Class_type ArrayIndexOutOfBounds)) = (x1d, x2d); (SOME ha. ha \<in> allocate x1d (Class_type ArrayStore)) = (x1e, x2e); (SOME ha. ha \<in> allocate x1e (Class_type NegativeArraySize)) = (x1f, x2f); (SOME ha. ha \<in> allocate x1f (Class_type ArithmeticException)) = (x1g, x2g); (SOME ha. ha \<in> allocate x1g (Class_type IllegalMonitorState)) = (x1h, x2h); (SOME ha. ha \<in> allocate x1h (Class_type IllegalThreadState)) = (x1i, x2i); (SOME ha. ha \<in> allocate x1i (Class_type InterruptedException)) = (x1j, x2j); (ai, bi) \<in> allocate x1h (Class_type IllegalThreadState); (aj, bj) \<in> allocate x1i (Class_type InterruptedException); (x1, x2) \<in> allocate empty_heap (Class_type Thread); (x1a, x2a) \<in> allocate x1 (Class_type NullPointer); (x1b, x2b) \<in> allocate x1a (Class_type ClassCast); (x1c, x2c) \<in> allocate x1b (Class_type OutOfMemory); (x1d, x2d) \<in> allocate x1c (Class_type ArrayIndexOutOfBounds); (x1e, x2e) \<in> allocate x1d (Class_type ArrayStore); (x1f, x2f) \<in> allocate x1e (Class_type NegativeArraySize); (x1g, x2g) \<in> allocate x1f (Class_type ArithmeticException); (x1h, x2h) \<in> allocate x1g (Class_type IllegalMonitorState)\<rbrakk> \<Longrightarrow> P,x1j \<turnstile> addr2thread_id x2 \<surd>t
[PROOF STEP]
apply(drule (1) allocate_Eps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi aj bj. \<lbrakk>wf_syscls P; (SOME ha. ha \<in> allocate empty_heap (Class_type Thread)) = (x1, x2); (SOME ha. ha \<in> allocate x1 (Class_type NullPointer)) = (x1a, x2a); (SOME ha. ha \<in> allocate x1a (Class_type ClassCast)) = (x1b, x2b); (SOME ha. ha \<in> allocate x1b (Class_type OutOfMemory)) = (x1c, x2c); (SOME ha. ha \<in> allocate x1c (Class_type ArrayIndexOutOfBounds)) = (x1d, x2d); (SOME ha. ha \<in> allocate x1d (Class_type ArrayStore)) = (x1e, x2e); (SOME ha. ha \<in> allocate x1e (Class_type NegativeArraySize)) = (x1f, x2f); (SOME ha. ha \<in> allocate x1f (Class_type ArithmeticException)) = (x1g, x2g); (SOME ha. ha \<in> allocate x1g (Class_type IllegalMonitorState)) = (x1h, x2h); (SOME ha. ha \<in> allocate x1h (Class_type IllegalThreadState)) = (x1i, x2i); (SOME ha. ha \<in> allocate x1i (Class_type InterruptedException)) = (x1j, x2j); (aj, bj) \<in> allocate x1i (Class_type InterruptedException); (x1, x2) \<in> allocate empty_heap (Class_type Thread); (x1a, x2a) \<in> allocate x1 (Class_type NullPointer); (x1b, x2b) \<in> allocate x1a (Class_type ClassCast); (x1c, x2c) \<in> allocate x1b (Class_type OutOfMemory); (x1d, x2d) \<in> allocate x1c (Class_type ArrayIndexOutOfBounds); (x1e, x2e) \<in> allocate x1d (Class_type ArrayStore); (x1f, x2f) \<in> allocate x1e (Class_type NegativeArraySize); (x1g, x2g) \<in> allocate x1f (Class_type ArithmeticException); (x1h, x2h) \<in> allocate x1g (Class_type IllegalMonitorState); (x1i, x2i) \<in> allocate x1h (Class_type IllegalThreadState)\<rbrakk> \<Longrightarrow> P,x1j \<turnstile> addr2thread_id x2 \<surd>t
[PROOF STEP]
apply(drule (1) allocate_Eps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi aj bj. \<lbrakk>wf_syscls P; (SOME ha. ha \<in> allocate empty_heap (Class_type Thread)) = (x1, x2); (SOME ha. ha \<in> allocate x1 (Class_type NullPointer)) = (x1a, x2a); (SOME ha. ha \<in> allocate x1a (Class_type ClassCast)) = (x1b, x2b); (SOME ha. ha \<in> allocate x1b (Class_type OutOfMemory)) = (x1c, x2c); (SOME ha. ha \<in> allocate x1c (Class_type ArrayIndexOutOfBounds)) = (x1d, x2d); (SOME ha. ha \<in> allocate x1d (Class_type ArrayStore)) = (x1e, x2e); (SOME ha. ha \<in> allocate x1e (Class_type NegativeArraySize)) = (x1f, x2f); (SOME ha. ha \<in> allocate x1f (Class_type ArithmeticException)) = (x1g, x2g); (SOME ha. ha \<in> allocate x1g (Class_type IllegalMonitorState)) = (x1h, x2h); (SOME ha. ha \<in> allocate x1h (Class_type IllegalThreadState)) = (x1i, x2i); (SOME ha. ha \<in> allocate x1i (Class_type InterruptedException)) = (x1j, x2j); (x1, x2) \<in> allocate empty_heap (Class_type Thread); (x1a, x2a) \<in> allocate x1 (Class_type NullPointer); (x1b, x2b) \<in> allocate x1a (Class_type ClassCast); (x1c, x2c) \<in> allocate x1b (Class_type OutOfMemory); (x1d, x2d) \<in> allocate x1c (Class_type ArrayIndexOutOfBounds); (x1e, x2e) \<in> allocate x1d (Class_type ArrayStore); (x1f, x2f) \<in> allocate x1e (Class_type NegativeArraySize); (x1g, x2g) \<in> allocate x1f (Class_type ArithmeticException); (x1h, x2h) \<in> allocate x1g (Class_type IllegalMonitorState); (x1i, x2i) \<in> allocate x1h (Class_type IllegalThreadState); (x1j, x2j) \<in> allocate x1i (Class_type InterruptedException)\<rbrakk> \<Longrightarrow> P,x1j \<turnstile> addr2thread_id x2 \<surd>t
[PROOF STEP]
apply(drule allocate_SomeD[where hT="Class_type Thread"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi aj bj. \<lbrakk>wf_syscls P; (SOME ha. ha \<in> allocate empty_heap (Class_type Thread)) = (x1, x2); (SOME ha. ha \<in> allocate x1 (Class_type NullPointer)) = (x1a, x2a); (SOME ha. ha \<in> allocate x1a (Class_type ClassCast)) = (x1b, x2b); (SOME ha. ha \<in> allocate x1b (Class_type OutOfMemory)) = (x1c, x2c); (SOME ha. ha \<in> allocate x1c (Class_type ArrayIndexOutOfBounds)) = (x1d, x2d); (SOME ha. ha \<in> allocate x1d (Class_type ArrayStore)) = (x1e, x2e); (SOME ha. ha \<in> allocate x1e (Class_type NegativeArraySize)) = (x1f, x2f); (SOME ha. ha \<in> allocate x1f (Class_type ArithmeticException)) = (x1g, x2g); (SOME ha. ha \<in> allocate x1g (Class_type IllegalMonitorState)) = (x1h, x2h); (SOME ha. ha \<in> allocate x1h (Class_type IllegalThreadState)) = (x1i, x2i); (SOME ha. ha \<in> allocate x1i (Class_type InterruptedException)) = (x1j, x2j); (x1a, x2a) \<in> allocate x1 (Class_type NullPointer); (x1b, x2b) \<in> allocate x1a (Class_type ClassCast); (x1c, x2c) \<in> allocate x1b (Class_type OutOfMemory); (x1d, x2d) \<in> allocate x1c (Class_type ArrayIndexOutOfBounds); (x1e, x2e) \<in> allocate x1d (Class_type ArrayStore); (x1f, x2f) \<in> allocate x1e (Class_type NegativeArraySize); (x1g, x2g) \<in> allocate x1f (Class_type ArithmeticException); (x1h, x2h) \<in> allocate x1g (Class_type IllegalMonitorState); (x1i, x2i) \<in> allocate x1h (Class_type IllegalThreadState); (x1j, x2j) \<in> allocate x1i (Class_type InterruptedException)\<rbrakk> \<Longrightarrow> is_htype P (Class_type Thread)
 2. \<And>x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi aj bj. \<lbrakk>wf_syscls P; (SOME ha. ha \<in> allocate empty_heap (Class_type Thread)) = (x1, x2); (SOME ha. ha \<in> allocate x1 (Class_type NullPointer)) = (x1a, x2a); (SOME ha. ha \<in> allocate x1a (Class_type ClassCast)) = (x1b, x2b); (SOME ha. ha \<in> allocate x1b (Class_type OutOfMemory)) = (x1c, x2c); (SOME ha. ha \<in> allocate x1c (Class_type ArrayIndexOutOfBounds)) = (x1d, x2d); (SOME ha. ha \<in> allocate x1d (Class_type ArrayStore)) = (x1e, x2e); (SOME ha. ha \<in> allocate x1e (Class_type NegativeArraySize)) = (x1f, x2f); (SOME ha. ha \<in> allocate x1f (Class_type ArithmeticException)) = (x1g, x2g); (SOME ha. ha \<in> allocate x1g (Class_type IllegalMonitorState)) = (x1h, x2h); (SOME ha. ha \<in> allocate x1h (Class_type IllegalThreadState)) = (x1i, x2i); (SOME ha. ha \<in> allocate x1i (Class_type InterruptedException)) = (x1j, x2j); (x1a, x2a) \<in> allocate x1 (Class_type NullPointer); (x1b, x2b) \<in> allocate x1a (Class_type ClassCast); (x1c, x2c) \<in> allocate x1b (Class_type OutOfMemory); (x1d, x2d) \<in> allocate x1c (Class_type ArrayIndexOutOfBounds); (x1e, x2e) \<in> allocate x1d (Class_type ArrayStore); (x1f, x2f) \<in> allocate x1e (Class_type NegativeArraySize); (x1g, x2g) \<in> allocate x1f (Class_type ArithmeticException); (x1h, x2h) \<in> allocate x1g (Class_type IllegalMonitorState); (x1i, x2i) \<in> allocate x1h (Class_type IllegalThreadState); (x1j, x2j) \<in> allocate x1i (Class_type InterruptedException); typeof_addr x1 x2 = \<lfloor>Class_type Thread\<rfloor>\<rbrakk> \<Longrightarrow> P,x1j \<turnstile> addr2thread_id x2 \<surd>t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi aj bj. \<lbrakk>wf_syscls P; (SOME ha. ha \<in> allocate empty_heap (Class_type Thread)) = (x1, x2); (SOME ha. ha \<in> allocate x1 (Class_type NullPointer)) = (x1a, x2a); (SOME ha. ha \<in> allocate x1a (Class_type ClassCast)) = (x1b, x2b); (SOME ha. ha \<in> allocate x1b (Class_type OutOfMemory)) = (x1c, x2c); (SOME ha. ha \<in> allocate x1c (Class_type ArrayIndexOutOfBounds)) = (x1d, x2d); (SOME ha. ha \<in> allocate x1d (Class_type ArrayStore)) = (x1e, x2e); (SOME ha. ha \<in> allocate x1e (Class_type NegativeArraySize)) = (x1f, x2f); (SOME ha. ha \<in> allocate x1f (Class_type ArithmeticException)) = (x1g, x2g); (SOME ha. ha \<in> allocate x1g (Class_type IllegalMonitorState)) = (x1h, x2h); (SOME ha. ha \<in> allocate x1h (Class_type IllegalThreadState)) = (x1i, x2i); (SOME ha. ha \<in> allocate x1i (Class_type InterruptedException)) = (x1j, x2j); (x1a, x2a) \<in> allocate x1 (Class_type NullPointer); (x1b, x2b) \<in> allocate x1a (Class_type ClassCast); (x1c, x2c) \<in> allocate x1b (Class_type OutOfMemory); (x1d, x2d) \<in> allocate x1c (Class_type ArrayIndexOutOfBounds); (x1e, x2e) \<in> allocate x1d (Class_type ArrayStore); (x1f, x2f) \<in> allocate x1e (Class_type NegativeArraySize); (x1g, x2g) \<in> allocate x1f (Class_type ArithmeticException); (x1h, x2h) \<in> allocate x1g (Class_type IllegalMonitorState); (x1i, x2i) \<in> allocate x1h (Class_type IllegalThreadState); (x1j, x2j) \<in> allocate x1i (Class_type InterruptedException); typeof_addr x1 x2 = \<lfloor>Class_type Thread\<rfloor>\<rbrakk> \<Longrightarrow> P,x1j \<turnstile> addr2thread_id x2 \<surd>t
[PROOF STEP]
apply(rule tconfI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi aj bj. \<lbrakk>wf_syscls P; (SOME ha. ha \<in> allocate empty_heap (Class_type Thread)) = (x1, x2); (SOME ha. ha \<in> allocate x1 (Class_type NullPointer)) = (x1a, x2a); (SOME ha. ha \<in> allocate x1a (Class_type ClassCast)) = (x1b, x2b); (SOME ha. ha \<in> allocate x1b (Class_type OutOfMemory)) = (x1c, x2c); (SOME ha. ha \<in> allocate x1c (Class_type ArrayIndexOutOfBounds)) = (x1d, x2d); (SOME ha. ha \<in> allocate x1d (Class_type ArrayStore)) = (x1e, x2e); (SOME ha. ha \<in> allocate x1e (Class_type NegativeArraySize)) = (x1f, x2f); (SOME ha. ha \<in> allocate x1f (Class_type ArithmeticException)) = (x1g, x2g); (SOME ha. ha \<in> allocate x1g (Class_type IllegalMonitorState)) = (x1h, x2h); (SOME ha. ha \<in> allocate x1h (Class_type IllegalThreadState)) = (x1i, x2i); (SOME ha. ha \<in> allocate x1i (Class_type InterruptedException)) = (x1j, x2j); (x1a, x2a) \<in> allocate x1 (Class_type NullPointer); (x1b, x2b) \<in> allocate x1a (Class_type ClassCast); (x1c, x2c) \<in> allocate x1b (Class_type OutOfMemory); (x1d, x2d) \<in> allocate x1c (Class_type ArrayIndexOutOfBounds); (x1e, x2e) \<in> allocate x1d (Class_type ArrayStore); (x1f, x2f) \<in> allocate x1e (Class_type NegativeArraySize); (x1g, x2g) \<in> allocate x1f (Class_type ArithmeticException); (x1h, x2h) \<in> allocate x1g (Class_type IllegalMonitorState); (x1i, x2i) \<in> allocate x1h (Class_type IllegalThreadState); (x1j, x2j) \<in> allocate x1i (Class_type InterruptedException); typeof_addr x1 x2 = \<lfloor>Class_type Thread\<rfloor>\<rbrakk> \<Longrightarrow> typeof_addr x1j (thread_id2addr (addr2thread_id x2)) = \<lfloor>Class_type (?C333 x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi aj bj)\<rfloor>
 2. \<And>x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi aj bj. \<lbrakk>wf_syscls P; (SOME ha. ha \<in> allocate empty_heap (Class_type Thread)) = (x1, x2); (SOME ha. ha \<in> allocate x1 (Class_type NullPointer)) = (x1a, x2a); (SOME ha. ha \<in> allocate x1a (Class_type ClassCast)) = (x1b, x2b); (SOME ha. ha \<in> allocate x1b (Class_type OutOfMemory)) = (x1c, x2c); (SOME ha. ha \<in> allocate x1c (Class_type ArrayIndexOutOfBounds)) = (x1d, x2d); (SOME ha. ha \<in> allocate x1d (Class_type ArrayStore)) = (x1e, x2e); (SOME ha. ha \<in> allocate x1e (Class_type NegativeArraySize)) = (x1f, x2f); (SOME ha. ha \<in> allocate x1f (Class_type ArithmeticException)) = (x1g, x2g); (SOME ha. ha \<in> allocate x1g (Class_type IllegalMonitorState)) = (x1h, x2h); (SOME ha. ha \<in> allocate x1h (Class_type IllegalThreadState)) = (x1i, x2i); (SOME ha. ha \<in> allocate x1i (Class_type InterruptedException)) = (x1j, x2j); (x1a, x2a) \<in> allocate x1 (Class_type NullPointer); (x1b, x2b) \<in> allocate x1a (Class_type ClassCast); (x1c, x2c) \<in> allocate x1b (Class_type OutOfMemory); (x1d, x2d) \<in> allocate x1c (Class_type ArrayIndexOutOfBounds); (x1e, x2e) \<in> allocate x1d (Class_type ArrayStore); (x1f, x2f) \<in> allocate x1e (Class_type NegativeArraySize); (x1g, x2g) \<in> allocate x1f (Class_type ArithmeticException); (x1h, x2h) \<in> allocate x1g (Class_type IllegalMonitorState); (x1i, x2i) \<in> allocate x1h (Class_type IllegalThreadState); (x1j, x2j) \<in> allocate x1i (Class_type InterruptedException); typeof_addr x1 x2 = \<lfloor>Class_type Thread\<rfloor>\<rbrakk> \<Longrightarrow> P \<turnstile> ?C333 x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi aj bj \<preceq>\<^sup>* Thread
[PROOF STEP]
apply(erule typeof_addr_hext_mono[OF hext_allocate])+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi aj bj. \<lbrakk>wf_syscls P; (SOME ha. ha \<in> allocate empty_heap (Class_type Thread)) = (x1, x2); (SOME ha. ha \<in> allocate x1 (Class_type NullPointer)) = (x1a, x2a); (SOME ha. ha \<in> allocate x1a (Class_type ClassCast)) = (x1b, x2b); (SOME ha. ha \<in> allocate x1b (Class_type OutOfMemory)) = (x1c, x2c); (SOME ha. ha \<in> allocate x1c (Class_type ArrayIndexOutOfBounds)) = (x1d, x2d); (SOME ha. ha \<in> allocate x1d (Class_type ArrayStore)) = (x1e, x2e); (SOME ha. ha \<in> allocate x1e (Class_type NegativeArraySize)) = (x1f, x2f); (SOME ha. ha \<in> allocate x1f (Class_type ArithmeticException)) = (x1g, x2g); (SOME ha. ha \<in> allocate x1g (Class_type IllegalMonitorState)) = (x1h, x2h); (SOME ha. ha \<in> allocate x1h (Class_type IllegalThreadState)) = (x1i, x2i); (SOME ha. ha \<in> allocate x1i (Class_type InterruptedException)) = (x1j, x2j); typeof_addr x1 x2 = \<lfloor>Class_type Thread\<rfloor>\<rbrakk> \<Longrightarrow> typeof_addr x1 (thread_id2addr (addr2thread_id x2)) = \<lfloor>Class_type (?C333 x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi aj bj)\<rfloor>
 2. \<And>x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi aj bj. \<lbrakk>wf_syscls P; (SOME ha. ha \<in> allocate empty_heap (Class_type Thread)) = (x1, x2); (SOME ha. ha \<in> allocate x1 (Class_type NullPointer)) = (x1a, x2a); (SOME ha. ha \<in> allocate x1a (Class_type ClassCast)) = (x1b, x2b); (SOME ha. ha \<in> allocate x1b (Class_type OutOfMemory)) = (x1c, x2c); (SOME ha. ha \<in> allocate x1c (Class_type ArrayIndexOutOfBounds)) = (x1d, x2d); (SOME ha. ha \<in> allocate x1d (Class_type ArrayStore)) = (x1e, x2e); (SOME ha. ha \<in> allocate x1e (Class_type NegativeArraySize)) = (x1f, x2f); (SOME ha. ha \<in> allocate x1f (Class_type ArithmeticException)) = (x1g, x2g); (SOME ha. ha \<in> allocate x1g (Class_type IllegalMonitorState)) = (x1h, x2h); (SOME ha. ha \<in> allocate x1h (Class_type IllegalThreadState)) = (x1i, x2i); (SOME ha. ha \<in> allocate x1i (Class_type InterruptedException)) = (x1j, x2j); (x1a, x2a) \<in> allocate x1 (Class_type NullPointer); (x1b, x2b) \<in> allocate x1a (Class_type ClassCast); (x1c, x2c) \<in> allocate x1b (Class_type OutOfMemory); (x1d, x2d) \<in> allocate x1c (Class_type ArrayIndexOutOfBounds); (x1e, x2e) \<in> allocate x1d (Class_type ArrayStore); (x1f, x2f) \<in> allocate x1e (Class_type NegativeArraySize); (x1g, x2g) \<in> allocate x1f (Class_type ArithmeticException); (x1h, x2h) \<in> allocate x1g (Class_type IllegalMonitorState); (x1i, x2i) \<in> allocate x1h (Class_type IllegalThreadState); (x1j, x2j) \<in> allocate x1i (Class_type InterruptedException); typeof_addr x1 x2 = \<lfloor>Class_type Thread\<rfloor>\<rbrakk> \<Longrightarrow> P \<turnstile> ?C333 x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi aj bj \<preceq>\<^sup>* Thread
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi aj bj. \<lbrakk>wf_syscls P; (SOME ha. ha \<in> allocate empty_heap (Class_type Thread)) = (x1, x2); (SOME ha. ha \<in> allocate x1 (Class_type NullPointer)) = (x1a, x2a); (SOME ha. ha \<in> allocate x1a (Class_type ClassCast)) = (x1b, x2b); (SOME ha. ha \<in> allocate x1b (Class_type OutOfMemory)) = (x1c, x2c); (SOME ha. ha \<in> allocate x1c (Class_type ArrayIndexOutOfBounds)) = (x1d, x2d); (SOME ha. ha \<in> allocate x1d (Class_type ArrayStore)) = (x1e, x2e); (SOME ha. ha \<in> allocate x1e (Class_type NegativeArraySize)) = (x1f, x2f); (SOME ha. ha \<in> allocate x1f (Class_type ArithmeticException)) = (x1g, x2g); (SOME ha. ha \<in> allocate x1g (Class_type IllegalMonitorState)) = (x1h, x2h); (SOME ha. ha \<in> allocate x1h (Class_type IllegalThreadState)) = (x1i, x2i); (SOME ha. ha \<in> allocate x1i (Class_type InterruptedException)) = (x1j, x2j); (x1a, x2a) \<in> allocate x1 (Class_type NullPointer); (x1b, x2b) \<in> allocate x1a (Class_type ClassCast); (x1c, x2c) \<in> allocate x1b (Class_type OutOfMemory); (x1d, x2d) \<in> allocate x1c (Class_type ArrayIndexOutOfBounds); (x1e, x2e) \<in> allocate x1d (Class_type ArrayStore); (x1f, x2f) \<in> allocate x1e (Class_type NegativeArraySize); (x1g, x2g) \<in> allocate x1f (Class_type ArithmeticException); (x1h, x2h) \<in> allocate x1g (Class_type IllegalMonitorState); (x1i, x2i) \<in> allocate x1h (Class_type IllegalThreadState); (x1j, x2j) \<in> allocate x1i (Class_type InterruptedException); typeof_addr x1 x2 = \<lfloor>Class_type Thread\<rfloor>\<rbrakk> \<Longrightarrow> P \<turnstile> Thread \<preceq>\<^sup>* Thread
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma start_heap_write_typeable:
  assumes "WriteMem ad al v \<in> set start_heap_obs"
  shows "\<exists>T. P,start_heap \<turnstile> ad@al : T \<and> P,start_heap \<turnstile> v :\<le> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>T. P,start_heap \<turnstile> ad@al : T \<and> P,start_heap \<turnstile> v :\<le> T
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
WriteMem ad al v \<in> set start_heap_obs

goal (1 subgoal):
 1. \<exists>T. P,start_heap \<turnstile> ad@al : T \<and> P,start_heap \<turnstile> v :\<le> T
[PROOF STEP]
unfolding start_heap_obs_def start_heap_def
[PROOF STATE]
proof (prove)
using this:
WriteMem ad al v \<in> set (map2 (\<lambda>C a. NewHeapElem a (Class_type C)) initialization_list (fst (snd start_heap_data)))

goal (1 subgoal):
 1. \<exists>T. P,fst start_heap_data \<turnstile> ad@al : T \<and> P,fst start_heap_data \<turnstile> v :\<le> T
[PROOF STEP]
by clarsimp


[STATEMENT]
lemma subadditiveI:
  assumes "\<And>m n. u (m+n) \<le> u m + u n"
  shows "subadditive u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subadditive u
[PROOF STEP]
unfolding subadditive_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m n. u (m + n) \<le> u m + u n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u (?m + ?n) \<le> u ?m + u ?n

goal (1 subgoal):
 1. \<forall>m n. u (m + n) \<le> u m + u n
[PROOF STEP]
by auto


[STATEMENT]
lemma subadditiveD:
  assumes "subadditive u"
  shows "u (m+n) \<le> u m + u n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u (m + n) \<le> u m + u n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
subadditive u

goal (1 subgoal):
 1. u (m + n) \<le> u m + u n
[PROOF STEP]
unfolding subadditive_def
[PROOF STATE]
proof (prove)
using this:
\<forall>m n. u (m + n) \<le> u m + u n

goal (1 subgoal):
 1. u (m + n) \<le> u m + u n
[PROOF STEP]
by auto


[STATEMENT]
lemma subadditive_un_le_nu1:
  assumes "subadditive u"
          "n > 0"
  shows "u n \<le> n * u 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u n \<le> real n * u 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u n \<le> real n * u 1
[PROOF STEP]
have *: "n = 0 \<or> (u n \<le> n * u 1)" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = 0 \<or> u n \<le> real n * u 1
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 = 0 \<or> u 0 \<le> real 0 * u 1
 2. \<And>n. n = 0 \<or> u n \<le> real n * u 1 \<Longrightarrow> Suc n = 0 \<or> u (Suc n) \<le> real (Suc n) * u 1
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. 0 = 0 \<or> u 0 \<le> real 0 * u 1
 2. \<And>n. n = 0 \<or> u n \<le> real n * u 1 \<Longrightarrow> Suc n = 0 \<or> u (Suc n) \<le> real (Suc n) * u 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = 0 \<or> u 0 \<le> real 0 * u 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 = 0 \<or> u 0 \<le> real 0 * u 1

goal (1 subgoal):
 1. \<And>n. n = 0 \<or> u n \<le> real n * u 1 \<Longrightarrow> Suc n = 0 \<or> u (Suc n) \<le> real (Suc n) * u 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. n = 0 \<or> u n \<le> real n * u 1 \<Longrightarrow> Suc n = 0 \<or> u (Suc n) \<le> real (Suc n) * u 1
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
n = 0 \<or> u n \<le> real n * u 1

goal (1 subgoal):
 1. \<And>n. n = 0 \<or> u n \<le> real n * u 1 \<Longrightarrow> Suc n = 0 \<or> u (Suc n) \<le> real (Suc n) * u 1
[PROOF STEP]
consider "n = 0" | "n > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = 0 \<Longrightarrow> thesis; 0 < n \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>n = 0 \<Longrightarrow> ?thesis; 0 < n \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>n. n = 0 \<or> u n \<le> real n * u 1 \<Longrightarrow> Suc n = 0 \<or> u (Suc n) \<le> real (Suc n) * u 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>n = 0 \<Longrightarrow> ?thesis; 0 < n \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n = 0 \<Longrightarrow> ?thesis; 0 < n \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. Suc n = 0 \<or> u (Suc n) \<le> real (Suc n) * u 1
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> Suc n = 0 \<or> u (Suc n) \<le> real (Suc n) * u 1
 2. 0 < n \<Longrightarrow> Suc n = 0 \<or> u (Suc n) \<le> real (Suc n) * u 1
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> Suc n = 0 \<or> u (Suc n) \<le> real (Suc n) * u 1
 2. 0 < n \<Longrightarrow> Suc n = 0 \<or> u (Suc n) \<le> real (Suc n) * u 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 0

goal (1 subgoal):
 1. Suc n = 0 \<or> u (Suc n) \<le> real (Suc n) * u 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc n = 0 \<or> u (Suc n) \<le> real (Suc n) * u 1

goal (1 subgoal):
 1. 0 < n \<Longrightarrow> Suc n = 0 \<or> u (Suc n) \<le> real (Suc n) * u 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> Suc n = 0 \<or> u (Suc n) \<le> real (Suc n) * u 1
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
0 < n

goal (1 subgoal):
 1. 0 < n \<Longrightarrow> Suc n = 0 \<or> u (Suc n) \<le> real (Suc n) * u 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < n
[PROOF STEP]
have "u (Suc n) \<le> u n + u 1"
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. u (Suc n) \<le> u n + u 1
[PROOF STEP]
using subadditiveD[OF assms(1), of n 1]
[PROOF STATE]
proof (prove)
using this:
0 < n
u (n + 1) \<le> u n + u 1

goal (1 subgoal):
 1. u (Suc n) \<le> u n + u 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u (Suc n) \<le> u n + u 1

goal (1 subgoal):
 1. 0 < n \<Longrightarrow> Suc n = 0 \<or> u (Suc n) \<le> real (Suc n) * u 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u (Suc n) \<le> u n + u 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u (Suc n) \<le> u n + u 1

goal (1 subgoal):
 1. Suc n = 0 \<or> u (Suc n) \<le> real (Suc n) * u 1
[PROOF STEP]
using Suc.IH 2
[PROOF STATE]
proof (prove)
using this:
u (Suc n) \<le> u n + u 1
n = 0 \<or> u n \<le> real n * u 1
0 < n

goal (1 subgoal):
 1. Suc n = 0 \<or> u (Suc n) \<le> real (Suc n) * u 1
[PROOF STEP]
by (auto simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
Suc n = 0 \<or> u (Suc n) \<le> real (Suc n) * u 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Suc n = 0 \<or> u (Suc n) \<le> real (Suc n) * u 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?n = 0 \<or> u ?n \<le> real ?n * u 1

goal (1 subgoal):
 1. u n \<le> real n * u 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u n \<le> real n * u 1
[PROOF STEP]
using *[of n] \<open>n > 0\<close>
[PROOF STATE]
proof (prove)
using this:
n = 0 \<or> u n \<le> real n * u 1
0 < n

goal (1 subgoal):
 1. u n \<le> real n * u 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u n \<le> real n * u 1

goal:
No subgoals!
[PROOF STEP]
qed