Theory TypeComp
section ‹Preservation of Well-Typedness in Stage 2›
theory TypeComp
imports
Exception_Tables
J1WellForm
"../BV/BVSpec"
"HOL-Library.Prefix_Order"
"HOL-Library.Sublist"
begin
declare nth_append[simp]
locale TC0 =
fixes P :: "'addr J1_prog" and mxl :: nat
begin
definition ty :: "ty list ⇒ 'addr expr1 ⇒ ty"
where "ty E e ≡ THE T. P,E ⊢1 e :: T"
definition ty⇩l :: "ty list ⇒ nat set ⇒ ty⇩l"
where "ty⇩l E A' ≡ map (λi. if i ∈ A' ∧ i < size E then OK(E!i) else Err) [0..<mxl]"
definition ty⇩i' :: "ty list ⇒ ty list ⇒ nat set option ⇒ ty⇩i'"
where "ty⇩i' ST E A ≡ case A of None ⇒ None | ⌊A'⌋ ⇒ Some(ST, ty⇩l E A')"
definition after :: "ty list ⇒ nat set option ⇒ ty list ⇒ 'addr expr1 ⇒ ty⇩i'"
where "after E A ST e ≡ ty⇩i' (ty E e # ST) E (A ⊔ 𝒜 e)"
end
locale TC1 = TC0 +
fixes wfmd
assumes wf_prog: "wf_prog wfmd P"
begin
lemma ty_def2 [simp]: "P,E ⊢1 e :: T ⟹ ty E e = T"
apply(unfold ty_def ty_def)
apply(blast intro: the_equality WT1_unique[OF wf_prog])
done
end
context TC0 begin
lemma ty⇩i'_None [simp]: "ty⇩i' ST E None = None"
by(simp add:ty⇩i'_def)
lemma ty⇩l_app_diff[simp]:
"ty⇩l (E@[T]) (A - {size E}) = ty⇩l E A"
by(auto simp add:ty⇩l_def hyperset_defs)
lemma ty⇩i'_app_diff[simp]:
"ty⇩i' ST (E @ [T]) (A ⊖ size E) = ty⇩i' ST E A"
by(auto simp add:ty⇩i'_def hyperset_defs)
lemma ty⇩l_antimono:
"A ⊆ A' ⟹ P ⊢ ty⇩l E A' [≤⇩⊤] ty⇩l E A"
by(auto simp:ty⇩l_def list_all2_conv_all_nth)
lemma ty⇩i'_antimono:
"A ⊆ A' ⟹ P ⊢ ty⇩i' ST E ⌊A'⌋ ≤' ty⇩i' ST E ⌊A⌋"
by(auto simp:ty⇩i'_def ty⇩l_def list_all2_conv_all_nth)
lemma ty⇩l_env_antimono:
"P ⊢ ty⇩l (E@[T]) A [≤⇩⊤] ty⇩l E A"
by(auto simp:ty⇩l_def list_all2_conv_all_nth)
lemma ty⇩i'_env_antimono:
"P ⊢ ty⇩i' ST (E@[T]) A ≤' ty⇩i' ST E A"
by(auto simp:ty⇩i'_def ty⇩l_def list_all2_conv_all_nth)
lemma ty⇩i'_incr:
"P ⊢ ty⇩i' ST (E @ [T]) ⌊insert (size E) A⌋ ≤' ty⇩i' ST E ⌊A⌋"
by(auto simp:ty⇩i'_def ty⇩l_def list_all2_conv_all_nth)
lemma ty⇩l_incr:
"P ⊢ ty⇩l (E @ [T]) (insert (size E) A) [≤⇩⊤] ty⇩l E A"
by(auto simp: hyperset_defs ty⇩l_def list_all2_conv_all_nth)
lemma ty⇩l_in_types:
"set E ⊆ types P ⟹ ty⇩l E A ∈ list mxl (err (types P))"
by(auto simp add:ty⇩l_def intro!:listI dest!: nth_mem)
function compT :: "ty list ⇒ nat hyperset ⇒ ty list ⇒ 'addr expr1 ⇒ ty⇩i' list"
and compTs :: "ty list ⇒ nat hyperset ⇒ ty list ⇒ 'addr expr1 list ⇒ ty⇩i' list"
where
"compT E A ST (new C) = []"
| "compT E A ST (newA T⌊e⌉) = compT E A ST e @ [after E A ST e]"
| "compT E A ST (Cast C e) = compT E A ST e @ [after E A ST e]"
| "compT E A ST (e instanceof T) = compT E A ST e @ [after E A ST e]"
| "compT E A ST (Val v) = []"
| "compT E A ST (e1 «bop» e2) =
(let ST1 = ty E e1#ST; A1 = A ⊔ 𝒜 e1 in
compT E A ST e1 @ [after E A ST e1] @
compT E A1 ST1 e2 @ [after E A1 ST1 e2])"
| "compT E A ST (Var i) = []"
| "compT E A ST (i := e) = compT E A ST e @ [after E A ST e, ty⇩i' ST E (A ⊔ 𝒜 e ⊔ ⌊{i}⌋)]"
| "compT E A ST (a⌊i⌉) =
(let ST1 = ty E a # ST; A1 = A ⊔ 𝒜 a
in compT E A ST a @ [after E A ST a] @ compT E A1 ST1 i @ [after E A1 ST1 i])"
| "compT E A ST (a⌊i⌉ := e) =
(let ST1 = ty E a # ST; A1 = A ⊔ 𝒜 a;
ST2 = ty E i # ST1; A2 = A1 ⊔ 𝒜 i; A3 = A2 ⊔ 𝒜 e
in compT E A ST a @ [after E A ST a] @ compT E A1 ST1 i @ [after E A1 ST1 i] @ compT E A2 ST2 e @ [after E A2 ST2 e, ty⇩i' ST E A3])"
| "compT E A ST (a∙length) = compT E A ST a @ [after E A ST a]"
| "compT E A ST (e∙F{D}) = compT E A ST e @ [after E A ST e]"
| "compT E A ST (e1∙F{D} := e2) =
(let ST1 = ty E e1#ST; A1 = A ⊔ 𝒜 e1; A2 = A1 ⊔ 𝒜 e2
in compT E A ST e1 @ [after E A ST e1] @ compT E A1 ST1 e2 @ [after E A1 ST1 e2] @ [ty⇩i' ST E A2])"
| "compT E A ST (e1∙compareAndSwap(D∙F, e2, e3)) =
(let ST1 = ty E e1 # ST; A1 = A ⊔ 𝒜 e1; ST2 = ty E e2 # ST1; A2 = A1 ⊔ 𝒜 e2; A3 = A2 ⊔ 𝒜 e3
in compT E A ST e1 @ [after E A ST e1] @ compT E A1 ST1 e2 @ [after E A1 ST1 e2] @ compT E A2 ST2 e3 @ [after E A2 ST2 e3])"
| "compT E A ST (e∙M(es)) =
compT E A ST e @ [after E A ST e] @
compTs E (A ⊔ 𝒜 e) (ty E e # ST) es"
| "compT E A ST {i:T=None; e} = compT (E@[T]) (A⊖i) ST e"
| "compT E A ST {i:T=⌊v⌋; e} =
[after E A ST (Val v), ty⇩i' ST (E@[T]) (A ⊔ ⌊{i}⌋)] @ compT (E@[T]) (A ⊔ ⌊{i}⌋) ST e"
| "compT E A ST (sync⇘i⇙ (e1) e2) =
(let A1 = A ⊔ 𝒜 e1 ⊔ ⌊{i}⌋; E1 = E @ [Class Object]; ST2 = ty E1 e2 # ST; A2 = A1 ⊔ 𝒜 e2
in compT E A ST e1 @
[after E A ST e1,
ty⇩i' (Class Object # Class Object # ST) E (A ⊔ 𝒜 e1),
ty⇩i' (Class Object # ST) E1 A1,
ty⇩i' ST E1 A1] @
compT E1 A1 ST e2 @
[ty⇩i' ST2 E1 A2, ty⇩i' (Class Object # ST2) E1 A2, ty⇩i' ST2 E1 A2,
ty⇩i' (Class Throwable # ST) E1 A1,
ty⇩i' (Class Object # Class Throwable # ST) E1 A1,
ty⇩i' (Class Throwable # ST) E1 A1])"
| "compT E A ST (insync⇘i⇙ (a) e) = []"
| "compT E A ST (e1;;e2) =
(let A1 = A ⊔ 𝒜 e1 in
compT E A ST e1 @ [after E A ST e1, ty⇩i' ST E A1] @
compT E A1 ST e2)"
| "compT E A ST (if (e) e1 else e2) =
(let A0 = A ⊔ 𝒜 e; τ = ty⇩i' ST E A0 in
compT E A ST e @ [after E A ST e, τ] @
compT E A0 ST e1 @ [after E A0 ST e1, τ] @
compT E A0 ST e2)"
| "compT E A ST (while (e) c) =
(let A0 = A ⊔ 𝒜 e; A1 = A0 ⊔ 𝒜 c; τ = ty⇩i' ST E A0 in
compT E A ST e @ [after E A ST e, τ] @
compT E A0 ST c @ [after E A0 ST c, ty⇩i' ST E A1, ty⇩i' ST E A0])"
| "compT E A ST (throw e) = compT E A ST e @ [after E A ST e]"
| "compT E A ST (try e1 catch(C i) e2) =
compT E A ST e1 @ [after E A ST e1] @
[ty⇩i' (Class C#ST) E A, ty⇩i' ST (E@[Class C]) (A ⊔ ⌊{i}⌋)] @
compT (E@[Class C]) (A ⊔ ⌊{i}⌋) ST e2"
| "compTs E A ST [] = []"
| "compTs E A ST (e#es) = compT E A ST e @ [after E A ST e] @
compTs E (A ⊔ (𝒜 e)) (ty E e # ST) es"
by pat_completeness simp_all
termination
apply(relation "case_sum (λp. size (snd (snd (snd p)))) (λp. size_list size (snd (snd (snd p)))) <*mlex*> {}")
apply(rule wf_mlex[OF wf_empty])
apply(rule mlex_less, simp)+
done
lemmas compT_compTs_induct =
compT_compTs.induct[
unfolded meta_all5_eq_conv meta_all4_eq_conv meta_all3_eq_conv meta_all2_eq_conv meta_all_eq_conv,
case_names
new NewArray Cast InstanceOf Val BinOp Var LAss AAcc AAss ALen FAcc FAss CompareAndSwap Call BlockNone BlockSome
Synchronized InSynchronized Seq Cond While throw TryCatch
Nil Cons]
definition compTa :: "ty list ⇒ nat hyperset ⇒ ty list ⇒ 'addr expr1 ⇒ ty⇩i' list"
where "compTa E A ST e ≡ compT E A ST e @ [after E A ST e]"
lemmas compE2_not_Nil = compE2_neq_Nil
declare compE2_not_Nil[simp]
lemma compT_sizes[simp]:
shows "size(compT E A ST e) = size(compE2 e) - 1"
and "size(compTs E A ST es) = size(compEs2 es)"
apply(induct E A ST e and E A ST es rule: compT_compTs_induct)
apply(auto split:nat_diff_split)
done
lemma compT_None_not_Some [simp]: "⌊τ⌋ ∉ set (compT E None ST e)"
and compTs_None_not_Some [simp]: "⌊τ⌋ ∉ set (compTs E None ST es)"
by(induct E A≡"None :: nat hyperset" ST e and E A≡"None :: nat hyperset" ST es rule: compT_compTs_induct) (simp_all add:after_def)
lemma pair_eq_ty⇩i'_conv:
"(⌊(ST, LT)⌋ = ty⇩i' ST⇩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 pair_conv_ty⇩i': "⌊(ST, ty⇩l E A)⌋ = ty⇩i' ST E ⌊A⌋"
by(simp add:ty⇩i'_def)
lemma ty⇩i'_antimono2:
"⟦ E ≤ E'; A ⊆ A' ⟧ ⟹ P ⊢ ty⇩i' ST E' ⌊A'⌋ ≤' ty⇩i' ST E ⌊A⌋"
by(auto simp:ty⇩i'_def ty⇩l_def list_all2_conv_all_nth less_eq_list_def prefix_def)
declare ty⇩i'_antimono [intro!] after_def[simp] pair_conv_ty⇩i'[simp] pair_eq_ty⇩i'_conv[simp]
lemma compT_LT_prefix:
"⟦ ⌊(ST,LT)⌋ ∈ set(compT E A ST0 e); ℬ e (size E) ⟧ ⟹ P ⊢ ⌊(ST,LT)⌋ ≤' ty⇩i' ST E A"
and compTs_LT_prefix:
"⟦ ⌊(ST,LT)⌋ ∈ set(compTs E A ST0 es); ℬs es (size E) ⟧ ⟹ P ⊢ ⌊(ST,LT)⌋ ≤' ty⇩i' ST E A"
proof(induct E A ST0 e and E A ST0 es rule: compT_compTs_induct)
case FAss thus ?case by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
next
case BinOp thus ?case
by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans split:bop.splits)
next
case Seq thus ?case by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
next
case While thus ?case by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
next
case Cond thus ?case by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
next
case BlockNone thus ?case by(auto)
next
case BlockSome thus ?case
by(clarsimp simp only: ty⇩i'_def)(fastforce intro: ty⇩i'_incr simp add: hyperset_defs elim: sup_state_opt_trans)
next
case Call thus ?case by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
next
case Cons thus ?case
by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
next
case TryCatch thus ?case
by(fastforce simp:hyperset_defs intro!: ty⇩i'_incr elim!:sup_state_opt_trans)
next
case NewArray thus ?case by(auto simp add: hyperset_defs)
next
case AAcc thus ?case by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
next
case AAss thus ?case by(auto simp:hyperset_defs Un_ac elim!:sup_state_opt_trans)
next
case ALen thus ?case by(auto simp add: hyperset_defs)
next
case CompareAndSwap thus ?case by(auto simp: hyperset_defs Un_ac elim!:sup_state_opt_trans)
next
case Synchronized thus ?case
by(fastforce simp add: hyperset_defs elim: sup_state_opt_trans intro: sup_state_opt_trans[OF ty⇩i'_incr] ty⇩i'_antimono2)
qed (auto simp:hyperset_defs)
declare ty⇩i'_antimono [rule del] after_def[simp del] pair_conv_ty⇩i'[simp del] pair_eq_ty⇩i'_conv[simp del]
lemma OK_None_states [iff]: "OK None ∈ states P mxs mxl"
by(simp add: JVM_states_unfold)
end
context TC1 begin
lemma after_in_states:
"⟦ P,E ⊢1 e :: T; set E ⊆ types P; set ST ⊆ types P; size ST + max_stack e ≤ mxs ⟧
⟹ OK (after E A ST e) ∈ states P mxs mxl"
apply(subgoal_tac "size ST + 1 ≤ mxs")
apply(simp add:after_def ty⇩i'_def JVM_states_unfold ty⇩l_in_types)
apply(clarify intro!: exI)
apply(rule conjI)
apply(rule exI[where x="length ST + 1"], fastforce)
apply(clarsimp)
apply(rule conjI[OF WT1_is_type[OF wf_prog]], auto intro: listI)
using max_stack1[of e] by simp
end
context TC0 begin
lemma OK_ty⇩i'_in_statesI [simp]:
"⟦ set E ⊆ types P; set ST ⊆ types P; size ST ≤ mxs ⟧
⟹ OK (ty⇩i' ST E A) ∈ states P mxs mxl"
apply(simp add:ty⇩i'_def JVM_states_unfold ty⇩l_in_types)
apply(blast intro!:listI)
done
end
lemma is_class_type_aux: "is_class P C ⟹ is_type P (Class C)"
by(simp)
context TC1 begin
declare is_type.simps[simp del] subsetI[rule del]
theorem
shows compT_states:
"⟦ P,E ⊢1 e :: T; set E ⊆ types P; set ST ⊆ types P;
size ST + max_stack e ≤ mxs; size E + max_vars e ≤ mxl ⟧
⟹ OK ` set(compT E A ST e) ⊆ states P mxs mxl"
(is "PROP ?P e E T A ST")
and compTs_states:
"⟦ P,E ⊢1 es[::]Ts; set E ⊆ types P; set ST ⊆ types P;
size ST + max_stacks es ≤ mxs; size E + max_varss es ≤ mxl ⟧
⟹ OK ` set(compTs E A ST es) ⊆ states P mxs mxl"
(is "PROP ?Ps es E Ts A ST")
proof(induct E A ST e and E A ST es arbitrary: T and Ts rule: compT_compTs_induct)
case new thus ?case by(simp)
next
case (Cast C e) thus ?case by (auto simp:after_in_states)
next
case InstanceOf thus ?case by (auto simp:after_in_states)
next
case Val thus ?case by(simp)
next
case Var thus ?case by(simp)
next
case LAss thus ?case by(auto simp:after_in_states)
next
case FAcc thus ?case by(auto simp:after_in_states)
next
case FAss thus ?case
by(auto simp:image_Un WT1_is_type[OF wf_prog] after_in_states)
next
case CompareAndSwap thus ?case by(auto simp:image_Un WT1_is_type[OF wf_prog] after_in_states)
next
case Seq thus ?case
by(auto simp:image_Un after_in_states)
next
case BinOp thus ?case
by(auto simp:image_Un WT1_is_type[OF wf_prog] after_in_states)
next
case Cond thus ?case
by(force simp:image_Un WT1_is_type[OF wf_prog] after_in_states)
next
case While thus ?case
by(auto simp:image_Un WT1_is_type[OF wf_prog] after_in_states)
next
case BlockNone thus ?case by auto
next
case (BlockSome E A ST i ty v exp)
with max_stack1[of exp] show ?case by(auto intro: after_in_states)
next
case (TryCatch E A ST e⇩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 WT1_is_type[OF wf_prog] after_in_states
is_class_type_aux)
next
case Nil thus ?case by simp
next
case Cons thus ?case
by(auto simp:image_Un WT1_is_type[OF wf_prog] after_in_states)
next
case throw thus ?case
by(auto simp: WT1_is_type[OF wf_prog] after_in_states)
next
case Call thus ?case
by(auto simp:image_Un WT1_is_type[OF wf_prog] after_in_states)
next
case NewArray thus ?case
by(auto simp:image_Un WT1_is_type[OF wf_prog] after_in_states)
next
case AAcc thus ?case by(auto simp:image_Un WT1_is_type[OF wf_prog] after_in_states)
next
case AAss thus ?case by(auto simp:image_Un WT1_is_type[OF wf_prog] after_in_states)
next
case ALen thus ?case by(auto simp:image_Un WT1_is_type[OF wf_prog] after_in_states)
next
case InSynchronized thus ?case by auto
next
case (Synchronized E A ST i exp1 exp2)
from ‹P,E ⊢1 sync⇘i⇙ (exp1) exp2 :: T› obtain T1
where wt1: "P,E ⊢1 exp1 :: T1" and T1: "is_refT T1" "T1 ≠ NT"
and wt2: "P,E@[Class Object] ⊢1 exp2 :: T" by auto
moreover note E = ‹set E ⊆ types P› with wf_prog
have E': "set (E@[Class Object]) ⊆ types P" by(auto simp add: is_type.simps)
moreover from wf_prog wt2 E' have T: "is_type P T" by(rule WT1_is_type)
note ST = ‹set ST ⊆ types P› with wf_prog
have ST': "set (Class Object # ST) ⊆ types P" by(auto simp add: is_type.simps)
moreover from wf_prog have throwable: "is_type P (Class Throwable)"
unfolding is_type.simps by(rule is_class_Throwable)
ultimately show ?case using Synchronized max_stack1[of exp2] T
by(auto simp add: image_Un after_in_states)
qed
declare is_type.simps[simp] subsetI[intro!]
end
locale TC2 = TC0 +
fixes T⇩r :: ty and mxs :: pc
begin
definition
wt_instrs :: "'addr instr list ⇒ ex_table ⇒ ty⇩i' list ⇒ bool" ("(⊢ _, _ /[::]/ _)" [0,0,51] 50)
where
"⊢ is,xt [::] τs ≡ size is < size τs ∧ pcs xt ⊆ {0..<size is} ∧ (∀pc< size is. P,T⇩r,mxs,size τs,xt ⊢ is!pc,pc :: τs)"
lemmas wt_defs = wt_instrs_def wt_instr_def app_def eff_def norm_eff_def
lemma wt_instrs_Nil [simp]: "τs ≠ [] ⟹ ⊢ [],[] [::] τs"
by(simp add:wt_defs)
end
locale TC3 = TC1 + TC2
lemma eff_None [simp]: "eff i P pc et None = []"
by (simp add: Effect.eff_def)
declare split_comp_eq[simp del]
lemma wt_instr_appR:
"⟦ P,T,m,mpc,xt ⊢ is!pc,pc :: τs;
pc < size is; size is < size τs; mpc ≤ size τs; mpc ≤ mpc' ⟧
⟹ P,T,m,mpc',xt ⊢ is!pc,pc :: τs@τs'"
by (fastforce simp:wt_instr_def app_def)
lemma relevant_entries_shift [simp]:
"relevant_entries P i (pc+n) (shift n xt) = shift n (relevant_entries P i pc xt)"
apply (induct xt)
apply (unfold relevant_entries_def shift_def)
apply simp
apply (auto simp add: is_relevant_entry_def)
done
lemma xcpt_eff_shift [simp]:
"xcpt_eff i P (pc+n) τ (shift n xt) =
map (λ(pc,τ). (pc + n, τ)) (xcpt_eff i P pc τ xt)"
apply(simp add: xcpt_eff_def)
apply(cases τ)
apply(auto simp add: shift_def)
done
lemma eff_shift [simp]:
"app⇩i (i, P, pc, m, T, τ) ⟹
eff i P (pc+n) (shift n xt) (Some τ) =
map (λ(pc,τ). (pc+n,τ)) (eff i P pc xt (Some τ))"
apply(simp add:eff_def norm_eff_def)
apply(cases "i",auto)
done
lemma xcpt_app_shift [simp]:
"xcpt_app i P (pc+n) m (shift n xt) τ = xcpt_app i P pc m xt τ"
by (simp add: xcpt_app_def) (auto simp add: shift_def)
lemma wt_instr_appL:
"⟦ P,T,m,mpc,xt ⊢ i,pc :: τs; pc < size τs; mpc ≤ size τs ⟧
⟹ P,T,m,mpc + size τs',shift (size τs') xt ⊢ i,pc+size τs' :: τs'@τs"
apply(clarsimp simp add: wt_instr_def app_def)
apply(auto)
apply(cases "i", auto)
done
lemma wt_instr_Cons:
"⟦ P,T,m,mpc - 1,[] ⊢ i,pc - 1 :: τs;
0 < pc; 0 < mpc; pc < size τs + 1; mpc ≤ size τs + 1 ⟧
⟹ P,T,m,mpc,[] ⊢ i,pc :: τ#τs"
apply(drule wt_instr_appL[where τs' = "[τ]"])
apply arith
apply arith
apply (simp split:nat_diff_split_asm)
done
lemma wt_instr_append:
"⟦ P,T,m,mpc - size τs',[] ⊢ i,pc - size τs' :: τs;
size τs' ≤ pc; size τs' ≤ mpc; pc < size τs + size τs'; mpc ≤ size τs + size τs' ⟧
⟹ P,T,m,mpc,[] ⊢ i,pc :: τs'@τs"
apply(drule wt_instr_appL[where τs' = τs'])
apply arith
apply arith
apply (simp split:nat_diff_split_asm)
done
lemma xcpt_app_pcs:
"pc ∉ pcs xt ⟹ xcpt_app i P pc mxs xt τ"
by (auto simp add: xcpt_app_def relevant_entries_def is_relevant_entry_def pcs_def)
lemma xcpt_eff_pcs:
"pc ∉ pcs xt ⟹ xcpt_eff i P pc τ xt = []"
by (cases τ)
(auto simp add: is_relevant_entry_def xcpt_eff_def relevant_entries_def pcs_def
intro!: filter_False)
lemma pcs_shift:
"pc < n ⟹ pc ∉ pcs (shift n xt)"
by (auto simp add: shift_def pcs_def)
lemma xcpt_eff_shift_pc_ge_n: assumes "x ∈ set (xcpt_eff i P pc τ (shift n xt))"
shows "n ≤ pc"
proof -
{ assume "pc < n"
hence "pc ∉ pcs (shift n xt)" by(rule pcs_shift)
with assms have False
by(auto simp add: pcs_def xcpt_eff_def is_relevant_entry_def relevant_entries_def split_beta cong: filter_cong) }
thus ?thesis by(cases "n ≤ pc")(auto)
qed
lemma wt_instr_appRx:
"⟦ P,T,m,mpc,xt ⊢ is!pc,pc :: τs; pc < size is; size is < size τs; mpc ≤ size τs ⟧
⟹ P,T,m,mpc,xt @ shift (size is) xt' ⊢ is!pc,pc :: τs"
apply(clarsimp simp:wt_instr_def eff_def app_def)
apply(fastforce dest: xcpt_eff_shift_pc_ge_n intro!: xcpt_app_pcs[OF pcs_shift])
done
lemma wt_instr_appLx:
"⟦ P,T,m,mpc,xt ⊢ i,pc :: τs; pc ∉ pcs xt' ⟧
⟹ P,T,m,mpc,xt'@xt ⊢ i,pc :: τs"
by (auto simp:wt_instr_def app_def eff_def xcpt_app_pcs xcpt_eff_pcs)
context TC2 begin
lemma wt_instrs_extR:
"⊢ is,xt [::] τs ⟹ ⊢ is,xt [::] τs @ τs'"
by(auto simp add:wt_instrs_def wt_instr_appR)
lemma wt_instrs_ext:
"⟦ ⊢ is⇩1,xt⇩1 [::] τs⇩1@τs⇩2; ⊢ is⇩2,xt⇩2 [::] τs⇩2; size τs⇩1 = size is⇩1 ⟧
⟹ ⊢ 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 simp add: pcs_shift_conv)
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" for 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 wt_instrs_ext2:
"⟦ ⊢ is⇩2,xt⇩2 [::] τs⇩2; ⊢ is⇩1,xt⇩1 [::] τs⇩1@τs⇩2; size τs⇩1 = size is⇩1 ⟧
⟹ ⊢ is⇩1@is⇩2, xt⇩1 @ shift (size is⇩1) xt⇩2 [::] τs⇩1@τs⇩2"
by(rule wt_instrs_ext)
corollary wt_instrs_ext_prefix [trans]:
"⟦ ⊢ is⇩1,xt⇩1 [::] τs⇩1@τs⇩2; ⊢ is⇩2,xt⇩2 [::] τs⇩3;
size τs⇩1 = size is⇩1; τs⇩3 ≤ τs⇩2 ⟧
⟹ ⊢ is⇩1@is⇩2, xt⇩1 @ shift (size is⇩1) xt⇩2 [::] τs⇩1@τs⇩2"
by(bestsimp simp:less_eq_list_def prefix_def elim: wt_instrs_ext dest:wt_instrs_extR)
corollary wt_instrs_app:
assumes is⇩1: "⊢ is⇩1,xt⇩1 [::] τs⇩1@[τ]"
assumes is⇩2: "⊢ is⇩2,xt⇩2 [::] τ#τs⇩2"
assumes s: "size τs⇩1 = size is⇩1"
shows "⊢ is⇩1@is⇩2, xt⇩1@shift (size is⇩1) xt⇩2 [::] τs⇩1@τ#τs⇩2"
proof -
from is⇩1 have "⊢ is⇩1,xt⇩1 [::] (τs⇩1@[τ])@τs⇩2"
by (rule wt_instrs_extR)
hence "⊢ is⇩1,xt⇩1 [::] τs⇩1@τ#τs⇩2" by simp
from this is⇩2 s show ?thesis by (rule wt_instrs_ext)
qed
corollary wt_instrs_app_last[trans]:
"⟦ ⊢ is⇩2,xt⇩2 [::] τ#τs⇩2; ⊢ is⇩1,xt⇩1 [::] τs⇩1;
last τs⇩1 = τ; size τs⇩1 = size is⇩1+1 ⟧
⟹ ⊢ 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 wt_instrs_append_last[trans]:
"⟦ ⊢ is,xt [::] τs; P,T⇩r,mxs,mpc,[] ⊢ i,pc :: τs;
pc = size is; mpc = size τs; size is + 1 < size τs ⟧
⟹ ⊢ is@[i],xt [::] τs"
apply(clarsimp simp add:wt_instrs_def)
apply(rule conjI, fastforce)
apply(fastforce intro!:wt_instr_appLx[where xt = "[]",simplified]
dest!:less_antisym)
done
corollary wt_instrs_app2:
"⟦ ⊢ (is⇩2 :: 'b instr list),xt⇩2 [::] τ'#τs⇩2; ⊢ is⇩1,xt⇩1 [::] τ#τs⇩1@[τ'];
xt' = xt⇩1 @ shift (size is⇩1) xt⇩2; size τs⇩1+1 = size is⇩1 ⟧
⟹ ⊢ is⇩1@is⇩2,xt' [::] τ#τs⇩1@τ'#τs⇩2"
using wt_instrs_app[where ?τs⇩1.0 = "τ # τs⇩1" and ?'b = "'b"] by simp
corollary wt_instrs_app2_simp[trans,simp]:
"⟦ ⊢ (is⇩2 :: 'b instr list),xt⇩2 [::] τ'#τs⇩2; ⊢ is⇩1,xt⇩1 [::] τ#τs⇩1@[τ']; size τs⇩1+1 = size is⇩1 ⟧
⟹ ⊢ 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" and ?'b = "'b"] by simp
corollary wt_instrs_Cons[simp]:
"⟦ τs ≠ []; ⊢ [i],[] [::] [τ,τ']; ⊢ is,xt [::] τ'#τs ⟧
⟹ ⊢ i#is,shift 1 xt [::] τ#τ'#τs"
using wt_instrs_app2[where ?is⇩1.0 = "[i]" and ?τs⇩1.0 = "[]" and ?is⇩2.0 = "is"
and ?xt⇩1.0 = "[]"]
by simp
corollary wt_instrs_Cons2[trans]:
assumes τs: "⊢ is,xt [::] τs"
assumes i: "P,T⇩r,mxs,mpc,[] ⊢ i,0 :: τ#τs"
assumes mpc: "mpc = size τs + 1"
shows "⊢ i#is,shift 1 xt [::] τ#τs"
proof -
from τs have "τs ≠ []" by (auto simp: wt_instrs_def)
with mpc i have "⊢ [i],[] [::] [τ]@τs" by (simp add: wt_instrs_def)
with τs show ?thesis by (fastforce dest: wt_instrs_ext)
qed
lemma wt_instrs_last_incr[trans]:
"⟦ ⊢ is,xt [::] τs@[τ]; P ⊢ τ ≤' τ' ⟧ ⟹ ⊢ is,xt [::] τs@[τ']"
apply(clarsimp simp add:wt_instrs_def wt_instr_def)
apply(rule conjI)
apply(fastforce)
apply(clarsimp)
apply(rename_tac pc' tau')
apply(erule allE, erule (1) impE)
apply(clarsimp)
apply(drule (1) bspec)
apply(clarsimp)
apply(subgoal_tac "pc' = size τs")
prefer 2
apply(clarsimp simp:app_def)
apply(drule (1) bspec)
apply(clarsimp)
apply(auto elim!:sup_state_opt_trans)
done
end
lemma [iff]: "xcpt_app i P pc mxs [] τ"
by (simp add: xcpt_app_def relevant_entries_def)
lemma [simp]: "xcpt_eff i P pc τ [] = []"
by (simp add: xcpt_eff_def relevant_entries_def)
context TC2 begin
lemma wt_New:
"⟦ is_class P C; size ST < mxs ⟧ ⟹
⊢ [New C],[] [::] [ty⇩i' ST E A, ty⇩i' (Class C#ST) E A]"
by(simp add:wt_defs ty⇩i'_def)
lemma wt_Cast:
"is_type P T ⟹
⊢ [Checkcast T],[] [::] [ty⇩i' (U # ST) E A, ty⇩i' (T # ST) E A]"
by(simp add: ty⇩i'_def wt_defs)
lemma wt_Instanceof:
"⟦ is_type P T; is_refT U ⟧ ⟹
⊢ [Instanceof T],[] [::] [ty⇩i' (U # ST) E A, ty⇩i' (Boolean # ST) E A]"
by(simp add: ty⇩i'_def wt_defs)
lemma wt_Push:
"⟦ size ST < mxs; typeof v = Some T ⟧
⟹ ⊢ [Push v],[] [::] [ty⇩i' ST E A, ty⇩i' (T#ST) E A]"
by(simp add: ty⇩i'_def wt_defs)
lemma wt_Pop:
"⊢ [Pop],[] [::] (ty⇩i' (T#ST) E A # ty⇩i' ST E A # τs)"
by(simp add: ty⇩i'_def wt_defs)
lemma wt_BinOpInstr:
"P ⊢ T1«bop»T2 :: T ⟹ ⊢ [BinOpInstr bop],[] [::] [ty⇩i' (T2 # T1 # ST) E A, ty⇩i' (T # ST) E A]"
by(auto simp:ty⇩i'_def wt_defs dest: WT_binop_WTrt_binop intro: list_all2_refl)
lemma wt_Load:
"⟦ size ST < mxs; size E ≤ mxl; i ∈∈ A; i < size E ⟧
⟹ ⊢ [Load i],[] [::] [ty⇩i' ST E A, ty⇩i' (E!i # ST) E A]"
by(auto simp add:ty⇩i'_def wt_defs ty⇩l_def hyperset_defs intro: widens_refl)
lemma wt_Store:
"⟦ P ⊢ T ≤ E!i; i < size E; size E ≤ mxl ⟧ ⟹
⊢ [Store i],[] [::] [ty⇩i' (T#ST) E A, ty⇩i' ST E (⌊{i}⌋ ⊔ A)]"
by(auto simp:hyperset_defs nth_list_update ty⇩i'_def wt_defs ty⇩l_def
intro:list_all2_all_nthI)
lemma wt_Get:
"⟦ P ⊢ C sees F:T (fm) in D; class_type_of' U = ⌊C⌋ ⟧ ⟹
⊢ [Getfield F D],[] [::] [ty⇩i' (U # ST) E A, ty⇩i' (T # ST) E A]"
by(cases U)(auto simp: ty⇩i'_def wt_defs dest: sees_field_idemp sees_field_decl_above intro: widens_refl widen_trans widen_array_object)
lemma wt_Put:
"⟦ P ⊢ C sees F:T (fm) in D; class_type_of' U = ⌊C⌋; P ⊢ T' ≤ T ⟧ ⟹
⊢ [Putfield F D],[] [::] [ty⇩i' (T' # U # ST) E A, ty⇩i' ST E A]"
by(cases U)(auto 4 3 intro: sees_field_idemp widen_trans widen_array_object dest: sees_field_decl_above simp: ty⇩i'_def wt_defs)
lemma wt_CAS:
"⟦ P ⊢ C sees F:T (fm) in D; class_type_of' U' = ⌊C⌋; volatile fm; P ⊢ T2 ≤ T; P ⊢ T3 ≤ T ⟧ ⟹
⊢ [CAS F D],[] [::] [ty⇩i' (T3 # T2 # U' # ST) E A, ty⇩i' (Boolean # ST) E A]"
by(cases U')(auto 4 4 simp add: ty⇩i'_def wt_defs intro: sees_field_idemp widen_trans widen_array_object dest: sees_field_decl_above)
lemma wt_Throw:
"P ⊢ C ≼⇧* Throwable ⟹ ⊢ [ThrowExc],[] [::] [ty⇩i' (Class C # ST) E A, τ']"
by(simp add: ty⇩i'_def wt_defs)
lemma wt_IfFalse:
"⟦ 2 ≤ i; nat i < size τs + 2; P ⊢ ty⇩i' ST E A ≤' τs ! nat(i - 2) ⟧
⟹ ⊢ [IfFalse i],[] [::] ty⇩i' (Boolean # ST) E A # ty⇩i' ST E A # τs"
by(auto simp add: ty⇩i'_def wt_defs eval_nat_numeral nat_diff_distrib)
lemma wt_Goto:
"⟦ 0 ≤ int pc + i; nat (int pc + i) < size τs; size τs ≤ mpc;
P ⊢ τs!pc ≤' τs ! nat (int pc + i) ⟧
⟹ P,T,mxs,mpc,[] ⊢ Goto i,pc :: τs"
by(clarsimp simp add: wt_defs)
end
context TC3 begin
lemma wt_Invoke:
"⟦ size es = size Ts'; class_type_of' U = ⌊C⌋; P ⊢ C sees M: Ts→T = m in D; P ⊢ Ts' [≤] Ts ⟧
⟹ ⊢ [Invoke M (size es)],[] [::] [ty⇩i' (rev Ts' @ U # ST) E A, ty⇩i' (T#ST) E A]"
apply(clarsimp simp add: ty⇩i'_def wt_defs)
apply safe
apply(simp_all (no_asm_use))
apply(auto simp add: intro: widens_refl)
done
end
declare nth_append[simp del]
declare [[simproc del: list_to_set_comprehension]]
context TC2 begin
corollary wt_instrs_app3[simp]:
"⟦ ⊢ (is⇩2 :: 'b instr list),[] [::] (τ' # τs⇩2); ⊢ is⇩1,xt⇩1 [::] τ # τs⇩1 @ [τ']; size τs⇩1+1 = size is⇩1⟧
⟹ ⊢ (is⇩1 @ is⇩2),xt⇩1 [::] τ # τs⇩1 @ τ' # τs⇩2"
using wt_instrs_app2[where ?xt⇩2.0 = "[]" and ?'b = "'b"] by (simp add:shift_def)
corollary wt_instrs_Cons3[simp]:
"⟦ τs ≠ []; ⊢ [i],[] [::] [τ,τ']; ⊢ is,[] [::] τ'#τs ⟧
⟹ ⊢ (i # is),[] [::] τ # τ' # τs"
using wt_instrs_Cons[where ?xt = "[]"]
by (simp add:shift_def)
lemma wt_instrs_xapp:
"⟦ ⊢ is⇩1 @ is⇩2, xt [::] τs⇩1 @ ty⇩i' (Class D # ST) E A # τs⇩2;
∀τ ∈ set τs⇩1. ∀ST' LT'. τ = Some(ST',LT') ⟶
size ST ≤ size ST' ∧ P ⊢ Some (drop (size ST' - size ST) ST',LT') ≤' ty⇩i' ST E A;
size is⇩1 = size τs⇩1; size ST < mxs; case Co of None ⇒ D = Throwable | Some C ⇒ D = C ∧ is_class P C ⟧ ⟹
⊢ is⇩1 @ is⇩2, xt @ [(0,size is⇩1 - Suc n,Co,size is⇩1,size ST)] [::] τs⇩1 @ ty⇩i' (Class D # ST) E A # τs⇩2"
apply(simp add:wt_instrs_def split del: option.split_asm)
apply(rule conjI)
apply(clarsimp split del: option.split_asm)
apply arith
apply(clarsimp split del: option.split_asm)
apply(erule allE, erule (1) impE)
apply(clarsimp simp add: wt_instr_def app_def eff_def split del: option.split_asm)
apply(rule conjI)
apply (thin_tac "∀x∈ A ∪ B. P x" for A B P)
apply (thin_tac "∀x∈ A ∪ B. P x" for A B P)
apply (clarsimp simp add: xcpt_app_def relevant_entries_def split del: option.split_asm)
apply (simp add: nth_append is_relevant_entry_def split: if_split_asm split del: option.split_asm)
apply (drule_tac x="τs⇩1!pc" in bspec)
apply (blast intro: nth_mem)
apply fastforce
apply fastforce
apply (rule conjI)
apply(clarsimp split del: option.split_asm)
apply (erule disjE, blast)
apply (erule disjE, blast)
apply (clarsimp simp add: xcpt_eff_def relevant_entries_def split: if_split_asm)
apply(clarsimp split del: option.split_asm)
apply (erule disjE, blast)
apply (erule disjE, blast)
apply (clarsimp simp add: xcpt_eff_def relevant_entries_def split: if_split_asm split del: option.split_asm)
apply (simp add: nth_append is_relevant_entry_def split: if_split_asm split del: option.split_asm)
apply (drule_tac x = "τs⇩1!pc" in bspec)
apply (blast intro: nth_mem)
apply (fastforce simp add: ty⇩i'_def)
done
lemma wt_instrs_xapp_Some[trans]:
"⟦ ⊢ 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 ⊢ 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 ⟧ ⟹
⊢ is⇩1 @ is⇩2, xt @ [(0,size is⇩1 - Suc n,Some C,size is⇩1,size ST)] [::] τs⇩1 @ ty⇩i' (Class C # ST) E A # τs⇩2"
by(erule (3) wt_instrs_xapp) simp
lemma wt_instrs_xapp_Any:
"⟦ ⊢ is⇩1 @ is⇩2, xt [::] τs⇩1 @ ty⇩i' (Class Throwable # ST) E A # τs⇩2;
∀τ ∈ set τs⇩1. ∀ST' LT'. τ = Some(ST',LT') ⟶
size ST ≤ size ST' ∧ P ⊢ Some (drop (size ST' - size ST) ST',LT') ≤' ty⇩i' ST E A;
size is⇩1 = size τs⇩1; size ST < mxs ⟧ ⟹
⊢ is⇩1 @ is⇩2, xt @ [(0,size is⇩1 - Suc n,None,size is⇩1,size ST)] [::] τs⇩1 @ ty⇩i' (Class Throwable # ST) E A # τs⇩2"
by(erule (3) wt_instrs_xapp) simp
end
declare [[simproc add: list_to_set_comprehension]]
declare nth_append[simp]
lemma drop_Cons_Suc:
"⋀xs. drop n xs = y#ys ⟹ drop (Suc n) xs = ys"
apply (induct n)
apply simp
apply (simp add: drop_Suc)
done
lemma drop_mess:
"⟦Suc (length xs⇩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
lemma drop_mess2:
assumes len: "Suc (Suc (length xs0)) ≤ length xs"
and drop: "drop (length xs - Suc (Suc (length xs0))) xs = x1 # x2 # xs0"
shows "drop (length xs - length xs0) xs = xs0"
proof(cases xs)
case Nil with assms show ?thesis by simp
next
case (Cons x xs')
note Cons[simp]
show ?thesis
proof(cases xs')
case Nil with assms show ?thesis by(simp)
next
case (Cons x' xs'')
note Cons[simp]
show ?thesis
proof(rule drop_mess)
from len show "Suc (length xs0) ≤ length xs" by simp
next
have "drop (length xs - length (x2 # xs0)) xs = x2 # xs0"
proof(rule drop_mess)
from len show "Suc (length (x2 # xs0)) ≤ length xs" by(simp)
next
from drop show "drop (length xs - Suc (length (x2 # xs0))) xs = x1 # x2 # xs0" by simp
qed
thus "drop (length xs - Suc (length xs0)) xs = x2 # xs0" by(simp)
qed
qed
qed
abbreviation postfix :: "'a list ⇒ 'a list ⇒ bool" ("(_/ ⤜ _)" [51, 50] 50) where
"postfix xs ys ≡ suffix ys xs"
lemma postfix_conv_eq_length_drop:
"ST' ⤜ ST ⟷ length ST ≤ length ST' ∧ drop (length ST' - length ST) ST' = ST"
apply(auto)
apply (metis append_eq_conv_conj append_take_drop_id diff_is_0_eq drop_0 linorder_not_less nat_le_linear suffix_take)
apply (metis append_take_drop_id length_drop suffix_take same_append_eq size_list_def)
by (metis suffix_drop)
declare suffix_ConsI[simp]
context TC0 begin
declare after_def[simp] pair_eq_ty⇩i'_conv[simp]
lemma
assumes "ST0 ⤜ ST'"
shows compT_ST_prefix:
"⌊(ST,LT)⌋ ∈ set(compT E A ST0 e) ⟹ ST ⤜ ST'"
and compTs_ST_prefix:
"⌊(ST,LT)⌋ ∈ set(compTs E A ST0 es) ⟹ ST ⤜ ST'"
using assms
by(induct E A ST0 e and E A ST0 es rule: compT_compTs_induct) auto
declare after_def[simp del] pair_eq_ty⇩i'_conv[simp del]
end
declare suffix_ConsI[simp del]
lemma fun_of_simp [simp]: "fun_of S x y = ((x,y) ∈ S)"
by (simp add: fun_of_def)
declare widens_refl [iff]
context TC3 begin
theorem compT_wt_instrs:
"⟦ P,E ⊢1 e :: T; 𝒟 e A; ℬ e (size E); size ST + max_stack e ≤ mxs; size E + max_vars e ≤ mxl; set E ⊆ types P ⟧
⟹ ⊢ compE2 e, compxE2 e 0 (size ST) [::] ty⇩i' ST E A # compT E A ST e @ [after E A ST e]"
(is "PROP ?P e E T A ST")
and compTs_wt_instrs:
"⟦ P,E ⊢1 es[::]Ts; 𝒟s es A; ℬs es (size E); size ST + max_stacks es ≤ mxs; size E + max_varss es ≤ mxl; set E ⊆ types P ⟧
⟹ let τs = ty⇩i' ST E A # compTs E A ST es
in ⊢ compEs2 es,compxEs2 es 0 (size ST) [::] τs ∧ last τs = ty⇩i' (rev Ts @ ST) E (A ⊔ 𝒜s es)"
(is "PROP ?Ps es E Ts A ST")
proof(induct E A ST e and E A ST es arbitrary: T and Ts rule: compT_compTs_induct)
case (TryCatch E A ST e⇩1 C i e⇩2)
hence [simp]: "i = size E" by simp
have wt⇩1: "P,E ⊢1 e⇩1 :: T" and wt⇩2: "P,E@[Class C] ⊢1 e⇩2 :: T"
and "class": "is_class P C" using TryCatch by auto
let ?A⇩1 = "A ⊔ 𝒜 e⇩1" let ?A⇩i = "A ⊔ ⌊{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 ⊔ 𝒜 e⇩2)"
let ?τ' = "ty⇩i' (T#ST) E (A ⊔ 𝒜 e⇩1 ⊓ (𝒜 e⇩2 ⊖ i))"
let ?go = "Goto (int(size(compE2 e⇩2)) + 2)"
have "PROP ?P e⇩2 ?E⇩i T ?A⇩i ST" by fact
hence "⊢ compE2 e⇩2,compxE2 e⇩2 0 (size ST) [::] (?τ⇩3 # ?τs⇩2) @ [?τ⇩2']"
using TryCatch.prems "class" by(auto simp:after_def)
also have "?A⇩i ⊔ 𝒜 e⇩2 = (A ⊔ 𝒜 e⇩2) ⊔ ⌊{size E}⌋"
by(fastforce simp:hyperset_defs)
also have "P ⊢ ty⇩i' (T#ST) ?E⇩i … ≤' ty⇩i' (T#ST) E (A ⊔ 𝒜 e⇩2)"
by(simp add:hyperset_defs ty⇩l_incr ty⇩i'_def)
also have "P ⊢ … ≤' ty⇩i' (T#ST) E (A ⊔ 𝒜 e⇩1 ⊓ (𝒜 e⇩2 ⊖ 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 "⊢ [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(compE2 e⇩2)+3,[] ⊢ ?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 "⊢ compE2 e⇩1,compxE2 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 "compE2 e⇩1 @ ?go # [Store i] @ compE2 e⇩2 =
(compE2 e⇩1 @ [?go]) @ (Store i # compE2 e⇩2)" by simp
also
let "?Q τ" = "∀ST' LT'. τ = ⌊(ST', LT')⌋ ⟶
size ST ≤ size ST' ∧ P ⊢ Some (drop (size ST' - size ST) ST',LT') ≤' ty⇩i' ST E A"
{
have "?Q (ty⇩i' ST E A)" by(clarsimp simp add: ty⇩i'_def)
moreover have "?Q (ty⇩i' (T # ST) E ?A⇩1)"
by (fastforce simp add: ty⇩i'_def hyperset_defs intro!: ty⇩l_antimono)
moreover { fix τ
assume τ: "τ ∈ set (compT E A ST e⇩1)"
hence "∀ST' LT'. τ = ⌊(ST', LT')⌋ ⟶ ST' ⤜ ST" by(auto intro: compT_ST_prefix[OF suffix_order.order_refl])
with τ have "?Q τ" unfolding postfix_conv_eq_length_drop using ‹ℬ (try e⇩1 catch(C i) e⇩2) (length E)›
by(fastforce dest!: compT_LT_prefix simp add: ty⇩i'_def) }
ultimately
have "∀τ∈set (ty⇩i' ST E A # compT E A ST e⇩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)(erule_tac x=0 in meta_allE, simp)
next
case (Synchronized E A ST i e1 e2)
note wt = ‹P,E ⊢1 sync⇘i⇙ (e1) e2 :: T›
then obtain U where wt1: "P,E ⊢1 e1 :: U"
and U: "is_refT U" "U ≠ NT"
and wt2: "P,E@[Class Object] ⊢1 e2 :: T" by auto
from ‹ℬ (sync⇘i⇙ (e1) e2) (length E)› have [simp]: "i = length E"
and B1: "ℬ e1 (length E)" and B2: "ℬ e2 (length (E@[Class Object]))" by auto
note lenST = ‹length ST + max_stack (sync⇘i⇙ (e1) e2) ≤ mxs›
note lenE = ‹length E + max_vars (sync⇘i⇙ (e1) e2) ≤ mxl›
let ?A1 = "A ⊔ 𝒜 e1" let ?A2 = "?A1 ⊔ ⌊{i}⌋"
let ?A3 = "?A2 ⊔ 𝒜 e2" let ?A4 = "?A1 ⊔ 𝒜 e2"
let ?E1 = "E @ [Class Object]"
let ?τ = "ty⇩i' ST E A" let ?τs1 = "compT E A ST e1"
let ?τ1 = "ty⇩i' (U#ST) E ?A1"
let ?τ1' = "ty⇩i' (Class Object # Class Object # ST) E ?A1"
let ?τ1'' = "ty⇩i' (Class Object#ST) ?E1 ?A2"
let ?τ1''' = "ty⇩i' ST ?E1 ?A2"
let ?τs2 = "compT ?E1 ?A2 ST e2"
let ?τ2 = "ty⇩i' (T#ST) ?E1 ?A3" let ?τ2' = "ty⇩i' (Class Object#T#ST) ?E1 ?A3"
let ?τ2'' = ?τ2
let ?τ3 = "ty⇩i' (Class Throwable#ST) ?E1 ?A2"
let ?τ3' = "ty⇩i' (Class Object#Class Throwable#ST) ?E1 ?A2"
let ?τ3'' = ?τ3
let ?τ' = "ty⇩i' (T#ST) E ?A4"
from lenE lenST max_stack1[of e2] U
have "⊢ [Load i, MExit, ThrowExc], [] [::] [?τ3, ?τ3', ?τ3'', ?τ']"
by(auto simp add: ty⇩i'_def ty⇩l_def wt_defs hyperset_defs nth_Cons split: nat.split)
also have "P,T⇩r,mxs,5,[] ⊢ Goto 4,0 :: [?τ2'', ?τ3, ?τ3', ?τ3'', ?τ']"
by(auto simp: hyperset_defs ty⇩i'_def wt_defs intro: ty⇩l_antimono ty⇩l_incr)
also have "P,T⇩r,mxs,6,[] ⊢ MExit,0 :: [?τ2', ?τ2'', ?τ3, ?τ3', ?τ3'', ?τ']"
by(auto simp: hyperset_defs ty⇩i'_def wt_defs intro: ty⇩l_antimono ty⇩l_incr)
also from lenE lenST max_stack1[of e2]
have "P,T⇩r,mxs,7,[] ⊢ Load i,0 :: [?τ2, ?τ2', ?τ2'', ?τ3, ?τ3', ?τ3'', ?τ']"
by(auto simp: hyperset_defs ty⇩i'_def wt_defs ty⇩l_def intro: ty⇩l_antimono)
also from ‹𝒟 (sync⇘i⇙ (e1) e2) A› have "𝒟 e2 (A ⊔ 𝒜 e1 ⊔ ⌊{length E}⌋)"
by(auto elim!: D_mono' simp add: hyperset_defs)
with ‹PROP ?P e2 ?E1 T ?A2 ST› Synchronized wt2 is_class_Object[OF wf_prog]
have "⊢ compE2 e2, compxE2 e2 0 (size ST) [::] ?τ1'''#?τs2@[?τ2]"
by(auto simp add: after_def)
finally have "⊢ (compE2 e2 @ [Load i, MExit, Goto 4]) @ [Load i, MExit, ThrowExc], compxE2 e2 0 (size ST) [::]
(?τ1''' # ?τs2 @ [?τ2, ?τ2', ?τ2'']) @ [?τ3, ?τ3', ?τ3'', ?τ']"
by(simp)
hence "⊢ (compE2 e2 @ [Load i, MExit, Goto 4]) @ [Load i, MExit, ThrowExc],
compxE2 e2 0 (size ST) @ [(0, size (compE2 e2 @ [Load i, MExit, Goto 4]) - Suc 2, None, size (compE2 e2 @ [Load i, MExit, Goto 4]), size ST)] [::]
(?τ1''' # ?τs2 @ [?τ2, ?τ2', ?τ2'']) @ [?τ3, ?τ3', ?τ3'', ?τ']"
proof(rule wt_instrs_xapp_Any)
from lenST show "length ST < mxs" by simp
next
show "∀τ∈set (?τ1''' # ?τs2 @ [?τ2, ?τ2', ?τ2'']). ∀ST' LT'.
τ = ⌊(ST', LT')⌋ ⟶ length ST ≤ length ST' ∧
P ⊢ ⌊(drop (length ST' - length ST) ST', LT')⌋ ≤' ty⇩i' ST (E @ [Class Object]) ?A2"
proof(intro strip)
fix τ ST' LT'
assume "τ∈set (?τ1''' # ?τs2 @ [?τ2, ?τ2', ?τ2''])" "τ = ⌊(ST', LT')⌋"
hence τ: "⌊(ST', LT')⌋ ∈ set (?τ1''' # ?τs2 @ [?τ2, ?τ2', ?τ2''])" by simp
show "length ST ≤ length ST' ∧ P ⊢ ⌊(drop (length ST' - length ST) ST', LT')⌋ ≤' ty⇩i' ST (E @ [Class Object]) ?A2"
proof(cases "⌊(ST', LT')⌋ ∈ set ?τs2")
case True
from compT_ST_prefix[OF suffix_order.order_refl this] compT_LT_prefix[OF this B2]
show ?thesis unfolding postfix_conv_eq_length_drop by(simp add: ty⇩i'_def)
next
case False
with τ show ?thesis
by(auto simp add: ty⇩i'_def hyperset_defs intro: ty⇩l_antimono)
qed
qed
qed simp
hence "⊢ compE2 e2 @ [Load i, MExit, Goto 4, Load i, MExit, ThrowExc],
compxE2 e2 0 (size ST) @ [(0, size (compE2 e2), None, Suc (Suc (Suc (size (compE2 e2)))), size ST)] [::]
?τ1''' # ?τs2 @ [?τ2, ?τ2', ?τ2'', ?τ3, ?τ3', ?τ3'', ?τ']" by simp
also from wt1 ‹set E ⊆ types P› have "is_type P U" by(rule WT1_is_type[OF wf_prog])
with U have "P ⊢ U ≤ Class Object" by(auto elim!: is_refT.cases intro: subcls_C_Object[OF _ wf_prog] widen_array_object)
with lenE lenST max_stack1[of e2]
have "⊢ [Dup, Store i, MEnter], [] [::] [?τ1, ?τ1', ?τ1''] @ [?τ1''']"
by(auto simp add: ty⇩i'_def ty⇩l_def wt_defs hyperset_defs nth_Cons nth_list_update list_all2_conv_all_nth split: nat.split)
finally have "⊢ Dup # Store i # MEnter # compE2 e2 @ [Load i, MExit, Goto 4, Load i, MExit, ThrowExc],
compxE2 e2 3 (size ST) @ [(3, 3 + size (compE2 e2), None, 6 + size (compE2 e2), size ST)]
[::] ?τ1 # ?τ1' # ?τ1'' # ?τ1''' # ?τs2 @ [?τ2, ?τ2', ?τ2'', ?τ3, ?τ3', ?τ3'', ?τ']"
by(simp add: eval_nat_numeral shift_def)
also from ‹PROP ?P e1 E U A ST› wt1 B1 ‹𝒟 (sync⇘i⇙ (e1) e2) A› lenE lenST ‹set E ⊆ types P›
have "⊢ compE2 e1, compxE2 e1 0 (size ST) [::] ?τ#?τs1@[?τ1]"
by(auto simp add: after_def)
finally show ?case using wt1 wt2 wt by(simp add: after_def ac_simps shift_Cons_tuple hyperUn_assoc)
next
case new thus ?case by(auto simp add:after_def wt_New)
next
case (BinOp E A ST e⇩1 bop e⇩2)
have T: "P,E ⊢1 e⇩1 «bop» e⇩2 :: T" by fact
then obtain T⇩1 T⇩2 where T⇩1: "P,E ⊢1 e⇩1 :: T⇩1" and T⇩2: "P,E ⊢1 e⇩2 :: T⇩2" and
bopT: "P ⊢ T⇩1«bop»T⇩2 :: T" by auto
let ?A⇩1 = "A ⊔ 𝒜 e⇩1" let ?A⇩2 = "?A⇩1 ⊔ 𝒜 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 "⊢ [BinOpInstr bop],[] [::] [?τ⇩2,?τ']" by(rule wt_BinOpInstr)
also from BinOp.hyps(2)[of T⇩2] BinOp.prems T⇩2 T⇩1
have "⊢ compE2 e⇩2, compxE2 e⇩2 0 (size (ty E e⇩1#ST)) [::] ?τ⇩1#?τs⇩2@[?τ⇩2]" by (auto simp: after_def)
also from BinOp T⇩1 have "⊢ compE2 e⇩1, compxE2 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 E A ST e es)
have "P,E ⊢1 e # es [::] Ts" by fact
then obtain T⇩e Ts' where
T⇩e: "P,E ⊢1 e :: T⇩e" and Ts': "P,E ⊢1 es [::] Ts'" and
Ts: "Ts = T⇩e#Ts'" by auto
let ?A⇩e = "A ⊔ 𝒜 e"
let ?τ = "ty⇩i' ST E A" let ?τs⇩e = "compT E A ST e"
let ?τ⇩e = "ty⇩i' (T⇩e#ST) E ?A⇩e" let ?τs' = "compTs E ?A⇩e (T⇩e#ST) es"
let ?τs = "?τ # ?τs⇩e @ (?τ⇩e # ?τs')"
from Cons.hyps(2) Cons.prems T⇩e Ts'
have "⊢ compEs2 es, compxEs2 es 0 (size (T⇩e#ST)) [::] ?τ⇩e#?τs'" by (simp add: after_def)
also from Cons T⇩e have "⊢ compE2 e, compxE2 e 0 (size ST) [::] ?τ#?τs⇩e@[?τ⇩e]" by (auto simp: after_def)
moreover
from Cons.hyps(2)[OF Ts'] Cons.prems T⇩e Ts' Ts
have "last ?τs = ty⇩i' (rev Ts@ST) E (?A⇩e ⊔ 𝒜s es)" by simp
ultimately show ?case using T⇩e
by(auto simp add: after_def hyperUn_assoc shift_compxEs2 stack_xlift_compxEs2 simp del: compxE2_size_convs compxEs2_size_convs compxEs2_stack_xlift_convs compxE2_stack_xlift_convs intro: wt_instrs_app2)
next
case (FAss E A ST e⇩1 F D e⇩2)
hence Void: "P,E ⊢1 e⇩1∙F{D} := e⇩2 :: Void" by auto
then obtain U C T T' fm where
C: "P,E ⊢1 e⇩1 :: U" and U: "class_type_of' U = ⌊C⌋" and sees: "P ⊢ C sees F:T (fm) in D" and
T': "P,E ⊢1 e⇩2 :: T'" and T'_T: "P ⊢ T' ≤ T" by auto
let ?A⇩1 = "A ⊔ 𝒜 e⇩1" let ?A⇩2 = "?A⇩1 ⊔ 𝒜 e⇩2"
let ?τ = "ty⇩i' ST E A" let ?τs⇩1 = "compT E A ST e⇩1"
let ?τ⇩1 = "ty⇩i' (U#ST) E ?A⇩1" let ?τs⇩2 = "compT E ?A⇩1 (U#ST) e⇩2"
let ?τ⇩2 = "ty⇩i' (T'#U#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 U
have "⊢ [Putfield F D,Push Unit],[] [::] [?τ⇩2,?τ⇩3,?τ']"
by (fastforce simp add: wt_Push wt_Put)
also from FAss.hyps(2)[of T'] FAss.prems T' C
have "⊢ compE2 e⇩2, compxE2 e⇩2 0 (size ST+1) [::] ?τ⇩1#?τs⇩2@[?τ⇩2]"
by (auto simp add: after_def hyperUn_assoc)
also from FAss C have "⊢ compE2 e⇩1, compxE2 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 T exp) thus ?case by (auto simp:after_def wt_Cast)
next
case (InstanceOf E A ST e) thus ?case
by(auto simp:after_def intro!: wt_Instanceof wt_instrs_app3 intro: widen_refT refT_widen)
next
case (BlockNone E A ST i Ti e)
from ‹P,E ⊢1 {i:Ti=None; e} :: T› have wte: "P,E@[Ti] ⊢1 e :: T"
and Ti: "is_type P Ti" by auto
let ?τs = "ty⇩i' ST E A # compT (E @ [Ti]) (A⊖i) ST e"
from BlockNone wte Ti
have "⊢ compE2 e, compxE2 e 0 (size ST) [::] ?τs @ [ty⇩i' (T#ST) (E@[Ti]) (A⊖(size E) ⊔ 𝒜 e)]"
by(auto simp add: after_def)
also have "P ⊢ ty⇩i' (T # ST) (E@[Ti]) (A ⊖ size E ⊔ 𝒜 e) ≤' ty⇩i' (T # ST) (E@[Ti]) ((A ⊔ 𝒜 e) ⊖ size E)"
by(auto simp add:hyperset_defs intro: ty⇩i'_antimono)
also have "… = ty⇩i' (T # ST) E (A ⊔ 𝒜 e)" by simp
also have "P ⊢ … ≤' ty⇩i' (T # ST) E (A ⊔ (𝒜 e ⊖ i))"
by(auto simp add:hyperset_defs intro: ty⇩i'_antimono)
finally show ?case using BlockNone.prems by(simp add: after_def)
next
case (BlockSome E A ST i Ti v e)
from ‹P,E ⊢1 {i:Ti=⌊v⌋; e} :: T› obtain Tv
where Tv: "P,E ⊢1 Val v :: Tv" "P ⊢ Tv ≤ Ti"
and wte: "P,E@[Ti] ⊢1 e :: T"
and Ti: "is_type P Ti" by auto
from ‹length ST + max_stack {i:Ti=⌊v⌋; e} ≤ mxs›
have lenST: "length ST + max_stack e ≤ mxs" by simp
from ‹length E + max_vars {i:Ti=⌊v⌋; e} ≤ mxl›
have lenE: "length (E@[Ti]) + max_vars e ≤ mxl" by simp
from ‹ℬ {i:Ti=⌊v⌋; e} (length E)› have [simp]: "i = length E"
and B: "ℬ e (length (E@[Ti]))" by auto
from BlockSome wte
have "⊢ compE2 e, compxE2 e 0 (size ST) [::] (ty⇩i' ST (E @ [Ti]) (A ⊔ ⌊{length E}⌋) # compT (E @ [Ti]) (A ⊔ ⌊{i}⌋) ST e) @ [ty⇩i' (T#ST) (E@[Ti]) (A ⊔ ⌊{size E}⌋ ⊔ 𝒜 e)]"
by(auto simp add: after_def)
also have "P ⊢ ty⇩i' (T # ST) (E @ [Ti]) (A ⊔ ⌊{length E}⌋ ⊔ 𝒜 e) ≤' ty⇩i' (T # ST) (E @ [Ti]) ((A ⊔ 𝒜 e) ⊖ length E)"
by(auto simp add: hyperset_defs intro: ty⇩i'_antimono)
also have "… = ty⇩i' (T # ST) E (A ⊔ 𝒜 e)" by simp
also have "P ⊢ … ≤' ty⇩i' (T # ST) E (A ⊔ (𝒜 e ⊖ i))"
by(auto simp add:hyperset_defs intro: ty⇩i'_antimono)
also note append_Cons
also {
from lenST max_stack1[of e] Tv
have "⊢ [Push v], [] [::] [ty⇩i' ST E A, ty⇩i' (ty E (Val v) # ST) E A]"
by(auto intro: wt_Push)
moreover from Tv lenE
have "⊢ [Store (length E)], [] [::] [ty⇩i' (Tv # ST) (E @ [Ti]) (A ⊖ length E), ty⇩i' ST (E @ [Ti]) (⌊{length E}⌋ ⊔ (A ⊖ length E))]"
by -(rule wt_Store, auto)
moreover have "ty⇩i' (Tv # ST) (E @ [Ti]) (A ⊖ length E) = ty⇩i' (Tv # ST) E A" by(simp add: ty⇩i'_def)
moreover have "⌊{length E}⌋ ⊔ (A ⊖ length E) = A ⊔ ⌊{length E}⌋" by(simp add: hyperset_defs)
ultimately have "⊢ [Push v, Store (length E)], [] [::] [ty⇩i' ST E A, ty⇩i' (Tv # ST) E A, ty⇩i' ST (E @ [Ti]) (A ⊔ ⌊{length E}⌋)]"
using Tv by(auto intro: wt_instrs_Cons3)
}
finally show ?case using Tv ‹P,E ⊢1 {i:Ti=⌊v⌋; e} :: T› wte by(simp add: after_def)
next
case Var thus ?case by(auto simp:after_def wt_Load)
next
case FAcc thus ?case by(auto simp:after_def wt_Get)
next
case (LAss E A ST i e) thus ?case using max_stack1[of e]
by(auto simp: hyper_insert_comm after_def wt_Store wt_Push simp del: hyperUn_comm hyperUn_leftComm)
next
case Nil thus ?case by auto
next
case throw thus ?case by(auto simp add: after_def wt_Throw)
next
case (While E A ST e c)
obtain Tc where wte: "P,E ⊢1 e :: Boolean" and wtc: "P,E ⊢1 c :: Tc"
and [simp]: "T = Void" using While by auto
have [simp]: "ty E (while (e) c) = Void" using While by simp
let ?A⇩0 = "A ⊔ 𝒜 e" let ?A⇩1 = "?A⇩0 ⊔ 𝒜 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 "⊢ [],[] [::] [] @ ?τs" by(simp add:wt_instrs_def)
also
from While.hyps(1)[of Boolean] While.prems
have "⊢ compE2 e,compxE2 e 0 (size ST) [::] ?τ # ?τs⇩e @ [?τ⇩e]"
by (auto simp:after_def)
also
have "[] @ ?τs = (?τ # ?τs⇩e) @ ?τ⇩e # ?τ⇩1 # ?τs⇩c @ [?τ⇩c,?τ⇩2,?τ⇩1,?τ']" by simp
also
let ?n⇩e = "size(compE2 e)" let ?n⇩c = "size(compE2 c)"
let ?if = "IfFalse (int ?n⇩c + 3)"
have "⊢ [?if],[] [::] ?τ⇩e # ?τ⇩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 from While.hyps(2)[of Tc] While.prems wtc
have "⊢ compE2 c,compxE2 c 0 (size ST) [::] ?τ⇩1 # ?τs⇩c @ [?τ⇩c]"
by (auto simp:after_def)
also have "?τs = (?τ # ?τs⇩e @ [?τ⇩e,?τ⇩1] @ ?τs⇩c) @ [?τ⇩c,?τ⇩2,?τ⇩1,?τ']" by simp
also have "⊢ [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 ⊢ ?τ⇩2 ≤' ?τ" by(fastforce intro: ty⇩i'_antimono simp: hyperset_defs)
hence "P,T⇩r,mxs,size ?τs,[] ⊢ ?go,?n⇩e+?n⇩c+2 :: ?τs"
by(simp add: wt_Goto split: nat_diff_split)
also have "?τs = (?τ # ?τs⇩e @ [?τ⇩e,?τ⇩1] @ ?τs⇩c @ [?τ⇩c, ?τ⇩2]) @ [?τ⇩1, ?τ']"
by simp
also have "⊢ [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 A ST e e⇩1 e⇩2)
obtain T⇩1 T⇩2 where wte: "P,E ⊢1 e :: Boolean"
and wt⇩1: "P,E ⊢1 e⇩1 :: T⇩1" and wt⇩2: "P,E ⊢1 e⇩2 :: T⇩2"
and sub⇩1: "P ⊢ T⇩1 ≤ T" and sub⇩2: "P ⊢ T⇩2 ≤ T"
using Cond by(auto dest: is_lub_upper)
have [simp]: "ty E (if (e) e⇩1 else e⇩2) = T" using Cond by simp
let ?A⇩0 = "A ⊔ 𝒜 e" let ?A⇩2 = "?A⇩0 ⊔ 𝒜 e⇩2" let ?A⇩1 = "?A⇩0 ⊔ 𝒜 e⇩1"
let ?A' = "?A⇩0 ⊔ 𝒜 e⇩1 ⊓ 𝒜 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 "⊢ compE2 e⇩2, compxE2 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 ⊢ 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 (compE2 e⇩2) + 1))"
from sub⇩1 have "P,T⇩r,mxs,size(compE2 e⇩2)+2,[] ⊢ ?g⇩2,0 :: ?τ⇩3#(?τ⇩2#?τs⇩2)@[?τ']"
by(cases "length (compE2 e⇩2)")
(auto simp: hyperset_defs wt_defs nth_Cons ty⇩i'_def neq_Nil_conv
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 "⊢ compE2 e⇩1,compxE2 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 (compE2 e⇩1) + 2))"
let ?code = "compE2 e⇩1 @ ?g⇩2 # compE2 e⇩2"
have "⊢ [?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 "⊢ compE2 e, compxE2 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 A ST e M es)
from ‹P,E ⊢1 e∙M(es) :: T›
obtain U C D Ts m Ts'
where C: "P,E ⊢1 e :: U"
and icto: "class_type_of' U = ⌊C⌋"
and "method": "P ⊢ C sees M:Ts → T = m in D"
and wtes: "P,E ⊢1 es [::] Ts'" and subs: "P ⊢ Ts' [≤] Ts"
by(cases) auto
from wtes have same_size: "size es = size Ts'" by(rule WTs1_same_size)
let ?A⇩0 = "A ⊔ 𝒜 e" let ?A⇩1 = "?A⇩0 ⊔ 𝒜s es"
let ?τ = "ty⇩i' ST E A" let ?τs⇩e = "compT E A ST e"
let ?τ⇩e = "ty⇩i' (U # ST) E ?A⇩0"
let ?τs⇩e⇩s = "compTs E ?A⇩0 (U # ST) es"
let ?τ⇩1 = "ty⇩i' (rev Ts' @ U # ST) E ?A⇩1"
let ?τ' = "ty⇩i' (T # ST) E ?A⇩1"
have "⊢ [Invoke M (size es)],[] [::] [?τ⇩1,?τ']"
by(rule wt_Invoke[OF same_size icto "method" subs])
also
from Call.hyps(2)[of Ts'] Call.prems wtes C
have "⊢ compEs2 es,compxEs2 es 0 (size ST+1) [::] ?τ⇩e # ?τs⇩e⇩s"
"last (?τ⇩e # ?τs⇩e⇩s) = ?τ⇩1"
by(auto simp add:after_def)
also have "(?τ⇩e # ?τs⇩e⇩s) @ [?τ'] = ?τ⇩e # ?τs⇩e⇩s @ [?τ']" by simp
also have "⊢ compE2 e,compxE2 e 0 (size ST) [::] ?τ # ?τs⇩e @ [?τ⇩e]"
using Call C by(auto simp add:after_def)
finally show ?case using Call.prems C
by(simp add:after_def hyperUn_assoc shift_compxEs2 stack_xlift_compxEs2 del: compxEs2_stack_xlift_convs compxEs2_size_convs)
next
case Seq thus ?case
by(auto simp:after_def)
(fastforce simp:wt_Push wt_Pop hyperUn_assoc
intro:wt_instrs_app2 wt_instrs_Cons)
next
case (NewArray E A ST Ta e)
from ‹P,E ⊢1 newA Ta⌊e⌉ :: T›
have "⊢ [NewArray Ta], [] [::] [ty⇩i' (Integer # ST) E (A ⊔ 𝒜 e), ty⇩i' (Ta⌊⌉ # ST) E (A ⊔ 𝒜 e)]"
by(auto simp:hyperset_defs ty⇩i'_def wt_defs ty⇩l_def)
with NewArray show ?case by(auto simp: after_def intro: wt_instrs_app3)
next
case (ALen E A ST exp)
{ fix T
have "⊢ [ALength], [] [::] [ty⇩i' (T⌊⌉ # ST) E (A ⊔ 𝒜 exp), ty⇩i' (Integer # ST) E (A ⊔ 𝒜 exp)]"
by(auto simp:hyperset_defs ty⇩i'_def wt_defs ty⇩l_def) }
with ALen show ?case by(auto simp add: after_def)(rule wt_instrs_app2, auto)
next
case (AAcc E A ST a i)
from ‹P,E ⊢1 a⌊i⌉ :: T› have wta: "P,E ⊢1 a :: T⌊⌉" and wti: "P,E ⊢1 i :: Integer" by auto
let ?A1 = "A ⊔ 𝒜 a" let ?A2 = "?A1 ⊔ 𝒜 i"
let ?τ = "ty⇩i' ST E A" let ?τsa = "compT E A ST a"
let ?τ1 = "ty⇩i' (T⌊⌉#ST) E ?A1" let ?τsi = "compT E ?A1 (T⌊⌉#ST) i"
let ?τ2 = "ty⇩i' (Integer#T⌊⌉#ST) E ?A2" let ?τ' = "ty⇩i' (T#ST) E ?A2"
have "⊢ [ALoad], [] [::] [?τ2,?τ']" by(auto simp add: ty⇩i'_def wt_defs)
also from AAcc.hyps(2)[of Integer] AAcc.prems wti wta
have "⊢ compE2 i, compxE2 i 0 (size ST+1) [::] ?τ1#?τsi@[?τ2]"
by(auto simp add: after_def)
also from wta AAcc have "⊢ compE2 a, compxE2 a 0 (size ST) [::] ?τ#?τsa@[?τ1]"
by(auto simp add: after_def)
finally show ?case using wta wti ‹P,E ⊢1 a⌊i⌉ :: T› by(simp add: after_def hyperUn_assoc)
next
case (AAss E A ST a i e)
note wt = ‹P,E ⊢1 a⌊i⌉ := e :: T›
then obtain Ta U where wta: "P,E ⊢1 a :: Ta⌊⌉" and wti: "P,E ⊢1 i :: Integer"
and wte: "P,E ⊢1 e :: U" and U: "P ⊢ U ≤ Ta" and [simp]: "T = Void" by auto
let ?A1 = "A ⊔ 𝒜 a" let ?A2 = "?A1 ⊔ 𝒜 i" let ?A3 = "?A2 ⊔ 𝒜 e"
let ?τ = "ty⇩i' ST E A" let ?τsa = "compT E A ST a"
let ?τ1 = "ty⇩i' (Ta⌊⌉#ST) E ?A1" let ?τsi = "compT E ?A1 (Ta⌊⌉#ST) i"
let ?τ2 = "ty⇩i' (Integer#Ta⌊⌉#ST) E ?A2" let ?τse = "compT E ?A2 (Integer#Ta⌊⌉#ST) e"
let ?τ3 = "ty⇩i' (U#Integer#Ta⌊⌉#ST) E ?A3" let ?τ4 = "ty⇩i' ST E ?A3"
let ?τ' = "ty⇩i' (Void#ST) E ?A3"
from ‹length ST + max_stack (a⌊i⌉ := e) ≤ mxs›
have "⊢ [AStore, Push Unit], [] [::] [?τ3,?τ4,?τ']"
by(auto simp add: ty⇩i'_def wt_defs nth_Cons split: nat.split)
also from AAss.hyps(3)[of U] wte AAss.prems wta wti
have "⊢ compE2 e, compxE2 e 0 (size ST+2) [::] ?τ2#?τse@[?τ3]"
by(auto simp add: after_def)
also from AAss.hyps(2)[of Integer] wti wta AAss.prems
have "⊢ compE2 i, compxE2 i 0 (size ST+1) [::] ?τ1#?τsi@[?τ2]"
by(auto simp add: after_def)
also from wta AAss have "⊢ compE2 a, compxE2 a 0 (size ST) [::] ?τ#?τsa@[?τ1]"
by(auto simp add: after_def)
finally show ?case using wta wti wte ‹P,E ⊢1 a⌊i⌉ := e :: T›
by(simp add: after_def hyperUn_assoc)
next
case (CompareAndSwap E A ST e1 D F e2 e3)
note wt = ‹P,E ⊢1 e1∙compareAndSwap(D∙F, e2, e3) :: T›
then obtain T1 T2 T3 C fm T' where [simp]: "T = Boolean"
and wt1: "P,E ⊢1 e1 :: T1" "class_type_of' T1 = ⌊C⌋" "P ⊢ C sees F:T' (fm) in D" "volatile fm"
and wt2: "P,E ⊢1 e2 :: T2" "P ⊢ T2 ≤ T'" and wt3: "P,E ⊢1 e3 :: T3" "P ⊢ T3 ≤ T'"
by auto
let ?A1 = "A ⊔ 𝒜 e1" let ?A2 = "?A1 ⊔ 𝒜 e2" let ?A3 = "?A2 ⊔ 𝒜 e3"
let ?τ = "ty⇩i' ST E A" let ?τs1 = "compT E A ST e1"
let ?τ1 = "ty⇩i' (T1#ST) E ?A1" let ?τs2 = "compT E ?A1 (T1#ST) e2"
let ?τ2 = "ty⇩i' (T2#T1#ST) E ?A2" let ?τs3 = "compT E ?A2 (T2#T1#ST) e3"
let ?τ3 = "ty⇩i' (T3#T2#T1#ST) E ?A3"
let ?τ' = "ty⇩i' (Boolean#ST) E ?A3"
from ‹length ST + max_stack (e1∙compareAndSwap(D∙F, e2, e3)) ≤ mxs›
have "⊢ [CAS F D], [] [::] [?τ3,?τ']" using wt1 wt2 wt3
by(cases T1)(auto simp add: ty⇩i'_def wt_defs nth_Cons split: nat.split intro: sees_field_idemp widen_trans[OF widen_array_object] dest: sees_field_decl_above)
also from CompareAndSwap.hyps(3)[of T3] wt3 CompareAndSwap.prems wt1 wt2
have "⊢ compE2 e3, compxE2 e3 0 (size ST+2) [::] ?τ2#?τs3@[?τ3]"
by(auto simp add: after_def)
also from CompareAndSwap.hyps(2)[of T2] wt2 wt1 CompareAndSwap.prems
have "⊢ compE2 e2, compxE2 e2 0 (size ST+1) [::] ?τ1#?τs2@[?τ2]"
by(auto simp add: after_def)
also from wt1 CompareAndSwap have "⊢ compE2 e1, compxE2 e1 0 (size ST) [::] ?τ#?τs1@[?τ1]"
by(auto simp add: after_def)
also have "ty E (e1∙compareAndSwap(D∙F, e2, e3)) = T" using wt by(rule ty_def2)
ultimately show ?case using wt1 wt2 wt3
by(simp add: after_def hyperUn_assoc)
next
case (InSynchronized i a exp) thus ?case by auto
qed
end
lemma states_compP [simp]: "states (compP f P) mxs mxl = states P mxs mxl"
by (simp add: JVM_states_unfold)
lemma [simp]: "app⇩i (i, compP f P, pc, mpc, T, τ) = app⇩i (i, P, pc, mpc, T, τ)"
proof -
{ fix ST LT
have "app⇩i (i, compP f P, pc, mpc, T, (ST, LT)) = app⇩i (i, P, pc, mpc, T, (ST, LT))"
proof(cases i)
case (Invoke M n)
have "⋀C Ts D. (∃T m. compP f P ⊢ C sees M: Ts→T = m in D) ⟷ (∃T m. P ⊢ C sees M: Ts→T = m in D)"
by(auto dest!: sees_method_compPD dest: sees_method_compP)
with Invoke show ?thesis by clarsimp
qed(simp_all) }
thus ?thesis by(cases τ) simp
qed
lemma [simp]: "is_relevant_entry (compP f P) i = is_relevant_entry P i"
apply (rule ext)+
apply (unfold is_relevant_entry_def)
apply (cases i)
apply auto
done
lemma [simp]: "relevant_entries (compP f P) i pc xt = relevant_entries P i pc xt"
by (simp add: relevant_entries_def)
lemma [simp]: "app i (compP f P) mpc T pc mxl xt τ = app i P mpc T pc mxl xt τ"
apply (simp add: app_def xcpt_app_def eff_def xcpt_eff_def norm_eff_def)
apply (fastforce simp add: image_def)
done
lemma [simp]: "app i P mpc T pc mxl xt τ ⟹ eff i (compP f P) pc xt τ = eff i P pc xt τ"
apply (clarsimp simp add: eff_def norm_eff_def xcpt_eff_def app_def)
apply (cases i)
apply(auto)
done
lemma [simp]: "widen (compP f P) = widen P"
apply (rule ext)+
apply (simp)
done
lemma [simp]: "compP f P ⊢ τ ≤' τ' = P ⊢ τ ≤' τ'"
by (simp add: sup_state_opt_def sup_state_def sup_ty_opt_def)
lemma [simp]: "compP f P,T,mpc,mxl,xt ⊢ i,pc :: τs = P,T,mpc,mxl,xt ⊢ i,pc :: τs"
by (simp add: wt_instr_def cong: conj_cong)
declare TC0.compT_sizes[simp] TC1.ty_def2[OF TC1.intro, simp]
lemma compT_method:
fixes e and A and C and Ts and mxl⇩0
defines [simp]: "E ≡ Class C # Ts"
and [simp]: "A ≡ ⌊{..size Ts}⌋"
and [simp]: "A' ≡ A ⊔ 𝒜 e"
and [simp]: "mxs ≡ max_stack e"
and [simp]: "mxl⇩0 ≡ max_vars e"
and [simp]: "mxl ≡ 1 + size Ts + mxl⇩0"
assumes wf_prog: "wf_prog p P"
shows "⟦ P,E ⊢1 e :: T; 𝒟 e A; ℬ e (size E); set E ⊆ types P; P ⊢ T ≤ T' ⟧ ⟹
wt_method (compP2 P) C Ts T' mxs mxl⇩0 (compE2 e @ [Return]) (compxE2 e 0 0)
(TC0.ty⇩i' mxl [] E A # TC0.compTa P mxl E A [] e)"
using wf_prog
apply(simp add:wt_method_def TC0.compTa_def TC0.after_def compP2_def compMb2_def)
apply(rule conjI)
apply(simp add:check_types_def TC0.OK_ty⇩i'_in_statesI)
apply(rule conjI)
apply(frule WT1_is_type[OF wf_prog])
apply simp
apply(insert max_stack1[of e])
apply(fastforce intro!: TC0.OK_ty⇩i'_in_statesI)
apply(erule (1) TC1.compT_states[OF TC1.intro])
apply simp
apply simp
apply simp
apply simp
apply(rule conjI)
apply(fastforce simp add:wt_start_def TC0.ty⇩i'_def TC0.ty⇩l_def list_all2_conv_all_nth nth_Cons split:nat.split dest:less_antisym)
apply (frule (1) TC3.compT_wt_instrs[OF TC3.intro[OF TC1.intro], where ST = "[]" and mxs = "max_stack e" and mxl = "1 + size Ts + max_vars e"])
apply simp
apply simp
apply simp
apply simp
apply simp
apply (clarsimp simp:TC2.wt_instrs_def TC0.after_def)
apply(rule conjI)
apply (fastforce)
apply(clarsimp)
apply(drule (1) less_antisym)
apply(thin_tac "∀x. P x" for P)
apply(clarsimp simp:TC2.wt_defs xcpt_app_pcs xcpt_eff_pcs TC0.ty⇩i'_def)
done
definition compTP :: "'addr J1_prog ⇒ ty⇩P"
where
"compTP P C M ≡
let (D,Ts,T,meth) = method P C M;
e = the meth;
E = Class C # Ts;
A = ⌊{..size Ts}⌋;
mxl = 1 + size Ts + max_vars e
in (TC0.ty⇩i' mxl [] E A # TC0.compTa P mxl E A [] e)"
theorem wt_compTP_compP2:
"wf_J1_prog P ⟹ wf_jvm_prog⇘compTP P⇙ (compP2 P)"
apply (simp add: wf_jvm_prog_phi_def compP2_def compMb2_def)
apply (rule wf_prog_compPI)
prefer 2 apply assumption
apply (clarsimp simp add: wf_mdecl_def)
apply (simp add: compTP_def)
apply (rule compT_method [simplified compP2_def compMb2_def, simplified])
apply assumption+
apply (drule (1) sees_wf_mdecl)
apply (simp add: wf_mdecl_def)
apply (fastforce intro: sees_method_is_class)
apply assumption
done
theorem wt_compP2:
"wf_J1_prog P ⟹ wf_jvm_prog (compP2 P)"
by(auto simp add: wf_jvm_prog_def intro: wt_compTP_compP2)
end