Theory JVMJ1
section ‹Correctness of Stage 2: From JVM to intermediate language›
theory JVMJ1 imports
J1JVMBisim
begin
declare split_paired_Ex[simp del]
lemma rec_option_is_case_option: "rec_option = case_option"
apply (rule ext)+
apply (rename_tac y)
apply (case_tac y)
apply auto
done
context J1_JVM_heap_base begin
lemma assumes ha: "typeof_addr h a = ⌊Class_type D⌋"
and subclsObj: "P ⊢ D ≼⇧* Throwable"
shows bisim1_xcp_τRed:
"⟦ P,e,h ⊢ (e', xs) ↔ (stk, loc, pc, ⌊a⌋);
match_ex_table (compP f P) (cname_of h a) pc (compxE2 e 0 0) = None;
∃n. n + max_vars e' ≤ length xs ∧ ℬ e n ⟧
⟹ τred1r P t h (e', xs) (Throw a, loc) ∧ P,e,h ⊢ (Throw a, loc) ↔ (stk, loc, pc, ⌊a⌋)"
and bisims1_xcp_τReds:
"⟦ P,es,h ⊢ (es', xs) [↔] (stk, loc, pc, ⌊a⌋);
match_ex_table (compP f P) (cname_of h a) pc (compxEs2 es 0 0) = None;
∃n. n + max_varss es' ≤ length xs ∧ ℬs es n ⟧
⟹ ∃vs es''. τreds1r P t h (es', xs) (map Val vs @ Throw a # es'', loc) ∧
P,es,h ⊢ (map Val vs @ Throw a # es'', loc) [↔] (stk, loc, pc, ⌊a⌋)"
proof(induct "(e', xs)" "(stk, loc, pc, ⌊a :: 'addr⌋)"
and "(es', xs)" "(stk, loc, pc, ⌊a :: 'addr⌋)"
arbitrary: e' xs stk loc pc and es' xs stk loc pc rule: bisim1_bisims1.inducts)
case bisim1NewThrow thus ?case
by(fastforce intro: bisim1_bisims1.intros)
next
case bisim1NewArray thus ?case
by(auto intro: rtranclp.rtrancl_into_rtrancl New1ArrayThrow bisim1_bisims1.intros dest: bisim1_ThrowD elim!: NewArray_τred1r_xt)
next
case bisim1NewArrayThrow thus ?case
by(fastforce intro: bisim1_bisims1.intros)
next
case bisim1NewArrayFail thus ?case
by(fastforce intro: bisim1_bisims1.intros)
next
case bisim1Cast thus ?case
by(fastforce intro: rtranclp.rtrancl_into_rtrancl Cast1Throw bisim1_bisims1.intros dest: bisim1_ThrowD elim!: Cast_τred1r_xt)
next
case bisim1CastThrow thus ?case
by(fastforce intro: bisim1_bisims1.intros)
next
case bisim1CastFail thus ?case
by(fastforce intro: bisim1_bisims1.intros)
next
case bisim1InstanceOf thus ?case
by(fastforce intro: rtranclp.rtrancl_into_rtrancl InstanceOf1Throw bisim1_bisims1.intros dest: bisim1_ThrowD elim!: InstanceOf_τred1r_xt)
next
case bisim1InstanceOfThrow thus ?case
by(fastforce intro: bisim1_bisims1.intros)
next
case bisim1BinOp1 thus ?case
by(fastforce intro: rtranclp.rtrancl_into_rtrancl Bin1OpThrow1 bisim1_bisims1.intros simp add: match_ex_table_append dest: bisim1_ThrowD elim!: BinOp_τred1r_xt1)
next
case bisim1BinOp2 thus ?case
by(clarsimp simp add: match_ex_table_append_not_pcs compxE2_size_convs compxE2_stack_xlift_convs match_ex_table_shift_pc_None)
(fastforce intro: rtranclp.rtrancl_into_rtrancl red1_reds1.intros bisim1BinOpThrow2 elim!: BinOp_τred1r_xt2)
next
case bisim1BinOpThrow1 thus ?case
by(auto simp add: match_ex_table_append intro: bisim1_bisims1.intros)
next
case (bisim1BinOpThrow2 e xs stk loc pc e1 bop)
note bisim = ‹P,e,h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)›
hence "xs = loc" by(auto dest: bisim1_ThrowD)
with bisim show ?case
by(auto intro: bisim1_bisims1.bisim1BinOpThrow2)
next
case bisim1BinOpThrow thus ?case
by(fastforce intro: bisim1_bisims1.intros)
next
case bisim1LAss1 thus ?case
by(fastforce intro: rtranclp.rtrancl_into_rtrancl LAss1Throw bisim1_bisims1.intros dest: bisim1_ThrowD elim!: LAss_τred1r)
next
case bisim1LAssThrow thus ?case
by(fastforce intro: bisim1_bisims1.intros)
next
case bisim1AAcc1 thus ?case
by(fastforce intro: rtranclp.rtrancl_into_rtrancl AAcc1Throw1 bisim1_bisims1.intros simp add: match_ex_table_append dest: bisim1_ThrowD elim!: AAcc_τred1r_xt1)
next
case bisim1AAcc2 thus ?case
by(clarsimp simp add: match_ex_table_append_not_pcs compxE2_size_convs compxE2_stack_xlift_convs match_ex_table_shift_pc_None)
(fastforce intro: rtranclp.rtrancl_into_rtrancl red1_reds1.intros bisim1AAccThrow2 elim!: AAcc_τred1r_xt2)
next
case bisim1AAccThrow1 thus ?case
by(auto simp add: match_ex_table_append intro: bisim1_bisims1.intros)
next
case bisim1AAccThrow2 thus ?case
by(auto simp add: match_ex_table_append intro: bisim1_bisims1.intros dest: bisim1_ThrowD)
next
case bisim1AAccFail thus ?case
by(fastforce intro: bisim1_bisims1.intros)
next
case bisim1AAss1 thus ?case
by(fastforce intro: rtranclp.rtrancl_into_rtrancl AAss1Throw1 bisim1_bisims1.intros simp add: match_ex_table_append dest: bisim1_ThrowD elim!: AAss_τred1r_xt1)
next
case bisim1AAss2 thus ?case
by(clarsimp simp add: compxE2_size_convs compxE2_stack_xlift_convs)
(fastforce simp add: match_ex_table_append intro: rtranclp.rtrancl_into_rtrancl red1_reds1.intros bisim1AAssThrow2 elim!: AAss_τred1r_xt2)
next
case bisim1AAss3 thus ?case
by(clarsimp simp add: compxE2_size_convs compxE2_stack_xlift_convs)
(fastforce simp add: match_ex_table_append intro: rtranclp.rtrancl_into_rtrancl red1_reds1.intros bisim1AAssThrow3 elim!: AAss_τred1r_xt3)
next
case bisim1AAssThrow1 thus ?case
by(auto simp add: match_ex_table_append intro: bisim1_bisims1.intros)
next
case (bisim1AAssThrow2 e xs stk loc pc i e2)
note bisim = ‹P,e,h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)›
hence "xs = loc" by(auto dest: bisim1_ThrowD)
with bisim show ?case
by(auto intro: bisim1_bisims1.bisim1AAssThrow2)
next
case (bisim1AAssThrow3 e xs stk loc pc A i)
note bisim = ‹P,e,h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)›
hence "xs = loc" by(auto dest: bisim1_ThrowD)
with bisim show ?case
by(auto intro: bisim1_bisims1.bisim1AAssThrow3)
next
case bisim1AAssFail thus ?case
by(fastforce intro: bisim1_bisims1.intros)
next
case bisim1ALength thus ?case
by(fastforce intro: rtranclp.rtrancl_into_rtrancl ALength1Throw bisim1_bisims1.intros dest: bisim1_ThrowD elim!: ALength_τred1r_xt)
next
case bisim1ALengthThrow thus ?case
by(fastforce intro: bisim1_bisims1.intros)
next
case bisim1ALengthNull thus ?case
by(fastforce intro: bisim1_bisims1.intros)
next
case bisim1FAcc thus ?case
by(fastforce intro: rtranclp.rtrancl_into_rtrancl FAcc1Throw bisim1_bisims1.intros dest: bisim1_ThrowD elim!: FAcc_τred1r_xt)
next
case bisim1FAccThrow thus ?case
by(fastforce intro: bisim1_bisims1.intros)
next
case bisim1FAccNull thus ?case
by(fastforce intro: bisim1_bisims1.intros)
next
case bisim1FAss1 thus ?case
by(fastforce intro: rtranclp.rtrancl_into_rtrancl FAss1Throw1 bisim1_bisims1.intros simp add: match_ex_table_append dest: bisim1_ThrowD elim!: FAss_τred1r_xt1)
next
case bisim1FAss2 thus ?case
by(clarsimp simp add: match_ex_table_append_not_pcs compxE2_size_convs compxE2_stack_xlift_convs)
(fastforce intro: rtranclp.rtrancl_into_rtrancl red1_reds1.intros bisim1FAssThrow2 elim!: FAss_τred1r_xt2)
next
case bisim1FAssThrow1 thus ?case
by(auto simp add: match_ex_table_append intro: bisim1_bisims1.intros)
next
case (bisim1FAssThrow2 e2 xs stk loc pc e)
note bisim = ‹P,e2,h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)›
hence "xs = loc" by(auto dest: bisim1_ThrowD)
with bisim show ?case
by(auto intro: bisim1_bisims1.bisim1FAssThrow2)
next
case bisim1FAssNull thus ?case
by(fastforce intro: bisim1_bisims1.intros)
next
case bisim1CAS1 thus ?case
by(fastforce intro: rtranclp.rtrancl_into_rtrancl CAS1Throw bisim1_bisims1.intros simp add: match_ex_table_append dest: bisim1_ThrowD elim!: CAS_τred1r_xt1)
next
case bisim1CAS2 thus ?case
by(clarsimp simp add: compxE2_size_convs compxE2_stack_xlift_convs)
(fastforce simp add: match_ex_table_append intro: rtranclp.rtrancl_into_rtrancl red1_reds1.intros bisim1CASThrow2 elim!: CAS_τred1r_xt2)
next
case bisim1CAS3 thus ?case
by(clarsimp simp add: compxE2_size_convs compxE2_stack_xlift_convs)
(fastforce simp add: match_ex_table_append intro: rtranclp.rtrancl_into_rtrancl red1_reds1.intros bisim1CASThrow3 elim!: CAS_τred1r_xt3)
next
case bisim1CASThrow1 thus ?case
by(auto simp add: match_ex_table_append intro: bisim1_bisims1.intros)
next
case (bisim1CASThrow2 e xs stk loc pc i e2)
note bisim = ‹P,e,h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)›
hence "xs = loc" by(auto dest: bisim1_ThrowD)
with bisim show ?case
by(auto intro: bisim1_bisims1.bisim1CASThrow2)
next
case (bisim1CASThrow3 e xs stk loc pc A i)
note bisim = ‹P,e,h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)›
hence "xs = loc" by(auto dest: bisim1_ThrowD)
with bisim show ?case
by(auto intro: bisim1_bisims1.bisim1CASThrow3)
next
case bisim1CASFail thus ?case
by(fastforce intro: bisim1_bisims1.intros)
next
case bisim1Call1 thus ?case
by(fastforce intro: rtranclp.rtrancl_into_rtrancl Call1ThrowObj bisim1_bisims1.intros simp add: match_ex_table_append dest: bisim1_ThrowD elim!: Call_τred1r_obj)
next
case bisim1CallParams thus ?case
by(clarsimp simp add: match_ex_table_append_not_pcs compxE2_size_convs compxEs2_size_convs compxE2_stack_xlift_convs compxEs2_stack_xlift_convs match_ex_table_shift_pc_None)
(fastforce intro: rtranclp.rtrancl_into_rtrancl Call1ThrowParams[OF refl] bisim1CallThrowParams elim!: Call_τred1r_param)
next
case bisim1CallThrowObj thus ?case
by(auto simp add: match_ex_table_append intro: bisim1_bisims1.intros)
next
case (bisim1CallThrowParams es vs es' xs stk loc pc obj M)
note bisim = ‹P,es,h ⊢ (map Val vs @ Throw a # es', xs) [↔] (stk, loc, pc, ⌊a⌋)›
hence "xs = loc" by(auto dest: bisims1_ThrowD)
with bisim show ?case
by(auto intro: bisim1_bisims1.bisim1CallThrowParams)
next
case bisim1CallThrow thus ?case
by(auto intro: bisim1_bisims1.intros)
next
case (bisim1BlockSome4 e e' xs stk loc pc V Ty v)
from ‹∃n. n + max_vars {V:Ty=None; e'} ≤ length xs ∧ ℬ {V:Ty=⌊v⌋; e} n›
have V: "V < length xs" by simp
from bisim1BlockSome4 have Red: "τred1r P t h (e', xs) (Throw a, loc)"
and bisim: "P,e,h ⊢ (Throw a, loc) ↔ (stk, loc, pc, ⌊a⌋)"
by(auto simp add: match_ex_table_append_not_pcs compxE2_size_convs compxEs2_size_convs compxE2_stack_xlift_convs compxEs2_stack_xlift_convs match_ex_table_shift_pc_None intro!: exI[where x="Suc V"] elim: meta_impE)
note len = τred1r_preserves_len[OF Red]
from Red have "τred1r P t h ({V:Ty=None; e'}, xs) ({V:Ty=None; Throw a}, loc)" by(auto intro: Block_None_τred1r_xt)
thus ?case using V len bisim
by(auto intro: τmove1BlockThrow Block1Throw bisim1BlockThrowSome elim!: rtranclp.rtrancl_into_rtrancl)
next
case bisim1BlockThrowSome thus ?case
by(auto dest: bisim1_ThrowD intro: bisim1_bisims1.bisim1BlockThrowSome)
next
case (bisim1BlockNone e e' xs stk loc pc V Ty)
hence Red: "τred1r P t h (e', xs) (Throw a, loc)"
and bisim: "P,e,h ⊢ (Throw a, loc) ↔ (stk, loc, pc, ⌊a⌋)"
by(auto elim: meta_impE intro!: exI[where x="Suc V"])
from Red have len: "length loc = length xs" by(rule τred1r_preserves_len)
from ‹∃n. n + max_vars {V:Ty=None; e'} ≤ length xs ∧ ℬ {V:Ty=None; e} n›
have V: "V < length xs" by simp
from Red have "τred1r P t h ({V:Ty=None; e'}, xs) ({V:Ty=None; Throw a}, loc)" by(rule Block_None_τred1r_xt)
thus ?case using V len bisim
by(auto intro: τmove1BlockThrow Block1Throw bisim1BlockThrowNone elim!: rtranclp.rtrancl_into_rtrancl)
next
case bisim1BlockThrowNone thus ?case
by(auto dest: bisim1_ThrowD intro: bisim1_bisims1.bisim1BlockThrowNone)
next
case bisim1Sync1 thus ?case
by(fastforce intro: rtranclp.rtrancl_into_rtrancl Synchronized1Throw1 bisim1_bisims1.intros simp add: match_ex_table_append dest: bisim1_ThrowD elim!: Sync_τred1r_xt)
next
case (bisim1Sync4 e2 e' xs stk loc pc V e1 a')
from ‹P,e2,h ⊢ (e', xs) ↔ (stk, loc, pc, ⌊a⌋)›
have "pc < length (compE2 e2)" by(auto dest!: bisim1_xcp_pcD)
with ‹match_ex_table (compP f P) (cname_of h a) (Suc (Suc (Suc (length (compE2 e1) + pc)))) (compxE2 (sync⇘V⇙ (e1) e2) 0 0) = None› subclsObj ha
have False by(simp add: match_ex_table_append matches_ex_entry_def split: if_split_asm)
thus ?case ..
next
case bisim1Sync10 thus ?case
by(fastforce intro: bisim1_bisims1.intros)
next
case bisim1Sync11 thus ?case
by(fastforce intro: bisim1_bisims1.intros)
next
case bisim1Sync12 thus ?case
by(fastforce intro: bisim1_bisims1.intros)
next
case bisim1Sync14 thus ?case
by(fastforce intro: bisim1_bisims1.intros)
next
case bisim1SyncThrow thus ?case
by(auto simp add: match_ex_table_append intro: bisim1_bisims1.intros)
next
case bisim1Seq1 thus ?case
by(fastforce intro: rtranclp.rtrancl_into_rtrancl Seq1Throw bisim1_bisims1.intros dest: bisim1_ThrowD elim!: Seq_τred1r_xt simp add: match_ex_table_append)
next
case bisim1SeqThrow1 thus ?case
by(auto simp add: match_ex_table_append intro: bisim1_bisims1.intros)
next
case bisim1Seq2 thus ?case
by(auto simp add: match_ex_table_append_not_pcs compxE2_size_convs compxE2_stack_xlift_convs match_ex_table_shift_pc_None intro: bisim1_bisims1.bisim1Seq2)
next
case bisim1Cond1 thus ?case
by(fastforce intro: rtranclp.rtrancl_into_rtrancl Cond1Throw bisim1_bisims1.intros dest: bisim1_ThrowD elim!: Cond_τred1r_xt simp add: match_ex_table_append)
next
case bisim1CondThen thus ?case
by(clarsimp simp add: match_ex_table_append)
(auto simp add: match_ex_table_append_not_pcs compxE2_size_convs compxE2_stack_xlift_convs match_ex_table_shift_pc_None intro: bisim1_bisims1.bisim1CondThen)
next
case bisim1CondElse thus ?case
by(clarsimp simp add: match_ex_table_append)
(auto simp add: match_ex_table_append_not_pcs compxE2_size_convs compxE2_stack_xlift_convs match_ex_table_shift_pc_None intro: bisim1_bisims1.bisim1CondElse)
next
case bisim1CondThrow thus ?case
by(auto simp add: match_ex_table_append intro: bisim1_bisims1.intros)
next
case bisim1While3 thus ?case
by(fastforce intro: rtranclp.rtrancl_into_rtrancl Cond1Throw bisim1_bisims1.intros dest: bisim1_ThrowD elim!: Cond_τred1r_xt simp add: match_ex_table_append)
next
case (bisim1While4 e e' xs stk loc pc c)
hence "τred1r P t h (e', xs) (Throw a, loc) ∧ P,e,h ⊢ (Throw a, loc) ↔ (stk, loc, pc, ⌊a⌋)"
by(auto simp add: match_ex_table_append_not_pcs compxE2_size_convs compxEs2_size_convs compxE2_stack_xlift_convs compxEs2_stack_xlift_convs match_ex_table_shift_pc_None)
hence "τred1r P t h (e';;while (c) e, xs) (Throw a, loc)"
"P,while (c) e,h ⊢ (Throw a, loc) ↔ (stk, loc, Suc (length (compE2 c) + pc), ⌊a⌋)"
by(auto intro: rtranclp.rtrancl_into_rtrancl Seq1Throw τmove1SeqThrow bisim1WhileThrow2 elim!: Seq_τred1r_xt)
thus ?case ..
next
case bisim1WhileThrow1 thus ?case
by(auto simp add: match_ex_table_append intro: bisim1_bisims1.intros)
next
case bisim1WhileThrow2 thus ?case
by(auto simp add: match_ex_table_append intro: bisim1_bisims1.intros dest: bisim1_ThrowD)
next
case bisim1Throw1 thus ?case
by(fastforce intro: rtranclp.rtrancl_into_rtrancl Throw1Throw bisim1_bisims1.intros dest: bisim1_ThrowD elim!: Throw_τred1r_xt)
next
case bisim1Throw2 thus ?case
by(fastforce intro: bisim1_bisims1.intros)
next
case bisim1ThrowNull thus ?case
by(fastforce intro: bisim1_bisims1.intros)
next
case bisim1ThrowThrow thus ?case
by(fastforce intro: bisim1_bisims1.intros)
next
case (bisim1Try e e' xs stk loc pc C V e2)
hence red: "τred1r P t h (e', xs) (Throw a, loc)"
and bisim: "P,e,h ⊢ (Throw a, loc) ↔ (stk, loc, pc, ⌊a⌋)"
by(auto simp add: match_ex_table_append)
from red have Red: "τred1r P t h (try e' catch(C V) e2, xs) (try Throw a catch(C V) e2, loc)" by(rule Try_τred1r_xt)
from ‹match_ex_table (compP f P) (cname_of h a) pc (compxE2 (try e catch(C V) e2) 0 0) = None›
have "¬ matches_ex_entry (compP f P) (cname_of h a) pc (0, length (compE2 e), ⌊C⌋, Suc (length (compE2 e)), 0)"
by(auto simp add: match_ex_table_append split: if_split_asm)
moreover from ‹P,e,h ⊢ (e', xs) ↔ (stk, loc, pc, ⌊a⌋)›
have "pc < length (compE2 e)" by(auto dest: bisim1_xcp_pcD)
ultimately have subcls: "¬ P ⊢ D ≼⇧* C" using ha by(simp add: matches_ex_entry_def cname_of_def)
with ha have "True,P,t ⊢1 ⟨try Throw a catch(C V) e2, (h, loc)⟩ -ε→ ⟨Throw a, (h, loc)⟩"
by -(rule Red1TryFail, auto)
moreover from bisim ha subcls
have "P,try e catch(C V) e2,h ⊢ (Throw a, loc) ↔ (stk, loc, pc, ⌊a⌋)"
by(rule bisim1TryFail)
ultimately show ?case using Red by(blast intro: rtranclp.rtrancl_into_rtrancl τmove1TryThrow)
next
case (bisim1TryCatch2 e2 e' xs stk loc pc e1 C V)
hence *: "τred1r P t h (e', xs) (Throw a, loc) ∧ P,e2,h ⊢ (Throw a, loc) ↔ (stk, loc, pc, ⌊a⌋)"
by(clarsimp simp add: match_ex_table_append matches_ex_entry_def split: if_split_asm)
(auto simp add: match_ex_table_append compxE2_size_convs compxE2_stack_xlift_convs match_ex_table_shift_pc_None elim: meta_impE intro!: exI[where x="Suc V"])
moreover note τred1r_preserves_len[OF *[THEN conjunct1]]
moreover from ‹∃n. n + max_vars {V:Class C=None; e'} ≤ length xs ∧ ℬ (try e1 catch(C V) e2) n›
have "V < length xs" by simp
ultimately show ?case
by(fastforce intro: rtranclp.rtrancl_into_rtrancl Block1Throw τmove1BlockThrow bisim1TryCatchThrow elim!: Block_None_τred1r_xt)
next
case (bisim1TryFail e xs stk loc pc C'' C' V e2)
note bisim = ‹P,e,h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)›
hence "xs = loc" by(auto dest: bisim1_ThrowD)
with bisim ‹typeof_addr h a = ⌊Class_type C''⌋› ‹¬ P ⊢ C'' ≼⇧* C'›
show ?case by(auto intro: bisim1_bisims1.bisim1TryFail)
next
case (bisim1TryCatchThrow e2 xs stk loc pc e C' V)
from ‹P,e2,h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)› have "xs = loc"
by(auto dest: bisim1_ThrowD)
with ‹P,e2,h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)› show ?case
by(auto intro: bisim1_bisims1.bisim1TryCatchThrow)
next
case (bisims1List1 e e' xs stk loc pc es)
hence "τred1r P t h (e', xs) (Throw a, loc)"
and bisim: "P,e,h ⊢ (Throw a, loc) ↔ (stk, loc, pc, ⌊a⌋)" by(auto simp add: match_ex_table_append)
hence "τreds1r P t h (e' # es, xs) (map Val [] @ Throw a # es, loc)" by(auto intro: τred1r_inj_τreds1r)
moreover from bisim
have "P,e#es,h ⊢ (Throw a # es, loc) [↔] (stk, loc, pc, ⌊a⌋)"
by(rule bisim1_bisims1.bisims1List1)
ultimately show ?case by fastforce
next
case (bisims1List2 es es' xs stk loc pc e v)
hence "∃vs es''. τreds1r P t h (es', xs) (map Val vs @ Throw a # es'', loc) ∧ P,es,h ⊢ (map Val vs @ Throw a # es'', loc) [↔] (stk, loc, pc, ⌊a⌋)"
by(auto simp add: match_ex_table_append_not_pcs compxEs2_size_convs compxEs2_stack_xlift_convs match_ex_table_shift_pc_None)
then obtain vs es'' where red: "τreds1r P t h (es', xs) (map Val vs @ Throw a # es'', loc)"
and bisim: "P,es,h ⊢ (map Val vs @ Throw a # es'', loc) [↔] (stk, loc, pc, ⌊a⌋)" by blast
from red have "τreds1r P t h (Val v # es', xs) (map Val (v # vs) @ Throw a # es'', loc)"
by(auto intro: τreds1r_cons_τreds1r)
moreover from bisim
have "P,e # es,h ⊢ (map Val (v # vs) @ Throw a # es'', loc) [↔] (stk @ [v], loc, length (compE2 e) + pc, ⌊a⌋)"
by(auto intro: bisim1_bisims1.bisims1List2)
ultimately show ?case by fastforce
qed
primrec conf_xcp' :: "'m prog ⇒ 'heap ⇒ 'addr option ⇒ bool" where
"conf_xcp' P h None = True"
| "conf_xcp' P h ⌊a⌋ = (∃D. typeof_addr h a = ⌊Class_type D⌋ ∧ P ⊢ D ≼⇧* Throwable)"
lemma conf_xcp_conf_xcp':
"conf_xcp P h xcp i ⟹ conf_xcp' P h xcp"
by(cases xcp) auto
lemma conf_xcp'_compP [simp]: "conf_xcp' (compP f P) = conf_xcp' P"
by(clarsimp simp add: fun_eq_iff conf_xcp'_def rec_option_is_case_option)
end
context J1_heap_base begin
lemmas τred1_Val_simps [simp] =
τred1r_Val τred1t_Val τreds1r_map_Val τreds1t_map_Val
end
context J1_JVM_conf_read begin
lemma assumes wf: "wf_J1_prog P"
and hconf: "hconf h" "preallocated h"
and tconf: "P,h ⊢ t √t"
shows red1_simulates_exec_instr:
"⟦ P, E, h ⊢ (e, xs) ↔ (stk, loc, pc, xcp);
exec_move_d P t E h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp');
n + max_vars e ≤ length xs; bsok E n; P,h ⊢ stk [:≤] ST; conf_xcp' (compP2 P) h xcp ⟧
⟹ ∃e'' xs''. P, E, h' ⊢ (e'', xs'') ↔ (stk', loc', pc', xcp') ∧
(if τmove2 (compP2 P) h stk E pc xcp
then h' = h ∧ (if xcp' = None ⟶ pc < pc' then τred1r else τred1t) P t h (e, xs) (e'', xs'')
else ∃ta' e' xs'. τred1r P t h (e, xs) (e', xs') ∧ True,P,t ⊢1 ⟨e', (h, xs')⟩ -ta'→ ⟨e'', (h', xs'')⟩ ∧ ta_bisim wbisim1 (extTA2J1 P ta') ta ∧ ¬ τmove1 P h e' ∧ (call1 e = None ∨ no_call2 E pc ∨ e' = e ∧ xs' = xs))"
(is "⟦ _; ?exec E stk loc pc xcp stk' loc' pc' xcp'; _; _; _; _ ⟧
⟹ ∃e'' xs''. P, E, h' ⊢ (e'', xs'') ↔ (stk', loc', pc', xcp') ∧ ?red e xs e'' xs'' E stk pc pc' xcp xcp'")
and reds1_simulates_exec_instr:
"⟦ P, Es, h ⊢ (es, xs) [↔] (stk, loc, pc, xcp);
exec_moves_d P t Es h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp');
n + max_varss es ≤ length xs; bsoks Es n; P,h ⊢ stk [:≤] ST; conf_xcp' (compP2 P) h xcp ⟧
⟹ ∃es'' xs''. P, Es, h' ⊢ (es'', xs'') [↔] (stk', loc', pc', xcp') ∧
(if τmoves2 (compP2 P) h stk Es pc xcp
then h' = h ∧ (if xcp' = None ⟶ pc < pc' then τreds1r else τreds1t) P t h (es, xs) (es'', xs'')
else ∃ta' es' xs'. τreds1r P t h (es, xs) (es', xs') ∧ True,P,t ⊢1 ⟨es', (h, xs')⟩ [-ta'→] ⟨es'', (h', xs'')⟩ ∧ ta_bisim wbisim1 (extTA2J1 P ta') ta ∧ ¬ τmoves1 P h es' ∧ (calls1 es = None ∨ no_calls2 Es pc ∨ es' = es ∧ xs' = xs))"
(is "⟦ _; ?execs Es stk loc pc xcp stk' loc' pc' xcp'; _; _; _; _ ⟧
⟹ ∃es'' xs''. P, Es, h' ⊢ (es'', xs'') [↔] (stk', loc', pc', xcp') ∧ ?reds es xs es'' xs'' Es stk pc pc' xcp xcp'")
proof(induction E n e xs stk loc pc xcp and Es n es xs stk loc pc xcp
arbitrary: stk' loc' pc' xcp' ST and stk' loc' pc' xcp' ST rule: bisim1_bisims1_inducts_split)
case (bisim1Val2 e n v xs)
from ‹?exec e [v] xs (length (compE2 e)) None stk' loc' pc' xcp'›
have False by(auto dest: exec_meth_length_compE2D simp add: exec_move_def)
thus ?case ..
next
case (bisim1New C' n xs)
note exec = ‹exec_move_d P t (new C') h ([], xs, 0, None) ta h' (stk', loc', pc', xcp')›
have τ: "¬ τmove2 (compP2 P) h [] (new C') 0 None" "¬ τmove1 P h (new C')" by(auto simp add: τmove2_iff)
show ?case
proof(cases "allocate h (Class_type C') = {}")
case True
have "P,new C',h' ⊢ (THROW OutOfMemory, xs) ↔ ([], xs, 0, ⌊addr_of_sys_xcpt OutOfMemory⌋)"
by(rule bisim1NewThrow)
with exec τ True show ?thesis
by(fastforce intro: Red1NewFail elim!: exec_meth.cases simp add: exec_move_def)
next
case False
have "⋀a h'. P,new C',h' ⊢ (addr a, xs) ↔ ([Addr a], xs, length (compE2 (new C')), None)"
by(rule bisim1Val2) auto
thus ?thesis using exec False τ
apply(simp add: exec_move_def)
apply(erule exec_meth.cases)
apply simp_all
apply clarsimp
apply(auto intro!: Red1New exI simp add: ta_bisim_def)
done
qed
next
case (bisim1NewThrow C' n xs)
from ‹?exec (new C') [] xs 0 ⌊addr_of_sys_xcpt OutOfMemory⌋ stk' loc' pc' xcp'›
have False by(auto elim: exec_meth.cases simp add: exec_move_def)
thus ?case ..
next
case (bisim1NewArray e n e' xs stk loc pc xcp U)
note IH = bisim1NewArray.IH(2)
note exec = ‹?exec (newA U⌊e⌉) stk loc pc xcp stk' loc' pc' xcp'›
note bisim = ‹P,e,h ⊢ (e', xs) ↔ (stk, loc, pc, xcp)›
note len = ‹n + max_vars (newA U⌊e'⌉) ≤ length xs›
note bsok = ‹bsok (newA U⌊e⌉) n›
from bisim have pc: "pc ≤ length (compE2 e)" by(rule bisim1_pc_length_compE2)
show ?case
proof(cases "pc < length (compE2 e)")
case True
with exec have exec': "?exec e stk loc pc xcp stk' loc' pc' xcp'"
by(auto simp add: exec_move_newArray)
from True have "τmove2 (compP2 P) h stk (newA U⌊e⌉) pc xcp = τmove2 (compP2 P) h stk e pc xcp" by(simp add: τmove2_iff)
moreover have "no_call2 e pc ⟹ no_call2 (newA U⌊e⌉) pc" by(simp add: no_call2_def)
ultimately show ?thesis using IH[OF exec' _ _ ‹P,h ⊢ stk [:≤] ST› ‹conf_xcp' (compP2 P) h xcp›] len bsok
by(fastforce intro: bisim1_bisims1.bisim1NewArray New1ArrayRed elim!: NewArray_τred1r_xt NewArray_τred1t_xt)
next
case False
with pc have [simp]: "pc = length (compE2 e)" by simp
with bisim obtain v where stk: "stk = [v]" and xcp: "xcp = None"
by(auto dest: bisim1_pc_length_compE2D)
with bisim pc len bsok have red: "τred1r P t h (e', xs) (Val v, loc)"
by(auto intro: bisim1_Val_τred1r simp add: bsok_def)
hence "τred1r P t h (newA U⌊e'⌉, xs) (newA U⌊Val v⌉, loc)" by(rule NewArray_τred1r_xt)
moreover have τ: "¬ τmove2 (compP2 P) h [v] (newA U⌊e⌉) pc None" by(simp add: τmove2_iff)
moreover have "¬ τmove1 P h (newA U⌊Val v⌉)" by auto
moreover from exec stk xcp obtain I
where [simp]: "v = Intg I" by(auto elim!: exec_meth.cases simp add: exec_move_def)
have "∃ta' e''. P,newA U⌊e⌉,h' ⊢ (e'',loc) ↔ (stk', loc', pc', xcp') ∧ True,P,t ⊢1 ⟨newA U⌊Val v⌉,(h, loc)⟩ -ta'→ ⟨e'',(h', loc)⟩ ∧ ta_bisim wbisim1 (extTA2J1 P ta') ta"
proof(cases "I <s 0")
case True with exec stk xcp show ?thesis
by(fastforce elim!: exec_meth.cases intro: bisim1NewArrayFail Red1NewArrayNegative simp add: exec_move_def)
next
case False
show ?thesis
proof(cases "allocate h (Array_type U (nat (sint I))) = {}")
case True
with False exec stk xcp show ?thesis
by(fastforce elim!: exec_meth.cases intro: bisim1NewArrayFail Red1NewArrayFail simp add: exec_move_def)
next
case False
have "⋀a h'. P,newA U⌊e⌉,h' ⊢ (addr a, loc) ↔ ([Addr a], loc, length (compE2 (newA U⌊e⌉)), None)"
by(rule bisim1Val2) simp
with False ‹¬ I <s 0› exec stk xcp show ?thesis
apply(simp add: exec_move_def)
apply(erule exec_meth.cases)
apply simp_all
apply clarsimp
apply(auto intro!: Red1NewArray exI simp add: ta_bisim_def)
done
qed
qed
moreover have "no_call2 (newA U⌊e⌉) pc" by(simp add: no_call2_def)
ultimately show ?thesis using exec stk xcp by fastforce
qed
next
case (bisim1NewArrayThrow e n a xs stk loc pc U)
note exec = ‹?exec (newA U⌊e⌉) stk loc pc ⌊a⌋ stk' loc' pc' xcp'›
note bisim = ‹P,e,h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)›
from bisim have pc: "pc < length (compE2 e)" by(auto dest: bisim1_ThrowD)
from bisim have "match_ex_table (compP2 P) (cname_of h a) (0 + pc) (compxE2 e 0 0) = None"
unfolding compP2_def by(rule bisim1_xcp_Some_not_caught)
with exec pc have False by (auto elim!: exec_meth.cases simp add: exec_move_def)
thus ?case ..
next
case (bisim1NewArrayFail e n U a xs v)
note exec = ‹?exec (newA U⌊e⌉) [v] xs (length (compE2 e)) ⌊a⌋ stk' loc' pc' xcp'›
hence False by(auto elim!: exec_meth.cases dest: match_ex_table_pc_length_compE2 simp add: exec_move_def)
thus ?case ..
next
case (bisim1Cast e n e' xs stk loc pc xcp U)
note IH = bisim1Cast.IH(2)
note exec = ‹?exec (Cast U e) stk loc pc xcp stk' loc' pc' xcp'›
note bisim = ‹P,e,h ⊢ (e', xs) ↔ (stk, loc, pc, xcp)›
note len = ‹n + max_vars (Cast U e') ≤ length xs›
note ST = ‹P,h ⊢ stk [:≤] ST›
note bsok = ‹bsok (Cast U e) n›
from bisim have pc: "pc ≤ length (compE2 e)" by(rule bisim1_pc_length_compE2)
show ?case
proof(cases "pc < length (compE2 e)")
case True
with exec have exec': "?exec e stk loc pc xcp stk' loc' pc' xcp'" by(auto simp add: exec_move_Cast)
from True have "τmove2 (compP2 P) h stk (Cast U e) pc xcp = τmove2 (compP2 P) h stk e pc xcp" by(simp add: τmove2_iff)
moreover have "no_call2 e pc ⟹ no_call2 (Cast U e) pc" by(simp add: no_call2_def)
ultimately show ?thesis using IH[OF exec' _ _ ST ‹conf_xcp' (compP2 P) h xcp›] len bsok
by(fastforce intro: bisim1_bisims1.bisim1Cast Cast1Red elim!: Cast_τred1r_xt Cast_τred1t_xt)
next
case False
with pc have [simp]: "pc = length (compE2 e)" by simp
with bisim obtain v where stk: "stk = [v]" and xcp: "xcp = None"
by(auto dest: bisim1_pc_length_compE2D)
with bisim pc len bsok have red: "τred1r P t h (e', xs) (Val v, loc)"
by(auto intro: bisim1_Val_τred1r simp add: bsok_def)
hence "τred1r P t h (Cast U e', xs) (Cast U (Val v), loc)" by(rule Cast_τred1r_xt)
also from exec have [simp]: "h' = h" "ta = ε" by(auto simp add: exec_move_def elim!: exec_meth.cases split: if_split_asm)
have "∃e''. P,Cast U e,h ⊢ (e'',loc) ↔ (stk', loc', pc', xcp') ∧ True,P,t ⊢1 ⟨Cast U (Val v),(h, loc)⟩ -ε→ ⟨e'',(h, loc)⟩"
proof(cases "P ⊢ the (typeof⇘h⇙ v) ≤ U")
case False with exec stk xcp bsok ST show ?thesis
by(fastforce simp add: compP2_def exec_move_def exec_meth_instr list_all2_Cons1 conf_def intro: bisim1CastFail Red1CastFail)
next
case True
have "P,Cast U e,h ⊢ (Val v, loc) ↔ ([v], loc, length (compE2 (Cast U e)), None)"
by(rule bisim1Val2) simp
with exec stk xcp ST True show ?thesis
by(fastforce simp add: compP2_def exec_move_def exec_meth_instr list_all2_Cons1 conf_def intro: Red1Cast)
qed
then obtain e'' where bisim': "P,Cast U e,h ⊢ (e'',loc) ↔ (stk', loc', pc', xcp')"
and red: "True,P,t ⊢1 ⟨Cast U (Val v),(h, loc)⟩ -ε→ ⟨e'',(h, loc)⟩" by blast
have "τmove1 P h (Cast U (Val v))" by(rule τmove1CastRed)
with red have "τred1t P t h (Cast U (Val v), loc) (e'', loc)" by(auto intro: τred1t_1step)
also have τ: "τmove2 (compP2 P) h [v] (Cast U e) pc None" by(simp add: τmove2_iff)
moreover have "no_call2 (Cast U e) pc" by(simp add: no_call2_def)
ultimately show ?thesis using exec stk xcp bisim' by fastforce
qed
next
case (bisim1CastThrow e n a xs stk loc pc U)
note exec = ‹?exec (Cast U e) stk loc pc ⌊a⌋ stk' loc' pc' xcp'›
note bisim = ‹P,e,h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)›
from bisim have pc: "pc < length (compE2 e)" by(auto dest: bisim1_ThrowD)
from bisim have "match_ex_table (compP2 P) (cname_of h a) (0 + pc) (compxE2 e 0 0) = None"
unfolding compP2_def by(rule bisim1_xcp_Some_not_caught)
with exec pc have False by (auto elim!: exec_meth.cases simp add: exec_move_def)
thus ?case ..
next
case (bisim1CastFail e n U xs v)
note exec = ‹?exec (Cast U e) [v] xs (length (compE2 e)) ⌊addr_of_sys_xcpt ClassCast⌋ stk' loc' pc' xcp'›
hence False by(auto elim!: exec_meth.cases dest: match_ex_table_pc_length_compE2 simp add: exec_move_def)
thus ?case ..
next
case (bisim1InstanceOf e n e' xs stk loc pc xcp U)
note IH = bisim1InstanceOf.IH(2)
note exec = ‹?exec (e instanceof U) stk loc pc xcp stk' loc' pc' xcp'›
note bisim = ‹P,e,h ⊢ (e', xs) ↔ (stk, loc, pc, xcp)›
note len = ‹n + max_vars (e' instanceof U) ≤ length xs›
note ST = ‹P,h ⊢ stk [:≤] ST›
note bsok = ‹bsok (e instanceof U) n›
from bisim have pc: "pc ≤ length (compE2 e)" by(rule bisim1_pc_length_compE2)
show ?case
proof(cases "pc < length (compE2 e)")
case True
with exec have exec': "?exec e stk loc pc xcp stk' loc' pc' xcp'" by(auto simp add: exec_move_InstanceOf)
from True have "τmove2 (compP2 P) h stk (e instanceof U) pc xcp = τmove2 (compP2 P) h stk e pc xcp"
by(simp add: τmove2_iff)
moreover have "no_call2 e pc ⟹ no_call2 (e instanceof U) pc" by(simp add: no_call2_def)
ultimately show ?thesis using IH[OF exec' _ _ ST ‹conf_xcp' (compP2 P) h xcp›] len bsok
by(fastforce intro: bisim1_bisims1.bisim1InstanceOf InstanceOf1Red elim!: InstanceOf_τred1r_xt InstanceOf_τred1t_xt)
next
case False
with pc have [simp]: "pc = length (compE2 e)" by simp
with bisim obtain v where stk: "stk = [v]" and xcp: "xcp = None"
by(auto dest: bisim1_pc_length_compE2D)
with bisim pc len bsok have red: "τred1r P t h (e', xs) (Val v, loc)"
by(auto intro: bisim1_Val_τred1r simp add: bsok_def)
hence "τred1r P t h (e' instanceof U, xs) ((Val v) instanceof U, loc)" by(rule InstanceOf_τred1r_xt)
also let ?v = "Bool (v ≠ Null ∧ P ⊢ the (typeof⇘h⇙ v) ≤ U)"
from exec ST stk xcp have [simp]: "h' = h" "ta = ε" "xcp' = None" "loc' = loc" "stk' = [?v]" "pc' = Suc pc"
by(auto simp add: exec_move_def list_all2_Cons1 conf_def compP2_def elim!: exec_meth.cases split: if_split_asm)
have bisim': "P,e instanceof U,h ⊢ (Val ?v, loc) ↔ ([?v], loc, length (compE2 (e instanceof U)), None)"
by(rule bisim1Val2) simp
from exec stk xcp ST
have red: "True,P,t ⊢1 ⟨(Val v) instanceof U,(h, loc)⟩ -ε→ ⟨Val ?v ,(h, loc)⟩"
by(auto simp add: compP2_def exec_move_def exec_meth_instr list_all2_Cons1 conf_def intro: Red1InstanceOf)
have "τmove1 P h ((Val v) instanceof U)" by(rule τmove1InstanceOfRed)
with red have "τred1t P t h ((Val v) instanceof U, loc) (Val ?v, loc)" by(auto intro: τred1t_1step)
also have τ: "τmove2 (compP2 P) h [v] (e instanceof U) pc None" by(simp add: τmove2_iff)
moreover have "no_call2 (e instanceof U) pc" by(simp add: no_call2_def)
ultimately show ?thesis using exec stk xcp bisim' by(fastforce)
qed
next
case (bisim1InstanceOfThrow e n a xs stk loc pc U)
note exec = ‹?exec (e instanceof U) stk loc pc ⌊a⌋ stk' loc' pc' xcp'›
note bisim = ‹P,e,h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)›
from bisim have pc: "pc < length (compE2 e)" by(auto dest: bisim1_ThrowD)
from bisim have "match_ex_table (compP2 P) (cname_of h a) (0 + pc) (compxE2 e 0 0) = None"
unfolding compP2_def by(rule bisim1_xcp_Some_not_caught)
with exec pc have False by (auto elim!: exec_meth.cases simp add: exec_move_def)
thus ?case ..
next
case (bisim1Val v n xs)
from ‹?exec (Val v) [] xs 0 None stk' loc' pc' xcp'›
have "stk' = [v]" "loc' = xs" "h' = h" "pc' = length (compE2 (Val v))" "xcp' = None"
by(auto elim: exec_meth.cases simp add: exec_move_def)
moreover have "P,Val v,h ⊢ (Val v, xs) ↔ ([v], xs, length (compE2 (Val v)), None)"
by(rule bisim1Val2) simp
moreover have "τmove2 (compP2 P) h [] (Val v) 0 None" by(rule τmove2Val)
ultimately show ?case by(auto)
next
case (bisim1Var V n xs)
note exec = ‹?exec (Var V) [] xs 0 None stk' loc' pc' xcp'›
moreover note len = ‹n + max_vars (Var V) ≤ length xs›
moreover have "τmove2 (compP2 P) h [] (Var V) 0 None" "τmove1 P h (Var V)"
by(auto intro: τmove1Var simp add: τmove2_iff)
moreover have "P,Var V,h ⊢ (Val (xs ! V), xs) ↔ ([xs ! V], xs, length (compE2 (Var V)), None)"
by(rule bisim1Val2) simp
ultimately show ?case by(fastforce elim!: exec_meth.cases intro: Red1Var r_into_rtranclp simp add: exec_move_def)
next
case (bisim1BinOp1 e1 n e1' xs stk loc pc xcp e2 bop)
note IH1 = bisim1BinOp1.IH(2)
note IH2 = bisim1BinOp1.IH(4)
note exec = ‹?exec (e1 «bop» e2) stk loc pc xcp stk' loc' pc' xcp'›
note bisim1 = ‹P,e1,h ⊢ (e1', xs) ↔ (stk, loc, pc, xcp)›
note bisim2 = ‹P,e2,h ⊢ (e2, loc) ↔ ([], loc, 0, None)›
note len = ‹n + max_vars (e1' «bop» e2) ≤ length xs›
note ST = ‹P,h ⊢ stk [:≤] ST›
note bsok = ‹bsok (e1 «bop» e2) n›
from bisim1 have pc: "pc ≤ length (compE2 e1)" by(rule bisim1_pc_length_compE2)
show ?case
proof(cases "pc < length (compE2 e1)")
case True
with exec have exec': "?exec e1 stk loc pc xcp stk' loc' pc' xcp'" by(auto simp add: exec_move_BinOp1)
from True have τ: "τmove2 (compP2 P) h stk (e1 «bop» e2) pc xcp = τmove2 (compP2 P) h stk e1 pc xcp"
by(simp add: τmove2_iff)
with IH1[OF exec' _ _ ST ‹conf_xcp' (compP2 P) h xcp›] bisim2 len bsok obtain e'' xs''
where bisim': "P,e1,h' ⊢ (e'', xs'') ↔ (stk', loc', pc', xcp')"
and red: "?red e1' xs e'' xs'' e1 stk pc pc' xcp xcp'" by auto
from bisim' have "P,e1 «bop» e2,h' ⊢ (e'' «bop» e2, xs'') ↔ (stk', loc', pc', xcp')"
by(rule bisim1_bisims1.bisim1BinOp1)
moreover from True have "no_call2 (e1 «bop» e2) pc = no_call2 e1 pc" by(simp add: no_call2_def)
ultimately show ?thesis using red τ
by(fastforce intro: Bin1OpRed1 elim!: BinOp_τred1r_xt1 BinOp_τred1t_xt1)
next
case False
with pc have pc: "pc = length (compE2 e1)" by auto
with bisim1 obtain v where e1': "is_val e1' ⟶ e1' = Val v"
and stk: "stk = [v]" and xcp: "xcp = None" and call: "call1 e1' = None"
by(auto dest: bisim1_pc_length_compE2D)
with bisim1 pc len bsok have rede1': "τred1r P t h (e1', xs) (Val v, loc)"
by(auto intro: bisim1_Val_τred1r simp add: bsok_def)
hence rede1'': "τred1r P t h (e1' «bop» e2, xs) (Val v «bop» e2, loc)" by(rule BinOp_τred1r_xt1)
moreover from pc exec stk xcp
have "exec_meth_d (compP2 P) (compE2 (e1 «bop» e2)) (compxE2 (e1 «bop» e2) 0 0) t h ([] @ [v], loc, length (compE2 e1) + 0, None) ta h' (stk', loc', pc', xcp')"
by(simp add: compxE2_size_convs compxE2_stack_xlift_convs exec_move_def)
hence exec': "exec_meth_d (compP2 P) (compE2 e2) (stack_xlift (length [v]) (compxE2 e2 0 0)) t h ([] @ [v], loc, 0, None) ta h' (stk', loc', pc' - length (compE2 e1), xcp')"
and pc': "pc' ≥ length (compE2 e1)" by(safe dest!: BinOp_exec2D)simp_all
then obtain PC' where PC': "pc' = length (compE2 e1) + PC'"
by -(rule that[where PC'35="pc' - length (compE2 e1)"], simp)
from exec' bisim2 obtain stk'' where stk': "stk' = stk'' @ [v]"
and exec'': "exec_move_d P t e2 h ([], loc, 0, None) ta h' (stk'', loc', pc' - length (compE2 e1), xcp')"
by(unfold exec_move_def)(drule (1) exec_meth_stk_split, auto)
with pc xcp have τ: "τmove2 (compP2 P) h [v] (e1 «bop» e2) (length (compE2 e1)) None = τmove2 (compP2 P) h [] e2 0 None"
using τinstr_stk_drop_exec_move[where stk="[]" and vs = "[v]"]
by(simp add: τmove2_iff τinstr_stk_drop_exec_move)
from bisim1 have "length xs = length loc" by(rule bisim1_length_xs)
with IH2[OF exec'', of "[]"] len bsok obtain e'' xs''
where bisim': "P,e2,h' ⊢ (e'', xs'') ↔ (stk'', loc', pc' - length (compE2 e1), xcp')"
and red: "?red e2 loc e'' xs'' e2 [] 0 (pc' - length (compE2 e1)) None xcp'" by auto
from bisim'
have "P,e1 «bop» e2,h' ⊢ (Val v «bop» e'', xs'') ↔ (stk'' @ [v], loc', length (compE2 e1) + (pc' - length (compE2 e1)), xcp')"
by(rule bisim1_bisims1.bisim1BinOp2)
moreover from red τ
have "?red (Val v «bop» e2) loc (Val v «bop» e'') xs'' (e1 «bop» e2) [v] (length (compE2 e1)) pc' None xcp'"
by(fastforce intro: Bin1OpRed2 elim!: BinOp_τred1r_xt2 BinOp_τred1t_xt2 simp add: no_call2_def)
moreover have "no_call2 (e1 «bop» e2) (length (compE2 e1))" by(simp add: no_call2_def)
ultimately show ?thesis using τ stk' pc xcp pc' PC' bisim1 bisim2 e1' stk call by(fastforce elim!: rtranclp_trans)
qed
next
case (bisim1BinOp2 e2 n e2' xs stk loc pc xcp e1 bop v1)
note IH2 = bisim1BinOp2.IH(2)
note exec = ‹?exec (e1 «bop» e2) (stk @ [v1]) loc (length (compE2 e1) + pc) xcp stk' loc' pc' xcp'›
note bisim1 = ‹P,e1,h ⊢ (e1, xs) ↔ ([], xs, 0, None)›
note bisim2 = ‹P,e2,h ⊢ (e2', xs) ↔ (stk, loc, pc, xcp)›
note len = ‹n + max_vars (Val v1 «bop» e2') ≤ length xs›
note bsok = ‹bsok (e1 «bop» e2) n›
note ST = ‹P,h ⊢ stk @ [v1] [:≤] ST›
then obtain ST2 T where "ST = ST2 @ [T]" "P,h ⊢ stk [:≤] ST2" "P,h ⊢ v1 :≤ T"
by(auto simp add: list_all2_append1 length_Suc_conv)
from bisim2 have pc: "pc ≤ length (compE2 e2)" by(rule bisim1_pc_length_compE2)
show ?case
proof(cases "pc < length (compE2 e2)")
case True
with exec have exec': "exec_meth_d (compP2 P) (compE2 e2) (stack_xlift (length [v1]) (compxE2 e2 0 0)) t h (stk @ [v1], loc, pc, xcp) ta h' (stk', loc', pc' - length (compE2 e1), xcp')"
and pc': "pc' ≥ length (compE2 e1)"
by(unfold exec_move_def)(safe dest!: BinOp_exec2D)
from exec' bisim2 obtain stk'' where stk': "stk' = stk'' @ [v1]"
and exec'': "exec_move_d P t e2 h (stk, loc, pc, xcp) ta h' (stk'', loc', pc' - length (compE2 e1), xcp')"
by -(drule (1) exec_meth_stk_split, auto simp add: exec_move_def)
with True have τ: "τmove2 (compP2 P) h (stk @ [v1]) (e1 «bop» e2) (length (compE2 e1) + pc) xcp = τmove2 (compP2 P) h stk e2 pc xcp"
by(auto simp add: τmove2_iff τinstr_stk_drop_exec_move)
from IH2[OF exec'' _ _ ‹P,h ⊢ stk [:≤] ST2› ‹conf_xcp' (compP2 P) h xcp›] len bsok obtain e'' xs''
where bisim': "P,e2,h' ⊢ (e'', xs'') ↔ (stk'', loc', pc' - length (compE2 e1), xcp')"
and red: "?red e2' xs e'' xs'' e2 stk pc (pc' - length (compE2 e1)) xcp xcp'" by auto
from bisim' have "P,e1 «bop» e2,h' ⊢ (Val v1 «bop» e'', xs'') ↔ (stk'' @ [v1], loc', length (compE2 e1) + (pc' - length (compE2 e1)), xcp')"
by(rule bisim1_bisims1.bisim1BinOp2)
with red τ stk' pc' True show ?thesis
by(fastforce intro: Bin1OpRed2 elim!: BinOp_τred1r_xt2 BinOp_τred1t_xt2 split: if_split_asm simp add: no_call2_def)
next
case False
with pc have [simp]: "pc = length (compE2 e2)" by simp
with bisim2 obtain v2 where e2': "is_val e2' ⟶ e2' = Val v2"
and stk: "stk = [v2]" and xcp: "xcp = None" and call: "call1 e2' = None"
by(auto dest: bisim1_pc_length_compE2D)
with bisim2 pc len bsok have red: "τred1r P t h (e2', xs) (Val v2, loc)"
by(auto intro: bisim1_Val_τred1r simp add: bsok_def)
hence red1: "τred1r P t h (Val v1 «bop» e2', xs) (Val v1 «bop» Val v2, loc)" by(rule BinOp_τred1r_xt2)
show ?thesis
proof(cases "the (binop bop v1 v2)")
case (Inl v)
note red1
also from exec xcp ST stk Inl
have "τred1r P t h (Val v1 «bop» Val v2, loc) (Val v, loc)"
by(force simp add: exec_move_def exec_meth_instr list_all2_Cons1 conf_def compP2_def dest: binop_progress intro: r_into_rtranclp Red1BinOp τmove1BinOp)
also have τ: "τmove2 (compP2 P) h [v2, v1] (e1 «bop» e2) (length (compE2 e1) + length (compE2 e2)) None"
by(simp add: τmove2_iff)
moreover have "P,e1 «bop» e2,h ⊢ (Val v, loc) ↔ ([v], loc, length (compE2 (e1 «bop» e2)), None)"
by(rule bisim1Val2) simp
ultimately show ?thesis using exec xcp stk call Inl by(auto simp add: exec_move_def exec_meth_instr)
next
case (Inr a)
note red1
also from exec xcp ST stk Inr
have "τred1r P t h (Val v1 «bop» Val v2, loc) (Throw a, loc)"
by(force simp add: exec_move_def exec_meth_instr list_all2_Cons1 conf_def compP2_def dest: binop_progress intro: r_into_rtranclp Red1BinOpFail τmove1BinOp)
also have τ: "τmove2 (compP2 P) h [v2, v1] (e1 «bop» e2) (length (compE2 e1) + length (compE2 e2)) None"
by(simp add: τmove2_iff)
moreover
have "P,e1 «bop» e2,h ⊢ (Throw a, loc) ↔ ([v2, v1], loc, length (compE2 e1) + length (compE2 e2), ⌊a⌋)"
by(rule bisim1BinOpThrow)
ultimately show ?thesis using exec xcp stk call Inr by(auto simp add: exec_move_def exec_meth_instr)
qed
qed
next
case (bisim1BinOpThrow1 e1 n a xs stk loc pc e2 bop)
note exec = ‹?exec (e1 «bop» e2) stk loc pc ⌊a⌋ stk' loc' pc' xcp'›
note bisim1 = ‹P,e1,h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)›
from bisim1 have pc: "pc < length (compE2 e1)" by(auto dest: bisim1_ThrowD)
from bisim1 have "match_ex_table (compP2 P) (cname_of h a) (0 + pc) (compxE2 e1 0 0) = None"
unfolding compP2_def by(rule bisim1_xcp_Some_not_caught)
with exec pc have False by(auto elim!: exec_meth.cases simp add: match_ex_table_not_pcs_None exec_move_def)
thus ?case ..
next
case (bisim1BinOpThrow2 e2 n a xs stk loc pc e1 bop v1)
note exec = ‹?exec (e1 «bop» e2) (stk @ [v1]) loc (length (compE2 e1) + pc) ⌊a⌋ stk' loc' pc' xcp'›
note bisim2 = ‹P,e2,h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)›
hence "match_ex_table (compP2 P) (cname_of h a) (length (compE2 e1) + pc) (compxE2 e2 (length (compE2 e1)) 0) = None"
unfolding compP2_def by(rule bisim1_xcp_Some_not_caught)
with exec have False
apply(auto elim!: exec_meth.cases simp add: match_ex_table_append_not_pcs exec_move_def)
apply(auto simp only: compxE2_size_convs compxE2_stack_xlift_convs match_ex_table_stack_xlift_eq_Some_conv)
done
thus ?case ..
next
case (bisim1BinOpThrow e1 n e2 bop a xs v1 v2)
note ‹?exec (e1 «bop» e2) [v1, v2] xs (length (compE2 e1) + length (compE2 e2)) ⌊a⌋ stk' loc' pc' xcp'›
hence False
by(auto elim!: exec_meth.cases simp add: match_ex_table_append_not_pcs compxE2_size_convs exec_move_def
dest!: match_ex_table_shift_pcD match_ex_table_pc_length_compE2)
thus ?case ..
next
case (bisim1LAss1 e n e' xs stk loc pc xcp V)
note IH = bisim1LAss1.IH(2)
note exec = ‹?exec (V := e) stk loc pc xcp stk' loc' pc' xcp'›
note bisim = ‹P,e,h ⊢ (e', xs) ↔ (stk, loc, pc, xcp)›
note len = ‹n + max_vars (V := e') ≤ length xs›
note bsok = ‹bsok (V:=e) n›
from bisim have pc: "pc ≤ length (compE2 e)" by(rule bisim1_pc_length_compE2)
show ?case
proof(cases "pc < length (compE2 e)")
case True
with exec have exec': "?exec e stk loc pc xcp stk' loc' pc' xcp'" by(auto simp add: exec_move_LAss)
from True have "τmove2 (compP2 P) h stk (V := e) pc xcp = τmove2 (compP2 P) h stk e pc xcp" by(simp add: τmove2_iff)
with IH[OF exec' _ _ ‹P,h ⊢ stk [:≤] ST› ‹conf_xcp' (compP2 P) h xcp›] len bsok show ?thesis
by(fastforce intro: bisim1_bisims1.bisim1LAss1 LAss1Red elim!: LAss_τred1r LAss_τred1t simp add: no_call2_def)
next
case False
with pc have [simp]: "pc = length (compE2 e)" by simp
with bisim obtain v where stk: "stk = [v]" and xcp: "xcp = None"
by(auto dest: bisim1_pc_length_compE2D)
with bisim pc len bsok have red: "τred1r P t h (e', xs) (Val v, loc)"
by(auto intro: bisim1_Val_τred1r simp add: bsok_def)
hence "τred1r P t h (V := e', xs) (V := Val v, loc)" by(rule LAss_τred1r)
also have "τmove1 P h (V := Val v)" by(rule τmove1LAssRed)
with exec stk xcp have "τred1r P t h (V := Val v, loc) (unit, loc[V := v])"
by(auto intro!: r_into_rtranclp Red1LAss simp add: exec_move_def elim!: exec_meth.cases)
also have τ: "τmove2 (compP2 P) h [v] (V := e) pc None" by(simp add: τmove2_iff)
moreover have "P,(V := e),h ⊢ (unit, loc[V := v]) ↔ ([], loc[V := v], Suc (length (compE2 e)), None)"
by(rule bisim1LAss2)
ultimately show ?thesis using exec stk xcp
by(fastforce elim!: exec_meth.cases simp add: exec_move_def)
qed
next
case (bisim1LAss2 e n V xs)
note bisim = ‹P,e,h ⊢ (e, xs) ↔ ([], xs, 0, None)›
note exec = ‹?exec (V := e) [] xs (Suc (length (compE2 e))) None stk' loc' pc' xcp'›
hence "stk' = [Unit]" "loc' = xs" "pc' = length (compE2 (V := e))" "xcp' = None" "h' = h"
by(auto elim!: exec_meth.cases simp add: exec_move_def)
moreover have "τmove2 (compP2 P) h [] (V := e) (Suc (length (compE2 e))) None" by(simp add: τmove2_iff)
moreover have "P,V:=e,h' ⊢ (unit, xs) ↔ ([Unit], xs, length (compE2 (V := e)), None)"
by(rule bisim1Val2) simp
ultimately show ?case by(auto)
next
case (bisim1LAssThrow e n a xs stk loc pc V)
note exec = ‹?exec (V := e) stk loc pc ⌊a⌋ stk' loc' pc' xcp'›
note bisim = ‹P,e,h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)›
from bisim have pc: "pc < length (compE2 e)" by(auto dest: bisim1_ThrowD)
from bisim have "match_ex_table (compP2 P) (cname_of h a) (0 + pc) (compxE2 e 0 0) = None"
unfolding compP2_def by(rule bisim1_xcp_Some_not_caught)
with exec pc have False by (auto elim!: exec_meth.cases simp add: exec_move_def)
thus ?case ..
next
case (bisim1AAcc1 a n a' xs stk loc pc xcp i)
note IH1 = bisim1AAcc1.IH(2)
note IH2 = bisim1AAcc1.IH(4)
note exec = ‹?exec (a⌊i⌉) stk loc pc xcp stk' loc' pc' xcp'›
note bisim1 = ‹P,a,h ⊢ (a', xs) ↔ (stk, loc, pc, xcp)›
note bisim2 = ‹P,i,h ⊢ (i, loc) ↔ ([], loc, 0, None)›
note len = ‹n + max_vars (a'⌊i⌉) ≤ length xs›
note bsok = ‹bsok (a⌊i⌉) n›
from bisim1 have pc: "pc ≤ length (compE2 a)" by(rule bisim1_pc_length_compE2)
show ?case
proof(cases "pc < length (compE2 a)")
case True
with exec have exec': "?exec a stk loc pc xcp stk' loc' pc' xcp'" by(auto simp add: exec_move_AAcc1)
from True have τ: "τmove2 (compP2 P) h stk (a⌊i⌉) pc xcp = τmove2 (compP2 P) h stk a pc xcp" by(auto intro: τmove2AAcc1)
with IH1[OF exec' _ _ ‹P,h ⊢ stk [:≤] ST› ‹conf_xcp' (compP2 P) h xcp›] len bsok obtain e'' xs''
where bisim': "P,a,h' ⊢ (e'', xs'') ↔ (stk', loc', pc', xcp')"
and red: "?red a' xs e'' xs'' a stk pc pc' xcp xcp'" by auto
from bisim' have "P,a⌊i⌉,h' ⊢ (e''⌊i⌉, xs'') ↔ (stk', loc', pc', xcp')" by(rule bisim1_bisims1.bisim1AAcc1)
moreover from True have "no_call2 (a⌊i⌉) pc = no_call2 a pc" by(simp add: no_call2_def)
ultimately show ?thesis using red τ by(fastforce intro: AAcc1Red1 elim!: AAcc_τred1r_xt1 AAcc_τred1t_xt1)
next
case False
with pc have pc: "pc = length (compE2 a)" by auto
with bisim1 obtain v where a': "is_val a' ⟶ a' = Val v"
and stk: "stk = [v]" and xcp: "xcp = None" and call: "call1 a' = None"
by(auto dest: bisim1_pc_length_compE2D)
with bisim1 pc len bsok have rede1': "τred1r P t h (a', xs) (Val v, loc)"
by(auto intro: bisim1_Val_τred1r simp add: bsok_def)
hence "τred1r P t h (a'⌊i⌉, xs) (Val v⌊i⌉, loc)" by(rule AAcc_τred1r_xt1)
moreover from pc exec stk xcp
have exec': "exec_meth_d (compP2 P) (compE2 a @ compE2 i @ [ALoad]) (compxE2 a 0 0 @ shift (length (compE2 a)) (stack_xlift (length [v]) (compxE2 i 0 0))) t h ([] @ [v], loc, length (compE2 a) + 0, None) ta h' (stk', loc', pc', xcp')"
by(simp add: compxE2_size_convs compxE2_stack_xlift_convs exec_move_def)
hence "exec_meth_d (compP2 P) (compE2 i @ [ALoad]) (stack_xlift (length [v]) (compxE2 i 0 0)) t h ([] @ [v], loc, 0, None) ta h' (stk', loc', pc' - length (compE2 a), xcp')"
by(rule exec_meth_drop_xt) auto
hence "exec_meth_d (compP2 P) (compE2 i) (stack_xlift (length [v]) (compxE2 i 0 0)) t h ([] @ [v], loc, 0, None) ta h' (stk', loc', pc' - length (compE2 a), xcp')"
by(rule exec_meth_take) simp
with bisim2 obtain stk'' where stk': "stk' = stk'' @ [v]"
and exec'': "exec_move_d P t i h ([], loc, 0, None) ta h' (stk'', loc', pc' - length (compE2 a), xcp')"
unfolding exec_move_def by(blast dest: exec_meth_stk_split)
with pc xcp have τ: "τmove2 (compP2 P) h ([] @ [v]) (a⌊i⌉) (length (compE2 a)) None = τmove2 (compP2 P) h [] i 0 None"
using τinstr_stk_drop_exec_move[where stk="[]" and vs="[v]"]
by(auto simp add: τmove2_iff τinstr_stk_drop_exec_move)
from bisim1 have "length xs = length loc" by(rule bisim1_length_xs)
with IH2[OF exec''] len bsok obtain e'' xs''
where bisim': "P,i,h' ⊢ (e'', xs'') ↔ (stk'', loc', pc' - length (compE2 a), xcp')"
and red: "?red i loc e'' xs'' i [] 0 (pc' - length (compE2 a)) None xcp'" by(fastforce)
from bisim'
have "P,a⌊i⌉,h' ⊢ (Val v⌊e''⌉, xs'') ↔ (stk'' @ [v], loc', length (compE2 a) + (pc' - length (compE2 a)), xcp')"
by(rule bisim1_bisims1.bisim1AAcc2)
moreover from red τ have "?red (Val v⌊i⌉) loc (Val v⌊e''⌉) xs'' (a⌊i⌉) [v] (length (compE2 a)) pc' None xcp'"
by(fastforce intro: AAcc1Red2 elim!: AAcc_τred1r_xt2 AAcc_τred1t_xt2 split: if_split_asm simp add: no_call2_def)
moreover from exec' have "pc' ≥ length (compE2 a)"
by(rule exec_meth_drop_xt_pc) auto
moreover have "no_call2 (a⌊i⌉) pc" using pc by(simp add: no_call2_def)
ultimately show ?thesis using τ stk' pc xcp stk call
by(fastforce elim!: rtranclp_trans)+
qed
next
case (bisim1AAcc2 i n i' xs stk loc pc xcp a v)
note IH2 = bisim1AAcc2.IH(2)
note exec = ‹?exec (a⌊i⌉) (stk @ [v]) loc (length (compE2 a) + pc) xcp stk' loc' pc' xcp'›
note bisim2 = ‹P,i,h ⊢ (i', xs) ↔ (stk, loc, pc, xcp)›
note len = ‹n + max_vars (Val v⌊i'⌉) ≤ length xs›
note bsok = ‹bsok (a⌊i⌉) n›
from bisim2 have pc: "pc ≤ length (compE2 i)" by(rule bisim1_pc_length_compE2)
show ?case
proof(cases "pc < length (compE2 i)")
case True
from exec have exec': "exec_meth_d (compP2 P) (compE2 a @ compE2 i @ [ALoad]) (compxE2 a 0 0 @ shift (length (compE2 a)) (stack_xlift (length [v]) (compxE2 i 0 0))) t h (stk @ [v], loc, length (compE2 a) + pc, xcp) ta h' (stk', loc', pc', xcp')"
by(simp add: shift_compxE2 stack_xlift_compxE2 exec_move_def)
hence "exec_meth_d (compP2 P) (compE2 i @ [ALoad]) (stack_xlift (length [v]) (compxE2 i 0 0)) t h (stk @ [v], loc, pc, xcp) ta h' (stk', loc', pc' - length (compE2 a), xcp')"
by(rule exec_meth_drop_xt) auto
hence "exec_meth_d (compP2 P) (compE2 i) (stack_xlift (length [v]) (compxE2 i 0 0)) t h (stk @ [v], loc, pc, xcp) ta h' (stk', loc', pc' - length (compE2 a), xcp')"
using True by(rule exec_meth_take)
with bisim2 obtain stk'' where stk': "stk' = stk'' @ [v]"
and exec'': "exec_move_d P t i h (stk, loc, pc, xcp) ta h' (stk'', loc', pc' - length (compE2 a), xcp')"
unfolding exec_move_def by(blast dest: exec_meth_stk_split)
with True have τ: "τmove2 (compP2 P) h (stk @ [v]) (a⌊i⌉) (length (compE2 a) + pc) xcp = τmove2 (compP2 P) h stk i pc xcp"
by(auto simp add: τmove2_iff τinstr_stk_drop_exec_move)
moreover from ‹P,h ⊢ stk @ [v] [:≤] ST› obtain ST2
where "P,h ⊢ stk [:≤] ST2" by(auto simp add: list_all2_append1)
from IH2[OF exec'' _ _ this ‹conf_xcp' (compP2 P) h xcp›] len bsok obtain e'' xs''
where bisim': "P,i,h' ⊢ (e'', xs'') ↔ (stk'', loc', pc' - length (compE2 a), xcp')"
and red: "?red i' xs e'' xs'' i stk pc (pc' - length (compE2 a)) xcp xcp'" by auto
from bisim' have "P,a⌊i⌉,h' ⊢ (Val v⌊e''⌉, xs'') ↔ (stk'' @ [v], loc', length (compE2 a) + (pc' - length (compE2 a)), xcp')"
by(rule bisim1_bisims1.bisim1AAcc2)
moreover from exec' have "pc' ≥ length (compE2 a)"
by(rule exec_meth_drop_xt_pc) auto
moreover have "no_call2 i pc ⟹ no_call2 (a⌊i⌉) (length (compE2 a) + pc)"
by(simp add: no_call2_def)
ultimately show ?thesis using red τ stk' True
by(fastforce intro: AAcc1Red2 elim!: AAcc_τred1r_xt2 AAcc_τred1t_xt2 split: if_split_asm)
next
case False
with pc have [simp]: "pc = length (compE2 i)" by simp
with bisim2 obtain v2 where i': "is_val i' ⟶ i' = Val v2"
and stk: "stk = [v2]" and xcp: "xcp = None" and call: "call1 i' = None"
by(auto dest: bisim1_pc_length_compE2D)
with bisim2 pc len bsok have red: "τred1r P t h (i', xs) (Val v2, loc)"
by(auto intro: bisim1_Val_τred1r simp add: bsok_def)
hence "τred1r P t h (Val v⌊i'⌉, xs) (Val v⌊Val v2⌉, loc)" by(rule AAcc_τred1r_xt2)
moreover have τ: "¬ τmove2 (compP2 P) h [v2, v] (a⌊i⌉) (length (compE2 a) + length (compE2 i)) None"
by(simp add: τmove2_iff)
moreover
have "∃ta' e''. P,a⌊i⌉,h' ⊢ (e'',loc) ↔ (stk', loc', pc', xcp') ∧ True,P,t ⊢1 ⟨Val v⌊Val v2⌉, (h, loc)⟩ -ta'→ ⟨e'',(h', loc)⟩ ∧ ta_bisim wbisim1 (extTA2J1 P ta') ta"
proof(cases "v = Null")
case True with exec stk xcp show ?thesis
by(fastforce elim!: exec_meth.cases simp add: exec_move_def intro: bisim1AAccFail Red1AAccNull)
next
case False
with exec xcp stk obtain U el A len I where [simp]: "v = Addr A" and hA: "typeof_addr h A = ⌊Array_type U len⌋"
and [simp]: "v2 = Intg I" by(auto simp add: exec_move_def exec_meth_instr is_Ref_def conf_def split: if_split_asm)
show ?thesis
proof(cases "0 <=s I ∧ sint I < int len")
case True
hence "¬ I <s 0" by auto
moreover
with exec xcp stk True hA obtain v3 where "stk' = [v3]" "heap_read h A (ACell (nat (sint I))) v3"
by(auto simp add: exec_move_def exec_meth_instr is_Ref_def)
moreover
have "P,a⌊i⌉,h' ⊢ (Val v3,loc) ↔ ([v3], loc, length (compE2 (a⌊i⌉)), None)"
by(rule bisim1Val2) simp
ultimately show ?thesis using exec stk xcp True hA
by(fastforce elim!: exec_meth.cases intro: Red1AAcc simp add: exec_move_def ta_upd_simps ta_bisim_def split: if_split_asm)
next
case False
with exec stk xcp hA show ?thesis
by(fastforce elim!: exec_meth.cases simp add: is_Ref_def exec_move_def intro: bisim1AAccFail Red1AAccBounds split: if_split_asm)
qed
qed
ultimately show ?thesis using exec xcp stk call by fastforce
qed
next
case (bisim1AAccThrow1 A n a xs stk loc pc i)
note exec = ‹?exec (A⌊i⌉) stk loc pc ⌊a⌋ stk' loc' pc' xcp'›
note bisim1 = ‹P,A,h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)›
from bisim1 have pc: "pc < length (compE2 A)" by(auto dest: bisim1_ThrowD)
from bisim1 have "match_ex_table (compP2 P) (cname_of h a) (0 + pc) (compxE2 A 0 0) = None"
unfolding compP2_def by(rule bisim1_xcp_Some_not_caught)
with exec pc have False
by(auto elim!: exec_meth.cases simp add: match_ex_table_not_pcs_None exec_move_def)
thus ?case ..
next
case (bisim1AAccThrow2 i n a xs stk loc pc A v)
note exec = ‹?exec (A⌊i⌉) (stk @ [v]) loc (length (compE2 A) + pc) ⌊a⌋ stk' loc' pc' xcp'›
note bisim2 = ‹P,i,h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)›
hence "match_ex_table (compP2 P) (cname_of h a) (length (compE2 A) + pc) (compxE2 i (length (compE2 A)) 0) = None"
unfolding compP2_def by(rule bisim1_xcp_Some_not_caught)
with exec have False
apply(auto elim!: exec_meth.cases simp add: match_ex_table_append_not_pcs exec_move_def)
apply(auto simp only: compxE2_size_convs compxE2_stack_xlift_convs match_ex_table_stack_xlift_eq_Some_conv)
done
thus ?case ..
next
case (bisim1AAccFail a n i ad xs v v')
note ‹?exec (a⌊i⌉) [v, v'] xs (length (compE2 a) + length (compE2 i)) ⌊ad⌋ stk' loc' pc' xcp'›
hence False
by(auto elim!: exec_meth.cases simp add: match_ex_table_append_not_pcs compxE2_size_convs exec_move_def
dest!: match_ex_table_shift_pcD match_ex_table_pc_length_compE2)
thus ?case ..
next
case (bisim1AAss1 a n a' xs stk loc pc xcp i e)
note IH1 = bisim1AAss1.IH(2)
note IH2 = bisim1AAss1.IH(4)
note exec = ‹?exec (a⌊i⌉ := e) stk loc pc xcp stk' loc' pc' xcp'›
note bisim1 = ‹P,a,h ⊢ (a', xs) ↔ (stk, loc, pc, xcp)›
note bisim2 = ‹P,i,h ⊢ (i, loc) ↔ ([], loc, 0, None)›
note len = ‹n + max_vars (a'⌊i⌉ := e) ≤ length xs›
note bsok = ‹bsok (a⌊i⌉ := e) n›
from bisim1 have pc: "pc ≤ length (compE2 a)" by(rule bisim1_pc_length_compE2)
show ?case
proof(cases "pc < length (compE2 a)")
case True
with exec have exec': "?exec a stk loc pc xcp stk' loc' pc' xcp'" by(simp add: exec_move_AAss1)
from True have τ: "τmove2 (compP2 P) h stk (a⌊i⌉ := e) pc xcp = τmove2 (compP2 P) h stk a pc xcp" by(simp add: τmove2_iff)
with IH1[OF exec' _ _ ‹P,h ⊢ stk [:≤] ST› ‹conf_xcp' (compP2 P) h xcp›] len bsok obtain e'' xs''
where bisim': "P,a,h' ⊢ (e'', xs'') ↔ (stk', loc', pc', xcp')"
and red: "?red a' xs e'' xs'' a stk pc pc' xcp xcp'" by auto
from bisim' have "P,a⌊i⌉ := e,h' ⊢ (e''⌊i⌉ := e, xs'') ↔ (stk', loc', pc', xcp')"
by(rule bisim1_bisims1.bisim1AAss1)
moreover from True have "no_call2 (a⌊i⌉ := e) pc = no_call2 a pc" by(simp add: no_call2_def)
ultimately show ?thesis using red τ by(fastforce intro: AAss1Red1 elim!: AAss_τred1r_xt1 AAss_τred1t_xt1)
next
case False
with pc have pc: "pc = length (compE2 a)" by auto
with bisim1 obtain v where a': "is_val a' ⟶ a' = Val v"
and stk: "stk = [v]" and xcp: "xcp = None" and call: "call1 a' = None"
by(auto dest: bisim1_pc_length_compE2D)
with bisim1 pc len bsok have rede1': "τred1r P t h (a', xs) (Val v, loc)"
by(auto intro: bisim1_Val_τred1r simp add: bsok_def)
hence "τred1r P t h (a'⌊i⌉ := e, xs) (Val v⌊i⌉ := e, loc)" by(rule AAss_τred1r_xt1)
moreover from pc exec stk xcp
have exec': "exec_meth_d (compP2 P) (compE2 a @ compE2 i @ compE2 e @ [AStore, Push Unit]) (compxE2 a 0 0 @ shift (length (compE2 a)) (stack_xlift (length [v]) (compxE2 i 0 0) @ shift (length (compE2 i)) (compxE2 e 0 (Suc (Suc 0))))) t h ([] @ [v], loc, length (compE2 a) + 0, None) ta h' (stk', loc', pc', xcp')"
by(simp add: compxE2_size_convs compxE2_stack_xlift_convs exec_move_def)
hence "exec_meth_d (compP2 P) (compE2 i @ compE2 e @ [AStore, Push Unit]) (stack_xlift (length [v]) (compxE2 i 0 0) @ shift (length (compE2 i)) (compxE2 e 0 (Suc (Suc 0)))) t h ([] @ [v], loc, 0, None) ta h' (stk', loc', pc' - length (compE2 a), xcp')"
by(rule exec_meth_drop_xt) auto
hence "exec_meth_d (compP2 P) (compE2 i) (stack_xlift (length [v]) (compxE2 i 0 0)) t h ([] @ [v], loc, 0, None) ta h' (stk', loc', pc' - length (compE2 a), xcp')"
by(rule exec_meth_take_xt) simp
with bisim2 obtain stk'' where stk': "stk' = stk'' @ [v]"
and exec'': "exec_move_d P t i h ([], loc, 0, None) ta h' (stk'', loc', pc' - length (compE2 a), xcp')"
unfolding exec_move_def by(blast dest: exec_meth_stk_split)
with pc xcp have τ: "τmove2 (compP2 P) h [v] (a⌊i⌉:= e) (length (compE2 a)) None = τmove2 (compP2 P) h [] i 0 None"
using τinstr_stk_drop_exec_move[where stk="[]" and vs="[v]"]
by(auto simp add: τmove2_iff)
from bisim1 have "length xs = length loc" by(rule bisim1_length_xs)
with IH2[OF exec''] len bsok obtain e'' xs''
where bisim': "P,i,h' ⊢ (e'', xs'') ↔ (stk'', loc', pc' - length (compE2 a), xcp')"
and red: "?red i loc e'' xs'' i [] 0 (pc' -