Theory TypeComp

(*  Title:      JinjaThreads/Compiler/TypeComp.thy
    Author:     Tobias Nipkow, Andreas Lochbihler
*)

section ‹Preservation of Well-Typedness in Stage 2›

theory TypeComp
imports 
  Exception_Tables
  J1WellForm
  "../BV/BVSpec"
  "HOL-Library.Prefix_Order"
  "HOL-Library.Sublist"
begin

(*<*)
declare nth_append[simp]
(*>*)

locale TC0 =
  fixes P :: "'addr J1_prog" and mxl :: nat
begin

definition ty :: "ty list ⇒ 'addr expr1 ⇒ ty"
where "ty E e ≡ THE T. P,E ⊢1 e :: T"

definition ty⇩_l :: "ty list ⇒ nat set ⇒ ty⇩_l"
where "ty⇩_l E A' ≡ map (λi. if i ∈ A' ∧ i < size E then OK(E!i) else Err) [0..<mxl]"

definition ty⇩_i' :: "ty list ⇒ ty list ⇒ nat set option ⇒ ty⇩_i'"
where "ty⇩_i' ST E A ≡ case A of None ⇒ None | ⌊A'⌋ ⇒ Some(ST, ty⇩_l E A')"

definition after :: "ty list ⇒ nat set option ⇒ ty list ⇒ 'addr expr1 ⇒ ty⇩_i'"
  where "after E A ST e ≡ ty⇩_i' (ty E e # ST) E (A ⊔ 𝒜 e)"

end

locale TC1 = TC0 +
  fixes wfmd
  assumes wf_prog: "wf_prog wfmd P"
begin

lemma ty_def2 [simp]: "P,E ⊢1 e :: T ⟹ ty E e = T"
apply(unfold ty_def ty_def)
apply(blast intro: the_equality WT1_unique[OF wf_prog])
done

end

context TC0 begin

lemma ty⇩_i'_None [simp]: "ty⇩_i' ST E None = None"
by(simp add:ty⇩_i'_def)

lemma ty⇩_l_app_diff[simp]:
 "ty⇩_l (E@[T]) (A - {size E}) = ty⇩_l E A"
by(auto simp add:ty⇩_l_def hyperset_defs)

lemma ty⇩_i'_app_diff[simp]:
 "ty⇩_i' ST (E @ [T]) (A ⊖ size E) = ty⇩_i' ST E A"
by(auto simp add:ty⇩_i'_def hyperset_defs)

lemma ty⇩_l_antimono:
 "A ⊆ A' ⟹ P ⊢ ty⇩_l E A' [≤⇩_⊤] ty⇩_l E A"
by(auto simp:ty⇩_l_def list_all2_conv_all_nth)


lemma ty⇩_i'_antimono:
 "A ⊆ A' ⟹ P ⊢ ty⇩_i' ST E ⌊A'⌋ ≤' ty⇩_i' ST E ⌊A⌋"
by(auto simp:ty⇩_i'_def ty⇩_l_def list_all2_conv_all_nth)

lemma ty⇩_l_env_antimono:
 "P ⊢ ty⇩_l (E@[T]) A [≤⇩_⊤] ty⇩_l E A" 
by(auto simp:ty⇩_l_def list_all2_conv_all_nth)


lemma ty⇩_i'_env_antimono:
 "P ⊢ ty⇩_i' ST (E@[T]) A ≤' ty⇩_i' ST E A" 
by(auto simp:ty⇩_i'_def ty⇩_l_def list_all2_conv_all_nth)


lemma ty⇩_i'_incr:
 "P ⊢ ty⇩_i' ST (E @ [T]) ⌊insert (size E) A⌋ ≤' ty⇩_i' ST E ⌊A⌋"
by(auto simp:ty⇩_i'_def ty⇩_l_def list_all2_conv_all_nth)


lemma ty⇩_l_incr:
 "P ⊢ ty⇩_l (E @ [T]) (insert (size E) A) [≤⇩_⊤] ty⇩_l E A"
by(auto simp: hyperset_defs ty⇩_l_def list_all2_conv_all_nth)


lemma ty⇩_l_in_types:
 "set E ⊆ types P ⟹ ty⇩_l E A ∈ list mxl (err (types P))"
by(auto simp add:ty⇩_l_def intro!:listI dest!: nth_mem)


function compT :: "ty list ⇒ nat hyperset ⇒ ty list ⇒ 'addr expr1 ⇒ ty⇩_i' list"
  and compTs :: "ty list ⇒ nat hyperset ⇒ ty list ⇒ 'addr expr1 list ⇒ ty⇩_i' list"
where
  "compT E A ST (new C) = []"
| "compT E A ST (newA T⌊e⌉) = compT E A ST e @ [after E A ST e]"
| "compT E A ST (Cast C e) = compT E A ST e @ [after E A ST e]"
| "compT E A ST (e instanceof T) = compT E A ST e @ [after E A ST e]"
| "compT E A ST (Val v) = []"
| "compT E A ST (e1 «bop» e2) =
  (let ST1 = ty E e1#ST; A1 = A ⊔ 𝒜 e1 in
   compT E A ST e1 @ [after E A ST e1] @
   compT E A1 ST1 e2 @ [after E A1 ST1 e2])"
| "compT E A ST (Var i) = []"
| "compT E A ST (i := e) = compT E A ST e @ [after E A ST e, ty⇩_i' ST E (A ⊔ 𝒜 e ⊔ ⌊{i}⌋)]"
| "compT E A ST (a⌊i⌉) =
  (let ST1 = ty E a # ST; A1 = A ⊔ 𝒜 a
   in  compT E A ST a @ [after E A ST a] @ compT E A1 ST1 i @ [after E A1 ST1 i])"
| "compT E A ST (a⌊i⌉ := e) =
  (let ST1 = ty E a # ST; A1 = A ⊔ 𝒜 a;
       ST2 = ty E i # ST1; A2 = A1 ⊔ 𝒜 i; A3 = A2 ⊔ 𝒜 e
   in compT E A ST a @ [after E A ST a] @ compT E A1 ST1 i @ [after E A1 ST1 i] @ compT E A2 ST2 e @ [after E A2 ST2 e, ty⇩_i' ST E A3])"
| "compT E A ST (a∙length) = compT E A ST a @ [after E A ST a]"
| "compT E A ST (e∙F{D}) = compT E A ST e @ [after E A ST e]"
| "compT E A ST (e1∙F{D} := e2) =
  (let ST1 = ty E e1#ST; A1 = A ⊔ 𝒜 e1; A2 = A1 ⊔ 𝒜 e2
   in  compT E A ST e1 @ [after E A ST e1] @ compT E A1 ST1 e2 @ [after E A1 ST1 e2] @ [ty⇩_i' ST E A2])"
| "compT E A ST (e1∙compareAndSwap(D∙F, e2, e3)) =
  (let ST1 = ty E e1 # ST; A1 = A ⊔ 𝒜 e1; ST2 = ty E e2 # ST1; A2 = A1 ⊔ 𝒜 e2; A3 = A2 ⊔ 𝒜 e3
   in  compT E A ST e1 @ [after E A ST e1] @ compT E A1 ST1 e2 @ [after E A1 ST1 e2] @ compT E A2 ST2 e3 @ [after E A2 ST2 e3])"
| "compT E A ST (e∙M(es)) =
   compT E A ST e @ [after E A ST e] @
   compTs E (A ⊔ 𝒜 e) (ty E e # ST) es"
| "compT E A ST {i:T=None; e} = compT (E@[T]) (A⊖i) ST e"
| "compT E A ST {i:T=⌊v⌋; e} = 
   [after E A ST (Val v), ty⇩_i' ST (E@[T]) (A ⊔ ⌊{i}⌋)] @ compT (E@[T]) (A ⊔ ⌊{i}⌋) ST e"

| "compT E A ST (sync⇘i⇙ (e1) e2) =
  (let A1 = A ⊔ 𝒜 e1 ⊔ ⌊{i}⌋; E1 = E @ [Class Object]; ST2 = ty E1 e2 # ST; A2 = A1 ⊔ 𝒜 e2
   in  compT E A ST e1 @
       [after E A ST e1,
        ty⇩_i' (Class Object # Class Object # ST) E (A ⊔ 𝒜 e1),
        ty⇩_i' (Class Object # ST) E1 A1,
        ty⇩_i' ST E1 A1] @
       compT E1 A1 ST e2 @ 
       [ty⇩_i' ST2 E1 A2, ty⇩_i' (Class Object # ST2) E1 A2, ty⇩_i' ST2 E1 A2, 
        ty⇩_i' (Class Throwable # ST) E1 A1,
        ty⇩_i' (Class Object # Class Throwable # ST) E1 A1,
        ty⇩_i' (Class Throwable # ST) E1 A1])"
| "compT E A ST (insync⇘i⇙ (a) e) = []"

| "compT E A ST (e1;;e2) =
  (let A1 = A ⊔ 𝒜 e1 in
   compT E A ST e1 @ [after E A ST e1, ty⇩_i' ST E A1] @
   compT E A1 ST e2)"
| "compT E A ST (if (e) e1 else e2) =
   (let A0 = A ⊔ 𝒜 e; τ = ty⇩_i' ST E A0 in
    compT E A ST e @ [after E A ST e, τ] @
    compT E A0 ST e1 @ [after E A0 ST e1, τ] @
    compT E A0 ST e2)"
| "compT E A ST (while (e) c) =
   (let A0 = A ⊔ 𝒜 e;  A1 = A0 ⊔ 𝒜 c; τ = ty⇩_i' ST E A0 in
    compT E A ST e @ [after E A ST e, τ] @
    compT E A0 ST c @ [after E A0 ST c, ty⇩_i' ST E A1, ty⇩_i' ST E A0])"
| "compT E A ST (throw e) = compT E A ST e @ [after E A ST e]"
| "compT E A ST (try e1 catch(C i) e2) =
   compT E A ST e1 @ [after E A ST e1] @
   [ty⇩_i' (Class C#ST) E A, ty⇩_i' ST (E@[Class C]) (A ⊔ ⌊{i}⌋)] @
   compT (E@[Class C]) (A ⊔ ⌊{i}⌋) ST e2"

| "compTs E A ST [] = []"
| "compTs E A ST (e#es) = compT E A ST e @ [after E A ST e] @
                            compTs E (A ⊔ (𝒜 e)) (ty E e # ST) es"
by pat_completeness simp_all
termination
apply(relation "case_sum (λp. size (snd (snd (snd p)))) (λp. size_list size (snd (snd (snd p)))) <*mlex*> {}")
apply(rule wf_mlex[OF wf_on_bot])
apply(rule mlex_less, simp)+
done

lemmas compT_compTs_induct =
  compT_compTs.induct[
    unfolded meta_all5_eq_conv meta_all4_eq_conv meta_all3_eq_conv meta_all2_eq_conv meta_all_eq_conv,
    case_names
      new NewArray Cast InstanceOf Val BinOp Var LAss AAcc AAss ALen FAcc FAss CompareAndSwap Call BlockNone BlockSome
      Synchronized InSynchronized Seq Cond While throw TryCatch
      Nil Cons]

definition compTa :: "ty list ⇒ nat hyperset ⇒ ty list ⇒ 'addr expr1 ⇒ ty⇩_i' list"
where "compTa E A ST e ≡ compT E A ST e @ [after E A ST e]"

lemmas compE2_not_Nil = compE2_neq_Nil
declare compE2_not_Nil[simp]

lemma compT_sizes[simp]:
  shows "size(compT E A ST e) = size(compE2 e) - 1"
  and "size(compTs E A ST es) = size(compEs2 es)"
apply(induct E A ST e and E A ST es rule: compT_compTs_induct)
apply(auto split:nat_diff_split)
done

lemma compT_None_not_Some [simp]: "⌊τ⌋ ∉ set (compT E None ST e)"
  and compTs_None_not_Some [simp]: "⌊τ⌋ ∉ set (compTs E None ST es)"
by(induct E A≡"None :: nat hyperset" ST e and E A≡"None :: nat hyperset" ST es rule: compT_compTs_induct) (simp_all add:after_def)

lemma pair_eq_ty⇩_i'_conv:
  "(⌊(ST, LT)⌋ = ty⇩_i' ST⇩₀ E A) = (case A of None ⇒ False | Some A ⇒ (ST = ST⇩₀ ∧ LT = ty⇩_l E A))"
by(simp add:ty⇩_i'_def)

lemma pair_conv_ty⇩_i': "⌊(ST, ty⇩_l E A)⌋ = ty⇩_i' ST E ⌊A⌋"
by(simp add:ty⇩_i'_def)

lemma ty⇩_i'_antimono2:
 "⟦ E ≤ E'; A ⊆ A' ⟧ ⟹ P ⊢ ty⇩_i' ST E' ⌊A'⌋ ≤' ty⇩_i' ST E ⌊A⌋"
by(auto simp:ty⇩_i'_def ty⇩_l_def list_all2_conv_all_nth less_eq_list_def prefix_def)

declare ty⇩_i'_antimono [intro!] after_def[simp] pair_conv_ty⇩_i'[simp] pair_eq_ty⇩_i'_conv[simp]

lemma compT_LT_prefix:
  "⟦ ⌊(ST,LT)⌋ ∈ set(compT E A ST0 e); ℬ e (size E) ⟧ ⟹ P ⊢ ⌊(ST,LT)⌋ ≤' ty⇩_i' ST E A"
  and compTs_LT_prefix:
  "⟦ ⌊(ST,LT)⌋ ∈ set(compTs E A ST0 es); ℬs es (size E) ⟧ ⟹ P ⊢ ⌊(ST,LT)⌋ ≤' ty⇩_i' ST E A"
proof(induct E A ST0 e and E A ST0 es rule: compT_compTs_induct)
  case FAss thus ?case by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
next
  case BinOp thus ?case
    by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans split:bop.splits)
next
  case Seq thus ?case by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
next
  case While thus ?case by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
next
  case Cond thus ?case by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
next
  case BlockNone thus ?case by(auto)
next
  case BlockSome thus ?case
    by(clarsimp simp only: ty⇩_i'_def)(fastforce intro: ty⇩_i'_incr simp add: hyperset_defs elim: sup_state_opt_trans)
next
  case Call thus ?case by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
next
  case Cons thus ?case
    by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
next
  case TryCatch thus ?case
    by(fastforce simp:hyperset_defs intro!: ty⇩_i'_incr elim!:sup_state_opt_trans)
next
  case NewArray thus ?case by(auto simp add: hyperset_defs)
next
  case AAcc thus ?case by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
next
  case AAss thus ?case by(auto simp:hyperset_defs Un_ac elim!:sup_state_opt_trans)
next
  case ALen thus ?case by(auto simp add: hyperset_defs)
next
  case CompareAndSwap thus ?case by(auto simp: hyperset_defs Un_ac elim!:sup_state_opt_trans)
next
  case Synchronized thus ?case
    by(fastforce simp add: hyperset_defs elim: sup_state_opt_trans intro: sup_state_opt_trans[OF ty⇩_i'_incr] ty⇩_i'_antimono2)
qed (auto simp:hyperset_defs)

declare ty⇩_i'_antimono [rule del] after_def[simp del] pair_conv_ty⇩_i'[simp del] pair_eq_ty⇩_i'_conv[simp del]

lemma OK_None_states [iff]: "OK None ∈ states P mxs mxl"
by(simp add: JVM_states_unfold)

end

context TC1 begin

lemma after_in_states:
 "⟦ P,E ⊢1 e :: T; set E ⊆ types P; set ST ⊆ types P; size ST + max_stack e ≤ mxs ⟧
 ⟹ OK (after E A ST e) ∈ states P mxs mxl"
apply(subgoal_tac "size ST + 1 ≤ mxs")
 apply(simp add:after_def ty⇩_i'_def JVM_states_unfold ty⇩_l_in_types)
 apply(clarify intro!: exI)
 apply(rule conjI)
  apply(rule exI[where x="length ST + 1"], fastforce)
 apply(clarsimp)
 apply(rule conjI[OF WT1_is_type[OF wf_prog]], auto intro: listI)
using max_stack1[of e] by simp

end

context TC0 begin

lemma OK_ty⇩_i'_in_statesI [simp]:
  "⟦ set E ⊆ types P; set ST ⊆ types P; size ST ≤ mxs ⟧
  ⟹ OK (ty⇩_i' ST E A) ∈ states P mxs mxl"
apply(simp add:ty⇩_i'_def JVM_states_unfold ty⇩_l_in_types)
apply(blast intro!:listI)
done

end

lemma is_class_type_aux: "is_class P C ⟹ is_type P (Class C)"
by(simp)

context TC1 begin

declare is_type.simps[simp del] subsetI[rule del]

theorem
  shows compT_states:
  "⟦ P,E ⊢1 e :: T; set E ⊆ types P; set ST ⊆ types P;
     size ST + max_stack e ≤ mxs; size E + max_vars e ≤ mxl ⟧
  ⟹ OK ` set(compT E A ST e) ⊆ states P mxs mxl"
  (is "PROP ?P e E T A ST")

  and compTs_states: 
  "⟦ P,E ⊢1 es[::]Ts;  set E ⊆ types P; set ST ⊆ types P;
    size ST + max_stacks es ≤ mxs; size E + max_varss es ≤ mxl ⟧
  ⟹ OK ` set(compTs E A ST es) ⊆ states P mxs mxl"
    (is "PROP ?Ps es E Ts A ST")
proof(induct E A ST e and E A ST es arbitrary: T and Ts rule: compT_compTs_induct)
  case new thus ?case by(simp)
next
  case (Cast C e) thus ?case by (auto simp:after_in_states)
next
  case InstanceOf thus ?case by (auto simp:after_in_states)
next
  case Val thus  ?case by(simp)
next
  case Var thus ?case by(simp)
next
  case LAss thus ?case  by(auto simp:after_in_states)
next
  case FAcc thus ?case by(auto simp:after_in_states)
next
  case FAss thus ?case
    by(auto simp:image_Un WT1_is_type[OF wf_prog] after_in_states)
next
  case CompareAndSwap thus ?case  by(auto simp:image_Un WT1_is_type[OF wf_prog] after_in_states)
next
  case Seq thus ?case
    by(auto simp:image_Un after_in_states)
next
  case BinOp thus ?case
    by(auto simp:image_Un WT1_is_type[OF wf_prog] after_in_states)
next
  case Cond thus ?case
    by(force simp:image_Un WT1_is_type[OF wf_prog] after_in_states)
next
  case While thus ?case
    by(auto simp:image_Un WT1_is_type[OF wf_prog] after_in_states)
next
  case BlockNone thus ?case by auto
next
  case (BlockSome E A ST i ty v exp)
  with max_stack1[of exp] show ?case by(auto intro: after_in_states)
next
  case (TryCatch E A ST e⇩₁ C i e⇩₂)
  moreover have "size ST + 1 ≤ mxs" using TryCatch.prems max_stack1[of e⇩₁] by auto
  ultimately show ?case  
    by(auto simp:image_Un WT1_is_type[OF wf_prog] after_in_states
                  is_class_type_aux)
next
  case Nil thus ?case by simp
next
  case Cons thus ?case
    by(auto simp:image_Un  WT1_is_type[OF wf_prog] after_in_states)
next
  case throw thus ?case
    by(auto simp: WT1_is_type[OF wf_prog] after_in_states)
next
  case Call thus ?case
    by(auto simp:image_Un WT1_is_type[OF wf_prog] after_in_states)
next
  case NewArray thus ?case
    by(auto simp:image_Un WT1_is_type[OF wf_prog] after_in_states)
next
  case AAcc thus ?case by(auto simp:image_Un WT1_is_type[OF wf_prog] after_in_states)
next
  case AAss thus ?case by(auto simp:image_Un WT1_is_type[OF wf_prog] after_in_states)
next
  case ALen thus ?case by(auto simp:image_Un WT1_is_type[OF wf_prog] after_in_states)
next
  case InSynchronized thus ?case by auto
next
  case (Synchronized E A ST i exp1 exp2)
  from ‹P,E ⊢1 sync⇘i⇙ (exp1) exp2 :: T› obtain T1
    where wt1: "P,E ⊢1 exp1 :: T1" and T1: "is_refT T1" "T1 ≠ NT"
    and wt2: "P,E@[Class Object] ⊢1 exp2 :: T" by auto
  moreover note E = ‹set E ⊆ types P› with wf_prog
  have E': "set (E@[Class Object]) ⊆ types P" by(auto simp add: is_type.simps)
  moreover from wf_prog wt2 E' have T: "is_type P T" by(rule WT1_is_type)
  note ST = ‹set ST ⊆ types P› with wf_prog
  have ST': "set (Class Object # ST) ⊆ types P" by(auto simp add: is_type.simps)
  moreover from wf_prog have throwable: "is_type P (Class Throwable)"
    unfolding is_type.simps by(rule is_class_Throwable)
  ultimately show ?case using Synchronized max_stack1[of exp2] T
    by(auto simp add: image_Un after_in_states)
qed

declare is_type.simps[simp] subsetI[intro!]

end


locale TC2 = TC0 +
  fixes T⇩_r :: ty and mxs :: pc
begin
  
definition
  wt_instrs :: "'addr instr list ⇒ ex_table ⇒ ty⇩_i' list ⇒ bool" (‹(⊢ _, _ /[::]/ _)› [0,0,51] 50)
where
  "⊢ is,xt [::] τs ≡ size is < size τs ∧ pcs xt ⊆ {0..<size is} ∧ (∀pc< size is. P,T⇩_r,mxs,size τs,xt ⊢ is!pc,pc :: τs)"

lemmas wt_defs = wt_instrs_def wt_instr_def app_def eff_def norm_eff_def

lemma wt_instrs_Nil [simp]: "τs ≠ [] ⟹ ⊢ [],[] [::] τs"
by(simp add:wt_defs)

end

locale TC3 = TC1 + TC2

lemma eff_None [simp]: "eff i P pc et None = []"
by (simp add: Effect.eff_def)

declare split_comp_eq[simp del]

lemma wt_instr_appR:
 "⟦ P,T,m,mpc,xt ⊢ is!pc,pc :: τs;
    pc < size is; size is < size τs; mpc ≤ size τs; mpc ≤ mpc' ⟧
  ⟹ P,T,m,mpc',xt ⊢ is!pc,pc :: τs@τs'"
by (fastforce simp:wt_instr_def app_def)


lemma relevant_entries_shift [simp]:
  "relevant_entries P i (pc+n) (shift n xt) = shift n (relevant_entries P i pc xt)"
  apply (induct xt)
  apply (unfold relevant_entries_def shift_def) 
   apply simp
  apply (auto simp add: is_relevant_entry_def)
  done



lemma xcpt_eff_shift [simp]:
  "xcpt_eff i P (pc+n) τ (shift n xt) =
   map (λ(pc,τ). (pc + n, τ)) (xcpt_eff i P pc τ xt)"
apply(simp add: xcpt_eff_def)
apply(cases τ)
apply(auto simp add: shift_def)
done


lemma  eff_shift [simp]:
  "app⇩_i (i, P, pc, m, T, τ) ⟹
   eff i P (pc+n) (shift n xt) (Some τ) =
   map (λ(pc,τ). (pc+n,τ)) (eff i P pc xt (Some τ))"
apply(simp add:eff_def norm_eff_def)
apply(cases "i",auto)
done


lemma xcpt_app_shift [simp]:
  "xcpt_app i P (pc+n) m (shift n xt) τ = xcpt_app i P pc m xt τ"
by (simp add: xcpt_app_def) (auto simp add: shift_def)


lemma wt_instr_appL:
  "⟦ P,T,m,mpc,xt ⊢ i,pc :: τs; pc < size τs; mpc ≤ size τs ⟧
  ⟹ P,T,m,mpc + size τs',shift (size τs') xt ⊢ i,pc+size τs' :: τs'@τs"
apply(clarsimp simp add: wt_instr_def app_def)
apply(auto)
apply(cases "i", auto)
done


lemma wt_instr_Cons:
  "⟦ P,T,m,mpc - 1,[] ⊢ i,pc - 1 :: τs;
     0 < pc; 0 < mpc; pc < size τs + 1; mpc ≤ size τs + 1 ⟧
  ⟹ P,T,m,mpc,[] ⊢ i,pc :: τ#τs"
apply(drule wt_instr_appL[where τs' = "[τ]"])
apply arith
apply arith
apply (simp split:nat_diff_split_asm)
done


lemma wt_instr_append:
  "⟦ P,T,m,mpc - size τs',[] ⊢ i,pc - size τs' :: τs;
     size τs' ≤ pc; size τs' ≤ mpc; pc < size τs + size τs'; mpc ≤ size τs + size τs' ⟧
  ⟹ P,T,m,mpc,[] ⊢ i,pc :: τs'@τs"
apply(drule wt_instr_appL[where τs' = τs'])
apply arith
apply arith
apply (simp split:nat_diff_split_asm)
done


lemma xcpt_app_pcs:
  "pc ∉ pcs xt ⟹ xcpt_app i P pc mxs xt τ"
by (auto simp add: xcpt_app_def relevant_entries_def is_relevant_entry_def pcs_def)


lemma xcpt_eff_pcs:
  "pc ∉ pcs xt ⟹ xcpt_eff i P pc τ xt = []"
by (cases τ)
   (auto simp add: is_relevant_entry_def xcpt_eff_def relevant_entries_def pcs_def
           intro!: filter_False)


lemma pcs_shift:
  "pc < n ⟹ pc ∉ pcs (shift n xt)" 
by (auto simp add: shift_def pcs_def)

lemma xcpt_eff_shift_pc_ge_n: assumes "x ∈ set (xcpt_eff i P pc τ (shift n xt))"
  shows "n ≤ pc"
proof -
  { assume "pc < n"
    hence "pc ∉ pcs (shift n xt)" by(rule pcs_shift)
    with assms have False
      by(auto simp add: pcs_def xcpt_eff_def is_relevant_entry_def relevant_entries_def split_beta cong: filter_cong) }
  thus ?thesis by(cases "n ≤ pc")(auto)
qed

lemma wt_instr_appRx:
  "⟦ P,T,m,mpc,xt ⊢ is!pc,pc :: τs; pc < size is; size is < size τs; mpc ≤ size τs ⟧
  ⟹ P,T,m,mpc,xt @ shift (size is) xt' ⊢ is!pc,pc :: τs"
apply(clarsimp simp:wt_instr_def eff_def app_def)
apply(fastforce dest: xcpt_eff_shift_pc_ge_n intro!: xcpt_app_pcs[OF pcs_shift])
done

lemma wt_instr_appLx: 
  "⟦ P,T,m,mpc,xt ⊢ i,pc :: τs; pc ∉ pcs xt' ⟧
  ⟹ P,T,m,mpc,xt'@xt ⊢ i,pc :: τs"
by (auto simp:wt_instr_def app_def eff_def xcpt_app_pcs xcpt_eff_pcs)


context TC2 begin

lemma wt_instrs_extR:
  "⊢ is,xt [::] τs ⟹ ⊢ is,xt [::] τs @ τs'"
by(auto simp add:wt_instrs_def wt_instr_appR)


lemma wt_instrs_ext:
  "⟦ ⊢ is⇩₁,xt⇩₁ [::] τs⇩₁@τs⇩₂; ⊢ is⇩₂,xt⇩₂ [::] τs⇩₂; size τs⇩₁ = size is⇩₁ ⟧
  ⟹ ⊢ is⇩₁@is⇩₂, xt⇩₁ @ shift (size is⇩₁) xt⇩₂ [::] τs⇩₁@τs⇩₂"
apply(clarsimp simp:wt_instrs_def)
apply(rule conjI, fastforce)
apply(rule conjI, fastforce simp add: pcs_shift_conv)
apply clarsimp
apply(rule conjI, fastforce simp:wt_instr_appRx)
apply clarsimp
apply(erule_tac x = "pc - size is⇩₁" in allE)+
apply(thin_tac "P ⟶ Q" for P Q)
apply(erule impE, arith) 
apply(drule_tac τs' = "τs⇩₁" in wt_instr_appL)
  apply arith
 apply simp
apply(fastforce simp add:add.commute intro!: wt_instr_appLx)
done


corollary wt_instrs_ext2:
  "⟦ ⊢ is⇩₂,xt⇩₂ [::] τs⇩₂; ⊢ is⇩₁,xt⇩₁ [::] τs⇩₁@τs⇩₂; size τs⇩₁ = size is⇩₁ ⟧
  ⟹ ⊢ is⇩₁@is⇩₂, xt⇩₁ @ shift (size is⇩₁) xt⇩₂ [::] τs⇩₁@τs⇩₂"
by(rule wt_instrs_ext)


corollary wt_instrs_ext_prefix [trans]:
  "⟦ ⊢ is⇩₁,xt⇩₁ [::] τs⇩₁@τs⇩₂; ⊢ is⇩₂,xt⇩₂ [::] τs⇩₃;
     size τs⇩₁ = size is⇩₁; τs⇩₃ ≤ τs⇩₂ ⟧
  ⟹ ⊢ is⇩₁@is⇩₂, xt⇩₁ @ shift (size is⇩₁) xt⇩₂ [::] τs⇩₁@τs⇩₂"
by(bestsimp simp:less_eq_list_def prefix_def elim: wt_instrs_ext dest:wt_instrs_extR)


corollary wt_instrs_app:
  assumes is⇩₁: "⊢ is⇩₁,xt⇩₁ [::] τs⇩₁@[τ]"
  assumes is⇩₂: "⊢ is⇩₂,xt⇩₂ [::] τ#τs⇩₂"
  assumes s: "size τs⇩₁ = size is⇩₁"
  shows "⊢ is⇩₁@is⇩₂, xt⇩₁@shift (size is⇩₁) xt⇩₂ [::] τs⇩₁@τ#τs⇩₂"
proof -
  from is⇩₁ have "⊢ is⇩₁,xt⇩₁ [::] (τs⇩₁@[τ])@τs⇩₂"
    by (rule wt_instrs_extR)
  hence "⊢ is⇩₁,xt⇩₁ [::] τs⇩₁@τ#τs⇩₂" by simp
  from this is⇩₂ s show ?thesis by (rule wt_instrs_ext) 
qed


corollary wt_instrs_app_last[trans]:
  "⟦ ⊢ is⇩₂,xt⇩₂ [::] τ#τs⇩₂; ⊢ is⇩₁,xt⇩₁ [::] τs⇩₁;
     last τs⇩₁ = τ;  size τs⇩₁ = size is⇩₁+1 ⟧
  ⟹ ⊢ is⇩₁@is⇩₂, xt⇩₁@shift (size is⇩₁) xt⇩₂ [::] τs⇩₁@τs⇩₂"
apply(cases τs⇩₁ rule:rev_cases)
 apply simp
apply(simp add:wt_instrs_app)
done


corollary wt_instrs_append_last[trans]:
  "⟦ ⊢ is,xt [::] τs; P,T⇩_r,mxs,mpc,[] ⊢ i,pc :: τs;
     pc = size is; mpc = size τs; size is + 1 < size τs ⟧
  ⟹ ⊢ is@[i],xt [::] τs"
apply(clarsimp simp add:wt_instrs_def)
apply(rule conjI, fastforce)
apply(fastforce intro!:wt_instr_appLx[where xt = "[]",simplified]
               dest!:less_antisym)
done


corollary wt_instrs_app2:
  "⟦ ⊢ (is⇩₂ :: 'b instr list),xt⇩₂ [::] τ'#τs⇩₂;  ⊢ is⇩₁,xt⇩₁ [::] τ#τs⇩₁@[τ'];
     xt' = xt⇩₁ @ shift (size is⇩₁) xt⇩₂;  size τs⇩₁+1 = size is⇩₁ ⟧
  ⟹ ⊢ is⇩₁@is⇩₂,xt' [::] τ#τs⇩₁@τ'#τs⇩₂"
using wt_instrs_app[where ?τs⇩₁.0 = "τ # τs⇩₁" and ?'b = "'b"] by simp


corollary wt_instrs_app2_simp[trans,simp]:
  "⟦ ⊢ (is⇩₂ :: 'b instr list),xt⇩₂ [::] τ'#τs⇩₂;  ⊢ is⇩₁,xt⇩₁ [::] τ#τs⇩₁@[τ']; size τs⇩₁+1 = size is⇩₁ ⟧
  ⟹ ⊢ is⇩₁@is⇩₂, xt⇩₁@shift (size is⇩₁) xt⇩₂ [::] τ#τs⇩₁@τ'#τs⇩₂"
using wt_instrs_app[where ?τs⇩₁.0 = "τ # τs⇩₁" and ?'b = "'b"] by simp


corollary wt_instrs_Cons[simp]:
  "⟦ τs ≠ []; ⊢ [i],[] [::] [τ,τ']; ⊢ is,xt [::] τ'#τs ⟧
  ⟹ ⊢ i#is,shift 1 xt [::] τ#τ'#τs"
using wt_instrs_app2[where ?is⇩₁.0 = "[i]" and ?τs⇩₁.0 = "[]" and ?is⇩₂.0 = "is"
                      and ?xt⇩₁.0 = "[]"]
by simp


corollary wt_instrs_Cons2[trans]:
  assumes τs: "⊢ is,xt [::] τs"
  assumes i: "P,T⇩_r,mxs,mpc,[] ⊢ i,0 :: τ#τs"
  assumes mpc: "mpc = size τs + 1"
  shows "⊢ i#is,shift 1 xt [::] τ#τs"
proof -
  from τs have "τs ≠ []" by (auto simp: wt_instrs_def)
  with mpc i have "⊢ [i],[] [::] [τ]@τs" by (simp add: wt_instrs_def)
  with τs show ?thesis by (fastforce dest: wt_instrs_ext)
qed


lemma wt_instrs_last_incr[trans]:
  "⟦ ⊢ is,xt [::] τs@[τ]; P ⊢ τ ≤' τ' ⟧ ⟹ ⊢ is,xt [::] τs@[τ']"
apply(clarsimp simp add:wt_instrs_def wt_instr_def)
apply(rule conjI)
apply(fastforce)
apply(clarsimp)
apply(rename_tac pc' tau')
apply(erule allE, erule (1) impE)
apply(clarsimp)
apply(drule (1) bspec)
apply(clarsimp)
apply(subgoal_tac "pc' = size τs")
prefer 2
apply(clarsimp simp:app_def)
apply(drule (1) bspec)
apply(clarsimp)
apply(auto elim!:sup_state_opt_trans)
done

end

lemma [iff]: "xcpt_app i P pc mxs [] τ"
by (simp add: xcpt_app_def relevant_entries_def)


lemma [simp]: "xcpt_eff i P pc τ [] = []"
by (simp add: xcpt_eff_def relevant_entries_def)

context TC2 begin

lemma wt_New:
  "⟦ is_class P C; size ST < mxs ⟧ ⟹
   ⊢ [New C],[] [::] [ty⇩_i' ST E A, ty⇩_i' (Class C#ST) E A]"
by(simp add:wt_defs ty⇩_i'_def)


lemma wt_Cast:
  "is_type P T ⟹
   ⊢ [Checkcast T],[] [::] [ty⇩_i' (U # ST) E A, ty⇩_i' (T # ST) E A]"
by(simp add: ty⇩_i'_def wt_defs)

lemma wt_Instanceof:
  "⟦ is_type P T; is_refT U ⟧ ⟹
   ⊢ [Instanceof T],[] [::] [ty⇩_i' (U # ST) E A, ty⇩_i' (Boolean # ST) E A]"
by(simp add: ty⇩_i'_def wt_defs)

lemma wt_Push:
  "⟦ size ST < mxs; typeof v = Some T ⟧
  ⟹ ⊢ [Push v],[] [::] [ty⇩_i' ST E A, ty⇩_i' (T#ST) E A]"
by(simp add: ty⇩_i'_def wt_defs)


lemma wt_Pop:
 "⊢ [Pop],[] [::] (ty⇩_i' (T#ST) E A # ty⇩_i' ST E A # τs)"
by(simp add: ty⇩_i'_def wt_defs)

lemma wt_BinOpInstr:
  "P ⊢ T1«bop»T2 :: T ⟹ ⊢ [BinOpInstr bop],[] [::] [ty⇩_i' (T2 # T1 # ST) E A, ty⇩_i' (T # ST) E A]"
by(auto simp:ty⇩_i'_def wt_defs dest: WT_binop_WTrt_binop intro: list_all2_refl)

lemma wt_Load:
  "⟦ size ST < mxs; size E ≤ mxl; i ∈∈ A; i < size E ⟧
  ⟹ ⊢ [Load i],[] [::] [ty⇩_i' ST E A, ty⇩_i' (E!i # ST) E A]"
by(auto simp add:ty⇩_i'_def wt_defs ty⇩_l_def hyperset_defs intro: widens_refl)


lemma wt_Store:
 "⟦ P ⊢ T ≤ E!i; i < size E; size E ≤ mxl ⟧ ⟹
  ⊢ [Store i],[] [::] [ty⇩_i' (T#ST) E A, ty⇩_i' ST E (⌊{i}⌋ ⊔ A)]"
by(auto simp:hyperset_defs nth_list_update ty⇩_i'_def wt_defs ty⇩_l_def
        intro:list_all2_all_nthI)


lemma wt_Get:
 "⟦ P ⊢ C sees F:T (fm) in D; class_type_of' U = ⌊C⌋ ⟧ ⟹
  ⊢ [Getfield F D],[] [::] [ty⇩_i' (U # ST) E A, ty⇩_i' (T # ST) E A]"
by(cases U)(auto simp: ty⇩_i'_def wt_defs dest: sees_field_idemp sees_field_decl_above intro: widens_refl widen_trans widen_array_object)

lemma wt_Put:
  "⟦ P ⊢ C sees F:T (fm) in D; class_type_of' U = ⌊C⌋; P ⊢ T' ≤ T ⟧ ⟹
  ⊢ [Putfield F D],[] [::] [ty⇩_i' (T' # U # ST) E A, ty⇩_i' ST E A]"
by(cases U)(auto 4 3 intro: sees_field_idemp widen_trans widen_array_object dest: sees_field_decl_above simp: ty⇩_i'_def wt_defs)

lemma wt_CAS:
  "⟦ P ⊢ C sees F:T (fm) in D; class_type_of' U' = ⌊C⌋; volatile fm; P ⊢ T2 ≤ T; P ⊢ T3 ≤ T ⟧ ⟹
  ⊢ [CAS F D],[] [::] [ty⇩_i' (T3 # T2 # U' # ST) E A, ty⇩_i' (Boolean # ST) E A]"
by(cases U')(auto 4 4 simp add: ty⇩_i'_def wt_defs intro: sees_field_idemp widen_trans widen_array_object dest: sees_field_decl_above)

lemma wt_Throw:
  "P ⊢ C ≼⇧^* Throwable ⟹ ⊢ [ThrowExc],[] [::] [ty⇩_i' (Class C # ST) E A, τ']"
by(simp add: ty⇩_i'_def wt_defs)


lemma wt_IfFalse:
  "⟦ 2 ≤ i; nat i < size τs + 2; P ⊢ ty⇩_i' ST E A ≤' τs ! nat(i - 2) ⟧
  ⟹ ⊢ [IfFalse i],[] [::] ty⇩_i' (Boolean # ST) E A # ty⇩_i' ST E A # τs"
by(auto simp add: ty⇩_i'_def wt_defs eval_nat_numeral nat_diff_distrib)


lemma wt_Goto:
 "⟦ 0 ≤ int pc + i; nat (int pc + i) < size τs; size τs ≤ mpc;
    P ⊢ τs!pc ≤' τs ! nat (int pc + i) ⟧
 ⟹ P,T,mxs,mpc,[] ⊢ Goto i,pc :: τs"
by(clarsimp simp add: wt_defs)

end

context TC3 begin

lemma wt_Invoke:
  "⟦ size es = size Ts'; class_type_of' U = ⌊C⌋; P ⊢ C sees M: Ts→T = m in D; P ⊢ Ts' [≤] Ts ⟧
  ⟹ ⊢ [Invoke M (size es)],[] [::] [ty⇩_i' (rev Ts' @ U # ST) E A, ty⇩_i' (T#ST) E A]"
apply(clarsimp simp add: ty⇩_i'_def wt_defs)
apply safe
apply(simp_all (no_asm_use))
apply(auto simp add: intro: widens_refl)
done

end

declare nth_append[simp del]
declare [[simproc del: list_to_set_comprehension]]

context TC2 begin

corollary wt_instrs_app3[simp]:
  "⟦ ⊢ (is⇩₂ :: 'b instr list),[] [::] (τ' # τs⇩₂);  ⊢ is⇩₁,xt⇩₁ [::] τ # τs⇩₁ @ [τ']; size τs⇩₁+1 = size is⇩₁⟧
  ⟹ ⊢ (is⇩₁ @ is⇩₂),xt⇩₁ [::] τ # τs⇩₁ @ τ' # τs⇩₂"
using wt_instrs_app2[where ?xt⇩₂.0 = "[]" and ?'b = "'b"] by (simp add:shift_def)


corollary wt_instrs_Cons3[simp]:
  "⟦ τs ≠ []; ⊢ [i],[] [::] [τ,τ']; ⊢ is,[] [::] τ'#τs ⟧
  ⟹ ⊢ (i # is),[] [::] τ # τ' # τs"
using wt_instrs_Cons[where ?xt = "[]"]
by (simp add:shift_def)

lemma wt_instrs_xapp:
  "⟦ ⊢ is⇩₁ @ is⇩₂, xt [::] τs⇩₁ @ ty⇩_i' (Class D # ST) E A # τs⇩₂;
     ∀τ ∈ set τs⇩₁. ∀ST' LT'. τ = Some(ST',LT') ⟶ 
      size ST ≤ size ST' ∧ P ⊢ Some (drop (size ST' - size ST) ST',LT') ≤' ty⇩_i' ST E A;
     size is⇩₁ = size τs⇩₁; size ST < mxs; case Co of None ⇒ D = Throwable | Some C ⇒ D = C ∧ is_class P C  ⟧ ⟹
  ⊢ is⇩₁ @ is⇩₂, xt @ [(0,size is⇩₁ - Suc n,Co,size is⇩₁,size ST)] [::] τs⇩₁ @ ty⇩_i' (Class D # ST) E A # τs⇩₂"
apply(simp add:wt_instrs_def split del: option.split_asm)
apply(rule conjI)
 apply(clarsimp split del: option.split_asm)
 apply arith
apply(clarsimp split del: option.split_asm)
apply(erule allE, erule (1) impE)
apply(clarsimp simp add: wt_instr_def app_def eff_def split del: option.split_asm)
apply(rule conjI)
 apply (thin_tac "∀x∈ A ∪ B. P x" for A B P)
 apply (thin_tac "∀x∈ A ∪ B. P x" for A B P)
 apply (clarsimp simp add: xcpt_app_def relevant_entries_def split del: option.split_asm)
 apply (simp add: nth_append is_relevant_entry_def split: if_split_asm split del: option.split_asm)
  apply (drule_tac x="τs⇩₁!pc" in bspec)
   apply (blast intro: nth_mem) 
  apply fastforce
 apply fastforce
apply (rule conjI)
 apply(clarsimp split del: option.split_asm)
 apply (erule disjE, blast)
 apply (erule disjE, blast)
 apply (clarsimp simp add: xcpt_eff_def relevant_entries_def split: if_split_asm)
apply(clarsimp split del: option.split_asm)
apply (erule disjE, blast)
apply (erule disjE, blast)
apply (clarsimp simp add: xcpt_eff_def relevant_entries_def split: if_split_asm split del: option.split_asm)
apply (simp add: nth_append is_relevant_entry_def split: if_split_asm split del: option.split_asm)
 apply (drule_tac x = "τs⇩₁!pc" in bspec)
  apply (blast intro: nth_mem)
 apply (fastforce simp add: ty⇩_i'_def)
done

lemma wt_instrs_xapp_Some[trans]:
  "⟦ ⊢ is⇩₁ @ is⇩₂, xt [::] τs⇩₁ @ ty⇩_i' (Class C # ST) E A # τs⇩₂;
     ∀τ ∈ set τs⇩₁. ∀ST' LT'. τ = Some(ST',LT') ⟶ 
      size ST ≤ size ST' ∧ P ⊢ Some (drop (size ST' - size ST) ST',LT') ≤' ty⇩_i' ST E A;
     size is⇩₁ = size τs⇩₁; is_class P C; size ST < mxs  ⟧ ⟹
  ⊢ is⇩₁ @ is⇩₂, xt @ [(0,size is⇩₁ - Suc n,Some C,size is⇩₁,size ST)] [::] τs⇩₁ @ ty⇩_i' (Class C # ST) E A # τs⇩₂"
by(erule (3) wt_instrs_xapp) simp

lemma wt_instrs_xapp_Any:
  "⟦ ⊢ is⇩₁ @ is⇩₂, xt [::] τs⇩₁ @ ty⇩_i' (Class Throwable # ST) E A # τs⇩₂;
     ∀τ ∈ set τs⇩₁. ∀ST' LT'. τ = Some(ST',LT') ⟶ 
      size ST ≤ size ST' ∧ P ⊢ Some (drop (size ST' - size ST) ST',LT') ≤' ty⇩_i' ST E A;
     size is⇩₁ = size τs⇩₁; size ST < mxs ⟧ ⟹
  ⊢ is⇩₁ @ is⇩₂, xt @ [(0,size is⇩₁ - Suc n,None,size is⇩₁,size ST)] [::] τs⇩₁ @ ty⇩_i' (Class Throwable # ST) E A # τs⇩₂"
by(erule (3) wt_instrs_xapp) simp

end

declare [[simproc add: list_to_set_comprehension]]
declare nth_append[simp]

lemma drop_Cons_Suc:
  "⋀xs. drop n xs = y#ys ⟹ drop (Suc n) xs = ys"
  apply (induct n)
   apply simp
  apply (simp add: drop_Suc)
  done

lemma drop_mess:
  "⟦Suc (length xs⇩₀) ≤ length xs; drop (length xs - Suc (length xs⇩₀)) xs = x # xs⇩₀⟧ 
  ⟹ drop (length xs - length xs⇩₀) xs = xs⇩₀"
apply (cases xs)
 apply simp
apply (simp add: Suc_diff_le)
apply (case_tac "length list - length xs⇩₀")
 apply simp
apply (simp add: drop_Cons_Suc)
done

lemma drop_mess2:
  assumes len: "Suc (Suc (length xs0)) ≤ length xs" 
  and drop: "drop (length xs - Suc (Suc (length xs0))) xs = x1 # x2 # xs0"
  shows "drop (length xs - length xs0) xs = xs0"
proof(cases xs)
  case Nil with assms show ?thesis by simp
next
  case (Cons x xs')
  note Cons[simp]
  show ?thesis
  proof(cases xs')
    case Nil with assms show ?thesis by(simp)
  next
    case (Cons x' xs'')
    note Cons[simp]
    show ?thesis 
    proof(rule drop_mess)
      from len show "Suc (length xs0) ≤ length xs" by simp
    next
      have "drop (length xs - length (x2 # xs0)) xs = x2 # xs0"
      proof(rule drop_mess)
        from len show "Suc (length (x2 # xs0)) ≤ length xs" by(simp)
      next
        from drop show "drop (length xs - Suc (length (x2 # xs0))) xs = x1 # x2 # xs0" by simp
      qed
      thus "drop (length xs - Suc (length xs0)) xs = x2 # xs0" by(simp)
    qed
  qed
qed

abbreviation postfix :: "'a list ⇒ 'a list ⇒ bool"  (‹(_/ ⤜ _)› [51, 50] 50) where
  "postfix xs ys ≡ suffix ys xs"

lemma postfix_conv_eq_length_drop: 
  "ST' ⤜ ST ⟷ length ST ≤ length ST' ∧ drop (length ST' - length ST) ST' = ST"
apply(auto)
apply (metis append_eq_conv_conj append_take_drop_id diff_is_0_eq drop_0 linorder_not_less nat_le_linear suffix_take)
apply (metis append_take_drop_id length_drop suffix_take same_append_eq size_list_def)
by (metis suffix_drop)

declare suffix_ConsI[simp]

context TC0 begin

declare after_def[simp] pair_eq_ty⇩_i'_conv[simp] 

lemma
  assumes "ST0 ⤜ ST'"
  shows compT_ST_prefix: 
  "⌊(ST,LT)⌋ ∈ set(compT E A ST0 e) ⟹ ST ⤜ ST'"

  and compTs_ST_prefix:
  "⌊(ST,LT)⌋ ∈ set(compTs E A ST0 es) ⟹ ST ⤜ ST'"
using assms
by(induct E A ST0 e and E A ST0 es rule: compT_compTs_induct) auto

declare after_def[simp del] pair_eq_ty⇩_i'_conv[simp del]

end
declare suffix_ConsI[simp del]

(* FIXME *)
lemma fun_of_simp [simp]: "fun_of S x y = ((x,y) ∈ S)" 
by (simp add: fun_of_def)

declare widens_refl [iff]

context TC3 begin

theorem compT_wt_instrs:
  "⟦ P,E ⊢1 e :: T; 𝒟 e A; ℬ e (size E); size ST + max_stack e ≤ mxs; size E + max_vars e ≤ mxl; set E ⊆ types P ⟧
  ⟹ ⊢ compE2 e, compxE2 e 0 (size ST) [::] ty⇩_i' ST E A # compT E A ST e @ [after E A ST e]"
  (is "PROP ?P e E T A ST")

  and compTs_wt_instrs:
  "⟦ P,E ⊢1 es[::]Ts;  𝒟s es A; ℬs es (size E); size ST + max_stacks es ≤ mxs; size E + max_varss es ≤ mxl; set E ⊆ types P ⟧
  ⟹ let τs = ty⇩_i' ST E A # compTs E A ST es
      in ⊢ compEs2 es,compxEs2 es 0 (size ST) [::] τs ∧ last τs = ty⇩_i' (rev Ts @ ST) E (A ⊔ 𝒜s es)"
  (is "PROP ?Ps es E Ts A ST")
proof(induct E A ST e and E A ST es arbitrary: T and Ts rule: compT_compTs_induct)
  case (TryCatch E A ST e⇩₁ C i e⇩₂)
  hence [simp]: "i = size E" by simp
  have wt⇩₁: "P,E ⊢1 e⇩₁ :: T" and wt⇩₂: "P,E@[Class C] ⊢1 e⇩₂ :: T"
    and "class": "is_class P C" using TryCatch by auto
  let ?A⇩₁ = "A ⊔ 𝒜 e⇩₁" let ?A⇩_i = "A ⊔ ⌊{i}⌋" let ?E⇩_i = "E @ [Class C]"
  let ?τ = "ty⇩_i' ST E A" let ?τs⇩₁ = "compT E A ST e⇩₁"
  let ?τ⇩₁ = "ty⇩_i' (T#ST) E ?A⇩₁" let ?τ⇩₂ = "ty⇩_i' (Class C#ST) E A"
  let ?τ⇩₃ = "ty⇩_i' ST ?E⇩_i ?A⇩_i" let ?τs⇩₂ = "compT ?E⇩_i ?A⇩_i ST e⇩₂"
  let ?τ⇩₂' = "ty⇩_i' (T#ST) ?E⇩_i (?A⇩_i ⊔ 𝒜 e⇩₂)"
  let ?τ' = "ty⇩_i' (T#ST) E (A ⊔ 𝒜 e⇩₁ ⊓ (𝒜 e⇩₂ ⊖ i))"
  let ?go = "Goto (int(size(compE2 e⇩₂)) + 2)"
  have "PROP ?P e⇩₂ ?E⇩_i T ?A⇩_i ST" by fact
  hence "⊢ compE2 e⇩₂,compxE2 e⇩₂ 0 (size ST) [::] (?τ⇩₃ # ?τs⇩₂) @ [?τ⇩₂']"
    using TryCatch.prems "class" by(auto simp:after_def)
  also have "?A⇩_i ⊔ 𝒜 e⇩₂ = (A ⊔ 𝒜 e⇩₂) ⊔ ⌊{size E}⌋"
    by(fastforce simp:hyperset_defs)
  also have "P ⊢ ty⇩_i' (T#ST) ?E⇩_i … ≤' ty⇩_i' (T#ST) E (A ⊔ 𝒜 e⇩₂)"
    by(simp add:hyperset_defs ty⇩_l_incr ty⇩_i'_def)
  also have "P ⊢ … ≤' ty⇩_i' (T#ST) E (A ⊔ 𝒜 e⇩₁ ⊓ (𝒜 e⇩₂ ⊖ i))"
    by(auto intro!: ty⇩_l_antimono simp:hyperset_defs ty⇩_i'_def)
  also have "(?τ⇩₃ # ?τs⇩₂) @ [?τ'] = ?τ⇩₃ # ?τs⇩₂ @ [?τ']" by simp
  also have "⊢ [Store i],[] [::] ?τ⇩₂ # [] @ [?τ⇩₃]"
    using TryCatch.prems
    by(auto simp:nth_list_update wt_defs ty⇩_i'_def ty⇩_l_def
      list_all2_conv_all_nth hyperset_defs)
  also have "[] @ (?τ⇩₃ # ?τs⇩₂ @ [?τ']) = (?τ⇩₃ # ?τs⇩₂ @ [?τ'])" by simp
  also have "P,T⇩_r,mxs,size(compE2 e⇩₂)+3,[] ⊢ ?go,0 :: ?τ⇩₁#?τ⇩₂#?τ⇩₃#?τs⇩₂ @ [?τ']"
    by(auto simp: hyperset_defs ty⇩_i'_def wt_defs nth_Cons nat_add_distrib
      fun_of_def intro: ty⇩_l_antimono list_all2_refl split:nat.split)
  also have "⊢ compE2 e⇩₁,compxE2 e⇩₁ 0 (size ST) [::] ?τ # ?τs⇩₁ @ [?τ⇩₁]"
    using TryCatch by(auto simp:after_def)
  also have "?τ # ?τs⇩₁ @ ?τ⇩₁ # ?τ⇩₂ # ?τ⇩₃ # ?τs⇩₂ @ [?τ'] =
             (?τ # ?τs⇩₁ @ [?τ⇩₁]) @ ?τ⇩₂ # ?τ⇩₃ # ?τs⇩₂ @ [?τ']" by simp
  also have "compE2 e⇩₁ @ ?go  # [Store i] @ compE2 e⇩₂ =
             (compE2 e⇩₁ @ [?go]) @ (Store i # compE2 e⇩₂)" by simp
  also 
  let "?Q τ" = "∀ST' LT'. τ = ⌊(ST', LT')⌋ ⟶ 
    size ST ≤ size ST' ∧ P ⊢ Some (drop (size ST' - size ST) ST',LT') ≤' ty⇩_i' ST E A"
  {
    have "?Q (ty⇩_i' ST E A)" by(clarsimp simp add: ty⇩_i'_def)
    moreover have "?Q (ty⇩_i' (T # ST) E ?A⇩₁)" 
      by (fastforce simp add: ty⇩_i'_def hyperset_defs intro!: ty⇩_l_antimono)
    moreover { fix τ
      assume τ: "τ ∈ set (compT E A ST e⇩₁)"
      hence "∀ST' LT'. τ = ⌊(ST', LT')⌋ ⟶ ST' ⤜ ST" by(auto intro: compT_ST_prefix[OF suffix_order.order_refl])
      with τ have "?Q τ" unfolding postfix_conv_eq_length_drop using ‹ℬ (try e⇩₁ catch(C i) e⇩₂) (length E)›
        by(fastforce dest!: compT_LT_prefix simp add: ty⇩_i'_def) }
    ultimately
    have "∀τ∈set (ty⇩_i' ST E A # compT E A ST e⇩₁ @ [ty⇩_i' (T # ST) E ?A⇩₁]). ?Q τ" by auto
  }
  also from TryCatch.prems max_stack1[of e⇩₁] have "size ST + 1 ≤ mxs" by auto
  ultimately show ?case using wt⇩₁ wt⇩₂ TryCatch.prems "class"
    by (simp add:after_def)(erule_tac x=0 in meta_allE, simp)
next
  case (Synchronized E A ST i e1 e2)
  note wt = ‹P,E ⊢1 sync⇘i⇙ (e1) e2 :: T›
  then obtain U where wt1: "P,E ⊢1 e1 :: U"
    and U: "is_refT U" "U ≠ NT"
    and wt2: "P,E@[Class Object] ⊢1 e2 :: T" by auto
  from ‹ℬ (sync⇘i⇙ (e1) e2) (length E)› have [simp]: "i = length E"
    and B1: "ℬ e1 (length E)" and B2: "ℬ e2 (length (E@[Class Object]))" by auto
  
  note lenST = ‹length ST + max_stack (sync⇘i⇙ (e1) e2) ≤ mxs› 
  note lenE = ‹length E + max_vars (sync⇘i⇙ (e1) e2) ≤ mxl›

  let ?A1 = "A ⊔ 𝒜 e1" let ?A2 = "?A1 ⊔ ⌊{i}⌋"
  let ?A3 = "?A2 ⊔ 𝒜 e2" let ?A4 = "?A1 ⊔ 𝒜 e2"
  let ?E1 = "E @ [Class Object]"
  let ?τ = "ty⇩_i' ST E A" let ?τs1 = "compT E A ST e1"
  let ?τ1 = "ty⇩_i' (U#ST) E ?A1"
  let ?τ1' = "ty⇩_i' (Class Object # Class Object # ST) E ?A1"
  let ?τ1'' = "ty⇩_i' (Class Object#ST) ?E1 ?A2"
  let ?τ1''' = "ty⇩_i' ST ?E1 ?A2"
  let ?τs2 = "compT ?E1 ?A2 ST e2"
  let ?τ2 = "ty⇩_i' (T#ST) ?E1 ?A3" let ?τ2' = "ty⇩_i' (Class Object#T#ST) ?E1 ?A3"
  let ?τ2'' = ?τ2
  let ?τ3 = "ty⇩_i' (Class Throwable#ST) ?E1 ?A2"
  let ?τ3' = "ty⇩_i' (Class Object#Class Throwable#ST) ?E1 ?A2"
  let ?τ3'' = ?τ3
  let ?τ' = "ty⇩_i' (T#ST) E ?A4"

  from lenE lenST max_stack1[of e2] U 
  have "⊢ [Load i, MExit, ThrowExc], [] [::] [?τ3, ?τ3', ?τ3'', ?τ']"
    by(auto simp add: ty⇩_i'_def ty⇩_l_def wt_defs hyperset_defs nth_Cons split: nat.split)
  also have "P,T⇩_r,mxs,5,[] ⊢ Goto 4,0 :: [?τ2'', ?τ3, ?τ3', ?τ3'', ?τ']"
    by(auto simp: hyperset_defs ty⇩_i'_def wt_defs intro: ty⇩_l_antimono ty⇩_l_incr)
  also have "P,T⇩_r,mxs,6,[] ⊢ MExit,0 :: [?τ2', ?τ2'', ?τ3, ?τ3', ?τ3'', ?τ']"
    by(auto simp: hyperset_defs ty⇩_i'_def wt_defs intro: ty⇩_l_antimono ty⇩_l_incr)
  also from lenE lenST max_stack1[of e2]
  have "P,T⇩_r,mxs,7,[] ⊢ Load i,0 :: [?τ2, ?τ2', ?τ2'', ?τ3, ?τ3', ?τ3'', ?τ']"
    by(auto simp: hyperset_defs ty⇩_i'_def wt_defs ty⇩_l_def intro: ty⇩_l_antimono)
  also from ‹𝒟 (sync⇘i⇙ (e1) e2) A› have "𝒟 e2 (A ⊔ 𝒜 e1 ⊔ ⌊{length E}⌋)"
    by(auto elim!: D_mono' simp add: hyperset_defs)
  with ‹PROP ?P e2 ?E1 T ?A2 ST› Synchronized wt2 is_class_Object[OF wf_prog]
  have "⊢ compE2 e2, compxE2 e2 0 (size ST) [::] ?τ1'''#?τs2@[?τ2]"
    by(auto simp add: after_def)
  finally have "⊢ (compE2 e2 @ [Load i, MExit, Goto 4]) @ [Load i, MExit, ThrowExc], compxE2 e2 0 (size ST) [::]
             (?τ1''' # ?τs2 @ [?τ2, ?τ2', ?τ2'']) @ [?τ3, ?τ3', ?τ3'', ?τ']"
    by(simp)
  hence "⊢ (compE2 e2 @ [Load i, MExit, Goto 4]) @ [Load i, MExit, ThrowExc],
           compxE2 e2 0 (size ST) @ [(0, size (compE2 e2 @ [Load i, MExit, Goto 4]) - Suc 2, None, size (compE2 e2 @ [Load i, MExit, Goto 4]), size ST)] [::]
           (?τ1''' # ?τs2 @ [?τ2, ?τ2', ?τ2'']) @ [?τ3, ?τ3', ?τ3'', ?τ']"
  proof(rule wt_instrs_xapp_Any)
    from lenST show "length ST < mxs" by simp
  next
    show "∀τ∈set (?τ1''' # ?τs2 @ [?τ2, ?τ2', ?τ2'']). ∀ST' LT'.
          τ = ⌊(ST', LT')⌋ ⟶ length ST ≤ length ST' ∧
          P ⊢ ⌊(drop (length ST' - length ST) ST',  LT')⌋ ≤' ty⇩_i' ST (E @ [Class Object]) ?A2"
    proof(intro strip)
      fix τ ST' LT'
      assume "τ∈set (?τ1''' # ?τs2 @ [?τ2, ?τ2', ?τ2''])" "τ = ⌊(ST', LT')⌋"
      hence τ: "⌊(ST', LT')⌋ ∈ set (?τ1''' # ?τs2 @ [?τ2, ?τ2', ?τ2''])" by simp
      show "length ST ≤ length ST' ∧ P ⊢ ⌊(drop (length ST' - length ST) ST',  LT')⌋ ≤' ty⇩_i' ST (E @ [Class Object]) ?A2"
      proof(cases "⌊(ST', LT')⌋ ∈ set ?τs2")
        case True
        from compT_ST_prefix[OF suffix_order.order_refl this] compT_LT_prefix[OF this B2]
        show ?thesis unfolding postfix_conv_eq_length_drop by(simp add: ty⇩_i'_def)
      next
        case False
        with τ show ?thesis
          by(auto simp add: ty⇩_i'_def hyperset_defs intro: ty⇩_l_antimono)
      qed
    qed
  qed simp
  hence "⊢ compE2 e2 @ [Load i, MExit, Goto 4, Load i, MExit, ThrowExc],
           compxE2 e2 0 (size ST) @ [(0, size (compE2 e2), None, Suc (Suc (Suc (size (compE2 e2)))), size ST)] [::]
           ?τ1''' # ?τs2 @ [?τ2, ?τ2', ?τ2'', ?τ3, ?τ3', ?τ3'', ?τ']" by simp
  also from wt1 ‹set E ⊆ types P› have "is_type P U" by(rule WT1_is_type[OF wf_prog])
  with U have "P ⊢ U ≤ Class Object" by(auto elim!: is_refT.cases intro: subcls_C_Object[OF _ wf_prog] widen_array_object)
  with lenE lenST max_stack1[of e2]
  have "⊢ [Dup, Store i, MEnter], [] [::] [?τ1, ?τ1', ?τ1''] @ [?τ1''']"
    by(auto simp add: ty⇩_i'_def ty⇩_l_def wt_defs hyperset_defs nth_Cons nth_list_update list_all2_conv_all_nth split: nat.split)
  finally have "⊢ Dup # Store i # MEnter # compE2 e2 @ [Load i, MExit, Goto 4, Load i, MExit, ThrowExc],
               compxE2 e2 3 (size ST) @ [(3, 3 + size (compE2 e2), None, 6 + size (compE2 e2), size ST)]
            [::] ?τ1 # ?τ1' # ?τ1'' # ?τ1''' # ?τs2 @ [?τ2, ?τ2', ?τ2'', ?τ3, ?τ3', ?τ3'', ?τ']"
    by(simp add: eval_nat_numeral shift_def)
  also from ‹PROP ?P e1 E U A ST› wt1 B1 ‹𝒟 (sync⇘i⇙ (e1) e2) A› lenE lenST ‹set E ⊆ types P›
  have "⊢ compE2 e1, compxE2 e1 0 (size ST) [::] ?τ#?τs1@[?τ1]"
    by(auto simp add: after_def)
  finally show ?case using wt1 wt2 wt by(simp add: after_def ac_simps shift_Cons_tuple hyperUn_assoc)
next
  case new thus ?case by(auto simp add:after_def wt_New)
next
  case (BinOp E A ST e⇩₁ bop e⇩₂) 
  have T: "P,E ⊢1 e⇩₁ «bop» e⇩₂ :: T" by fact
  then obtain T⇩₁ T⇩₂ where T⇩₁: "P,E ⊢1 e⇩₁ :: T⇩₁" and T⇩₂: "P,E ⊢1 e⇩₂ :: T⇩₂" and 
    bopT: "P ⊢ T⇩₁«bop»T⇩₂ :: T" by auto
  let ?A⇩₁ = "A ⊔ 𝒜 e⇩₁" let ?A⇩₂ = "?A⇩₁ ⊔ 𝒜 e⇩₂"
  let ?τ = "ty⇩_i' ST E A" let ?τs⇩₁ = "compT E A ST e⇩₁"
  let ?τ⇩₁ = "ty⇩_i' (T⇩₁#ST) E ?A⇩₁" let ?τs⇩₂ = "compT E ?A⇩₁ (T⇩₁#ST) e⇩₂"
  let ?τ⇩₂ = "ty⇩_i' (T⇩₂#T⇩₁#ST) E ?A⇩₂" let ?τ' = "ty⇩_i' (T#ST) E ?A⇩₂"
  from bopT have "⊢ [BinOpInstr bop],[] [::] [?τ⇩₂,?τ']" by(rule wt_BinOpInstr)
  also from BinOp.hyps(2)[of T⇩₂] BinOp.prems T⇩₂ T⇩₁
  have "⊢ compE2 e⇩₂, compxE2 e⇩₂ 0 (size (ty E e⇩₁#ST)) [::] ?τ⇩₁#?τs⇩₂@[?τ⇩₂]" by (auto simp: after_def)
  also from BinOp T⇩₁ have "⊢ compE2 e⇩₁, compxE2 e⇩₁ 0 (size ST) [::] ?τ#?τs⇩₁@[?τ⇩₁]" 
    by (auto simp: after_def)
  finally show ?case using T T⇩₁ T⇩₂ by (simp add: after_def hyperUn_assoc)
next
  case (Cons E A ST e es)
  have "P,E ⊢1 e # es [::] Ts" by fact
  then obtain T⇩_e Ts' where 
    T⇩_e: "P,E ⊢1 e :: T⇩_e" and Ts': "P,E ⊢1 es [::] Ts'" and
    Ts: "Ts = T⇩_e#Ts'" by auto
  let ?A⇩_e = "A ⊔ 𝒜 e"  
  let ?τ = "ty⇩_i' ST E A" let ?τs⇩_e = "compT E A ST e"  
  let ?τ⇩_e = "ty⇩_i' (T⇩_e#ST) E ?A⇩_e" let ?τs' = "compTs E ?A⇩_e (T⇩_e#ST) es"
  let ?τs = "?τ # ?τs⇩_e @ (?τ⇩_e # ?τs')"
  from Cons.hyps(2) Cons.prems T⇩_e Ts'
  have "⊢ compEs2 es, compxEs2 es 0 (size (T⇩_e#ST)) [::] ?τ⇩_e#?τs'" by (simp add: after_def)
  also from Cons T⇩_e have "⊢ compE2 e, compxE2 e 0 (size ST) [::] ?τ#?τs⇩_e@[?τ⇩_e]" by (auto simp: after_def)
  moreover
  from Cons.hyps(2)[OF Ts'] Cons.prems T⇩_e Ts' Ts
  have "last ?τs = ty⇩_i' (rev Ts@ST) E (?A⇩_e ⊔ 𝒜s es)" by simp
  ultimately show ?case using T⇩_e
    by(auto simp add: after_def hyperUn_assoc shift_compxEs2 stack_xlift_compxEs2 simp del: compxE2_size_convs compxEs2_size_convs compxEs2_stack_xlift_convs compxE2_stack_xlift_convs intro: wt_instrs_app2)
next
  case (FAss E A ST e⇩₁ F D e⇩₂)
  hence Void: "P,E ⊢1 e⇩₁∙F{D} := e⇩₂ :: Void" by auto
  then obtain U C T T' fm where    
    C: "P,E ⊢1 e⇩₁ :: U" and U: "class_type_of' U = ⌊C⌋" and sees: "P ⊢ C sees F:T (fm) in D" and
    T': "P,E ⊢1 e⇩₂ :: T'" and T'_T: "P ⊢ T' ≤ T" by auto
  let ?A⇩₁ = "A ⊔ 𝒜 e⇩₁" let ?A⇩₂ = "?A⇩₁ ⊔ 𝒜 e⇩₂"  
  let ?τ = "ty⇩_i' ST E A" let ?τs⇩₁ = "compT E A ST e⇩₁"
  let ?τ⇩₁ = "ty⇩_i' (U#ST) E ?A⇩₁" let ?τs⇩₂ = "compT E ?A⇩₁ (U#ST) e⇩₂"
  let ?τ⇩₂ = "ty⇩_i' (T'#U#ST) E ?A⇩₂" let ?τ⇩₃ = "ty⇩_i' ST E ?A⇩₂"
  let ?τ' = "ty⇩_i' (Void#ST) E ?A⇩₂"
  from FAss.prems sees T'_T U
  have "⊢ [Putfield F D,Push Unit],[] [::] [?τ⇩₂,?τ⇩₃,?τ']"
    by (fastforce simp add: wt_Push wt_Put)
  also from FAss.hyps(2)[of T'] FAss.prems T' C
  have "⊢ compE2 e⇩₂, compxE2 e⇩₂ 0 (size ST+1) [::] ?τ⇩₁#?τs⇩₂@[?τ⇩₂]"
    by (auto simp add: after_def hyperUn_assoc) 
  also from FAss C have "⊢ compE2 e⇩₁, compxE2 e⇩₁ 0 (size ST) [::] ?τ#?τs⇩₁@[?τ⇩₁]" 
    by (auto simp add: after_def)
  finally show ?case using Void C T' by (simp add: after_def hyperUn_assoc) 
next
  case Val thus ?case by(auto simp:after_def wt_Push)
next
  case (Cast T exp) thus ?case by (auto simp:after_def wt_Cast)
next
  case (InstanceOf E A ST e) thus ?case
    by(auto simp:after_def intro!: wt_Instanceof wt_instrs_app3 intro: widen_refT refT_widen)
next
  case (BlockNone E A ST i Ti e)
  from ‹P,E ⊢1 {i:Ti=None; e} :: T› have wte: "P,E@[Ti] ⊢1 e :: T"
    and Ti: "is_type P Ti" by auto
  let ?τs = "ty⇩_i' ST E A # compT (E @ [Ti]) (A⊖i) ST e"
  from BlockNone wte Ti
  have "⊢ compE2 e, compxE2 e 0 (size ST) [::] ?τs @ [ty⇩_i' (T#ST) (E@[Ti]) (A⊖(size E) ⊔ 𝒜 e)]"
    by(auto simp add: after_def)
  also have "P ⊢ ty⇩_i' (T # ST) (E@[Ti]) (A ⊖ size E ⊔ 𝒜 e) ≤' ty⇩_i' (T # ST) (E@[Ti]) ((A ⊔ 𝒜 e) ⊖ size E)"
    by(auto simp add:hyperset_defs intro: ty⇩_i'_antimono)
  also have "… = ty⇩_i' (T # ST) E (A ⊔ 𝒜 e)" by simp
  also have "P ⊢ … ≤' ty⇩_i' (T # ST) E (A ⊔ (𝒜 e ⊖ i))"
    by(auto simp add:hyperset_defs intro: ty⇩_i'_antimono)
  finally show ?case using BlockNone.prems by(simp add: after_def)
next
  case (BlockSome E A ST i Ti v e)
  from ‹P,E ⊢1 {i:Ti=⌊v⌋; e} :: T› obtain Tv
    where Tv: "P,E ⊢1 Val v :: Tv" "P ⊢ Tv ≤ Ti"
    and wte: "P,E@[Ti] ⊢1 e :: T"
    and Ti: "is_type P Ti" by auto
  from ‹length ST + max_stack {i:Ti=⌊v⌋; e} ≤ mxs›
  have lenST: "length ST + max_stack e ≤ mxs" by simp
  from ‹length E + max_vars {i:Ti=⌊v⌋; e} ≤ mxl›
  have lenE: "length (E@[Ti]) + max_vars e ≤ mxl" by simp
  from ‹ℬ {i:Ti=⌊v⌋; e} (length E)› have [simp]: "i = length E"
    and B: "ℬ e (length (E@[Ti]))" by auto


  from BlockSome wte
  have "⊢ compE2 e, compxE2 e 0 (size ST) [::] (ty⇩_i' ST (E @ [Ti]) (A ⊔ ⌊{length E}⌋) # compT (E @ [Ti]) (A ⊔ ⌊{i}⌋) ST e) @ [ty⇩_i' (T#ST) (E@[Ti]) (A ⊔ ⌊{size E}⌋ ⊔ 𝒜 e)]"
    by(auto simp add: after_def)
  also have "P ⊢ ty⇩_i' (T # ST) (E @ [Ti]) (A ⊔ ⌊{length E}⌋ ⊔ 𝒜 e) ≤' ty⇩_i' (T # ST) (E @ [Ti]) ((A ⊔ 𝒜 e) ⊖ length E)"
    by(auto simp add: hyperset_defs intro: ty⇩_i'_antimono)
  also have "… = ty⇩_i' (T # ST) E (A ⊔ 𝒜 e)" by simp
  also have "P ⊢ … ≤' ty⇩_i' (T # ST) E (A ⊔ (𝒜 e ⊖ i))"
    by(auto simp add:hyperset_defs intro: ty⇩_i'_antimono)
  also note append_Cons
  also {
    from lenST max_stack1[of e] Tv
    have "⊢ [Push v], [] [::] [ty⇩_i' ST E A, ty⇩_i' (ty E (Val v) # ST) E A]"
      by(auto intro: wt_Push)
    moreover from Tv lenE
    have "⊢ [Store (length E)], [] [::] [ty⇩_i' (Tv # ST) (E @ [Ti]) (A ⊖ length E), ty⇩_i' ST (E @ [Ti]) (⌊{length E}⌋ ⊔ (A ⊖ length E))]"
      by -(rule wt_Store, auto)
    moreover have "ty⇩_i' (Tv # ST) (E @ [Ti]) (A ⊖ length E) = ty⇩_i' (Tv # ST) E A" by(simp add: ty⇩_i'_def)
    moreover have "⌊{length E}⌋ ⊔ (A ⊖ length E) = A ⊔ ⌊{length E}⌋" by(simp add: hyperset_defs)
    ultimately have "⊢ [Push v, Store (length E)], [] [::] [ty⇩_i' ST E A, ty⇩_i' (Tv # ST) E A, ty⇩_i' ST (E @ [Ti]) (A ⊔ ⌊{length E}⌋)]"
      using Tv by(auto intro: wt_instrs_Cons3)
  }
  finally show ?case using Tv ‹P,E ⊢1 {i:Ti=⌊v⌋; e} :: T› wte by(simp add: after_def)
next
  case Var thus ?case by(auto simp:after_def wt_Load)
next
  case FAcc thus ?case by(auto simp:after_def wt_Get)
next
  case (LAss E A ST i e) thus ?case using max_stack1[of e]
    by(auto simp: hyper_insert_comm after_def wt_Store wt_Push simp del: hyperUn_comm hyperUn_leftComm)
next
  case Nil thus ?case by auto
next
  case throw thus ?case by(auto simp add: after_def wt_Throw)
next
  case (While E A ST e c)
  obtain Tc where wte: "P,E ⊢1 e :: Boolean" and wtc: "P,E ⊢1 c :: Tc"
    and [simp]: "T = Void" using While by auto
  have [simp]: "ty E (while (e) c) = Void" using While by simp
  let ?A⇩₀ = "A ⊔ 𝒜 e" let ?A⇩₁ = "?A⇩₀ ⊔ 𝒜 c"
  let ?τ = "ty⇩_i' ST E A" let ?τs⇩_e = "compT E A ST e"
  let ?τ⇩_e = "ty⇩_i' (Boolean#ST) E ?A⇩₀" let ?τ⇩₁ = "ty⇩_i' ST E ?A⇩₀"
  let ?τs⇩_c = "compT E ?A⇩₀ ST c" let ?τ⇩_c = "ty⇩_i' (Tc#ST) E ?A⇩₁"
  let ?τ⇩₂ = "ty⇩_i' ST E ?A⇩₁" let ?τ' = "ty⇩_i' (Void#ST) E ?A⇩₀"
  let ?τs = "(?τ # ?τs⇩_e @ [?τ⇩_e]) @ ?τ⇩₁ # ?τs⇩_c @ [?τ⇩_c, ?τ⇩₂, ?τ⇩₁, ?τ']"
  have "⊢ [],[] [::] [] @ ?τs" by(simp add:wt_instrs_def)
  also
  from While.hyps(1)[of Boolean] While.prems
  have "⊢ compE2 e,compxE2 e 0 (size ST) [::] ?τ # ?τs⇩_e @ [?τ⇩_e]"
    by (auto simp:after_def)
  also
  have "[] @ ?τs = (?τ # ?τs⇩_e) @ ?τ⇩_e # ?τ⇩₁ # ?τs⇩_c @ [?τ⇩_c,?τ⇩₂,?τ⇩₁,?τ']" by simp
  also
  let ?n⇩_e = "size(compE2 e)"  let ?n⇩_c = "size(compE2 c)"
  let ?if = "IfFalse (int ?n⇩_c + 3)"
  have "⊢ [?if],[] [::] ?τ⇩_e # ?τ⇩₁ # ?τs⇩_c @ [?τ⇩_c, ?τ⇩₂, ?τ⇩₁, ?τ']"
    by(simp add: wt_instr_Cons wt_instr_append wt_IfFalse
                 nat_add_distrib split: nat_diff_split)
  also
  have "(?τ # ?τs⇩_e) @ (?τ⇩_e # ?τ⇩₁ # ?τs⇩_c @ [?τ⇩_c, ?τ⇩₂, ?τ⇩₁, ?τ']) = ?τs" by simp
  also from While.hyps(2)[of Tc] While.prems wtc
  have "⊢ compE2 c,compxE2 c 0 (size ST) [::] ?τ⇩₁ # ?τs⇩_c @ [?τ⇩_c]"
    by (auto simp:after_def)
  also have "?τs = (?τ # ?τs⇩_e @ [?τ⇩_e,?τ⇩₁] @ ?τs⇩_c) @ [?τ⇩_c,?τ⇩₂,?τ⇩₁,?τ']" by simp
  also have "⊢ [Pop],[] [::] [?τ⇩_c, ?τ⇩₂]"  by(simp add:wt_Pop)
  also have "(?τ # ?τs⇩_e @ [?τ⇩_e,?τ⇩₁] @ ?τs⇩_c) @ [?τ⇩_c,?τ⇩₂,?τ⇩₁,?τ'] = ?τs" by simp
  also let ?go = "Goto (-int(?n⇩_c+?n⇩_e+2))"
  have "P ⊢ ?τ⇩₂ ≤' ?τ" by(fastforce intro: ty⇩_i'_antimono simp: hyperset_defs)
  hence "P,T⇩_r,mxs,size ?τs,[] ⊢ ?go,?n⇩_e+?n⇩_c+2 :: ?τs"
    by(simp add: wt_Goto split: nat_diff_split)
  also have "?τs = (?τ # ?τs⇩_e @ [?τ⇩_e,?τ⇩₁] @ ?τs⇩_c @ [?τ⇩_c, ?τ⇩₂]) @ [?τ⇩₁, ?τ']"
    by simp
  also have "⊢ [Push Unit],[] [::] [?τ⇩₁,?τ']"
    using While.prems max_stack1[of c] by(auto simp add:wt_Push)
  finally show ?case using wtc wte
    by (simp add:after_def)
next
  case (Cond E A ST e e⇩₁ e⇩₂)
  obtain T⇩₁ T⇩₂ where wte: "P,E ⊢1 e :: Boolean"
    and wt⇩₁: "P,E ⊢1 e⇩₁ :: T⇩₁" and wt⇩₂: "P,E ⊢1 e⇩₂ :: T⇩₂"
    and sub⇩₁: "P ⊢ T⇩₁ ≤ T" and sub⇩₂: "P ⊢ T⇩₂ ≤ T"
    using Cond by(auto dest: is_lub_upper)
  have [simp]: "ty E (if (e) e⇩₁ else e⇩₂) = T" using Cond by simp
  let ?A⇩₀ = "A ⊔ 𝒜 e" let ?A⇩₂ = "?A⇩₀ ⊔ 𝒜 e⇩₂" let ?A⇩₁ = "?A⇩₀ ⊔ 𝒜 e⇩₁"
  let ?A' = "?A⇩₀ ⊔ 𝒜 e⇩₁ ⊓ 𝒜 e⇩₂"
  let ?τ⇩₂ = "ty⇩_i' ST E ?A⇩₀" let ?τ' = "ty⇩_i' (T#ST) E ?A'"
  let ?τs⇩₂ = "compT E ?A⇩₀ ST e⇩₂"
  have "PROP ?P e⇩₂ E T⇩₂ ?A⇩₀ ST" by fact
  hence "⊢ compE2 e⇩₂, compxE2 e⇩₂ 0 (size ST) [::] (?τ⇩₂#?τs⇩₂) @ [ty⇩_i' (T⇩₂#ST) E ?A⇩₂]"
    using Cond.prems wt⇩₂ by(auto simp add:after_def)
  also have "P ⊢ ty⇩_i' (T⇩₂#ST) E ?A⇩₂ ≤' ?τ'" using sub⇩₂
    by(auto simp add: hyperset_defs ty⇩_i'_def intro!: ty⇩_l_antimono)
  also
  let ?τ⇩₃ = "ty⇩_i' (T⇩₁ # ST) E ?A⇩₁"
  let ?g⇩₂ = "Goto(int (size (compE2 e⇩₂) + 1))"
  from sub⇩₁ have "P,T⇩_r,mxs,size(compE2 e⇩₂)+2,[] ⊢ ?g⇩₂,0 :: ?τ⇩₃#(?τ⇩₂#?τs⇩₂)@[?τ']"
    by(cases "length (compE2 e⇩₂)")
      (auto simp: hyperset_defs wt_defs nth_Cons ty⇩_i'_def neq_Nil_conv
             split:nat.split intro!: ty⇩_l_antimono)
  also let ?τs⇩₁ = "compT E ?A⇩₀ ST e⇩₁"
  have "PROP ?P e⇩₁ E T⇩₁ ?A⇩₀ ST" by fact
  hence "⊢ compE2 e⇩₁,compxE2 e⇩₁ 0 (size ST) [::] ?τ⇩₂ # ?τs⇩₁ @ [?τ⇩₃]"
    using Cond.prems wt⇩₁ by(auto simp add:after_def)
  also
  let ?τs⇩₁⇩₂ = "?τ⇩₂ # ?τs⇩₁ @ ?τ⇩₃ # (?τ⇩₂ # ?τs⇩₂) @ [?τ']"
  let ?τ⇩₁ = "ty⇩_i' (Boolean#ST) E ?A⇩₀"
  let ?g⇩₁ = "IfFalse(int (size (compE2 e⇩₁) + 2))"
  let ?code = "compE2 e⇩₁ @ ?g⇩₂ # compE2 e⇩₂"
  have "⊢ [?g⇩₁],[] [::] [?τ⇩₁] @ ?τs⇩₁⇩₂"
    by(simp add: wt_IfFalse nat_add_distrib split:nat_diff_split)
  also (wt_instrs_ext2) have "[?τ⇩₁] @ ?τs⇩₁⇩₂ = ?τ⇩₁ # ?τs⇩₁⇩₂" by simp also
  let ?τ = "ty⇩_i' ST E A"
  have "PROP ?P e E Boolean A ST" by fact
  hence "⊢ compE2 e, compxE2 e 0 (size ST) [::] ?τ # compT E A ST e @ [?τ⇩₁]"
    using Cond.prems wte by(auto simp add:after_def)
  finally show ?case using wte wt⇩₁ wt⇩₂ by(simp add:after_def hyperUn_assoc)
next
  case (Call E A ST e M es)
  from ‹P,E ⊢1 e∙M(es) :: T›
  obtain U C D Ts m Ts'
    where C: "P,E ⊢1 e :: U"
    and icto: "class_type_of' U = ⌊C⌋"
    and "method": "P ⊢ C sees M:Ts → T = m in D"
    and wtes: "P,E ⊢1 es [::] Ts'" and subs: "P ⊢ Ts' [≤] Ts"
    by(cases) auto
  from wtes have same_size: "size es = size Ts'" by(rule WTs1_same_size)
  let ?A⇩₀ = "A ⊔ 𝒜 e" let ?A⇩₁ = "?A⇩₀ ⊔ 𝒜s es"
  let ?τ = "ty⇩_i' ST E A" let ?τs⇩_e = "compT E A ST e"
  let ?τ⇩_e = "ty⇩_i' (U # ST) E ?A⇩₀"
  let ?τs⇩_e⇩_s = "compTs E ?A⇩₀ (U # ST) es"
  let ?τ⇩₁ = "ty⇩_i' (rev Ts' @ U # ST) E ?A⇩₁"
  let ?τ' = "ty⇩_i' (T # ST) E ?A⇩₁"
  have "⊢ [Invoke M (size es)],[] [::] [?τ⇩₁,?τ']"
    by(rule wt_Invoke[OF same_size icto "method" subs])
  also
  from Call.hyps(2)[of Ts'] Call.prems wtes C
  have "⊢ compEs2 es,compxEs2 es 0 (size ST+1) [::] ?τ⇩_e # ?τs⇩_e⇩_s"
    "last (?τ⇩_e # ?τs⇩_e⇩_s) = ?τ⇩₁"
    by(auto simp add:after_def)
  also have "(?τ⇩_e # ?τs⇩_e⇩_s) @ [?τ'] = ?τ⇩_e # ?τs⇩_e⇩_s @ [?τ']" by simp
  also have "⊢ compE2 e,compxE2 e 0 (size ST) [::] ?τ # ?τs⇩_e @ [?τ⇩_e]"
    using Call C by(auto simp add:after_def)
  finally show ?case using Call.prems C
    by(simp add:after_def hyperUn_assoc shift_compxEs2 stack_xlift_compxEs2 del: compxEs2_stack_xlift_convs compxEs2_size_convs)
next
  case Seq thus ?case
    by(auto simp:after_def)
      (fastforce simp:wt_Push wt_Pop hyperUn_assoc
                intro:wt_instrs_app2 wt_instrs_Cons)
next
  case (NewArray E A ST Ta e)
  from ‹P,E ⊢1 newA Ta⌊e⌉ :: T›
  have "⊢ [NewArray Ta], [] [::] [ty⇩_i' (Integer # ST) E (A ⊔ 𝒜 e), ty⇩_i' (Ta⌊⌉ # ST) E (A ⊔ 𝒜 e)]"
    by(auto simp:hyperset_defs ty⇩_i'_def wt_defs ty⇩_l_def)
  with NewArray show ?case by(auto simp: after_def intro: wt_instrs_app3)
next
  case (ALen E A ST exp)
  { fix T
    have "⊢ [ALength], [] [::] [ty⇩_i' (T⌊⌉ # ST) E (A ⊔ 𝒜 exp), ty⇩_i' (Integer # ST) E (A ⊔ 𝒜 exp)]"
      by(auto simp:hyperset_defs ty⇩_i'_def wt_defs ty⇩_l_def) }
  with ALen show ?case by(auto simp add: after_def)(rule wt_instrs_app2, auto)
next
  case (AAcc E A ST a i)
  from ‹P,E ⊢1 a⌊i⌉ :: T› have wta: "P,E ⊢1 a :: T⌊⌉" and wti: "P,E ⊢1 i :: Integer" by auto
  let ?A1 = "A ⊔ 𝒜 a" let ?A2 = "?A1 ⊔ 𝒜 i"  
  let ?τ = "ty⇩_i' ST E A" let ?τsa = "compT E A ST a"
  let ?τ1 = "ty⇩_i' (T⌊⌉#ST) E ?A1" let ?τsi = "compT E ?A1 (T⌊⌉#ST) i"
  let ?τ2 = "ty⇩_i' (Integer#T⌊⌉#ST) E ?A2" let ?τ' = "ty⇩_i' (T#ST) E ?A2"
  have "⊢ [ALoad], [] [::] [?τ2,?τ']" by(auto simp add: ty⇩_i'_def wt_defs)
  also from AAcc.hyps(2)[of Integer] AAcc.prems wti wta
  have "⊢ compE2 i, compxE2 i 0 (size ST+1) [::] ?τ1#?τsi@[?τ2]"
    by(auto simp add: after_def)
  also from wta AAcc have "⊢ compE2 a, compxE2 a 0 (size ST) [::] ?τ#?τsa@[?τ1]" 
    by(auto simp add: after_def)
  finally show ?case using wta wti ‹P,E ⊢1 a⌊i⌉ :: T› by(simp add: after_def hyperUn_assoc)
next
  case (AAss E A ST a i e)
  note wt = ‹P,E ⊢1 a⌊i⌉ := e :: T›
  then obtain Ta U where wta: "P,E ⊢1 a :: Ta⌊⌉" and wti: "P,E ⊢1 i :: Integer"
    and wte: "P,E ⊢1 e :: U" and U: "P ⊢ U ≤ Ta" and [simp]: "T = Void" by auto
  let ?A1 = "A ⊔ 𝒜 a" let ?A2 = "?A1 ⊔ 𝒜 i" let ?A3 = "?A2 ⊔ 𝒜 e"
  let ?τ = "ty⇩_i' ST E A" let ?τsa = "compT E A ST a"
  let ?τ1 = "ty⇩_i' (Ta⌊⌉#ST) E ?A1" let ?τsi = "compT E ?A1 (Ta⌊⌉#ST) i"
  let ?τ2 = "ty⇩_i' (Integer#Ta⌊⌉#ST) E ?A2" let ?τse = "compT E ?A2 (Integer#Ta⌊⌉#ST) e"
  let ?τ3 = "ty⇩_i' (U#Integer#Ta⌊⌉#ST) E ?A3" let ?τ4 = "ty⇩_i' ST E ?A3"
  let ?τ' = "ty⇩_i' (Void#ST) E ?A3"
  from ‹length ST + max_stack (a⌊i⌉ := e) ≤ mxs›
  have "⊢ [AStore, Push Unit], [] [::] [?τ3,?τ4,?τ']"
    by(auto simp add: ty⇩_i'_def wt_defs nth_Cons split: nat.split)
  also from AAss.hyps(3)[of U] wte AAss.prems wta wti
  have "⊢ compE2 e, compxE2 e 0 (size ST+2) [::] ?τ2#?τse@[?τ3]"
    by(auto simp add: after_def)
  also from AAss.hyps(2)[of Integer] wti wta AAss.prems
  have "⊢ compE2 i, compxE2 i 0 (size ST+1) [::] ?τ1#?τsi@[?τ2]"
    by(auto simp add: after_def)
  also from wta AAss have "⊢ compE2 a, compxE2 a 0 (size ST) [::] ?τ#?τsa@[?τ1]" 
    by(auto simp add: after_def)
  finally show ?case using wta wti wte ‹P,E ⊢1 a⌊i⌉ := e :: T›
    by(simp add: after_def hyperUn_assoc)
next
  case (CompareAndSwap E A ST e1 D F e2 e3)
  note wt = ‹P,E ⊢1 e1∙compareAndSwap(D∙F, e2, e3) :: T›
  then obtain T1 T2 T3 C fm T' where [simp]: "T = Boolean"
    and wt1: "P,E ⊢1 e1 :: T1" "class_type_of' T1 = ⌊C⌋" "P ⊢ C sees F:T' (fm) in D" "volatile fm"
    and wt2: "P,E ⊢1 e2 :: T2" "P ⊢ T2 ≤ T'" and wt3: "P,E ⊢1 e3 :: T3" "P ⊢ T3 ≤ T'"
    by auto
  let ?A1 = "A ⊔ 𝒜 e1" let ?A2 = "?A1 ⊔ 𝒜 e2" let ?A3 = "?A2 ⊔ 𝒜 e3"
  let ?τ = "ty⇩_i' ST E A" let ?τs1 = "compT E A ST e1"
  let ?τ1 = "ty⇩_i' (T1#ST) E ?A1" let ?τs2 = "compT E ?A1 (T1#ST) e2"
  let ?τ2 = "ty⇩_i' (T2#T1#ST) E ?A2" let ?τs3 = "compT E ?A2 (T2#T1#ST) e3"
  let ?τ3 = "ty⇩_i' (T3#T2#T1#ST) E ?A3"
  let ?τ' = "ty⇩_i' (Boolean#ST) E ?A3"
  from ‹length ST + max_stack (e1∙compareAndSwap(D∙F, e2, e3)) ≤ mxs›
  have "⊢ [CAS F D], [] [::] [?τ3,?τ']" using wt1 wt2 wt3
    by(cases T1)(auto simp add: ty⇩_i'_def wt_defs nth_Cons split: nat.split intro: sees_field_idemp widen_trans[OF widen_array_object] dest: sees_field_decl_above)
  also from CompareAndSwap.hyps(3)[of T3] wt3 CompareAndSwap.prems wt1 wt2
  have "⊢ compE2 e3, compxE2 e3 0 (size ST+2) [::] ?τ2#?τs3@[?τ3]"
    by(auto simp add: after_def)
  also from CompareAndSwap.hyps(2)[of T2] wt2 wt1 CompareAndSwap.prems
  have "⊢ compE2 e2, compxE2 e2 0 (size ST+1) [::] ?τ1#?τs2@[?τ2]"
    by(auto simp add: after_def)
  also from wt1 CompareAndSwap have "⊢ compE2 e1, compxE2 e1 0 (size ST) [::] ?τ#?τs1@[?τ1]" 
    by(auto simp add: after_def)
  also have "ty E (e1∙compareAndSwap(D∙F, e2, e3)) = T" using wt by(rule ty_def2)
  ultimately show ?case using wt1 wt2 wt3
    by(simp add: after_def hyperUn_assoc)
next
  case (InSynchronized i a exp) thus ?case by auto
qed

end

lemma states_compP [simp]: "states (compP f P) mxs mxl = states P mxs mxl"
by (simp add: JVM_states_unfold)

lemma [simp]: "app⇩_i (i, compP f P, pc, mpc, T, τ) = app⇩_i (i, P, pc, mpc, T, τ)"
proof -
  { fix ST LT
    have "app⇩_i (i, compP f P, pc, mpc, T, (ST, LT)) = app⇩_i (i, P, pc, mpc, T, (ST, LT))"
    proof(cases i)
      case (Invoke M n)
      have "⋀C Ts D. (∃T m. compP f P ⊢ C sees M: Ts→T = m in D) ⟷ (∃T m. P ⊢ C sees M: Ts→T = m in D)"
        by(auto dest!: sees_method_compPD dest: sees_method_compP)
      with Invoke show ?thesis by clarsimp
    qed(simp_all) }
  thus ?thesis by(cases τ) simp
qed

  
lemma [simp]: "is_relevant_entry (compP f P) i = is_relevant_entry P i"
  apply (rule ext)+
  apply (unfold is_relevant_entry_def)
  apply (cases i)
  apply auto
  done

lemma [simp]: "relevant_entries (compP f P) i pc xt = relevant_entries P i pc xt"
by (simp add: relevant_entries_def)

lemma [simp]: "app i (compP f P) mpc T pc mxl xt τ = app i P mpc T pc mxl xt τ"
  apply (simp add: app_def xcpt_app_def eff_def xcpt_eff_def norm_eff_def)
  apply (fastforce simp add: image_def)
  done

lemma [simp]: "app i P mpc T pc mxl xt τ ⟹ eff i (compP f P) pc xt τ = eff i P pc xt τ"
  apply (clarsimp simp add: eff_def norm_eff_def xcpt_eff_def app_def)
  apply (cases i)
  apply(auto)
  done

lemma [simp]: "widen (compP f P) = widen P"
  apply (rule ext)+
  apply (simp)
  done
  
lemma [simp]: "compP f P ⊢ τ ≤' τ' = P ⊢ τ ≤' τ'" (*<*)
by (simp add: sup_state_opt_def sup_state_def sup_ty_opt_def)(*>*)

lemma [simp]: "compP f P,T,mpc,mxl,xt ⊢ i,pc :: τs = P,T,mpc,mxl,xt ⊢ i,pc :: τs"
by (simp add: wt_instr_def cong: conj_cong)

declare TC0.compT_sizes[simp]  TC1.ty_def2[OF TC1.intro, simp]

lemma compT_method:
  fixes e and A and C and Ts and mxl⇩₀
  defines [simp]: "E ≡ Class C # Ts"
      and [simp]: "A ≡ ⌊{..size Ts}⌋"
      and [simp]: "A' ≡ A ⊔ 𝒜 e"
      and [simp]: "mxs ≡ max_stack e"
      and [simp]: "mxl⇩₀ ≡ max_vars e"
      and [simp]: "mxl ≡ 1 + size Ts + mxl⇩₀"
  assumes wf_prog: "wf_prog p P"
  shows "⟦ P,E ⊢1 e :: T; 𝒟 e A; ℬ e (size E); set E ⊆ types P; P ⊢ T ≤ T' ⟧ ⟹
   wt_method (compP2 P) C Ts T' mxs mxl⇩₀ (compE2 e @ [Return]) (compxE2 e 0 0)
      (TC0.ty⇩_i' mxl [] E A # TC0.compTa P mxl E A [] e)"
(*<*)
using wf_prog
apply(simp add:wt_method_def TC0.compTa_def TC0.after_def compP2_def compMb2_def)
apply(rule conjI)
 apply(simp add:check_types_def TC0.OK_ty⇩_i'_in_statesI)
 apply(rule conjI)
  apply(frule WT1_is_type[OF wf_prog])
   apply simp
  apply(insert max_stack1[of e])
  apply(fastforce intro!: TC0.OK_ty⇩_i'_in_statesI)
 apply(erule (1) TC1.compT_states[OF TC1.intro])
    apply simp
   apply simp
  apply simp
 apply simp
apply(rule conjI)
 apply(fastforce simp add:wt_start_def TC0.ty⇩_i'_def TC0.ty⇩_l_def list_all2_conv_all_nth nth_Cons split:nat.split dest:less_antisym)
apply (frule (1) TC3.compT_wt_instrs[OF TC3.intro[OF TC1.intro], where ST = "[]" and mxs = "max_stack e" and mxl = "1 + size Ts + max_vars e"])
     apply simp
    apply simp
   apply simp
  apply simp
 apply simp
apply (clarsimp simp:TC2.wt_instrs_def TC0.after_def)
apply(rule conjI)
 apply (fastforce)
apply(clarsimp)
apply(drule (1) less_antisym)
apply(thin_tac "∀x. P x" for P)
apply(clarsimp simp:TC2.wt_defs xcpt_app_pcs xcpt_eff_pcs TC0.ty⇩_i'_def)
done
(*>*)


definition compTP :: "'addr J1_prog ⇒ ty⇩_P"
where
  "compTP P C M  ≡
  let (D,Ts,T,meth) = method P C M;
       e = the meth;
       E = Class C # Ts;
       A = ⌊{..size Ts}⌋;
       mxl = 1 + size Ts + max_vars e
  in  (TC0.ty⇩_i' mxl [] E A # TC0.compTa P mxl E A [] e)"

theorem wt_compTP_compP2:
  "wf_J1_prog P ⟹ wf_jvm_prog⇘compTP P⇙ (compP2 P)"
  apply (simp add: wf_jvm_prog_phi_def compP2_def compMb2_def)
  apply (rule wf_prog_compPI)
   prefer 2 apply assumption
  apply (clarsimp simp add: wf_mdecl_def)
  apply (simp add: compTP_def)
  apply (rule compT_method [simplified compP2_def compMb2_def, simplified])
       apply assumption+
    apply (drule (1) sees_wf_mdecl)
    apply (simp add: wf_mdecl_def)
   apply (fastforce intro: sees_method_is_class)
  apply assumption
  done


theorem wt_compP2:
  "wf_J1_prog P ⟹ wf_jvm_prog (compP2 P)"
by(auto simp add: wf_jvm_prog_def intro: wt_compTP_compP2)

end