Theory TypeComp

(*  Title:      Jinja/Compiler/TypeComp.thy

    Author:     Tobias Nipkow
    Copyright   TUM 2003
*)

header {* \isaheader{Preservation of Well-Typedness} *}

theory TypeComp
imports Compiler "../BV/BVSpec"
begin

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

locale TC0 =
  fixes P :: "J⇣1_prog" and mxl :: nat
begin

definition "ty E e = (THE T. P,E \<turnstile>⇩1 e :: T)"

definition "ty⇣l E A' = map (λi. if i ∈ A' ∧ i < size E then OK(E!i) else Err) [0..<mxl]"

definition "ty⇣i' ST E A = (case A of None => None | ⌊A'⌋ => Some(ST, ty⇣l E A'))"

definition "after E A ST e = ty⇣i' (ty E e # ST) E (A \<squnion> \<A> e)"

end

lemma (in TC0) ty_def2 [simp]: "P,E \<turnstile>⇩1 e :: T ==> ty E e = T"
(*<*)
apply (unfold ty_def)
apply(blast intro: the_equality WT⇣1_unique)
done
(*>*)

lemma (in TC0) [simp]: "ty⇣i' ST E None = None"
(*<*)by (simp add: ty⇣i'_def)(*>*)

lemma (in TC0) 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 (in TC0) ty⇣i'_app_diff[simp]:
 "ty⇣i' ST (E @ [T]) (A \<ominus> size E) = ty⇣i' ST E A"
(*<*)by(auto simp add:ty⇣i'_def hyperset_defs)(*>*)


lemma (in TC0) ty⇣l_antimono:
 "A ⊆ A' ==> P \<turnstile> ty⇣l E A' [≤⇩\<top>] ty⇣l E A"
(*<*)by(auto simp:ty⇣l_def list_all2_conv_all_nth)(*>*)


lemma (in TC0) ty⇣i'_antimono:
 "A ⊆ A' ==> P \<turnstile> 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 (in TC0) ty⇣l_env_antimono:
 "P \<turnstile> ty⇣l (E@[T]) A [≤⇩\<top>] ty⇣l E A" 
(*<*)by(auto simp:ty⇣l_def list_all2_conv_all_nth)(*>*)


lemma (in TC0) ty⇣i'_env_antimono:
 "P \<turnstile> 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 (in TC0) ty⇣i'_incr:
 "P \<turnstile> 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 (in TC0) ty⇣l_incr:
 "P \<turnstile> ty⇣l (E @ [T]) (insert (size E) A) [≤⇩\<top>] ty⇣l E A"
(*<*)by(auto simp: hyperset_defs ty⇣l_def list_all2_conv_all_nth)(*>*)


lemma (in TC0) 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)(*>*)

locale TC1 = TC0
begin

primrec compT :: "ty list => nat hyperset => ty list => expr⇣1 => ty⇣i' list" and
   compTs :: "ty list => nat hyperset => ty list => expr⇣1 list => ty⇣i' list" where
"compT E A ST (new C) = []"
| "compT E A ST (Cast C e) =  
   compT E A ST e @ [after E A ST e]"
| "compT E A ST (Val v) = []"
| "compT E A ST (e⇣1 «bop» e⇣2) =
  (let ST⇣1 = ty E e⇣1#ST; A⇣1 = A \<squnion> \<A> e⇣1 in
   compT E A ST e⇣1 @ [after E A ST e⇣1] @
   compT E A⇣1 ST⇣1 e⇣2 @ [after E A⇣1 ST⇣1 e⇣2])"
| "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 \<squnion> \<A> e \<squnion> ⌊{i}⌋)]"
| "compT E A ST (e•F{D}) = 
   compT E A ST e @ [after E A ST e]"
| "compT E A ST (e⇣1•F{D} := e⇣2) =
  (let ST⇣1 = ty   E e⇣1#ST; A⇣1 = A \<squnion> \<A> e⇣1; A⇣2 = A⇣1 \<squnion> \<A> e⇣2 in
   compT E A ST e⇣1 @ [after E A ST e⇣1] @
   compT E A⇣1 ST⇣1 e⇣2 @ [after E A⇣1 ST⇣1 e⇣2] @
   [ty⇣i' ST E A⇣2])"
| "compT E A ST {i:T; e} = compT (E@[T]) (A\<ominus>i) ST e"
| "compT E A ST (e⇣1;;e⇣2) =
  (let A⇣1 = A \<squnion> \<A> e⇣1 in
   compT E A ST e⇣1 @ [after E A ST e⇣1, ty⇣i' ST E A⇣1] @
   compT E A⇣1 ST e⇣2)"
| "compT E A ST (if (e) e⇣1 else e⇣2) =
   (let A⇣0 = A \<squnion> \<A> e; τ = ty⇣i' ST E A⇣0 in
    compT E A ST e @ [after E A ST e, τ] @
    compT E A⇣0 ST e⇣1 @ [after E A⇣0 ST e⇣1, τ] @
    compT E A⇣0 ST e⇣2)"
| "compT E A ST (while (e) c) =
   (let A⇣0 = A \<squnion> \<A> e;  A⇣1 = A⇣0 \<squnion> \<A> c; τ = ty⇣i' ST E A⇣0 in
    compT E A ST e @ [after E A ST e, τ] @
    compT E A⇣0 ST c @ [after E A⇣0 ST c, ty⇣i' ST E A⇣1, ty⇣i' ST E A⇣0])"
| "compT E A ST (throw e) = compT E A ST e @ [after E A ST e]"
| "compT E A ST (e•M(es)) =
   compT E A ST e @ [after E A ST e] @
   compTs E (A \<squnion> \<A> e) (ty   E e # ST) es"
| "compT E A ST (try e⇣1 catch(C i) e⇣2) =
   compT E A ST e⇣1 @ [after E A ST e⇣1] @
   [ty⇣i' (Class C#ST) E A, ty⇣i' ST (E@[Class C]) (A \<squnion> ⌊{i}⌋)] @
   compT (E@[Class C]) (A \<squnion> ⌊{i}⌋) ST e⇣2"
| "compTs E A ST [] = []"
| "compTs  E A ST (e#es) = compT E A ST e @ [after E A ST e] @
                            compTs E (A \<squnion> (\<A> e)) (ty E e # ST) es"

definition compT⇣a :: "ty list => nat hyperset => ty list => expr⇣1 => ty⇣i' list" where
  "compT⇣a E A ST e = compT E A ST e @ [after E A ST e]"

end

lemma compE⇣2_not_Nil[simp]: "compE⇣2 e ≠ []"
(*<*)by(induct e) auto(*>*)

lemma (in TC1) compT_sizes[simp]:
shows "!!E A ST. size(compT E A ST e) = size(compE⇣2 e) - 1"
and "!!E A ST. size(compTs E A ST es) = size(compEs⇣2 es)"
(*<*)
apply(induct e and es)
apply(auto split:bop.splits nat_diff_split)
done
(*>*)


lemma (in TC1) [simp]: "!!ST E. ⌊τ⌋ ∉ set (compT E None ST e)"
and [simp]: "!!ST E. ⌊τ⌋ ∉ set (compTs E None ST es)"
(*<*)by(induct e and es) (simp_all add:after_def)(*>*)


lemma (in TC0) pair_eq_ty⇣i'_conv:
  "(⌊(ST, LT)⌋ = ty⇣i' ST⇣0 E A) =
  (case A of None => False | Some A => (ST = ST⇣0 ∧ LT = ty⇣l E A))"
(*<*)by(simp add:ty⇣i'_def)(*>*)


lemma (in TC0) pair_conv_ty⇣i':
  "⌊(ST, ty⇣l E A)⌋ = ty⇣i' ST E ⌊A⌋"
(*<*)by(simp add:ty⇣i'_def)(*>*)

(*<*)
declare (in TC0)
  ty⇣i'_antimono [intro!] after_def[simp]
  pair_conv_ty⇣i'[simp] pair_eq_ty⇣i'_conv[simp]
(*>*)


lemma (in TC1) compT_LT_prefix:
 "!!E A ST⇣0. [| ⌊(ST,LT)⌋ ∈ set(compT E A ST⇣0 e); \<B> e (size E) |]
               ==> P \<turnstile> ⌊(ST,LT)⌋ ≤' ty⇣i' ST E A"
and
 "!!E A ST⇣0. [| ⌊(ST,LT)⌋ ∈ set(compTs E A ST⇣0 es); \<B>s es (size E) |]
               ==> P \<turnstile> ⌊(ST,LT)⌋ ≤' ty⇣i' ST E A"
(*<*)
proof(induct e and es)
  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 Block thus ?case
    by(force simp add:hyperset_defs ty⇣i'_def simp del:pair_conv_ty⇣i'
             elim!:sup_state_opt_trans)
next
  case Call thus ?case by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
next
  case Cons_exp 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'_env_antimono *) ty⇣i'_incr
                elim!:sup_state_opt_trans)
qed (auto simp:hyperset_defs)

declare (in TC0)
  ty⇣i'_antimono [rule del] after_def[simp del]
  pair_conv_ty⇣i'[simp del] pair_eq_ty⇣i'_conv[simp del]
(*>*)


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

lemma (in TC0) after_in_states:
 "[| wf_prog p P; P,E \<turnstile>⇩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(blast intro!:listI WT⇣1_is_type)
using max_stack1[of e] apply simp
done
(*>*)


lemma (in TC0) 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
(*>*)


lemma is_class_type_aux: "is_class P C ==> is_type P (Class C)"
(*<*)by(simp)(*>*)

(*<*)
declare is_type_simps[simp del] subsetI[rule del]
(*>*)

theorem (in TC1) compT_states:
assumes wf: "wf_prog p P"
shows "!!E T A ST.
  [| P,E \<turnstile>⇩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 "!!E T A ST. PROP ?P e E T A ST")(*>*)

and "!!E Ts A ST.
  [| P,E \<turnstile>⇩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 "!!E Ts A ST. PROP ?Ps es E Ts A ST")
proof(induct e and es)
  case new thus ?case by(simp)
next
  case (Cast C e) thus ?case by (auto simp:after_in_states[OF wf])
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[OF wf])
next
  case FAcc thus ?case by(auto simp:after_in_states[OF wf])
next
  case FAss thus ?case
    by(auto simp:image_Un WT⇣1_is_type[OF wf] after_in_states[OF wf])
next
  case Seq thus ?case
    by(auto simp:image_Un after_in_states[OF wf])
next
  case BinOp thus ?case
    by(auto simp:image_Un WT⇣1_is_type[OF wf] after_in_states[OF wf])
next
  case Cond thus ?case
    by(force simp:image_Un WT⇣1_is_type[OF wf] after_in_states[OF wf])
next
  case While thus ?case
    by(auto simp:image_Un WT⇣1_is_type[OF wf] after_in_states[OF wf])
next
  case Block thus ?case by(auto)
next
  case (TryCatch e⇣1 C i e⇣2)
  moreover have "size ST + 1 ≤ mxs" using TryCatch.prems max_stack1[of e⇣1] by auto
  ultimately show ?case  
    by(auto simp:image_Un WT⇣1_is_type[OF wf] after_in_states[OF wf]
                  is_class_type_aux)
next
  case Nil_exp thus ?case by simp
next
  case Cons_exp thus ?case
    by(auto simp:image_Un  WT⇣1_is_type[OF wf] after_in_states[OF wf])
next
  case throw thus ?case
    by(auto simp: WT⇣1_is_type[OF wf] after_in_states[OF wf])
next
  case Call thus ?case
    by(auto simp:image_Un WT⇣1_is_type[OF wf] after_in_states[OF wf])
qed

declare is_type_simps[simp] subsetI[intro!]
(*>*)


definition shift :: "nat => ex_table => ex_table"
where
  "shift n xt ≡ map (λ(from,to,C,handler,depth). (from+n,to+n,C,handler+n,depth)) xt"


lemma [simp]: "shift 0 xt = xt"
(*<*)by(induct xt)(auto simp:shift_def)(*>*)

lemma [simp]: "shift n [] = []"
(*<*)by(simp add:shift_def)(*>*)

lemma [simp]: "shift n (xt⇣1 @ xt⇣2) = shift n xt⇣1 @ shift n xt⇣2"
(*<*)by(simp add:shift_def)(*>*)

lemma [simp]: "shift m (shift n xt) = shift (m+n) xt"
(*<*)by(induct xt)(auto simp:shift_def)(*>*)

lemma [simp]: "pcs (shift n xt) = {pc+n|pc. pc ∈ pcs xt}"
(*<*)
apply(auto simp:shift_def pcs_def)
apply(rule_tac x = "x-n" in exI)
apply (force split:nat_diff_split)
done
(*>*)


lemma shift_compxE⇣2:
shows "!!pc pc' d. shift pc (compxE⇣2 e pc' d) = compxE⇣2 e (pc' + pc) d"
and  "!!pc pc' d. shift pc (compxEs⇣2 es pc' d) = compxEs⇣2 es (pc' + pc) d"
(*<*)
apply(induct e and es)
apply(auto simp:shift_def add_ac)
done
(*>*)


lemma compxE⇣2_size_convs[simp]:
shows "n ≠ 0 ==> compxE⇣2 e n d = shift n (compxE⇣2 e 0 d)"
and "n ≠ 0 ==> compxEs⇣2 es n d = shift n (compxEs⇣2 es 0 d)"
(*<*)by(simp_all add:shift_compxE⇣2)(*>*)

locale TC2 = TC1 +
  fixes T⇣r :: ty and mxs :: pc
begin

definition
  wt_instrs :: "instr list => ex_table => ty⇣i' list => bool"
    ("(\<turnstile> _, _ /[::]/ _)" [0,0,51] 50) where
  "\<turnstile> is,xt [::] τs <-> size is < size τs ∧ pcs xt ⊆ {0..<size is} ∧
  (∀pc< size is. P,T⇣r,mxs,size τs,xt \<turnstile> is!pc,pc :: τs)"

end

notation TC2.wt_instrs ("(_,_,_ \<turnstile>/ _, _ /[::]/ _)" [50,50,50,50,50,51] 50)

(*<*)
lemmas (in TC2) wt_defs =
  wt_instrs_def wt_instr_def app_def eff_def norm_eff_def
(*>*)

lemma (in TC2) [simp]: "τs ≠ [] ==> \<turnstile> [],[] [::] τs"
(*<*) by (simp add: wt_defs) (*>*)

lemma [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 \<turnstile> is!pc,pc :: τs;
    pc < size is; size is < size τs; mpc ≤ size τs; mpc ≤ mpc' |]
  ==> P,T,m,mpc',xt \<turnstile> 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 [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  [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 [simp]:
  "xcpt_app i P (pc+n) mxs (shift n xt) τ = xcpt_app i P pc mxs xt τ"
(*<*)by (simp add: xcpt_app_def) (auto simp add: shift_def)(*>*)


lemma wt_instr_appL:
  "[| P,T,m,mpc,xt \<turnstile> i,pc :: τs; pc < size τs; mpc ≤ size τs |]
  ==> P,T,m,mpc + size τs',shift (size τs') xt \<turnstile> i,pc+size τs' :: τs'@τs"
(*<*)
apply(auto simp:wt_instr_def app_def)
prefer 2 apply(fast)
prefer 2 apply(fast)
apply(cases "i",auto)
done
(*>*)


lemma wt_instr_Cons:
  "[| P,T,m,mpc - 1,[] \<turnstile> i,pc - 1 :: τs;
     0 < pc; 0 < mpc; pc < size τs + 1; mpc ≤ size τs + 1 |]
  ==> P,T,m,mpc,[] \<turnstile> 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',[] \<turnstile> 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,[] \<turnstile> 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 wt_instr_appRx:
  "[| P,T,m,mpc,xt \<turnstile> is!pc,pc :: τs; pc < size is; size is < size τs; mpc ≤ size τs |]
  ==> P,T,m,mpc,xt @ shift (size is) xt' \<turnstile> is!pc,pc :: τs"
(*<*)by (auto simp:wt_instr_def eff_def app_def xcpt_app_pcs xcpt_eff_pcs)(*>*)


lemma wt_instr_appLx: 
  "[| P,T,m,mpc,xt \<turnstile> i,pc :: τs; pc ∉ pcs xt' |]
  ==> P,T,m,mpc,xt'@xt \<turnstile> i,pc :: τs"
(*<*)by (auto simp:wt_instr_def app_def eff_def xcpt_app_pcs xcpt_eff_pcs)(*>*)


lemma (in TC2) wt_instrs_extR:
  "\<turnstile> is,xt [::] τs ==> \<turnstile> is,xt [::] τs @ τs'"
(*<*)by(auto simp add:wt_instrs_def wt_instr_appR)(*>*)


lemma (in TC2) wt_instrs_ext:
  "[| \<turnstile> is⇣1,xt⇣1 [::] τs⇣1@τs⇣2; \<turnstile> is⇣2,xt⇣2 [::] τs⇣2; size τs⇣1 = size is⇣1 |]
  ==> \<turnstile> is⇣1@is⇣2, xt⇣1 @ shift (size is⇣1) xt⇣2 [::] τs⇣1@τs⇣2"
(*<*)
apply(clarsimp simp:wt_instrs_def)
apply(rule conjI, fastforce)
apply(rule conjI, fastforce)
apply clarsimp
apply(rule conjI, fastforce simp:wt_instr_appRx)
apply clarsimp
apply(erule_tac x = "pc - size is⇣1" in allE)+
apply(thin_tac "?P --> ?Q")
apply(erule impE, arith) 
apply(drule_tac τs' = "τs⇣1" in wt_instr_appL)
  apply arith
 apply simp
apply(fastforce simp add:add_commute intro!: wt_instr_appLx)
done
(*>*)

corollary (in TC2) wt_instrs_ext2:
  "[| \<turnstile> is⇣2,xt⇣2 [::] τs⇣2; \<turnstile> is⇣1,xt⇣1 [::] τs⇣1@τs⇣2; size τs⇣1 = size is⇣1 |]
  ==> \<turnstile> is⇣1@is⇣2, xt⇣1 @ shift (size is⇣1) xt⇣2 [::] τs⇣1@τs⇣2"
(*<*)by(rule wt_instrs_ext)(*>*)


corollary (in TC2) wt_instrs_ext_prefix [trans]:
  "[| \<turnstile> is⇣1,xt⇣1 [::] τs⇣1@τs⇣2; \<turnstile> is⇣2,xt⇣2 [::] τs⇣3;
     size τs⇣1 = size is⇣1; prefixeq τs⇣3 τs⇣2 |]
  ==> \<turnstile> is⇣1@is⇣2, xt⇣1 @ shift (size is⇣1) xt⇣2 [::] τs⇣1@τs⇣2"
(*<*)by(bestsimp simp:prefixeq_def elim: wt_instrs_ext dest:wt_instrs_extR)(*>*)


corollary (in TC2) wt_instrs_app:
  assumes is⇣1: "\<turnstile> is⇣1,xt⇣1 [::] τs⇣1@[τ]"
  assumes is⇣2: "\<turnstile> is⇣2,xt⇣2 [::] τ#τs⇣2"
  assumes s: "size τs⇣1 = size is⇣1"
  shows "\<turnstile> is⇣1@is⇣2, xt⇣1@shift (size is⇣1) xt⇣2 [::] τs⇣1@τ#τs⇣2"
(*<*)
proof -
  from is⇣1 have "\<turnstile> is⇣1,xt⇣1 [::] (τs⇣1@[τ])@τs⇣2"
    by (rule wt_instrs_extR)
  hence "\<turnstile> is⇣1,xt⇣1 [::] τs⇣1@τ#τs⇣2" by simp
  from this is⇣2 s show ?thesis by (rule wt_instrs_ext) 
qed
(*>*)


corollary (in TC2) wt_instrs_app_last[trans]:
  "[| \<turnstile> is⇣2,xt⇣2 [::] τ#τs⇣2; \<turnstile> is⇣1,xt⇣1 [::] τs⇣1;
     last τs⇣1 = τ;  size τs⇣1 = size is⇣1+1 |]
  ==> \<turnstile> is⇣1@is⇣2, xt⇣1@shift (size is⇣1) xt⇣2 [::] τs⇣1@τs⇣2"
(*<*)
apply(cases τs⇣1 rule:rev_cases)
 apply simp
apply(simp add:wt_instrs_app)
done
(*>*)


corollary (in TC2) wt_instrs_append_last[trans]:
  "[| \<turnstile> is,xt [::] τs; P,T⇣r,mxs,mpc,[] \<turnstile> i,pc :: τs;
     pc = size is; mpc = size τs; size is + 1 < size τs |]
  ==> \<turnstile> 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 (in TC2) wt_instrs_app2:
  "[| \<turnstile> is⇣2,xt⇣2 [::] τ'#τs⇣2;  \<turnstile> is⇣1,xt⇣1 [::] τ#τs⇣1@[τ'];
     xt' = xt⇣1 @ shift (size is⇣1) xt⇣2;  size τs⇣1+1 = size is⇣1 |]
  ==> \<turnstile> is⇣1@is⇣2,xt' [::] τ#τs⇣1@τ'#τs⇣2"
(*<*)using wt_instrs_app[where ?τs⇣1.0 = "τ # τs⇣1"] by simp (*>*)


corollary (in TC2) wt_instrs_app2_simp[trans,simp]:
  "[| \<turnstile> is⇣2,xt⇣2 [::] τ'#τs⇣2;  \<turnstile> is⇣1,xt⇣1 [::] τ#τs⇣1@[τ']; size τs⇣1+1 = size is⇣1 |]
  ==> \<turnstile> is⇣1@is⇣2, xt⇣1@shift (size is⇣1) xt⇣2 [::] τ#τs⇣1@τ'#τs⇣2"
(*<*)using wt_instrs_app[where ?τs⇣1.0 = "τ # τs⇣1"] by simp(*>*)


corollary (in TC2) wt_instrs_Cons[simp]:
  "[| τs ≠ []; \<turnstile> [i],[] [::] [τ,τ']; \<turnstile> is,xt [::] τ'#τs |]
  ==> \<turnstile> i#is,shift 1 xt [::] τ#τ'#τs"
(*<*)
using wt_instrs_app2[where ?is⇣1.0 = "[i]" and ?τs⇣1.0 = "[]" and ?is⇣2.0 = "is"
                      and ?xt⇣1.0 = "[]"]
by simp


corollary (in TC2) wt_instrs_Cons2[trans]:
  assumes τs: "\<turnstile> is,xt [::] τs"
  assumes i: "P,T⇣r,mxs,mpc,[] \<turnstile> i,0 :: τ#τs"
  assumes mpc: "mpc = size τs + 1"
  shows "\<turnstile> i#is,shift 1 xt [::] τ#τs"
(*<*)
proof -
  from τs have "τs ≠ []" by (auto simp: wt_instrs_def)
  with mpc i have "\<turnstile> [i],[] [::] [τ]@τs" by (simp add: wt_instrs_def)
  with τs show ?thesis by (fastforce dest: wt_instrs_ext)
qed
(*>*)


lemma (in TC2) wt_instrs_last_incr[trans]:
  "[| \<turnstile> is,xt [::] τs@[τ]; P \<turnstile> τ ≤' τ' |] ==> \<turnstile> 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
(*>*)


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)(*>*)


lemma (in TC2) wt_New:
  "[| is_class P C; size ST < mxs |] ==>
   \<turnstile> [New C],[] [::] [ty⇣i' ST E A, ty⇣i' (Class C#ST) E A]"
(*<*)by(simp add:wt_defs ty⇣i'_def)(*>*)


lemma (in TC2) wt_Cast:
  "is_class P C ==>
   \<turnstile> [Checkcast C],[] [::] [ty⇣i' (Class D # ST) E A, ty⇣i' (Class C # ST) E A]"
(*<*)by(simp add: ty⇣i'_def wt_defs)(*>*)


lemma (in TC2) wt_Push:
  "[| size ST < mxs; typeof v = Some T |]
  ==> \<turnstile> [Push v],[] [::] [ty⇣i' ST E A, ty⇣i' (T#ST) E A]"
(*<*)by(simp add: ty⇣i'_def wt_defs)(*>*)


lemma (in TC2) wt_Pop:
 "\<turnstile> [Pop],[] [::] (ty⇣i' (T#ST) E A # ty⇣i' ST E A # τs)"
(*<*)by(simp add: ty⇣i'_def wt_defs)(*>*)


lemma (in TC2) wt_CmpEq:
  "[| P \<turnstile> T⇣1 ≤ T⇣2 ∨ P \<turnstile> T⇣2 ≤ T⇣1|]
  ==> \<turnstile> [CmpEq],[] [::] [ty⇣i' (T⇣2 # T⇣1 # ST) E A, ty⇣i' (Boolean # ST) E A]"
(*<*) by(auto simp:ty⇣i'_def wt_defs elim!: refTE not_refTE) (*>*)


lemma (in TC2) wt_IAdd:
  "\<turnstile> [IAdd],[] [::] [ty⇣i' (Integer#Integer#ST) E A, ty⇣i' (Integer#ST) E A]"
(*<*)by(simp add:ty⇣i'_def wt_defs)(*>*)


lemma (in TC2) wt_Load:
  "[| size ST < mxs; size E ≤ mxl; i ∈∈ A; i < size E |]
  ==> \<turnstile> [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)(*>*)


lemma (in TC2) wt_Store:
 "[| P \<turnstile> T ≤ E!i; i < size E; size E ≤ mxl |] ==>
  \<turnstile> [Store i],[] [::] [ty⇣i' (T#ST) E A, ty⇣i' ST E (⌊{i}⌋ \<squnion> A)]"
(*<*)
by(auto simp:hyperset_defs nth_list_update ty⇣i'_def wt_defs ty⇣l_def
        intro:list_all2_all_nthI)
(*>*)


lemma (in TC2) wt_Get:
 "[| P \<turnstile> C sees F:T in D |] ==>
  \<turnstile> [Getfield F D],[] [::] [ty⇣i' (Class C # ST) E A, ty⇣i' (T # ST) E A]"
(*<*)by(auto simp: ty⇣i'_def wt_defs dest: sees_field_idemp sees_field_decl_above)(*>*)


lemma (in TC2) wt_Put:
  "[| P \<turnstile> C sees F:T in D; P \<turnstile> T' ≤ T |] ==>
  \<turnstile> [Putfield F D],[] [::] [ty⇣i' (T' # Class C # ST) E A, ty⇣i' ST E A]"
(*<*)by(auto intro: sees_field_idemp sees_field_decl_above simp: ty⇣i'_def wt_defs)(*>*)


lemma (in TC2) wt_Throw:
  "\<turnstile> [Throw],[] [::] [ty⇣i' (Class C # ST) E A, τ']"
(*<*)by(auto simp: ty⇣i'_def wt_defs)(*>*)


lemma (in TC2) wt_IfFalse:
  "[| 2 ≤ i; nat i < size τs + 2; P \<turnstile> ty⇣i' ST E A ≤' τs ! nat(i - 2) |]
  ==> \<turnstile> [IfFalse i],[] [::] ty⇣i' (Boolean # ST) E A # ty⇣i' ST E A # τs"
(*<*)
by(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 \<turnstile> τs!pc ≤' τs ! nat (int pc + i) |]
 ==> P,T,mxs,mpc,[] \<turnstile> Goto i,pc :: τs"
(*<*)by(clarsimp simp add: TC2.wt_defs)(*>*)


lemma (in TC2) wt_Invoke:
  "[| size es = size Ts'; P \<turnstile> C sees M: Ts->T = m in D; P \<turnstile> Ts' [≤] Ts |]
  ==> \<turnstile> [Invoke M (size es)],[] [::] [ty⇣i' (rev Ts' @ Class C # ST) E A, ty⇣i' (T#ST) E A]"
(*<*)by(fastforce simp add: ty⇣i'_def wt_defs)(*>*)


corollary (in TC2) wt_instrs_app3[simp]:
  "[| \<turnstile> is⇣2,[] [::] (τ' # τs⇣2);  \<turnstile> is⇣1,xt⇣1 [::] τ # τs⇣1 @ [τ']; size τs⇣1+1 = size is⇣1|]
  ==> \<turnstile> (is⇣1 @ is⇣2),xt⇣1 [::] τ # τs⇣1 @ τ' # τs⇣2"
(*<*)using wt_instrs_app2[where ?xt⇣2.0 = "[]"] by (simp add:shift_def)(*>*)


corollary (in TC2) wt_instrs_Cons3[simp]:
  "[| τs ≠ []; \<turnstile> [i],[] [::] [τ,τ']; \<turnstile> is,[] [::] τ'#τs |]
  ==> \<turnstile> (i # is),[] [::] τ # τ' # τs"
(*<*)
using wt_instrs_Cons[where ?xt = "[]"]
by (simp add:shift_def)

(*<*)
declare nth_append[simp del]
declare [[simproc del: list_to_set_comprehension]]
(*>*)

lemma (in TC2) wt_instrs_xapp[trans]:
  "[| \<turnstile> is⇣1 @ is⇣2, xt [::] τs⇣1 @ ty⇣i' (Class C # ST) E A # τs⇣2;
     ∀τ ∈ set τs⇣1. ∀ST' LT'. τ = Some(ST',LT') --> 
      size ST ≤ size ST' ∧ P \<turnstile> Some (drop (size ST' - size ST) ST',LT') ≤' ty⇣i' ST E A;
     size is⇣1 = size τs⇣1; is_class P C; size ST < mxs  |] ==>
  \<turnstile> is⇣1 @ is⇣2, xt @ [(0,size is⇣1 - 1,C,size is⇣1,size ST)] [::] τs⇣1 @ ty⇣i' (Class C # ST) E A # τs⇣2"
(*<*)
apply(simp add:wt_instrs_def)
apply(rule conjI)
 apply(clarsimp)
 apply arith
apply clarsimp
apply(erule allE, erule (1) impE)
apply(clarsimp simp add: wt_instr_def app_def eff_def)
apply(rule conjI)
 apply (thin_tac "∀x∈ ?A ∪ ?B. ?P x")
 apply (thin_tac "∀x∈ ?A ∪ ?B. ?P x")
 apply (clarsimp simp add: xcpt_app_def relevant_entries_def)
 apply (simp add: nth_append is_relevant_entry_def split: split_if_asm)
  apply (drule_tac x="τs⇣1!pc" in bspec)
   apply (blast intro: nth_mem) 
  apply fastforce   
apply (rule conjI)
 apply clarsimp
 apply (erule disjE, blast)
 apply (erule disjE, blast)
 apply (clarsimp simp add: xcpt_eff_def relevant_entries_def split: split_if_asm)
apply clarsimp
apply (erule disjE, blast)
apply (erule disjE, blast)
apply (clarsimp simp add: xcpt_eff_def relevant_entries_def split: split_if_asm)
apply (simp add: nth_append is_relevant_entry_def split: split_if_asm)
 apply (drule_tac x = "τs⇣1!pc" in bspec)
  apply (blast intro: nth_mem) 
 apply (fastforce simp add: ty⇣i'_def)
done

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⇣0) ≤ length xs; drop (length xs - Suc (length xs⇣0)) xs = x # xs⇣0|] 
  ==> drop (length xs - length xs⇣0) xs = xs⇣0"
apply (cases xs)
 apply simp
apply (simp add: Suc_diff_le)
apply (case_tac "length list - length xs⇣0")
 apply simp
apply (simp add: drop_Cons_Suc)
done

(*<*)
declare (in TC0)
  after_def[simp] pair_eq_ty⇣i'_conv[simp]
(*>*)

lemma (in TC1) compT_ST_prefix:
 "!!E A ST⇣0. ⌊(ST,LT)⌋ ∈ set(compT E A ST⇣0 e) ==> 
  size ST⇣0 ≤ size ST ∧ drop (size ST - size ST⇣0) ST = ST⇣0"
and
 "!!E A ST⇣0. ⌊(ST,LT)⌋ ∈ set(compTs E A ST⇣0 es) ==> 
  size ST⇣0 ≤ size ST ∧ drop (size ST - size ST⇣0) ST = ST⇣0"
(*<*)
proof(induct e and es)
  case (FAss e⇣1 F D e⇣2)
  moreover {
    let ?ST⇣0 = "ty E e⇣1 # ST⇣0"
    fix A assume "⌊(ST, LT)⌋ ∈ set (compT E A ?ST⇣0 e⇣2)"
    with FAss
    have "length ?ST⇣0 ≤ length ST ∧ drop (size ST - size ?ST⇣0) ST = ?ST⇣0" by blast
    hence ?case  by (clarsimp simp add: drop_mess)
  }
  ultimately show ?case by auto
next
  case TryCatch thus ?case by auto
next
  case Block thus ?case by auto
next
  case Seq thus ?case by auto
next
  case While thus ?case by auto
next
  case Cond thus ?case by auto
next
  case (Call e M es)
  moreover {
    let ?ST⇣0 = "ty E e # ST⇣0"
    fix A assume "⌊(ST, LT)⌋ ∈ set (compTs E A ?ST⇣0 es)"
    with Call
    have "length ?ST⇣0 ≤ length ST ∧ drop (size ST - size ?ST⇣0) ST = ?ST⇣0" by blast
    hence ?case  by (clarsimp simp add: drop_mess)
  }
  ultimately show ?case by auto
next
  case (Cons_exp e es)
  moreover {
    let ?ST⇣0 = "ty E e # ST⇣0"
    fix A assume "⌊(ST, LT)⌋ ∈ set (compTs E A ?ST⇣0 es)"
    with Cons_exp
    have "length ?ST⇣0 ≤ length ST ∧ drop (size ST - size ?ST⇣0) ST = ?ST⇣0" by blast
    hence ?case  by (clarsimp simp add: drop_mess)
  }
  ultimately show ?case by auto
next
  case (BinOp e⇣1 bop e⇣2)
  moreover {
    let ?ST⇣0 = "ty E e⇣1 # ST⇣0"
    fix A assume "⌊(ST, LT)⌋ ∈ set (compT E A ?ST⇣0 e⇣2)"
    with BinOp 
    have "length ?ST⇣0 ≤ length ST ∧ drop (size ST - size ?ST⇣0) ST = ?ST⇣0" by blast
    hence ?case by (clarsimp simp add: drop_mess)
  }
  ultimately show ?case by auto
next
  case new thus ?case by auto
next
  case Val thus ?case by auto    
next
  case Cast thus ?case by auto
next
  case Var thus ?case by auto
next
  case LAss thus ?case by auto
next
  case throw thus ?case by auto
next
  case FAcc thus ?case by auto
next
  case Nil_exp thus ?case by auto
qed 

declare (in TC0) 
  after_def[simp del] pair_eq_ty⇣i'_conv[simp del]
(*>*)

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

theorem (in TC2) compT_wt_instrs: "!!E T A ST.
  [| P,E \<turnstile>⇩1 e :: T; \<D> e A; \<B> e (size E); 
    size ST + max_stack e ≤ mxs; size E + max_vars e ≤ mxl |]
  ==> \<turnstile> compE⇣2 e, compxE⇣2 e 0 (size ST) [::]
                 ty⇣i' ST E A # compT E A ST e @ [after E A ST e]"
(*<*)(is "!!E T A ST. PROP ?P e E T A ST")(*>*)

and "!!E Ts A ST.
  [| P,E \<turnstile>⇩1 es[::]Ts;  \<D>s es A; \<B>s es (size E); 
    size ST + max_stacks es ≤ mxs; size E + max_varss es ≤ mxl |]
  ==> let τs = ty⇣i' ST E A # compTs E A ST es in
       \<turnstile> compEs⇣2 es,compxEs⇣2 es 0 (size ST) [::] τs ∧
       last τs = ty⇣i' (rev Ts @ ST) E (A \<squnion> \<A>s es)"
(*<*)
(is "!!E Ts A ST. PROP ?Ps es E Ts A ST")
proof(induct e and es)
  case (TryCatch e⇣1 C i e⇣2)
  hence [simp]: "i = size E" by simp
  have wt⇣1: "P,E \<turnstile>⇩1 e⇣1 :: T" and wt⇣2: "P,E@[Class C] \<turnstile>⇩1 e⇣2 :: T"
    and "class": "is_class P C" using TryCatch by auto
  let ?A⇣1 = "A \<squnion> \<A> e⇣1" let ?A⇣i = "A \<squnion> ⌊{i}⌋" let ?E⇣i = "E @ [Class C]"
  let ?τ = "ty⇣i' ST E A" let ?τs⇣1 = "compT E A ST e⇣1"
  let ?τ⇣1 = "ty⇣i' (T#ST) E ?A⇣1" let ?τ⇣2 = "ty⇣i' (Class C#ST) E A"
  let ?τ⇣3 = "ty⇣i' ST ?E⇣i ?A⇣i" let ?τs⇣2 = "compT ?E⇣i ?A⇣i ST e⇣2"
  let ?τ⇣2' = "ty⇣i' (T#ST) ?E⇣i (?A⇣i \<squnion> \<A> e⇣2)"
  let ?τ' = "ty⇣i' (T#ST) E (A \<squnion> \<A> e⇣1 \<sqinter> (\<A> e⇣2 \<ominus> i))"
  let ?go = "Goto (int(size(compE⇣2 e⇣2)) + 2)"
  have "PROP ?P e⇣2 ?E⇣i T ?A⇣i ST" by fact
  hence "\<turnstile> compE⇣2 e⇣2,compxE⇣2 e⇣2 0 (size ST) [::] (?τ⇣3 # ?τs⇣2) @ [?τ⇣2']"
    using TryCatch.prems by(auto simp:after_def)
  also have "?A⇣i \<squnion> \<A> e⇣2 = (A \<squnion> \<A> e⇣2) \<squnion> ⌊{size E}⌋"
    by(fastforce simp:hyperset_defs)
  also have "P \<turnstile> ty⇣i' (T#ST) ?E⇣i … ≤' ty⇣i' (T#ST) E (A \<squnion> \<A> e⇣2)"
    by(simp add:hyperset_defs ty⇣l_incr ty⇣i'_def)
  also have "P \<turnstile> … ≤' ty⇣i' (T#ST) E (A \<squnion> \<A> e⇣1 \<sqinter> (\<A> e⇣2 \<ominus> i))"
    by(auto intro!: ty⇣l_antimono simp:hyperset_defs ty⇣i'_def)
  also have "(?τ⇣3 # ?τs⇣2) @ [?τ'] = ?τ⇣3 # ?τs⇣2 @ [?τ']" by simp
  also have "\<turnstile> [Store i],[] [::] ?τ⇣2 # [] @ [?τ⇣3]"
    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 "[] @ (?τ⇣3 # ?τs⇣2 @ [?τ']) = (?τ⇣3 # ?τs⇣2 @ [?τ'])" by simp
  also have "P,T⇣r,mxs,size(compE⇣2 e⇣2)+3,[] \<turnstile> ?go,0 :: ?τ⇣1#?τ⇣2#?τ⇣3#?τs⇣2 @ [?τ']"
    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 "\<turnstile> compE⇣2 e⇣1,compxE⇣2 e⇣1 0 (size ST) [::] ?τ # ?τs⇣1 @ [?τ⇣1]"
    using TryCatch by(auto simp:after_def)
  also have "?τ # ?τs⇣1 @ ?τ⇣1 # ?τ⇣2 # ?τ⇣3 # ?τs⇣2 @ [?τ'] =
             (?τ # ?τs⇣1 @ [?τ⇣1]) @ ?τ⇣2 # ?τ⇣3 # ?τs⇣2 @ [?τ']" by simp
  also have "compE⇣2 e⇣1 @ ?go  # [Store i] @ compE⇣2 e⇣2 =
             (compE⇣2 e⇣1 @ [?go]) @ (Store i # compE⇣2 e⇣2)" by simp
  also 
  let "?Q τ" = "∀ST' LT'. τ = ⌊(ST', LT')⌋ --> 
    size ST ≤ size ST' ∧ P \<turnstile> 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⇣1)" 
      by (fastforce simp add: ty⇣i'_def hyperset_defs intro!: ty⇣l_antimono)
    moreover have "!!τ. τ ∈ set (compT E A ST e⇣1) ==> ?Q τ" using TryCatch.prems
      by clarsimp (frule compT_ST_prefix,
                   fastforce dest!: compT_LT_prefix simp add: ty⇣i'_def)
    ultimately
    have "∀τ∈set (ty⇣i' ST E A # compT E A ST e⇣1 @ [ty⇣i' (T # ST) E ?A⇣1]). ?Q τ" 
      by auto
  }
  also from TryCatch.prems max_stack1[of e⇣1] have "size ST + 1 ≤ mxs" by auto
  ultimately show ?case using wt⇣1 wt⇣2 TryCatch.prems "class"
    by (simp add:after_def)
next
  case new thus ?case by(auto simp add:after_def wt_New)
next
  case (BinOp e⇣1 bop e⇣2) 
  let ?op = "case bop of Eq => [CmpEq] | Add => [IAdd]"
  have T: "P,E \<turnstile>⇩1 e⇣1 «bop» e⇣2 :: T" by fact
  then obtain T⇣1 T⇣2 where T⇣1: "P,E \<turnstile>⇩1 e⇣1 :: T⇣1" and T⇣2: "P,E \<turnstile>⇩1 e⇣2 :: T⇣2" and 
    bopT: "case bop of Eq => (P \<turnstile> T⇣1 ≤ T⇣2 ∨ P \<turnstile> T⇣2 ≤ T⇣1) ∧ T = Boolean 
                    | Add => T⇣1 = Integer ∧ T⇣2 = Integer ∧ T = Integer" by auto
  let ?A⇣1 = "A \<squnion> \<A> e⇣1" let ?A⇣2 = "?A⇣1 \<squnion> \<A> e⇣2"
  let ?τ = "ty⇣i' ST E A" let ?τs⇣1 = "compT E A ST e⇣1"
  let ?τ⇣1 = "ty⇣i' (T⇣1#ST) E ?A⇣1" let ?τs⇣2 = "compT E ?A⇣1 (T⇣1#ST) e⇣2"
  let ?τ⇣2 = "ty⇣i' (T⇣2#T⇣1#ST) E ?A⇣2" let ?τ' = "ty⇣i' (T#ST) E ?A⇣2"
  from bopT have "\<turnstile> ?op,[] [::] [?τ⇣2,?τ']" 
    by (cases bop) (auto simp add: wt_CmpEq wt_IAdd)
  also have "PROP ?P e⇣2 E T⇣2 ?A⇣1 (T⇣1#ST)" by fact
  with BinOp.prems T⇣2 
  have "\<turnstile> compE⇣2 e⇣2, compxE⇣2 e⇣2 0 (size (T⇣1#ST)) [::] ?τ⇣1#?τs⇣2@[?τ⇣2]" 
    by (auto simp: after_def)
  also from BinOp T⇣1 have "\<turnstile> compE⇣2 e⇣1, compxE⇣2 e⇣1 0 (size ST) [::] ?τ#?τs⇣1@[?τ⇣1]" 
    by (auto simp: after_def)
  finally show ?case using T T⇣1 T⇣2 by (simp add: after_def hyperUn_assoc)
next
  case (Cons_exp e es)
  have "P,E \<turnstile>⇩1 e # es [::] Ts" by fact
  then obtain T⇣e Ts' where 
    T⇣e: "P,E \<turnstile>⇩1 e :: T⇣e" and Ts': "P,E \<turnstile>⇩1 es [::] Ts'" and
    Ts: "Ts = T⇣e#Ts'" by auto
  let ?A⇣e = "A \<squnion> \<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')"
  have Ps: "PROP ?Ps es E Ts' ?A⇣e (T⇣e#ST)" by fact
  with Cons_exp.prems T⇣e Ts'
  have "\<turnstile> compEs⇣2 es, compxEs⇣2 es 0 (size (T⇣e#ST)) [::] ?τ⇣e#?τs'" by (simp add: after_def)
  also from Cons_exp T⇣e have "\<turnstile> compE⇣2 e, compxE⇣2 e 0 (size ST) [::] ?τ#?τs⇣e@[?τ⇣e]" 
    by (auto simp: after_def)
  moreover
  from Ps Cons_exp.prems T⇣e Ts' Ts
  have "last ?τs = ty⇣i' (rev Ts@ST) E (?A⇣e \<squnion> \<A>s es)" by simp
  ultimately show ?case using T⇣e by (simp add: after_def hyperUn_assoc)
next
  case (FAss e⇣1 F D e⇣2)
  hence Void: "P,E \<turnstile>⇩1 e⇣1•F{D} := e⇣2 :: Void" by auto
  then obtain C T T' where    
    C: "P,E \<turnstile>⇩1 e⇣1 :: Class C" and sees: "P \<turnstile> C sees F:T in D" and
    T': "P,E \<turnstile>⇩1 e⇣2 :: T'" and T'_T: "P \<turnstile> T' ≤ T" by auto
  let ?A⇣1 = "A \<squnion> \<A> e⇣1" let ?A⇣2 = "?A⇣1 \<squnion> \<A> e⇣2"  
  let ?τ = "ty⇣i' ST E A" let ?τs⇣1 = "compT E A ST e⇣1"
  let ?τ⇣1 = "ty⇣i' (Class C#ST) E ?A⇣1" let ?τs⇣2 = "compT E ?A⇣1 (Class C#ST) e⇣2"
  let ?τ⇣2 = "ty⇣i' (T'#Class C#ST) E ?A⇣2" let ?τ⇣3 = "ty⇣i' ST E ?A⇣2"
  let ?τ' = "ty⇣i' (Void#ST) E ?A⇣2"
  from FAss.prems sees T'_T 
  have "\<turnstile> [Putfield F D,Push Unit],[] [::] [?τ⇣2,?τ⇣3,?τ']"
    by (fastforce simp add: wt_Push wt_Put)
  also have "PROP ?P e⇣2 E T' ?A⇣1 (Class C#ST)" by fact
  with FAss.prems T' 
  have "\<turnstile> compE⇣2 e⇣2, compxE⇣2 e⇣2 0 (size ST+1) [::] ?τ⇣1#?τs⇣2@[?τ⇣2]"
    by (auto simp add: after_def hyperUn_assoc) 
  also from FAss C have "\<turnstile> compE⇣2 e⇣1, compxE⇣2 e⇣1 0 (size ST) [::] ?τ#?τs⇣1@[?τ⇣1]" 
    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 thus ?case by (auto simp:after_def wt_Cast)
next
  case (Block i T⇣i e)
  let ?τs = "ty⇣i' ST E A # compT (E @ [T⇣i]) (A\<ominus>i) ST e"
  have IH: "PROP ?P e (E@[T⇣i]) T (A\<ominus>i) ST" by fact
  hence "\<turnstile> compE⇣2 e, compxE⇣2 e 0 (size ST) [::]
         ?τs @ [ty⇣i' (T#ST) (E@[T⇣i]) (A\<ominus>(size E) \<squnion> \<A> e)]"
    using Block.prems by (auto simp add: after_def)
  also have "P \<turnstile> ty⇣i' (T # ST) (E@[T⇣i]) (A \<ominus> size E \<squnion> \<A> e) ≤'
                 ty⇣i' (T # ST) (E@[T⇣i]) ((A \<squnion> \<A> e) \<ominus> size E)"
     by(auto simp add:hyperset_defs intro: ty⇣i'_antimono)
  also have "… = ty⇣i' (T # ST) E (A \<squnion> \<A> e)" by simp
  also have "P \<turnstile> … ≤' ty⇣i' (T # ST) E (A \<squnion> (\<A> e \<ominus> i))"
     by(auto simp add:hyperset_defs intro: ty⇣i'_antimono)
  finally show ?case using Block.prems 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 i e) thus ?case using max_stack1[of e]
    by(auto simp: hyper_insert_comm after_def wt_Store wt_Push)
next
  case Nil_exp thus ?case by auto
next
  case throw thus ?case by(auto simp add: after_def wt_Throw)
next
  case (While e c)
  obtain Tc where wte: "P,E \<turnstile>⇩1 e :: Boolean" and wtc: "P,E \<turnstile>⇩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⇣0 = "A \<squnion> \<A> e" let ?A⇣1 = "?A⇣0 \<squnion> \<A> c"
  let ?τ = "ty⇣i' ST E A" let ?τs⇣e = "compT E A ST e"
  let ?τ⇣e = "ty⇣i' (Boolean#ST) E ?A⇣0" let ?τ⇣1 = "ty⇣i' ST E ?A⇣0"
  let ?τs⇣c = "compT E ?A⇣0 ST c" let ?τ⇣c = "ty⇣i' (Tc#ST) E ?A⇣1"
  let ?τ⇣2 = "ty⇣i' ST E ?A⇣1" let ?τ' = "ty⇣i' (Void#ST) E ?A⇣0"
  let ?τs = "(?τ # ?τs⇣e @ [?τ⇣e]) @ ?τ⇣1 # ?τs⇣c @ [?τ⇣c, ?τ⇣2, ?τ⇣1, ?τ']"
  have "\<turnstile> [],[] [::] [] @ ?τs" by(simp add:wt_instrs_def)
  also
  have "PROP ?P e E Boolean A ST" by fact
  hence "\<turnstile> compE⇣2 e,compxE⇣2 e 0 (size ST) [::] ?τ # ?τs⇣e @ [?τ⇣e]"
    using While.prems by (auto simp:after_def)
  also
  have "[] @ ?τs = (?τ # ?τs⇣e) @ ?τ⇣e # ?τ⇣1 # ?τs⇣c @ [?τ⇣c,?τ⇣2,?τ⇣1,?τ']" by simp
  also
  let ?n⇣e = "size(compE⇣2 e)"  let ?n⇣c = "size(compE⇣2 c)"
  let ?if = "IfFalse (int ?n⇣c + 3)"
  have "\<turnstile> [?if],[] [::] ?τ⇣e # ?τ⇣1 # ?τs⇣c @ [?τ⇣c, ?τ⇣2, ?τ⇣1, ?τ']"
    by(simp add: wt_instr_Cons wt_instr_append wt_IfFalse
                 nat_add_distrib split: nat_diff_split)
  also
  have "(?τ # ?τs⇣e) @ (?τ⇣e # ?τ⇣1 # ?τs⇣c @ [?τ⇣c, ?τ⇣2, ?τ⇣1, ?τ']) = ?τs" by simp
  also
  have "PROP ?P c E Tc ?A⇣0 ST" by fact
  hence "\<turnstile> compE⇣2 c,compxE⇣2 c 0 (size ST) [::] ?τ⇣1 # ?τs⇣c @ [?τ⇣c]"
    using While.prems wtc by (auto simp:after_def)
  also have "?τs = (?τ # ?τs⇣e @ [?τ⇣e,?τ⇣1] @ ?τs⇣c) @ [?τ⇣c,?τ⇣2,?τ⇣1,?τ']" by simp
  also have "\<turnstile> [Pop],[] [::] [?τ⇣c, ?τ⇣2]"  by(simp add:wt_Pop)
  also have "(?τ # ?τs⇣e @ [?τ⇣e,?τ⇣1] @ ?τs⇣c) @ [?τ⇣c,?τ⇣2,?τ⇣1,?τ'] = ?τs" by simp
  also let ?go = "Goto (-int(?n⇣c+?n⇣e+2))"
  have "P \<turnstile> ?τ⇣2 ≤' ?τ" by(fastforce intro: ty⇣i'_antimono simp: hyperset_defs)
  hence "P,T⇣r,mxs,size ?τs,[] \<turnstile> ?go,?n⇣e+?n⇣c+2 :: ?τs"
    by(simp add: wt_Goto split: nat_diff_split)
  also have "?τs = (?τ # ?τs⇣e @ [?τ⇣e,?τ⇣1] @ ?τs⇣c @ [?τ⇣c, ?τ⇣2]) @ [?τ⇣1, ?τ']"
    by simp
  also have "\<turnstile> [Push Unit],[] [::] [?τ⇣1,?τ']"
    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 e⇣1 e⇣2)
  obtain T⇣1 T⇣2 where wte: "P,E \<turnstile>⇩1 e :: Boolean"
    and wt⇣1: "P,E \<turnstile>⇩1 e⇣1 :: T⇣1" and wt⇣2: "P,E \<turnstile>⇩1 e⇣2 :: T⇣2"
    and sub⇣1: "P \<turnstile> T⇣1 ≤ T" and sub⇣2: "P \<turnstile> T⇣2 ≤ T"
    using Cond by auto
  have [simp]: "ty E (if (e) e⇣1 else e⇣2) = T" using Cond by simp
  let ?A⇣0 = "A \<squnion> \<A> e" let ?A⇣2 = "?A⇣0 \<squnion> \<A> e⇣2" let ?A⇣1 = "?A⇣0 \<squnion> \<A> e⇣1"
  let ?A' = "?A⇣0 \<squnion> \<A> e⇣1 \<sqinter> \<A> e⇣2"
  let ?τ⇣2 = "ty⇣i' ST E ?A⇣0" let ?τ' = "ty⇣i' (T#ST) E ?A'"
  let ?τs⇣2 = "compT E ?A⇣0 ST e⇣2"
  have "PROP ?P e⇣2 E T⇣2 ?A⇣0 ST" by fact
  hence "\<turnstile> compE⇣2 e⇣2, compxE⇣2 e⇣2 0 (size ST) [::] (?τ⇣2#?τs⇣2) @ [ty⇣i' (T⇣2#ST) E ?A⇣2]"
    using Cond.prems wt⇣2 by(auto simp add:after_def)
  also have "P \<turnstile> ty⇣i' (T⇣2#ST) E ?A⇣2 ≤' ?τ'" using sub⇣2
    by(auto simp add: hyperset_defs ty⇣i'_def intro!: ty⇣l_antimono)
  also
  let ?τ⇣3 = "ty⇣i' (T⇣1 # ST) E ?A⇣1"
  let ?g⇣2 = "Goto(int (size (compE⇣2 e⇣2) + 1))"
  from sub⇣1 have "P,T⇣r,mxs,size(compE⇣2 e⇣2)+2,[] \<turnstile> ?g⇣2,0 :: ?τ⇣3#(?τ⇣2#?τs⇣2)@[?τ']"
    by(auto simp: hyperset_defs wt_defs nth_Cons ty⇣i'_def
             split:nat.split intro!: ty⇣l_antimono)
  also
  let ?τs⇣1 = "compT E ?A⇣0 ST e⇣1"
  have "PROP ?P e⇣1 E T⇣1 ?A⇣0 ST" by fact
  hence "\<turnstile> compE⇣2 e⇣1,compxE⇣2 e⇣1 0 (size ST) [::] ?τ⇣2 # ?τs⇣1 @ [?τ⇣3]"
    using Cond.prems wt⇣1 by(auto simp add:after_def)
  also
  let ?τs⇣1⇣2 = "?τ⇣2 # ?τs⇣1 @ ?τ⇣3 # (?τ⇣2 # ?τs⇣2) @ [?τ']"
  let ?τ⇣1 = "ty⇣i' (Boolean#ST) E ?A⇣0"
  let ?g⇣1 = "IfFalse(int (size (compE⇣2 e⇣1) + 2))"
  let ?code = "compE⇣2 e⇣1 @ ?g⇣2 # compE⇣2 e⇣2"
  have "\<turnstile> [?g⇣1],[] [::] [?τ⇣1] @ ?τs⇣1⇣2"
    by(simp add: wt_IfFalse nat_add_distrib split:nat_diff_split)
  also (wt_instrs_ext2) have "[?τ⇣1] @ ?τs⇣1⇣2 = ?τ⇣1 # ?τs⇣1⇣2" by simp also
  let ?τ = "ty⇣i' ST E A"
  have "PROP ?P e E Boolean A ST" by fact
  hence "\<turnstile> compE⇣2 e, compxE⇣2 e 0 (size ST) [::] ?τ # compT E A ST e @ [?τ⇣1]"
    using Cond.prems wte by(auto simp add:after_def)
  finally show ?case using wte wt⇣1 wt⇣2 by(simp add:after_def hyperUn_assoc)
next
  case (Call e M es)
  obtain C D Ts m Ts' where C: "P,E \<turnstile>⇩1 e :: Class C"
    and method: "P \<turnstile> C sees M:Ts -> T = m in D"
    and wtes: "P,E \<turnstile>⇩1 es [::] Ts'" and subs: "P \<turnstile> Ts' [≤] Ts"
    using Call.prems by auto
  from wtes have same_size: "size es = size Ts'" by(rule WTs⇣1_same_size)
  let ?A⇣0 = "A \<squnion> \<A> e" let ?A⇣1 = "?A⇣0 \<squnion> \<A>s es"
  let ?τ = "ty⇣i' ST E A" let ?τs⇣e = "compT E A ST e"
  let ?τ⇣e = "ty⇣i' (Class C # ST) E ?A⇣0"
  let ?τs⇣e⇣s = "compTs E ?A⇣0 (Class C # ST) es"
  let ?τ⇣1 = "ty⇣i' (rev Ts' @ Class C # ST) E ?A⇣1"
  let ?τ' = "ty⇣i' (T # ST) E ?A⇣1"
  have "\<turnstile> [Invoke M (size es)],[] [::] [?τ⇣1,?τ']"
    by(rule wt_Invoke[OF same_size method subs])
  also
  have "PROP ?Ps es E Ts' ?A⇣0 (Class C # ST)" by fact
  hence "\<turnstile> compEs⇣2 es,compxEs⇣2 es 0 (size ST+1) [::] ?τ⇣e # ?τs⇣e⇣s"
        "last (?τ⇣e # ?τs⇣e⇣s) = ?τ⇣1"
    using Call.prems wtes by(auto simp add:after_def)
  also have "(?τ⇣e # ?τs⇣e⇣s) @ [?τ'] = ?τ⇣e # ?τs⇣e⇣s @ [?τ']" by simp
  also have "\<turnstile> compE⇣2 e,compxE⇣2 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)
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)
qed
(*>*)


lemma [simp]: "types (compP f P) = types P"
(*<*)by auto(*>*)

lemma [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, τ)"
(*<*)
  apply (cases τ)  
  apply (cases i)
  apply auto
   apply (fastforce dest!: sees_method_compPD)
  apply (force dest: sees_method_compP)
  done
(*>*)
  
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]: "subtype (compP f P) = subtype P"
(*<*)
  apply (rule ext)+
  apply (simp)
  done
(*>*)
  
lemma [simp]: "compP f P \<turnstile> τ ≤' τ' = P \<turnstile> τ ≤' τ'"
(*<*) by (simp add: sup_state_opt_def sup_state_def sup_ty_opt_def)(*>*)

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

declare TC1.compT_sizes[simp]  TC0.ty_def2[simp]

context TC2
begin

lemma compT_method:
  fixes e and A and C and Ts and mxl⇣0
  defines [simp]: "E ≡ Class C # Ts"
    and [simp]: "A ≡ ⌊{..size Ts}⌋"
    and [simp]: "A' ≡ A \<squnion> \<A> e"
    and [simp]: "mxl⇣0 ≡ max_vars e"
  assumes mxs: "max_stack e = mxs"
    and mxl: "Suc (length Ts + max_vars e) = mxl"
  assumes assm: "wf_prog p P" "P,E \<turnstile>⇩1 e :: T" "\<D> e A" "\<B> e (size E)"
    "set E ⊆ types P" "P \<turnstile> T ≤ T⇣r"
  shows "wt_method (compP⇣2 P) C Ts T⇣r mxs mxl⇣0 (compE⇣2 e @ [Return])
    (compxE⇣2 e 0 0) (ty⇣i' [] E A # compT⇣a E A [] e)"
(*<*)
using assms apply (simp add: wt_method_def compT⇣a_def after_def mxl)
apply (rule conjI)
apply (simp add: check_types_def OK_ty⇣i'_in_statesI)
apply (rule conjI)
apply (drule (1) WT⇣1_is_type)
apply simp
apply (insert max_stack1 [of e])
apply (rule OK_ty⇣i'_in_statesI) apply (simp_all add: mxs)[3]
apply (erule compT_states(1))
apply assumption
apply (simp_all add: mxs mxl)[4]
apply (rule conjI)
apply (auto simp add: wt_start_def ty⇣i'_def ty⇣l_def list_all2_conv_all_nth
  nth_Cons mxl split: nat.split dest: less_antisym)[1]
apply (frule (1) TC2.compT_wt_instrs [of P _ _ _ _ "[]" "max_stack e" "Suc (length Ts + max_vars e)" T⇣r])
apply simp_all
apply (clarsimp simp: after_def)
apply (rule conjI)
apply (clarsimp simp: wt_instrs_def after_def mxl mxs)
apply clarsimp
apply (drule (1) less_antisym)
apply (clarsimp simp: wt_defs xcpt_app_pcs xcpt_eff_pcs ty⇣i'_def)
done
(*>*)

end

definition compTP :: "J⇣1_prog => ty⇣P" where
  "compTP P C M = (
  let (D,Ts,T,e) = method P C M;
       E = Class C # Ts;
       A = ⌊{..size Ts}⌋;
       mxl = 1 + size Ts + max_vars e
  in  (TC0.ty⇣i' mxl [] E A # TC1.compT⇣a P mxl E A [] e))"

theorem wt_compP⇣2:
  "wf_J⇣1_prog P ==> wf_jvm_prog (compP⇣2 P)"
(*<*)
  apply (simp add: wf_jvm_prog_def wf_jvm_prog_phi_def)
  apply(rule_tac x = "compTP P" in exI)
  apply (rule wf_prog_compPI)
   prefer 2 apply assumption
  apply (clarsimp simp add: wf_mdecl_def)
  apply (simp add: compTP_def)
  apply (rule TC2.compT_method [simplified])
       apply (rule refl)
       apply (rule refl)
       apply assumption
       apply assumption
       apply assumption
       apply assumption
    apply (drule (1) sees_wf_mdecl)
    apply (simp add: wf_mdecl_def)
   apply (blast intro: sees_method_is_class)
  apply assumption
  done
(*>*)

theorem wt_J2JVM:
  "wf_J_prog P ==> wf_jvm_prog (J2JVM P)"
(*<*)
apply(simp only:o_def J2JVM_def)
apply(blast intro:wt_compP⇣2 compP⇣1_pres_wf)
done

end