header {*
\chapter{Compilation}\label{cha:comp}
\isaheader{The JinjaThreads source language with explicit call stacks}
*}
theory J0 imports
"../J/WWellForm"
"../J/WellType"
"../J/Threaded"
"../Framework/FWBisimulation"
begin
declare widen_refT [elim]
consts
call :: "('a,'b) exp => (addr × mname × val list) option"
calls :: "('a,'b) exp list => (addr × mname × val list) option"
primrec
"call (new C) = None"
"call (newA T⌊e⌉) = call e"
"call (Cast C e) = call e"
"call (Val v) = None"
"call (Var V) = None"
"call (V:=e) = call e"
"call (e «bop» e') = (if is_val e then call e' else call e)"
"call (a⌊i⌉) = (if is_val a then call i else call a)"
"call (AAss a i e) = (if is_val a then (if is_val i then call e else call i) else call a)"
"call (a•length) = call a"
"call (e•F{D}) = call e"
"call (FAss e F D e') = (if is_val e then call e' else call e)"
"call (e•M(es)) = (if is_val e then
(if is_vals es ∧ is_addr e then ⌊(THE a. e = addr a, M, THE vs. es = map Val vs)⌋ else calls es)
else call e)"
"call ({V:T=vo; e}) = call e"
"call (syncV (o') e) = call o'"
"call (insyncV (a) e) = call e"
"call (e;;e') = call e"
"call (if (e) e1 else e2) = call e"
"call (while(b) e) = None"
"call (throw e) = call e"
"call (try e1 catch(C V) e2) = call e1"
"calls [] = None"
"calls (e#es) = (if is_val e then calls es else call e)"
declare domIff[iff, simp del]
lemma calls_append [simp]:
"calls (es @ es') = (if calls es = None ∧ is_vals es then calls es' else calls es)"
apply(induct es, auto)
done
lemma call_callE [consumes 1, case_names CallObj CallParams Call]:
"[| call (obj•M(pns)) = ⌊(a, M', vs)⌋;
call obj = ⌊(a, M', vs)⌋ ==> thesis;
!!v. [| obj = Val v; calls pns = ⌊(a, M', vs)⌋ |] ==> thesis;
[| obj = addr a; pns = map Val vs; M = M' |] ==> thesis |] ==> thesis"
by(auto split: split_if_asm simp add: is_vals_conv)
lemma calls_conv:
"calls es = ⌊aMvs⌋ <-> (∃vs e es'. es = map Val vs @ e # es' ∧ call e = ⌊aMvs⌋)"
proof(induct es)
case Nil thus ?case by simp
next
case (Cons e es)
note IH = `(calls es = ⌊aMvs⌋) = (∃vs e es'. es = map Val vs @ e # es' ∧ call e = ⌊aMvs⌋)`
show ?case
proof(cases "is_val e")
case True
then obtain v where e: "e = Val v" by auto
hence "calls (e # es) = calls es" by(auto)
moreover from e
have "(calls es = ⌊aMvs⌋) = (∃vs e' es'. e # es = map Val (v # vs) @ e' # es' ∧ call e' = ⌊aMvs⌋)"
unfolding IH by(auto)
also from e have "… = (∃vs e' es'. e # es = map Val vs @ e' # es' ∧ call e' = ⌊aMvs⌋)"
apply(auto simp add: Cons_eq_append_conv)
apply(rule_tac x="v # vs" in exI)
by(clarsimp)
finally show ?thesis .
next
case False
show ?thesis
proof(rule iffI)
assume "calls (e # es) = ⌊aMvs⌋"
with False have "call e = ⌊aMvs⌋" by(auto)
hence "e # es = map Val [] @ e # es" "call e = ⌊aMvs⌋" by auto
thus "∃vs e' es'. e # es = map Val vs @ e' # es' ∧ call e' = ⌊aMvs⌋" by blast
next
assume "∃vs e' es'. e # es = map Val vs @ e' # es' ∧ call e' = ⌊aMvs⌋"
then obtain vs e' es' where "e # es = map Val vs @ e' # es'" "call e' = ⌊aMvs⌋" by(blast)
moreover
with False have "vs = []"
by-(erule contrapos_np, auto simp add: neq_Nil_conv)
ultimately show "calls (e # es) = ⌊aMvs⌋" by(auto)
qed
qed
qed
lemma calls_map_Val [simp]:
"calls (map Val vs) = None"
by(induct vs, auto)
lemma call_not_is_val [dest]: "call e = ⌊aMvs⌋ ==> ¬ is_val e"
by(cases e, auto)
lemma is_calls_not_is_vals [dest]: "calls es = ⌊aMvs⌋ ==> ¬ is_vals es"
by(induct es, auto)
consts
inline_call :: "('a,'b) exp => ('a,'b) exp => ('a,'b) exp"
inline_calls :: "('a,'b) exp => ('a,'b) exp list => ('a,'b) exp list"
primrec
"inline_call f (new C) = new C"
"inline_call f (newA T⌊e⌉) = newA T⌊inline_call f e⌉"
"inline_call f (Cast C e) = Cast C (inline_call f e)"
"inline_call f (Val v) = Val v"
"inline_call f (Var V) = Var V"
"inline_call f (V:=e) = V := inline_call f e"
"inline_call f (e «bop» e') = (if is_val e then (e «bop» inline_call f e') else (inline_call f e «bop» e'))"
"inline_call f (a⌊i⌉) = (if is_val a then a⌊inline_call f i⌉ else (inline_call f a)⌊i⌉)"
"inline_call f (AAss a i e) = (if is_val a then if is_val i then AAss a i (inline_call f e) else AAss a (inline_call f i) e else AAss (inline_call f a) i e)"
"inline_call f (a•length) = inline_call f a•length"
"inline_call f (e•F{D}) = inline_call f e•F{D}"
"inline_call f (FAss e F D e') = (if is_val e then FAss e F D (inline_call f e') else FAss (inline_call f e) F D e')"
"inline_call f (e•M(es)) = (if is_val e then if is_vals es ∧ is_addr e then f else e•M(inline_calls f es) else inline_call f e•M(es))"
"inline_call f ({V:T=vo; e}) = {V:T=vo; inline_call f e}"
"inline_call f (syncV (o') e) = syncV (inline_call f o') e"
"inline_call f (insyncV (a) e) = insyncV (a) (inline_call f e)"
"inline_call f (e;;e') = inline_call f e;;e'"
"inline_call f (if (b) e else e') = (if (inline_call f b) e else e')"
"inline_call f (while (b) e) = while (b) e"
"inline_call f (throw e) = throw (inline_call f e)"
"inline_call f (try e1 catch(C V) e2) = try inline_call f e1 catch(C V) e2"
"inline_calls f [] = []"
"inline_calls f (e#es) = (if is_val e then e # inline_calls f es else inline_call f e # es)"
lemma inline_calls_map_Val_append [simp]:
"inline_calls f (map Val vs @ es) = map Val vs @ inline_calls f es"
by(induct vs, auto)
lemma inline_call_eq_Val_aux:
"inline_call e E = Val v ==> call E = ⌊aMvs⌋ ==> e = Val v"
by(induct E)(auto split: split_if_asm)
lemmas inline_call_eq_Val [dest] = inline_call_eq_Val_aux inline_call_eq_Val_aux[OF sym, THEN sym]
lemma inline_calls_eq_empty [simp]: "inline_calls e es = [] <-> es = []"
by(cases es, auto)
lemma inline_calls_map_Val [simp]: "inline_calls e (map Val vs) = map Val vs"
by(induct vs) auto
lemma fixes E :: "('a,'b) exp" and Es :: "('a,'b) exp list"
shows inline_call_eq_Throw [dest]: "inline_call e E = Throw a ==> call E = ⌊aMvs⌋ ==> e = Throw a ∨ e = addr a"
and True
by(induct E and Es)(fastsimp split:split_if_asm)+
lemma Throw_eq_inline_call_eq [dest]:
"inline_call e E = Throw a ==> call E = ⌊aMvs⌋ ==> Throw a = e ∨ addr a = e"
by(auto dest: inline_call_eq_Throw[OF sym])
lemma is_vals_inline_calls [dest]:
"[| is_vals (inline_calls e es); calls es = ⌊aMvs⌋ |] ==> is_val e"
by(induct es, auto split: split_if_asm)
lemma [dest]: "[| inline_calls e es = map Val vs; calls es = ⌊aMvs⌋ |] ==> is_val e"
"[| map Val vs = inline_calls e es; calls es = ⌊aMvs⌋ |] ==> is_val e"
by(fastsimp intro!: is_vals_inline_calls del: is_val.intros simp add: is_vals_conv elim: sym)+
lemma inline_calls_eq_Val_Throw [dest]:
"[| inline_calls e es = map Val vs @ Throw a # es'; calls es = ⌊aMvs⌋ |] ==> e = Throw a ∨ is_val e"
apply(induct es arbitrary: vs a es')
apply(auto simp add: Cons_eq_append_conv split: split_if_asm)
done
lemma Val_Throw_eq_inline_calls [dest]:
"[| map Val vs @ Throw a # es' = inline_calls e es; calls es = ⌊aMvs⌋ |] ==> Throw a = e ∨ is_val e"
by(auto dest: inline_calls_eq_Val_Throw[OF sym])
declare option.split [split del] split_if_asm [split] split_if [split del]
lemma call_inline_call [simp]:
"call e = ⌊aMvs⌋ ==> call (inline_call {v:T=vo; e'} e) = call e'"
"calls es = ⌊aMvs⌋ ==> calls (inline_calls {v:T=vo;e'} es) = call e'"
apply(induct e and es)
apply(fastsimp)
apply(fastsimp)
apply(fastsimp)
apply(fastsimp)
apply(fastsimp split: split_if)
apply(fastsimp)
apply(fastsimp)
apply(fastsimp split: split_if)
apply(clarsimp)
apply(fastsimp split: split_if)
apply(fastsimp split: split_if)
apply(fastsimp)
apply(fastsimp)
apply(fastsimp split: split_if)
apply(fastsimp split: split_if)
apply(fastsimp)
apply(fastsimp)
apply(fastsimp)
apply(fastsimp)
apply(fastsimp)
apply(fastsimp)
apply(fastsimp)
apply(fastsimp)
apply(fastsimp)
apply(fastsimp split: split_if)
done
declare option.split [split] split_if [split] split_if_asm [split del]
lemma fv_inline_call: "call e = ⌊aMvs⌋ ==> fv (inline_call e' e) ⊆ fv e ∪ fv e'"
and fvs_inline_calls: "calls es = ⌊aMvs⌋ ==> fvs (inline_calls e' es) ⊆ fvs es ∪ fv e'"
by(induct e and es)(fastsimp split: split_if_asm)+
lemma contains_insync_inline_call_conv:
"contains_insync (inline_call e e') <-> contains_insync e ∧ call e' ≠ None ∨ contains_insync e'"
and contains_insyncs_inline_calls_conv:
"contains_insyncs (inline_calls e es') <-> contains_insync e ∧ calls es' ≠ None ∨ contains_insyncs es'"
by(induct e' and es')(auto split: split_if_asm simp add: is_vals_conv)
lemma contains_insync_inline_call [simp]:
"call e' = ⌊aMvs⌋ ==> contains_insync (inline_call e e') <-> contains_insync e ∨ contains_insync e'"
and contains_insyncs_inline_calls [simp]:
"calls es' = ⌊aMvs⌋ ==> contains_insyncs (inline_calls e es') <-> contains_insync e ∨ contains_insyncs es'"
by(simp_all add: contains_insync_inline_call_conv contains_insyncs_inline_calls_conv)
definition synthesized_call :: "'m prog => heap => (addr × mname × val list) => bool"
where "synthesized_call P h = (λ(a, M, vs). ∃T. typeofh (Addr a) = ⌊T⌋ ∧ is_external_call P T M)"
lemma synthesized_call_conv:
"synthesized_call P h (a, M, vs) = (∃T. typeofh (Addr a) = ⌊T⌋ ∧ is_external_call P T M)"
by(simp add: synthesized_call_def)
types
J0_thread_action = "(addr,thread_id,expr × expr list,heap,addr,obs_event option) thread_action"
translations
"J0_thread_action" <= (type) "(nat,nat,expr × expr list,heap,nat,obs_event option) thread_action"
definition extNTA2J0 :: "J_prog => (cname × mname × addr) => (expr × expr list)"
where
"extNTA2J0 P = (λ(C, M, a). let (D, _, _, _, body) = method P C M
in ({this:Class D=⌊Addr a⌋; body}, [addr a•M([])]))"
lemma extNTA2J0_iff [simp]:
"extNTA2J0 P (C, M, a) =
({this:Class (fst (method P C M))=⌊Addr a⌋; snd (snd (snd (snd (method P C M))))}, [addr a•M([])])"
by(simp add: extNTA2J0_def split_def)
abbreviation extTA2J0 :: "J_prog => external_thread_action => J0_thread_action"
where "extTA2J0 P ≡ convert_extTA (extNTA2J0 P)"
inductive red0 :: "J_prog => expr => expr list => heap =>
J0_thread_action => expr => expr list => heap => bool"
("_ \<turnstile>0 ((1⟨_'/_,/_⟩) -_->/ (1⟨_'/_,/_⟩))" [51,0,0,0,0,0,0,0] 81)
for P ::J_prog
where
red0Red:
"[| extTA2J0 P,P \<turnstile> ⟨e, (h, empty)⟩ -ta-> ⟨e', (h', xs')⟩;
∀aMvs. call e = ⌊aMvs⌋ --> synthesized_call P h aMvs |]
==> P \<turnstile>0 ⟨e/es, h⟩ -ta-> ⟨e'/es, h'⟩"
| red0Call:
"[| call e = ⌊(a, M, vs)⌋; h a = ⌊Obj C fs⌋; ¬ is_external_call P (Class C) M; P \<turnstile> C sees M:Ts->T = (pns, body) in D;
size vs = size pns; size Ts = size pns |]
==> P \<turnstile>0 ⟨e/es, h⟩ -ε-> ⟨blocks(this#pns, Class D#Ts, Addr a#vs, body)/e#es, h⟩"
| red0Return:
"final e' ==> P \<turnstile>0 ⟨e'/e#es, h⟩ -ε-> ⟨inline_call e' e/es, h⟩"
lemma fv_extRet2J [simp]: "fv (extRet2J va) = {}"
by(cases va) simp_all
lemma assumes wf: "wwf_J_prog P"
shows red_fv_subset: "extTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩ ==> fv e' ⊆ fv e"
and reds_fvs_subset: "extTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩ ==> fvs es' ⊆ fvs es"
proof(induct rule: red_reds.inducts)
case (RedCall s a C fs M Ts T pns body D vs)
hence "fv body ⊆ {this} ∪ set pns"
using wf by(fastsimp dest!:sees_wf_mdecl simp:wf_mdecl_def)
with RedCall show ?case by fastsimp
qed(fastsimp)+
declare domIff[iff del]
lemma assumes wwf: "wwf_J_prog P"
shows red_fv_ok: "[| extTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩; fv e ⊆ dom (lcl s) |] ==> fv e' ⊆ dom (lcl s')"
and reds_fvs_ok: "[| extTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩; fvs es ⊆ dom (lcl s) |] ==> fvs es' ⊆ dom (lcl s')"
proof(induct rule: red_reds.inducts)
case (RedCall s a C fs M Ts T pns body D vs)
from `P \<turnstile> C sees M: Ts->T = (pns, body) in D` have "wwf_J_mdecl P D (M,Ts,t,pns,body)"
by(auto dest!: sees_wf_mdecl[OF wwf] simp add: wf_mdecl_def)
with RedCall show ?case by(auto)
next
case (BlockRed e h x V vo ta e' h' x' T)
note red = `extTA,P \<turnstile> ⟨e,(h, x(V := vo))⟩ -ta-> ⟨e',(h', x')⟩`
hence "fv e' ⊆ fv e" by(auto dest: red_fv_subset[OF wwf] del: subsetI)
moreover from ` fv {V:T=vo; e} ⊆ dom (lcl (h, x))`
have "fv e - {V} ⊆ dom x" by(simp)
ultimately have "fv e' - {V} ⊆ dom x - {V}" by(auto)
moreover from red have "dom (x(V := vo)) ⊆ dom x'"
by(auto dest: red_lcl_incr del: subsetI)
ultimately have "fv e' - {V} ⊆ dom x' - {V}"
by(auto split: split_if_asm)
thus ?case by(auto simp del: fun_upd_apply)
qed(fastsimp dest: red_lcl_incr del: subsetI)+
lemma is_call_red_state_unchanged:
"[| extTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩; call e = ⌊aMvs⌋; ¬ synthesized_call P (hp s) aMvs |] ==> s' = s ∧ ta = ε"
and is_calls_reds_state_unchanged:
"[| extTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩; calls es = ⌊aMvs⌋; ¬ synthesized_call P (hp s) aMvs |] ==> s' = s ∧ ta = ε"
apply(induct rule: red_reds.inducts)
apply(fastsimp split: split_if_asm simp add: synthesized_call_def)+
done
lemma called_methodD:
"[| extTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩; call e = ⌊(a, M, vs)⌋; ¬ synthesized_call P (hp s) (a, M, vs) |]
==> ∃C fs D Us U pns body. hp s' = hp s ∧ hp s a = ⌊Obj C fs⌋ ∧ P \<turnstile> C sees M: Us->U = (pns, body) in D ∧
length vs = length pns ∧ length Us = length pns"
(is "[| _; _; _ |] ==> ?concl")
and called_methodsD:
"[| extTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩; calls es = ⌊(a, M, vs)⌋; ¬ synthesized_call P (hp s) (a, M, vs) |]
==> ∃C fs D Us U pns body. hp s' = hp s ∧ hp s a = ⌊Obj C fs⌋ ∧ P \<turnstile> C sees M: Us->U = (pns, body) in D ∧
length vs = length pns ∧ length Us = length pns"
(is "[| _; _; _ |] ==> ?concl")
apply(induct rule: red_reds.inducts)
apply(auto split: split_if_asm simp add: synthesized_call_def)
apply(fastsimp)
done
abbreviation mred0 :: "J_prog => (addr,addr,expr × expr list,heap,addr,obs_event) semantics"
where "mred0 P ≡ (λ((e, es), h) ta ((e', es'), h'). red0 P e es h ta e' es' h')"
section {* Silent moves *}
primrec τmove0 :: "'m prog => heap => ('a, 'b) exp => bool"
and τmoves0 :: "'m prog => heap => ('a, 'b) exp list => bool"
where
"τmove0 P h (new C) <-> False"
| "τmove0 P h (newA T⌊e⌉) <-> τmove0 P h e ∨ (∃a. e = Throw a)"
| "τmove0 P h (Cast U e) <-> τmove0 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v)"
| "τmove0 P h (e «bop» e') <-> τmove0 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v ∧
(τmove0 P h e' ∨ (∃a. e' = Throw a) ∨ (∃v. e' = Val v)))"
| "τmove0 P h (Val v) <-> False"
| "τmove0 P h (Var V) <-> True"
| "τmove0 P h (V := e) <-> τmove0 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v)"
| "τmove0 P h (a⌊i⌉) <-> τmove0 P h a ∨ (∃ad. a = Throw ad) ∨ (∃v. a = Val v ∧ (τmove0 P h i ∨ (∃a. i = Throw a)))"
| "τmove0 P h (AAss a i e) <-> τmove0 P h a ∨ (∃ad. a = Throw ad) ∨ (∃v. a = Val v ∧
(τmove0 P h i ∨ (∃a. i = Throw a) ∨ (∃v. i = Val v ∧ (τmove0 P h e ∨ (∃a. e = Throw a)))))"
| "τmove0 P h (a•length) <-> τmove0 P h a ∨ (∃ad. a = Throw ad)"
| "τmove0 P h (e•F{D}) <-> τmove0 P h e ∨ (∃a. e = Throw a)"
| "τmove0 P h (FAss e F D e') <-> τmove0 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v ∧ (τmove0 P h e' ∨ (∃a. e' = Throw a)))"
| "τmove0 P h (e•M(es)) <-> τmove0 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v ∧
((τmoves0 P h es ∨ (∃vs a es'. es = map Val vs @ Throw a # es')) ∨
(∃vs. es = map Val vs ∧ (v = Null ∨ (∀T. typeofh v = ⌊T⌋ --> ¬ is_external_call P T M)))))"
| "τmove0 P h ({V:T=vo; e}) <-> τmove0 P h e ∨ ((∃a. e = Throw a) ∨ (∃v. e = Val v))"
| "τmove0 P h (syncV'(e) e') <-> τmove0 P h e ∨ (∃a. e = Throw a)"
| "τmove0 P h (insyncV'(ad) e) <-> τmove0 P h e"
| "τmove0 P h (e;;e') <-> τmove0 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v)"
| "τmove0 P h (if (e) e' else e'') <-> τmove0 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v)"
| "τmove0 P h (while (e) e') = True"
| "τmove0 P h (throw e) <-> τmove0 P h e ∨ (∃a. e = Throw a) ∨ e = null"
| "τmove0 P h (try e catch(C V) e') <-> τmove0 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v)"
| "τmoves0 P h [] <-> False"
| "τmoves0 P h (e # es) <-> τmove0 P h e ∨ (∃v. e = Val v ∧ τmoves0 P h es)"
lemma τmove0_τmoves0_intros:
fixes e e1 e2 e' :: "('a, 'b) exp" and es :: "('a, 'b) exp list"
shows τmove0NewArray: "τmove0 P h e ==> τmove0 P h (newA T⌊e⌉)"
and τmove0Cast: "τmove0 P h e ==> τmove0 P h (Cast U e)"
and τmove0CastRed: "τmove0 P h (Cast U (Val v))"
and τmove0BinOp1: "τmove0 P h e ==> τmove0 P h (e«bop»e')"
and τmove0BinOp2: "τmove0 P h e ==> τmove0 P h (Val v«bop»e)"
and τmove0BinOp: "τmove0 P h (Val v«bop»Val v')"
and τmove0Var: "τmove0 P h (Var V)"
and τmove0LAss: "τmove0 P h e ==> τmove0 P h (V := e)"
and τmove0LAssRed: "τmove0 P h (V := Val v)"
and τmove0AAcc1: "τmove0 P h e ==> τmove0 P h (e⌊e'⌉)"
and τmove0AAcc2: "τmove0 P h e ==> τmove0 P h (Val v⌊e⌉)"
and τmove0AAss1: "τmove0 P h e ==> τmove0 P h (e⌊e1⌉ := e2)"
and τmove0AAss2: "τmove0 P h e ==> τmove0 P h (Val v⌊e⌉ := e')"
and τmove0AAss3: "τmove0 P h e ==> τmove0 P h (Val v⌊Val v'⌉ := e)"
and τmove0ALength: "τmove0 P h e ==> τmove0 P h (e•length)"
and τmove0FAcc: "τmove0 P h e ==> τmove0 P h (e•F{D})"
and τmove0FAss1: "τmove0 P h e ==> τmove0 P h (FAss e F D e')"
and τmove0FAss2: "τmove0 P h e ==> τmove0 P h (Val v•F{D} := e)"
and τmove0CallObj: "τmove0 P h e ==> τmove0 P h (e•M(es))"
and τmove0CallParams: "τmoves0 P h es ==> τmove0 P h (Val v•M(es))"
and τmove0Call: "(!!T. typeofh v = ⌊T⌋ ==> ¬ is_external_call P T M) ==> τmove0 P h (Val v•M(map Val vs))"
and τmove0Block: "τmove0 P h e ==> τmove0 P h {V:T=vo; e}"
and τmove0BlockRed: "τmove0 P h {V:T=vo; Val v}"
and τmove0Sync: "τmove0 P h e ==> τmove0 P h (syncV' (e) e')"
and τmove0InSync: "τmove0 P h e ==> τmove0 P h (insyncV' (a) e)"
and τmove0Seq: "τmove0 P h e ==> τmove0 P h (e;;e')"
and τmove0SeqRed: "τmove0 P h (Val v;; e')"
and τmove0Cond: "τmove0 P h e ==> τmove0 P h (if (e) e1 else e2)"
and τmove0CondRed: "τmove0 P h (if (Val v) e1 else e2)"
and τmove0WhileRed: "τmove0 P h (while (e) e')"
and τmove0Throw: "τmove0 P h e ==> τmove0 P h (throw e)"
and τmove0ThrowNull: "τmove0 P h (throw null)"
and τmove0Try: "τmove0 P h e ==> τmove0 P h (try e catch(C V) e')"
and τmove0TryRed: "τmove0 P h (try Val v catch(C V) e)"
and τmove0TryThrow: "τmove0 P h (try Throw a catch(C V) e)"
and τmove0NewArrayThrow: "τmove0 P h (newA T⌊Throw a⌉)"
and τmove0CastThrow: "τmove0 P h (Cast T (Throw a))"
and τmove0BinOpThrow1: "τmove0 P h (Throw a «bop» e')"
and τmove0BinOpThrow2: "τmove0 P h (Val v «bop» Throw a)"
and τmove0LAssThrow: "τmove0 P h (V:=(Throw a))"
and τmove0AAccThrow1: "τmove0 P h (Throw a⌊e⌉)"
and τmove0AAccThrow2: "τmove0 P h (Val v⌊Throw a⌉)"
and τmove0AAssThrow1: "τmove0 P h (AAss (Throw a) e e')"
and τmove0AAssThrow2: "τmove0 P h (AAss (Val v) (Throw a) e')"
and τmove0AAssThrow3: "τmove0 P h (AAss (Val v) (Val v') (Throw a))"
and τmove0ALengthThrow: "τmove0 P h (Throw a•length)"
and τmove0FAccThrow: "τmove0 P h (Throw a•F{D})"
and τmove0FAssThrow1: "τmove0 P h (Throw a•F{D} := e)"
and τmove0FAssThrow2: "τmove0 P h (FAss (Val v) F D (Throw a))"
and τmove0CallThrowObj: "τmove0 P h (Throw a•M(es))"
and τmove0CallThrowParams: "τmove0 P h (Val v•M(map Val vs @ Throw a # es))"
and τmove0BlockThrow: "τmove0 P h {V:T=vo; Throw a}"
and τmove0SyncThrow: "τmove0 P h (syncV' (Throw a) e)"
and τmove0SeqThrow: "τmove0 P h (Throw a;;e)"
and τmove0CondThrow: "τmove0 P h (if (Throw a) e1 else e2)"
and τmove0ThrowThrow: "τmove0 P h (throw (Throw a))"
and τmoves0Hd: "τmove0 P h e ==> τmoves0 P h (e # es)"
and τmoves0Tl: "τmoves0 P h es ==> τmoves0 P h (Val v # es)"
apply auto
done
lemma τmoves0_map_Val [iff]:
"¬ τmoves0 P h (map Val vs)"
by(induct vs) auto
lemma τmoves0_map_Val_append [simp]:
"τmoves0 P h (map Val vs @ es) = τmoves0 P h es"
by(induct vs)(auto)
lemma no_reds_map_Val_Throw [simp]:
"extTA,P \<turnstile> ⟨map Val vs @ Throw a # es, s⟩ [-ta->] ⟨es', s'⟩ = False"
by(induct vs arbitrary: es')(auto elim: reds.cases)
lemma red_τ_taD: "[| extTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩; τmove0 P (hp s) e |] ==> ta = ε"
and reds_τ_taD: "[| extTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩; τmoves0 P (hp s) es |] ==> ta = ε"
apply(induct rule: red_reds.inducts)
apply(fastsimp simp add: map_eq_append_conv)+
done
lemma τmove0_heap_unchanged: "[| extTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩; τmove0 P (hp s) e |] ==> hp s' = hp s"
and τmoves0_heap_unchanged: "[| extTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩; τmoves0 P (hp s) es |] ==> hp s' = hp s"
apply(induct rule: red_reds.inducts)
apply(auto)
apply(fastsimp simp add: map_eq_append_conv)
done
primrec τMove0 :: "'m prog => heap => (expr × expr list) => bool"
where
"τMove0 P h (e, exs) = (τmove0 P h e ∨ final e)"
lemma τMove0_iff:
"τMove0 P h ees <-> (let (e, _) = ees in τmove0 P h e ∨ final e)"
by(cases ees)(simp)
definition no_call :: "'m prog => heap => ('a, 'b) exp => bool"
where "no_call P h e = (∀aMvs. call e = ⌊aMvs⌋ --> synthesized_call P h aMvs)"
definition no_calls :: "'m prog => heap => ('a, 'b) exp list => bool"
where "no_calls P h es = (∀aMvs. calls es = ⌊aMvs⌋ --> synthesized_call P h aMvs)"
lemma no_call_simps [simp]:
"no_call P h (new C) = True"
"no_call P h (newA T⌊e⌉) = no_call P h e"
"no_call P h (Cast T e) = no_call P h e"
"no_call P h (Val v) = True"
"no_call P h (Var V) = True"
"no_call P h (V := e) = no_call P h e"
"no_call P h (e «bop» e') = (if is_val e then no_call P h e' else no_call P h e)"
"no_call P h (a⌊i⌉) = (if is_val a then no_call P h i else no_call P h a)"
"no_call P h (AAss a i e) = (if is_val a then (if is_val i then no_call P h e else no_call P h i) else no_call P h a)"
"no_call P h (a•length) = no_call P h a"
"no_call P h (e•F{D}) = no_call P h e"
"no_call P h (FAss e F D e') = (if is_val e then no_call P h e' else no_call P h e)"
"no_call P h (e•M(es)) = (if is_val e then (if is_vals es ∧ is_addr e then synthesized_call P h (THE a. e = addr a, M, THE vs. es = map Val vs) else no_calls P h es) else no_call P h e)"
"no_call P h ({V:T=vo; e}) = no_call P h e"
"no_call P h (syncV' (e) e') = no_call P h e"
"no_call P h (insyncV' (ad) e) = no_call P h e"
"no_call P h (e;;e') = no_call P h e"
"no_call P h (if (e) e1 else e2) = no_call P h e"
"no_call P h (while(e) e') = True"
"no_call P h (throw e) = no_call P h e"
"no_call P h (try e catch(C V) e') = no_call P h e"
by(auto simp add: no_call_def no_calls_def)
lemma no_calls_simps [simp]:
"no_calls P h [] = True"
"no_calls P h (e # es) = (if is_val e then no_calls P h es else no_call P h e)"
by(simp_all add: no_call_def no_calls_def)
lemma no_calls_map_Val [simp]:
"no_calls P h (map Val vs)"
by(induct vs) simp_all
definition τred0 :: "(external_thread_action => (addr,thread_id,'x,heap,addr,obs_event option) thread_action) =>
J_prog => heap => (expr × locals) => (expr × locals) => bool"
where "τred0 extTA P h exs e'xs' = (extTA,P \<turnstile> ⟨fst exs, (h, snd exs)⟩ -ε-> ⟨fst e'xs', (h, snd e'xs')⟩ ∧ τmove0 P h (fst exs) ∧ no_call P h (fst exs))"
definition τreds0 :: "(external_thread_action => (addr,thread_id,'x,heap,addr,obs_event option) thread_action) =>
J_prog => heap => (expr list × locals) => (expr list × locals) => bool"
where "τreds0 extTA P h esxs es'xs' = (extTA,P \<turnstile> ⟨fst esxs, (h, snd esxs)⟩ [-ε->] ⟨fst es'xs', (h, snd es'xs')⟩ ∧ τmoves0 P h (fst esxs) ∧ no_calls P h (fst esxs))"
abbreviation τred0t :: "(external_thread_action => (addr,thread_id,'x,heap,addr,obs_event option) thread_action) =>
J_prog => heap => (expr × locals) => (expr × locals) => bool"
where "τred0t extTA P h ≡ (τred0 extTA P h)^++"
abbreviation τreds0t :: "(external_thread_action => (addr,thread_id,'x,heap,addr,obs_event option) thread_action) =>
J_prog => heap => (expr list × locals) => (expr list × locals) => bool"
where "τreds0t extTA P h ≡ (τreds0 extTA P h)^++"
abbreviation τred0r :: "(external_thread_action => (addr,thread_id,'x,heap,addr,obs_event option) thread_action) =>
J_prog => heap => (expr × locals) => (expr × locals) => bool"
where "τred0r extTA P h ≡ (τred0 extTA P h)^**"
abbreviation τreds0r :: "(external_thread_action => (addr,thread_id,'x,heap,addr,obs_event option) thread_action) =>
J_prog => heap => (expr list × locals) => (expr list × locals) => bool"
where "τreds0r extTA P h ≡ (τreds0 extTA P h)^**"
lemma τred0_iff [iff]:
"τred0 extTA P h (e, xs) (e', xs') = (extTA,P \<turnstile> ⟨e, (h, xs)⟩ -ε-> ⟨e', (h, xs')⟩ ∧ τmove0 P h e ∧ no_call P h e)"
by(simp add: τred0_def)
lemma τreds0_iff [iff]:
"τreds0 extTA P h (es, xs) (es', xs') = (extTA,P \<turnstile> ⟨es, (h, xs)⟩ [-ε->] ⟨es', (h, xs')⟩ ∧ τmoves0 P h es ∧ no_calls P h es)"
by(simp add: τreds0_def)
lemma τred0t_1step:
"[| extTA,P \<turnstile> ⟨e, (h, xs)⟩ -ε-> ⟨e', (h, xs')⟩; τmove0 P h e; no_call P h e |]
==> τred0t extTA P h (e, xs) (e', xs')"
by(blast intro: tranclp.r_into_trancl)
lemma τred0t_2step:
"[| extTA,P \<turnstile> ⟨e, (h, xs)⟩ -ε-> ⟨e', (h, xs')⟩; τmove0 P h e; no_call P h e;
extTA,P \<turnstile> ⟨e', (h, xs')⟩ -ε-> ⟨e'', (h, xs'')⟩; τmove0 P h e'; no_call P h e' |]
==> τred0t extTA P h (e, xs) (e'', xs'')"
by(blast intro: tranclp.trancl_into_trancl[OF τred0t_1step])
lemma τred1t_3step:
"[| extTA,P \<turnstile> ⟨e, (h, xs)⟩ -ε-> ⟨e', (h, xs')⟩; τmove0 P h e; no_call P h e;
extTA,P \<turnstile> ⟨e', (h, xs')⟩ -ε-> ⟨e'', (h, xs'')⟩; τmove0 P h e'; no_call P h e';
extTA,P \<turnstile> ⟨e'', (h, xs'')⟩ -ε-> ⟨e''', (h, xs''')⟩; τmove0 P h e''; no_call P h e'' |]
==> τred0t extTA P h (e, xs) (e''', xs''')"
by(blast intro: tranclp.trancl_into_trancl[OF τred0t_2step])
lemma τreds0t_1step:
"[| extTA,P \<turnstile> ⟨es, (h, xs)⟩ [-ε->] ⟨es', (h, xs')⟩; τmoves0 P h es; no_calls P h es |]
==> τreds0t extTA P h (es, xs) (es', xs')"
by(blast intro: tranclp.r_into_trancl)
lemma τreds0t_2step:
"[| extTA,P \<turnstile> ⟨es, (h, xs)⟩ [-ε->] ⟨es', (h, xs')⟩; τmoves0 P h es; no_calls P h es;
extTA,P \<turnstile> ⟨es', (h, xs')⟩ [-ε->] ⟨es'', (h, xs'')⟩; τmoves0 P h es'; no_calls P h es' |]
==> τreds0t extTA P h (es, xs) (es'', xs'')"
by(blast intro: tranclp.trancl_into_trancl[OF τreds0t_1step])
lemma τreds0t_3step:
"[| extTA,P \<turnstile> ⟨es, (h, xs)⟩ [-ε->] ⟨es', (h, xs')⟩; τmoves0 P h es; no_calls P h es;
extTA,P \<turnstile> ⟨es', (h, xs')⟩ [-ε->] ⟨es'', (h, xs'')⟩; τmoves0 P h es'; no_calls P h es';
extTA,P \<turnstile> ⟨es'', (h, xs'')⟩ [-ε->] ⟨es''', (h, xs''')⟩; τmoves0 P h es''; no_calls P h es'' |]
==> τreds0t extTA P h (es, xs) (es''', xs''')"
by(blast intro: tranclp.trancl_into_trancl[OF τreds0t_2step])
lemma τred0r_1step:
"[| extTA,P \<turnstile> ⟨e, (h, xs)⟩ -ε-> ⟨e', (h, xs')⟩; τmove0 P h e; no_call P h e |]
==> τred0r extTA P h (e, xs) (e', xs')"
by(blast intro: r_into_rtranclp)
lemma τred0r_2step:
"[| extTA,P \<turnstile> ⟨e, (h, xs)⟩ -ε-> ⟨e', (h, xs')⟩; τmove0 P h e; no_call P h e;
extTA,P \<turnstile> ⟨e', (h, xs')⟩ -ε-> ⟨e'', (h, xs'')⟩; τmove0 P h e'; no_call P h e' |]
==> τred0r extTA P h (e, xs) (e'', xs'')"
by(blast intro: rtranclp.rtrancl_into_rtrancl[OF τred0r_1step])
lemma τred0r_3step:
"[| extTA,P \<turnstile> ⟨e, (h, xs)⟩ -ε-> ⟨e', (h, xs')⟩; τmove0 P h e; no_call P h e;
extTA,P \<turnstile> ⟨e', (h, xs')⟩ -ε-> ⟨e'', (h, xs'')⟩; τmove0 P h e'; no_call P h e';
extTA,P \<turnstile> ⟨e'', (h, xs'')⟩ -ε-> ⟨e''', (h, xs''')⟩; τmove0 P h e''; no_call P h e'' |]
==> τred0r extTA P h (e, xs) (e''', xs''')"
by(blast intro: rtranclp.rtrancl_into_rtrancl[OF τred0r_2step])
lemma τreds0r_1step:
"[| extTA,P \<turnstile> ⟨es, (h, xs)⟩ [-ε->] ⟨es', (h, xs')⟩; τmoves0 P h es; no_calls P h es |]
==> τreds0r extTA P h (es, xs) (es', xs')"
by(blast intro: r_into_rtranclp)
lemma τreds0r_2step:
"[| extTA,P \<turnstile> ⟨es, (h, xs)⟩ [-ε->] ⟨es', (h, xs')⟩; τmoves0 P h es; no_calls P h es;
extTA,P \<turnstile> ⟨es', (h, xs')⟩ [-ε->] ⟨es'', (h, xs'')⟩; τmoves0 P h es'; no_calls P h es' |]
==> τreds0r extTA P h (es, xs) (es'', xs'')"
by(blast intro: rtranclp.rtrancl_into_rtrancl[OF τreds0r_1step])
lemma τreds0r_3step:
"[| extTA,P \<turnstile> ⟨es, (h, xs)⟩ [-ε->] ⟨es', (h, xs')⟩; τmoves0 P h es; no_calls P h es;
extTA,P \<turnstile> ⟨es', (h, xs')⟩ [-ε->] ⟨es'', (h, xs'')⟩; τmoves0 P h es'; no_calls P h es';
extTA,P \<turnstile> ⟨es'', (h, xs'')⟩ [-ε->] ⟨es''', (h, xs''')⟩; τmoves0 P h es''; no_calls P h es'' |]
==> τreds0r extTA P h (es, xs) (es''', xs''')"
by(blast intro: rtranclp.rtrancl_into_rtrancl[OF τreds0r_2step])
lemma τred0t_inj_τreds0t: "τred0t extTA P h (e, xs) (e', xs') ==> τreds0t extTA P h (e # es, xs) (e' # es, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl ListRed1)
lemma τreds0t_cons_τreds0t: "τreds0t extTA P h (es, xs) (es', xs') ==> τreds0t extTA P h (Val v # es, xs) (Val v # es', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl ListRed2)
lemma τred0r_inj_τreds0r: "τred0r extTA P h (e, xs) (e', xs') ==> τreds0r extTA P h (e # es, xs) (e' # es, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl ListRed1)
lemma τreds0r_cons_τreds0r: "τreds0r extTA P h (es, xs) (es', xs') ==> τreds0r extTA P h (Val v # es, xs) (Val v # es', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl ListRed2)
lemma NewArray_τred0t_xt:
"τred0t extTA P h (e, xs) (e', xs') ==> τred0t extTA P h (newA T⌊e⌉, xs) (newA T⌊e'⌉, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl NewArrayRed)
lemma Cast_τred0t_xt:
"τred0t extTA P h (e, xs) (e', xs') ==> τred0t extTA P h (Cast T e, xs) (Cast T e', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl CastRed)
lemma BinOp_τred0t_xt1:
"τred0t extTA P h (e1, xs) (e1', xs') ==> τred0t extTA P h (e1 «bop» e2, xs) (e1' «bop» e2, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl BinOpRed1)
lemma BinOp_τred0t_xt2:
"τred0t extTA P h (e2, xs) (e2', xs') ==> τred0t extTA P h (Val v «bop» e2, xs) (Val v «bop» e2', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl BinOpRed2)
lemma LAss_τred0t:
"τred0t extTA P h (e, xs) (e', xs') ==> τred0t extTA P h (V := e, xs) (V := e', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl LAssRed)
lemma AAcc_τred0t_xt1:
"τred0t extTA P h (a, xs) (a', xs') ==> τred0t extTA P h (a⌊i⌉, xs) (a'⌊i⌉, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl AAccRed1)
lemma AAcc_τred0t_xt2:
"τred0t extTA P h (i, xs) (i', xs') ==> τred0t extTA P h (Val a⌊i⌉, xs) (Val a⌊i'⌉, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl AAccRed2)
lemma AAss_τred0t_xt1:
"τred0t extTA P h (a, xs) (a', xs') ==> τred0t extTA P h (a⌊i⌉ := e, xs) (a'⌊i⌉ := e, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl AAssRed1)
lemma AAss_τred0t_xt2:
"τred0t extTA P h (i, xs) (i', xs') ==> τred0t extTA P h (Val a⌊i⌉ := e, xs) (Val a⌊i'⌉ := e, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl AAssRed2)
lemma AAss_τred0t_xt3:
"τred0t extTA P h (e, xs) (e', xs') ==> τred0t extTA P h (Val a⌊Val i⌉ := e, xs) (Val a⌊Val i⌉ := e', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl AAssRed3)
lemma ALength_τred0t_xt:
"τred0t extTA P h (a, xs) (a', xs') ==> τred0t extTA P h (a•length, xs) (a'•length, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl ALengthRed)
lemma FAcc_τred0t_xt:
"τred0t extTA P h (e, xs) (e', xs') ==> τred0t extTA P h (e•F{D}, xs) (e'•F{D}, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl FAccRed)
lemma FAss_τred0t_xt1:
"τred0t extTA P h (e, xs) (e', xs') ==> τred0t extTA P h (e•F{D} := e2, xs) (e'•F{D} := e2, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl FAssRed1)
lemma FAss_τred0t_xt2:
"τred0t extTA P h (e, xs) (e', xs') ==> τred0t extTA P h (Val v•F{D} := e, xs) (Val v•F{D} := e', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl FAssRed2)
lemma Call_τred0t_obj:
"τred0t extTA P h (e, xs) (e', xs') ==> τred0t extTA P h (e•M(ps), xs) (e'•M(ps), xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl CallObj)
lemma Call_τred0t_param:
"τreds0t extTA P h (es, xs) (es', xs') ==> τred0t extTA P h (Val v•M(es), xs) (Val v•M(es'), xs')"
by(induct rule: tranclp_induct2)(fastsimp intro: tranclp.trancl_into_trancl CallParams)+
lemma Block_τred0t_xt:
"τred0t extTA P h (e, xs(V := vo)) (e', xs') ==> τred0t extTA P h ({V:T=vo; e}, xs) ({V:T=xs' V; e'}, xs'(V := xs V))"
proof(induct rule: tranclp_induct2)
case base thus ?case by(auto intro: BlockRed simp del: fun_upd_apply)
next
case (step e' xs' e'' xs'')
from `τred0 extTA P h (e', xs') (e'', xs'')`
have "extTA,P \<turnstile> ⟨e',(h, xs')⟩ -ε-> ⟨e'',(h, xs'')⟩" "τmove0 P h e'" "no_call P h e'" by auto
hence "extTA,P \<turnstile> ⟨e',(h, xs'(V := xs V, V := xs' V))⟩ -ε-> ⟨e'',(h, xs'')⟩" by simp
from BlockRed[OF this, of T] `τmove0 P h e'` `no_call P h e'`
have "τred0 extTA P h ({V:T=xs' V; e'}, xs'(V := xs V)) ({V:T=xs'' V; e''}, xs''(V := xs V))" by(auto)
with `τred0t extTA P h ({V:T=vo; e}, xs) ({V:T=xs' V; e'}, xs'(V := xs V))` show ?case ..
qed
lemma Sync_τred0t_xt:
"τred0t extTA P h (e, xs) (e', xs') ==> τred0t extTA P h (syncV (e) e2, xs) (syncV (e') e2, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl SynchronizedRed1)
lemma InSync_τred0t_xt:
"τred0t extTA P h (e, xs) (e', xs') ==> τred0t extTA P h (insyncV (a) e, xs) (insyncV (a) e', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl SynchronizedRed2)
lemma Seq_τred0t_xt:
"τred0t extTA P h (e, xs) (e', xs') ==> τred0t extTA P h (e;;e2, xs) (e';;e2, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl SeqRed)
lemma Cond_τred0t_xt:
"τred0t extTA P h (e, xs) (e', xs') ==> τred0t extTA P h (if (e) e1 else e2, xs) (if (e') e1 else e2, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl CondRed)
lemma Throw_τred0t_xt:
"τred0t extTA P h (e, xs) (e', xs') ==> τred0t extTA P h (throw e, xs) (throw e', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl ThrowRed)
lemma Try_τred0t_xt:
"τred0t extTA P h (e, xs) (e', xs') ==> τred0t extTA P h (try e catch(C V) e2, xs) (try e' catch(C V) e2, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl TryRed)
lemma NewArray_τred0r_xt:
"τred0r extTA P h (e, xs) (e', xs') ==> τred0r extTA P h (newA T⌊e⌉, xs) (newA T⌊e'⌉, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl NewArrayRed)
lemma Cast_τred0r_xt:
"τred0r extTA P h (e, xs) (e', xs') ==> τred0r extTA P h (Cast T e, xs) (Cast T e', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl CastRed)
lemma BinOp_τred0r_xt1:
"τred0r extTA P h (e1, xs) (e1', xs') ==> τred0r extTA P h (e1 «bop» e2, xs) (e1' «bop» e2, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl BinOpRed1)
lemma BinOp_τred0r_xt2:
"τred0r extTA P h (e2, xs) (e2', xs') ==> τred0r extTA P h (Val v «bop» e2, xs) (Val v «bop» e2', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl BinOpRed2)
lemma LAss_τred0r:
"τred0r extTA P h (e, xs) (e', xs') ==> τred0r extTA P h (V := e, xs) (V := e', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl LAssRed)
lemma AAcc_τred0r_xt1:
"τred0r extTA P h (a, xs) (a', xs') ==> τred0r extTA P h (a⌊i⌉, xs) (a'⌊i⌉, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl AAccRed1)
lemma AAcc_τred0r_xt2:
"τred0r extTA P h (i, xs) (i', xs') ==> τred0r extTA P h (Val a⌊i⌉, xs) (Val a⌊i'⌉, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl AAccRed2)
lemma AAss_τred0r_xt1:
"τred0r extTA P h (a, xs) (a', xs') ==> τred0r extTA P h (a⌊i⌉ := e, xs) (a'⌊i⌉ := e, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl AAssRed1)
lemma AAss_τred0r_xt2:
"τred0r extTA P h (i, xs) (i', xs') ==> τred0r extTA P h (Val a⌊i⌉ := e, xs) (Val a⌊i'⌉ := e, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl AAssRed2)
lemma AAss_τred0r_xt3:
"τred0r extTA P h (e, xs) (e', xs') ==> τred0r extTA P h (Val a⌊Val i⌉ := e, xs) (Val a⌊Val i⌉ := e', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl AAssRed3)
lemma ALength_τred0r_xt:
"τred0r extTA P h (a, xs) (a', xs') ==> τred0r extTA P h (a•length, xs) (a'•length, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl ALengthRed)
lemma FAcc_τred0r_xt:
"τred0r extTA P h (e, xs) (e', xs') ==> τred0r extTA P h (e•F{D}, xs) (e'•F{D}, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl FAccRed)
lemma FAss_τred0r_xt1:
"τred0r extTA P h (e, xs) (e', xs') ==> τred0r extTA P h (e•F{D} := e2, xs) (e'•F{D} := e2, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl FAssRed1)
lemma FAss_τred0r_xt2:
"τred0r extTA P h (e, xs) (e', xs') ==> τred0r extTA P h (Val v•F{D} := e, xs) (Val v•F{D} := e', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl FAssRed2)
lemma Call_τred0r_obj:
"τred0r extTA P h (e, xs) (e', xs') ==> τred0r extTA P h (e•M(ps), xs) (e'•M(ps), xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl CallObj)
lemma Call_τred0r_param:
"τreds0r extTA P h (es, xs) (es', xs') ==> τred0r extTA P h (Val v•M(es), xs) (Val v•M(es'), xs')"
by(induct rule: rtranclp_induct2)(fastsimp intro: rtranclp.rtrancl_into_rtrancl CallParams)+
lemma Block_τred0r_xt:
"τred0r extTA P h (e, xs(V := vo)) (e', xs') ==> τred0r extTA P h ({V:T=vo; e}, xs) ({V:T=xs' V; e'}, xs'(V := xs V))"
proof(induct rule: rtranclp_induct2)
case refl thus ?case by(simp del: fun_upd_apply)(auto simp add: fun_upd_apply)
next
case (step e' xs' e'' xs'')
from `τred0 extTA P h (e', xs') (e'', xs'')`
have "extTA,P \<turnstile> ⟨e',(h, xs')⟩ -ε-> ⟨e'',(h, xs'')⟩" "τmove0 P h e'" "no_call P h e'" by auto
hence "extTA,P \<turnstile> ⟨e',(h, xs'(V := xs V, V := xs' V))⟩ -ε-> ⟨e'',(h, xs'')⟩" by simp
from BlockRed[OF this, of T] `τmove0 P h e'` `no_call P h e'`
have "τred0 extTA P h ({V:T=xs' V; e'}, xs'(V := xs V)) ({V:T=xs'' V; e''}, xs''(V := xs V))" by auto
with `τred0r extTA P h ({V:T=vo; e}, xs) ({V:T=xs' V; e'}, xs'(V := xs V))` show ?case ..
qed
lemma Sync_τred0r_xt:
"τred0r extTA P h (e, xs) (e', xs') ==> τred0r extTA P h (syncV (e) e2, xs) (syncV (e') e2, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl SynchronizedRed1)
lemma InSync_τred0r_xt:
"τred0r extTA P h (e, xs) (e', xs') ==> τred0r extTA P h (insyncV (a) e, xs) (insyncV (a) e', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl SynchronizedRed2)
lemma Seq_τred0r_xt:
"τred0r extTA P h (e, xs) (e', xs') ==> τred0r extTA P h (e;;e2, xs) (e';;e2, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl SeqRed)
lemma Cond_τred0r_xt:
"τred0r extTA P h (e, xs) (e', xs') ==> τred0r extTA P h (if (e) e1 else e2, xs) (if (e') e1 else e2, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl CondRed)
lemma Throw_τred0r_xt:
"τred0r extTA P h (e, xs) (e', xs') ==> τred0r extTA P h (throw e, xs) (throw e', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl ThrowRed)
lemma Try_τred0r_xt:
"τred0r extTA P h (e, xs) (e', xs') ==> τred0r extTA P h (try e catch(C V) e2, xs) (try e' catch(C V) e2, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl TryRed)
definition τRed0 :: "J_prog => heap => (expr × expr list) => (expr × expr list) => bool"
where "τRed0 P h ees e'es' = (P \<turnstile>0 ⟨fst ees/snd ees, h⟩ -ε-> ⟨fst e'es'/snd e'es', h⟩ ∧ τMove0 P h ees)"
lemma τRed0_conv [iff]:
"τRed0 P h (e, es) (e', es') = (P \<turnstile>0 ⟨e/es, h⟩ -ε-> ⟨e'/es', h⟩ ∧ τMove0 P h (e, es))"
by(simp add: τRed0_def)
lemma τred0r_lcl_incr:
"τred0r extTA P h (e, xs) (e', xs') ==> dom xs ⊆ dom xs'"
by(induct rule: rtranclp_induct2)(auto dest: red_lcl_incr del: subsetI)
lemma τred0t_lcl_incr:
"τred0t extTA P h (e, xs) (e', xs') ==> dom xs ⊆ dom xs'"
by(rule τred0r_lcl_incr)(rule tranclp_into_rtranclp)
lemma τred0r_dom_lcl:
assumes wwf: "wwf_J_prog P"
shows "τred0r extTA P h (e, xs) (e', xs') ==> dom xs' ⊆ dom xs ∪ fv e"
apply(induct rule: converse_rtranclp_induct2)
apply blast
apply(clarsimp del: subsetI)
apply(frule red_dom_lcl)
apply(drule red_fv_subset[OF wwf])
apply auto
done
lemma τred0t_dom_lcl:
assumes wwf: "wwf_J_prog P"
shows "τred0t extTA P h (e, xs) (e', xs') ==> dom xs' ⊆ dom xs ∪ fv e"
by(rule τred0r_dom_lcl[OF wwf])(rule tranclp_into_rtranclp)
lemma τred0r_fv_subset:
assumes wwf: "wwf_J_prog P"
shows "τred0r extTA P h (e, xs) (e', xs') ==> fv e' ⊆ fv e"
by(induct rule: converse_rtranclp_induct2)(auto dest: red_fv_subset[OF wwf])
lemma τred0t_fv_subset:
assumes wwf: "wwf_J_prog P"
shows "τred0t extTA P h (e, xs) (e', xs') ==> fv e' ⊆ fv e"
by(rule τred0r_fv_subset[OF wwf])(rule tranclp_into_rtranclp)
abbreviation τRed0r :: "J_prog => heap => (expr × expr list) => (expr × expr list) => bool"
where "τRed0r P h ≡ (τRed0 P h)^**"
abbreviation τRed0t :: "J_prog => heap => (expr × expr list) => (expr × expr list) => bool"
where "τRed0t P h ≡ (τRed0 P h)^++"
lemma fixes e :: "('a, 'b) exp" and es :: "('a, 'b) exp list"
shows τmove0_not_call: "[| τmove0 P h e; call e = ⌊aMvs⌋ |] ==> ¬ synthesized_call P h aMvs"
and τmoves0_not_calls: "[| τmoves0 P h es; calls es = ⌊aMvs⌋ |] ==> ¬ synthesized_call P h aMvs"
apply(induct e and es)
apply(auto simp add: is_vals_conv append_eq_map_conv map_eq_append_conv split: split_if_asm)
apply(auto simp add: synthesized_call_def)
done
lemma fixes e :: "('a, 'b) exp" and es :: "('a, 'b) exp list"
shows τmove0_callD: "call e = ⌊aMvs⌋ ==> τmove0 P h e <-> ¬ synthesized_call P h aMvs"
and τmoves0_callsD: "calls es = ⌊aMvs⌋ ==> τmoves0 P h es <-> ¬ synthesized_call P h aMvs"
apply(induct e and es)
apply(auto split: split_if_asm simp add: is_vals_conv)
apply(auto simp add: synthesized_call_def map_eq_append_conv)
done
lemma τred0_into_τRed0:
assumes red: "τred0 (extTA2J0 P) P h (e, empty) (e', xs')"
shows "τRed0 P h (e, es) (e', es)"
proof -
from red have red: "extTA2J0 P,P \<turnstile> ⟨e, (h, empty)⟩ -ε-> ⟨e', (h, xs')⟩" and "τmove0 P h e" and "no_call P h e" by auto
hence "P \<turnstile>0 ⟨e/es,h⟩ -ε-> ⟨e'/es,h⟩"
by-(erule red0Red,auto simp add: no_call_def)
thus ?thesis using `τmove0 P h e` by(auto)
qed
lemma τred0r_into_τRed0r:
assumes wwf: "wwf_J_prog P"
shows
"[| τred0r (extTA2J0 P) P h (e, empty) (e'', empty); fv e = {} |]
==> τRed0r P h (e, es) (e'', es)"
proof(induct e xs≡"empty :: locals" rule: converse_rtranclp_induct2)
case refl show ?case by blast
next
case (step e xs e' xs')
from `τred0 (extTA2J0 P) P h (e, xs) (e', xs')`
have red: "extTA2J0 P,P \<turnstile> ⟨e, (h, xs)⟩ -ε-> ⟨e', (h, xs')⟩" and "τmove0 P h e" and "no_call P h e" by auto
from wwf red have "fv e' ⊆ fv e" by(rule red_fv_subset)
with `fv e = {}` have "fv e' = {}" by blast
moreover from red_dom_lcl[OF red] `fv e = {}` `xs = empty`
have "dom xs' = {}" by(auto split:split_if_asm)
hence "xs' = empty" by(auto)
ultimately have "τRed0r P h (e', es) (e'', es)" by(rule step)
moreover from red `τmove0 P h e` `xs' = empty` `xs = empty` `no_call P h e`
have "τRed0 P h (e, es) (e', es)" by(auto simp add: no_call_def intro!: red0Red)
ultimately show ?case by(blast intro: converse_rtranclp_into_rtranclp)
qed
lemma τred0t_into_τRed0t:
assumes wwf: "wwf_J_prog P"
shows
"[| τred0t (extTA2J0 P) P h (e, empty) (e'', empty); fv e = {} |]
==> τRed0t P h (e, es) (e'', es)"
proof(induct e xs≡"empty :: locals" rule: converse_tranclp_induct2)
case (base e xs)
thus ?case by(blast intro!: tranclp.r_into_trancl τred0_into_τRed0)
next
case (step e xs e' xs')
from `τred0 (extTA2J0 P) P h (e, xs) (e', xs')`
have red: "extTA2J0 P,P \<turnstile> ⟨e, (h, xs)⟩ -ε-> ⟨e', (h, xs')⟩" and "τmove0 P h e" and "no_call P h e" by auto
from wwf red have "fv e' ⊆ fv e" by(rule red_fv_subset)
with `fv e = {}` have "fv e' = {}" by blast
moreover from red_dom_lcl[OF red] `fv e = {}` `xs = empty`
have "dom xs' = {}" by(auto split:split_if_asm)
hence "xs' = empty" by auto
ultimately have "τRed0t P h (e', es) (e'', es)" by(rule step)
moreover from red `τmove0 P h e` `xs' = empty` `xs = empty` `no_call P h e`
have "τRed0 P h (e, es) (e', es)" by(auto simp add: no_call_def intro!: red0Red)
ultimately show ?case by(blast intro: tranclp_into_tranclp2)
qed
abbreviation τMOVE :: "'m prog => ((expr × locals) × heap, J_thread_action) trsys"
where "τMOVE ≡ λP ((e, x), h) ta s'. τmove0 P h e ∧ ta = ε"
abbreviation τMOVE0 :: "'m prog => ((expr × expr list) × heap, J0_thread_action) trsys"
where "τMOVE0 ≡ λP (es, h) ta s. τMove0 P h es ∧ ta = ε"
abbreviation final_expr0 :: "expr × expr list => bool" where
"final_expr0 ≡ λ(e, es). final e ∧ es = []"
lemma red0_mthr: "multithreaded (mred0 P)"
apply(unfold_locales)
apply(auto elim!: red0.cases)
by(auto dest: red_new_thread_heap)
interpretation red0_mthr: multithreaded final_expr0 "mred0 P" for P
by(rule red0_mthr)
interpretation red_τmthr: τmultithreaded final_expr "mred P" "τMOVE P" for P
by(unfold_locales)
interpretation red0_τmthr: τmultithreaded final_expr0 "mred0 P" "τMOVE0 P" for P
.
lemma red0_final_thread_wf: "final_thread_wf final_expr0 (mred0 P)"
by(unfold_locales)(auto elim!: red0.cases)
interpretation red0_mthr: final_thread_wf final_expr0 "mred0 P" for P
by(rule red0_final_thread_wf)
lemma red_τmthr_wf: "τmultithreaded_wf final_expr (mred P) (τMOVE P) wfs"
proof
fix x1 m1 ta1 x1' m1'
assume "mred P (x1, m1) ta1 (x1', m1')" "τMOVE P (x1, m1) ta1 (x1', m1')"
thus "m1 = m1'" by(auto dest: τmove0_heap_unchanged simp add: split_def)
qed(simp add: split_beta)
interpretation red_τmthr_wf: τmultithreaded_wf final_expr "mred P" "τMOVE P" wfs for P wfs
by(rule red_τmthr_wf)
lemma red0_τmthr_wf: "τmultithreaded_wf final_expr0 (mred0 P) (τMOVE0 P) wfs"
proof
fix x1 m1 ta1 x1' m1'
assume "mred0 P (x1, m1) ta1 (x1', m1')" "τMOVE0 P (x1, m1) ta1 (x1', m1')"
thus "m1 = m1'" by(cases x1)(fastsimp elim!: red0.cases dest: τmove0_heap_unchanged)
qed(simp add: split_beta)
interpretation red0_τmthr_wf: τmultithreaded_wf final_expr0 "mred0 P" "τMOVE0 P" wfs for P wfs
by(rule red0_τmthr_wf)
end