Theory TypeComp (Isabelle repository version)

(*  Title:      Jinja/Compiler/TypeComp.thy
    ID:         $Id: TypeComp.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Tobias Nipkow
    Copyright   TUM 2003
*)

header {* \isaheader{Preservation of Well-Typedness} *}
(*
ML{*add_path"../JVM/";add_path"../BV/";add_path"../DFA/"*}
*)

theory TypeComp = Compiler + BVSpec:

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

constdefs
  ty :: "J₁_prog => ty list => expr₁ => ty"
  "ty P E e  ≡  THE T. P,E \<turnstile>₁ e :: T"

  ty_l:: "nat => ty list => nat set => ty_l"
  "ty_l m E A' ≡ map (λi. if i ∈ A' ∧ i < size E then OK(E!i) else Err) [0..m(]"

  ty_i' :: "nat => ty list => ty list => nat set option => ty_i'"
  "ty_i' m ST E A ≡ case A of None => None | ⌊A'⌋ => Some(ST, ty_l m E A')"

  after :: "J₁_prog => nat => ty list => nat set option => ty list => expr₁ => ty_i'"
  "after P m E A ST e  ≡ ty_i' m (ty P E e # ST) E (A \<squnion> \<A> e)"

locale (open) TC0 =
  fixes P and mxl

  fixes ty :: "ty list => expr₁ => ty"
  defines "ty E e ≡ TypeComp.ty P E e"

  fixes ty_l:: "ty list => nat set => ty_l"
  defines ty_l: "ty_l E A' ≡ TypeComp.ty_l mxl E A'"

  fixes ty_i' :: "ty list => ty list => nat set option => ty_i'"
  defines ty_i': "ty_i' ST E A ≡ TypeComp.ty_i' mxl ST E A"

  fixes after :: "ty list => nat set option => ty list => expr₁ => ty_i'"
  defines after: "after E A ST e ≡ TypeComp.after P mxl E A ST e"

  notes after_def = TypeComp.after_def [of P mxl, folded after ty_def ty_i']
  notes ty_i'_def = TypeComp.ty_i'_def [of mxl, folded ty_l ty_i']
  notes ty_l_def = TypeComp.ty_l_def [of mxl, folded ty_l]

lemma (in TC0) ty_def2 [simp]: "P,E \<turnstile>₁ e :: T ==> ty E e = T"
(*<*)
apply(unfold ty_def TypeComp.ty_def)
apply(blast intro: the_equality WT₁_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)(*>*)


consts
 compT :: "J₁_prog => nat => ty list => nat hyperset => ty list => expr₁ => ty_i' list"
 compTs :: "J₁_prog => nat => ty list => nat hyperset => ty list => expr₁ list => ty_i' list"

primrec
"compT P m E A ST (new C) = []"
"compT P m E A ST (Cast C e) =  
   compT P m E A ST e @ [after P m E A ST e]"
"compT P m E A ST (Val v) = []"
"compT P m E A ST (e₁ «bop» e₂) =
  (let ST₁ = ty P E e₁#ST; A₁ = A \<squnion> \<A> e₁ in
   compT P m E A ST e₁ @ [after P m E A ST e₁] @
   compT P m E A₁ ST₁ e₂ @ [after P m E A₁ ST₁ e₂])"
"compT P m E A ST (Var i) = []"
"compT P m E A ST (i := e) = compT P m E A ST e @
   [after P m E A ST e, ty_i' m ST E (A \<squnion> \<A> e \<squnion> ⌊{i}⌋)]"
"compT P m E A ST (e\<bullet>F{D}) = 
   compT P m E A ST e @ [after P m E A ST e]"
"compT P m E A ST (e₁\<bullet>F{D} := e₂) =
  (let ST₁ = ty P E e₁#ST; A₁ = A \<squnion> \<A> e₁; A₂ = A₁ \<squnion> \<A> e₂ in
   compT P m E A ST e₁ @ [after P m E A ST e₁] @
   compT P m E A₁ ST₁ e₂ @ [after P m E A₁ ST₁ e₂] @
   [ty_i' m ST E A₂])"
"compT P m E A ST {i:T; e} = compT P m (E@[T]) (A\<ominus>i) ST e"
"compT P m E A ST (e₁;;e₂) =
  (let A₁ = A \<squnion> \<A> e₁ in
   compT P m E A ST e₁ @ [after P m E A ST e₁, ty_i' m ST E A₁] @
   compT P m E A₁ ST e₂)"
"compT P m E A ST (if (e) e₁ else e₂) =
   (let A₀ = A \<squnion> \<A> e; τ = ty_i' m ST E A₀ in
    compT P m E A ST e @ [after P m E A ST e, τ] @
    compT P m E A₀ ST e₁ @ [after P m E A₀ ST e₁, τ] @
    compT P m E A₀ ST e₂)"
"compT P m E A ST (while (e) c) =
   (let A₀ = A \<squnion> \<A> e;  A₁ = A₀ \<squnion> \<A> c; τ = ty_i' m ST E A₀ in
    compT P m E A ST e @ [after P m E A ST e, τ] @
    compT P m E A₀ ST c @ [after P m E A₀ ST c, ty_i' m ST E A₁, ty_i' m ST E A₀])"
"compT P m E A ST (throw e) = compT P m E A ST e @ [after P m E A ST e]"
"compT P m E A ST (e\<bullet>M(es)) =
   compT P m E A ST e @ [after P m E A ST e] @
   compTs P m E (A \<squnion> \<A> e) (ty P E e # ST) es"
"compT P m E A ST (try e₁ catch(C i) e₂) =
   compT P m E A ST e₁ @ [after P m E A ST e₁] @
   [ty_i' m (Class C#ST) E A, ty_i' m ST (E@[Class C]) (A \<squnion> ⌊{i}⌋)] @
   compT P m (E@[Class C]) (A \<squnion> ⌊{i}⌋) ST e₂"
"compTs P m E A ST [] = []"
"compTs P m E A ST (e#es) = compT P m E A ST e @ [after P m E A ST e] @
                            compTs P m E (A \<squnion> (\<A> e)) (ty P E e # ST) es"

constdefs
  compT_a :: "J₁_prog => nat => ty list => nat hyperset => ty list => expr₁ => ty_i' list"
  "compT_a P mxl E A ST e ≡ compT P mxl E A ST e @ [after P mxl E A ST e]"

locale (open) TC1 = TC0 +
  fixes compT :: "ty list => nat hyperset => ty list => expr₁ => ty_i' list"
  defines compT: "compT E A ST e ≡ TypeComp.compT P mxl E A ST e"

  fixes compTs :: "ty list => nat hyperset => ty list => expr₁ list => ty_i' list"
  defines compTs: "compTs E A ST es ≡ TypeComp.compTs P mxl E A ST es"

  fixes compT_a :: "ty list => nat hyperset => ty list => expr₁ => ty_i' list"
  defines compT_a: "compT_a E A ST e ≡ TypeComp.compT_a P mxl E A ST e"

  notes compT_simps[simp] = TypeComp.compT_compTs.simps [of P mxl,
        folded compT compTs ty_def ty_i' after]
  notes compT_a_def = TypeComp.compT_a_def[of P mxl,
        folded compT_a compT after]

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


lemma (in TC1) compT_sizes[simp]:
shows "!!E A ST. size(compT E A ST e) = size(compE₂ e) - 1"
and "!!E A ST. size(compTs E A ST es) = size(compEs₂ 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₀ E A) =
  (case A of None => False | Some A => (ST = ST₀ ∧ 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₀. [| ⌊(ST,LT)⌋ ∈ set(compT E A ST₀ e); \<B> e (size E) |]
               ==> P \<turnstile> ⌊(ST,LT)⌋ ≤' ty_i' ST E A"
and
 "!!E A ST₀. [| ⌊(ST,LT)⌋ ∈ set(compTs E A ST₀ 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(fastsimp simp:hyperset_defs elim!:sup_state_opt_trans)
next
  case BinOp thus ?case
    by(fastsimp simp:hyperset_defs elim!:sup_state_opt_trans split:bop.splits)
next
  case Seq thus ?case by(fastsimp simp:hyperset_defs elim!:sup_state_opt_trans)
next
  case While thus ?case by(fastsimp simp:hyperset_defs elim!:sup_state_opt_trans)
next
  case Cond thus ?case by(fastsimp 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(fastsimp simp:hyperset_defs elim!:sup_state_opt_trans)
next
  case Cons_exp thus ?case
    by(fastsimp simp:hyperset_defs elim!:sup_state_opt_trans)
next
  case TryCatch thus ?case
    by(fastsimp 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>₁ 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₁_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>₁ 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>₁ 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₁_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₁_is_type[OF wf] after_in_states[OF wf])
next
  case Cond thus ?case
    by(force simp:image_Un WT₁_is_type[OF wf] after_in_states[OF wf])
next
  case While thus ?case
    by(auto simp:image_Un WT₁_is_type[OF wf] after_in_states[OF wf])
next
  case Block thus ?case by(auto)
next
  case (TryCatch 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 WT₁_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₁_is_type[OF wf] after_in_states[OF wf])
next
  case throw thus ?case
    by(auto simp: WT₁_is_type[OF wf] after_in_states[OF wf])
next
  case Call thus ?case
    by(auto simp:image_Un WT₁_is_type[OF wf] after_in_states[OF wf])
qed

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


constdefs
  shift :: "nat => ex_table => ex_table"
  "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₁ @ xt₂) = shift n xt₁ @ shift n xt₂"
(*<*)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₂:
shows "!!pc pc' d. shift pc (compxE₂ e pc' d) = compxE₂ e (pc' + pc) d"
and  "!!pc pc' d. shift pc (compxEs₂ es pc' d) = compxEs₂ es (pc' + pc) d"
(*<*)
apply(induct e and es)
apply(auto simp:shift_def add_ac)
done
(*>*)


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


constdefs
  wt_instrs :: "'m prog => ty => pc => instr list => ex_table => ty_i' list => bool"
  ("(_,_,_ \<turnstile>/ _, _ /[::]/ _)" [50,50,50,50,50,51] 50)
  "P,T,mxs \<turnstile> is,xt [::] τs ≡
  size is < size τs ∧ pcs xt ⊆ {0..size is(} ∧
  (∀pc< size is. P,T,mxs,size τs,xt \<turnstile> is!pc,pc :: τs)"

locale (open) TC2 = TC1 +
  fixes T_r and mxs
  fixes wt_instrs :: "instr list => ex_table => ty_i' list => bool"
                     ("(\<turnstile> _, _ /[::]/ _)" [0,0,51] 50)
  defines wt_instrs: "\<turnstile> is,xt [::] τs ≡ P,T_r,mxs \<turnstile> is,xt [::] τs"

  notes wt_instrs_def = TypeComp.wt_instrs_def[of P T_r mxs, folded wt_instrs]

(*<*)
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 (fastsimp 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 map_compose [symmetric])
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)
apply arith
apply arith
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₁,xt₁ [::] τs₁@τs₂; \<turnstile> is₂,xt₂ [::] τs₂; size τs₁ = size is₁ |]
  ==> \<turnstile> is₁@is₂, xt₁ @ shift (size is₁) xt₂ [::] τs₁@τs₂"
(*<*)
apply(clarsimp simp:wt_instrs_def)
apply(rule conjI, fastsimp)
apply(rule conjI, fastsimp)
apply clarsimp
apply(rule conjI, fastsimp simp:wt_instr_appRx)
apply clarsimp
apply(erule_tac x = "pc - size is₁" in allE)+
apply(erule impE,arith)
apply(drule_tac τs' = "τs₁" in wt_instr_appL)
  apply arith
 apply simp
apply(fastsimp simp add:add_commute intro!: wt_instr_appLx)
done
(*>*)

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


corollary (in TC2) wt_instrs_ext_prefix [trans]:
  "[| \<turnstile> is₁,xt₁ [::] τs₁@τs₂; \<turnstile> is₂,xt₂ [::] τs₃;
     size τs₁ = size is₁; τs₃ ≤ τs₂ |]
  ==> \<turnstile> is₁@is₂, xt₁ @ shift (size is₁) xt₂ [::] τs₁@τs₂"
(*<*)by(bestsimp simp:prefix_def elim: wt_instrs_ext dest:wt_instrs_extR)(*>*)


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


corollary (in TC2) wt_instrs_app_last[trans]:
  "[| \<turnstile> is₂,xt₂ [::] τ#τs₂; \<turnstile> is₁,xt₁ [::] τs₁;
     last τs₁ = τ;  size τs₁ = size is₁+1 |]
  ==> \<turnstile> 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 (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, fastsimp)
apply(fastsimp intro!:wt_instr_appLx[where xt = "[]",simplified]
               dest!:less_antisym)
done
(*>*)


(*<*)
ML_setup {* simpset_ref() := simpset() delloop "split_all_tac" *}
(*>*)


corollary (in TC2) wt_instrs_app2:
  "[| \<turnstile> is₂,xt₂ [::] τ'#τs₂;  \<turnstile> is₁,xt₁ [::] τ#τs₁@[τ'];
     xt' = xt₁ @ shift (size is₁) xt₂;  size τs₁+1 = size is₁ |]
  ==> \<turnstile> is₁@is₂,xt' [::] τ#τs₁@τ'#τs₂"
(*<*)using wt_instrs_app[where ?τs₁.0 = "τ # τs₁"] by simp (*>*)


corollary (in TC2) wt_instrs_app2_simp[trans,simp]:
  "[| \<turnstile> is₂,xt₂ [::] τ'#τs₂;  \<turnstile> is₁,xt₁ [::] τ#τs₁@[τ']; size τs₁+1 = size is₁ |]
  ==> \<turnstile> is₁@is₂, xt₁@shift (size is₁) xt₂ [::] τ#τs₁@τ'#τs₂"
(*<*)using wt_instrs_app[where ?τs₁.0 = "τ # τs₁"] 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₁.0 = "[i]" and ?τs₁.0 = "[]" and ?is₂.0 = "is"
                      and ?xt₁.0 = "[]"]
by simp

ML_setup
  {*simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)*}
(*>*)


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 (fastsimp 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(fastsimp)
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₁ ≤ T₂ ∨ P \<turnstile> T₂ ≤ T₁|]
  ==> \<turnstile> [CmpEq],[] [::] [ty_i' (T₂ # T₁ # 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"
(*<*)
apply(clarsimp simp add: ty_i'_def wt_defs)
apply(auto simp add: nth_Cons split:nat.split)
apply arith
apply(simp add:nat_diff_distrib)
done
(*>*)


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(fastsimp simp add: ty_i'_def wt_defs)(*>*)

(*<*)
ML_setup {* simpset_ref() := simpset() delloop "split_all_tac"*}
(*>*)


corollary (in TC2) wt_instrs_app3[simp]:
  "[| \<turnstile> is₂,[] [::] (τ' # τs₂);  \<turnstile> is₁,xt₁ [::] τ # τs₁ @ [τ']; size τs₁+1 = size is₁|]
  ==> \<turnstile> (is₁ @ is₂),xt₁ [::] τ # τs₁ @ τ' # τs₂"
(*<*)using wt_instrs_app2[where ?xt₂.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)

ML_setup
  {* simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac) *}
(*>*)

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

lemma (in TC2) wt_instrs_xapp[trans]:
  "[| \<turnstile> is₁ @ is₂, xt [::] τs₁ @ ty_i' (Class C # ST) E A # τs₂;
     ∀τ ∈ set τs₁. ∀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₁ = size τs₁; is_class P C; size ST < mxs  |] ==>
  \<turnstile> is₁ @ is₂, xt @ [(0,size is₁ - 1,C,size is₁,size ST)] [::] τs₁ @ ty_i' (Class C # ST) E A # τs₂"
(*<*)
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₁!pc" in bspec)
   apply (blast intro: nth_mem) 
  apply fastsimp   
 apply arith
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₁!pc" in bspec)
  apply (blast intro: nth_mem) 
 apply (fastsimp simp add: ty_i'_def)
apply arith
done

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

(*<*)
declare (in TC0)
  after_def[simp] pair_eq_ty_i'_conv[simp]
(*>*)

lemma (in TC1) compT_ST_prefix:
 "!!E A ST₀. ⌊(ST,LT)⌋ ∈ set(compT E A ST₀ e) ==> 
  size ST₀ ≤ size ST ∧ drop (size ST - size ST₀) ST = ST₀"
and
 "!!E A ST₀. ⌊(ST,LT)⌋ ∈ set(compTs E A ST₀ es) ==> 
  size ST₀ ≤ size ST ∧ drop (size ST - size ST₀) ST = ST₀"
(*<*)
proof(induct e and es)
  case (FAss e₁ F D e₂)
  moreover {
    let ?ST₀ = "ty E e₁ # ST₀"
    fix A assume "⌊(ST, LT)⌋ ∈ set (compT E A ?ST₀ e₂)"
    with FAss
    have "length ?ST₀ ≤ length ST ∧ drop (size ST - size ?ST₀) ST = ?ST₀" 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₀ = "ty E e # ST₀"
    fix A assume "⌊(ST, LT)⌋ ∈ set (compTs E A ?ST₀ es)"
    with Call
    have "length ?ST₀ ≤ length ST ∧ drop (size ST - size ?ST₀) ST = ?ST₀" by blast
    hence ?case  by (clarsimp simp add: drop_mess)
  }
  ultimately show ?case by auto
next
  case (Cons_exp e es)
  moreover {
    let ?ST₀ = "ty E e # ST₀"
    fix A assume "⌊(ST, LT)⌋ ∈ set (compTs E A ?ST₀ es)"
    with Cons_exp
    have "length ?ST₀ ≤ length ST ∧ drop (size ST - size ?ST₀) ST = ?ST₀" by blast
    hence ?case  by (clarsimp simp add: drop_mess)
  }
  ultimately show ?case by auto
next
  case (BinOp e₁ bop e₂)
  moreover {
    let ?ST₀ = "ty E e₁ # ST₀"
    fix A assume "⌊(ST, LT)⌋ ∈ set (compT E A ?ST₀ e₂)"
    with BinOp 
    have "length ?ST₀ ≤ length ST ∧ drop (size ST - size ?ST₀) ST = ?ST₀" 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>₁ e :: T; \<D> e A; \<B> e (size E); 
    size ST + max_stack e ≤ mxs; size E + max_vars e ≤ mxl |]
  ==> \<turnstile> compE₂ e, compxE₂ 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>₁ 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₂ es,compxEs₂ 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₁ C i e₂)
  hence [simp]: "i = size E" by simp
  have wt₁: "P,E \<turnstile>₁ e₁ :: T" and wt₂: "P,E@[Class C] \<turnstile>₁ e₂ :: T"
    and class: "is_class P C" using TryCatch by auto
  let ?A₁ = "A \<squnion> \<A> e₁" let ?A_i = "A \<squnion> ⌊{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 \<squnion> \<A> e₂)"
  let ?τ' = "ty_i' (T#ST) E (A \<squnion> \<A> e₁ \<sqinter> (\<A> e₂ \<ominus> i))"
  let ?go = "Goto (int(size(compE₂ e₂)) + 2)"
  have "PROP ?P e₂ ?E_i T ?A_i ST".
  hence "\<turnstile> compE₂ e₂,compxE₂ e₂ 0 (size ST) [::] (?τ₃ # ?τs₂) @ [?τ₂']"
    using TryCatch.prems by(auto simp:after_def)
  also have "?A_i \<squnion> \<A> e₂ = (A \<squnion> \<A> e₂) \<squnion> ⌊{size E}⌋"
    by(fastsimp simp:hyperset_defs)
  also have "P \<turnstile> ty_i' (T#ST) ?E_i … ≤' ty_i' (T#ST) E (A \<squnion> \<A> e₂)"
    by(simp add:hyperset_defs ty_l_incr ty_i'_def)
  also have "P \<turnstile> … ≤' ty_i' (T#ST) E (A \<squnion> \<A> e₁ \<sqinter> (\<A> e₂ \<ominus> i))"
    by(auto intro!: ty_l_antimono simp:hyperset_defs ty_i'_def)
  also have "(?τ₃ # ?τs₂) @ [?τ'] = ?τ₃ # ?τs₂ @ [?τ']" by simp
  also have "\<turnstile> [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(compE₂ e₂)+3,[] \<turnstile> ?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 "\<turnstile> compE₂ e₁,compxE₂ e₁ 0 (size ST) [::] ?τ # ?τs₁ @ [?τ₁]"
    using TryCatch by(auto simp:after_def)
  also have "?τ # ?τs₁ @ ?τ₁ # ?τ₂ # ?τ₃ # ?τs₂ @ [?τ'] =
             (?τ # ?τs₁ @ [?τ₁]) @ ?τ₂ # ?τ₃ # ?τs₂ @ [?τ']" by simp
  also have "compE₂ e₁ @ ?go  # [Store i] @ compE₂ e₂ =
             (compE₂ e₁ @ [?go]) @ (Store i # compE₂ e₂)" 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₁)" 
      by (fastsimp simp add: ty_i'_def hyperset_defs intro!: ty_l_antimono)
    moreover have "!!τ. τ ∈ set (compT E A ST e₁) ==> ?Q τ" using TryCatch.prems
      by clarsimp (frule compT_ST_prefix,
                   fastsimp 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)
next
  case new thus ?case by(auto simp add:after_def wt_New)
next
  case (BinOp e₁ bop e₂) 
  let ?op = "case bop of Eq => [CmpEq] | Add => [IAdd]"
  have T: "P,E \<turnstile>₁ e₁ «bop» e₂ :: T" .
  then obtain T₁ T₂ where T₁: "P,E \<turnstile>₁ e₁ :: T₁" and T₂: "P,E \<turnstile>₁ e₂ :: T₂" and 
    bopT: "case bop of Eq => (P \<turnstile> T₁ ≤ T₂ ∨ P \<turnstile> T₂ ≤ T₁) ∧ T = Boolean 
                    | Add => T₁ = Integer ∧ T₂ = Integer ∧ T = Integer" by auto
  let ?A₁ = "A \<squnion> \<A> e₁" let ?A₂ = "?A₁ \<squnion> \<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 "\<turnstile> ?op,[] [::] [?τ₂,?τ']" 
    by (cases bop) (auto simp add: wt_CmpEq wt_IAdd)
  also have "PROP ?P e₂ E T₂ ?A₁ (T₁#ST)" .
  with BinOp.prems T₂ 
  have "\<turnstile> compE₂ e₂, compxE₂ e₂ 0 (size (T₁#ST)) [::] ?τ₁#?τs₂@[?τ₂]" 
    by (auto simp: after_def)
  also from BinOp T₁ have "\<turnstile> compE₂ e₁, compxE₂ 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_exp e es)
  have "P,E \<turnstile>₁ e # es [::] Ts" .
  then obtain T_e Ts' where 
    T_e: "P,E \<turnstile>₁ e :: T_e" and Ts': "P,E \<turnstile>₁ 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)" .
  with Cons_exp.prems T_e Ts'
  have "\<turnstile> compEs₂ es, compxEs₂ es 0 (size (T_e#ST)) [::] ?τ_e#?τs'" by (simp add: after_def)
  also from Cons_exp T_e have "\<turnstile> compE₂ e, compxE₂ 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₁ F D e₂)
  hence Void: "P,E \<turnstile>₁ e₁\<bullet>F{D} := e₂ :: Void" by auto
  then obtain C T T' where    
    C: "P,E \<turnstile>₁ e₁ :: Class C" and sees: "P \<turnstile> C sees F:T in D" and
    T': "P,E \<turnstile>₁ e₂ :: T'" and T'_T: "P \<turnstile> T' ≤ T" by auto
  let ?A₁ = "A \<squnion> \<A> e₁" let ?A₂ = "?A₁ \<squnion> \<A> e₂"  
  let ?τ = "ty_i' ST E A" let ?τs₁ = "compT E A ST e₁"
  let ?τ₁ = "ty_i' (Class C#ST) E ?A₁" let ?τs₂ = "compT E ?A₁ (Class C#ST) e₂"
  let ?τ₂ = "ty_i' (T'#Class C#ST) E ?A₂" let ?τ₃ = "ty_i' ST E ?A₂"
  let ?τ' = "ty_i' (Void#ST) E ?A₂"
  from FAss.prems sees T'_T 
  have "\<turnstile> [Putfield F D,Push Unit],[] [::] [?τ₂,?τ₃,?τ']"
    by (fastsimp simp add: wt_Push wt_Put)
  also have "PROP ?P e₂ E T' ?A₁ (Class C#ST)".
  with FAss.prems T' 
  have "\<turnstile> compE₂ e₂, compxE₂ e₂ 0 (size ST+1) [::] ?τ₁#?τs₂@[?τ₂]"
    by (auto simp add: after_def hyperUn_assoc) 
  also from FAss C have "\<turnstile> compE₂ e₁, compxE₂ 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 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" .
  hence "\<turnstile> compE₂ e, compxE₂ 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>₁ e :: Boolean" and wtc: "P,E \<turnstile>₁ 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 \<squnion> \<A> e" let ?A₁ = "?A₀ \<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₀" 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 "\<turnstile> [],[] [::] [] @ ?τs" by(simp add:wt_instrs_def)
  also
  have "PROP ?P e E Boolean A ST" .
  hence "\<turnstile> compE₂ e,compxE₂ e 0 (size ST) [::] ?τ # ?τs_e @ [?τ_e]"
    using While.prems by (auto simp:after_def)
  also
  have "[] @ ?τs = (?τ # ?τs_e) @ ?τ_e # ?τ₁ # ?τs_c @ [?τ_c,?τ₂,?τ₁,?τ']" by simp
  also
  let ?n_e = "size(compE₂ e)"  let ?n_c = "size(compE₂ c)"
  let ?if = "IfFalse (int ?n_c + 3)"
  have "\<turnstile> [?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
  have "PROP ?P c E Tc ?A₀ ST" .
  hence "\<turnstile> compE₂ c,compxE₂ c 0 (size ST) [::] ?τ₁ # ?τs_c @ [?τ_c]"
    using While.prems wtc by (auto simp:after_def)
  also have "?τs = (?τ # ?τs_e @ [?τ_e,?τ₁] @ ?τs_c) @ [?τ_c,?τ₂,?τ₁,?τ']" by simp
  also have "\<turnstile> [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 \<turnstile> ?τ₂ ≤' ?τ" by(fastsimp 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,?τ₁] @ ?τs_c @ [?τ_c, ?τ₂]) @ [?τ₁, ?τ']"
    by simp
  also have "\<turnstile> [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) (simp add:nat_number)
next
  case (Cond e e₁ e₂)
  obtain T₁ T₂ where wte: "P,E \<turnstile>₁ e :: Boolean"
    and wt₁: "P,E \<turnstile>₁ e₁ :: T₁" and wt₂: "P,E \<turnstile>₁ e₂ :: T₂"
    and sub₁: "P \<turnstile> T₁ ≤ T" and sub₂: "P \<turnstile> T₂ ≤ T"
    using Cond by auto
  have [simp]: "ty E (if (e) e₁ else e₂) = T" using Cond by simp
  let ?A₀ = "A \<squnion> \<A> e" let ?A₂ = "?A₀ \<squnion> \<A> e₂" let ?A₁ = "?A₀ \<squnion> \<A> e₁"
  let ?A' = "?A₀ \<squnion> \<A> e₁ \<sqinter> \<A> 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" .
  hence "\<turnstile> compE₂ e₂, compxE₂ e₂ 0 (size ST) [::] (?τ₂#?τs₂) @ [ty_i' (T₂#ST) E ?A₂]"
    using Cond.prems wt₂ by(auto simp add:after_def)
  also have "P \<turnstile> 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 (compE₂ e₂) + 1))"
  have "P,T_r,mxs,size(compE₂ e₂)+2,[] \<turnstile> ?g₂,0 :: ?τ₃#(?τ₂#?τs₂)@[?τ']"
    by(auto simp: hyperset_defs wt_defs nth_Cons ty_i'_def
             split:nat.split intro!: ty_l_antimono)
  also
  let ?τs₁ = "compT E ?A₀ ST e₁"
  have "PROP ?P e₁ E T₁ ?A₀ ST" .
  hence "\<turnstile> compE₂ e₁,compxE₂ 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 (compE₂ e₁) + 2))"
  let ?code = "compE₂ e₁ @ ?g₂ # compE₂ e₂"
  have "\<turnstile> [?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" .
  hence "\<turnstile> compE₂ e, compxE₂ 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 M es)
  obtain C D Ts m Ts' where C: "P,E \<turnstile>₁ e :: Class C"
    and method: "P \<turnstile> C sees M:Ts -> T = m in D"
    and wtes: "P,E \<turnstile>₁ 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₁_same_size)
  let ?A₀ = "A \<squnion> \<A> e" let ?A₁ = "?A₀ \<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₀"
  let ?τs_e_s = "compTs E ?A₀ (Class C # ST) es"
  let ?τ₁ = "ty_i' (rev Ts' @ Class C # ST) E ?A₁"
  let ?τ' = "ty_i' (T # ST) E ?A₁"
  have "\<turnstile> [Invoke M (size es)],[] [::] [?τ₁,?τ']"
    by(rule wt_Invoke[OF same_size method subs])
  also
  have "PROP ?Ps es E Ts' ?A₀ (Class C # ST)".
  hence "\<turnstile> compEs₂ es,compxEs₂ es 0 (size ST+1) [::] ?τ_e # ?τs_e_s"
        "last (?τ_e # ?τs_e_s) = ?τ₁"
    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₂ e,compxE₂ 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)
      (fastsimp 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 (fastsimp 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 (fastsimp 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]

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 \<squnion> \<A> e"
    and [simp]: "mxs ≡ max_stack e"
    and [simp]: "mxl₀ ≡ max_vars e"
    and [simp]: "mxl ≡ 1 + size Ts + mxl₀"
shows "[| wf_prog p P; P,E \<turnstile>₁ e :: T; \<D> e A; \<B> e (size E); 
          set E ⊆ types P; P \<turnstile> T ≤ T' |] ==>
   wt_method (compP₂ P) C Ts T' mxs mxl₀ (compE₂ e @ [Return]) (compxE₂ e 0 0)
      (ty_i' mxl [] E A # compT_a P mxl E A [] e)"
(*<*)
apply(simp add:wt_method_def compT_a_def after_def)
apply(rule conjI)
apply(simp add:check_types_def TC0.OK_ty_i'_in_statesI)
apply(rule conjI)
apply(drule (1) WT₁_is_type)
apply simp
apply(insert max_stack1[of e])
apply(fastsimp intro!: TC0.OK_ty_i'_in_statesI)
apply(erule (1) TC1.compT_states)
apply simp
apply simp
apply simp
apply simp
apply(rule conjI)
apply(fastsimp simp add:wt_start_def ty_i'_def ty_l_def list_all2_conv_all_nth nth_Cons split:nat.split dest:less_antisym)
apply (frule (1) TC2.compT_wt_instrs
 [where ST = "[]" and mxs = "max_stack e" and mxl = "1 + size Ts + max_vars e"])
apply simp
apply simp
apply simp
apply simp
apply (clarsimp simp:wt_instrs_def after_def)
apply(rule conjI)
apply clarsimp apply (fastsimp)
apply(clarsimp)
apply(drule (1) less_antisym)
apply(thin_tac "∀x. ?P x")
apply(clarsimp simp:TC2.wt_defs xcpt_app_pcs xcpt_eff_pcs ty_i'_def)
apply(cases "size (compE₂ e)")
 apply (simp del: compxE₂_size_convs nth_append  add: neq_Nil_conv)
apply (simp)
done
(*>*)


constdefs
  compTP :: "J₁_prog => ty_P"
  "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  (ty_i' mxl [] E A # compT_a P mxl E A [] e)"

theorem wt_compP₂:
  "wf_J₁_prog P ==> wf_jvm_prog (compP₂ 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 compT_method [simplified])
       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₂ compP₁_pres_wf)
done
(*>*)


end

lemma ty_def2:

  WT₁ P E e T ==> ty P E e = T

lemma

  ty_i' mxl ST E None = None

lemma ty_l_app_diff:

  ty_l mxl (E @ [T]) (A - {length E}) = ty_l mxl E A

lemma ty_i'_app_diff:

  ty_i' mxl ST (E @ [T]) (A \<ominus> length E) = ty_i' mxl ST E A

lemma ty_l_antimono:

  A <= A' ==> P |- ty_l mxl E A' [<=T] ty_l mxl E A

lemma ty_i'_antimono:

  A <= A' ==> P |- ty_i' mxl ST E ⌊A'⌋ <=' ty_i' mxl ST E ⌊A⌋

lemma ty_l_env_antimono:

  P |- ty_l mxl (E @ [T]) A [<=T] ty_l mxl E A

lemma ty_i'_env_antimono:

  P |- ty_i' mxl ST (E @ [T]) A <=' ty_i' mxl ST E A

lemma ty_i'_incr:

  P |- ty_i' mxl ST (E @ [T]) ⌊insert (length E) A⌋ <=' ty_i' mxl ST E ⌊A⌋

lemma ty_l_incr:

  P |- ty_l mxl (E @ [T]) (insert (length E) A) [<=T] ty_l mxl E A

lemma ty_l_in_types:

  set E <= types P ==> ty_l mxl E A : list mxl (err (types P))

lemma compE₂_not_Nil:

  compE₂ e ~= []

lemma

  length (compT P mxl E A ST e) = length (compE₂ e) - 1

and

  length (compTs P mxl E A ST es) = length (compEs₂ es)

lemma

  ⌊τ⌋ ~: set (compT P mxl E None ST e)

and

  ⌊τ⌋ ~: set (compTs P mxl E None ST es)

lemma pair_eq_ty_i'_conv:

  (⌊(ST, LT)⌋ = ty_i' mxl ST₀ E A) =
  (case A of None => False | ⌊A⌋ => ST = ST₀ & LT = ty_l mxl E A)

lemma pair_conv_ty_i':

  ⌊(ST, ty_l mxl E A)⌋ = ty_i' mxl ST E ⌊A⌋

lemma compT_LT_prefix:

  [| ⌊(ST, LT)⌋ : set (compT P mxl E A ST₀ e); \<B> e (length E) |]
  ==> P |- ⌊(ST, LT)⌋ <=' ty_i' mxl ST E A

and

  [| ⌊(ST, LT)⌋ : set (compTs P mxl E A ST₀ es); \<B>s es (length E) |]
  ==> P |- ⌊(ST, LT)⌋ <=' ty_i' mxl ST E A

lemma

  OK None : states P mxs mxl

lemma after_in_states:

  [| wf_prog p P; WT₁ P E e T; set E <= types P; set ST <= types P;
     length ST + max_stack e <= mxs |]
  ==> OK (after P mxl E A ST e) : states P mxs mxl

lemma OK_ty_i'_in_statesI:

  [| set E <= types P; set ST <= types P; length ST <= mxs |]
  ==> OK (ty_i' mxl ST E A) : states P mxs mxl

lemma is_class_type_aux:

  is_class P C ==> is_type P (Class C)

theorem

  [| wf_prog p P; WT₁ P E e T; set E <= types P; set ST <= types P;
     length ST + max_stack e <= mxs; length E + max_vars e <= mxl |]
  ==> OK ` set (compT P mxl E A ST e) <= states P mxs mxl

and

  [| wf_prog p P; WTs₁ P E es Ts; set E <= types P; set ST <= types P;
     length ST + max_stacks es <= mxs; length E + max_varss es <= mxl |]
  ==> OK ` set (compTs P mxl E A ST es) <= states P mxs mxl

lemma

  shift 0 xt = xt

lemma

  shift n [] = []

lemma

  shift n (xt₁ @ xt₂) = shift n xt₁ @ shift n xt₂

lemma

  shift m (shift n xt) = shift (m + n) xt

lemma

  pcs (shift n xt) = {pc + n |pc. pc : pcs xt}

lemma

  shift pc (compxE₂ e pc' d) = compxE₂ e (pc' + pc) d

and

  shift pc (compxEs₂ es pc' d) = compxEs₂ es (pc' + pc) d

lemma

  n ~= 0 ==> compxE₂ e n d = shift n (compxE₂ e 0 d)

and

  n ~= 0 ==> compxEs₂ es n d = shift n (compxEs₂ es 0 d)

lemmas wt_defs:

  P,T_r,mxs \<turnstile> is, xt [::] τs ==
  length is < length τs &
  pcs xt <= {0..length is(} &
  (ALL pc<length is. P,T_r,mxs,length τs,xt \<turnstile> is ! pc,pc :: τs)

  P,T,mxs,mpc,xt \<turnstile> i,pc :: τs ==
  app i P mxs T pc mpc xt (τs ! pc) &
  (ALL (pc', τ'):set (eff i P pc xt (τs ! pc)). P |- τ' <=' τs ! pc')

  app i P mxs T_r pc mpc xt t ==
  case t of None => True
  | ⌊τ⌋ =>
      app_i (i, P, pc, mxs, T_r, τ) &
      xcpt_app i P pc mxs xt τ & (ALL (pc', τ'):set (eff i P pc xt t). pc' < mpc)

  eff i P pc et t ==
  case t of None => [] | ⌊τ⌋ => norm_eff i P pc τ @ xcpt_eff i P pc τ et

  norm_eff i P pc τ == map (%pc'. (pc', ⌊eff_i (i, P, τ)⌋)) (succs i τ pc)

lemma

  τs ~= [] ==> P,T_r,mxs \<turnstile> [], [] [::] τs

lemma

  eff i P pc et None = []

lemma wt_instr_appR:

  [| P,T,m,mpc,xt \<turnstile> is ! pc,pc :: τs; pc < length is;
     length is < length τs; mpc <= length τs; mpc <= mpc' |]
  ==> P,T,m,mpc',xt \<turnstile> is ! pc,pc :: τs @ τs'

lemma relevant_entries_shift:

  relevant_entries P i (pc + n) (shift n xt) =
  shift n (relevant_entries P i pc xt)

lemma

  xcpt_eff i P (pc + n) τ (shift n xt) =
  map (%(pc, τ). (pc + n, τ)) (xcpt_eff i P pc τ xt)

lemma

  app_i (i, P, pc, m, T, τ)
  ==> eff i P (pc + n) (shift n xt) ⌊τ⌋ =
      map (%(pc, τ). (pc + n, τ)) (eff i P pc xt ⌊τ⌋)

lemma

  xcpt_app i P (pc + n) mxs (shift n xt) τ = xcpt_app i P pc mxs xt τ

lemma wt_instr_appL:

  [| P,T,m,mpc,xt \<turnstile> i,pc :: τs; pc < length τs; mpc <= length τs |]
  ==> P,T,m,mpc +
            length
             τs',shift (length τs') xt \<turnstile> i,pc + length τs' :: τs' @ τs

lemma wt_instr_Cons:

  [| P,T,m,mpc - 1,[] \<turnstile> i,pc - 1 :: τs; 0 < pc; 0 < mpc;
     pc < length τs + 1; mpc <= length τs + 1 |]
  ==> P,T,m,mpc,[] \<turnstile> i,pc :: τ # τs

lemma wt_instr_append:

  [| P,T,m,mpc - length τs',[] \<turnstile> i,pc - length τs' :: τs;
     length τs' <= pc; length τs' <= mpc; pc < length τs + length τs';
     mpc <= length τs + length τs' |]
  ==> P,T,m,mpc,[] \<turnstile> i,pc :: τs' @ τs

lemma xcpt_app_pcs:

  pc ~: pcs xt ==> xcpt_app i P pc mxs xt τ

lemma xcpt_eff_pcs:

  pc ~: pcs xt ==> xcpt_eff i P pc τ xt = []

lemma pcs_shift:

  pc < n ==> pc ~: pcs (shift n xt)

lemma wt_instr_appRx:

  [| P,T,m,mpc,xt \<turnstile> is ! pc,pc :: τs; pc < length is;
     length is < length τs; mpc <= length τs |]
  ==> P,T,m,mpc,xt @ shift (length is) xt' \<turnstile> is ! pc,pc :: τs

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

lemma wt_instrs_extR:

  P,T_r,mxs \<turnstile> is, xt [::] τs
  ==> P,T_r,mxs \<turnstile> is, xt [::] τs @ τs'

lemma wt_instrs_ext:

  [| P,T_r,mxs \<turnstile> is₁, xt₁ [::] τs₁ @ τs₂;
     P,T_r,mxs \<turnstile> is₂, xt₂ [::] τs₂; length τs₁ = length is₁ |]
  ==> P,T_r,mxs \<turnstile> is₁ @ is₂, xt₁ @ shift (length is₁) xt₂ [::] τs₁ @ τs₂

corollary wt_instrs_ext2:

  [| P,T_r,mxs \<turnstile> is₂, xt₂ [::] τs₂;
     P,T_r,mxs \<turnstile> is₁, xt₁ [::] τs₁ @ τs₂; length τs₁ = length is₁ |]
  ==> P,T_r,mxs \<turnstile> is₁ @ is₂, xt₁ @ shift (length is₁) xt₂ [::] τs₁ @ τs₂

corollary wt_instrs_ext_prefix:

  [| P,T_r,mxs \<turnstile> is₁, xt₁ [::] τs₁ @ τs₂;
     P,T_r,mxs \<turnstile> is₂, xt₂ [::] τs₃; length τs₁ = length is₁;
     τs₃ <= τs₂ |]
  ==> P,T_r,mxs \<turnstile> is₁ @ is₂, xt₁ @ shift (length is₁) xt₂ [::] τs₁ @ τs₂

corollary

  [| P,T_r,mxs \<turnstile> is₁, xt₁ [::] τs₁ @ [τ];
     P,T_r,mxs \<turnstile> is₂, xt₂ [::] τ # τs₂; length τs₁ = length is₁ |]
  ==> P,T_r,mxs \<turnstile> is₁ @ is₂, xt₁ @ shift (length is₁) xt₂ [::]
      τs₁ @ τ # τs₂

corollary wt_instrs_app_last:

  [| P,T_r,mxs \<turnstile> is₂, xt₂ [::] τ # τs₂;
     P,T_r,mxs \<turnstile> is₁, xt₁ [::] τs₁; last τs₁ = τ;
     length τs₁ = length is₁ + 1 |]
  ==> P,T_r,mxs \<turnstile> is₁ @ is₂, xt₁ @ shift (length is₁) xt₂ [::] τs₁ @ τs₂

corollary wt_instrs_append_last:

  [| P,T_r,mxs \<turnstile> is, xt [::] τs;
     P,T_r,mxs,mpc,[] \<turnstile> i,pc :: τs; pc = length is; mpc = length τs;
     length is + 1 < length τs |]
  ==> P,T_r,mxs \<turnstile> is @ [i], xt [::] τs

corollary wt_instrs_app2:

  [| P,T_r,mxs \<turnstile> is₂, xt₂ [::] τ' # τs₂;
     P,T_r,mxs \<turnstile> is₁, xt₁ [::] τ # τs₁ @ [τ'];
     xt' = xt₁ @ shift (length is₁) xt₂; length τs₁ + 1 = length is₁ |]
  ==> P,T_r,mxs \<turnstile> is₁ @ is₂, xt' [::] τ # τs₁ @ τ' # τs₂

corollary wt_instrs_app2_simp:

  [| P,T_r,mxs \<turnstile> is₂, xt₂ [::] τ' # τs₂;
     P,T_r,mxs \<turnstile> is₁, xt₁ [::] τ # τs₁ @ [τ'];
     length τs₁ + 1 = length is₁ |]
  ==> P,T_r,mxs \<turnstile> is₁ @ is₂, xt₁ @ shift (length is₁) xt₂ [::]
      τ # τs₁ @ τ' # τs₂

corollary wt_instrs_Cons:

  [| τs ~= []; P,T_r,mxs \<turnstile> [i], [] [::] [τ, τ'];
     P,T_r,mxs \<turnstile> is, xt [::] τ' # τs |]
  ==> P,T_r,mxs \<turnstile> i # is, shift 1 xt [::] τ # τ' # τs

corollary

  [| P,T_r,mxs \<turnstile> is, xt [::] τs;
     P,T_r,mxs,mpc,[] \<turnstile> i,0 :: τ # τs; mpc = length τs + 1 |]
  ==> P,T_r,mxs \<turnstile> i # is, shift 1 xt [::] τ # τs

lemma wt_instrs_last_incr:

  [| P,T_r,mxs \<turnstile> is, xt [::] τs @ [τ]; P |- τ <=' τ' |]
  ==> P,T_r,mxs \<turnstile> is, xt [::] τs @ [τ']

lemma

  xcpt_app i P pc mxs [] τ

lemma

  xcpt_eff i P pc τ [] = []

lemma wt_New:

  [| is_class P C; length ST < mxs |]
  ==> P,T_r,mxs \<turnstile> [New C], [] [::]
      [ty_i' mxl ST E A, ty_i' mxl (Class C # ST) E A]

lemma wt_Cast:

  is_class P C
  ==> P,T_r,mxs \<turnstile> [Checkcast C], [] [::]
      [ty_i' mxl (Class D # ST) E A, ty_i' mxl (Class C # ST) E A]

lemma wt_Push:

  [| length ST < mxs; typeof v = ⌊T⌋ |]
  ==> P,T_r,mxs \<turnstile> [Push v], [] [::]
      [ty_i' mxl ST E A, ty_i' mxl (T # ST) E A]

lemma wt_Pop:

  P,T_r,mxs \<turnstile> [Pop], [] [::]
  ty_i' mxl (T # ST) E A # ty_i' mxl ST E A # τs

lemma wt_CmpEq:

  widen P T₁ T₂ | widen P T₂ T₁
  ==> P,T_r,mxs \<turnstile> [CmpEq], [] [::]
      [ty_i' mxl (T₂ # T₁ # ST) E A, ty_i' mxl (Boolean # ST) E A]

lemma wt_IAdd:

  P,T_r,mxs \<turnstile> [IAdd], [] [::]
  [ty_i' mxl (Integer # Integer # ST) E A, ty_i' mxl (Integer # ST) E A]

lemma wt_Load:

  [| length ST < mxs; length E <= mxl; i ∈∈ A; i < length E |]
  ==> P,T_r,mxs \<turnstile> [Load i], [] [::]
      [ty_i' mxl ST E A, ty_i' mxl (E ! i # ST) E A]

lemma wt_Store:

  [| widen P T (E ! i); i < length E; length E <= mxl |]
  ==> P,T_r,mxs \<turnstile> [Store i], [] [::]
      [ty_i' mxl (T # ST) E A, ty_i' mxl ST E (⌊{i}⌋ \<squnion> A)]

lemma wt_Get:

  P \<turnstile> C sees F:T in D
  ==> P,T_r,mxs \<turnstile> [Getfield F D], [] [::]
      [ty_i' mxl (Class C # ST) E A, ty_i' mxl (T # ST) E A]

lemma wt_Put:

  [| P \<turnstile> C sees F:T in D; widen P T' T |]
  ==> P,T_r,mxs \<turnstile> [Putfield F D], [] [::]
      [ty_i' mxl (T' # Class C # ST) E A, ty_i' mxl ST E A]

lemma wt_Throw:

  P,T_r,mxs \<turnstile> [Throw], [] [::] [ty_i' mxl (Class C # ST) E A, τ']

lemma wt_IfFalse:

  [| 2 <= i; nat i < length τs + 2; P |- ty_i' mxl ST E A <=' τs ! nat (i - 2) |]
  ==> P,T_r,mxs \<turnstile> [IfFalse i], [] [::]
      ty_i' mxl (Boolean # ST) E A # ty_i' mxl ST E A # τs

lemma wt_Goto:

  [| 0 <= int pc + i; nat (int pc + i) < length τs; length τs <= mpc;
     P |- τs ! pc <=' τs ! nat (int pc + i) |]
  ==> P,T,mxs,mpc,[] \<turnstile> Goto i,pc :: τs

lemma wt_Invoke:

  [| size es = length Ts'; P \<turnstile> C sees M: Ts->T = m in D;
     widens P Ts' Ts |]
  ==> P,T_r,mxs \<turnstile> [Invoke M (size es)], [] [::]
      [ty_i' mxl (rev Ts' @ Class C # ST) E A, ty_i' mxl (T # ST) E A]

corollary wt_instrs_app3:

  [| P,T_r,mxs \<turnstile> is₂, [] [::] τ' # τs₂;
     P,T_r,mxs \<turnstile> is₁, xt₁ [::] τ # τs₁ @ [τ'];
     length τs₁ + 1 = length is₁ |]
  ==> P,T_r,mxs \<turnstile> is₁ @ is₂, xt₁ [::] τ # τs₁ @ τ' # τs₂

corollary wt_instrs_Cons3:

  [| τs ~= []; P,T_r,mxs \<turnstile> [i], [] [::] [τ, τ'];
     P,T_r,mxs \<turnstile> is, [] [::] τ' # τs |]
  ==> P,T_r,mxs \<turnstile> i # is, [] [::] τ # τ' # τs

lemma wt_instrs_xapp:

  [| P,T_r,mxs \<turnstile> is₁ @ is₂, xt [::]
     τs₁ @ ty_i' mxl (Class C # ST) E A # τs₂;
     ALL τ:set τs₁.
        ALL ST' LT'.
           τ = ⌊(ST', LT')⌋ -->
           length ST <= length ST' &
           P |- ⌊(drop (length ST' - length ST) ST', LT')⌋ <=' ty_i' mxl ST E A;
     length is₁ = length τs₁; is_class P C; length ST < mxs |]
  ==> P,T_r,mxs \<turnstile>
      is₁ @ is₂, xt @ [(0, length is₁ - 1, C, length is₁, length ST)] [::]
      τs₁ @ ty_i' mxl (Class C # ST) E A # τs₂

lemma drop_Cons_Suc:

  drop n xs = y # ys ==> drop (Suc n) xs = ys

lemma drop_mess:

  [| Suc (length xs₀) <= length xs;
     drop (length xs - Suc (length xs₀)) xs = x # xs₀ |]
  ==> drop (length xs - length xs₀) xs = xs₀

lemma compT_ST_prefix:

  ⌊(ST, LT)⌋ : set (compT P mxl E A ST₀ e)
  ==> length ST₀ <= length ST & drop (length ST - length ST₀) ST = ST₀

and

  ⌊(ST, LT)⌋ : set (compTs P mxl E A ST₀ es)
  ==> length ST₀ <= length ST & drop (length ST - length ST₀) ST = ST₀

lemma fun_of_simp:

  fun_of S x y = ((x, y) : S)

theorem compT_wt_instrs:

  [| WT₁ P E e T; \<D> e A; \<B> e (length E); length ST + max_stack e <= mxs;
     length E + max_vars e <= mxl |]
  ==> P,T_r,mxs \<turnstile> compE₂ e, compxE₂ e 0 (length ST) [::]
      ty_i' mxl ST E A # compT P mxl E A ST e @ [after P mxl E A ST e]

and

  [| WTs₁ P E es Ts; \<D>s es A; \<B>s es (length E);
     length ST + max_stacks es <= mxs; length E + max_varss es <= mxl |]
  ==> let τs = ty_i' mxl ST E A # compTs P mxl E A ST es
      in P,T_r,mxs \<turnstile> compEs₂ es, compxEs₂ es 0 (length ST) [::] τs &
         last τs = ty_i' mxl (rev Ts @ ST) E (A \<squnion> \<A>s es)

lemma

  types (compP f P) = types P

lemma

  states (compP f P) mxs mxl = states P mxs mxl

lemma

  app_i (i, compP f P, pc, mpc, T, τ) = app_i (i, P, pc, mpc, T, τ)

lemma

  is_relevant_entry (compP f P) i = is_relevant_entry P i

lemma

  relevant_entries (compP f P) i pc xt = relevant_entries P i pc xt

lemma

  app i (compP f P) mpc T pc mxl xt τ = app i P mpc T pc mxl xt τ

lemma

  app i P mpc T pc mxl xt τ ==> eff i (compP f P) pc xt τ = eff i P pc xt τ

lemma

  subtype (compP f P) = subtype P

lemma

  compP f P |- τ <=' τ' = P |- τ <=' τ'

lemma

  compP f P,T,mpc,mxl,xt \<turnstile> i,pc :: τs =
  P,T,mpc,mxl,xt \<turnstile> i,pc :: τs

lemma

  [| wf_prog p P; WT₁ P (Class C # Ts) e T; \<D> e ⌊{..length Ts}⌋;
     \<B> e (length (Class C # Ts)); set (Class C # Ts) <= types P;
     widen P T T' |]
  ==> wt_method (compP₂ P) C Ts T' (max_stack e) (max_vars e)
       (compE₂ e @ [Return]) (compxE₂ e 0 0)
       (ty_i' (1 + length Ts + max_vars e) [] (Class C # Ts) ⌊{..length Ts}⌋ #
        compT_a P (1 + length Ts + max_vars e) (Class C # Ts) ⌊{..length Ts}⌋ [] e)

theorem wt_compP₂:

  wf_J₁_prog P ==> wf_jvm_prog (compP₂ P)

theorem wt_J2JVM:

  wf_J_prog P ==> wf_jvm_prog (J2JVM P)